Util: added util lemmas needed to instantiate EdDSA25519.

3 files changed, 151 insertions, 0 deletions

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
new file mode 100644
index 000000000..afed2a231
--- /dev/null
+++ b/src/Util/NatUtil.v
@@ -0,0 +1,56 @@
+Require Import NPeano Omega.
+
+Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
+Proof.
+  intros.
+  assert (b = 1 * b) by omega.
+  rewrite H0 at 1.
+  rewrite <- Nat.div_add by auto.
+  reflexivity.
+Qed.
+
+Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2).
+Proof.
+  assert (4 <> 0) as ne40 by omega.
+  induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. {
+    rewrite H0 in H1.
+    simpl in H1.
+    rewrite H1.
+    exists 0; auto.
+  } {
+    rewrite mult_succ_r in H1.
+    assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; omega).
+    rewrite <- Nat.add_1_r in H.
+    replace x with ((x - 4) + 4) in H by omega.
+    rewrite div_minus in H by auto.
+    apply Nat.add_cancel_r in H.
+    replace x with ((x - 4) + (1 * 4)) in H0 by omega.
+    rewrite Nat.mod_add in H0 by auto.
+    pose proof (IHc _ H H0).
+    destruct H2.
+    exists (x0 + 1).
+    rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto.
+    replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega.
+    apply Nat.add_cancel_r in H1.
+    replace (2 * (x0 + 1)) with (2 * x0 + 2)
+      by (rewrite Nat.mul_add_distr_l; auto).
+    rewrite H2.
+    rewrite <- Nat.div_add by omega.
+    f_equal.
+    simpl.
+    apply Nat.sub_add; auto.
+  }
+Qed.
+
+Lemma Nat2N_inj_lt : forall n m, (N.of_nat n < N.of_nat m)%N <-> n < m.
+Proof.
+  split; intros. {
+    rewrite nat_compare_lt.
+    rewrite Nnat.Nat2N.inj_compare.
+    rewrite N.compare_lt_iff; auto.
+  } {
+    rewrite <- N.compare_lt_iff.
+    rewrite <- Nnat.Nat2N.inj_compare.
+    rewrite <- nat_compare_lt; auto.
+  }
+Qed.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
new file mode 100644
index 000000000..4a54e5437
--- /dev/null
+++ b/src/Util/NumTheoryUtil.v
@@ -0,0 +1,81 @@
+Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
+Require Import Omega NPeano Arith.
+Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil.
+Local Open Scope Z.
+
+Lemma euler_criterion : forall (a x p : Z) (prime_p : prime p),
+  (x * 2 + 1 = p)%Z -> (a ^ x mod p = 1)%Z ->
+    exists b : Z, (0 <= b < p /\ b * b mod p = a)%Z.
+Admitted.
+
+Lemma divide2_1mod4 : forall x, x mod 4 = 1 -> 0 <= x -> (2 | x / 2).
+Proof.
+  intros.
+  assert (Z.to_nat x mod 4 = 1)%nat. {
+    replace 1%Z with (Z.of_nat 1) in H by auto.
+    replace (x mod 4)%Z with (Z.of_nat (Z.to_nat x mod 4)) in H
+      by (rewrite mod_Zmod by omega; rewrite Z2Nat.id; auto).
+    apply Nat2Z.inj in H; auto.
+  }
+  remember (Z.to_nat x / 4)%nat as c.
+  pose proof (divide2_1mod4_nat c (Z.to_nat x) Heqc H1).
+  destruct H2.
+  replace 2%nat with (Z.to_nat 2) in H2 by auto.
+  apply inj_eq in H2.
+  rewrite div_Zdiv in H2 by (replace (Z.to_nat 2) with 2%nat by auto; omega).
+  rewrite Nat2Z.inj_mul in H2.
+  do 2 rewrite Z2Nat.id in H2 by (auto || omega).
+  rewrite Z.mul_comm in H2.
+  symmetry in H2.
+  apply Zdivide_intro in H2; auto.
+Qed.
+
+Lemma minus1_even_pow : forall x y, (2 | y) -> (1 < x) -> (0 <= y) -> ((x - 1) ^ y mod x = 1).
+Proof.
+  intros.
+  apply Zdivide_Zdiv_eq in H; try omega.
+  rewrite H.
+  rewrite Z.pow_mul_r by omega.
+  assert ((x - 1)^2 mod x = 1). {
+    replace ((x - 1)^2) with (x ^ 2 - 2 * x + 1)
+      by (do 2 rewrite Z.pow_2_r; rewrite Z.mul_sub_distr_l; do 2 rewrite Z.mul_sub_distr_r; omega).
+    rewrite Zplus_mod.
+    rewrite Z.pow_2_r.
+    rewrite <- Z.mul_sub_distr_r.
+    rewrite Z_mod_mult.
+    do 2 rewrite Zmod_1_l by auto; auto.
+  }
+  rewrite <- (Z2Nat.id (y / 2)) by omega.
+  induction (Z.to_nat (y / 2)); try apply Zmod_1_l; auto.
+  rewrite Nat2Z.inj_succ.
+  rewrite Z.pow_succ_r by apply Zle_0_nat.
+  rewrite Zmult_mod.
+  rewrite IHn.
+  rewrite H2.
+  simpl.
+  apply Zmod_1_l; auto.
+Qed.
+
+Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p),
+  (p mod 4 = 1)%Z -> exists b : Z, (0 <= b < p /\ b * b mod p = p - 1)%Z.
+Proof.
+  intros.
+  assert (4 <> 0)%Z by omega.
+  pose proof (Z.div_mod p 4 H0).
+  pose proof (prime_ge_2 p (prime_p)).
+  assert (2 | p / 2)%Z by (apply divide2_1mod4; (auto || omega)).
+  apply (euler_criterion (p - 1) (p / 2) p prime_p);
+    [ | apply minus1_even_pow; (omega || auto); apply Z_div_pos; omega].
+  rewrite <- H.
+  rewrite H1 at 3.
+  f_equal.
+  replace 4%Z with (2 * 2)%Z by auto.
+  rewrite <- Z.div_div by omega.
+  rewrite <- Zdivide_Zdiv_eq_2 by (auto || omega).
+  replace (2 * 2 * (p / 2) / 2)%Z with (2 * (2 * (p / 2)) / 2)%Z
+    by (f_equal; apply Z.mul_assoc).
+  rewrite ZUtil.Z_div_mul' by omega.
+  rewrite Z.mul_comm.
+  auto.
+Qed.
+
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 5950f57ad..1a48abfd6 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,5 +1,7 @@
 Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
+Require Import Crypto.Util.NatUtil.
+Require Import Bedrock.Word.
 Local Open Scope Z.
 
 Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
@@ -50,3 +52,15 @@ Qed.
 Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
   intuition.
 Qed.
+
+Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)).
+Proof.
+  induction n; intros; auto.
+  simpl pow2.
+  rewrite Nat2Z.inj_succ.
+  rewrite Z.pow_succ_r by apply Zle_0_nat.
+  rewrite untimes2.
+  rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
+  rewrite <- IHn.
+  auto.
+Qed.