1 files changed, 84 insertions, 170 deletions

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..5314ee37c 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,186 +1,100 @@
-Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
+Require Import Crypto.Algebra Crypto.Tactics.Nsatz.
 
-Require Import Crypto.Spec.ModularArithmetic.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Local Open Scope F_scope.
-  
+Generalizable All Variables.
 Section Pre.
-  Context {q : BinInt.Z}.
-  Context {a : F q}.
-  Context {d : F q}.
-  Context {prime_q : Znumtheory.prime q}.
-  Context {two_lt_q : 2 < q}.
-  Context {a_nonzero : a <> 0}.
-  Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
-  Context {d_nonsquare : forall x, x^2 <> d}.
-
-  Add Field Ffield_Z : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Notation "0" := zero.  Local Notation "1" := one.
+  Local Infix "+" := add. Local Infix "*" := mul.
+  Local Infix "-" := sub. Local Infix "/" := div.
+  Local Notation "x '^' 2" := (x*x) (at level 30).
+
+  Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
+
+  Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}.
+  Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}.
+  Context {char_gt_2 : 1+1 <> 0}.
+
   (* the canonical definitions are in Spec *)
-  Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
-  Local Notation unifiedAdd' P1' P2' := (
-    let '(x1, y1) := P1' in
-    let '(x2, y2) := P2' in
-    (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
-  ).
-  
-  Lemma char_gt_2 : ZToField 2 <> (0: F q).
-    intro; find_injection.
-    pose proof two_lt_q.
-    rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega.
-  Qed.
+  Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
+  Definition unifiedAdd' (P1' P2':F*F) : F*F :=
+    let (x1, y1) := P1' in
+    let (x2, y2) := P2' in
+    pair (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))).
 
-  Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
-  Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
-  
-  Ltac whatsNotZero :=
-    repeat match goal with
-    | [H: ?lhs = ?rhs |- _ ] =>
-        match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end;
-        assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
-    | [H: ?lhs = ?rhs |- _ ] =>
-        match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end;
-        assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0)
-    | [H: (?a^?p)%F <> 0 |- _ ] =>
-        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
-        let Y:=fresh in let Z:=fresh in try (
-          assert (p <> 0%N) as Z by (intro Y; inversion Y);
-          assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0);
-          clear Z)
-    | [H: (?a*?b)%F <> 0 |- _ ] =>
-        match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end;
-        assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0)
-    | [H: (?a*?b)%F <> 0 |- _ ] =>
-        match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end;
-        assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0)
-    end.
+  Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *.
 
   Lemma edwardsAddComplete' x1 y1 x2 y2 :
