val validate_long_retry_body:LP.validator parse_long_retry_body
let validate_long_retry_body : LP.validator parse_long_retry_body =
  validate_common_long `LP.validate_nondep_then` LP.validate_bounded_vlbytes 0 20
val validate_long_retry_body:LP.validator parse_long_retry_body
let validate_long_retry_body:LP.validator parse_long_retry_body =
validate_common_long `LP.validate_nondep_then` (LP.validate_bounded_vlbytes 0 20)
QUIC.Impl.Header.Public.fst.checked
QUIC.Spec.Header.Public.fst.checked QUIC.Spec.Header.Public.fst.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.VarInt.fsti.checked QUIC.Impl.Base.fst.checked prims.fst.checked LowParse.TacLib.fst.checked LowParse.Low.Writers.Instances.fst.checked LowParse.Low.BitSum.fst.checked LowParse.Low.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked
QUIC.Impl.Header.Public.fst
LowParse.Low.Combinators.validate_nondep_then LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Int.parse_u32_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_kind LowParse.Spec.BoundedInt.log256' LowParse.Spec.Bytes.parse_all_bytes_kind QUIC.Spec.Header.Public.common_long_t QUIC.Spec.Header.Public.parse_common_long QUIC.Impl.Header.Public.validate_common_long LowParse.Spec.Bytes.parse_bounded_vlbytes_t LowParse.Spec.Bytes.parse_bounded_vlbytes LowParse.Low.Bytes.validate_bounded_vlbytes
module QUIC.Impl.Header.Public
open QUIC.Spec.Header.Public
open QUIC.Impl.Base

friend QUIC.Spec.Header.Public

module LP = LowParse.Low

inline_for_extraction
let validate_common_long : LP.validator parse_common_long =
  LP.validate_u32 () `LP.validate_nondep_then` (LP.validate_bounded_vlbytes 0 20 `LP.validate_nondep_then` LP.validate_bounded_vlbytes 0 20)

module VI = QUIC.Impl.VarInt

inline_for_extraction
let validate_payload_and_pn_length : LP.validator parse_payload_and_pn_length =
  LP.validate_filter
    VI.validate_varint
    VI.read_varint
    payload_and_pn_length_prop
    (fun x -> payload_and_pn_length_prop x)

inline_for_extraction
let validate_long_zero_rtt_body : LP.validator parse_long_zero_rtt_body =
  validate_common_long `LP.validate_nondep_then` validate_payload_and_pn_length

inline_for_extraction
let validate_long_handshake_body : LP.validator parse_long_handshake_body =
  validate_common_long `LP.validate_nondep_then` validate_payload_and_pn_length

inline_for_extraction
val validate_long_retry_body:LP.validator parse_long_retry_body
LowParse.Low.Base.validator QUIC.Spec.Header.Public.parse_long_retry_body