TLA Line data Source code
1 : // evmone: Fast Ethereum Virtual Machine implementation
2 : // Copyright 2023 The evmone Authors.
3 : // SPDX-License-Identifier: Apache-2.0
4 :
5 : #include "bn254.hpp"
6 :
7 : namespace evmmax::bn254
8 : {
9 :
10 : namespace
11 : {
12 : const ModArith<uint256> Fp{FieldPrime};
13 : const auto B = Fp.to_mont(3);
14 : const auto B3 = Fp.to_mont(3 * 3);
15 : } // namespace
16 :
17 UBC 0 : bool validate(const Point& pt) noexcept
18 : {
19 0 : if (pt.is_inf())
20 0 : return true;
21 :
22 0 : const auto xm = Fp.to_mont(pt.x);
23 0 : const auto ym = Fp.to_mont(pt.y);
24 0 : const auto y2 = Fp.mul(ym, ym);
25 0 : const auto x2 = Fp.mul(xm, xm);
26 0 : const auto x3 = Fp.mul(x2, xm);
27 0 : const auto x3_3 = Fp.add(x3, B);
28 0 : return y2 == x3_3;
29 : }
30 :
31 0 : Point add(const Point& pt1, const Point& pt2) noexcept
32 : {
33 0 : if (pt1.is_inf())
34 0 : return pt2;
35 0 : if (pt2.is_inf())
36 0 : return pt1;
37 :
38 : // b3 == 9 for y^2 == x^3 + 3
39 0 : const auto r = ecc::add(Fp, ecc::to_proj(Fp, pt1), ecc::to_proj(Fp, pt2), B3);
40 :
41 0 : return ecc::to_affine(Fp, field_inv, r);
42 : }
43 :
44 0 : Point mul(const Point& pt, const uint256& c) noexcept
45 : {
46 0 : if (pt.is_inf())
47 0 : return pt;
48 :
49 0 : if (c == 0)
50 0 : return {};
51 :
52 0 : const auto pr = ecc::mul(Fp, ecc::to_proj(Fp, pt), c, B3);
53 :
54 0 : return ecc::to_affine(Fp, field_inv, pr);
55 : }
56 :
57 0 : uint256 field_inv(const ModArith<uint256>& m, const uint256& x) noexcept
58 : {
59 : // Computes modular exponentiation
60 : // x^0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd45
61 : // Operations: 247 squares 56 multiplies
62 : // Generated by github.com/mmcloughlin/addchain v0.4.0.
63 : // addchain search 0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd45
64 : // > bn254_field_inv.acc
65 : // addchain gen -tmpl expmod.tmpl bn254_field_inv.acc
66 : // > bn254_field_inv.cpp
67 : //
68 : // Inversion computation is derived from the addition chain:
69 : //
70 : // _10 = 2*1
71 : // _11 = 1 + _10
72 : // _101 = _10 + _11
73 : // _110 = 1 + _101
74 : // _1000 = _10 + _110
75 : // _1101 = _101 + _1000
76 : // _10010 = _101 + _1101
77 : // _10011 = 1 + _10010
78 : // _10100 = 1 + _10011
79 : // _10111 = _11 + _10100
80 : // _11100 = _101 + _10111
81 : // _100000 = _1101 + _10011
82 : // _100011 = _11 + _100000
83 : // _101011 = _1000 + _100011
84 : // _101111 = _10011 + _11100
85 : // _1000001 = _10010 + _101111
86 : // _1010011 = _10010 + _1000001
87 : // _1011011 = _1000 + _1010011
88 : // _1100001 = _110 + _1011011
89 : // _1110101 = _10100 + _1100001
90 : // _10010001 = _11100 + _1110101
91 : // _10010101 = _100000 + _1110101
92 : // _10110101 = _100000 + _10010101
93 : // _10111011 = _110 + _10110101
94 : // _11000001 = _110 + _10111011
95 : // _11000011 = _10 + _11000001
96 : // _11010011 = _10010 + _11000001
97 : // _11100001 = _100000 + _11000001
98 : // _11100011 = _10 + _11100001
99 : // _11100111 = _110 + _11100001
100 : // i57 = ((_11000001 << 8 + _10010001) << 10 + _11100111) << 7
101 : // i76 = ((_10111 + i57) << 9 + _10011) << 7 + _1101
102 : // i109 = ((i76 << 14 + _1010011) << 9 + _11100001) << 8
103 : // i127 = ((_1000001 + i109) << 10 + _1011011) << 5 + _1101
104 : // i161 = ((i127 << 8 + _11) << 12 + _101011) << 12
105 : // i186 = ((_10111011 + i161) << 8 + _101111) << 14 + _10110101
106 : // i214 = ((i186 << 9 + _10010001) << 5 + _1101) << 12
107 : // i236 = ((_11100011 + i214) << 8 + _10010101) << 11 + _11010011
108 : // i268 = ((i236 << 7 + _1100001) << 11 + _100011) << 12
109 : // i288 = ((_1011011 + i268) << 9 + _11000011) << 8 + _11100111
110 : // return (i288 << 7 + _1110101) << 6 + _101
111 : //
112 : // Operations: 247 squares 56 m.multiplies
113 : //
114 : // Generated by github.com/mmcloughlin/addchain v0.4.0.
115 :
116 : // Allocate Temporaries.
117 0 : uint256 t0;
118 0 : uint256 t1;
119 0 : uint256 t2;
120 0 : uint256 t3;
121 0 : uint256 t4;
122 0 : uint256 t5;
123 0 : uint256 t6;
124 0 : uint256 t7;
125 0 : uint256 t8;
126 0 : uint256 t9;
127 0 : uint256 t10;
128 0 : uint256 t11;
129 0 : uint256 t12;
130 0 : uint256 t13;
131 0 : uint256 t14;
132 0 : uint256 t15;
133 0 : uint256 t16;
134 0 : uint256 t17;
135 0 : uint256 t18;
136 0 : uint256 t19;
137 0 : uint256 t20;
138 0 : uint256 t21;
139 : // Step 1: t8 = x^0x2
140 0 : t8 = m.mul(x, x);
141 :
142 : // Step 2: t15 = x^0x3
143 0 : t15 = m.mul(x, t8);
144 :
145 : // Step 3: z = x^0x5
146 0 : auto z = m.mul(t8, t15);
147 :
148 : // Step 4: t1 = x^0x6
149 0 : t1 = m.mul(x, z);
150 :
151 : // Step 5: t3 = x^0x8
152 0 : t3 = m.mul(t8, t1);
153 :
154 : // Step 6: t9 = x^0xd
155 0 : t9 = m.mul(z, t3);
156 :
157 : // Step 7: t6 = x^0x12
158 0 : t6 = m.mul(z, t9);
159 :
160 : // Step 8: t19 = x^0x13
161 0 : t19 = m.mul(x, t6);
162 :
163 : // Step 9: t0 = x^0x14
164 0 : t0 = m.mul(x, t19);
165 :
166 : // Step 10: t20 = x^0x17
167 0 : t20 = m.mul(t15, t0);
168 :
169 : // Step 11: t2 = x^0x1c
170 0 : t2 = m.mul(z, t20);
171 :
172 : // Step 12: t17 = x^0x20
173 0 : t17 = m.mul(t9, t19);
174 :
175 : // Step 13: t4 = x^0x23
176 0 : t4 = m.mul(t15, t17);
177 :
178 : // Step 14: t14 = x^0x2b
179 0 : t14 = m.mul(t3, t4);
180 :
181 : // Step 15: t12 = x^0x2f
182 0 : t12 = m.mul(t19, t2);
183 :
184 : // Step 16: t16 = x^0x41
185 0 : t16 = m.mul(t6, t12);
186 :
187 : // Step 17: t18 = x^0x53
188 0 : t18 = m.mul(t6, t16);
189 :
190 : // Step 18: t3 = x^0x5b
191 0 : t3 = m.mul(t3, t18);
192 :
193 : // Step 19: t5 = x^0x61
194 0 : t5 = m.mul(t1, t3);
195 :
196 : // Step 20: t0 = x^0x75
197 0 : t0 = m.mul(t0, t5);
198 :
199 : // Step 21: t10 = x^0x91
200 0 : t10 = m.mul(t2, t0);
201 :
202 : // Step 22: t7 = x^0x95
203 0 : t7 = m.mul(t17, t0);
204 :
205 : // Step 23: t11 = x^0xb5
206 0 : t11 = m.mul(t17, t7);
207 :
208 : // Step 24: t13 = x^0xbb
209 0 : t13 = m.mul(t1, t11);
210 :
211 : // Step 25: t21 = x^0xc1
212 0 : t21 = m.mul(t1, t13);
213 :
214 : // Step 26: t2 = x^0xc3
215 0 : t2 = m.mul(t8, t21);
216 :
217 : // Step 27: t6 = x^0xd3
218 0 : t6 = m.mul(t6, t21);
219 :
220 : // Step 28: t17 = x^0xe1
221 0 : t17 = m.mul(t17, t21);
222 :
223 : // Step 29: t8 = x^0xe3
224 0 : t8 = m.mul(t8, t17);
225 :
226 : // Step 30: t1 = x^0xe7
227 0 : t1 = m.mul(t1, t17);
228 :
229 : // Step 38: t21 = x^0xc100
230 0 : for (int i = 0; i < 8; ++i)
231 0 : t21 = m.mul(t21, t21);
232 :
233 : // Step 39: t21 = x^0xc191
234 0 : t21 = m.mul(t10, t21);
235 :
236 : // Step 49: t21 = x^0x3064400
237 0 : for (int i = 0; i < 10; ++i)
238 0 : t21 = m.mul(t21, t21);
239 :
240 : // Step 50: t21 = x^0x30644e7
241 0 : t21 = m.mul(t1, t21);
242 :
243 : // Step 57: t21 = x^0x183227380
244 0 : for (int i = 0; i < 7; ++i)
245 0 : t21 = m.mul(t21, t21);
246 :
247 : // Step 58: t20 = x^0x183227397
248 0 : t20 = m.mul(t20, t21);
249 :
250 : // Step 67: t20 = x^0x30644e72e00
251 0 : for (int i = 0; i < 9; ++i)
252 0 : t20 = m.mul(t20, t20);
253 :
254 : // Step 68: t19 = x^0x30644e72e13
255 0 : t19 = m.mul(t19, t20);
256 :
257 : // Step 75: t19 = x^0x1832273970980
258 0 : for (int i = 0; i < 7; ++i)
259 0 : t19 = m.mul(t19, t19);
260 :
261 : // Step 76: t19 = x^0x183227397098d
262 0 : t19 = m.mul(t9, t19);
263 :
264 : // Step 90: t19 = x^0x60c89ce5c2634000
265 0 : for (int i = 0; i < 14; ++i)
266 0 : t19 = m.mul(t19, t19);
267 :
268 : // Step 91: t18 = x^0x60c89ce5c2634053
269 0 : t18 = m.mul(t18, t19);
270 :
271 : // Step 100: t18 = x^0xc19139cb84c680a600
272 0 : for (int i = 0; i < 9; ++i)
273 0 : t18 = m.mul(t18, t18);
274 :
275 : // Step 101: t17 = x^0xc19139cb84c680a6e1
276 0 : t17 = m.mul(t17, t18);
277 :
278 : // Step 109: t17 = x^0xc19139cb84c680a6e100
279 0 : for (int i = 0; i < 8; ++i)
280 0 : t17 = m.mul(t17, t17);
281 :
282 : // Step 110: t16 = x^0xc19139cb84c680a6e141
283 0 : t16 = m.mul(t16, t17);
284 :
285 : // Step 120: t16 = x^0x30644e72e131a029b850400
286 0 : for (int i = 0; i < 10; ++i)
287 0 : t16 = m.mul(t16, t16);
288 :
289 : // Step 121: t16 = x^0x30644e72e131a029b85045b
290 0 : t16 = m.mul(t3, t16);
291 :
292 : // Step 126: t16 = x^0x60c89ce5c263405370a08b60
293 0 : for (int i = 0; i < 5; ++i)
294 0 : t16 = m.mul(t16, t16);
295 :
296 : // Step 127: t16 = x^0x60c89ce5c263405370a08b6d
297 0 : t16 = m.mul(t9, t16);
298 :
299 : // Step 135: t16 = x^0x60c89ce5c263405370a08b6d00
300 0 : for (int i = 0; i < 8; ++i)
301 0 : t16 = m.mul(t16, t16);
302 :
303 : // Step 136: t15 = x^0x60c89ce5c263405370a08b6d03
304 0 : t15 = m.mul(t15, t16);
305 :
306 : // Step 148: t15 = x^0x60c89ce5c263405370a08b6d03000
307 0 : for (int i = 0; i < 12; ++i)
308 0 : t15 = m.mul(t15, t15);
309 :
310 : // Step 149: t14 = x^0x60c89ce5c263405370a08b6d0302b
311 0 : t14 = m.mul(t14, t15);
312 :
313 : // Step 161: t14 = x^0x60c89ce5c263405370a08b6d0302b000
314 0 : for (int i = 0; i < 12; ++i)
315 0 : t14 = m.mul(t14, t14);
316 :
317 : // Step 162: t13 = x^0x60c89ce5c263405370a08b6d0302b0bb
318 0 : t13 = m.mul(t13, t14);
319 :
320 : // Step 170: t13 = x^0x60c89ce5c263405370a08b6d0302b0bb00
321 0 : for (int i = 0; i < 8; ++i)
322 0 : t13 = m.mul(t13, t13);
323 :
324 : // Step 171: t12 = x^0x60c89ce5c263405370a08b6d0302b0bb2f
325 0 : t12 = m.mul(t12, t13);
326 :
327 : // Step 185: t12 = x^0x183227397098d014dc2822db40c0ac2ecbc000
328 0 : for (int i = 0; i < 14; ++i)
329 0 : t12 = m.mul(t12, t12);
330 :
331 : // Step 186: t11 = x^0x183227397098d014dc2822db40c0ac2ecbc0b5
332 0 : t11 = m.mul(t11, t12);
333 :
334 : // Step 195: t11 = x^0x30644e72e131a029b85045b68181585d97816a00
335 0 : for (int i = 0; i < 9; ++i)
336 0 : t11 = m.mul(t11, t11);
337 :
338 : // Step 196: t10 = x^0x30644e72e131a029b85045b68181585d97816a91
339 0 : t10 = m.mul(t10, t11);
340 :
341 : // Step 201: t10 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d5220
342 0 : for (int i = 0; i < 5; ++i)
343 0 : t10 = m.mul(t10, t10);
344 :
345 : // Step 202: t9 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d522d
346 0 : t9 = m.mul(t9, t10);
347 :
348 : // Step 214: t9 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d522d000
349 0 : for (int i = 0; i < 12; ++i)
350 0 : t9 = m.mul(t9, t9);
351 :
352 : // Step 215: t8 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d522d0e3
353 0 : t8 = m.mul(t8, t9);
354 :
355 : // Step 223: t8 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d522d0e300
356 0 : for (int i = 0; i < 8; ++i)
357 0 : t8 = m.mul(t8, t8);
358 :
359 : // Step 224: t7 = x^0x60c89ce5c263405370a08b6d0302b0bb2f02d522d0e395
360 0 : t7 = m.mul(t7, t8);
361 :
362 : // Step 235: t7 = x^0x30644e72e131a029b85045b68181585d97816a916871ca800
363 0 : for (int i = 0; i < 11; ++i)
364 0 : t7 = m.mul(t7, t7);
365 :
366 : // Step 236: t6 = x^0x30644e72e131a029b85045b68181585d97816a916871ca8d3
367 0 : t6 = m.mul(t6, t7);
368 :
369 : // Step 243: t6 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e546980
370 0 : for (int i = 0; i < 7; ++i)
371 0 : t6 = m.mul(t6, t6);
372 :
373 : // Step 244: t5 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e5469e1
374 0 : t5 = m.mul(t5, t6);
375 :
376 : // Step 255: t5 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f0800
377 0 : for (int i = 0; i < 11; ++i)
378 0 : t5 = m.mul(t5, t5);
379 :
380 : // Step 256: t4 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f0823
381 0 : t4 = m.mul(t4, t5);
382 :
383 : // Step 268: t4 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f0823000
384 0 : for (int i = 0; i < 12; ++i)
385 0 : t4 = m.mul(t4, t4);
386 :
387 : // Step 269: t3 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f082305b
388 0 : t3 = m.mul(t3, t4);
389 :
390 : // Step 278: t3 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e5469e10460b600
391 0 : for (int i = 0; i < 9; ++i)
392 0 : t3 = m.mul(t3, t3);
393 :
394 : // Step 279: t2 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e5469e10460b6c3
395 0 : t2 = m.mul(t2, t3);
396 :
397 : // Step 287: t2 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e5469e10460b6c300
398 0 : for (int i = 0; i < 8; ++i)
399 0 : t2 = m.mul(t2, t2);
400 :
401 : // Step 288: t1 = x^0x183227397098d014dc2822db40c0ac2ecbc0b548b438e5469e10460b6c3e7
402 0 : t1 = m.mul(t1, t2);
403 :
404 : // Step 295: t1 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f082305b61f380
405 0 : for (int i = 0; i < 7; ++i)
406 0 : t1 = m.mul(t1, t1);
407 :
408 : // Step 296: t0 = x^0xc19139cb84c680a6e14116da060561765e05aa45a1c72a34f082305b61f3f5
409 0 : t0 = m.mul(t0, t1);
410 :
411 : // Step 302: t0 = x^0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd40
412 0 : for (int i = 0; i < 6; ++i)
413 0 : t0 = m.mul(t0, t0);
414 :
415 : // Step 303: z = x^0x30644e72e131a029b85045b68181585d97816a916871ca8d3c208c16d87cfd45
416 0 : z = m.mul(z, t0);
417 :
418 0 : return z;
419 : }
420 :
421 : } // namespace evmmax::bn254
|
