From e09860ee6ec8fa5b2b541a8854c9786a32496283 Mon Sep 17 00:00:00 2001
From: Tim Ruffing <crypto@timruffing.de>
Date: Fri, 4 Feb 2022 15:24:33 +0100
Subject: [PATCH] group: Further simply gej_add_ge

---
 sage/prove_group_implementations.sage | 11 ++++-------
 src/group_impl.h                      | 19 +++++++++++++++----
 2 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/sage/prove_group_implementations.sage b/sage/prove_group_implementations.sage
index b6bdfa3e76..3aa5ad911e 100644
--- a/sage/prove_group_implementations.sage
+++ b/sage/prove_group_implementations.sage
@@ -195,12 +195,6 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
     n = m
   t = rr_alt^2
   rz = a.Z * m_alt
-  infinity = False
-  if (branch & 4) != 0:
-    infinity = True
-    zeroes.update({rz : 'r.z = 0'})
-  else:
-    nonzeroes.update({rz : 'r.z != 0'})
   t = t + q
   rx = t
   t = t * 2
@@ -213,8 +207,11 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
     rx = b.X
     ry = b.Y
     rz = 1
-  if infinity:
+  if (branch & 4) != 0:
+    zeroes.update({rz : 'r.z = 0'})
     return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zeroes, nonzero=nonzeroes), point_at_infinity())
+  else:
+    nonzeroes.update({rz : 'r.z != 0'})
   return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zeroes, nonzero=nonzeroes), jacobianpoint(rx, ry, rz))
 
 def formula_secp256k1_gej_add_ge_old(branch, a, b):
diff --git a/src/group_impl.h b/src/group_impl.h
index a028cc53c6..cadb0d3583 100644
--- a/src/group_impl.h
+++ b/src/group_impl.h
@@ -492,7 +492,7 @@ static void secp256k1_gej_add_ge(secp256k1_gej *r, const secp256k1_gej *a, const
     /* Operations: 7 mul, 5 sqr, 24 add/cmov/half/mul_int/negate/normalize_weak/normalizes_to_zero */
     secp256k1_fe zz, u1, u2, s1, s2, t, tt, m, n, q, rr;
     secp256k1_fe m_alt, rr_alt;
-    int infinity, degenerate;
+    int degenerate;
     VERIFY_CHECK(!b->infinity);
     VERIFY_CHECK(a->infinity == 0 || a->infinity == 1);
 
@@ -587,7 +587,6 @@ static void secp256k1_gej_add_ge(secp256k1_gej *r, const secp256k1_gej *a, const
     secp256k1_fe_cmov(&n, &m, degenerate);              /* n = M^3 * Malt (2) */
     secp256k1_fe_sqr(&t, &rr_alt);                      /* t = Ralt^2 (1) */
     secp256k1_fe_mul(&r->z, &a->z, &m_alt);             /* r->z = Z3 = Malt*Z (1) */
-    infinity = secp256k1_fe_normalizes_to_zero(&r->z) & ~a->infinity;
     secp256k1_fe_add(&t, &q);                           /* t = Ralt^2 + Q (2) */
     r->x = t;                                           /* r->x = X3 = Ralt^2 + Q (2) */
     secp256k1_fe_mul_int(&t, 2);                        /* t = 2*X3 (4) */
@@ -597,11 +596,23 @@ static void secp256k1_gej_add_ge(secp256k1_gej *r, const secp256k1_gej *a, const
     secp256k1_fe_negate(&r->y, &t, 3);                  /* r->y = -(Ralt*(2*X3 + Q) + M^3*Malt) (4) */
     secp256k1_fe_half(&r->y);                           /* r->y = Y3 = -(Ralt*(2*X3 + Q) + M^3*Malt)/2 (3) */
 
-    /** In case a->infinity == 1, replace r with (b->x, b->y, 1). */
+    /* In case a->infinity == 1, replace r with (b->x, b->y, 1). */
     secp256k1_fe_cmov(&r->x, &b->x, a->infinity);
     secp256k1_fe_cmov(&r->y, &b->y, a->infinity);
     secp256k1_fe_cmov(&r->z, &secp256k1_fe_one, a->infinity);
-    r->infinity = infinity;
+
+    /* If a->infinity = 1 then r->infinity = (1 == 0) = 0.
+
+       Now assume a->infinity = 0. This implies Z = Z1 != 0.
+
+       Case y1 = -y2:
+       We have degenerate = 1, r->z = (x1 - x2) * Z.
+       Then r->infinity = ((x1 - x2)Z == 0) = (x1 == -x2) = (a == -b).
+
+       Case y1 != -y2:
+       We have degenerate = 0, r->z = (y1 + y2) * Z.
+       Then r->infinity = ((y1 + y2)Z == 0) = (y1 == y2) = 0. */
+    r->infinity = secp256k1_fe_normalizes_to_zero(&r->z);
 }
 
 static void secp256k1_gej_rescale(secp256k1_gej *r, const secp256k1_fe *s) {