val tags_append_aux (a: alg) (prior ms0 ms1: list msg) (hs0 hs1: list anyTag)
    : Lemma (requires (tags a prior ms0 hs0 /\ tags a (prior @ ms0) ms1 hs1))
      (ensures (tags a prior (ms0 @ ms1) (hs0 @ hs1)))
      (decreases ms0)
val tags_append_aux (a: alg) (prior ms0 ms1: list msg) (hs0 hs1: list anyTag)
    : Lemma (requires (tags a prior ms0 hs0 /\ tags a (prior @ ms0) ms1 hs1))
      (ensures (tags a prior (ms0 @ ms1) (hs0 @ hs1)))
      (decreases ms0)
let rec tags_append_aux
  (a: alg)
  (prior ms0 ms1: list msg)
  (hs0 hs1: list anyTag)
: Lemma
  (requires (tags a prior ms0 hs0 /\ tags a (prior @ ms0) ms1 hs1))
  (ensures (tags a prior (ms0 @ ms1) (hs0 @ hs1)))
  (decreases ms0)
= match ms0 with
  | [] ->
    List.Tot.append_l_nil prior
  | m :: ms ->
    let prior_before = prior in
    let prior = prior @ [m] in
    let _ : squash (tags a (prior @ ms) ms1 hs1) =
      List.Tot.append_assoc prior_before [m] ms
    in
    if tagged m
    then
      let (_::hs) = hs0 in
      tags_append_aux a prior ms ms1 hs hs1
    else
      tags_append_aux a prior ms ms1 hs0 hs1
module MiTLS.HandshakeLog
open MiTLS

(* see als comments in Handshake.fsti *) 

open FStar.Seq
open FStar.Error

open MiTLS.Mem 
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.HandshakeMessages
open MiTLS.Hashing
open MiTLS.Hashing.CRF // now using incremental, collision-resistant, agile Hashing.
open FStar.Bytes //18-08-31 reordered 
open MiTLS.Range  // cwinter: the extracted OCaml file contains a reference to this, which is not reflected in the .depend file?
module Parse = MiTLS.Parse

module HS = FStar.HyperStack

