1 /* Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --inline --static --use-value-barrier p256 32 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp */
2 /* curve description: p256 */
3 /* machine_wordsize = 32 (from "32") */
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 = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from "2^256 - 2^224 + 2^192 + 2^96 - 1") */
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] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) */
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] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) + (z[7] << 224) in */
18 /* if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256 */
19
20 #include <stdint.h>
21 typedef unsigned char fiat_p256_uint1;
22 typedef signed char fiat_p256_int1;
23 #if defined(__GNUC__) || defined(__clang__)
24 # define FIAT_P256_FIAT_INLINE __inline__
25 #else
26 # define FIAT_P256_FIAT_INLINE
27 #endif
28
29 /* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
30 /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
31 typedef uint32_t fiat_p256_montgomery_domain_field_element[8];
32
33 /* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
34 /* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
35 typedef uint32_t fiat_p256_non_montgomery_domain_field_element[8];
36
37 #if (-1 & 3) != 3
38 #error "This code only works on a two's complement system"
39 #endif
40
41 #if !defined(FIAT_P256_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
fiat_p256_value_barrier_u32(uint32_t a)42 static __inline__ uint32_t fiat_p256_value_barrier_u32(uint32_t a) {
43 __asm__("" : "+r"(a) : /* no inputs */);
44 return a;
45 }
46 #else
47 # define fiat_p256_value_barrier_u32(x) (x)
48 #endif
49
50
51 /*
52 * The function fiat_p256_addcarryx_u32 is an addition with carry.
53 *
54 * Postconditions:
55 * out1 = (arg1 + arg2 + arg3) mod 2^32
56 * out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
57 *
58 * Input Bounds:
59 * arg1: [0x0 ~> 0x1]
60 * arg2: [0x0 ~> 0xffffffff]
61 * arg3: [0x0 ~> 0xffffffff]
62 * Output Bounds:
63 * out1: [0x0 ~> 0xffffffff]
64 * out2: [0x0 ~> 0x1]
65 */
fiat_p256_addcarryx_u32(uint32_t * out1,fiat_p256_uint1 * out2,fiat_p256_uint1 arg1,uint32_t arg2,uint32_t arg3)66 static FIAT_P256_FIAT_INLINE void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) {
67 uint64_t x1;
68 uint32_t x2;
69 fiat_p256_uint1 x3;
70 x1 = ((arg1 + (uint64_t)arg2) + arg3);
71 x2 = (uint32_t)(x1 & UINT32_C(0xffffffff));
72 x3 = (fiat_p256_uint1)(x1 >> 32);
73 *out1 = x2;
74 *out2 = x3;
75 }
76
77 /*
78 * The function fiat_p256_subborrowx_u32 is a subtraction with borrow.
79 *
80 * Postconditions:
81 * out1 = (-arg1 + arg2 + -arg3) mod 2^32
82 * out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
83 *
84 * Input Bounds:
85 * arg1: [0x0 ~> 0x1]
86 * arg2: [0x0 ~> 0xffffffff]
87 * arg3: [0x0 ~> 0xffffffff]
88 * Output Bounds:
89 * out1: [0x0 ~> 0xffffffff]
90 * out2: [0x0 ~> 0x1]
91 */
fiat_p256_subborrowx_u32(uint32_t * out1,fiat_p256_uint1 * out2,fiat_p256_uint1 arg1,uint32_t arg2,uint32_t arg3)92 static FIAT_P256_FIAT_INLINE void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) {
93 int64_t x1;
94 fiat_p256_int1 x2;
95 uint32_t x3;
96 x1 = ((arg2 - (int64_t)arg1) - arg3);
97 x2 = (fiat_p256_int1)(x1 >> 32);
98 x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
99 *out1 = x3;
100 *out2 = (fiat_p256_uint1)(0x0 - x2);
101 }
102
103 /*
104 * The function fiat_p256_mulx_u32 is a multiplication, returning the full double-width result.
105 *
106 * Postconditions:
107 * out1 = (arg1 * arg2) mod 2^32
108 * out2 = ⌊arg1 * arg2 / 2^32⌋
109 *
110 * Input Bounds:
111 * arg1: [0x0 ~> 0xffffffff]
112 * arg2: [0x0 ~> 0xffffffff]
113 * Output Bounds:
114 * out1: [0x0 ~> 0xffffffff]
115 * out2: [0x0 ~> 0xffffffff]
116 */
fiat_p256_mulx_u32(uint32_t * out1,uint32_t * out2,uint32_t arg1,uint32_t arg2)117 static FIAT_P256_FIAT_INLINE void fiat_p256_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, uint32_t arg2) {
118 uint64_t x1;
119 uint32_t x2;
120 uint32_t x3;
121 x1 = ((uint64_t)arg1 * arg2);
122 x2 = (uint32_t)(x1 & UINT32_C(0xffffffff));
123 x3 = (uint32_t)(x1 >> 32);
124 *out1 = x2;
125 *out2 = x3;
126 }
127
128 /*
129 * The function fiat_p256_cmovznz_u32 is a single-word conditional move.
130 *
131 * Postconditions:
132 * out1 = (if arg1 = 0 then arg2 else arg3)
133 *
134 * Input Bounds:
135 * arg1: [0x0 ~> 0x1]
136 * arg2: [0x0 ~> 0xffffffff]
137 * arg3: [0x0 ~> 0xffffffff]
138 * Output Bounds:
139 * out1: [0x0 ~> 0xffffffff]
140 */
fiat_p256_cmovznz_u32(uint32_t * out1,fiat_p256_uint1 arg1,uint32_t arg2,uint32_t arg3)141 static FIAT_P256_FIAT_INLINE void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) {
142 fiat_p256_uint1 x1;
143 uint32_t x2;
144 uint32_t x3;
145 x1 = (!(!arg1));
146 x2 = ((fiat_p256_int1)(0x0 - x1) & UINT32_C(0xffffffff));
147 x3 = ((fiat_p256_value_barrier_u32(x2) & arg3) | (fiat_p256_value_barrier_u32((~x2)) & arg2));
148 *out1 = x3;
149 }
150
151 /*
152 * The function fiat_p256_mul multiplies two field elements in the Montgomery domain.
153 *
154 * Preconditions:
155 * 0 ≤ eval arg1 < m
156 * 0 ≤ eval arg2 < m
157 * Postconditions:
158 * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
159 * 0 ≤ eval out1 < m
160 *
161 */
fiat_p256_mul(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1,const fiat_p256_montgomery_domain_field_element arg2)162 static FIAT_P256_FIAT_INLINE void fiat_p256_mul(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1, const fiat_p256_montgomery_domain_field_element arg2) {
163 uint32_t x1;
164 uint32_t x2;
165 uint32_t x3;
166 uint32_t x4;
167 uint32_t x5;
168 uint32_t x6;
169 uint32_t x7;
170 uint32_t x8;
171 uint32_t x9;
172 uint32_t x10;
173 uint32_t x11;
174 uint32_t x12;
175 uint32_t x13;
176 uint32_t x14;
177 uint32_t x15;
178 uint32_t x16;
179 uint32_t x17;
180 uint32_t x18;
181 uint32_t x19;
182 uint32_t x20;
183 uint32_t x21;
184 uint32_t x22;
185 uint32_t x23;
186 uint32_t x24;
187 uint32_t x25;
188 fiat_p256_uint1 x26;
189 uint32_t x27;
190 fiat_p256_uint1 x28;
191 uint32_t x29;
192 fiat_p256_uint1 x30;
193 uint32_t x31;
194 fiat_p256_uint1 x32;
195 uint32_t x33;
196 fiat_p256_uint1 x34;
197 uint32_t x35;
198 fiat_p256_uint1 x36;
199 uint32_t x37;
200 fiat_p256_uint1 x38;
201 uint32_t x39;
202 uint32_t x40;
203 uint32_t x41;
204 uint32_t x42;
205 uint32_t x43;
206 uint32_t x44;
207 uint32_t x45;
208 uint32_t x46;
209 uint32_t x47;
210 uint32_t x48;
211 fiat_p256_uint1 x49;
212 uint32_t x50;
213 fiat_p256_uint1 x51;
214 uint32_t x52;
215 uint32_t x53;
216 fiat_p256_uint1 x54;
217 uint32_t x55;
218 fiat_p256_uint1 x56;
219 uint32_t x57;
220 fiat_p256_uint1 x58;
221 uint32_t x59;
222 fiat_p256_uint1 x60;
223 uint32_t x61;
224 fiat_p256_uint1 x62;
225 uint32_t x63;
226 fiat_p256_uint1 x64;
227 uint32_t x65;
228 fiat_p256_uint1 x66;
229 uint32_t x67;
230 fiat_p256_uint1 x68;
231 uint32_t x69;
232 fiat_p256_uint1 x70;
233 uint32_t x71;
234 uint32_t x72;
235 uint32_t x73;
236 uint32_t x74;
237 uint32_t x75;
238 uint32_t x76;
239 uint32_t x77;
240 uint32_t x78;
241 uint32_t x79;
242 uint32_t x80;
243 uint32_t x81;
244 uint32_t x82;
245 uint32_t x83;
246 uint32_t x84;
247 uint32_t x85;
248 uint32_t x86;
249 uint32_t x87;
250 fiat_p256_uint1 x88;
251 uint32_t x89;
252 fiat_p256_uint1 x90;
253 uint32_t x91;
254 fiat_p256_uint1 x92;
255 uint32_t x93;
256 fiat_p256_uint1 x94;
257 uint32_t x95;
258 fiat_p256_uint1 x96;
259 uint32_t x97;
260 fiat_p256_uint1 x98;
261 uint32_t x99;
262 fiat_p256_uint1 x100;
263 uint32_t x101;
264 uint32_t x102;
265 fiat_p256_uint1 x103;
266 uint32_t x104;
267 fiat_p256_uint1 x105;
268 uint32_t x106;
269 fiat_p256_uint1 x107;
270 uint32_t x108;
271 fiat_p256_uint1 x109;
272 uint32_t x110;
273 fiat_p256_uint1 x111;
274 uint32_t x112;
275 fiat_p256_uint1 x113;
276 uint32_t x114;
277 fiat_p256_uint1 x115;
278 uint32_t x116;
279 fiat_p256_uint1 x117;
280 uint32_t x118;
281 fiat_p256_uint1 x119;
282 uint32_t x120;
283 uint32_t x121;
284 uint32_t x122;
285 uint32_t x123;
286 uint32_t x124;
287 uint32_t x125;
288 uint32_t x126;
289 uint32_t x127;
290 uint32_t x128;
291 fiat_p256_uint1 x129;
292 uint32_t x130;
293 fiat_p256_uint1 x131;
294 uint32_t x132;
295 uint32_t x133;
296 fiat_p256_uint1 x134;
297 uint32_t x135;
298 fiat_p256_uint1 x136;
299 uint32_t x137;
300 fiat_p256_uint1 x138;
301 uint32_t x139;
302 fiat_p256_uint1 x140;
303 uint32_t x141;
304 fiat_p256_uint1 x142;
305 uint32_t x143;
306 fiat_p256_uint1 x144;
307 uint32_t x145;
308 fiat_p256_uint1 x146;
309 uint32_t x147;
310 fiat_p256_uint1 x148;
311 uint32_t x149;
312 fiat_p256_uint1 x150;
313 uint32_t x151;
314 uint32_t x152;
315 uint32_t x153;
316 uint32_t x154;
317 uint32_t x155;
318 uint32_t x156;
319 uint32_t x157;
320 uint32_t x158;
321 uint32_t x159;
322 uint32_t x160;
323 uint32_t x161;
324 uint32_t x162;
325 uint32_t x163;
326 uint32_t x164;
327 uint32_t x165;
328 uint32_t x166;
329 uint32_t x167;
330 uint32_t x168;
331 fiat_p256_uint1 x169;
332 uint32_t x170;
333 fiat_p256_uint1 x171;
334 uint32_t x172;
335 fiat_p256_uint1 x173;
336 uint32_t x174;
337 fiat_p256_uint1 x175;
338 uint32_t x176;
339 fiat_p256_uint1 x177;
340 uint32_t x178;
341 fiat_p256_uint1 x179;
342 uint32_t x180;
343 fiat_p256_uint1 x181;
344 uint32_t x182;
345 uint32_t x183;
346 fiat_p256_uint1 x184;
347 uint32_t x185;
348 fiat_p256_uint1 x186;
349 uint32_t x187;
350 fiat_p256_uint1 x188;
351 uint32_t x189;
352 fiat_p256_uint1 x190;
353 uint32_t x191;
354 fiat_p256_uint1 x192;
355 uint32_t x193;
356 fiat_p256_uint1 x194;
357 uint32_t x195;
358 fiat_p256_uint1 x196;
359 uint32_t x197;
360 fiat_p256_uint1 x198;
361 uint32_t x199;
362 fiat_p256_uint1 x200;
363 uint32_t x201;
364 uint32_t x202;
365 uint32_t x203;
366 uint32_t x204;
367 uint32_t x205;
368 uint32_t x206;
369 uint32_t x207;
370 uint32_t x208;
371 uint32_t x209;
372 fiat_p256_uint1 x210;
373 uint32_t x211;
374 fiat_p256_uint1 x212;
375 uint32_t x213;
376 uint32_t x214;
377 fiat_p256_uint1 x215;
378 uint32_t x216;
379 fiat_p256_uint1 x217;
380 uint32_t x218;
381 fiat_p256_uint1 x219;
382 uint32_t x220;
383 fiat_p256_uint1 x221;
384 uint32_t x222;
385 fiat_p256_uint1 x223;
386 uint32_t x224;
387 fiat_p256_uint1 x225;
388 uint32_t x226;
389 fiat_p256_uint1 x227;
390 uint32_t x228;
391 fiat_p256_uint1 x229;
392 uint32_t x230;
393 fiat_p256_uint1 x231;
394 uint32_t x232;
395 uint32_t x233;
396 uint32_t x234;
397 uint32_t x235;
398 uint32_t x236;
399 uint32_t x237;
400 uint32_t x238;
401 uint32_t x239;
402 uint32_t x240;
403 uint32_t x241;
404 uint32_t x242;
405 uint32_t x243;
406 uint32_t x244;
407 uint32_t x245;
408 uint32_t x246;
409 uint32_t x247;
410 uint32_t x248;
411 uint32_t x249;
412 fiat_p256_uint1 x250;
413 uint32_t x251;
414 fiat_p256_uint1 x252;
415 uint32_t x253;
416 fiat_p256_uint1 x254;
417 uint32_t x255;
418 fiat_p256_uint1 x256;
419 uint32_t x257;
420 fiat_p256_uint1 x258;
421 uint32_t x259;
422 fiat_p256_uint1 x260;
423 uint32_t x261;
424 fiat_p256_uint1 x262;
425 uint32_t x263;
426 uint32_t x264;
427 fiat_p256_uint1 x265;
428 uint32_t x266;
429 fiat_p256_uint1 x267;
430 uint32_t x268;
431 fiat_p256_uint1 x269;
432 uint32_t x270;
433 fiat_p256_uint1 x271;
434 uint32_t x272;
435 fiat_p256_uint1 x273;
436 uint32_t x274;
437 fiat_p256_uint1 x275;
438 uint32_t x276;
439 fiat_p256_uint1 x277;
440 uint32_t x278;
441 fiat_p256_uint1 x279;
442 uint32_t x280;
443 fiat_p256_uint1 x281;
444 uint32_t x282;
445 uint32_t x283;
446 uint32_t x284;
447 uint32_t x285;
448 uint32_t x286;
449 uint32_t x287;
450 uint32_t x288;
451 uint32_t x289;
452 uint32_t x290;
453 fiat_p256_uint1 x291;
454 uint32_t x292;
455 fiat_p256_uint1 x293;
456 uint32_t x294;
457 uint32_t x295;
458 fiat_p256_uint1 x296;
459 uint32_t x297;
460 fiat_p256_uint1 x298;
461 uint32_t x299;
462 fiat_p256_uint1 x300;
463 uint32_t x301;
464 fiat_p256_uint1 x302;
465 uint32_t x303;
466 fiat_p256_uint1 x304;
467 uint32_t x305;
468 fiat_p256_uint1 x306;
469 uint32_t x307;
470 fiat_p256_uint1 x308;
471 uint32_t x309;
472 fiat_p256_uint1 x310;
473 uint32_t x311;
474 fiat_p256_uint1 x312;
475 uint32_t x313;
476 uint32_t x314;
477 uint32_t x315;
478 uint32_t x316;
479 uint32_t x317;
480 uint32_t x318;
481 uint32_t x319;
482 uint32_t x320;
483 uint32_t x321;
484 uint32_t x322;
485 uint32_t x323;
486 uint32_t x324;
487 uint32_t x325;
488 uint32_t x326;
489 uint32_t x327;
490 uint32_t x328;
491 uint32_t x329;
492 uint32_t x330;
493 fiat_p256_uint1 x331;
494 uint32_t x332;
495 fiat_p256_uint1 x333;
496 uint32_t x334;
497 fiat_p256_uint1 x335;
498 uint32_t x336;
499 fiat_p256_uint1 x337;
500 uint32_t x338;
501 fiat_p256_uint1 x339;
502 uint32_t x340;
503 fiat_p256_uint1 x341;
504 uint32_t x342;
505 fiat_p256_uint1 x343;
506 uint32_t x344;
507 uint32_t x345;
508 fiat_p256_uint1 x346;
509 uint32_t x347;
510 fiat_p256_uint1 x348;
511 uint32_t x349;
512 fiat_p256_uint1 x350;
513 uint32_t x351;
514 fiat_p256_uint1 x352;
515 uint32_t x353;
516 fiat_p256_uint1 x354;
517 uint32_t x355;
518 fiat_p256_uint1 x356;
519 uint32_t x357;
520 fiat_p256_uint1 x358;
521 uint32_t x359;
522 fiat_p256_uint1 x360;
523 uint32_t x361;
524 fiat_p256_uint1 x362;
525 uint32_t x363;
526 uint32_t x364;
527 uint32_t x365;
528 uint32_t x366;
529 uint32_t x367;
530 uint32_t x368;
531 uint32_t x369;
532 uint32_t x370;
533 uint32_t x371;
534 fiat_p256_uint1 x372;
535 uint32_t x373;
536 fiat_p256_uint1 x374;
537 uint32_t x375;
538 uint32_t x376;
539 fiat_p256_uint1 x377;
540 uint32_t x378;
541 fiat_p256_uint1 x379;
542 uint32_t x380;
543 fiat_p256_uint1 x381;
544 uint32_t x382;
545 fiat_p256_uint1 x383;
546 uint32_t x384;
547 fiat_p256_uint1 x385;
548 uint32_t x386;
549 fiat_p256_uint1 x387;
550 uint32_t x388;
551 fiat_p256_uint1 x389;
552 uint32_t x390;
553 fiat_p256_uint1 x391;
554 uint32_t x392;
555 fiat_p256_uint1 x393;
556 uint32_t x394;
557 uint32_t x395;
558 uint32_t x396;
559 uint32_t x397;
560 uint32_t x398;
561 uint32_t x399;
562 uint32_t x400;
563 uint32_t x401;
564 uint32_t x402;
565 uint32_t x403;
566 uint32_t x404;
567 uint32_t x405;
568 uint32_t x406;
569 uint32_t x407;
570 uint32_t x408;
571 uint32_t x409;
572 uint32_t x410;
573 uint32_t x411;
574 fiat_p256_uint1 x412;
575 uint32_t x413;
576 fiat_p256_uint1 x414;
577 uint32_t x415;
578 fiat_p256_uint1 x416;
579 uint32_t x417;
580 fiat_p256_uint1 x418;
581 uint32_t x419;
582 fiat_p256_uint1 x420;
583 uint32_t x421;
584 fiat_p256_uint1 x422;
585 uint32_t x423;
586 fiat_p256_uint1 x424;
587 uint32_t x425;
588 uint32_t x426;
589 fiat_p256_uint1 x427;
590 uint32_t x428;
591 fiat_p256_uint1 x429;
592 uint32_t x430;
593 fiat_p256_uint1 x431;
594 uint32_t x432;
595 fiat_p256_uint1 x433;
596 uint32_t x434;
597 fiat_p256_uint1 x435;
598 uint32_t x436;
599 fiat_p256_uint1 x437;
600 uint32_t x438;
601 fiat_p256_uint1 x439;
602 uint32_t x440;
603 fiat_p256_uint1 x441;
604 uint32_t x442;
605 fiat_p256_uint1 x443;
606 uint32_t x444;
607 uint32_t x445;
608 uint32_t x446;
609 uint32_t x447;
610 uint32_t x448;
611 uint32_t x449;
612 uint32_t x450;
613 uint32_t x451;
614 uint32_t x452;
615 fiat_p256_uint1 x453;
616 uint32_t x454;
617 fiat_p256_uint1 x455;
618 uint32_t x456;
619 uint32_t x457;
620 fiat_p256_uint1 x458;
621 uint32_t x459;
622 fiat_p256_uint1 x460;
623 uint32_t x461;
624 fiat_p256_uint1 x462;
625 uint32_t x463;
626 fiat_p256_uint1 x464;
627 uint32_t x465;
628 fiat_p256_uint1 x466;
629 uint32_t x467;
630 fiat_p256_uint1 x468;
631 uint32_t x469;
632 fiat_p256_uint1 x470;
633 uint32_t x471;
634 fiat_p256_uint1 x472;
635 uint32_t x473;
636 fiat_p256_uint1 x474;
637 uint32_t x475;
638 uint32_t x476;
639 uint32_t x477;
640 uint32_t x478;
641 uint32_t x479;
642 uint32_t x480;
643 uint32_t x481;
644 uint32_t x482;
645 uint32_t x483;
646 uint32_t x484;
647 uint32_t x485;
648 uint32_t x486;
649 uint32_t x487;
650 uint32_t x488;
651 uint32_t x489;
652 uint32_t x490;
653 uint32_t x491;
654 uint32_t x492;
655 fiat_p256_uint1 x493;
656 uint32_t x494;
657 fiat_p256_uint1 x495;
658 uint32_t x496;
659 fiat_p256_uint1 x497;
660 uint32_t x498;
661 fiat_p256_uint1 x499;
662 uint32_t x500;
663 fiat_p256_uint1 x501;
664 uint32_t x502;
665 fiat_p256_uint1 x503;
666 uint32_t x504;
667 fiat_p256_uint1 x505;
668 uint32_t x506;
669 uint32_t x507;
670 fiat_p256_uint1 x508;
671 uint32_t x509;
672 fiat_p256_uint1 x510;
673 uint32_t x511;
674 fiat_p256_uint1 x512;
675 uint32_t x513;
676 fiat_p256_uint1 x514;
677 uint32_t x515;
678 fiat_p256_uint1 x516;
679 uint32_t x517;
680 fiat_p256_uint1 x518;
681 uint32_t x519;
682 fiat_p256_uint1 x520;
683 uint32_t x521;
684 fiat_p256_uint1 x522;
685 uint32_t x523;
686 fiat_p256_uint1 x524;
687 uint32_t x525;
688 uint32_t x526;
689 uint32_t x527;
690 uint32_t x528;
691 uint32_t x529;
692 uint32_t x530;
693 uint32_t x531;
694 uint32_t x532;
695 uint32_t x533;
696 fiat_p256_uint1 x534;
697 uint32_t x535;
698 fiat_p256_uint1 x536;
699 uint32_t x537;
700 uint32_t x538;
701 fiat_p256_uint1 x539;
702 uint32_t x540;
703 fiat_p256_uint1 x541;
704 uint32_t x542;
705 fiat_p256_uint1 x543;
706 uint32_t x544;
707 fiat_p256_uint1 x545;
708 uint32_t x546;
709 fiat_p256_uint1 x547;
710 uint32_t x548;
711 fiat_p256_uint1 x549;
712 uint32_t x550;
713 fiat_p256_uint1 x551;
714 uint32_t x552;
715 fiat_p256_uint1 x553;
716 uint32_t x554;
717 fiat_p256_uint1 x555;
718 uint32_t x556;
719 uint32_t x557;
720 uint32_t x558;
721 uint32_t x559;
722 uint32_t x560;
723 uint32_t x561;
724 uint32_t x562;
725 uint32_t x563;
726 uint32_t x564;
727 uint32_t x565;
728 uint32_t x566;
729 uint32_t x567;
730 uint32_t x568;
731 uint32_t x569;
732 uint32_t x570;
733 uint32_t x571;
734 uint32_t x572;
735 uint32_t x573;
736 fiat_p256_uint1 x574;
737 uint32_t x575;
738 fiat_p256_uint1 x576;
739 uint32_t x577;
740 fiat_p256_uint1 x578;
741 uint32_t x579;
742 fiat_p256_uint1 x580;
743 uint32_t x581;
744 fiat_p256_uint1 x582;
745 uint32_t x583;
746 fiat_p256_uint1 x584;
747 uint32_t x585;
748 fiat_p256_uint1 x586;
749 uint32_t x587;
750 uint32_t x588;
751 fiat_p256_uint1 x589;
752 uint32_t x590;
753 fiat_p256_uint1 x591;
754 uint32_t x592;
755 fiat_p256_uint1 x593;
756 uint32_t x594;
757 fiat_p256_uint1 x595;
758 uint32_t x596;
759 fiat_p256_uint1 x597;
760 uint32_t x598;
761 fiat_p256_uint1 x599;
762 uint32_t x600;
763 fiat_p256_uint1 x601;
764 uint32_t x602;
765 fiat_p256_uint1 x603;
766 uint32_t x604;
767 fiat_p256_uint1 x605;
768 uint32_t x606;
769 uint32_t x607;
770 uint32_t x608;
771 uint32_t x609;
772 uint32_t x610;
773 uint32_t x611;
774 uint32_t x612;
775 uint32_t x613;
776 uint32_t x614;
777 fiat_p256_uint1 x615;
778 uint32_t x616;
779 fiat_p256_uint1 x617;
780 uint32_t x618;
781 uint32_t x619;
782 fiat_p256_uint1 x620;
783 uint32_t x621;
784 fiat_p256_uint1 x622;
785 uint32_t x623;
786 fiat_p256_uint1 x624;
787 uint32_t x625;
788 fiat_p256_uint1 x626;
789 uint32_t x627;
790 fiat_p256_uint1 x628;
791 uint32_t x629;
792 fiat_p256_uint1 x630;
793 uint32_t x631;
794 fiat_p256_uint1 x632;
795 uint32_t x633;
796 fiat_p256_uint1 x634;
797 uint32_t x635;
798 fiat_p256_uint1 x636;
799 uint32_t x637;
800 uint32_t x638;
801 fiat_p256_uint1 x639;
802 uint32_t x640;
803 fiat_p256_uint1 x641;
804 uint32_t x642;
805 fiat_p256_uint1 x643;
806 uint32_t x644;
807 fiat_p256_uint1 x645;
808 uint32_t x646;
809 fiat_p256_uint1 x647;
810 uint32_t x648;
811 fiat_p256_uint1 x649;
812 uint32_t x650;
813 fiat_p256_uint1 x651;
814 uint32_t x652;
815 fiat_p256_uint1 x653;
816 uint32_t x654;
817 fiat_p256_uint1 x655;
818 uint32_t x656;
819 uint32_t x657;
820 uint32_t x658;
821 uint32_t x659;
822 uint32_t x660;
823 uint32_t x661;
824 uint32_t x662;
825 uint32_t x663;
826 x1 = (arg1[1]);
827 x2 = (arg1[2]);
828 x3 = (arg1[3]);
829 x4 = (arg1[4]);
830 x5 = (arg1[5]);
831 x6 = (arg1[6]);
832 x7 = (arg1[7]);
833 x8 = (arg1[0]);
834 fiat_p256_mulx_u32(&x9, &x10, x8, (arg2[7]));
835 fiat_p256_mulx_u32(&x11, &x12, x8, (arg2[6]));
836 fiat_p256_mulx_u32(&x13, &x14, x8, (arg2[5]));
837 fiat_p256_mulx_u32(&x15, &x16, x8, (arg2[4]));
838 fiat_p256_mulx_u32(&x17, &x18, x8, (arg2[3]));
839 fiat_p256_mulx_u32(&x19, &x20, x8, (arg2[2]));
840 fiat_p256_mulx_u32(&x21, &x22, x8, (arg2[1]));
841 fiat_p256_mulx_u32(&x23, &x24, x8, (arg2[0]));
842 fiat_p256_addcarryx_u32(&x25, &x26, 0x0, x24, x21);
843 fiat_p256_addcarryx_u32(&x27, &x28, x26, x22, x19);
844 fiat_p256_addcarryx_u32(&x29, &x30, x28, x20, x17);
845 fiat_p256_addcarryx_u32(&x31, &x32, x30, x18, x15);
846 fiat_p256_addcarryx_u32(&x33, &x34, x32, x16, x13);
847 fiat_p256_addcarryx_u32(&x35, &x36, x34, x14, x11);
848 fiat_p256_addcarryx_u32(&x37, &x38, x36, x12, x9);
849 x39 = (x38 + x10);
850 fiat_p256_mulx_u32(&x40, &x41, x23, UINT32_C(0xffffffff));
851 fiat_p256_mulx_u32(&x42, &x43, x23, UINT32_C(0xffffffff));
852 fiat_p256_mulx_u32(&x44, &x45, x23, UINT32_C(0xffffffff));
853 fiat_p256_mulx_u32(&x46, &x47, x23, UINT32_C(0xffffffff));
854 fiat_p256_addcarryx_u32(&x48, &x49, 0x0, x47, x44);
855 fiat_p256_addcarryx_u32(&x50, &x51, x49, x45, x42);
856 x52 = (x51 + x43);
857 fiat_p256_addcarryx_u32(&x53, &x54, 0x0, x23, x46);
858 fiat_p256_addcarryx_u32(&x55, &x56, x54, x25, x48);
859 fiat_p256_addcarryx_u32(&x57, &x58, x56, x27, x50);
860 fiat_p256_addcarryx_u32(&x59, &x60, x58, x29, x52);
861 fiat_p256_addcarryx_u32(&x61, &x62, x60, x31, 0x0);
862 fiat_p256_addcarryx_u32(&x63, &x64, x62, x33, 0x0);
863 fiat_p256_addcarryx_u32(&x65, &x66, x64, x35, x23);
864 fiat_p256_addcarryx_u32(&x67, &x68, x66, x37, x40);
865 fiat_p256_addcarryx_u32(&x69, &x70, x68, x39, x41);
866 fiat_p256_mulx_u32(&x71, &x72, x1, (arg2[7]));
867 fiat_p256_mulx_u32(&x73, &x74, x1, (arg2[6]));
868 fiat_p256_mulx_u32(&x75, &x76, x1, (arg2[5]));
869 fiat_p256_mulx_u32(&x77, &x78, x1, (arg2[4]));
870 fiat_p256_mulx_u32(&x79, &x80, x1, (arg2[3]));
871 fiat_p256_mulx_u32(&x81, &x82, x1, (arg2[2]));
872 fiat_p256_mulx_u32(&x83, &x84, x1, (arg2[1]));
873 fiat_p256_mulx_u32(&x85, &x86, x1, (arg2[0]));
874 fiat_p256_addcarryx_u32(&x87, &x88, 0x0, x86, x83);
875 fiat_p256_addcarryx_u32(&x89, &x90, x88, x84, x81);
876 fiat_p256_addcarryx_u32(&x91, &x92, x90, x82, x79);
877 fiat_p256_addcarryx_u32(&x93, &x94, x92, x80, x77);
878 fiat_p256_addcarryx_u32(&x95, &x96, x94, x78, x75);
879 fiat_p256_addcarryx_u32(&x97, &x98, x96, x76, x73);
880 fiat_p256_addcarryx_u32(&x99, &x100, x98, x74, x71);
881 x101 = (x100 + x72);
882 fiat_p256_addcarryx_u32(&x102, &x103, 0x0, x55, x85);
883 fiat_p256_addcarryx_u32(&x104, &x105, x103, x57, x87);
884 fiat_p256_addcarryx_u32(&x106, &x107, x105, x59, x89);
885 fiat_p256_addcarryx_u32(&x108, &x109, x107, x61, x91);
886 fiat_p256_addcarryx_u32(&x110, &x111, x109, x63, x93);
887 fiat_p256_addcarryx_u32(&x112, &x113, x111, x65, x95);
888 fiat_p256_addcarryx_u32(&x114, &x115, x113, x67, x97);
889 fiat_p256_addcarryx_u32(&x116, &x117, x115, x69, x99);
890 fiat_p256_addcarryx_u32(&x118, &x119, x117, x70, x101);
891 fiat_p256_mulx_u32(&x120, &x121, x102, UINT32_C(0xffffffff));
892 fiat_p256_mulx_u32(&x122, &x123, x102, UINT32_C(0xffffffff));
893 fiat_p256_mulx_u32(&x124, &x125, x102, UINT32_C(0xffffffff));
894 fiat_p256_mulx_u32(&x126, &x127, x102, UINT32_C(0xffffffff));
895 fiat_p256_addcarryx_u32(&x128, &x129, 0x0, x127, x124);
896 fiat_p256_addcarryx_u32(&x130, &x131, x129, x125, x122);
897 x132 = (x131 + x123);
898 fiat_p256_addcarryx_u32(&x133, &x134, 0x0, x102, x126);
899 fiat_p256_addcarryx_u32(&x135, &x136, x134, x104, x128);
900 fiat_p256_addcarryx_u32(&x137, &x138, x136, x106, x130);
901 fiat_p256_addcarryx_u32(&x139, &x140, x138, x108, x132);
902 fiat_p256_addcarryx_u32(&x141, &x142, x140, x110, 0x0);
903 fiat_p256_addcarryx_u32(&x143, &x144, x142, x112, 0x0);
904 fiat_p256_addcarryx_u32(&x145, &x146, x144, x114, x102);
905 fiat_p256_addcarryx_u32(&x147, &x148, x146, x116, x120);
906 fiat_p256_addcarryx_u32(&x149, &x150, x148, x118, x121);
907 x151 = ((uint32_t)x150 + x119);
908 fiat_p256_mulx_u32(&x152, &x153, x2, (arg2[7]));
909 fiat_p256_mulx_u32(&x154, &x155, x2, (arg2[6]));
910 fiat_p256_mulx_u32(&x156, &x157, x2, (arg2[5]));
911 fiat_p256_mulx_u32(&x158, &x159, x2, (arg2[4]));
912 fiat_p256_mulx_u32(&x160, &x161, x2, (arg2[3]));
913 fiat_p256_mulx_u32(&x162, &x163, x2, (arg2[2]));
914 fiat_p256_mulx_u32(&x164, &x165, x2, (arg2[1]));
915 fiat_p256_mulx_u32(&x166, &x167, x2, (arg2[0]));
916 fiat_p256_addcarryx_u32(&x168, &x169, 0x0, x167, x164);
917 fiat_p256_addcarryx_u32(&x170, &x171, x169, x165, x162);
918 fiat_p256_addcarryx_u32(&x172, &x173, x171, x163, x160);
919 fiat_p256_addcarryx_u32(&x174, &x175, x173, x161, x158);
920 fiat_p256_addcarryx_u32(&x176, &x177, x175, x159, x156);
921 fiat_p256_addcarryx_u32(&x178, &x179, x177, x157, x154);
922 fiat_p256_addcarryx_u32(&x180, &x181, x179, x155, x152);
923 x182 = (x181 + x153);
924 fiat_p256_addcarryx_u32(&x183, &x184, 0x0, x135, x166);
925 fiat_p256_addcarryx_u32(&x185, &x186, x184, x137, x168);
926 fiat_p256_addcarryx_u32(&x187, &x188, x186, x139, x170);
927 fiat_p256_addcarryx_u32(&x189, &x190, x188, x141, x172);
928 fiat_p256_addcarryx_u32(&x191, &x192, x190, x143, x174);
929 fiat_p256_addcarryx_u32(&x193, &x194, x192, x145, x176);
930 fiat_p256_addcarryx_u32(&x195, &x196, x194, x147, x178);
931 fiat_p256_addcarryx_u32(&x197, &x198, x196, x149, x180);
932 fiat_p256_addcarryx_u32(&x199, &x200, x198, x151, x182);
933 fiat_p256_mulx_u32(&x201, &x202, x183, UINT32_C(0xffffffff));
934 fiat_p256_mulx_u32(&x203, &x204, x183, UINT32_C(0xffffffff));
935 fiat_p256_mulx_u32(&x205, &x206, x183, UINT32_C(0xffffffff));
936 fiat_p256_mulx_u32(&x207, &x208, x183, UINT32_C(0xffffffff));
937 fiat_p256_addcarryx_u32(&x209, &x210, 0x0, x208, x205);
938 fiat_p256_addcarryx_u32(&x211, &x212, x210, x206, x203);
939 x213 = (x212 + x204);
940 fiat_p256_addcarryx_u32(&x214, &x215, 0x0, x183, x207);
941 fiat_p256_addcarryx_u32(&x216, &x217, x215, x185, x209);
942 fiat_p256_addcarryx_u32(&x218, &x219, x217, x187, x211);
943 fiat_p256_addcarryx_u32(&x220, &x221, x219, x189, x213);
944 fiat_p256_addcarryx_u32(&x222, &x223, x221, x191, 0x0);
945 fiat_p256_addcarryx_u32(&x224, &x225, x223, x193, 0x0);
946 fiat_p256_addcarryx_u32(&x226, &x227, x225, x195, x183);
947 fiat_p256_addcarryx_u32(&x228, &x229, x227, x197, x201);
948 fiat_p256_addcarryx_u32(&x230, &x231, x229, x199, x202);
949 x232 = ((uint32_t)x231 + x200);
950 fiat_p256_mulx_u32(&x233, &x234, x3, (arg2[7]));
951 fiat_p256_mulx_u32(&x235, &x236, x3, (arg2[6]));
952 fiat_p256_mulx_u32(&x237, &x238, x3, (arg2[5]));
953 fiat_p256_mulx_u32(&x239, &x240, x3, (arg2[4]));
954 fiat_p256_mulx_u32(&x241, &x242, x3, (arg2[3]));
955 fiat_p256_mulx_u32(&x243, &x244, x3, (arg2[2]));
956 fiat_p256_mulx_u32(&x245, &x246, x3, (arg2[1]));
957 fiat_p256_mulx_u32(&x247, &x248, x3, (arg2[0]));
958 fiat_p256_addcarryx_u32(&x249, &x250, 0x0, x248, x245);
959 fiat_p256_addcarryx_u32(&x251, &x252, x250, x246, x243);
960 fiat_p256_addcarryx_u32(&x253, &x254, x252, x244, x241);
961 fiat_p256_addcarryx_u32(&x255, &x256, x254, x242, x239);
962 fiat_p256_addcarryx_u32(&x257, &x258, x256, x240, x237);
963 fiat_p256_addcarryx_u32(&x259, &x260, x258, x238, x235);
964 fiat_p256_addcarryx_u32(&x261, &x262, x260, x236, x233);
965 x263 = (x262 + x234);
966 fiat_p256_addcarryx_u32(&x264, &x265, 0x0, x216, x247);
967 fiat_p256_addcarryx_u32(&x266, &x267, x265, x218, x249);
968 fiat_p256_addcarryx_u32(&x268, &x269, x267, x220, x251);
969 fiat_p256_addcarryx_u32(&x270, &x271, x269, x222, x253);
970 fiat_p256_addcarryx_u32(&x272, &x273, x271, x224, x255);
971 fiat_p256_addcarryx_u32(&x274, &x275, x273, x226, x257);
972 fiat_p256_addcarryx_u32(&x276, &x277, x275, x228, x259);
973 fiat_p256_addcarryx_u32(&x278, &x279, x277, x230, x261);
974 fiat_p256_addcarryx_u32(&x280, &x281, x279, x232, x263);
975 fiat_p256_mulx_u32(&x282, &x283, x264, UINT32_C(0xffffffff));
976 fiat_p256_mulx_u32(&x284, &x285, x264, UINT32_C(0xffffffff));
977 fiat_p256_mulx_u32(&x286, &x287, x264, UINT32_C(0xffffffff));
978 fiat_p256_mulx_u32(&x288, &x289, x264, UINT32_C(0xffffffff));
979 fiat_p256_addcarryx_u32(&x290, &x291, 0x0, x289, x286);
980 fiat_p256_addcarryx_u32(&x292, &x293, x291, x287, x284);
981 x294 = (x293 + x285);
982 fiat_p256_addcarryx_u32(&x295, &x296, 0x0, x264, x288);
983 fiat_p256_addcarryx_u32(&x297, &x298, x296, x266, x290);
984 fiat_p256_addcarryx_u32(&x299, &x300, x298, x268, x292);
985 fiat_p256_addcarryx_u32(&x301, &x302, x300, x270, x294);
986 fiat_p256_addcarryx_u32(&x303, &x304, x302, x272, 0x0);
987 fiat_p256_addcarryx_u32(&x305, &x306, x304, x274, 0x0);
988 fiat_p256_addcarryx_u32(&x307, &x308, x306, x276, x264);
989 fiat_p256_addcarryx_u32(&x309, &x310, x308, x278, x282);
990 fiat_p256_addcarryx_u32(&x311, &x312, x310, x280, x283);
991 x313 = ((uint32_t)x312 + x281);
992 fiat_p256_mulx_u32(&x314, &x315, x4, (arg2[7]));
993 fiat_p256_mulx_u32(&x316, &x317, x4, (arg2[6]));
994 fiat_p256_mulx_u32(&x318, &x319, x4, (arg2[5]));
995 fiat_p256_mulx_u32(&x320, &x321, x4, (arg2[4]));
996 fiat_p256_mulx_u32(&x322, &x323, x4, (arg2[3]));
997 fiat_p256_mulx_u32(&x324, &x325, x4, (arg2[2]));
998 fiat_p256_mulx_u32(&x326, &x327, x4, (arg2[1]));
999 fiat_p256_mulx_u32(&x328, &x329, x4, (arg2[0]));
1000 fiat_p256_addcarryx_u32(&x330, &x331, 0x0, x329, x326);
1001 fiat_p256_addcarryx_u32(&x332, &x333, x331, x327, x324);
1002 fiat_p256_addcarryx_u32(&x334, &x335, x333, x325, x322);
1003 fiat_p256_addcarryx_u32(&x336, &x337, x335, x323, x320);
1004 fiat_p256_addcarryx_u32(&x338, &x339, x337, x321, x318);
1005 fiat_p256_addcarryx_u32(&x340, &x341, x339, x319, x316);
1006 fiat_p256_addcarryx_u32(&x342, &x343, x341, x317, x314);
1007 x344 = (x343 + x315);
1008 fiat_p256_addcarryx_u32(&x345, &x346, 0x0, x297, x328);
1009 fiat_p256_addcarryx_u32(&x347, &x348, x346, x299, x330);
1010 fiat_p256_addcarryx_u32(&x349, &x350, x348, x301, x332);
1011 fiat_p256_addcarryx_u32(&x351, &x352, x350, x303, x334);
1012 fiat_p256_addcarryx_u32(&x353, &x354, x352, x305, x336);
1013 fiat_p256_addcarryx_u32(&x355, &x356, x354, x307, x338);
1014 fiat_p256_addcarryx_u32(&x357, &x358, x356, x309, x340);
1015 fiat_p256_addcarryx_u32(&x359, &x360, x358, x311, x342);
1016 fiat_p256_addcarryx_u32(&x361, &x362, x360, x313, x344);
1017 fiat_p256_mulx_u32(&x363, &x364, x345, UINT32_C(0xffffffff));
1018 fiat_p256_mulx_u32(&x365, &x366, x345, UINT32_C(0xffffffff));
1019 fiat_p256_mulx_u32(&x367, &x368, x345, UINT32_C(0xffffffff));
1020 fiat_p256_mulx_u32(&x369, &x370, x345, UINT32_C(0xffffffff));
1021 fiat_p256_addcarryx_u32(&x371, &x372, 0x0, x370, x367);
1022 fiat_p256_addcarryx_u32(&x373, &x374, x372, x368, x365);
1023 x375 = (x374 + x366);
1024 fiat_p256_addcarryx_u32(&x376, &x377, 0x0, x345, x369);
1025 fiat_p256_addcarryx_u32(&x378, &x379, x377, x347, x371);
1026 fiat_p256_addcarryx_u32(&x380, &x381, x379, x349, x373);
1027 fiat_p256_addcarryx_u32(&x382, &x383, x381, x351, x375);
1028 fiat_p256_addcarryx_u32(&x384, &x385, x383, x353, 0x0);
1029 fiat_p256_addcarryx_u32(&x386, &x387, x385, x355, 0x0);
1030 fiat_p256_addcarryx_u32(&x388, &x389, x387, x357, x345);
1031 fiat_p256_addcarryx_u32(&x390, &x391, x389, x359, x363);
1032 fiat_p256_addcarryx_u32(&x392, &x393, x391, x361, x364);
1033 x394 = ((uint32_t)x393 + x362);
1034 fiat_p256_mulx_u32(&x395, &x396, x5, (arg2[7]));
1035 fiat_p256_mulx_u32(&x397, &x398, x5, (arg2[6]));
1036 fiat_p256_mulx_u32(&x399, &x400, x5, (arg2[5]));
1037 fiat_p256_mulx_u32(&x401, &x402, x5, (arg2[4]));
1038 fiat_p256_mulx_u32(&x403, &x404, x5, (arg2[3]));
1039 fiat_p256_mulx_u32(&x405, &x406, x5, (arg2[2]));
1040 fiat_p256_mulx_u32(&x407, &x408, x5, (arg2[1]));
1041 fiat_p256_mulx_u32(&x409, &x410, x5, (arg2[0]));
1042 fiat_p256_addcarryx_u32(&x411, &x412, 0x0, x410, x407);
1043 fiat_p256_addcarryx_u32(&x413, &x414, x412, x408, x405);
1044 fiat_p256_addcarryx_u32(&x415, &x416, x414, x406, x403);
1045 fiat_p256_addcarryx_u32(&x417, &x418, x416, x404, x401);
1046 fiat_p256_addcarryx_u32(&x419, &x420, x418, x402, x399);
1047 fiat_p256_addcarryx_u32(&x421, &x422, x420, x400, x397);
1048 fiat_p256_addcarryx_u32(&x423, &x424, x422, x398, x395);
1049 x425 = (x424 + x396);
1050 fiat_p256_addcarryx_u32(&x426, &x427, 0x0, x378, x409);
1051 fiat_p256_addcarryx_u32(&x428, &x429, x427, x380, x411);
1052 fiat_p256_addcarryx_u32(&x430, &x431, x429, x382, x413);
1053 fiat_p256_addcarryx_u32(&x432, &x433, x431, x384, x415);
1054 fiat_p256_addcarryx_u32(&x434, &x435, x433, x386, x417);
1055 fiat_p256_addcarryx_u32(&x436, &x437, x435, x388, x419);
1056 fiat_p256_addcarryx_u32(&x438, &x439, x437, x390, x421);
1057 fiat_p256_addcarryx_u32(&x440, &x441, x439, x392, x423);
1058 fiat_p256_addcarryx_u32(&x442, &x443, x441, x394, x425);
1059 fiat_p256_mulx_u32(&x444, &x445, x426, UINT32_C(0xffffffff));
1060 fiat_p256_mulx_u32(&x446, &x447, x426, UINT32_C(0xffffffff));
1061 fiat_p256_mulx_u32(&x448, &x449, x426, UINT32_C(0xffffffff));
1062 fiat_p256_mulx_u32(&x450, &x451, x426, UINT32_C(0xffffffff));
1063 fiat_p256_addcarryx_u32(&x452, &x453, 0x0, x451, x448);
1064 fiat_p256_addcarryx_u32(&x454, &x455, x453, x449, x446);
1065 x456 = (x455 + x447);
1066 fiat_p256_addcarryx_u32(&x457, &x458, 0x0, x426, x450);
1067 fiat_p256_addcarryx_u32(&x459, &x460, x458, x428, x452);
1068 fiat_p256_addcarryx_u32(&x461, &x462, x460, x430, x454);
1069 fiat_p256_addcarryx_u32(&x463, &x464, x462, x432, x456);
1070 fiat_p256_addcarryx_u32(&x465, &x466, x464, x434, 0x0);
1071 fiat_p256_addcarryx_u32(&x467, &x468, x466, x436, 0x0);
1072 fiat_p256_addcarryx_u32(&x469, &x470, x468, x438, x426);
1073 fiat_p256_addcarryx_u32(&x471, &x472, x470, x440, x444);
1074 fiat_p256_addcarryx_u32(&x473, &x474, x472, x442, x445);
1075 x475 = ((uint32_t)x474 + x443);
1076 fiat_p256_mulx_u32(&x476, &x477, x6, (arg2[7]));
1077 fiat_p256_mulx_u32(&x478, &x479, x6, (arg2[6]));
1078 fiat_p256_mulx_u32(&x480, &x481, x6, (arg2[5]));
1079 fiat_p256_mulx_u32(&x482, &x483, x6, (arg2[4]));
1080 fiat_p256_mulx_u32(&x484, &x485, x6, (arg2[3]));
1081 fiat_p256_mulx_u32(&x486, &x487, x6, (arg2[2]));
1082 fiat_p256_mulx_u32(&x488, &x489, x6, (arg2[1]));
1083 fiat_p256_mulx_u32(&x490, &x491, x6, (arg2[0]));
1084 fiat_p256_addcarryx_u32(&x492, &x493, 0x0, x491, x488);
1085 fiat_p256_addcarryx_u32(&x494, &x495, x493, x489, x486);
1086 fiat_p256_addcarryx_u32(&x496, &x497, x495, x487, x484);
1087 fiat_p256_addcarryx_u32(&x498, &x499, x497, x485, x482);
1088 fiat_p256_addcarryx_u32(&x500, &x501, x499, x483, x480);
1089 fiat_p256_addcarryx_u32(&x502, &x503, x501, x481, x478);
1090 fiat_p256_addcarryx_u32(&x504, &x505, x503, x479, x476);
1091 x506 = (x505 + x477);
1092 fiat_p256_addcarryx_u32(&x507, &x508, 0x0, x459, x490);
1093 fiat_p256_addcarryx_u32(&x509, &x510, x508, x461, x492);
1094 fiat_p256_addcarryx_u32(&x511, &x512, x510, x463, x494);
1095 fiat_p256_addcarryx_u32(&x513, &x514, x512, x465, x496);
1096 fiat_p256_addcarryx_u32(&x515, &x516, x514, x467, x498);
1097 fiat_p256_addcarryx_u32(&x517, &x518, x516, x469, x500);
1098 fiat_p256_addcarryx_u32(&x519, &x520, x518, x471, x502);
1099 fiat_p256_addcarryx_u32(&x521, &x522, x520, x473, x504);
1100 fiat_p256_addcarryx_u32(&x523, &x524, x522, x475, x506);
1101 fiat_p256_mulx_u32(&x525, &x526, x507, UINT32_C(0xffffffff));
1102 fiat_p256_mulx_u32(&x527, &x528, x507, UINT32_C(0xffffffff));
1103 fiat_p256_mulx_u32(&x529, &x530, x507, UINT32_C(0xffffffff));
1104 fiat_p256_mulx_u32(&x531, &x532, x507, UINT32_C(0xffffffff));
1105 fiat_p256_addcarryx_u32(&x533, &x534, 0x0, x532, x529);
1106 fiat_p256_addcarryx_u32(&x535, &x536, x534, x530, x527);
1107 x537 = (x536 + x528);
1108 fiat_p256_addcarryx_u32(&x538, &x539, 0x0, x507, x531);
1109 fiat_p256_addcarryx_u32(&x540, &x541, x539, x509, x533);
1110 fiat_p256_addcarryx_u32(&x542, &x543, x541, x511, x535);
1111 fiat_p256_addcarryx_u32(&x544, &x545, x543, x513, x537);
1112 fiat_p256_addcarryx_u32(&x546, &x547, x545, x515, 0x0);
1113 fiat_p256_addcarryx_u32(&x548, &x549, x547, x517, 0x0);
1114 fiat_p256_addcarryx_u32(&x550, &x551, x549, x519, x507);
1115 fiat_p256_addcarryx_u32(&x552, &x553, x551, x521, x525);
1116 fiat_p256_addcarryx_u32(&x554, &x555, x553, x523, x526);
1117 x556 = ((uint32_t)x555 + x524);
1118 fiat_p256_mulx_u32(&x557, &x558, x7, (arg2[7]));
1119 fiat_p256_mulx_u32(&x559, &x560, x7, (arg2[6]));
1120 fiat_p256_mulx_u32(&x561, &x562, x7, (arg2[5]));
1121 fiat_p256_mulx_u32(&x563, &x564, x7, (arg2[4]));
1122 fiat_p256_mulx_u32(&x565, &x566, x7, (arg2[3]));
1123 fiat_p256_mulx_u32(&x567, &x568, x7, (arg2[2]));
1124 fiat_p256_mulx_u32(&x569, &x570, x7, (arg2[1]));
1125 fiat_p256_mulx_u32(&x571, &x572, x7, (arg2[0]));
1126 fiat_p256_addcarryx_u32(&x573, &x574, 0x0, x572, x569);
1127 fiat_p256_addcarryx_u32(&x575, &x576, x574, x570, x567);
1128 fiat_p256_addcarryx_u32(&x577, &x578, x576, x568, x565);
1129 fiat_p256_addcarryx_u32(&x579, &x580, x578, x566, x563);
1130 fiat_p256_addcarryx_u32(&x581, &x582, x580, x564, x561);
1131 fiat_p256_addcarryx_u32(&x583, &x584, x582, x562, x559);
1132 fiat_p256_addcarryx_u32(&x585, &x586, x584, x560, x557);
1133 x587 = (x586 + x558);
1134 fiat_p256_addcarryx_u32(&x588, &x589, 0x0, x540, x571);
1135 fiat_p256_addcarryx_u32(&x590, &x591, x589, x542, x573);
1136 fiat_p256_addcarryx_u32(&x592, &x593, x591, x544, x575);
1137 fiat_p256_addcarryx_u32(&x594, &x595, x593, x546, x577);
1138 fiat_p256_addcarryx_u32(&x596, &x597, x595, x548, x579);
1139 fiat_p256_addcarryx_u32(&x598, &x599, x597, x550, x581);
1140 fiat_p256_addcarryx_u32(&x600, &x601, x599, x552, x583);
1141 fiat_p256_addcarryx_u32(&x602, &x603, x601, x554, x585);
1142 fiat_p256_addcarryx_u32(&x604, &x605, x603, x556, x587);
1143 fiat_p256_mulx_u32(&x606, &x607, x588, UINT32_C(0xffffffff));
1144 fiat_p256_mulx_u32(&x608, &x609, x588, UINT32_C(0xffffffff));
1145 fiat_p256_mulx_u32(&x610, &x611, x588, UINT32_C(0xffffffff));
1146 fiat_p256_mulx_u32(&x612, &x613, x588, UINT32_C(0xffffffff));
1147 fiat_p256_addcarryx_u32(&x614, &x615, 0x0, x613, x610);
1148 fiat_p256_addcarryx_u32(&x616, &x617, x615, x611, x608);
1149 x618 = (x617 + x609);
1150 fiat_p256_addcarryx_u32(&x619, &x620, 0x0, x588, x612);
1151 fiat_p256_addcarryx_u32(&x621, &x622, x620, x590, x614);
1152 fiat_p256_addcarryx_u32(&x623, &x624, x622, x592, x616);
1153 fiat_p256_addcarryx_u32(&x625, &x626, x624, x594, x618);
1154 fiat_p256_addcarryx_u32(&x627, &x628, x626, x596, 0x0);
1155 fiat_p256_addcarryx_u32(&x629, &x630, x628, x598, 0x0);
1156 fiat_p256_addcarryx_u32(&x631, &x632, x630, x600, x588);
1157 fiat_p256_addcarryx_u32(&x633, &x634, x632, x602, x606);
1158 fiat_p256_addcarryx_u32(&x635, &x636, x634, x604, x607);
1159 x637 = ((uint32_t)x636 + x605);
1160 fiat_p256_subborrowx_u32(&x638, &x639, 0x0, x621, UINT32_C(0xffffffff));
1161 fiat_p256_subborrowx_u32(&x640, &x641, x639, x623, UINT32_C(0xffffffff));
1162 fiat_p256_subborrowx_u32(&x642, &x643, x641, x625, UINT32_C(0xffffffff));
1163 fiat_p256_subborrowx_u32(&x644, &x645, x643, x627, 0x0);
1164 fiat_p256_subborrowx_u32(&x646, &x647, x645, x629, 0x0);
1165 fiat_p256_subborrowx_u32(&x648, &x649, x647, x631, 0x0);
1166 fiat_p256_subborrowx_u32(&x650, &x651, x649, x633, 0x1);
1167 fiat_p256_subborrowx_u32(&x652, &x653, x651, x635, UINT32_C(0xffffffff));
1168 fiat_p256_subborrowx_u32(&x654, &x655, x653, x637, 0x0);
1169 fiat_p256_cmovznz_u32(&x656, x655, x638, x621);
1170 fiat_p256_cmovznz_u32(&x657, x655, x640, x623);
1171 fiat_p256_cmovznz_u32(&x658, x655, x642, x625);
1172 fiat_p256_cmovznz_u32(&x659, x655, x644, x627);
1173 fiat_p256_cmovznz_u32(&x660, x655, x646, x629);
1174 fiat_p256_cmovznz_u32(&x661, x655, x648, x631);
1175 fiat_p256_cmovznz_u32(&x662, x655, x650, x633);
1176 fiat_p256_cmovznz_u32(&x663, x655, x652, x635);
1177 out1[0] = x656;
1178 out1[1] = x657;
1179 out1[2] = x658;
1180 out1[3] = x659;
1181 out1[4] = x660;
1182 out1[5] = x661;
1183 out1[6] = x662;
1184 out1[7] = x663;
1185 }
1186
1187 /*
1188 * The function fiat_p256_square squares a field element in the Montgomery domain.
1189 *
1190 * Preconditions:
1191 * 0 ≤ eval arg1 < m
1192 * Postconditions:
1193 * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
1194 * 0 ≤ eval out1 < m
1195 *
1196 */
fiat_p256_square(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1)1197 static FIAT_P256_FIAT_INLINE void fiat_p256_square(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1) {
1198 uint32_t x1;
1199 uint32_t x2;
1200 uint32_t x3;
1201 uint32_t x4;
1202 uint32_t x5;
1203 uint32_t x6;
1204 uint32_t x7;
1205 uint32_t x8;
1206 uint32_t x9;
1207 uint32_t x10;
1208 uint32_t x11;
1209 uint32_t x12;
1210 uint32_t x13;
1211 uint32_t x14;
1212 uint32_t x15;
1213 uint32_t x16;
1214 uint32_t x17;
1215 uint32_t x18;
1216 uint32_t x19;
1217 uint32_t x20;
1218 uint32_t x21;
1219 uint32_t x22;
1220 uint32_t x23;
1221 uint32_t x24;
1222 uint32_t x25;
1223 fiat_p256_uint1 x26;
1224 uint32_t x27;
1225 fiat_p256_uint1 x28;
1226 uint32_t x29;
1227 fiat_p256_uint1 x30;
1228 uint32_t x31;
1229 fiat_p256_uint1 x32;
1230 uint32_t x33;
1231 fiat_p256_uint1 x34;
1232 uint32_t x35;
1233 fiat_p256_uint1 x36;
1234 uint32_t x37;
1235 fiat_p256_uint1 x38;
1236 uint32_t x39;
1237 uint32_t x40;
1238 uint32_t x41;
1239 uint32_t x42;
1240 uint32_t x43;
1241 uint32_t x44;
1242 uint32_t x45;
1243 uint32_t x46;
1244 uint32_t x47;
1245 uint32_t x48;
1246 fiat_p256_uint1 x49;
1247 uint32_t x50;
1248 fiat_p256_uint1 x51;
1249 uint32_t x52;
1250 uint32_t x53;
1251 fiat_p256_uint1 x54;
1252 uint32_t x55;
1253 fiat_p256_uint1 x56;
1254 uint32_t x57;
1255 fiat_p256_uint1 x58;
1256 uint32_t x59;
1257 fiat_p256_uint1 x60;
1258 uint32_t x61;
1259 fiat_p256_uint1 x62;
1260 uint32_t x63;
1261 fiat_p256_uint1 x64;
1262 uint32_t x65;
1263 fiat_p256_uint1 x66;
1264 uint32_t x67;
1265 fiat_p256_uint1 x68;
1266 uint32_t x69;
1267 fiat_p256_uint1 x70;
1268 uint32_t x71;
1269 uint32_t x72;
1270 uint32_t x73;
1271 uint32_t x74;
1272 uint32_t x75;
1273 uint32_t x76;
1274 uint32_t x77;
1275 uint32_t x78;
1276 uint32_t x79;
1277 uint32_t x80;
1278 uint32_t x81;
1279 uint32_t x82;
1280 uint32_t x83;
1281 uint32_t x84;
1282 uint32_t x85;
1283 uint32_t x86;
1284 uint32_t x87;
1285 fiat_p256_uint1 x88;
1286 uint32_t x89;
1287 fiat_p256_uint1 x90;
1288 uint32_t x91;
1289 fiat_p256_uint1 x92;
1290 uint32_t x93;
1291 fiat_p256_uint1 x94;
1292 uint32_t x95;
1293 fiat_p256_uint1 x96;
1294 uint32_t x97;
1295 fiat_p256_uint1 x98;
1296 uint32_t x99;
1297 fiat_p256_uint1 x100;
1298 uint32_t x101;
1299 uint32_t x102;
1300 fiat_p256_uint1 x103;
1301 uint32_t x104;
1302 fiat_p256_uint1 x105;
1303 uint32_t x106;
1304 fiat_p256_uint1 x107;
1305 uint32_t x108;
1306 fiat_p256_uint1 x109;
1307 uint32_t x110;
1308 fiat_p256_uint1 x111;
1309 uint32_t x112;
1310 fiat_p256_uint1 x113;
1311 uint32_t x114;
1312 fiat_p256_uint1 x115;
1313 uint32_t x116;
1314 fiat_p256_uint1 x117;
1315 uint32_t x118;
1316 fiat_p256_uint1 x119;
1317 uint32_t x120;
1318 uint32_t x121;
1319 uint32_t x122;
1320 uint32_t x123;
1321 uint32_t x124;
1322 uint32_t x125;
1323 uint32_t x126;
1324 uint32_t x127;
1325 uint32_t x128;
1326 fiat_p256_uint1 x129;
1327 uint32_t x130;
1328 fiat_p256_uint1 x131;
1329 uint32_t x132;
1330 uint32_t x133;
1331 fiat_p256_uint1 x134;
1332 uint32_t x135;
1333 fiat_p256_uint1 x136;
1334 uint32_t x137;
1335 fiat_p256_uint1 x138;
1336 uint32_t x139;
1337 fiat_p256_uint1 x140;
1338 uint32_t x141;
1339 fiat_p256_uint1 x142;
1340 uint32_t x143;
1341 fiat_p256_uint1 x144;
1342 uint32_t x145;
1343 fiat_p256_uint1 x146;
1344 uint32_t x147;
1345 fiat_p256_uint1 x148;
1346 uint32_t x149;
1347 fiat_p256_uint1 x150;
1348 uint32_t x151;
1349 uint32_t x152;
1350 uint32_t x153;
1351 uint32_t x154;
1352 uint32_t x155;
1353 uint32_t x156;
1354 uint32_t x157;
1355 uint32_t x158;
1356 uint32_t x159;
1357 uint32_t x160;
1358 uint32_t x161;
1359 uint32_t x162;
1360 uint32_t x163;
1361 uint32_t x164;
1362 uint32_t x165;
1363 uint32_t x166;
1364 uint32_t x167;
1365 uint32_t x168;
1366 fiat_p256_uint1 x169;
1367 uint32_t x170;
1368 fiat_p256_uint1 x171;
1369 uint32_t x172;
1370 fiat_p256_uint1 x173;
1371 uint32_t x174;
1372 fiat_p256_uint1 x175;
1373 uint32_t x176;
1374 fiat_p256_uint1 x177;
1375 uint32_t x178;
1376 fiat_p256_uint1 x179;
1377 uint32_t x180;
1378 fiat_p256_uint1 x181;
1379 uint32_t x182;
1380 uint32_t x183;
1381 fiat_p256_uint1 x184;
1382 uint32_t x185;
1383 fiat_p256_uint1 x186;
1384 uint32_t x187;
1385 fiat_p256_uint1 x188;
1386 uint32_t x189;
1387 fiat_p256_uint1 x190;
1388 uint32_t x191;
1389 fiat_p256_uint1 x192;
1390 uint32_t x193;
1391 fiat_p256_uint1 x194;
1392 uint32_t x195;
1393 fiat_p256_uint1 x196;
1394 uint32_t x197;
1395 fiat_p256_uint1 x198;
1396 uint32_t x199;
1397 fiat_p256_uint1 x200;
1398 uint32_t x201;
1399 uint32_t x202;
1400 uint32_t x203;
1401 uint32_t x204;
1402 uint32_t x205;
1403 uint32_t x206;
1404 uint32_t x207;
1405 uint32_t x208;
1406 uint32_t x209;
1407 fiat_p256_uint1 x210;
1408 uint32_t x211;
1409 fiat_p256_uint1 x212;
1410 uint32_t x213;
1411 uint32_t x214;
1412 fiat_p256_uint1 x215;
1413 uint32_t x216;
1414 fiat_p256_uint1 x217;
1415 uint32_t x218;
1416 fiat_p256_uint1 x219;
1417 uint32_t x220;
1418 fiat_p256_uint1 x221;
1419 uint32_t x222;
1420 fiat_p256_uint1 x223;
1421 uint32_t x224;
1422 fiat_p256_uint1 x225;
1423 uint32_t x226;
1424 fiat_p256_uint1 x227;
1425 uint32_t x228;
1426 fiat_p256_uint1 x229;
1427 uint32_t x230;
1428 fiat_p256_uint1 x231;
1429 uint32_t x232;
1430 uint32_t x233;
1431 uint32_t x234;
1432 uint32_t x235;
1433 uint32_t x236;
1434 uint32_t x237;
1435 uint32_t x238;
1436 uint32_t x239;
1437 uint32_t x240;
1438 uint32_t x241;
1439 uint32_t x242;
1440 uint32_t x243;
1441 uint32_t x244;
1442 uint32_t x245;
1443 uint32_t x246;
1444 uint32_t x247;
1445 uint32_t x248;
1446 uint32_t x249;
1447 fiat_p256_uint1 x250;
1448 uint32_t x251;
1449 fiat_p256_uint1 x252;
1450 uint32_t x253;
1451 fiat_p256_uint1 x254;
1452 uint32_t x255;
1453 fiat_p256_uint1 x256;
1454 uint32_t x257;
1455 fiat_p256_uint1 x258;
1456 uint32_t x259;
1457 fiat_p256_uint1 x260;
1458 uint32_t x261;
1459 fiat_p256_uint1 x262;
1460 uint32_t x263;
1461 uint32_t x264;
1462 fiat_p256_uint1 x265;
1463 uint32_t x266;
1464 fiat_p256_uint1 x267;
1465 uint32_t x268;
1466 fiat_p256_uint1 x269;
1467 uint32_t x270;
1468 fiat_p256_uint1 x271;
1469 uint32_t x272;
1470 fiat_p256_uint1 x273;
1471 uint32_t x274;
1472 fiat_p256_uint1 x275;
1473 uint32_t x276;
1474 fiat_p256_uint1 x277;
1475 uint32_t x278;
1476 fiat_p256_uint1 x279;
1477 uint32_t x280;
1478 fiat_p256_uint1 x281;
1479 uint32_t x282;
1480 uint32_t x283;
1481 uint32_t x284;
1482 uint32_t x285;
1483 uint32_t x286;
1484 uint32_t x287;
1485 uint32_t x288;
1486 uint32_t x289;
1487 uint32_t x290;
1488 fiat_p256_uint1 x291;
1489 uint32_t x292;
1490 fiat_p256_uint1 x293;
1491 uint32_t x294;
1492 uint32_t x295;
1493 fiat_p256_uint1 x296;
1494 uint32_t x297;
1495 fiat_p256_uint1 x298;
1496 uint32_t x299;
1497 fiat_p256_uint1 x300;
1498 uint32_t x301;
1499 fiat_p256_uint1 x302;
1500 uint32_t x303;
1501 fiat_p256_uint1 x304;
1502 uint32_t x305;
1503 fiat_p256_uint1 x306;
1504 uint32_t x307;
1505 fiat_p256_uint1 x308;
1506 uint32_t x309;
1507 fiat_p256_uint1 x310;
1508 uint32_t x311;
1509 fiat_p256_uint1 x312;
1510 uint32_t x313;
1511 uint32_t x314;
1512 uint32_t x315;
1513 uint32_t x316;
1514 uint32_t x317;
1515 uint32_t x318;
1516 uint32_t x319;
1517 uint32_t x320;
1518 uint32_t x321;
1519 uint32_t x322;
1520 uint32_t x323;
1521 uint32_t x324;
1522 uint32_t x325;
1523 uint32_t x326;
1524 uint32_t x327;
1525 uint32_t x328;
1526 uint32_t x329;
1527 uint32_t x330;
1528 fiat_p256_uint1 x331;
1529 uint32_t x332;
1530 fiat_p256_uint1 x333;
1531 uint32_t x334;
1532 fiat_p256_uint1 x335;
1533 uint32_t x336;
1534 fiat_p256_uint1 x337;
1535 uint32_t x338;
1536 fiat_p256_uint1 x339;
1537 uint32_t x340;
1538 fiat_p256_uint1 x341;
1539 uint32_t x342;
1540 fiat_p256_uint1 x343;
1541 uint32_t x344;
1542 uint32_t x345;
1543 fiat_p256_uint1 x346;
1544 uint32_t x347;
1545 fiat_p256_uint1 x348;
1546 uint32_t x349;
1547 fiat_p256_uint1 x350;
1548 uint32_t x351;
1549 fiat_p256_uint1 x352;
1550 uint32_t x353;
1551 fiat_p256_uint1 x354;
1552 uint32_t x355;
1553 fiat_p256_uint1 x356;
1554 uint32_t x357;
1555 fiat_p256_uint1 x358;
1556 uint32_t x359;
1557 fiat_p256_uint1 x360;
1558 uint32_t x361;
1559 fiat_p256_uint1 x362;
1560 uint32_t x363;
1561 uint32_t x364;
1562 uint32_t x365;
1563 uint32_t x366;
1564 uint32_t x367;
1565 uint32_t x368;
1566 uint32_t x369;
1567 uint32_t x370;
1568 uint32_t x371;
1569 fiat_p256_uint1 x372;
1570 uint32_t x373;
1571 fiat_p256_uint1 x374;
1572 uint32_t x375;
1573 uint32_t x376;
1574 fiat_p256_uint1 x377;
1575 uint32_t x378;
1576 fiat_p256_uint1 x379;
1577 uint32_t x380;
1578 fiat_p256_uint1 x381;
1579 uint32_t x382;
1580 fiat_p256_uint1 x383;
1581 uint32_t x384;
1582 fiat_p256_uint1 x385;
1583 uint32_t x386;
1584 fiat_p256_uint1 x387;
1585 uint32_t x388;
1586 fiat_p256_uint1 x389;
1587 uint32_t x390;
1588 fiat_p256_uint1 x391;
1589 uint32_t x392;
1590 fiat_p256_uint1 x393;
1591 uint32_t x394;
1592 uint32_t x395;
1593 uint32_t x396;
1594 uint32_t x397;
1595 uint32_t x398;
1596 uint32_t x399;
1597 uint32_t x400;
1598 uint32_t x401;
1599 uint32_t x402;
1600 uint32_t x403;
1601 uint32_t x404;
1602 uint32_t x405;
1603 uint32_t x406;
1604 uint32_t x407;
1605 uint32_t x408;
1606 uint32_t x409;
1607 uint32_t x410;
1608 uint32_t x411;
1609 fiat_p256_uint1 x412;
1610 uint32_t x413;
1611 fiat_p256_uint1 x414;
1612 uint32_t x415;
1613 fiat_p256_uint1 x416;
1614 uint32_t x417;
1615 fiat_p256_uint1 x418;
1616 uint32_t x419;
1617 fiat_p256_uint1 x420;
1618 uint32_t x421;
1619 fiat_p256_uint1 x422;
1620 uint32_t x423;
1621 fiat_p256_uint1 x424;
1622 uint32_t x425;
1623 uint32_t x426;
1624 fiat_p256_uint1 x427;
1625 uint32_t x428;
1626 fiat_p256_uint1 x429;
1627 uint32_t x430;
1628 fiat_p256_uint1 x431;
1629 uint32_t x432;
1630 fiat_p256_uint1 x433;
1631 uint32_t x434;
1632 fiat_p256_uint1 x435;
1633 uint32_t x436;
1634 fiat_p256_uint1 x437;
1635 uint32_t x438;
1636 fiat_p256_uint1 x439;
1637 uint32_t x440;
1638 fiat_p256_uint1 x441;
1639 uint32_t x442;
1640 fiat_p256_uint1 x443;
1641 uint32_t x444;
1642 uint32_t x445;
1643 uint32_t x446;
1644 uint32_t x447;
1645 uint32_t x448;
1646 uint32_t x449;
1647 uint32_t x450;
1648 uint32_t x451;
1649 uint32_t x452;
1650 fiat_p256_uint1 x453;
1651 uint32_t x454;
1652 fiat_p256_uint1 x455;
1653 uint32_t x456;
1654 uint32_t x457;
1655 fiat_p256_uint1 x458;
1656 uint32_t x459;
1657 fiat_p256_uint1 x460;
1658 uint32_t x461;
1659 fiat_p256_uint1 x462;
1660 uint32_t x463;
1661 fiat_p256_uint1 x464;
1662 uint32_t x465;
1663 fiat_p256_uint1 x466;
1664 uint32_t x467;
1665 fiat_p256_uint1 x468;
1666 uint32_t x469;
1667 fiat_p256_uint1 x470;
1668 uint32_t x471;
1669 fiat_p256_uint1 x472;
1670 uint32_t x473;
1671 fiat_p256_uint1 x474;
1672 uint32_t x475;
1673 uint32_t x476;
1674 uint32_t x477;
1675 uint32_t x478;
1676 uint32_t x479;
1677 uint32_t x480;
1678 uint32_t x481;
1679 uint32_t x482;
1680 uint32_t x483;
1681 uint32_t x484;
1682 uint32_t x485;
1683 uint32_t x486;
1684 uint32_t x487;
1685 uint32_t x488;
1686 uint32_t x489;
1687 uint32_t x490;
1688 uint32_t x491;
1689 uint32_t x492;
1690 fiat_p256_uint1 x493;
1691 uint32_t x494;
1692 fiat_p256_uint1 x495;
1693 uint32_t x496;
1694 fiat_p256_uint1 x497;
1695 uint32_t x498;
1696 fiat_p256_uint1 x499;
1697 uint32_t x500;
1698 fiat_p256_uint1 x501;
1699 uint32_t x502;
1700 fiat_p256_uint1 x503;
1701 uint32_t x504;
1702 fiat_p256_uint1 x505;
1703 uint32_t x506;
1704 uint32_t x507;
1705 fiat_p256_uint1 x508;
1706 uint32_t x509;
1707 fiat_p256_uint1 x510;
1708 uint32_t x511;
1709 fiat_p256_uint1 x512;
1710 uint32_t x513;
1711 fiat_p256_uint1 x514;
1712 uint32_t x515;
1713 fiat_p256_uint1 x516;
1714 uint32_t x517;
1715 fiat_p256_uint1 x518;
1716 uint32_t x519;
1717 fiat_p256_uint1 x520;
1718 uint32_t x521;
1719 fiat_p256_uint1 x522;
1720 uint32_t x523;
1721 fiat_p256_uint1 x524;
1722 uint32_t x525;
1723 uint32_t x526;
1724 uint32_t x527;
1725 uint32_t x528;
1726 uint32_t x529;
1727 uint32_t x530;
1728 uint32_t x531;
1729 uint32_t x532;
1730 uint32_t x533;
1731 fiat_p256_uint1 x534;
1732 uint32_t x535;
1733 fiat_p256_uint1 x536;
1734 uint32_t x537;
1735 uint32_t x538;
1736 fiat_p256_uint1 x539;
1737 uint32_t x540;
1738 fiat_p256_uint1 x541;
1739 uint32_t x542;
1740 fiat_p256_uint1 x543;
1741 uint32_t x544;
1742 fiat_p256_uint1 x545;
1743 uint32_t x546;
1744 fiat_p256_uint1 x547;
1745 uint32_t x548;
1746 fiat_p256_uint1 x549;
1747 uint32_t x550;
1748 fiat_p256_uint1 x551;
1749 uint32_t x552;
1750 fiat_p256_uint1 x553;
1751 uint32_t x554;
1752 fiat_p256_uint1 x555;
1753 uint32_t x556;
1754 uint32_t x557;
1755 uint32_t x558;
1756 uint32_t x559;
1757 uint32_t x560;
1758 uint32_t x561;
1759 uint32_t x562;
1760 uint32_t x563;
1761 uint32_t x564;
1762 uint32_t x565;
1763 uint32_t x566;
1764 uint32_t x567;
1765 uint32_t x568;
1766 uint32_t x569;
1767 uint32_t x570;
1768 uint32_t x571;
1769 uint32_t x572;
1770 uint32_t x573;
1771 fiat_p256_uint1 x574;
1772 uint32_t x575;
1773 fiat_p256_uint1 x576;
1774 uint32_t x577;
1775 fiat_p256_uint1 x578;
1776 uint32_t x579;
1777 fiat_p256_uint1 x580;
1778 uint32_t x581;
1779 fiat_p256_uint1 x582;
1780 uint32_t x583;
1781 fiat_p256_uint1 x584;
1782 uint32_t x585;
1783 fiat_p256_uint1 x586;
1784 uint32_t x587;
1785 uint32_t x588;
1786 fiat_p256_uint1 x589;
1787 uint32_t x590;
1788 fiat_p256_uint1 x591;
1789 uint32_t x592;
1790 fiat_p256_uint1 x593;
1791 uint32_t x594;
1792 fiat_p256_uint1 x595;
1793 uint32_t x596;
1794 fiat_p256_uint1 x597;
1795 uint32_t x598;
1796 fiat_p256_uint1 x599;
1797 uint32_t x600;
1798 fiat_p256_uint1 x601;
1799 uint32_t x602;
1800 fiat_p256_uint1 x603;
1801 uint32_t x604;
1802 fiat_p256_uint1 x605;
1803 uint32_t x606;
1804 uint32_t x607;
1805 uint32_t x608;
1806 uint32_t x609;
1807 uint32_t x610;
1808 uint32_t x611;
1809 uint32_t x612;
1810 uint32_t x613;
1811 uint32_t x614;
1812 fiat_p256_uint1 x615;
1813 uint32_t x616;
1814 fiat_p256_uint1 x617;
1815 uint32_t x618;
1816 uint32_t x619;
1817 fiat_p256_uint1 x620;
1818 uint32_t x621;
1819 fiat_p256_uint1 x622;
1820 uint32_t x623;
1821 fiat_p256_uint1 x624;
1822 uint32_t x625;
1823 fiat_p256_uint1 x626;
1824 uint32_t x627;
1825 fiat_p256_uint1 x628;
1826 uint32_t x629;
1827 fiat_p256_uint1 x630;
1828 uint32_t x631;
1829 fiat_p256_uint1 x632;
1830 uint32_t x633;
1831 fiat_p256_uint1 x634;
1832 uint32_t x635;
1833 fiat_p256_uint1 x636;
1834 uint32_t x637;
1835 uint32_t x638;
1836 fiat_p256_uint1 x639;
1837 uint32_t x640;
1838 fiat_p256_uint1 x641;
1839 uint32_t x642;
1840 fiat_p256_uint1 x643;
1841 uint32_t x644;
1842 fiat_p256_uint1 x645;
1843 uint32_t x646;
1844 fiat_p256_uint1 x647;
1845 uint32_t x648;
1846 fiat_p256_uint1 x649;
1847 uint32_t x650;
1848 fiat_p256_uint1 x651;
1849 uint32_t x652;
1850 fiat_p256_uint1 x653;
1851 uint32_t x654;
1852 fiat_p256_uint1 x655;
1853 uint32_t x656;
1854 uint32_t x657;
1855 uint32_t x658;
1856 uint32_t x659;
1857 uint32_t x660;
1858 uint32_t x661;
1859 uint32_t x662;
1860 uint32_t x663;
1861 x1 = (arg1[1]);
1862 x2 = (arg1[2]);
1863 x3 = (arg1[3]);
1864 x4 = (arg1[4]);
1865 x5 = (arg1[5]);
1866 x6 = (arg1[6]);
1867 x7 = (arg1[7]);
1868 x8 = (arg1[0]);
1869 fiat_p256_mulx_u32(&x9, &x10, x8, (arg1[7]));
1870 fiat_p256_mulx_u32(&x11, &x12, x8, (arg1[6]));
1871 fiat_p256_mulx_u32(&x13, &x14, x8, (arg1[5]));
1872 fiat_p256_mulx_u32(&x15, &x16, x8, (arg1[4]));
1873 fiat_p256_mulx_u32(&x17, &x18, x8, (arg1[3]));
1874 fiat_p256_mulx_u32(&x19, &x20, x8, (arg1[2]));
1875 fiat_p256_mulx_u32(&x21, &x22, x8, (arg1[1]));
1876 fiat_p256_mulx_u32(&x23, &x24, x8, (arg1[0]));
1877 fiat_p256_addcarryx_u32(&x25, &x26, 0x0, x24, x21);
1878 fiat_p256_addcarryx_u32(&x27, &x28, x26, x22, x19);
1879 fiat_p256_addcarryx_u32(&x29, &x30, x28, x20, x17);
1880 fiat_p256_addcarryx_u32(&x31, &x32, x30, x18, x15);
1881 fiat_p256_addcarryx_u32(&x33, &x34, x32, x16, x13);
1882 fiat_p256_addcarryx_u32(&x35, &x36, x34, x14, x11);
1883 fiat_p256_addcarryx_u32(&x37, &x38, x36, x12, x9);
1884 x39 = (x38 + x10);
1885 fiat_p256_mulx_u32(&x40, &x41, x23, UINT32_C(0xffffffff));
1886 fiat_p256_mulx_u32(&x42, &x43, x23, UINT32_C(0xffffffff));
1887 fiat_p256_mulx_u32(&x44, &x45, x23, UINT32_C(0xffffffff));
1888 fiat_p256_mulx_u32(&x46, &x47, x23, UINT32_C(0xffffffff));
1889 fiat_p256_addcarryx_u32(&x48, &x49, 0x0, x47, x44);
1890 fiat_p256_addcarryx_u32(&x50, &x51, x49, x45, x42);
1891 x52 = (x51 + x43);
1892 fiat_p256_addcarryx_u32(&x53, &x54, 0x0, x23, x46);
1893 fiat_p256_addcarryx_u32(&x55, &x56, x54, x25, x48);
1894 fiat_p256_addcarryx_u32(&x57, &x58, x56, x27, x50);
1895 fiat_p256_addcarryx_u32(&x59, &x60, x58, x29, x52);
1896 fiat_p256_addcarryx_u32(&x61, &x62, x60, x31, 0x0);
1897 fiat_p256_addcarryx_u32(&x63, &x64, x62, x33, 0x0);
1898 fiat_p256_addcarryx_u32(&x65, &x66, x64, x35, x23);
1899 fiat_p256_addcarryx_u32(&x67, &x68, x66, x37, x40);
1900 fiat_p256_addcarryx_u32(&x69, &x70, x68, x39, x41);
1901 fiat_p256_mulx_u32(&x71, &x72, x1, (arg1[7]));
1902 fiat_p256_mulx_u32(&x73, &x74, x1, (arg1[6]));
1903 fiat_p256_mulx_u32(&x75, &x76, x1, (arg1[5]));
1904 fiat_p256_mulx_u32(&x77, &x78, x1, (arg1[4]));
1905 fiat_p256_mulx_u32(&x79, &x80, x1, (arg1[3]));
1906 fiat_p256_mulx_u32(&x81, &x82, x1, (arg1[2]));
1907 fiat_p256_mulx_u32(&x83, &x84, x1, (arg1[1]));
1908 fiat_p256_mulx_u32(&x85, &x86, x1, (arg1[0]));
1909 fiat_p256_addcarryx_u32(&x87, &x88, 0x0, x86, x83);
1910 fiat_p256_addcarryx_u32(&x89, &x90, x88, x84, x81);
1911 fiat_p256_addcarryx_u32(&x91, &x92, x90, x82, x79);
1912 fiat_p256_addcarryx_u32(&x93, &x94, x92, x80, x77);
1913 fiat_p256_addcarryx_u32(&x95, &x96, x94, x78, x75);
1914 fiat_p256_addcarryx_u32(&x97, &x98, x96, x76, x73);
1915 fiat_p256_addcarryx_u32(&x99, &x100, x98, x74, x71);
1916 x101 = (x100 + x72);
1917 fiat_p256_addcarryx_u32(&x102, &x103, 0x0, x55, x85);
1918 fiat_p256_addcarryx_u32(&x104, &x105, x103, x57, x87);
1919 fiat_p256_addcarryx_u32(&x106, &x107, x105, x59, x89);
1920 fiat_p256_addcarryx_u32(&x108, &x109, x107, x61, x91);
1921 fiat_p256_addcarryx_u32(&x110, &x111, x109, x63, x93);
1922 fiat_p256_addcarryx_u32(&x112, &x113, x111, x65, x95);
1923 fiat_p256_addcarryx_u32(&x114, &x115, x113, x67, x97);
1924 fiat_p256_addcarryx_u32(&x116, &x117, x115, x69, x99);
1925 fiat_p256_addcarryx_u32(&x118, &x119, x117, x70, x101);
1926 fiat_p256_mulx_u32(&x120, &x121, x102, UINT32_C(0xffffffff));
1927 fiat_p256_mulx_u32(&x122, &x123, x102, UINT32_C(0xffffffff));
1928 fiat_p256_mulx_u32(&x124, &x125, x102, UINT32_C(0xffffffff));
1929 fiat_p256_mulx_u32(&x126, &x127, x102, UINT32_C(0xffffffff));
1930 fiat_p256_addcarryx_u32(&x128, &x129, 0x0, x127, x124);
1931 fiat_p256_addcarryx_u32(&x130, &x131, x129, x125, x122);
1932 x132 = (x131 + x123);
1933 fiat_p256_addcarryx_u32(&x133, &x134, 0x0, x102, x126);
1934 fiat_p256_addcarryx_u32(&x135, &x136, x134, x104, x128);
1935 fiat_p256_addcarryx_u32(&x137, &x138, x136, x106, x130);
1936 fiat_p256_addcarryx_u32(&x139, &x140, x138, x108, x132);
1937 fiat_p256_addcarryx_u32(&x141, &x142, x140, x110, 0x0);
1938 fiat_p256_addcarryx_u32(&x143, &x144, x142, x112, 0x0);
1939 fiat_p256_addcarryx_u32(&x145, &x146, x144, x114, x102);
1940 fiat_p256_addcarryx_u32(&x147, &x148, x146, x116, x120);
1941 fiat_p256_addcarryx_u32(&x149, &x150, x148, x118, x121);
1942 x151 = ((uint32_t)x150 + x119);
1943 fiat_p256_mulx_u32(&x152, &x153, x2, (arg1[7]));
1944 fiat_p256_mulx_u32(&x154, &x155, x2, (arg1[6]));
1945 fiat_p256_mulx_u32(&x156, &x157, x2, (arg1[5]));
1946 fiat_p256_mulx_u32(&x158, &x159, x2, (arg1[4]));
1947 fiat_p256_mulx_u32(&x160, &x161, x2, (arg1[3]));
1948 fiat_p256_mulx_u32(&x162, &x163, x2, (arg1[2]));
1949 fiat_p256_mulx_u32(&x164, &x165, x2, (arg1[1]));
1950 fiat_p256_mulx_u32(&x166, &x167, x2, (arg1[0]));
1951 fiat_p256_addcarryx_u32(&x168, &x169, 0x0, x167, x164);
1952 fiat_p256_addcarryx_u32(&x170, &x171, x169, x165, x162);
1953 fiat_p256_addcarryx_u32(&x172, &x173, x171, x163, x160);
1954 fiat_p256_addcarryx_u32(&x174, &x175, x173, x161, x158);
1955 fiat_p256_addcarryx_u32(&x176, &x177, x175, x159, x156);
1956 fiat_p256_addcarryx_u32(&x178, &x179, x177, x157, x154);
1957 fiat_p256_addcarryx_u32(&x180, &x181, x179, x155, x152);
1958 x182 = (x181 + x153);
1959 fiat_p256_addcarryx_u32(&x183, &x184, 0x0, x135, x166);
1960 fiat_p256_addcarryx_u32(&x185, &x186, x184, x137, x168);
1961 fiat_p256_addcarryx_u32(&x187, &x188, x186, x139, x170);
1962 fiat_p256_addcarryx_u32(&x189, &x190, x188, x141, x172);
1963 fiat_p256_addcarryx_u32(&x191, &x192, x190, x143, x174);
1964 fiat_p256_addcarryx_u32(&x193, &x194, x192, x145, x176);
1965 fiat_p256_addcarryx_u32(&x195, &x196, x194, x147, x178);
1966 fiat_p256_addcarryx_u32(&x197, &x198, x196, x149, x180);
1967 fiat_p256_addcarryx_u32(&x199, &x200, x198, x151, x182);
1968 fiat_p256_mulx_u32(&x201, &x202, x183, UINT32_C(0xffffffff));
1969 fiat_p256_mulx_u32(&x203, &x204, x183, UINT32_C(0xffffffff));
1970 fiat_p256_mulx_u32(&x205, &x206, x183, UINT32_C(0xffffffff));
1971 fiat_p256_mulx_u32(&x207, &x208, x183, UINT32_C(0xffffffff));
1972 fiat_p256_addcarryx_u32(&x209, &x210, 0x0, x208, x205);
1973 fiat_p256_addcarryx_u32(&x211, &x212, x210, x206, x203);
1974 x213 = (x212 + x204);
1975 fiat_p256_addcarryx_u32(&x214, &x215, 0x0, x183, x207);
1976 fiat_p256_addcarryx_u32(&x216, &x217, x215, x185, x209);
1977 fiat_p256_addcarryx_u32(&x218, &x219, x217, x187, x211);
1978 fiat_p256_addcarryx_u32(&x220, &x221, x219, x189, x213);
1979 fiat_p256_addcarryx_u32(&x222, &x223, x221, x191, 0x0);
1980 fiat_p256_addcarryx_u32(&x224, &x225, x223, x193, 0x0);
1981 fiat_p256_addcarryx_u32(&x226, &x227, x225, x195, x183);
1982 fiat_p256_addcarryx_u32(&x228, &x229, x227, x197, x201);
1983 fiat_p256_addcarryx_u32(&x230, &x231, x229, x199, x202);
1984 x232 = ((uint32_t)x231 + x200);
1985 fiat_p256_mulx_u32(&x233, &x234, x3, (arg1[7]));
1986 fiat_p256_mulx_u32(&x235, &x236, x3, (arg1[6]));
1987 fiat_p256_mulx_u32(&x237, &x238, x3, (arg1[5]));
1988 fiat_p256_mulx_u32(&x239, &x240, x3, (arg1[4]));
1989 fiat_p256_mulx_u32(&x241, &x242, x3, (arg1[3]));
1990 fiat_p256_mulx_u32(&x243, &x244, x3, (arg1[2]));
1991 fiat_p256_mulx_u32(&x245, &x246, x3, (arg1[1]));
1992 fiat_p256_mulx_u32(&x247, &x248, x3, (arg1[0]));
1993 fiat_p256_addcarryx_u32(&x249, &x250, 0x0, x248, x245);
1994 fiat_p256_addcarryx_u32(&x251, &x252, x250, x246, x243);
1995 fiat_p256_addcarryx_u32(&x253, &x254, x252, x244, x241);
1996 fiat_p256_addcarryx_u32(&x255, &x256, x254, x242, x239);
1997 fiat_p256_addcarryx_u32(&x257, &x258, x256, x240, x237);
1998 fiat_p256_addcarryx_u32(&x259, &x260, x258, x238, x235);
1999 fiat_p256_addcarryx_u32(&x261, &x262, x260, x236, x233);
2000 x263 = (x262 + x234);
2001 fiat_p256_addcarryx_u32(&x264, &x265, 0x0, x216, x247);
2002 fiat_p256_addcarryx_u32(&x266, &x267, x265, x218, x249);
2003 fiat_p256_addcarryx_u32(&x268, &x269, x267, x220, x251);
2004 fiat_p256_addcarryx_u32(&x270, &x271, x269, x222, x253);
2005 fiat_p256_addcarryx_u32(&x272, &x273, x271, x224, x255);
2006 fiat_p256_addcarryx_u32(&x274, &x275, x273, x226, x257);
2007 fiat_p256_addcarryx_u32(&x276, &x277, x275, x228, x259);
2008 fiat_p256_addcarryx_u32(&x278, &x279, x277, x230, x261);
2009 fiat_p256_addcarryx_u32(&x280, &x281, x279, x232, x263);
2010 fiat_p256_mulx_u32(&x282, &x283, x264, UINT32_C(0xffffffff));
2011 fiat_p256_mulx_u32(&x284, &x285, x264, UINT32_C(0xffffffff));
2012 fiat_p256_mulx_u32(&x286, &x287, x264, UINT32_C(0xffffffff));
2013 fiat_p256_mulx_u32(&x288, &x289, x264, UINT32_C(0xffffffff));
2014 fiat_p256_addcarryx_u32(&x290, &x291, 0x0, x289, x286);
2015 fiat_p256_addcarryx_u32(&x292, &x293, x291, x287, x284);
2016 x294 = (x293 + x285);
2017 fiat_p256_addcarryx_u32(&x295, &x296, 0x0, x264, x288);
2018 fiat_p256_addcarryx_u32(&x297, &x298, x296, x266, x290);
2019 fiat_p256_addcarryx_u32(&x299, &x300, x298, x268, x292);
2020 fiat_p256_addcarryx_u32(&x301, &x302, x300, x270, x294);
2021 fiat_p256_addcarryx_u32(&x303, &x304, x302, x272, 0x0);
2022 fiat_p256_addcarryx_u32(&x305, &x306, x304, x274, 0x0);
2023 fiat_p256_addcarryx_u32(&x307, &x308, x306, x276, x264);
2024 fiat_p256_addcarryx_u32(&x309, &x310, x308, x278, x282);
2025 fiat_p256_addcarryx_u32(&x311, &x312, x310, x280, x283);
2026 x313 = ((uint32_t)x312 + x281);
2027 fiat_p256_mulx_u32(&x314, &x315, x4, (arg1[7]));
2028 fiat_p256_mulx_u32(&x316, &x317, x4, (arg1[6]));
2029 fiat_p256_mulx_u32(&x318, &x319, x4, (arg1[5]));
2030 fiat_p256_mulx_u32(&x320, &x321, x4, (arg1[4]));
2031 fiat_p256_mulx_u32(&x322, &x323, x4, (arg1[3]));
2032 fiat_p256_mulx_u32(&x324, &x325, x4, (arg1[2]));
2033 fiat_p256_mulx_u32(&x326, &x327, x4, (arg1[1]));
2034 fiat_p256_mulx_u32(&x328, &x329, x4, (arg1[0]));
2035 fiat_p256_addcarryx_u32(&x330, &x331, 0x0, x329, x326);
2036 fiat_p256_addcarryx_u32(&x332, &x333, x331, x327, x324);
2037 fiat_p256_addcarryx_u32(&x334, &x335, x333, x325, x322);
2038 fiat_p256_addcarryx_u32(&x336, &x337, x335, x323, x320);
2039 fiat_p256_addcarryx_u32(&x338, &x339, x337, x321, x318);
2040 fiat_p256_addcarryx_u32(&x340, &x341, x339, x319, x316);
2041 fiat_p256_addcarryx_u32(&x342, &x343, x341, x317, x314);
2042 x344 = (x343 + x315);
2043 fiat_p256_addcarryx_u32(&x345, &x346, 0x0, x297, x328);
2044 fiat_p256_addcarryx_u32(&x347, &x348, x346, x299, x330);
2045 fiat_p256_addcarryx_u32(&x349, &x350, x348, x301, x332);
2046 fiat_p256_addcarryx_u32(&x351, &x352, x350, x303, x334);
2047 fiat_p256_addcarryx_u32(&x353, &x354, x352, x305, x336);
2048 fiat_p256_addcarryx_u32(&x355, &x356, x354, x307, x338);
2049 fiat_p256_addcarryx_u32(&x357, &x358, x356, x309, x340);
2050 fiat_p256_addcarryx_u32(&x359, &x360, x358, x311, x342);
2051 fiat_p256_addcarryx_u32(&x361, &x362, x360, x313, x344);
2052 fiat_p256_mulx_u32(&x363, &x364, x345, UINT32_C(0xffffffff));
2053 fiat_p256_mulx_u32(&x365, &x366, x345, UINT32_C(0xffffffff));
2054 fiat_p256_mulx_u32(&x367, &x368, x345, UINT32_C(0xffffffff));
2055 fiat_p256_mulx_u32(&x369, &x370, x345, UINT32_C(0xffffffff));
2056 fiat_p256_addcarryx_u32(&x371, &x372, 0x0, x370, x367);
2057 fiat_p256_addcarryx_u32(&x373, &x374, x372, x368, x365);
2058 x375 = (x374 + x366);
2059 fiat_p256_addcarryx_u32(&x376, &x377, 0x0, x345, x369);
2060 fiat_p256_addcarryx_u32(&x378, &x379, x377, x347, x371);
2061 fiat_p256_addcarryx_u32(&x380, &x381, x379, x349, x373);
2062 fiat_p256_addcarryx_u32(&x382, &x383, x381, x351, x375);
2063 fiat_p256_addcarryx_u32(&x384, &x385, x383, x353, 0x0);
2064 fiat_p256_addcarryx_u32(&x386, &x387, x385, x355, 0x0);
2065 fiat_p256_addcarryx_u32(&x388, &x389, x387, x357, x345);
2066 fiat_p256_addcarryx_u32(&x390, &x391, x389, x359, x363);
2067 fiat_p256_addcarryx_u32(&x392, &x393, x391, x361, x364);
2068 x394 = ((uint32_t)x393 + x362);
2069 fiat_p256_mulx_u32(&x395, &x396, x5, (arg1[7]));
2070 fiat_p256_mulx_u32(&x397, &x398, x5, (arg1[6]));
2071 fiat_p256_mulx_u32(&x399, &x400, x5, (arg1[5]));
2072 fiat_p256_mulx_u32(&x401, &x402, x5, (arg1[4]));
2073 fiat_p256_mulx_u32(&x403, &x404, x5, (arg1[3]));
2074 fiat_p256_mulx_u32(&x405, &x406, x5, (arg1[2]));
2075 fiat_p256_mulx_u32(&x407, &x408, x5, (arg1[1]));
2076 fiat_p256_mulx_u32(&x409, &x410, x5, (arg1[0]));
2077 fiat_p256_addcarryx_u32(&x411, &x412, 0x0, x410, x407);
2078 fiat_p256_addcarryx_u32(&x413, &x414, x412, x408, x405);
2079 fiat_p256_addcarryx_u32(&x415, &x416, x414, x406, x403);
2080 fiat_p256_addcarryx_u32(&x417, &x418, x416, x404, x401);
2081 fiat_p256_addcarryx_u32(&x419, &x420, x418, x402, x399);
2082 fiat_p256_addcarryx_u32(&x421, &x422, x420, x400, x397);
2083 fiat_p256_addcarryx_u32(&x423, &x424, x422, x398, x395);
2084 x425 = (x424 + x396);
2085 fiat_p256_addcarryx_u32(&x426, &x427, 0x0, x378, x409);
2086 fiat_p256_addcarryx_u32(&x428, &x429, x427, x380, x411);
2087 fiat_p256_addcarryx_u32(&x430, &x431, x429, x382, x413);
2088 fiat_p256_addcarryx_u32(&x432, &x433, x431, x384, x415);
2089 fiat_p256_addcarryx_u32(&x434, &x435, x433, x386, x417);
2090 fiat_p256_addcarryx_u32(&x436, &x437, x435, x388, x419);
2091 fiat_p256_addcarryx_u32(&x438, &x439, x437, x390, x421);
2092 fiat_p256_addcarryx_u32(&x440, &x441, x439, x392, x423);
2093 fiat_p256_addcarryx_u32(&x442, &x443, x441, x394, x425);
2094 fiat_p256_mulx_u32(&x444, &x445, x426, UINT32_C(0xffffffff));
2095 fiat_p256_mulx_u32(&x446, &x447, x426, UINT32_C(0xffffffff));
2096 fiat_p256_mulx_u32(&x448, &x449, x426, UINT32_C(0xffffffff));
2097 fiat_p256_mulx_u32(&x450, &x451, x426, UINT32_C(0xffffffff));
2098 fiat_p256_addcarryx_u32(&x452, &x453, 0x0, x451, x448);
2099 fiat_p256_addcarryx_u32(&x454, &x455, x453, x449, x446);
2100 x456 = (x455 + x447);
2101 fiat_p256_addcarryx_u32(&x457, &x458, 0x0, x426, x450);
2102 fiat_p256_addcarryx_u32(&x459, &x460, x458, x428, x452);
2103 fiat_p256_addcarryx_u32(&x461, &x462, x460, x430, x454);
2104 fiat_p256_addcarryx_u32(&x463, &x464, x462, x432, x456);
2105 fiat_p256_addcarryx_u32(&x465, &x466, x464, x434, 0x0);
2106 fiat_p256_addcarryx_u32(&x467, &x468, x466, x436, 0x0);
2107 fiat_p256_addcarryx_u32(&x469, &x470, x468, x438, x426);
2108 fiat_p256_addcarryx_u32(&x471, &x472, x470, x440, x444);
2109 fiat_p256_addcarryx_u32(&x473, &x474, x472, x442, x445);
2110 x475 = ((uint32_t)x474 + x443);
2111 fiat_p256_mulx_u32(&x476, &x477, x6, (arg1[7]));
2112 fiat_p256_mulx_u32(&x478, &x479, x6, (arg1[6]));
2113 fiat_p256_mulx_u32(&x480, &x481, x6, (arg1[5]));
2114 fiat_p256_mulx_u32(&x482, &x483, x6, (arg1[4]));
2115 fiat_p256_mulx_u32(&x484, &x485, x6, (arg1[3]));
2116 fiat_p256_mulx_u32(&x486, &x487, x6, (arg1[2]));
2117 fiat_p256_mulx_u32(&x488, &x489, x6, (arg1[1]));
2118 fiat_p256_mulx_u32(&x490, &x491, x6, (arg1[0]));
2119 fiat_p256_addcarryx_u32(&x492, &x493, 0x0, x491, x488);
2120 fiat_p256_addcarryx_u32(&x494, &x495, x493, x489, x486);
2121 fiat_p256_addcarryx_u32(&x496, &x497, x495, x487, x484);
2122 fiat_p256_addcarryx_u32(&x498, &x499, x497, x485, x482);
2123 fiat_p256_addcarryx_u32(&x500, &x501, x499, x483, x480);
2124 fiat_p256_addcarryx_u32(&x502, &x503, x501, x481, x478);
2125 fiat_p256_addcarryx_u32(&x504, &x505, x503, x479, x476);
2126 x506 = (x505 + x477);
2127 fiat_p256_addcarryx_u32(&x507, &x508, 0x0, x459, x490);
2128 fiat_p256_addcarryx_u32(&x509, &x510, x508, x461, x492);
2129 fiat_p256_addcarryx_u32(&x511, &x512, x510, x463, x494);
2130 fiat_p256_addcarryx_u32(&x513, &x514, x512, x465, x496);
2131 fiat_p256_addcarryx_u32(&x515, &x516, x514, x467, x498);
2132 fiat_p256_addcarryx_u32(&x517, &x518, x516, x469, x500);
2133 fiat_p256_addcarryx_u32(&x519, &x520, x518, x471, x502);
2134 fiat_p256_addcarryx_u32(&x521, &x522, x520, x473, x504);
2135 fiat_p256_addcarryx_u32(&x523, &x524, x522, x475, x506);
2136 fiat_p256_mulx_u32(&x525, &x526, x507, UINT32_C(0xffffffff));
2137 fiat_p256_mulx_u32(&x527, &x528, x507, UINT32_C(0xffffffff));
2138 fiat_p256_mulx_u32(&x529, &x530, x507, UINT32_C(0xffffffff));
2139 fiat_p256_mulx_u32(&x531, &x532, x507, UINT32_C(0xffffffff));
2140 fiat_p256_addcarryx_u32(&x533, &x534, 0x0, x532, x529);
2141 fiat_p256_addcarryx_u32(&x535, &x536, x534, x530, x527);
2142 x537 = (x536 + x528);
2143 fiat_p256_addcarryx_u32(&x538, &x539, 0x0, x507, x531);
2144 fiat_p256_addcarryx_u32(&x540, &x541, x539, x509, x533);
2145 fiat_p256_addcarryx_u32(&x542, &x543, x541, x511, x535);
2146 fiat_p256_addcarryx_u32(&x544, &x545, x543, x513, x537);
2147 fiat_p256_addcarryx_u32(&x546, &x547, x545, x515, 0x0);
2148 fiat_p256_addcarryx_u32(&x548, &x549, x547, x517, 0x0);
2149 fiat_p256_addcarryx_u32(&x550, &x551, x549, x519, x507);
2150 fiat_p256_addcarryx_u32(&x552, &x553, x551, x521, x525);
2151 fiat_p256_addcarryx_u32(&x554, &x555, x553, x523, x526);
2152 x556 = ((uint32_t)x555 + x524);
2153 fiat_p256_mulx_u32(&x557, &x558, x7, (arg1[7]));
2154 fiat_p256_mulx_u32(&x559, &x560, x7, (arg1[6]));
2155 fiat_p256_mulx_u32(&x561, &x562, x7, (arg1[5]));
2156 fiat_p256_mulx_u32(&x563, &x564, x7, (arg1[4]));
2157 fiat_p256_mulx_u32(&x565, &x566, x7, (arg1[3]));
2158 fiat_p256_mulx_u32(&x567, &x568, x7, (arg1[2]));
2159 fiat_p256_mulx_u32(&x569, &x570, x7, (arg1[1]));
2160 fiat_p256_mulx_u32(&x571, &x572, x7, (arg1[0]));
2161 fiat_p256_addcarryx_u32(&x573, &x574, 0x0, x572, x569);
2162 fiat_p256_addcarryx_u32(&x575, &x576, x574, x570, x567);
2163 fiat_p256_addcarryx_u32(&x577, &x578, x576, x568, x565);
2164 fiat_p256_addcarryx_u32(&x579, &x580, x578, x566, x563);
2165 fiat_p256_addcarryx_u32(&x581, &x582, x580, x564, x561);
2166 fiat_p256_addcarryx_u32(&x583, &x584, x582, x562, x559);
2167 fiat_p256_addcarryx_u32(&x585, &x586, x584, x560, x557);
2168 x587 = (x586 + x558);
2169 fiat_p256_addcarryx_u32(&x588, &x589, 0x0, x540, x571);
2170 fiat_p256_addcarryx_u32(&x590, &x591, x589, x542, x573);
2171 fiat_p256_addcarryx_u32(&x592, &x593, x591, x544, x575);
2172 fiat_p256_addcarryx_u32(&x594, &x595, x593, x546, x577);
2173 fiat_p256_addcarryx_u32(&x596, &x597, x595, x548, x579);
2174 fiat_p256_addcarryx_u32(&x598, &x599, x597, x550, x581);
2175 fiat_p256_addcarryx_u32(&x600, &x601, x599, x552, x583);
2176 fiat_p256_addcarryx_u32(&x602, &x603, x601, x554, x585);
2177 fiat_p256_addcarryx_u32(&x604, &x605, x603, x556, x587);
2178 fiat_p256_mulx_u32(&x606, &x607, x588, UINT32_C(0xffffffff));
2179 fiat_p256_mulx_u32(&x608, &x609, x588, UINT32_C(0xffffffff));
2180 fiat_p256_mulx_u32(&x610, &x611, x588, UINT32_C(0xffffffff));
2181 fiat_p256_mulx_u32(&x612, &x613, x588, UINT32_C(0xffffffff));
2182 fiat_p256_addcarryx_u32(&x614, &x615, 0x0, x613, x610);
2183 fiat_p256_addcarryx_u32(&x616, &x617, x615, x611, x608);
2184 x618 = (x617 + x609);
2185 fiat_p256_addcarryx_u32(&x619, &x620, 0x0, x588, x612);
2186 fiat_p256_addcarryx_u32(&x621, &x622, x620, x590, x614);
2187 fiat_p256_addcarryx_u32(&x623, &x624, x622, x592, x616);
2188 fiat_p256_addcarryx_u32(&x625, &x626, x624, x594, x618);
2189 fiat_p256_addcarryx_u32(&x627, &x628, x626, x596, 0x0);
2190 fiat_p256_addcarryx_u32(&x629, &x630, x628, x598, 0x0);
2191 fiat_p256_addcarryx_u32(&x631, &x632, x630, x600, x588);
2192 fiat_p256_addcarryx_u32(&x633, &x634, x632, x602, x606);
2193 fiat_p256_addcarryx_u32(&x635, &x636, x634, x604, x607);
2194 x637 = ((uint32_t)x636 + x605);
2195 fiat_p256_subborrowx_u32(&x638, &x639, 0x0, x621, UINT32_C(0xffffffff));
2196 fiat_p256_subborrowx_u32(&x640, &x641, x639, x623, UINT32_C(0xffffffff));
2197 fiat_p256_subborrowx_u32(&x642, &x643, x641, x625, UINT32_C(0xffffffff));
2198 fiat_p256_subborrowx_u32(&x644, &x645, x643, x627, 0x0);
2199 fiat_p256_subborrowx_u32(&x646, &x647, x645, x629, 0x0);
2200 fiat_p256_subborrowx_u32(&x648, &x649, x647, x631, 0x0);
2201 fiat_p256_subborrowx_u32(&x650, &x651, x649, x633, 0x1);
2202 fiat_p256_subborrowx_u32(&x652, &x653, x651, x635, UINT32_C(0xffffffff));
2203 fiat_p256_subborrowx_u32(&x654, &x655, x653, x637, 0x0);
2204 fiat_p256_cmovznz_u32(&x656, x655, x638, x621);
2205 fiat_p256_cmovznz_u32(&x657, x655, x640, x623);
2206 fiat_p256_cmovznz_u32(&x658, x655, x642, x625);
2207 fiat_p256_cmovznz_u32(&x659, x655, x644, x627);
2208 fiat_p256_cmovznz_u32(&x660, x655, x646, x629);
2209 fiat_p256_cmovznz_u32(&x661, x655, x648, x631);
2210 fiat_p256_cmovznz_u32(&x662, x655, x650, x633);
2211 fiat_p256_cmovznz_u32(&x663, x655, x652, x635);
2212 out1[0] = x656;
2213 out1[1] = x657;
2214 out1[2] = x658;
2215 out1[3] = x659;
2216 out1[4] = x660;
2217 out1[5] = x661;
2218 out1[6] = x662;
2219 out1[7] = x663;
2220 }
2221
2222 /*
2223 * The function fiat_p256_add adds two field elements in the Montgomery domain.
2224 *
2225 * Preconditions:
2226 * 0 ≤ eval arg1 < m
2227 * 0 ≤ eval arg2 < m
2228 * Postconditions:
2229 * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
2230 * 0 ≤ eval out1 < m
2231 *
2232 */
fiat_p256_add(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1,const fiat_p256_montgomery_domain_field_element arg2)2233 static FIAT_P256_FIAT_INLINE void fiat_p256_add(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1, const fiat_p256_montgomery_domain_field_element arg2) {
2234 uint32_t x1;
2235 fiat_p256_uint1 x2;
2236 uint32_t x3;
2237 fiat_p256_uint1 x4;
2238 uint32_t x5;
2239 fiat_p256_uint1 x6;
2240 uint32_t x7;
2241 fiat_p256_uint1 x8;
2242 uint32_t x9;
2243 fiat_p256_uint1 x10;
2244 uint32_t x11;
2245 fiat_p256_uint1 x12;
2246 uint32_t x13;
2247 fiat_p256_uint1 x14;
2248 uint32_t x15;
2249 fiat_p256_uint1 x16;
2250 uint32_t x17;
2251 fiat_p256_uint1 x18;
2252 uint32_t x19;
2253 fiat_p256_uint1 x20;
2254 uint32_t x21;
2255 fiat_p256_uint1 x22;
2256 uint32_t x23;
2257 fiat_p256_uint1 x24;
2258 uint32_t x25;
2259 fiat_p256_uint1 x26;
2260 uint32_t x27;
2261 fiat_p256_uint1 x28;
2262 uint32_t x29;
2263 fiat_p256_uint1 x30;
2264 uint32_t x31;
2265 fiat_p256_uint1 x32;
2266 uint32_t x33;
2267 fiat_p256_uint1 x34;
2268 uint32_t x35;
2269 uint32_t x36;
2270 uint32_t x37;
2271 uint32_t x38;
2272 uint32_t x39;
2273 uint32_t x40;
2274 uint32_t x41;
2275 uint32_t x42;
2276 fiat_p256_addcarryx_u32(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
2277 fiat_p256_addcarryx_u32(&x3, &x4, x2, (arg1[1]), (arg2[1]));
2278 fiat_p256_addcarryx_u32(&x5, &x6, x4, (arg1[2]), (arg2[2]));
2279 fiat_p256_addcarryx_u32(&x7, &x8, x6, (arg1[3]), (arg2[3]));
2280 fiat_p256_addcarryx_u32(&x9, &x10, x8, (arg1[4]), (arg2[4]));
2281 fiat_p256_addcarryx_u32(&x11, &x12, x10, (arg1[5]), (arg2[5]));
2282 fiat_p256_addcarryx_u32(&x13, &x14, x12, (arg1[6]), (arg2[6]));
2283 fiat_p256_addcarryx_u32(&x15, &x16, x14, (arg1[7]), (arg2[7]));
2284 fiat_p256_subborrowx_u32(&x17, &x18, 0x0, x1, UINT32_C(0xffffffff));
2285 fiat_p256_subborrowx_u32(&x19, &x20, x18, x3, UINT32_C(0xffffffff));
2286 fiat_p256_subborrowx_u32(&x21, &x22, x20, x5, UINT32_C(0xffffffff));
2287 fiat_p256_subborrowx_u32(&x23, &x24, x22, x7, 0x0);
2288 fiat_p256_subborrowx_u32(&x25, &x26, x24, x9, 0x0);
2289 fiat_p256_subborrowx_u32(&x27, &x28, x26, x11, 0x0);
2290 fiat_p256_subborrowx_u32(&x29, &x30, x28, x13, 0x1);
2291 fiat_p256_subborrowx_u32(&x31, &x32, x30, x15, UINT32_C(0xffffffff));
2292 fiat_p256_subborrowx_u32(&x33, &x34, x32, x16, 0x0);
2293 fiat_p256_cmovznz_u32(&x35, x34, x17, x1);
2294 fiat_p256_cmovznz_u32(&x36, x34, x19, x3);
2295 fiat_p256_cmovznz_u32(&x37, x34, x21, x5);
2296 fiat_p256_cmovznz_u32(&x38, x34, x23, x7);
2297 fiat_p256_cmovznz_u32(&x39, x34, x25, x9);
2298 fiat_p256_cmovznz_u32(&x40, x34, x27, x11);
2299 fiat_p256_cmovznz_u32(&x41, x34, x29, x13);
2300 fiat_p256_cmovznz_u32(&x42, x34, x31, x15);
2301 out1[0] = x35;
2302 out1[1] = x36;
2303 out1[2] = x37;
2304 out1[3] = x38;
2305 out1[4] = x39;
2306 out1[5] = x40;
2307 out1[6] = x41;
2308 out1[7] = x42;
2309 }
2310
2311 /*
2312 * The function fiat_p256_sub subtracts two field elements in the Montgomery domain.
2313 *
2314 * Preconditions:
2315 * 0 ≤ eval arg1 < m
2316 * 0 ≤ eval arg2 < m
2317 * Postconditions:
2318 * eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
2319 * 0 ≤ eval out1 < m
2320 *
2321 */
fiat_p256_sub(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1,const fiat_p256_montgomery_domain_field_element arg2)2322 static FIAT_P256_FIAT_INLINE void fiat_p256_sub(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1, const fiat_p256_montgomery_domain_field_element arg2) {
2323 uint32_t x1;
2324 fiat_p256_uint1 x2;
2325 uint32_t x3;
2326 fiat_p256_uint1 x4;
2327 uint32_t x5;
2328 fiat_p256_uint1 x6;
2329 uint32_t x7;
2330 fiat_p256_uint1 x8;
2331 uint32_t x9;
2332 fiat_p256_uint1 x10;
2333 uint32_t x11;
2334 fiat_p256_uint1 x12;
2335 uint32_t x13;
2336 fiat_p256_uint1 x14;
2337 uint32_t x15;
2338 fiat_p256_uint1 x16;
2339 uint32_t x17;
2340 uint32_t x18;
2341 fiat_p256_uint1 x19;
2342 uint32_t x20;
2343 fiat_p256_uint1 x21;
2344 uint32_t x22;
2345 fiat_p256_uint1 x23;
2346 uint32_t x24;
2347 fiat_p256_uint1 x25;
2348 uint32_t x26;
2349 fiat_p256_uint1 x27;
2350 uint32_t x28;
2351 fiat_p256_uint1 x29;
2352 uint32_t x30;
2353 fiat_p256_uint1 x31;
2354 uint32_t x32;
2355 fiat_p256_uint1 x33;
2356 fiat_p256_subborrowx_u32(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
2357 fiat_p256_subborrowx_u32(&x3, &x4, x2, (arg1[1]), (arg2[1]));
2358 fiat_p256_subborrowx_u32(&x5, &x6, x4, (arg1[2]), (arg2[2]));
2359 fiat_p256_subborrowx_u32(&x7, &x8, x6, (arg1[3]), (arg2[3]));
2360 fiat_p256_subborrowx_u32(&x9, &x10, x8, (arg1[4]), (arg2[4]));
2361 fiat_p256_subborrowx_u32(&x11, &x12, x10, (arg1[5]), (arg2[5]));
2362 fiat_p256_subborrowx_u32(&x13, &x14, x12, (arg1[6]), (arg2[6]));
2363 fiat_p256_subborrowx_u32(&x15, &x16, x14, (arg1[7]), (arg2[7]));
2364 fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff));
2365 fiat_p256_addcarryx_u32(&x18, &x19, 0x0, x1, x17);
2366 fiat_p256_addcarryx_u32(&x20, &x21, x19, x3, x17);
2367 fiat_p256_addcarryx_u32(&x22, &x23, x21, x5, x17);
2368 fiat_p256_addcarryx_u32(&x24, &x25, x23, x7, 0x0);
2369 fiat_p256_addcarryx_u32(&x26, &x27, x25, x9, 0x0);
2370 fiat_p256_addcarryx_u32(&x28, &x29, x27, x11, 0x0);
2371 fiat_p256_addcarryx_u32(&x30, &x31, x29, x13, (fiat_p256_uint1)(x17 & 0x1));
2372 fiat_p256_addcarryx_u32(&x32, &x33, x31, x15, x17);
2373 out1[0] = x18;
2374 out1[1] = x20;
2375 out1[2] = x22;
2376 out1[3] = x24;
2377 out1[4] = x26;
2378 out1[5] = x28;
2379 out1[6] = x30;
2380 out1[7] = x32;
2381 }
2382
2383 /*
2384 * The function fiat_p256_opp negates a field element in the Montgomery domain.
2385 *
2386 * Preconditions:
2387 * 0 ≤ eval arg1 < m
2388 * Postconditions:
2389 * eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
2390 * 0 ≤ eval out1 < m
2391 *
2392 */
fiat_p256_opp(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1)2393 static FIAT_P256_FIAT_INLINE void fiat_p256_opp(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1) {
2394 uint32_t x1;
2395 fiat_p256_uint1 x2;
2396 uint32_t x3;
2397 fiat_p256_uint1 x4;
2398 uint32_t x5;
2399 fiat_p256_uint1 x6;
2400 uint32_t x7;
2401 fiat_p256_uint1 x8;
2402 uint32_t x9;
2403 fiat_p256_uint1 x10;
2404 uint32_t x11;
2405 fiat_p256_uint1 x12;
2406 uint32_t x13;
2407 fiat_p256_uint1 x14;
2408 uint32_t x15;
2409 fiat_p256_uint1 x16;
2410 uint32_t x17;
2411 uint32_t x18;
2412 fiat_p256_uint1 x19;
2413 uint32_t x20;
2414 fiat_p256_uint1 x21;
2415 uint32_t x22;
2416 fiat_p256_uint1 x23;
2417 uint32_t x24;
2418 fiat_p256_uint1 x25;
2419 uint32_t x26;
2420 fiat_p256_uint1 x27;
2421 uint32_t x28;
2422 fiat_p256_uint1 x29;
2423 uint32_t x30;
2424 fiat_p256_uint1 x31;
2425 uint32_t x32;
2426 fiat_p256_uint1 x33;
2427 fiat_p256_subborrowx_u32(&x1, &x2, 0x0, 0x0, (arg1[0]));
2428 fiat_p256_subborrowx_u32(&x3, &x4, x2, 0x0, (arg1[1]));
2429 fiat_p256_subborrowx_u32(&x5, &x6, x4, 0x0, (arg1[2]));
2430 fiat_p256_subborrowx_u32(&x7, &x8, x6, 0x0, (arg1[3]));
2431 fiat_p256_subborrowx_u32(&x9, &x10, x8, 0x0, (arg1[4]));
2432 fiat_p256_subborrowx_u32(&x11, &x12, x10, 0x0, (arg1[5]));
2433 fiat_p256_subborrowx_u32(&x13, &x14, x12, 0x0, (arg1[6]));
2434 fiat_p256_subborrowx_u32(&x15, &x16, x14, 0x0, (arg1[7]));
2435 fiat_p256_cmovznz_u32(&x17, x16, 0x0, UINT32_C(0xffffffff));
2436 fiat_p256_addcarryx_u32(&x18, &x19, 0x0, x1, x17);
2437 fiat_p256_addcarryx_u32(&x20, &x21, x19, x3, x17);
2438 fiat_p256_addcarryx_u32(&x22, &x23, x21, x5, x17);
2439 fiat_p256_addcarryx_u32(&x24, &x25, x23, x7, 0x0);
2440 fiat_p256_addcarryx_u32(&x26, &x27, x25, x9, 0x0);
2441 fiat_p256_addcarryx_u32(&x28, &x29, x27, x11, 0x0);
2442 fiat_p256_addcarryx_u32(&x30, &x31, x29, x13, (fiat_p256_uint1)(x17 & 0x1));
2443 fiat_p256_addcarryx_u32(&x32, &x33, x31, x15, x17);
2444 out1[0] = x18;
2445 out1[1] = x20;
2446 out1[2] = x22;
2447 out1[3] = x24;
2448 out1[4] = x26;
2449 out1[5] = x28;
2450 out1[6] = x30;
2451 out1[7] = x32;
2452 }
2453
2454 /*
2455 * The function fiat_p256_from_montgomery translates a field element out of the Montgomery domain.
2456 *
2457 * Preconditions:
2458 * 0 ≤ eval arg1 < m
2459 * Postconditions:
2460 * eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^8) mod m
2461 * 0 ≤ eval out1 < m
2462 *
2463 */
fiat_p256_from_montgomery(fiat_p256_non_montgomery_domain_field_element out1,const fiat_p256_montgomery_domain_field_element arg1)2464 static FIAT_P256_FIAT_INLINE void fiat_p256_from_montgomery(fiat_p256_non_montgomery_domain_field_element out1, const fiat_p256_montgomery_domain_field_element arg1) {
2465 uint32_t x1;
2466 uint32_t x2;
2467 uint32_t x3;
2468 uint32_t x4;
2469 uint32_t x5;
2470 uint32_t x6;
2471 uint32_t x7;
2472 uint32_t x8;
2473 uint32_t x9;
2474 uint32_t x10;
2475 fiat_p256_uint1 x11;
2476 uint32_t x12;
2477 fiat_p256_uint1 x13;
2478 uint32_t x14;
2479 fiat_p256_uint1 x15;
2480 uint32_t x16;
2481 fiat_p256_uint1 x17;
2482 uint32_t x18;
2483 fiat_p256_uint1 x19;
2484 uint32_t x20;
2485 fiat_p256_uint1 x21;
2486 uint32_t x22;
2487 fiat_p256_uint1 x23;
2488 uint32_t x24;
2489 fiat_p256_uint1 x25;
2490 uint32_t x26;
2491 fiat_p256_uint1 x27;
2492 uint32_t x28;
2493 uint32_t x29;
2494 uint32_t x30;
2495 uint32_t x31;
2496 uint32_t x32;
2497 uint32_t x33;
2498 uint32_t x34;
2499 uint32_t x35;
2500 uint32_t x36;
2501 fiat_p256_uint1 x37;
2502 uint32_t x38;
2503 fiat_p256_uint1 x39;
2504 uint32_t x40;
2505 fiat_p256_uint1 x41;
2506 uint32_t x42;
2507 fiat_p256_uint1 x43;
2508 uint32_t x44;
2509 fiat_p256_uint1 x45;
2510 uint32_t x46;
2511 fiat_p256_uint1 x47;
2512 uint32_t x48;
2513 fiat_p256_uint1 x49;
2514 uint32_t x50;
2515 fiat_p256_uint1 x51;
2516 uint32_t x52;
2517 fiat_p256_uint1 x53;
2518 uint32_t x54;
2519 fiat_p256_uint1 x55;
2520 uint32_t x56;
2521 fiat_p256_uint1 x57;
2522 uint32_t x58;
2523 uint32_t x59;
2524 uint32_t x60;
2525 uint32_t x61;
2526 uint32_t x62;
2527 uint32_t x63;
2528 uint32_t x64;
2529 uint32_t x65;
2530 uint32_t x66;
2531 fiat_p256_uint1 x67;
2532 uint32_t x68;
2533 fiat_p256_uint1 x69;
2534 uint32_t x70;
2535 fiat_p256_uint1 x71;
2536 uint32_t x72;
2537 fiat_p256_uint1 x73;
2538 uint32_t x74;
2539 fiat_p256_uint1 x75;
2540 uint32_t x76;
2541 fiat_p256_uint1 x77;
2542 uint32_t x78;
2543 fiat_p256_uint1 x79;
2544 uint32_t x80;
2545 fiat_p256_uint1 x81;
2546 uint32_t x82;
2547 fiat_p256_uint1 x83;
2548 uint32_t x84;
2549 fiat_p256_uint1 x85;
2550 uint32_t x86;
2551 fiat_p256_uint1 x87;
2552 uint32_t x88;
2553 fiat_p256_uint1 x89;
2554 uint32_t x90;
2555 fiat_p256_uint1 x91;
2556 uint32_t x92;
2557 fiat_p256_uint1 x93;
2558 uint32_t x94;
2559 fiat_p256_uint1 x95;
2560 uint32_t x96;
2561 fiat_p256_uint1 x97;
2562 uint32_t x98;
2563 fiat_p256_uint1 x99;
2564 uint32_t x100;
2565 fiat_p256_uint1 x101;
2566 uint32_t x102;
2567 uint32_t x103;
2568 uint32_t x104;
2569 uint32_t x105;
2570 uint32_t x106;
2571 uint32_t x107;
2572 uint32_t x108;
2573 uint32_t x109;
2574 uint32_t x110;
2575 fiat_p256_uint1 x111;
2576 uint32_t x112;
2577 fiat_p256_uint1 x113;
2578 uint32_t x114;
2579 fiat_p256_uint1 x115;
2580 uint32_t x116;
2581 fiat_p256_uint1 x117;
2582 uint32_t x118;
2583 fiat_p256_uint1 x119;
2584 uint32_t x120;
2585 fiat_p256_uint1 x121;
2586 uint32_t x122;
2587 fiat_p256_uint1 x123;
2588 uint32_t x124;
2589 fiat_p256_uint1 x125;
2590 uint32_t x126;
2591 fiat_p256_uint1 x127;
2592 uint32_t x128;
2593 fiat_p256_uint1 x129;
2594 uint32_t x130;
2595 fiat_p256_uint1 x131;
2596 uint32_t x132;
2597 fiat_p256_uint1 x133;
2598 uint32_t x134;
2599 fiat_p256_uint1 x135;
2600 uint32_t x136;
2601 fiat_p256_uint1 x137;
2602 uint32_t x138;
2603 fiat_p256_uint1 x139;
2604 uint32_t x140;
2605 fiat_p256_uint1 x141;
2606 uint32_t x142;
2607 fiat_p256_uint1 x143;
2608 uint32_t x144;
2609 fiat_p256_uint1 x145;
2610 uint32_t x146;
2611 fiat_p256_uint1 x147;
2612 uint32_t x148;
2613 uint32_t x149;
2614 uint32_t x150;
2615 uint32_t x151;
2616 uint32_t x152;
2617 uint32_t x153;
2618 uint32_t x154;
2619 uint32_t x155;
2620 uint32_t x156;
2621 fiat_p256_uint1 x157;
2622 uint32_t x158;
2623 fiat_p256_uint1 x159;
2624 uint32_t x160;
2625 fiat_p256_uint1 x161;
2626 uint32_t x162;
2627 fiat_p256_uint1 x163;
2628 uint32_t x164;
2629 fiat_p256_uint1 x165;
2630 uint32_t x166;
2631 fiat_p256_uint1 x167;
2632 uint32_t x168;
2633 fiat_p256_uint1 x169;
2634 uint32_t x170;
2635 fiat_p256_uint1 x171;
2636 uint32_t x172;
2637 fiat_p256_uint1 x173;
2638 uint32_t x174;
2639 fiat_p256_uint1 x175;
2640 uint32_t x176;
2641 fiat_p256_uint1 x177;
2642 uint32_t x178;
2643 fiat_p256_uint1 x179;
2644 uint32_t x180;
2645 fiat_p256_uint1 x181;
2646 uint32_t x182;
2647 fiat_p256_uint1 x183;
2648 uint32_t x184;
2649 fiat_p256_uint1 x185;
2650 uint32_t x186;
2651 fiat_p256_uint1 x187;
2652 uint32_t x188;
2653 fiat_p256_uint1 x189;
2654 uint32_t x190;
2655 fiat_p256_uint1 x191;
2656 uint32_t x192;
2657 fiat_p256_uint1 x193;
2658 uint32_t x194;
2659 uint32_t x195;
2660 uint32_t x196;
2661 uint32_t x197;
2662 uint32_t x198;
2663 uint32_t x199;
2664 uint32_t x200;
2665 uint32_t x201;
2666 uint32_t x202;
2667 fiat_p256_uint1 x203;
2668 uint32_t x204;
2669 fiat_p256_uint1 x205;
2670 uint32_t x206;
2671 fiat_p256_uint1 x207;
2672 uint32_t x208;
2673 fiat_p256_uint1 x209;
2674 uint32_t x210;
2675 fiat_p256_uint1 x211;
2676 uint32_t x212;
2677 fiat_p256_uint1 x213;
2678 uint32_t x214;
2679 fiat_p256_uint1 x215;
2680 uint32_t x216;
2681 fiat_p256_uint1 x217;
2682 uint32_t x218;
2683 fiat_p256_uint1 x219;
2684 uint32_t x220;
2685 fiat_p256_uint1 x221;
2686 uint32_t x222;
2687 fiat_p256_uint1 x223;
2688 uint32_t x224;
2689 fiat_p256_uint1 x225;
2690 uint32_t x226;
2691 fiat_p256_uint1 x227;
2692 uint32_t x228;
2693 fiat_p256_uint1 x229;
2694 uint32_t x230;
2695 fiat_p256_uint1 x231;
2696 uint32_t x232;
2697 fiat_p256_uint1 x233;
2698 uint32_t x234;
2699 fiat_p256_uint1 x235;
2700 uint32_t x236;
2701 fiat_p256_uint1 x237;
2702 uint32_t x238;
2703 fiat_p256_uint1 x239;
2704 uint32_t x240;
2705 uint32_t x241;
2706 uint32_t x242;
2707 uint32_t x243;
2708 uint32_t x244;
2709 uint32_t x245;
2710 uint32_t x246;
2711 uint32_t x247;
2712 uint32_t x248;
2713 fiat_p256_uint1 x249;
2714 uint32_t x250;
2715 fiat_p256_uint1 x251;
2716 uint32_t x252;
2717 fiat_p256_uint1 x253;
2718 uint32_t x254;
2719 fiat_p256_uint1 x255;
2720 uint32_t x256;
2721 fiat_p256_uint1 x257;
2722 uint32_t x258;
2723 fiat_p256_uint1 x259;
2724 uint32_t x260;
2725 fiat_p256_uint1 x261;
2726 uint32_t x262;
2727 fiat_p256_uint1 x263;
2728 uint32_t x264;
2729 fiat_p256_uint1 x265;
2730 uint32_t x266;
2731 fiat_p256_uint1 x267;
2732 uint32_t x268;
2733 fiat_p256_uint1 x269;
2734 uint32_t x270;
2735 fiat_p256_uint1 x271;
2736 uint32_t x272;
2737 fiat_p256_uint1 x273;
2738 uint32_t x274;
2739 fiat_p256_uint1 x275;
2740 uint32_t x276;
2741 fiat_p256_uint1 x277;
2742 uint32_t x278;
2743 fiat_p256_uint1 x279;
2744 uint32_t x280;
2745 fiat_p256_uint1 x281;
2746 uint32_t x282;
2747 fiat_p256_uint1 x283;
2748 uint32_t x284;
2749 fiat_p256_uint1 x285;
2750 uint32_t x286;
2751 uint32_t x287;
2752 uint32_t x288;
2753 uint32_t x289;
2754 uint32_t x290;
2755 uint32_t x291;
2756 uint32_t x292;
2757 uint32_t x293;
2758 uint32_t x294;
2759 fiat_p256_uint1 x295;
2760 uint32_t x296;
2761 fiat_p256_uint1 x297;
2762 uint32_t x298;
2763 fiat_p256_uint1 x299;
2764 uint32_t x300;
2765 fiat_p256_uint1 x301;
2766 uint32_t x302;
2767 fiat_p256_uint1 x303;
2768 uint32_t x304;
2769 fiat_p256_uint1 x305;
2770 uint32_t x306;
2771 fiat_p256_uint1 x307;
2772 uint32_t x308;
2773 fiat_p256_uint1 x309;
2774 uint32_t x310;
2775 fiat_p256_uint1 x311;
2776 uint32_t x312;
2777 fiat_p256_uint1 x313;
2778 uint32_t x314;
2779 fiat_p256_uint1 x315;
2780 uint32_t x316;
2781 fiat_p256_uint1 x317;
2782 uint32_t x318;
2783 fiat_p256_uint1 x319;
2784 uint32_t x320;
2785 fiat_p256_uint1 x321;
2786 uint32_t x322;
2787 fiat_p256_uint1 x323;
2788 uint32_t x324;
2789 fiat_p256_uint1 x325;
2790 uint32_t x326;
2791 fiat_p256_uint1 x327;
2792 uint32_t x328;
2793 fiat_p256_uint1 x329;
2794 uint32_t x330;
2795 fiat_p256_uint1 x331;
2796 uint32_t x332;
2797 fiat_p256_uint1 x333;
2798 uint32_t x334;
2799 uint32_t x335;
2800 uint32_t x336;
2801 uint32_t x337;
2802 uint32_t x338;
2803 uint32_t x339;
2804 uint32_t x340;
2805 uint32_t x341;
2806 x1 = (arg1[0]);
2807 fiat_p256_mulx_u32(&x2, &x3, x1, UINT32_C(0xffffffff));
2808 fiat_p256_mulx_u32(&x4, &x5, x1, UINT32_C(0xffffffff));
2809 fiat_p256_mulx_u32(&x6, &x7, x1, UINT32_C(0xffffffff));
2810 fiat_p256_mulx_u32(&x8, &x9, x1, UINT32_C(0xffffffff));
2811 fiat_p256_addcarryx_u32(&x10, &x11, 0x0, x9, x6);
2812 fiat_p256_addcarryx_u32(&x12, &x13, x11, x7, x4);
2813 fiat_p256_addcarryx_u32(&x14, &x15, 0x0, x1, x8);
2814 fiat_p256_addcarryx_u32(&x16, &x17, x15, 0x0, x10);
2815 fiat_p256_addcarryx_u32(&x18, &x19, x17, 0x0, x12);
2816 fiat_p256_addcarryx_u32(&x20, &x21, x19, 0x0, (x13 + x5));
2817 fiat_p256_addcarryx_u32(&x22, &x23, 0x0, x16, (arg1[1]));
2818 fiat_p256_addcarryx_u32(&x24, &x25, x23, x18, 0x0);
2819 fiat_p256_addcarryx_u32(&x26, &x27, x25, x20, 0x0);
2820 fiat_p256_mulx_u32(&x28, &x29, x22, UINT32_C(0xffffffff));
2821 fiat_p256_mulx_u32(&x30, &x31, x22, UINT32_C(0xffffffff));
2822 fiat_p256_mulx_u32(&x32, &x33, x22, UINT32_C(0xffffffff));
2823 fiat_p256_mulx_u32(&x34, &x35, x22, UINT32_C(0xffffffff));
2824 fiat_p256_addcarryx_u32(&x36, &x37, 0x0, x35, x32);
2825 fiat_p256_addcarryx_u32(&x38, &x39, x37, x33, x30);
2826 fiat_p256_addcarryx_u32(&x40, &x41, 0x0, x22, x34);
2827 fiat_p256_addcarryx_u32(&x42, &x43, x41, x24, x36);
2828 fiat_p256_addcarryx_u32(&x44, &x45, x43, x26, x38);
2829 fiat_p256_addcarryx_u32(&x46, &x47, x45, ((uint32_t)x27 + x21), (x39 + x31));
2830 fiat_p256_addcarryx_u32(&x48, &x49, 0x0, x2, x22);
2831 fiat_p256_addcarryx_u32(&x50, &x51, x49, x3, x28);
2832 fiat_p256_addcarryx_u32(&x52, &x53, 0x0, x42, (arg1[2]));
2833 fiat_p256_addcarryx_u32(&x54, &x55, x53, x44, 0x0);
2834 fiat_p256_addcarryx_u32(&x56, &x57, x55, x46, 0x0);
2835 fiat_p256_mulx_u32(&x58, &x59, x52, UINT32_C(0xffffffff));
2836 fiat_p256_mulx_u32(&x60, &x61, x52, UINT32_C(0xffffffff));
2837 fiat_p256_mulx_u32(&x62, &x63, x52, UINT32_C(0xffffffff));
2838 fiat_p256_mulx_u32(&x64, &x65, x52, UINT32_C(0xffffffff));
2839 fiat_p256_addcarryx_u32(&x66, &x67, 0x0, x65, x62);
2840 fiat_p256_addcarryx_u32(&x68, &x69, x67, x63, x60);
2841 fiat_p256_addcarryx_u32(&x70, &x71, 0x0, x52, x64);
2842 fiat_p256_addcarryx_u32(&x72, &x73, x71, x54, x66);
2843 fiat_p256_addcarryx_u32(&x74, &x75, x73, x56, x68);
2844 fiat_p256_addcarryx_u32(&x76, &x77, x75, ((uint32_t)x57 + x47), (x69 + x61));
2845 fiat_p256_addcarryx_u32(&x78, &x79, x77, x1, 0x0);
2846 fiat_p256_addcarryx_u32(&x80, &x81, x79, x48, 0x0);
2847 fiat_p256_addcarryx_u32(&x82, &x83, x81, x50, x52);
2848 fiat_p256_addcarryx_u32(&x84, &x85, x83, (x51 + x29), x58);
2849 fiat_p256_addcarryx_u32(&x86, &x87, 0x0, x72, (arg1[3]));
2850 fiat_p256_addcarryx_u32(&x88, &x89, x87, x74, 0x0);
2851 fiat_p256_addcarryx_u32(&x90, &x91, x89, x76, 0x0);
2852 fiat_p256_addcarryx_u32(&x92, &x93, x91, x78, 0x0);
2853 fiat_p256_addcarryx_u32(&x94, &x95, x93, x80, 0x0);
2854 fiat_p256_addcarryx_u32(&x96, &x97, x95, x82, 0x0);
2855 fiat_p256_addcarryx_u32(&x98, &x99, x97, x84, 0x0);
2856 fiat_p256_addcarryx_u32(&x100, &x101, x99, (x85 + x59), 0x0);
2857 fiat_p256_mulx_u32(&x102, &x103, x86, UINT32_C(0xffffffff));
2858 fiat_p256_mulx_u32(&x104, &x105, x86, UINT32_C(0xffffffff));
2859 fiat_p256_mulx_u32(&x106, &x107, x86, UINT32_C(0xffffffff));
2860 fiat_p256_mulx_u32(&x108, &x109, x86, UINT32_C(0xffffffff));
2861 fiat_p256_addcarryx_u32(&x110, &x111, 0x0, x109, x106);
2862 fiat_p256_addcarryx_u32(&x112, &x113, x111, x107, x104);
2863 fiat_p256_addcarryx_u32(&x114, &x115, 0x0, x86, x108);
2864 fiat_p256_addcarryx_u32(&x116, &x117, x115, x88, x110);
2865 fiat_p256_addcarryx_u32(&x118, &x119, x117, x90, x112);
2866 fiat_p256_addcarryx_u32(&x120, &x121, x119, x92, (x113 + x105));
2867 fiat_p256_addcarryx_u32(&x122, &x123, x121, x94, 0x0);
2868 fiat_p256_addcarryx_u32(&x124, &x125, x123, x96, 0x0);
2869 fiat_p256_addcarryx_u32(&x126, &x127, x125, x98, x86);
2870 fiat_p256_addcarryx_u32(&x128, &x129, x127, x100, x102);
2871 fiat_p256_addcarryx_u32(&x130, &x131, x129, x101, x103);
2872 fiat_p256_addcarryx_u32(&x132, &x133, 0x0, x116, (arg1[4]));
2873 fiat_p256_addcarryx_u32(&x134, &x135, x133, x118, 0x0);
2874 fiat_p256_addcarryx_u32(&x136, &x137, x135, x120, 0x0);
2875 fiat_p256_addcarryx_u32(&x138, &x139, x137, x122, 0x0);
2876 fiat_p256_addcarryx_u32(&x140, &x141, x139, x124, 0x0);
2877 fiat_p256_addcarryx_u32(&x142, &x143, x141, x126, 0x0);
2878 fiat_p256_addcarryx_u32(&x144, &x145, x143, x128, 0x0);
2879 fiat_p256_addcarryx_u32(&x146, &x147, x145, x130, 0x0);
2880 fiat_p256_mulx_u32(&x148, &x149, x132, UINT32_C(0xffffffff));
2881 fiat_p256_mulx_u32(&x150, &x151, x132, UINT32_C(0xffffffff));
2882 fiat_p256_mulx_u32(&x152, &x153, x132, UINT32_C(0xffffffff));
2883 fiat_p256_mulx_u32(&x154, &x155, x132, UINT32_C(0xffffffff));
2884 fiat_p256_addcarryx_u32(&x156, &x157, 0x0, x155, x152);
2885 fiat_p256_addcarryx_u32(&x158, &x159, x157, x153, x150);
2886 fiat_p256_addcarryx_u32(&x160, &x161, 0x0, x132, x154);
2887 fiat_p256_addcarryx_u32(&x162, &x163, x161, x134, x156);
2888 fiat_p256_addcarryx_u32(&x164, &x165, x163, x136, x158);
2889 fiat_p256_addcarryx_u32(&x166, &x167, x165, x138, (x159 + x151));
2890 fiat_p256_addcarryx_u32(&x168, &x169, x167, x140, 0x0);
2891 fiat_p256_addcarryx_u32(&x170, &x171, x169, x142, 0x0);
2892 fiat_p256_addcarryx_u32(&x172, &x173, x171, x144, x132);
2893 fiat_p256_addcarryx_u32(&x174, &x175, x173, x146, x148);
2894 fiat_p256_addcarryx_u32(&x176, &x177, x175, ((uint32_t)x147 + x131), x149);
2895 fiat_p256_addcarryx_u32(&x178, &x179, 0x0, x162, (arg1[5]));
2896 fiat_p256_addcarryx_u32(&x180, &x181, x179, x164, 0x0);
2897 fiat_p256_addcarryx_u32(&x182, &x183, x181, x166, 0x0);
2898 fiat_p256_addcarryx_u32(&x184, &x185, x183, x168, 0x0);
2899 fiat_p256_addcarryx_u32(&x186, &x187, x185, x170, 0x0);
2900 fiat_p256_addcarryx_u32(&x188, &x189, x187, x172, 0x0);
2901 fiat_p256_addcarryx_u32(&x190, &x191, x189, x174, 0x0);
2902 fiat_p256_addcarryx_u32(&x192, &x193, x191, x176, 0x0);
2903 fiat_p256_mulx_u32(&x194, &x195, x178, UINT32_C(0xffffffff));
2904 fiat_p256_mulx_u32(&x196, &x197, x178, UINT32_C(0xffffffff));
2905 fiat_p256_mulx_u32(&x198, &x199, x178, UINT32_C(0xffffffff));
2906 fiat_p256_mulx_u32(&x200, &x201, x178, UINT32_C(0xffffffff));
2907 fiat_p256_addcarryx_u32(&x202, &x203, 0x0, x201, x198);
2908 fiat_p256_addcarryx_u32(&x204, &x205, x203, x199, x196);
2909 fiat_p256_addcarryx_u32(&x206, &x207, 0x0, x178, x200);
2910 fiat_p256_addcarryx_u32(&x208, &x209, x207, x180, x202);
2911 fiat_p256_addcarryx_u32(&x210, &x211, x209, x182, x204);
2912 fiat_p256_addcarryx_u32(&x212, &x213, x211, x184, (x205 + x197));
2913 fiat_p256_addcarryx_u32(&x214, &x215, x213, x186, 0x0);
2914 fiat_p256_addcarryx_u32(&x216, &x217, x215, x188, 0x0);
2915 fiat_p256_addcarryx_u32(&x218, &x219, x217, x190, x178);
2916 fiat_p256_addcarryx_u32(&x220, &x221, x219, x192, x194);
2917 fiat_p256_addcarryx_u32(&x222, &x223, x221, ((uint32_t)x193 + x177), x195);
2918 fiat_p256_addcarryx_u32(&x224, &x225, 0x0, x208, (arg1[6]));
2919 fiat_p256_addcarryx_u32(&x226, &x227, x225, x210, 0x0);
2920 fiat_p256_addcarryx_u32(&x228, &x229, x227, x212, 0x0);
2921 fiat_p256_addcarryx_u32(&x230, &x231, x229, x214, 0x0);
2922 fiat_p256_addcarryx_u32(&x232, &x233, x231, x216, 0x0);
2923 fiat_p256_addcarryx_u32(&x234, &x235, x233, x218, 0x0);
2924 fiat_p256_addcarryx_u32(&x236, &x237, x235, x220, 0x0);
2925 fiat_p256_addcarryx_u32(&x238, &x239, x237, x222, 0x0);
2926 fiat_p256_mulx_u32(&x240, &x241, x224, UINT32_C(0xffffffff));
2927 fiat_p256_mulx_u32(&x242, &x243, x224, UINT32_C(0xffffffff));
2928 fiat_p256_mulx_u32(&x244, &x245, x224, UINT32_C(0xffffffff));
2929 fiat_p256_mulx_u32(&x246, &x247, x224, UINT32_C(0xffffffff));
2930 fiat_p256_addcarryx_u32(&x248, &x249, 0x0, x247, x244);
2931 fiat_p256_addcarryx_u32(&x250, &x251, x249, x245, x242);
2932 fiat_p256_addcarryx_u32(&x252, &x253, 0x0, x224, x246);
2933 fiat_p256_addcarryx_u32(&x254, &x255, x253, x226, x248);
2934 fiat_p256_addcarryx_u32(&x256, &x257, x255, x228, x250);
2935 fiat_p256_addcarryx_u32(&x258, &x259, x257, x230, (x251 + x243));
2936 fiat_p256_addcarryx_u32(&x260, &x261, x259, x232, 0x0);
2937 fiat_p256_addcarryx_u32(&x262, &x263, x261, x234, 0x0);
2938 fiat_p256_addcarryx_u32(&x264, &x265, x263, x236, x224);
2939 fiat_p256_addcarryx_u32(&x266, &x267, x265, x238, x240);
2940 fiat_p256_addcarryx_u32(&x268, &x269, x267, ((uint32_t)x239 + x223), x241);
2941 fiat_p256_addcarryx_u32(&x270, &x271, 0x0, x254, (arg1[7]));
2942 fiat_p256_addcarryx_u32(&x272, &x273, x271, x256, 0x0);
2943 fiat_p256_addcarryx_u32(&x274, &x275, x273, x258, 0x0);
2944 fiat_p256_addcarryx_u32(&x276, &x277, x275, x260, 0x0);
2945 fiat_p256_addcarryx_u32(&x278, &x279, x277, x262, 0x0);
2946 fiat_p256_addcarryx_u32(&x280, &x281, x279, x264, 0x0);
2947 fiat_p256_addcarryx_u32(&x282, &x283, x281, x266, 0x0);
2948 fiat_p256_addcarryx_u32(&x284, &x285, x283, x268, 0x0);
2949 fiat_p256_mulx_u32(&x286, &x287, x270, UINT32_C(0xffffffff));
2950 fiat_p256_mulx_u32(&x288, &x289, x270, UINT32_C(0xffffffff));
2951 fiat_p256_mulx_u32(&x290, &x291, x270, UINT32_C(0xffffffff));
2952 fiat_p256_mulx_u32(&x292, &x293, x270, UINT32_C(0xffffffff));
2953 fiat_p256_addcarryx_u32(&x294, &x295, 0x0, x293, x290);
2954 fiat_p256_addcarryx_u32(&x296, &x297, x295, x291, x288);
2955 fiat_p256_addcarryx_u32(&x298, &x299, 0x0, x270, x292);
2956 fiat_p256_addcarryx_u32(&x300, &x301, x299, x272, x294);
2957 fiat_p256_addcarryx_u32(&x302, &x303, x301, x274, x296);
2958 fiat_p256_addcarryx_u32(&x304, &x305, x303, x276, (x297 + x289));
2959 fiat_p256_addcarryx_u32(&x306, &x307, x305, x278, 0x0);
2960 fiat_p256_addcarryx_u32(&x308, &x309, x307, x280, 0x0);
2961 fiat_p256_addcarryx_u32(&x310, &x311, x309, x282, x270);
2962 fiat_p256_addcarryx_u32(&x312, &x313, x311, x284, x286);
2963 fiat_p256_addcarryx_u32(&x314, &x315, x313, ((uint32_t)x285 + x269), x287);
2964 fiat_p256_subborrowx_u32(&x316, &x317, 0x0, x300, UINT32_C(0xffffffff));
2965 fiat_p256_subborrowx_u32(&x318, &x319, x317, x302, UINT32_C(0xffffffff));
2966 fiat_p256_subborrowx_u32(&x320, &x321, x319, x304, UINT32_C(0xffffffff));
2967 fiat_p256_subborrowx_u32(&x322, &x323, x321, x306, 0x0);
2968 fiat_p256_subborrowx_u32(&x324, &x325, x323, x308, 0x0);
2969 fiat_p256_subborrowx_u32(&x326, &x327, x325, x310, 0x0);
2970 fiat_p256_subborrowx_u32(&x328, &x329, x327, x312, 0x1);
2971 fiat_p256_subborrowx_u32(&x330, &x331, x329, x314, UINT32_C(0xffffffff));
2972 fiat_p256_subborrowx_u32(&x332, &x333, x331, x315, 0x0);
2973 fiat_p256_cmovznz_u32(&x334, x333, x316, x300);
2974 fiat_p256_cmovznz_u32(&x335, x333, x318, x302);
2975 fiat_p256_cmovznz_u32(&x336, x333, x320, x304);
2976 fiat_p256_cmovznz_u32(&x337, x333, x322, x306);
2977 fiat_p256_cmovznz_u32(&x338, x333, x324, x308);
2978 fiat_p256_cmovznz_u32(&x339, x333, x326, x310);
2979 fiat_p256_cmovznz_u32(&x340, x333, x328, x312);
2980 fiat_p256_cmovznz_u32(&x341, x333, x330, x314);
2981 out1[0] = x334;
2982 out1[1] = x335;
2983 out1[2] = x336;
2984 out1[3] = x337;
2985 out1[4] = x338;
2986 out1[5] = x339;
2987 out1[6] = x340;
2988 out1[7] = x341;
2989 }
2990
2991 /*
2992 * The function fiat_p256_to_montgomery translates a field element into the Montgomery domain.
2993 *
2994 * Preconditions:
2995 * 0 ≤ eval arg1 < m
2996 * Postconditions:
2997 * eval (from_montgomery out1) mod m = eval arg1 mod m
2998 * 0 ≤ eval out1 < m
2999 *
3000 */
fiat_p256_to_montgomery(fiat_p256_montgomery_domain_field_element out1,const fiat_p256_non_montgomery_domain_field_element arg1)3001 static FIAT_P256_FIAT_INLINE void fiat_p256_to_montgomery(fiat_p256_montgomery_domain_field_element out1, const fiat_p256_non_montgomery_domain_field_element arg1) {
3002 uint32_t x1;
3003 uint32_t x2;
3004 uint32_t x3;
3005 uint32_t x4;
3006 uint32_t x5;
3007 uint32_t x6;
3008 uint32_t x7;
3009 uint32_t x8;
3010 uint32_t x9;
3011 uint32_t x10;
3012 uint32_t x11;
3013 uint32_t x12;
3014 uint32_t x13;
3015 uint32_t x14;
3016 uint32_t x15;
3017 uint32_t x16;
3018 uint32_t x17;
3019 uint32_t x18;
3020 uint32_t x19;
3021 uint32_t x20;
3022 uint32_t x21;
3023 uint32_t x22;
3024 uint32_t x23;
3025 fiat_p256_uint1 x24;
3026 uint32_t x25;
3027 fiat_p256_uint1 x26;
3028 uint32_t x27;
3029 fiat_p256_uint1 x28;
3030 uint32_t x29;
3031 fiat_p256_uint1 x30;
3032 uint32_t x31;
3033 fiat_p256_uint1 x32;
3034 uint32_t x33;
3035 uint32_t x34;
3036 uint32_t x35;
3037 uint32_t x36;
3038 uint32_t x37;
3039 uint32_t x38;
3040 uint32_t x39;
3041 uint32_t x40;
3042 uint32_t x41;
3043 fiat_p256_uint1 x42;
3044 uint32_t x43;
3045 fiat_p256_uint1 x44;
3046 uint32_t x45;
3047 fiat_p256_uint1 x46;
3048 uint32_t x47;
3049 fiat_p256_uint1 x48;
3050 uint32_t x49;
3051 fiat_p256_uint1 x50;
3052 uint32_t x51;
3053 fiat_p256_uint1 x52;
3054 uint32_t x53;
3055 fiat_p256_uint1 x54;
3056 uint32_t x55;
3057 fiat_p256_uint1 x56;
3058 uint32_t x57;
3059 fiat_p256_uint1 x58;
3060 uint32_t x59;
3061 fiat_p256_uint1 x60;
3062 uint32_t x61;
3063 fiat_p256_uint1 x62;
3064 uint32_t x63;
3065 uint32_t x64;
3066 uint32_t x65;
3067 uint32_t x66;
3068 uint32_t x67;
3069 uint32_t x68;
3070 uint32_t x69;
3071 uint32_t x70;
3072 uint32_t x71;
3073 uint32_t x72;
3074 uint32_t x73;
3075 uint32_t x74;
3076 uint32_t x75;
3077 uint32_t x76;
3078 uint32_t x77;
3079 fiat_p256_uint1 x78;
3080 uint32_t x79;
3081 fiat_p256_uint1 x80;
3082 uint32_t x81;
3083 fiat_p256_uint1 x82;
3084 uint32_t x83;
3085 fiat_p256_uint1 x84;
3086 uint32_t x85;
3087 fiat_p256_uint1 x86;
3088 uint32_t x87;
3089 fiat_p256_uint1 x88;
3090 uint32_t x89;
3091 fiat_p256_uint1 x90;
3092 uint32_t x91;
3093 fiat_p256_uint1 x92;
3094 uint32_t x93;
3095 fiat_p256_uint1 x94;
3096 uint32_t x95;
3097 fiat_p256_uint1 x96;
3098 uint32_t x97;
3099 fiat_p256_uint1 x98;
3100 uint32_t x99;
3101 fiat_p256_uint1 x100;
3102 uint32_t x101;
3103 fiat_p256_uint1 x102;
3104 uint32_t x103;
3105 uint32_t x104;
3106 uint32_t x105;
3107 uint32_t x106;
3108 uint32_t x107;
3109 uint32_t x108;
3110 uint32_t x109;
3111 uint32_t x110;
3112 uint32_t x111;
3113 fiat_p256_uint1 x112;
3114 uint32_t x113;
3115 fiat_p256_uint1 x114;
3116 uint32_t x115;
3117 fiat_p256_uint1 x116;
3118 uint32_t x117;
3119 fiat_p256_uint1 x118;
3120 uint32_t x119;
3121 fiat_p256_uint1 x120;
3122 uint32_t x121;
3123 fiat_p256_uint1 x122;
3124 uint32_t x123;
3125 fiat_p256_uint1 x124;
3126 uint32_t x125;
3127 fiat_p256_uint1 x126;
3128 uint32_t x127;
3129 fiat_p256_uint1 x128;
3130 uint32_t x129;
3131 fiat_p256_uint1 x130;
3132 uint32_t x131;
3133 fiat_p256_uint1 x132;
3134 uint32_t x133;
3135 uint32_t x134;
3136 uint32_t x135;
3137 uint32_t x136;
3138 uint32_t x137;
3139 uint32_t x138;
3140 uint32_t x139;
3141 uint32_t x140;
3142 uint32_t x141;
3143 uint32_t x142;
3144 uint32_t x143;
3145 uint32_t x144;
3146 uint32_t x145;
3147 uint32_t x146;
3148 uint32_t x147;
3149 fiat_p256_uint1 x148;
3150 uint32_t x149;
3151 fiat_p256_uint1 x150;
3152 uint32_t x151;
3153 fiat_p256_uint1 x152;
3154 uint32_t x153;
3155 fiat_p256_uint1 x154;
3156 uint32_t x155;
3157 fiat_p256_uint1 x156;
3158 uint32_t x157;
3159 fiat_p256_uint1 x158;
3160 uint32_t x159;
3161 fiat_p256_uint1 x160;
3162 uint32_t x161;
3163 fiat_p256_uint1 x162;
3164 uint32_t x163;
3165 fiat_p256_uint1 x164;
3166 uint32_t x165;
3167 fiat_p256_uint1 x166;
3168 uint32_t x167;
3169 fiat_p256_uint1 x168;
3170 uint32_t x169;
3171 fiat_p256_uint1 x170;
3172 uint32_t x171;
3173 fiat_p256_uint1 x172;
3174 uint32_t x173;
3175 uint32_t x174;
3176 uint32_t x175;
3177 uint32_t x176;
3178 uint32_t x177;
3179 uint32_t x178;
3180 uint32_t x179;
3181 uint32_t x180;
3182 uint32_t x181;
3183 fiat_p256_uint1 x182;
3184 uint32_t x183;
3185 fiat_p256_uint1 x184;
3186 uint32_t x185;
3187 fiat_p256_uint1 x186;
3188 uint32_t x187;
3189 fiat_p256_uint1 x188;
3190 uint32_t x189;
3191 fiat_p256_uint1 x190;
3192 uint32_t x191;
3193 fiat_p256_uint1 x192;
3194 uint32_t x193;
3195 fiat_p256_uint1 x194;
3196 uint32_t x195;
3197 fiat_p256_uint1 x196;
3198 uint32_t x197;
3199 fiat_p256_uint1 x198;
3200 uint32_t x199;
3201 fiat_p256_uint1 x200;
3202 uint32_t x201;
3203 fiat_p256_uint1 x202;
3204 uint32_t x203;
3205 uint32_t x204;
3206 uint32_t x205;
3207 uint32_t x206;
3208 uint32_t x207;
3209 uint32_t x208;
3210 uint32_t x209;
3211 uint32_t x210;
3212 uint32_t x211;
3213 uint32_t x212;
3214 uint32_t x213;
3215 uint32_t x214;
3216 uint32_t x215;
3217 uint32_t x216;
3218 uint32_t x217;
3219 fiat_p256_uint1 x218;
3220 uint32_t x219;
3221 fiat_p256_uint1 x220;
3222 uint32_t x221;
3223 fiat_p256_uint1 x222;
3224 uint32_t x223;
3225 fiat_p256_uint1 x224;
3226 uint32_t x225;
3227 fiat_p256_uint1 x226;
3228 uint32_t x227;
3229 fiat_p256_uint1 x228;
3230 uint32_t x229;
3231 fiat_p256_uint1 x230;
3232 uint32_t x231;
3233 fiat_p256_uint1 x232;
3234 uint32_t x233;
3235 fiat_p256_uint1 x234;
3236 uint32_t x235;
3237 fiat_p256_uint1 x236;
3238 uint32_t x237;
3239 fiat_p256_uint1 x238;
3240 uint32_t x239;
3241 fiat_p256_uint1 x240;
3242 uint32_t x241;
3243 fiat_p256_uint1 x242;
3244 uint32_t x243;
3245 uint32_t x244;
3246 uint32_t x245;
3247 uint32_t x246;
3248 uint32_t x247;
3249 uint32_t x248;
3250 uint32_t x249;
3251 uint32_t x250;
3252 uint32_t x251;
3253 fiat_p256_uint1 x252;
3254 uint32_t x253;
3255 fiat_p256_uint1 x254;
3256 uint32_t x255;
3257 fiat_p256_uint1 x256;
3258 uint32_t x257;
3259 fiat_p256_uint1 x258;
3260 uint32_t x259;
3261 fiat_p256_uint1 x260;
3262 uint32_t x261;
3263 fiat_p256_uint1 x262;
3264 uint32_t x263;
3265 fiat_p256_uint1 x264;
3266 uint32_t x265;
3267 fiat_p256_uint1 x266;
3268 uint32_t x267;
3269 fiat_p256_uint1 x268;
3270 uint32_t x269;
3271 fiat_p256_uint1 x270;
3272 uint32_t x271;
3273 fiat_p256_uint1 x272;
3274 uint32_t x273;
3275 uint32_t x274;
3276 uint32_t x275;
3277 uint32_t x276;
3278 uint32_t x277;
3279 uint32_t x278;
3280 uint32_t x279;
3281 uint32_t x280;
3282 uint32_t x281;
3283 uint32_t x282;
3284 uint32_t x283;
3285 uint32_t x284;
3286 uint32_t x285;
3287 uint32_t x286;
3288 uint32_t x287;
3289 fiat_p256_uint1 x288;
3290 uint32_t x289;
3291 fiat_p256_uint1 x290;
3292 uint32_t x291;
3293 fiat_p256_uint1 x292;
3294 uint32_t x293;
3295 fiat_p256_uint1 x294;
3296 uint32_t x295;
3297 fiat_p256_uint1 x296;
3298 uint32_t x297;
3299 fiat_p256_uint1 x298;
3300 uint32_t x299;
3301 fiat_p256_uint1 x300;
3302 uint32_t x301;
3303 fiat_p256_uint1 x302;
3304 uint32_t x303;
3305 fiat_p256_uint1 x304;
3306 uint32_t x305;
3307 fiat_p256_uint1 x306;
3308 uint32_t x307;
3309 fiat_p256_uint1 x308;
3310 uint32_t x309;
3311 fiat_p256_uint1 x310;
3312 uint32_t x311;
3313 fiat_p256_uint1 x312;
3314 uint32_t x313;
3315 uint32_t x314;
3316 uint32_t x315;
3317 uint32_t x316;
3318 uint32_t x317;
3319 uint32_t x318;
3320 uint32_t x319;
3321 uint32_t x320;
3322 uint32_t x321;
3323 fiat_p256_uint1 x322;
3324 uint32_t x323;
3325 fiat_p256_uint1 x324;
3326 uint32_t x325;
3327 fiat_p256_uint1 x326;
3328 uint32_t x327;
3329 fiat_p256_uint1 x328;
3330 uint32_t x329;
3331 fiat_p256_uint1 x330;
3332 uint32_t x331;
3333 fiat_p256_uint1 x332;
3334 uint32_t x333;
3335 fiat_p256_uint1 x334;
3336 uint32_t x335;
3337 fiat_p256_uint1 x336;
3338 uint32_t x337;
3339 fiat_p256_uint1 x338;
3340 uint32_t x339;
3341 fiat_p256_uint1 x340;
3342 uint32_t x341;
3343 fiat_p256_uint1 x342;
3344 uint32_t x343;
3345 uint32_t x344;
3346 uint32_t x345;
3347 uint32_t x346;
3348 uint32_t x347;
3349 uint32_t x348;
3350 uint32_t x349;
3351 uint32_t x350;
3352 uint32_t x351;
3353 uint32_t x352;
3354 uint32_t x353;
3355 uint32_t x354;
3356 uint32_t x355;
3357 uint32_t x356;
3358 uint32_t x357;
3359 fiat_p256_uint1 x358;
3360 uint32_t x359;
3361 fiat_p256_uint1 x360;
3362 uint32_t x361;
3363 fiat_p256_uint1 x362;
3364 uint32_t x363;
3365 fiat_p256_uint1 x364;
3366 uint32_t x365;
3367 fiat_p256_uint1 x366;
3368 uint32_t x367;
3369 fiat_p256_uint1 x368;
3370 uint32_t x369;
3371 fiat_p256_uint1 x370;
3372 uint32_t x371;
3373 fiat_p256_uint1 x372;
3374 uint32_t x373;
3375 fiat_p256_uint1 x374;
3376 uint32_t x375;
3377 fiat_p256_uint1 x376;
3378 uint32_t x377;
3379 fiat_p256_uint1 x378;
3380 uint32_t x379;
3381 fiat_p256_uint1 x380;
3382 uint32_t x381;
3383 fiat_p256_uint1 x382;
3384 uint32_t x383;
3385 uint32_t x384;
3386 uint32_t x385;
3387 uint32_t x386;
3388 uint32_t x387;
3389 uint32_t x388;
3390 uint32_t x389;
3391 uint32_t x390;
3392 uint32_t x391;
3393 fiat_p256_uint1 x392;
3394 uint32_t x393;
3395 fiat_p256_uint1 x394;
3396 uint32_t x395;
3397 fiat_p256_uint1 x396;
3398 uint32_t x397;
3399 fiat_p256_uint1 x398;
3400 uint32_t x399;
3401 fiat_p256_uint1 x400;
3402 uint32_t x401;
3403 fiat_p256_uint1 x402;
3404 uint32_t x403;
3405 fiat_p256_uint1 x404;
3406 uint32_t x405;
3407 fiat_p256_uint1 x406;
3408 uint32_t x407;
3409 fiat_p256_uint1 x408;
3410 uint32_t x409;
3411 fiat_p256_uint1 x410;
3412 uint32_t x411;
3413 fiat_p256_uint1 x412;
3414 uint32_t x413;
3415 uint32_t x414;
3416 uint32_t x415;
3417 uint32_t x416;
3418 uint32_t x417;
3419 uint32_t x418;
3420 uint32_t x419;
3421 uint32_t x420;
3422 uint32_t x421;
3423 uint32_t x422;
3424 uint32_t x423;
3425 uint32_t x424;
3426 uint32_t x425;
3427 uint32_t x426;
3428 uint32_t x427;
3429 fiat_p256_uint1 x428;
3430 uint32_t x429;
3431 fiat_p256_uint1 x430;
3432 uint32_t x431;
3433 fiat_p256_uint1 x432;
3434 uint32_t x433;
3435 fiat_p256_uint1 x434;
3436 uint32_t x435;
3437 fiat_p256_uint1 x436;
3438 uint32_t x437;
3439 fiat_p256_uint1 x438;
3440 uint32_t x439;
3441 fiat_p256_uint1 x440;
3442 uint32_t x441;
3443 fiat_p256_uint1 x442;
3444 uint32_t x443;
3445 fiat_p256_uint1 x444;
3446 uint32_t x445;
3447 fiat_p256_uint1 x446;
3448 uint32_t x447;
3449 fiat_p256_uint1 x448;
3450 uint32_t x449;
3451 fiat_p256_uint1 x450;
3452 uint32_t x451;
3453 fiat_p256_uint1 x452;
3454 uint32_t x453;
3455 uint32_t x454;
3456 uint32_t x455;
3457 uint32_t x456;
3458 uint32_t x457;
3459 uint32_t x458;
3460 uint32_t x459;
3461 uint32_t x460;
3462 uint32_t x461;
3463 fiat_p256_uint1 x462;
3464 uint32_t x463;
3465 fiat_p256_uint1 x464;
3466 uint32_t x465;
3467 fiat_p256_uint1 x466;
3468 uint32_t x467;
3469 fiat_p256_uint1 x468;
3470 uint32_t x469;
3471 fiat_p256_uint1 x470;
3472 uint32_t x471;
3473 fiat_p256_uint1 x472;
3474 uint32_t x473;
3475 fiat_p256_uint1 x474;
3476 uint32_t x475;
3477 fiat_p256_uint1 x476;
3478 uint32_t x477;
3479 fiat_p256_uint1 x478;
3480 uint32_t x479;
3481 fiat_p256_uint1 x480;
3482 uint32_t x481;
3483 fiat_p256_uint1 x482;
3484 uint32_t x483;
3485 uint32_t x484;
3486 uint32_t x485;
3487 uint32_t x486;
3488 uint32_t x487;
3489 uint32_t x488;
3490 uint32_t x489;
3491 uint32_t x490;
3492 uint32_t x491;
3493 uint32_t x492;
3494 uint32_t x493;
3495 uint32_t x494;
3496 uint32_t x495;
3497 uint32_t x496;
3498 uint32_t x497;
3499 fiat_p256_uint1 x498;
3500 uint32_t x499;
3501 fiat_p256_uint1 x500;
3502 uint32_t x501;
3503 fiat_p256_uint1 x502;
3504 uint32_t x503;
3505 fiat_p256_uint1 x504;
3506 uint32_t x505;
3507 fiat_p256_uint1 x506;
3508 uint32_t x507;
3509 fiat_p256_uint1 x508;
3510 uint32_t x509;
3511 fiat_p256_uint1 x510;
3512 uint32_t x511;
3513 fiat_p256_uint1 x512;
3514 uint32_t x513;
3515 fiat_p256_uint1 x514;
3516 uint32_t x515;
3517 fiat_p256_uint1 x516;
3518 uint32_t x517;
3519 fiat_p256_uint1 x518;
3520 uint32_t x519;
3521 fiat_p256_uint1 x520;
3522 uint32_t x521;
3523 fiat_p256_uint1 x522;
3524 uint32_t x523;
3525 uint32_t x524;
3526 uint32_t x525;
3527 uint32_t x526;
3528 uint32_t x527;
3529 uint32_t x528;
3530 uint32_t x529;
3531 uint32_t x530;
3532 uint32_t x531;
3533 fiat_p256_uint1 x532;
3534 uint32_t x533;
3535 fiat_p256_uint1 x534;
3536 uint32_t x535;
3537 fiat_p256_uint1 x536;
3538 uint32_t x537;
3539 fiat_p256_uint1 x538;
3540 uint32_t x539;
3541 fiat_p256_uint1 x540;
3542 uint32_t x541;
3543 fiat_p256_uint1 x542;
3544 uint32_t x543;
3545 fiat_p256_uint1 x544;
3546 uint32_t x545;
3547 fiat_p256_uint1 x546;
3548 uint32_t x547;
3549 fiat_p256_uint1 x548;
3550 uint32_t x549;
3551 fiat_p256_uint1 x550;
3552 uint32_t x551;
3553 fiat_p256_uint1 x552;
3554 uint32_t x553;
3555 fiat_p256_uint1 x554;
3556 uint32_t x555;
3557 fiat_p256_uint1 x556;
3558 uint32_t x557;
3559 fiat_p256_uint1 x558;
3560 uint32_t x559;
3561 fiat_p256_uint1 x560;
3562 uint32_t x561;
3563 fiat_p256_uint1 x562;
3564 uint32_t x563;
3565 fiat_p256_uint1 x564;
3566 uint32_t x565;
3567 fiat_p256_uint1 x566;
3568 uint32_t x567;
3569 fiat_p256_uint1 x568;
3570 uint32_t x569;
3571 fiat_p256_uint1 x570;
3572 uint32_t x571;
3573 uint32_t x572;
3574 uint32_t x573;
3575 uint32_t x574;
3576 uint32_t x575;
3577 uint32_t x576;
3578 uint32_t x577;
3579 uint32_t x578;
3580 x1 = (arg1[1]);
3581 x2 = (arg1[2]);
3582 x3 = (arg1[3]);
3583 x4 = (arg1[4]);
3584 x5 = (arg1[5]);
3585 x6 = (arg1[6]);
3586 x7 = (arg1[7]);
3587 x8 = (arg1[0]);
3588 fiat_p256_mulx_u32(&x9, &x10, x8, 0x4);
3589 fiat_p256_mulx_u32(&x11, &x12, x8, UINT32_C(0xfffffffd));
3590 fiat_p256_mulx_u32(&x13, &x14, x8, UINT32_C(0xffffffff));
3591 fiat_p256_mulx_u32(&x15, &x16, x8, UINT32_C(0xfffffffe));
3592 fiat_p256_mulx_u32(&x17, &x18, x8, UINT32_C(0xfffffffb));
3593 fiat_p256_mulx_u32(&x19, &x20, x8, UINT32_C(0xffffffff));
3594 fiat_p256_mulx_u32(&x21, &x22, x8, 0x3);
3595 fiat_p256_addcarryx_u32(&x23, &x24, 0x0, x20, x17);
3596 fiat_p256_addcarryx_u32(&x25, &x26, x24, x18, x15);
3597 fiat_p256_addcarryx_u32(&x27, &x28, x26, x16, x13);
3598 fiat_p256_addcarryx_u32(&x29, &x30, x28, x14, x11);
3599 fiat_p256_addcarryx_u32(&x31, &x32, x30, x12, x9);
3600 fiat_p256_mulx_u32(&x33, &x34, x21, UINT32_C(0xffffffff));
3601 fiat_p256_mulx_u32(&x35, &x36, x21, UINT32_C(0xffffffff));
3602 fiat_p256_mulx_u32(&x37, &x38, x21, UINT32_C(0xffffffff));
3603 fiat_p256_mulx_u32(&x39, &x40, x21, UINT32_C(0xffffffff));
3604 fiat_p256_addcarryx_u32(&x41, &x42, 0x0, x40, x37);
3605 fiat_p256_addcarryx_u32(&x43, &x44, x42, x38, x35);
3606 fiat_p256_addcarryx_u32(&x45, &x46, 0x0, x21, x39);
3607 fiat_p256_addcarryx_u32(&x47, &x48, x46, x22, x41);
3608 fiat_p256_addcarryx_u32(&x49, &x50, x48, x19, x43);
3609 fiat_p256_addcarryx_u32(&x51, &x52, x50, x23, (x44 + x36));
3610 fiat_p256_addcarryx_u32(&x53, &x54, x52, x25, 0x0);
3611 fiat_p256_addcarryx_u32(&x55, &x56, x54, x27, 0x0);
3612 fiat_p256_addcarryx_u32(&x57, &x58, x56, x29, x21);
3613 fiat_p256_addcarryx_u32(&x59, &x60, x58, x31, x33);
3614 fiat_p256_addcarryx_u32(&x61, &x62, x60, (x32 + x10), x34);
3615 fiat_p256_mulx_u32(&x63, &x64, x1, 0x4);
3616 fiat_p256_mulx_u32(&x65, &x66, x1, UINT32_C(0xfffffffd));
3617 fiat_p256_mulx_u32(&x67, &x68, x1, UINT32_C(0xffffffff));
3618 fiat_p256_mulx_u32(&x69, &x70, x1, UINT32_C(0xfffffffe));
3619 fiat_p256_mulx_u32(&x71, &x72, x1, UINT32_C(0xfffffffb));
3620 fiat_p256_mulx_u32(&x73, &x74, x1, UINT32_C(0xffffffff));
3621 fiat_p256_mulx_u32(&x75, &x76, x1, 0x3);
3622 fiat_p256_addcarryx_u32(&x77, &x78, 0x0, x74, x71);
3623 fiat_p256_addcarryx_u32(&x79, &x80, x78, x72, x69);
3624 fiat_p256_addcarryx_u32(&x81, &x82, x80, x70, x67);
3625 fiat_p256_addcarryx_u32(&x83, &x84, x82, x68, x65);
3626 fiat_p256_addcarryx_u32(&x85, &x86, x84, x66, x63);
3627 fiat_p256_addcarryx_u32(&x87, &x88, 0x0, x47, x75);
3628 fiat_p256_addcarryx_u32(&x89, &x90, x88, x49, x76);
3629 fiat_p256_addcarryx_u32(&x91, &x92, x90, x51, x73);
3630 fiat_p256_addcarryx_u32(&x93, &x94, x92, x53, x77);
3631 fiat_p256_addcarryx_u32(&x95, &x96, x94, x55, x79);
3632 fiat_p256_addcarryx_u32(&x97, &x98, x96, x57, x81);
3633 fiat_p256_addcarryx_u32(&x99, &x100, x98, x59, x83);
3634 fiat_p256_addcarryx_u32(&x101, &x102, x100, x61, x85);
3635 fiat_p256_mulx_u32(&x103, &x104, x87, UINT32_C(0xffffffff));
3636 fiat_p256_mulx_u32(&x105, &x106, x87, UINT32_C(0xffffffff));
3637 fiat_p256_mulx_u32(&x107, &x108, x87, UINT32_C(0xffffffff));
3638 fiat_p256_mulx_u32(&x109, &x110, x87, UINT32_C(0xffffffff));
3639 fiat_p256_addcarryx_u32(&x111, &x112, 0x0, x110, x107);
3640 fiat_p256_addcarryx_u32(&x113, &x114, x112, x108, x105);
3641 fiat_p256_addcarryx_u32(&x115, &x116, 0x0, x87, x109);
3642 fiat_p256_addcarryx_u32(&x117, &x118, x116, x89, x111);
3643 fiat_p256_addcarryx_u32(&x119, &x120, x118, x91, x113);
3644 fiat_p256_addcarryx_u32(&x121, &x122, x120, x93, (x114 + x106));
3645 fiat_p256_addcarryx_u32(&x123, &x124, x122, x95, 0x0);
3646 fiat_p256_addcarryx_u32(&x125, &x126, x124, x97, 0x0);
3647 fiat_p256_addcarryx_u32(&x127, &x128, x126, x99, x87);
3648 fiat_p256_addcarryx_u32(&x129, &x130, x128, x101, x103);
3649 fiat_p256_addcarryx_u32(&x131, &x132, x130, (((uint32_t)x102 + x62) + (x86 + x64)), x104);
3650 fiat_p256_mulx_u32(&x133, &x134, x2, 0x4);
3651 fiat_p256_mulx_u32(&x135, &x136, x2, UINT32_C(0xfffffffd));
3652 fiat_p256_mulx_u32(&x137, &x138, x2, UINT32_C(0xffffffff));
3653 fiat_p256_mulx_u32(&x139, &x140, x2, UINT32_C(0xfffffffe));
3654 fiat_p256_mulx_u32(&x141, &x142, x2, UINT32_C(0xfffffffb));
3655 fiat_p256_mulx_u32(&x143, &x144, x2, UINT32_C(0xffffffff));
3656 fiat_p256_mulx_u32(&x145, &x146, x2, 0x3);
3657 fiat_p256_addcarryx_u32(&x147, &x148, 0x0, x144, x141);
3658 fiat_p256_addcarryx_u32(&x149, &x150, x148, x142, x139);
3659 fiat_p256_addcarryx_u32(&x151, &x152, x150, x140, x137);
3660 fiat_p256_addcarryx_u32(&x153, &x154, x152, x138, x135);
3661 fiat_p256_addcarryx_u32(&x155, &x156, x154, x136, x133);
3662 fiat_p256_addcarryx_u32(&x157, &x158, 0x0, x117, x145);
3663 fiat_p256_addcarryx_u32(&x159, &x160, x158, x119, x146);
3664 fiat_p256_addcarryx_u32(&x161, &x162, x160, x121, x143);
3665 fiat_p256_addcarryx_u32(&x163, &x164, x162, x123, x147);
3666 fiat_p256_addcarryx_u32(&x165, &x166, x164, x125, x149);
3667 fiat_p256_addcarryx_u32(&x167, &x168, x166, x127, x151);
3668 fiat_p256_addcarryx_u32(&x169, &x170, x168, x129, x153);
3669 fiat_p256_addcarryx_u32(&x171, &x172, x170, x131, x155);
3670 fiat_p256_mulx_u32(&x173, &x174, x157, UINT32_C(0xffffffff));
3671 fiat_p256_mulx_u32(&x175, &x176, x157, UINT32_C(0xffffffff));
3672 fiat_p256_mulx_u32(&x177, &x178, x157, UINT32_C(0xffffffff));
3673 fiat_p256_mulx_u32(&x179, &x180, x157, UINT32_C(0xffffffff));
3674 fiat_p256_addcarryx_u32(&x181, &x182, 0x0, x180, x177);
3675 fiat_p256_addcarryx_u32(&x183, &x184, x182, x178, x175);
3676 fiat_p256_addcarryx_u32(&x185, &x186, 0x0, x157, x179);
3677 fiat_p256_addcarryx_u32(&x187, &x188, x186, x159, x181);
3678 fiat_p256_addcarryx_u32(&x189, &x190, x188, x161, x183);
3679 fiat_p256_addcarryx_u32(&x191, &x192, x190, x163, (x184 + x176));
3680 fiat_p256_addcarryx_u32(&x193, &x194, x192, x165, 0x0);
3681 fiat_p256_addcarryx_u32(&x195, &x196, x194, x167, 0x0);
3682 fiat_p256_addcarryx_u32(&x197, &x198, x196, x169, x157);
3683 fiat_p256_addcarryx_u32(&x199, &x200, x198, x171, x173);
3684 fiat_p256_addcarryx_u32(&x201, &x202, x200, (((uint32_t)x172 + x132) + (x156 + x134)), x174);
3685 fiat_p256_mulx_u32(&x203, &x204, x3, 0x4);
3686 fiat_p256_mulx_u32(&x205, &x206, x3, UINT32_C(0xfffffffd));
3687 fiat_p256_mulx_u32(&x207, &x208, x3, UINT32_C(0xffffffff));
3688 fiat_p256_mulx_u32(&x209, &x210, x3, UINT32_C(0xfffffffe));
3689 fiat_p256_mulx_u32(&x211, &x212, x3, UINT32_C(0xfffffffb));
3690 fiat_p256_mulx_u32(&x213, &x214, x3, UINT32_C(0xffffffff));
3691 fiat_p256_mulx_u32(&x215, &x216, x3, 0x3);
3692 fiat_p256_addcarryx_u32(&x217, &x218, 0x0, x214, x211);
3693 fiat_p256_addcarryx_u32(&x219, &x220, x218, x212, x209);
3694 fiat_p256_addcarryx_u32(&x221, &x222, x220, x210, x207);
3695 fiat_p256_addcarryx_u32(&x223, &x224, x222, x208, x205);
3696 fiat_p256_addcarryx_u32(&x225, &x226, x224, x206, x203);
3697 fiat_p256_addcarryx_u32(&x227, &x228, 0x0, x187, x215);
3698 fiat_p256_addcarryx_u32(&x229, &x230, x228, x189, x216);
3699 fiat_p256_addcarryx_u32(&x231, &x232, x230, x191, x213);
3700 fiat_p256_addcarryx_u32(&x233, &x234, x232, x193, x217);
3701 fiat_p256_addcarryx_u32(&x235, &x236, x234, x195, x219);
3702 fiat_p256_addcarryx_u32(&x237, &x238, x236, x197, x221);
3703 fiat_p256_addcarryx_u32(&x239, &x240, x238, x199, x223);
3704 fiat_p256_addcarryx_u32(&x241, &x242, x240, x201, x225);
3705 fiat_p256_mulx_u32(&x243, &x244, x227, UINT32_C(0xffffffff));
3706 fiat_p256_mulx_u32(&x245, &x246, x227, UINT32_C(0xffffffff));
3707 fiat_p256_mulx_u32(&x247, &x248, x227, UINT32_C(0xffffffff));
3708 fiat_p256_mulx_u32(&x249, &x250, x227, UINT32_C(0xffffffff));
3709 fiat_p256_addcarryx_u32(&x251, &x252, 0x0, x250, x247);
3710 fiat_p256_addcarryx_u32(&x253, &x254, x252, x248, x245);
3711 fiat_p256_addcarryx_u32(&x255, &x256, 0x0, x227, x249);
3712 fiat_p256_addcarryx_u32(&x257, &x258, x256, x229, x251);
3713 fiat_p256_addcarryx_u32(&x259, &x260, x258, x231, x253);
3714 fiat_p256_addcarryx_u32(&x261, &x262, x260, x233, (x254 + x246));
3715 fiat_p256_addcarryx_u32(&x263, &x264, x262, x235, 0x0);
3716 fiat_p256_addcarryx_u32(&x265, &x266, x264, x237, 0x0);
3717 fiat_p256_addcarryx_u32(&x267, &x268, x266, x239, x227);
3718 fiat_p256_addcarryx_u32(&x269, &x270, x268, x241, x243);
3719 fiat_p256_addcarryx_u32(&x271, &x272, x270, (((uint32_t)x242 + x202) + (x226 + x204)), x244);
3720 fiat_p256_mulx_u32(&x273, &x274, x4, 0x4);
3721 fiat_p256_mulx_u32(&x275, &x276, x4, UINT32_C(0xfffffffd));
3722 fiat_p256_mulx_u32(&x277, &x278, x4, UINT32_C(0xffffffff));
3723 fiat_p256_mulx_u32(&x279, &x280, x4, UINT32_C(0xfffffffe));
3724 fiat_p256_mulx_u32(&x281, &x282, x4, UINT32_C(0xfffffffb));
3725 fiat_p256_mulx_u32(&x283, &x284, x4, UINT32_C(0xffffffff));
3726 fiat_p256_mulx_u32(&x285, &x286, x4, 0x3);
3727 fiat_p256_addcarryx_u32(&x287, &x288, 0x0, x284, x281);
3728 fiat_p256_addcarryx_u32(&x289, &x290, x288, x282, x279);
3729 fiat_p256_addcarryx_u32(&x291, &x292, x290, x280, x277);
3730 fiat_p256_addcarryx_u32(&x293, &x294, x292, x278, x275);
3731 fiat_p256_addcarryx_u32(&x295, &x296, x294, x276, x273);
3732 fiat_p256_addcarryx_u32(&x297, &x298, 0x0, x257, x285);
3733 fiat_p256_addcarryx_u32(&x299, &x300, x298, x259, x286);
3734 fiat_p256_addcarryx_u32(&x301, &x302, x300, x261, x283);
3735 fiat_p256_addcarryx_u32(&x303, &x304, x302, x263, x287);
3736 fiat_p256_addcarryx_u32(&x305, &x306, x304, x265, x289);
3737 fiat_p256_addcarryx_u32(&x307, &x308, x306, x267, x291);
3738 fiat_p256_addcarryx_u32(&x309, &x310, x308, x269, x293);
3739 fiat_p256_addcarryx_u32(&x311, &x312, x310, x271, x295);
3740 fiat_p256_mulx_u32(&x313, &x314, x297, UINT32_C(0xffffffff));
3741 fiat_p256_mulx_u32(&x315, &x316, x297, UINT32_C(0xffffffff));
3742 fiat_p256_mulx_u32(&x317, &x318, x297, UINT32_C(0xffffffff));
3743 fiat_p256_mulx_u32(&x319, &x320, x297, UINT32_C(0xffffffff));
3744 fiat_p256_addcarryx_u32(&x321, &x322, 0x0, x320, x317);
3745 fiat_p256_addcarryx_u32(&x323, &x324, x322, x318, x315);
3746 fiat_p256_addcarryx_u32(&x325, &x326, 0x0, x297, x319);
3747 fiat_p256_addcarryx_u32(&x327, &x328, x326, x299, x321);
3748 fiat_p256_addcarryx_u32(&x329, &x330, x328, x301, x323);
3749 fiat_p256_addcarryx_u32(&x331, &x332, x330, x303, (x324 + x316));
3750 fiat_p256_addcarryx_u32(&x333, &x334, x332, x305, 0x0);
3751 fiat_p256_addcarryx_u32(&x335, &x336, x334, x307, 0x0);
3752 fiat_p256_addcarryx_u32(&x337, &x338, x336, x309, x297);
3753 fiat_p256_addcarryx_u32(&x339, &x340, x338, x311, x313);
3754 fiat_p256_addcarryx_u32(&x341, &x342, x340, (((uint32_t)x312 + x272) + (x296 + x274)), x314);
3755 fiat_p256_mulx_u32(&x343, &x344, x5, 0x4);
3756 fiat_p256_mulx_u32(&x345, &x346, x5, UINT32_C(0xfffffffd));
3757 fiat_p256_mulx_u32(&x347, &x348, x5, UINT32_C(0xffffffff));
3758 fiat_p256_mulx_u32(&x349, &x350, x5, UINT32_C(0xfffffffe));
3759 fiat_p256_mulx_u32(&x351, &x352, x5, UINT32_C(0xfffffffb));
3760 fiat_p256_mulx_u32(&x353, &x354, x5, UINT32_C(0xffffffff));
3761 fiat_p256_mulx_u32(&x355, &x356, x5, 0x3);
3762 fiat_p256_addcarryx_u32(&x357, &x358, 0x0, x354, x351);
3763 fiat_p256_addcarryx_u32(&x359, &x360, x358, x352, x349);
3764 fiat_p256_addcarryx_u32(&x361, &x362, x360, x350, x347);
3765 fiat_p256_addcarryx_u32(&x363, &x364, x362, x348, x345);
3766 fiat_p256_addcarryx_u32(&x365, &x366, x364, x346, x343);
3767 fiat_p256_addcarryx_u32(&x367, &x368, 0x0, x327, x355);
3768 fiat_p256_addcarryx_u32(&x369, &x370, x368, x329, x356);
3769 fiat_p256_addcarryx_u32(&x371, &x372, x370, x331, x353);
3770 fiat_p256_addcarryx_u32(&x373, &x374, x372, x333, x357);
3771 fiat_p256_addcarryx_u32(&x375, &x376, x374, x335, x359);
3772 fiat_p256_addcarryx_u32(&x377, &x378, x376, x337, x361);
3773 fiat_p256_addcarryx_u32(&x379, &x380, x378, x339, x363);
3774 fiat_p256_addcarryx_u32(&x381, &x382, x380, x341, x365);
3775 fiat_p256_mulx_u32(&x383, &x384, x367, UINT32_C(0xffffffff));
3776 fiat_p256_mulx_u32(&x385, &x386, x367, UINT32_C(0xffffffff));
3777 fiat_p256_mulx_u32(&x387, &x388, x367, UINT32_C(0xffffffff));
3778 fiat_p256_mulx_u32(&x389, &x390, x367, UINT32_C(0xffffffff));
3779 fiat_p256_addcarryx_u32(&x391, &x392, 0x0, x390, x387);
3780 fiat_p256_addcarryx_u32(&x393, &x394, x392, x388, x385);
3781 fiat_p256_addcarryx_u32(&x395, &x396, 0x0, x367, x389);
3782 fiat_p256_addcarryx_u32(&x397, &x398, x396, x369, x391);
3783 fiat_p256_addcarryx_u32(&x399, &x400, x398, x371, x393);
3784 fiat_p256_addcarryx_u32(&x401, &x402, x400, x373, (x394 + x386));
3785 fiat_p256_addcarryx_u32(&x403, &x404, x402, x375, 0x0);
3786 fiat_p256_addcarryx_u32(&x405, &x406, x404, x377, 0x0);
3787 fiat_p256_addcarryx_u32(&x407, &x408, x406, x379, x367);
3788 fiat_p256_addcarryx_u32(&x409, &x410, x408, x381, x383);
3789 fiat_p256_addcarryx_u32(&x411, &x412, x410, (((uint32_t)x382 + x342) + (x366 + x344)), x384);
3790 fiat_p256_mulx_u32(&x413, &x414, x6, 0x4);
3791 fiat_p256_mulx_u32(&x415, &x416, x6, UINT32_C(0xfffffffd));
3792 fiat_p256_mulx_u32(&x417, &x418, x6, UINT32_C(0xffffffff));
3793 fiat_p256_mulx_u32(&x419, &x420, x6, UINT32_C(0xfffffffe));
3794 fiat_p256_mulx_u32(&x421, &x422, x6, UINT32_C(0xfffffffb));
3795 fiat_p256_mulx_u32(&x423, &x424, x6, UINT32_C(0xffffffff));
3796 fiat_p256_mulx_u32(&x425, &x426, x6, 0x3);
3797 fiat_p256_addcarryx_u32(&x427, &x428, 0x0, x424, x421);
3798 fiat_p256_addcarryx_u32(&x429, &x430, x428, x422, x419);
3799 fiat_p256_addcarryx_u32(&x431, &x432, x430, x420, x417);
3800 fiat_p256_addcarryx_u32(&x433, &x434, x432, x418, x415);
3801 fiat_p256_addcarryx_u32(&x435, &x436, x434, x416, x413);
3802 fiat_p256_addcarryx_u32(&x437, &x438, 0x0, x397, x425);
3803 fiat_p256_addcarryx_u32(&x439, &x440, x438, x399, x426);
3804 fiat_p256_addcarryx_u32(&x441, &x442, x440, x401, x423);
3805 fiat_p256_addcarryx_u32(&x443, &x444, x442, x403, x427);
3806 fiat_p256_addcarryx_u32(&x445, &x446, x444, x405, x429);
3807 fiat_p256_addcarryx_u32(&x447, &x448, x446, x407, x431);
3808 fiat_p256_addcarryx_u32(&x449, &x450, x448, x409, x433);
3809 fiat_p256_addcarryx_u32(&x451, &x452, x450, x411, x435);
3810 fiat_p256_mulx_u32(&x453, &x454, x437, UINT32_C(0xffffffff));
3811 fiat_p256_mulx_u32(&x455, &x456, x437, UINT32_C(0xffffffff));
3812 fiat_p256_mulx_u32(&x457, &x458, x437, UINT32_C(0xffffffff));
3813 fiat_p256_mulx_u32(&x459, &x460, x437, UINT32_C(0xffffffff));
3814 fiat_p256_addcarryx_u32(&x461, &x462, 0x0, x460, x457);
3815 fiat_p256_addcarryx_u32(&x463, &x464, x462, x458, x455);
3816 fiat_p256_addcarryx_u32(&x465, &x466, 0x0, x437, x459);
3817 fiat_p256_addcarryx_u32(&x467, &x468, x466, x439, x461);
3818 fiat_p256_addcarryx_u32(&x469, &x470, x468, x441, x463);
3819 fiat_p256_addcarryx_u32(&x471, &x472, x470, x443, (x464 + x456));
3820 fiat_p256_addcarryx_u32(&x473, &x474, x472, x445, 0x0);
3821 fiat_p256_addcarryx_u32(&x475, &x476, x474, x447, 0x0);
3822 fiat_p256_addcarryx_u32(&x477, &x478, x476, x449, x437);
3823 fiat_p256_addcarryx_u32(&x479, &x480, x478, x451, x453);
3824 fiat_p256_addcarryx_u32(&x481, &x482, x480, (((uint32_t)x452 + x412) + (x436 + x414)), x454);
3825 fiat_p256_mulx_u32(&x483, &x484, x7, 0x4);
3826 fiat_p256_mulx_u32(&x485, &x486, x7, UINT32_C(0xfffffffd));
3827 fiat_p256_mulx_u32(&x487, &x488, x7, UINT32_C(0xffffffff));
3828 fiat_p256_mulx_u32(&x489, &x490, x7, UINT32_C(0xfffffffe));
3829 fiat_p256_mulx_u32(&x491, &x492, x7, UINT32_C(0xfffffffb));
3830 fiat_p256_mulx_u32(&x493, &x494, x7, UINT32_C(0xffffffff));
3831 fiat_p256_mulx_u32(&x495, &x496, x7, 0x3);
3832 fiat_p256_addcarryx_u32(&x497, &x498, 0x0, x494, x491);
3833 fiat_p256_addcarryx_u32(&x499, &x500, x498, x492, x489);
3834 fiat_p256_addcarryx_u32(&x501, &x502, x500, x490, x487);
3835 fiat_p256_addcarryx_u32(&x503, &x504, x502, x488, x485);
3836 fiat_p256_addcarryx_u32(&x505, &x506, x504, x486, x483);
3837 fiat_p256_addcarryx_u32(&x507, &x508, 0x0, x467, x495);
3838 fiat_p256_addcarryx_u32(&x509, &x510, x508, x469, x496);
3839 fiat_p256_addcarryx_u32(&x511, &x512, x510, x471, x493);
3840 fiat_p256_addcarryx_u32(&x513, &x514, x512, x473, x497);
3841 fiat_p256_addcarryx_u32(&x515, &x516, x514, x475, x499);
3842 fiat_p256_addcarryx_u32(&x517, &x518, x516, x477, x501);
3843 fiat_p256_addcarryx_u32(&x519, &x520, x518, x479, x503);
3844 fiat_p256_addcarryx_u32(&x521, &x522, x520, x481, x505);
3845 fiat_p256_mulx_u32(&x523, &x524, x507, UINT32_C(0xffffffff));
3846 fiat_p256_mulx_u32(&x525, &x526, x507, UINT32_C(0xffffffff));
3847 fiat_p256_mulx_u32(&x527, &x528, x507, UINT32_C(0xffffffff));
3848 fiat_p256_mulx_u32(&x529, &x530, x507, UINT32_C(0xffffffff));
3849 fiat_p256_addcarryx_u32(&x531, &x532, 0x0, x530, x527);
3850 fiat_p256_addcarryx_u32(&x533, &x534, x532, x528, x525);
3851 fiat_p256_addcarryx_u32(&x535, &x536, 0x0, x507, x529);
3852 fiat_p256_addcarryx_u32(&x537, &x538, x536, x509, x531);
3853 fiat_p256_addcarryx_u32(&x539, &x540, x538, x511, x533);
3854 fiat_p256_addcarryx_u32(&x541, &x542, x540, x513, (x534 + x526));
3855 fiat_p256_addcarryx_u32(&x543, &x544, x542, x515, 0x0);
3856 fiat_p256_addcarryx_u32(&x545, &x546, x544, x517, 0x0);
3857 fiat_p256_addcarryx_u32(&x547, &x548, x546, x519, x507);
3858 fiat_p256_addcarryx_u32(&x549, &x550, x548, x521, x523);
3859 fiat_p256_addcarryx_u32(&x551, &x552, x550, (((uint32_t)x522 + x482) + (x506 + x484)), x524);
3860 fiat_p256_subborrowx_u32(&x553, &x554, 0x0, x537, UINT32_C(0xffffffff));
3861 fiat_p256_subborrowx_u32(&x555, &x556, x554, x539, UINT32_C(0xffffffff));
3862 fiat_p256_subborrowx_u32(&x557, &x558, x556, x541, UINT32_C(0xffffffff));
3863 fiat_p256_subborrowx_u32(&x559, &x560, x558, x543, 0x0);
3864 fiat_p256_subborrowx_u32(&x561, &x562, x560, x545, 0x0);
3865 fiat_p256_subborrowx_u32(&x563, &x564, x562, x547, 0x0);
3866 fiat_p256_subborrowx_u32(&x565, &x566, x564, x549, 0x1);
3867 fiat_p256_subborrowx_u32(&x567, &x568, x566, x551, UINT32_C(0xffffffff));
3868 fiat_p256_subborrowx_u32(&x569, &x570, x568, x552, 0x0);
3869 fiat_p256_cmovznz_u32(&x571, x570, x553, x537);
3870 fiat_p256_cmovznz_u32(&x572, x570, x555, x539);
3871 fiat_p256_cmovznz_u32(&x573, x570, x557, x541);
3872 fiat_p256_cmovznz_u32(&x574, x570, x559, x543);
3873 fiat_p256_cmovznz_u32(&x575, x570, x561, x545);
3874 fiat_p256_cmovznz_u32(&x576, x570, x563, x547);
3875 fiat_p256_cmovznz_u32(&x577, x570, x565, x549);
3876 fiat_p256_cmovznz_u32(&x578, x570, x567, x551);
3877 out1[0] = x571;
3878 out1[1] = x572;
3879 out1[2] = x573;
3880 out1[3] = x574;
3881 out1[4] = x575;
3882 out1[5] = x576;
3883 out1[6] = x577;
3884 out1[7] = x578;
3885 }
3886
3887 /*
3888 * The function fiat_p256_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
3889 *
3890 * Preconditions:
3891 * 0 ≤ eval arg1 < m
3892 * Postconditions:
3893 * out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
3894 *
3895 * Input Bounds:
3896 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3897 * Output Bounds:
3898 * out1: [0x0 ~> 0xffffffff]
3899 */
fiat_p256_nonzero(uint32_t * out1,const uint32_t arg1[8])3900 static FIAT_P256_FIAT_INLINE void fiat_p256_nonzero(uint32_t* out1, const uint32_t arg1[8]) {
3901 uint32_t x1;
3902 x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | (arg1[7]))))))));
3903 *out1 = x1;
3904 }
3905
3906 /*
3907 * The function fiat_p256_selectznz is a multi-limb conditional select.
3908 *
3909 * Postconditions:
3910 * eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
3911 *
3912 * Input Bounds:
3913 * arg1: [0x0 ~> 0x1]
3914 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3915 * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3916 * Output Bounds:
3917 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3918 */
fiat_p256_selectznz(uint32_t out1[8],fiat_p256_uint1 arg1,const uint32_t arg2[8],const uint32_t arg3[8])3919 static FIAT_P256_FIAT_INLINE void fiat_p256_selectznz(uint32_t out1[8], fiat_p256_uint1 arg1, const uint32_t arg2[8], const uint32_t arg3[8]) {
3920 uint32_t x1;
3921 uint32_t x2;
3922 uint32_t x3;
3923 uint32_t x4;
3924 uint32_t x5;
3925 uint32_t x6;
3926 uint32_t x7;
3927 uint32_t x8;
3928 fiat_p256_cmovznz_u32(&x1, arg1, (arg2[0]), (arg3[0]));
3929 fiat_p256_cmovznz_u32(&x2, arg1, (arg2[1]), (arg3[1]));
3930 fiat_p256_cmovznz_u32(&x3, arg1, (arg2[2]), (arg3[2]));
3931 fiat_p256_cmovznz_u32(&x4, arg1, (arg2[3]), (arg3[3]));
3932 fiat_p256_cmovznz_u32(&x5, arg1, (arg2[4]), (arg3[4]));
3933 fiat_p256_cmovznz_u32(&x6, arg1, (arg2[5]), (arg3[5]));
3934 fiat_p256_cmovznz_u32(&x7, arg1, (arg2[6]), (arg3[6]));
3935 fiat_p256_cmovznz_u32(&x8, arg1, (arg2[7]), (arg3[7]));
3936 out1[0] = x1;
3937 out1[1] = x2;
3938 out1[2] = x3;
3939 out1[3] = x4;
3940 out1[4] = x5;
3941 out1[5] = x6;
3942 out1[6] = x7;
3943 out1[7] = x8;
3944 }
3945
3946 /*
3947 * The function fiat_p256_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
3948 *
3949 * Preconditions:
3950 * 0 ≤ eval arg1 < m
3951 * Postconditions:
3952 * out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
3953 *
3954 * Input Bounds:
3955 * arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3956 * Output Bounds:
3957 * 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]]
3958 */
fiat_p256_to_bytes(uint8_t out1[32],const uint32_t arg1[8])3959 static FIAT_P256_FIAT_INLINE void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) {
3960 uint32_t x1;
3961 uint32_t x2;
3962 uint32_t x3;
3963 uint32_t x4;
3964 uint32_t x5;
3965 uint32_t x6;
3966 uint32_t x7;
3967 uint32_t x8;
3968 uint8_t x9;
3969 uint32_t x10;
3970 uint8_t x11;
3971 uint32_t x12;
3972 uint8_t x13;
3973 uint8_t x14;
3974 uint8_t x15;
3975 uint32_t x16;
3976 uint8_t x17;
3977 uint32_t x18;
3978 uint8_t x19;
3979 uint8_t x20;
3980 uint8_t x21;
3981 uint32_t x22;
3982 uint8_t x23;
3983 uint32_t x24;
3984 uint8_t x25;
3985 uint8_t x26;
3986 uint8_t x27;
3987 uint32_t x28;
3988 uint8_t x29;
3989 uint32_t x30;
3990 uint8_t x31;
3991 uint8_t x32;
3992 uint8_t x33;
3993 uint32_t x34;
3994 uint8_t x35;
3995 uint32_t x36;
3996 uint8_t x37;
3997 uint8_t x38;
3998 uint8_t x39;
3999 uint32_t x40;
4000 uint8_t x41;
4001 uint32_t x42;
4002 uint8_t x43;
4003 uint8_t x44;
4004 uint8_t x45;
4005 uint32_t x46;
4006 uint8_t x47;
4007 uint32_t x48;
4008 uint8_t x49;
4009 uint8_t x50;
4010 uint8_t x51;
4011 uint32_t x52;
4012 uint8_t x53;
4013 uint32_t x54;
4014 uint8_t x55;
4015 uint8_t x56;
4016 x1 = (arg1[7]);
4017 x2 = (arg1[6]);
4018 x3 = (arg1[5]);
4019 x4 = (arg1[4]);
4020 x5 = (arg1[3]);
4021 x6 = (arg1[2]);
4022 x7 = (arg1[1]);
4023 x8 = (arg1[0]);
4024 x9 = (uint8_t)(x8 & UINT8_C(0xff));
4025 x10 = (x8 >> 8);
4026 x11 = (uint8_t)(x10 & UINT8_C(0xff));
4027 x12 = (x10 >> 8);
4028 x13 = (uint8_t)(x12 & UINT8_C(0xff));
4029 x14 = (uint8_t)(x12 >> 8);
4030 x15 = (uint8_t)(x7 & UINT8_C(0xff));
4031 x16 = (x7 >> 8);
4032 x17 = (uint8_t)(x16 & UINT8_C(0xff));
4033 x18 = (x16 >> 8);
4034 x19 = (uint8_t)(x18 & UINT8_C(0xff));
4035 x20 = (uint8_t)(x18 >> 8);
4036 x21 = (uint8_t)(x6 & UINT8_C(0xff));
4037 x22 = (x6 >> 8);
4038 x23 = (uint8_t)(x22 & UINT8_C(0xff));
4039 x24 = (x22 >> 8);
4040 x25 = (uint8_t)(x24 & UINT8_C(0xff));
4041 x26 = (uint8_t)(x24 >> 8);
4042 x27 = (uint8_t)(x5 & UINT8_C(0xff));
4043 x28 = (x5 >> 8);
4044 x29 = (uint8_t)(x28 & UINT8_C(0xff));
4045 x30 = (x28 >> 8);
4046 x31 = (uint8_t)(x30 & UINT8_C(0xff));
4047 x32 = (uint8_t)(x30 >> 8);
4048 x33 = (uint8_t)(x4 & UINT8_C(0xff));
4049 x34 = (x4 >> 8);
4050 x35 = (uint8_t)(x34 & UINT8_C(0xff));
4051 x36 = (x34 >> 8);
4052 x37 = (uint8_t)(x36 & UINT8_C(0xff));
4053 x38 = (uint8_t)(x36 >> 8);
4054 x39 = (uint8_t)(x3 & UINT8_C(0xff));
4055 x40 = (x3 >> 8);
4056 x41 = (uint8_t)(x40 & UINT8_C(0xff));
4057 x42 = (x40 >> 8);
4058 x43 = (uint8_t)(x42 & UINT8_C(0xff));
4059 x44 = (uint8_t)(x42 >> 8);
4060 x45 = (uint8_t)(x2 & UINT8_C(0xff));
4061 x46 = (x2 >> 8);
4062 x47 = (uint8_t)(x46 & UINT8_C(0xff));
4063 x48 = (x46 >> 8);
4064 x49 = (uint8_t)(x48 & UINT8_C(0xff));
4065 x50 = (uint8_t)(x48 >> 8);
4066 x51 = (uint8_t)(x1 & UINT8_C(0xff));
4067 x52 = (x1 >> 8);
4068 x53 = (uint8_t)(x52 & UINT8_C(0xff));
4069 x54 = (x52 >> 8);
4070 x55 = (uint8_t)(x54 & UINT8_C(0xff));
4071 x56 = (uint8_t)(x54 >> 8);
4072 out1[0] = x9;
4073 out1[1] = x11;
4074 out1[2] = x13;
4075 out1[3] = x14;
4076 out1[4] = x15;
4077 out1[5] = x17;
4078 out1[6] = x19;
4079 out1[7] = x20;
4080 out1[8] = x21;
4081 out1[9] = x23;
4082 out1[10] = x25;
4083 out1[11] = x26;
4084 out1[12] = x27;
4085 out1[13] = x29;
4086 out1[14] = x31;
4087 out1[15] = x32;
4088 out1[16] = x33;
4089 out1[17] = x35;
4090 out1[18] = x37;
4091 out1[19] = x38;
4092 out1[20] = x39;
4093 out1[21] = x41;
4094 out1[22] = x43;
4095 out1[23] = x44;
4096 out1[24] = x45;
4097 out1[25] = x47;
4098 out1[26] = x49;
4099 out1[27] = x50;
4100 out1[28] = x51;
4101 out1[29] = x53;
4102 out1[30] = x55;
4103 out1[31] = x56;
4104 }
4105
4106 /*
4107 * The function fiat_p256_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
4108 *
4109 * Preconditions:
4110 * 0 ≤ bytes_eval arg1 < m
4111 * Postconditions:
4112 * eval out1 mod m = bytes_eval arg1 mod m
4113 * 0 ≤ eval out1 < m
4114 *
4115 * Input Bounds:
4116 * 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]]
4117 * Output Bounds:
4118 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4119 */
fiat_p256_from_bytes(uint32_t out1[8],const uint8_t arg1[32])4120 static FIAT_P256_FIAT_INLINE void fiat_p256_from_bytes(uint32_t out1[8], const uint8_t arg1[32]) {
4121 uint32_t x1;
4122 uint32_t x2;
4123 uint32_t x3;
4124 uint8_t x4;
4125 uint32_t x5;
4126 uint32_t x6;
4127 uint32_t x7;
4128 uint8_t x8;
4129 uint32_t x9;
4130 uint32_t x10;
4131 uint32_t x11;
4132 uint8_t x12;
4133 uint32_t x13;
4134 uint32_t x14;
4135 uint32_t x15;
4136 uint8_t x16;
4137 uint32_t x17;
4138 uint32_t x18;
4139 uint32_t x19;
4140 uint8_t x20;
4141 uint32_t x21;
4142 uint32_t x22;
4143 uint32_t x23;
4144 uint8_t x24;
4145 uint32_t x25;
4146 uint32_t x26;
4147 uint32_t x27;
4148 uint8_t x28;
4149 uint32_t x29;
4150 uint32_t x30;
4151 uint32_t x31;
4152 uint8_t x32;
4153 uint32_t x33;
4154 uint32_t x34;
4155 uint32_t x35;
4156 uint32_t x36;
4157 uint32_t x37;
4158 uint32_t x38;
4159 uint32_t x39;
4160 uint32_t x40;
4161 uint32_t x41;
4162 uint32_t x42;
4163 uint32_t x43;
4164 uint32_t x44;
4165 uint32_t x45;
4166 uint32_t x46;
4167 uint32_t x47;
4168 uint32_t x48;
4169 uint32_t x49;
4170 uint32_t x50;
4171 uint32_t x51;
4172 uint32_t x52;
4173 uint32_t x53;
4174 uint32_t x54;
4175 uint32_t x55;
4176 uint32_t x56;
4177 x1 = ((uint32_t)(arg1[31]) << 24);
4178 x2 = ((uint32_t)(arg1[30]) << 16);
4179 x3 = ((uint32_t)(arg1[29]) << 8);
4180 x4 = (arg1[28]);
4181 x5 = ((uint32_t)(arg1[27]) << 24);
4182 x6 = ((uint32_t)(arg1[26]) << 16);
4183 x7 = ((uint32_t)(arg1[25]) << 8);
4184 x8 = (arg1[24]);
4185 x9 = ((uint32_t)(arg1[23]) << 24);
4186 x10 = ((uint32_t)(arg1[22]) << 16);
4187 x11 = ((uint32_t)(arg1[21]) << 8);
4188 x12 = (arg1[20]);
4189 x13 = ((uint32_t)(arg1[19]) << 24);
4190 x14 = ((uint32_t)(arg1[18]) << 16);
4191 x15 = ((uint32_t)(arg1[17]) << 8);
4192 x16 = (arg1[16]);
4193 x17 = ((uint32_t)(arg1[15]) << 24);
4194 x18 = ((uint32_t)(arg1[14]) << 16);
4195 x19 = ((uint32_t)(arg1[13]) << 8);
4196 x20 = (arg1[12]);
4197 x21 = ((uint32_t)(arg1[11]) << 24);
4198 x22 = ((uint32_t)(arg1[10]) << 16);
4199 x23 = ((uint32_t)(arg1[9]) << 8);
4200 x24 = (arg1[8]);
4201 x25 = ((uint32_t)(arg1[7]) << 24);
4202 x26 = ((uint32_t)(arg1[6]) << 16);
4203 x27 = ((uint32_t)(arg1[5]) << 8);
4204 x28 = (arg1[4]);
4205 x29 = ((uint32_t)(arg1[3]) << 24);
4206 x30 = ((uint32_t)(arg1[2]) << 16);
4207 x31 = ((uint32_t)(arg1[1]) << 8);
4208 x32 = (arg1[0]);
4209 x33 = (x31 + (uint32_t)x32);
4210 x34 = (x30 + x33);
4211 x35 = (x29 + x34);
4212 x36 = (x27 + (uint32_t)x28);
4213 x37 = (x26 + x36);
4214 x38 = (x25 + x37);
4215 x39 = (x23 + (uint32_t)x24);
4216 x40 = (x22 + x39);
4217 x41 = (x21 + x40);
4218 x42 = (x19 + (uint32_t)x20);
4219 x43 = (x18 + x42);
4220 x44 = (x17 + x43);
4221 x45 = (x15 + (uint32_t)x16);
4222 x46 = (x14 + x45);
4223 x47 = (x13 + x46);
4224 x48 = (x11 + (uint32_t)x12);
4225 x49 = (x10 + x48);
4226 x50 = (x9 + x49);
4227 x51 = (x7 + (uint32_t)x8);
4228 x52 = (x6 + x51);
4229 x53 = (x5 + x52);
4230 x54 = (x3 + (uint32_t)x4);
4231 x55 = (x2 + x54);
4232 x56 = (x1 + x55);
4233 out1[0] = x35;
4234 out1[1] = x38;
4235 out1[2] = x41;
4236 out1[3] = x44;
4237 out1[4] = x47;
4238 out1[5] = x50;
4239 out1[6] = x53;
4240 out1[7] = x56;
4241 }
4242
4243 /*
4244 * The function fiat_p256_set_one returns the field element one in the Montgomery domain.
4245 *
4246 * Postconditions:
4247 * eval (from_montgomery out1) mod m = 1 mod m
4248 * 0 ≤ eval out1 < m
4249 *
4250 */
fiat_p256_set_one(fiat_p256_montgomery_domain_field_element out1)4251 static FIAT_P256_FIAT_INLINE void fiat_p256_set_one(fiat_p256_montgomery_domain_field_element out1) {
4252 out1[0] = 0x1;
4253 out1[1] = 0x0;
4254 out1[2] = 0x0;
4255 out1[3] = UINT32_C(0xffffffff);
4256 out1[4] = UINT32_C(0xffffffff);
4257 out1[5] = UINT32_C(0xffffffff);
4258 out1[6] = UINT32_C(0xfffffffe);
4259 out1[7] = 0x0;
4260 }
4261
4262 /*
4263 * The function fiat_p256_msat returns the saturated representation of the prime modulus.
4264 *
4265 * Postconditions:
4266 * twos_complement_eval out1 = m
4267 * 0 ≤ eval out1 < m
4268 *
4269 * Output Bounds:
4270 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4271 */
fiat_p256_msat(uint32_t out1[9])4272 static FIAT_P256_FIAT_INLINE void fiat_p256_msat(uint32_t out1[9]) {
4273 out1[0] = UINT32_C(0xffffffff);
4274 out1[1] = UINT32_C(0xffffffff);
4275 out1[2] = UINT32_C(0xffffffff);
4276 out1[3] = 0x0;
4277 out1[4] = 0x0;
4278 out1[5] = 0x0;
4279 out1[6] = 0x1;
4280 out1[7] = UINT32_C(0xffffffff);
4281 out1[8] = 0x0;
4282 }
4283
4284 /*
4285 * The function fiat_p256_divstep computes a divstep.
4286 *
4287 * Preconditions:
4288 * 0 ≤ eval arg4 < m
4289 * 0 ≤ eval arg5 < m
4290 * Postconditions:
4291 * out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
4292 * twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
4293 * 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⌋)
4294 * 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)
4295 * 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)
4296 * 0 ≤ eval out5 < m
4297 * 0 ≤ eval out5 < m
4298 * 0 ≤ eval out2 < m
4299 * 0 ≤ eval out3 < m
4300 *
4301 * Input Bounds:
4302 * arg1: [0x0 ~> 0xffffffff]
4303 * arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4304 * arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4305 * arg4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4306 * arg5: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4307 * Output Bounds:
4308 * out1: [0x0 ~> 0xffffffff]
4309 * out2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4310 * out3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4311 * out4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4312 * out5: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4313 */
fiat_p256_divstep(uint32_t * out1,uint32_t out2[9],uint32_t out3[9],uint32_t out4[8],uint32_t out5[8],uint32_t arg1,const uint32_t arg2[9],const uint32_t arg3[9],const uint32_t arg4[8],const uint32_t arg5[8])4314 static FIAT_P256_FIAT_INLINE void fiat_p256_divstep(uint32_t* out1, uint32_t out2[9], uint32_t out3[9], uint32_t out4[8], uint32_t out5[8], uint32_t arg1, const uint32_t arg2[9], const uint32_t arg3[9], const uint32_t arg4[8], const uint32_t arg5[8]) {
4315 uint32_t x1;
4316 fiat_p256_uint1 x2;
4317 fiat_p256_uint1 x3;
4318 uint32_t x4;
4319 fiat_p256_uint1 x5;
4320 uint32_t x6;
4321 uint32_t x7;
4322 uint32_t x8;
4323 uint32_t x9;
4324 uint32_t x10;
4325 uint32_t x11;
4326 uint32_t x12;
4327 uint32_t x13;
4328 uint32_t x14;
4329 uint32_t x15;
4330 uint32_t x16;
4331 fiat_p256_uint1 x17;
4332 uint32_t x18;
4333 fiat_p256_uint1 x19;
4334 uint32_t x20;
4335 fiat_p256_uint1 x21;
4336 uint32_t x22;
4337 fiat_p256_uint1 x23;
4338 uint32_t x24;
4339 fiat_p256_uint1 x25;
4340 uint32_t x26;
4341 fiat_p256_uint1 x27;
4342 uint32_t x28;
4343 fiat_p256_uint1 x29;
4344 uint32_t x30;
4345 fiat_p256_uint1 x31;
4346 uint32_t x32;
4347 fiat_p256_uint1 x33;
4348 uint32_t x34;
4349 uint32_t x35;
4350 uint32_t x36;
4351 uint32_t x37;
4352 uint32_t x38;
4353 uint32_t x39;
4354 uint32_t x40;
4355 uint32_t x41;
4356 uint32_t x42;
4357 uint32_t x43;
4358 uint32_t x44;
4359 uint32_t x45;
4360 uint32_t x46;
4361 uint32_t x47;
4362 uint32_t x48;
4363 uint32_t x49;
4364 uint32_t x50;
4365 uint32_t x51;
4366 fiat_p256_uint1 x52;
4367 uint32_t x53;
4368 fiat_p256_uint1 x54;
4369 uint32_t x55;
4370 fiat_p256_uint1 x56;
4371 uint32_t x57;
4372 fiat_p256_uint1 x58;
4373 uint32_t x59;
4374 fiat_p256_uint1 x60;
4375 uint32_t x61;
4376 fiat_p256_uint1 x62;
4377 uint32_t x63;
4378 fiat_p256_uint1 x64;
4379 uint32_t x65;
4380 fiat_p256_uint1 x66;
4381 uint32_t x67;
4382 fiat_p256_uint1 x68;
4383 uint32_t x69;
4384 fiat_p256_uint1 x70;
4385 uint32_t x71;
4386 fiat_p256_uint1 x72;
4387 uint32_t x73;
4388 fiat_p256_uint1 x74;
4389 uint32_t x75;
4390 fiat_p256_uint1 x76;
4391 uint32_t x77;
4392 fiat_p256_uint1 x78;
4393 uint32_t x79;
4394 fiat_p256_uint1 x80;
4395 uint32_t x81;
4396 fiat_p256_uint1 x82;
4397 uint32_t x83;
4398 fiat_p256_uint1 x84;
4399 uint32_t x85;
4400 uint32_t x86;
4401 uint32_t x87;
4402 uint32_t x88;
4403 uint32_t x89;
4404 uint32_t x90;
4405 uint32_t x91;
4406 uint32_t x92;
4407 uint32_t x93;
4408 fiat_p256_uint1 x94;
4409 uint32_t x95;
4410 fiat_p256_uint1 x96;
4411 uint32_t x97;
4412 fiat_p256_uint1 x98;
4413 uint32_t x99;
4414 fiat_p256_uint1 x100;
4415 uint32_t x101;
4416 fiat_p256_uint1 x102;
4417 uint32_t x103;
4418 fiat_p256_uint1 x104;
4419 uint32_t x105;
4420 fiat_p256_uint1 x106;
4421 uint32_t x107;
4422 fiat_p256_uint1 x108;
4423 uint32_t x109;
4424 uint32_t x110;
4425 fiat_p256_uint1 x111;
4426 uint32_t x112;
4427 fiat_p256_uint1 x113;
4428 uint32_t x114;
4429 fiat_p256_uint1 x115;
4430 uint32_t x116;
4431 fiat_p256_uint1 x117;
4432 uint32_t x118;
4433 fiat_p256_uint1 x119;
4434 uint32_t x120;
4435 fiat_p256_uint1 x121;
4436 uint32_t x122;
4437 fiat_p256_uint1 x123;
4438 uint32_t x124;
4439 fiat_p256_uint1 x125;
4440 uint32_t x126;
4441 uint32_t x127;
4442 uint32_t x128;
4443 uint32_t x129;
4444 uint32_t x130;
4445 uint32_t x131;
4446 uint32_t x132;
4447 uint32_t x133;
4448 fiat_p256_uint1 x134;
4449 uint32_t x135;
4450 uint32_t x136;
4451 uint32_t x137;
4452 uint32_t x138;
4453 uint32_t x139;
4454 uint32_t x140;
4455 uint32_t x141;
4456 uint32_t x142;
4457 uint32_t x143;
4458 uint32_t x144;
4459 fiat_p256_uint1 x145;
4460 uint32_t x146;
4461 fiat_p256_uint1 x147;
4462 uint32_t x148;
4463 fiat_p256_uint1 x149;
4464 uint32_t x150;
4465 fiat_p256_uint1 x151;
4466 uint32_t x152;
4467 fiat_p256_uint1 x153;
4468 uint32_t x154;
4469 fiat_p256_uint1 x155;
4470 uint32_t x156;
4471 fiat_p256_uint1 x157;
4472 uint32_t x158;
4473 fiat_p256_uint1 x159;
4474 uint32_t x160;
4475 fiat_p256_uint1 x161;
4476 uint32_t x162;
4477 uint32_t x163;
4478 uint32_t x164;
4479 uint32_t x165;
4480 uint32_t x166;
4481 uint32_t x167;
4482 uint32_t x168;
4483 uint32_t x169;
4484 uint32_t x170;
4485 fiat_p256_uint1 x171;
4486 uint32_t x172;
4487 fiat_p256_uint1 x173;
4488 uint32_t x174;
4489 fiat_p256_uint1 x175;
4490 uint32_t x176;
4491 fiat_p256_uint1 x177;
4492 uint32_t x178;
4493 fiat_p256_uint1 x179;
4494 uint32_t x180;
4495 fiat_p256_uint1 x181;
4496 uint32_t x182;
4497 fiat_p256_uint1 x183;
4498 uint32_t x184;
4499 fiat_p256_uint1 x185;
4500 uint32_t x186;
4501 fiat_p256_uint1 x187;
4502 uint32_t x188;
4503 fiat_p256_uint1 x189;
4504 uint32_t x190;
4505 fiat_p256_uint1 x191;
4506 uint32_t x192;
4507 fiat_p256_uint1 x193;
4508 uint32_t x194;
4509 fiat_p256_uint1 x195;
4510 uint32_t x196;
4511 fiat_p256_uint1 x197;
4512 uint32_t x198;
4513 fiat_p256_uint1 x199;
4514 uint32_t x200;
4515 fiat_p256_uint1 x201;
4516 uint32_t x202;
4517 fiat_p256_uint1 x203;
4518 uint32_t x204;
4519 fiat_p256_uint1 x205;
4520 uint32_t x206;
4521 uint32_t x207;
4522 uint32_t x208;
4523 uint32_t x209;
4524 uint32_t x210;
4525 uint32_t x211;
4526 uint32_t x212;
4527 uint32_t x213;
4528 uint32_t x214;
4529 uint32_t x215;
4530 uint32_t x216;
4531 uint32_t x217;
4532 uint32_t x218;
4533 uint32_t x219;
4534 uint32_t x220;
4535 uint32_t x221;
4536 uint32_t x222;
4537 uint32_t x223;
4538 uint32_t x224;
4539 uint32_t x225;
4540 uint32_t x226;
4541 uint32_t x227;
4542 uint32_t x228;
4543 uint32_t x229;
4544 uint32_t x230;
4545 fiat_p256_addcarryx_u32(&x1, &x2, 0x0, (~arg1), 0x1);
4546 x3 = (fiat_p256_uint1)((fiat_p256_uint1)(x1 >> 31) & (fiat_p256_uint1)((arg3[0]) & 0x1));
4547 fiat_p256_addcarryx_u32(&x4, &x5, 0x0, (~arg1), 0x1);
4548 fiat_p256_cmovznz_u32(&x6, x3, arg1, x4);
4549 fiat_p256_cmovznz_u32(&x7, x3, (arg2[0]), (arg3[0]));
4550 fiat_p256_cmovznz_u32(&x8, x3, (arg2[1]), (arg3[1]));
4551 fiat_p256_cmovznz_u32(&x9, x3, (arg2[2]), (arg3[2]));
4552 fiat_p256_cmovznz_u32(&x10, x3, (arg2[3]), (arg3[3]));
4553 fiat_p256_cmovznz_u32(&x11, x3, (arg2[4]), (arg3[4]));
4554 fiat_p256_cmovznz_u32(&x12, x3, (arg2[5]), (arg3[5]));
4555 fiat_p256_cmovznz_u32(&x13, x3, (arg2[6]), (arg3[6]));
4556 fiat_p256_cmovznz_u32(&x14, x3, (arg2[7]), (arg3[7]));
4557 fiat_p256_cmovznz_u32(&x15, x3, (arg2[8]), (arg3[8]));
4558 fiat_p256_addcarryx_u32(&x16, &x17, 0x0, 0x1, (~(arg2[0])));
4559 fiat_p256_addcarryx_u32(&x18, &x19, x17, 0x0, (~(arg2[1])));
4560 fiat_p256_addcarryx_u32(&x20, &x21, x19, 0x0, (~(arg2[2])));
4561 fiat_p256_addcarryx_u32(&x22, &x23, x21, 0x0, (~(arg2[3])));
4562 fiat_p256_addcarryx_u32(&x24, &x25, x23, 0x0, (~(arg2[4])));
4563 fiat_p256_addcarryx_u32(&x26, &x27, x25, 0x0, (~(arg2[5])));
4564 fiat_p256_addcarryx_u32(&x28, &x29, x27, 0x0, (~(arg2[6])));
4565 fiat_p256_addcarryx_u32(&x30, &x31, x29, 0x0, (~(arg2[7])));
4566 fiat_p256_addcarryx_u32(&x32, &x33, x31, 0x0, (~(arg2[8])));
4567 fiat_p256_cmovznz_u32(&x34, x3, (arg3[0]), x16);
4568 fiat_p256_cmovznz_u32(&x35, x3, (arg3[1]), x18);
4569 fiat_p256_cmovznz_u32(&x36, x3, (arg3[2]), x20);
4570 fiat_p256_cmovznz_u32(&x37, x3, (arg3[3]), x22);
4571 fiat_p256_cmovznz_u32(&x38, x3, (arg3[4]), x24);
4572 fiat_p256_cmovznz_u32(&x39, x3, (arg3[5]), x26);
4573 fiat_p256_cmovznz_u32(&x40, x3, (arg3[6]), x28);
4574 fiat_p256_cmovznz_u32(&x41, x3, (arg3[7]), x30);
4575 fiat_p256_cmovznz_u32(&x42, x3, (arg3[8]), x32);
4576 fiat_p256_cmovznz_u32(&x43, x3, (arg4[0]), (arg5[0]));
4577 fiat_p256_cmovznz_u32(&x44, x3, (arg4[1]), (arg5[1]));
4578 fiat_p256_cmovznz_u32(&x45, x3, (arg4[2]), (arg5[2]));
4579 fiat_p256_cmovznz_u32(&x46, x3, (arg4[3]), (arg5[3]));
4580 fiat_p256_cmovznz_u32(&x47, x3, (arg4[4]), (arg5[4]));
4581 fiat_p256_cmovznz_u32(&x48, x3, (arg4[5]), (arg5[5]));
4582 fiat_p256_cmovznz_u32(&x49, x3, (arg4[6]), (arg5[6]));
4583 fiat_p256_cmovznz_u32(&x50, x3, (arg4[7]), (arg5[7]));
4584 fiat_p256_addcarryx_u32(&x51, &x52, 0x0, x43, x43);
4585 fiat_p256_addcarryx_u32(&x53, &x54, x52, x44, x44);
4586 fiat_p256_addcarryx_u32(&x55, &x56, x54, x45, x45);
4587 fiat_p256_addcarryx_u32(&x57, &x58, x56, x46, x46);
4588 fiat_p256_addcarryx_u32(&x59, &x60, x58, x47, x47);
4589 fiat_p256_addcarryx_u32(&x61, &x62, x60, x48, x48);
4590 fiat_p256_addcarryx_u32(&x63, &x64, x62, x49, x49);
4591 fiat_p256_addcarryx_u32(&x65, &x66, x64, x50, x50);
4592 fiat_p256_subborrowx_u32(&x67, &x68, 0x0, x51, UINT32_C(0xffffffff));
4593 fiat_p256_subborrowx_u32(&x69, &x70, x68, x53, UINT32_C(0xffffffff));
4594 fiat_p256_subborrowx_u32(&x71, &x72, x70, x55, UINT32_C(0xffffffff));
4595 fiat_p256_subborrowx_u32(&x73, &x74, x72, x57, 0x0);
4596 fiat_p256_subborrowx_u32(&x75, &x76, x74, x59, 0x0);
4597 fiat_p256_subborrowx_u32(&x77, &x78, x76, x61, 0x0);
4598 fiat_p256_subborrowx_u32(&x79, &x80, x78, x63, 0x1);
4599 fiat_p256_subborrowx_u32(&x81, &x82, x80, x65, UINT32_C(0xffffffff));
4600 fiat_p256_subborrowx_u32(&x83, &x84, x82, x66, 0x0);
4601 x85 = (arg4[7]);
4602 x86 = (arg4[6]);
4603 x87 = (arg4[5]);
4604 x88 = (arg4[4]);
4605 x89 = (arg4[3]);
4606 x90 = (arg4[2]);
4607 x91 = (arg4[1]);
4608 x92 = (arg4[0]);
4609 fiat_p256_subborrowx_u32(&x93, &x94, 0x0, 0x0, x92);
4610 fiat_p256_subborrowx_u32(&x95, &x96, x94, 0x0, x91);
4611 fiat_p256_subborrowx_u32(&x97, &x98, x96, 0x0, x90);
4612 fiat_p256_subborrowx_u32(&x99, &x100, x98, 0x0, x89);
4613 fiat_p256_subborrowx_u32(&x101, &x102, x100, 0x0, x88);
4614 fiat_p256_subborrowx_u32(&x103, &x104, x102, 0x0, x87);
4615 fiat_p256_subborrowx_u32(&x105, &x106, x104, 0x0, x86);
4616 fiat_p256_subborrowx_u32(&x107, &x108, x106, 0x0, x85);
4617 fiat_p256_cmovznz_u32(&x109, x108, 0x0, UINT32_C(0xffffffff));
4618 fiat_p256_addcarryx_u32(&x110, &x111, 0x0, x93, x109);
4619 fiat_p256_addcarryx_u32(&x112, &x113, x111, x95, x109);
4620 fiat_p256_addcarryx_u32(&x114, &x115, x113, x97, x109);
4621 fiat_p256_addcarryx_u32(&x116, &x117, x115, x99, 0x0);
4622 fiat_p256_addcarryx_u32(&x118, &x119, x117, x101, 0x0);
4623 fiat_p256_addcarryx_u32(&x120, &x121, x119, x103, 0x0);
4624 fiat_p256_addcarryx_u32(&x122, &x123, x121, x105, (fiat_p256_uint1)(x109 & 0x1));
4625 fiat_p256_addcarryx_u32(&x124, &x125, x123, x107, x109);
4626 fiat_p256_cmovznz_u32(&x126, x3, (arg5[0]), x110);
4627 fiat_p256_cmovznz_u32(&x127, x3, (arg5[1]), x112);
4628 fiat_p256_cmovznz_u32(&x128, x3, (arg5[2]), x114);
4629 fiat_p256_cmovznz_u32(&x129, x3, (arg5[3]), x116);
4630 fiat_p256_cmovznz_u32(&x130, x3, (arg5[4]), x118);
4631 fiat_p256_cmovznz_u32(&x131, x3, (arg5[5]), x120);
4632 fiat_p256_cmovznz_u32(&x132, x3, (arg5[6]), x122);
4633 fiat_p256_cmovznz_u32(&x133, x3, (arg5[7]), x124);
4634 x134 = (fiat_p256_uint1)(x34 & 0x1);
4635 fiat_p256_cmovznz_u32(&x135, x134, 0x0, x7);
4636 fiat_p256_cmovznz_u32(&x136, x134, 0x0, x8);
4637 fiat_p256_cmovznz_u32(&x137, x134, 0x0, x9);
4638 fiat_p256_cmovznz_u32(&x138, x134, 0x0, x10);
4639 fiat_p256_cmovznz_u32(&x139, x134, 0x0, x11);
4640 fiat_p256_cmovznz_u32(&x140, x134, 0x0, x12);
4641 fiat_p256_cmovznz_u32(&x141, x134, 0x0, x13);
4642 fiat_p256_cmovznz_u32(&x142, x134, 0x0, x14);
4643 fiat_p256_cmovznz_u32(&x143, x134, 0x0, x15);
4644 fiat_p256_addcarryx_u32(&x144, &x145, 0x0, x34, x135);
4645 fiat_p256_addcarryx_u32(&x146, &x147, x145, x35, x136);
4646 fiat_p256_addcarryx_u32(&x148, &x149, x147, x36, x137);
4647 fiat_p256_addcarryx_u32(&x150, &x151, x149, x37, x138);
4648 fiat_p256_addcarryx_u32(&x152, &x153, x151, x38, x139);
4649 fiat_p256_addcarryx_u32(&x154, &x155, x153, x39, x140);
4650 fiat_p256_addcarryx_u32(&x156, &x157, x155, x40, x141);
4651 fiat_p256_addcarryx_u32(&x158, &x159, x157, x41, x142);
4652 fiat_p256_addcarryx_u32(&x160, &x161, x159, x42, x143);
4653 fiat_p256_cmovznz_u32(&x162, x134, 0x0, x43);
4654 fiat_p256_cmovznz_u32(&x163, x134, 0x0, x44);
4655 fiat_p256_cmovznz_u32(&x164, x134, 0x0, x45);
4656 fiat_p256_cmovznz_u32(&x165, x134, 0x0, x46);
4657 fiat_p256_cmovznz_u32(&x166, x134, 0x0, x47);
4658 fiat_p256_cmovznz_u32(&x167, x134, 0x0, x48);
4659 fiat_p256_cmovznz_u32(&x168, x134, 0x0, x49);
4660 fiat_p256_cmovznz_u32(&x169, x134, 0x0, x50);
4661 fiat_p256_addcarryx_u32(&x170, &x171, 0x0, x126, x162);
4662 fiat_p256_addcarryx_u32(&x172, &x173, x171, x127, x163);
4663 fiat_p256_addcarryx_u32(&x174, &x175, x173, x128, x164);
4664 fiat_p256_addcarryx_u32(&x176, &x177, x175, x129, x165);
4665 fiat_p256_addcarryx_u32(&x178, &x179, x177, x130, x166);
4666 fiat_p256_addcarryx_u32(&x180, &x181, x179, x131, x167);
4667 fiat_p256_addcarryx_u32(&x182, &x183, x181, x132, x168);
4668 fiat_p256_addcarryx_u32(&x184, &x185, x183, x133, x169);
4669 fiat_p256_subborrowx_u32(&x186, &x187, 0x0, x170, UINT32_C(0xffffffff));
4670 fiat_p256_subborrowx_u32(&x188, &x189, x187, x172, UINT32_C(0xffffffff));
4671 fiat_p256_subborrowx_u32(&x190, &x191, x189, x174, UINT32_C(0xffffffff));
4672 fiat_p256_subborrowx_u32(&x192, &x193, x191, x176, 0x0);
4673 fiat_p256_subborrowx_u32(&x194, &x195, x193, x178, 0x0);
4674 fiat_p256_subborrowx_u32(&x196, &x197, x195, x180, 0x0);
4675 fiat_p256_subborrowx_u32(&x198, &x199, x197, x182, 0x1);
4676 fiat_p256_subborrowx_u32(&x200, &x201, x199, x184, UINT32_C(0xffffffff));
4677 fiat_p256_subborrowx_u32(&x202, &x203, x201, x185, 0x0);
4678 fiat_p256_addcarryx_u32(&x204, &x205, 0x0, x6, 0x1);
4679 x206 = ((x144 >> 1) | ((x146 << 31) & UINT32_C(0xffffffff)));
4680 x207 = ((x146 >> 1) | ((x148 << 31) & UINT32_C(0xffffffff)));
4681 x208 = ((x148 >> 1) | ((x150 << 31) & UINT32_C(0xffffffff)));
4682 x209 = ((x150 >> 1) | ((x152 << 31) & UINT32_C(0xffffffff)));
4683 x210 = ((x152 >> 1) | ((x154 << 31) & UINT32_C(0xffffffff)));
4684 x211 = ((x154 >> 1) | ((x156 << 31) & UINT32_C(0xffffffff)));
4685 x212 = ((x156 >> 1) | ((x158 << 31) & UINT32_C(0xffffffff)));
4686 x213 = ((x158 >> 1) | ((x160 << 31) & UINT32_C(0xffffffff)));
4687 x214 = ((x160 & UINT32_C(0x80000000)) | (x160 >> 1));
4688 fiat_p256_cmovznz_u32(&x215, x84, x67, x51);
4689 fiat_p256_cmovznz_u32(&x216, x84, x69, x53);
4690 fiat_p256_cmovznz_u32(&x217, x84, x71, x55);
4691 fiat_p256_cmovznz_u32(&x218, x84, x73, x57);
4692 fiat_p256_cmovznz_u32(&x219, x84, x75, x59);
4693 fiat_p256_cmovznz_u32(&x220, x84, x77, x61);
4694 fiat_p256_cmovznz_u32(&x221, x84, x79, x63);
4695 fiat_p256_cmovznz_u32(&x222, x84, x81, x65);
4696 fiat_p256_cmovznz_u32(&x223, x203, x186, x170);
4697 fiat_p256_cmovznz_u32(&x224, x203, x188, x172);
4698 fiat_p256_cmovznz_u32(&x225, x203, x190, x174);
4699 fiat_p256_cmovznz_u32(&x226, x203, x192, x176);
4700 fiat_p256_cmovznz_u32(&x227, x203, x194, x178);
4701 fiat_p256_cmovznz_u32(&x228, x203, x196, x180);
4702 fiat_p256_cmovznz_u32(&x229, x203, x198, x182);
4703 fiat_p256_cmovznz_u32(&x230, x203, x200, x184);
4704 *out1 = x204;
4705 out2[0] = x7;
4706 out2[1] = x8;
4707 out2[2] = x9;
4708 out2[3] = x10;
4709 out2[4] = x11;
4710 out2[5] = x12;
4711 out2[6] = x13;
4712 out2[7] = x14;
4713 out2[8] = x15;
4714 out3[0] = x206;
4715 out3[1] = x207;
4716 out3[2] = x208;
4717 out3[3] = x209;
4718 out3[4] = x210;
4719 out3[5] = x211;
4720 out3[6] = x212;
4721 out3[7] = x213;
4722 out3[8] = x214;
4723 out4[0] = x215;
4724 out4[1] = x216;
4725 out4[2] = x217;
4726 out4[3] = x218;
4727 out4[4] = x219;
4728 out4[5] = x220;
4729 out4[6] = x221;
4730 out4[7] = x222;
4731 out5[0] = x223;
4732 out5[1] = x224;
4733 out5[2] = x225;
4734 out5[3] = x226;
4735 out5[4] = x227;
4736 out5[5] = x228;
4737 out5[6] = x229;
4738 out5[7] = x230;
4739 }
4740
4741 /*
4742 * The function fiat_p256_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
4743 *
4744 * Postconditions:
4745 * 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⌋)
4746 * 0 ≤ eval out1 < m
4747 *
4748 * Output Bounds:
4749 * out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
4750 */
fiat_p256_divstep_precomp(uint32_t out1[8])4751 static FIAT_P256_FIAT_INLINE void fiat_p256_divstep_precomp(uint32_t out1[8]) {
4752 out1[0] = UINT32_C(0xb8000000);
4753 out1[1] = UINT32_C(0x67ffffff);
4754 out1[2] = UINT32_C(0x38000000);
4755 out1[3] = UINT32_C(0xc0000000);
4756 out1[4] = UINT32_C(0x7fffffff);
4757 out1[5] = UINT32_C(0xd8000000);
4758 out1[6] = UINT32_C(0xffffffff);
4759 out1[7] = UINT32_C(0x2fffffff);
4760 }
4761