Inside Bitcoin

1# Test libsecp256k1' group operation implementations using prover.sage
2
3import sys
4
5load("group_prover.sage")
6load("weierstrass_prover.sage")
7
8def 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
27def 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
66def 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
102def 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
146def 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
208def 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