val parse_packet_number_opt_kind : LowParse.Spec.Base.parser_kind
let parse_packet_number_opt_kind = LP.strong_parser_kind 0 4 None
module QUIC.Spec.Header.Parse

module PN = QUIC.Spec.PacketNumber
module Public = QUIC.Spec.Header.Public
module LP = LowParse.Spec.Combinators
module Secret = QUIC.Secret.Int
module BF = LowParse.BitFields
module U8 = FStar.UInt8
module Seq = QUIC.Secret.Seq
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast

let protected_bits_pn_length
  (is_short: bool)
  (pb: bitfield (if is_short then 5 else 4))
: Tot PN.packet_number_length_t
= Secret.to_u32 #Secret.U8 (1uy `Secret.add` Secret.get_bitfield #Secret.U8 pb 0ul 2ul)

let get_pn_length
  (h: Public.header)
: Tot PN.packet_number_length_t 
= protected_bits_pn_length (Public.PShort? h) (Public.get_protected_bits h)

let protected_bits_reserved
  (is_short: bool)
  (pb: bitfield (if is_short then 5 else 4))
: Tot (bitfield 2)
= if is_short
  then BF.uint8.BF.get_bitfield pb 3 5
  else BF.uint8.BF.get_bitfield pb 2 4

let get_reserved_bits
  (h: Public.header)
: Tot (bitfield 2)
= protected_bits_reserved (Public.PShort? h) (Public.get_protected_bits h)

let packet_number_opt
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (h: Public.header' cid_len)
: Tot Type0
= if Public.is_retry h
  then unit
  else PN.packet_number_t' last (get_pn_length h)
/
QUIC.Spec.PacketNumber.fsti.checked QUIC.Spec.Header.Public.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked
QUIC.Spec.Header.Parse.fst
LowParse.Spec.Base.parser_kind
LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some
let parse_packet_number_opt_kind =
  
LP.strong_parser_kind 0 4 None