prove_group_implementations.sage (9197B)
1 # Test libsecp256k1' group operation implementations using prover.sage 2 3 import sys 4 5 load("group_prover.sage") 6 load("weierstrass_prover.sage") 7 8 def formula_haskellsecp256k1_v0_1_0_gej_double_var(a): 9 """libsecp256k1's haskellsecp256k1_v0_1_0_gej_double_var, used by various addition functions""" 10 rz = a.Z * a.Y 11 s = a.Y^2 12 l = a.X^2 13 l = l * 3 14 l = l / 2 15 t = -s 16 t = t * a.X 17 rx = l^2 18 rx = rx + t 19 rx = rx + t 20 s = s^2 21 t = t + rx 22 ry = t * l 23 ry = ry + s 24 ry = -ry 25 return jacobianpoint(rx, ry, rz) 26 27 def formula_haskellsecp256k1_v0_1_0_gej_add_var(branch, a, b): 28 """libsecp256k1's haskellsecp256k1_v0_1_0_gej_add_var""" 29 if branch == 0: 30 return (constraints(), constraints(nonzero={a.Infinity : 'a_infinite'}), b) 31 if branch == 1: 32 return (constraints(), constraints(zero={a.Infinity : 'a_finite'}, nonzero={b.Infinity : 'b_infinite'}), a) 33 z22 = b.Z^2 34 z12 = a.Z^2 35 u1 = a.X * z22 36 u2 = b.X * z12 37 s1 = a.Y * z22 38 s1 = s1 * b.Z 39 s2 = b.Y * z12 40 s2 = s2 * a.Z 41 h = -u1 42 h = h + u2 43 i = -s2 44 i = i + s1 45 if branch == 2: 46 r = formula_haskellsecp256k1_v0_1_0_gej_double_var(a) 47 return (constraints(), constraints(zero={h : 'h=0', i : 'i=0', a.Infinity : 'a_finite', b.Infinity : 'b_finite'}), r) 48 if branch == 3: 49 return (constraints(), constraints(zero={h : 'h=0', a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={i : 'i!=0'}), point_at_infinity()) 50 t = h * b.Z 51 rz = a.Z * t 52 h2 = h^2 53 h2 = -h2 54 h3 = h2 * h 55 t = u1 * h2 56 rx = i^2 57 rx = rx + h3 58 rx = rx + t 59 rx = rx + t 60 t = t + rx 61 ry = t * i 62 h3 = h3 * s1 63 ry = ry + h3 64 return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz)) 65 66 def formula_haskellsecp256k1_v0_1_0_gej_add_ge_var(branch, a, b): 67 """libsecp256k1's haskellsecp256k1_v0_1_0_gej_add_ge_var, which assume bz==1""" 68 if branch == 0: 69 return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(nonzero={a.Infinity : 'a_infinite'}), b) 70 if branch == 1: 71 return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite'}, nonzero={b.Infinity : 'b_infinite'}), a) 72 z12 = a.Z^2 73 u1 = a.X 74 u2 = b.X * z12 75 s1 = a.Y 76 s2 = b.Y * z12 77 s2 = s2 * a.Z 78 h = -u1 79 h = h + u2 80 i = -s2 81 i = i + s1 82 if (branch == 2): 83 r = formula_haskellsecp256k1_v0_1_0_gej_double_var(a) 84 return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0', i : 'i=0'}), r) 85 if (branch == 3): 86 return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0'}, nonzero={i : 'i!=0'}), point_at_infinity()) 87 rz = a.Z * h 88 h2 = h^2 89 h2 = -h2 90 h3 = h2 * h 91 t = u1 * h2 92 rx = i^2 93 rx = rx + h3 94 rx = rx + t 95 rx = rx + t 96 t = t + rx 97 ry = t * i 98 h3 = h3 * s1 99 ry = ry + h3 100 return (constraints(zero={b.Z - 1 : 'b.z=1'}), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz)) 101 102 def formula_haskellsecp256k1_v0_1_0_gej_add_zinv_var(branch, a, b): 103 """libsecp256k1's haskellsecp256k1_v0_1_0_gej_add_zinv_var""" 104 bzinv = b.Z^(-1) 105 if branch == 0: 106 rinf = b.Infinity 107 bzinv2 = bzinv^2 108 bzinv3 = bzinv2 * bzinv 109 rx = b.X * bzinv2 110 ry = b.Y * bzinv3 111 rz = 1 112 return (constraints(), constraints(nonzero={a.Infinity : 'a_infinite'}), jacobianpoint(rx, ry, rz, rinf)) 113 if branch == 1: 114 return (constraints(), constraints(zero={a.Infinity : 'a_finite'}, nonzero={b.Infinity : 'b_infinite'}), a) 115 azz = a.Z * bzinv 116 z12 = azz^2 117 u1 = a.X 118 u2 = b.X * z12 119 s1 = a.Y 120 s2 = b.Y * z12 121 s2 = s2 * azz 122 h = -u1 123 h = h + u2 124 i = -s2 125 i = i + s1 126 if branch == 2: 127 r = formula_haskellsecp256k1_v0_1_0_gej_double_var(a) 128 return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0', i : 'i=0'}), r) 129 if branch == 3: 130 return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite', h : 'h=0'}, nonzero={i : 'i!=0'}), point_at_infinity()) 131 rz = a.Z * h 132 h2 = h^2 133 h2 = -h2 134 h3 = h2 * h 135 t = u1 * h2 136 rx = i^2 137 rx = rx + h3 138 rx = rx + t 139 rx = rx + t 140 t = t + rx 141 ry = t * i 142 h3 = h3 * s1 143 ry = ry + h3 144 return (constraints(), constraints(zero={a.Infinity : 'a_finite', b.Infinity : 'b_finite'}, nonzero={h : 'h!=0'}), jacobianpoint(rx, ry, rz)) 145 146 def formula_haskellsecp256k1_v0_1_0_gej_add_ge(branch, a, b): 147 """libsecp256k1's haskellsecp256k1_v0_1_0_gej_add_ge""" 148 zeroes = {} 149 nonzeroes = {} 150 a_infinity = False 151 if (branch & 2) != 0: 152 nonzeroes.update({a.Infinity : 'a_infinite'}) 153 a_infinity = True 154 else: 155 zeroes.update({a.Infinity : 'a_finite'}) 156 zz = a.Z^2 157 u1 = a.X 158 u2 = b.X * zz 159 s1 = a.Y 160 s2 = b.Y * zz 161 s2 = s2 * a.Z 162 t = u1 163 t = t + u2 164 m = s1 165 m = m + s2 166 rr = t^2 167 m_alt = -u2 168 tt = u1 * m_alt 169 rr = rr + tt 170 degenerate = (branch & 1) != 0 171 if degenerate: 172 zeroes.update({m : 'm_zero'}) 173 else: 174 nonzeroes.update({m : 'm_nonzero'}) 175 rr_alt = s1 176 rr_alt = rr_alt * 2 177 m_alt = m_alt + u1 178 if not degenerate: 179 rr_alt = rr 180 m_alt = m 181 n = m_alt^2 182 q = -t 183 q = q * n 184 n = n^2 185 if degenerate: 186 n = m 187 t = rr_alt^2 188 rz = a.Z * m_alt 189 t = t + q 190 rx = t 191 t = t * 2 192 t = t + q 193 t = t * rr_alt 194 t = t + n 195 ry = -t 196 ry = ry / 2 197 if a_infinity: 198 rx = b.X 199 ry = b.Y 200 rz = 1 201 if (branch & 4) != 0: 202 zeroes.update({rz : 'r.z = 0'}) 203 return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zeroes, nonzero=nonzeroes), point_at_infinity()) 204 else: 205 nonzeroes.update({rz : 'r.z != 0'}) 206 return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zeroes, nonzero=nonzeroes), jacobianpoint(rx, ry, rz)) 207 208 def formula_haskellsecp256k1_v0_1_0_gej_add_ge_old(branch, a, b): 209 """libsecp256k1's old haskellsecp256k1_v0_1_0_gej_add_ge, which fails when ay+by=0 but ax!=bx""" 210 a_infinity = (branch & 1) != 0 211 zero = {} 212 nonzero = {} 213 if a_infinity: 214 nonzero.update({a.Infinity : 'a_infinite'}) 215 else: 216 zero.update({a.Infinity : 'a_finite'}) 217 zz = a.Z^2 218 u1 = a.X 219 u2 = b.X * zz 220 s1 = a.Y 221 s2 = b.Y * zz 222 s2 = s2 * a.Z 223 z = a.Z 224 t = u1 225 t = t + u2 226 m = s1 227 m = m + s2 228 n = m^2 229 q = n * t 230 n = n^2 231 rr = t^2 232 t = u1 * u2 233 t = -t 234 rr = rr + t 235 t = rr^2 236 rz = m * z 237 infinity = False 238 if (branch & 2) != 0: 239 if not a_infinity: 240 infinity = True 241 else: 242 return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(nonzero={z : 'conflict_a'}, zero={z : 'conflict_b'}), point_at_infinity()) 243 zero.update({rz : 'r.z=0'}) 244 else: 245 nonzero.update({rz : 'r.z!=0'}) 246 rz = rz * (0 if a_infinity else 2) 247 rx = t 248 q = -q 249 rx = rx + q 250 q = q * 3 251 t = t * 2 252 t = t + q 253 t = t * rr 254 t = t + n 255 ry = -t 256 rx = rx * (0 if a_infinity else 4) 257 ry = ry * (0 if a_infinity else 4) 258 t = b.X 259 t = t * (1 if a_infinity else 0) 260 rx = rx + t 261 t = b.Y 262 t = t * (1 if a_infinity else 0) 263 ry = ry + t 264 t = (1 if a_infinity else 0) 265 rz = rz + t 266 if infinity: 267 return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), point_at_infinity()) 268 return (constraints(zero={b.Z - 1 : 'b.z=1', b.Infinity : 'b_finite'}), constraints(zero=zero, nonzero=nonzero), jacobianpoint(rx, ry, rz)) 269 270 if __name__ == "__main__": 271 success = True 272 success = success & check_symbolic_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_var) 273 success = success & check_symbolic_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_ge_var) 274 success = success & check_symbolic_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_zinv_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_zinv_var) 275 success = success & check_symbolic_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge", 0, 7, 8, formula_haskellsecp256k1_v0_1_0_gej_add_ge) 276 success = success & (not check_symbolic_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge_old [should fail]", 0, 7, 4, formula_haskellsecp256k1_v0_1_0_gej_add_ge_old)) 277 278 if len(sys.argv) >= 2 and sys.argv[1] == "--exhaustive": 279 success = success & check_exhaustive_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_var, 43) 280 success = success & check_exhaustive_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_ge_var, 43) 281 success = success & check_exhaustive_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_zinv_var", 0, 7, 5, formula_haskellsecp256k1_v0_1_0_gej_add_zinv_var, 43) 282 success = success & check_exhaustive_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge", 0, 7, 8, formula_haskellsecp256k1_v0_1_0_gej_add_ge, 43) 283 success = success & (not check_exhaustive_jacobian_weierstrass("haskellsecp256k1_v0_1_0_gej_add_ge_old [should fail]", 0, 7, 4, formula_haskellsecp256k1_v0_1_0_gej_add_ge_old, 43)) 284 285 sys.exit(int(not success))