val block_len (a: SCipher.cipher_alg) : x: U32.t{U32.v x = SCipher.block_length a}
val block_len (a: SCipher.cipher_alg) : x: U32.t{U32.v x = SCipher.block_length a}
let block_len (a: SCipher.cipher_alg):
  x:U32.t { U32.v x = SCipher.block_length a }
=
  let open SCipher in
  match a with | CHACHA20 -> 64ul | _ -> 16ul
module QUIC.Impl.Header
friend QUIC.Spec.Header

open QUIC.Impl.Header.Base

module Parse = QUIC.Spec.Header.Parse
module ParseImpl = QUIC.Impl.Header.Parse
module Spec = QUIC.Spec.Header
module PN = QUIC.Spec.PacketNumber.Base

module B = LowStar.Buffer

module Cipher = EverCrypt.Cipher
module AEAD = EverCrypt.AEAD
module HKDF = EverCrypt.HKDF

module U8 = FStar.UInt8
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module G = FStar.Ghost
module Seq = QUIC.Secret.Seq
module Secret = QUIC.Secret.Int
module SecretBuffer = QUIC.Secret.Buffer

module Lemmas = QUIC.Impl.Lemmas
module BF = LowParse.BitFields

module SCipher = Spec.Agile.Cipher
module SAEAD = Spec.Agile.AEAD

(* There are a few places where EverCrypt needs public data whereas it
could/should be secret. Thus, we may need some declassification
locally using Lib.RawIntTypes, but we definitely don't want to make
secret integers globally transparent using friend *)

module ADMITDeclassify = Lib.RawIntTypes
/
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.Lemmas.fsti.checked QUIC.Impl.Header.Parse.fsti.checked QUIC.Impl.Header.Base.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.AEAD.fsti.checked
QUIC.Impl.Header.fst
a: Spec.Agile.Cipher.cipher_alg
  -> x: FStar.UInt32.t{FStar.UInt32.v x = Spec.Agile.Cipher.block_length a}
Spec.Agile.Cipher.cipher_alg FStar.UInt32.__uint_to_t FStar.UInt32.t Prims.b2t Prims.op_Equality Prims.int FStar.UInt32.v Spec.Agile.Cipher.block_length
let block_len (a: SCipher.cipher_alg) : x: U32.t{U32.v x = SCipher.block_length a} =
  
let open SCipher in
match a with
| CHACHA20 -> 64ul
| _ -> 16ul