val lemma_bytes_and_mod4: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100000000 - 1) == x % 0x100000000)
let lemma_bytes_and_mod4 x =
  assert_by_tactic (logand #64 x (0x100000000 - 1) == mod #64 x 0x100000000) bv_tac
val lemma_bytes_and_mod4: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100000000 - 1) == x % 0x100000000)
let lemma_bytes_and_mod4 x =
assert_by_tactic (logand #64 x (0x100000000 - 1) == mod #64 x 0x100000000) bv_tac
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
FStar.UInt.uint_t FStar.Tactics.Effect.assert_by_tactic Prims.eq2 FStar.UInt.logand Prims.op_Subtraction FStar.UInt.mod FStar.Tactics.BV.bv_tac Prims.unit
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
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)

let lemma_mul_strict_upper_bound (x:int) (x_bound:int) (y:int) (y_bound:int) =
  lemma_mult_le_right y x x_bound;
  if x_bound = 0 || y_bound = 0 then ()
  else
    if y = 0 then
    begin
      assert_norm(x*0 = 0);
      pos_times_pos_is_pos x_bound y_bound
    end
    else
      lemma_mult_lt_left x_bound y y_bound

let lemma_bytes_shift_power2 (y:nat64) =
  lemma_bytes_shift_power2 y;
  reveal_ishl_all 64

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


open FStar.UInt
open FStar.Tactics
open FStar.Tactics.BV

val lemma_bytes_and_mod0: x: uint_t 64 ->
  Lemma (logand #64 x  (0x1 - 1) == x % 0x1)
val lemma_bytes_and_mod1: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100 - 1) == x % 0x100)
val lemma_bytes_and_mod2: x: uint_t 64 ->
  Lemma (logand #64 x  (0x10000 - 1) == x % 0x10000)
val lemma_bytes_and_mod3: x: uint_t 64 ->
  Lemma (logand #64 x  (0x1000000 - 1) == x % 0x1000000)
val lemma_bytes_and_mod4: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100000000 - 1) == x % 0x100000000)
val lemma_bytes_and_mod5: x: uint_t 64 ->
  Lemma (logand #64 x  (0x10000000000 - 1) == x % 0x10000000000)
val lemma_bytes_and_mod6: x: uint_t 64 ->
  Lemma (logand #64 x  (0x1000000000000 - 1) == x % 0x1000000000000)
val lemma_bytes_and_mod7: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100000000000000 - 1) == x % 0x100000000000000)

#push-options "--z3cliopt smt.arith.nl=true"
let lemma_bytes_and_mod0 x =
  assert_by_tactic (logand #64 x (0x1 - 1) == mod #64 x 0x1) bv_tac

let lemma_bytes_and_mod1 x =
  assert_by_tactic (logand #64 x (0x100 - 1) == mod #64 x 0x100) bv_tac

let lemma_bytes_and_mod2 x =
  assert_by_tactic (logand #64 x (0x10000 - 1) == mod #64 x 0x10000) bv_tac
let lemma_bytes_and_mod3 x =
  assert_by_tactic (logand #64 x (0x1000000 - 1) == mod #64 x 0x1000000) bv_tac
val lemma_bytes_and_mod4: x: uint_t 64 ->
  Lemma (logand #64 x  (0x100000000 - 1) == x % 0x100000000)
x: FStar.UInt.uint_t 64
  -> FStar.Pervasives.Lemma (ensures FStar.UInt.logand x (0x100000000 - 1) == x % 0x100000000)