val aadmax : FStar.UInt32.t
let aadmax =
  assert_norm (2000 <= pow2 32 - 1);
  2000ul
(**
  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)) }
/
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
FStar.UInt32.t
FStar.UInt32.__uint_to_t Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2
let aadmax =
  
assert_norm (2000 <= pow2 32 - 1);
2000ul