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

λ x x0 : word64 * word64 * word64 * word64 * word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
 λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
 uint64_t x25, uint64_t x26 = mulx_u64(x5, x15);
 uint64_t x28, uint64_t x29 = mulx_u64(x5, x17);
 uint64_t x31, uint64_t x32 = mulx_u64(x5, x19);
 uint64_t x34, uint64_t x35 = mulx_u64(x5, x21);
 uint64_t x37, uint64_t x38 = mulx_u64(x5, x23);
 uint64_t x40, uint64_t x41 = mulx_u64(x5, x22);
 uint64_t x43, uint8_t x44 = addcarryx_u64(0x0, x26, x28);
 uint64_t x46, uint8_t x47 = addcarryx_u64(x44, x29, x31);
 uint64_t x49, uint8_t x50 = addcarryx_u64(x47, x32, x34);
 uint64_t x52, uint8_t x53 = addcarryx_u64(x50, x35, x37);
 uint64_t x55, uint8_t x56 = addcarryx_u64(x53, x38, x40);
 uint64_t x58, uint8_t _ = addcarryx_u64(0x0, x56, x41);
 uint64_t x61, uint64_t x62 = mulx_u64(x25, 0xffffffffffffffffL);
 uint64_t x64, uint64_t x65 = mulx_u64(x25, 0xffffffffffffffffL);
 uint64_t x67, uint64_t x68 = mulx_u64(x25, 0xfffffffdffffffffL);
 uint64_t x70, uint64_t x71 = mulx_u64(x25, 0xffffffffffffffffL);
 uint64_t x73, uint64_t x74 = mulx_u64(x25, 0xffffffffffffffffL);
 uint64_t x76, uint8_t x77 = mulx_u64_out_u8(x25, 0x3);
 uint64_t x79, uint8_t x80 = addcarryx_u64(0x0, x62, x64);
 uint64_t x82, uint8_t x83 = addcarryx_u64(x80, x65, x67);
 uint64_t x85, uint8_t x86 = addcarryx_u64(x83, x68, x70);
 uint64_t x88, uint8_t x89 = addcarryx_u64(x86, x71, x73);
 uint64_t x91, uint8_t x92 = addcarryx_u64(x89, x74, x76);
 uint8_t x93 = (x92 + x77);
 uint64_t _, uint8_t x96 = addcarryx_u64(0x0, x25, x61);
 uint64_t x98, uint8_t x99 = addcarryx_u64(x96, x43, x79);
 uint64_t x101, uint8_t x102 = addcarryx_u64(x99, x46, x82);
 uint64_t x104, uint8_t x105 = addcarryx_u64(x102, x49, x85);
 uint64_t x107, uint8_t x108 = addcarryx_u64(x105, x52, x88);
 uint64_t x110, uint8_t x111 = addcarryx_u64(x108, x55, x91);
 uint64_t x113, uint8_t x114 = addcarryx_u64(x111, x58, x93);
 uint64_t x116, uint64_t x117 = mulx_u64(x7, x15);
 uint64_t x119, uint64_t x120 = mulx_u64(x7, x17);
 uint64_t x122, uint64_t x123 = mulx_u64(x7, x19);
 uint64_t x125, uint64_t x126 = mulx_u64(x7, x21);
 uint64_t x128, uint64_t x129 = mulx_u64(x7, x23);
 uint64_t x131, uint64_t x132 = mulx_u64(x7, x22);
 uint64_t x134, uint8_t x135 = addcarryx_u64(0x0, x117, x119);
 uint64_t x137, uint8_t x138 = addcarryx_u64(x135, x120, x122);
 uint64_t x140, uint8_t x141 = addcarryx_u64(x138, x123, x125);
 uint64_t x143, uint8_t x144 = addcarryx_u64(x141, x126, x128);
 uint64_t x146, uint8_t x147 = addcarryx_u64(x144, x129, x131);
 uint64_t x149, uint8_t _ = addcarryx_u64(0x0, x147, x132);
 uint64_t x152, uint8_t x153 = addcarryx_u64(0x0, x98, x116);
 uint64_t x155, uint8_t x156 = addcarryx_u64(x153, x101, x134);
 uint64_t x158, uint8_t x159 = addcarryx_u64(x156, x104, x137);
 uint64_t x161, uint8_t x162 = addcarryx_u64(x159, x107, x140);
 uint64_t x164, uint8_t x165 = addcarryx_u64(x162, x110, x143);
 uint64_t x167, uint8_t x168 = addcarryx_u64(x165, x113, x146);
 uint64_t x170, uint8_t x171 = addcarryx_u64(x168, x114, x149);
 uint64_t x173, uint64_t x174 = mulx_u64(x152, 0xffffffffffffffffL);
 uint64_t x176, uint64_t x177 = mulx_u64(x152, 0xffffffffffffffffL);
 uint64_t x179, uint64_t x180 = mulx_u64(x152, 0xfffffffdffffffffL);
 uint64_t x182, uint64_t x183 = mulx_u64(x152, 0xffffffffffffffffL);
 uint64_t x185, uint64_t x186 = mulx_u64(x152, 0xffffffffffffffffL);
 uint64_t x188, uint8_t x189 = mulx_u64_out_u8(x152, 0x3);
 uint64_t x191, uint8_t x192 = addcarryx_u64(0x0, x174, x176);
 uint64_t x194, uint8_t x195 = addcarryx_u64(x192, x177, x179);
 uint64_t x197, uint8_t x198 = addcarryx_u64(x195, x180, x182);
 uint64_t x200, uint8_t x201 = addcarryx_u64(x198, x183, x185);
 uint64_t x203, uint8_t x204 = addcarryx_u64(x201, x186, x188);
 uint8_t x205 = (x204 + x189);
 uint64_t _, uint8_t x208 = addcarryx_u64(0x0, x152, x173);
 uint64_t x210, uint8_t x211 = addcarryx_u64(x208, x155, x191);
 uint64_t x213, uint8_t x214 = addcarryx_u64(x211, x158, x194);
 uint64_t x216, uint8_t x217 = addcarryx_u64(x214, x161, x197);
 uint64_t x219, uint8_t x220 = addcarryx_u64(x217, x164, x200);
 uint64_t x222, uint8_t x223 = addcarryx_u64(x220, x167, x203);
 uint64_t x225, uint8_t x226 = addcarryx_u64(x223, x170, x205);
 uint8_t x227 = (x226 + x171);
 uint64_t x229, uint64_t x230 = mulx_u64(x9, x15);
 uint64_t x232, uint64_t x233 = mulx_u64(x9, x17);
 uint64_t x235, uint64_t x236 = mulx_u64(x9, x19);
 uint64_t x238, uint64_t x239 = mulx_u64(x9, x21);
 uint64_t x241, uint64_t x242 = mulx_u64(x9, x23);
 uint64_t x244, uint64_t x245 = mulx_u64(x9, x22);
 uint64_t x247, uint8_t x248 = addcarryx_u64(0x0, x230, x232);
 uint64_t x250, uint8_t x251 = addcarryx_u64(x248, x233, x235);
 uint64_t x253, uint8_t x254 = addcarryx_u64(x251, x236, x238);
 uint64_t x256, uint8_t x257 = addcarryx_u64(x254, x239, x241);
 uint64_t x259, uint8_t x260 = addcarryx_u64(x257, x242, x244);
 uint64_t x262, uint8_t _ = addcarryx_u64(0x0, x260, x245);
 uint64_t x265, uint8_t x266 = addcarryx_u64(0x0, x210, x229);
 uint64_t x268, uint8_t x269 = addcarryx_u64(x266, x213, x247);
 uint64_t x271, uint8_t x272 = addcarryx_u64(x269, x216, x250);
 uint64_t x274, uint8_t x275 = addcarryx_u64(x272, x219, x253);
 uint64_t x277, uint8_t x278 = addcarryx_u64(x275, x222, x256);
 uint64_t x280, uint8_t x281 = addcarryx_u64(x278, x225, x259);
 uint64_t x283, uint8_t x284 = addcarryx_u64(x281, x227, x262);
 uint64_t x286, uint64_t x287 = mulx_u64(x265, 0xffffffffffffffffL);
 uint64_t x289, uint64_t x290 = mulx_u64(x265, 0xffffffffffffffffL);
 uint64_t x292, uint64_t x293 = mulx_u64(x265, 0xfffffffdffffffffL);
 uint64_t x295, uint64_t x296 = mulx_u64(x265, 0xffffffffffffffffL);
 uint64_t x298, uint64_t x299 = mulx_u64(x265, 0xffffffffffffffffL);
 uint64_t x301, uint8_t x302 = mulx_u64_out_u8(x265, 0x3);
 uint64_t x304, uint8_t x305 = addcarryx_u64(0x0, x287, x289);
 uint64_t x307, uint8_t x308 = addcarryx_u64(x305, x290, x292);
 uint64_t x310, uint8_t x311 = addcarryx_u64(x308, x293, x295);
 uint64_t x313, uint8_t x314 = addcarryx_u64(x311, x296, x298);
 uint64_t x316, uint8_t x317 = addcarryx_u64(x314, x299, x301);
 uint8_t x318 = (x317 + x302);
 uint64_t _, uint8_t x321 = addcarryx_u64(0x0, x265, x286);
 uint64_t x323, uint8_t x324 = addcarryx_u64(x321, x268, x304);
 uint64_t x326, uint8_t x327 = addcarryx_u64(x324, x271, x307);
 uint64_t x329, uint8_t x330 = addcarryx_u64(x327, x274, x310);
 uint64_t x332, uint8_t x333 = addcarryx_u64(x330, x277, x313);
 uint64_t x335, uint8_t x336 = addcarryx_u64(x333, x280, x316);
 uint64_t x338, uint8_t x339 = addcarryx_u64(x336, x283, x318);
 uint8_t x340 = (x339 + x284);
 uint64_t x342, uint64_t x343 = mulx_u64(x11, x15);
 uint64_t x345, uint64_t x346 = mulx_u64(x11, x17);
 uint64_t x348, uint64_t x349 = mulx_u64(x11, x19);
 uint64_t x351, uint64_t x352 = mulx_u64(x11, x21);
 uint64_t x354, uint64_t x355 = mulx_u64(x11, x23);
 uint64_t x357, uint64_t x358 = mulx_u64(x11, x22);
 uint64_t x360, uint8_t x361 = addcarryx_u64(0x0, x343, x345);
 uint64_t x363, uint8_t x364 = addcarryx_u64(x361, x346, x348);
 uint64_t x366, uint8_t x367 = addcarryx_u64(x364, x349, x351);
 uint64_t x369, uint8_t x370 = addcarryx_u64(x367, x352, x354);
 uint64_t x372, uint8_t x373 = addcarryx_u64(x370, x355, x357);
 uint64_t x375, uint8_t _ = addcarryx_u64(0x0, x373, x358);
 uint64_t x378, uint8_t x379 = addcarryx_u64(0x0, x323, x342);
 uint64_t x381, uint8_t x382 = addcarryx_u64(x379, x326, x360);
 uint64_t x384, uint8_t x385 = addcarryx_u64(x382, x329, x363);
 uint64_t x387, uint8_t x388 = addcarryx_u64(x385, x332, x366);
 uint64_t x390, uint8_t x391 = addcarryx_u64(x388, x335, x369);
 uint64_t x393, uint8_t x394 = addcarryx_u64(x391, x338, x372);
 uint64_t x396, uint8_t x397 = addcarryx_u64(x394, x340, x375);
 uint64_t x399, uint64_t x400 = mulx_u64(x378, 0xffffffffffffffffL);
 uint64_t x402, uint64_t x403 = mulx_u64(x378, 0xffffffffffffffffL);
 uint64_t x405, uint64_t x406 = mulx_u64(x378, 0xfffffffdffffffffL);
 uint64_t x408, uint64_t x409 = mulx_u64(x378, 0xffffffffffffffffL);
 uint64_t x411, uint64_t x412 = mulx_u64(x378, 0xffffffffffffffffL);
 uint64_t x414, uint8_t x415 = mulx_u64_out_u8(x378, 0x3);
 uint64_t x417, uint8_t x418 = addcarryx_u64(0x0, x400, x402);
 uint64_t x420, uint8_t x421 = addcarryx_u64(x418, x403, x405);
 uint64_t x423, uint8_t x424 = addcarryx_u64(x421, x406, x408);
 uint64_t x426, uint8_t x427 = addcarryx_u64(x424, x409, x411);
 uint64_t x429, uint8_t x430 = addcarryx_u64(x427, x412, x414);
 uint8_t x431 = (x430 + x415);
 uint64_t _, uint8_t x434 = addcarryx_u64(0x0, x378, x399);
 uint64_t x436, uint8_t x437 = addcarryx_u64(x434, x381, x417);
 uint64_t x439, uint8_t x440 = addcarryx_u64(x437, x384, x420);
 uint64_t x442, uint8_t x443 = addcarryx_u64(x440, x387, x423);
 uint64_t x445, uint8_t x446 = addcarryx_u64(x443, x390, x426);
 uint64_t x448, uint8_t x449 = addcarryx_u64(x446, x393, x429);
 uint64_t x451, uint8_t x452 = addcarryx_u64(x449, x396, x431);
 uint8_t x453 = (x452 + x397);
 uint64_t x455, uint64_t x456 = mulx_u64(x13, x15);
 uint64_t x458, uint64_t x459 = mulx_u64(x13, x17);
 uint64_t x461, uint64_t x462 = mulx_u64(x13, x19);
 uint64_t x464, uint64_t x465 = mulx_u64(x13, x21);
 uint64_t x467, uint64_t x468 = mulx_u64(x13, x23);
 uint64_t x470, uint64_t x471 = mulx_u64(x13, x22);
 uint64_t x473, uint8_t x474 = addcarryx_u64(0x0, x456, x458);
 uint64_t x476, uint8_t x477 = addcarryx_u64(x474, x459, x461);
 uint64_t x479, uint8_t x480 = addcarryx_u64(x477, x462, x464);
 uint64_t x482, uint8_t x483 = addcarryx_u64(x480, x465, x467);
 uint64_t x485, uint8_t x486 = addcarryx_u64(x483, x468, x470);
 uint64_t x488, uint8_t _ = addcarryx_u64(0x0, x486, x471);
 uint64_t x491, uint8_t x492 = addcarryx_u64(0x0, x436, x455);
 uint64_t x494, uint8_t x495 = addcarryx_u64(x492, x439, x473);
 uint64_t x497, uint8_t x498 = addcarryx_u64(x495, x442, x476);
 uint64_t x500, uint8_t x501 = addcarryx_u64(x498, x445, x479);
 uint64_t x503, uint8_t x504 = addcarryx_u64(x501, x448, x482);
 uint64_t x506, uint8_t x507 = addcarryx_u64(x504, x451, x485);
 uint64_t x509, uint8_t x510 = addcarryx_u64(x507, x453, x488);
 uint64_t x512, uint64_t x513 = mulx_u64(x491, 0xffffffffffffffffL);
 uint64_t x515, uint64_t x516 = mulx_u64(x491, 0xffffffffffffffffL);
 uint64_t x518, uint64_t x519 = mulx_u64(x491, 0xfffffffdffffffffL);
 uint64_t x521, uint64_t x522 = mulx_u64(x491, 0xffffffffffffffffL);
 uint64_t x524, uint64_t x525 = mulx_u64(x491, 0xffffffffffffffffL);
 uint64_t x527, uint8_t x528 = mulx_u64_out_u8(x491, 0x3);
 uint64_t x530, uint8_t x531 = addcarryx_u64(0x0, x513, x515);
 uint64_t x533, uint8_t x534 = addcarryx_u64(x531, x516, x518);
 uint64_t x536, uint8_t x537 = addcarryx_u64(x534, x519, x521);
 uint64_t x539, uint8_t x540 = addcarryx_u64(x537, x522, x524);
 uint64_t x542, uint8_t x543 = addcarryx_u64(x540, x525, x527);
 uint8_t x544 = (x543 + x528);
 uint64_t _, uint8_t x547 = addcarryx_u64(0x0, x491, x512);
 uint64_t x549, uint8_t x550 = addcarryx_u64(x547, x494, x530);
 uint64_t x552, uint8_t x553 = addcarryx_u64(x550, x497, x533);
 uint64_t x555, uint8_t x556 = addcarryx_u64(x553, x500, x536);
 uint64_t x558, uint8_t x559 = addcarryx_u64(x556, x503, x539);
 uint64_t x561, uint8_t x562 = addcarryx_u64(x559, x506, x542);
 uint64_t x564, uint8_t x565 = addcarryx_u64(x562, x509, x544);
 uint8_t x566 = (x565 + x510);
 uint64_t x568, uint64_t x569 = mulx_u64(x12, x15);
 uint64_t x571, uint64_t x572 = mulx_u64(x12, x17);
 uint64_t x574, uint64_t x575 = mulx_u64(x12, x19);
 uint64_t x577, uint64_t x578 = mulx_u64(x12, x21);
 uint64_t x580, uint64_t x581 = mulx_u64(x12, x23);
 uint64_t x583, uint64_t x584 = mulx_u64(x12, x22);
 uint64_t x586, uint8_t x587 = addcarryx_u64(0x0, x569, x571);
 uint64_t x589, uint8_t x590 = addcarryx_u64(x587, x572, x574);
 uint64_t x592, uint8_t x593 = addcarryx_u64(x590, x575, x577);
 uint64_t x595, uint8_t x596 = addcarryx_u64(x593, x578, x580);
 uint64_t x598, uint8_t x599 = addcarryx_u64(x596, x581, x583);
 uint64_t x601, uint8_t _ = addcarryx_u64(0x0, x599, x584);
 uint64_t x604, uint8_t x605 = addcarryx_u64(0x0, x549, x568);
 uint64_t x607, uint8_t x608 = addcarryx_u64(x605, x552, x586);
 uint64_t x610, uint8_t x611 = addcarryx_u64(x608, x555, x589);
 uint64_t x613, uint8_t x614 = addcarryx_u64(x611, x558, x592);
 uint64_t x616, uint8_t x617 = addcarryx_u64(x614, x561, x595);
 uint64_t x619, uint8_t x620 = addcarryx_u64(x617, x564, x598);
 uint64_t x622, uint8_t x623 = addcarryx_u64(x620, x566, x601);
 uint64_t x625, uint64_t x626 = mulx_u64(x604, 0xffffffffffffffffL);
 uint64_t x628, uint64_t x629 = mulx_u64(x604, 0xffffffffffffffffL);
 uint64_t x631, uint64_t x632 = mulx_u64(x604, 0xfffffffdffffffffL);
 uint64_t x634, uint64_t x635 = mulx_u64(x604, 0xffffffffffffffffL);
 uint64_t x637, uint64_t x638 = mulx_u64(x604, 0xffffffffffffffffL);
 uint64_t x640, uint8_t x641 = mulx_u64_out_u8(x604, 0x3);
 uint64_t x643, uint8_t x644 = addcarryx_u64(0x0, x626, x628);
 uint64_t x646, uint8_t x647 = addcarryx_u64(x644, x629, x631);
 uint64_t x649, uint8_t x650 = addcarryx_u64(x647, x632, x634);
 uint64_t x652, uint8_t x653 = addcarryx_u64(x650, x635, x637);
 uint64_t x655, uint8_t x656 = addcarryx_u64(x653, x638, x640);
 uint8_t x657 = (x656 + x641);
 uint64_t _, uint8_t x660 = addcarryx_u64(0x0, x604, x625);
 uint64_t x662, uint8_t x663 = addcarryx_u64(x660, x607, x643);
 uint64_t x665, uint8_t x666 = addcarryx_u64(x663, x610, x646);
 uint64_t x668, uint8_t x669 = addcarryx_u64(x666, x613, x649);
 uint64_t x671, uint8_t x672 = addcarryx_u64(x669, x616, x652);
 uint64_t x674, uint8_t x675 = addcarryx_u64(x672, x619, x655);
 uint64_t x677, uint8_t x678 = addcarryx_u64(x675, x622, x657);
 uint8_t x679 = (x678 + x623);
 uint64_t x681, uint8_t x682 = subborrow_u64(0x0, x662, 0xffffffffffffffffL);
 uint64_t x684, uint8_t x685 = subborrow_u64(x682, x665, 0xffffffffffffffffL);
 uint64_t x687, uint8_t x688 = subborrow_u64(x685, x668, 0xfffffffdffffffffL);
 uint64_t x690, uint8_t x691 = subborrow_u64(x688, x671, 0xffffffffffffffffL);
 uint64_t x693, uint8_t x694 = subborrow_u64(x691, x674, 0xffffffffffffffffL);
 uint64_t x696, uint8_t x697 = subborrow_u64(x694, x677, 0x3);
 uint64_t _, uint8_t x700 = subborrow_u64(x697, x679, 0x0);
 uint64_t x701 = cmovznz64(x700, x696, x677);
 uint64_t x702 = cmovznz64(x700, x693, x674);
 uint64_t x703 = cmovznz64(x700, x690, x671);
 uint64_t x704 = cmovznz64(x700, x687, x668);
 uint64_t x705 = cmovznz64(x700, x684, x665);
 uint64_t x706 = cmovznz64(x700, x681, x662);
 return (x701, x702, x703, x704, x705, x706))
(x, x0)%core
     : 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)