Differential D9374 Diff 28087 src/secp256k1/sage/weierstrass_prover.sage

Changeset View

Standalone View

src/secp256k1/sage/weierstrass_prover.sage

Show First 20 Lines • Show All 169 Lines • ▼ Show 20 Lines	laws_jacobian_weierstrass = {
'add_infinite_b': law_jacobian_weierstrass_add_infinite_b,		'add_infinite_b': law_jacobian_weierstrass_add_infinite_b,
'add_infinite_ab': law_jacobian_weierstrass_add_infinite_ab		'add_infinite_ab': law_jacobian_weierstrass_add_infinite_ab
}		}


def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):		def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):
"""Verify an implementation of addition of Jacobian points on a Weierstrass curve, by executing and validating the result for every possible addition in a prime field"""		"""Verify an implementation of addition of Jacobian points on a Weierstrass curve, by executing and validating the result for every possible addition in a prime field"""
F = Integers(p)		F = Integers(p)
print "Formula %s on Z%i:" % (name, p)		print("Formula %s on Z%i:" % (name, p))
points = []		points = []
for x in xrange(0, p):		for x in range(0, p):
for y in xrange(0, p):		for y in range(0, p):
point = affinepoint(F(x), F(y))		point = affinepoint(F(x), F(y))
r, e = concrete_verify(on_weierstrass_curve(A, B, point))		r, e = concrete_verify(on_weierstrass_curve(A, B, point))
if r:		if r:
points.append(point)		points.append(point)

for za in xrange(1, p):		for za in range(1, p):
for zb in xrange(1, p):		for zb in range(1, p):
for pa in points:		for pa in points:
for pb in points:		for pb in points:
for ia in xrange(2):		for ia in range(2):
for ib in xrange(2):		for ib in range(2):
pA = jacobianpoint(pa.x * F(za)^2, pa.y * F(za)^3, F(za), ia)		pA = jacobianpoint(pa.x * F(za)^2, pa.y * F(za)^3, F(za), ia)
pB = jacobianpoint(pb.x * F(zb)^2, pb.y * F(zb)^3, F(zb), ib)		pB = jacobianpoint(pb.x * F(zb)^2, pb.y * F(zb)^3, F(zb), ib)
for branch in xrange(0, branches):		for branch in range(0, branches):
assumeAssert, assumeBranch, pC = formula(branch, pA, pB)		assumeAssert, assumeBranch, pC = formula(branch, pA, pB)
pC.X = F(pC.X)		pC.X = F(pC.X)
pC.Y = F(pC.Y)		pC.Y = F(pC.Y)
pC.Z = F(pC.Z)		pC.Z = F(pC.Z)
pC.Infinity = F(pC.Infinity)		pC.Infinity = F(pC.Infinity)
r, e = concrete_verify(assumeAssert + assumeBranch)		r, e = concrete_verify(assumeAssert + assumeBranch)
if r:		if r:
match = False		match = False
for key in laws_jacobian_weierstrass:		for key in laws_jacobian_weierstrass:
assumeLaw, require = laws_jacobian_weierstrass[key](A, B, pa, pb, pA, pB, pC)		assumeLaw, require = laws_jacobian_weierstrass[key](A, B, pa, pb, pA, pB, pC)
r, e = concrete_verify(assumeLaw)		r, e = concrete_verify(assumeLaw)
if r:		if r:
if match:		if match:
print " multiple branches for (%s,%s,%s,%s) + (%s,%s,%s,%s)" % (pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity)		print(" multiple branches for (%s,%s,%s,%s) + (%s,%s,%s,%s)" % (pA.X, pA.Y, pA.Z, pA.Infinity, pB.X, pB.Y, pB.Z, pB.Infinity))
else:		else:
match = True		match = True
r, e = concrete_verify(require)		r, e = concrete_verify(require)
if not r:		if not r:
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(" 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		print()


def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC):		def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC):
assumeLaw, require = f(A, B, pa, pb, pA, pB, pC)		assumeLaw, require = f(A, B, pa, pb, pA, pB, pC)
return check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require)		return check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require)

def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):		def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
"""Verify an implementation of addition of Jacobian points on a Weierstrass curve symbolically"""		"""Verify an implementation of addition of Jacobian points on a Weierstrass curve symbolically"""
Show All 13 Lines	def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
pA = jacobianpoint(ax * Az^2, ay * Az^3, Az, Ai)		pA = jacobianpoint(ax * Az^2, ay * Az^3, Az, Ai)
pB = jacobianpoint(bx * Bz^2, by * Bz^3, Bz, Bi)		pB = jacobianpoint(bx * Bz^2, by * Bz^3, Bz, Bi)

res = {}		res = {}

for key in laws_jacobian_weierstrass:		for key in laws_jacobian_weierstrass:
res[key] = []		res[key] = []

print ("Formula " + name + ":")		print("Formula " + name + ":")
count = 0		count = 0
for branch in xrange(branches):		for branch in range(branches):
assumeFormula, assumeBranch, pC = formula(branch, pA, pB)		assumeFormula, assumeBranch, pC = formula(branch, pA, pB)
pC.X = lift(pC.X)		pC.X = lift(pC.X)
pC.Y = lift(pC.Y)		pC.Y = lift(pC.Y)
pC.Z = lift(pC.Z)		pC.Z = lift(pC.Z)
pC.Infinity = lift(pC.Infinity)		pC.Infinity = lift(pC.Infinity)

for key in laws_jacobian_weierstrass:		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))		res[key].append((check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC), branch))

for key in res:		for key in res:
print " %s:" % key		print(" %s:" % key)
val = res[key]		val = res[key]
for x in val:		for x in val:
if x[0] is not None:		if x[0] is not None:
print " branch %i: %s" % (x[1], x[0])		print(" branch %i: %s" % (x[1], x[0]))

print		print()