PointFormats: all Edwards25519 points are onCurve

3 files changed, 296 insertions, 306 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index 8dc513a28..edcf6a24c 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -2,14 +2,36 @@ Require Import Zpower ZArith Znumtheory.
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Crypto.Curves.PointFormats.
 
-Module Curve25519.
-  Import M.
-  Module Import GT := GaloisTheory M.
-  Local Open Scope GF_scope.
+Definition two_255_19 := 2^255 - 19. (* <http://safecurves.cr.yp.to/primeproofs.html> *)
+Fact two_255_19_prime : prime two_255_19. Admitted.
+Module Modulus25519 <: Modulus.
+  Definition modulus := exist _ two_255_19 two_255_19_prime.
+End Modulus25519.
+
+Module Curve25519Params <: TwistedEdwardsParams Modulus25519 <: Minus1Params Modulus25519.
+  Module Import GFDefs := GaloisDefs Modulus25519.
+  Coercion inject : Z >-> GF.
+
+  Definition a : GF := -1.
+  Definition d : GF := -121665 / 121666.
+
+  Lemma a_nonzero : a <> 0.
+  Proof.
+    discriminate.
+  Qed.
+
+  Lemma a_square : exists x, x * x = a.
+  Proof.
+    unfold a.
+    exists 19681161376707505956807079304988542015446066515923890162744021073123829784752.
+    (* vm_compute runs out of memory. *) 
+  Admitted.
 
-  Definition A : GF := ZToGF 486662.
-  Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF.
+  Lemma  d_nonsquare : forall x, x * x <> d.
+    (* <https://en.wikipedia.org/wiki/Euler%27s_criterion> *)
+  Admitted.
 
+  Definition A : GF := 486662.
   (* Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. *)
 
   (* Module-izing Twisted was a breaking change
@@ -24,7 +46,8 @@ Module Curve25519.
 
   *)
 
-  Definition basepointY := ZToGF 4 / ZToGF 5.
-  (* TODO(andreser): implement (in PointFormats) recoverX from <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
-End Curve25519.
+  Definition basepointY := 4 / 5.
+End Curve25519Params.
 
+Module Edwards25519 := CompleteTwistedEdwardsCurve Modulus25519 Curve25519Params.
+Module Edwards25519Minus1Twisted := Minus1Format Modulus25519 Curve25519Params.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 4c5572ea7..6db178aea 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -1,14 +1,14 @@
-
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Tactics.VerdiTactics.
+Require Import Logic.Eqdep_dec.
 
-Module TwistedEdwardsDefs (M : Modulus).
+Module GaloisDefs (M : Modulus).
   Module Export GT := GaloisTheory M.
   Open Scope GF_scope.
-End TwistedEdwardsDefs.
+End GaloisDefs.
 
 Module Type TwistedEdwardsParams (M : Modulus).
-  Module Export Defs := TwistedEdwardsDefs M.
+  Module Export GFDefs := GaloisDefs M.
   Parameter a : GF.
   Axiom a_nonzero : a <> 0.
   Axiom a_square : exists x, x * x = a.
@@ -22,304 +22,293 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
   * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
   * <https://eprint.iacr.org/2015/677.pdf>
   *)
-  Record point := mkPoint {projX : GF; projY : GF}.
-  Notation "'(' x ',' y ')'" := (mkPoint x y). 
-  Definition zero := (0, 1).
-  Definition unifiedAdd (P1 P2 : point) : point :=
-    let x1 := projX P1 in
-    let y1 := projY P1 in
-    let x2 := projX P2 in
-    let y2 := projY P2 in
-    mkPoint
-      ((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2))
-      ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))
-    .
-
-  Definition onCurve : point -> Prop := fun P =>
-    let x := projX P in
-    let y := projY P in
-    a*x^2 + y^2 = 1 + d*x^2*y^2.
-  
+  Definition onCurve P := let '(x,y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2.
+  Definition point := { P | onCurve P}.
+  Definition mkPoint := exist onCurve.
+
+  Definition projX (P:point) := fst (proj1_sig P).
+  Definition projY (P:point) := snd (proj1_sig P).
+
+  Definition checkOnCurve x y : if Zbool.Zeq_bool (a*x^2 + y^2) (1 + d*x^2*y^2) then point else True.
+    break_if. exists (x, y). exact (GFdecidable  _ _ Heqb). trivial.
+  Defined.
+  Hint Unfold onCurve mkPoint.
+
+  Definition zero : point. exists (0, 1).
+    abstract (unfold onCurve; ring).
+  Defined.
+
+  Definition unifiedAdd' (P1' P2' : (GF*GF)) :=
+    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))).
+
+  Definition unifiedAdd (P1 P2 : point) : point. refine (
+    let 'exist P1' pf1 := P1 in
+    let 'exist P2' pf2 := P2 in
+    mkPoint (unifiedAdd' P1' P2') _).
+  Proof.
+    destruct P1' as [x1 y1], P2' as [x2 y2]; unfold unifiedAdd', onCurve.
+    admit. (* field will likely work here, but I have not done this by hand *)
+  Defined.
   Local Infix "+" := unifiedAdd.
 
-  (* Naive implementation *)
-  Fixpoint scalarMultSpec (n:nat) (P : point) : point :=
+  Fixpoint scalarMult (n:nat) (P : point) : point :=
     match n with 
     | O => zero
-    | S n' => P + scalarMultSpec n' P
+    | S n' => P + scalarMult n' P
     end
   .
-
-  (* TODO: non-naive *)
-  Definition scalarMult := scalarMultSpec.
-  
 End CompleteTwistedEdwardsCurve.
 
+
 Module Type CompleteTwistedEdwardsPointFormat (M : Modulus) (Import P : TwistedEdwardsParams M).
   Module Curve := CompleteTwistedEdwardsCurve M P.
   Parameter point : Type.
-  Parameter mkPoint : forall (x y:GF), point.
-  Parameter projX : point -> GF.
-  Parameter projY : point -> GF.
+  Parameter encode : (GF*GF) -> point.
+  Parameter decode : point -> (GF*GF).
   Parameter unifiedAdd : point -> point -> point.
 
-  Parameter rep : point -> Curve.point -> Prop.
+  Parameter rep : point -> (GF*GF) -> Prop.
   Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-  Axiom mkPoint_rep: forall x y, mkPoint x y ~= Curve.mkPoint x y.
+
+  Axiom encode_rep: forall P, encode P ~= P.
+  Axiom decode_rep : forall P rP, P ~= rP -> decode P = rP.
   Axiom unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ ->
-    P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ).
-  Axiom projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP.
-  Axiom projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP.
+    P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ).
 End CompleteTwistedEdwardsPointFormat.
 
 Module CompleteTwistedEdwardsFacts (M : Modulus) (Import P : TwistedEdwardsParams M).
   Module Import Curve := CompleteTwistedEdwardsCurve M P.
