val max_ctr (a: aeadAlg) : Tot (n: nat{n = 18446744073709551615})
val max_ctr (a: aeadAlg) : Tot (n: nat{n = 18446744073709551615})
let max_ctr (a:aeadAlg) : Tot (n:nat{n = 18446744073709551615}) =
  assert_norm (pow2 64 - 1 = 18446744073709551615);
  pow2 64 - 1
module MiTLS.AEAD_GCM
open MiTLS
// AEAD-GCM mode for the TLS record layer, as specified in RFC 5288.
// We support both AES_128_GCM and AES_256_GCM, differing only in their key sizes

open FStar.Heap
open FStar.HyperStack
open FStar.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.LHAEPlain

module Range = MiTLS.Range
open MiTLS.Range

open FStar.Monotonic.Seq

module Range = MiTLS.Range
module AEAD = MiTLS.AEADProvider
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

type id = i:id{ ID12? i /\ AEAD? (aeAlg_of_id i) }
let alg (i:id) = let AEAD ae _ = aeAlg_of_id i in ae

type cipher (i:id) = c:bytes{ valid_clen i (length c) }

type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i
/
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.EverCrypt.fsti.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.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.AEAD_GCM.fst
a: MiTLS.CipherSuite.aeadAlg -> n: Prims.nat{n = 18446744073709551615}
MiTLS.CipherSuite.aeadAlg Prims.op_Subtraction Prims.pow2 Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality Prims.int Prims.nat
let max_ctr (a: aeadAlg) : Tot (n: nat{n = 18446744073709551615}) =
  
assert_norm (pow2 64 - 1 = 18446744073709551615);
pow2 64 - 1