val encrypt: #i:id -> e:writer i -> ad:adata i
  -> r:Range.range{fst r = snd r /\ snd r <= max_TLSPlaintext_fragment_length}
  -> p:plain i ad r
  -> ST (cipher i)
     (requires (fun h0 ->
       HS.disjoint e.region (AEADProvider.log_region e.aead) /\
       sel h0 (ctr e.counter) < max_ctr (alg i)))
     (ensures  (fun h0 c h1 ->
       modifies (Set.as_set [e.log_region; AEADProvider.log_region e.aead]) h0 h1
       /\ h1 `HS.contains` (ctr e.counter)
       /\ sel h1 (ctr e.counter) == sel h0 (ctr e.counter) + 1
       /\ length c = Range.targetLength i r
       /\ (authId i ==>
	     (let log = ilog e.log in
	      let ilog = sel h0 log in
	      let seqn = sel h0 (ctr e.counter) in
        lemma_repr_bytes_values seqn;
	      let ad' = LHAEPlain.makeAD i seqn ad in
	      let ent = Entry c ad' p in
	      let n   = Seq.length ilog in
	      h1 `HS.contains` log
        /\ witnessed (at_least n ent log)
	      /\ sel h1 log == snoc ilog ent))))
val encrypt: #i:id -> e:writer i -> ad:adata i
  -> r:Range.range{fst r = snd r /\ snd r <= max_TLSPlaintext_fragment_length}
  -> p:plain i ad r
  -> ST (cipher i)
     (requires (fun h0 ->
       HS.disjoint e.region (AEADProvider.log_region e.aead) /\
       sel h0 (ctr e.counter) < max_ctr (alg i)))
     (ensures  (fun h0 c h1 ->
       modifies (Set.as_set [e.log_region; AEADProvider.log_region e.aead]) h0 h1
       /\ h1 `HS.contains` (ctr e.counter)
       /\ sel h1 (ctr e.counter) == sel h0 (ctr e.counter) + 1
       /\ length c = Range.targetLength i r
       /\ (authId i ==>
	     (let log = ilog e.log in
	      let ilog = sel h0 log in
	      let seqn = sel h0 (ctr e.counter) in
        lemma_repr_bytes_values seqn;
	      let ad' = LHAEPlain.makeAD i seqn ad in
	      let ent = Entry c ad' p in
	      let n   = Seq.length ilog in
	      h1 `HS.contains` log
        /\ witnessed (at_least n ent log)
	      /\ sel h1 log == snoc ilog ent))))
let encrypt #i e ad r p =
  let seqn = HST.op_Bang (ctr e.counter) in
  lemma_repr_bytes_values seqn;
  let ad' = LHAEPlain.makeAD i seqn ad in
  AEAD_GCM.encrypt #i e ad' r p
(**
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))
  (ensures  (genPost parent))
let gen p i = AEAD_GCM.gen p i

val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
  (requires (fun h0 ->
    HS.disjoint parent w.region /\
    HS.disjoint parent (AEADProvider.region w.aead)))
  (ensures  (fun h0 (r:reader i) h1 ->
    True //TODO
    ))
let genReader p #i w = AEAD_GCM.genReader p #i w

let coerce parent i kv iv = AEAD_GCM.coerce parent i kv iv
let leak (#i:id{~(authId i)}) (#role:rw) state = AEAD_GCM.leak #i #role state

(*------------------------------------------------------------------*)
#set-options "--z3rlimit 100 --max_ifuel 1 --initial_ifuel 0 --max_fuel 1 --initial_fuel 0"
val encrypt: #i:id -> e:writer i -> ad:adata i
  -> r:Range.range{fst r = snd r /\ snd r <= max_TLSPlaintext_fragment_length}
  -> p:plain i ad r
  -> ST (cipher i)
     (requires (fun h0 ->
       HS.disjoint e.region (AEADProvider.log_region e.aead) /\
       sel h0 (ctr e.counter) < max_ctr (alg i)))
     (ensures  (fun h0 c h1 ->
       modifies (Set.as_set [e.log_region; AEADProvider.log_region e.aead]) h0 h1
       /\ h1 `HS.contains` (ctr e.counter)
       /\ sel h1 (ctr e.counter) == sel h0 (ctr e.counter) + 1
       /\ length c = Range.targetLength i r
       /\ (authId i ==>
	     (let log = ilog e.log in
	      let ilog = sel h0 log in
	      let seqn = sel h0 (ctr e.counter) in
        lemma_repr_bytes_values seqn;
	      let ad' = LHAEPlain.makeAD i seqn ad in
	      let ent = Entry c ad' p in
	      let n   = Seq.length ilog in
	      h1 `HS.contains` log
        /\ witnessed (at_least n ent log)
	      /\ sel h1 log == snoc ilog ent))))
/
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

    e: MiTLS.StatefulLHAE.writer i ->
    ad: MiTLS.StatefulPlain.adata i ->
    r:
      MiTLS.Range.range
        { FStar.Pervasives.Native.fst r = FStar.Pervasives.Native.snd r /\
          FStar.Pervasives.Native.snd r <= MiTLS.TLSConstants.max_TLSPlaintext_fragment_length } ->
    p: MiTLS.StatefulPlain.plain i ad r
  -> FStar.HyperStack.ST.ST (MiTLS.StatefulLHAE.cipher i)
MiTLS.StatefulLHAE.id MiTLS.StatefulLHAE.writer MiTLS.StatefulPlain.adata MiTLS.Range.range Prims.l_and Prims.b2t Prims.op_Equality Prims.nat FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd Prims.op_LessThanOrEqual MiTLS.TLSConstants.max_TLSPlaintext_fragment_length MiTLS.StatefulPlain.plain MiTLS.AEAD_GCM.encrypt MiTLS.AEAD_GCM.cipher MiTLS.LHAEPlain.adata MiTLS.LHAEPlain.makeAD MiTLS.StatefulLHAE.cipher Prims.unit FStar.Bytes.lemma_repr_bytes_values MiTLS.TLSInfo.authId FStar.Monotonic.Seq.seqn_val MiTLS.AEAD_GCM.__proj__State__item__log_region MiTLS.TLSConstants.Writer MiTLS.AEAD_GCM.entry MiTLS.AEAD_GCM.__proj__State__item__region MiTLS.AEAD_GCM.__proj__State__item__log MiTLS.AEAD_GCM.max_ctr MiTLS.AEAD_GCM.alg Prims.bool MiTLS.AEAD_GCM.counter FStar.HyperStack.ST.op_Bang FStar.Monotonic.Seq.increases MiTLS.AEAD_GCM.ctr MiTLS.AEAD_GCM.__proj__State__item__counter
let encrypt #i e ad r p =
  
let seqn = HST.op_Bang (ctr e.counter) in
lemma_repr_bytes_values seqn;
let ad' = LHAEPlain.makeAD i seqn ad in
AEAD_GCM.encrypt #i e ad' r p