-  Lemma twistedAddCompletePlus : forall (P1 P2:point)
-    (oc1:onCurve P1) (oc2:onCurve P2),
-    let x1 := projX P1 in
-    let y1 := projY P1 in
-    let x2 := projX P2 in
-    let y2 := projY P2 in
+  Lemma twistedAddCompletePlus : forall (P1 P2:point),
+    let '(x1, y1) := proj1_sig P1 in
+    let '(x2, y2) := proj1_sig P2 in
     (1 + d*x1*x2*y1*y2) <> 0.
     (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
   Admitted.
-  Lemma twistedAddCompleteMinus : forall (P1 P2:point)
-    (oc1:onCurve P1) (oc2:onCurve P2),
-    let x1 := projX P1 in
-    let y1 := projY P1 in
-    let x2 := projX P2 in
-    let y2 := projY P2 in
+  Lemma twistedAddCompleteMinus : forall (P1 P2:point),
+    let '(x1, y1) := proj1_sig P1 in
+    let '(x2, y2) := proj1_sig P2 in
     (1 - d*x1*x2*y1*y2) <> 0.
     (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
   Admitted.
 
+  Lemma point_eq : forall x1 x2 y1 y2,
+    x1 = x2 -> y1 = y2 ->
+    forall p1 p2,
+    mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2.
+  Proof.
+    intros; subst; f_equal.
+    apply (UIP_dec). (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
+    admit. (* GF_eq_dec *)
+  Qed.
+  Hint Resolve point_eq.
+
   Hint Unfold unifiedAdd onCurve.
   Ltac twisted := autounfold; intros;
-                  repeat match goal with
-                             | [ x : point |- _ ] => destruct x
-                         end; simpl; repeat (ring || f_equal); field.
+                  repeat (match goal with
+                             | [ x : point |- _ ] => destruct x; unfold onCurve in *
+                             | [ x : (GF*GF)%type |- _ ] => destruct x
+                             | [  |- exist _ _ _ = exist _ _ _ ] => eapply point_eq
+                         end; simpl; repeat (ring || f_equal)).
   Local Infix "+" := unifiedAdd.
   Lemma twistedAddComm : forall A B, (A+B = B+A).
   Proof.
     twisted.
   Qed.
 
-  Lemma twistedAddAssoc : forall A B C
-    (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C),
-    (A+(B+C) = (A+B)+C).
+  Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C.
   Proof.
-    (* uh... I don't actually know where this is proven... *)
+    (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
   Admitted.
 
-  Lemma zeroOnCurve : onCurve (0, 1).
-  Proof.
-    twisted.
-  Qed.
   Lemma zeroIsIdentity : forall P, P + zero = P.
   Proof.
-    admit.
-  Qed.
+    twisted.
+    (* the denominators are 1 and numerators are equal *)
+  Admitted.
 
 End CompleteTwistedEdwardsFacts.
 
 Module Type Minus1Params (Import M : Modulus) <: TwistedEdwardsParams M.
-  Module Export Defs := TwistedEdwardsDefs M.
+  Module Export GFDefs := GaloisDefs M.
   Open Scope GF_scope.
-  Definition a := 0 - 1.
+  Definition a := inject (- 1).
   Axiom a_nonzero : a <> 0.
   Axiom a_square : exists x, x * x = a.
   Parameter d : GF.
   Axiom d_nonsquare : forall x, x * x <> d.
 End Minus1Params.
 
-Module Minus1Twisted (M : Modulus) (Import P : Minus1Params M).
-  Module Import Curve := CompleteTwistedEdwardsCurve M P.
+Module Minus1Format (M : Modulus) (Import P : Minus1Params M) <: CompleteTwistedEdwardsPointFormat M P.
+  Module Import Facts := CompleteTwistedEdwardsFacts M P.
+  Module Import Curve := Facts.Curve.
+  (** [projective] represents a point on an elliptic curve using projective
+  * Edwards coordinates for twisted edwards curves with a=-1 (see
+  * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html>
+  * <https://en.wikipedia.org/wiki/Edwards_curve#Projective_homogeneous_coordinates>) *)
+  Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}.
+  Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z).
+
+  Definition twistedToProjective (P : (GF*GF)) : projective :=
+    let '(x, y) := P in (x, y, 1).
+
+  Definition projectiveToTwisted (P : projective) : GF * GF :=
+    let 'mkProjective X Y Z := P in
+    pair (X/Z) (Y/Z).
+  Hint Unfold projectiveToTwisted twistedToProjective.
+
+  Lemma GFdiv_1 : forall x, x/1 = x.
+  Admitted.
+  Hint Resolve GFdiv_1.
+
+  Lemma twistedProjectiveInv P : projectiveToTwisted (twistedToProjective P) = P.
+  Proof.
+    twisted; eapply GFdiv_1.
+  Qed.
+
+  (** [extended] represents a point on an elliptic curve using extended projective
+  * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
+  Record extended := mkExtended {extendedToProjective : projective; extendedT : GF}.
+
+  Definition point := extended.
+  Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T).
+  Definition extendedValid (P : point) : Prop :=
+    let pP := extendedToProjective P in
+    let X := projectiveX pP in
+    let Y := projectiveY pP in
+    let Z := projectiveZ pP in
+    let T := extendedT P in
+    T = X*Y/Z.
+
+
+  Definition twistedToExtended (P : (GF*GF)) : point :=
+    let '(x, y) := P in (x, y, 1, x*y).
+  Definition encode P := let '(x, y) := P in twistedToExtended (x, y).
+
+  Definition decode (P : point) :=
+    projectiveToTwisted (extendedToProjective P).
+  Local Hint Unfold extendedValid twistedToExtended decode projectiveToTwisted Curve.unifiedAdd'.
+
+  Lemma twistedExtendedInv : forall P,
+    decode (twistedToExtended P) = P.
+  Proof.
+    twisted; eapply GFdiv_1.
+  Qed.
+
+  Lemma twistedToExtendedValid : forall P, extendedValid (twistedToExtended P).
+  Proof.
+    autounfold.
+    destruct P.
+    simpl.
+    rewrite GFdiv_1; reflexivity.
+  Qed.
+
+  Definition rep (P:point) (rP:(GF*GF)) : Prop :=
+    decode P = rP /\ extendedValid P.
+  Local Notation "P '~=' rP" := (rep P rP) (at level 70).
+  Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with
+                           | [ x : rep ?a ?b |- _ ] => destruct x
+                           end).
+
+  Lemma encode_rep : forall P, encode P ~= P.
+  Proof.
+    split.
+    apply twistedExtendedInv.
+    apply twistedToExtendedValid.
+  Qed.
 
-  Module Minus1Format <: CompleteTwistedEdwardsPointFormat M P.
-    Module Import Facts := CompleteTwistedEdwardsFacts M P.
-    (** [projective] represents a point on an elliptic curve using projective
-    * Edwards coordinates for twisted edwards curves with a=-1 (see
-    * <https://hyperelliptic.org/EFD/g1p/auto-edwards-projective.html>
-    * <https://en.wikipedia.org/wiki/Edwards_curve#Projective_homogeneous_coordinates>) *)
-    Record projective := mkProjective {projectiveX : GF; projectiveY : GF; projectiveZ : GF}.
-    Local Notation "'(' X ',' Y ',' Z ')'" := (mkProjective X Y Z).
-
-    Definition twistedToProjective (P : Curve.point) : projective :=
-      let x := Curve.projX P in
-      let y := Curve.projY P in
-      (x, y, 1).
-
-    Local Notation "'(' X ',' Y ')'" := (Curve.mkPoint X Y).
-    Definition projectiveToTwisted (P : projective) : Curve.point :=
-      let X := projectiveX P in
-      let Y := projectiveY P in
-      let Z := projectiveZ P in
-      (X/Z, Y/Z).
-
-    Hint Unfold projectiveToTwisted twistedToProjective.
-
-    Lemma twistedProjectiveInv : forall P,
-      projectiveToTwisted (twistedToProjective P) = P.
-    Proof.
-      admit.
-    Qed.
-
-    (** [extended] represents a point on an elliptic curve using extended projective
-    * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
-    Record extended := mkExtended {extendedToProjective : projective; extendedT : GF}.
-    (*Error: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name.*)
-
-    Definition point := extended.
-    Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended (X, Y, Z) T).
-    Definition extendedValid (P : point) : Prop :=
-      let pP := extendedToProjective P in
-      let X := projectiveX pP in
-      let Y := projectiveY pP in
-      let Z := projectiveZ pP in
-      let T := extendedT P in
-      T = X*Y/Z.
-
-
-    Definition twistedToExtended (P : Curve.point) : point :=
-      let x := Curve.projX P in
-      let y := Curve.projY P in
-      (x, y, 1, x*y).
-    Definition mkPoint x y := twistedToExtended (x, y).
-
-    Definition extendedToTwisted (P : point) : Curve.point :=
-      projectiveToTwisted (extendedToProjective P).
-    Local Hint Unfold extendedValid twistedToExtended extendedToTwisted projectiveToTwisted Curve.unifiedAdd mkPoint.
-
-    Lemma twistedExtendedInv : forall P,
-      extendedToTwisted (twistedToExtended P) = P.
-    Proof.
-      apply twistedProjectiveInv.
-    Qed.
-
-    Lemma twistedToExtendedValid : forall (P : Curve.point), extendedValid (twistedToExtended P).
-    Proof.
-      autounfold.
-      destruct P.
-      simpl.
-      admit.
-      (* field. *)
-    Qed.
-
-    Definition rep (P:point) (rP:Curve.point) : Prop :=
-      extendedToTwisted P = rP /\ extendedValid P.
-    Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Curve.mkPoint x y).
-    Proof.
-      split.
-      apply twistedExtendedInv.
-      apply twistedToExtendedValid.
-    Qed.
-    Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-
-    Definition projX P := Curve.projX (extendedToTwisted P).
-    Definition projY P := Curve.projY (extendedToTwisted P).
-
-    Ltac rep := repeat progress (intros; autounfold; subst; auto; match goal with
-                             | [ x : rep ?a ?b |- _ ] => destruct x
-                             end).
-    Lemma projX_rep : forall P rP, P ~= rP -> projX P = Curve.projX rP.
-    Proof.
-      rep.
-    Qed.
-    Lemma projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP.
-    Proof.
-      rep.
-    Qed.
-
-    Local Notation "2" := (1+1).
-    (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
-    Definition unifiedAdd (P1 P2 : point) : point :=
-      let k := 2 * d in
-      let pP1 := extendedToProjective P1 in
-      let X1 := projectiveX pP1 in
-      let Y1 := projectiveY pP1 in
-      let Z1 := projectiveZ pP1 in
-      let T1 := extendedT P1 in
-      let pP2 := extendedToProjective P2 in
-      let X2 := projectiveX pP2 in
-      let Y2 := projectiveY pP2 in
-      let Z2 := projectiveZ pP2 in
-      let T2 := extendedT P2 in
-      let  A := (Y1-X1)*(Y2-X2) in
-      let  B := (Y1+X1)*(Y2+X2) in
-      let  C := T1*k*T2 in
-      let  D := Z1*2*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
-      mkExtended (mkProjective X3 Y3 Z3) T3.
-
-    Delimit Scope extendedM1_scope with extendedM1.
-    Infix "+" := unifiedAdd : extendedM1_scope.
-
-    Lemma unifiedAddCon : forall (P1 P2:point)
-      (hv1:extendedValid P1) (hv2:extendedValid P2),
-      extendedValid (P1 + P2)%extendedM1.
-    Proof.
-      intros.
-      remember ((P1+P2)%extendedM1) as P3.
-      destruct P1 as [[X1 Y1 Z1] T1].
-      destruct P2 as [[X2 Y2 Z2] T2].
-      destruct P3 as [[X3 Y3 Z3] T3].
-      unfold extendedValid, extendedToProjective, projectiveToTwisted, Curve.projX, Curve.projY in *.
-      invcs HeqP3.
-      subst.
-      (* field. -- fails. but it works in sage:
-  sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2");
-  print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-  ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) ==
-  ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
-  (2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-  ((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-  ((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) /
-  ((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
-  (2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))'
-        Outputs:
-          True
-      *)
-    Admitted.
-
-    Ltac extended0 := repeat progress (autounfold; simpl); intros;
-                      repeat match goal with
-                             | [ x : Curve.point |- _ ] => destruct x
-                             | [ x : point |- _ ] => destruct x
-                             | [ x : projective |- _ ] => destruct x
-                             end; simpl in *; subst.
-
-    Ltac extended := extended0; repeat (ring || f_equal)(*; field*).
-
-    Lemma unifiedAddToTwisted : forall (P1 P2 : point) (tP1 tP2 : Curve.point)
-      (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : extendedToTwisted P1 = tP1)
-      (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : extendedToTwisted P2 = tP2),
-      extendedToTwisted (P1 + P2)%extendedM1 = Curve.unifiedAdd tP1 tP2.
-    Proof.
-      extended0.
-      apply f_equal2.
-      (* case 1 verified by hand: follows from field and completeness of edwards addition *)
-      (* field should work here *)
-    Admitted.
-
-    Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd rP rQ).
-    Proof.
-      split; rep.
-      apply unifiedAddToTwisted; auto.
-      apply unifiedAddCon; auto.
-    Qed.
-
-    Module Curve := Curve.
-  End Minus1Format.
-
-End Minus1Twisted.
+  Lemma decode_rep : forall P rP, P ~= rP -> decode P = rP.
+  Proof.
+    rep.
+  Qed.
+
+
+  Local Notation "2" := (1+1).
+  (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *)
+  Definition unifiedAdd (P1 P2 : point) : point :=
+    let k := 2 * d in
+    let pP1 := extendedToProjective P1 in
+    let X1 := projectiveX pP1 in
+    let Y1 := projectiveY pP1 in
+    let Z1 := projectiveZ pP1 in
+    let T1 := extendedT P1 in
+    let pP2 := extendedToProjective P2 in
+    let X2 := projectiveX pP2 in
+    let Y2 := projectiveY pP2 in
+    let Z2 := projectiveZ pP2 in
+    let T2 := extendedT P2 in
+    let  A := (Y1-X1)*(Y2-X2) in
+    let  B := (Y1+X1)*(Y2+X2) in
+    let  C := T1*k*T2 in
+    let  D := Z1*2*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
+    mkExtended (mkProjective X3 Y3 Z3) T3.
+
+  Delimit Scope extendedM1_scope with extendedM1.
+  Infix "+" := unifiedAdd : extendedM1_scope.
+
+  Lemma unifiedAddCon : forall (P1 P2:point)
+    (hv1:extendedValid P1) (hv2:extendedValid P2),
+    extendedValid (P1 + P2)%extendedM1.
+  Proof.
+    intros.
+    remember ((P1+P2)%extendedM1) as P3.
+    destruct P1 as [[X1 Y1 Z1] T1].
+    destruct P2 as [[X2 Y2 Z2] T2].
+    destruct P3 as [[X3 Y3 Z3] T3].
+    unfold extendedValid, extendedToProjective, projectiveToTwisted in *.
+    invcs HeqP3.
+    subst.
+    (* field. -- fails. but it works in sage:
+sage -c 'var("d X1 X2 Y1 Y2 Z1 Z2");
+print(bool((((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
+((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) ==
+((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2)) *
+(2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
+((2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
+((Y1 + X1) * (Y2 + X2) - (Y1 - X1) * (Y2 - X2))) /
+((2 * Z1 * Z2 - 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2)) *
+(2 * Z1 * Z2 + 2 * ((0 - d) / a) * (X1 * Y1 / Z1) * (X2 * Y2 / Z2))))))'
+      Outputs:
+        True
+    *)
+  Admitted.
+
+  Ltac extended0 := repeat progress (autounfold; simpl); intros;
+                    repeat match goal with
+                           | [ x : Curve.point |- _ ] => destruct x
+                           | [ x : point |- _ ] => destruct x
+                           | [ x : projective |- _ ] => destruct x
+                           end; simpl in *; subst.
+
+  Ltac extended := extended0; repeat (ring || f_equal)(*; field*).
+
+  Lemma unifiedAddToTwisted : forall (P1 P2 : point) tP1 tP2
+    (P1con : extendedValid P1) (P1on : Curve.onCurve tP1) (P1rep : decode P1 = tP1)
+    (P2con : extendedValid P2) (P2on : Curve.onCurve tP2) (P2rep : decode P2 = tP2),
+    decode (P1 + P2)%extendedM1 = Curve.unifiedAdd' tP1 tP2.
+  Proof.
+    extended0.
+    apply f_equal2.
+    (* case 1 verified by hand: follows from field and completeness of edwards addition *)
+  Admitted.
+
+  Lemma unifiedAdd_rep: forall P Q rP rQ, Curve.onCurve rP -> Curve.onCurve rQ ->
+    P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Curve.unifiedAdd' rP rQ).
+  Proof.
+    split; rep.
+    apply unifiedAddToTwisted; auto.
+    apply unifiedAddCon; auto.
+  Qed.
+End Minus1Format.
 
 
 (*
@@ -443,13 +432,3 @@ Module WeirstrassMontgomery (Import M : Modulus).
   *)
 
 End WeirstrassMontgomery.
-
-(* FIXME: remove after [field] with modulus as a parameter (34d9f8a6e6a4be439d1c56a8b999d2c21ee12a46) is fixed *)
-Require Import Zpower ZArith Znumtheory.
-Definition two_255_19 := (two_p 255) - 19.
-Lemma two_255_19_prime : prime two_255_19. Admitted.
-Definition prime25519 := exist _ two_255_19 two_255_19_prime.
-Module M <: Modulus.
-  Definition modulus := prime25519.
-End M.
-
diff --git a/src/Galois/EdDSA.v b/src/Galois/EdDSA.v
index 7ab02718f..57b070148 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -5,6 +5,18 @@ Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
 Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
 
+(* TODO : where should this be? *)
+Definition wfirstn {m} {n} (w : word m) (H : (n <= m)%nat) : word n.
+  replace m with (n + (m - n))%nat in * by (symmetry; apply le_plus_minus; apply H)
+.
+  exact (split1 n (m - n) w).
+Defined.
+
+Lemma wtl_WS : forall b {n} (w : word n), wtl (WS b w) = w.
+Proof.
+  auto.
+Qed.
+
 Class Encoding (T B:Type) := {
   enc : T -> B ;
   dec : B -> option T ;
@@ -12,6 +24,7 @@ Class Encoding (T B:Type) := {
 }.
 Notation "'encoding' 'of' T 'as' B" := (Encoding T B) (at level 50).
 
+
 (* Spec from <https://eprint.iacr.org/2015/677.pdf> *)
 Module Type EdDSAParams.
   Open Scope Z_scope.
@@ -27,7 +40,7 @@ Module Type EdDSAParams.
   Module Modulus_q <: Modulus.
     Definition modulus := q.
   End Modulus_q.
-  Module Export CurveDefs := TwistedEdwardsDefs Modulus_q.
+  Module Export GFDefs := GaloisDefs Modulus_q.
 
   Parameter b : nat.
   Axiom b_valid : 2^(b - 1) > q.
@@ -74,7 +87,7 @@ Module Type EdDSAParams.
   *  This set forms a group with neutral element 0 = (0, 1) under the
   *    twisted Edwards addition law. *)
   Module CurveParameters <: TwistedEdwardsParams Modulus_q.
-    Module Defs := CurveDefs.
+    Module GFDefs := GFDefs.
     Definition a : GF := a.
     Definition a_nonzero := a_nonzero.
     Definition a_square := a_square.
@@ -85,7 +98,6 @@ Module Type EdDSAParams.
 
   Parameter B : point. (* element of E *)
   Axiom B_not_identity : B <> zero.
-  Axiom B_valid : onCurve B.
 
   (*
   * An odd prime l such that lB = 0 and (2^c)l = #E.
@@ -110,21 +122,8 @@ Module Type EdDSAParams.
   *)
   Parameter H'_out_len : nat -> nat.
   Parameter H' : forall {n}, word n -> word (H'_out_len n).
-
 End EdDSAParams.
 
-(* TODO : where should this be? *)
-Definition wfirstn {m} {n} (w : word m) (H : (n <= m)%nat) : word n.
-  replace m with (n + (m - n))%nat in * by (symmetry; apply le_plus_minus; apply H)
-.
-  exact (split1 n (m - n) w).
-Defined.
-
-Lemma wtl_WS : forall b {n} (w : word n), wtl (WS b w) = w.
-Proof.
-  auto.
-Qed.
-
 Module EdDSADefs (Import P : EdDSAParams).
   Infix "++" := combine.
   Infix "*" := scalarMult.
@@ -156,13 +155,13 @@ End EdDSADefs.
 Module Type EdDSA (Import P : EdDSAParams).
   Module Import Spec := EdDSADefs P.
 
-  (* FIXME: make [point] represent points on the curve *)
   Parameter PointEncoding : encoding of point as word b.
   Axiom encode_point_spec : forall P, enc P = encode_point_ref P.
 
   Parameter public : secretkey -> publickey.
   Axiom public_spec : forall sk, public sk = enc ((curveKey sk) * B).
 
+  (* TODO: use GF for both GF(q) and GF(l) *)
   Parameter sign : publickey -> secretkey -> forall {n}, word n -> signature.
   Axiom sign_spec : forall A_ sk {n} (M : word n), sign A_ sk M = 
     let r := wordToNat (H (randKey sk  ++ M)) in
@@ -170,18 +169,14 @@ Module Type EdDSA (Import P : EdDSAParams).
     let S := (r + curveKey sk * wordToNat (H (enc R ++ A_ ++ M)))%nat mod (Z.to_nat l) in
     enc R ++ natToWord b S.
 
-  Parameter verify : publickey -> signature -> forall {n}, word n -> bool.
-  Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ sig M = true <->
+  Parameter verify : publickey -> forall {n}, word n -> signature -> bool.
+  Axiom verify_spec : forall A_ sig {n} (M : word n), verify A_ M sig  = true <-> (
     let R_ := split1 b b sig in
     let S_ := split2 b b sig in
     let S := wordToNat S_ in
-    match dec A_ with
-    | None => False
-    | Some A => match dec R_ with
-                | None => False
-                | Some R => S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A)
-                end
-    end.
+    exists A, dec A_ = Some A /\
+    exists R, dec R_ = Some R /\
+    S * B = R + (wordToNat (H (R_ ++ A_ ++ M )) * A) ).
 End EdDSA.
 
 Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P).
@@ -216,23 +211,16 @@ Module EdDSAFacts (Import P : EdDSAParams) (Import Impl : EdDSA P).
   Lemma l_gt_zero : (Z.to_nat l <> 0)%nat.
   Admitted.
 
-  (* TODO : move to TwistedEdwardsFacts *)
-  Lemma scalarMultOnCurve : forall n P, onCurve P -> onCurve (n * P).
-  Proof.
-    intros; induction n0; boring.
-  Admitted.
-  Hint Resolve scalarMultOnCurve.
-
   (* TODO : move somewhere else (EdDSAFacts?) *)
   Lemma verify_valid_passes : forall sk {n} (M : word n),
-    verify (public sk) (sign (public sk) sk M) M = true.
+    verify (public sk) M (sign (public sk) sk M) = true.
   Proof.
     intros; rewrite verify_spec.
     intros; subst R_.
     rewrite decode_sign_split1.
     rewrite public_spec.
-    rewrite encoding_valid by auto.
-    rewrite encoding_valid by auto.
+    exists (curveKey sk * B); intuition; [apply encoding_valid|].
+    exists (wordToNat (H (randKey sk ++ M)) * B); intuition; [apply encoding_valid|].
     subst S S_.
     rewrite decode_sign_split2.
     remember (wordToNat (H (randKey sk ++ M))) as r.