val lemma_poly_bits64 (u:unit) : Lemma
  (requires True)
  (ensures
    (forall (x:nat64).{:pattern (shift_right64 x 2)} shift_right64 x 2 == x / 4) /\
    (forall (x:nat64).{:pattern (shift_right64 x 4)} shift_right64 x 4 == x / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 3)} logand64 x 3 == x % 4) /\
    (forall (x:nat64).{:pattern (logand64 x 15)} logand64 x 15 == x % 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0)} logand64 x 0 == 0) /\
    (forall (x:nat64).{:pattern (logand64 x 0xffffffffffffffff)} logand64 x 0xffffffffffffffff == x) /\
    (forall (x:nat64).{:pattern (logand64 x 0xfffffffffffffffc)} logand64 x 0xfffffffffffffffc == (x / 4) * 4) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0fffffff)} logand64 x 0x0ffffffc0fffffff < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} logand64 x 0x0ffffffc0ffffffc < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} (logand64 x 0x0ffffffc0ffffffc) % 4 == 0) /\
    (forall (x:nat64) (y:nat64).{:pattern (logand64 x y)} logand64 x y == logand64 y x))
let lemma_poly_bits64 () =
    forall_intro (lemma_shr2_nat);
    forall_intro (lemma_shr4_nat);
    forall_intro (lemma_and_mod_n_nat);
    forall_intro (lemma_and_constants_nat);
    forall_intro (lemma_clear_lower_2_nat);
    forall_intro (lemma_poly_constants_nat);
    forall_intro_2 (lemma_and_commutes_nat)
val lemma_poly_bits64 (u:unit) : Lemma
  (requires True)
  (ensures
    (forall (x:nat64).{:pattern (shift_right64 x 2)} shift_right64 x 2 == x / 4) /\
    (forall (x:nat64).{:pattern (shift_right64 x 4)} shift_right64 x 4 == x / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 3)} logand64 x 3 == x % 4) /\
    (forall (x:nat64).{:pattern (logand64 x 15)} logand64 x 15 == x % 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0)} logand64 x 0 == 0) /\
    (forall (x:nat64).{:pattern (logand64 x 0xffffffffffffffff)} logand64 x 0xffffffffffffffff == x) /\
    (forall (x:nat64).{:pattern (logand64 x 0xfffffffffffffffc)} logand64 x 0xfffffffffffffffc == (x / 4) * 4) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0fffffff)} logand64 x 0x0ffffffc0fffffff < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} logand64 x 0x0ffffffc0ffffffc < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} (logand64 x 0x0ffffffc0ffffffc) % 4 == 0) /\
    (forall (x:nat64) (y:nat64).{:pattern (logand64 x y)} logand64 x y == logand64 y x))
let lemma_poly_bits64 () =
forall_intro (lemma_shr2_nat);
forall_intro (lemma_shr4_nat);
forall_intro (lemma_and_mod_n_nat);
forall_intro (lemma_and_constants_nat);
forall_intro (lemma_clear_lower_2_nat);
forall_intro (lemma_poly_constants_nat);
forall_intro_2 (lemma_and_commutes_nat)
Vale.Poly1305.Math.fst.checked
Vale.Poly1305.Bitvectors.fsti.checked Vale.Math.Lemmas.Int.fsti.checked Vale.Def.TypesNative_s.fst.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.Canon.fst.checked FStar.Tactics.BV.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Vale.Poly1305.Math.fst
Prims.unit FStar.Classical.forall_intro_2 Vale.Def.Types_s.nat64 Prims.eq2 Vale.Poly1305.Math.logand64 Vale.Poly1305.Math.lemma_and_commutes_nat FStar.Classical.forall_intro Prims.l_and Prims.b2t Prims.op_LessThan Prims.int Prims.op_Modulus Vale.Poly1305.Math.lemma_poly_constants_nat FStar.Mul.op_Star Prims.op_Division Vale.Poly1305.Math.lemma_clear_lower_2_nat Vale.Poly1305.Math.lemma_and_constants_nat Vale.Poly1305.Math.lemma_and_mod_n_nat Vale.Poly1305.Math.shift_right64 Vale.Poly1305.Math.lemma_shr4_nat Vale.Poly1305.Math.lemma_shr2_nat
module Vale.Poly1305.Math

open FStar.Tactics
open FStar.Tactics.Canon
open FStar.Math.Lemmas
// open FStar.Math.Lib
open Vale.Math.Lemmas.Int
open FStar.Tactics.CanonCommSemiring
open FStar.Mul
open Vale.Def.TypesNative_s
open Vale.Arch.TypesNative
open FStar.Classical
open Vale.Poly1305.Bitvectors

