Update sage files for new formulae

- formula_secp256k1_gej_double_var
- formula_secp256k1_gej_add_ge

Author: peterdettman

sage/prove_group_implementations.sage

@@ -8,25 +8,20 @@ load("weierstrass_prover.sage")
 def formula_secp256k1_gej_double_var(a):
   """libsecp256k1's secp256k1_gej_double_var, used by various addition functions"""
   rz = a.Z * a.Y
-  rz = rz * 2
-  t1 = a.X^2
-  t1 = t1 * 3
-  t2 = t1^2
-  t3 = a.Y^2
-  t3 = t3 * 2
-  t4 = t3^2
-  t4 = t4 * 2
-  t3 = t3 * a.X
-  rx = t3
-  rx = rx * 4
-  rx = -rx
-  rx = rx + t2
-  t2 = -t2
-  t3 = t3 * 6
-  t3 = t3 + t2
-  ry = t1 * t3
-  t2 = -t4
-  ry = ry + t2
+  s = a.Y^2
+  l = a.X^2
+  l = l * 3
+  l = l / 2
+  t = -s
+  t = t * a.X
+  rx = l^2
+  rx = rx + t
+  rx = rx + t
+  s = s^2
+  t = t + rx
+  ry = t * l
+  ry = ry + s
+  ry = -ry
   return jacobianpoint(rx, ry, rz)
 
 def formula_secp256k1_gej_add_var(branch, a, b):
@@ -197,7 +192,8 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
     rr_alt = rr
     m_alt = m
   n = m_alt^2
-  q = n * t
+  q = -t
+  q = q * n
   n = n^2
   if degenerate:
     n = m
@@ -210,17 +206,14 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
     zeroes.update({rz : 'r.z=0'})
   else:
     nonzeroes.update({rz : 'r.z!=0'})
-  rz = rz * 2
-  q = -q
   t = t + q
   rx = t
   t = t * 2
   t = t + q
   t = t * rr_alt
   t = t + n
   ry = -t
-  rx = rx * 4
-  ry = ry * 4
+  ry = ry / 2
   if a_infinity:
     rx = b.X
     ry = b.Y