22 // entries t[0]...t[9], represents the integer t[0]+2^26 t[1]+2^51 t[2]+2^77
23 // t[3]+2^102 t[4]+...+2^230 t[9].
191   uint64_t x1 = ((uint64_t)(arg1[9]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
192   uint64_t x2 = ((uint64_t)(arg1[9]) * ((arg2[8]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
193   uint64_t x3 = ((uint64_t)(arg1[9]) * ((arg2[7]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
194   uint64_t x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
195   uint64_t x5 = ((uint64_t)(arg1[9]) * ((arg2[5]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
196   uint64_t x6 = ((uint64_t)(arg1[9]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
197   uint64_t x7 = ((uint64_t)(arg1[9]) * ((arg2[3]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
198   uint64_t x8 = ((uint64_t)(arg1[9]) * ((arg2[2]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
199   uint64_t x9 = ((uint64_t)(arg1[9]) * ((arg2[1]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
200   uint64_t x10 = ((uint64_t)(arg1[8]) * ((arg2[9]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
208   uint64_t x18 = ((uint64_t)(arg1[7]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
215   uint64_t x25 = ((uint64_t)(arg1[6]) * ((arg2[9]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
221   uint64_t x31 = ((uint64_t)(arg1[5]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
226   uint64_t x36 = ((uint64_t)(arg1[4]) * ((arg2[9]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
230   uint64_t x40 = ((uint64_t)(arg1[3]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
233   uint64_t x43 = ((uint64_t)(arg1[2]) * ((arg2[9]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
235   uint64_t x45 = ((uint64_t)(arg1[1]) * ((arg2[9]) * ((uint32_t)0x2 * UINT8_C(0x13))));  in fiat_25519_carry_mul()
236   uint64_t x46 = ((uint64_t)(arg1[9]) * (arg2[0]));  in fiat_25519_carry_mul()
281   uint64_t x91 = ((uint64_t)(arg1[0]) * (arg2[9]));  in fiat_25519_carry_mul()
347   out1[9] = x139;  in fiat_25519_carry_mul()
357   uint32_t x1 = ((arg1[9]) * (uint32_t)UINT8_C(0x13));  in fiat_25519_carry_square()
359   uint32_t x3 = ((arg1[9]) * (uint32_t)0x2);  in fiat_25519_carry_square()
375   uint64_t x19 = ((uint64_t)(arg1[9]) * (x1 * (uint32_t)0x2));  in fiat_25519_carry_square()
486   out1[9] = x112;  in fiat_25519_carry_square()
505   uint32_t x10 = ((x9 >> 26) + (arg1[9]));  in fiat_25519_carry()
527   out1[9] = x22;  in fiat_25519_carry()
547   uint32_t x10 = ((arg1[9]) + (arg2[9]));  in fiat_25519_add()
557   out1[9] = x10;  in fiat_25519_add()
577   uint32_t x10 = ((UINT32_C(0x3fffffe) + (arg1[9])) - (arg2[9]));  in fiat_25519_sub()
587   out1[9] = x10;  in fiat_25519_sub()
606   uint32_t x10 = (UINT32_C(0x3fffffe) - (arg1[9]));  in fiat_25519_opp()
616   out1[9] = x10;  in fiat_25519_opp()
655   fiat_25519_subborrowx_u25(&x19, &x20, x18, (arg1[9]), UINT32_C(0x1ffffff));  in fiat_25519_to_bytes()
774   out1[9] = x72;  in fiat_25519_to_bytes()
828   uint32_t x23 = ((uint32_t)(arg1[9]) << 21);  in fiat_25519_from_bytes()
882   out1[9] = x67;  in fiat_25519_from_bytes()