val valid_long_initial_body_elim
      (h0: HS.mem)
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (pos: U32.t)
    : Lemma (requires (LP.valid parse_long_initial_body h0 sl pos))
      (ensures
        (LP.valid parse_long_initial_body h0 sl pos /\
          LP.valid_content_pos (parse_common_long
              `LP.nondep_then`
              ((LP.parse_bounded_vlgenbytes 0
                    token_max_len
                    (VI.parse_bounded_varint 0 token_max_len))
                `LP.nondep_then`
                parse_payload_and_pn_length))
            h0
            sl
            pos
            (LP.contents parse_long_initial_body h0 sl pos)
            (LP.get_valid_pos parse_long_initial_body h0 sl pos)))
let valid_long_initial_body_elim
  (h0: HS.mem)
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (pos: U32.t)
: Lemma
  (requires (LP.valid parse_long_initial_body h0 sl pos))
  (ensures (
    LP.valid parse_long_initial_body h0 sl pos /\
    LP.valid_content_pos
      (parse_common_long `LP.nondep_then` (LP.parse_bounded_vlgenbytes 0 token_max_len (VI.parse_bounded_varint 0 token_max_len) `LP.nondep_then` parse_payload_and_pn_length))
      h0
      sl
      pos
      (LP.contents parse_long_initial_body h0 sl pos)
      (LP.get_valid_pos parse_long_initial_body h0 sl pos)
  ))
= LP.valid_facts parse_long_initial_body h0 sl pos;
  LP.valid_facts
    (parse_common_long `LP.nondep_then` (LP.parse_bounded_vlgenbytes 0 token_max_len (VI.parse_bounded_varint 0 token_max_len) `LP.nondep_then` parse_payload_and_pn_length))
    h0 sl pos
val valid_long_initial_body_elim
      (h0: HS.mem)
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (pos: U32.t)
    : Lemma (requires (LP.valid parse_long_initial_body h0 sl pos))
      (ensures
        (LP.valid parse_long_initial_body h0 sl pos /\
          LP.valid_content_pos (parse_common_long
              `LP.nondep_then`
              ((LP.parse_bounded_vlgenbytes 0
                    token_max_len
                    (VI.parse_bounded_varint 0 token_max_len))
                `LP.nondep_then`
                parse_payload_and_pn_length))
            h0
            sl
            pos
            (LP.contents parse_long_initial_body h0 sl pos)
            (LP.get_valid_pos parse_long_initial_body h0 sl pos)))
let valid_long_initial_body_elim
      (h0: HS.mem)
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (pos: U32.t)
    : Lemma (requires (LP.valid parse_long_initial_body h0 sl pos))
      (ensures
        (LP.valid parse_long_initial_body h0 sl pos /\
          LP.valid_content_pos (parse_common_long
              `LP.nondep_then`
              ((LP.parse_bounded_vlgenbytes 0
                    token_max_len
                    (VI.parse_bounded_varint 0 token_max_len))
                `LP.nondep_then`
                parse_payload_and_pn_length))
            h0
            sl
            pos
            (LP.contents parse_long_initial_body h0 sl pos)
            (LP.get_valid_pos parse_long_initial_body h0 sl pos))) =
LP.valid_facts parse_long_initial_body h0 sl pos;
LP.valid_facts (parse_common_long
    `LP.nondep_then`
    ((LP.parse_bounded_vlgenbytes 0 token_max_len (VI.parse_bounded_varint 0 token_max_len))
      `LP.nondep_then`
      parse_payload_and_pn_length))
  h0
  sl
  pos
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
FStar.Monotonic.HyperStack.mem LowParse.Slice.slice LowStar.Buffer.trivial_preorder LowParse.Bytes.byte FStar.UInt32.t LowParse.Low.Base.Spec.valid_facts 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 LowParse.Spec.VLGen.parse_bounded_vlgen_kind QUIC.Spec.VarInt.parse_varint_kind QUIC.Spec.Base.token_max_len LowParse.Spec.Combinators.parse_filter_kind FStar.Pervasives.Native.tuple2 QUIC.Spec.Header.Public.common_long_t LowParse.Spec.Bytes.parse_bounded_vlbytes_t QUIC.Spec.Header.Public.payload_and_pn_length_t' LowParse.Spec.Combinators.nondep_then QUIC.Spec.Header.Public.parse_common_long LowParse.Spec.Bytes.parse_bounded_vlgenbytes QUIC.Spec.VarInt.parse_bounded_varint QUIC.Spec.Header.Public.parse_payload_and_pn_length Prims.unit QUIC.Spec.Header.Public.long_initial_body_t QUIC.Spec.Header.Public.parse_long_initial_body LowParse.Low.Base.Spec.valid Prims.squash Prims.l_and LowParse.Low.Base.Spec.valid_content_pos LowParse.Low.Base.Spec.contents LowParse.Low.Base.Spec.get_valid_pos Prims.Nil FStar.Pervasives.pattern
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)
: 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

#pop-options

