rewrite ExtendedCoordinates, fix Ed25519

6 files changed, 148 insertions, 283 deletions

diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 7f580380f..c1c514171 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -115,10 +115,11 @@ Section Homomorphism_rev.
           {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
           {phi'_id : phi' id = ID}.
 
-  Local Instance group_from_redundant_representation
-    : @group H eq op id inv.
+  Lemma group_from_redundant_representation
+    : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'.
   Proof.
     repeat match goal with
+           | [ H : _/\_ |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
            | [ H : monoid |- _ ] => destruct H; try clear H
            | [ H : is_associative |- _ ] => destruct H; try clear H
@@ -132,7 +133,7 @@ Section Homomorphism_rev.
            | [ H : eq _ _ |- _ ] => apply phi'_eq in H
            | [ |- eq _ _ ] => apply phi'_eq
            | [ H : EQ _ _ |- _ ] => rewrite H
-           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id by reflexivity
+           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity
            | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity
            | _ => solve [ eauto ]
            end.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 066886e83..8110ad5cd 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -19,7 +19,6 @@ Module IntegralDomain.
   Module _LargeCharacteristicReflective.
     Section ReflectiveNsatzSideConditionProver.
       Import BinInt BinNat BinPos.
-      Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted.
       Context {R eq zero one opp add sub mul}
               {ring:@Algebra.ring R eq zero one opp add sub mul}
               {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}.
@@ -50,8 +49,9 @@ Module IntegralDomain.
 
       Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
       Proof.
+        Set Printing All.
         induction c; simpl CtoZ; simpl denote;
-          repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity.
+          repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity.
       Qed.
 
       (* TODO: move *)
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index b69e9b191..f39d730f2 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -135,15 +135,46 @@ Section Homomorphism.
   Qed.
 End Homomorphism.
 
+(* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *)
 Ltac push_homomorphism phi :=
-  let H := constr:(_:is_homomorphism(phi:=phi)) in
-  repeat rewrite
-         ?(homomorphism_zero(     phi_homom:=H)),
-         ?(homomorphism_one(is_homomorphism:=H)),
-         ?(homomorphism_add(      phi_homom:=H)),
-         ?(homomorphism_opp(      phi_homom:=H)),
-         ?(homomorphism_sub(      phi_homom:=H)),
-         ?(homomorphism_mul(is_homomorphism:=H)).
+  let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
+  pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_0;
+  pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_1;
+  pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_p;
+  pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_o;
+  pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_s;
+  pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_m;
+  (rewrite_strat bottomup (terms _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m));
+  clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m.
+
+Ltac pull_homomorphism phi :=
+  let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
+  pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_0;
+  pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_1;
+  pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_p;
+  pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_o;
+  pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_s;
+  pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_m;
+  symmetry in _pull_homomrphism_0;
+  symmetry in _pull_homomrphism_1;
+  symmetry in _pull_homomrphism_p;
+  symmetry in _pull_homomrphism_o;
+  symmetry in _pull_homomrphism_s;
+  symmetry in _pull_homomrphism_m;
+  (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m));
+  clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m.
 
 Lemma isomorphism_to_subring_ring
       {T EQ ZERO ONE OPP ADD SUB MUL}
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 42c394f07..32303a7bd 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -126,54 +126,11 @@ Module E.
                                                      F Feq Fone Fadd Fmul KtoF}.
     Context {HisoF:forall x, Feq (KtoF (FtoK x)) x}.
     Context {Ka} {Ha:Keq (FtoK Fa) Ka} {Kd} {Hd:Keq (FtoK Fd) Kd}.
-    Print Field.
-
-    (* for Ring *)
-    Ltac push_homomorphism phi :=
-      let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
-      pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_0;
-      pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_1;
-      pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_p;
-      pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_o;
-      pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_s;
-      pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
-        as _push_homomrphism_m;
-      (rewrite_strat bottomup (terms _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m));
-      clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m.
-        
-    (* for Ring *)
-    Ltac pull_homomorphism phi :=
-      let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
-      pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_0;
-      pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_1;
-      pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_p;
-      pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_o;
-      pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_s;
-      pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
-        as _pull_homomrphism_m;
-      symmetry in _pull_homomrphism_0;
-      symmetry in _pull_homomrphism_1;
-      symmetry in _pull_homomrphism_p;
-      symmetry in _pull_homomrphism_o;
-      symmetry in _pull_homomrphism_s;
-      symmetry in _pull_homomrphism_m;
-      (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m));
-      clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m.
 
     Lemma nonzero_Ka : ~ Keq Ka Kzero.
     Proof.
       rewrite <-Ha.