(* A flag for runtime debugging of handshakelog data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false. *)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("HSL| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_HSL then print else (fun _ -> ())

// FIXME(ADL): the ghost transcript is buggy in the KaRaMeL-extracted version

let erased_transcript : Type0 =
    if false then hs_transcript
    else FStar.Ghost.erased hs_transcript

let reveal_log (l:erased_transcript) : GTot (hs_transcript) =
    if false then l
    else FStar.Ghost.reveal l

let hide_log (l:hs_transcript) : Tot erased_transcript =
    if false then l
    else FStar.Ghost.hide l

(** TODO: move to FStar.Ghost (breach of abstraction)  *)
let elift1_def (#a #b: Type) (f: (a -> GTot b)) (x: FStar.Ghost.erased a) : Lemma (FStar.Ghost.elift1 f x == FStar.Ghost.hide (f (FStar.Ghost.reveal x))) = ()

let ghost_bind
  (#a #b: Type)
  (x: erased a)
  (f: (
    (x': a) ->
    Pure (erased b)
    (requires (x' == FStar.Ghost.reveal x))
    (ensures (fun _ -> True))
  ))
: Tot (y: erased b { y == f (FStar.Ghost.reveal x) } )
= f (FStar.Ghost.reveal x)

inline_for_extraction
let bind_log
  (l: erased_transcript)
  (f: (
    (x: hs_transcript) ->
    Pure erased_transcript
    (requires (x == reveal_log l))
    (ensures (fun _ -> True))
  ))
: Tot (y: erased_transcript { y == f (reveal_log l) } )
= if false then f l
  else ghost_bind #hs_transcript #hs_transcript l f

let empty_hs_transcript : erased_transcript = hide_log []

let append_hs_transcript
    (l:erased_transcript)
    (ml:list msg { valid_transcript (reveal_log l @ ml) } )
    : Tot erased_transcript =
      bind_log l (fun l' -> hide_log (append_transcript l' ml))

let extend_hs_transcript (l:erased_transcript) (m:msg { valid_transcript (reveal_log l @ [m]) } ) : Tot erased_transcript =
    append_hs_transcript l [m]


private
let coerce (t2: Type) (#t1: Type) (x1: t1)
    : Pure t2 (requires (t1 == t2))
              (ensures (fun y -> y == x1))
    = x1

let print_hsl (hsl:erased_transcript) : Tot bool =
    if false then
    let hsl = coerce hs_transcript hsl in
        (* ^ otherwise, a `reveal` coercion will be inserted below and
         *   bump this function into GHOST. This only makes sense in an
         *   unsatisfiable context (which we are from the `if false`) since
         *   `erased_transcript` is an `erased _`, and cannot be a `list _`. *)
    let sl = List.Tot.map HandshakeMessages.string_of_handshakeMessage hsl in
    let s = List.Tot.fold_left (fun x y -> x^", "^y) "" sl in
    IO.debug_print_string ("Current log: " ^ s)
    else false

(* TODO: move to something like List.GTot *)
let rec gforall_list_to_list_refined
  (#a: Type)
  (f: (a -> GTot bool))
  (l: list a { gforall f l } )
: Tot (l': list (x: a {f x}))
= match l with
  | [] -> []
  | x :: q -> x :: gforall_list_to_list_refined f q

let rec valid_transcript_to_list_valid_hs_msg_aux
  (v: option protocolVersion)
  (l: list hs_msg { gforall (valid_hs_msg_prop v) l } )
: Tot (list (valid_hs_msg v))
=
(* FIXME: WHY WHY WHY can this not be defined as:
   gforall_list_to_list_refined (valid_hs_msg_prop v) l
*)
  match l with
  | [] -> []
  | a :: q -> a :: valid_transcript_to_list_valid_hs_msg_aux v q

let rec valid_transcript_to_list_valid_hs_msg_aux_inj
  (v: option protocolVersion)
  (l1: list hs_msg { gforall (valid_hs_msg_prop v) l1 } )
  (l2: list hs_msg { gforall (valid_hs_msg_prop v) l2 } )
: Lemma
  (requires (valid_transcript_to_list_valid_hs_msg_aux v l1 == valid_transcript_to_list_valid_hs_msg_aux v l2))
  (ensures (l1 == l2))
= match l1, l2 with
  | _ :: q1, _ :: q2 -> valid_transcript_to_list_valid_hs_msg_aux_inj v q1 q2
  | _ -> ()

let transcript_bytes l =
  let v = transcript_version l in
  handshakeMessagesBytes v (valid_transcript_to_list_valid_hs_msg_aux v l)

#set-options "--z3rlimit 64 --admit_smt_queries true"

let transcript_format_injective ms0 ms1 =
  let f ()
  : Lemma
    (requires (FStar.Bytes.equal (transcript_bytes ms0) (transcript_bytes ms1)))
    (ensures (ms0 == ms1))
  = match ms0 with
    | [] -> ()
    | ClientHello ch0 :: q0 ->
      let v = transcript_version ms0 in
      let (ClientHello ch1 :: q1) = ms1 in
      let v1 = transcript_version ms1 in
      let l0 = handshakeMessagesBytes v (valid_transcript_to_list_valid_hs_msg_aux v q0) in
      let l1 = handshakeMessagesBytes v1 (valid_transcript_to_list_valid_hs_msg_aux v1 q1) in
      clientHelloBytes_is_injective_strong ch0 l0 ch1 l1;
      begin match q0 with
      | [] -> ()
      | ServerHello sh0 :: q0' ->
        let (ServerHello sh1 :: q1') = q1 in
        serverHelloBytes_is_injective_strong sh0 (handshakeMessagesBytes v (valid_transcript_to_list_valid_hs_msg_aux v q0')) sh1 (handshakeMessagesBytes v1 (valid_transcript_to_list_valid_hs_msg_aux v1 q1'));
        handshakeMessagesBytes_is_injective v (valid_transcript_to_list_valid_hs_msg_aux v ms0) (valid_transcript_to_list_valid_hs_msg_aux v ms1);
        valid_transcript_to_list_valid_hs_msg_aux_inj v ms0 ms1
      end
  in
  Classical.move_requires f ()

//The type below includes buffers, the log, the hash, and the params needed to parse and hash the log.
//Note that a lot of this information is available in the log itself.
//In particular: pv+kex+hash_alg can be read from CH/SH, dh_group can be read from SKE
//TODO: decide whether to keep these parameters explicit or compute them from the log

#reset-options "--admit_smt_queries true"
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.CRF.fsti.checked MiTLS.Hashing.fsti.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.IO.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Error.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
MiTLS.HandshakeLog.fst

    a: MiTLS.Hashing.Spec.alg ->
    prior: Prims.list MiTLS.HandshakeLog.msg ->
    ms0: Prims.list MiTLS.HandshakeLog.msg ->
    ms1: Prims.list MiTLS.HandshakeLog.msg ->
    hs0: Prims.list MiTLS.Hashing.Spec.anyTag ->
    hs1: Prims.list MiTLS.Hashing.Spec.anyTag
  -> FStar.Pervasives.Lemma
      (requires
        MiTLS.HandshakeLog.tags a prior ms0 hs0 /\ MiTLS.HandshakeLog.tags a (prior @ ms0) ms1 hs1)
      (ensures MiTLS.HandshakeLog.tags a prior (ms0 @ ms1) (hs0 @ hs1))
      (decreases ms0)
MiTLS.Hashing.Spec.alg Prims.list MiTLS.HandshakeLog.msg MiTLS.Hashing.Spec.anyTag FStar.List.Tot.Properties.append_l_nil MiTLS.HandshakeLog.tagged MiTLS.HandshakeLog.tags_append_aux Prims.unit Prims.bool Prims.squash MiTLS.HandshakeLog.tags FStar.List.Tot.Base.append FStar.List.Tot.Properties.append_assoc Prims.Cons Prims.Nil Prims.l_and FStar.Pervasives.pattern
let rec tags_append_aux (a: alg) (prior ms0 ms1: list msg) (hs0 hs1: list anyTag)
    : Lemma (requires (tags a prior ms0 hs0 /\ tags a (prior @ ms0) ms1 hs1))
      (ensures (tags a prior (ms0 @ ms1) (hs0 @ hs1)))
      (decreases ms0) =
  
match ms0 with
| [] -> List.Tot.append_l_nil prior
| m :: ms ->
  let prior_before = prior in
  let prior = prior @ [m] in
  let _:squash (tags a (prior @ ms) ms1 hs1) = List.Tot.append_assoc prior_before [m] ms in
  if tagged m
  then
    let _ :: hs = hs0 in
    tags_append_aux a prior ms ms1 hs hs1
  else tags_append_aux a prior ms ms1 hs0 hs1