1 files changed, 306 insertions, 0 deletions
diff --git a/crypto/secp256k1/libsecp256k1/sage/secp256k1.sage b/crypto/secp256k1/libsecp256k1/sage/secp256k1.sage
new file mode 100644
index 000000000..a97e732f7
--- /dev/null
+++ b/crypto/secp256k1/libsecp256k1/sage/secp256k1.sage
@@ -0,0 +1,306 @@
+# Test libsecp256k1' group operation implementations using prover.sage
+
+import sys
+
+load("group_prover.sage")
+load("weierstrass_prover.sage")
+
+def formula_secp256k1_gej_double_var(a):
+  """libsecp256k1's secp256k1_gej_double_var, used by various addition functions"""
+  rz = a.Z * a.Y
+  rz = rz * 2
+  t1 = a.X^2
+  t1 = t1 * 3
+  t2 = t1^2
+  t3 = a.Y^2
+  t3 = t3 * 2
+  t4 = t3^2
+  t4 = t4 * 2
+  t3 = t3 * a.X
+  rx = t3
+  rx = rx * 4
+  rx = -rx
+  rx = rx + t2
+  t2 = -t2
+  t3 = t3 * 6
+  t3 = t3 + t2
+  ry = t1 * t3
+  t2 = -t4
+  ry = ry + t2
+  return jacobianpoint(rx, ry, rz)
+
+def formula_secp256k1_gej_add_var(branch, a, b):
+  """libsecp256k1's secp256k1_gej_add_var"""
+  if branch == 0:
+    return (constraints(), constraints(nonzero={a.Infinity : 'a_infinite'}), b)
+  if branch == 1:
+    return (constraints(), constraints(zero={a.Infinity : 'a_finite'}, nonzero={b.Infinity : 'b_infinite'}), a)
+  z22 = b.Z^2
+  z12 = a.Z^2
+  u1 = a.X * z22
+  u2 = b.X * z12
+  s1 = a.Y * z22
+  s1 = s1 * b.Z
+  s2 = b.Y * z12
+  s2 = s2 * a.Z
+  h = -u1
+  h = h + u2
+  i = -s1
+  i = i + s2
+  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
+  h2 = h^2
+  h3 = h2 * h
+  h = h * b.Z
+  rz = a.Z * h
+  t = u1 * h2
+  rx = t
+  rx = rx * 2
+  rx = rx + h3
+  rx = -rx
+  rx = rx + i2
+  ry = -rx
+  ry = ry + t
+  ry = ry * 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))
+
+def formula_secp256k1_gej_add_ge_var(branch, a, b):
+  """libsecp256k1's secp256k1_gej_add_ge_var, which assume bz==1"""
+  if branch == 0:
+    return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(nonzero={a.Infinity : 'a_infinite'}), b)
+  if branch == 1:
+    return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite'}, nonzero={b.Infinity : 'b_infinite'}), a)
+  z12 = a.Z^2
+  u1 = a.X
+  u2 = b.X * z12
+  s1 = a.Y
+  s2 = b.Y * z12
+  s2 = s2 * a.Z
+  h = -u1
+  h = h + u2
+  i = -s1
+  i = i + s2
+  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
+  t = u1 * h2
+  rx = t
+  rx = rx * 2
+  rx = rx + h3
+  rx = -rx
+  rx = rx + i2
+  ry = -rx
+  ry = ry + t
+  ry = ry * 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
+    rx = b.X * bzinv2
+    ry = b.Y * bzinv3
+    rz = 1
+    return (constraints(), constraints(zero={b.Infinity : 'b_finite'}, nonzero={a.Infinity : 'a_infinite'}), jacobianpoint(rx, ry, rz))
+  azz = a.Z * bzinv
+  z12 = azz^2
+  u1 = a.X
+  u2 = b.X * z12
+  s1 = a.Y
+  s2 = b.Y * z12
+  s2 = s2 * azz
+  h = -u1
+  h = h + u2
+  i = -s1
+  i = i + s2
+  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
+  h2 = h^2
+  h3 = h * h2
+  rz = a.Z
+  rz = rz * h
+  t = u1 * h2
+  rx = t
+  rx = rx * 2
+  rx = rx + h3
+  rx = -rx
+  rx = rx + i2
+  ry = -rx
+  ry = ry + t
+  ry = ry * 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))
+
+def formula_secp256k1_gej_add_ge(branch, a, b):
+  """libsecp256k1's secp256k1_gej_add_ge"""
+  zeroes = {}
+  nonzeroes = {}
+  a_infinity = False
+  if (branch & 4) != 0:
+    nonzeroes.update({a.Infinity : 'a_infinite'})
+    a_infinity = True
+  else:
+    zeroes.update({a.Infinity : 'a_finite'})
+  zz = a.Z^2
+  u1 = a.X
+  u2 = b.X * zz
+  s1 = a.Y
+  s2 = b.Y * zz
+  s2 = s2 * a.Z
+  t = u1
+  t = t + u2
+  m = s1
+  m = m + s2
+  rr = t^2
+  m_alt = -u2
+  tt = u1 * m_alt
+  rr = rr + tt
+  degenerate = (branch & 3) == 3
+  if (branch & 1) != 0:
+    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
+  if not degenerate:
+    rr_alt = rr
+    m_alt = m
+  n = m_alt^2
+  q = n * t
+  n = n^2
+  if degenerate:
+    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'})
+  rz = rz * 2
+  q = -q
+  t = t + q
+  rx = t
+  t = t * 2
+  t = t + q
+  t = t * rr_alt
+  t = t + n
+  ry = -t
+  rx = rx * 4
+  ry = ry * 4
+  if a_infinity:
+    rx = b.X
+    ry = b.Y
+    rz = 1
+  if infinity:
+    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), jacobianpoint(rx, ry, rz))
+
+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"""
+  a_infinity = (branch & 1) != 0
+  zero = {}
+  nonzero = {}
+  if a_infinity:
+    nonzero.update({a.Infinity : 'a_infinite'})
+  else:
+    zero.update({a.Infinity : 'a_finite'})
+  zz = a.Z^2
+  u1 = a.X
+  u2 = b.X * zz
+  s1 = a.Y
+  s2 = b.Y * zz
+  s2 = s2 * a.Z
+  z = a.Z
+  t = u1
+  t = t + u2
+  m = s1
+  m = m + s2
+  n = m^2
+  q = n * t
+  n = n^2
+  rr = t^2
+  t = u1 * u2
+  t = -t
+  rr = rr + t
+  t = rr^2
+  rz = m * z
+  infinity = False
+  if (branch & 2) != 0:
+    if not a_infinity:
+      infinity = True
+    else:
+      return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(nonzero={z : 'conflict_a'}, zero={z : 'conflict_b'}), point_at_infinity())
+    zero.update({rz : 'r.z=0'})
+  else:
+    nonzero.update({rz : 'r.z!=0'})
+  rz = rz * (0 if a_infinity else 2)
+  rx = t
+  q = -q
+  rx = rx + q
+  q = q * 3
+  t = t * 2
+  t = t + q
+  t = t * rr
+  t = t + n
+  ry = -t
+  rx = rx * (0 if a_infinity else 4)
+  ry = ry * (0 if a_infinity else 4)
+  t = b.X
+  t = t * (1 if a_infinity else 0)
+  rx = rx + t
+  t = b.Y
+  t = t * (1 if a_infinity else 0)
+  ry = ry + t
+  t = (1 if a_infinity else 0)
+  rz = rz + t
+  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), jacobianpoint(rx, ry, rz))
+
+if __name__ == "__main__":
+  check_symbolic_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var)
+  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_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var)
+  check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 16, formula_secp256k1_gej_add_ge)
+  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)
+    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)
+    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)