let token_max_len = 16383
let token_max_len =
16383
QUIC.Spec.Base.fst.checked
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
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 })

let header_len_bound = 16500 // FIXME: this should be in line with the parser kind

inline_for_extraction
let short_dcid_len_t = (short_dcid_len: U32.t { U32.v short_dcid_len <= 20 })

inline_for_extraction
val token_max_len : Prims.int
Prims.int