-    onCurve (x1, y1) ->
-    onCurve (x2, y2) ->
+    onCurve (pair x1 y1) ->
+    onCurve (pair x2 y2) ->
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
-    intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
-  
-    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
-    destruct a_square as [sqrt_a a_square'].
-    rewrite <-a_square' in *.
-  
-    (* Furthermore... *)
-    pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
-    rewrite Hc2 in Heqt at 2.
-    replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2))
-       with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field.
-    rewrite Hcontra in Heqt.
-    replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
-    rewrite <-Hc1 in Heqt.
-  
-    (* main equation for both potentially nonzero denominators *)
-    destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
-      try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
-        assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 =
-                 f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2)
-                   (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field;
-        rewrite Hcontra in Heqw1;
-        replace (1 * y1^2) with (y1^2) in * by field;
-        rewrite <- Heqt in *;
-        assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 /
-                                 (x1 * y1 * (f (sqrt_a * x2)  y2))^2)
-                                 by (rewriteAny; field; auto);
-        match goal with [H: d = (?n^2)/(?l^2) |- _ ] =>
-            destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
-        end
-      end.
-  
-    assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
-  
-    replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
-  
-    (* contradiction: product of nonzero things is zero *)
-    destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
-    destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
-    apply Ha_nonzero; field.
+    unfold onCurve, not; use_sqrt_a; intros.
+    destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0);
+      lazymatch goal with
+      | [H: not (eq (?f (sqrt_a * x2)  y2) 0) |- _ ]
+        => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
+                                           /(f (sqrt_a * x2) y2   *   x1 * y1           ))
+      | _ => apply a_nonzero
+      end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict.
   Qed.
 
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
-    onCurve (x1, y1) ->
-    onCurve (x2, y2) ->
-    (1 + d*x1*x2*y1*y2) <> 0.
-  Proof.
-    intros Hc1 Hc2; simpl in Hc1, Hc2.
-    intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H].
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
-    - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
-      intro Hz; rewrite Hz in H; intuition.
-  Qed.
-  
+    onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0.
+  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
-    onCurve (x1, y1) ->
-    onCurve (x2, y2) ->
-    (1 - d*x1*x2*y1*y2) <> 0.
-  Proof.
-    intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H].
-    - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto.
-    - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
-      intro Hz; rewrite Hz in H; apply H; field.
-  Qed.
-  
-  Definition zeroOnCurve : onCurve (0, 1).
-    simpl. field.
-  Qed.
-  
-  Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
-    (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
-    onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
+    onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0.
+  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
+
+  Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed.
+
+  Lemma unifiedAdd'_onCurve : forall P1 P2,
+    onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
   Proof.
-    (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
-      * c=1 and an extra a in front of x^2 *) 
-  
-    injection H; clear H; intros.
-  
-    Ltac t x1 y1 x2 y2 :=
-      assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
-             = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
-      assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
-             = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
-    t x1 y1 x2 y2; t x2 y2 x1 y1.
-  
-    remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
-      (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
-    assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
-    assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +(
-    (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
-     y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
-    replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-  
-    match goal with [ |- ?x = 1 ] => replace x with
-    ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
-     ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
-      d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/
-    ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end.
-    - rewrite <-HT1, <-HT2; field; rewrite HT1.
-      replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2))
-      with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field.
-      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
-        edwardsAddCompleteMinus, edwardsAddCompletePlus.
-    - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2)
-         with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2))
-           by field;
-      auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
-        edwardsAddCompleteMinus, edwardsAddCompletePlus.
+    unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2.
+    field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus.
   Qed.
-  
-  Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
-    onCurve (unifiedAdd' P1 P2).
+End Pre.
+
+Import Group Ring Field.
+
+(* TODO: move -- this does not need to be defined before [point] *)
+Section RespectsFieldHomomorphism.
+  Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}.
+  Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}.
+  Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
+  Context {phi:F->K} `{@is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}.
+  Context {A D:F} {a d:K} {a_ok:phi A=a} {d_ok:phi D=d}.
+
+  Let phip  := fun (P':F*F) => let (x, y) := P' in (phi x, phi y).
+
+  Let eqp := fun (P1' P2':K*K) =>
+    let (x1, y1) := P1' in
+    let (x2, y2) := P2' in
+    and (eq x1 x2) (eq y1 y2).
+
+  Create HintDb field_homomorphism discriminated.
+  Hint Rewrite
+       homomorphism_one
+       homomorphism_add
+       homomorphism_sub
+       homomorphism_mul
+       homomorphism_div
+       a_ok
+       d_ok
+       : field_homomorphism.
+
+  Lemma morphism_unidiedAdd' : forall P Q:F*F,
+    eqp
+      (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q))
+            (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)).
   Proof.
-    intros; destruct P1, P2.
-    remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
-    eapply unifiedAdd'_onCurve'; eauto.
+    intros [x1 y1] [x2 y2].
+    cbv [unifiedAdd' phip eqp];
+      apply conj;
+      (rewrite_strat topdown hints field_homomorphism); reflexivity.
   Qed.
-End Pre.
\ No newline at end of file
+End RespectsFieldHomomorphism.
\ No newline at end of file