18  * entries t[0]...t[9], represents the integer t[0]+2^26 t[1]+2^51 t[2]+2^77
41 	h[0] = a0&((1<<26)-1);                    /* 26 used, 32-26 left.   26 */  in fe_frombytes_impl()
104 	t = -!!t; /* all set if nonzero, 0 if 0 */  in cmovznz32()
119 	{ const u32 x2 = in1[0];  in fe_freeze()
120 	{ u32 x20; u8/*bool*/ x21 = subborrow_u26(0x0, x2, 0x3ffffed, &x20);  in fe_freeze()
121 	{ u32 x23; u8/*bool*/ x24 = subborrow_u25(x21, x4, 0x1ffffff, &x23);  in fe_freeze()
122 	{ u32 x26; u8/*bool*/ x27 = subborrow_u26(x24, x6, 0x3ffffff, &x26);  in fe_freeze()
123 	{ u32 x29; u8/*bool*/ x30 = subborrow_u25(x27, x8, 0x1ffffff, &x29);  in fe_freeze()
124 	{ u32 x32; u8/*bool*/ x33 = subborrow_u26(x30, x10, 0x3ffffff, &x32);  in fe_freeze()
125 	{ u32 x35; u8/*bool*/ x36 = subborrow_u25(x33, x12, 0x1ffffff, &x35);  in fe_freeze()
126 	{ u32 x38; u8/*bool*/ x39 = subborrow_u26(x36, x14, 0x3ffffff, &x38);  in fe_freeze()
127 	{ u32 x41; u8/*bool*/ x42 = subborrow_u25(x39, x16, 0x1ffffff, &x41);  in fe_freeze()
128 	{ u32 x44; u8/*bool*/ x45 = subborrow_u26(x42, x18, 0x3ffffff, &x44);  in fe_freeze()
129 	{ u32 x47; u8/*bool*/ x48 = subborrow_u25(x45, x17, 0x1ffffff, &x47);  in fe_freeze()
130 	{ u32 x49 = cmovznz32(x48, 0x0, 0xffffffff);  in fe_freeze()
131 	{ u32 x50 = (x49 & 0x3ffffed);  in fe_freeze()
132 	{ u32 x52; u8/*bool*/ x53 = addcarryx_u26(0x0, x20, x50, &x52);  in fe_freeze()
133 	{ u32 x54 = (x49 & 0x1ffffff);  in fe_freeze()
135 	{ u32 x58 = (x49 & 0x3ffffff);  in fe_freeze()
137 	{ u32 x62 = (x49 & 0x1ffffff);  in fe_freeze()
139 	{ u32 x66 = (x49 & 0x3ffffff);  in fe_freeze()
141 	{ u32 x70 = (x49 & 0x1ffffff);  in fe_freeze()
143 	{ u32 x74 = (x49 & 0x3ffffff);  in fe_freeze()
145 	{ u32 x78 = (x49 & 0x1ffffff);  in fe_freeze()
147 	{ u32 x82 = (x49 & 0x3ffffff);  in fe_freeze()
149 	{ u32 x86 = (x49 & 0x1ffffff);  in fe_freeze()
151 	out[0] = x52;  in fe_freeze()
168 	s[0] = h[0] >> 0;  in fe_tobytes()
169 	s[1] = h[0] >> 8;  in fe_tobytes()
170 	s[2] = h[0] >> 16;  in fe_tobytes()
171 	s[3] = (h[0] >> 24) | (h[1] << 2);  in fe_tobytes()
184 	s[16] = h[5] >> 0;  in fe_tobytes()
213 /* h = 0 */
216 	memset(h, 0, sizeof(u32) * 10);  in fe_0()
222 	memset(h, 0, sizeof(u32) * 10);  in fe_1()
223 	h->v[0] = 1;  in fe_1()
237 	{ const u32 x5 = in1[0];  in fe_add_impl()
243 	{ const u32 x31 = in2[4];  in fe_add_impl()  local
247 	{ const u32 x23 = in2[0];  in fe_add_impl()
248 	out[0] = (x5 + x23);  in fe_add_impl()
252 	out[4] = (x13 + x31);  in fe_add_impl()
280 	{ const u32 x5 = in1[0];  in fe_sub_impl()
286 	{ const u32 x31 = in2[4];  in fe_sub_impl()  local
290 	{ const u32 x23 = in2[0];  in fe_sub_impl()
291 	out[0] = ((0x7ffffda + x5) - x23);  in fe_sub_impl()
292 	out[1] = ((0x3fffffe + x7) - x25);  in fe_sub_impl()
293 	out[2] = ((0x7fffffe + x9) - x27);  in fe_sub_impl()
294 	out[3] = ((0x3fffffe + x11) - x29);  in fe_sub_impl()
295 	out[4] = ((0x7fffffe + x13) - x31);  in fe_sub_impl()
296 	out[5] = ((0x3fffffe + x15) - x33);  in fe_sub_impl()
297 	out[6] = ((0x7fffffe + x17) - x35);  in fe_sub_impl()
298 	out[7] = ((0x3fffffe + x19) - x37);  in fe_sub_impl()
299 	out[8] = ((0x7fffffe + x21) - x39);  in fe_sub_impl()
300 	out[9] = ((0x3fffffe + x20) - x38);  in fe_sub_impl()
323 	{ const u32 x5 = in1[0];  in fe_mul_impl()
329 	{ const u32 x31 = in2[4];  in fe_mul_impl()  local
333 	{ const u32 x23 = in2[0];  in fe_mul_impl()
336 	{ u64 x42 = ((((u64)(0x2 * x25) * x7) + ((u64)x23 * x9)) + ((u64)x27 * x5));  in fe_mul_impl()
338 …{ u64 x44 = (((((u64)x27 * x9) + (0x2 * (((u64)x25 * x11) + ((u64)x29 * x7)))) + ((u64)x23 * x13))…  in fe_mul_impl()
339 …{ u64 x45 = (((((((u64)x27 * x11) + ((u64)x29 * x9)) + ((u64)x25 * x13)) + ((u64)x31 * x7)) + ((u6…  in fe_mul_impl()
340 …{ u64 x46 = (((((0x2 * ((((u64)x29 * x11) + ((u64)x25 * x15)) + ((u64)x33 * x7))) + ((u64)x27 * x1…  in fe_mul_impl()
341 …{ u64 x47 = (((((((((u64)x29 * x13) + ((u64)x31 * x11)) + ((u64)x27 * x15)) + ((u64)x33 * x9)) + (…  in fe_mul_impl()
342 …{ u64 x48 = (((((((u64)x31 * x13) + (0x2 * (((((u64)x29 * x15) + ((u64)x33 * x11)) + ((u64)x25 * x…  in fe_mul_impl()
343 …{ u64 x49 = (((((((((((u64)x31 * x15) + ((u64)x33 * x13)) + ((u64)x29 * x17)) + ((u64)x35 * x11)) …  in fe_mul_impl()
344 …{ u64 x50 = (((((0x2 * ((((((u64)x33 * x15) + ((u64)x29 * x19)) + ((u64)x37 * x11)) + ((u64)x25 * …  in fe_mul_impl()
345 …{ u64 x51 = (((((((((u64)x33 * x17) + ((u64)x35 * x15)) + ((u64)x31 * x19)) + ((u64)x37 * x13)) + …  in fe_mul_impl()
346 …2 = (((((u64)x35 * x17) + (0x2 * (((((u64)x33 * x19) + ((u64)x37 * x15)) + ((u64)x29 * x20)) + ((u…  in fe_mul_impl()
347 …* x19) + ((u64)x37 * x17)) + ((u64)x33 * x21)) + ((u64)x39 * x15)) + ((u64)x31 * x20)) + ((u64)x38…  in fe_mul_impl()
348 …{ u64 x54 = (((0x2 * ((((u64)x37 * x19) + ((u64)x33 * x20)) + ((u64)x38 * x15))) + ((u64)x35 * x21…  in fe_mul_impl()
350 	{ u64 x56 = (((u64)x39 * x21) + (0x2 * (((u64)x37 * x20) + ((u64)x38 * x19))));  in fe_mul_impl()
352 	{ u64 x58 = ((u64)(0x2 * x38) * x20);  in fe_mul_impl()
353 	{ u64 x59 = (x48 + (x58 << 0x4));  in fe_mul_impl()
354 	{ u64 x60 = (x59 + (x58 << 0x1));  in fe_mul_impl()
356 	{ u64 x62 = (x47 + (x57 << 0x4));  in fe_mul_impl()
357 	{ u64 x63 = (x62 + (x57 << 0x1));  in fe_mul_impl()
359 	{ u64 x65 = (x46 + (x56 << 0x4));  in fe_mul_impl()
360 	{ u64 x66 = (x65 + (x56 << 0x1));  in fe_mul_impl()
362 	{ u64 x68 = (x45 + (x55 << 0x4));  in fe_mul_impl()
363 	{ u64 x69 = (x68 + (x55 << 0x1));  in fe_mul_impl()
365 	{ u64 x71 = (x44 + (x54 << 0x4));  in fe_mul_impl()
366 	{ u64 x72 = (x71 + (x54 << 0x1));  in fe_mul_impl()
368 	{ u64 x74 = (x43 + (x53 << 0x4));  in fe_mul_impl()
369 	{ u64 x75 = (x74 + (x53 << 0x1));  in fe_mul_impl()
371 	{ u64 x77 = (x42 + (x52 << 0x4));  in fe_mul_impl()
372 	{ u64 x78 = (x77 + (x52 << 0x1));  in fe_mul_impl()
374 	{ u64 x80 = (x41 + (x51 << 0x4));  in fe_mul_impl()
375 	{ u64 x81 = (x80 + (x51 << 0x1));  in fe_mul_impl()
377 	{ u64 x83 = (x40 + (x50 << 0x4));  in fe_mul_impl()
378 	{ u64 x84 = (x83 + (x50 << 0x1));  in fe_mul_impl()
380 	{ u64 x86 = (x85 >> 0x1a);  in fe_mul_impl()
381 	{ u32 x87 = ((u32)x85 & 0x3ffffff);  in fe_mul_impl()
383 	{ u64 x89 = (x88 >> 0x19);  in fe_mul_impl()
384 	{ u32 x90 = ((u32)x88 & 0x1ffffff);  in fe_mul_impl()
386 	{ u64 x92 = (x91 >> 0x1a);  in fe_mul_impl()
387 	{ u32 x93 = ((u32)x91 & 0x3ffffff);  in fe_mul_impl()
389 	{ u64 x95 = (x94 >> 0x19);  in fe_mul_impl()
390 	{ u32 x96 = ((u32)x94 & 0x1ffffff);  in fe_mul_impl()
392 	{ u64 x98 = (x97 >> 0x1a);  in fe_mul_impl()
393 	{ u32 x99 = ((u32)x97 & 0x3ffffff);  in fe_mul_impl()
395 	{ u64 x101 = (x100 >> 0x19);  in fe_mul_impl()
396 	{ u32 x102 = ((u32)x100 & 0x1ffffff);  in fe_mul_impl()
398 	{ u64 x104 = (x103 >> 0x1a);  in fe_mul_impl()
399 	{ u32 x105 = ((u32)x103 & 0x3ffffff);  in fe_mul_impl()
401 	{ u64 x107 = (x106 >> 0x19);  in fe_mul_impl()
402 	{ u32 x108 = ((u32)x106 & 0x1ffffff);  in fe_mul_impl()
404 	{ u64 x110 = (x109 >> 0x1a);  in fe_mul_impl()
405 	{ u32 x111 = ((u32)x109 & 0x3ffffff);  in fe_mul_impl()
407 	{ u64 x113 = (x112 >> 0x19);  in fe_mul_impl()
408 	{ u32 x114 = ((u32)x112 & 0x1ffffff);  in fe_mul_impl()
409 	{ u64 x115 = (x87 + (0x13 * x113));  in fe_mul_impl()
410 	{ u32 x116 = (u32) (x115 >> 0x1a);  in fe_mul_impl()
411 	{ u32 x117 = ((u32)x115 & 0x3ffffff);  in fe_mul_impl()
413 	{ u32 x119 = (x118 >> 0x19);  in fe_mul_impl()
414 	{ u32 x120 = (x118 & 0x1ffffff);  in fe_mul_impl()
415 	out[0] = x117;  in fe_mul_impl()
455 	{ const u32 x2 = in1[0];  in fe_sqr_impl()
457 	{ u64 x20 = ((u64)(0x2 * x2) * x4);  in fe_sqr_impl()
458 	{ u64 x21 = (0x2 * (((u64)x4 * x4) + ((u64)x2 * x6)));  in fe_sqr_impl()
459 	{ u64 x22 = (0x2 * (((u64)x4 * x6) + ((u64)x2 * x8)));  in fe_sqr_impl()
460 	{ u64 x23 = ((((u64)x6 * x6) + ((u64)(0x4 * x4) * x8)) + ((u64)(0x2 * x2) * x10));  in fe_sqr_impl()
461 	{ u64 x24 = (0x2 * ((((u64)x6 * x8) + ((u64)x4 * x10)) + ((u64)x2 * x12)));  in fe_sqr_impl()
462 …{ u64 x25 = (0x2 * (((((u64)x8 * x8) + ((u64)x6 * x10)) + ((u64)x2 * x14)) + ((u64)(0x2 * x4) * x1…  in fe_sqr_impl()
463 	{ u64 x26 = (0x2 * (((((u64)x8 * x10) + ((u64)x6 * x12)) + ((u64)x4 * x14)) + ((u64)x2 * x16)));  in fe_sqr_impl()
464 …{ u64 x27 = (((u64)x10 * x10) + (0x2 * ((((u64)x6 * x14) + ((u64)x2 * x18)) + (0x2 * (((u64)x4 * x…  in fe_sqr_impl()
465 …{ u64 x28 = (0x2 * ((((((u64)x10 * x12) + ((u64)x8 * x14)) + ((u64)x6 * x16)) + ((u64)x4 * x18)) +…  in fe_sqr_impl()
466 …{ u64 x29 = (0x2 * (((((u64)x12 * x12) + ((u64)x10 * x14)) + ((u64)x6 * x18)) + (0x2 * (((u64)x8 *…  in fe_sqr_impl()
467 	{ u64 x30 = (0x2 * (((((u64)x12 * x14) + ((u64)x10 * x16)) + ((u64)x8 * x18)) + ((u64)x6 * x17)));  in fe_sqr_impl()
468 …{ u64 x31 = (((u64)x14 * x14) + (0x2 * (((u64)x10 * x18) + (0x2 * (((u64)x12 * x16) + ((u64)x8 * x…  in fe_sqr_impl()  local
469 	{ u64 x32 = (0x2 * ((((u64)x14 * x16) + ((u64)x12 * x18)) + ((u64)x10 * x17)));  in fe_sqr_impl()
470 	{ u64 x33 = (0x2 * ((((u64)x16 * x16) + ((u64)x14 * x18)) + ((u64)(0x2 * x12) * x17)));  in fe_sqr_impl()
471 	{ u64 x34 = (0x2 * (((u64)x16 * x18) + ((u64)x14 * x17)));  in fe_sqr_impl()
472 	{ u64 x35 = (((u64)x18 * x18) + ((u64)(0x4 * x16) * x17));  in fe_sqr_impl()
473 	{ u64 x36 = ((u64)(0x2 * x18) * x17);  in fe_sqr_impl()
474 	{ u64 x37 = ((u64)(0x2 * x17) * x17);  in fe_sqr_impl()
475 	{ u64 x38 = (x27 + (x37 << 0x4));  in fe_sqr_impl()
476 	{ u64 x39 = (x38 + (x37 << 0x1));  in fe_sqr_impl()
478 	{ u64 x41 = (x26 + (x36 << 0x4));  in fe_sqr_impl()
479 	{ u64 x42 = (x41 + (x36 << 0x1));  in fe_sqr_impl()
481 	{ u64 x44 = (x25 + (x35 << 0x4));  in fe_sqr_impl()
482 	{ u64 x45 = (x44 + (x35 << 0x1));  in fe_sqr_impl()
484 	{ u64 x47 = (x24 + (x34 << 0x4));  in fe_sqr_impl()
485 	{ u64 x48 = (x47 + (x34 << 0x1));  in fe_sqr_impl()
487 	{ u64 x50 = (x23 + (x33 << 0x4));  in fe_sqr_impl()
488 	{ u64 x51 = (x50 + (x33 << 0x1));  in fe_sqr_impl()
490 	{ u64 x53 = (x22 + (x32 << 0x4));  in fe_sqr_impl()
491 	{ u64 x54 = (x53 + (x32 << 0x1));  in fe_sqr_impl()
493 	{ u64 x56 = (x21 + (x31 << 0x4));  in fe_sqr_impl()
494 	{ u64 x57 = (x56 + (x31 << 0x1));  in fe_sqr_impl()
495 	{ u64 x58 = (x57 + x31);  in fe_sqr_impl()
496 	{ u64 x59 = (x20 + (x30 << 0x4));  in fe_sqr_impl()
497 	{ u64 x60 = (x59 + (x30 << 0x1));  in fe_sqr_impl()
499 	{ u64 x62 = (x19 + (x29 << 0x4));  in fe_sqr_impl()
500 	{ u64 x63 = (x62 + (x29 << 0x1));  in fe_sqr_impl()
502 	{ u64 x65 = (x64 >> 0x1a);  in fe_sqr_impl()
503 	{ u32 x66 = ((u32)x64 & 0x3ffffff);  in fe_sqr_impl()
505 	{ u64 x68 = (x67 >> 0x19);  in fe_sqr_impl()
506 	{ u32 x69 = ((u32)x67 & 0x1ffffff);  in fe_sqr_impl()
508 	{ u64 x71 = (x70 >> 0x1a);  in fe_sqr_impl()
509 	{ u32 x72 = ((u32)x70 & 0x3ffffff);  in fe_sqr_impl()
511 	{ u64 x74 = (x73 >> 0x19);  in fe_sqr_impl()
512 	{ u32 x75 = ((u32)x73 & 0x1ffffff);  in fe_sqr_impl()
514 	{ u64 x77 = (x76 >> 0x1a);  in fe_sqr_impl()
515 	{ u32 x78 = ((u32)x76 & 0x3ffffff);  in fe_sqr_impl()
517 	{ u64 x80 = (x79 >> 0x19);  in fe_sqr_impl()
518 	{ u32 x81 = ((u32)x79 & 0x1ffffff);  in fe_sqr_impl()
520 	{ u64 x83 = (x82 >> 0x1a);  in fe_sqr_impl()
521 	{ u32 x84 = ((u32)x82 & 0x3ffffff);  in fe_sqr_impl()
523 	{ u64 x86 = (x85 >> 0x19);  in fe_sqr_impl()
524 	{ u32 x87 = ((u32)x85 & 0x1ffffff);  in fe_sqr_impl()
526 	{ u64 x89 = (x88 >> 0x1a);  in fe_sqr_impl()
527 	{ u32 x90 = ((u32)x88 & 0x3ffffff);  in fe_sqr_impl()
529 	{ u64 x92 = (x91 >> 0x19);  in fe_sqr_impl()
530 	{ u32 x93 = ((u32)x91 & 0x1ffffff);  in fe_sqr_impl()
531 	{ u64 x94 = (x66 + (0x13 * x92));  in fe_sqr_impl()
532 	{ u32 x95 = (u32) (x94 >> 0x1a);  in fe_sqr_impl()
533 	{ u32 x96 = ((u32)x94 & 0x3ffffff);  in fe_sqr_impl()
535 	{ u32 x98 = (x97 >> 0x19);  in fe_sqr_impl()
536 	{ u32 x99 = (x97 & 0x1ffffff);  in fe_sqr_impl()
537 	out[0] = x96;  in fe_sqr_impl()
618  * replace (f,g) with (f,g) if b == 0.
620  * Preconditions: b in {0,1}
625 	b = 0 - b;  in fe_cswap()
626 	for (i = 0; i < 10; i++) {  in fe_cswap()
634 /* NOTE: based on fiat-crypto fe_mul, edited for in2=121666, 0, 0.*/
646 	{ const u32 x5 = in1[0];  in fe_mul_121666_impl()
647 	{ const u32 x38 = 0;  in fe_mul_121666_impl()
648 	{ const u32 x39 = 0;  in fe_mul_121666_impl()
649 	{ const u32 x37 = 0;  in fe_mul_121666_impl()
650 	{ const u32 x35 = 0;  in fe_mul_121666_impl()
651 	{ const u32 x33 = 0;  in fe_mul_121666_impl()
652 	{ const u32 x31 = 0;  in fe_mul_121666_impl()  local
653 	{ const u32 x29 = 0;  in fe_mul_121666_impl()
654 	{ const u32 x27 = 0;  in fe_mul_121666_impl()
655 	{ const u32 x25 = 0;  in fe_mul_121666_impl()
659 	{ u64 x42 = ((((u64)(0x2 * x25) * x7) + ((u64)x23 * x9)) + ((u64)x27 * x5));  in fe_mul_121666_impl()
661 …{ u64 x44 = (((((u64)x27 * x9) + (0x2 * (((u64)x25 * x11) + ((u64)x29 * x7)))) + ((u64)x23 * x13))…  in fe_mul_121666_impl()
662 …{ u64 x45 = (((((((u64)x27 * x11) + ((u64)x29 * x9)) + ((u64)x25 * x13)) + ((u64)x31 * x7)) + ((u6…  in fe_mul_121666_impl()
663 …{ u64 x46 = (((((0x2 * ((((u64)x29 * x11) + ((u64)x25 * x15)) + ((u64)x33 * x7))) + ((u64)x27 * x1…  in fe_mul_121666_impl()
664 …{ u64 x47 = (((((((((u64)x29 * x13) + ((u64)x31 * x11)) + ((u64)x27 * x15)) + ((u64)x33 * x9)) + (…  in fe_mul_121666_impl()
665 …{ u64 x48 = (((((((u64)x31 * x13) + (0x2 * (((((u64)x29 * x15) + ((u64)x33 * x11)) + ((u64)x25 * x…  in fe_mul_121666_impl()
666 …{ u64 x49 = (((((((((((u64)x31 * x15) + ((u64)x33 * x13)) + ((u64)x29 * x17)) + ((u64)x35 * x11)) …  in fe_mul_121666_impl()
667 …{ u64 x50 = (((((0x2 * ((((((u64)x33 * x15) + ((u64)x29 * x19)) + ((u64)x37 * x11)) + ((u64)x25 * …  in fe_mul_121666_impl()
668 …{ u64 x51 = (((((((((u64)x33 * x17) + ((u64)x35 * x15)) + ((u64)x31 * x19)) + ((u64)x37 * x13)) + …  in fe_mul_121666_impl()
669 …2 = (((((u64)x35 * x17) + (0x2 * (((((u64)x33 * x19) + ((u64)x37 * x15)) + ((u64)x29 * x20)) + ((u…  in fe_mul_121666_impl()
670 …* x19) + ((u64)x37 * x17)) + ((u64)x33 * x21)) + ((u64)x39 * x15)) + ((u64)x31 * x20)) + ((u64)x38…  in fe_mul_121666_impl()
671 …{ u64 x54 = (((0x2 * ((((u64)x37 * x19) + ((u64)x33 * x20)) + ((u64)x38 * x15))) + ((u64)x35 * x21…  in fe_mul_121666_impl()
673 	{ u64 x56 = (((u64)x39 * x21) + (0x2 * (((u64)x37 * x20) + ((u64)x38 * x19))));  in fe_mul_121666_impl()
675 	{ u64 x58 = ((u64)(0x2 * x38) * x20);  in fe_mul_121666_impl()
676 	{ u64 x59 = (x48 + (x58 << 0x4));  in fe_mul_121666_impl()
677 	{ u64 x60 = (x59 + (x58 << 0x1));  in fe_mul_121666_impl()
679 	{ u64 x62 = (x47 + (x57 << 0x4));  in fe_mul_121666_impl()
680 	{ u64 x63 = (x62 + (x57 << 0x1));  in fe_mul_121666_impl()
682 	{ u64 x65 = (x46 + (x56 << 0x4));  in fe_mul_121666_impl()
683 	{ u64 x66 = (x65 + (x56 << 0x1));  in fe_mul_121666_impl()
685 	{ u64 x68 = (x45 + (x55 << 0x4));  in fe_mul_121666_impl()
686 	{ u64 x69 = (x68 + (x55 << 0x1));  in fe_mul_121666_impl()
688 	{ u64 x71 = (x44 + (x54 << 0x4));  in fe_mul_121666_impl()
689 	{ u64 x72 = (x71 + (x54 << 0x1));  in fe_mul_121666_impl()
691 	{ u64 x74 = (x43 + (x53 << 0x4));  in fe_mul_121666_impl()
692 	{ u64 x75 = (x74 + (x53 << 0x1));  in fe_mul_121666_impl()
694 	{ u64 x77 = (x42 + (x52 << 0x4));  in fe_mul_121666_impl()
695 	{ u64 x78 = (x77 + (x52 << 0x1));  in fe_mul_121666_impl()
697 	{ u64 x80 = (x41 + (x51 << 0x4));  in fe_mul_121666_impl()
698 	{ u64 x81 = (x80 + (x51 << 0x1));  in fe_mul_121666_impl()
700 	{ u64 x83 = (x40 + (x50 << 0x4));  in fe_mul_121666_impl()
701 	{ u64 x84 = (x83 + (x50 << 0x1));  in fe_mul_121666_impl()
703 	{ u64 x86 = (x85 >> 0x1a);  in fe_mul_121666_impl()
704 	{ u32 x87 = ((u32)x85 & 0x3ffffff);  in fe_mul_121666_impl()
706 	{ u64 x89 = (x88 >> 0x19);  in fe_mul_121666_impl()
707 	{ u32 x90 = ((u32)x88 & 0x1ffffff);  in fe_mul_121666_impl()
709 	{ u64 x92 = (x91 >> 0x1a);  in fe_mul_121666_impl()
710 	{ u32 x93 = ((u32)x91 & 0x3ffffff);  in fe_mul_121666_impl()
712 	{ u64 x95 = (x94 >> 0x19);  in fe_mul_121666_impl()
713 	{ u32 x96 = ((u32)x94 & 0x1ffffff);  in fe_mul_121666_impl()
715 	{ u64 x98 = (x97 >> 0x1a);  in fe_mul_121666_impl()
716 	{ u32 x99 = ((u32)x97 & 0x3ffffff);  in fe_mul_121666_impl()
718 	{ u64 x101 = (x100 >> 0x19);  in fe_mul_121666_impl()
719 	{ u32 x102 = ((u32)x100 & 0x1ffffff);  in fe_mul_121666_impl()
721 	{ u64 x104 = (x103 >> 0x1a);  in fe_mul_121666_impl()
722 	{ u32 x105 = ((u32)x103 & 0x3ffffff);  in fe_mul_121666_impl()
724 	{ u64 x107 = (x106 >> 0x19);  in fe_mul_121666_impl()
725 	{ u32 x108 = ((u32)x106 & 0x1ffffff);  in fe_mul_121666_impl()
727 	{ u64 x110 = (x109 >> 0x1a);  in fe_mul_121666_impl()
728 	{ u32 x111 = ((u32)x109 & 0x3ffffff);  in fe_mul_121666_impl()
730 	{ u64 x113 = (x112 >> 0x19);  in fe_mul_121666_impl()
731 	{ u32 x114 = ((u32)x112 & 0x1ffffff);  in fe_mul_121666_impl()
732 	{ u64 x115 = (x87 + (0x13 * x113));  in fe_mul_121666_impl()
733 	{ u32 x116 = (u32) (x115 >> 0x1a);  in fe_mul_121666_impl()
734 	{ u32 x117 = ((u32)x115 & 0x3ffffff);  in fe_mul_121666_impl()
736 	{ u32 x119 = (x118 >> 0x19);  in fe_mul_121666_impl()
737 	{ u32 x120 = (x118 & 0x1ffffff);  in fe_mul_121666_impl()
738 	out[0] = x117;  in fe_mul_121666_impl()
762 	unsigned swap = 0;  in curve25519_generic()
771 	 * that x1 != 0 is the x coordinate of some point on the curve. It was  in curve25519_generic()
772 	 * also checked in Coq that doing a ladderstep with x1 = x3 = 0 gives  in curve25519_generic()
773 	 * z2' = z3' = 0, and z2 = z3 = 0 gives z2' = z3' = 0. The statement was  in curve25519_generic()
791 	 * preconditions: 0 <= e < 2^255 (not necessarily e < order),  in curve25519_generic()
792 	 * fe_invert(0) = 0  in curve25519_generic()
800 	for (pos = 254; pos >= 0; --pos) {  in curve25519_generic()
804 		 * where x1 != 0:  in curve25519_generic()
805 		 *   pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3  in curve25519_generic()
823 …* x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()
824 …* x1  = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()