val logand_mask (#n: pos) (a: U.uint_t n) (m: nat{m <= n})
    : Lemma (pow2 m <= pow2 n /\ U.logand #n a (pow2 m - 1) == a % pow2 m)
val logand_mask (#n: pos) (a: U.uint_t n) (m: nat{m <= n})
    : Lemma (pow2 m <= pow2 n /\ U.logand #n a (pow2 m - 1) == a % pow2 m)
let logand_mask (#n:pos) (a:U.uint_t n) (m:nat{m <= n})
: Lemma (pow2 m <= pow2 n /\ U.logand #n a (pow2 m - 1) == a % pow2 m)
= if m = 0
  then U.logand_lemma_1 a
  else if m = n
  then begin
    FStar.Math.Lemmas.small_mod a (pow2 n);
    U.logand_lemma_2 a
  end
  else U.logand_mask a m
module QUIC.Spec.PacketNumber.Lemmas

let replace_modulo' (a b new_mod:nat) : Pure nat
  (requires b > 0 /\ new_mod < b)
  (ensures fun res -> res % b = new_mod /\ res / b = a / b) =
  let open FStar.Math.Lemmas in
  let res = a - a%b + new_mod in
  lemma_mod_plus new_mod (a/b) b;
  small_mod new_mod b;
  res

#push-options "--z3rlimit 256"
let lemma_replace_modulo_bound_aux (k:nat) (a:nat) (b:nat) (u:nat)
  : Lemma (requires a < pow2 k /\ a % pow2 u == 0 /\ b < pow2 u /\ u < k)
  (ensures a + b < pow2 k) =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  lemma_div_mod a (pow2 u);
  assert(a + b == pow2 u * (a / pow2 u) + b);
  lemma_div_plus b (a / pow2 u) (pow2 u);
  small_div b (pow2 u);
  lemma_div_lt_nat a k u;
  assert((a / pow2 u) < pow2 (k-u));
  assert(((a + b) / pow2 u) / pow2 (k-u) < 1);
  division_multiplication_lemma (a+b) (pow2 u) (pow2 (k-u));
  pow2_plus u (k-u)
#pop-options

#push-options "--z3rlimit 1024"

#restart-solver
let lemma_replace_modulo_bound (a mod_pow new_mod up_pow:nat) : Lemma
  (requires
    mod_pow < up_pow /\
    new_mod < pow2 mod_pow /\
    a < pow2 up_pow)
  (ensures replace_modulo' a (pow2 mod_pow) new_mod < pow2 up_pow) =
  let open FStar.Math.Lemmas in
  let open FStar.Mul in
  let (pmod,umod) = (pow2 mod_pow, pow2 up_pow) in
  lemma_div_mod a pmod;
  multiple_modulo_lemma (a / pmod) pmod;
  lemma_replace_modulo_bound_aux up_pow (a-a%pow2 mod_pow) new_mod mod_pow

module U64 = FStar.UInt64

#restart-solver

module Secret = QUIC.Secret.Int
module U = FStar.UInt
/
QUIC.Secret.Int.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Ghost.fsti.checked
QUIC.Spec.PacketNumber.Lemmas.fst
a: FStar.UInt.uint_t n -> m: Prims.nat{m <= n}
  -> FStar.Pervasives.Lemma
    (ensures
      Prims.pow2 m <= Prims.pow2 n /\ FStar.UInt.logand a (Prims.pow2 m - 1) == a % Prims.pow2 m)
Prims.pos FStar.UInt.uint_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Equality Prims.int FStar.UInt.logand_lemma_1 Prims.bool Prims.l_or Prims.op_GreaterThan Prims.l_and Prims.op_GreaterThanOrEqual FStar.UInt.logand_lemma_2 Prims.unit FStar.Math.Lemmas.small_mod Prims.pow2 FStar.UInt.logand_mask Prims.l_True Prims.squash Prims.eq2 FStar.UInt.logand Prims.op_Subtraction Prims.op_Modulus Prims.Nil FStar.Pervasives.pattern
let logand_mask (#n: pos) (a: U.uint_t n) (m: nat{m <= n})
    : Lemma (pow2 m <= pow2 n /\ U.logand #n a (pow2 m - 1) == a % pow2 m) =
  
if m = 0
then U.logand_lemma_1 a
else
  if m = n
  then
    (FStar.Math.Lemmas.small_mod a (pow2 n);
      U.logand_lemma_2 a)
  else U.logand_mask a m