val empty_hs_transcript:erased_transcript
val empty_hs_transcript:erased_transcript
let empty_hs_transcript : erased_transcript = hide_log []
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
/
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
MiTLS.HandshakeLog.erased_transcript
MiTLS.HandshakeLog.hide_log Prims.Nil MiTLS.HandshakeLog.msg
let empty_hs_transcript:erased_transcript =
  
hide_log []