You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
306 lines
8.6 KiB
306 lines
8.6 KiB
# 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)
|
|
|