path: root/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femulDisplay.log

λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
 λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
 uint64_t x33, uint64_t x34 = mulx_u64(x5, x19);
 uint64_t x36, uint64_t x37 = mulx_u64(x5, x21);
 uint64_t x39, uint64_t x40 = mulx_u64(x5, x23);
 uint64_t x42, uint64_t x43 = mulx_u64(x5, x25);
 uint64_t x45, uint64_t x46 = mulx_u64(x5, x27);
 uint64_t x48, uint64_t x49 = mulx_u64(x5, x29);
 uint64_t x51, uint64_t x52 = mulx_u64(x5, x31);
 uint64_t x54, uint64_t x55 = mulx_u64(x5, x30);
 uint64_t x57, uint8_t x58 = addcarryx_u64(0x0, x34, x36);
 uint64_t x60, uint8_t x61 = addcarryx_u64(x58, x37, x39);
 uint64_t x63, uint8_t x64 = addcarryx_u64(x61, x40, x42);
 uint64_t x66, uint8_t x67 = addcarryx_u64(x64, x43, x45);
 uint64_t x69, uint8_t x70 = addcarryx_u64(x67, x46, x48);
 uint64_t x72, uint8_t x73 = addcarryx_u64(x70, x49, x51);
 uint64_t x75, uint8_t x76 = addcarryx_u64(x73, x52, x54);
 uint64_t x78, uint8_t _ = addcarryx_u64(0x0, x76, x55);
 uint64_t x81, uint64_t x82 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x84, uint64_t x85 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x87, uint64_t x88 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x90, uint64_t x91 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x93, uint64_t x94 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x96, uint64_t x97 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x99, uint64_t x100 = mulx_u64(x33, 0xffffffffffffffffL);
 uint64_t x102, uint64_t x103 = mulx_u64(x33, 0xfe14ffffffffffffL);
 uint64_t x105, uint8_t x106 = addcarryx_u64(0x0, x82, x84);
 uint64_t x108, uint8_t x109 = addcarryx_u64(x106, x85, x87);
 uint64_t x111, uint8_t x112 = addcarryx_u64(x109, x88, x90);
 uint64_t x114, uint8_t x115 = addcarryx_u64(x112, x91, x93);
 uint64_t x117, uint8_t x118 = addcarryx_u64(x115, x94, x96);
 uint64_t x120, uint8_t x121 = addcarryx_u64(x118, x97, x99);
 uint64_t x123, uint8_t x124 = addcarryx_u64(x121, x100, x102);
 uint64_t x126, uint8_t _ = addcarryx_u64(0x0, x124, x103);
 uint64_t _, uint8_t x130 = addcarryx_u64(0x0, x33, x81);
 uint64_t x132, uint8_t x133 = addcarryx_u64(x130, x57, x105);
 uint64_t x135, uint8_t x136 = addcarryx_u64(x133, x60, x108);
 uint64_t x138, uint8_t x139 = addcarryx_u64(x136, x63, x111);
 uint64_t x141, uint8_t x142 = addcarryx_u64(x139, x66, x114);
 uint64_t x144, uint8_t x145 = addcarryx_u64(x142, x69, x117);
 uint64_t x147, uint8_t x148 = addcarryx_u64(x145, x72, x120);
 uint64_t x150, uint8_t x151 = addcarryx_u64(x148, x75, x123);
 uint64_t x153, uint8_t x154 = addcarryx_u64(x151, x78, x126);
 uint8_t x155 = (x154 + 0x0);
 uint64_t x157, uint64_t x158 = mulx_u64(x7, x19);
 uint64_t x160, uint64_t x161 = mulx_u64(x7, x21);
 uint64_t x163, uint64_t x164 = mulx_u64(x7, x23);
 uint64_t x166, uint64_t x167 = mulx_u64(x7, x25);
 uint64_t x169, uint64_t x170 = mulx_u64(x7, x27);
 uint64_t x172, uint64_t x173 = mulx_u64(x7, x29);
 uint64_t x175, uint64_t x176 = mulx_u64(x7, x31);
 uint64_t x178, uint64_t x179 = mulx_u64(x7, x30);
 uint64_t x181, uint8_t x182 = addcarryx_u64(0x0, x158, x160);
 uint64_t x184, uint8_t x185 = addcarryx_u64(x182, x161, x163);
 uint64_t x187, uint8_t x188 = addcarryx_u64(x185, x164, x166);
 uint64_t x190, uint8_t x191 = addcarryx_u64(x188, x167, x169);
 uint64_t x193, uint8_t x194 = addcarryx_u64(x191, x170, x172);
 uint64_t x196, uint8_t x197 = addcarryx_u64(x194, x173, x175);
 uint64_t x199, uint8_t x200 = addcarryx_u64(x197, x176, x178);
 uint64_t x202, uint8_t _ = addcarryx_u64(0x0, x200, x179);
 uint64_t x205, uint8_t x206 = addcarryx_u64(0x0, x132, x157);
 uint64_t x208, uint8_t x209 = addcarryx_u64(x206, x135, x181);
 uint64_t x211, uint8_t x212 = addcarryx_u64(x209, x138, x184);
 uint64_t x214, uint8_t x215 = addcarryx_u64(x212, x141, x187);
 uint64_t x217, uint8_t x218 = addcarryx_u64(x215, x144, x190);
 uint64_t x220, uint8_t x221 = addcarryx_u64(x218, x147, x193);
 uint64_t x223, uint8_t x224 = addcarryx_u64(x221, x150, x196);
 uint64_t x226, uint8_t x227 = addcarryx_u64(x224, x153, x199);
 uint64_t x229, uint8_t x230 = addcarryx_u64(x227, x155, x202);
 uint64_t x232, uint64_t x233 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x235, uint64_t x236 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x238, uint64_t x239 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x241, uint64_t x242 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x244, uint64_t x245 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x247, uint64_t x248 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x250, uint64_t x251 = mulx_u64(x205, 0xffffffffffffffffL);
 uint64_t x253, uint64_t x254 = mulx_u64(x205, 0xfe14ffffffffffffL);
 uint64_t x256, uint8_t x257 = addcarryx_u64(0x0, x233, x235);
 uint64_t x259, uint8_t x260 = addcarryx_u64(x257, x236, x238);
 uint64_t x262, uint8_t x263 = addcarryx_u64(x260, x239, x241);
 uint64_t x265, uint8_t x266 = addcarryx_u64(x263, x242, x244);
 uint64_t x268, uint8_t x269 = addcarryx_u64(x266, x245, x247);
 uint64_t x271, uint8_t x272 = addcarryx_u64(x269, x248, x250);
 uint64_t x274, uint8_t x275 = addcarryx_u64(x272, x251, x253);
 uint64_t x277, uint8_t _ = addcarryx_u64(0x0, x275, x254);
 uint64_t _, uint8_t x281 = addcarryx_u64(0x0, x205, x232);
 uint64_t x283, uint8_t x284 = addcarryx_u64(x281, x208, x256);
 uint64_t x286, uint8_t x287 = addcarryx_u64(x284, x211, x259);
 uint64_t x289, uint8_t x290 = addcarryx_u64(x287, x214, x262);
 uint64_t x292, uint8_t x293 = addcarryx_u64(x290, x217, x265);
 uint64_t x295, uint8_t x296 = addcarryx_u64(x293, x220, x268);
 uint64_t x298, uint8_t x299 = addcarryx_u64(x296, x223, x271);
 uint64_t x301, uint8_t x302 = addcarryx_u64(x299, x226, x274);
 uint64_t x304, uint8_t x305 = addcarryx_u64(x302, x229, x277);
 uint8_t x306 = (x305 + x230);
 uint64_t x308, uint64_t x309 = mulx_u64(x9, x19);
 uint64_t x311, uint64_t x312 = mulx_u64(x9, x21);
 uint64_t x314, uint64_t x315 = mulx_u64(x9, x23);
 uint64_t x317, uint64_t x318 = mulx_u64(x9, x25);
 uint64_t x320, uint64_t x321 = mulx_u64(x9, x27);
 uint64_t x323, uint64_t x324 = mulx_u64(x9, x29);
 uint64_t x326, uint64_t x327 = mulx_u64(x9, x31);
 uint64_t x329, uint64_t x330 = mulx_u64(x9, x30);
 uint64_t x332, uint8_t x333 = addcarryx_u64(0x0, x309, x311);
 uint64_t x335, uint8_t x336 = addcarryx_u64(x333, x312, x314);
 uint64_t x338, uint8_t x339 = addcarryx_u64(x336, x315, x317);
 uint64_t x341, uint8_t x342 = addcarryx_u64(x339, x318, x320);
 uint64_t x344, uint8_t x345 = addcarryx_u64(x342, x321, x323);
 uint64_t x347, uint8_t x348 = addcarryx_u64(x345, x324, x326);
 uint64_t x350, uint8_t x351 = addcarryx_u64(x348, x327, x329);
 uint64_t x353, uint8_t _ = addcarryx_u64(0x0, x351, x330);
 uint64_t x356, uint8_t x357 = addcarryx_u64(0x0, x283, x308);
 uint64_t x359, uint8_t x360 = addcarryx_u64(x357, x286, x332);
 uint64_t x362, uint8_t x363 = addcarryx_u64(x360, x289, x335);
 uint64_t x365, uint8_t x366 = addcarryx_u64(x363, x292, x338);
 uint64_t x368, uint8_t x369 = addcarryx_u64(x366, x295, x341);
 uint64_t x371, uint8_t x372 = addcarryx_u64(x369, x298, x344);
 uint64_t x374, uint8_t x375 = addcarryx_u64(x372, x301, x347);
 uint64_t x377, uint8_t x378 = addcarryx_u64(x375, x304, x350);
 uint64_t x380, uint8_t x381 = addcarryx_u64(x378, x306, x353);
 uint64_t x383, uint64_t x384 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x386, uint64_t x387 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x389, uint64_t x390 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x392, uint64_t x393 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x395, uint64_t x396 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x398, uint64_t x399 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x401, uint64_t x402 = mulx_u64(x356, 0xffffffffffffffffL);
 uint64_t x404, uint64_t x405 = mulx_u64(x356, 0xfe14ffffffffffffL);
 uint64_t x407, uint8_t x408 = addcarryx_u64(0x0, x384, x386);
 uint64_t x410, uint8_t x411 = addcarryx_u64(x408, x387, x389);
 uint64_t x413, uint8_t x414 = addcarryx_u64(x411, x390, x392);
 uint64_t x416, uint8_t x417 = addcarryx_u64(x414, x393, x395);
 uint64_t x419, uint8_t x420 = addcarryx_u64(x417, x396, x398);
 uint64_t x422, uint8_t x423 = addcarryx_u64(x420, x399, x401);
 uint64_t x425, uint8_t x426 = addcarryx_u64(x423, x402, x404);
 uint64_t x428, uint8_t _ = addcarryx_u64(0x0, x426, x405);
 uint64_t _, uint8_t x432 = addcarryx_u64(0x0, x356, x383);
 uint64_t x434, uint8_t x435 = addcarryx_u64(x432, x359, x407);
 uint64_t x437, uint8_t x438 = addcarryx_u64(x435, x362, x410);
 uint64_t x440, uint8_t x441 = addcarryx_u64(x438, x365, x413);
 uint64_t x443, uint8_t x444 = addcarryx_u64(x441, x368, x416);
 uint64_t x446, uint8_t x447 = addcarryx_u64(x444, x371, x419);
 uint64_t x449, uint8_t x450 = addcarryx_u64(x447, x374, x422);
 uint64_t x452, uint8_t x453 = addcarryx_u64(x450, x377, x425);
 uint64_t x455, uint8_t x456 = addcarryx_u64(x453, x380, x428);
 uint8_t x457 = (x456 + x381);
 uint64_t x459, uint64_t x460 = mulx_u64(x11, x19);
 uint64_t x462, uint64_t x463 = mulx_u64(x11, x21);
 uint64_t x465, uint64_t x466 = mulx_u64(x11, x23);
 uint64_t x468, uint64_t x469 = mulx_u64(x11, x25);
 uint64_t x471, uint64_t x472 = mulx_u64(x11, x27);
 uint64_t x474, uint64_t x475 = mulx_u64(x11, x29);
 uint64_t x477, uint64_t x478 = mulx_u64(x11, x31);
 uint64_t x480, uint64_t x481 = mulx_u64(x11, x30);
 uint64_t x483, uint8_t x484 = addcarryx_u64(0x0, x460, x462);
 uint64_t x486, uint8_t x487 = addcarryx_u64(x484, x463, x465);
 uint64_t x489, uint8_t x490 = addcarryx_u64(x487, x466, x468);
 uint64_t x492, uint8_t x493 = addcarryx_u64(x490, x469, x471);
 uint64_t x495, uint8_t x496 = addcarryx_u64(x493, x472, x474);
 uint64_t x498, uint8_t x499 = addcarryx_u64(x496, x475, x477);
 uint64_t x501, uint8_t x502 = addcarryx_u64(x499, x478, x480);
 uint64_t x504, uint8_t _ = addcarryx_u64(0x0, x502, x481);
 uint64_t x507, uint8_t x508 = addcarryx_u64(0x0, x434, x459);
 uint64_t x510, uint8_t x511 = addcarryx_u64(x508, x437, x483);
 uint64_t x513, uint8_t x514 = addcarryx_u64(x511, x440, x486);
 uint64_t x516, uint8_t x517 = addcarryx_u64(x514, x443, x489);
 uint64_t x519, uint8_t x520 = addcarryx_u64(x517, x446, x492);
 uint64_t x522, uint8_t x523 = addcarryx_u64(x520, x449, x495);
 uint64_t x525, uint8_t x526 = addcarryx_u64(x523, x452, x498);
 uint64_t x528, uint8_t x529 = addcarryx_u64(x526, x455, x501);
 uint64_t x531, uint8_t x532 = addcarryx_u64(x529, x457, x504);
 uint64_t x534, uint64_t x535 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x537, uint64_t x538 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x540, uint64_t x541 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x543, uint64_t x544 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x546, uint64_t x547 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x549, uint64_t x550 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x552, uint64_t x553 = mulx_u64(x507, 0xffffffffffffffffL);
 uint64_t x555, uint64_t x556 = mulx_u64(x507, 0xfe14ffffffffffffL);
 uint64_t x558, uint8_t x559 = addcarryx_u64(0x0, x535, x537);
 uint64_t x561, uint8_t x562 = addcarryx_u64(x559, x538, x540);
 uint64_t x564, uint8_t x565 = addcarryx_u64(x562, x541, x543);
 uint64_t x567, uint8_t x568 = addcarryx_u64(x565, x544, x546);
 uint64_t x570, uint8_t x571 = addcarryx_u64(x568, x547, x549);
 uint64_t x573, uint8_t x574 = addcarryx_u64(x571, x550, x552);
 uint64_t x576, uint8_t x577 = addcarryx_u64(x574, x553, x555);
 uint64_t x579, uint8_t _ = addcarryx_u64(0x0, x577, x556);
 uint64_t _, uint8_t x583 = addcarryx_u64(0x0, x507, x534);
 uint64_t x585, uint8_t x586 = addcarryx_u64(x583, x510, x558);
 uint64_t x588, uint8_t x589 = addcarryx_u64(x586, x513, x561);
 uint64_t x591, uint8_t x592 = addcarryx_u64(x589, x516, x564);
 uint64_t x594, uint8_t x595 = addcarryx_u64(x592, x519, x567);
 uint64_t x597, uint8_t x598 = addcarryx_u64(x595, x522, x570);
 uint64_t x600, uint8_t x601 = addcarryx_u64(x598, x525, x573);
 uint64_t x603, uint8_t x604 = addcarryx_u64(x601, x528, x576);
 uint64_t x606, uint8_t x607 = addcarryx_u64(x604, x531, x579);
 uint8_t x608 = (x607 + x532);
 uint64_t x610, uint64_t x611 = mulx_u64(x13, x19);
 uint64_t x613, uint64_t x614 = mulx_u64(x13, x21);
 uint64_t x616, uint64_t x617 = mulx_u64(x13, x23);
 uint64_t x619, uint64_t x620 = mulx_u64(x13, x25);
 uint64_t x622, uint64_t x623 = mulx_u64(x13, x27);
 uint64_t x625, uint64_t x626 = mulx_u64(x13, x29);
 uint64_t x628, uint64_t x629 = mulx_u64(x13, x31);
 uint64_t x631, uint64_t x632 = mulx_u64(x13, x30);
 uint64_t x634, uint8_t x635 = addcarryx_u64(0x0, x611, x613);
 uint64_t x637, uint8_t x638 = addcarryx_u64(x635, x614, x616);
 uint64_t x640, uint8_t x641 = addcarryx_u64(x638, x617, x619);
 uint64_t x643, uint8_t x644 = addcarryx_u64(x641, x620, x622);
 uint64_t x646, uint8_t x647 = addcarryx_u64(x644, x623, x625);
 uint64_t x649, uint8_t x650 = addcarryx_u64(x647, x626, x628);
 uint64_t x652, uint8_t x653 = addcarryx_u64(x650, x629, x631);
 uint64_t x655, uint8_t _ = addcarryx_u64(0x0, x653, x632);
 uint64_t x658, uint8_t x659 = addcarryx_u64(0x0, x585, x610);
 uint64_t x661, uint8_t x662 = addcarryx_u64(x659, x588, x634);
 uint64_t x664, uint8_t x665 = addcarryx_u64(x662, x591, x637);
 uint64_t x667, uint8_t x668 = addcarryx_u64(x665, x594, x640);
 uint64_t x670, uint8_t x671 = addcarryx_u64(x668, x597, x643);
 uint64_t x673, uint8_t x674 = addcarryx_u64(x671, x600, x646);
 uint64_t x676, uint8_t x677 = addcarryx_u64(x674, x603, x649);
 uint64_t x679, uint8_t x680 = addcarryx_u64(x677, x606, x652);
 uint64_t x682, uint8_t x683 = addcarryx_u64(x680, x608, x655);
 uint64_t x685, uint64_t x686 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x688, uint64_t x689 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x691, uint64_t x692 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x694, uint64_t x695 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x697, uint64_t x698 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x700, uint64_t x701 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x703, uint64_t x704 = mulx_u64(x658, 0xffffffffffffffffL);
 uint64_t x706, uint64_t x707 = mulx_u64(x658, 0xfe14ffffffffffffL);
 uint64_t x709, uint8_t x710 = addcarryx_u64(0x0, x686, x688);
 uint64_t x712, uint8_t x713 = addcarryx_u64(x710, x689, x691);
 uint64_t x715, uint8_t x716 = addcarryx_u64(x713, x692, x694);
 uint64_t x718, uint8_t x719 = addcarryx_u64(x716, x695, x697);
 uint64_t x721, uint8_t x722 = addcarryx_u64(x719, x698, x700);
 uint64_t x724, uint8_t x725 = addcarryx_u64(x722, x701, x703);
 uint64_t x727, uint8_t x728 = addcarryx_u64(x725, x704, x706);
 uint64_t x730, uint8_t _ = addcarryx_u64(0x0, x728, x707);
 uint64_t _, uint8_t x734 = addcarryx_u64(0x0, x658, x685);
 uint64_t x736, uint8_t x737 = addcarryx_u64(x734, x661, x709);
 uint64_t x739, uint8_t x740 = addcarryx_u64(x737, x664, x712);
 uint64_t x742, uint8_t x743 = addcarryx_u64(x740, x667, x715);
 uint64_t x745, uint8_t x746 = addcarryx_u64(x743, x670, x718);
 uint64_t x748, uint8_t x749 = addcarryx_u64(x746, x673, x721);
 uint64_t x751, uint8_t x752 = addcarryx_u64(x749, x676, x724);
 uint64_t x754, uint8_t x755 = addcarryx_u64(x752, x679, x727);
 uint64_t x757, uint8_t x758 = addcarryx_u64(x755, x682, x730);
 uint8_t x759 = (x758 + x683);
 uint64_t x761, uint64_t x762 = mulx_u64(x15, x19);
 uint64_t x764, uint64_t x765 = mulx_u64(x15, x21);
 uint64_t x767, uint64_t x768 = mulx_u64(x15, x23);
 uint64_t x770, uint64_t x771 = mulx_u64(x15, x25);
 uint64_t x773, uint64_t x774 = mulx_u64(x15, x27);
 uint64_t x776, uint64_t x777 = mulx_u64(x15, x29);
 uint64_t x779, uint64_t x780 = mulx_u64(x15, x31);
 uint64_t x782, uint64_t x783 = mulx_u64(x15, x30);
 uint64_t x785, uint8_t x786 = addcarryx_u64(0x0, x762, x764);
 uint64_t x788, uint8_t x789 = addcarryx_u64(x786, x765, x767);
 uint64_t x791, uint8_t x792 = addcarryx_u64(x789, x768, x770);
 uint64_t x794, uint8_t x795 = addcarryx_u64(x792, x771, x773);
 uint64_t x797, uint8_t x798 = addcarryx_u64(x795, x774, x776);
 uint64_t x800, uint8_t x801 = addcarryx_u64(x798, x777, x779);
 uint64_t x803, uint8_t x804 = addcarryx_u64(x801, x780, x782);
 uint64_t x806, uint8_t _ = addcarryx_u64(0x0, x804, x783);
 uint64_t x809, uint8_t x810 = addcarryx_u64(0x0, x736, x761);
 uint64_t x812, uint8_t x813 = addcarryx_u64(x810, x739, x785);
 uint64_t x815, uint8_t x816 = addcarryx_u64(x813, x742, x788);
 uint64_t x818, uint8_t x819 = addcarryx_u64(x816, x745, x791);
 uint64_t x821, uint8_t x822 = addcarryx_u64(x819, x748, x794);
 uint64_t x824, uint8_t x825 = addcarryx_u64(x822, x751, x797);
 uint64_t x827, uint8_t x828 = addcarryx_u64(x825, x754, x800);
 uint64_t x830, uint8_t x831 = addcarryx_u64(x828, x757, x803);
 uint64_t x833, uint8_t x834 = addcarryx_u64(x831, x759, x806);
 uint64_t x836, uint64_t x837 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x839, uint64_t x840 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x842, uint64_t x843 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x845, uint64_t x846 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x848, uint64_t x849 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x851, uint64_t x852 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x854, uint64_t x855 = mulx_u64(x809, 0xffffffffffffffffL);
 uint64_t x857, uint64_t x858 = mulx_u64(x809, 0xfe14ffffffffffffL);
 uint64_t x860, uint8_t x861 = addcarryx_u64(0x0, x837, x839);
 uint64_t x863, uint8_t x864 = addcarryx_u64(x861, x840, x842);
 uint64_t x866, uint8_t x867 = addcarryx_u64(x864, x843, x845);
 uint64_t x869, uint8_t x870 = addcarryx_u64(x867, x846, x848);
 uint64_t x872, uint8_t x873 = addcarryx_u64(x870, x849, x851);
 uint64_t x875, uint8_t x876 = addcarryx_u64(x873, x852, x854);
 uint64_t x878, uint8_t x879 = addcarryx_u64(x876, x855, x857);
 uint64_t x881, uint8_t _ = addcarryx_u64(0x0, x879, x858);
 uint64_t _, uint8_t x885 = addcarryx_u64(0x0, x809, x836);
 uint64_t x887, uint8_t x888 = addcarryx_u64(x885, x812, x860);
 uint64_t x890, uint8_t x891 = addcarryx_u64(x888, x815, x863);
 uint64_t x893, uint8_t x894 = addcarryx_u64(x891, x818, x866);
 uint64_t x896, uint8_t x897 = addcarryx_u64(x894, x821, x869);
 uint64_t x899, uint8_t x900 = addcarryx_u64(x897, x824, x872);
 uint64_t x902, uint8_t x903 = addcarryx_u64(x900, x827, x875);
 uint64_t x905, uint8_t x906 = addcarryx_u64(x903, x830, x878);
 uint64_t x908, uint8_t x909 = addcarryx_u64(x906, x833, x881);
 uint8_t x910 = (x909 + x834);
 uint64_t x912, uint64_t x913 = mulx_u64(x17, x19);
 uint64_t x915, uint64_t x916 = mulx_u64(x17, x21);
 uint64_t x918, uint64_t x919 = mulx_u64(x17, x23);
 uint64_t x921, uint64_t x922 = mulx_u64(x17, x25);
 uint64_t x924, uint64_t x925 = mulx_u64(x17, x27);
 uint64_t x927, uint64_t x928 = mulx_u64(x17, x29);
 uint64_t x930, uint64_t x931 = mulx_u64(x17, x31);
 uint64_t x933, uint64_t x934 = mulx_u64(x17, x30);
 uint64_t x936, uint8_t x937 = addcarryx_u64(0x0, x913, x915);
 uint64_t x939, uint8_t x940 = addcarryx_u64(x937, x916, x918);
 uint64_t x942, uint8_t x943 = addcarryx_u64(x940, x919, x921);
 uint64_t x945, uint8_t x946 = addcarryx_u64(x943, x922, x924);
 uint64_t x948, uint8_t x949 = addcarryx_u64(x946, x925, x927);
 uint64_t x951, uint8_t x952 = addcarryx_u64(x949, x928, x930);
 uint64_t x954, uint8_t x955 = addcarryx_u64(x952, x931, x933);
 uint64_t x957, uint8_t _ = addcarryx_u64(0x0, x955, x934);
 uint64_t x960, uint8_t x961 = addcarryx_u64(0x0, x887, x912);
 uint64_t x963, uint8_t x964 = addcarryx_u64(x961, x890, x936);
 uint64_t x966, uint8_t x967 = addcarryx_u64(x964, x893, x939);
 uint64_t x969, uint8_t x970 = addcarryx_u64(x967, x896, x942);
 uint64_t x972, uint8_t x973 = addcarryx_u64(x970, x899, x945);
 uint64_t x975, uint8_t x976 = addcarryx_u64(x973, x902, x948);
 uint64_t x978, uint8_t x979 = addcarryx_u64(x976, x905, x951);
 uint64_t x981, uint8_t x982 = addcarryx_u64(x979, x908, x954);
 uint64_t x984, uint8_t x985 = addcarryx_u64(x982, x910, x957);
 uint64_t x987, uint64_t x988 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x990, uint64_t x991 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x993, uint64_t x994 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x996, uint64_t x997 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x999, uint64_t x1000 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x1002, uint64_t x1003 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x1005, uint64_t x1006 = mulx_u64(x960, 0xffffffffffffffffL);
 uint64_t x1008, uint64_t x1009 = mulx_u64(x960, 0xfe14ffffffffffffL);
 uint64_t x1011, uint8_t x1012 = addcarryx_u64(0x0, x988, x990);
 uint64_t x1014, uint8_t x1015 = addcarryx_u64(x1012, x991, x993);
 uint64_t x1017, uint8_t x1018 = addcarryx_u64(x1015, x994, x996);
 uint64_t x1020, uint8_t x1021 = addcarryx_u64(x1018, x997, x999);
 uint64_t x1023, uint8_t x1024 = addcarryx_u64(x1021, x1000, x1002);
 uint64_t x1026, uint8_t x1027 = addcarryx_u64(x1024, x1003, x1005);
 uint64_t x1029, uint8_t x1030 = addcarryx_u64(x1027, x1006, x1008);
 uint64_t x1032, uint8_t _ = addcarryx_u64(0x0, x1030, x1009);
 uint64_t _, uint8_t x1036 = addcarryx_u64(0x0, x960, x987);
 uint64_t x1038, uint8_t x1039 = addcarryx_u64(x1036, x963, x1011);
 uint64_t x1041, uint8_t x1042 = addcarryx_u64(x1039, x966, x1014);
 uint64_t x1044, uint8_t x1045 = addcarryx_u64(x1042, x969, x1017);
 uint64_t x1047, uint8_t x1048 = addcarryx_u64(x1045, x972, x1020);
 uint64_t x1050, uint8_t x1051 = addcarryx_u64(x1048, x975, x1023);
 uint64_t x1053, uint8_t x1054 = addcarryx_u64(x1051, x978, x1026);
 uint64_t x1056, uint8_t x1057 = addcarryx_u64(x1054, x981, x1029);
 uint64_t x1059, uint8_t x1060 = addcarryx_u64(x1057, x984, x1032);
 uint8_t x1061 = (x1060 + x985);
 uint64_t x1063, uint64_t x1064 = mulx_u64(x16, x19);
 uint64_t x1066, uint64_t x1067 = mulx_u64(x16, x21);
 uint64_t x1069, uint64_t x1070 = mulx_u64(x16, x23);
 uint64_t x1072, uint64_t x1073 = mulx_u64(x16, x25);
 uint64_t x1075, uint64_t x1076 = mulx_u64(x16, x27);
 uint64_t x1078, uint64_t x1079 = mulx_u64(x16, x29);
 uint64_t x1081, uint64_t x1082 = mulx_u64(x16, x31);
 uint64_t x1084, uint64_t x1085 = mulx_u64(x16, x30);
 uint64_t x1087, uint8_t x1088 = addcarryx_u64(0x0, x1064, x1066);
 uint64_t x1090, uint8_t x1091 = addcarryx_u64(x1088, x1067, x1069);
 uint64_t x1093, uint8_t x1094 = addcarryx_u64(x1091, x1070, x1072);
 uint64_t x1096, uint8_t x1097 = addcarryx_u64(x1094, x1073, x1075);
 uint64_t x1099, uint8_t x1100 = addcarryx_u64(x1097, x1076, x1078);
 uint64_t x1102, uint8_t x1103 = addcarryx_u64(x1100, x1079, x1081);
 uint64_t x1105, uint8_t x1106 = addcarryx_u64(x1103, x1082, x1084);
 uint64_t x1108, uint8_t _ = addcarryx_u64(0x0, x1106, x1085);
 uint64_t x1111, uint8_t x1112 = addcarryx_u64(0x0, x1038, x1063);
 uint64_t x1114, uint8_t x1115 = addcarryx_u64(x1112, x1041, x1087);
 uint64_t x1117, uint8_t x1118 = addcarryx_u64(x1115, x1044, x1090);
 uint64_t x1120, uint8_t x1121 = addcarryx_u64(x1118, x1047, x1093);
 uint64_t x1123, uint8_t x1124 = addcarryx_u64(x1121, x1050, x1096);
 uint64_t x1126, uint8_t x1127 = addcarryx_u64(x1124, x1053, x1099);
 uint64_t x1129, uint8_t x1130 = addcarryx_u64(x1127, x1056, x1102);
 uint64_t x1132, uint8_t x1133 = addcarryx_u64(x1130, x1059, x1105);
 uint64_t x1135, uint8_t x1136 = addcarryx_u64(x1133, x1061, x1108);
 uint64_t x1138, uint64_t x1139 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1141, uint64_t x1142 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1144, uint64_t x1145 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1147, uint64_t x1148 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1150, uint64_t x1151 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1153, uint64_t x1154 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1156, uint64_t x1157 = mulx_u64(x1111, 0xffffffffffffffffL);
 uint64_t x1159, uint64_t x1160 = mulx_u64(x1111, 0xfe14ffffffffffffL);
 uint64_t x1162, uint8_t x1163 = addcarryx_u64(0x0, x1139, x1141);
 uint64_t x1165, uint8_t x1166 = addcarryx_u64(x1163, x1142, x1144);
 uint64_t x1168, uint8_t x1169 = addcarryx_u64(x1166, x1145, x1147);
 uint64_t x1171, uint8_t x1172 = addcarryx_u64(x1169, x1148, x1150);
 uint64_t x1174, uint8_t x1175 = addcarryx_u64(x1172, x1151, x1153);
 uint64_t x1177, uint8_t x1178 = addcarryx_u64(x1175, x1154, x1156);
 uint64_t x1180, uint8_t x1181 = addcarryx_u64(x1178, x1157, x1159);
 uint64_t x1183, uint8_t _ = addcarryx_u64(0x0, x1181, x1160);
 uint64_t _, uint8_t x1187 = addcarryx_u64(0x0, x1111, x1138);
 uint64_t x1189, uint8_t x1190 = addcarryx_u64(x1187, x1114, x1162);
 uint64_t x1192, uint8_t x1193 = addcarryx_u64(x1190, x1117, x1165);
 uint64_t x1195, uint8_t x1196 = addcarryx_u64(x1193, x1120, x1168);
 uint64_t x1198, uint8_t x1199 = addcarryx_u64(x1196, x1123, x1171);
 uint64_t x1201, uint8_t x1202 = addcarryx_u64(x1199, x1126, x1174);
 uint64_t x1204, uint8_t x1205 = addcarryx_u64(x1202, x1129, x1177);
 uint64_t x1207, uint8_t x1208 = addcarryx_u64(x1205, x1132, x1180);
 uint64_t x1210, uint8_t x1211 = addcarryx_u64(x1208, x1135, x1183);
 uint8_t x1212 = (x1211 + x1136);
 uint64_t x1214, uint8_t x1215 = subborrow_u64(0x0, x1189, 0xffffffffffffffffL);
 uint64_t x1217, uint8_t x1218 = subborrow_u64(x1215, x1192, 0xffffffffffffffffL);
 uint64_t x1220, uint8_t x1221 = subborrow_u64(x1218, x1195, 0xffffffffffffffffL);
 uint64_t x1223, uint8_t x1224 = subborrow_u64(x1221, x1198, 0xffffffffffffffffL);
 uint64_t x1226, uint8_t x1227 = subborrow_u64(x1224, x1201, 0xffffffffffffffffL);
 uint64_t x1229, uint8_t x1230 = subborrow_u64(x1227, x1204, 0xffffffffffffffffL);
 uint64_t x1232, uint8_t x1233 = subborrow_u64(x1230, x1207, 0xffffffffffffffffL);
 uint64_t x1235, uint8_t x1236 = subborrow_u64(x1233, x1210, 0xfe14ffffffffffffL);
 uint64_t _, uint8_t x1239 = subborrow_u64(x1236, x1212, 0x0);
 uint64_t x1240 = cmovznz64(x1239, x1235, x1210);
 uint64_t x1241 = cmovznz64(x1239, x1232, x1207);
 uint64_t x1242 = cmovznz64(x1239, x1229, x1204);
 uint64_t x1243 = cmovznz64(x1239, x1226, x1201);
 uint64_t x1244 = cmovznz64(x1239, x1223, x1198);
 uint64_t x1245 = cmovznz64(x1239, x1220, x1195);
 uint64_t x1246 = cmovznz64(x1239, x1217, x1192);
 uint64_t x1247 = cmovznz64(x1239, x1214, x1189);
 return (x1240, x1241, x1242, x1243, x1244, x1245, x1246, x1247))
(x, x0)%core
     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)