weierstrass_prover.sage (9796B)
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