val is_stlhae : i: MiTLS.TLSInfo.id -> Prims.bool
let is_stlhae (i:id) =
  if ID12? i && AEAD? (aeAlg_of_id i) then
    let is_aes128 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES128_GCM in
    let is_aes256 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES256_GCM in
    is_aes128 || is_aes256
  else
    false
(**
Authenticated encryptions of streams of TLS fragments (from Content)
multiplexing StatefulLHAE and StreamAE with (some) length hiding
(for now, under-specifying ciphertexts lengths and values)
*)
module MiTLS.StAE
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically


open FStar.HyperStack
open FStar.Bytes

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


module HS   = FStar.HyperStack

module MS   = FStar.Monotonic.Seq
module C    = MiTLS.Content

module Stream = MiTLS.StreamAE
module StLHAE = MiTLS.StatefulLHAE
module Range = MiTLS.Range
#set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"

////////////////////////////////////////////////////////////////////////////////
//Distinguishing the two multiplexing choices of StAE based on the ids
////////////////////////////////////////////////////////////////////////////////
let is_stream i = ID13? i
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StreamPlain.fst.checked MiTLS.StreamAE.fst.checked MiTLS.StatefulPlain.fst.checked MiTLS.StatefulLHAE.fst.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.LHAEPlain.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Content.fst.checked MiTLS.AEADProvider.fsti.checked MiTLS.AEAD_GCM.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.StAE.fst
i: MiTLS.TLSInfo.id -> Prims.bool
MiTLS.TLSInfo.id Prims.op_AmpAmp MiTLS.TLSInfo.uu___is_ID12 MiTLS.CipherSuite.uu___is_AEAD MiTLS.TLSInfo.aeAlg_of_id Prims.op_BarBar Prims.bool Prims.op_Equality MiTLS.EverCrypt.aead_alg MiTLS.CipherSuite.__proj__AEAD__item___0 MiTLS.EverCrypt.AES256_GCM MiTLS.EverCrypt.AES128_GCM
let is_stlhae (i: id) =
  
if ID12? i && AEAD? (aeAlg_of_id i)
then
  let is_aes128 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES128_GCM in
  let is_aes256 = AEAD?._0 (aeAlg_of_id i) = EverCrypt.AES256_GCM in
  is_aes128 || is_aes256
else false