Edwards coordinates precomputed addition formula

3 files changed, 210 insertions, 134 deletions

diff --git a/src/Curves/Edwards/XYZT.v b/src/Curves/Edwards/XYZT.v
deleted file mode 100644
index 3604e9b2e..000000000
--- a/src/Curves/Edwards/XYZT.v
+++ /dev/null
@@ -1,134 +0,0 @@
-Require Import Coq.Classes.Morphisms.
-
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs.
-
-Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
-Require Export Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.UniquePose.
-
-Module Extended.
-  Section ExtendedCoordinates.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
-            {Feq_dec:DecidableRel Feq}.
-    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
-    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
-    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^ 2" := (x*x).
-
-    Context {a d: F}
-            {nonzero_a : a <> 0}
-            {square_a : exists sqrt_a, sqrt_a^2 = a}
-            {nonsquare_d : forall x, x^2 <> d}.
-    Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
-
-    Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
-    (** [Extended.point] represents a point on an elliptic curve using extended projective
-     * Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
-    Definition point := { P | let '(X,Y,Z,T) := P in
-                              a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
-                              /\ X * Y = Z * T
-                              /\ Z <> 0 }.
-    Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
-    Definition eq (P1 P2:point) :=
-        let '(X1, Y1, Z1, _) := coordinates P1 in
-        let '(X2, Y2, Z2, _) := coordinates P2 in
-        Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
-
-    Ltac t_step :=
-      match goal with
-      | |- Proper _ _ => intro
-      | _ => progress intros
-      | _ => progress destruct_head' prod
-      | _ => progress destruct_head' @E.point
-      | _ => progress destruct_head' point
-      | _ => progress destruct_head' and
-      | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in *
-      | |- _ /\ _ => split | |- _ <-> _ => split
-      end.
-    Ltac t := repeat t_step; Field.fsatz.
-
-    Global Instance Equivalence_eq : Equivalence eq.
-    Proof using Feq_dec field nonzero_a. split; repeat intro; t. Qed.
-    Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
-    Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined.
-
-    Program Definition from_twisted (P:Epoint) : point :=
-      let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy).
-    Next Obligation. t. Qed.
-    Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted.
-    Proof using Type. cbv [from_twisted]; t. Qed.
-
-    Program Definition to_twisted (P:point) : Epoint :=
-      let XYZT := coordinates P in let T := snd XYZT in
-      let XYZ  := fst XYZT in      let Z := snd XYZ in
-      let XY   := fst XYZ in       let Y := snd XY in
-      let X    := fst XY in
-      let iZ := Finv Z in ((X*iZ), (Y*iZ)).
-    Next Obligation. t. Qed.
-    Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted.
-    Proof using Type. cbv [to_twisted]; t. Qed.
-
-    Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P.
-    Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
-    Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
-    Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
-
-    Program Definition zero : point := (0, 1, 1, 0).
-    Next Obligation. t. Qed.
-
-    Program Definition opp P : point :=
-      match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end.
-    Next Obligation. t. Qed.
-
-    Section TwistMinusOne.
-      Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}.
-      Program Definition m1add
-              (P1 P2:point) : point :=
-        match coordinates P1, coordinates P2 return F*F*F*F with
-          (X1, Y1, Z1, T1), (X2, Y2, Z2, T2) =>
-          let A := (Y1-X1)*(Y2-X2) in
-          let B := (Y1+X1)*(Y2+X2) in
-          let C := T1*twice_d*T2 in
-          let D := Z1*(Z2+Z2) in
-          let E := B-A in
-          let F := D-C in
-          let G := D+C in
-          let H := B+A in
-          let X3 := E*F in
-          let Y3 := G*H in
-          let T3 := E*H in
-          let Z3 := F*G in
-          (X3, Y3, Z3, T3)
-        end.
-      Next Obligation.
-        match goal with
-        | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
-          => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2)))
-        end; t.
-      Qed.
-
-      Global Instance isomorphic_commutative_group_m1 :
-        @Group.isomorphic_commutative_groups
-          Epoint E.eq
-            (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d))
-            (E.zero(nonzero_a:=nonzero_a))
-            (E.opp(nonzero_a:=nonzero_a))
-          point eq m1add zero opp
-          from_twisted to_twisted.
-      Proof.
-        eapply Group.commutative_group_by_isomorphism; try exact _.
-        par: abstract
-               (cbv [to_twisted from_twisted zero opp m1add]; intros;
-                repeat match goal with
-                       | |- context[E.add ?P ?Q] =>
-                         unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q)) end;
-                t).
-      Qed.
-    End TwistMinusOne.
-  End ExtendedCoordinates.
-End Extended.
diff --git a/src/Curves/Edwards/XYZT/Basic.v b/src/Curves/Edwards/XYZT/Basic.v
new file mode 100644
index 000000000..1d327cd40
--- /dev/null
+++ b/src/Curves/Edwards/XYZT/Basic.v
@@ -0,0 +1,132 @@
+Require Import Coq.Classes.Morphisms.
+
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs.
+
+Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
+Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.UniquePose.
+
+Section ExtendedCoordinates.
+  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+          {Feq_dec:DecidableRel Feq}.
+  Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+  Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+  Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+  Local Notation "x ^ 2" := (x*x).
+
+  Context {a d: F}
+          {nonzero_a : a <> 0}
+          {square_a : exists sqrt_a, sqrt_a^2 = a}
+          {nonsquare_d : forall x, x^2 <> d}.
+  Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
+
+  Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
+  (** [Extended.point] represents a point on an elliptic curve using extended projective
+   * Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
+  Definition point := { P | let '(X,Y,Z,T) := P in
+                            a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
+                            /\ X * Y = Z * T
+                            /\ Z <> 0 }.
+  Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
+  Definition eq (P1 P2:point) :=
+    let '(X1, Y1, Z1, _) := coordinates P1 in
+    let '(X2, Y2, Z2, _) := coordinates P2 in
+    Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
+
+  Ltac t_step :=
+    match goal with
+    | |- Proper _ _ => intro
+    | _ => progress intros
+    | _ => progress destruct_head' prod
+    | _ => progress destruct_head' @E.point
+    | _ => progress destruct_head' point
+    | _ => progress destruct_head' and
+    | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in *
+    | |- _ /\ _ => split | |- _ <-> _ => split
+    end.
+  Ltac t := repeat t_step; Field.fsatz.
+
+  Global Instance Equivalence_eq : Equivalence eq.
+  Proof using Feq_dec field nonzero_a. split; repeat intro; t. Qed.
+  Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
+  Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined.
+
+  Program Definition from_twisted (P:Epoint) : point :=
+    let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy).
+  Next Obligation. t. Qed.
+  Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted.
+  Proof using Type. cbv [from_twisted]; t. Qed.
+
+  Program Definition to_twisted (P:point) : Epoint :=
+    let XYZT := coordinates P in let T := snd XYZT in
+                                 let XYZ  := fst XYZT in      let Z := snd XYZ in
+                                                              let XY   := fst XYZ in       let Y := snd XY in
+                                                                                           let X    := fst XY in
+                                                                                           let iZ := Finv Z in ((X*iZ), (Y*iZ)).
+  Next Obligation. t. Qed.
+  Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted.
+  Proof using Type. cbv [to_twisted]; t. Qed.
+
+  Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P.
+  Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
+  Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
+  Proof using Type. cbv [to_twisted from_twisted]; t. Qed.
+
+  Program Definition zero : point := (0, 1, 1, 0).
+  Next Obligation. t. Qed.
+
+  Program Definition opp P : point :=
+    match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end.
+  Next Obligation. t. Qed.
+
+  Section TwistMinusOne.
+    Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}.
+    Program Definition m1add
+            (P1 P2:point) : point :=
+      match coordinates P1, coordinates P2 return F*F*F*F with
+        (X1, Y1, Z1, T1), (X2, Y2, Z2, T2) =>
+        let A := (Y1-X1)*(Y2-X2) in
+        let B := (Y1+X1)*(Y2+X2) in
+        let C := T1*twice_d*T2 in
+        let D := Z1*(Z2+Z2) in
+        let E := B-A in
+        let F := D-C in
+        let G := D+C in
+        let H := B+A in
+        let X3 := E*F in
+        let Y3 := G*H in
+        let T3 := E*H in
+        let Z3 := F*G in
+        (X3, Y3, Z3, T3)
+      end.
+    Next Obligation.
+      match goal with
+      | [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
+        => pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2)))
+      end; t.
+    Qed.
+
+    Global Instance isomorphic_commutative_group_m1 :
+      @Group.isomorphic_commutative_groups
+        Epoint E.eq
+        (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d))
+        (E.zero(nonzero_a:=nonzero_a))
+        (E.opp(nonzero_a:=nonzero_a))
+        point eq m1add zero opp
+        from_twisted to_twisted.
+    Proof.
+      eapply Group.commutative_group_by_isomorphism; try exact _.
+      par: abstract
+             (cbv [to_twisted from_twisted zero opp m1add]; intros;
+              repeat match goal with
+                     | |- context[E.add ?P ?Q] =>
+                       unique pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _  (proj2_sig P)  _ _  (proj2_sig Q)) end;
+              t).
+    Qed.
+  End TwistMinusOne.
+End ExtendedCoordinates.
diff --git a/src/Curves/Edwards/XYZT/Precomputed.v b/src/Curves/Edwards/XYZT/Precomputed.v
new file mode 100644
index 000000000..6b925c020
--- /dev/null
+++ b/src/Curves/Edwards/XYZT/Precomputed.v
@@ -0,0 +1,78 @@
+Require Import Crypto.Util.Decidable Crypto.Util.Notations Crypto.Algebra.Hierarchy.
+
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.XYZT.Basic.
+Require Import Coq.Classes.Morphisms.
+
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Algebra.Field.
+
+Section ExtendedCoordinates.
+  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+          {Feq_dec:DecidableRel Feq}.
+
+  Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+  Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+  Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+  Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+  Local Notation "x ^ 2" := (x*x).
+
+  Context {a d: F}
+          {nonzero_a : a <> 0}
+          {square_a : exists sqrt_a, sqrt_a^2 = a}
+          {nonsquare_d : forall x, x^2 <> d}.
+  Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
+
+  Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
+  Definition precomputed_point : Type := F*F*F.
+
+  Definition of_twisted (P:Epoint) :=
+    let '(x, y) := E.coordinates P in
+    (y+x, y-x, (let xy := x*y in xy+xy)*d).
+
+  Section TwistMinusOne.
+    Context {a_eq_minus1:a = Fopp 1}.
+    Definition m1add_precomputed_coordinates (P:F*F*F*F) (Q:precomputed_point) : F*F*F*F :=
+    let '(X1, Y1, Z1, T1) := P in
+    let '(ypx2, ymx2, xy2d2) := Q in
+    let YpX1 := Y1+X1 in
+    let YmX1 := Y1-X1 in
+    let A := YpX1*ypx2 in
+    let B := YmX1*ymx2 in
+    let C := xy2d2*T1 in
+    let D := Z1+Z1 in
+    let X3 := A-B in
+    let Y3 := A+B in
+    let Z3 := D+C in
+    let T3 := D-C in
+    (* X/Z, Y/T = x, y *)
+    let X3 := X3*T3 in
+    let Y3 := Y3*Z3 in
+    let Z3 := T3*Z3 in
+    let T3 := X3*Y3 in
+    (X3, Y3, Z3, T3).
+
+    Create HintDb points_as_coordinates discriminated.
+    Hint Unfold XYZT.Basic.point XYZT.Basic.coordinates XYZT.Basic.from_twisted XYZT.Basic.m1add
+         E.point E.coordinates m1add_precomputed_coordinates of_twisted precomputed_point : points_as_coordinates.
+    Local Notation m1add := (Basic.m1add(nonzero_a:=nonzero_a)(square_a:=square_a)(a_eq_minus1:=a_eq_minus1)(nonsquare_d:=nonsquare_d)(k_eq_2d:=reflexivity _)).
+    Local Notation XYZT_of_twisted := (Basic.from_twisted(nonzero_a:=nonzero_a)(d:=d)).
+    Lemma m1add_precomputed_coordinates_correct P Q :
+      let '(X1, Y1, Z1, T1) := m1add_precomputed_coordinates (XYZT.Basic.coordinates P) (of_twisted Q) in
+      let '(X2, Y2, Z2, T2) := coordinates (m1add P (XYZT_of_twisted Q)) in
+            Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.
+    Proof.
+      repeat match goal with
+             | _ => progress autounfold with points_as_coordinates in *
+             | _ => progress destruct_head' @prod
+             | _ => progress destruct_head' @sig
+             | _ => progress destruct_head' @and
+             | _ => progress cbv [proj1_sig fst snd]
+             | |- _ /\ _ => split
+             end; fsatz.
+    Qed.
+  End TwistMinusOne.
+End ExtendedCoordinates.
\ No newline at end of file