val first_byte:LPB.bitsum' LPB.uint8 8
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 ())
        )
      )
  )
val first_byte:LPB.bitsum' LPB.uint8 8
let first_byte:LPB.bitsum' LPB.uint8 8 =
LPB.BitSum' _
  _
  header_form
  (function
    | Short -> LPB.BitSum' _ _ fixed_bit (fun _ -> LPB.BitField 1 (LPB.BitField 5 (LPB.BitStop ())))
    | Long ->
      LPB.BitSum' _
        _
        fixed_bit
        (fun _ -> LPB.BitSum' _ _ long_packet_type (function | _ -> LPB.BitField 4 (LPB.BitStop ()))
        ))
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
LowParse.Spec.BitSum.BitSum' FStar.UInt8.t LowParse.BitFields.uint8 QUIC.Spec.Header.Public.header_form_t QUIC.Spec.Header.Public.header_form LowParse.Spec.Enum.enum_key LowParse.BitFields.bitfield Prims.op_Subtraction 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
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
val first_byte:LPB.bitsum' LPB.uint8 8
LowParse.Spec.BitSum.bitsum' LowParse.BitFields.uint8 8