-      pull_homomorphism FtoK.
+      Ring.pull_homomorphism FtoK.
       intro X.
       eapply (Monoid.is_homomorphism_phi_proper(phi:=KtoF)) in X.
       rewrite 2HisoF in X.
@@ -183,14 +140,14 @@ Module E.
     Lemma square_Ka : exists sqrt_a, Keq (Kmul sqrt_a sqrt_a) Ka.
     Proof.
       destruct square_a as [sqrt_a]. exists (FtoK sqrt_a).
-      pull_homomorphism FtoK. rewrite <-Ha.
+      Ring.pull_homomorphism FtoK. rewrite <-Ha.
       eapply Monoid.is_homomorphism_phi_proper; assumption.
     Qed.
 
     Lemma nonsquare_Kd : forall x, not (Keq (Kmul x x) Kd).
     Proof.
       intros x X. apply (nonsquare_d (KtoF x)).
-      pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF.
+      Ring.pull_homomorphism KtoF. rewrite X. rewrite <-Hd, HisoF.
       reflexivity.
     Qed.
 
@@ -211,7 +168,6 @@ Module E.
     Local Notation KzeroP  := (E.zero(nonzero_a:=nonzero_Ka)(d:=Kd)).
     Local Notation FaddP   := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
     Local Notation KaddP   := (E.add(nonzero_a:=nonzero_Ka)(square_a:=square_Ka)(nonsquare_d:=nonsquare_Kd)).
