val epochs_inv' (#r:rgn) (#n:random) (es: seq (epoch r n)) : Type0
val epochs_inv' (#r:rgn) (#n:random) (es: seq (epoch r n)) : Type0
let epochs_inv' (#r:rgn) (#n:random) (es: seq (epoch r n)) = epochs_inv es
(**
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"

let epoch_region_inv'
  (#i:id)
  (hs_rgn:rgn)
  (r:reader (peerId i))
  (w:writer i)
= epoch_region_inv hs_rgn r w
/
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.Mem.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.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.fst
es: FStar.Seq.Base.seq (MiTLS.Old.Epochs.epoch r n) -> Type0
MiTLS.Mem.rgn MiTLS.TLSInfo.random FStar.Seq.Base.seq MiTLS.Old.Epochs.epoch MiTLS.Old.Epochs.epochs_inv
let epochs_inv' (#r: rgn) (#n: random) (es: seq (epoch r n)) =
  
epochs_inv es