val validate_payload_and_pn_length:LP.validator parse_payload_and_pn_length
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)
val validate_payload_and_pn_length:LP.validator parse_payload_and_pn_length
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)
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_filter QUIC.Spec.VarInt.parse_varint_kind QUIC.UInt62.t QUIC.Spec.VarInt.parse_varint QUIC.Impl.VarInt.validate_varint QUIC.Impl.VarInt.read_varint QUIC.Spec.Header.Public.payload_and_pn_length_prop Prims.bool Prims.eq2
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
val validate_payload_and_pn_length:LP.validator parse_payload_and_pn_length
LowParse.Low.Base.validator QUIC.Spec.Header.Public.parse_payload_and_pn_length