From e6ed3705b602cd8e51612ce6d3728654bc2d1aec Mon Sep 17 00:00:00 2001
From: Peter Dettman <peter.dettman@gmail.com>
Date: Sun, 26 Dec 2021 23:42:55 +0700
Subject: [PATCH] Update sage files for new formulae

---
 sage/prove_group_implementations.sage | 74 ++++++++++++---------------
 1 file changed, 32 insertions(+), 42 deletions(-)

diff --git a/sage/prove_group_implementations.sage b/sage/prove_group_implementations.sage
index a97e732f7f..5f807eeb8e 100644
--- a/sage/prove_group_implementations.sage
+++ b/sage/prove_group_implementations.sage
@@ -45,29 +45,26 @@ def formula_secp256k1_gej_add_var(branch, a, b):
   s2 = s2 * a.Z
   h = -u1
   h = h + u2
-  i = -s1
-  i = i + s2
+  i = -s2
+  i = i + s1
   if branch == 2:
     r = formula_secp256k1_gej_double_var(a)
     return (constraints(), constraints(zero={h : 'h=0', i : 'i=0', a.Infinity : 'a_finite', b.Infinity : 'b_finite'}), r)
   if branch == 3:
     return (constraints(), constraints(zero={h : 'h=0', a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={i : 'i!=0'}), point_at_infinity())
-  i2 = i^2
+  t = h * b.Z
+  rz = a.Z * t
   h2 = h^2
+  h2 = -h2
   h3 = h2 * h
-  h = h * b.Z
-  rz = a.Z * h
   t = u1 * h2
-  rx = t
-  rx = rx * 2
+  rx = i^2
   rx = rx + h3
-  rx = -rx
-  rx = rx + i2
-  ry = -rx
-  ry = ry + t
-  ry = ry * i
+  rx = rx + t
+  rx = rx + t
+  t = t + rx
+  ry = t * i
   h3 = h3 * s1
-  h3 = -h3
   ry = ry + h3
   return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz))
 
@@ -85,36 +82,31 @@ def formula_secp256k1_gej_add_ge_var(branch, a, b):
   s2 = s2 * a.Z
   h = -u1
   h = h + u2
-  i = -s1
-  i = i + s2
+  i = -s2
+  i = i + s1
   if (branch == 2):
     r = formula_secp256k1_gej_double_var(a)
     return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0', i : 'i=0'}), r)
   if (branch == 3):
     return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0'}, nonzero={i : 'i!=0'}), point_at_infinity())
-  i2 = i^2
-  h2 = h^2
-  h3 = h * h2
   rz = a.Z * h
+  h2 = h^2
+  h2 = -h2
+  h3 = h2 * h
   t = u1 * h2
-  rx = t
-  rx = rx * 2
+  rx = i^2
   rx = rx + h3
-  rx = -rx
-  rx = rx + i2
-  ry = -rx
-  ry = ry + t
-  ry = ry * i
+  rx = rx + t
+  rx = rx + t
+  t = t + rx
+  ry = t * i
   h3 = h3 * s1
-  h3 = -h3
   ry = ry + h3
   return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz))
 
 def formula_secp256k1_gej_add_zinv_var(branch, a, b):
   """libsecp256k1's secp256k1_gej_add_zinv_var"""
   bzinv = b.Z^(-1)
-  if branch == 0:
-    return (constraints(), constraints(nonzero={b.Infinity : 'b_infinite'}), a)
   if branch == 1:
     bzinv2 = bzinv^2
     bzinv3 = bzinv2 * bzinv
@@ -122,6 +114,8 @@ def formula_secp256k1_gej_add_zinv_var(branch, a, b):
     ry = b.Y * bzinv3
     rz = 1
     return (constraints(), constraints(zero={b.Infinity : 'b_finite'}, nonzero={a.Infinity : 'a_infinite'}), jacobianpoint(rx, ry, rz))
+  if branch == 0:
+    return (constraints(), constraints(nonzero={b.Infinity : 'b_infinite'}), a)
   azz = a.Z * bzinv
   z12 = azz^2
   u1 = a.X
@@ -131,29 +125,25 @@ def formula_secp256k1_gej_add_zinv_var(branch, a, b):
   s2 = s2 * azz
   h = -u1
   h = h + u2
-  i = -s1
-  i = i + s2
+  i = -s2
+  i = i + s1
   if branch == 2:
     r = formula_secp256k1_gej_double_var(a)
     return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0', i : 'i=0'}), r)
   if branch == 3:
     return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0'}, nonzero={i : 'i!=0'}), point_at_infinity())
-  i2 = i^2
+  rz = a.Z * h
   h2 = h^2
-  h3 = h * h2
-  rz = a.Z
-  rz = rz * h
+  h2 = -h2
+  h3 = h2 * h
   t = u1 * h2
-  rx = t
-  rx = rx * 2
+  rx = i^2
   rx = rx + h3
-  rx = -rx
-  rx = rx + i2
-  ry = -rx
-  ry = ry + t
-  ry = ry * i
+  rx = rx + t
+  rx = rx + t
+  t = t + rx
+  ry = t * i
   h3 = h3 * s1
-  h3 = -h3
   ry = ry + h3
   return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz))