Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

sage: Fix incompatibility with sage 9.4 #1068

Merged
merged 6 commits into from
Feb 5, 2022
Merged

sage: Fix incompatibility with sage 9.4 #1068

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e108d00
sage: Fix incompatibility with sage 9.4
real-or-random Jan 31, 2022
b54d843
sage: Fix printing of errors
real-or-random Jan 31, 2022
eae7586
sage: Exit with non-zero status in case of failures
real-or-random Jan 31, 2022
77cfa98
sage: Normalize sign of polynomial factors in prover
real-or-random Feb 3, 2022
d8d5485
ci: Run sage prover on CI
real-or-random Feb 3, 2022
ebb1bee
sage: Ensure that constraints are always fastfracs
real-or-random Feb 4, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 42 additions & 19 deletions sage/group_prover.sage
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,30 @@ class constraints:
def __repr__(self):
return "%s" % self

def normalize_factor(p):
"""Normalizes the sign of primitive polynomials (as returned by factor())

This function ensures that the polynomial has a positive leading coefficient.

This is necessary because recent sage versions (starting with v9.3 or v9.4,
we don't know) are inconsistent about the placement of the minus sign in
polynomial factorizations:
```
sage: R.<ax,bx,ay,by,Az,Bz,Ai,Bi> = PolynomialRing(QQ,8,order='invlex')
sage: R((-2 * (bx - ax)) ^ 1).factor()
(-2) * (bx - ax)
sage: R((-2 * (bx - ax)) ^ 2).factor()
(4) * (-bx + ax)^2
sage: R((-2 * (bx - ax)) ^ 3).factor()
(8) * (-bx + ax)^3
```
"""
# Assert p is not 0 and that its non-zero coeffients are coprime.
# (We could just work with the primitive part p/p.content() but we want to be
# aware if factor() does not return a primitive part in future sage versions.)
assert p.content() == 1
# Ensure that the first non-zero coefficient is positive.
return p if p.lc() > 0 else -p
sipa marked this conversation as resolved.
Show resolved Hide resolved

def conflicts(R, con):
"""Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
Expand Down Expand Up @@ -204,10 +228,10 @@ def get_nonzero_set(R, assume):
nonzero = set()
for nz in map(numerator, assume.nonzero):
for (f,n) in nz.factor():
nonzero.add(f)
nonzero.add(normalize_factor(f))
rnz = zero.reduce(nz)
for (f,n) in rnz.factor():
nonzero.add(f)
nonzero.add(normalize_factor(f))
return nonzero


Expand All @@ -222,27 +246,27 @@ def prove_nonzero(R, exprs, assume):
return (False, [exprs[expr]])
allexprs = reduce(lambda a,b: numerator(a)*numerator(b), exprs, 1)
for (f, n) in allexprs.factor():
if f not in nonzero:
if normalize_factor(f) not in nonzero:
ok = False
if ok:
return (True, None)
ok = True
for (f, n) in zero.reduce(numerator(allexprs)).factor():
if f not in nonzero:
for (f, n) in zero.reduce(allexprs).factor():
if normalize_factor(f) not in nonzero:
ok = False
if ok:
return (True, None)
ok = True
for expr in exprs:
for (f,n) in numerator(expr).factor():
if f not in nonzero:
if normalize_factor(f) not in nonzero:
ok = False
if ok:
return (True, None)
ok = True
for expr in exprs:
for (f,n) in zero.reduce(numerator(expr)).factor():
if f not in nonzero:
if normalize_factor(f) not in nonzero:
expl.add(exprs[expr])
if expl:
return (False, list(expl))
Expand All @@ -254,7 +278,7 @@ def prove_zero(R, exprs, assume):
"""Check whether all of the passed expressions are provably zero, given assumptions"""
r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume)
if not r:
return (False, map(lambda x: "Possibly zero denominator: %s" % x, e))
return (False, list(map(lambda x: "Possibly zero denominator: %s" % x, e)))
zero = R.ideal(list(map(numerator, assume.zero)))
nonzero = prod(x for x in assume.nonzero)
expl = []
Expand All @@ -279,17 +303,17 @@ def describe_extra(R, assume, assumeExtra):
if base not in zero:
add = []
for (f, n) in numerator(base).factor():
if f not in nonzero:
add += ["%s" % f]
if normalize_factor(f) not in nonzero:
add += ["%s" % normalize_factor(f)]
if add:
ret.add((" * ".join(add)) + " = 0 [%s]" % assumeExtra.zero[base])
# Iterate over the extra nonzero expressions
for nz in assumeExtra.nonzero:
nzr = zeroextra.reduce(numerator(nz))
if nzr not in zeroextra:
for (f,n) in nzr.factor():
if zeroextra.reduce(f) not in nonzero:
ret.add("%s != 0" % zeroextra.reduce(f))
if normalize_factor(zeroextra.reduce(f)) not in nonzero:
ret.add("%s != 0" % normalize_factor(zeroextra.reduce(f)))
return ", ".join(x for x in ret)


Expand All @@ -299,22 +323,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 "OK (assuming %s)" % describe
else:
return "OK"
return (True, "OK%s" % describe)


def concrete_verify(c):
Expand Down
23 changes: 13 additions & 10 deletions sage/prove_group_implementations.sage
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
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)
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_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 & (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)
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)
success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var, 43)
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is buggy for --exhaustive, let me fix this.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok done. Also cherry-picked a commit from https://github.com/real-or-random/secp256k1/commits/202202-gej_add_ge that I discovered when working on #1033.

Copy link
Contributor

@jonasnick jonasnick Feb 4, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The commit looks fine but is there a specific reason why it was added?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added it because it fixes a bug in the group prover that prevents us to look into other group formulas. In particular, it stopped me from playing around with the formula here because it may return a literal 1: https://github.com/real-or-random/secp256k1/blob/dc53e24a1b63ec07a9ab086280cab1355cd3a881/sage/prove_group_implementations.sage#L209

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, thanks that makes sense.

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 & (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))
11 changes: 10 additions & 1 deletion sage/weierstrass_prover.sage
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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):
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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