val pn_epoch : e: MiTLS.Old.Epochs.epoch hs_rgn n
  -> FStar.Pervasives.Native.option FStar.Bytes.bytes *
    FStar.Pervasives.Native.option FStar.Bytes.bytes
let pn_epoch (#hs_rgn:rgn) (#n:random) (e:epoch hs_rgn n) =
  let Epoch _ _ _ pn = e in pn
(**
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)) = ()
let print s = discard (IO.debug_print_string ("EPO| "^s^"\n"))
unfold let trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_Epochs then print else (fun _ -> ())


type epoch_region_inv (#i:id) (hs_rgn:rgn) (r:reader (peerId i)) (w:writer i) =
  disjoint hs_rgn (region w) /\
  parent (region w) <> HS.root /\
  parent (region r) <> HS.root /\
  // grandparent of each writer is a sibling of the handshake
  parent hs_rgn = parent (parent (region w))  /\
  disjoint (region w) (region r) /\
  // they are all colored as epoch regions
  is_epoch_rgn (region w) /\
  is_epoch_rgn (region r) /\
  is_epoch_rgn (parent (region w)) /\
  is_epoch_rgn (parent (region r)) /\
  //except for the hs_rgn, of course
  is_hs_rgn hs_rgn

val epoch_region_inv'
  (#i:id)
  (hs_rgn:rgn)
  (r:reader (peerId i))
  (w:writer i) : Type0

noeq type epoch (hs_rgn:rgn) (n:random) =
  | Epoch: #i:id{nonce_of_id i = n} ->
      h :Negotiation.handshake ->
      r: reader (peerId i) ->
      w: writer i {epoch_region_inv' hs_rgn r w} ->
      pn: option bytes * option bytes ->
      epoch hs_rgn n

// we would extend/adapt it for TLS 1.3,
// e.g. to notify 0RTT/forwad-privacy transitions
// for now epoch completion is a total function on handshake --- should be stateful

let epoch_id #r #n (e:epoch r n) : StAE.stae_id = Epoch?.i e

let reveal_epoch_region_inv_all (u:unit)
  : Lemma (forall i hs_rgn r w.{:pattern (epoch_region_inv' #i hs_rgn r w)}
       epoch_region_inv' #i hs_rgn r w   <==>
       epoch_region_inv #i hs_rgn r w)
=
  ()

let reveal_epoch_region_inv (#hs_rgn:rgn) (#n:random) (e:epoch hs_rgn n)
  : Lemma (let r = Epoch?.r e in
       let w = Epoch?.w e in
       epoch_region_inv hs_rgn r w)
=
  ()

let writer_epoch (#hs_rgn:rgn) (#n:random) (e:epoch hs_rgn n)
  : Tot (w:writer (e.i) {epoch_region_inv hs_rgn (Epoch?.r e) w})
=
  Epoch?.w e

let reader_epoch (#hs_rgn:rgn) (#n:random) (e:epoch hs_rgn n)
  : Tot (r:reader (peerId e.i) {epoch_region_inv hs_rgn r (Epoch?.w e)})
=
  Epoch?.r e
/
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
e: MiTLS.Old.Epochs.epoch hs_rgn n
  -> FStar.Pervasives.Native.option FStar.Bytes.bytes *
    FStar.Pervasives.Native.option FStar.Bytes.bytes
MiTLS.Mem.rgn MiTLS.Old.Epochs.random MiTLS.Old.Epochs.epoch MiTLS.TLSInfo.id Prims.b2t Prims.op_Equality MiTLS.TLSInfo.random MiTLS.TLSInfo.nonce_of_id MiTLS.Negotiation.handshake MiTLS.StAE.reader MiTLS.TLSInfo.peerId MiTLS.StAE.writer MiTLS.Old.Epochs.epoch_region_inv' FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Bytes.bytes
let pn_epoch (#hs_rgn: rgn) (#n: random) (e: epoch hs_rgn n) =
  
let Epoch _ _ _ pn = e in
pn