val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))
val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))
let gen p i = AEAD_GCM.gen p i
(**
Stateful, agile, length-hiding authenticated encryption with additional data
Implemented by appending a fragment sequence number to the additional data of
the underlying LHAE scheme
*)
module MiTLS.StatefulLHAE
open MiTLS

module HS = FStar.HyperStack //Added automatically
module HST = FStar.HyperStack.ST //Added automatically

open FStar.Seq
open FStar.Monotonic.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.AEAD_GCM
open MiTLS.StatefulPlain

module Range = MiTLS.Range

#set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"

// TODO: TEMPORARY, until we add back LHAE
type id = AEAD_GCM.id

let alg (i:id) = AEAD_GCM.alg i

type cipher (i:id) = StatefulPlain.cipher i

(* decrypted plaintexts, within a range computed from the cipher length *)
type dplain (i:id) (ad:adata i) (c:cipher i) =
  StatefulPlain.plain i ad (Range.cipherRangeClass i (length c))

type state (i:id) (rw:rw) =
  AEAD_GCM.state i rw

let region #i #rw s = AEAD_GCM.State?.region #i #rw s

noextract
let log_region #i #rw s = AEAD_GCM.State?.log_region #i #rw s

let log #i #rw s = AEAD_GCM.State?.log #i #rw s

let counter #i #rw s = AEAD_GCM.State?.counter #i #rw s

type reader i = state i Reader
type writer i = state i Writer

val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StatefulPlain.fst.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.LHAEPlain.fst.checked MiTLS.AEADProvider.fsti.checked MiTLS.AEAD_GCM.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.StatefulLHAE.fst
parent: MiTLS.Mem.rgn -> i: MiTLS.StatefulLHAE.id
  -> FStar.HyperStack.ST.ST (MiTLS.StatefulLHAE.writer i)
MiTLS.Mem.rgn MiTLS.StatefulLHAE.id MiTLS.AEAD_GCM.gen MiTLS.AEAD_GCM.writer MiTLS.StatefulLHAE.writer
let gen p i =
  
AEAD_GCM.gen p i