val 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)
  : Lemma
  (requires
    p > 0 /\
    r1 >= 0 /\
    n > 0 /\
    4 * (n * n) == p + 5 /\
    r == r1 * n + r0 /\
    h == h2 * (n * n) + h1 * n + h0 /\
    s1 == r1 + (r1 / 4) /\
    r1 % 4 == 0 /\
    d0 == h0 * r0 + h1 * s1 /\
    d1 == h0 * r1 + h1 * r0 + h2 * s1 /\
    d2 == h2 * r0 /\
    hh == d2 * (n * n) + d1 * n + d0)
  (ensures (h * r) % p == hh % p)
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 ())
val 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)
  : Lemma
  (requires
    p > 0 /\
    r1 >= 0 /\
    n > 0 /\
    4 * (n * n) == p + 5 /\
    r == r1 * n + r0 /\
    h == h2 * (n * n) + h1 * n + h0 /\
    s1 == r1 + (r1 / 4) /\
    r1 % 4 == 0 /\
    d0 == h0 * r0 + h1 * s1 /\
    d1 == h0 * r1 + h1 * r0 + h2 * s1 /\
    d2 == h2 * r0 /\
    hh == d2 * (n * n) + d1 * n + d0)
  (ensures (h * r) % p == hh % p)
let lemma_poly_multiply (n p r h r0 r1 h0 h1 h2 s1 d0 d1 d2 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
let b = ((h2 * n + h1) * r1_4) in
modulo_addition_lemma hh_expand p b;
FStar.Tactics.Effect.assert_by_tactic (h_r_expand == hh_expand + b * ((n * n) * 4 + (- 5)))
  (fun _ ->
      ();
      (int_semiring ()))
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.int FStar.Tactics.Effect.assert_by_tactic Prims.eq2 Prims.op_Addition FStar.Mul.op_Star Prims.op_Minus Prims.unit FStar.Tactics.CanonCommSemiring.int_semiring Vale.Math.Lemmas.Int.modulo_addition_lemma Prims.op_Division
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"
val 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)
  : Lemma
  (requires
    p > 0 /\
    r1 >= 0 /\
    n > 0 /\
    4 * (n * n) == p + 5 /\
    r == r1 * n + r0 /\
    h == h2 * (n * n) + h1 * n + h0 /\
    s1 == r1 + (r1 / 4) /\
    r1 % 4 == 0 /\
    d0 == h0 * r0 + h1 * s1 /\
    d1 == h0 * r1 + h1 * r0 + h2 * s1 /\
    d2 == h2 * r0 /\
    hh == d2 * (n * n) + d1 * n + d0)
  (ensures (h * r) % p == hh % p)

    n: Prims.int ->
    p: Prims.int ->
    r: Prims.int ->
    h: Prims.int ->
    r0: Prims.int ->
    r1: Prims.int ->
    h0: Prims.int ->
    h1: Prims.int ->
    h2: Prims.int ->
    s1: Prims.int ->
    d0: Prims.int ->
    d1: Prims.int ->
    d2: Prims.int ->
    hh: Prims.int
  -> FStar.Pervasives.Lemma
      (requires
        p > 0 /\ r1 >= 0 /\ n > 0 /\ 4 * (n * n) == p + 5 /\ r == r1 * n + r0 /\
        h == h2 * (n * n) + h1 * n + h0 /\ s1 == r1 + r1 / 4 /\ r1 % 4 == 0 /\
        d0 == h0 * r0 + h1 * s1 /\ d1 == h0 * r1 + h1 * r0 + h2 * s1 /\ d2 == h2 * r0 /\
        hh == d2 * (n * n) + d1 * n + d0) (ensures h * r % p == hh % p)