ported some of EdDSA25519 to new field framework

4 files changed, 180 insertions, 2 deletions

diff --git a/_CoqProject b/_CoqProject
index e6991793b..bda8f5178 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -21,6 +21,7 @@ src/Rep/ECRep.v
 src/Rep/GaloisRep.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/EdDSA.v
+src/Spec/EdDSA25519.v
 src/Spec/ModularArithmetic.v
 src/Specific/EdDSA25519.v
 src/Specific/GF25519.v
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index bff6d1948..e05eafcdc 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -49,4 +49,41 @@ Section CompleteEdwardsCurveTheorems.
     Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
            ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
   Qed.
+
+  Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F.
+    intros ? eq_zero.
+    pose proof prime_q.
+    destruct square_a as [sqrt_a sqrt_a_id].
+    rewrite <- sqrt_a_id in eq_zero.
+    Check Fq_square_mul_sub.
+    destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero].
+    + pose proof (nonsquare_d sqrt_d); auto.
+    + subst.
+      rewrite Fq_pow_zero in sqrt_a_id by congruence.
+      auto using nonzero_a.
+  Qed.
+  
+  Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F.
+  Proof.
+    intros y eq_zero.
+    pose proof prime_q.
+    eapply F_minus_swap in eq_zero.
+    eauto using (d_y2_a_nonzero y).
+  Qed.
+
+  (* solve for x ^ 2 *)
+  Lemma onCurve_solve_x2 : (forall x y, onCurve (x, y) ->
+    x ^ 2 = (y ^ 2 - 1) / (d * (y ^ 2) - a))%F.
+  Proof.
+    intros ? ? onCurve_x_y.
+    pose proof prime_q.
+    unfold onCurve in onCurve_x_y.
+    eapply F_div_mul; auto using (d_y2_a_nonzero y).
+    replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring.
+    rewrite F_sub_add_swap.
+    replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring.
+    rewrite onCurve_x_y.
+    ring.
+  Qed.
+
 End CompleteEdwardsCurveTheorems.
