weierstrass_prover.sage raw
1 # Prover implementation for Weierstrass curves of the form
2 # y^2 = x^3 + A * x + B, specifically with a = 0 and b = 7, with group laws
3 # operating on affine and Jacobian coordinates, including the point at infinity
4 # represented by a 4th variable in coordinates.
5
6 load("group_prover.sage")
7
8
9 class affinepoint:
10 def __init__(self, x, y, infinity=0):
11 self.x = x
12 self.y = y
13 self.infinity = infinity
14 def __str__(self):
15 return "affinepoint(x=%s,y=%s,inf=%s)" % (self.x, self.y, self.infinity)
16
17
18 class jacobianpoint:
19 def __init__(self, x, y, z, infinity=0):
20 self.X = x
21 self.Y = y
22 self.Z = z
23 self.Infinity = infinity
24 def __str__(self):
25 return "jacobianpoint(X=%s,Y=%s,Z=%s,inf=%s)" % (self.X, self.Y, self.Z, self.Infinity)
26
27
28 def point_at_infinity():
29 return jacobianpoint(1, 1, 1, 1)
30
31
32 def negate(p):
33 if p.__class__ == affinepoint:
34 return affinepoint(p.x, -p.y)
35 if p.__class__ == jacobianpoint:
36 return jacobianpoint(p.X, -p.Y, p.Z)
37 assert(False)
38
39
40 def on_weierstrass_curve(A, B, p):
41 """Return a set of zero-expressions for an affine point to be on the curve"""
42 return constraints(zero={p.x^3 + A*p.x + B - p.y^2: 'on_curve'})
43
44
45 def tangential_to_weierstrass_curve(A, B, p12, p3):
46 """Return a set of zero-expressions for ((x12,y12),(x3,y3)) to be a line that is tangential to the curve at (x12,y12)"""
47 return constraints(zero={
48 (p12.y - p3.y) * (p12.y * 2) - (p12.x^2 * 3 + A) * (p12.x - p3.x): 'tangential_to_curve'
49 })
50
51
52 def colinear(p1, p2, p3):
53 """Return a set of zero-expressions for ((x1,y1),(x2,y2),(x3,y3)) to be collinear"""
54 return constraints(zero={
55 (p1.y - p2.y) * (p1.x - p3.x) - (p1.y - p3.y) * (p1.x - p2.x): 'colinear_1',
56 (p2.y - p3.y) * (p2.x - p1.x) - (p2.y - p1.y) * (p2.x - p3.x): 'colinear_2',
57 (p3.y - p1.y) * (p3.x - p2.x) - (p3.y - p2.y) * (p3.x - p1.x): 'colinear_3'
58 })
59
60
61 def good_affine_point(p):
62 return constraints(nonzero={p.x : 'nonzero_x', p.y : 'nonzero_y'})
63
64
65 def good_jacobian_point(p):
66 return constraints(nonzero={p.X : 'nonzero_X', p.Y : 'nonzero_Y', p.Z^6 : 'nonzero_Z'})
67
68
69 def good_point(p):
70 return constraints(nonzero={p.Z^6 : 'nonzero_X'})
71
72
73 def finite(p, *affine_fns):
74 con = good_point(p) + constraints(zero={p.Infinity : 'finite_point'})
75 if p.Z != 0:
76 return con + reduce(lambda a, b: a + b, (f(affinepoint(p.X / p.Z^2, p.Y / p.Z^3)) for f in affine_fns), con)
77 else:
78 return con
79
80 def infinite(p):
81 return constraints(nonzero={p.Infinity : 'infinite_point'})
82
83
84 def law_jacobian_weierstrass_add(A, B, pa, pb, pA, pB, pC):
85 """Check whether the passed set of coordinates is a valid Jacobian add, given assumptions"""
86 assumeLaw = (good_affine_point(pa) +
87 good_affine_point(pb) +
88 good_jacobian_point(pA) +
89 good_jacobian_point(pB) +
90 on_weierstrass_curve(A, B, pa) +
91 on_weierstrass_curve(A, B, pb) +
92 finite(pA) +
93 finite(pB) +
94 constraints(nonzero={pa.x - pb.x : 'different_x'}))
95 require = (finite(pC, lambda pc: on_weierstrass_curve(A, B, pc) +
96 colinear(pa, pb, negate(pc))))
97 return (assumeLaw, require)
98
99
100 def law_jacobian_weierstrass_double(A, B, pa, pb, pA, pB, pC):
101 """Check whether the passed set of coordinates is a valid Jacobian doubling, given assumptions"""
102 assumeLaw = (good_affine_point(pa) +
103 good_affine_point(pb) +
104 good_jacobian_point(pA) +
105 good_jacobian_point(pB) +
106 on_weierstrass_curve(A, B, pa) +
107 on_weierstrass_curve(A, B, pb) +
108 finite(pA) +
109 finite(pB) +
110 constraints(zero={pa.x - pb.x : 'equal_x', pa.y - pb.y : 'equal_y'}))
111 require = (finite(pC, lambda pc: on_weierstrass_curve(A, B, pc) +
112 tangential_to_weierstrass_curve(A, B, pa, negate(pc))))
113 return (assumeLaw, require)
114
115
116 def law_jacobian_weierstrass_add_opposites(A, B, pa, pb, pA, pB, pC):
117 assumeLaw = (good_affine_point(pa) +
118 good_affine_point(pb) +
119 good_jacobian_point(pA) +
120 good_jacobian_point(pB) +
121 on_weierstrass_curve(A, B, pa) +
122 on_weierstrass_curve(A, B, pb) +
123 finite(pA) +
124 finite(pB) +
125 constraints(zero={pa.x - pb.x : 'equal_x', pa.y + pb.y : 'opposite_y'}))
126 require = infinite(pC)
127 return (assumeLaw, require)
128
129
130 def law_jacobian_weierstrass_add_infinite_a(A, B, pa, pb, pA, pB, pC):
131 assumeLaw = (good_affine_point(pa) +
132 good_affine_point(pb) +
133 good_jacobian_point(pA) +
134 good_jacobian_point(pB) +
135 on_weierstrass_curve(A, B, pb) +
136 infinite(pA) +
137 finite(pB))
138 require = finite(pC, lambda pc: constraints(zero={pc.x - pb.x : 'c.x=b.x', pc.y - pb.y : 'c.y=b.y'}))
139 return (assumeLaw, require)
140
141
142 def law_jacobian_weierstrass_add_infinite_b(A, B, pa, pb, pA, pB, pC):
143 assumeLaw = (good_affine_point(pa) +
144 good_affine_point(pb) +
145 good_jacobian_point(pA) +
146 good_jacobian_point(pB) +
147 on_weierstrass_curve(A, B, pa) +
148 infinite(pB) +
149 finite(pA))
150 require = finite(pC, lambda pc: constraints(zero={pc.x - pa.x : 'c.x=a.x', pc.y - pa.y : 'c.y=a.y'}))
151 return (assumeLaw, require)
152
153
154 def law_jacobian_weierstrass_add_infinite_ab(A, B, pa, pb, pA, pB, pC):
155 assumeLaw = (good_affine_point(pa) +
156 good_affine_point(pb) +
157 good_jacobian_point(pA) +
158 good_jacobian_point(pB) +
159 infinite(pA) +
160 infinite(pB))
161 require = infinite(pC)
162 return (assumeLaw, require)
163
164
165 laws_jacobian_weierstrass = {
166 'add': law_jacobian_weierstrass_add,
167 'double': law_jacobian_weierstrass_double,
168 'add_opposite': law_jacobian_weierstrass_add_opposites,
169 'add_infinite_a': law_jacobian_weierstrass_add_infinite_a,
170 'add_infinite_b': law_jacobian_weierstrass_add_infinite_b,
171 'add_infinite_ab': law_jacobian_weierstrass_add_infinite_ab
172 }
173
174
175 def check_exhaustive_jacobian_weierstrass(name, A, B, branches, formula, p):
176 """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"""
177 F = Integers(p)
178 print("Formula %s on Z%i:" % (name, p))
179 points = []
180 for x in range(0, p):
181 for y in range(0, p):
182 point = affinepoint(F(x), F(y))
183 r, e = concrete_verify(on_weierstrass_curve(A, B, point))
184 if r:
185 points.append(point)
186
187 ret = True
188 for za in range(1, p):
189 for zb in range(1, p):
190 for pa in points:
191 for pb in points:
192 for ia in range(2):
193 for ib in range(2):
194 pA = jacobianpoint(pa.x * F(za)^2, pa.y * F(za)^3, F(za), ia)
195 pB = jacobianpoint(pb.x * F(zb)^2, pb.y * F(zb)^3, F(zb), ib)
196 for branch in range(0, branches):
197 assumeAssert, assumeBranch, pC = formula(branch, pA, pB)
198 pC.X = F(pC.X)
199 pC.Y = F(pC.Y)
200 pC.Z = F(pC.Z)
201 pC.Infinity = F(pC.Infinity)
202 r, e = concrete_verify(assumeAssert + assumeBranch)
203 if r:
204 match = False
205 for key in laws_jacobian_weierstrass:
206 assumeLaw, require = laws_jacobian_weierstrass[key](A, B, pa, pb, pA, pB, pC)
207 r, e = concrete_verify(assumeLaw)
208 if r:
209 if match:
210 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))
211 else:
212 match = True
213 r, e = concrete_verify(require)
214 if not r:
215 ret = False
216 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))
217
218 print()
219 return ret
220
221
222 def check_symbolic_function(R, assumeAssert, assumeBranch, f, A, B, pa, pb, pA, pB, pC):
223 assumeLaw, require = f(A, B, pa, pb, pA, pB, pC)
224 return check_symbolic(R, assumeLaw, assumeAssert, assumeBranch, require)
225
226 def check_symbolic_jacobian_weierstrass(name, A, B, branches, formula):
227 """Verify an implementation of addition of Jacobian points on a Weierstrass curve symbolically"""
228 R.<ax,bx,ay,by,Az,Bz,Ai,Bi> = PolynomialRing(QQ,8,order='invlex')
229 lift = lambda x: fastfrac(R,x)
230 ax = lift(ax)
231 ay = lift(ay)
232 Az = lift(Az)
233 bx = lift(bx)
234 by = lift(by)
235 Bz = lift(Bz)
236 Ai = lift(Ai)
237 Bi = lift(Bi)
238
239 pa = affinepoint(ax, ay, Ai)
240 pb = affinepoint(bx, by, Bi)
241 pA = jacobianpoint(ax * Az^2, ay * Az^3, Az, Ai)
242 pB = jacobianpoint(bx * Bz^2, by * Bz^3, Bz, Bi)
243
244 res = {}
245
246 for key in laws_jacobian_weierstrass:
247 res[key] = []
248
249 print("Formula " + name + ":")
250 count = 0
251 ret = True
252 for branch in range(branches):
253 assumeFormula, assumeBranch, pC = formula(branch, pA, pB)
254 assumeBranch = assumeBranch.map(lift)
255 assumeFormula = assumeFormula.map(lift)
256 pC.X = lift(pC.X)
257 pC.Y = lift(pC.Y)
258 pC.Z = lift(pC.Z)
259 pC.Infinity = lift(pC.Infinity)
260
261 for key in laws_jacobian_weierstrass:
262 success, msg = check_symbolic_function(R, assumeFormula, assumeBranch, laws_jacobian_weierstrass[key], A, B, pa, pb, pA, pB, pC)
263 if not success:
264 ret = False
265 res[key].append((msg, branch))
266
267 for key in res:
268 print(" %s:" % key)
269 val = res[key]
270 for x in val:
271 if x[0] is not None:
272 print(" branch %i: %s" % (x[1], x[0]))
273
274 print()
275 return ret
276