change weierstrass spec, prove most cases of associativity

1 files changed, 13 insertions, 7 deletions

diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 8b5480620..3f8ab2100 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -48,18 +48,24 @@ Module W.
            _
            (match coordinates P1, coordinates P2 return _ with
             | (x1, y1), (x2, y2) =>
-              if x1 =? x2 then
-                if y2 =? -y1 then ∞
-                else  ((3*x1^2+a)^2 / (2*y1)^2 - x1 - x1,
-                        (2*x1+x1)*(3*x1^2+a) / (2*y1) - (3*x1^2+a)^3/(2*y1)^3-y1)
-              else    ((y2-y1)^2 / (x2-x1)^2 - x1 - x2,
-                        (2*x1+x2)*(y2-y1) / (x2-x1) - (y2-y1)^3 / (x2-x1)^3 - y1)
+              if x1 =? x2
+              then
+                if y2 =? -y1
+                then ∞
+                else let k := (3*x1^2+a)/(2*y1) in
+                     let x3 := k^2-x1-x1 in
+                     let y3 := k*(x1-x3)-y1 in
+                     (x3, y3)
+              else let k := (y2-y1)/(x2-x1) in
+                   let x3 := k^2-x1-x2 in
+                   let y3 := k*(x1-x3)-y1 in
+                   (x3, y3)
             | ∞, ∞ => ∞
             | ∞, _ => coordinates P2
             | _, ∞ => coordinates P1
             end)
            _.
-    Next Obligation. exact (Pre.unifiedAdd'_onCurve _ _ (proj2_sig _) (proj2_sig _)). Qed.
+    Next Obligation. Admitted.
 
     Fixpoint mul (n:nat) (P : point) : point :=
       match n with