diff --git a/src/Spec/EdDSA25519.v b/src/Spec/EdDSA25519.v
new file mode 100644
index 000000000..c4547860a
--- /dev/null
+++ b/src/Spec/EdDSA25519.v
@@ -0,0 +1,137 @@
+Require Import ZArith.ZArith Zpower ZArith Znumtheory.
+Require Import NPeano NArith.
+Require Import Crypto.Spec.EdDSA.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
+Require Import Crypto.Curves.PointFormats.
+Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.NumTheoryUtil.
+Require Import Bedrock.Word.
+Require Import VerdiTactics.
+Require Import Decidable.
+Require Import Omega.
+
+Local Open Scope nat_scope.
+Definition q : Z := (2 ^ 255 - 19)%Z.
+Lemma prime_q : prime q. Admitted.
+Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed.
+
+Definition a : F q := opp 1%F.
+
+(* TODO (jadep) : make the proofs about a and d more general *)
+Lemma nonzero_a : a <> 0%F.
+Proof.
+  unfold a.
+  intro eq_opp1_0.
+  apply (@Fq_1_neq_0 q prime_q).
+  rewrite <- (F_opp_spec 1%F).
+  rewrite eq_opp1_0.
+  symmetry; apply F_add_0_r.
+Qed.
+
+Ltac q_bound := pose proof two_lt_q; omega.
+Lemma square_a : isSquare a.
+Proof.
+  Lemma q_1mod4 : (q mod 4 = 1)%Z. reflexivity. Qed.
+  intros.
+  pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square.
+  destruct minus1_square as [b b_id].
+  apply square_Zmod_F.
+  exists b; rewrite b_id.
+  unfold a.
+  rewrite opp_ZToField.
+  rewrite FieldToZ_ZToField.
+  rewrite Z.mod_small; q_bound.
+Qed.
+
+(* TODO *)
+(* d = .*)
+Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
+Lemma nonsquare_d : forall x, (x^2 <> d)%F. Admitted.
+(* Definition nonsquare_d : (forall x, x^2 <> d) := euler_criterion_if d. <-- currently not computable in reasonable time *)
+
+Instance TEParams : TwistedEdwardsParams := {
+  q := q;
+  prime_q := prime_q;
+  two_lt_q := two_lt_q;
+  a := a;
+  nonzero_a := nonzero_a;
+  square_a := square_a;
+  d := d;
+  nonsquare_d := nonsquare_d
+}.
+
+  Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n.
+  Admitted.
+
+  Definition b := 256.
+  Lemma b_valid : (2 ^ (b - 1) > Z.to_nat CompleteEdwardsCurve.q)%nat.
+  Proof.
+    replace (CompleteEdwardsCurve.q) with q by reflexivity.
+    unfold q, gt.
+    replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
+      by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat).
+    rewrite <- Z2Nat.inj_lt; compute; congruence.
+  Qed.
+
+  Definition c := 3.
+  Lemma c_valid : c = 2 \/ c = 3.
+  Proof.
+    right; auto.
+  Qed.
+
+  Definition n := b - 2.
+  Lemma n_ge_c : n >= c.
+  Proof.
+    unfold n, c, b; omega.
+  Qed.
+  Lemma n_le_b : n <= b.
+  Proof.
+    unfold n, b; omega.
+  Qed.
+
+  Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z.
+  Lemma prime_l : prime (Z.of_nat l). Admitted.
+  Lemma l_odd : l > 2.
+  Proof.
+    unfold l, proj1_sig.
+    rewrite Z2Nat.inj_add; try omega.
+    apply lt_plus_trans.
+    compute; omega.
+  Qed.
+  Lemma l_bound : l < pow2 b.
+  Proof.
+    rewrite Zpow_pow2.
+    unfold l.
+    rewrite <- Z2Nat.inj_lt; compute; congruence.
+  Qed.
+
+  Definition H : forall n : nat, word n -> word (b + b). Admitted.
+  Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
+  Definition B_nonzero : B <> zero. Admitted.
+  Definition l_order_B : scalarMult l B = zero. Admitted.
+  Definition FqEncoding : encoding of F q as word (b - 1). Admitted.
+  Definition FlEncoding : encoding of F (Z.of_nat l) as word b. Admitted.
+  Definition PointEncoding : encoding of point as word b. Admitted.
+
+Instance x : EdDSAParams := {
+  E := TEParams;
+  b := b;
+  H := H;
+  c := c;
+  n := n;
+  B := B;
+  l := l;
+  FqEncoding := FqEncoding;
+  FlEncoding := FlEncoding;
+  PointEncoding := PointEncoding;
+ 
+  b_valid := b_valid;
+  c_valid := c_valid;
+  n_ge_c := n_ge_c;
+  n_le_b := n_le_b;
+  B_not_identity := B_nonzero;
+  l_prime := prime_l;
+  l_odd := l_odd;
+  l_order_B := l_order_B
+}.
+
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v
index d037339b4..242661bc5 100644
--- a/src/Specific/EdDSA25519.v
+++ b/src/Specific/EdDSA25519.v
@@ -89,13 +89,15 @@ Module EdDSA25519_Params <: EdDSAParams.
       + auto.
       + pose proof q_odd; unfold q in *; omega.
       + apply div2_p_1mod4; auto.
-      + apply nonzero_range; auto.
+      + rewrite GF_Zmod.
+        apply nonzero_range; auto.
       + rewrite GFexp_Zpow in A by (auto || apply Z_div_pos; prime_bound).
         rewrite inject_mod_eq in A.
         apply gf_eq in A.
         replace (GFToZ 1) with 1%Z in A by auto.
         rewrite GFToZ_inject in A.
         rewrite Z.mod_mod in A by auto.
+        rewrite GF_Zmod.
         exact A.
     } {
       rewrite GFexp_Zpow by first [apply Z.div_pos; pose proof q_odd; omega | auto].
@@ -104,7 +106,8 @@ Module EdDSA25519_Params <: EdDSAParams.
       rewrite GFToZ_inject.
       apply euler_criterion; auto.
       + apply nonzero_range; auto.
-      + apply square_Zmod_GF; auto.
+      + rewrite <- GF_Zmod.
+        apply square_Zmod_GF; auto.
     }
   Qed.