-    Check KaddP.
 
     Obligation Tactic := idtac.
     Program Definition point_phi (P:Fpoint) : Kpoint := exist _ (
@@ -246,7 +202,7 @@ Module E.
              | _ => rewrite !(homomorphism_div(phi:=FtoK)) by assumption
              | _ => rewrite !Ha
              | _ => rewrite !Hd
-             | _ => push_homomorphism FtoK
+             | _ => Ring.push_homomorphism FtoK
              | |- _ ?x ?x => reflexivity
              | _ => eapply Monoid.is_homomorphism_phi_proper; assumption
              end.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 263884419..b2dbbc73d 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -1,35 +1,41 @@
-Require Export Crypto.Spec.CompleteEdwardsCurve.
+Require Import Coq.Classes.Morphisms.
+
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
 Require Import Crypto.Algebra Crypto.Algebra.
-Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Coq.Logic.Eqdep_dec.
-Require Import Crypto.Tactics.VerdiTactics.
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relation_Definitions.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Notations.
-Require Export Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
+Require Export Crypto.Util.FixCoqMistakes Crypto.Util.Tactics.
 
 Module Extended.
   Section ExtendedCoordinates.
-    Import Group Ring Field.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {prm:@E.twisted_edwards_params F Feq Fzero Fone Fopp Fadd Fsub Fmul a d}
+            {char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one)}
             {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 := (@E.onCurve F Feq Fone Fadd Fmul a d) (only parsing).
 
+    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 with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
-    Definition point := { P | let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y }.
+     * 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
@@ -39,17 +45,21 @@ Module Extended.
       | _ => progress destruct_head' @E.point
       | _ => progress destruct_head' point
       | _ => progress destruct_head' and
-      | _ => E._gather_nonzeros
-      | _ => progress cbv [CompleteEdwardsCurve.E.eq E.onCurve E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig E.onCurve] in *
+      | _ => progress cbv [eq CompleteEdwardsCurve.E.eq E.eq E.zero E.add E.opp fst snd coordinates E.coordinates proj1_sig] in *
       | |- _ /\ _ => split | |- _ <-> _ => split
-      | _ => rewrite <-!(field_div_definition(field:=field))
-      | _ => solve [fsatz]
       end.
-    Ltac t := repeat t_step.
+    Ltac t := repeat t_step; Field.fsatz.
+
+    Global Instance Equivalence_eq : Equivalence eq.
+    Proof. 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. cbv [from_twisted]; t. Qed.
 
     Program Definition to_twisted (P:point) : Epoint := 
       let XYZT := coordinates P in let T := snd XYZT in
@@ -58,211 +68,71 @@ Module Extended.
       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. cbv [to_twisted]; t. Qed.
 
-    Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q).
-
-    Definition eq_noinv (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.
-
-    Lemma eq_noinv_eq P Q : eq P Q <-> eq_noinv P Q.
-    Proof. cbv [eq_noinv eq to_twisted from_twisted]; t. Qed.
-    Global Instance DecidableRel_eq_noinv : Decidable.DecidableRel eq_noinv.
-    Proof.
-      intros P Q.
-      destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; simpl; exact _.
-    Defined.
-    Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
-    Proof.
-      intros ? ?.
-      eapply @Decidable_iff_to_flip_impl; [eapply eq_noinv_eq | exact _].
-    Defined.
-
-    Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; cbv [eq] in *; t. Qed.
-    Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. cbv [eq]; t. Qed.
-    Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. cbv [eq to_twisted]; t. Qed.
     Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P.
     Proof. cbv [to_twisted from_twisted]; t. Qed.
+    Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
+    Proof. cbv [to_twisted from_twisted]; t. Qed.
 
-    Section Proper.
-      Global Instance point_Proper : Proper (fieldwise (n:=4) Feq ==> iff)
-                                            (fun P => let '(X,Y,Z,T) := P in onCurve(X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y).
-      Proof. repeat intro; cbv [tuple tuple' fieldwise fieldwise'] in *; t. Qed.
-      Global Instance point_Proper_impl
-        : Proper (fieldwise (n:=4) Feq ==> Basics.impl)
-                 (fun P => let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y).
-      Proof. intros A B H H'; apply (@point_Proper A B H); assumption. Qed.
-      Global Instance point_Proper_flip_impl
-        : Proper (fieldwise (n:=4) Feq ==> Basics.flip Basics.impl)
-                 (fun P => let '(X,Y,Z,T) := P in onCurve (X/Z) (Y/Z) /\ Z<>0 /\ Z*T=X*Y).
-      Proof. intros A B H H'; apply (@point_Proper A B H); assumption. Qed.
-    End Proper.
-
-    Section TwistMinus1.
-      Context {a_eq_minus1 : a = Fopp 1}.
-      Context {twice_d:F} {Htwice_d:twice_d = d + d}.
-      (** 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> *)
-      Section generic. (* TODO(jgross) what is this section? *)
-        Context (F4 : Type)
-                (pair4 : F -> F -> F -> F -> F4)
-                (let_in : F -> (F -> F4) -> F4).
-        Local Notation "'slet' x := y 'in' z" := (let_in y (fun x => z)).
-        Definition add_coordinates_gen P1 P2 : F4 :=
-          let '(X1, Y1, Z1, T1) := P1 in
-          let '(X2, Y2, Z2, T2) := P2 in
-          slet  A := (Y1-X1)*(Y2-X2) in
-          slet  B := (Y1+X1)*(Y2+X2) in
-          slet  C := T1*twice_d*T2 in
-          slet  D := Z1*(Z2+Z2) in
-          slet  E := B-A in
-          slet  F := D-C in
-          slet  G := D+C in
-          slet  H := B+A in
-          slet X3 := E*F in
-          slet Y3 := G*H in
-          slet T3 := E*H in
-          slet Z3 := F*G in
-          pair4 X3 Y3 Z3 T3.
-      End generic.
-      Definition add_coordinates P1 P2 : F*F*F*F :=
-        Eval cbv beta delta [add_coordinates_gen] in
-          @add_coordinates_gen
-            (F*F*F*F)
-            (fun X3 Y3 Z3 T3 => (X3, Y3, Z3, T3))
-            (fun x f => let y := x in f y)
-            P1 P2.
-
-      Lemma add_coordinates_correct (P Q:point) :
-        let '(X,Y,Z,T) := add_coordinates (coordinates P) (coordinates Q) in
-        let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in
-        (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z).
-      Proof. cbv [E.add add_coordinates to_twisted] in *. t. Qed.
-
-      Context {add_coordinates_opt}
-              {add_coordinates_opt_correct
-               : forall P1 P2, fieldwise (n:=4) Feq (add_coordinates_opt P1 P2) (add_coordinates P1 P2)}.
+    Program Definition zero : point := (0, 1, 1, 0).
+    Next Obligation. t. Qed.
 
-      Axiom admit : forall {T}, T.
-      Obligation Tactic := idtac.
-      Program Definition add_unopt (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q).
-      Next Obligation.
-        intros P Q.
-        pose proof (add_coordinates_correct P Q) as Hrep.
-        destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ].
-        cbv; cbv in Hrep; destruct Hrep as [HA HB]; cbv in HP; cbv in HQ.
-        rewrite <-!HA, <-!HB; clear HA HB; repeat split; intros.
-        all: try (
-        goal_to_field_equality field;
-        inequalities_to_inverse_equations field;
-        divisions_to_inverses field;
-        inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit))));
-        IntegralDomain.nsatz).
-        (* TODO: in the onCurve proof for tw coordinate addition we get nonzero-denominator hypotheses from the definition itself. here the definition is not available, but we still need them... *)
-        exact admit.
-      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.
 