#reset-options "--smtencoding.elim_box true --z3cliopt smt.arith.nl=true --max_fuel 1 --max_ifuel 1 --smtencoding.nl_arith_repr native --z3rlimit 100 --using_facts_from Prims --using_facts_from FStar.Math.Lemmas"

val lemma_mul_div_comm: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0 /\ a % b = 0))
          (ensures (a/b)*c == a * (c/b))
let lemma_mul_div_comm a b c =
    ()

val lemma_exact_mul: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0))
          (ensures ((a*c) % b = 0))
let lemma_exact_mul a b c =
  (* a*c = c*a *)
  swap_mul a c;

  (* (c*a)%b = ((c%b)*a)%b *)
  lemma_mod_mul_distr_l c a b;
  ()

val lemma_mul_div_sep: a:nat -> b:pos -> c:nat ->
    Lemma (requires (c % b = 0) /\ (a*c) % b = 0)
          (ensures (a*c)/b == a * (c/b))
let lemma_mul_div_sep a b c = ()

val swap_add: a:int -> b:int -> c:int -> Lemma
      (a + b + c = a + c + b)
let swap_add a b c = ()

#reset-options "--z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --z3cliopt smt.arith.nl=true --max_fuel 0 --max_ifuel 1 --smtencoding.elim_box true --smtencoding.nl_arith_repr wrapped --smtencoding.l_arith_repr native --z3rlimit 15"

let lemma_mul_increases(x y:pos) :
  Lemma (y <= y * x) = ()

val multiplication_order_lemma_int: a:int -> b:int -> p:pos ->
    Lemma (a < b <==> p * a < p * b)
let multiplication_order_lemma_int a b p = ()

val multiplication_order_eq_lemma_int: a:int -> b:int -> p:pos ->
    Lemma (a <= b <==> p * a <= p * b)
let multiplication_order_eq_lemma_int a b p = ()

#reset-options "--z3cliopt smt.QI.EAGER_THRESHOLD=100 --z3cliopt smt.CASE_SPLIT=3 --z3cliopt smt.arith.nl=false --max_fuel 0 --max_ifuel 1 --smtencoding.elim_box true --smtencoding.nl_arith_repr wrapped --smtencoding.l_arith_repr native --z3rlimit 8"

let lemma_poly_multiply (n:int) (p:int) (r:int) (h:int) (r0:int) (r1:int) (h0:int) (h1:int)
                        (h2:int) (s1:int) (d0:int) (d1:int) (d2:int) (hh:int) =
  let r1_4 = r1 / 4 in
  let h_r_expand = (h2 * (n * n) + h1 * n + h0) * ((r1_4 * 4) * n + r0) in
  let hh_expand = (h2 * r0) * (n * n) + (h0 * (r1_4 * 4) + h1 * r0 + h2 * (5 * r1_4)) * n
    + (h0 * r0 + h1 * (5 * r1_4)) in
  //assert (h * r == h_r_expand);
  //assert (hh == hh_expand);
  let b = ((h2 * n + h1) * r1_4) in
  modulo_addition_lemma hh_expand p b;
  assert (h_r_expand == hh_expand + b * (n * n * 4 + (-5)))
  by (int_semiring ())


let lemma_poly_reduce (n:int) (p:int) (h:int) (h2:int) (h10:int) (c:int) (hh:int) =
   let h2_4 = h2 / 4 in
   let h2_m = h2 % 4 in
   let h_expand = h10 + (h2_4 * 4 + h2_m) * (n * n) in
   let hh_expand = h10 + (h2_m) * (n * n) + h2_4 * 5 in
   lemma_div_mod h (n * n);
   modulo_addition_lemma hh_expand p h2_4;
   assert (h_expand == hh_expand + h2_4 * (n * n * 4 + (-5)))
   by (int_semiring ())


(* These lemmas go through because of SMT patterns,
   is that the right style to use here?*)

let lemma_shr2_nat (x:nat64) :
  Lemma (shift_right64 x 2 == x / 4) =
  reveal_ishr 64 x 2
let lemma_shr4_nat (x:nat64) :
  Lemma (shift_right64 x 4 == x / 16) =
  reveal_ishr 64 x 4
let lemma_and_mod_n_nat (x:nat64) :
 Lemma (logand64 x 3 == x % 4 /\
        logand64 x 15 == x % 16) =
  reveal_iand 64 x 3;
  reveal_iand 64 x 15
let lemma_and_constants_nat (x:nat64) :
  Lemma (logand64 x 0 == 0 /\
         logand64 x 0xffffffffffffffff == x) =
  reveal_iand 64 x 0;
  reveal_iand 64 x 0xffffffffffffffff

