From ac694189f4b45eb7278d08a919c4a7e118ed503e Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sun, 20 Mar 2016 18:59:20 -0400
Subject: Ed25519: d is nonsquare

---
 src/ModularArithmetic/PrimeFieldTheorems.v | 12 +++++++++++-
 src/Spec/Ed25519.v                         | 30 +++++++++++++++++++-----------
 2 files changed, 30 insertions(+), 12 deletions(-)

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 444971901..29eba0d01 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -294,7 +294,7 @@ Section VariousModPrime.
     }
   Qed.
 
-  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
+  Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q),
     if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1))
     then (isSquare a) else (forall b, b ^ 2 <> a).
   Proof.
@@ -309,6 +309,16 @@ Section VariousModPrime.
       apply euler_criterion_F in a_square; auto.
   Qed.
 
+  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
+    if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1)
+    then (isSquare a) else (forall b, b ^ 2 <> a).
+  Proof.
+    intros.
+    pose proof (euler_criterion_if' a q_odd) as H.
+    unfold F_eqb in *; simpl in *.
+    rewrite !Zmod_small, !@FieldToZ_pow_efficient in H by omega; eauto.
+  Qed.
+
   Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
   Proof.
     intros ? ? squares_eq.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 92c36b56c..d6d02b93f 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -43,11 +43,26 @@ Proof.
   rewrite Z.mod_small; q_bound.
 Qed.
 
-(* TODO *)
-(* d = .*)
+Hint Rewrite
+ @FieldToZ_add
+ @FieldToZ_mul
+ @FieldToZ_opp
+ @FieldToZ_inv_efficient
+ @FieldToZ_pow_efficient
+ @FieldToZ_ZToField
+ @Zmod_mod
+ : ZToField.
+
 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 *)
+Lemma nonsquare_d : forall x, (x^2 <> d)%F.
+  pose proof @euler_criterion_if q prime_q d two_lt_q.
+  match goal with
+    [H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H]
+  end.
+  unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..].
+  vm_compute. (* 10s *)
+  exact eq_refl.
+Qed. (* 10s *)
 
 Instance TEParams : TwistedEdwardsParams := {
   q := q;
@@ -117,13 +132,6 @@ Definition FlEncoding : encoding of F (Z.of_nat l) as word b :=
 
 Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
 
-Hint Rewrite
- @FieldToZ_pow_efficient
- @FieldToZ_ZToField
- @FieldToZ_opp
- @FieldToZ_ZToField : ZToField
- .
-
 Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F.
 Proof.
   apply F_eq.
-- 
cgit v1.2.3