#push-options "--z3rlimit 256 --z3cliopt smt.arith.nl=false --query_stats --max_fuel 9 --initial_fuel 9 --max_ifuel 9 --initial_ifuel 9 --query_stats"

#restart-solver

let read_header_body_long_retry
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (cid_len: U32.t { U32.v cid_len <= 20 } )
  (protected_bits: LPB.bitfield LPB.uint8 4)
: Tot (read_header_body_t sl cid_len (| Long, (| (), (| Retry, (protected_bits, ()) |) |) |) )
= fun len ->
    let h0 = HST.get () in
    assert_norm (LPB.bitsum'_key_of_t first_byte (| Long, (| (), (| Retry, (protected_bits, ()) |) |) |)  == (| Long, (| (), (| Retry, () |) |) |) );
    LP.valid_nondep_then h0 parse_common_long (LP.parse_bounded_vlbytes 0 20) sl 1ul;
    LP.valid_nondep_then h0 LP.parse_u32 (LP.parse_bounded_vlbytes 0 20 `LP.nondep_then` LP.parse_bounded_vlbytes 0 20) sl 1ul;
    let version = LP.read_u32 sl 1ul in
    let pos1 = LP.jump_u32 sl 1ul in
    LP.valid_nondep_then h0 (LP.parse_bounded_vlbytes 0 20) (LP.parse_bounded_vlbytes 0 20) sl pos1;
    let dcid = LP.get_vlbytes_contents 0 20 sl pos1 in
    let dcid_len = LP.bounded_vlbytes_payload_length 0 20 sl pos1 in
    let pos2 = LP.jump_bounded_vlbytes 0 20 sl pos1 in
    let scid = LP.get_vlbytes_contents 0 20 sl pos2 in
    let scid_len = LP.bounded_vlbytes_payload_length 0 20 sl pos2 in
    let pos3 = LP.jump_bounded_vlbytes 0 20 sl pos2 in
    let odcid = LP.get_vlbytes_contents 0 20 sl pos3 in
    let odcid_len = LP.bounded_vlbytes_payload_length 0 20 sl pos3 in
    let spec = PRetry odcid odcid_len in
    (PLong (Secret.hide #Secret.U8 protected_bits) version dcid dcid_len scid scid_len spec)

#pop-options

let valid_long_initial_body_elim
  (h0: HS.mem)
  (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
  (pos: U32.t)
: Lemma
  (requires (LP.valid parse_long_initial_body h0 sl pos))
  (ensures (
    LP.valid parse_long_initial_body h0 sl pos /\
    LP.valid_content_pos
      (parse_common_long `LP.nondep_then` (LP.parse_bounded_vlgenbytes 0 token_max_len (VI.parse_bounded_varint 0 token_max_len) `LP.nondep_then` parse_payload_and_pn_length))
      h0
      sl
      pos
      (LP.contents parse_long_initial_body h0 sl pos)
      (LP.get_valid_pos parse_long_initial_body h0 sl pos)
val valid_long_initial_body_elim
      (h0: HS.mem)
      (sl: LP.slice (B.trivial_preorder _) (B.trivial_preorder _))
      (pos: U32.t)
    : Lemma (requires (LP.valid parse_long_initial_body h0 sl pos))
      (ensures
        (LP.valid parse_long_initial_body h0 sl pos /\
          LP.valid_content_pos (parse_common_long
              `LP.nondep_then`
              ((LP.parse_bounded_vlgenbytes 0
                    token_max_len
                    (VI.parse_bounded_varint 0 token_max_len))
                `LP.nondep_then`
                parse_payload_and_pn_length))
            h0
            sl
            pos
            (LP.contents parse_long_initial_body h0 sl pos)
            (LP.get_valid_pos parse_long_initial_body h0 sl pos)))

    h0: FStar.Monotonic.HyperStack.mem ->
    sl:
      LowParse.Slice.slice (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte)
        (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte) ->
    pos: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
      (requires
        LowParse.Low.Base.Spec.valid QUIC.Spec.Header.Public.parse_long_initial_body h0 sl pos)
      (ensures
        LowParse.Low.Base.Spec.valid QUIC.Spec.Header.Public.parse_long_initial_body h0 sl pos /\
        LowParse.Low.Base.Spec.valid_content_pos (LowParse.Spec.Combinators.nondep_then QUIC.Spec.Header.Public.parse_common_long
              (LowParse.Spec.Combinators.nondep_then (LowParse.Spec.Bytes.parse_bounded_vlgenbytes 0
                      QUIC.Spec.Base.token_max_len
                      (QUIC.Spec.VarInt.parse_bounded_varint 0 QUIC.Spec.Base.token_max_len))
                  QUIC.Spec.Header.Public.parse_payload_and_pn_length))
          h0
          sl
          pos
          (LowParse.Low.Base.Spec.contents QUIC.Spec.Header.Public.parse_long_initial_body h0 sl pos
          )
          (LowParse.Low.Base.Spec.get_valid_pos QUIC.Spec.Header.Public.parse_long_initial_body
              h0
              sl
              pos))