rust-secp256k1-unsafe-fast/secp256k1-sys/depend/secp256k1/sage/group_prover.sage

354 lines
13 KiB
Python
Raw Normal View History

# This code supports verifying group implementations which have branches
# or conditional statements (like cmovs), by allowing each execution path
# to independently set assumptions on input or intermediary variables.
#
# The general approach is:
# * A constraint is a tuple of two sets of symbolic expressions:
# the first of which are required to evaluate to zero, the second of which
# are required to evaluate to nonzero.
# - A constraint is said to be conflicting if any of its nonzero expressions
# is in the ideal with basis the zero expressions (in other words: when the
# zero expressions imply that one of the nonzero expressions are zero).
# * There is a list of laws that describe the intended behaviour, including
# laws for addition and doubling. Each law is called with the symbolic point
# coordinates as arguments, and returns:
# - A constraint describing the assumptions under which it is applicable,
# called "assumeLaw"
# - A constraint describing the requirements of the law, called "require"
# * Implementations are transliterated into functions that operate as well on
# algebraic input points, and are called once per combination of branches
# executed. Each execution returns:
# - A constraint describing the assumptions this implementation requires
# (such as Z1=1), called "assumeFormula"
# - A constraint describing the assumptions this specific branch requires,
# but which is by construction guaranteed to cover the entire space by
# merging the results from all branches, called "assumeBranch"
# - The result of the computation
# * All combinations of laws with implementation branches are tried, and:
# - If the combination of assumeLaw, assumeFormula, and assumeBranch results
# in a conflict, it means this law does not apply to this branch, and it is
# skipped.
# - For others, we try to prove the require constraints hold, assuming the
# information in assumeLaw + assumeFormula + assumeBranch, and if this does
# not succeed, we fail.
# + To prove an expression is zero, we check whether it belongs to the
# ideal with the assumed zero expressions as basis. This test is exact.
# + To prove an expression is nonzero, we check whether each of its
# factors is contained in the set of nonzero assumptions' factors.
# This test is not exact, so various combinations of original and
# reduced expressions' factors are tried.
# - If we succeed, we print out the assumptions from assumeFormula that
# weren't implied by assumeLaw already. Those from assumeBranch are skipped,
# as we assume that all constraints in it are complementary with each other.
#
# Based on the sage verification scripts used in the Explicit-Formulas Database
# by Tanja Lange and others, see https://hyperelliptic.org/EFD
class fastfrac:
"""Fractions over rings."""
def __init__(self,R,top,bot=1):
"""Construct a fractional, given a ring, a numerator, and denominator."""
self.R = R
if parent(top) == ZZ or parent(top) == R:
self.top = R(top)
self.bot = R(bot)
elif top.__class__ == fastfrac:
self.top = top.top
self.bot = top.bot * bot
else:
self.top = R(numerator(top))
self.bot = R(denominator(top)) * bot
def iszero(self,I):
"""Return whether this fraction is zero given an ideal."""
return self.top in I and self.bot not in I
def reduce(self,assumeZero):
zero = self.R.ideal(list(map(numerator, assumeZero)))
return fastfrac(self.R, zero.reduce(self.top)) / fastfrac(self.R, zero.reduce(self.bot))
def __add__(self,other):
"""Add two fractions."""
if parent(other) == ZZ:
return fastfrac(self.R,self.top + self.bot * other,self.bot)
if other.__class__ == fastfrac:
return fastfrac(self.R,self.top * other.bot + self.bot * other.top,self.bot * other.bot)
return NotImplemented
def __sub__(self,other):
"""Subtract two fractions."""
if parent(other) == ZZ:
return fastfrac(self.R,self.top - self.bot * other,self.bot)
if other.__class__ == fastfrac:
return fastfrac(self.R,self.top * other.bot - self.bot * other.top,self.bot * other.bot)
return NotImplemented
def __neg__(self):
"""Return the negation of a fraction."""
return fastfrac(self.R,-self.top,self.bot)
def __mul__(self,other):
"""Multiply two fractions."""
if parent(other) == ZZ:
return fastfrac(self.R,self.top * other,self.bot)
if other.__class__ == fastfrac:
return fastfrac(self.R,self.top * other.top,self.bot * other.bot)
return NotImplemented
def __rmul__(self,other):
"""Multiply something else with a fraction."""
return self.__mul__(other)
def __truediv__(self,other):
"""Divide two fractions."""
if parent(other) == ZZ:
return fastfrac(self.R,self.top,self.bot * other)
if other.__class__ == fastfrac:
return fastfrac(self.R,self.top * other.bot,self.bot * other.top)
return NotImplemented
# Compatibility wrapper for Sage versions based on Python 2
def __div__(self,other):
"""Divide two fractions."""
return self.__truediv__(other)
def __pow__(self,other):
"""Compute a power of a fraction."""
if parent(other) == ZZ:
if other < 0:
# Negative powers require flipping top and bottom
return fastfrac(self.R,self.bot ^ (-other),self.top ^ (-other))
else:
return fastfrac(self.R,self.top ^ other,self.bot ^ other)
return NotImplemented
def __str__(self):
return "fastfrac((" + str(self.top) + ") / (" + str(self.bot) + "))"
def __repr__(self):
return "%s" % self
def numerator(self):
return self.top
class constraints:
"""A set of constraints, consisting of zero and nonzero expressions.
Constraints can either be used to express knowledge or a requirement.
Both the fields zero and nonzero are maps from expressions to description
strings. The expressions that are the keys in zero are required to be zero,
and the expressions that are the keys in nonzero are required to be nonzero.
Note that (a != 0) and (b != 0) is the same as (a*b != 0), so all keys in
nonzero could be multiplied into a single key. This is often much less
efficient to work with though, so we keep them separate inside the
constraints. This allows higher-level code to do fast checks on the individual
nonzero elements, or combine them if needed for stronger checks.
We can't multiply the different zero elements, as it would suffice for one of
the factors to be zero, instead of all of them. Instead, the zero elements are
typically combined into an ideal first.
"""
def __init__(self, **kwargs):
if 'zero' in kwargs:
self.zero = dict(kwargs['zero'])
else:
self.zero = dict()
if 'nonzero' in kwargs:
self.nonzero = dict(kwargs['nonzero'])
else:
self.nonzero = dict()
def negate(self):
return constraints(zero=self.nonzero, nonzero=self.zero)
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
def map(self, fun):
return constraints(zero={fun(k): v for k, v in self.zero.items()}, nonzero={fun(k): v for k, v in self.nonzero.items()})
def __add__(self, other):
zero = self.zero.copy()
zero.update(other.zero)
nonzero = self.nonzero.copy()
nonzero.update(other.nonzero)
return constraints(zero=zero, nonzero=nonzero)
def __str__(self):
return "constraints(zero=%s,nonzero=%s)" % (self.zero, self.nonzero)
def __repr__(self):
return "%s" % self
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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
```
"""
2023-09-27 18:37:09 +00:00
# Assert p is not 0 and that its non-zero coefficients are coprime.
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
# (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
def conflicts(R, con):
"""Check whether any of the passed non-zero assumptions is implied by the zero assumptions"""
zero = R.ideal(list(map(numerator, con.zero)))
if 1 in zero:
return True
# First a cheap check whether any of the individual nonzero terms conflict on
# their own.
for nonzero in con.nonzero:
if nonzero.iszero(zero):
return True
# It can be the case that entries in the nonzero set do not individually
# conflict with the zero set, but their combination does. For example, knowing
# that either x or y is zero is equivalent to having x*y in the zero set.
# Having x or y individually in the nonzero set is not a conflict, but both
# simultaneously is, so that is the right thing to check for.
if reduce(lambda a,b: a * b, con.nonzero, fastfrac(R, 1)).iszero(zero):
return True
return False
def get_nonzero_set(R, assume):
"""Calculate a simple set of nonzero expressions"""
zero = R.ideal(list(map(numerator, assume.zero)))
nonzero = set()
for nz in map(numerator, assume.nonzero):
for (f,n) in nz.factor():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
nonzero.add(normalize_factor(f))
rnz = zero.reduce(nz)
for (f,n) in rnz.factor():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
nonzero.add(normalize_factor(f))
return nonzero
def prove_nonzero(R, exprs, assume):
"""Check whether an expression is provably nonzero, given assumptions"""
zero = R.ideal(list(map(numerator, assume.zero)))
nonzero = get_nonzero_set(R, assume)
expl = set()
ok = True
for expr in exprs:
if numerator(expr) in zero:
return (False, [exprs[expr]])
allexprs = reduce(lambda a,b: numerator(a)*numerator(b), exprs, 1)
for (f, n) in allexprs.factor():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
if normalize_factor(f) not in nonzero:
ok = False
if ok:
return (True, None)
ok = True
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
if normalize_factor(f) not in nonzero:
expl.add(exprs[expr])
if expl:
return (False, list(expl))
else:
return (True, None)
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:
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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 = []
for expr in exprs:
if not expr.iszero(zero):
expl.append(exprs[expr])
if not expl:
return (True, None)
return (False, expl)
def describe_extra(R, assume, assumeExtra):
"""Describe what assumptions are added, given existing assumptions"""
zerox = assume.zero.copy()
zerox.update(assumeExtra.zero)
zero = R.ideal(list(map(numerator, assume.zero)))
zeroextra = R.ideal(list(map(numerator, zerox)))
nonzero = get_nonzero_set(R, assume)
ret = set()
# Iterate over the extra zero expressions
for base in assumeExtra.zero:
if base not in zero:
add = []
for (f, n) in numerator(base).factor():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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():
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
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)
def check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require):
"""Check a set of zero and nonzero requirements, given a set of zero and nonzero assumptions"""
assume = assumeLaw + assumeAssert + assumeBranch
if conflicts(R, assume):
# This formula does not apply
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
return (True, None)
describe = describe_extra(R, assumeLaw + assumeBranch, assumeAssert)
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
if describe != "":
describe = " (assuming " + describe + ")"
ok, msg = prove_zero(R, require.zero, assume)
if not ok:
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
return (False, "FAIL, %s fails%s" % (str(msg), describe))
res, expl = prove_nonzero(R, require.nonzero, assume)
if not res:
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
return (False, "FAIL, %s fails%s" % (str(expl), describe))
Upgrade the vendored libsecp256k1 code `libsecp256k1` v0.2.0 was just released. Update the vendored code using `./vendor-libsecp.sh depend 0_8_0 21ffe4b` ``` git show 21ffe4b commit 21ffe4b22a9683cf24ae0763359e401d1284cc7a (tag: v0.2.0) Merge: 8c949f5 e025ccd Author: Pieter Wuille <pieter@wuille.net> Date: Mon Dec 12 17:00:52 2022 -0500 Merge bitcoin-core/secp256k1#1055: Prepare initial release e025ccdf7473702a76bb13d763dc096548ffefba release: prepare for initial release 0.2.0 (Jonas Nick) 6d1784a2e2c1c5a8d89ffb08a7f76fa15e84fff5 build: add missing files to EXTRA_DIST (Jonas Nick) 13bf1b6b324f2ed1c1fb4c8d17a4febd3556839e changelog: make order of change types match keepachangelog.com (Jonas Nick) b1f992a552785395d2e60b10862626fd11f66f84 doc: improve release process (Jonas Nick) ad39e2dc417f85c1577a6a6a9c519f5c60453def build: change package version to 0.1.0-dev (Jonas Nick) 90618e9263ebc2a0d73d487d6d94fd3af96b973c doc: move CHANGELOG from doc/ to root directory (Jonas Nick) Pull request description: Based on #964 ACKs for top commit: sipa: ACK e025ccdf7473702a76bb13d763dc096548ffefba Tree-SHA512: b9ab71d7362537d383a32b5e321ef44069f00e3e92340375bcd662267bc5a60c2bad60222998e6602cfac24ad65efb23d772eac37c86065036b90ef090b54c49 ``` Requires a new version of `secp256k1-sys`, use v0.8.0 - Update the `secp256k1-sys` manifest (including links field) - Update symbols to use 0_8_0 - Add a changelog entry - depend on the new version in `secp256k1` Which in turn requires a new version of `secp256k1`, use v0.26.0
2022-12-20 21:11:14 +00:00
return (True, "OK%s" % describe)
def concrete_verify(c):
for k in c.zero:
if k != 0:
return (False, c.zero[k])
for k in c.nonzero:
if k == 0:
return (False, c.nonzero[k])
return (True, None)