λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32, Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, uint32_t x29, uint32_t x30 = mulx_u32(x5, x17); uint32_t x32, uint32_t x33 = mulx_u32(x5, x19); uint32_t x35, uint32_t x36 = mulx_u32(x5, x21); uint32_t x38, uint32_t x39 = mulx_u32(x5, x23); uint32_t x41, uint32_t x42 = mulx_u32(x5, x25); uint32_t x44, uint32_t x45 = mulx_u32(x5, x27); uint32_t x47, uint32_t x48 = mulx_u32(x5, x26); uint32_t x50, uint8_t x51 = addcarryx_u32(0x0, x30, x32); uint32_t x53, uint8_t x54 = addcarryx_u32(x51, x33, x35); uint32_t x56, uint8_t x57 = addcarryx_u32(x54, x36, x38); uint32_t x59, uint8_t x60 = addcarryx_u32(x57, x39, x41); uint32_t x62, uint8_t x63 = addcarryx_u32(x60, x42, x44); uint32_t x65, uint8_t x66 = addcarryx_u32(x63, x45, x47); uint32_t x68, uint8_t _ = addcarryx_u32(0x0, x66, x48); uint32_t x71, uint32_t _ = mulx_u32(x29, 0xdcfdcfdd); uint32_t x74, uint32_t x75 = mulx_u32(x71, 0xffffff8b); uint32_t x77, uint32_t x78 = mulx_u32(x71, 0xffffffff); uint32_t x80, uint32_t x81 = mulx_u32(x71, 0xffffffff); uint32_t x83, uint32_t x84 = mulx_u32(x71, 0xffffffff); uint32_t x86, uint32_t x87 = mulx_u32(x71, 0xffffffff); uint32_t x89, uint32_t x90 = mulx_u32(x71, 0xffffffff); uint32_t x92, uint32_t x93 = mulx_u32(x71, 0x3fffffff); uint32_t x95, uint8_t x96 = addcarryx_u32(0x0, x75, x77); uint32_t x98, uint8_t x99 = addcarryx_u32(x96, x78, x80); uint32_t x101, uint8_t x102 = addcarryx_u32(x99, x81, x83); uint32_t x104, uint8_t x105 = addcarryx_u32(x102, x84, x86); uint32_t x107, uint8_t x108 = addcarryx_u32(x105, x87, x89); uint32_t x110, uint8_t x111 = addcarryx_u32(x108, x90, x92); uint32_t x113, uint8_t _ = addcarryx_u32(0x0, x111, x93); uint32_t _, uint8_t x117 = addcarryx_u32(0x0, x29, x74); uint32_t x119, uint8_t x120 = addcarryx_u32(x117, x50, x95); uint32_t x122, uint8_t x123 = addcarryx_u32(x120, x53, x98); uint32_t x125, uint8_t x126 = addcarryx_u32(x123, x56, x101); uint32_t x128, uint8_t x129 = addcarryx_u32(x126, x59, x104); uint32_t x131, uint8_t x132 = addcarryx_u32(x129, x62, x107); uint32_t x134, uint8_t x135 = addcarryx_u32(x132, x65, x110); uint32_t x137, uint8_t x138 = addcarryx_u32(x135, x68, x113); uint32_t x140, uint32_t x141 = mulx_u32(x7, x17); uint32_t x143, uint32_t x144 = mulx_u32(x7, x19); uint32_t x146, uint32_t x147 = mulx_u32(x7, x21); uint32_t x149, uint32_t x150 = mulx_u32(x7, x23); uint32_t x152, uint32_t x153 = mulx_u32(x7, x25); uint32_t x155, uint32_t x156 = mulx_u32(x7, x27); uint32_t x158, uint32_t x159 = mulx_u32(x7, x26); uint32_t x161, uint8_t x162 = addcarryx_u32(0x0, x141, x143); uint32_t x164, uint8_t x165 = addcarryx_u32(x162, x144, x146); uint32_t x167, uint8_t x168 = addcarryx_u32(x165, x147, x149); uint32_t x170, uint8_t x171 = addcarryx_u32(x168, x150, x152); uint32_t x173, uint8_t x174 = addcarryx_u32(x171, x153, x155); uint32_t x176, uint8_t x177 = addcarryx_u32(x174, x156, x158); uint32_t x179, uint8_t _ = addcarryx_u32(0x0, x177, x159); uint32_t x182, uint8_t x183 = addcarryx_u32(0x0, x119, x140); uint32_t x185, uint8_t x186 = addcarryx_u32(x183, x122, x161); uint32_t x188, uint8_t x189 = addcarryx_u32(x186, x125, x164); uint32_t x191, uint8_t x192 = addcarryx_u32(x189, x128, x167); uint32_t x194, uint8_t x195 = addcarryx_u32(x192, x131, x170); uint32_t x197, uint8_t x198 = addcarryx_u32(x195, x134, x173); uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x137, x176); uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x138, x179); uint32_t x206, uint32_t _ = mulx_u32(x182, 0xdcfdcfdd); uint32_t x209, uint32_t x210 = mulx_u32(x206, 0xffffff8b); uint32_t x212, uint32_t x213 = mulx_u32(x206, 0xffffffff); uint32_t x215, uint32_t x216 = mulx_u32(x206, 0xffffffff); uint32_t x218, uint32_t x219 = mulx_u32(x206, 0xffffffff); uint32_t x221, uint32_t x222 = mulx_u32(x206, 0xffffffff); uint32_t x224, uint32_t x225 = mulx_u32(x206, 0xffffffff); uint32_t x227, uint32_t x228 = mulx_u32(x206, 0x3fffffff); uint32_t x230, uint8_t x231 = addcarryx_u32(0x0, x210, x212); uint32_t x233, uint8_t x234 = addcarryx_u32(x231, x213, x215); uint32_t x236, uint8_t x237 = addcarryx_u32(x234, x216, x218); uint32_t x239, uint8_t x240 = addcarryx_u32(x237, x219, x221); uint32_t x242, uint8_t x243 = addcarryx_u32(x240, x222, x224); uint32_t x245, uint8_t x246 = addcarryx_u32(x243, x225, x227); uint32_t x248, uint8_t _ = addcarryx_u32(0x0, x246, x228); uint32_t _, uint8_t x252 = addcarryx_u32(0x0, x182, x209); uint32_t x254, uint8_t x255 = addcarryx_u32(x252, x185, x230); uint32_t x257, uint8_t x258 = addcarryx_u32(x255, x188, x233); uint32_t x260, uint8_t x261 = addcarryx_u32(x258, x191, x236); uint32_t x263, uint8_t x264 = addcarryx_u32(x261, x194, x239); uint32_t x266, uint8_t x267 = addcarryx_u32(x264, x197, x242); uint32_t x269, uint8_t x270 = addcarryx_u32(x267, x200, x245); uint32_t x272, uint8_t x273 = addcarryx_u32(x270, x203, x248); uint8_t x274 = (x273 + x204); uint32_t x276, uint32_t x277 = mulx_u32(x9, x17); uint32_t x279, uint32_t x280 = mulx_u32(x9, x19); uint32_t x282, uint32_t x283 = mulx_u32(x9, x21); uint32_t x285, uint32_t x286 = mulx_u32(x9, x23); uint32_t x288, uint32_t x289 = mulx_u32(x9, x25); uint32_t x291, uint32_t x292 = mulx_u32(x9, x27); uint32_t x294, uint32_t x295 = mulx_u32(x9, x26); uint32_t x297, uint8_t x298 = addcarryx_u32(0x0, x277, x279); uint32_t x300, uint8_t x301 = addcarryx_u32(x298, x280, x282); uint32_t x303, uint8_t x304 = addcarryx_u32(x301, x283, x285); uint32_t x306, uint8_t x307 = addcarryx_u32(x304, x286, x288); uint32_t x309, uint8_t x310 = addcarryx_u32(x307, x289, x291); uint32_t x312, uint8_t x313 = addcarryx_u32(x310, x292, x294); uint32_t x315, uint8_t _ = addcarryx_u32(0x0, x313, x295); uint32_t x318, uint8_t x319 = addcarryx_u32(0x0, x254, x276); uint32_t x321, uint8_t x322 = addcarryx_u32(x319, x257, x297); uint32_t x324, uint8_t x325 = addcarryx_u32(x322, x260, x300); uint32_t x327, uint8_t x328 = addcarryx_u32(x325, x263, x303); uint32_t x330, uint8_t x331 = addcarryx_u32(x328, x266, x306); uint32_t x333, uint8_t x334 = addcarryx_u32(x331, x269, x309); uint32_t x336, uint8_t x337 = addcarryx_u32(x334, x272, x312); uint32_t x339, uint8_t x340 = addcarryx_u32(x337, x274, x315); uint32_t x342, uint32_t _ = mulx_u32(x318, 0xdcfdcfdd); uint32_t x345, uint32_t x346 = mulx_u32(x342, 0xffffff8b); uint32_t x348, uint32_t x349 = mulx_u32(x342, 0xffffffff); uint32_t x351, uint32_t x352 = mulx_u32(x342, 0xffffffff); uint32_t x354, uint32_t x355 = mulx_u32(x342, 0xffffffff); uint32_t x357, uint32_t x358 = mulx_u32(x342, 0xffffffff); uint32_t x360, uint32_t x361 = mulx_u32(x342, 0xffffffff); uint32_t x363, uint32_t x364 = mulx_u32(x342, 0x3fffffff); uint32_t x366, uint8_t x367 = addcarryx_u32(0x0, x346, x348); uint32_t x369, uint8_t x370 = addcarryx_u32(x367, x349, x351); uint32_t x372, uint8_t x373 = addcarryx_u32(x370, x352, x354); uint32_t x375, uint8_t x376 = addcarryx_u32(x373, x355, x357); uint32_t x378, uint8_t x379 = addcarryx_u32(x376, x358, x360); uint32_t x381, uint8_t x382 = addcarryx_u32(x379, x361, x363); uint32_t x384, uint8_t _ = addcarryx_u32(0x0, x382, x364); uint32_t _, uint8_t x388 = addcarryx_u32(0x0, x318, x345); uint32_t x390, uint8_t x391 = addcarryx_u32(x388, x321, x366); uint32_t x393, uint8_t x394 = addcarryx_u32(x391, x324, x369); uint32_t x396, uint8_t x397 = addcarryx_u32(x394, x327, x372); uint32_t x399, uint8_t x400 = addcarryx_u32(x397, x330, x375); uint32_t x402, uint8_t x403 = addcarryx_u32(x400, x333, x378); uint32_t x405, uint8_t x406 = addcarryx_u32(x403, x336, x381); uint32_t x408, uint8_t x409 = addcarryx_u32(x406, x339, x384); uint8_t x410 = (x409 + x340); uint32_t x412, uint32_t x413 = mulx_u32(x11, x17); uint32_t x415, uint32_t x416 = mulx_u32(x11, x19); uint32_t x418, uint32_t x419 = mulx_u32(x11, x21); uint32_t x421, uint32_t x422 = mulx_u32(x11, x23); uint32_t x424, uint32_t x425 = mulx_u32(x11, x25); uint32_t x427, uint32_t x428 = mulx_u32(x11, x27); uint32_t x430, uint32_t x431 = mulx_u32(x11, x26); uint32_t x433, uint8_t x434 = addcarryx_u32(0x0, x413, x415); uint32_t x436, uint8_t x437 = addcarryx_u32(x434, x416, x418); uint32_t x439, uint8_t x440 = addcarryx_u32(x437, x419, x421); uint32_t x442, uint8_t x443 = addcarryx_u32(x440, x422, x424); uint32_t x445, uint8_t x446 = addcarryx_u32(x443, x425, x427); uint32_t x448, uint8_t x449 = addcarryx_u32(x446, x428, x430); uint32_t x451, uint8_t _ = addcarryx_u32(0x0, x449, x431); uint32_t x454, uint8_t x455 = addcarryx_u32(0x0, x390, x412); uint32_t x457, uint8_t x458 = addcarryx_u32(x455, x393, x433); uint32_t x460, uint8_t x461 = addcarryx_u32(x458, x396, x436); uint32_t x463, uint8_t x464 = addcarryx_u32(x461, x399, x439); uint32_t x466, uint8_t x467 = addcarryx_u32(x464, x402, x442); uint32_t x469, uint8_t x470 = addcarryx_u32(x467, x405, x445); uint32_t x472, uint8_t x473 = addcarryx_u32(x470, x408, x448); uint32_t x475, uint8_t x476 = addcarryx_u32(x473, x410, x451); uint32_t x478, uint32_t _ = mulx_u32(x454, 0xdcfdcfdd); uint32_t x481, uint32_t x482 = mulx_u32(x478, 0xffffff8b); uint32_t x484, uint32_t x485 = mulx_u32(x478, 0xffffffff); uint32_t x487, uint32_t x488 = mulx_u32(x478, 0xffffffff); uint32_t x490, uint32_t x491 = mulx_u32(x478, 0xffffffff); uint32_t x493, uint32_t x494 = mulx_u32(x478, 0xffffffff); uint32_t x496, uint32_t x497 = mulx_u32(x478, 0xffffffff); uint32_t x499, uint32_t x500 = mulx_u32(x478, 0x3fffffff); uint32_t x502, uint8_t x503 = addcarryx_u32(0x0, x482, x484); uint32_t x505, uint8_t x506 = addcarryx_u32(x503, x485, x487); uint32_t x508, uint8_t x509 = addcarryx_u32(x506, x488, x490); uint32_t x511, uint8_t x512 = addcarryx_u32(x509, x491, x493); uint32_t x514, uint8_t x515 = addcarryx_u32(x512, x494, x496); uint32_t x517, uint8_t x518 = addcarryx_u32(x515, x497, x499); uint32_t x520, uint8_t _ = addcarryx_u32(0x0, x518, x500); uint32_t _, uint8_t x524 = addcarryx_u32(0x0, x454, x481); uint32_t x526, uint8_t x527 = addcarryx_u32(x524, x457, x502); uint32_t x529, uint8_t x530 = addcarryx_u32(x527, x460, x505); uint32_t x532, uint8_t x533 = addcarryx_u32(x530, x463, x508); uint32_t x535, uint8_t x536 = addcarryx_u32(x533, x466, x511); uint32_t x538, uint8_t x539 = addcarryx_u32(x536, x469, x514); uint32_t x541, uint8_t x542 = addcarryx_u32(x539, x472, x517); uint32_t x544, uint8_t x545 = addcarryx_u32(x542, x475, x520); uint8_t x546 = (x545 + x476); uint32_t x548, uint32_t x549 = mulx_u32(x13, x17); uint32_t x551, uint32_t x552 = mulx_u32(x13, x19); uint32_t x554, uint32_t x555 = mulx_u32(x13, x21); uint32_t x557, uint32_t x558 = mulx_u32(x13, x23); uint32_t x560, uint32_t x561 = mulx_u32(x13, x25); uint32_t x563, uint32_t x564 = mulx_u32(x13, x27); uint32_t x566, uint32_t x567 = mulx_u32(x13, x26); uint32_t x569, uint8_t x570 = addcarryx_u32(0x0, x549, x551); uint32_t x572, uint8_t x573 = addcarryx_u32(x570, x552, x554); uint32_t x575, uint8_t x576 = addcarryx_u32(x573, x555, x557); uint32_t x578, uint8_t x579 = addcarryx_u32(x576, x558, x560); uint32_t x581, uint8_t x582 = addcarryx_u32(x579, x561, x563); uint32_t x584, uint8_t x585 = addcarryx_u32(x582, x564, x566); uint32_t x587, uint8_t _ = addcarryx_u32(0x0, x585, x567); uint32_t x590, uint8_t x591 = addcarryx_u32(0x0, x526, x548); uint32_t x593, uint8_t x594 = addcarryx_u32(x591, x529, x569); uint32_t x596, uint8_t x597 = addcarryx_u32(x594, x532, x572); uint32_t x599, uint8_t x600 = addcarryx_u32(x597, x535, x575); uint32_t x602, uint8_t x603 = addcarryx_u32(x600, x538, x578); uint32_t x605, uint8_t x606 = addcarryx_u32(x603, x541, x581); uint32_t x608, uint8_t x609 = addcarryx_u32(x606, x544, x584); uint32_t x611, uint8_t x612 = addcarryx_u32(x609, x546, x587); uint32_t x614, uint32_t _ = mulx_u32(x590, 0xdcfdcfdd); uint32_t x617, uint32_t x618 = mulx_u32(x614, 0xffffff8b); uint32_t x620, uint32_t x621 = mulx_u32(x614, 0xffffffff); uint32_t x623, uint32_t x624 = mulx_u32(x614, 0xffffffff); uint32_t x626, uint32_t x627 = mulx_u32(x614, 0xffffffff); uint32_t x629, uint32_t x630 = mulx_u32(x614, 0xffffffff); uint32_t x632, uint32_t x633 = mulx_u32(x614, 0xffffffff); uint32_t x635, uint32_t x636 = mulx_u32(x614, 0x3fffffff); uint32_t x638, uint8_t x639 = addcarryx_u32(0x0, x618, x620); uint32_t x641, uint8_t x642 = addcarryx_u32(x639, x621, x623); uint32_t x644, uint8_t x645 = addcarryx_u32(x642, x624, x626); uint32_t x647, uint8_t x648 = addcarryx_u32(x645, x627, x629); uint32_t x650, uint8_t x651 = addcarryx_u32(x648, x630, x632); uint32_t x653, uint8_t x654 = addcarryx_u32(x651, x633, x635); uint32_t x656, uint8_t _ = addcarryx_u32(0x0, x654, x636); uint32_t _, uint8_t x660 = addcarryx_u32(0x0, x590, x617); uint32_t x662, uint8_t x663 = addcarryx_u32(x660, x593, x638); uint32_t x665, uint8_t x666 = addcarryx_u32(x663, x596, x641); uint32_t x668, uint8_t x669 = addcarryx_u32(x666, x599, x644); uint32_t x671, uint8_t x672 = addcarryx_u32(x669, x602, x647); uint32_t x674, uint8_t x675 = addcarryx_u32(x672, x605, x650); uint32_t x677, uint8_t x678 = addcarryx_u32(x675, x608, x653); uint32_t x680, uint8_t x681 = addcarryx_u32(x678, x611, x656); uint8_t x682 = (x681 + x612); uint32_t x684, uint32_t x685 = mulx_u32(x15, x17); uint32_t x687, uint32_t x688 = mulx_u32(x15, x19); uint32_t x690, uint32_t x691 = mulx_u32(x15, x21); uint32_t x693, uint32_t x694 = mulx_u32(x15, x23); uint32_t x696, uint32_t x697 = mulx_u32(x15, x25); uint32_t x699, uint32_t x700 = mulx_u32(x15, x27); uint32_t x702, uint32_t x703 = mulx_u32(x15, x26); uint32_t x705, uint8_t x706 = addcarryx_u32(0x0, x685, x687); uint32_t x708, uint8_t x709 = addcarryx_u32(x706, x688, x690); uint32_t x711, uint8_t x712 = addcarryx_u32(x709, x691, x693); uint32_t x714, uint8_t x715 = addcarryx_u32(x712, x694, x696); uint32_t x717, uint8_t x718 = addcarryx_u32(x715, x697, x699); uint32_t x720, uint8_t x721 = addcarryx_u32(x718, x700, x702); uint32_t x723, uint8_t _ = addcarryx_u32(0x0, x721, x703); uint32_t x726, uint8_t x727 = addcarryx_u32(0x0, x662, x684); uint32_t x729, uint8_t x730 = addcarryx_u32(x727, x665, x705); uint32_t x732, uint8_t x733 = addcarryx_u32(x730, x668, x708); uint32_t x735, uint8_t x736 = addcarryx_u32(x733, x671, x711); uint32_t x738, uint8_t x739 = addcarryx_u32(x736, x674, x714); uint32_t x741, uint8_t x742 = addcarryx_u32(x739, x677, x717); uint32_t x744, uint8_t x745 = addcarryx_u32(x742, x680, x720); uint32_t x747, uint8_t x748 = addcarryx_u32(x745, x682, x723); uint32_t x750, uint32_t _ = mulx_u32(x726, 0xdcfdcfdd); uint32_t x753, uint32_t x754 = mulx_u32(x750, 0xffffff8b); uint32_t x756, uint32_t x757 = mulx_u32(x750, 0xffffffff); uint32_t x759, uint32_t x760 = mulx_u32(x750, 0xffffffff); uint32_t x762, uint32_t x763 = mulx_u32(x750, 0xffffffff); uint32_t x765, uint32_t x766 = mulx_u32(x750, 0xffffffff); uint32_t x768, uint32_t x769 = mulx_u32(x750, 0xffffffff); uint32_t x771, uint32_t x772 = mulx_u32(x750, 0x3fffffff); uint32_t x774, uint8_t x775 = addcarryx_u32(0x0, x754, x756); uint32_t x777, uint8_t x778 = addcarryx_u32(x775, x757, x759); uint32_t x780, uint8_t x781 = addcarryx_u32(x778, x760, x762); uint32_t x783, uint8_t x784 = addcarryx_u32(x781, x763, x765); uint32_t x786, uint8_t x787 = addcarryx_u32(x784, x766, x768); uint32_t x789, uint8_t x790 = addcarryx_u32(x787, x769, x771); uint32_t x792, uint8_t _ = addcarryx_u32(0x0, x790, x772); uint32_t _, uint8_t x796 = addcarryx_u32(0x0, x726, x753); uint32_t x798, uint8_t x799 = addcarryx_u32(x796, x729, x774); uint32_t x801, uint8_t x802 = addcarryx_u32(x799, x732, x777); uint32_t x804, uint8_t x805 = addcarryx_u32(x802, x735, x780); uint32_t x807, uint8_t x808 = addcarryx_u32(x805, x738, x783); uint32_t x810, uint8_t x811 = addcarryx_u32(x808, x741, x786); uint32_t x813, uint8_t x814 = addcarryx_u32(x811, x744, x789); uint32_t x816, uint8_t x817 = addcarryx_u32(x814, x747, x792); uint8_t x818 = (x817 + x748); uint32_t x820, uint32_t x821 = mulx_u32(x14, x17); uint32_t x823, uint32_t x824 = mulx_u32(x14, x19); uint32_t x826, uint32_t x827 = mulx_u32(x14, x21); uint32_t x829, uint32_t x830 = mulx_u32(x14, x23); uint32_t x832, uint32_t x833 = mulx_u32(x14, x25); uint32_t x835, uint32_t x836 = mulx_u32(x14, x27); uint32_t x838, uint32_t x839 = mulx_u32(x14, x26); uint32_t x841, uint8_t x842 = addcarryx_u32(0x0, x821, x823); uint32_t x844, uint8_t x845 = addcarryx_u32(x842, x824, x826); uint32_t x847, uint8_t x848 = addcarryx_u32(x845, x827, x829); uint32_t x850, uint8_t x851 = addcarryx_u32(x848, x830, x832); uint32_t x853, uint8_t x854 = addcarryx_u32(x851, x833, x835); uint32_t x856, uint8_t x857 = addcarryx_u32(x854, x836, x838); uint32_t x859, uint8_t _ = addcarryx_u32(0x0, x857, x839); uint32_t x862, uint8_t x863 = addcarryx_u32(0x0, x798, x820); uint32_t x865, uint8_t x866 = addcarryx_u32(x863, x801, x841); uint32_t x868, uint8_t x869 = addcarryx_u32(x866, x804, x844); uint32_t x871, uint8_t x872 = addcarryx_u32(x869, x807, x847); uint32_t x874, uint8_t x875 = addcarryx_u32(x872, x810, x850); uint32_t x877, uint8_t x878 = addcarryx_u32(x875, x813, x853); uint32_t x880, uint8_t x881 = addcarryx_u32(x878, x816, x856); uint32_t x883, uint8_t x884 = addcarryx_u32(x881, x818, x859); uint32_t x886, uint32_t _ = mulx_u32(x862, 0xdcfdcfdd); uint32_t x889, uint32_t x890 = mulx_u32(x886, 0xffffff8b); uint32_t x892, uint32_t x893 = mulx_u32(x886, 0xffffffff); uint32_t x895, uint32_t x896 = mulx_u32(x886, 0xffffffff); uint32_t x898, uint32_t x899 = mulx_u32(x886, 0xffffffff); uint32_t x901, uint32_t x902 = mulx_u32(x886, 0xffffffff); uint32_t x904, uint32_t x905 = mulx_u32(x886, 0xffffffff); uint32_t x907, uint32_t x908 = mulx_u32(x886, 0x3fffffff); uint32_t x910, uint8_t x911 = addcarryx_u32(0x0, x890, x892); uint32_t x913, uint8_t x914 = addcarryx_u32(x911, x893, x895); uint32_t x916, uint8_t x917 = addcarryx_u32(x914, x896, x898); uint32_t x919, uint8_t x920 = addcarryx_u32(x917, x899, x901); uint32_t x922, uint8_t x923 = addcarryx_u32(x920, x902, x904); uint32_t x925, uint8_t x926 = addcarryx_u32(x923, x905, x907); uint32_t x928, uint8_t _ = addcarryx_u32(0x0, x926, x908); uint32_t _, uint8_t x932 = addcarryx_u32(0x0, x862, x889); uint32_t x934, uint8_t x935 = addcarryx_u32(x932, x865, x910); uint32_t x937, uint8_t x938 = addcarryx_u32(x935, x868, x913); uint32_t x940, uint8_t x941 = addcarryx_u32(x938, x871, x916); uint32_t x943, uint8_t x944 = addcarryx_u32(x941, x874, x919); uint32_t x946, uint8_t x947 = addcarryx_u32(x944, x877, x922); uint32_t x949, uint8_t x950 = addcarryx_u32(x947, x880, x925); uint32_t x952, uint8_t x953 = addcarryx_u32(x950, x883, x928); uint8_t x954 = (x953 + x884); uint32_t x956, uint8_t x957 = subborrow_u32(0x0, x934, 0xffffff8b); uint32_t x959, uint8_t x960 = subborrow_u32(x957, x937, 0xffffffff); uint32_t x962, uint8_t x963 = subborrow_u32(x960, x940, 0xffffffff); uint32_t x965, uint8_t x966 = subborrow_u32(x963, x943, 0xffffffff); uint32_t x968, uint8_t x969 = subborrow_u32(x966, x946, 0xffffffff); uint32_t x971, uint8_t x972 = subborrow_u32(x969, x949, 0xffffffff); uint32_t x974, uint8_t x975 = subborrow_u32(x972, x952, 0x3fffffff); uint32_t _, uint8_t x978 = subborrow_u32(x975, x954, 0x0); uint32_t x979 = cmovznz(x978, x974, x952); uint32_t x980 = cmovznz(x978, x971, x949); uint32_t x981 = cmovznz(x978, x968, x946); uint32_t x982 = cmovznz(x978, x965, x943); uint32_t x983 = cmovznz(x978, x962, x940); uint32_t x984 = cmovznz(x978, x959, x937); uint32_t x985 = cmovznz(x978, x956, x934); return (x979, x980, x981, x982, x983, x984, x985)) (x, x0)%core : 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)