-      Program Definition add (P Q:point) : point := add_coordinates_opt (coordinates P) (coordinates Q).
+    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. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
+
+      Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : group /\ _ /\ _ :=
+                 @Group.group_from_redundant_representation
+                   _ _ _ _ _
+                   ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a')
+                                                  (nonsquare_d:=nonsquare_d')).(abelian_group_group))
+                   _
+                   eq
+                   m1add
+                   zero
+                   opp
+                   from_twisted
+                   to_twisted
+                   to_twisted_from_twisted
+                   _ _ _ _.
+      Next Obligation. cbv [to_twisted]. t. Qed.
       Next Obligation.
-        intros; eapply point_Proper_flip_impl;
-          [ apply add_coordinates_opt_correct
-          | exact (proj2_sig (add_unopt P Q)) ].
-      Qed.
-      Local Hint Unfold add : bash.
-
-      Lemma to_twisted_add_unopt P Q : E.eq (to_twisted (add_unopt P Q)) (E.add (to_twisted P) (to_twisted Q)).
-      Proof.
-        clear add_coordinates_opt add_coordinates_opt_correct.
-        pose proof (add_coordinates_correct P Q) as Hrep.
-        destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ].
-        cbv in *.
-        destruct Hrep as [HA HB].
-        split;
-        goal_to_field_equality field;
-        inequalities_to_inverse_equations field;
-        divisions_to_inverses field;
-        (* and now we need the nonzeros here too *)
-        inverses_to_equations_by field ltac:((solve_debugfail ltac:((exact admit))));
-        IntegralDomain.nsatz.
-      Qed.
-
-      Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)).
-      Proof.
-        rewrite <- to_twisted_add_unopt.
-        { pose proof (add_coordinates_opt_correct (coordinates P) (coordinates Q)).
-          cbv [add add_unopt].
-          do 2 match goal with
-               | [ |- context[exist _ ?x ?p] ]
-                 => first [ is_var p; fail 1
-                          | generalize p; cbv zeta; generalize dependent x ]
-               end.
-          clear add_coordinates_opt add_coordinates_opt_correct.
-          cbv [to_twisted coordinates proj1_sig E.eq E.coordinates fst snd] in *.
-          repeat match goal with
-                 | _ => intro
-                 | [ H : prod _ _ |- _ ] => destruct H
-                 | [ H : and _ _ |- _ ] => destruct H
-                 | _ => progress simpl in *
-                 | [ |- and _ _ ] => split
-                 | [ H : ?x = ?y |- context[?x] ] => is_var x; rewrite H
-                 | _ => reflexivity
-                 end. admit. }
-      Admitted. (* TODO: FIXME *)
-
-      Global Instance Proper_add : Proper (eq==>eq==>eq) add.
-      Proof.
-        unfold eq. intros x y H x0 y0 H0.
-        transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity.
-      Qed.
-
-      Lemma homomorphism_to_twisted : @Monoid.is_homomorphism point eq add Epoint E.eq E.add to_twisted.
-      Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed.
-
-      Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)).
-      Proof.
-        pose proof (to_twisted_add (from_twisted P) (from_twisted Q)).
-        unfold eq; rewrite !to_twisted_from_twisted in *.
-        symmetry; assumption.
-      Qed.
-
-      Lemma homomorphism_from_twisted : @Monoid.is_homomorphism Epoint E.eq E.add point eq add from_twisted.
-      Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed.
-
-      Definition zero : point := from_twisted E.zero.
-      Definition opp P : point := from_twisted (E.opp (to_twisted P)).
-      Lemma extended_group : @group point eq add zero opp.
-      Proof.
-        eapply @isomorphism_to_subgroup_group; eauto with typeclass_instances core.
-        - apply DecidableRel_eq.
-        - unfold opp. repeat intro. match goal with [H:_|-_] => rewrite H; reflexivity end.
-        - intros. apply to_twisted_add.
-        - unfold opp; intros; rewrite to_twisted_from_twisted; reflexivity.
-        - unfold zero; intros; rewrite to_twisted_from_twisted; reflexivity.
-      Qed.
-    End TwistMinus1.
+        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. cbv [to_twisted m1add]. t. Qed.
+      Next Obligation. cbv [to_twisted opp]. t. Qed.
+      Next Obligation. cbv [to_twisted zero]. t. Qed.
+      Global Instance group x y z
+        : group := proj1 (_group_proof x y z).
+      Global Instance homomorphism_from_twisted x y z :
+        Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)).
+      Global Instance homomorphism_to_twisted x y z :
+        Monoid.is_homomorphism := proj2 (proj2 (_group_proof x y z)).
+    End TwistMinusOne.
   End ExtendedCoordinates.
