val genPost : parent: FStar.Monotonic.HyperHeap.rid ->
    h0: FStar.Monotonic.HyperStack.mem ->
    w: MiTLS.StreamAE.writer i ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.logical
let genPost (#i:id) parent h0 (w:writer i) h1 =
  modifies_none h0 h1 /\
  HS.parent w.region = parent /\
  HS.fresh_region w.region h0 h1 /\
  color w.region = color parent /\
//  extends (AEAD.region w.aead) parent /\
//  HS.fresh_region (AEAD.region w.aead) h0 h1 /\
//  color (AEAD.region w.aead) = color parent /\
  (authId i ==>
      (h1 `HS.contains` (ilog w.log) /\
       sel h1 (ilog w.log) == Seq.empty)) /\
  h1 `HS.contains` (ctr w.counter) /\
  sel h1 (ctr w.counter) == 0
(**
Provides authenticated encryption for a stream of variable-length plaintexts;
concretely, we use AES_GCM but any other AEAD algorithm would do.
*)
module MiTLS.StreamAE
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically

open FStar.HyperStack
open FStar.Seq
open FStar.Monotonic.Seq
open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.StreamPlain

module AEAD = MiTLS.AEADProvider
module HS = FStar.HyperStack

type rid = HST.erid

type id = i:id { ID13? i }

let alg (i:id) =
  let AEAD ae _ = aeAlg_of_id i in ae

let ltag i : nat = UInt32.v (EverCrypt.aead_tagLen (alg i))
let cipherLen i (l:plainLen) : nat = l + ltag i
type cipher i (l:plainLen) = lbytes (cipherLen i l)

// will require proving before decryption
let lenCipher i (c:bytes { ltag i <= length c }) : nat = length c - ltag i

type entry (i:id) =
  | Entry: l:plainLen -> c:cipher i l -> p:plain i l -> entry i

// key materials (from the AEAD provider)
type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i
 
let ideal_log (r:erid) (i:id) = log_t r (entry i)

let log_ref (r:erid) (i:id) : Tot Type0 =
  if authId i then ideal_log r i else unit

noextract
let ilog (#r:erid) (#i:id) (l:log_ref r i{authId i}) : Tot (ideal_log r i) =
  l

irreducible let max_ctr: n:nat{n = 18446744073709551615} =
  assert_norm (pow2 64 - 1 = 18446744073709551615);
  pow2 64 - 1

type counter = c:nat{c <= max_ctr}

let ideal_ctr (#l:erid) (r: erid) (i:id) (log:ideal_log l i) : Tot Type0 =
  FStar.Monotonic.Seq.seqn r log max_ctr
  // An increasing counter, at most min(length log, 2^64-1)

let concrete_ctr (r:erid) (i:id) : Tot Type0 =
  m_rref r counter increases

let ctr_ref (#l:erid) (r:erid) (i:id) (log:log_ref l i) : Tot Type0 =
  if authId i
  then ideal_ctr r i (log <: ideal_log l i)
  else m_rref r counter increases

let ctr (#l:erid) (#r:erid) (#i:id) (#log:log_ref l i) (c:ctr_ref r i log)
  : Tot (m_rref r (if authId i
		   then seqn_val #l #(entry i) r log max_ctr
		   else counter)
		increases) =
  c

// kept concrete for log and counter, but the key and iv should be private.
noeq type state (i:id) (rw:rw) =
  | State: #region: rgn
         -> #log_region: rgn{if rw = Writer then region = log_region else HS.disjoint region log_region}
         -> aead: AEAD.state i rw
         -> log: log_ref log_region i // ghost, subject to cryptographic assumption
         -> counter: ctr_ref region i log // types are sufficient to anti-alias log and counter
         -> state i rw

// Some invariants:
// - the writer counter is the length of the log; the reader counter is lower or equal
// - gen is called at most once for each (i:id), generating distinct refs for each (i:id)
// - the log is monotonic

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

#set-options "--admit_smt_queries true"
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StreamPlain.fst.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.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.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.StreamAE.fst

    parent: FStar.Monotonic.HyperHeap.rid ->
    h0: FStar.Monotonic.HyperStack.mem ->
    w: MiTLS.StreamAE.writer i ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.logical
MiTLS.StreamAE.id FStar.Monotonic.HyperHeap.rid FStar.Monotonic.HyperStack.mem MiTLS.StreamAE.writer Prims.l_and FStar.HyperStack.ST.modifies_none Prims.b2t Prims.op_Equality FStar.Monotonic.HyperHeap.parent MiTLS.StreamAE.__proj__State__item__region MiTLS.TLSConstants.Writer FStar.Monotonic.HyperStack.fresh_region Prims.int FStar.Monotonic.HyperHeap.color Prims.l_imp MiTLS.TLSInfo.authId FStar.Monotonic.HyperStack.contains FStar.Seq.Base.seq MiTLS.StreamAE.entry FStar.Monotonic.Seq.grows MiTLS.StreamAE.ilog MiTLS.StreamAE.__proj__State__item__log_region MiTLS.StreamAE.__proj__State__item__log Prims.eq2 FStar.Monotonic.HyperStack.sel FStar.Seq.Base.empty FStar.Monotonic.Seq.seqn_val MiTLS.StreamAE.max_ctr Prims.bool MiTLS.StreamAE.counter FStar.Monotonic.Seq.increases MiTLS.StreamAE.ctr MiTLS.StreamAE.__proj__State__item__counter Prims.logical
let genPost (#i: id) parent h0 (w: writer i) h1 =
  
modifies_none h0 h1 /\ HS.parent w.region = parent /\ HS.fresh_region w.region h0 h1 /\
color w.region = color parent /\
(authId i ==> (h1 `HS.contains` (ilog w.log) /\ sel h1 (ilog w.log) == Seq.empty)) /\
h1 `HS.contains` (ctr w.counter) /\ sel h1 (ctr w.counter) == 0