Changeset View
Changeset View
Standalone View
Standalone View
src/secp256k1/sage/prove_group_implementations.sage
| Show First 20 Lines • Show All 142 Lines • ▼ Show 20 Lines | def formula_secp256k1_gej_add_zinv_var(branch, a, b): | ||||
| ry = ry + h3 | ry = ry + h3 | ||||
| return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz)) | return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz)) | ||||
| def formula_secp256k1_gej_add_ge(branch, a, b): | def formula_secp256k1_gej_add_ge(branch, a, b): | ||||
| """libsecp256k1's secp256k1_gej_add_ge""" | """libsecp256k1's secp256k1_gej_add_ge""" | ||||
| zeroes = {} | zeroes = {} | ||||
| nonzeroes = {} | nonzeroes = {} | ||||
| a_infinity = False | a_infinity = False | ||||
| if (branch & 4) != 0: | if (branch & 2) != 0: | ||||
| nonzeroes.update({a.Infinity : 'a_infinite'}) | nonzeroes.update({a.Infinity : 'a_infinite'}) | ||||
| a_infinity = True | a_infinity = True | ||||
| else: | else: | ||||
| zeroes.update({a.Infinity : 'a_finite'}) | zeroes.update({a.Infinity : 'a_finite'}) | ||||
| zz = a.Z^2 | zz = a.Z^2 | ||||
| u1 = a.X | u1 = a.X | ||||
| u2 = b.X * zz | u2 = b.X * zz | ||||
| s1 = a.Y | s1 = a.Y | ||||
| s2 = b.Y * zz | s2 = b.Y * zz | ||||
| s2 = s2 * a.Z | s2 = s2 * a.Z | ||||
| t = u1 | t = u1 | ||||
| t = t + u2 | t = t + u2 | ||||
| m = s1 | m = s1 | ||||
| m = m + s2 | m = m + s2 | ||||
| rr = t^2 | rr = t^2 | ||||
| m_alt = -u2 | m_alt = -u2 | ||||
| tt = u1 * m_alt | tt = u1 * m_alt | ||||
| rr = rr + tt | rr = rr + tt | ||||
| degenerate = (branch & 3) == 3 | degenerate = (branch & 1) != 0 | ||||
| if (branch & 1) != 0: | if degenerate: | ||||
| zeroes.update({m : 'm_zero'}) | zeroes.update({m : 'm_zero'}) | ||||
| else: | else: | ||||
| nonzeroes.update({m : 'm_nonzero'}) | 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 = s1 | ||||
| rr_alt = rr_alt * 2 | rr_alt = rr_alt * 2 | ||||
| m_alt = m_alt + u1 | m_alt = m_alt + u1 | ||||
| if not degenerate: | if not degenerate: | ||||
| rr_alt = rr | rr_alt = rr | ||||
| m_alt = m | m_alt = m | ||||
| n = m_alt^2 | n = m_alt^2 | ||||
| q = -t | q = -t | ||||
| q = q * n | q = q * n | ||||
| n = n^2 | n = n^2 | ||||
| if degenerate: | if degenerate: | ||||
| n = m | n = m | ||||
| t = rr_alt^2 | t = rr_alt^2 | ||||
| rz = a.Z * m_alt | 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 | t = t + q | ||||
| rx = t | rx = t | ||||
| t = t * 2 | t = t * 2 | ||||
| t = t + q | t = t + q | ||||
| t = t * rr_alt | t = t * rr_alt | ||||
| t = t + n | t = t + n | ||||
| ry = -t | ry = -t | ||||
| ry = ry / 2 | ry = ry / 2 | ||||
| if a_infinity: | if a_infinity: | ||||
| rx = b.X | rx = b.X | ||||
| ry = b.Y | ry = b.Y | ||||
| rz = 1 | 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()) | 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)) | 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): | def formula_secp256k1_gej_add_ge_old(branch, a, b): | ||||
| """libsecp256k1's old secp256k1_gej_add_ge, which fails when ay+by=0 but ax!=bx""" | """libsecp256k1's old secp256k1_gej_add_ge, which fails when ay+by=0 but ax!=bx""" | ||||
| a_infinity = (branch & 1) != 0 | a_infinity = (branch & 1) != 0 | ||||
| zero = {} | zero = {} | ||||
| nonzero = {} | nonzero = {} | ||||
| if a_infinity: | if a_infinity: | ||||
| ▲ Show 20 Lines • Show All 53 Lines • ▼ Show 20 Lines | if infinity: | ||||
| return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), point_at_infinity()) | return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), point_at_infinity()) | ||||
| return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), jacobianpoint(rx, ry, rz)) | 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__": | if __name__ == "__main__": | ||||
| success = True | success = True | ||||
| 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_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_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_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)) | 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": | 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_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_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_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)) | 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)) | sys.exit(int(not success)) | ||||