val incr_epoch_ctr :
  #a:Type0 ->
  #p:(seq a -> Type0) ->
  #r:rgn ->
  #is:MS.i_seq r a p ->
  ctr:epoch_ctr r is ->
  ST unit
    (requires fun h -> 1 + sel h ctr < Seq.length (i_sel h is))
    (ensures (fun h0 _ h1 ->
      let ctr_as_hsref =  ctr in
      modifies_one r h0 h1 /\
      HS.modifies_ref r (Set.singleton (Heap.addr_of (as_ref ctr_as_hsref))) ( h0) ( h1) /\
      sel h1 ctr = sel h0 ctr + 1))
val incr_epoch_ctr :
  #a:Type0 ->
  #p:(seq a -> Type0) ->
  #r:rgn ->
  #is:MS.i_seq r a p ->
  ctr:epoch_ctr r is ->
  ST unit
    (requires fun h -> 1 + sel h ctr < Seq.length (i_sel h is))
    (ensures (fun h0 _ h1 ->
      let ctr_as_hsref =  ctr in
      modifies_one r h0 h1 /\
      HS.modifies_ref r (Set.singleton (Heap.addr_of (as_ref ctr_as_hsref))) ( h0) ( h1) /\
      sel h1 ctr = sel h0 ctr + 1))
let incr_epoch_ctr #a #p #r #is ctr =
  HST.recall ctr;
  let cur = HST.op_Bang ctr in
  MS.int_at_most_is_stable is (cur + 1);
  HST.mr_witness is (int_at_most (cur + 1) is);
  HST.op_Colon_Equals ctr (cur + 1)
(**
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

let epochs_inv' (#r:rgn) (#n:random) (es: seq (epoch r n)) = epochs_inv es

let reveal_epochs_inv' (u:unit)
  : Lemma (forall (r:rgn) (#n:random) (es:seq (epoch r n)). {:pattern (epochs_inv' es)}
         epochs_inv' es
         <==>
         epochs_inv es)
  = ()

#reset-options "--using_facts_from FStar --using_facts_from Prims --using_facts_from Epochs --using_facts_from Parse --admit_smt_queries true"

let alloc_log_and_ctrs #a #p r =
  let init = Seq.empty in
  let is = alloc_mref_iseq p r init in
  HST.mr_witness is (int_at_most (-1) is);
  let c1 : epoch_ctr #a #p r is = HST.ralloc r (-1) in
  let c2 : epoch_ctr #a #p r is = HST.ralloc r (-1) in
  (| is, c1, c2 |)

// #reset-options
/
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
ctr: MiTLS.Old.Epochs.epoch_ctr r is -> FStar.HyperStack.ST.ST Prims.unit
FStar.Seq.Base.seq MiTLS.Mem.rgn FStar.Monotonic.Seq.i_seq MiTLS.Old.Epochs.epoch_ctr FStar.HyperStack.ST.op_Colon_Equals MiTLS.Old.Epochs.epoch_ctr_inv FStar.Monotonic.Seq.increases Prims.op_Addition Prims.unit FStar.HyperStack.ST.mr_witness FStar.Monotonic.Seq.grows_p FStar.Monotonic.Seq.int_at_most FStar.Monotonic.Seq.int_at_most_is_stable FStar.HyperStack.ST.op_Bang FStar.HyperStack.ST.recall
let incr_epoch_ctr #a #p #r #is ctr =
  
HST.recall ctr;
let cur = HST.op_Bang ctr in
MS.int_at_most_is_stable is (cur + 1);
HST.mr_witness is (int_at_most (cur + 1) is);
HST.op_Colon_Equals ctr (cur + 1)