val parse_packet_number_kind' (sz: packet_number_length_t) : GTot parser_kind
let parse_packet_number_kind'
  (sz: packet_number_length_t)
: GTot parser_kind
= total_constant_size_parser_kind (Secret.v sz)
val parse_packet_number_kind' (sz: packet_number_length_t) : GTot parser_kind
let parse_packet_number_kind' (sz: packet_number_length_t) : GTot parser_kind =
total_constant_size_parser_kind (Secret.v sz)
QUIC.Spec.PacketNumber.fsti.checked
QUIC.UInt62.fst.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
QUIC.Spec.PacketNumber.fsti
QUIC.Spec.PacketNumber.Base.packet_number_length_t LowParse.Spec.Base.total_constant_size_parser_kind QUIC.Secret.Int.Base.v Lib.IntTypes.U32 Lib.IntTypes.SEC LowParse.Spec.Base.parser_kind
module QUIC.Spec.PacketNumber
include QUIC.Spec.PacketNumber.Base
open LowParse.Spec.Base

module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module Secret = QUIC.Secret.Int

inline_for_extraction
let parse_packet_number_kind = strong_parser_kind 1 4 None

val parse_packet_number
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
: Tot (parser parse_packet_number_kind (packet_number_t' last pn_len))

inline_for_extraction
let parse_packet_number_kind'
  (sz: packet_number_length_t)
val parse_packet_number_kind' (sz: packet_number_length_t) : GTot parser_kind
sz: QUIC.Spec.PacketNumber.Base.packet_number_length_t -> Prims.GTot LowParse.Spec.Base.parser_kind