val 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
val 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
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
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
/
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

    short_dcid_len: QUIC.Spec.Base.short_dcid_len_t ->
    t: Type0 ->
    f: (_: LowParse.Spec.BitSum.bitsum'_type QUIC.Spec.Header.Public.first_byte -> t) ->
    m: QUIC.Spec.Header.Public.header' short_dcid_len
  -> t
QUIC.Spec.Base.short_dcid_len_t LowParse.Spec.BitSum.bitsum'_type FStar.UInt8.t LowParse.BitFields.uint8 QUIC.Spec.Header.Public.first_byte QUIC.Spec.Header.Public.header' QUIC.Spec.Base.bitfield Prims.bool QUIC.Spec.Base.vlbytes Prims.Mkdtuple2 LowParse.Spec.Enum.enum_key QUIC.Spec.Header.Public.header_form_t LowParse.BitFields.bitfield QUIC.Spec.Header.Public.header_form LowParse.Spec.BitSum.bitsum'_type' Prims.op_Subtraction LowParse.Spec.BitSum.BitSum' Prims.unit 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 QUIC.Spec.Header.Public.Short FStar.Pervasives.Native.Mktuple2 FStar.UInt8.__uint_to_t FStar.UInt32.t QUIC.Spec.Header.Public.long_header_specifics QUIC.Spec.Base.token_max_len QUIC.Spec.Base.payload_and_pn_length_t QUIC.Spec.Header.Public.Long QUIC.Spec.Header.Public.Initial QUIC.Spec.Header.Public.ZeroRTT QUIC.Spec.Header.Public.Handshake QUIC.Spec.Header.Public.Retry
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 ->
  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, ()) |) |) |)