val add_epoch :
  #r:rgn -> #n:random -> es:epochs r n -> e:epoch r n ->
  ST unit
    (requires fun h -> let is = MkEpochs?.es es in epochs_inv #r #n (Seq.snoc (i_sel h is) e))
    (ensures fun h0 x h1 ->
        let es = MkEpochs?.es es in
        let es_as_hsref =  es in
        modifies_one r h0 h1 /\ HS.modifies_ref r (Set.singleton (HS.as_addr es_as_hsref)) ( h0) ( h1) /\
        i_sel h1 es == Seq.snoc (i_sel h0 es) e)
val add_epoch :
  #r:rgn -> #n:random -> es:epochs r n -> e:epoch r n ->
  ST unit
    (requires fun h -> let is = MkEpochs?.es es in epochs_inv #r #n (Seq.snoc (i_sel h is) e))
    (ensures fun h0 x h1 ->
        let es = MkEpochs?.es es in
        let es_as_hsref =  es in
        modifies_one r h0 h1 /\ HS.modifies_ref r (Set.singleton (HS.as_addr es_as_hsref)) ( h0) ( h1) /\
        i_sel h1 es == Seq.snoc (i_sel h0 es) e)
let add_epoch #r #n (MkEpochs es _ _ _) e = MS.i_write_at_end es e
(**
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

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)

let create (r:rgn) (n:random) =
  let (| esref, c1, c2 |) = alloc_log_and_ctrs #(epoch r n) #(epochs_inv #r #n) r in
  let xkr = alloc_mref_iseq (fun s -> Seq.length s <= 2) r Seq.empty in
  assume False; //17-06-30 TODO restore framing with extra field
  MkEpochs esref c1 c2 xkr
/
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: MiTLS.Old.Epochs.epochs r n -> e: MiTLS.Old.Epochs.epoch r n
  -> FStar.HyperStack.ST.ST Prims.unit
MiTLS.Mem.rgn MiTLS.TLSInfo.random MiTLS.Old.Epochs.epochs MiTLS.Old.Epochs.epoch FStar.Monotonic.Seq.i_seq MiTLS.Old.Epochs.epochs_inv MiTLS.Old.Epochs.epoch_ctr MiTLS.Old.KeySchedule.exportKey FStar.Seq.Base.seq Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Monotonic.Seq.i_write_at_end Prims.unit
let add_epoch #r #n (MkEpochs es _ _ _) e =
  
MS.i_write_at_end es e