14  * entries t[0]...t[9], represents the integer t[0]+2^26 t[1]+2^51 t[2]+2^77
37 	h[0] = a0&((1<<26)-1);                    /* 26 used, 32-26 left.   26 */  in fe_frombytes_impl()
100 	t = -!!t; /* all set if nonzero, 0 if 0 */  in cmovznz32()
115 	{ const u32 x2 = in1[0];  in fe_freeze()
116 	{ u32 x20; u8/*bool*/ x21 = subborrow_u26(0x0, x2, 0x3ffffed, &x20);  in fe_freeze()
117 	{ u32 x23; u8/*bool*/ x24 = subborrow_u25(x21, x4, 0x1ffffff, &x23);  in fe_freeze()
118 	{ u32 x26; u8/*bool*/ x27 = subborrow_u26(x24, x6, 0x3ffffff, &x26);  in fe_freeze()
119 	{ u32 x29; u8/*bool*/ x30 = subborrow_u25(x27, x8, 0x1ffffff, &x29);  in fe_freeze()
120 	{ u32 x32; u8/*bool*/ x33 = subborrow_u26(x30, x10, 0x3ffffff, &x32);  in fe_freeze()
121 	{ u32 x35; u8/*bool*/ x36 = subborrow_u25(x33, x12, 0x1ffffff, &x35);  in fe_freeze()
122 	{ u32 x38; u8/*bool*/ x39 = subborrow_u26(x36, x14, 0x3ffffff, &x38);  in fe_freeze()
123 	{ u32 x41; u8/*bool*/ x42 = subborrow_u25(x39, x16, 0x1ffffff, &x41);  in fe_freeze()
124 	{ u32 x44; u8/*bool*/ x45 = subborrow_u26(x42, x18, 0x3ffffff, &x44);  in fe_freeze()
125 	{ u32 x47; u8/*bool*/ x48 = subborrow_u25(x45, x17, 0x1ffffff, &x47);  in fe_freeze()
126 	{ u32 x49 = cmovznz32(x48, 0x0, 0xffffffff);  in fe_freeze()
127 	{ u32 x50 = (x49 & 0x3ffffed);  in fe_freeze()
128 	{ u32 x52; u8/*bool*/ x53 = addcarryx_u26(0x0, x20, x50, &x52);  in fe_freeze()
129 	{ u32 x54 = (x49 & 0x1ffffff);  in fe_freeze()
131 	{ u32 x58 = (x49 & 0x3ffffff);  in fe_freeze()
133 	{ u32 x62 = (x49 & 0x1ffffff);  in fe_freeze()
135 	{ u32 x66 = (x49 & 0x3ffffff);  in fe_freeze()
137 	{ u32 x70 = (x49 & 0x1ffffff);  in fe_freeze()
139 	{ u32 x74 = (x49 & 0x3ffffff);  in fe_freeze()
141 	{ u32 x78 = (x49 & 0x1ffffff);  in fe_freeze()
143 	{ u32 x82 = (x49 & 0x3ffffff);  in fe_freeze()
145 	{ u32 x86 = (x49 & 0x1ffffff);  in fe_freeze()
147 	out[0] = x52;  in fe_freeze()
164 	s[0] = h[0] >> 0;  in fe_tobytes()
165 	s[1] = h[0] >> 8;  in fe_tobytes()
166 	s[2] = h[0] >> 16;  in fe_tobytes()
167 	s[3] = (h[0] >> 24) | (h[1] << 2);  in fe_tobytes()
180 	s[16] = h[5] >> 0;  in fe_tobytes()
209 /* h = 0 */
212 	memset(h, 0, sizeof(u32) * 10);  in fe_0()
218 	memset(h, 0, sizeof(u32) * 10);  in fe_1()
219 	h->v[0] = 1;  in fe_1()
226 	{ const u32 x19 = in1[7];  in fe_add_impl()  local
233 	{ const u32 x5 = in1[0];  in fe_add_impl()
243 	{ const u32 x23 = in2[0];  in fe_add_impl()
244 	out[0] = (x5 + x23);  in fe_add_impl()
251 	out[7] = (x19 + x37);  in fe_add_impl()
269 	{ const u32 x19 = in1[7];  in fe_sub_impl()  local
276 	{ const u32 x5 = in1[0];  in fe_sub_impl()
286 	{ const u32 x23 = in2[0];  in fe_sub_impl()
287 	out[0] = ((0x7ffffda + x5) - x23);  in fe_sub_impl()
288 	out[1] = ((0x3fffffe + x7) - x25);  in fe_sub_impl()
289 	out[2] = ((0x7fffffe + x9) - x27);  in fe_sub_impl()
290 	out[3] = ((0x3fffffe + x11) - x29);  in fe_sub_impl()
291 	out[4] = ((0x7fffffe + x13) - x31);  in fe_sub_impl()
292 	out[5] = ((0x3fffffe + x15) - x33);  in fe_sub_impl()
293 	out[6] = ((0x7fffffe + x17) - x35);  in fe_sub_impl()
294 	out[7] = ((0x3fffffe + x19) - x37);  in fe_sub_impl()
295 	out[8] = ((0x7fffffe + x21) - x39);  in fe_sub_impl()
296 	out[9] = ((0x3fffffe + x20) - x38);  in fe_sub_impl()
312 	{ const u32 x19 = in1[7];  in fe_mul_impl()  local
319 	{ const u32 x5 = in1[0];  in fe_mul_impl()
329 	{ const u32 x23 = in2[0];  in fe_mul_impl()
332 	{ u64 x42 = ((((u64)(0x2 * x25) * x7) + ((u64)x23 * x9)) + ((u64)x27 * x5));  in fe_mul_impl()
334 …{ u64 x44 = (((((u64)x27 * x9) + (0x2 * (((u64)x25 * x11) + ((u64)x29 * x7)))) + ((u64)x23 * x13))…  in fe_mul_impl()
336 …{ u64 x46 = (((((0x2 * ((((u64)x29 * x11) + ((u64)x25 * x15)) + ((u64)x33 * x7))) + ((u64)x27 * x1…  in fe_mul_impl()
337 …)) + ((u64)x33 * x9)) + ((u64)x25 * x17)) + ((u64)x35 * x7)) + ((u64)x23 * x19)) + ((u64)x37 * x5)…  in fe_mul_impl()
338 …{ u64 x48 = (((((((u64)x31 * x13) + (0x2 * (((((u64)x29 * x15) + ((u64)x33 * x11)) + ((u64)x25 * x…  in fe_mul_impl()
339 … + ((u64)x33 * x13)) + ((u64)x29 * x17)) + ((u64)x35 * x11)) + ((u64)x27 * x19)) + ((u64)x37 * x9)…  in fe_mul_impl()
340 …{ u64 x50 = (((((0x2 * ((((((u64)x33 * x15) + ((u64)x29 * x19)) + ((u64)x37 * x11)) + ((u64)x25 * …  in fe_mul_impl()
341 …{ u64 x51 = (((((((((u64)x33 * x17) + ((u64)x35 * x15)) + ((u64)x31 * x19)) + ((u64)x37 * x13)) + …  in fe_mul_impl()
342 …{ u64 x52 = (((((u64)x35 * x17) + (0x2 * (((((u64)x33 * x19) + ((u64)x37 * x15)) + ((u64)x29 * x20…  in fe_mul_impl()
343 …{ u64 x53 = (((((((u64)x35 * x19) + ((u64)x37 * x17)) + ((u64)x33 * x21)) + ((u64)x39 * x15)) + ((…  in fe_mul_impl()
344 …{ u64 x54 = (((0x2 * ((((u64)x37 * x19) + ((u64)x33 * x20)) + ((u64)x38 * x15))) + ((u64)x35 * x21…  in fe_mul_impl()
345 	{ u64 x55 = (((((u64)x37 * x21) + ((u64)x39 * x19)) + ((u64)x35 * x20)) + ((u64)x38 * x17));  in fe_mul_impl()
346 	{ u64 x56 = (((u64)x39 * x21) + (0x2 * (((u64)x37 * x20) + ((u64)x38 * x19))));  in fe_mul_impl()
348 	{ u64 x58 = ((u64)(0x2 * x38) * x20);  in fe_mul_impl()
349 	{ u64 x59 = (x48 + (x58 << 0x4));  in fe_mul_impl()
350 	{ u64 x60 = (x59 + (x58 << 0x1));  in fe_mul_impl()
352 	{ u64 x62 = (x47 + (x57 << 0x4));  in fe_mul_impl()
353 	{ u64 x63 = (x62 + (x57 << 0x1));  in fe_mul_impl()
355 	{ u64 x65 = (x46 + (x56 << 0x4));  in fe_mul_impl()
356 	{ u64 x66 = (x65 + (x56 << 0x1));  in fe_mul_impl()
358 	{ u64 x68 = (x45 + (x55 << 0x4));  in fe_mul_impl()
359 	{ u64 x69 = (x68 + (x55 << 0x1));  in fe_mul_impl()
361 	{ u64 x71 = (x44 + (x54 << 0x4));  in fe_mul_impl()
362 	{ u64 x72 = (x71 + (x54 << 0x1));  in fe_mul_impl()
364 	{ u64 x74 = (x43 + (x53 << 0x4));  in fe_mul_impl()
365 	{ u64 x75 = (x74 + (x53 << 0x1));  in fe_mul_impl()
367 	{ u64 x77 = (x42 + (x52 << 0x4));  in fe_mul_impl()
368 	{ u64 x78 = (x77 + (x52 << 0x1));  in fe_mul_impl()
370 	{ u64 x80 = (x41 + (x51 << 0x4));  in fe_mul_impl()
371 	{ u64 x81 = (x80 + (x51 << 0x1));  in fe_mul_impl()
373 	{ u64 x83 = (x40 + (x50 << 0x4));  in fe_mul_impl()
374 	{ u64 x84 = (x83 + (x50 << 0x1));  in fe_mul_impl()
376 	{ u64 x86 = (x85 >> 0x1a);  in fe_mul_impl()
377 	{ u32 x87 = ((u32)x85 & 0x3ffffff);  in fe_mul_impl()
379 	{ u64 x89 = (x88 >> 0x19);  in fe_mul_impl()
380 	{ u32 x90 = ((u32)x88 & 0x1ffffff);  in fe_mul_impl()
382 	{ u64 x92 = (x91 >> 0x1a);  in fe_mul_impl()
383 	{ u32 x93 = ((u32)x91 & 0x3ffffff);  in fe_mul_impl()
385 	{ u64 x95 = (x94 >> 0x19);  in fe_mul_impl()
386 	{ u32 x96 = ((u32)x94 & 0x1ffffff);  in fe_mul_impl()
388 	{ u64 x98 = (x97 >> 0x1a);  in fe_mul_impl()
389 	{ u32 x99 = ((u32)x97 & 0x3ffffff);  in fe_mul_impl()
391 	{ u64 x101 = (x100 >> 0x19);  in fe_mul_impl()
392 	{ u32 x102 = ((u32)x100 & 0x1ffffff);  in fe_mul_impl()
394 	{ u64 x104 = (x103 >> 0x1a);  in fe_mul_impl()
395 	{ u32 x105 = ((u32)x103 & 0x3ffffff);  in fe_mul_impl()
397 	{ u64 x107 = (x106 >> 0x19);  in fe_mul_impl()
398 	{ u32 x108 = ((u32)x106 & 0x1ffffff);  in fe_mul_impl()
400 	{ u64 x110 = (x109 >> 0x1a);  in fe_mul_impl()
401 	{ u32 x111 = ((u32)x109 & 0x3ffffff);  in fe_mul_impl()
403 	{ u64 x113 = (x112 >> 0x19);  in fe_mul_impl()
404 	{ u32 x114 = ((u32)x112 & 0x1ffffff);  in fe_mul_impl()
405 	{ u64 x115 = (x87 + (0x13 * x113));  in fe_mul_impl()
406 	{ u32 x116 = (u32) (x115 >> 0x1a);  in fe_mul_impl()
407 	{ u32 x117 = ((u32)x115 & 0x3ffffff);  in fe_mul_impl()
409 	{ u32 x119 = (x118 >> 0x19);  in fe_mul_impl()
410 	{ u32 x120 = (x118 & 0x1ffffff);  in fe_mul_impl()
411 	out[0] = x117;  in fe_mul_impl()
451 	{ const u32 x2 = in1[0];  in fe_sqr_impl()
452 	{ u64 x19 = ((u64)x2 * x2);  in fe_sqr_impl()  local
453 	{ u64 x20 = ((u64)(0x2 * x2) * x4);  in fe_sqr_impl()
454 	{ u64 x21 = (0x2 * (((u64)x4 * x4) + ((u64)x2 * x6)));  in fe_sqr_impl()
455 	{ u64 x22 = (0x2 * (((u64)x4 * x6) + ((u64)x2 * x8)));  in fe_sqr_impl()
456 	{ u64 x23 = ((((u64)x6 * x6) + ((u64)(0x4 * x4) * x8)) + ((u64)(0x2 * x2) * x10));  in fe_sqr_impl()
457 	{ u64 x24 = (0x2 * ((((u64)x6 * x8) + ((u64)x4 * x10)) + ((u64)x2 * x12)));  in fe_sqr_impl()
458 …{ u64 x25 = (0x2 * (((((u64)x8 * x8) + ((u64)x6 * x10)) + ((u64)x2 * x14)) + ((u64)(0x2 * x4) * x1…  in fe_sqr_impl()
459 	{ u64 x26 = (0x2 * (((((u64)x8 * x10) + ((u64)x6 * x12)) + ((u64)x4 * x14)) + ((u64)x2 * x16)));  in fe_sqr_impl()
460 …{ u64 x27 = (((u64)x10 * x10) + (0x2 * ((((u64)x6 * x14) + ((u64)x2 * x18)) + (0x2 * (((u64)x4 * x…  in fe_sqr_impl()
461 …{ u64 x28 = (0x2 * ((((((u64)x10 * x12) + ((u64)x8 * x14)) + ((u64)x6 * x16)) + ((u64)x4 * x18)) +…  in fe_sqr_impl()
462 …{ u64 x29 = (0x2 * (((((u64)x12 * x12) + ((u64)x10 * x14)) + ((u64)x6 * x18)) + (0x2 * (((u64)x8 *…  in fe_sqr_impl()
463 	{ u64 x30 = (0x2 * (((((u64)x12 * x14) + ((u64)x10 * x16)) + ((u64)x8 * x18)) + ((u64)x6 * x17)));  in fe_sqr_impl()
464 …{ u64 x31 = (((u64)x14 * x14) + (0x2 * (((u64)x10 * x18) + (0x2 * (((u64)x12 * x16) + ((u64)x8 * x…  in fe_sqr_impl()
465 	{ u64 x32 = (0x2 * ((((u64)x14 * x16) + ((u64)x12 * x18)) + ((u64)x10 * x17)));  in fe_sqr_impl()
466 	{ u64 x33 = (0x2 * ((((u64)x16 * x16) + ((u64)x14 * x18)) + ((u64)(0x2 * x12) * x17)));  in fe_sqr_impl()
467 	{ u64 x34 = (0x2 * (((u64)x16 * x18) + ((u64)x14 * x17)));  in fe_sqr_impl()
468 	{ u64 x35 = (((u64)x18 * x18) + ((u64)(0x4 * x16) * x17));  in fe_sqr_impl()
469 	{ u64 x36 = ((u64)(0x2 * x18) * x17);  in fe_sqr_impl()
470 	{ u64 x37 = ((u64)(0x2 * x17) * x17);  in fe_sqr_impl()
471 	{ u64 x38 = (x27 + (x37 << 0x4));  in fe_sqr_impl()
472 	{ u64 x39 = (x38 + (x37 << 0x1));  in fe_sqr_impl()
474 	{ u64 x41 = (x26 + (x36 << 0x4));  in fe_sqr_impl()
475 	{ u64 x42 = (x41 + (x36 << 0x1));  in fe_sqr_impl()
477 	{ u64 x44 = (x25 + (x35 << 0x4));  in fe_sqr_impl()
478 	{ u64 x45 = (x44 + (x35 << 0x1));  in fe_sqr_impl()
480 	{ u64 x47 = (x24 + (x34 << 0x4));  in fe_sqr_impl()
481 	{ u64 x48 = (x47 + (x34 << 0x1));  in fe_sqr_impl()
483 	{ u64 x50 = (x23 + (x33 << 0x4));  in fe_sqr_impl()
484 	{ u64 x51 = (x50 + (x33 << 0x1));  in fe_sqr_impl()
486 	{ u64 x53 = (x22 + (x32 << 0x4));  in fe_sqr_impl()
487 	{ u64 x54 = (x53 + (x32 << 0x1));  in fe_sqr_impl()
489 	{ u64 x56 = (x21 + (x31 << 0x4));  in fe_sqr_impl()
490 	{ u64 x57 = (x56 + (x31 << 0x1));  in fe_sqr_impl()
492 	{ u64 x59 = (x20 + (x30 << 0x4));  in fe_sqr_impl()
493 	{ u64 x60 = (x59 + (x30 << 0x1));  in fe_sqr_impl()
495 	{ u64 x62 = (x19 + (x29 << 0x4));  in fe_sqr_impl()
496 	{ u64 x63 = (x62 + (x29 << 0x1));  in fe_sqr_impl()
498 	{ u64 x65 = (x64 >> 0x1a);  in fe_sqr_impl()
499 	{ u32 x66 = ((u32)x64 & 0x3ffffff);  in fe_sqr_impl()
501 	{ u64 x68 = (x67 >> 0x19);  in fe_sqr_impl()
502 	{ u32 x69 = ((u32)x67 & 0x1ffffff);  in fe_sqr_impl()
504 	{ u64 x71 = (x70 >> 0x1a);  in fe_sqr_impl()
505 	{ u32 x72 = ((u32)x70 & 0x3ffffff);  in fe_sqr_impl()
507 	{ u64 x74 = (x73 >> 0x19);  in fe_sqr_impl()
508 	{ u32 x75 = ((u32)x73 & 0x1ffffff);  in fe_sqr_impl()
510 	{ u64 x77 = (x76 >> 0x1a);  in fe_sqr_impl()
511 	{ u32 x78 = ((u32)x76 & 0x3ffffff);  in fe_sqr_impl()
513 	{ u64 x80 = (x79 >> 0x19);  in fe_sqr_impl()
514 	{ u32 x81 = ((u32)x79 & 0x1ffffff);  in fe_sqr_impl()
516 	{ u64 x83 = (x82 >> 0x1a);  in fe_sqr_impl()
517 	{ u32 x84 = ((u32)x82 & 0x3ffffff);  in fe_sqr_impl()
519 	{ u64 x86 = (x85 >> 0x19);  in fe_sqr_impl()
520 	{ u32 x87 = ((u32)x85 & 0x1ffffff);  in fe_sqr_impl()
522 	{ u64 x89 = (x88 >> 0x1a);  in fe_sqr_impl()
523 	{ u32 x90 = ((u32)x88 & 0x3ffffff);  in fe_sqr_impl()
525 	{ u64 x92 = (x91 >> 0x19);  in fe_sqr_impl()
526 	{ u32 x93 = ((u32)x91 & 0x1ffffff);  in fe_sqr_impl()
527 	{ u64 x94 = (x66 + (0x13 * x92));  in fe_sqr_impl()
528 	{ u32 x95 = (u32) (x94 >> 0x1a);  in fe_sqr_impl()
529 	{ u32 x96 = ((u32)x94 & 0x3ffffff);  in fe_sqr_impl()
531 	{ u32 x98 = (x97 >> 0x19);  in fe_sqr_impl()
532 	{ u32 x99 = (x97 & 0x1ffffff);  in fe_sqr_impl()
533 	out[0] = x96;  in fe_sqr_impl()
614  * replace (f,g) with (f,g) if b == 0.
616  * Preconditions: b in {0,1}
621 	b = 0 - b;  in fe_cswap()
622 	for (i = 0; i < 10; i++) {  in fe_cswap()
630 /* NOTE: based on fiat-crypto fe_mul, edited for in2=121666, 0, 0.*/
635 	{ const u32 x19 = in1[7];  in fe_mul_121666_impl()  local
642 	{ const u32 x5 = in1[0];  in fe_mul_121666_impl()
643 	{ const u32 x38 = 0;  in fe_mul_121666_impl()
644 	{ const u32 x39 = 0;  in fe_mul_121666_impl()
645 	{ const u32 x37 = 0;  in fe_mul_121666_impl()
646 	{ const u32 x35 = 0;  in fe_mul_121666_impl()
647 	{ const u32 x33 = 0;  in fe_mul_121666_impl()
648 	{ const u32 x31 = 0;  in fe_mul_121666_impl()
649 	{ const u32 x29 = 0;  in fe_mul_121666_impl()
650 	{ const u32 x27 = 0;  in fe_mul_121666_impl()
651 	{ const u32 x25 = 0;  in fe_mul_121666_impl()
655 	{ u64 x42 = ((((u64)(0x2 * x25) * x7) + ((u64)x23 * x9)) + ((u64)x27 * x5));  in fe_mul_121666_impl()
657 …{ u64 x44 = (((((u64)x27 * x9) + (0x2 * (((u64)x25 * x11) + ((u64)x29 * x7)))) + ((u64)x23 * x13))…  in fe_mul_121666_impl()
659 …{ u64 x46 = (((((0x2 * ((((u64)x29 * x11) + ((u64)x25 * x15)) + ((u64)x33 * x7))) + ((u64)x27 * x1…  in fe_mul_121666_impl()
660 …)) + ((u64)x33 * x9)) + ((u64)x25 * x17)) + ((u64)x35 * x7)) + ((u64)x23 * x19)) + ((u64)x37 * x5)…  in fe_mul_121666_impl()
661 …{ u64 x48 = (((((((u64)x31 * x13) + (0x2 * (((((u64)x29 * x15) + ((u64)x33 * x11)) + ((u64)x25 * x…  in fe_mul_121666_impl()
662 … + ((u64)x33 * x13)) + ((u64)x29 * x17)) + ((u64)x35 * x11)) + ((u64)x27 * x19)) + ((u64)x37 * x9)…  in fe_mul_121666_impl()
663 …{ u64 x50 = (((((0x2 * ((((((u64)x33 * x15) + ((u64)x29 * x19)) + ((u64)x37 * x11)) + ((u64)x25 * …  in fe_mul_121666_impl()
664 …{ u64 x51 = (((((((((u64)x33 * x17) + ((u64)x35 * x15)) + ((u64)x31 * x19)) + ((u64)x37 * x13)) + …  in fe_mul_121666_impl()
665 …{ u64 x52 = (((((u64)x35 * x17) + (0x2 * (((((u64)x33 * x19) + ((u64)x37 * x15)) + ((u64)x29 * x20…  in fe_mul_121666_impl()
666 …{ u64 x53 = (((((((u64)x35 * x19) + ((u64)x37 * x17)) + ((u64)x33 * x21)) + ((u64)x39 * x15)) + ((…  in fe_mul_121666_impl()
667 …{ u64 x54 = (((0x2 * ((((u64)x37 * x19) + ((u64)x33 * x20)) + ((u64)x38 * x15))) + ((u64)x35 * x21…  in fe_mul_121666_impl()
668 	{ u64 x55 = (((((u64)x37 * x21) + ((u64)x39 * x19)) + ((u64)x35 * x20)) + ((u64)x38 * x17));  in fe_mul_121666_impl()
669 	{ u64 x56 = (((u64)x39 * x21) + (0x2 * (((u64)x37 * x20) + ((u64)x38 * x19))));  in fe_mul_121666_impl()
671 	{ u64 x58 = ((u64)(0x2 * x38) * x20);  in fe_mul_121666_impl()
672 	{ u64 x59 = (x48 + (x58 << 0x4));  in fe_mul_121666_impl()
673 	{ u64 x60 = (x59 + (x58 << 0x1));  in fe_mul_121666_impl()
675 	{ u64 x62 = (x47 + (x57 << 0x4));  in fe_mul_121666_impl()
676 	{ u64 x63 = (x62 + (x57 << 0x1));  in fe_mul_121666_impl()
678 	{ u64 x65 = (x46 + (x56 << 0x4));  in fe_mul_121666_impl()
679 	{ u64 x66 = (x65 + (x56 << 0x1));  in fe_mul_121666_impl()
681 	{ u64 x68 = (x45 + (x55 << 0x4));  in fe_mul_121666_impl()
682 	{ u64 x69 = (x68 + (x55 << 0x1));  in fe_mul_121666_impl()
684 	{ u64 x71 = (x44 + (x54 << 0x4));  in fe_mul_121666_impl()
685 	{ u64 x72 = (x71 + (x54 << 0x1));  in fe_mul_121666_impl()
687 	{ u64 x74 = (x43 + (x53 << 0x4));  in fe_mul_121666_impl()
688 	{ u64 x75 = (x74 + (x53 << 0x1));  in fe_mul_121666_impl()
690 	{ u64 x77 = (x42 + (x52 << 0x4));  in fe_mul_121666_impl()
691 	{ u64 x78 = (x77 + (x52 << 0x1));  in fe_mul_121666_impl()
693 	{ u64 x80 = (x41 + (x51 << 0x4));  in fe_mul_121666_impl()
694 	{ u64 x81 = (x80 + (x51 << 0x1));  in fe_mul_121666_impl()
696 	{ u64 x83 = (x40 + (x50 << 0x4));  in fe_mul_121666_impl()
697 	{ u64 x84 = (x83 + (x50 << 0x1));  in fe_mul_121666_impl()
699 	{ u64 x86 = (x85 >> 0x1a);  in fe_mul_121666_impl()
700 	{ u32 x87 = ((u32)x85 & 0x3ffffff);  in fe_mul_121666_impl()
702 	{ u64 x89 = (x88 >> 0x19);  in fe_mul_121666_impl()
703 	{ u32 x90 = ((u32)x88 & 0x1ffffff);  in fe_mul_121666_impl()
705 	{ u64 x92 = (x91 >> 0x1a);  in fe_mul_121666_impl()
706 	{ u32 x93 = ((u32)x91 & 0x3ffffff);  in fe_mul_121666_impl()
708 	{ u64 x95 = (x94 >> 0x19);  in fe_mul_121666_impl()
709 	{ u32 x96 = ((u32)x94 & 0x1ffffff);  in fe_mul_121666_impl()
711 	{ u64 x98 = (x97 >> 0x1a);  in fe_mul_121666_impl()
712 	{ u32 x99 = ((u32)x97 & 0x3ffffff);  in fe_mul_121666_impl()
714 	{ u64 x101 = (x100 >> 0x19);  in fe_mul_121666_impl()
715 	{ u32 x102 = ((u32)x100 & 0x1ffffff);  in fe_mul_121666_impl()
717 	{ u64 x104 = (x103 >> 0x1a);  in fe_mul_121666_impl()
718 	{ u32 x105 = ((u32)x103 & 0x3ffffff);  in fe_mul_121666_impl()
720 	{ u64 x107 = (x106 >> 0x19);  in fe_mul_121666_impl()
721 	{ u32 x108 = ((u32)x106 & 0x1ffffff);  in fe_mul_121666_impl()
723 	{ u64 x110 = (x109 >> 0x1a);  in fe_mul_121666_impl()
724 	{ u32 x111 = ((u32)x109 & 0x3ffffff);  in fe_mul_121666_impl()
726 	{ u64 x113 = (x112 >> 0x19);  in fe_mul_121666_impl()
727 	{ u32 x114 = ((u32)x112 & 0x1ffffff);  in fe_mul_121666_impl()
728 	{ u64 x115 = (x87 + (0x13 * x113));  in fe_mul_121666_impl()
729 	{ u32 x116 = (u32) (x115 >> 0x1a);  in fe_mul_121666_impl()
730 	{ u32 x117 = ((u32)x115 & 0x3ffffff);  in fe_mul_121666_impl()
732 	{ u32 x119 = (x118 >> 0x19);  in fe_mul_121666_impl()
733 	{ u32 x120 = (x118 & 0x1ffffff);  in fe_mul_121666_impl()
734 	out[0] = x117;  in fe_mul_121666_impl()
758 	unsigned swap = 0;  in curve25519_generic()
767 	 * that x1 != 0 is the x coordinate of some point on the curve. It was  in curve25519_generic()
768 	 * also checked in Coq that doing a ladderstep with x1 = x3 = 0 gives  in curve25519_generic()
769 	 * z2' = z3' = 0, and z2 = z3 = 0 gives z2' = z3' = 0. The statement was  in curve25519_generic()
787 	 * preconditions: 0 <= e < 2^255 (not necessarily e < order),  in curve25519_generic()
788 	 * fe_invert(0) = 0  in curve25519_generic()
796 	for (pos = 254; pos >= 0; --pos) {  in curve25519_generic()
800 		 * where x1 != 0:  in curve25519_generic()
801 		 *   pos >= -1; if z2 = 0 then x2 is nonzero; if z3 = 0 then x3  in curve25519_generic()
819 …* x1 != 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()
820 …* x1  = 0 <https://github.com/mit-plv/fiat-crypto/blob/2456d821825521f7e03e65882cc3521795b0320f/sr…  in curve25519_generic()