val payload_and_pn_length_prop (x: U62.t) : Tot bool
let payload_and_pn_length_prop
  (x: U62.t)
: Tot bool
= x `U64.gte` 20uL
val payload_and_pn_length_prop (x: U62.t) : Tot bool
let payload_and_pn_length_prop (x: U62.t) : Tot bool =
x `U64.gte` 20uL
QUIC.Spec.Header.Public.fst.checked
QUIC.Spec.VarInt.fsti.checked prims.fst.checked LowParse.Spec.Enum.fst.checked LowParse.Spec.BitSum.fst.checked LowParse.Spec.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
QUIC.Spec.Header.Public.fst
QUIC.UInt62.t FStar.UInt64.gte FStar.UInt64.__uint_to_t Prims.bool
module QUIC.Spec.Header.Public

module LP = LowParse.Spec
module LPB = LowParse.Spec.BitSum

inline_for_extraction
type header_form_t =
  | Long
  | Short

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let header_form : LP.enum header_form_t (LPB.bitfield LPB.uint8 1) = [
  Long, 1uy;
  Short, 0uy;
]

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let fixed_bit : LP.enum unit (LPB.bitfield LPB.uint8 1) = [
  (), 1uy;
]

inline_for_extraction
type long_packet_type_t =
  | Initial
  | ZeroRTT
  | Handshake
  | Retry

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let long_packet_type : LP.enum long_packet_type_t (LPB.bitfield LPB.uint8 2) = [
  Initial, 0uy;
  ZeroRTT, 1uy;
  Handshake, 2uy;
  Retry, 3uy;
]

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let first_byte : LPB.bitsum' LPB.uint8 8 =
  LPB.BitSum' _ _ header_form (function
    | Short ->
      LPB.BitSum' _ _ fixed_bit (fun _ ->
        LPB.BitField (* spin bit *) 1 (
          LPB.BitField (* protected bits *) 5 (
            LPB.BitStop ()
          )
        )
      )
    | Long ->
      LPB.BitSum' _ _ fixed_bit (fun _ ->
        LPB.BitSum' _ _ long_packet_type (function
          | _ -> LPB.BitField (* protected bits *) 4 (LPB.BitStop ())
        )
      )
  )

#push-options "--z3rlimit 16"

inline_for_extraction
noextract
let first_byte_of_header'
  (short_dcid_len: short_dcid_len_t)
  (t: Type0)
  (f: (LPB.bitsum'_type first_byte -> Tot t))
  (m: header' short_dcid_len)
: Tot t
= match m with
  | PShort protected_bits spin dcid ->
    let spin : LPB.bitfield LPB.uint8 1 = if spin then 1uy else 0uy in
    f (| Short, (| (), (spin, (protected_bits, () ) ) |) |)
  | PLong protected_bits version dcid scid spec ->
    begin match spec with
    | PInitial _ payload_and_pn_length ->
      f (| Long, (| (), (| Initial, (protected_bits, () ) |) |) |)
    | PZeroRTT payload_and_pn_length ->
      f (| Long, (| (), (| ZeroRTT, (protected_bits, () ) |) |) |)
    | PHandshake payload_and_pn_length ->
      f (| Long, (| (), (| Handshake, (protected_bits, () ) |) |) |)
    | PRetry _ ->
      f (| Long, (| (), (| Retry, (protected_bits, () ) |) |) |)
    end

#pop-options

let first_byte_of_header
  (short_dcid_len: short_dcid_len_t)
  (m: header' short_dcid_len)
: Tot (LPB.bitsum'_type first_byte)
= first_byte_of_header' short_dcid_len (LPB.bitsum'_type first_byte) id m

[@LPB.filter_bitsum'_t_attr]
inline_for_extraction
noextract
let common_long_t
: Type0
= (U32.t & (LP.parse_bounded_vlbytes_t 0 20 & LP.parse_bounded_vlbytes_t 0 20))

inline_for_extraction
let payload_and_pn_length_prop
  (x: U62.t)
val payload_and_pn_length_prop (x: U62.t) : Tot bool
x: QUIC.UInt62.t -> Prims.bool