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

λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
Interp-η
(λ var : Syntax.base_type → Type,
 λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
 uint32_t x33, uint32_t x34 = mulx_u32(x5, x19);
 uint32_t x36, uint32_t x37 = mulx_u32(x5, x21);
 uint32_t x39, uint32_t x40 = mulx_u32(x5, x23);
 uint32_t x42, uint32_t x43 = mulx_u32(x5, x25);
 uint32_t x45, uint32_t x46 = mulx_u32(x5, x27);
 uint32_t x48, uint32_t x49 = mulx_u32(x5, x29);
 uint32_t x51, uint32_t x52 = mulx_u32(x5, x31);
 uint32_t x54, uint32_t x55 = mulx_u32(x5, x30);
 uint32_t x57, uint8_t x58 = addcarryx_u32(0x0, x34, x36);
 uint32_t x60, uint8_t x61 = addcarryx_u32(x58, x37, x39);
 uint32_t x63, uint8_t x64 = addcarryx_u32(x61, x40, x42);
 uint32_t x66, uint8_t x67 = addcarryx_u32(x64, x43, x45);
 uint32_t x69, uint8_t x70 = addcarryx_u32(x67, x46, x48);
 uint32_t x72, uint8_t x73 = addcarryx_u32(x70, x49, x51);
 uint32_t x75, uint8_t x76 = addcarryx_u32(x73, x52, x54);
 uint32_t x78, uint8_t _ = addcarryx_u32(0x0, x76, x55);
 uint32_t x81, uint32_t x82 = mulx_u32(x33, 0xffffffff);
 uint32_t x84, uint32_t x85 = mulx_u32(x33, 0xffffffff);
 uint32_t x87, uint32_t x88 = mulx_u32(x33, 0xffffffff);
 uint32_t x90, uint32_t x91 = mulx_u32(x33, 0xffffffff);
 uint32_t x93, uint8_t x94 = addcarryx_u32(0x0, x82, x84);
 uint32_t x96, uint8_t x97 = addcarryx_u32(x94, x85, x87);
 uint32_t x99, uint8_t x100 = addcarryx_u32(x97, x88, 0x0);
 uint8_t x101 = (0x0 + 0x0);
 uint32_t _, uint8_t x104 = addcarryx_u32(0x0, x33, x81);
 uint32_t x106, uint8_t x107 = addcarryx_u32(x104, x57, x93);
 uint32_t x109, uint8_t x110 = addcarryx_u32(x107, x60, x96);
 uint32_t x112, uint8_t x113 = addcarryx_u32(x110, x63, x99);
 uint32_t x115, uint8_t x116 = addcarryx_u32(x113, x66, x100);
 uint32_t x118, uint8_t x119 = addcarryx_u32(x116, x69, x101);
 uint32_t x121, uint8_t x122 = addcarryx_u32(x119, x72, x33);
 uint32_t x124, uint8_t x125 = addcarryx_u32(x122, x75, x90);
 uint32_t x127, uint8_t x128 = addcarryx_u32(x125, x78, x91);
 uint8_t x129 = (x128 + 0x0);
 uint32_t x131, uint32_t x132 = mulx_u32(x7, x19);
 uint32_t x134, uint32_t x135 = mulx_u32(x7, x21);
 uint32_t x137, uint32_t x138 = mulx_u32(x7, x23);
 uint32_t x140, uint32_t x141 = mulx_u32(x7, x25);
 uint32_t x143, uint32_t x144 = mulx_u32(x7, x27);
 uint32_t x146, uint32_t x147 = mulx_u32(x7, x29);
 uint32_t x149, uint32_t x150 = mulx_u32(x7, x31);
 uint32_t x152, uint32_t x153 = mulx_u32(x7, x30);
 uint32_t x155, uint8_t x156 = addcarryx_u32(0x0, x132, x134);
 uint32_t x158, uint8_t x159 = addcarryx_u32(x156, x135, x137);
 uint32_t x161, uint8_t x162 = addcarryx_u32(x159, x138, x140);
 uint32_t x164, uint8_t x165 = addcarryx_u32(x162, x141, x143);
 uint32_t x167, uint8_t x168 = addcarryx_u32(x165, x144, x146);
 uint32_t x170, uint8_t x171 = addcarryx_u32(x168, x147, x149);
 uint32_t x173, uint8_t x174 = addcarryx_u32(x171, x150, x152);
 uint32_t x176, uint8_t _ = addcarryx_u32(0x0, x174, x153);
 uint32_t x179, uint8_t x180 = addcarryx_u32(0x0, x106, x131);
 uint32_t x182, uint8_t x183 = addcarryx_u32(x180, x109, x155);
 uint32_t x185, uint8_t x186 = addcarryx_u32(x183, x112, x158);
 uint32_t x188, uint8_t x189 = addcarryx_u32(x186, x115, x161);
 uint32_t x191, uint8_t x192 = addcarryx_u32(x189, x118, x164);
 uint32_t x194, uint8_t x195 = addcarryx_u32(x192, x121, x167);
 uint32_t x197, uint8_t x198 = addcarryx_u32(x195, x124, x170);
 uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x127, x173);
 uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x129, x176);
 uint32_t x206, uint32_t x207 = mulx_u32(x179, 0xffffffff);
 uint32_t x209, uint32_t x210 = mulx_u32(x179, 0xffffffff);
 uint32_t x212, uint32_t x213 = mulx_u32(x179, 0xffffffff);
 uint32_t x215, uint32_t x216 = mulx_u32(x179, 0xffffffff);
 uint32_t x218, uint8_t x219 = addcarryx_u32(0x0, x207, x209);
 uint32_t x221, uint8_t x222 = addcarryx_u32(x219, x210, x212);
 uint32_t x224, uint8_t x225 = addcarryx_u32(x222, x213, 0x0);
 uint8_t x226 = (0x0 + 0x0);
 uint32_t _, uint8_t x229 = addcarryx_u32(0x0, x179, x206);
 uint32_t x231, uint8_t x232 = addcarryx_u32(x229, x182, x218);
 uint32_t x234, uint8_t x235 = addcarryx_u32(x232, x185, x221);
 uint32_t x237, uint8_t x238 = addcarryx_u32(x235, x188, x224);
 uint32_t x240, uint8_t x241 = addcarryx_u32(x238, x191, x225);
 uint32_t x243, uint8_t x244 = addcarryx_u32(x241, x194, x226);
 uint32_t x246, uint8_t x247 = addcarryx_u32(x244, x197, x179);
 uint32_t x249, uint8_t x250 = addcarryx_u32(x247, x200, x215);
 uint32_t x252, uint8_t x253 = addcarryx_u32(x250, x203, x216);
 uint8_t x254 = (x253 + x204);
 uint32_t x256, uint32_t x257 = mulx_u32(x9, x19);
 uint32_t x259, uint32_t x260 = mulx_u32(x9, x21);
 uint32_t x262, uint32_t x263 = mulx_u32(x9, x23);
 uint32_t x265, uint32_t x266 = mulx_u32(x9, x25);
 uint32_t x268, uint32_t x269 = mulx_u32(x9, x27);
 uint32_t x271, uint32_t x272 = mulx_u32(x9, x29);
 uint32_t x274, uint32_t x275 = mulx_u32(x9, x31);
 uint32_t x277, uint32_t x278 = mulx_u32(x9, x30);
 uint32_t x280, uint8_t x281 = addcarryx_u32(0x0, x257, x259);
 uint32_t x283, uint8_t x284 = addcarryx_u32(x281, x260, x262);
 uint32_t x286, uint8_t x287 = addcarryx_u32(x284, x263, x265);
 uint32_t x289, uint8_t x290 = addcarryx_u32(x287, x266, x268);
 uint32_t x292, uint8_t x293 = addcarryx_u32(x290, x269, x271);
 uint32_t x295, uint8_t x296 = addcarryx_u32(x293, x272, x274);
 uint32_t x298, uint8_t x299 = addcarryx_u32(x296, x275, x277);
 uint32_t x301, uint8_t _ = addcarryx_u32(0x0, x299, x278);
 uint32_t x304, uint8_t x305 = addcarryx_u32(0x0, x231, x256);
 uint32_t x307, uint8_t x308 = addcarryx_u32(x305, x234, x280);
 uint32_t x310, uint8_t x311 = addcarryx_u32(x308, x237, x283);
 uint32_t x313, uint8_t x314 = addcarryx_u32(x311, x240, x286);
 uint32_t x316, uint8_t x317 = addcarryx_u32(x314, x243, x289);
 uint32_t x319, uint8_t x320 = addcarryx_u32(x317, x246, x292);
 uint32_t x322, uint8_t x323 = addcarryx_u32(x320, x249, x295);
 uint32_t x325, uint8_t x326 = addcarryx_u32(x323, x252, x298);
 uint32_t x328, uint8_t x329 = addcarryx_u32(x326, x254, x301);
 uint32_t x331, uint32_t x332 = mulx_u32(x304, 0xffffffff);
 uint32_t x334, uint32_t x335 = mulx_u32(x304, 0xffffffff);
 uint32_t x337, uint32_t x338 = mulx_u32(x304, 0xffffffff);
 uint32_t x340, uint32_t x341 = mulx_u32(x304, 0xffffffff);
 uint32_t x343, uint8_t x344 = addcarryx_u32(0x0, x332, x334);
 uint32_t x346, uint8_t x347 = addcarryx_u32(x344, x335, x337);
 uint32_t x349, uint8_t x350 = addcarryx_u32(x347, x338, 0x0);
 uint8_t x351 = (0x0 + 0x0);
 uint32_t _, uint8_t x354 = addcarryx_u32(0x0, x304, x331);
 uint32_t x356, uint8_t x357 = addcarryx_u32(x354, x307, x343);
 uint32_t x359, uint8_t x360 = addcarryx_u32(x357, x310, x346);
 uint32_t x362, uint8_t x363 = addcarryx_u32(x360, x313, x349);
 uint32_t x365, uint8_t x366 = addcarryx_u32(x363, x316, x350);
 uint32_t x368, uint8_t x369 = addcarryx_u32(x366, x319, x351);
 uint32_t x371, uint8_t x372 = addcarryx_u32(x369, x322, x304);
 uint32_t x374, uint8_t x375 = addcarryx_u32(x372, x325, x340);
 uint32_t x377, uint8_t x378 = addcarryx_u32(x375, x328, x341);
 uint8_t x379 = (x378 + x329);
 uint32_t x381, uint32_t x382 = mulx_u32(x11, x19);
 uint32_t x384, uint32_t x385 = mulx_u32(x11, x21);
 uint32_t x387, uint32_t x388 = mulx_u32(x11, x23);
 uint32_t x390, uint32_t x391 = mulx_u32(x11, x25);
 uint32_t x393, uint32_t x394 = mulx_u32(x11, x27);
 uint32_t x396, uint32_t x397 = mulx_u32(x11, x29);
 uint32_t x399, uint32_t x400 = mulx_u32(x11, x31);
 uint32_t x402, uint32_t x403 = mulx_u32(x11, x30);
 uint32_t x405, uint8_t x406 = addcarryx_u32(0x0, x382, x384);
 uint32_t x408, uint8_t x409 = addcarryx_u32(x406, x385, x387);
 uint32_t x411, uint8_t x412 = addcarryx_u32(x409, x388, x390);
 uint32_t x414, uint8_t x415 = addcarryx_u32(x412, x391, x393);
 uint32_t x417, uint8_t x418 = addcarryx_u32(x415, x394, x396);
 uint32_t x420, uint8_t x421 = addcarryx_u32(x418, x397, x399);
 uint32_t x423, uint8_t x424 = addcarryx_u32(x421, x400, x402);
 uint32_t x426, uint8_t _ = addcarryx_u32(0x0, x424, x403);
 uint32_t x429, uint8_t x430 = addcarryx_u32(0x0, x356, x381);
 uint32_t x432, uint8_t x433 = addcarryx_u32(x430, x359, x405);
 uint32_t x435, uint8_t x436 = addcarryx_u32(x433, x362, x408);
 uint32_t x438, uint8_t x439 = addcarryx_u32(x436, x365, x411);
 uint32_t x441, uint8_t x442 = addcarryx_u32(x439, x368, x414);
 uint32_t x444, uint8_t x445 = addcarryx_u32(x442, x371, x417);
 uint32_t x447, uint8_t x448 = addcarryx_u32(x445, x374, x420);
 uint32_t x450, uint8_t x451 = addcarryx_u32(x448, x377, x423);
 uint32_t x453, uint8_t x454 = addcarryx_u32(x451, x379, x426);
 uint32_t x456, uint32_t x457 = mulx_u32(x429, 0xffffffff);
 uint32_t x459, uint32_t x460 = mulx_u32(x429, 0xffffffff);
 uint32_t x462, uint32_t x463 = mulx_u32(x429, 0xffffffff);
 uint32_t x465, uint32_t x466 = mulx_u32(x429, 0xffffffff);
 uint32_t x468, uint8_t x469 = addcarryx_u32(0x0, x457, x459);
 uint32_t x471, uint8_t x472 = addcarryx_u32(x469, x460, x462);
 uint32_t x474, uint8_t x475 = addcarryx_u32(x472, x463, 0x0);
 uint8_t x476 = (0x0 + 0x0);
 uint32_t _, uint8_t x479 = addcarryx_u32(0x0, x429, x456);
 uint32_t x481, uint8_t x482 = addcarryx_u32(x479, x432, x468);
 uint32_t x484, uint8_t x485 = addcarryx_u32(x482, x435, x471);
 uint32_t x487, uint8_t x488 = addcarryx_u32(x485, x438, x474);
 uint32_t x490, uint8_t x491 = addcarryx_u32(x488, x441, x475);
 uint32_t x493, uint8_t x494 = addcarryx_u32(x491, x444, x476);
 uint32_t x496, uint8_t x497 = addcarryx_u32(x494, x447, x429);
 uint32_t x499, uint8_t x500 = addcarryx_u32(x497, x450, x465);
 uint32_t x502, uint8_t x503 = addcarryx_u32(x500, x453, x466);
 uint8_t x504 = (x503 + x454);
 uint32_t x506, uint32_t x507 = mulx_u32(x13, x19);
 uint32_t x509, uint32_t x510 = mulx_u32(x13, x21);
 uint32_t x512, uint32_t x513 = mulx_u32(x13, x23);
 uint32_t x515, uint32_t x516 = mulx_u32(x13, x25);
 uint32_t x518, uint32_t x519 = mulx_u32(x13, x27);
 uint32_t x521, uint32_t x522 = mulx_u32(x13, x29);
 uint32_t x524, uint32_t x525 = mulx_u32(x13, x31);
 uint32_t x527, uint32_t x528 = mulx_u32(x13, x30);
 uint32_t x530, uint8_t x531 = addcarryx_u32(0x0, x507, x509);
 uint32_t x533, uint8_t x534 = addcarryx_u32(x531, x510, x512);
 uint32_t x536, uint8_t x537 = addcarryx_u32(x534, x513, x515);
 uint32_t x539, uint8_t x540 = addcarryx_u32(x537, x516, x518);
 uint32_t x542, uint8_t x543 = addcarryx_u32(x540, x519, x521);
 uint32_t x545, uint8_t x546 = addcarryx_u32(x543, x522, x524);
 uint32_t x548, uint8_t x549 = addcarryx_u32(x546, x525, x527);
 uint32_t x551, uint8_t _ = addcarryx_u32(0x0, x549, x528);
 uint32_t x554, uint8_t x555 = addcarryx_u32(0x0, x481, x506);
 uint32_t x557, uint8_t x558 = addcarryx_u32(x555, x484, x530);
 uint32_t x560, uint8_t x561 = addcarryx_u32(x558, x487, x533);
 uint32_t x563, uint8_t x564 = addcarryx_u32(x561, x490, x536);
 uint32_t x566, uint8_t x567 = addcarryx_u32(x564, x493, x539);
 uint32_t x569, uint8_t x570 = addcarryx_u32(x567, x496, x542);
 uint32_t x572, uint8_t x573 = addcarryx_u32(x570, x499, x545);
 uint32_t x575, uint8_t x576 = addcarryx_u32(x573, x502, x548);
 uint32_t x578, uint8_t x579 = addcarryx_u32(x576, x504, x551);
 uint32_t x581, uint32_t x582 = mulx_u32(x554, 0xffffffff);
 uint32_t x584, uint32_t x585 = mulx_u32(x554, 0xffffffff);
 uint32_t x587, uint32_t x588 = mulx_u32(x554, 0xffffffff);
 uint32_t x590, uint32_t x591 = mulx_u32(x554, 0xffffffff);
 uint32_t x593, uint8_t x594 = addcarryx_u32(0x0, x582, x584);
 uint32_t x596, uint8_t x597 = addcarryx_u32(x594, x585, x587);
 uint32_t x599, uint8_t x600 = addcarryx_u32(x597, x588, 0x0);
 uint8_t x601 = (0x0 + 0x0);
 uint32_t _, uint8_t x604 = addcarryx_u32(0x0, x554, x581);
 uint32_t x606, uint8_t x607 = addcarryx_u32(x604, x557, x593);
 uint32_t x609, uint8_t x610 = addcarryx_u32(x607, x560, x596);
 uint32_t x612, uint8_t x613 = addcarryx_u32(x610, x563, x599);
 uint32_t x615, uint8_t x616 = addcarryx_u32(x613, x566, x600);
 uint32_t x618, uint8_t x619 = addcarryx_u32(x616, x569, x601);
 uint32_t x621, uint8_t x622 = addcarryx_u32(x619, x572, x554);
 uint32_t x624, uint8_t x625 = addcarryx_u32(x622, x575, x590);
 uint32_t x627, uint8_t x628 = addcarryx_u32(x625, x578, x591);
 uint8_t x629 = (x628 + x579);
 uint32_t x631, uint32_t x632 = mulx_u32(x15, x19);
 uint32_t x634, uint32_t x635 = mulx_u32(x15, x21);
 uint32_t x637, uint32_t x638 = mulx_u32(x15, x23);
 uint32_t x640, uint32_t x641 = mulx_u32(x15, x25);
 uint32_t x643, uint32_t x644 = mulx_u32(x15, x27);
 uint32_t x646, uint32_t x647 = mulx_u32(x15, x29);
 uint32_t x649, uint32_t x650 = mulx_u32(x15, x31);
 uint32_t x652, uint32_t x653 = mulx_u32(x15, x30);
 uint32_t x655, uint8_t x656 = addcarryx_u32(0x0, x632, x634);
 uint32_t x658, uint8_t x659 = addcarryx_u32(x656, x635, x637);
 uint32_t x661, uint8_t x662 = addcarryx_u32(x659, x638, x640);
 uint32_t x664, uint8_t x665 = addcarryx_u32(x662, x641, x643);
 uint32_t x667, uint8_t x668 = addcarryx_u32(x665, x644, x646);
 uint32_t x670, uint8_t x671 = addcarryx_u32(x668, x647, x649);
 uint32_t x673, uint8_t x674 = addcarryx_u32(x671, x650, x652);
 uint32_t x676, uint8_t _ = addcarryx_u32(0x0, x674, x653);
 uint32_t x679, uint8_t x680 = addcarryx_u32(0x0, x606, x631);
 uint32_t x682, uint8_t x683 = addcarryx_u32(x680, x609, x655);
 uint32_t x685, uint8_t x686 = addcarryx_u32(x683, x612, x658);
 uint32_t x688, uint8_t x689 = addcarryx_u32(x686, x615, x661);
 uint32_t x691, uint8_t x692 = addcarryx_u32(x689, x618, x664);
 uint32_t x694, uint8_t x695 = addcarryx_u32(x692, x621, x667);
 uint32_t x697, uint8_t x698 = addcarryx_u32(x695, x624, x670);
 uint32_t x700, uint8_t x701 = addcarryx_u32(x698, x627, x673);
 uint32_t x703, uint8_t x704 = addcarryx_u32(x701, x629, x676);
 uint32_t x706, uint32_t x707 = mulx_u32(x679, 0xffffffff);
 uint32_t x709, uint32_t x710 = mulx_u32(x679, 0xffffffff);
 uint32_t x712, uint32_t x713 = mulx_u32(x679, 0xffffffff);
 uint32_t x715, uint32_t x716 = mulx_u32(x679, 0xffffffff);
 uint32_t x718, uint8_t x719 = addcarryx_u32(0x0, x707, x709);
 uint32_t x721, uint8_t x722 = addcarryx_u32(x719, x710, x712);
 uint32_t x724, uint8_t x725 = addcarryx_u32(x722, x713, 0x0);
 uint8_t x726 = (0x0 + 0x0);
 uint32_t _, uint8_t x729 = addcarryx_u32(0x0, x679, x706);
 uint32_t x731, uint8_t x732 = addcarryx_u32(x729, x682, x718);
 uint32_t x734, uint8_t x735 = addcarryx_u32(x732, x685, x721);
 uint32_t x737, uint8_t x738 = addcarryx_u32(x735, x688, x724);
 uint32_t x740, uint8_t x741 = addcarryx_u32(x738, x691, x725);
 uint32_t x743, uint8_t x744 = addcarryx_u32(x741, x694, x726);
 uint32_t x746, uint8_t x747 = addcarryx_u32(x744, x697, x679);
 uint32_t x749, uint8_t x750 = addcarryx_u32(x747, x700, x715);
 uint32_t x752, uint8_t x753 = addcarryx_u32(x750, x703, x716);
 uint8_t x754 = (x753 + x704);
 uint32_t x756, uint32_t x757 = mulx_u32(x17, x19);
 uint32_t x759, uint32_t x760 = mulx_u32(x17, x21);
 uint32_t x762, uint32_t x763 = mulx_u32(x17, x23);
 uint32_t x765, uint32_t x766 = mulx_u32(x17, x25);
 uint32_t x768, uint32_t x769 = mulx_u32(x17, x27);
 uint32_t x771, uint32_t x772 = mulx_u32(x17, x29);
 uint32_t x774, uint32_t x775 = mulx_u32(x17, x31);
 uint32_t x777, uint32_t x778 = mulx_u32(x17, x30);
 uint32_t x780, uint8_t x781 = addcarryx_u32(0x0, x757, x759);
 uint32_t x783, uint8_t x784 = addcarryx_u32(x781, x760, x762);
 uint32_t x786, uint8_t x787 = addcarryx_u32(x784, x763, x765);
 uint32_t x789, uint8_t x790 = addcarryx_u32(x787, x766, x768);
 uint32_t x792, uint8_t x793 = addcarryx_u32(x790, x769, x771);
 uint32_t x795, uint8_t x796 = addcarryx_u32(x793, x772, x774);
 uint32_t x798, uint8_t x799 = addcarryx_u32(x796, x775, x777);
 uint32_t x801, uint8_t _ = addcarryx_u32(0x0, x799, x778);
 uint32_t x804, uint8_t x805 = addcarryx_u32(0x0, x731, x756);
 uint32_t x807, uint8_t x808 = addcarryx_u32(x805, x734, x780);
 uint32_t x810, uint8_t x811 = addcarryx_u32(x808, x737, x783);
 uint32_t x813, uint8_t x814 = addcarryx_u32(x811, x740, x786);
 uint32_t x816, uint8_t x817 = addcarryx_u32(x814, x743, x789);
 uint32_t x819, uint8_t x820 = addcarryx_u32(x817, x746, x792);
 uint32_t x822, uint8_t x823 = addcarryx_u32(x820, x749, x795);
 uint32_t x825, uint8_t x826 = addcarryx_u32(x823, x752, x798);
 uint32_t x828, uint8_t x829 = addcarryx_u32(x826, x754, x801);
 uint32_t x831, uint32_t x832 = mulx_u32(x804, 0xffffffff);
 uint32_t x834, uint32_t x835 = mulx_u32(x804, 0xffffffff);
 uint32_t x837, uint32_t x838 = mulx_u32(x804, 0xffffffff);
 uint32_t x840, uint32_t x841 = mulx_u32(x804, 0xffffffff);
 uint32_t x843, uint8_t x844 = addcarryx_u32(0x0, x832, x834);
 uint32_t x846, uint8_t x847 = addcarryx_u32(x844, x835, x837);
 uint32_t x849, uint8_t x850 = addcarryx_u32(x847, x838, 0x0);
 uint8_t x851 = (0x0 + 0x0);
 uint32_t _, uint8_t x854 = addcarryx_u32(0x0, x804, x831);
 uint32_t x856, uint8_t x857 = addcarryx_u32(x854, x807, x843);
 uint32_t x859, uint8_t x860 = addcarryx_u32(x857, x810, x846);
 uint32_t x862, uint8_t x863 = addcarryx_u32(x860, x813, x849);
 uint32_t x865, uint8_t x866 = addcarryx_u32(x863, x816, x850);
 uint32_t x868, uint8_t x869 = addcarryx_u32(x866, x819, x851);
 uint32_t x871, uint8_t x872 = addcarryx_u32(x869, x822, x804);
 uint32_t x874, uint8_t x875 = addcarryx_u32(x872, x825, x840);
 uint32_t x877, uint8_t x878 = addcarryx_u32(x875, x828, x841);
 uint8_t x879 = (x878 + x829);
 uint32_t x881, uint32_t x882 = mulx_u32(x16, x19);
 uint32_t x884, uint32_t x885 = mulx_u32(x16, x21);
 uint32_t x887, uint32_t x888 = mulx_u32(x16, x23);
 uint32_t x890, uint32_t x891 = mulx_u32(x16, x25);
 uint32_t x893, uint32_t x894 = mulx_u32(x16, x27);
 uint32_t x896, uint32_t x897 = mulx_u32(x16, x29);
 uint32_t x899, uint32_t x900 = mulx_u32(x16, x31);
 uint32_t x902, uint32_t x903 = mulx_u32(x16, x30);
 uint32_t x905, uint8_t x906 = addcarryx_u32(0x0, x882, x884);
 uint32_t x908, uint8_t x909 = addcarryx_u32(x906, x885, x887);
 uint32_t x911, uint8_t x912 = addcarryx_u32(x909, x888, x890);
 uint32_t x914, uint8_t x915 = addcarryx_u32(x912, x891, x893);
 uint32_t x917, uint8_t x918 = addcarryx_u32(x915, x894, x896);
 uint32_t x920, uint8_t x921 = addcarryx_u32(x918, x897, x899);
 uint32_t x923, uint8_t x924 = addcarryx_u32(x921, x900, x902);
 uint32_t x926, uint8_t _ = addcarryx_u32(0x0, x924, x903);
 uint32_t x929, uint8_t x930 = addcarryx_u32(0x0, x856, x881);
 uint32_t x932, uint8_t x933 = addcarryx_u32(x930, x859, x905);
 uint32_t x935, uint8_t x936 = addcarryx_u32(x933, x862, x908);
 uint32_t x938, uint8_t x939 = addcarryx_u32(x936, x865, x911);
 uint32_t x941, uint8_t x942 = addcarryx_u32(x939, x868, x914);
 uint32_t x944, uint8_t x945 = addcarryx_u32(x942, x871, x917);
 uint32_t x947, uint8_t x948 = addcarryx_u32(x945, x874, x920);
 uint32_t x950, uint8_t x951 = addcarryx_u32(x948, x877, x923);
 uint32_t x953, uint8_t x954 = addcarryx_u32(x951, x879, x926);
 uint32_t x956, uint32_t x957 = mulx_u32(x929, 0xffffffff);
 uint32_t x959, uint32_t x960 = mulx_u32(x929, 0xffffffff);
 uint32_t x962, uint32_t x963 = mulx_u32(x929, 0xffffffff);
 uint32_t x965, uint32_t x966 = mulx_u32(x929, 0xffffffff);
 uint32_t x968, uint8_t x969 = addcarryx_u32(0x0, x957, x959);
 uint32_t x971, uint8_t x972 = addcarryx_u32(x969, x960, x962);
 uint32_t x974, uint8_t x975 = addcarryx_u32(x972, x963, 0x0);
 uint8_t x976 = (0x0 + 0x0);
 uint32_t _, uint8_t x979 = addcarryx_u32(0x0, x929, x956);
 uint32_t x981, uint8_t x982 = addcarryx_u32(x979, x932, x968);
 uint32_t x984, uint8_t x985 = addcarryx_u32(x982, x935, x971);
 uint32_t x987, uint8_t x988 = addcarryx_u32(x985, x938, x974);
 uint32_t x990, uint8_t x991 = addcarryx_u32(x988, x941, x975);
 uint32_t x993, uint8_t x994 = addcarryx_u32(x991, x944, x976);
 uint32_t x996, uint8_t x997 = addcarryx_u32(x994, x947, x929);
 uint32_t x999, uint8_t x1000 = addcarryx_u32(x997, x950, x965);
 uint32_t x1002, uint8_t x1003 = addcarryx_u32(x1000, x953, x966);
 uint8_t x1004 = (x1003 + x954);
 uint32_t x1006, uint8_t x1007 = subborrow_u32(0x0, x981, 0xffffffff);
 uint32_t x1009, uint8_t x1010 = subborrow_u32(x1007, x984, 0xffffffff);
 uint32_t x1012, uint8_t x1013 = subborrow_u32(x1010, x987, 0xffffffff);
 uint32_t x1015, uint8_t x1016 = subborrow_u32(x1013, x990, 0x0);
 uint32_t x1018, uint8_t x1019 = subborrow_u32(x1016, x993, 0x0);
 uint32_t x1021, uint8_t x1022 = subborrow_u32(x1019, x996, 0x0);
 uint32_t x1024, uint8_t x1025 = subborrow_u32(x1022, x999, 0x1);
 uint32_t x1027, uint8_t x1028 = subborrow_u32(x1025, x1002, 0xffffffff);
 uint32_t _, uint8_t x1031 = subborrow_u32(x1028, x1004, 0x0);
 uint32_t x1032 = cmovznz32(x1031, x1027, x1002);
 uint32_t x1033 = cmovznz32(x1031, x1024, x999);
 uint32_t x1034 = cmovznz32(x1031, x1021, x996);
 uint32_t x1035 = cmovznz32(x1031, x1018, x993);
 uint32_t x1036 = cmovznz32(x1031, x1015, x990);
 uint32_t x1037 = cmovznz32(x1031, x1012, x987);
 uint32_t x1038 = cmovznz32(x1031, x1009, x984);
 uint32_t x1039 = cmovznz32(x1031, x1006, x981);
 return (x1032, x1033, x1034, x1035, x1036, x1037, x1038, x1039))
(x, x0)%core
     : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)