val alg : i: MiTLS.StreamAE.id -> MiTLS.CipherSuite.aeadAlg
let alg (i:id) =
  let AEAD ae _ = aeAlg_of_id i in ae
(**
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 }
/
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
i: MiTLS.StreamAE.id -> MiTLS.CipherSuite.aeadAlg
MiTLS.StreamAE.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