194   uint64_t x4 = ((uint64_t)(arg1[9]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
203   uint64_t x13 = ((uint64_t)(arg1[8]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
211   uint64_t x21 = ((uint64_t)(arg1[7]) * ((arg2[6]) * (uint32_t)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()
216   uint64_t x26 = ((uint64_t)(arg1[6]) * ((arg2[8]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
217   uint64_t x27 = ((uint64_t)(arg1[6]) * ((arg2[7]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
218   uint64_t x28 = ((uint64_t)(arg1[6]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
219   uint64_t x29 = ((uint64_t)(arg1[6]) * ((arg2[5]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
220   uint64_t x30 = ((uint64_t)(arg1[6]) * ((arg2[4]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
224   uint64_t x34 = ((uint64_t)(arg1[5]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
229   uint64_t x39 = ((uint64_t)(arg1[4]) * ((arg2[6]) * (uint32_t)UINT8_C(0x13)));  in fiat_25519_carry_mul()
242   uint64_t x52 = ((uint64_t)(arg1[6]) * (arg2[3]));  in fiat_25519_carry_mul()
243   uint64_t x53 = ((uint64_t)(arg1[6]) * (arg2[2]));  in fiat_25519_carry_mul()
244   uint64_t x54 = ((uint64_t)(arg1[6]) * (arg2[1]));  in fiat_25519_carry_mul()
245   uint64_t x55 = ((uint64_t)(arg1[6]) * (arg2[0]));  in fiat_25519_carry_mul()
257   uint64_t x67 = ((uint64_t)(arg1[3]) * (arg2[6]));  in fiat_25519_carry_mul()
265   uint64_t x75 = ((uint64_t)(arg1[2]) * (arg2[6]));  in fiat_25519_carry_mul()
274   uint64_t x84 = ((uint64_t)(arg1[1]) * (arg2[6]));  in fiat_25519_carry_mul()
284   uint64_t x94 = ((uint64_t)(arg1[0]) * (arg2[6]));  in fiat_25519_carry_mul()
344   out1[6] = x130;  in fiat_25519_carry_mul()
366   uint32_t x10 = ((arg1[6]) * (uint32_t)UINT8_C(0x13));  in fiat_25519_carry_square()
368   uint32_t x12 = ((arg1[6]) * (uint32_t)0x2);  in fiat_25519_carry_square()
381   uint64_t x25 = ((uint64_t)(arg1[6]) * x2);  in fiat_25519_carry_square()
382   uint64_t x26 = ((arg1[6]) * x5);  in fiat_25519_carry_square()
383   uint64_t x27 = ((uint64_t)(arg1[6]) * x8);  in fiat_25519_carry_square()
384   uint64_t x28 = ((uint64_t)(arg1[6]) * x10);  in fiat_25519_carry_square()
483   out1[6] = x103;  in fiat_25519_carry_square()
502   uint32_t x7 = ((x6 >> 25) + (arg1[6]));  in fiat_25519_carry()
524   out1[6] = x19;  in fiat_25519_carry()
544   uint32_t x7 = ((arg1[6]) + (arg2[6]));  in fiat_25519_add()
554   out1[6] = x7;  in fiat_25519_add()
574   uint32_t x7 = ((UINT32_C(0x7fffffe) + (arg1[6])) - (arg2[6]));  in fiat_25519_sub()
584   out1[6] = x7;  in fiat_25519_sub()
603   uint32_t x7 = (UINT32_C(0x7fffffe) - (arg1[6]));  in fiat_25519_opp()
613   out1[6] = x7;  in fiat_25519_opp()
646   fiat_25519_subborrowx_u26(&x13, &x14, x12, (arg1[6]), UINT32_C(0x3ffffff));  in fiat_25519_to_bytes()
688   uint32_t x42 = (x40 << 6);  in fiat_25519_to_bytes()
692   uint32_t x46 = (x30 << 6);  in fiat_25519_to_bytes()
771   out1[6] = x65;  in fiat_25519_to_bytes()
831   uint32_t x26 = ((uint32_t)(arg1[6]) << 22);  in fiat_25519_from_bytes()
833   uint32_t x28 = ((uint32_t)(arg1[4]) << 6);  in fiat_25519_from_bytes()
879   out1[6] = x60;  in fiat_25519_from_bytes()