val read_header_body_short
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (cid_len: U32.t{U32.v cid_len <= 20})
      (spin: LPB.bitfield LPB.uint8 1)
      (protected_bits: LPB.bitfield LPB.uint8 5)
    : Tot (read_header_body_t sl cid_len (| Short, (| (), (spin, (protected_bits, ())) |) |))
let read_header_body_short
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (cid_len: U32.t { U32.v cid_len <= 20 } )
  (spin: LPB.bitfield LPB.uint8 1)
  (protected_bits: LPB.bitfield LPB.uint8 5)
: Tot (read_header_body_t sl cid_len (| Short, (| (), (spin, (protected_bits, () ) ) |) |) )
= fun len ->
    let h0 = HST.get () in
    assert_norm (LPB.bitsum'_key_of_t first_byte (| Short, (| (), (spin, (protected_bits, ()) ) |) |) == (| Short, (| (), () |) |) );
    LP.valid_weaken (LP.strong_parser_kind 0 20 None) (LP.parse_flbytes (U32.v cid_len)) h0 sl 1ul;
    LP.valid_flbytes_elim h0 (U32.v cid_len) sl 1ul;
    let pos = LP.jump_flbytes (U32.v cid_len) cid_len sl 1ul in
    let dcid = B.sub sl.LP.base 1ul (pos `U32.sub` 1ul) in
    PShort (Secret.hide #Secret.U8 protected_bits) (spin = 1uy) dcid cid_len
val read_header_body_short
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (cid_len: U32.t{U32.v cid_len <= 20})
      (spin: LPB.bitfield LPB.uint8 1)
      (protected_bits: LPB.bitfield LPB.uint8 5)
    : Tot (read_header_body_t sl cid_len (| Short, (| (), (spin, (protected_bits, ())) |) |))
let read_header_body_short
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (cid_len: U32.t{U32.v cid_len <= 20})
      (spin: LPB.bitfield LPB.uint8 1)
      (protected_bits: LPB.bitfield LPB.uint8 5)
    : Tot (read_header_body_t sl cid_len (| Short, (| (), (spin, (protected_bits, ())) |) |)) =
fun len ->
  let h0 = HST.get () in
  assert_norm (LPB.bitsum'_key_of_t first_byte (| Short, (| (), (spin, (protected_bits, ())) |) |) ==
      (| Short, (| (), () |) |));
  LP.valid_weaken (LP.strong_parser_kind 0 20 None) (LP.parse_flbytes (U32.v cid_len)) h0 sl 1ul;
  LP.valid_flbytes_elim h0 (U32.v cid_len) sl 1ul;
  let pos = LP.jump_flbytes (U32.v cid_len) cid_len sl 1ul in
  let dcid = B.sub sl.LP.base 1ul (pos `U32.sub` 1ul) in
  PShort (Secret.hide #Secret.U8 protected_bits) (spin = 1uy) dcid cid_len
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.Slice.slice LowStar.Buffer.trivial_preorder LowParse.Bytes.byte FStar.UInt32.t Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowParse.BitFields.bitfield FStar.UInt8.t LowParse.BitFields.uint8 Prims.unit QUIC.Impl.Header.Public.PShort QUIC.Secret.Int.hide Lib.IntTypes.U8 Lib.IntTypes.PUB Prims.op_Equality FStar.UInt8.__uint_to_t QUIC.Impl.Header.Public.header LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.sub LowParse.Slice.__proj__Mkslice__item__base FStar.UInt32.__uint_to_t FStar.Ghost.hide FStar.UInt32.sub LowParse.Low.Bytes.jump_flbytes LowParse.Low.Bytes.valid_flbytes_elim LowParse.Low.Base.valid_weaken LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some LowParse.Spec.Base.total_constant_size_parser_kind FStar.Bytes.lbytes LowParse.Spec.Bytes.parse_flbytes FStar.Pervasives.assert_norm Prims.eq2 Prims.dtuple2 LowParse.Spec.Enum.enum_key QUIC.Spec.Header.Public.header_form_t QUIC.Spec.Header.Public.header_form LowParse.Spec.BitSum.bitsum'_key_type Prims.op_Subtraction LowParse.Spec.BitSum.BitSum' QUIC.Spec.Header.Public.fixed_bit LowParse.Spec.BitSum.BitField LowParse.Spec.BitSum.BitStop LowParse.Spec.BitSum.bitsum' QUIC.Spec.Header.Public.long_packet_type_t QUIC.Spec.Header.Public.long_packet_type LowParse.Spec.BitSum.bitsum'_key_of_t QUIC.Spec.Header.Public.first_byte Prims.Mkdtuple2 LowParse.Spec.BitSum.bitsum'_type' QUIC.Spec.Header.Public.Short FStar.Pervasives.Native.Mktuple2 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get QUIC.Impl.Header.Public.read_header_body_t
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)
=
  (LPB.mk_filter_bitsum'_t' first_byte)

[@@ (LT.postprocess_with pp_bitsum_norm_tac) ]
inline_for_extraction
noextract
let mk_validate_header_body_cases
: LPB.validate_bitsum_cases_t first_byte
=
  (LPB.mk_validate_bitsum_cases_t' first_byte)

let validate_header
  (short_dcid_len: short_dcid_len_t)
: Tot (LP.validator (parse_header short_dcid_len))
= LPB.validate_bitsum
    first_byte
    (first_byte_of_header short_dcid_len)
    (header_body_type short_dcid_len)
    (header_synth short_dcid_len)
    (LP.validate_u8 ())
    LP.read_u8
    (filter_first_byte)
    (parse_header_body short_dcid_len)
    (validate_header_body_cases short_dcid_len)
    (mk_validate_header_body_cases)

[@@ (LT.postprocess_with pp_bitsum_norm_tac) ]
inline_for_extraction
noextract
let destr_first_byte
: (LPB.destr_bitsum'_t first_byte)
=
  (LPB.mk_destr_bitsum'_t first_byte)


(* Length computations need to be transparent because the precondition
to QUIC.Impl.encrypt requires the user to provide a destination buffer
large enough to contain the byte representation of the header *)

let read_header_body_post
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (cid_len: U32.t { U32.v cid_len <= 20 } )
  (tg: LPB.bitsum'_type first_byte)
  (h: HS.mem)
  (x: header)
  (h' : HS.mem)
: GTot Type0
= LP.valid (parse_header cid_len) h sl 0ul /\ (
    let hd = LP.contents (parse_header cid_len) h sl 0ul in
    let len = LP.get_valid_pos (parse_header cid_len) h sl 0ul in
    header_live x h' /\
    LP.loc_slice_from_to sl 0ul len `B.loc_includes` header_footprint x /\
    g_header x h' == hd
    )

inline_for_extraction
noextract
let read_header_body_t
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (cid_len: U32.t { U32.v cid_len <= 20 } )
  (tg: LPB.bitsum'_type first_byte)
: Tot (Type u#0)
= unit ->
  HST.Stack header
  (requires (fun h ->
    let p = dsnd (parse_header_body cid_len (LPB.bitsum'_key_of_t first_byte tg)) in
    LP.valid (parse_header cid_len) h sl 0ul /\ (
    let len = LP.get_valid_pos (parse_header cid_len) h sl 0ul in
    1 <= U32.v sl.LP.len /\
    LP.valid_pos p h sl 1ul len /\
    LP.contents (parse_header cid_len) h sl 0ul == (header_synth cid_len).LPB.f tg (LP.contents p h sl 1ul)
  )))
  (ensures (fun h x h' ->
    B.modifies B.loc_none h h' /\
    read_header_body_post sl cid_len tg h x h'
  ))

#push-options "--z3rlimit 128 --z3cliopt smt.arith.nl=false --using_facts_from '*,-FStar.Int.Cast' --query_stats --max_fuel 9 --initial_fuel 9 --max_ifuel 9 --initial_ifuel 9 --query_stats"

#restart-solver

let read_header_body_short
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (cid_len: U32.t { U32.v cid_len <= 20 } )
  (spin: LPB.bitfield LPB.uint8 1)
  (protected_bits: LPB.bitfield LPB.uint8 5)
val read_header_body_short
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (cid_len: U32.t{U32.v cid_len <= 20})
      (spin: LPB.bitfield LPB.uint8 1)
      (protected_bits: LPB.bitfield LPB.uint8 5)
    : Tot (read_header_body_t sl cid_len (| Short, (| (), (spin, (protected_bits, ())) |) |))

    sl:
      LowParse.Slice.slice (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte)
        (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte) ->
    cid_len: FStar.UInt32.t{FStar.UInt32.v cid_len <= 20} ->
    spin: LowParse.BitFields.bitfield LowParse.BitFields.uint8 1 ->
    protected_bits: LowParse.BitFields.bitfield LowParse.BitFields.uint8 5
  -> QUIC.Impl.Header.Public.read_header_body_t sl
      cid_len
      (|
        QUIC.Spec.Header.Public.Short,
        (| (), FStar.Pervasives.Native.Mktuple2 spin (protected_bits, ()) |)
      |)