val expand_pn'
      (pn_len: nat{pn_len < 4})
      (last: nat{last + 1 < pow2 62})
      (npn: nat{npn < bound_npn' pn_len})
    : Tot (pn: nat{pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn})
let expand_pn'
  (pn_len: nat { pn_len < 4 })
  (last: nat { last + 1 < pow2 62})
  (npn: nat { npn < bound_npn' pn_len })
: Tot (pn: nat { pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn })
=
  let open FStar.Mul in
  let open FStar.Math.Lemmas in
  let expected = last + 1 in
  let bound = bound_npn' pn_len in
  let candidate = replace_modulo' expected bound npn in
  lemma_replace_modulo_bound expected (8*(pn_len+1)) npn 62;
  if candidate <= last + 1 - bound/2
     && candidate < pow2 62 - bound then // the test for overflow (candidate < pow2 62 - bound) is not present in draft 22.
    let _ = lemma_mod_plus candidate 1 bound in
    candidate + bound
  else if candidate > last + 1 + bound/2
          && candidate >= bound then // in draft 22 the test for underflow (candidate >= bound) uses a strict inequality, which makes it impossible to expand npn to 0
    let _ = lemma_mod_plus candidate (-1) bound in
    candidate - bound
  else candidate
val expand_pn'
      (pn_len: nat{pn_len < 4})
      (last: nat{last + 1 < pow2 62})
      (npn: nat{npn < bound_npn' pn_len})
    : Tot (pn: nat{pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn})
let expand_pn'
      (pn_len: nat{pn_len < 4})
      (last: nat{last + 1 < pow2 62})
      (npn: nat{npn < bound_npn' pn_len})
    : Tot (pn: nat{pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn}) =
let open FStar.Mul in
let open FStar.Math.Lemmas in
let expected = last + 1 in
let bound = bound_npn' pn_len in
let candidate = replace_modulo' expected bound npn in
lemma_replace_modulo_bound expected (8 * (pn_len + 1)) npn 62;
if candidate <= last + 1 - bound / 2 && candidate < pow2 62 - bound
then
  let _ = lemma_mod_plus candidate 1 bound in
  candidate + bound
else
  if candidate > last + 1 + bound / 2 && candidate >= bound
  then
    let _ = lemma_mod_plus candidate (- 1) bound in
    candidate - bound
  else candidate
QUIC.Spec.PacketNumber.fst.checked
QUIC.Spec.PacketNumber.Lemmas.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.BoundedInt.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.Classical.fsti.checked
QUIC.Spec.PacketNumber.fst
Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Addition Prims.pow2 QUIC.Spec.PacketNumber.Base.bound_npn' Prims.op_AmpAmp Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.op_Division Prims.unit FStar.Math.Lemmas.lemma_mod_plus Prims.bool Prims.op_GreaterThan Prims.op_GreaterThanOrEqual Prims.op_Minus Prims.l_and QUIC.Spec.PacketNumber.Base.in_window Prims.eq2 Prims.int Prims.op_Modulus QUIC.Spec.PacketNumber.Lemmas.lemma_replace_modulo_bound FStar.Mul.op_Star QUIC.Spec.PacketNumber.Lemmas.replace_modulo' Prims.l_or Prims.op_Multiply
module QUIC.Spec.PacketNumber
open QUIC.Spec.PacketNumber.Lemmas
open LowParse.Spec.Combinators
open LowParse.Spec.BoundedInt

(* From https://tools.ietf.org/html/draft-ietf-quic-transport-22#appendix-A *)

module Cast = FStar.Int.Cast
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8

module Secret = QUIC.Secret.Int

let reduce_pn'
  (pn_len: nat { pn_len < 4 })
  (pn: nat)
: Tot nat
= pn % (bound_npn' pn_len)

let in_window_self (pn_len: nat { pn_len < 4 }) (pn:nat) : Lemma
  (in_window pn_len pn (if pn = 0 then 0 else pn - 1))
= ()

#push-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"
let expand_pn'
  (pn_len: nat { pn_len < 4 })
  (last: nat { last + 1 < pow2 62})
  (npn: nat { npn < bound_npn' pn_len })
: Tot (pn: nat { pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn })
val expand_pn'
      (pn_len: nat{pn_len < 4})
      (last: nat{last + 1 < pow2 62})
      (npn: nat{npn < bound_npn' pn_len})
    : Tot (pn: nat{pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn})

    pn_len: Prims.nat{pn_len < 4} ->
    last: Prims.nat{last + 1 < Prims.pow2 62} ->
    npn: Prims.nat{npn < QUIC.Spec.PacketNumber.Base.bound_npn' pn_len}
  -> pn:
    Prims.nat
      { pn < Prims.pow2 62 /\ QUIC.Spec.PacketNumber.Base.in_window pn_len last pn /\
        pn % QUIC.Spec.PacketNumber.Base.bound_npn' pn_len == npn }