Merge #1078: group: Save a normalize_to_zero in gej_add_ge

e089eec group: Further simply gej_add_ge (Tim Ruffing)
ac71020 group: Save a normalize_to_zero in gej_add_ge (Tim Ruffing)

Pull request description:

  As discovered  by sipa in #1033.

  See commit message for reasoning but note that the infinity handling will be replaced in the second commit again.

ACKs for top commit:
  sipa:
    ACK e089eec
  apoelstra:
    ACK e089eec

Tree-SHA512: fb1b5742e73dd8b2172b4d3e2852490cfd626e8673b72274d281fa34b04e9368a186895fb9cd232429c22b14011df136f4c09bdc7332beef2b3657f7f2798d66

Author: sipa

sage/prove_group_implementations.sage

@@ -148,7 +148,7 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
   zeroes = {}
   nonzeroes = {}
   a_infinity = False
-  if (branch & 4) != 0:
+  if (branch & 2) != 0:
     nonzeroes.update({a.Infinity : 'a_infinite'})
     a_infinity = True
   else:
@@ -167,15 +167,11 @@ def formula_secp256k1_gej_add_ge(branch, a, b):
   m_alt = -u2
   tt = u1 * m_alt
   rr = rr + tt
-  degenerate = (branch & 3) == 3
-  if (branch & 1) != 0:
+  degenerate = (branch & 1) != 0
+  if degenerate:
     zeroes.update({m : 'm_zero'})
   else:
     nonzeroes.update({m : 'm_nonzero'})
-  if (branch & 2) != 0:
-    zeroes.update({rr : 'rr_zero'})
-  else:
-    nonzeroes.update({rr : 'rr_nonzero'})
   rr_alt = s1
   rr_alt = rr_alt * 2
   m_alt = m_alt + u1
@@ -190,13 +186,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 & 8) != 0:
-    if not a_infinity:
-      infinity = True
-    zeroes.update({rz : 'r.z=0'})
-  else:
-    nonzeroes.update({rz : 'r.z!=0'})
   t = t + q
   rx = t
   t = t * 2
@@ -209,8 +198,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):
@@ -280,14 +272,14 @@ if __name__ == "__main__":
   success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var)
   success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var)
   success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var)
-  success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 16, formula_secp256k1_gej_add_ge)
+  success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 8, formula_secp256k1_gej_add_ge)
   success = success & (not check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old))
 
   if len(sys.argv) >= 2 and sys.argv[1] == "--exhaustive":
     success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var, 43)
     success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var, 43)
     success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var, 43)
-    success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 16, formula_secp256k1_gej_add_ge, 43)
+    success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 8, formula_secp256k1_gej_add_ge, 43)
     success = success & (not check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old, 43))
 
   sys.exit(int(not success))

src/group_impl.h

@@ -532,11 +532,11 @@ 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);
 
-    /** In:
+    /*  In:
      *    Eric Brier and Marc Joye, Weierstrass Elliptic Curves and Side-Channel Attacks.
      *    In D. Naccache and P. Paillier, Eds., Public Key Cryptography, vol. 2274 of Lecture Notes in Computer Science, pages 335-345. Springer-Verlag, 2002.
      *  we find as solution for a unified addition/doubling formula:
@@ -598,10 +598,9 @@ static void secp256k1_gej_add_ge(secp256k1_gej *r, const secp256k1_gej *a, const
     secp256k1_fe_negate(&m_alt, &u2, 1);                /* Malt = -X2*Z1^2 */
     secp256k1_fe_mul(&tt, &u1, &m_alt);                 /* tt = -U1*U2 (2) */
     secp256k1_fe_add(&rr, &tt);                         /* rr = R = T^2-U1*U2 (3) */
-    /** If lambda = R/M = 0/0 we have a problem (except in the "trivial"
-     *  case that Z = z1z2 = 0, and this is special-cased later on). */
-    degenerate = secp256k1_fe_normalizes_to_zero(&m) &
-                 secp256k1_fe_normalizes_to_zero(&rr);
+    /* If lambda = R/M = R/0 we have a problem (except in the "trivial"
+     * case that Z = z1z2 = 0, and this is special-cased later on). */
+    degenerate = secp256k1_fe_normalizes_to_zero(&m);
     /* This only occurs when y1 == -y2 and x1^3 == x2^3, but x1 != x2.
      * This means either x1 == beta*x2 or beta*x1 == x2, where beta is
      * a nontrivial cube root of one. In either case, an alternate
@@ -613,7 +612,7 @@ static void secp256k1_gej_add_ge(secp256k1_gej *r, const secp256k1_gej *a, const
 
     secp256k1_fe_cmov(&rr_alt, &rr, !degenerate);
     secp256k1_fe_cmov(&m_alt, &m, !degenerate);
-    /* Now Ralt / Malt = lambda and is guaranteed not to be 0/0.
+    /* Now Ralt / Malt = lambda and is guaranteed not to be Ralt / 0.
      * From here on out Ralt and Malt represent the numerator
      * and denominator of lambda; R and M represent the explicit
      * expressions x1^2 + x2^2 + x1x2 and y1 + y2. */
@@ -628,7 +627,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) */
@@ -638,11 +636,28 @@ 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;
+
+    /* Set r->infinity if r->z is 0.
+     *
+     * If a->infinity is set, then r->infinity = (r->z == 0) = (1 == 0) = false,
+     * which is correct because the function assumes that b is not infinity.
+     *
+     * Now assume !a->infinity. This implies Z = Z1 != 0.
+     *
+     * Case y1 = -y2:
+     * In this case we could have a = -b, namely if x1 = x2.
+     * We have degenerate = true, r->z = (x1 - x2) * Z.
+     * Then r->infinity = ((x1 - x2)Z == 0) = (x1 == x2) = (a == -b).
+     *
+     * Case y1 != -y2:
+     * In this case, we can't have a = -b.
+     * We have degenerate = false, r->z = (y1 + y2) * Z.
+     * Then r->infinity = ((y1 + y2)Z == 0) = (y1 == -y2) = false. */
+    r->infinity = secp256k1_fe_normalizes_to_zero(&r->z);
 }
 
 static void secp256k1_gej_rescale(secp256k1_gej *r, const secp256k1_fe *s) {