val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
let max (a b:int) : Tot (n:int{n >= a /\ n >= b}) =
  if a > b then a else b
val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
let max (a b: int) : Tot (n: int{n >= a /\ n >= b}) =
if a > b then a else b
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.int Prims.op_GreaterThan Prims.bool Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual
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 })
=
  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
#pop-options
val max (a b: int) : Tot (n: int{n >= a /\ n >= b})
a: Prims.int -> b: Prims.int -> n: Prims.int{n >= a /\ n >= b}