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 | |||||