val bound_npn' (pn_len: nat{pn_len < 4}) : Tot (y: nat{y == pow2 (8 `op_Multiply` (pn_len + 1))})
let bound_npn' (pn_len:nat { pn_len < 4 }) : Tot (y: nat {y == pow2 (8 `op_Multiply` (pn_len + 1)) }) =
  assert_norm (pow2 8 == 256);
  assert_norm (pow2 16 == 65536);
  assert_norm (pow2 24 == 16777216);
  assert_norm (pow2 32 == 4294967296);
  match pn_len with
  | 0 -> 256
  | 1 -> 65536
  | 2 -> 16777216
  | 3 -> 4294967296
val bound_npn' (pn_len: nat{pn_len < 4}) : Tot (y: nat{y == pow2 (8 `op_Multiply` (pn_len + 1))})
let bound_npn' (pn_len: nat{pn_len < 4}) : Tot (y: nat{y == pow2 (8 `op_Multiply` (pn_len + 1))}) =
assert_norm (pow2 8 == 256);
assert_norm (pow2 16 == 65536);
assert_norm (pow2 24 == 16777216);
assert_norm (pow2 32 == 4294967296);
match pn_len with
| 0 -> 256
| 1 -> 65536
| 2 -> 16777216
| 3 -> 4294967296
QUIC.Spec.PacketNumber.Base.fst.checked
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
Prims.nat Prims.b2t Prims.op_LessThan Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Prims.op_GreaterThan Prims.pow2 Prims.op_Multiply Prims.op_Addition Prims.unit FStar.Pervasives.assert_norm
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 })

inline_for_extraction
let last_packet_number_t = (last: U62.secret { Secret.v last + 1 < U62.v U62.bound})


(* Packet number *)
val bound_npn' (pn_len: nat{pn_len < 4}) : Tot (y: nat{y == pow2 (8 `op_Multiply` (pn_len + 1))})
pn_len: Prims.nat{pn_len < 4} -> y: Prims.nat{y == Prims.pow2 (8 * (pn_len + 1))}