let lemma_clear_lower_2_nat (x:nat64) :
  Lemma (logand64 x 0xfffffffffffffffc == (x/4)*4) =
  reveal_iand 64 x 0xfffffffffffffffc;
  assert (x < pow2_64);
  assert ((x/4)*4 < pow2_64);
  modulo_lemma ((x/4)*4) (pow2_64)

// reveal_iand_all 64 does not work here.
let lemma_poly_constants_nat (x:nat64) :
  Lemma (logand64 x 0x0ffffffc0fffffff < 0x1000000000000000 /\
         logand64 x 0x0ffffffc0ffffffc < 0x1000000000000000 /\
         (logand64 x 0x0ffffffc0ffffffc) % 4 == 0) =
  reveal_iand 64 x 0x0ffffffc0fffffff;
  reveal_iand 64 x 0x0ffffffc0ffffffc

let lemma_and_commutes_nat (x y:nat64) :
  Lemma (logand64 x y == logand64 y x) =
  reveal_iand_all 64;
  lemma_and_commutes x y


// using forall_intro on original bitvector lemmas and
// ireveal_and_all etc. does not solve the goal
val lemma_poly_bits64 (u:unit) : Lemma
  (requires True)
  (ensures
    (forall (x:nat64).{:pattern (shift_right64 x 2)} shift_right64 x 2 == x / 4) /\
    (forall (x:nat64).{:pattern (shift_right64 x 4)} shift_right64 x 4 == x / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 3)} logand64 x 3 == x % 4) /\
    (forall (x:nat64).{:pattern (logand64 x 15)} logand64 x 15 == x % 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0)} logand64 x 0 == 0) /\
    (forall (x:nat64).{:pattern (logand64 x 0xffffffffffffffff)} logand64 x 0xffffffffffffffff == x) /\
    (forall (x:nat64).{:pattern (logand64 x 0xfffffffffffffffc)} logand64 x 0xfffffffffffffffc == (x / 4) * 4) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0fffffff)} logand64 x 0x0ffffffc0fffffff < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} logand64 x 0x0ffffffc0ffffffc < pow2_64 / 16) /\
    (forall (x:nat64).{:pattern (logand64 x 0x0ffffffc0ffffffc)} (logand64 x 0x0ffffffc0ffffffc) % 4 == 0) /\
    (forall (x:nat64) (y:nat64).{:pattern (logand64 x y)} logand64 x y == logand64 y x))
u68: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      (forall (x: Vale.Def.Types_s.nat64). {:pattern Vale.Poly1305.Math.shift_right64 x 2}
          Vale.Poly1305.Math.shift_right64 x 2 == x / 4) /\
      (forall (x: Vale.Def.Types_s.nat64). {:pattern Vale.Poly1305.Math.shift_right64 x 4}
          Vale.Poly1305.Math.shift_right64 x 4 == x / 16) /\
      (forall (x: Vale.Def.Types_s.nat64). {:pattern Vale.Poly1305.Math.logand64 x 3}
          Vale.Poly1305.Math.logand64 x 3 == x % 4) /\
      (forall (x: Vale.Def.Types_s.nat64). {:pattern Vale.Poly1305.Math.logand64 x 15}
          Vale.Poly1305.Math.logand64 x 15 == x % 16) /\
      (forall (x: Vale.Def.Types_s.nat64). {:pattern Vale.Poly1305.Math.logand64 x 0}
          Vale.Poly1305.Math.logand64 x 0 == 0) /\
      (forall (x: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x 0xffffffffffffffff}
          Vale.Poly1305.Math.logand64 x 0xffffffffffffffff == x) /\
      (forall (x: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x 0xfffffffffffffffc}
          Vale.Poly1305.Math.logand64 x 0xfffffffffffffffc == (x / 4) * 4) /\
      (forall (x: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x 0x0ffffffc0fffffff}
          Vale.Poly1305.Math.logand64 x 0x0ffffffc0fffffff < Vale.Def.Words_s.pow2_64 / 16) /\
      (forall (x: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x 0x0ffffffc0ffffffc}
          Vale.Poly1305.Math.logand64 x 0x0ffffffc0ffffffc < Vale.Def.Words_s.pow2_64 / 16) /\
      (forall (x: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x 0x0ffffffc0ffffffc}
          Vale.Poly1305.Math.logand64 x 0x0ffffffc0ffffffc % 4 == 0) /\
      (forall (x: Vale.Def.Types_s.nat64) (y: Vale.Def.Types_s.nat64).
          {:pattern Vale.Poly1305.Math.logand64 x y}
          Vale.Poly1305.Math.logand64 x y == Vale.Poly1305.Math.logand64 y x))