val contains_addr : rid: FStar.Monotonic.HyperHeap.rid -> a: MiTLS.AEAD.address -> m: FStar.Monotonic.HyperStack.mem
  -> Prims.logical
let contains_addr (rid:rid) (a:address) (m:mem) =
  ~(addr_unused_in rid a m)
(**
  This interfaces provides an abstraction for the verified Hacl* Crypto.AEAD.Main module,
  using FStar.Bytes rather than buffers.
*)
module MiTLS.AEAD
open MiTLS
module HS = FStar.HyperStack //Added automatically

module I = MiTLS.Crypto.Indexing
module U32 = FStar.UInt32
module U128 = FStar.UInt128
module Plain = MiTLS.Crypto.Plain

open FStar.Bytes
open FStar.UInt32
open MiTLS.Mem
open MiTLS.Pkg

let ivlen (alg:I.cipherAlg) = 12ul

let taglen = 16ul

let iv (alg:I.cipherAlg) =
  let open FStar.Mul in
  n:U128.t { U128.v n < pow2 (8 * v (ivlen alg)) }

let aadmax =
  assert_norm (2000 <= pow2 32 - 1);
  2000ul // arbitrary; enough for TLS

type aadlen_32 = l:U32.t {l <=^ aadmax}

val keylen   : I.id -> U32.t

val statelen : I.id -> U32.t

type cipher (i:I.id) (l:nat{l + v taglen < pow2 32}) = lbytes (l + (UInt32.v taglen))

type cipher32 (i:I.id) (l:U32.t{UInt.size (v l + 16) 32}) = lbytes32 (l +^ taglen)

inline_for_extraction
val entry : i:I.id -> Type0

let nonce (i:I.id) = iv (I.cipherAlg_of_id i)

type adata = b:bytes{length b <= v aadmax}

type plainLen = l:Plain.plainLen{l + v taglen < pow2 32}

val mk_entry (#i:I.id) :
    nonce:nonce i ->
    ad:adata ->
    #l:plainLen ->
    p:Plain.plain i l ->
    c:cipher i (Seq.length (Plain.as_bytes p)) ->
    entry i

val entry_injective (#i:I.id)
                    (n:nonce i) (n':nonce i)
                    (ad:adata) (ad':adata)
                    (#l:plainLen) (#l':plainLen)
                    (p:Plain.plain i l) (p':Plain.plain i l')
                      (c:cipher i (Seq.length (Plain.as_bytes p))) (c':cipher i (Seq.length (Plain.as_bytes p')))
  : Lemma (let e  = mk_entry n ad p c in
           let e' = mk_entry n' ad' p' c' in
           (e == e' <==> (n == n' /\ ad == ad' /\ l == l' /\ p == p' /\ c == c')))

val nonce_of_entry (#i:_) (e:entry i) : nonce i

let safeMac (i:I.id) = Flag.safeHS i && Flag.mac1 i

let safeId  (i:I.id) = Flag.safeId i

val aead_state: I.id -> I.rw -> Type0

val log_region: #i:_ -> #rw:_ -> aead_state i rw -> subrgn tls_tables_region

val prf_region: i:I.id -> subrgn tls_tables_region

val log: #i:_ -> #rw:_ -> s:aead_state i rw{safeMac i} -> mem -> GTot (Seq.seq (entry i))

let address = nat

let addr_unused_in (rid:rid) (a:address) (m0:mem) =
  Monotonic.Heap.addr_unused_in a (Map.sel (HS.get_hmap m0) rid)
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Flag.fst.checked MiTLS.Crypto.Plain.fsti.checked MiTLS.Crypto.Indexing.fst.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.Heap.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.AEAD.fsti
rid: FStar.Monotonic.HyperHeap.rid -> a: MiTLS.AEAD.address -> m: FStar.Monotonic.HyperStack.mem
  -> Prims.logical
FStar.Monotonic.HyperHeap.rid MiTLS.AEAD.address FStar.Monotonic.HyperStack.mem Prims.l_not MiTLS.AEAD.addr_unused_in Prims.logical
let contains_addr (rid: rid) (a: address) (m: mem) =
  
~(addr_unused_in rid a m)