val header_len_bound : Prims.int
let header_len_bound = 16500
module QUIC.Spec.Base

module FB = FStar.Bytes
module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module S = FStar.Seq
module Secret = QUIC.Secret.Int

type byte = FStar.UInt8.t
type bytes = S.seq byte
type lbytes (n:nat) = b:bytes{S.length b = n}

inline_for_extraction
noextract
let bitfield
  (sz: nat { sz <= 8 })
: Tot eqtype
= (x: U8.t { U8.v x < pow2 sz })

inline_for_extraction
noextract
let secret_bitfield
  (sz: nat { sz <= 8 })
: Tot Type0
= (x: Secret.uint8 { Secret.v x < pow2 sz })

type payload_and_pn_length_t = (payload_and_pn_length: U62.t { U64.v payload_and_pn_length >= 20 })
/
QUIC.UInt62.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
QUIC.Spec.Base.fst
Prims.int
let header_len_bound =
  
16500