val key_len (a: ea) : x: U8.t{U8.v x = Spec.Agile.AEAD.key_length a}
let key_len (a: ea): x:U8.t { U8.v x = Spec.Agile.AEAD.key_length a } =
  let open Spec.Agile.AEAD in
  match a with
  | AES128_GCM -> 16uy
  | AES256_GCM -> 32uy
  | CHACHA20_POLY1305 -> 32uy
val key_len (a: ea) : x: U8.t{U8.v x = Spec.Agile.AEAD.key_length a}
let key_len (a: ea) : x: U8.t{U8.v x = Spec.Agile.AEAD.key_length a} =
let open Spec.Agile.AEAD in
match a with
| AES128_GCM -> 16uy
| AES256_GCM -> 32uy
| CHACHA20_POLY1305 -> 32uy
QUIC.State.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked QUIC.Impl.fsti.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.CTR.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.State.fst
QUIC.Spec.Crypto.ea FStar.UInt8.__uint_to_t FStar.UInt8.t Prims.b2t Prims.op_Equality Prims.int Prims.l_or FStar.UInt.size FStar.UInt8.n FStar.Integers.op_Greater_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.UInt8.v Spec.Agile.AEAD.key_length
module QUIC.State

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF
module CTR = EverCrypt.CTR
module IB = LowStar.ImmutableBuffer
module U32 = FStar.UInt32

module Seq = QUIC.Secret.Seq
module SecretBuffer = QUIC.Secret.Buffer

module SHKDF = Spec.Agile.HKDF
module SHD = Spec.Hash.Definitions

open LowStar.BufferOps (* for the !* notation *)

module Spec = QUIC.Spec
module Impl = QUIC.Impl
module Lemmas = QUIC.Impl.Lemmas


/// Helpers
/// -------
val key_len (a: ea) : x: U8.t{U8.v x = Spec.Agile.AEAD.key_length a}
a: QUIC.Spec.Crypto.ea -> x: FStar.UInt8.t{FStar.UInt8.v x = Spec.Agile.AEAD.key_length a}