val last_packet_number_t : Type0
let last_packet_number_t = (last: U62.secret { Secret.v last + 1 < U62.v U62.bound})
module QUIC.Spec.PacketNumber.Base

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

inline_for_extraction
noextract
type packet_number_length_t = (x: Secret.uint32 { 1 <= Secret.v x /\ Secret.v x <= 4 })
/
QUIC.UInt62.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
QUIC.Spec.PacketNumber.Base.fst
Type0
QUIC.UInt62.secret Prims.b2t Prims.op_LessThan Prims.op_Addition QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt64.v QUIC.UInt62.bound
let last_packet_number_t =
  
(last: U62.secret{Secret.v last + 1 < U62.v U62.bound})