prove_group_implementations.sage raw

   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    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_secp256k1_gej_add_var(branch, a, b):
  28    """libsecp256k1's secp256k1_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_secp256k1_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_secp256k1_gej_add_ge_var(branch, a, b):
  67    """libsecp256k1's secp256k1_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_secp256k1_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_secp256k1_gej_add_zinv_var(branch, a, b):
 103    """libsecp256k1's secp256k1_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_secp256k1_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_secp256k1_gej_add_ge(branch, a, b):
 147    """libsecp256k1's secp256k1_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_secp256k1_gej_add_ge_old(branch, a, b):
 209    """libsecp256k1's old secp256k1_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("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var)
 273    success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var)
 274    success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var)
 275    success = success & check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 8, formula_secp256k1_gej_add_ge)
 276    success = success & (not check_symbolic_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old))
 277  
 278    if len(sys.argv) >= 2 and sys.argv[1] == "--exhaustive":
 279      success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_var", 0, 7, 5, formula_secp256k1_gej_add_var, 43)
 280      success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge_var", 0, 7, 5, formula_secp256k1_gej_add_ge_var, 43)
 281      success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_zinv_var", 0, 7, 5, formula_secp256k1_gej_add_zinv_var, 43)
 282      success = success & check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge", 0, 7, 8, formula_secp256k1_gej_add_ge, 43)
 283      success = success & (not check_exhaustive_jacobian_weierstrass("secp256k1_gej_add_ge_old [should fail]", 0, 7, 4, formula_secp256k1_gej_add_ge_old, 43))
 284  
 285    sys.exit(int(not success))
 286