use improved fsatz on various elliptic curve things

partial correctness of projective addition

stronger projective addition proof

fixup

5 files changed, 498 insertions, 148 deletions

diff --git a/src/CompleteEdwardsCurve/EdwardsMontgomery.v b/src/CompleteEdwardsCurve/EdwardsMontgomery.v
new file mode 100644
index 000000000..2a987735d
--- /dev/null
+++ b/src/CompleteEdwardsCurve/EdwardsMontgomery.v
@@ -0,0 +1,113 @@
+Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
+
+Require Import Crypto.Util.Notations Crypto.Util.Decidable.
+Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+
+Module E.
+  Section EdwardsMontgomery.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
+            {Feq_dec:DecidableRel Feq}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x).
+
+    Context {a d: F}
+            {nonzero_a : a <> 0}
+            {square_a : exists sqrt_a, sqrt_a^2 = a}
+            {nonsquare_d : forall x, x^2 <> d}.
+    Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
+    Local Notation Ezero  := (E.zero(nonzero_a:=nonzero_a)(d:=d)).
+    Local Notation Eadd   := (E.add(nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d)).
+    Local Notation Eopp   := (E.opp(nonzero_a:=nonzero_a)(d:=d)).
+
+    Let a_neq_d : a <> d.
+    Proof. intro X.
+           edestruct square_a. eapply nonsquare_d.
+           rewrite <-X. eassumption. Qed.
+
+    
+    Local Notation "2" := (1+1). Local Notation "4" := (1+1+1+1).
+    Local Notation MontgomeryA := (2*(a+d)/(a-d)).
+    Local Notation MontgomeryB := (4/(a-d)).
+
+    Let b_nonzero : MontgomeryB <> 0. Proof. fsatz. Qed.
+
+    Local Notation Mpoint := (@M.point F Feq Fadd Fmul MontgomeryA MontgomeryB).
+    Local Notation Madd := (@M.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 MontgomeryA MontgomeryB b_nonzero).
+    Local Notation "'∞'" := (inr tt) : core_scope.
+
+    Ltac t_step :=
+        match goal with
+        | _ => solve [ contradiction | trivial ]
+        | _ => progress intros
+        | _ => progress subst
+        | _ => progress Tactics.DestructHead.destruct_head' @M.point
+        | _ => progress Tactics.DestructHead.destruct_head' @prod
+        | _ => progress Tactics.DestructHead.destruct_head' @sum
+        | _ => progress Tactics.DestructHead.destruct_head' @and
+        | _ => progress Sum.inversion_sum
+        | _ => progress Prod.inversion_prod
+        | _ => progress Tactics.BreakMatch.break_match_hyps
+        | _ => progress Tactics.BreakMatch.break_match
+        | _ => progress cbv [E.coordinates M.coordinates E.add M.add E.zero M.zero E.eq M.eq E.opp M.opp proj1_sig fst snd] in *
+        | |- _ /\ _ => split
+        end.
+    Ltac t := repeat t_step.
+
+    Program Definition to_Montgomery (P:Epoint) : Mpoint :=
+      match E.coordinates P return F*F+_ with
+      | (x, y) => 
+        if dec (y <> 1 /\ x <> 0)
+        then inl ((1+y)/(1-y), (1+y)/(x-x*y))
+        else ∞
+      end.
+    Next Obligation. Proof. t. fsatz. Qed.
+
+    (* The exceptional cases are tricky. *)
+    (* See https://eprint.iacr.org/2008/013.pdf page 5 before continuing *)
+
+    Program Definition of_Montgomery (P:Mpoint) : Epoint :=
+      match M.coordinates P return F*F with
+      | inl (x,y) =>
+        if dec (y = 0)
+        then (0, Fopp 1)
+        else (x/y, (x-1)/(x+1))
+      | ∞ => pair 0 1
+      end.
+    Next Obligation.
+    Proof.
+      t; try fsatz.
+      assert (f1 <> Fopp 1) by admit (* ad, d are nonsero *); fsatz.
+    Admitted.
+
+    Import BinNums.
+    (* TODO: characteristic weakening lemmas *)
+    Context {char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}.
+    Context {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+
+    Program Definition _EM : _ /\ _ /\ _ :=
+      @Group.group_from_redundant_representation
+        Mpoint M.eq Madd M.zero M.opp
+        (M.group(discr_nonzero:=_))
+        Epoint E.eq Eadd Ezero Eopp
+        of_Montgomery
+        to_Montgomery
+        _ _ _ _ _
+    .
+    Next Obligation. Proof. Admitted. (* discriminant nonzero *)
+    Next Obligation. Proof. Admitted. (* M->E->M *)
+    Next Obligation. Proof. Admitted. (* M->E->M *)
+    Next Obligation. Proof. Admitted. (* add *)
+    Next Obligation. Proof. Admitted. (* opp *)
+    Next Obligation. Proof. cbv [of_Montgomery to_Montgomery]; t; fsatz. Qed.
+
+    Global Instance homomorphism_of_Montgomery : Monoid.is_homomorphism(phi:=of_Montgomery) := proj1 (proj2 _EM).
+    Global Instance homomorphism_to_Montgomery : Monoid.is_homomorphism(phi:=to_Montgomery) := proj2 (proj2 _EM).
+  End EdwardsMontgomery.
+End E.
diff --git a/src/MontgomeryCurveTheorems.v b/src/MontgomeryCurveTheorems.v
new file mode 100644
index 000000000..2f226b594
--- /dev/null
+++ b/src/MontgomeryCurveTheorems.v
@@ -0,0 +1,112 @@
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings.
+Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.WeierstrassCurve.WeierstrassCurveTheorems.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "- x" := (Fopp x).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "2" := (1+1). Local Notation "3" := (1+2).
+    Local Notation "'∞'" := unit : type_scope.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+    Local Open Scope core_scope.
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+
+    Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b :=
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation. Proof. destruct P; cbv; break_match; trivial; fsatz. Qed.
+
+    Ltac t :=
+      repeat
+        match goal with
+        | _ => solve [ trivial ]
+        | _ => progress intros
+        | _ => progress subst
+        | _ => progress Tactics.DestructHead.destruct_head' @M.point
+        | _ => progress Tactics.DestructHead.destruct_head' @prod
+        | _ => progress Tactics.DestructHead.destruct_head' @sum
+        | _ => progress Tactics.DestructHead.destruct_head' @and
+        | _ => progress Sum.inversion_sum
+        | _ => progress Prod.inversion_prod
+        | _ => progress Tactics.BreakMatch.break_match_hyps
+        | _ => progress Tactics.BreakMatch.break_match
+        | _ => progress cbv [M.coordinates M.add M.zero M.eq opp proj1_sig] in *
+        | _ => progress cbv [W.coordinates W.add W.zero W.eq W.inv proj1_sig] in *
+        | |- _ /\ _ => split | |- _ <-> _ => split
+        end.
+
+    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+
+    Section MontgomeryWeierstrass.
+      Local Notation "4" := (1+3).
+      Local Notation "16" := (4*4).
+      Local Notation "9" := (3*3).
+      Local Notation "27" := (3*9).
+      Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+
+
+      Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
+      Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
+      Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
+      Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
+      Program Definition to_Weierstrass (P:@point) : Wpoint :=
+        match M.coordinates P return F*F+∞ with
+        | (x, y) => ((x + a/3)/b, y/b)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. t; fsatz. Qed.
+
+      Program Definition of_Weierstrass (P:Wpoint) : point :=
+        match W.coordinates P return F*F+∞ with
+        | (x,y) => (b*x-a/3, b*y)
+        | _ => ∞
+        end.
+      Next Obligation. Proof. t. fsatz. Qed.
+
+      (*TODO: rename inv to opp, make it not require [discr_nonzero] *)
+      Context {discr_nonzero : (2 + 1 + 1) * WeierstrassA * WeierstrassA * WeierstrassA +
+                               ((2 + 1 + 1) ^ 2 + (2 + 1 + 1) + (2 + 1 + 1) + 1 + 1 + 1) *
+                               WeierstrassB * WeierstrassB <> 0}.
+      (* TODO: weakening lemma for characteristic *)
+      Context {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}.
+      Local Notation Wopp := (@W.inv F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv WeierstrassA WeierstrassB field Feq_dec discr_nonzero).
+
+      Program Definition _MW : _ /\ _ /\ _ :=
+        @Group.group_from_redundant_representation
+          Wpoint W.eq Wadd W.zero Wopp
+          (abelian_group_group (W.commutative_group(discriminant_nonzero:=discr_nonzero)))
+          point M.eq (M.add(b_nonzero:=b_nonzero)) M.zero opp
+          of_Weierstrass
+          to_Weierstrass
+          _ _ _ _ _
+      .
+      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
+      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
+      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
+      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
+      Next Obligation. Proof. cbv [of_Weierstrass to_Weierstrass]; t; clear discr_nonzero; fsatz. Qed.
+
+      Global Instance group : Algebra.group := proj1 _MW.
+      Global Instance homomorphism_of_Weierstrass : Monoid.is_homomorphism(phi:=of_Weierstrass) := proj1 (proj2 _MW).
+      Global Instance homomorphism_to_Weierstrass : Monoid.is_homomorphism(phi:=to_Weierstrass) := proj2 (proj2 _MW).
+    End MontgomeryWeierstrass.
+  End MontgomeryCurve.
+End M.
\ No newline at end of file
diff --git a/src/MontgomeryX.v b/src/MontgomeryX.v
new file mode 100644
index 000000000..b3e9a5ae8
--- /dev/null
+++ b/src/MontgomeryX.v
@@ -0,0 +1,82 @@
+Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
+
+Module M.
+  Section MontgomeryCurve.
+    Import BinNat.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
+            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "+" := Fadd. Local Infix "*" := Fmul.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x).
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Notation "'∞'" := (inr tt) : core_scope.
+    Local Notation "( x , y )" := (inl (pair x y)).
+
+    Context {a b: F} {b_nonzero:b <> 0}.
+    Local Notation add := (M.add(b_nonzero:=b_nonzero)).
+    Local Notation opp := (M.opp(b_nonzero:=b_nonzero)).
+    Local Notation point := (@M.point F Feq Fadd Fmul a b).
+
+    Program Definition to_xz (P:point) : F*F :=
+      match M.coordinates P with
+      | (x, y) => pair x 1
+      | ∞ => pair 1 0
+      end.
+
+    (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *)
+    Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
+    Definition xzladderstep (x1:F) (Q Q':F*F) : ((F*F)*(F*F)) :=
+      match Q, Q' with
+        pair x z, pair x' z' => 
+        let A := x+z in
+        let B := x-z in
+        let AA := A^2 in
+        let BB := B^2 in
+        let x2 := AA*BB in
+        let E := AA-BB in
+        let z2 := E*(AA + a24*E) in
+        let C := x'+z' in
+        let D := x'-z' in
+        let CB := C*B in
+        let DA := D*A in
+        let x3 := (DA+CB)^2 in
+        let z3 := x1*(DA-CB)^2 in
+        (pair (pair x2 z2) (pair x3 z3))
+      end.
+
+    Ltac t :=
+      repeat
+        match goal with
+        | _ => solve [ contradiction | trivial ]
+        | _ => progress intros
+        | _ => progress subst
+        | _ => progress Tactics.DestructHead.destruct_head' @M.point
+        | _ => progress Tactics.DestructHead.destruct_head' @prod
+        | _ => progress Tactics.DestructHead.destruct_head' @sum
+        | _ => progress Tactics.DestructHead.destruct_head' @and
+        | _ => progress Sum.inversion_sum
+        | _ => progress Prod.inversion_prod
+        | _ => progress Tactics.BreakMatch.break_match_hyps
+        | _ => progress Tactics.BreakMatch.break_match
+        | _ => progress cbv [fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep to_xz] in *
+        | |- _ /\ _ => split
+        end.
+
+    Lemma xzladderstep_correct 
+          (Q Q':point) x z x' z' x1 x2 z2 x3 z3
+          (Hl:Logic.eq (pair(pair x2 z2)(pair x3 z3)) (xzladderstep x1 (pair x z) (pair x' z')))
+          (H:match M.coordinates Q with∞=>z=0/\x<>0|(xQ,y)=>xQ=x/z/\z<>0  (* TODO *) /\ y <> 0 (* TODO: prove this from non-squareness of a^2 - 4 *) end)
+          (H':match M.coordinates Q' with∞=>z'=0/\x'<>0|(xQ',_)=>xQ'=x'/z'/\z'<>0 end)
+          (H1:match M.coordinates (add Q (opp Q')) with∞=>False|(x,y)=>x=x1/\x<>0 end):
+      match M.coordinates (add Q Q) with∞=>z2=0/\x2<>0|(xQQ,_)=>xQQ=x2/z2/\z2<>0 end /\
+      match M.coordinates (add Q Q') with∞=>z3=0/\x3<>0|(xQQ',_)=>xQQ'=x3/z3/\z3<>0 end.
+    Proof. t; abstract fsatz. Qed.
+  End MontgomeryCurve.
+End M.
\ No newline at end of file
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index cff35104c..a12f2ef96 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -1,20 +1,22 @@
-Require Crypto.Algebra.
+Require Crypto.Algebra Crypto.Algebra.Field.
 Require Crypto.Util.GlobalSettings.
-
-Require Import Crypto.Spec.WeierstrassCurve.
+Require Crypto.Util.Tactics Crypto.Util.Sum Crypto.Util.Prod.
 
 Module M.
   Section MontgomeryCurve.
     Import BinNat.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {Feq_dec:Decidable.DecidableRel Feq}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "- x" := (Fopp x).
-    Local Notation "x ^ 2" := (x*x) (at level 30). Local Notation "x ^ 3" := (x*x^2) (at level 30).
+    Local Notation "x ^ 2" := (x*x) (at level 30).
+    Local Notation "x ^ 3" := (x*x^2) (at level 30).
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Notation "2" := (1+1). Local Notation "3" := (1+2).
-
     Local Notation "'∞'" := unit : type_scope.
     Local Notation "'∞'" := (inr tt) : core_scope.
     Local Notation "( x , y )" := (inl (pair x y)).
@@ -22,12 +24,14 @@ Module M.
 
     Context {a b: F} {b_nonzero:b <> 0}.
 
-    Definition point := { P | match P with
-                              | (x, y) => b*y^2 = x^3 + a*x^2 + x
-                              | ∞ => True
-                              end }.
+    Definition point := { P : F*F+∞ | match P with
+                                      | (x, y) => b*y^2 = x^3 + a*x^2 + x
+                                      | ∞ => True
+                                      end }.
     Definition coordinates (P:point) : (F*F + ∞) := proj1_sig P.
 
+    Program Definition zero : point := ∞.
+
     Definition eq (P1 P2:point) :=
       match coordinates P1, coordinates P2 with
       | (x1, y1), (x2, y2) => x1 = x2 /\ y1 = y2
@@ -35,150 +39,36 @@ Module M.
       | _, _ => False
       end.
 
-    Import Crypto.Util.Tactics Crypto.Algebra.Field.
-    Ltac t :=
-      destruct_head' point; destruct_head' sum; destruct_head' prod;
-        break_match; simpl in *; break_match_hyps; trivial; try discriminate;
-        repeat match goal with
-               | |- _ /\ _ => split
-               | [H:@Logic.eq (sum _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
-               | [H:@Logic.eq (prod _ _ ) _ _ |- _] => symmetry in H; injection H; intros; clear H
-               end;
-        subst; try fsatz.
-
     Program Definition add (P1 P2:point) : point :=
             match coordinates P1, coordinates P2 return F*F+∞ with
               (x1, y1), (x2, y2) =>
               if Decidable.dec (x1 = x2)
               then if Decidable.dec (y1 = - y2)
                    then ∞
-                   else (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)
-              else (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)
-            | ∞, ∞ =>                      ∞
-            | ∞, _ =>                      coordinates P2
-            | _, ∞ =>                      coordinates P1
+                   else let k := (3*x1^2 + 2*a*x1 + 1)/(2*b*y1) in
+                        (b*k^2 - a - x1 - x1, (2*x1 + x1 + a)*k - b*k^3 - y1)
+              else let k := (y2 - y1)/(x2-x1) in
+                   (b*k^2 - a - x1 - x2, (2*x1 + x2 + a)*k - b*k^3 - y1)
+            | ∞, ∞ => ∞
+            | ∞, _ => coordinates P2
+            | _, ∞ => coordinates P1
             end.
-    Next Obligation. Proof. t. Qed.
-
-    Program Definition zero : point := ∞.
-
-    Program Definition opp (P:point) : point :=
-      match P return F*F+∞ with
-      | (x, y) => (x, -y)
-      | ∞ => ∞
-      end.
-    Next Obligation. Proof. t. Qed.
-
-    Local Notation "4" := (1+3).
-    Local Notation "16" := (4*4).
-    Local Notation "9" := (3*3).
-    Local Notation "27" := (3*9).
-    Context {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
-
-    Local Notation WeierstrassA := ((3-a^2)/(3*b^2)).
-    Local Notation WeierstrassB := ((2*a^3-9*a)/(27*b^3)).
-    Local Notation Wpoint := (@W.point F Feq Fadd Fmul WeierstrassA WeierstrassB).
-    Local Notation Wadd := (@W.add F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv field Feq_dec char_ge_3 WeierstrassA WeierstrassB).
-
-    Program Definition to_Weierstrass (P:point) : Wpoint :=
-      match coordinates P return F*F+∞ with
-      | (x, y) => ((x + a/3)/b, y/b)
-      | _ => ∞
-      end.
-    Next Obligation.
-    Proof. clear char_ge_3; destruct P; t. Qed.
-
-    Program Definition of_Weierstrass (P:Wpoint) : point :=
-      match W.coordinates P return F*F+∞ with
-      | (x,y) => (b*x-a/3, b*y)
-      | _ => ∞
-      end.
-    Next Obligation.
-    Proof. clear char_ge_3; destruct P; t. Qed.
-
-    (* TODO: move *)
-    Program Definition Wopp (P:Wpoint) : Wpoint :=
-      match P return F*F+∞ with
-      | (x, y) => (x, -y)
-      | ∞ => ∞
-      end.
-    Next Obligation. destruct P; t. Qed.
-
-    Axiom Wgroup : @Algebra.group Wpoint (@W.eq F Feq Fadd Fmul WeierstrassA WeierstrassB)
-         Wadd (@W.zero F Feq Fadd Fmul WeierstrassA WeierstrassB) Wopp.
-    Program Definition _MW : _ /\ _ /\ _ :=
-      @Group.group_from_redundant_representation
-        Wpoint W.eq Wadd W.zero Wopp
-        Wgroup
-        point eq add zero opp
-        of_Weierstrass
-        to_Weierstrass
-        _ _ _ _ _
-        .
-    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *; t. Qed.
-    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. 2:intuition idtac. 2:intuition idtac. 2:intuition idtac.
-                     { repeat split; destruct_head' and; t. } Qed.
     Next Obligation.
-      (* addition case, same issue as in Weierstrass associativity *) 
-      cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add coordinates W.coordinates proj1_sig] in *.
-      clear char_ge_3. t. Qed.
-    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. Qed.
-    Next Obligation. cbv [W.eq eq to_Weierstrass of_Weierstrass W.add add Wopp opp coordinates W.coordinates proj1_sig] in *. clear char_ge_3. t. Qed.
-    
-    Section AddX.
-      Lemma homogeneous_x_differential_addition_releations P1 P2 :
-          match coordinates (add P2 (opp P1)), coordinates P1, coordinates P2, coordinates (add P1 P2) with
-          | (x, _), (x1, _), (x2, _), (x3, _) =>
-            if Decidable.dec (x1 = x2)
-            then x3 * (4*x1*(x1^2 + a*x1 + 1)) = (x1^2 - 1)^2
-            else x3 * (x*(x1-x2)^2) = (x1*x2 - 1)^2
-          | _, _, _, _ => True
-          end.
-      Proof. t. Qed.
-
-      Program Definition to_xz (P:point) : F*F :=
-        match coordinates P with
-        | (x, y) => pair x 1
-        | ∞ => pair 1 0
-        end.
-
-      (* From Explicit Formulas Database by Lange and Bernstein,
-         credited to 1987 Montgomery "Speeding the Pollard and elliptic curve
-         methods of factorization", page 261, fifth and sixth displays, plus
-         common-subexpression elimination, plus assumption Z1=1 *)
-      
-      Context {a24:F} {a24_correct:4*a24 = a+2}. (* TODO: +2 or -2 ? *)
-      Definition xzladderstep (X1:F) (P1 P2:F*F) : ((F*F)*(F*F)) :=
-        match P1, P2 with
-          pair X2 Z2, pair X3 Z3 => 
-          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 + a24*E) in
-          (pair (pair X4 Z4) (pair X5 Z5))
-        end.
-
-      Require Import Crypto.Util.Tuple.
-
-      (* TODO: look up this lemma statement -- the current one may not be right *)
-      Lemma xzladderstep_to_xz X1 P1 P2
-        (HX1 : match coordinates (add P1 (opp P2)) with (x,y) => X1 = x | _ => False end)
-        : fieldwise (n:=2) (fieldwise (n:=2) Feq)
-                    (xzladderstep X1 (to_xz P1) (to_xz P2))
-                    (pair (to_xz (add P1 P2)) (to_xz (add P1 P1))).
-        destruct P1 as [[[??]|?]?], P2 as [[[??]|?]?];
-          cbv [fst snd xzladderstep to_xz add coordinates proj1_sig opp fieldwise fieldwise'] in *;
-          break_match_hyps; break_match; repeat split; try contradiction.
-      Abort.
-    End AddX.
+    Proof. 
+      repeat match goal with
+             | _ => solve [ trivial ]
+             | _ => progress Tactics.DestructHead.destruct_head' @point
+             | _ => progress Tactics.DestructHead.destruct_head' @prod
+             | _ => progress Tactics.DestructHead.destruct_head' @sum
+             | _ => progress Sum.inversion_sum
+             | _ => progress Prod.inversion_prod
+             | _ => progress Tactics.BreakMatch.break_match_hyps
+             | _ => progress Tactics.BreakMatch.break_match
+             | _ => progress subst
+             | _ => progress cbv [coordinates proj1_sig] in *
+             | |- _ /\ _ => split
+             | |- _ => Field.fsatz
+             end.
+    Qed.
   End MontgomeryCurve.
-End M.
\ No newline at end of file
+End M.
diff --git a/src/WeierstrassCurve/Projective.v b/src/WeierstrassCurve/Projective.v
new file mode 100644
index 000000000..a62bf027a
--- /dev/null
+++ b/src/WeierstrassCurve/Projective.v
@@ -0,0 +1,153 @@
+Require Import Crypto.Spec.WeierstrassCurve.
+Require Import Crypto.Util.Decidable Crypto.Util.Tactics Crypto.Algebra.Field.
+Require Import Crypto.Util.Notations Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.Sigma.
+
+Module Projective.
+  Section Projective.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
+            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
+            {Feq_dec:DecidableRel Feq}.
+    Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Notation "0" := Fzero.  Local Notation "1" := Fone.
+    Local Infix "+" := Fadd. Local Infix "-" := Fsub.
+    Local Infix "*" := Fmul. Local Infix "/" := Fdiv.
+    Local Notation "x ^ 2" := (x*x). Local Notation "x ^ 3" := (x*x^2).
+    Local Notation Wpoint := (@W.point F Feq Fadd Fmul a b).
+
+    (* Originally from
+    <http://www.mat.uniroma3.it/users/pappa/CORSI/CR510_13_14/BosmaLenstra.pdf>
+    "Commplete Systems of Addition Laws" by Bosma and Lenstra;
+    optimized in <https://eprint.iacr.org/2015/1060.pdf> "Complete
+    addition formulas for prime order elliptic curves" Algorithm 1
+    "Complete, projective point addition for arbitrary prime order
+    short Weierstrass curves" by Joost Renes, Craig Costello, and
+    Lejla Batina. *)
+
+    Ltac t :=
+      repeat match goal with
+             | _ => solve [ contradiction | trivial ]
+             | _ => progress cbv zeta
+             | _ => progress intros
+             | _ => progress destruct_head' @W.point
+             | _ => progress destruct_head' sum
+             | _ => progress destruct_head' prod
+             | _ => progress destruct_head' unit
+             | _ => progress destruct_head' and
+             | _ => progress specialize_by assumption
+             | _ => progress cbv [W.eq W.add W.coordinates proj1_sig] in *
+             | _ => progress break_match_hyps
+             | _ => progress break_match
+             | |- _ /\ _ => split
+             end.
+
+    Definition point : Type := { P : F*F*F | let '(X,Y,Z) := P in Y^2*Z = X^3 + a*X*Z^2 + b*Z^3 /\ (Z = 0 -> Y <> 0) }.
+
+    Program Definition to_affine (P:point) : Wpoint :=
+      match proj1_sig P return F*F+_ with
+      | (X, Y, Z) =>
+        if dec (Z = 0) then inr tt
+        else inl (X/Z, Y/Z)
+      end.
+    Next Obligation. Proof. t. fsatz. Qed.
+
+    Program Definition of_affine (P:Wpoint) : point :=
+      match W.coordinates P return F*F*F with
+      | inl (x, y) => (x, y, 1)
+      | inr _ => (0, 1, 0)
+      end.
+    Next Obligation. Proof. t; fsatz. Qed.
+
+    Program Definition opp (P:point) : point :=
+      match proj1_sig P return F*F*F with
+      | (X, Y, Z) => (X, Fopp Y, Z)
+      end.
+    Next Obligation. Proof. t; fsatz. Qed.
+
+    Context (three_b:F) (three_b_correct: three_b = b+b+b).
+    Local Notation "4" := (1+1+1+1). Local Notation "27" := (4*4 + 4+4 +1+1+1).
+    Context {discriminant_nonzero: id(4*a*a*a + 27*b*b <> 0)}.
+
+    Program Definition add (P Q:point)
+            (y_PmQ_nz: match W.coordinates (W.add (to_affine P) (to_affine (opp Q))) return Prop with
+                       | inr _ => True
+                       | inl (_, y) => y <> 0
+                       end) : point :=
+      match proj1_sig P, proj1_sig Q return F*F*F with (X1, Y1, Z1), (X2, Y2, Z2) =>
+        let t0 := X1*X2 in
+        let t1 := Y1*Y2 in
+        let t2 := Z1*Z2 in
+        let t3 := X1+Y1 in
+        let t4 := X2+Y2 in
+        let t3 := t3*t4 in
+        let t4 := t0+t1 in
+        let t3 := t3-t4 in
+        let t4 := X1+Z1 in
+        let t5 := X2+Z2 in
+        let t4 := t4*t5 in
+        let t5 := t0+t2 in
+        let t4 := t4-t5 in
+        let t5 := Y1+Z1 in
+        let X3 := Y2+Z2 in
+        let t5 := t5*X3 in
+        let X3 := t1+t2 in
+        let t5 := t5-X3 in
+        let Z3 := a*t4 in
+        let X3 := three_b*t2 in
+        let Z3 := X3+Z3 in
+        let X3 := t1-Z3 in
+        let Z3 := t1+Z3 in
+        let Y3 := X3*Z3 in
+        let t1 := t0+t0 in
+        let t1 := t1+t0 in
+        let t2 := a*t2 in
+        let t4 := three_b*t4 in
+        let t1 := t1+t2 in
+        let t2 := t0-t2 in
+        let t2 := a*t2 in
+        let t4 := t4+t2 in
+        let t0 := t1*t4 in
+        let Y3 := Y3+t0 in
+        let t0 := t5*t4 in
+        let X3 := t3*X3 in
+        let X3 := X3-t0 in
+        let t0 := t3*t1 in
+        let Z3 := t5*Z3 in
+        let Z3 := Z3+t0 in
+        (X3, Y3, Z3)
+      end.
+    Next Obligation.
+    Proof.
+      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
+      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      t.
+      all: try abstract fsatz.
+      (* FIXME: the final fsatz starts requiring 56 <> 0 if
+           - the next assert block is removed
+           - the assertion is changed to [Y2 = Fopp Y1] *)
+      assert (Y2 / Z2 = Fopp (Y1 / Z1)) by (
+        assert (forall pfP pfQ, match W.coordinates (W.add (to_affine (exist _ (X1,Y1,Z1) pfP)) (to_affine (exist _ (X2,Y2,Z2) pfQ))) with inl _ => False | _ => True end) by (cbv [to_affine]; t; fsatz); cbv [to_affine] in *; t; specialize_by (t;fsatz); t; fsatz).
+      unfold id in discriminant_nonzero; fsatz.
+    Qed.
+
+    Lemma to_affine_add P Q H :
+      W.eq
+        (to_affine (add P Q H))
+        (WeierstrassCurve.W.add (to_affine P) (to_affine Q)).
+    Proof.
+      destruct P as [p ?]; destruct p as [p Z1]; destruct p as [X1 Y1].
+      destruct Q as [q ?]; destruct q as [q Z2]; destruct q as [X2 Y2].
+      cbv [add opp to_affine] in *; t.
+      all: try abstract fsatz.
+
+      (* zero + P = P   -- cases for x and y *)
+      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      assert (X1 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+
+      (* P  + zero = P   -- cases for x and y *)
+      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+      assert (X2 = 0) by (setoid_subst_rel Feq; Nsatz.nsatz_power 3%nat); t; fsatz.
+    Qed.
+  End Projective.
+End Projective.
\ No newline at end of file