Changeset View
Changeset View
Standalone View
Standalone View
src/secp256k1/sage/group_prover.sage
Show First 20 Lines • Show All 59 Lines • ▼ Show 20 Lines | else: | ||||
self.top = R(numerator(top)) | self.top = R(numerator(top)) | ||||
self.bot = R(denominator(top)) * bot | self.bot = R(denominator(top)) * bot | ||||
def iszero(self,I): | def iszero(self,I): | ||||
"""Return whether this fraction is zero given an ideal.""" | """Return whether this fraction is zero given an ideal.""" | ||||
return self.top in I and self.bot not in I | return self.top in I and self.bot not in I | ||||
def reduce(self,assumeZero): | def reduce(self,assumeZero): | ||||
zero = self.R.ideal(map(numerator, assumeZero)) | zero = self.R.ideal(list(map(numerator, assumeZero))) | ||||
return fastfrac(self.R, zero.reduce(self.top)) / fastfrac(self.R, zero.reduce(self.bot)) | return fastfrac(self.R, zero.reduce(self.top)) / fastfrac(self.R, zero.reduce(self.bot)) | ||||
def __add__(self,other): | def __add__(self,other): | ||||
"""Add two fractions.""" | """Add two fractions.""" | ||||
if parent(other) == ZZ: | if parent(other) == ZZ: | ||||
return fastfrac(self.R,self.top + self.bot * other,self.bot) | return fastfrac(self.R,self.top + self.bot * other,self.bot) | ||||
if other.__class__ == fastfrac: | if other.__class__ == fastfrac: | ||||
return fastfrac(self.R,self.top * other.bot + self.bot * other.top,self.bot * other.bot) | return fastfrac(self.R,self.top * other.bot + self.bot * other.top,self.bot * other.bot) | ||||
Show All 18 Lines | def __mul__(self,other): | ||||
if other.__class__ == fastfrac: | if other.__class__ == fastfrac: | ||||
return fastfrac(self.R,self.top * other.top,self.bot * other.bot) | return fastfrac(self.R,self.top * other.top,self.bot * other.bot) | ||||
return NotImplemented | return NotImplemented | ||||
def __rmul__(self,other): | def __rmul__(self,other): | ||||
"""Multiply something else with a fraction.""" | """Multiply something else with a fraction.""" | ||||
return self.__mul__(other) | return self.__mul__(other) | ||||
def __div__(self,other): | def __truediv__(self,other): | ||||
"""Divide two fractions.""" | """Divide two fractions.""" | ||||
if parent(other) == ZZ: | if parent(other) == ZZ: | ||||
return fastfrac(self.R,self.top,self.bot * other) | return fastfrac(self.R,self.top,self.bot * other) | ||||
if other.__class__ == fastfrac: | if other.__class__ == fastfrac: | ||||
return fastfrac(self.R,self.top * other.bot,self.bot * other.top) | return fastfrac(self.R,self.top * other.bot,self.bot * other.top) | ||||
return NotImplemented | 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): | def __pow__(self,other): | ||||
"""Compute a power of a fraction.""" | """Compute a power of a fraction.""" | ||||
if parent(other) == ZZ: | if parent(other) == ZZ: | ||||
if other < 0: | if other < 0: | ||||
# Negative powers require flipping top and bottom | # Negative powers require flipping top and bottom | ||||
return fastfrac(self.R,self.bot ^ (-other),self.top ^ (-other)) | return fastfrac(self.R,self.bot ^ (-other),self.top ^ (-other)) | ||||
else: | else: | ||||
return fastfrac(self.R,self.top ^ other,self.bot ^ other) | return fastfrac(self.R,self.top ^ other,self.bot ^ other) | ||||
▲ Show 20 Lines • Show All 51 Lines • ▼ Show 20 Lines | def __str__(self): | ||||
return "constraints(zero=%s,nonzero=%s)" % (self.zero, self.nonzero) | return "constraints(zero=%s,nonzero=%s)" % (self.zero, self.nonzero) | ||||
def __repr__(self): | def __repr__(self): | ||||
return "%s" % self | return "%s" % self | ||||
def conflicts(R, con): | def conflicts(R, con): | ||||
"""Check whether any of the passed non-zero assumptions is implied by the zero assumptions""" | """Check whether any of the passed non-zero assumptions is implied by the zero assumptions""" | ||||
zero = R.ideal(map(numerator, con.zero)) | zero = R.ideal(list(map(numerator, con.zero))) | ||||
if 1 in zero: | if 1 in zero: | ||||
return True | return True | ||||
# First a cheap check whether any of the individual nonzero terms conflict on | # First a cheap check whether any of the individual nonzero terms conflict on | ||||
# their own. | # their own. | ||||
for nonzero in con.nonzero: | for nonzero in con.nonzero: | ||||
if nonzero.iszero(zero): | if nonzero.iszero(zero): | ||||
return True | return True | ||||
# It can be the case that entries in the nonzero set do not individually | # 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 | # 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. | # 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 | # 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. | # 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): | if reduce(lambda a,b: a * b, con.nonzero, fastfrac(R, 1)).iszero(zero): | ||||
return True | return True | ||||
return False | return False | ||||
def get_nonzero_set(R, assume): | def get_nonzero_set(R, assume): | ||||
"""Calculate a simple set of nonzero expressions""" | """Calculate a simple set of nonzero expressions""" | ||||
zero = R.ideal(map(numerator, assume.zero)) | zero = R.ideal(list(map(numerator, assume.zero))) | ||||
nonzero = set() | nonzero = set() | ||||
for nz in map(numerator, assume.nonzero): | for nz in map(numerator, assume.nonzero): | ||||
for (f,n) in nz.factor(): | for (f,n) in nz.factor(): | ||||
nonzero.add(f) | nonzero.add(f) | ||||
rnz = zero.reduce(nz) | rnz = zero.reduce(nz) | ||||
for (f,n) in rnz.factor(): | for (f,n) in rnz.factor(): | ||||
nonzero.add(f) | nonzero.add(f) | ||||
return nonzero | return nonzero | ||||
def prove_nonzero(R, exprs, assume): | def prove_nonzero(R, exprs, assume): | ||||
"""Check whether an expression is provably nonzero, given assumptions""" | """Check whether an expression is provably nonzero, given assumptions""" | ||||
zero = R.ideal(map(numerator, assume.zero)) | zero = R.ideal(list(map(numerator, assume.zero))) | ||||
nonzero = get_nonzero_set(R, assume) | nonzero = get_nonzero_set(R, assume) | ||||
expl = set() | expl = set() | ||||
ok = True | ok = True | ||||
for expr in exprs: | for expr in exprs: | ||||
if numerator(expr) in zero: | if numerator(expr) in zero: | ||||
return (False, [exprs[expr]]) | return (False, [exprs[expr]]) | ||||
allexprs = reduce(lambda a,b: numerator(a)*numerator(b), exprs, 1) | allexprs = reduce(lambda a,b: numerator(a)*numerator(b), exprs, 1) | ||||
for (f, n) in allexprs.factor(): | for (f, n) in allexprs.factor(): | ||||
Show All 25 Lines | else: | ||||
return (True, None) | return (True, None) | ||||
def prove_zero(R, exprs, assume): | def prove_zero(R, exprs, assume): | ||||
"""Check whether all of the passed expressions are provably zero, given assumptions""" | """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) | r, e = prove_nonzero(R, dict(map(lambda x: (fastfrac(R, x.bot, 1), exprs[x]), exprs)), assume) | ||||
if not r: | if not r: | ||||
return (False, map(lambda x: "Possibly zero denominator: %s" % x, e)) | return (False, map(lambda x: "Possibly zero denominator: %s" % x, e)) | ||||
zero = R.ideal(map(numerator, assume.zero)) | zero = R.ideal(list(map(numerator, assume.zero))) | ||||
nonzero = prod(x for x in assume.nonzero) | nonzero = prod(x for x in assume.nonzero) | ||||
expl = [] | expl = [] | ||||
for expr in exprs: | for expr in exprs: | ||||
if not expr.iszero(zero): | if not expr.iszero(zero): | ||||
expl.append(exprs[expr]) | expl.append(exprs[expr]) | ||||
if not expl: | if not expl: | ||||
return (True, None) | return (True, None) | ||||
return (False, expl) | return (False, expl) | ||||
def describe_extra(R, assume, assumeExtra): | def describe_extra(R, assume, assumeExtra): | ||||
"""Describe what assumptions are added, given existing assumptions""" | """Describe what assumptions are added, given existing assumptions""" | ||||
zerox = assume.zero.copy() | zerox = assume.zero.copy() | ||||
zerox.update(assumeExtra.zero) | zerox.update(assumeExtra.zero) | ||||
zero = R.ideal(map(numerator, assume.zero)) | zero = R.ideal(list(map(numerator, assume.zero))) | ||||
zeroextra = R.ideal(map(numerator, zerox)) | zeroextra = R.ideal(list(map(numerator, zerox))) | ||||
nonzero = get_nonzero_set(R, assume) | nonzero = get_nonzero_set(R, assume) | ||||
ret = set() | ret = set() | ||||
# Iterate over the extra zero expressions | # Iterate over the extra zero expressions | ||||
for base in assumeExtra.zero: | for base in assumeExtra.zero: | ||||
if base not in zero: | if base not in zero: | ||||
add = [] | add = [] | ||||
for (f, n) in numerator(base).factor(): | for (f, n) in numerator(base).factor(): | ||||
if f not in nonzero: | if f not in nonzero: | ||||
▲ Show 20 Lines • Show All 45 Lines • Show Last 20 Lines |