val filter_first_byte:(LPB.filter_bitsum'_t first_byte)
let filter_first_byte
: (LPB.filter_bitsum'_t first_byte)
=
  (LPB.mk_filter_bitsum'_t' first_byte)
val filter_first_byte:(LPB.filter_bitsum'_t first_byte)
let filter_first_byte:(LPB.filter_bitsum'_t first_byte) =
(LPB.mk_filter_bitsum'_t' first_byte)
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.Spec.BitSum.filter_bitsum'_bitsum'_intro FStar.UInt8.t LowParse.BitFields.uint8 QUIC.Spec.Header.Public.header_form_t Prims.Cons FStar.Pervasives.Native.tuple2 LowParse.BitFields.bitfield FStar.Pervasives.Native.Mktuple2 QUIC.Spec.Header.Public.Long FStar.UInt8.__uint_to_t QUIC.Spec.Header.Public.Short Prims.Nil LowParse.Spec.Enum.enum_key LowParse.Spec.BitSum.BitSum' Prims.unit QUIC.Spec.Header.Public.fixed_bit LowParse.Spec.BitSum.BitField LowParse.Spec.BitSum.BitStop LowParse.Spec.BitSum.bitsum' Prims.op_Subtraction QUIC.Spec.Header.Public.long_packet_type_t QUIC.Spec.Header.Public.long_packet_type LowParse.Spec.BitSum.filter_bitsum'_bitsum'_cons QUIC.Spec.Header.Public.Initial QUIC.Spec.Header.Public.ZeroRTT QUIC.Spec.Header.Public.Handshake QUIC.Spec.Header.Public.Retry LowParse.Spec.BitSum.filter_bitsum'_bitfield LowParse.Spec.BitSum.filter_bitsum'_bitstop FStar.List.Tot.Base.append LowParse.Spec.BitSum.filter_bitsum'_bitsum'_nil
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
let validate_long_retry_body : LP.validator parse_long_retry_body =
  validate_common_long `LP.validate_nondep_then` LP.validate_bounded_vlbytes 0 20

inline_for_extraction
let validate_long_initial_body : LP.validator parse_long_initial_body =
  validate_common_long `LP.validate_nondep_then` (LP.validate_bounded_vlgenbytes 0 0ul token_max_len (U32.uint_to_t token_max_len) (VI.validate_bounded_varint 0ul (U32.uint_to_t token_max_len)) (VI.read_bounded_varint 0 token_max_len) `LP.validate_nondep_then` validate_payload_and_pn_length)

module LPB = LowParse.Low.BitSum

#push-options "--z3rlimit 32 --max_fuel 8 --max_ifuel 8 --initial_fuel 8 --initial_ifuel 8"

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let validate_header_body_cases
  (short_dcid_len: short_dcid_len_t)
  (k' : LPB.bitsum'_key_type first_byte)
: Tot (LP.validator (dsnd (parse_header_body short_dcid_len k')))
= match LP.coerce (LPB.bitsum'_key_type first_byte) k' with
  | (| Short, (| (), () |) |) ->
    LP.validate_weaken (LP.strong_parser_kind 0 20 None) (LP.validate_flbytes (U32.v short_dcid_len) (FStar.Int.Cast.uint32_to_uint64 short_dcid_len)) ()
  | (| Long, (| (), (| Initial, () |) |) |) ->
    validate_long_initial_body
  | (| Long, (| (), (| ZeroRTT, () |) |) |) ->
    validate_long_zero_rtt_body
  | (| Long, (| (), (| Handshake, () |) |) |) ->
    validate_long_handshake_body
  | (| Long, (| (), (| Retry, () |) |) |) ->
    validate_long_retry_body


(* TODO: move to something like LowParse.Spec.Tac.BitSum *)
module LT = LowParse.TacLib
noextract
let pp_bitsum_norm_tac () : LT.Tac unit =
  LT.norm [primops; iota; zeta; delta_attr [`%LPB.filter_bitsum'_t_attr]];
  LT.trefl ()

[@@ (LT.postprocess_with pp_bitsum_norm_tac) ]
inline_for_extraction
noextract
let filter_first_byte
: (LPB.filter_bitsum'_t first_byte)
val filter_first_byte:(LPB.filter_bitsum'_t first_byte)
LowParse.Spec.BitSum.filter_bitsum'_t QUIC.Spec.Header.Public.first_byte