Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.

3 files changed, 439 insertions, 451 deletions

diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v
index fc40d9136..8dc513a28 100644
--- a/src/Curves/Curve25519.v
+++ b/src/Curves/Curve25519.v
@@ -3,14 +3,14 @@ Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.Com
 Require Import Crypto.Curves.PointFormats.
 
 Module Curve25519.
-  Module PF := PointFormats.
-  Import PF.
+  Import M.
+  Module Import GT := GaloisTheory M.
   Local Open Scope GF_scope.
 
   Definition A : GF := ZToGF 486662.
   Definition d : GF := ((0 -ZToGF 121665) / (ZToGF 121666))%GF.
 
-  Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A.
+  (* Definition montgomeryOnCurve25519 := montgomeryOnCurve 1 A. *)
 
   (* Module-izing Twisted was a breaking change
   Definition m1TwistedOnCurve25519 := twistedOnCurve (0 -1) d.
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 8ab81e0a8..6ec9aba68 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -2,436 +2,397 @@
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory Crypto.Galois.ComputationalGaloisField.
 Require Import Tactics.VerdiTactics.
 
-(* 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.
-
-
-(** Theory of elliptic curves over prime fields for cryptographic applications,
-with focus on the curves in <https://tools.ietf.org/html/draft-ladd-safecurves-04> *)
-Module PointFormats.
-  Module F := ComputationalGaloisField M.
-  Export M F F.T.
-  Local Open Scope GF_scope.
-  Local Notation "2" := (1+1).
-  Local Notation "3" := (1+1+1).
-  Local Notation "4" := (1+1+1+1).
-  Local Notation "27" := (3*3*3).
-
-  Module Type TwistedA.
-    Parameter a : GF.
-    Axiom a_nonzero : a <> 0.
-    Axiom a_square : exists sqrt_a, sqrt_a^2 = a.
-  End TwistedA.
-
-  Module Type TwistedD.
-    Parameter d : GF.
-    Axiom d_nonsquare : forall not_sqrt_d, not_sqrt_d^2 <> d.
-  End TwistedD.
-
-  Module CompleteTwistedEdwardsSpec (Import ta:TwistedA) (Import td:TwistedD).
-    (** Twisted Ewdwards curves with complete addition laws. References:
-    * <https://eprint.iacr.org/2008/013.pdf>
-    * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
-    * <https://eprint.iacr.org/2015/677.pdf>
-    *)
-    Record point := mkPoint {projX : GF; projY : GF}.
+Module Type TwistedEdwardsParams (Import M : Modulus).
+    Module Export GT := GaloisTheory M.
+    Open Scope GF_scope.
+    Definition twistedA := { a : GF | a <> 0 /\ exists sqrt_a, sqrt_a^2 = a }.
+    Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }.
+
+    Parameter a : twistedA.
+    Parameter d : twistedD.
+
+    Definition twistedAToGF (a : twistedA) := proj1_sig a.
+    Coercion twistedAToGF : twistedA >-> GF.
+    Definition twistedDToGF (d : twistedD) := proj1_sig d.
+    Coercion twistedDToGF : twistedD >-> GF.
+End TwistedEdwardsParams.
+
+Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParams M).
+  (** Twisted Ewdwards curves with complete addition laws. References:
+  * <https://eprint.iacr.org/2008/013.pdf>
+  * <http://ed25519.cr.yp.to/ed25519-20110926.pdf>
+  * <https://eprint.iacr.org/2015/677.pdf>
+  *)
+  Record point := mkPoint {projX : GF; projY : GF}.
+
+  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.
+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 unifiedAdd : point -> point -> point.
+
+  Parameter rep : point -> Curve.point -> 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 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.
+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
+    (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
+    (1 - d*x1*x2*y1*y2) <> 0.
+    (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
+  Admitted.
+
+  Hint Unfold unifiedAdd onCurve.
+  Ltac twisted := autounfold; intros;
+                  repeat match goal with
+                             | [ x : point |- _ ] => destruct x
+                         end; simpl; repeat (ring || f_equal); field.
+  Local Infix "+" := unifiedAdd.
+  Lemma twistedAddComm : forall A B, (A+B = B+A).
+  Proof.
+    twisted.
+  Qed.
 
-    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.
-  End CompleteTwistedEdwardsSpec.
-
-  Module Type CompleteTwistedEdwardsPointFormat (ta:TwistedA) (td:TwistedD).
-    Module Spec := CompleteTwistedEdwardsSpec ta td.
-    Parameter point : Type.
-    Parameter mkPoint : forall (x y:GF), point.
-    Parameter projX : point -> GF.
-    Parameter projY : point -> GF.
-    Parameter unifiedAdd : point -> point -> point.
-
-    Parameter rep : point -> Spec.point -> Prop.
-    Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-    Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y.
-    Axiom unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ).
-    Axiom projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP.
-    Axiom projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP.
-  End CompleteTwistedEdwardsPointFormat.
-
-  Module CompleteTwistedEdwardsFacts (Import ta:TwistedA) (Import td:TwistedD).
-    Module Import Spec := CompleteTwistedEdwardsSpec ta td.
-
-    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
-      (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
-      (1 - d*x1*x2*y1*y2) <> 0.
-      (* "Twisted Edwards Curves" <http://eprint.iacr.org/2008/013.pdf> section 6 *)
-    Admitted.
+  Lemma twistedAddAssoc : forall A B C
+    (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C),
+    (A+(B+C) = (A+B)+C).
+  Proof.
+    (* uh... I don't actually know where this is proven... *)
+  Admitted.
 
-    Hint Unfold unifiedAdd onCurve.
-    Ltac twisted := autounfold; intros;
-                    repeat match goal with
-                               | [ x : point |- _ ] => destruct x
-                           end; simpl; repeat (ring || f_equal); field.
-    Local Infix "+" := unifiedAdd.
-    Lemma twistedAddComm : forall A B, (A+B = B+A).
+  Local Notation "'(' x ',' y ')'" := (mkPoint x y).
+  Definition zero := (0, 1).
+  Lemma zeroOnCurve : onCurve (0, 1).
+  Proof.
+    twisted.
+  Qed.
+  Lemma zeroIsIdentity : forall P, P + zero = P.
+  Proof.
+    admit.
+  Qed.
+End CompleteTwistedEdwardsFacts.
+
+Module Minus1Twisted (Import M : Modulus).
+  Module Minus1Params <: TwistedEdwardsParams M.
+    Module Export GT := GaloisTheory M.
+    Open Scope GF_scope.
+    Definition isSquareAndNonzero (a : GF) :=  a <> 0 /\ exists sqrt_a, sqrt_a^2 = a.
+    Definition twistedA := { a : GF | isSquareAndNonzero a }.
+    Definition twistedD := { d : GF | forall not_sqrt_d, not_sqrt_d^2 <> d }.
+
+    Axiom minusOneIsSquareAndNonzero : isSquareAndNonzero (0 - 1).
+    Definition a : twistedA := exist _ _ minusOneIsSquareAndNonzero.
+
+    Parameter d : twistedD.
+
+    Definition twistedAToGF (a : twistedA) := proj1_sig a.
+    Coercion twistedAToGF : twistedA >-> GF.
+    Definition twistedDToGF (d : twistedD) := proj1_sig d.
+    Coercion twistedDToGF : twistedD >-> GF.
+  End Minus1Params.
+  Import Minus1Params.
+
+  Module Import Curve := CompleteTwistedEdwardsCurve M Minus1Params.
+
+  Module Minus1Format <: CompleteTwistedEdwardsPointFormat M Minus1Params.
+    Module Import Facts := CompleteTwistedEdwardsFacts M Minus1Params.
+    (** [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.
-      twisted.
+      admit.
     Qed.
 
-    Lemma twistedAddAssoc : forall A B C
-      (ocA:onCurve A) (ocB:onCurve B) (ocC:onCurve C),
-      (A+(B+C) = (A+B)+C).
+    (** [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.
-      (* uh... I don't actually know where this is proven... *)
-    Admitted.
+      apply twistedProjectiveInv.
+    Qed.
 
-    Local Notation "'(' x ',' y ')'" := (mkPoint x y).
-    Definition zero := (0, 1).
-    Lemma zeroOnCurve : onCurve (0, 1).
+    Lemma twistedToExtendedValid : forall (P : Curve.point), extendedValid (twistedToExtended P).
     Proof.
-      twisted.
+      autounfold.
+      destruct P.
+      simpl.
+      admit.
+      (* field. *)
     Qed.
-    Lemma zeroIsIdentity : forall P, P + zero = P.
+
+    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.
-      twisted.
+      split.
+      apply twistedExtendedInv.
+      apply twistedToExtendedValid.
     Qed.
-  End CompleteTwistedEdwardsFacts.
-
+    Local Notation "P '~=' rP" := (rep P rP) (at level 70).
 
-  Module CompleteTwistedEdwardsSpecPointFormat (ta:TwistedA) (td:TwistedD)
-      <: CompleteTwistedEdwardsPointFormat ta td.
-    Module Spec := CompleteTwistedEdwardsSpec ta td.
-    Definition point := Spec.point.
-    Definition mkPoint := Spec.mkPoint.
-    Definition projX := Spec.projX.
-    Definition projY := Spec.projY.
-    Definition unifiedAdd := Spec.unifiedAdd.
+    Definition projX P := Curve.projX (extendedToTwisted P).
+    Definition projY P := Curve.projY (extendedToTwisted P).
 
-    Definition rep : point -> point -> Prop := eq.
-    Local Hint Unfold rep.
-    Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-    Local Ltac trivialRep := autounfold; intros; subst; auto.
-    Lemma mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y.
-      trivialRep.
-    Qed.
-    Lemma unifiedAdd_rep: forall P Q rP rQ, Spec.onCurve rP -> Spec.onCurve rQ ->
-      P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ).
-      trivialRep.
-    Qed.
-    Lemma projX_rep : forall P rP, P ~= rP -> projX P = Spec.projX rP.
-      trivialRep.
+    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 = Spec.projY rP.
-      trivialRep.
+    Lemma projY_rep : forall P rP, P ~= rP -> projY P = Curve.projY rP.
+    Proof.
+      rep.
     Qed.
-  End CompleteTwistedEdwardsSpecPointFormat.
-
-  Module Type Minus1IsSquare.
-    Axiom minusOneIsSquare : exists sqrt_a, sqrt_a^2 = 0 - 1.
-  End Minus1IsSquare.
-
-  Module Minus1Twisted (m1s:Minus1IsSquare) (Import td:TwistedD).
-    Module ta <: TwistedA.
-      Definition a : GF := 0 - 1.
-      Lemma a_square : exists sqrt_a, sqrt_a^2 = a.
-      Proof.
-        apply m1s.minusOneIsSquare.
-      Qed.
-      Lemma a_nonzero : a <> 0.
-      Proof.
-        discriminate.
-        (* This result happens to be trivial in the concrete modulus!
-         * We probably want a generic [0 <> 1] fact to use when we parameterize more. *)
-      Qed.
-    End ta.
-    Import ta.
-
-    Module Spec := CompleteTwistedEdwardsSpec ta td.
-
-    Module Format <: CompleteTwistedEdwardsPointFormat ta td.
-      Module Import Facts := CompleteTwistedEdwardsFacts ta td.
-
-      (** [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 : Spec.point) : projective :=
-        let x := Spec.projX P in
-        let y := Spec.projY P in
-        (x, y, 1).
-
-      Local Notation "'(' X ',' Y ')'" := (Spec.mkPoint X Y).
-      Definition projectiveToTwisted (P : projective) : Spec.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.
-        twisted.
-      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 : Spec.point) : point :=
-        let x := Spec.projX P in
-        let y := Spec.projY P in
-        (x, y, 1, x*y).
-      Definition mkPoint x y := twistedToExtended (x, y).
-
-      Definition extendedToTwisted (P : point) : Spec.point :=
-        projectiveToTwisted (extendedToProjective P).
-      Local Hint Unfold extendedValid twistedToExtended extendedToTwisted projectiveToTwisted Spec.unifiedAdd mkPoint.
-
-      Lemma twistedExtendedInv : forall P,
-        extendedToTwisted (twistedToExtended P) = P.
-      Proof.
-        apply twistedProjectiveInv.
-      Qed.
-
-      Lemma twistedToExtendedValid : forall (P : Spec.point), extendedValid (twistedToExtended P).
-      Proof.
-        autounfold.
-        destruct P.
-        simpl.
-        field.
-      Qed.
-        
-      Definition rep (P:point) (rP:Spec.point) : Prop :=
-        extendedToTwisted P = rP /\ extendedValid P.
-      Lemma mkPoint_rep : forall x y, rep (mkPoint x y) (Spec.mkPoint x y).
-      Proof.
-        split.
-        apply twistedExtendedInv.
-        apply twistedToExtendedValid.
-      Qed.
-      Local Notation "P '~=' rP" := (rep P rP) (at level 70).
-
-      Definition projX P := Spec.projX (extendedToTwisted P).
-      Definition projY P := Spec.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 = Spec.projX rP.
-      Proof.
-        rep.
-      Qed.
-      Lemma projY_rep : forall P rP, P ~= rP -> projY P = Spec.projY rP.
-      Proof.
-        rep.
-      Qed.
-
-      (** 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, Spec.projX, Spec.projY in *.
-        invcs HeqP3.
-        subst.
-        (* field. -- fails. but it works in sage:
+
+    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 : Spec.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 : Spec.point)
-        (P1con : extendedValid P1) (P1on : Spec.onCurve tP1) (P1rep : extendedToTwisted P1 = tP1)
-        (P2con : extendedValid P2) (P2on : Spec.onCurve tP2) (P2rep : extendedToTwisted P2 = tP2),
-        extendedToTwisted (P1 + P2)%extendedM1 = Spec.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, Spec.onCurve rP -> Spec.onCurve rQ ->
-        P ~= rP -> Q ~= rQ -> (unifiedAdd P Q) ~= (Spec.unifiedAdd rP rQ).
-      Proof.
-        split; rep.
-        apply unifiedAddToTwisted; auto.
-        apply unifiedAddCon; auto.
-      Qed.
-
-      Module Spec := Spec.
-    End Format.
-  End Minus1Twisted.
+  ((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.
 
-  (*
-  (** [precomputed] represents a point on an elliptic curve using "precomputed"
-  * Edwards coordinates, as used for fixed-base scalar multiplication
-  * (see <http://ed25519.cr.yp.to/ed25519-20110926.pdf> section 4: addition). *)
-  Record precomputed := mkPrecomputed {precomputedSum : GF;
-                                       precomputedDifference : GF;
-                                       precomputed2dxy : GF}.
-  Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed :=
-    let x := twistedX P in
-    let y := twistedY P in
-    mkPrecomputed (y+x) (y-x) (2*d*x*y).
-  *)
+    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.
+
+
+(*
+(** [precomputed] represents a point on an elliptic curve using "precomputed"
+* Edwards coordinates, as used for fixed-base scalar multiplication
+* (see <http://ed25519.cr.yp.to/ed25519-20110926.pdf> section 4: addition). *)
+Record precomputed := mkPrecomputed {precomputedSum : GF;
+                                   precomputedDifference : GF;
+                                   precomputed2dxy : GF}.
+Definition twistedToPrecomputed (d:GF) (P : twisted) : precomputed :=
+let x := twistedX P in
+let y := twistedY P in
+mkPrecomputed (y+x) (y-x) (2*d*x*y).
+*)
+
+Module WeirstrassMontgomery (Import M : Modulus).
+  Module Import GT := GaloisTheory M.
+  Local Open Scope GF_scope.
+  Local Notation "2" := (1+1).
+  Local Notation "3" := (1+1+1).
+  Local Notation "4" := (1+1+1+1).
+  Local Notation "27" := (3*3*3).
   (** [weierstrass] represents a point on an elliptic curve using Weierstrass
   * coordinates (<http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf>) definition 13.1*)
   Record weierstrass := mkWeierstrass {weierstrassX : GF; weierstrassY : GF}.
   Definition weierstrassOnCurve (a1 a2 a3 a4 a5 a6:GF) (P : weierstrass) : Prop :=
-    let x := weierstrassX P in
-    let y := weierstrassY P in
-    y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6.
+  let x := weierstrassX P in
+  let y := weierstrassY P in
+  y^2 + a1*x*y + a3*y = x^3 + a2*x^2 + a4*x + a6.
 
   (** [montgomery] represents a point on an elliptic curve using Montgomery
   * coordinates (see <https://en.wikipedia.org/wiki/Montgomery_curve>) *)
   Record montgomery := mkMontgomery {montgomeryX : GF; montgomeryY : GF}.
   Definition montgomeryOnCurve (B A:GF) (P : montgomery) : Prop :=
-    let x := montgomeryX P in
-    let y := montgomeryY P in
-    B*y^2 = x^3 + A*x^2 + x.
+  let x := montgomeryX P in
+  let y := montgomeryY P in
+  B*y^2 = x^3 + A*x^2 + x.
 
   (** see <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> section 13.2.3.c and <https://en.wikipedia.org/wiki/Montgomery_curve#Equivalence_with_Weierstrass_curves> *)
   Definition montgomeryToWeierstrass (B A:GF) (P : montgomery) : weierstrass :=
-    let x := montgomeryX P in
-    let y := montgomeryY P in
-    mkWeierstrass (x/B + A/(3*B)) (y/B).
-
-  Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery), 
-    let a4 := 1/B^2 - A^2/(3*B^2) in
-    let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in
-    let P' := montgomeryToWeierstrass B A P in
-    montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'.
+  let x := montgomeryX P in
+  let y := montgomeryY P in
+  mkWeierstrass (x/B + A/(3*B)) (y/B).
+
+  Lemma montgomeryToWeierstrassOnCurve : forall (B A:GF) (P:montgomery),
+  let a4 := 1/B^2 - A^2/(3*B^2) in
+  let a6 := 0- A^3/(27*B^3) - a4*A/(3*B) in
+  let P' := montgomeryToWeierstrass B A P in
+  montgomeryOnCurve B A P -> weierstrassOnCurve 0 0 0 a4 0 a6 P'.
   Proof.
-    intros.
-    unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *.
-    remember (weierstrassY P') as y in *.
-    remember (weierstrassX P') as x in *.
-    remember (montgomeryX P) as u in *.
-    remember (montgomeryY P) as v in *.
-    clear Hequ Heqv Heqy Heqx P'.
-    (* This is not currently important and makes field run out of memory. Maybe
-    * because I transcribed it incorrectly... *)
+  intros.
+  unfold montgomeryToWeierstrass, montgomeryOnCurve, weierstrassOnCurve in *.
+  remember (weierstrassY P') as y in *.
+  remember (weierstrassX P') as x in *.
+  remember (montgomeryX P) as u in *.
+  remember (montgomeryY P) as v in *.
+  clear Hequ Heqv Heqy Heqx P'.
+  (* This is not currently important and makes field run out of memory. Maybe
+  * because I transcribed it incorrectly... *)
   Abort.
 
 
   (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom.html> *)
-  Definition montgomeryAddDistinct (B A:GF) (P1 P2:montgomery) : montgomery := 
-    let x1 := montgomeryX P1 in
-    let y1 := montgomeryY P1 in
-    let x2 := montgomeryX P2 in
-    let y2 := montgomeryY P2 in
-    mkMontgomery
-    (B*(y2-y1)^2/(x2-x1)^2-A-x1-x2)
-    ((2*x1+x2+A)*(y2-y1)/(x2-x1)-B*(y2-y1)^3/(x2-x1)^3-y1).
+  Definition montgomeryAddDistinct (B A:GF) (P1 P2:montgomery) : montgomery :=
+  let x1 := montgomeryX P1 in
+  let y1 := montgomeryY P1 in
+  let x2 := montgomeryX P2 in
+  let y2 := montgomeryY P2 in
+  mkMontgomery
+  (B*(y2-y1)^2/(x2-x1)^2-A-x1-x2)
+  ((2*x1+x2+A)*(y2-y1)/(x2-x1)-B*(y2-y1)^3/(x2-x1)^3-y1).
   Definition montgomeryDouble (B A:GF) (P1:montgomery) : montgomery :=
-    let x1 := montgomeryX P1 in
-    let y1 := montgomeryY P1 in
-    mkMontgomery
-    (B*(3*x1^2+2*A*x1+1)^2/(2*B*y1)^2-A-x1-x1)
-    ((2*x1+x1+A)*(3*x1^2+2*A*x1+1)/(2*B*y1)-B*(3*x1^2+2*A*x1+1)^3/(2*B*y1)^3-y1).
+  let x1 := montgomeryX P1 in
+  let y1 := montgomeryY P1 in
+  mkMontgomery
+  (B*(3*x1^2+2*A*x1+1)^2/(2*B*y1)^2-A-x1-x1)
+  ((2*x1+x1+A)*(3*x1^2+2*A*x1+1)/(2*B*y1)-B*(3*x1^2+2*A*x1+1)^3/(2*B*y1)^3-y1).
   Definition montgomeryNegate P := mkMontgomery (montgomeryX P) (0-montgomeryY P).
 
   (** [montgomeryXFrac] represents a point on an elliptic curve using Montgomery x
@@ -442,38 +403,49 @@ Module PointFormats.
   Definition montgomeryXFracToMontgomeryX P : GF := (montgomeryXFracX P) / (montgomeryXFracZ P).
 
   (* from <http://www.hyperelliptic.org/EFD/g1p/auto-montgom-xz.html#ladder-mladd-1987-m>,
-   * also appears in <https://tools.ietf.org/html/draft-josefsson-tls-curve25519-06#appendix-A.1.3> *)
+  * also appears in <https://tools.ietf.org/html/draft-josefsson-tls-curve25519-06#appendix-A.1.3> *)
   Definition montgomeryDifferentialDoubleAndAdd (a : GF)
-    (X1 : GF) (P2 P3 : montgomeryXFrac) : (montgomeryXFrac * montgomeryXFrac) :=
-      let X2 := montgomeryXFracX P2 in
-      let Z2 := montgomeryXFracZ P2 in
-      let X3 := montgomeryXFracX P3 in
-      let Z3 := montgomeryXFracZ P3 in
-      let A  := X2 + Z2 in
-      let AA := A^2 in
-      let B  := X2 - Z2 in
-      let BB := B^2 in
-      let E  := AA - BB in
-      let C  := X3 + Z3 in
-      let D  := X3 - Z3 in
-      let DA := D * A in
-      let CB := C * B in
-      let X5 := (DA + CB)^2 in
-      let Z5 := X1 * (DA - CB)^2 in
-      let X4 := AA * BB in
-      let Z4 := E * (BB + (a-2)/4 * E) in
-      (mkMontgomeryXFrac X4 Z4, mkMontgomeryXFrac X5 Z5).
+  (X1 : GF) (P2 P3 : montgomeryXFrac) : (montgomeryXFrac * montgomeryXFrac) :=
+    let X2 := montgomeryXFracX P2 in
+    let Z2 := montgomeryXFracZ P2 in
+    let X3 := montgomeryXFracX P3 in
+    let Z3 := montgomeryXFracZ P3 in
+    let A  := X2 + Z2 in
+    let AA := A^2 in
+    let B  := X2 - Z2 in
+    let BB := B^2 in
+    let E  := AA - BB in
+    let C  := X3 + Z3 in
+    let D  := X3 - Z3 in
+    let DA := D * A in
+    let CB := C * B in
+    let X5 := (DA + CB)^2 in
+    let Z5 := X1 * (DA - CB)^2 in
+    let X4 := AA * BB in
+    let Z4 := E * (BB + (a-2)/4 * E) in
+    (mkMontgomeryXFrac X4 Z4, mkMontgomeryXFrac X5 Z5).
 
   (*
   (* <https://eprint.iacr.org/2008/013.pdf> Theorem 3.2. *)
   (* TODO: exceptional points *)
-  Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery := 
-    let x := twistedX P in
-    let y := twistedY P in
-    mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)).
+  Definition twistedToMontfomery (a d:GF) (P : twisted) : montgomery :=
+  let x := twistedX P in
+  let y := twistedY P in
+  mkMontgomery ((1+y)/(1-y)) ((1+y)/((1-y)*x)).
   Definition montgomeryToTwisted (B A:GF) (P : montgomery) : twisted :=
-    let X := montgomeryX P in
-    let Y := montgomeryY P in
-    mkTwisted (X/Y) ((X-1)/(X+1)).
-   *)
-End PointFormats.
+  let X := montgomeryX P in
+  let Y := montgomeryY P in
+  mkTwisted (X/Y) ((X-1)/(X+1)).
+  *)
+
+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 ed89b52ce..45ed05243 100644
--- a/src/Galois/EdDSA.v
+++ b/src/Galois/EdDSA.v
@@ -7,25 +7,15 @@ Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
 Local Open Scope Z_scope.
 
-Module Type GFEncoding (Import M : Modulus).
-  Module Import GF := GaloisTheory M.
-  Parameter b : nat.
-  Parameter decode : word (b - 1) -> GF.
-  Parameter encode : GF -> word (b - 1).
-  Axiom consistent : forall x, decode(encode x) = x.
-End GFEncoding.
-
 Module Type PointFormatsSpec (Import Q : Modulus).
   Module Import GT := GaloisTheory Q.
 
   Parameter a : GF.
-  Axiom a_square: exists x, (x * x = a)%GF.
 
   Parameter d : GF.
-  Axiom d_not_square : forall x, ((x * x = d)%GF -> False).
 
   Record point := mkPoint{x : GF; y : GF}.
-  Parameter id : point.
+  Definition id := (mkPoint 0 1)%GF.
 
   Parameter onCurve : point -> Prop.
 
@@ -35,10 +25,9 @@ Module Type PointFormatsSpec (Import Q : Modulus).
   Parameter add : point -> point -> point.
   Axiom add_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (add P Q).
   Axiom add_id : forall P, add P id = P.
-
 End PointFormatsSpec.
 
-Module Type EdDSAParams (Import Q : Modulus) (Import Enc : GFEncoding Q) (PF : PointFormatsSpec Q).
+Module Type EdDSAParams.
   (* Spec from https://eprint.iacr.org/2015/677.pdf *)
 
   (*
@@ -47,25 +36,33 @@ Module Type EdDSAParams (Import Q : Modulus) (Import Enc : GFEncoding Q) (PF : P
   *   since the size of q constrains the size of l below.
   * There are additional security concerns when q is not chosen to be prime.
   *)
-  Definition q := modulus.
+  Parameter q : Prime.
   Axiom q_odd : Z.odd q = true.
 
+  Module Modulus_q <: Modulus.
+    Definition modulus := q.
+  End Modulus_q.
+  Module Import GF := GaloisTheory Modulus_q.
+
   (*
   * An integer b with 2^(b − 1) > q.
   * EdDSA public keys have exactly b bits,
   *   and EdDSA signatures have exactly 2b bits.
   *)
+  Parameter b : nat.
   Axiom b_valid : 2^((Z.of_nat b) - 1) > q.
 
   (* A (b − 1)-bit encoding of elements of the finite field Fq. *)
-  Import Enc.GF.
+  Parameter decode : word (b - 1) -> GF.
+  Parameter encode : GF -> word (b - 1).
+  Axiom consistent : forall x, decode( encode x) = x.
 
   (*
   * A cryptographic hash function H producing 2b-bit output.
   * Conservative hash functions are recommended and do not have much
   *   impact on the total cost of EdDSA.
   *)
-  Parameter H : forall n, word n -> word (2 * b).
+  Parameter H : forall n, word n -> word (b + b).
 
   (*
   * An integer c \in {2, 3}. Secret EdDSA scalars are multiples of 2c.
@@ -96,14 +93,17 @@ Module Type EdDSAParams (Import Q : Modulus) (Import Enc : GFEncoding Q) (PF : P
   * The original specification of EdDSA did not include this parameter:
   *   it implicitly took a = −1 (and required q mod 4 = 1).
   *)
-  Definition a := PF.a.
+  Parameter a : GF.
+  Axiom a_nonzero : a <> 0%GF.
+  Axiom a_square: exists x, (x * x = a)%GF.
 
   (*
   * A non-square element d of Fq.
   * The exact choice of d (together with a and q) is important for security,
   *   and is the main topic considered in “curve selection”.
   *)
-  Definition d := PF.d.
+  Definition d : GF := PF.d.
+  Axiom d_not_square : forall x, ((x * x = d)%GF -> False).
 
   (*
   *  An element B \neq (0, 1) of the set
@@ -111,6 +111,7 @@ Module Type EdDSAParams (Import Q : Modulus) (Import Enc : GFEncoding Q) (PF : P
   *  This set forms a group with neutral element 0 = (0, 1) under the
   *    twisted Edwards addition law.
   *)
+  Declare Module PF : PointFormatsSpec Modulus_q.
   Parameter B : PF.point.
   Axiom B_valid : PF.onCurve B.
   Axiom B_not_identity : B = PF.id -> False.
@@ -139,21 +140,36 @@ Module Type EdDSAParams (Import Q : Modulus) (Import Enc : GFEncoding Q) (PF : P
 
 End EdDSAParams.
 
-Module Type EdDSA (Q : Modulus) (Import Enc : GFEncoding Q) (Import PF : PointFormatsSpec Q) (Import P : EdDSAParams Q Enc PF).
-  Import Enc.GF.
+Module Type EdDSA (Import P : EdDSAParams).
+  Import P.PF P.GF.
   Parameter encode_point : point -> word b.
   Parameter decode_point : word b -> point.
+  Record secret.
+  Parameter public : secret -> word b.
+  Parameter signature : secret -> forall n, word n -> word (b + b).
+End EdDSA.
 
-  Module Type Key.
-    Parameter secret : word b.
-    Definition whdZ {n} (w : word (S n)) := if (whd w) then 1 else 0.
-    Fixpoint word_sum (n : nat) (coef : nat -> Z) : word n -> Z :=
-      match n with
-        | 0%nat => fun w => 0
-        | S n' => fun w => (word_sum n' (fun i => coef (S i)) (wtl w)) + ((coef n') * whdZ w)
-      end.
-    Definition s := two_power_nat n + word_sum b two_power_nat secret.
-    Definition public := H b (encode_point (scalar_mul (inject s) B)).
-  End Key.
+Module EdDSAImpl (Import P : EdDSAParams) <: EdDSA P.
+  Import P.PF P.GF.
+  Definition encode_point (p : point) := wzero b. (* TODO *)
 
-End EdDSA.
+  Definition decode_point (w : word b) := id.  (* TODO *)
+
+  (* Utilities for words -- TODO : move *)
+  Definition leading_ones n := natToWord b (wordToNat (wone n)).
+  Definition c_to_n_window := wxor (leading_ones c) (leading_ones n).
+
+  (* Precompute s and the high half of H(k) *)
+  Record secret := mkSecret{
+    key : word b;
+    s : Z;
+    hash_high : word b;
+    s_def : s =  wordToZ (wand c_to_n_window key);
+    hash_high_def : hash_high = split2 b b (H b key)
+  }.
+
+  Definition public (sk : secret) := H b (encode_point (scalar_mul (inject (s sk)) B)).
+
+  Definition signature (sk : secret) n (w : word n) := wzero (b + b).
+
+End EdDSAImpl.