val alg : i: MiTLS.AEAD_GCM.id -> MiTLS.CipherSuite.aeadAlg
let alg (i:id) = let AEAD ae _ = aeAlg_of_id i in ae
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'"
/
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
i: MiTLS.AEAD_GCM.id -> MiTLS.CipherSuite.aeadAlg
MiTLS.AEAD_GCM.id MiTLS.CipherSuite.aeadAlg MiTLS.CipherSuite.hash_alg MiTLS.CipherSuite.aeAlg MiTLS.TLSInfo.aeAlg_of_id
let alg (i: id) =
  
let AEAD ae _ = aeAlg_of_id i in
ae