sage: Exit with non-zero status in case of failures

sage/group_prover.sage

@@ -299,22 +299,21 @@ def check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require):
 
   if conflicts(R, assume):
     # This formula does not apply
-    return None
+    return (True, None)
 
   describe = describe_extra(R, assumeLaw + assumeBranch, assumeAssert)
+  if describe != "":
+    describe = " (assuming " + describe + ")"
 
   ok, msg = prove_zero(R, require.zero, assume)
   if not ok:
-    return "FAIL, %s fails (assuming %s)" % (str(msg), describe)
+    return (False, "FAIL, %s fails%s" % (str(msg), describe))
 
   res, expl = prove_nonzero(R, require.nonzero, assume)
   if not res:
-    return "FAIL, %s fails (assuming %s)" % (str(expl), describe)
+    return (False, "FAIL, %s fails%s" % (str(expl), describe))
 
-  if describe != "":
+  return (True, "OK%s" % describe)
-    return "OK (assuming %s)" % describe
-  else:
-    return "OK"
 
 
 def concrete_verify(c):

sage/prove_group_implementations.sage

@@ -292,15 +292,18 @@ def formula_secp256k1_gej_add_ge_old(branch, a, b):
   return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), jacobianpoint(rx, ry, rz))
 
 if __name__ == "__main__":
-  check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var)
+  success = True
-  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_var", 0, 7, 5, formula_secp256k1_gej_add_var)
-  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_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var)
-  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_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var)
-  check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old)
+  success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 16, 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":
-    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_var", 0, 7, 5, formula_secp256k1_gej_add_var, 43)
-    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_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var, 43)
-    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_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var, 43)
-    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, 16, formula_secp256k1_gej_add_ge, 43)
-    check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old, 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))

sage/weierstrass_prover.sage

@@ -184,6 +184,7 @@ def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):
       if r:
         points.append(point)
 
+  ret = True
   for za in range(1, p):
     for zb in range(1, p):
       for pa in points:
@@ -211,8 +212,11 @@ def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):
                         match = True
                       r, e = concrete_verify(require)
                       if not r:
+                        ret = False
                         print("  failure in branch %i for (%s,%s,%s,%s) + (%s,%s,%s,%s) = (%s,%s,%s,%s): %s" % (branch, pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity, pC.X, pC.Y, pC.Z, pC.Infinity, e))
+
   print()
+  return ret
 
 
 def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC):
@@ -244,6 +248,7 @@ def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
 
   print("Formula " + name + ":")
   count = 0
+  ret = True
   for branch in range(branches):
     assumeFormula, assumeBranch, pC = formula(branch, pA, pB)
     pC.X = lift(pC.X)
@@ -252,7 +257,10 @@ def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
     pC.Infinity = lift(pC.Infinity)
 
     for key in laws_jacobian_weierstrass:
-      res[key].append((check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC), branch))
+      success, msg = check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC)
+      if not success:
+        ret = False
+      res[key].append((msg, branch))
 
   for key in res:
     print("  %s:" % key)
@@ -262,3 +270,4 @@ def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
         print("    branch %i: %s" % (x[1], x[0]))
 
   print()
+  return ret