moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from CompleteEdwardsCurve, where the precondition is not in scope.

4 files changed, 38 insertions, 27 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index a6b61d2dd..dd40a4510 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -93,29 +93,4 @@ Section CompleteEdwardsCurveTheorems.
       auto using d_y2_a_nonzero.
   Qed.
 
-  (* TODO : move to ModularArithmeticTheorems? *)
-  Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F.
-
-  Lemma solve_sqrt_valid : forall (p : point),
-    sqrt_valid (solve_for_x2 (snd (proj1_sig p))).
-  Admitted.
-
-  Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
-    onCurve (sqrt_mod_q (solve_for_x2 y), y).
-  Proof.
-    intros.
-    unfold sqrt_valid in *.
-    apply solve_correct; auto.
-  Qed.
-
-  Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
-    onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y).
-  Proof.
-    intros y sqrt_valid_x2.
-    unfold sqrt_valid in *.
-    apply solve_correct.
-    rewrite <- sqrt_valid_x2 at 2.
-    ring.
-  Qed.
-
 End CompleteEdwardsCurveTheorems.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index aa86c395b..9fdc01d0d 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -197,7 +197,7 @@ Section VariousModPrime.
   Proof.
     intros; field. (* TODO: Warning: Collision between bound variables ... *)
   Qed.
- 
+
   Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0).
   Proof.
     split; intro A.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 04e6a5fc2..c12799751 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -115,7 +115,10 @@ Qed.
 Definition FlEncoding : encoding of F (Z.of_nat l) as word b :=
   @modular_word_encoding (Z.of_nat l) b l_pos l_bound.
 
-Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding.
+Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
+(* Admitting until field exponentiation can compute this in reasonable time *)
+Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1)%F. Admitted.
+Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid.
 
 Definition H : forall n : nat, word n -> word (b + b). Admitted.
 Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index ea662a6b7..18097b676 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -21,6 +21,39 @@ Section PointEncoding.
      div (@Fmorph_div_theory q),
      power_tac (@Fpower_theory q) [Fexp_tac]).
 
+  Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F.
+
+  Lemma solve_sqrt_valid : forall (p : point),
+    sqrt_valid (solve_for_x2 (snd (proj1_sig p))).
+  Proof.
+    intros.
+    destruct p as [[x y] onCurve_xy]; simpl.
+    rewrite (solve_correct x y) in onCurve_xy.
+    rewrite <- onCurve_xy.
+    unfold sqrt_valid.
+    eapply sqrt_mod_q_valid; eauto.
+    unfold isSquare; eauto.
+    Grab Existential Variables. eauto.
+  Qed.
+
+  Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
+    onCurve (sqrt_mod_q (solve_for_x2 y), y).
+  Proof.
+    intros.
+    unfold sqrt_valid in *.
+    apply solve_correct; auto.
+  Qed.
+
+  Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) ->
+    onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y).
+  Proof.
+    intros y sqrt_valid_x2.
+    unfold sqrt_valid in *.
+    apply solve_correct.
+    rewrite <- sqrt_valid_x2 at 2.
+    ring.
+  Qed.
+
 Definition sign_bit (x : F q) := (wordToN (enc (opp x)) <? wordToN (enc x))%N.
 Definition point_enc (p : point) : word (S sz) := let '(x,y) := proj1_sig p in
   WS (sign_bit x) (enc y).