1// Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name secp256k1 '' 64 '2^256 - 2^32 - 977' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
2// curve description (via package name): secp256k1
3// machine_wordsize = 64 (from "64")
4// requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp
5// m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f (from "2^256 - 2^32 - 977")
6//
7// NOTE: In addition to the bounds specified above each function, all
8// functions synthesized for this Montgomery arithmetic require the
9// input to be strictly less than the prime modulus (m), and also
10// require the input to be in the unique saturated representation.
11// All functions also ensure that these two properties are true of
12// return values.
13//
14// Computed values:
15// eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192)
16// bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248)
17// twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in
18// if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256
19
20const std = @import("std");
21const mode = @import("builtin").mode; // Checked arithmetic is disabled in non-debug modes to avoid side channels
22
23// The type MontgomeryDomainFieldElement is a field element in the Montgomery domain.
24// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
25pub const MontgomeryDomainFieldElement = [4]u64;
26
27// The type NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain.
28// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
29pub const NonMontgomeryDomainFieldElement = [4]u64;
30
31/// The function addcarryxU64 is an addition with carry.
32///
33/// Postconditions:
34/// out1 = (arg1 + arg2 + arg3) mod 2^64
35/// out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
36///
37/// Input Bounds:
38/// arg1: [0x0 ~> 0x1]
39/// arg2: [0x0 ~> 0xffffffffffffffff]
40/// arg3: [0x0 ~> 0xffffffffffffffff]
41/// Output Bounds:
42/// out1: [0x0 ~> 0xffffffffffffffff]
43/// out2: [0x0 ~> 0x1]
44fn addcarryxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
45 const x = @as(u128, arg2) +% arg3 +% arg1;
46 out1.* = @truncate(x);
47 out2.* = @truncate(x >> 64);
48}
49
50/// The function subborrowxU64 is a subtraction with borrow.
51///
52/// Postconditions:
53/// out1 = (-arg1 + arg2 + -arg3) mod 2^64
54/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
55///
56/// Input Bounds:
57/// arg1: [0x0 ~> 0x1]
58/// arg2: [0x0 ~> 0xffffffffffffffff]
59/// arg3: [0x0 ~> 0xffffffffffffffff]
60/// Output Bounds:
61/// out1: [0x0 ~> 0xffffffffffffffff]
62/// out2: [0x0 ~> 0x1]
63fn subborrowxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
64 const x = @as(u128, arg2) -% arg3 -% arg1;
65 out1.* = @truncate(x);
66 out2.* = @truncate(x >> 64);
67}
68
69/// The function mulxU64 is a multiplication, returning the full double-width result.
70///
71/// Postconditions:
72/// out1 = (arg1 * arg2) mod 2^64
73/// out2 = ⌊arg1 * arg2 / 2^64⌋
74///
75/// Input Bounds:
76/// arg1: [0x0 ~> 0xffffffffffffffff]
77/// arg2: [0x0 ~> 0xffffffffffffffff]
78/// Output Bounds:
79/// out1: [0x0 ~> 0xffffffffffffffff]
80/// out2: [0x0 ~> 0xffffffffffffffff]
81fn mulxU64(out1: *u64, out2: *u64, arg1: u64, arg2: u64) void {
82 @setRuntimeSafety(mode == .debug);
83
84 const x = @as(u128, arg1) * @as(u128, arg2);
85 out1.* = @as(u64, @truncate(x));
86 out2.* = @as(u64, @truncate(x >> 64));
87}
88
89/// The function cmovznzU64 is a single-word conditional move.
90///
91/// Postconditions:
92/// out1 = (if arg1 = 0 then arg2 else arg3)
93///
94/// Input Bounds:
95/// arg1: [0x0 ~> 0x1]
96/// arg2: [0x0 ~> 0xffffffffffffffff]
97/// arg3: [0x0 ~> 0xffffffffffffffff]
98/// Output Bounds:
99/// out1: [0x0 ~> 0xffffffffffffffff]
100fn cmovznzU64(out1: *u64, arg1: u1, arg2: u64, arg3: u64) void {
101 @setRuntimeSafety(mode == .debug);
102
103 const mask = 0 -% @as(u64, arg1);
104 out1.* = (mask & arg3) | ((~mask) & arg2);
105}
106
107/// The function mul multiplies two field elements in the Montgomery domain.
108///
109/// Preconditions:
110/// 0 ≤ eval arg1 < m
111/// 0 ≤ eval arg2 < m
112/// Postconditions:
113/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
114/// 0 ≤ eval out1 < m
115///
116pub fn mul(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
117 @setRuntimeSafety(mode == .debug);
118
119 const x1 = (arg1[1]);
120 const x2 = (arg1[2]);
121 const x3 = (arg1[3]);
122 const x4 = (arg1[0]);
123 var x5: u64 = undefined;
124 var x6: u64 = undefined;
125 mulxU64(&x5, &x6, x4, (arg2[3]));
126 var x7: u64 = undefined;
127 var x8: u64 = undefined;
128 mulxU64(&x7, &x8, x4, (arg2[2]));
129 var x9: u64 = undefined;
130 var x10: u64 = undefined;
131 mulxU64(&x9, &x10, x4, (arg2[1]));
132 var x11: u64 = undefined;
133 var x12: u64 = undefined;
134 mulxU64(&x11, &x12, x4, (arg2[0]));
135 var x13: u64 = undefined;
136 var x14: u1 = undefined;
137 addcarryxU64(&x13, &x14, 0x0, x12, x9);
138 var x15: u64 = undefined;
139 var x16: u1 = undefined;
140 addcarryxU64(&x15, &x16, x14, x10, x7);
141 var x17: u64 = undefined;
142 var x18: u1 = undefined;
143 addcarryxU64(&x17, &x18, x16, x8, x5);
144 const x19 = (@as(u64, x18) + x6);
145 var x20: u64 = undefined;
146 var x21: u64 = undefined;
147 mulxU64(&x20, &x21, x11, 0xd838091dd2253531);
148 var x22: u64 = undefined;
149 var x23: u64 = undefined;
150 mulxU64(&x22, &x23, x20, 0xffffffffffffffff);
151 var x24: u64 = undefined;
152 var x25: u64 = undefined;
153 mulxU64(&x24, &x25, x20, 0xffffffffffffffff);
154 var x26: u64 = undefined;
155 var x27: u64 = undefined;
156 mulxU64(&x26, &x27, x20, 0xffffffffffffffff);
157 var x28: u64 = undefined;
158 var x29: u64 = undefined;
159 mulxU64(&x28, &x29, x20, 0xfffffffefffffc2f);
160 var x30: u64 = undefined;
161 var x31: u1 = undefined;
162 addcarryxU64(&x30, &x31, 0x0, x29, x26);
163 var x32: u64 = undefined;
164 var x33: u1 = undefined;
165 addcarryxU64(&x32, &x33, x31, x27, x24);
166 var x34: u64 = undefined;
167 var x35: u1 = undefined;
168 addcarryxU64(&x34, &x35, x33, x25, x22);
169 const x36 = (@as(u64, x35) + x23);
170 var x37: u64 = undefined;
171 var x38: u1 = undefined;
172 addcarryxU64(&x37, &x38, 0x0, x11, x28);
173 var x39: u64 = undefined;
174 var x40: u1 = undefined;
175 addcarryxU64(&x39, &x40, x38, x13, x30);
176 var x41: u64 = undefined;
177 var x42: u1 = undefined;
178 addcarryxU64(&x41, &x42, x40, x15, x32);
179 var x43: u64 = undefined;
180 var x44: u1 = undefined;
181 addcarryxU64(&x43, &x44, x42, x17, x34);
182 var x45: u64 = undefined;
183 var x46: u1 = undefined;
184 addcarryxU64(&x45, &x46, x44, x19, x36);
185 var x47: u64 = undefined;
186 var x48: u64 = undefined;
187 mulxU64(&x47, &x48, x1, (arg2[3]));
188 var x49: u64 = undefined;
189 var x50: u64 = undefined;
190 mulxU64(&x49, &x50, x1, (arg2[2]));
191 var x51: u64 = undefined;
192 var x52: u64 = undefined;
193 mulxU64(&x51, &x52, x1, (arg2[1]));
194 var x53: u64 = undefined;
195 var x54: u64 = undefined;
196 mulxU64(&x53, &x54, x1, (arg2[0]));
197 var x55: u64 = undefined;
198 var x56: u1 = undefined;
199 addcarryxU64(&x55, &x56, 0x0, x54, x51);
200 var x57: u64 = undefined;
201 var x58: u1 = undefined;
202 addcarryxU64(&x57, &x58, x56, x52, x49);
203 var x59: u64 = undefined;
204 var x60: u1 = undefined;
205 addcarryxU64(&x59, &x60, x58, x50, x47);
206 const x61 = (@as(u64, x60) + x48);
207 var x62: u64 = undefined;
208 var x63: u1 = undefined;
209 addcarryxU64(&x62, &x63, 0x0, x39, x53);
210 var x64: u64 = undefined;
211 var x65: u1 = undefined;
212 addcarryxU64(&x64, &x65, x63, x41, x55);
213 var x66: u64 = undefined;
214 var x67: u1 = undefined;
215 addcarryxU64(&x66, &x67, x65, x43, x57);
216 var x68: u64 = undefined;
217 var x69: u1 = undefined;
218 addcarryxU64(&x68, &x69, x67, x45, x59);
219 var x70: u64 = undefined;
220 var x71: u1 = undefined;
221 addcarryxU64(&x70, &x71, x69, @as(u64, x46), x61);
222 var x72: u64 = undefined;
223 var x73: u64 = undefined;
224 mulxU64(&x72, &x73, x62, 0xd838091dd2253531);
225 var x74: u64 = undefined;
226 var x75: u64 = undefined;
227 mulxU64(&x74, &x75, x72, 0xffffffffffffffff);
228 var x76: u64 = undefined;
229 var x77: u64 = undefined;
230 mulxU64(&x76, &x77, x72, 0xffffffffffffffff);
231 var x78: u64 = undefined;
232 var x79: u64 = undefined;
233 mulxU64(&x78, &x79, x72, 0xffffffffffffffff);
234 var x80: u64 = undefined;
235 var x81: u64 = undefined;
236 mulxU64(&x80, &x81, x72, 0xfffffffefffffc2f);
237 var x82: u64 = undefined;
238 var x83: u1 = undefined;
239 addcarryxU64(&x82, &x83, 0x0, x81, x78);
240 var x84: u64 = undefined;
241 var x85: u1 = undefined;
242 addcarryxU64(&x84, &x85, x83, x79, x76);
243 var x86: u64 = undefined;
244 var x87: u1 = undefined;
245 addcarryxU64(&x86, &x87, x85, x77, x74);
246 const x88 = (@as(u64, x87) + x75);
247 var x89: u64 = undefined;
248 var x90: u1 = undefined;
249 addcarryxU64(&x89, &x90, 0x0, x62, x80);
250 var x91: u64 = undefined;
251 var x92: u1 = undefined;
252 addcarryxU64(&x91, &x92, x90, x64, x82);
253 var x93: u64 = undefined;
254 var x94: u1 = undefined;
255 addcarryxU64(&x93, &x94, x92, x66, x84);
256 var x95: u64 = undefined;
257 var x96: u1 = undefined;
258 addcarryxU64(&x95, &x96, x94, x68, x86);
259 var x97: u64 = undefined;
260 var x98: u1 = undefined;
261 addcarryxU64(&x97, &x98, x96, x70, x88);
262 const x99 = (@as(u64, x98) + @as(u64, x71));
263 var x100: u64 = undefined;
264 var x101: u64 = undefined;
265 mulxU64(&x100, &x101, x2, (arg2[3]));
266 var x102: u64 = undefined;
267 var x103: u64 = undefined;
268 mulxU64(&x102, &x103, x2, (arg2[2]));
269 var x104: u64 = undefined;
270 var x105: u64 = undefined;
271 mulxU64(&x104, &x105, x2, (arg2[1]));
272 var x106: u64 = undefined;
273 var x107: u64 = undefined;
274 mulxU64(&x106, &x107, x2, (arg2[0]));
275 var x108: u64 = undefined;
276 var x109: u1 = undefined;
277 addcarryxU64(&x108, &x109, 0x0, x107, x104);
278 var x110: u64 = undefined;
279 var x111: u1 = undefined;
280 addcarryxU64(&x110, &x111, x109, x105, x102);
281 var x112: u64 = undefined;
282 var x113: u1 = undefined;
283 addcarryxU64(&x112, &x113, x111, x103, x100);
284 const x114 = (@as(u64, x113) + x101);
285 var x115: u64 = undefined;
286 var x116: u1 = undefined;
287 addcarryxU64(&x115, &x116, 0x0, x91, x106);
288 var x117: u64 = undefined;
289 var x118: u1 = undefined;
290 addcarryxU64(&x117, &x118, x116, x93, x108);
291 var x119: u64 = undefined;
292 var x120: u1 = undefined;
293 addcarryxU64(&x119, &x120, x118, x95, x110);
294 var x121: u64 = undefined;
295 var x122: u1 = undefined;
296 addcarryxU64(&x121, &x122, x120, x97, x112);
297 var x123: u64 = undefined;
298 var x124: u1 = undefined;
299 addcarryxU64(&x123, &x124, x122, x99, x114);
300 var x125: u64 = undefined;
301 var x126: u64 = undefined;
302 mulxU64(&x125, &x126, x115, 0xd838091dd2253531);
303 var x127: u64 = undefined;
304 var x128: u64 = undefined;
305 mulxU64(&x127, &x128, x125, 0xffffffffffffffff);
306 var x129: u64 = undefined;
307 var x130: u64 = undefined;
308 mulxU64(&x129, &x130, x125, 0xffffffffffffffff);
309 var x131: u64 = undefined;
310 var x132: u64 = undefined;
311 mulxU64(&x131, &x132, x125, 0xffffffffffffffff);
312 var x133: u64 = undefined;
313 var x134: u64 = undefined;
314 mulxU64(&x133, &x134, x125, 0xfffffffefffffc2f);
315 var x135: u64 = undefined;
316 var x136: u1 = undefined;
317 addcarryxU64(&x135, &x136, 0x0, x134, x131);
318 var x137: u64 = undefined;
319 var x138: u1 = undefined;
320 addcarryxU64(&x137, &x138, x136, x132, x129);
321 var x139: u64 = undefined;
322 var x140: u1 = undefined;
323 addcarryxU64(&x139, &x140, x138, x130, x127);
324 const x141 = (@as(u64, x140) + x128);
325 var x142: u64 = undefined;
326 var x143: u1 = undefined;
327 addcarryxU64(&x142, &x143, 0x0, x115, x133);
328 var x144: u64 = undefined;
329 var x145: u1 = undefined;
330 addcarryxU64(&x144, &x145, x143, x117, x135);
331 var x146: u64 = undefined;
332 var x147: u1 = undefined;
333 addcarryxU64(&x146, &x147, x145, x119, x137);
334 var x148: u64 = undefined;
335 var x149: u1 = undefined;
336 addcarryxU64(&x148, &x149, x147, x121, x139);
337 var x150: u64 = undefined;
338 var x151: u1 = undefined;
339 addcarryxU64(&x150, &x151, x149, x123, x141);
340 const x152 = (@as(u64, x151) + @as(u64, x124));
341 var x153: u64 = undefined;
342 var x154: u64 = undefined;
343 mulxU64(&x153, &x154, x3, (arg2[3]));
344 var x155: u64 = undefined;
345 var x156: u64 = undefined;
346 mulxU64(&x155, &x156, x3, (arg2[2]));
347 var x157: u64 = undefined;
348 var x158: u64 = undefined;
349 mulxU64(&x157, &x158, x3, (arg2[1]));
350 var x159: u64 = undefined;
351 var x160: u64 = undefined;
352 mulxU64(&x159, &x160, x3, (arg2[0]));
353 var x161: u64 = undefined;
354 var x162: u1 = undefined;
355 addcarryxU64(&x161, &x162, 0x0, x160, x157);
356 var x163: u64 = undefined;
357 var x164: u1 = undefined;
358 addcarryxU64(&x163, &x164, x162, x158, x155);
359 var x165: u64 = undefined;
360 var x166: u1 = undefined;
361 addcarryxU64(&x165, &x166, x164, x156, x153);
362 const x167 = (@as(u64, x166) + x154);
363 var x168: u64 = undefined;
364 var x169: u1 = undefined;
365 addcarryxU64(&x168, &x169, 0x0, x144, x159);
366 var x170: u64 = undefined;
367 var x171: u1 = undefined;
368 addcarryxU64(&x170, &x171, x169, x146, x161);
369 var x172: u64 = undefined;
370 var x173: u1 = undefined;
371 addcarryxU64(&x172, &x173, x171, x148, x163);
372 var x174: u64 = undefined;
373 var x175: u1 = undefined;
374 addcarryxU64(&x174, &x175, x173, x150, x165);
375 var x176: u64 = undefined;
376 var x177: u1 = undefined;
377 addcarryxU64(&x176, &x177, x175, x152, x167);
378 var x178: u64 = undefined;
379 var x179: u64 = undefined;
380 mulxU64(&x178, &x179, x168, 0xd838091dd2253531);
381 var x180: u64 = undefined;
382 var x181: u64 = undefined;
383 mulxU64(&x180, &x181, x178, 0xffffffffffffffff);
384 var x182: u64 = undefined;
385 var x183: u64 = undefined;
386 mulxU64(&x182, &x183, x178, 0xffffffffffffffff);
387 var x184: u64 = undefined;
388 var x185: u64 = undefined;
389 mulxU64(&x184, &x185, x178, 0xffffffffffffffff);
390 var x186: u64 = undefined;
391 var x187: u64 = undefined;
392 mulxU64(&x186, &x187, x178, 0xfffffffefffffc2f);
393 var x188: u64 = undefined;
394 var x189: u1 = undefined;
395 addcarryxU64(&x188, &x189, 0x0, x187, x184);
396 var x190: u64 = undefined;
397 var x191: u1 = undefined;
398 addcarryxU64(&x190, &x191, x189, x185, x182);
399 var x192: u64 = undefined;
400 var x193: u1 = undefined;
401 addcarryxU64(&x192, &x193, x191, x183, x180);
402 const x194 = (@as(u64, x193) + x181);
403 var x195: u64 = undefined;
404 var x196: u1 = undefined;
405 addcarryxU64(&x195, &x196, 0x0, x168, x186);
406 var x197: u64 = undefined;
407 var x198: u1 = undefined;
408 addcarryxU64(&x197, &x198, x196, x170, x188);
409 var x199: u64 = undefined;
410 var x200: u1 = undefined;
411 addcarryxU64(&x199, &x200, x198, x172, x190);
412 var x201: u64 = undefined;
413 var x202: u1 = undefined;
414 addcarryxU64(&x201, &x202, x200, x174, x192);
415 var x203: u64 = undefined;
416 var x204: u1 = undefined;
417 addcarryxU64(&x203, &x204, x202, x176, x194);
418 const x205 = (@as(u64, x204) + @as(u64, x177));
419 var x206: u64 = undefined;
420 var x207: u1 = undefined;
421 subborrowxU64(&x206, &x207, 0x0, x197, 0xfffffffefffffc2f);
422 var x208: u64 = undefined;
423 var x209: u1 = undefined;
424 subborrowxU64(&x208, &x209, x207, x199, 0xffffffffffffffff);
425 var x210: u64 = undefined;
426 var x211: u1 = undefined;
427 subborrowxU64(&x210, &x211, x209, x201, 0xffffffffffffffff);
428 var x212: u64 = undefined;
429 var x213: u1 = undefined;
430 subborrowxU64(&x212, &x213, x211, x203, 0xffffffffffffffff);
431 var x214: u64 = undefined;
432 var x215: u1 = undefined;
433 subborrowxU64(&x214, &x215, x213, x205, 0x0);
434 var x216: u64 = undefined;
435 cmovznzU64(&x216, x215, x206, x197);
436 var x217: u64 = undefined;
437 cmovznzU64(&x217, x215, x208, x199);
438 var x218: u64 = undefined;
439 cmovznzU64(&x218, x215, x210, x201);
440 var x219: u64 = undefined;
441 cmovznzU64(&x219, x215, x212, x203);
442 out1[0] = x216;
443 out1[1] = x217;
444 out1[2] = x218;
445 out1[3] = x219;
446}
447
448/// The function square squares a field element in the Montgomery domain.
449///
450/// Preconditions:
451/// 0 ≤ eval arg1 < m
452/// Postconditions:
453/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
454/// 0 ≤ eval out1 < m
455///
456pub fn square(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
457 @setRuntimeSafety(mode == .debug);
458
459 const x1 = (arg1[1]);
460 const x2 = (arg1[2]);
461 const x3 = (arg1[3]);
462 const x4 = (arg1[0]);
463 var x5: u64 = undefined;
464 var x6: u64 = undefined;
465 mulxU64(&x5, &x6, x4, (arg1[3]));
466 var x7: u64 = undefined;
467 var x8: u64 = undefined;
468 mulxU64(&x7, &x8, x4, (arg1[2]));
469 var x9: u64 = undefined;
470 var x10: u64 = undefined;
471 mulxU64(&x9, &x10, x4, (arg1[1]));
472 var x11: u64 = undefined;
473 var x12: u64 = undefined;
474 mulxU64(&x11, &x12, x4, (arg1[0]));
475 var x13: u64 = undefined;
476 var x14: u1 = undefined;
477 addcarryxU64(&x13, &x14, 0x0, x12, x9);
478 var x15: u64 = undefined;
479 var x16: u1 = undefined;
480 addcarryxU64(&x15, &x16, x14, x10, x7);
481 var x17: u64 = undefined;
482 var x18: u1 = undefined;
483 addcarryxU64(&x17, &x18, x16, x8, x5);
484 const x19 = (@as(u64, x18) + x6);
485 var x20: u64 = undefined;
486 var x21: u64 = undefined;
487 mulxU64(&x20, &x21, x11, 0xd838091dd2253531);
488 var x22: u64 = undefined;
489 var x23: u64 = undefined;
490 mulxU64(&x22, &x23, x20, 0xffffffffffffffff);
491 var x24: u64 = undefined;
492 var x25: u64 = undefined;
493 mulxU64(&x24, &x25, x20, 0xffffffffffffffff);
494 var x26: u64 = undefined;
495 var x27: u64 = undefined;
496 mulxU64(&x26, &x27, x20, 0xffffffffffffffff);
497 var x28: u64 = undefined;
498 var x29: u64 = undefined;
499 mulxU64(&x28, &x29, x20, 0xfffffffefffffc2f);
500 var x30: u64 = undefined;
501 var x31: u1 = undefined;
502 addcarryxU64(&x30, &x31, 0x0, x29, x26);
503 var x32: u64 = undefined;
504 var x33: u1 = undefined;
505 addcarryxU64(&x32, &x33, x31, x27, x24);
506 var x34: u64 = undefined;
507 var x35: u1 = undefined;
508 addcarryxU64(&x34, &x35, x33, x25, x22);
509 const x36 = (@as(u64, x35) + x23);
510 var x37: u64 = undefined;
511 var x38: u1 = undefined;
512 addcarryxU64(&x37, &x38, 0x0, x11, x28);
513 var x39: u64 = undefined;
514 var x40: u1 = undefined;
515 addcarryxU64(&x39, &x40, x38, x13, x30);
516 var x41: u64 = undefined;
517 var x42: u1 = undefined;
518 addcarryxU64(&x41, &x42, x40, x15, x32);
519 var x43: u64 = undefined;
520 var x44: u1 = undefined;
521 addcarryxU64(&x43, &x44, x42, x17, x34);
522 var x45: u64 = undefined;
523 var x46: u1 = undefined;
524 addcarryxU64(&x45, &x46, x44, x19, x36);
525 var x47: u64 = undefined;
526 var x48: u64 = undefined;
527 mulxU64(&x47, &x48, x1, (arg1[3]));
528 var x49: u64 = undefined;
529 var x50: u64 = undefined;
530 mulxU64(&x49, &x50, x1, (arg1[2]));
531 var x51: u64 = undefined;
532 var x52: u64 = undefined;
533 mulxU64(&x51, &x52, x1, (arg1[1]));
534 var x53: u64 = undefined;
535 var x54: u64 = undefined;
536 mulxU64(&x53, &x54, x1, (arg1[0]));
537 var x55: u64 = undefined;
538 var x56: u1 = undefined;
539 addcarryxU64(&x55, &x56, 0x0, x54, x51);
540 var x57: u64 = undefined;
541 var x58: u1 = undefined;
542 addcarryxU64(&x57, &x58, x56, x52, x49);
543 var x59: u64 = undefined;
544 var x60: u1 = undefined;
545 addcarryxU64(&x59, &x60, x58, x50, x47);
546 const x61 = (@as(u64, x60) + x48);
547 var x62: u64 = undefined;
548 var x63: u1 = undefined;
549 addcarryxU64(&x62, &x63, 0x0, x39, x53);
550 var x64: u64 = undefined;
551 var x65: u1 = undefined;
552 addcarryxU64(&x64, &x65, x63, x41, x55);
553 var x66: u64 = undefined;
554 var x67: u1 = undefined;
555 addcarryxU64(&x66, &x67, x65, x43, x57);
556 var x68: u64 = undefined;
557 var x69: u1 = undefined;
558 addcarryxU64(&x68, &x69, x67, x45, x59);
559 var x70: u64 = undefined;
560 var x71: u1 = undefined;
561 addcarryxU64(&x70, &x71, x69, @as(u64, x46), x61);
562 var x72: u64 = undefined;
563 var x73: u64 = undefined;
564 mulxU64(&x72, &x73, x62, 0xd838091dd2253531);
565 var x74: u64 = undefined;
566 var x75: u64 = undefined;
567 mulxU64(&x74, &x75, x72, 0xffffffffffffffff);
568 var x76: u64 = undefined;
569 var x77: u64 = undefined;
570 mulxU64(&x76, &x77, x72, 0xffffffffffffffff);
571 var x78: u64 = undefined;
572 var x79: u64 = undefined;
573 mulxU64(&x78, &x79, x72, 0xffffffffffffffff);
574 var x80: u64 = undefined;
575 var x81: u64 = undefined;
576 mulxU64(&x80, &x81, x72, 0xfffffffefffffc2f);
577 var x82: u64 = undefined;
578 var x83: u1 = undefined;
579 addcarryxU64(&x82, &x83, 0x0, x81, x78);
580 var x84: u64 = undefined;
581 var x85: u1 = undefined;
582 addcarryxU64(&x84, &x85, x83, x79, x76);
583 var x86: u64 = undefined;
584 var x87: u1 = undefined;
585 addcarryxU64(&x86, &x87, x85, x77, x74);
586 const x88 = (@as(u64, x87) + x75);
587 var x89: u64 = undefined;
588 var x90: u1 = undefined;
589 addcarryxU64(&x89, &x90, 0x0, x62, x80);
590 var x91: u64 = undefined;
591 var x92: u1 = undefined;
592 addcarryxU64(&x91, &x92, x90, x64, x82);
593 var x93: u64 = undefined;
594 var x94: u1 = undefined;
595 addcarryxU64(&x93, &x94, x92, x66, x84);
596 var x95: u64 = undefined;
597 var x96: u1 = undefined;
598 addcarryxU64(&x95, &x96, x94, x68, x86);
599 var x97: u64 = undefined;
600 var x98: u1 = undefined;
601 addcarryxU64(&x97, &x98, x96, x70, x88);
602 const x99 = (@as(u64, x98) + @as(u64, x71));
603 var x100: u64 = undefined;
604 var x101: u64 = undefined;
605 mulxU64(&x100, &x101, x2, (arg1[3]));
606 var x102: u64 = undefined;
607 var x103: u64 = undefined;
608 mulxU64(&x102, &x103, x2, (arg1[2]));
609 var x104: u64 = undefined;
610 var x105: u64 = undefined;
611 mulxU64(&x104, &x105, x2, (arg1[1]));
612 var x106: u64 = undefined;
613 var x107: u64 = undefined;
614 mulxU64(&x106, &x107, x2, (arg1[0]));
615 var x108: u64 = undefined;
616 var x109: u1 = undefined;
617 addcarryxU64(&x108, &x109, 0x0, x107, x104);
618 var x110: u64 = undefined;
619 var x111: u1 = undefined;
620 addcarryxU64(&x110, &x111, x109, x105, x102);
621 var x112: u64 = undefined;
622 var x113: u1 = undefined;
623 addcarryxU64(&x112, &x113, x111, x103, x100);
624 const x114 = (@as(u64, x113) + x101);
625 var x115: u64 = undefined;
626 var x116: u1 = undefined;
627 addcarryxU64(&x115, &x116, 0x0, x91, x106);
628 var x117: u64 = undefined;
629 var x118: u1 = undefined;
630 addcarryxU64(&x117, &x118, x116, x93, x108);
631 var x119: u64 = undefined;
632 var x120: u1 = undefined;
633 addcarryxU64(&x119, &x120, x118, x95, x110);
634 var x121: u64 = undefined;
635 var x122: u1 = undefined;
636 addcarryxU64(&x121, &x122, x120, x97, x112);
637 var x123: u64 = undefined;
638 var x124: u1 = undefined;
639 addcarryxU64(&x123, &x124, x122, x99, x114);
640 var x125: u64 = undefined;
641 var x126: u64 = undefined;
642 mulxU64(&x125, &x126, x115, 0xd838091dd2253531);
643 var x127: u64 = undefined;
644 var x128: u64 = undefined;
645 mulxU64(&x127, &x128, x125, 0xffffffffffffffff);
646 var x129: u64 = undefined;
647 var x130: u64 = undefined;
648 mulxU64(&x129, &x130, x125, 0xffffffffffffffff);
649 var x131: u64 = undefined;
650 var x132: u64 = undefined;
651 mulxU64(&x131, &x132, x125, 0xffffffffffffffff);
652 var x133: u64 = undefined;
653 var x134: u64 = undefined;
654 mulxU64(&x133, &x134, x125, 0xfffffffefffffc2f);
655 var x135: u64 = undefined;
656 var x136: u1 = undefined;
657 addcarryxU64(&x135, &x136, 0x0, x134, x131);
658 var x137: u64 = undefined;
659 var x138: u1 = undefined;
660 addcarryxU64(&x137, &x138, x136, x132, x129);
661 var x139: u64 = undefined;
662 var x140: u1 = undefined;
663 addcarryxU64(&x139, &x140, x138, x130, x127);
664 const x141 = (@as(u64, x140) + x128);
665 var x142: u64 = undefined;
666 var x143: u1 = undefined;
667 addcarryxU64(&x142, &x143, 0x0, x115, x133);
668 var x144: u64 = undefined;
669 var x145: u1 = undefined;
670 addcarryxU64(&x144, &x145, x143, x117, x135);
671 var x146: u64 = undefined;
672 var x147: u1 = undefined;
673 addcarryxU64(&x146, &x147, x145, x119, x137);
674 var x148: u64 = undefined;
675 var x149: u1 = undefined;
676 addcarryxU64(&x148, &x149, x147, x121, x139);
677 var x150: u64 = undefined;
678 var x151: u1 = undefined;
679 addcarryxU64(&x150, &x151, x149, x123, x141);
680 const x152 = (@as(u64, x151) + @as(u64, x124));
681 var x153: u64 = undefined;
682 var x154: u64 = undefined;
683 mulxU64(&x153, &x154, x3, (arg1[3]));
684 var x155: u64 = undefined;
685 var x156: u64 = undefined;
686 mulxU64(&x155, &x156, x3, (arg1[2]));
687 var x157: u64 = undefined;
688 var x158: u64 = undefined;
689 mulxU64(&x157, &x158, x3, (arg1[1]));
690 var x159: u64 = undefined;
691 var x160: u64 = undefined;
692 mulxU64(&x159, &x160, x3, (arg1[0]));
693 var x161: u64 = undefined;
694 var x162: u1 = undefined;
695 addcarryxU64(&x161, &x162, 0x0, x160, x157);
696 var x163: u64 = undefined;
697 var x164: u1 = undefined;
698 addcarryxU64(&x163, &x164, x162, x158, x155);
699 var x165: u64 = undefined;
700 var x166: u1 = undefined;
701 addcarryxU64(&x165, &x166, x164, x156, x153);
702 const x167 = (@as(u64, x166) + x154);
703 var x168: u64 = undefined;
704 var x169: u1 = undefined;
705 addcarryxU64(&x168, &x169, 0x0, x144, x159);
706 var x170: u64 = undefined;
707 var x171: u1 = undefined;
708 addcarryxU64(&x170, &x171, x169, x146, x161);
709 var x172: u64 = undefined;
710 var x173: u1 = undefined;
711 addcarryxU64(&x172, &x173, x171, x148, x163);
712 var x174: u64 = undefined;
713 var x175: u1 = undefined;
714 addcarryxU64(&x174, &x175, x173, x150, x165);
715 var x176: u64 = undefined;
716 var x177: u1 = undefined;
717 addcarryxU64(&x176, &x177, x175, x152, x167);
718 var x178: u64 = undefined;
719 var x179: u64 = undefined;
720 mulxU64(&x178, &x179, x168, 0xd838091dd2253531);
721 var x180: u64 = undefined;
722 var x181: u64 = undefined;
723 mulxU64(&x180, &x181, x178, 0xffffffffffffffff);
724 var x182: u64 = undefined;
725 var x183: u64 = undefined;
726 mulxU64(&x182, &x183, x178, 0xffffffffffffffff);
727 var x184: u64 = undefined;
728 var x185: u64 = undefined;
729 mulxU64(&x184, &x185, x178, 0xffffffffffffffff);
730 var x186: u64 = undefined;
731 var x187: u64 = undefined;
732 mulxU64(&x186, &x187, x178, 0xfffffffefffffc2f);
733 var x188: u64 = undefined;
734 var x189: u1 = undefined;
735 addcarryxU64(&x188, &x189, 0x0, x187, x184);
736 var x190: u64 = undefined;
737 var x191: u1 = undefined;
738 addcarryxU64(&x190, &x191, x189, x185, x182);
739 var x192: u64 = undefined;
740 var x193: u1 = undefined;
741 addcarryxU64(&x192, &x193, x191, x183, x180);
742 const x194 = (@as(u64, x193) + x181);
743 var x195: u64 = undefined;
744 var x196: u1 = undefined;
745 addcarryxU64(&x195, &x196, 0x0, x168, x186);
746 var x197: u64 = undefined;
747 var x198: u1 = undefined;
748 addcarryxU64(&x197, &x198, x196, x170, x188);
749 var x199: u64 = undefined;
750 var x200: u1 = undefined;
751 addcarryxU64(&x199, &x200, x198, x172, x190);
752 var x201: u64 = undefined;
753 var x202: u1 = undefined;
754 addcarryxU64(&x201, &x202, x200, x174, x192);
755 var x203: u64 = undefined;
756 var x204: u1 = undefined;
757 addcarryxU64(&x203, &x204, x202, x176, x194);
758 const x205 = (@as(u64, x204) + @as(u64, x177));
759 var x206: u64 = undefined;
760 var x207: u1 = undefined;
761 subborrowxU64(&x206, &x207, 0x0, x197, 0xfffffffefffffc2f);
762 var x208: u64 = undefined;
763 var x209: u1 = undefined;
764 subborrowxU64(&x208, &x209, x207, x199, 0xffffffffffffffff);
765 var x210: u64 = undefined;
766 var x211: u1 = undefined;
767 subborrowxU64(&x210, &x211, x209, x201, 0xffffffffffffffff);
768 var x212: u64 = undefined;
769 var x213: u1 = undefined;
770 subborrowxU64(&x212, &x213, x211, x203, 0xffffffffffffffff);
771 var x214: u64 = undefined;
772 var x215: u1 = undefined;
773 subborrowxU64(&x214, &x215, x213, x205, 0x0);
774 var x216: u64 = undefined;
775 cmovznzU64(&x216, x215, x206, x197);
776 var x217: u64 = undefined;
777 cmovznzU64(&x217, x215, x208, x199);
778 var x218: u64 = undefined;
779 cmovznzU64(&x218, x215, x210, x201);
780 var x219: u64 = undefined;
781 cmovznzU64(&x219, x215, x212, x203);
782 out1[0] = x216;
783 out1[1] = x217;
784 out1[2] = x218;
785 out1[3] = x219;
786}
787
788/// The function add adds two field elements in the Montgomery domain.
789///
790/// Preconditions:
791/// 0 ≤ eval arg1 < m
792/// 0 ≤ eval arg2 < m
793/// Postconditions:
794/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
795/// 0 ≤ eval out1 < m
796///
797pub fn add(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
798 @setRuntimeSafety(mode == .debug);
799
800 var x1: u64 = undefined;
801 var x2: u1 = undefined;
802 addcarryxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
803 var x3: u64 = undefined;
804 var x4: u1 = undefined;
805 addcarryxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
806 var x5: u64 = undefined;
807 var x6: u1 = undefined;
808 addcarryxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
809 var x7: u64 = undefined;
810 var x8: u1 = undefined;
811 addcarryxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
812 var x9: u64 = undefined;
813 var x10: u1 = undefined;
814 subborrowxU64(&x9, &x10, 0x0, x1, 0xfffffffefffffc2f);
815 var x11: u64 = undefined;
816 var x12: u1 = undefined;
817 subborrowxU64(&x11, &x12, x10, x3, 0xffffffffffffffff);
818 var x13: u64 = undefined;
819 var x14: u1 = undefined;
820 subborrowxU64(&x13, &x14, x12, x5, 0xffffffffffffffff);
821 var x15: u64 = undefined;
822 var x16: u1 = undefined;
823 subborrowxU64(&x15, &x16, x14, x7, 0xffffffffffffffff);
824 var x17: u64 = undefined;
825 var x18: u1 = undefined;
826 subborrowxU64(&x17, &x18, x16, @as(u64, x8), 0x0);
827 var x19: u64 = undefined;
828 cmovznzU64(&x19, x18, x9, x1);
829 var x20: u64 = undefined;
830 cmovznzU64(&x20, x18, x11, x3);
831 var x21: u64 = undefined;
832 cmovznzU64(&x21, x18, x13, x5);
833 var x22: u64 = undefined;
834 cmovznzU64(&x22, x18, x15, x7);
835 out1[0] = x19;
836 out1[1] = x20;
837 out1[2] = x21;
838 out1[3] = x22;
839}
840
841/// The function sub subtracts two field elements in the Montgomery domain.
842///
843/// Preconditions:
844/// 0 ≤ eval arg1 < m
845/// 0 ≤ eval arg2 < m
846/// Postconditions:
847/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
848/// 0 ≤ eval out1 < m
849///
850pub fn sub(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
851 @setRuntimeSafety(mode == .debug);
852
853 var x1: u64 = undefined;
854 var x2: u1 = undefined;
855 subborrowxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
856 var x3: u64 = undefined;
857 var x4: u1 = undefined;
858 subborrowxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
859 var x5: u64 = undefined;
860 var x6: u1 = undefined;
861 subborrowxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
862 var x7: u64 = undefined;
863 var x8: u1 = undefined;
864 subborrowxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
865 var x9: u64 = undefined;
866 cmovznzU64(&x9, x8, 0x0, 0xffffffffffffffff);
867 var x10: u64 = undefined;
868 var x11: u1 = undefined;
869 addcarryxU64(&x10, &x11, 0x0, x1, (x9 & 0xfffffffefffffc2f));
870 var x12: u64 = undefined;
871 var x13: u1 = undefined;
872 addcarryxU64(&x12, &x13, x11, x3, x9);
873 var x14: u64 = undefined;
874 var x15: u1 = undefined;
875 addcarryxU64(&x14, &x15, x13, x5, x9);
876 var x16: u64 = undefined;
877 var x17: u1 = undefined;
878 addcarryxU64(&x16, &x17, x15, x7, x9);
879 out1[0] = x10;
880 out1[1] = x12;
881 out1[2] = x14;
882 out1[3] = x16;
883}
884
885/// The function opp negates a field element in the Montgomery domain.
886///
887/// Preconditions:
888/// 0 ≤ eval arg1 < m
889/// Postconditions:
890/// eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
891/// 0 ≤ eval out1 < m
892///
893pub fn opp(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
894 @setRuntimeSafety(mode == .debug);
895
896 var x1: u64 = undefined;
897 var x2: u1 = undefined;
898 subborrowxU64(&x1, &x2, 0x0, 0x0, (arg1[0]));
899 var x3: u64 = undefined;
900 var x4: u1 = undefined;
901 subborrowxU64(&x3, &x4, x2, 0x0, (arg1[1]));
902 var x5: u64 = undefined;
903 var x6: u1 = undefined;
904 subborrowxU64(&x5, &x6, x4, 0x0, (arg1[2]));
905 var x7: u64 = undefined;
906 var x8: u1 = undefined;
907 subborrowxU64(&x7, &x8, x6, 0x0, (arg1[3]));
908 var x9: u64 = undefined;
909 cmovznzU64(&x9, x8, 0x0, 0xffffffffffffffff);
910 var x10: u64 = undefined;
911 var x11: u1 = undefined;
912 addcarryxU64(&x10, &x11, 0x0, x1, (x9 & 0xfffffffefffffc2f));
913 var x12: u64 = undefined;
914 var x13: u1 = undefined;
915 addcarryxU64(&x12, &x13, x11, x3, x9);
916 var x14: u64 = undefined;
917 var x15: u1 = undefined;
918 addcarryxU64(&x14, &x15, x13, x5, x9);
919 var x16: u64 = undefined;
920 var x17: u1 = undefined;
921 addcarryxU64(&x16, &x17, x15, x7, x9);
922 out1[0] = x10;
923 out1[1] = x12;
924 out1[2] = x14;
925 out1[3] = x16;
926}
927
928/// The function fromMontgomery translates a field element out of the Montgomery domain.
929///
930/// Preconditions:
931/// 0 ≤ eval arg1 < m
932/// Postconditions:
933/// eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
934/// 0 ≤ eval out1 < m
935///
936pub fn fromMontgomery(out1: *NonMontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
937 @setRuntimeSafety(mode == .debug);
938
939 const x1 = (arg1[0]);
940 var x2: u64 = undefined;
941 var x3: u64 = undefined;
942 mulxU64(&x2, &x3, x1, 0xd838091dd2253531);
943 var x4: u64 = undefined;
944 var x5: u64 = undefined;
945 mulxU64(&x4, &x5, x2, 0xffffffffffffffff);
946 var x6: u64 = undefined;
947 var x7: u64 = undefined;
948 mulxU64(&x6, &x7, x2, 0xffffffffffffffff);
949 var x8: u64 = undefined;
950 var x9: u64 = undefined;
951 mulxU64(&x8, &x9, x2, 0xffffffffffffffff);
952 var x10: u64 = undefined;
953 var x11: u64 = undefined;
954 mulxU64(&x10, &x11, x2, 0xfffffffefffffc2f);
955 var x12: u64 = undefined;
956 var x13: u1 = undefined;
957 addcarryxU64(&x12, &x13, 0x0, x11, x8);
958 var x14: u64 = undefined;
959 var x15: u1 = undefined;
960 addcarryxU64(&x14, &x15, x13, x9, x6);
961 var x16: u64 = undefined;
962 var x17: u1 = undefined;
963 addcarryxU64(&x16, &x17, x15, x7, x4);
964 var x18: u64 = undefined;
965 var x19: u1 = undefined;
966 addcarryxU64(&x18, &x19, 0x0, x1, x10);
967 var x20: u64 = undefined;
968 var x21: u1 = undefined;
969 addcarryxU64(&x20, &x21, x19, 0x0, x12);
970 var x22: u64 = undefined;
971 var x23: u1 = undefined;
972 addcarryxU64(&x22, &x23, x21, 0x0, x14);
973 var x24: u64 = undefined;
974 var x25: u1 = undefined;
975 addcarryxU64(&x24, &x25, x23, 0x0, x16);
976 var x26: u64 = undefined;
977 var x27: u1 = undefined;
978 addcarryxU64(&x26, &x27, x25, 0x0, (@as(u64, x17) + x5));
979 var x28: u64 = undefined;
980 var x29: u1 = undefined;
981 addcarryxU64(&x28, &x29, 0x0, x20, (arg1[1]));
982 var x30: u64 = undefined;
983 var x31: u1 = undefined;
984 addcarryxU64(&x30, &x31, x29, x22, 0x0);
985 var x32: u64 = undefined;
986 var x33: u1 = undefined;
987 addcarryxU64(&x32, &x33, x31, x24, 0x0);
988 var x34: u64 = undefined;
989 var x35: u1 = undefined;
990 addcarryxU64(&x34, &x35, x33, x26, 0x0);
991 var x36: u64 = undefined;
992 var x37: u64 = undefined;
993 mulxU64(&x36, &x37, x28, 0xd838091dd2253531);
994 var x38: u64 = undefined;
995 var x39: u64 = undefined;
996 mulxU64(&x38, &x39, x36, 0xffffffffffffffff);
997 var x40: u64 = undefined;
998 var x41: u64 = undefined;
999 mulxU64(&x40, &x41, x36, 0xffffffffffffffff);
1000 var x42: u64 = undefined;
1001 var x43: u64 = undefined;
1002 mulxU64(&x42, &x43, x36, 0xffffffffffffffff);
1003 var x44: u64 = undefined;
1004 var x45: u64 = undefined;
1005 mulxU64(&x44, &x45, x36, 0xfffffffefffffc2f);
1006 var x46: u64 = undefined;
1007 var x47: u1 = undefined;
1008 addcarryxU64(&x46, &x47, 0x0, x45, x42);
1009 var x48: u64 = undefined;
1010 var x49: u1 = undefined;
1011 addcarryxU64(&x48, &x49, x47, x43, x40);
1012 var x50: u64 = undefined;
1013 var x51: u1 = undefined;
1014 addcarryxU64(&x50, &x51, x49, x41, x38);
1015 var x52: u64 = undefined;
1016 var x53: u1 = undefined;
1017 addcarryxU64(&x52, &x53, 0x0, x28, x44);
1018 var x54: u64 = undefined;
1019 var x55: u1 = undefined;
1020 addcarryxU64(&x54, &x55, x53, x30, x46);
1021 var x56: u64 = undefined;
1022 var x57: u1 = undefined;
1023 addcarryxU64(&x56, &x57, x55, x32, x48);
1024 var x58: u64 = undefined;
1025 var x59: u1 = undefined;
1026 addcarryxU64(&x58, &x59, x57, x34, x50);
1027 var x60: u64 = undefined;
1028 var x61: u1 = undefined;
1029 addcarryxU64(&x60, &x61, x59, (@as(u64, x35) + @as(u64, x27)), (@as(u64, x51) + x39));
1030 var x62: u64 = undefined;
1031 var x63: u1 = undefined;
1032 addcarryxU64(&x62, &x63, 0x0, x54, (arg1[2]));
1033 var x64: u64 = undefined;
1034 var x65: u1 = undefined;
1035 addcarryxU64(&x64, &x65, x63, x56, 0x0);
1036 var x66: u64 = undefined;
1037 var x67: u1 = undefined;
1038 addcarryxU64(&x66, &x67, x65, x58, 0x0);
1039 var x68: u64 = undefined;
1040 var x69: u1 = undefined;
1041 addcarryxU64(&x68, &x69, x67, x60, 0x0);
1042 var x70: u64 = undefined;
1043 var x71: u64 = undefined;
1044 mulxU64(&x70, &x71, x62, 0xd838091dd2253531);
1045 var x72: u64 = undefined;
1046 var x73: u64 = undefined;
1047 mulxU64(&x72, &x73, x70, 0xffffffffffffffff);
1048 var x74: u64 = undefined;
1049 var x75: u64 = undefined;
1050 mulxU64(&x74, &x75, x70, 0xffffffffffffffff);
1051 var x76: u64 = undefined;
1052 var x77: u64 = undefined;
1053 mulxU64(&x76, &x77, x70, 0xffffffffffffffff);
1054 var x78: u64 = undefined;
1055 var x79: u64 = undefined;
1056 mulxU64(&x78, &x79, x70, 0xfffffffefffffc2f);
1057 var x80: u64 = undefined;
1058 var x81: u1 = undefined;
1059 addcarryxU64(&x80, &x81, 0x0, x79, x76);
1060 var x82: u64 = undefined;
1061 var x83: u1 = undefined;
1062 addcarryxU64(&x82, &x83, x81, x77, x74);
1063 var x84: u64 = undefined;
1064 var x85: u1 = undefined;
1065 addcarryxU64(&x84, &x85, x83, x75, x72);
1066 var x86: u64 = undefined;
1067 var x87: u1 = undefined;
1068 addcarryxU64(&x86, &x87, 0x0, x62, x78);
1069 var x88: u64 = undefined;
1070 var x89: u1 = undefined;
1071 addcarryxU64(&x88, &x89, x87, x64, x80);
1072 var x90: u64 = undefined;
1073 var x91: u1 = undefined;
1074 addcarryxU64(&x90, &x91, x89, x66, x82);
1075 var x92: u64 = undefined;
1076 var x93: u1 = undefined;
1077 addcarryxU64(&x92, &x93, x91, x68, x84);
1078 var x94: u64 = undefined;
1079 var x95: u1 = undefined;
1080 addcarryxU64(&x94, &x95, x93, (@as(u64, x69) + @as(u64, x61)), (@as(u64, x85) + x73));
1081 var x96: u64 = undefined;
1082 var x97: u1 = undefined;
1083 addcarryxU64(&x96, &x97, 0x0, x88, (arg1[3]));
1084 var x98: u64 = undefined;
1085 var x99: u1 = undefined;
1086 addcarryxU64(&x98, &x99, x97, x90, 0x0);
1087 var x100: u64 = undefined;
1088 var x101: u1 = undefined;
1089 addcarryxU64(&x100, &x101, x99, x92, 0x0);
1090 var x102: u64 = undefined;
1091 var x103: u1 = undefined;
1092 addcarryxU64(&x102, &x103, x101, x94, 0x0);
1093 var x104: u64 = undefined;
1094 var x105: u64 = undefined;
1095 mulxU64(&x104, &x105, x96, 0xd838091dd2253531);
1096 var x106: u64 = undefined;
1097 var x107: u64 = undefined;
1098 mulxU64(&x106, &x107, x104, 0xffffffffffffffff);
1099 var x108: u64 = undefined;
1100 var x109: u64 = undefined;
1101 mulxU64(&x108, &x109, x104, 0xffffffffffffffff);
1102 var x110: u64 = undefined;
1103 var x111: u64 = undefined;
1104 mulxU64(&x110, &x111, x104, 0xffffffffffffffff);
1105 var x112: u64 = undefined;
1106 var x113: u64 = undefined;
1107 mulxU64(&x112, &x113, x104, 0xfffffffefffffc2f);
1108 var x114: u64 = undefined;
1109 var x115: u1 = undefined;
1110 addcarryxU64(&x114, &x115, 0x0, x113, x110);
1111 var x116: u64 = undefined;
1112 var x117: u1 = undefined;
1113 addcarryxU64(&x116, &x117, x115, x111, x108);
1114 var x118: u64 = undefined;
1115 var x119: u1 = undefined;
1116 addcarryxU64(&x118, &x119, x117, x109, x106);
1117 var x120: u64 = undefined;
1118 var x121: u1 = undefined;
1119 addcarryxU64(&x120, &x121, 0x0, x96, x112);
1120 var x122: u64 = undefined;
1121 var x123: u1 = undefined;
1122 addcarryxU64(&x122, &x123, x121, x98, x114);
1123 var x124: u64 = undefined;
1124 var x125: u1 = undefined;
1125 addcarryxU64(&x124, &x125, x123, x100, x116);
1126 var x126: u64 = undefined;
1127 var x127: u1 = undefined;
1128 addcarryxU64(&x126, &x127, x125, x102, x118);
1129 var x128: u64 = undefined;
1130 var x129: u1 = undefined;
1131 addcarryxU64(&x128, &x129, x127, (@as(u64, x103) + @as(u64, x95)), (@as(u64, x119) + x107));
1132 var x130: u64 = undefined;
1133 var x131: u1 = undefined;
1134 subborrowxU64(&x130, &x131, 0x0, x122, 0xfffffffefffffc2f);
1135 var x132: u64 = undefined;
1136 var x133: u1 = undefined;
1137 subborrowxU64(&x132, &x133, x131, x124, 0xffffffffffffffff);
1138 var x134: u64 = undefined;
1139 var x135: u1 = undefined;
1140 subborrowxU64(&x134, &x135, x133, x126, 0xffffffffffffffff);
1141 var x136: u64 = undefined;
1142 var x137: u1 = undefined;
1143 subborrowxU64(&x136, &x137, x135, x128, 0xffffffffffffffff);
1144 var x138: u64 = undefined;
1145 var x139: u1 = undefined;
1146 subborrowxU64(&x138, &x139, x137, @as(u64, x129), 0x0);
1147 var x140: u64 = undefined;
1148 cmovznzU64(&x140, x139, x130, x122);
1149 var x141: u64 = undefined;
1150 cmovznzU64(&x141, x139, x132, x124);
1151 var x142: u64 = undefined;
1152 cmovznzU64(&x142, x139, x134, x126);
1153 var x143: u64 = undefined;
1154 cmovznzU64(&x143, x139, x136, x128);
1155 out1[0] = x140;
1156 out1[1] = x141;
1157 out1[2] = x142;
1158 out1[3] = x143;
1159}
1160
1161/// The function toMontgomery translates a field element into the Montgomery domain.
1162///
1163/// Preconditions:
1164/// 0 ≤ eval arg1 < m
1165/// Postconditions:
1166/// eval (from_montgomery out1) mod m = eval arg1 mod m
1167/// 0 ≤ eval out1 < m
1168///
1169pub fn toMontgomery(out1: *MontgomeryDomainFieldElement, arg1: NonMontgomeryDomainFieldElement) void {
1170 @setRuntimeSafety(mode == .debug);
1171
1172 const x1 = (arg1[1]);
1173 const x2 = (arg1[2]);
1174 const x3 = (arg1[3]);
1175 const x4 = (arg1[0]);
1176 var x5: u64 = undefined;
1177 var x6: u64 = undefined;
1178 mulxU64(&x5, &x6, x4, 0x7a2000e90a1);
1179 var x7: u64 = undefined;
1180 var x8: u1 = undefined;
1181 addcarryxU64(&x7, &x8, 0x0, x6, x4);
1182 var x9: u64 = undefined;
1183 var x10: u64 = undefined;
1184 mulxU64(&x9, &x10, x5, 0xd838091dd2253531);
1185 var x11: u64 = undefined;
1186 var x12: u64 = undefined;
1187 mulxU64(&x11, &x12, x9, 0xffffffffffffffff);
1188 var x13: u64 = undefined;
1189 var x14: u64 = undefined;
1190 mulxU64(&x13, &x14, x9, 0xffffffffffffffff);
1191 var x15: u64 = undefined;
1192 var x16: u64 = undefined;
1193 mulxU64(&x15, &x16, x9, 0xffffffffffffffff);
1194 var x17: u64 = undefined;
1195 var x18: u64 = undefined;
1196 mulxU64(&x17, &x18, x9, 0xfffffffefffffc2f);
1197 var x19: u64 = undefined;
1198 var x20: u1 = undefined;
1199 addcarryxU64(&x19, &x20, 0x0, x18, x15);
1200 var x21: u64 = undefined;
1201 var x22: u1 = undefined;
1202 addcarryxU64(&x21, &x22, x20, x16, x13);
1203 var x23: u64 = undefined;
1204 var x24: u1 = undefined;
1205 addcarryxU64(&x23, &x24, x22, x14, x11);
1206 var x25: u64 = undefined;
1207 var x26: u1 = undefined;
1208 addcarryxU64(&x25, &x26, 0x0, x5, x17);
1209 var x27: u64 = undefined;
1210 var x28: u1 = undefined;
1211 addcarryxU64(&x27, &x28, x26, x7, x19);
1212 var x29: u64 = undefined;
1213 var x30: u1 = undefined;
1214 addcarryxU64(&x29, &x30, x28, @as(u64, x8), x21);
1215 var x31: u64 = undefined;
1216 var x32: u1 = undefined;
1217 addcarryxU64(&x31, &x32, x30, 0x0, x23);
1218 var x33: u64 = undefined;
1219 var x34: u1 = undefined;
1220 addcarryxU64(&x33, &x34, x32, 0x0, (@as(u64, x24) + x12));
1221 var x35: u64 = undefined;
1222 var x36: u64 = undefined;
1223 mulxU64(&x35, &x36, x1, 0x7a2000e90a1);
1224 var x37: u64 = undefined;
1225 var x38: u1 = undefined;
1226 addcarryxU64(&x37, &x38, 0x0, x36, x1);
1227 var x39: u64 = undefined;
1228 var x40: u1 = undefined;
1229 addcarryxU64(&x39, &x40, 0x0, x27, x35);
1230 var x41: u64 = undefined;
1231 var x42: u1 = undefined;
1232 addcarryxU64(&x41, &x42, x40, x29, x37);
1233 var x43: u64 = undefined;
1234 var x44: u1 = undefined;
1235 addcarryxU64(&x43, &x44, x42, x31, @as(u64, x38));
1236 var x45: u64 = undefined;
1237 var x46: u1 = undefined;
1238 addcarryxU64(&x45, &x46, x44, x33, 0x0);
1239 var x47: u64 = undefined;
1240 var x48: u64 = undefined;
1241 mulxU64(&x47, &x48, x39, 0xd838091dd2253531);
1242 var x49: u64 = undefined;
1243 var x50: u64 = undefined;
1244 mulxU64(&x49, &x50, x47, 0xffffffffffffffff);
1245 var x51: u64 = undefined;
1246 var x52: u64 = undefined;
1247 mulxU64(&x51, &x52, x47, 0xffffffffffffffff);
1248 var x53: u64 = undefined;
1249 var x54: u64 = undefined;
1250 mulxU64(&x53, &x54, x47, 0xffffffffffffffff);
1251 var x55: u64 = undefined;
1252 var x56: u64 = undefined;
1253 mulxU64(&x55, &x56, x47, 0xfffffffefffffc2f);
1254 var x57: u64 = undefined;
1255 var x58: u1 = undefined;
1256 addcarryxU64(&x57, &x58, 0x0, x56, x53);
1257 var x59: u64 = undefined;
1258 var x60: u1 = undefined;
1259 addcarryxU64(&x59, &x60, x58, x54, x51);
1260 var x61: u64 = undefined;
1261 var x62: u1 = undefined;
1262 addcarryxU64(&x61, &x62, x60, x52, x49);
1263 var x63: u64 = undefined;
1264 var x64: u1 = undefined;
1265 addcarryxU64(&x63, &x64, 0x0, x39, x55);
1266 var x65: u64 = undefined;
1267 var x66: u1 = undefined;
1268 addcarryxU64(&x65, &x66, x64, x41, x57);
1269 var x67: u64 = undefined;
1270 var x68: u1 = undefined;
1271 addcarryxU64(&x67, &x68, x66, x43, x59);
1272 var x69: u64 = undefined;
1273 var x70: u1 = undefined;
1274 addcarryxU64(&x69, &x70, x68, x45, x61);
1275 var x71: u64 = undefined;
1276 var x72: u1 = undefined;
1277 addcarryxU64(&x71, &x72, x70, (@as(u64, x46) + @as(u64, x34)), (@as(u64, x62) + x50));
1278 var x73: u64 = undefined;
1279 var x74: u64 = undefined;
1280 mulxU64(&x73, &x74, x2, 0x7a2000e90a1);
1281 var x75: u64 = undefined;
1282 var x76: u1 = undefined;
1283 addcarryxU64(&x75, &x76, 0x0, x74, x2);
1284 var x77: u64 = undefined;
1285 var x78: u1 = undefined;
1286 addcarryxU64(&x77, &x78, 0x0, x65, x73);
1287 var x79: u64 = undefined;
1288 var x80: u1 = undefined;
1289 addcarryxU64(&x79, &x80, x78, x67, x75);
1290 var x81: u64 = undefined;
1291 var x82: u1 = undefined;
1292 addcarryxU64(&x81, &x82, x80, x69, @as(u64, x76));
1293 var x83: u64 = undefined;
1294 var x84: u1 = undefined;
1295 addcarryxU64(&x83, &x84, x82, x71, 0x0);
1296 var x85: u64 = undefined;
1297 var x86: u64 = undefined;
1298 mulxU64(&x85, &x86, x77, 0xd838091dd2253531);
1299 var x87: u64 = undefined;
1300 var x88: u64 = undefined;
1301 mulxU64(&x87, &x88, x85, 0xffffffffffffffff);
1302 var x89: u64 = undefined;
1303 var x90: u64 = undefined;
1304 mulxU64(&x89, &x90, x85, 0xffffffffffffffff);
1305 var x91: u64 = undefined;
1306 var x92: u64 = undefined;
1307 mulxU64(&x91, &x92, x85, 0xffffffffffffffff);
1308 var x93: u64 = undefined;
1309 var x94: u64 = undefined;
1310 mulxU64(&x93, &x94, x85, 0xfffffffefffffc2f);
1311 var x95: u64 = undefined;
1312 var x96: u1 = undefined;
1313 addcarryxU64(&x95, &x96, 0x0, x94, x91);
1314 var x97: u64 = undefined;
1315 var x98: u1 = undefined;
1316 addcarryxU64(&x97, &x98, x96, x92, x89);
1317 var x99: u64 = undefined;
1318 var x100: u1 = undefined;
1319 addcarryxU64(&x99, &x100, x98, x90, x87);
1320 var x101: u64 = undefined;
1321 var x102: u1 = undefined;
1322 addcarryxU64(&x101, &x102, 0x0, x77, x93);
1323 var x103: u64 = undefined;
1324 var x104: u1 = undefined;
1325 addcarryxU64(&x103, &x104, x102, x79, x95);
1326 var x105: u64 = undefined;
1327 var x106: u1 = undefined;
1328 addcarryxU64(&x105, &x106, x104, x81, x97);
1329 var x107: u64 = undefined;
1330 var x108: u1 = undefined;
1331 addcarryxU64(&x107, &x108, x106, x83, x99);
1332 var x109: u64 = undefined;
1333 var x110: u1 = undefined;
1334 addcarryxU64(&x109, &x110, x108, (@as(u64, x84) + @as(u64, x72)), (@as(u64, x100) + x88));
1335 var x111: u64 = undefined;
1336 var x112: u64 = undefined;
1337 mulxU64(&x111, &x112, x3, 0x7a2000e90a1);
1338 var x113: u64 = undefined;
1339 var x114: u1 = undefined;
1340 addcarryxU64(&x113, &x114, 0x0, x112, x3);
1341 var x115: u64 = undefined;
1342 var x116: u1 = undefined;
1343 addcarryxU64(&x115, &x116, 0x0, x103, x111);
1344 var x117: u64 = undefined;
1345 var x118: u1 = undefined;
1346 addcarryxU64(&x117, &x118, x116, x105, x113);
1347 var x119: u64 = undefined;
1348 var x120: u1 = undefined;
1349 addcarryxU64(&x119, &x120, x118, x107, @as(u64, x114));
1350 var x121: u64 = undefined;
1351 var x122: u1 = undefined;
1352 addcarryxU64(&x121, &x122, x120, x109, 0x0);
1353 var x123: u64 = undefined;
1354 var x124: u64 = undefined;
1355 mulxU64(&x123, &x124, x115, 0xd838091dd2253531);
1356 var x125: u64 = undefined;
1357 var x126: u64 = undefined;
1358 mulxU64(&x125, &x126, x123, 0xffffffffffffffff);
1359 var x127: u64 = undefined;
1360 var x128: u64 = undefined;
1361 mulxU64(&x127, &x128, x123, 0xffffffffffffffff);
1362 var x129: u64 = undefined;
1363 var x130: u64 = undefined;
1364 mulxU64(&x129, &x130, x123, 0xffffffffffffffff);
1365 var x131: u64 = undefined;
1366 var x132: u64 = undefined;
1367 mulxU64(&x131, &x132, x123, 0xfffffffefffffc2f);
1368 var x133: u64 = undefined;
1369 var x134: u1 = undefined;
1370 addcarryxU64(&x133, &x134, 0x0, x132, x129);
1371 var x135: u64 = undefined;
1372 var x136: u1 = undefined;
1373 addcarryxU64(&x135, &x136, x134, x130, x127);
1374 var x137: u64 = undefined;
1375 var x138: u1 = undefined;
1376 addcarryxU64(&x137, &x138, x136, x128, x125);
1377 var x139: u64 = undefined;
1378 var x140: u1 = undefined;
1379 addcarryxU64(&x139, &x140, 0x0, x115, x131);
1380 var x141: u64 = undefined;
1381 var x142: u1 = undefined;
1382 addcarryxU64(&x141, &x142, x140, x117, x133);
1383 var x143: u64 = undefined;
1384 var x144: u1 = undefined;
1385 addcarryxU64(&x143, &x144, x142, x119, x135);
1386 var x145: u64 = undefined;
1387 var x146: u1 = undefined;
1388 addcarryxU64(&x145, &x146, x144, x121, x137);
1389 var x147: u64 = undefined;
1390 var x148: u1 = undefined;
1391 addcarryxU64(&x147, &x148, x146, (@as(u64, x122) + @as(u64, x110)), (@as(u64, x138) + x126));
1392 var x149: u64 = undefined;
1393 var x150: u1 = undefined;
1394 subborrowxU64(&x149, &x150, 0x0, x141, 0xfffffffefffffc2f);
1395 var x151: u64 = undefined;
1396 var x152: u1 = undefined;
1397 subborrowxU64(&x151, &x152, x150, x143, 0xffffffffffffffff);
1398 var x153: u64 = undefined;
1399 var x154: u1 = undefined;
1400 subborrowxU64(&x153, &x154, x152, x145, 0xffffffffffffffff);
1401 var x155: u64 = undefined;
1402 var x156: u1 = undefined;
1403 subborrowxU64(&x155, &x156, x154, x147, 0xffffffffffffffff);
1404 var x157: u64 = undefined;
1405 var x158: u1 = undefined;
1406 subborrowxU64(&x157, &x158, x156, @as(u64, x148), 0x0);
1407 var x159: u64 = undefined;
1408 cmovznzU64(&x159, x158, x149, x141);
1409 var x160: u64 = undefined;
1410 cmovznzU64(&x160, x158, x151, x143);
1411 var x161: u64 = undefined;
1412 cmovznzU64(&x161, x158, x153, x145);
1413 var x162: u64 = undefined;
1414 cmovznzU64(&x162, x158, x155, x147);
1415 out1[0] = x159;
1416 out1[1] = x160;
1417 out1[2] = x161;
1418 out1[3] = x162;
1419}
1420
1421/// The function nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
1422///
1423/// Preconditions:
1424/// 0 ≤ eval arg1 < m
1425/// Postconditions:
1426/// out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
1427///
1428/// Input Bounds:
1429/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1430/// Output Bounds:
1431/// out1: [0x0 ~> 0xffffffffffffffff]
1432pub fn nonzero(out1: *u64, arg1: [4]u64) void {
1433 @setRuntimeSafety(mode == .debug);
1434
1435 const x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | (arg1[3]))));
1436 out1.* = x1;
1437}
1438
1439/// The function selectznz is a multi-limb conditional select.
1440///
1441/// Postconditions:
1442/// out1 = (if arg1 = 0 then arg2 else arg3)
1443///
1444/// Input Bounds:
1445/// arg1: [0x0 ~> 0x1]
1446/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1447/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1448/// Output Bounds:
1449/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1450pub fn selectznz(out1: *[4]u64, arg1: u1, arg2: [4]u64, arg3: [4]u64) void {
1451 @setRuntimeSafety(mode == .debug);
1452
1453 var x1: u64 = undefined;
1454 cmovznzU64(&x1, arg1, (arg2[0]), (arg3[0]));
1455 var x2: u64 = undefined;
1456 cmovznzU64(&x2, arg1, (arg2[1]), (arg3[1]));
1457 var x3: u64 = undefined;
1458 cmovznzU64(&x3, arg1, (arg2[2]), (arg3[2]));
1459 var x4: u64 = undefined;
1460 cmovznzU64(&x4, arg1, (arg2[3]), (arg3[3]));
1461 out1[0] = x1;
1462 out1[1] = x2;
1463 out1[2] = x3;
1464 out1[3] = x4;
1465}
1466
1467/// The function toBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
1468///
1469/// Preconditions:
1470/// 0 ≤ eval arg1 < m
1471/// Postconditions:
1472/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
1473///
1474/// Input Bounds:
1475/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1476/// Output Bounds:
1477/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
1478pub fn toBytes(out1: *[32]u8, arg1: [4]u64) void {
1479 @setRuntimeSafety(mode == .debug);
1480
1481 const x1 = (arg1[3]);
1482 const x2 = (arg1[2]);
1483 const x3 = (arg1[1]);
1484 const x4 = (arg1[0]);
1485 const x5 = @as(u8, @truncate((x4 & 0xff)));
1486 const x6 = (x4 >> 8);
1487 const x7 = @as(u8, @truncate((x6 & 0xff)));
1488 const x8 = (x6 >> 8);
1489 const x9 = @as(u8, @truncate((x8 & 0xff)));
1490 const x10 = (x8 >> 8);
1491 const x11 = @as(u8, @truncate((x10 & 0xff)));
1492 const x12 = (x10 >> 8);
1493 const x13 = @as(u8, @truncate((x12 & 0xff)));
1494 const x14 = (x12 >> 8);
1495 const x15 = @as(u8, @truncate((x14 & 0xff)));
1496 const x16 = (x14 >> 8);
1497 const x17 = @as(u8, @truncate((x16 & 0xff)));
1498 const x18 = @as(u8, @truncate((x16 >> 8)));
1499 const x19 = @as(u8, @truncate((x3 & 0xff)));
1500 const x20 = (x3 >> 8);
1501 const x21 = @as(u8, @truncate((x20 & 0xff)));
1502 const x22 = (x20 >> 8);
1503 const x23 = @as(u8, @truncate((x22 & 0xff)));
1504 const x24 = (x22 >> 8);
1505 const x25 = @as(u8, @truncate((x24 & 0xff)));
1506 const x26 = (x24 >> 8);
1507 const x27 = @as(u8, @truncate((x26 & 0xff)));
1508 const x28 = (x26 >> 8);
1509 const x29 = @as(u8, @truncate((x28 & 0xff)));
1510 const x30 = (x28 >> 8);
1511 const x31 = @as(u8, @truncate((x30 & 0xff)));
1512 const x32 = @as(u8, @truncate((x30 >> 8)));
1513 const x33 = @as(u8, @truncate((x2 & 0xff)));
1514 const x34 = (x2 >> 8);
1515 const x35 = @as(u8, @truncate((x34 & 0xff)));
1516 const x36 = (x34 >> 8);
1517 const x37 = @as(u8, @truncate((x36 & 0xff)));
1518 const x38 = (x36 >> 8);
1519 const x39 = @as(u8, @truncate((x38 & 0xff)));
1520 const x40 = (x38 >> 8);
1521 const x41 = @as(u8, @truncate((x40 & 0xff)));
1522 const x42 = (x40 >> 8);
1523 const x43 = @as(u8, @truncate((x42 & 0xff)));
1524 const x44 = (x42 >> 8);
1525 const x45 = @as(u8, @truncate((x44 & 0xff)));
1526 const x46 = @as(u8, @truncate((x44 >> 8)));
1527 const x47 = @as(u8, @truncate((x1 & 0xff)));
1528 const x48 = (x1 >> 8);
1529 const x49 = @as(u8, @truncate((x48 & 0xff)));
1530 const x50 = (x48 >> 8);
1531 const x51 = @as(u8, @truncate((x50 & 0xff)));
1532 const x52 = (x50 >> 8);
1533 const x53 = @as(u8, @truncate((x52 & 0xff)));
1534 const x54 = (x52 >> 8);
1535 const x55 = @as(u8, @truncate((x54 & 0xff)));
1536 const x56 = (x54 >> 8);
1537 const x57 = @as(u8, @truncate((x56 & 0xff)));
1538 const x58 = (x56 >> 8);
1539 const x59 = @as(u8, @truncate((x58 & 0xff)));
1540 const x60 = @as(u8, @truncate((x58 >> 8)));
1541 out1[0] = x5;
1542 out1[1] = x7;
1543 out1[2] = x9;
1544 out1[3] = x11;
1545 out1[4] = x13;
1546 out1[5] = x15;
1547 out1[6] = x17;
1548 out1[7] = x18;
1549 out1[8] = x19;
1550 out1[9] = x21;
1551 out1[10] = x23;
1552 out1[11] = x25;
1553 out1[12] = x27;
1554 out1[13] = x29;
1555 out1[14] = x31;
1556 out1[15] = x32;
1557 out1[16] = x33;
1558 out1[17] = x35;
1559 out1[18] = x37;
1560 out1[19] = x39;
1561 out1[20] = x41;
1562 out1[21] = x43;
1563 out1[22] = x45;
1564 out1[23] = x46;
1565 out1[24] = x47;
1566 out1[25] = x49;
1567 out1[26] = x51;
1568 out1[27] = x53;
1569 out1[28] = x55;
1570 out1[29] = x57;
1571 out1[30] = x59;
1572 out1[31] = x60;
1573}
1574
1575/// The function fromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
1576///
1577/// Preconditions:
1578/// 0 ≤ bytes_eval arg1 < m
1579/// Postconditions:
1580/// eval out1 mod m = bytes_eval arg1 mod m
1581/// 0 ≤ eval out1 < m
1582///
1583/// Input Bounds:
1584/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
1585/// Output Bounds:
1586/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1587pub fn fromBytes(out1: *[4]u64, arg1: [32]u8) void {
1588 @setRuntimeSafety(mode == .debug);
1589
1590 const x1 = (@as(u64, (arg1[31])) << 56);
1591 const x2 = (@as(u64, (arg1[30])) << 48);
1592 const x3 = (@as(u64, (arg1[29])) << 40);
1593 const x4 = (@as(u64, (arg1[28])) << 32);
1594 const x5 = (@as(u64, (arg1[27])) << 24);
1595 const x6 = (@as(u64, (arg1[26])) << 16);
1596 const x7 = (@as(u64, (arg1[25])) << 8);
1597 const x8 = (arg1[24]);
1598 const x9 = (@as(u64, (arg1[23])) << 56);
1599 const x10 = (@as(u64, (arg1[22])) << 48);
1600 const x11 = (@as(u64, (arg1[21])) << 40);
1601 const x12 = (@as(u64, (arg1[20])) << 32);
1602 const x13 = (@as(u64, (arg1[19])) << 24);
1603 const x14 = (@as(u64, (arg1[18])) << 16);
1604 const x15 = (@as(u64, (arg1[17])) << 8);
1605 const x16 = (arg1[16]);
1606 const x17 = (@as(u64, (arg1[15])) << 56);
1607 const x18 = (@as(u64, (arg1[14])) << 48);
1608 const x19 = (@as(u64, (arg1[13])) << 40);
1609 const x20 = (@as(u64, (arg1[12])) << 32);
1610 const x21 = (@as(u64, (arg1[11])) << 24);
1611 const x22 = (@as(u64, (arg1[10])) << 16);
1612 const x23 = (@as(u64, (arg1[9])) << 8);
1613 const x24 = (arg1[8]);
1614 const x25 = (@as(u64, (arg1[7])) << 56);
1615 const x26 = (@as(u64, (arg1[6])) << 48);
1616 const x27 = (@as(u64, (arg1[5])) << 40);
1617 const x28 = (@as(u64, (arg1[4])) << 32);
1618 const x29 = (@as(u64, (arg1[3])) << 24);
1619 const x30 = (@as(u64, (arg1[2])) << 16);
1620 const x31 = (@as(u64, (arg1[1])) << 8);
1621 const x32 = (arg1[0]);
1622 const x33 = (x31 + @as(u64, x32));
1623 const x34 = (x30 + x33);
1624 const x35 = (x29 + x34);
1625 const x36 = (x28 + x35);
1626 const x37 = (x27 + x36);
1627 const x38 = (x26 + x37);
1628 const x39 = (x25 + x38);
1629 const x40 = (x23 + @as(u64, x24));
1630 const x41 = (x22 + x40);
1631 const x42 = (x21 + x41);
1632 const x43 = (x20 + x42);
1633 const x44 = (x19 + x43);
1634 const x45 = (x18 + x44);
1635 const x46 = (x17 + x45);
1636 const x47 = (x15 + @as(u64, x16));
1637 const x48 = (x14 + x47);
1638 const x49 = (x13 + x48);
1639 const x50 = (x12 + x49);
1640 const x51 = (x11 + x50);
1641 const x52 = (x10 + x51);
1642 const x53 = (x9 + x52);
1643 const x54 = (x7 + @as(u64, x8));
1644 const x55 = (x6 + x54);
1645 const x56 = (x5 + x55);
1646 const x57 = (x4 + x56);
1647 const x58 = (x3 + x57);
1648 const x59 = (x2 + x58);
1649 const x60 = (x1 + x59);
1650 out1[0] = x39;
1651 out1[1] = x46;
1652 out1[2] = x53;
1653 out1[3] = x60;
1654}
1655
1656/// The function setOne returns the field element one in the Montgomery domain.
1657///
1658/// Postconditions:
1659/// eval (from_montgomery out1) mod m = 1 mod m
1660/// 0 ≤ eval out1 < m
1661///
1662pub fn setOne(out1: *MontgomeryDomainFieldElement) void {
1663 @setRuntimeSafety(mode == .debug);
1664
1665 out1[0] = 0x1000003d1;
1666 out1[1] = 0x0;
1667 out1[2] = 0x0;
1668 out1[3] = 0x0;
1669}
1670
1671/// The function msat returns the saturated representation of the prime modulus.
1672///
1673/// Postconditions:
1674/// twos_complement_eval out1 = m
1675/// 0 ≤ eval out1 < m
1676///
1677/// Output Bounds:
1678/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1679pub fn msat(out1: *[5]u64) void {
1680 @setRuntimeSafety(mode == .debug);
1681
1682 out1[0] = 0xfffffffefffffc2f;
1683 out1[1] = 0xffffffffffffffff;
1684 out1[2] = 0xffffffffffffffff;
1685 out1[3] = 0xffffffffffffffff;
1686 out1[4] = 0x0;
1687}
1688
1689/// The function divstep computes a divstep.
1690///
1691/// Preconditions:
1692/// 0 ≤ eval arg4 < m
1693/// 0 ≤ eval arg5 < m
1694/// Postconditions:
1695/// out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
1696/// twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
1697/// twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)
1698/// eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)
1699/// eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)
1700/// 0 ≤ eval out5 < m
1701/// 0 ≤ eval out5 < m
1702/// 0 ≤ eval out2 < m
1703/// 0 ≤ eval out3 < m
1704///
1705/// Input Bounds:
1706/// arg1: [0x0 ~> 0xffffffffffffffff]
1707/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1708/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1709/// arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1710/// arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1711/// Output Bounds:
1712/// out1: [0x0 ~> 0xffffffffffffffff]
1713/// out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1714/// out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1715/// out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1716/// out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1717pub fn divstep(out1: *u64, out2: *[5]u64, out3: *[5]u64, out4: *[4]u64, out5: *[4]u64, arg1: u64, arg2: [5]u64, arg3: [5]u64, arg4: [4]u64, arg5: [4]u64) void {
1718 @setRuntimeSafety(mode == .debug);
1719
1720 var x1: u64 = undefined;
1721 var x2: u1 = undefined;
1722 addcarryxU64(&x1, &x2, 0x0, (~arg1), 0x1);
1723 const x3 = (@as(u1, @truncate((x1 >> 63))) & @as(u1, @truncate(((arg3[0]) & 0x1))));
1724 var x4: u64 = undefined;
1725 var x5: u1 = undefined;
1726 addcarryxU64(&x4, &x5, 0x0, (~arg1), 0x1);
1727 var x6: u64 = undefined;
1728 cmovznzU64(&x6, x3, arg1, x4);
1729 var x7: u64 = undefined;
1730 cmovznzU64(&x7, x3, (arg2[0]), (arg3[0]));
1731 var x8: u64 = undefined;
1732 cmovznzU64(&x8, x3, (arg2[1]), (arg3[1]));
1733 var x9: u64 = undefined;
1734 cmovznzU64(&x9, x3, (arg2[2]), (arg3[2]));
1735 var x10: u64 = undefined;
1736 cmovznzU64(&x10, x3, (arg2[3]), (arg3[3]));
1737 var x11: u64 = undefined;
1738 cmovznzU64(&x11, x3, (arg2[4]), (arg3[4]));
1739 var x12: u64 = undefined;
1740 var x13: u1 = undefined;
1741 addcarryxU64(&x12, &x13, 0x0, 0x1, (~(arg2[0])));
1742 var x14: u64 = undefined;
1743 var x15: u1 = undefined;
1744 addcarryxU64(&x14, &x15, x13, 0x0, (~(arg2[1])));
1745 var x16: u64 = undefined;
1746 var x17: u1 = undefined;
1747 addcarryxU64(&x16, &x17, x15, 0x0, (~(arg2[2])));
1748 var x18: u64 = undefined;
1749 var x19: u1 = undefined;
1750 addcarryxU64(&x18, &x19, x17, 0x0, (~(arg2[3])));
1751 var x20: u64 = undefined;
1752 var x21: u1 = undefined;
1753 addcarryxU64(&x20, &x21, x19, 0x0, (~(arg2[4])));
1754 var x22: u64 = undefined;
1755 cmovznzU64(&x22, x3, (arg3[0]), x12);
1756 var x23: u64 = undefined;
1757 cmovznzU64(&x23, x3, (arg3[1]), x14);
1758 var x24: u64 = undefined;
1759 cmovznzU64(&x24, x3, (arg3[2]), x16);
1760 var x25: u64 = undefined;
1761 cmovznzU64(&x25, x3, (arg3[3]), x18);
1762 var x26: u64 = undefined;
1763 cmovznzU64(&x26, x3, (arg3[4]), x20);
1764 var x27: u64 = undefined;
1765 cmovznzU64(&x27, x3, (arg4[0]), (arg5[0]));
1766 var x28: u64 = undefined;
1767 cmovznzU64(&x28, x3, (arg4[1]), (arg5[1]));
1768 var x29: u64 = undefined;
1769 cmovznzU64(&x29, x3, (arg4[2]), (arg5[2]));
1770 var x30: u64 = undefined;
1771 cmovznzU64(&x30, x3, (arg4[3]), (arg5[3]));
1772 var x31: u64 = undefined;
1773 var x32: u1 = undefined;
1774 addcarryxU64(&x31, &x32, 0x0, x27, x27);
1775 var x33: u64 = undefined;
1776 var x34: u1 = undefined;
1777 addcarryxU64(&x33, &x34, x32, x28, x28);
1778 var x35: u64 = undefined;
1779 var x36: u1 = undefined;
1780 addcarryxU64(&x35, &x36, x34, x29, x29);
1781 var x37: u64 = undefined;
1782 var x38: u1 = undefined;
1783 addcarryxU64(&x37, &x38, x36, x30, x30);
1784 var x39: u64 = undefined;
1785 var x40: u1 = undefined;
1786 subborrowxU64(&x39, &x40, 0x0, x31, 0xfffffffefffffc2f);
1787 var x41: u64 = undefined;
1788 var x42: u1 = undefined;
1789 subborrowxU64(&x41, &x42, x40, x33, 0xffffffffffffffff);
1790 var x43: u64 = undefined;
1791 var x44: u1 = undefined;
1792 subborrowxU64(&x43, &x44, x42, x35, 0xffffffffffffffff);
1793 var x45: u64 = undefined;
1794 var x46: u1 = undefined;
1795 subborrowxU64(&x45, &x46, x44, x37, 0xffffffffffffffff);
1796 var x47: u64 = undefined;
1797 var x48: u1 = undefined;
1798 subborrowxU64(&x47, &x48, x46, @as(u64, x38), 0x0);
1799 const x49 = (arg4[3]);
1800 const x50 = (arg4[2]);
1801 const x51 = (arg4[1]);
1802 const x52 = (arg4[0]);
1803 var x53: u64 = undefined;
1804 var x54: u1 = undefined;
1805 subborrowxU64(&x53, &x54, 0x0, 0x0, x52);
1806 var x55: u64 = undefined;
1807 var x56: u1 = undefined;
1808 subborrowxU64(&x55, &x56, x54, 0x0, x51);
1809 var x57: u64 = undefined;
1810 var x58: u1 = undefined;
1811 subborrowxU64(&x57, &x58, x56, 0x0, x50);
1812 var x59: u64 = undefined;
1813 var x60: u1 = undefined;
1814 subborrowxU64(&x59, &x60, x58, 0x0, x49);
1815 var x61: u64 = undefined;
1816 cmovznzU64(&x61, x60, 0x0, 0xffffffffffffffff);
1817 var x62: u64 = undefined;
1818 var x63: u1 = undefined;
1819 addcarryxU64(&x62, &x63, 0x0, x53, (x61 & 0xfffffffefffffc2f));
1820 var x64: u64 = undefined;
1821 var x65: u1 = undefined;
1822 addcarryxU64(&x64, &x65, x63, x55, x61);
1823 var x66: u64 = undefined;
1824 var x67: u1 = undefined;
1825 addcarryxU64(&x66, &x67, x65, x57, x61);
1826 var x68: u64 = undefined;
1827 var x69: u1 = undefined;
1828 addcarryxU64(&x68, &x69, x67, x59, x61);
1829 var x70: u64 = undefined;
1830 cmovznzU64(&x70, x3, (arg5[0]), x62);
1831 var x71: u64 = undefined;
1832 cmovznzU64(&x71, x3, (arg5[1]), x64);
1833 var x72: u64 = undefined;
1834 cmovznzU64(&x72, x3, (arg5[2]), x66);
1835 var x73: u64 = undefined;
1836 cmovznzU64(&x73, x3, (arg5[3]), x68);
1837 const x74 = @as(u1, @truncate((x22 & 0x1)));
1838 var x75: u64 = undefined;
1839 cmovznzU64(&x75, x74, 0x0, x7);
1840 var x76: u64 = undefined;
1841 cmovznzU64(&x76, x74, 0x0, x8);
1842 var x77: u64 = undefined;
1843 cmovznzU64(&x77, x74, 0x0, x9);
1844 var x78: u64 = undefined;
1845 cmovznzU64(&x78, x74, 0x0, x10);
1846 var x79: u64 = undefined;
1847 cmovznzU64(&x79, x74, 0x0, x11);
1848 var x80: u64 = undefined;
1849 var x81: u1 = undefined;
1850 addcarryxU64(&x80, &x81, 0x0, x22, x75);
1851 var x82: u64 = undefined;
1852 var x83: u1 = undefined;
1853 addcarryxU64(&x82, &x83, x81, x23, x76);
1854 var x84: u64 = undefined;
1855 var x85: u1 = undefined;
1856 addcarryxU64(&x84, &x85, x83, x24, x77);
1857 var x86: u64 = undefined;
1858 var x87: u1 = undefined;
1859 addcarryxU64(&x86, &x87, x85, x25, x78);
1860 var x88: u64 = undefined;
1861 var x89: u1 = undefined;
1862 addcarryxU64(&x88, &x89, x87, x26, x79);
1863 var x90: u64 = undefined;
1864 cmovznzU64(&x90, x74, 0x0, x27);
1865 var x91: u64 = undefined;
1866 cmovznzU64(&x91, x74, 0x0, x28);
1867 var x92: u64 = undefined;
1868 cmovznzU64(&x92, x74, 0x0, x29);
1869 var x93: u64 = undefined;
1870 cmovznzU64(&x93, x74, 0x0, x30);
1871 var x94: u64 = undefined;
1872 var x95: u1 = undefined;
1873 addcarryxU64(&x94, &x95, 0x0, x70, x90);
1874 var x96: u64 = undefined;
1875 var x97: u1 = undefined;
1876 addcarryxU64(&x96, &x97, x95, x71, x91);
1877 var x98: u64 = undefined;
1878 var x99: u1 = undefined;
1879 addcarryxU64(&x98, &x99, x97, x72, x92);
1880 var x100: u64 = undefined;
1881 var x101: u1 = undefined;
1882 addcarryxU64(&x100, &x101, x99, x73, x93);
1883 var x102: u64 = undefined;
1884 var x103: u1 = undefined;
1885 subborrowxU64(&x102, &x103, 0x0, x94, 0xfffffffefffffc2f);
1886 var x104: u64 = undefined;
1887 var x105: u1 = undefined;
1888 subborrowxU64(&x104, &x105, x103, x96, 0xffffffffffffffff);
1889 var x106: u64 = undefined;
1890 var x107: u1 = undefined;
1891 subborrowxU64(&x106, &x107, x105, x98, 0xffffffffffffffff);
1892 var x108: u64 = undefined;
1893 var x109: u1 = undefined;
1894 subborrowxU64(&x108, &x109, x107, x100, 0xffffffffffffffff);
1895 var x110: u64 = undefined;
1896 var x111: u1 = undefined;
1897 subborrowxU64(&x110, &x111, x109, @as(u64, x101), 0x0);
1898 var x112: u64 = undefined;
1899 var x113: u1 = undefined;
1900 addcarryxU64(&x112, &x113, 0x0, x6, 0x1);
1901 const x114 = ((x80 >> 1) | ((x82 << 63) & 0xffffffffffffffff));
1902 const x115 = ((x82 >> 1) | ((x84 << 63) & 0xffffffffffffffff));
1903 const x116 = ((x84 >> 1) | ((x86 << 63) & 0xffffffffffffffff));
1904 const x117 = ((x86 >> 1) | ((x88 << 63) & 0xffffffffffffffff));
1905 const x118 = ((x88 & 0x8000000000000000) | (x88 >> 1));
1906 var x119: u64 = undefined;
1907 cmovznzU64(&x119, x48, x39, x31);
1908 var x120: u64 = undefined;
1909 cmovznzU64(&x120, x48, x41, x33);
1910 var x121: u64 = undefined;
1911 cmovznzU64(&x121, x48, x43, x35);
1912 var x122: u64 = undefined;
1913 cmovznzU64(&x122, x48, x45, x37);
1914 var x123: u64 = undefined;
1915 cmovznzU64(&x123, x111, x102, x94);
1916 var x124: u64 = undefined;
1917 cmovznzU64(&x124, x111, x104, x96);
1918 var x125: u64 = undefined;
1919 cmovznzU64(&x125, x111, x106, x98);
1920 var x126: u64 = undefined;
1921 cmovznzU64(&x126, x111, x108, x100);
1922 out1.* = x112;
1923 out2[0] = x7;
1924 out2[1] = x8;
1925 out2[2] = x9;
1926 out2[3] = x10;
1927 out2[4] = x11;
1928 out3[0] = x114;
1929 out3[1] = x115;
1930 out3[2] = x116;
1931 out3[3] = x117;
1932 out3[4] = x118;
1933 out4[0] = x119;
1934 out4[1] = x120;
1935 out4[2] = x121;
1936 out4[3] = x122;
1937 out5[0] = x123;
1938 out5[1] = x124;
1939 out5[2] = x125;
1940 out5[3] = x126;
1941}
1942
1943/// The function divstepPrecomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
1944///
1945/// Postconditions:
1946/// eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)
1947/// 0 ≤ eval out1 < m
1948///
1949/// Output Bounds:
1950/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1951pub fn divstepPrecomp(out1: *[4]u64) void {
1952 @setRuntimeSafety(mode == .debug);
1953
1954 out1[0] = 0xf201a41831525e0a;
1955 out1[1] = 0x9953f9ddcd648d85;
1956 out1[2] = 0xe86029463db210a9;
1957 out1[3] = 0x24fb8a3104b03709;
1958}