-
-  Lemma add_coordinates_respectful_hetero
-        F Fadd Fsub Fmul twice_d P Q
-        F' Fadd' Fsub' Fmul' twice_d' P' Q'
-        (R : F -> F' -> Prop)
-        (Hadd : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fadd x y) (Fadd' x' y'))
-        (Hsub : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fsub x y) (Fsub' x' y'))
-        (Hmul : forall x x' (Hx : R x x') y y' (Hy : R y y'), R (Fmul x y) (Fmul' x' y'))
-        (Htwice_d : R twice_d twice_d')
-        (HP : Tuple.fieldwise (n:=4) R P P')
-        (HQ : Tuple.fieldwise (n:=4) R Q Q')
-    : Tuple.fieldwise
-        (n:=4) R
-        (@add_coordinates F Fadd Fsub Fmul twice_d P Q)
-        (@add_coordinates F' Fadd' Fsub' Fmul' twice_d' P' Q').
-  Proof.
-    repeat match goal with
-           | [ H : and _ _ |- _ ] => destruct H
-           | [ H : prod _ _ |- _ ] => destruct H
-           | _ => progress unfold add_coordinates, fieldwise, fieldwise', fst, snd, tuple, tuple' in *
-           | [ |- and _ _ ] => split
-           | _ => solve [ auto ]
-           end.
-  Qed.
 End Extended.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 45179a81e..02f59c9e5 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -83,6 +83,13 @@ Section Ed25519.
           (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
   Proof.
     split; try exact _.
-    timeout 1 match goal with H:?P |- ?P => idtac end.
-  Admitted.
+    (* COQBUG: https://coq.inria.fr/bugs/show_bug.cgi?id=5366 *)
+    (* timeout 1 match goal with H:?P |- ?P => idtac end. *)
+    Crypto.Util.Decidable.vm_decide.
+    Crypto.Util.Decidable.vm_decide.
+    Crypto.Util.Decidable.vm_decide.
+    Crypto.Util.Decidable.vm_decide.
+    Crypto.Util.Decidable.vm_decide.
+    exact l_order_B.
+  Qed.
 End Ed25519.