val parse_packet_number_kind : LowParse.Spec.Base.parser_kind
let parse_packet_number_kind = strong_parser_kind 1 4 None
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
/
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
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_kind =
  
strong_parser_kind 1 4 None