sage/prove_group_implementations.sage

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