val trace (s: string) : ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1))
val trace (s: string) : ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1))
let trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_Epochs then print else (fun _ -> ())
(**
This modules implements the mutable state for the successive StAE epochs which is used by TLS.
Its separation from Handshake and coding is somewhat arbitrary.
An elaboration would ensure that keys in old epochs are erased.
(i.e. we only keep old epoch AE logs for specifying authentication)
*)
module MiTLS.Old.Epochs
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically

open FStar.Heap
open FStar.Seq // DO NOT move further below, it would shadow `FStar.HyperStack.mem`
open FStar.HyperStack
open FStar.Monotonic.Seq
open FStar.Error
open FStar.Bytes

open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
module Range = MiTLS.Range
open MiTLS.Range
open MiTLS.StAE
//open Negotiation
open MiTLS.Mem

module ST = FStar.HyperStack.ST 
module HS = FStar.HyperStack
module MS = FStar.Monotonic.Seq
module Secret = MiTLS.Old.KeySchedule

#set-options "--admit_smt_queries true"

type random = TLSInfo.random

(* debug printing *)
let discard (_:bool) : ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) = ()
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StAE.fst.checked MiTLS.Range.fst.checked MiTLS.Old.KeySchedule.fsti.checked MiTLS.Negotiation.fst.checked MiTLS.Mem.fst.checked MiTLS.DebugFlags.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Old.Epochs.fsti
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.DebugFlags.debug_Epochs MiTLS.Old.Epochs.print Prims.bool Prims.string Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Prims.eq2
let trace: s: string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) =
  
if DebugFlags.debug_Epochs then print else (fun _ -> ())