val in_window (pn_len: nat{pn_len < 4}) (last pn: nat) : Tot bool
val in_window (pn_len: nat{pn_len < 4}) (last pn: nat) : Tot bool
let in_window (pn_len: nat { pn_len < 4 }) (last pn:nat) : Tot bool =
  let h = bound_npn' pn_len in
  (last+1 < h/2 && pn < h) ||
  (last+1 >= U62.v U62.bound - h/2 && pn >= U62.v U62.bound - h) ||
  (last+1 - h/2 < pn && pn <= last+1 + h/2)
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 *)

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.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
pn_len: Prims.nat{pn_len < 4} -> last: Prims.nat -> pn: Prims.nat -> Prims.bool
Prims.nat Prims.b2t Prims.op_LessThan Prims.op_BarBar Prims.op_AmpAmp Prims.op_Addition Prims.op_Division Prims.op_GreaterThanOrEqual Prims.op_Subtraction FStar.UInt64.v QUIC.UInt62.bound Prims.op_LessThanOrEqual Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThan Prims.pow2 Prims.op_Multiply QUIC.Spec.PacketNumber.Base.bound_npn' Prims.bool
let in_window (pn_len: nat{pn_len < 4}) (last pn: nat) : Tot bool =
  
let h = bound_npn' pn_len in
(last + 1 < h / 2 && pn < h) || (last + 1 >= U62.v U62.bound - h / 2 && pn >= U62.v U62.bound - h) ||
(last + 1 - h / 2 < pn && pn <= last + 1 + h / 2)