build two montgomery files, including 32-bit p256

author: Andres Erbsen <andreser@google.com> 2017-11-15 20:04:11 +0000
committer: Andres Erbsen <andreser@google.com> 2017-11-15 20:04:11 +0000
commit: ba11f2c1999e845180da3ea770e3c8309aa18c60 (patch)
tree: 95bb6bdc59f81aa29f63a5e51baebcdb62c40281 /src
parent: fc4765b347fa561b7ba6e909ce771788848861ef (diff)
4 files changed, 1604 insertions, 0 deletions
diff --git a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femul.c b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femul.c
new file mode 100644
index 000000000..c9e60baf3
--- /dev/null
+++ b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femul.c
@@ -0,0 +1,379 @@
+static void femul(uint32_t out[8], const uint32_t in1[8], const uint32_t in2[8]) {
+  { const uint32_t x16 = in1[7];
+  { const uint32_t x17 = in1[6];
+  { const uint32_t x15 = in1[5];
+  { const uint32_t x13 = in1[4];
+  { const uint32_t x11 = in1[3];
+  { const uint32_t x9 = in1[2];
+  { const uint32_t x7 = in1[1];
+  { const uint32_t x5 = in1[0];
+  { const uint32_t x30 = in2[7];
+  { const uint32_t x31 = in2[6];
+  { const uint32_t x29 = in2[5];
+  { const uint32_t x27 = in2[4];
+  { const uint32_t x25 = in2[3];
+  { const uint32_t x23 = in2[2];
+  { const uint32_t x21 = in2[1];
+  { const uint32_t x19 = in2[0];
+  { uint32_t x34;  uint32_t x33 = _mulx_u32(x5, x19, &x34);
+  { uint32_t x37;  uint32_t x36 = _mulx_u32(x5, x21, &x37);
+  { uint32_t x40;  uint32_t x39 = _mulx_u32(x5, x23, &x40);
+  { uint32_t x43;  uint32_t x42 = _mulx_u32(x5, x25, &x43);
+  { uint32_t x46;  uint32_t x45 = _mulx_u32(x5, x27, &x46);
+  { uint32_t x49;  uint32_t x48 = _mulx_u32(x5, x29, &x49);
+  { uint32_t x52;  uint32_t x51 = _mulx_u32(x5, x31, &x52);
+  { uint32_t x55;  uint32_t x54 = _mulx_u32(x5, x30, &x55);
+  { uint32_t x57; uint8_t x58 = _addcarryx_u32(0x0, x34, x36, &x57);
+  { uint32_t x60; uint8_t x61 = _addcarryx_u32(x58, x37, x39, &x60);
+  { uint32_t x63; uint8_t x64 = _addcarryx_u32(x61, x40, x42, &x63);
+  { uint32_t x66; uint8_t x67 = _addcarryx_u32(x64, x43, x45, &x66);
+  { uint32_t x69; uint8_t x70 = _addcarryx_u32(x67, x46, x48, &x69);
+  { uint32_t x72; uint8_t x73 = _addcarryx_u32(x70, x49, x51, &x72);
+  { uint32_t x75; uint8_t x76 = _addcarryx_u32(x73, x52, x54, &x75);
+  { uint32_t x78; uint8_t _ = _addcarryx_u32(0x0, x76, x55, &x78);
+  { uint32_t x82;  uint32_t x81 = _mulx_u32(x33, 0xffffffff, &x82);
+  { uint32_t x85;  uint32_t x84 = _mulx_u32(x33, 0xffffffff, &x85);
+  { uint32_t x88;  uint32_t x87 = _mulx_u32(x33, 0xffffffff, &x88);
+  { uint32_t x91;  uint32_t x90 = _mulx_u32(x33, 0xffffffff, &x91);
+  { uint32_t x93; uint8_t x94 = _addcarryx_u32(0x0, x82, x84, &x93);
+  { uint32_t x96; uint8_t x97 = _addcarryx_u32(x94, x85, x87, &x96);
+  { uint32_t x99; uint8_t x100 = _addcarryx_u32(x97, x88, 0x0, &x99);
+  { 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, &x106);
+  { uint32_t x109; uint8_t x110 = _addcarryx_u32(x107, x60, x96, &x109);
+  { uint32_t x112; uint8_t x113 = _addcarryx_u32(x110, x63, x99, &x112);
+  { uint32_t x115; uint8_t x116 = _addcarryx_u32(x113, x66, x100, &x115);
+  { uint32_t x118; uint8_t x119 = _addcarryx_u32(x116, x69, x101, &x118);
+  { uint32_t x121; uint8_t x122 = _addcarryx_u32(x119, x72, x33, &x121);
+  { uint32_t x124; uint8_t x125 = _addcarryx_u32(x122, x75, x90, &x124);
+  { uint32_t x127; uint8_t x128 = _addcarryx_u32(x125, x78, x91, &x127);
+  { uint8_t x129 = (x128 + 0x0);
+  { uint32_t x132;  uint32_t x131 = _mulx_u32(x7, x19, &x132);
+  { uint32_t x135;  uint32_t x134 = _mulx_u32(x7, x21, &x135);
+  { uint32_t x138;  uint32_t x137 = _mulx_u32(x7, x23, &x138);
+  { uint32_t x141;  uint32_t x140 = _mulx_u32(x7, x25, &x141);
+  { uint32_t x144;  uint32_t x143 = _mulx_u32(x7, x27, &x144);
+  { uint32_t x147;  uint32_t x146 = _mulx_u32(x7, x29, &x147);
+  { uint32_t x150;  uint32_t x149 = _mulx_u32(x7, x31, &x150);
+  { uint32_t x153;  uint32_t x152 = _mulx_u32(x7, x30, &x153);
+  { uint32_t x155; uint8_t x156 = _addcarryx_u32(0x0, x132, x134, &x155);
+  { uint32_t x158; uint8_t x159 = _addcarryx_u32(x156, x135, x137, &x158);
+  { uint32_t x161; uint8_t x162 = _addcarryx_u32(x159, x138, x140, &x161);
+  { uint32_t x164; uint8_t x165 = _addcarryx_u32(x162, x141, x143, &x164);
+  { uint32_t x167; uint8_t x168 = _addcarryx_u32(x165, x144, x146, &x167);
+  { uint32_t x170; uint8_t x171 = _addcarryx_u32(x168, x147, x149, &x170);
+  { uint32_t x173; uint8_t x174 = _addcarryx_u32(x171, x150, x152, &x173);
+  { uint32_t x176; uint8_t _ = _addcarryx_u32(0x0, x174, x153, &x176);
+  { uint32_t x179; uint8_t x180 = _addcarryx_u32(0x0, x106, x131, &x179);
+  { uint32_t x182; uint8_t x183 = _addcarryx_u32(x180, x109, x155, &x182);
+  { uint32_t x185; uint8_t x186 = _addcarryx_u32(x183, x112, x158, &x185);
+  { uint32_t x188; uint8_t x189 = _addcarryx_u32(x186, x115, x161, &x188);
+  { uint32_t x191; uint8_t x192 = _addcarryx_u32(x189, x118, x164, &x191);
+  { uint32_t x194; uint8_t x195 = _addcarryx_u32(x192, x121, x167, &x194);
+  { uint32_t x197; uint8_t x198 = _addcarryx_u32(x195, x124, x170, &x197);
+  { uint32_t x200; uint8_t x201 = _addcarryx_u32(x198, x127, x173, &x200);
+  { uint32_t x203; uint8_t x204 = _addcarryx_u32(x201, x129, x176, &x203);
+  { uint32_t x207;  uint32_t x206 = _mulx_u32(x179, 0xffffffff, &x207);
+  { uint32_t x210;  uint32_t x209 = _mulx_u32(x179, 0xffffffff, &x210);
+  { uint32_t x213;  uint32_t x212 = _mulx_u32(x179, 0xffffffff, &x213);
+  { uint32_t x216;  uint32_t x215 = _mulx_u32(x179, 0xffffffff, &x216);
+  { uint32_t x218; uint8_t x219 = _addcarryx_u32(0x0, x207, x209, &x218);
+  { uint32_t x221; uint8_t x222 = _addcarryx_u32(x219, x210, x212, &x221);
+  { uint32_t x224; uint8_t x225 = _addcarryx_u32(x222, x213, 0x0, &x224);
+  { 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, &x231);
+  { uint32_t x234; uint8_t x235 = _addcarryx_u32(x232, x185, x221, &x234);
+  { uint32_t x237; uint8_t x238 = _addcarryx_u32(x235, x188, x224, &x237);
+  { uint32_t x240; uint8_t x241 = _addcarryx_u32(x238, x191, x225, &x240);
+  { uint32_t x243; uint8_t x244 = _addcarryx_u32(x241, x194, x226, &x243);
+  { uint32_t x246; uint8_t x247 = _addcarryx_u32(x244, x197, x179, &x246);
+  { uint32_t x249; uint8_t x250 = _addcarryx_u32(x247, x200, x215, &x249);
+  { uint32_t x252; uint8_t x253 = _addcarryx_u32(x250, x203, x216, &x252);
+  { uint8_t x254 = (x253 + x204);
+  { uint32_t x257;  uint32_t x256 = _mulx_u32(x9, x19, &x257);
+  { uint32_t x260;  uint32_t x259 = _mulx_u32(x9, x21, &x260);
+  { uint32_t x263;  uint32_t x262 = _mulx_u32(x9, x23, &x263);
+  { uint32_t x266;  uint32_t x265 = _mulx_u32(x9, x25, &x266);
+  { uint32_t x269;  uint32_t x268 = _mulx_u32(x9, x27, &x269);
+  { uint32_t x272;  uint32_t x271 = _mulx_u32(x9, x29, &x272);
+  { uint32_t x275;  uint32_t x274 = _mulx_u32(x9, x31, &x275);
+  { uint32_t x278;  uint32_t x277 = _mulx_u32(x9, x30, &x278);
+  { uint32_t x280; uint8_t x281 = _addcarryx_u32(0x0, x257, x259, &x280);
+  { uint32_t x283; uint8_t x284 = _addcarryx_u32(x281, x260, x262, &x283);
+  { uint32_t x286; uint8_t x287 = _addcarryx_u32(x284, x263, x265, &x286);
+  { uint32_t x289; uint8_t x290 = _addcarryx_u32(x287, x266, x268, &x289);
+  { uint32_t x292; uint8_t x293 = _addcarryx_u32(x290, x269, x271, &x292);
+  { uint32_t x295; uint8_t x296 = _addcarryx_u32(x293, x272, x274, &x295);
+  { uint32_t x298; uint8_t x299 = _addcarryx_u32(x296, x275, x277, &x298);
+  { uint32_t x301; uint8_t _ = _addcarryx_u32(0x0, x299, x278, &x301);
+  { uint32_t x304; uint8_t x305 = _addcarryx_u32(0x0, x231, x256, &x304);
+  { uint32_t x307; uint8_t x308 = _addcarryx_u32(x305, x234, x280, &x307);
+  { uint32_t x310; uint8_t x311 = _addcarryx_u32(x308, x237, x283, &x310);
+  { uint32_t x313; uint8_t x314 = _addcarryx_u32(x311, x240, x286, &x313);
+  { uint32_t x316; uint8_t x317 = _addcarryx_u32(x314, x243, x289, &x316);
+  { uint32_t x319; uint8_t x320 = _addcarryx_u32(x317, x246, x292, &x319);
+  { uint32_t x322; uint8_t x323 = _addcarryx_u32(x320, x249, x295, &x322);
+  { uint32_t x325; uint8_t x326 = _addcarryx_u32(x323, x252, x298, &x325);
+  { uint32_t x328; uint8_t x329 = _addcarryx_u32(x326, x254, x301, &x328);
+  { uint32_t x332;  uint32_t x331 = _mulx_u32(x304, 0xffffffff, &x332);
+  { uint32_t x335;  uint32_t x334 = _mulx_u32(x304, 0xffffffff, &x335);
+  { uint32_t x338;  uint32_t x337 = _mulx_u32(x304, 0xffffffff, &x338);
+  { uint32_t x341;  uint32_t x340 = _mulx_u32(x304, 0xffffffff, &x341);
+  { uint32_t x343; uint8_t x344 = _addcarryx_u32(0x0, x332, x334, &x343);
+  { uint32_t x346; uint8_t x347 = _addcarryx_u32(x344, x335, x337, &x346);
+  { uint32_t x349; uint8_t x350 = _addcarryx_u32(x347, x338, 0x0, &x349);
+  { 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, &x356);
+  { uint32_t x359; uint8_t x360 = _addcarryx_u32(x357, x310, x346, &x359);
+  { uint32_t x362; uint8_t x363 = _addcarryx_u32(x360, x313, x349, &x362);
+  { uint32_t x365; uint8_t x366 = _addcarryx_u32(x363, x316, x350, &x365);
+  { uint32_t x368; uint8_t x369 = _addcarryx_u32(x366, x319, x351, &x368);
+  { uint32_t x371; uint8_t x372 = _addcarryx_u32(x369, x322, x304, &x371);
+  { uint32_t x374; uint8_t x375 = _addcarryx_u32(x372, x325, x340, &x374);
+  { uint32_t x377; uint8_t x378 = _addcarryx_u32(x375, x328, x341, &x377);
+  { uint8_t x379 = (x378 + x329);
+  { uint32_t x382;  uint32_t x381 = _mulx_u32(x11, x19, &x382);
+  { uint32_t x385;  uint32_t x384 = _mulx_u32(x11, x21, &x385);
+  { uint32_t x388;  uint32_t x387 = _mulx_u32(x11, x23, &x388);
+  { uint32_t x391;  uint32_t x390 = _mulx_u32(x11, x25, &x391);
+  { uint32_t x394;  uint32_t x393 = _mulx_u32(x11, x27, &x394);
+  { uint32_t x397;  uint32_t x396 = _mulx_u32(x11, x29, &x397);
+  { uint32_t x400;  uint32_t x399 = _mulx_u32(x11, x31, &x400);
+  { uint32_t x403;  uint32_t x402 = _mulx_u32(x11, x30, &x403);
+  { uint32_t x405; uint8_t x406 = _addcarryx_u32(0x0, x382, x384, &x405);
+  { uint32_t x408; uint8_t x409 = _addcarryx_u32(x406, x385, x387, &x408);
+  { uint32_t x411; uint8_t x412 = _addcarryx_u32(x409, x388, x390, &x411);
+  { uint32_t x414; uint8_t x415 = _addcarryx_u32(x412, x391, x393, &x414);
+  { uint32_t x417; uint8_t x418 = _addcarryx_u32(x415, x394, x396, &x417);
+  { uint32_t x420; uint8_t x421 = _addcarryx_u32(x418, x397, x399, &x420);
+  { uint32_t x423; uint8_t x424 = _addcarryx_u32(x421, x400, x402, &x423);
+  { uint32_t x426; uint8_t _ = _addcarryx_u32(0x0, x424, x403, &x426);
+  { uint32_t x429; uint8_t x430 = _addcarryx_u32(0x0, x356, x381, &x429);
+  { uint32_t x432; uint8_t x433 = _addcarryx_u32(x430, x359, x405, &x432);
+  { uint32_t x435; uint8_t x436 = _addcarryx_u32(x433, x362, x408, &x435);
+  { uint32_t x438; uint8_t x439 = _addcarryx_u32(x436, x365, x411, &x438);
+  { uint32_t x441; uint8_t x442 = _addcarryx_u32(x439, x368, x414, &x441);
+  { uint32_t x444; uint8_t x445 = _addcarryx_u32(x442, x371, x417, &x444);
+  { uint32_t x447; uint8_t x448 = _addcarryx_u32(x445, x374, x420, &x447);
+  { uint32_t x450; uint8_t x451 = _addcarryx_u32(x448, x377, x423, &x450);
+  { uint32_t x453; uint8_t x454 = _addcarryx_u32(x451, x379, x426, &x453);
+  { uint32_t x457;  uint32_t x456 = _mulx_u32(x429, 0xffffffff, &x457);
+  { uint32_t x460;  uint32_t x459 = _mulx_u32(x429, 0xffffffff, &x460);
+  { uint32_t x463;  uint32_t x462 = _mulx_u32(x429, 0xffffffff, &x463);
+  { uint32_t x466;  uint32_t x465 = _mulx_u32(x429, 0xffffffff, &x466);
+  { uint32_t x468; uint8_t x469 = _addcarryx_u32(0x0, x457, x459, &x468);
+  { uint32_t x471; uint8_t x472 = _addcarryx_u32(x469, x460, x462, &x471);
+  { uint32_t x474; uint8_t x475 = _addcarryx_u32(x472, x463, 0x0, &x474);
+  { 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, &x481);
+  { uint32_t x484; uint8_t x485 = _addcarryx_u32(x482, x435, x471, &x484);
+  { uint32_t x487; uint8_t x488 = _addcarryx_u32(x485, x438, x474, &x487);
+  { uint32_t x490; uint8_t x491 = _addcarryx_u32(x488, x441, x475, &x490);
+  { uint32_t x493; uint8_t x494 = _addcarryx_u32(x491, x444, x476, &x493);
+  { uint32_t x496; uint8_t x497 = _addcarryx_u32(x494, x447, x429, &x496);
+  { uint32_t x499; uint8_t x500 = _addcarryx_u32(x497, x450, x465, &x499);
+  { uint32_t x502; uint8_t x503 = _addcarryx_u32(x500, x453, x466, &x502);
+  { uint8_t x504 = (x503 + x454);
+  { uint32_t x507;  uint32_t x506 = _mulx_u32(x13, x19, &x507);
+  { uint32_t x510;  uint32_t x509 = _mulx_u32(x13, x21, &x510);
+  { uint32_t x513;  uint32_t x512 = _mulx_u32(x13, x23, &x513);
+  { uint32_t x516;  uint32_t x515 = _mulx_u32(x13, x25, &x516);
+  { uint32_t x519;  uint32_t x518 = _mulx_u32(x13, x27, &x519);
+  { uint32_t x522;  uint32_t x521 = _mulx_u32(x13, x29, &x522);
+  { uint32_t x525;  uint32_t x524 = _mulx_u32(x13, x31, &x525);
+  { uint32_t x528;  uint32_t x527 = _mulx_u32(x13, x30, &x528);
+  { uint32_t x530; uint8_t x531 = _addcarryx_u32(0x0, x507, x509, &x530);
+  { uint32_t x533; uint8_t x534 = _addcarryx_u32(x531, x510, x512, &x533);
+  { uint32_t x536; uint8_t x537 = _addcarryx_u32(x534, x513, x515, &x536);
+  { uint32_t x539; uint8_t x540 = _addcarryx_u32(x537, x516, x518, &x539);
+  { uint32_t x542; uint8_t x543 = _addcarryx_u32(x540, x519, x521, &x542);
+  { uint32_t x545; uint8_t x546 = _addcarryx_u32(x543, x522, x524, &x545);
+  { uint32_t x548; uint8_t x549 = _addcarryx_u32(x546, x525, x527, &x548);
+  { uint32_t x551; uint8_t _ = _addcarryx_u32(0x0, x549, x528, &x551);
+  { uint32_t x554; uint8_t x555 = _addcarryx_u32(0x0, x481, x506, &x554);
+  { uint32_t x557; uint8_t x558 = _addcarryx_u32(x555, x484, x530, &x557);
+  { uint32_t x560; uint8_t x561 = _addcarryx_u32(x558, x487, x533, &x560);
+  { uint32_t x563; uint8_t x564 = _addcarryx_u32(x561, x490, x536, &x563);
+  { uint32_t x566; uint8_t x567 = _addcarryx_u32(x564, x493, x539, &x566);
+  { uint32_t x569; uint8_t x570 = _addcarryx_u32(x567, x496, x542, &x569);
+  { uint32_t x572; uint8_t x573 = _addcarryx_u32(x570, x499, x545, &x572);
+  { uint32_t x575; uint8_t x576 = _addcarryx_u32(x573, x502, x548, &x575);
+  { uint32_t x578; uint8_t x579 = _addcarryx_u32(x576, x504, x551, &x578);
+  { uint32_t x582;  uint32_t x581 = _mulx_u32(x554, 0xffffffff, &x582);
+  { uint32_t x585;  uint32_t x584 = _mulx_u32(x554, 0xffffffff, &x585);
+  { uint32_t x588;  uint32_t x587 = _mulx_u32(x554, 0xffffffff, &x588);
+  { uint32_t x591;  uint32_t x590 = _mulx_u32(x554, 0xffffffff, &x591);
+  { uint32_t x593; uint8_t x594 = _addcarryx_u32(0x0, x582, x584, &x593);
+  { uint32_t x596; uint8_t x597 = _addcarryx_u32(x594, x585, x587, &x596);
+  { uint32_t x599; uint8_t x600 = _addcarryx_u32(x597, x588, 0x0, &x599);
+  { 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, &x606);
+  { uint32_t x609; uint8_t x610 = _addcarryx_u32(x607, x560, x596, &x609);
+  { uint32_t x612; uint8_t x613 = _addcarryx_u32(x610, x563, x599, &x612);
+  { uint32_t x615; uint8_t x616 = _addcarryx_u32(x613, x566, x600, &x615);
+  { uint32_t x618; uint8_t x619 = _addcarryx_u32(x616, x569, x601, &x618);
+  { uint32_t x621; uint8_t x622 = _addcarryx_u32(x619, x572, x554, &x621);
+  { uint32_t x624; uint8_t x625 = _addcarryx_u32(x622, x575, x590, &x624);
+  { uint32_t x627; uint8_t x628 = _addcarryx_u32(x625, x578, x591, &x627);
+  { uint8_t x629 = (x628 + x579);
+  { uint32_t x632;  uint32_t x631 = _mulx_u32(x15, x19, &x632);
+  { uint32_t x635;  uint32_t x634 = _mulx_u32(x15, x21, &x635);
+  { uint32_t x638;  uint32_t x637 = _mulx_u32(x15, x23, &x638);
+  { uint32_t x641;  uint32_t x640 = _mulx_u32(x15, x25, &x641);
+  { uint32_t x644;  uint32_t x643 = _mulx_u32(x15, x27, &x644);
+  { uint32_t x647;  uint32_t x646 = _mulx_u32(x15, x29, &x647);
+  { uint32_t x650;  uint32_t x649 = _mulx_u32(x15, x31, &x650);
+  { uint32_t x653;  uint32_t x652 = _mulx_u32(x15, x30, &x653);
+  { uint32_t x655; uint8_t x656 = _addcarryx_u32(0x0, x632, x634, &x655);
+  { uint32_t x658; uint8_t x659 = _addcarryx_u32(x656, x635, x637, &x658);
+  { uint32_t x661; uint8_t x662 = _addcarryx_u32(x659, x638, x640, &x661);
+  { uint32_t x664; uint8_t x665 = _addcarryx_u32(x662, x641, x643, &x664);
+  { uint32_t x667; uint8_t x668 = _addcarryx_u32(x665, x644, x646, &x667);
+  { uint32_t x670; uint8_t x671 = _addcarryx_u32(x668, x647, x649, &x670);
+  { uint32_t x673; uint8_t x674 = _addcarryx_u32(x671, x650, x652, &x673);
+  { uint32_t x676; uint8_t _ = _addcarryx_u32(0x0, x674, x653, &x676);
+  { uint32_t x679; uint8_t x680 = _addcarryx_u32(0x0, x606, x631, &x679);
+  { uint32_t x682; uint8_t x683 = _addcarryx_u32(x680, x609, x655, &x682);
+  { uint32_t x685; uint8_t x686 = _addcarryx_u32(x683, x612, x658, &x685);
+  { uint32_t x688; uint8_t x689 = _addcarryx_u32(x686, x615, x661, &x688);
+  { uint32_t x691; uint8_t x692 = _addcarryx_u32(x689, x618, x664, &x691);
+  { uint32_t x694; uint8_t x695 = _addcarryx_u32(x692, x621, x667, &x694);
+  { uint32_t x697; uint8_t x698 = _addcarryx_u32(x695, x624, x670, &x697);
+  { uint32_t x700; uint8_t x701 = _addcarryx_u32(x698, x627, x673, &x700);
+  { uint32_t x703; uint8_t x704 = _addcarryx_u32(x701, x629, x676, &x703);
+  { uint32_t x707;  uint32_t x706 = _mulx_u32(x679, 0xffffffff, &x707);
+  { uint32_t x710;  uint32_t x709 = _mulx_u32(x679, 0xffffffff, &x710);
+  { uint32_t x713;  uint32_t x712 = _mulx_u32(x679, 0xffffffff, &x713);
+  { uint32_t x716;  uint32_t x715 = _mulx_u32(x679, 0xffffffff, &x716);
+  { uint32_t x718; uint8_t x719 = _addcarryx_u32(0x0, x707, x709, &x718);
+  { uint32_t x721; uint8_t x722 = _addcarryx_u32(x719, x710, x712, &x721);
+  { uint32_t x724; uint8_t x725 = _addcarryx_u32(x722, x713, 0x0, &x724);
+  { 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, &x731);
+  { uint32_t x734; uint8_t x735 = _addcarryx_u32(x732, x685, x721, &x734);
+  { uint32_t x737; uint8_t x738 = _addcarryx_u32(x735, x688, x724, &x737);
+  { uint32_t x740; uint8_t x741 = _addcarryx_u32(x738, x691, x725, &x740);
+  { uint32_t x743; uint8_t x744 = _addcarryx_u32(x741, x694, x726, &x743);
+  { uint32_t x746; uint8_t x747 = _addcarryx_u32(x744, x697, x679, &x746);
+  { uint32_t x749; uint8_t x750 = _addcarryx_u32(x747, x700, x715, &x749);
+  { uint32_t x752; uint8_t x753 = _addcarryx_u32(x750, x703, x716, &x752);
+  { uint8_t x754 = (x753 + x704);
+  { uint32_t x757;  uint32_t x756 = _mulx_u32(x17, x19, &x757);
+  { uint32_t x760;  uint32_t x759 = _mulx_u32(x17, x21, &x760);
+  { uint32_t x763;  uint32_t x762 = _mulx_u32(x17, x23, &x763);
+  { uint32_t x766;  uint32_t x765 = _mulx_u32(x17, x25, &x766);
+  { uint32_t x769;  uint32_t x768 = _mulx_u32(x17, x27, &x769);
+  { uint32_t x772;  uint32_t x771 = _mulx_u32(x17, x29, &x772);
+  { uint32_t x775;  uint32_t x774 = _mulx_u32(x17, x31, &x775);
+  { uint32_t x778;  uint32_t x777 = _mulx_u32(x17, x30, &x778);
+  { uint32_t x780; uint8_t x781 = _addcarryx_u32(0x0, x757, x759, &x780);
+  { uint32_t x783; uint8_t x784 = _addcarryx_u32(x781, x760, x762, &x783);
+  { uint32_t x786; uint8_t x787 = _addcarryx_u32(x784, x763, x765, &x786);
+  { uint32_t x789; uint8_t x790 = _addcarryx_u32(x787, x766, x768, &x789);
+  { uint32_t x792; uint8_t x793 = _addcarryx_u32(x790, x769, x771, &x792);
+  { uint32_t x795; uint8_t x796 = _addcarryx_u32(x793, x772, x774, &x795);
+  { uint32_t x798; uint8_t x799 = _addcarryx_u32(x796, x775, x777, &x798);
+  { uint32_t x801; uint8_t _ = _addcarryx_u32(0x0, x799, x778, &x801);
+  { uint32_t x804; uint8_t x805 = _addcarryx_u32(0x0, x731, x756, &x804);
+  { uint32_t x807; uint8_t x808 = _addcarryx_u32(x805, x734, x780, &x807);
+  { uint32_t x810; uint8_t x811 = _addcarryx_u32(x808, x737, x783, &x810);
+  { uint32_t x813; uint8_t x814 = _addcarryx_u32(x811, x740, x786, &x813);
+  { uint32_t x816; uint8_t x817 = _addcarryx_u32(x814, x743, x789, &x816);
+  { uint32_t x819; uint8_t x820 = _addcarryx_u32(x817, x746, x792, &x819);
+  { uint32_t x822; uint8_t x823 = _addcarryx_u32(x820, x749, x795, &x822);
+  { uint32_t x825; uint8_t x826 = _addcarryx_u32(x823, x752, x798, &x825);
+  { uint32_t x828; uint8_t x829 = _addcarryx_u32(x826, x754, x801, &x828);
+  { uint32_t x832;  uint32_t x831 = _mulx_u32(x804, 0xffffffff, &x832);
+  { uint32_t x835;  uint32_t x834 = _mulx_u32(x804, 0xffffffff, &x835);
+  { uint32_t x838;  uint32_t x837 = _mulx_u32(x804, 0xffffffff, &x838);
+  { uint32_t x841;  uint32_t x840 = _mulx_u32(x804, 0xffffffff, &x841);
+  { uint32_t x843; uint8_t x844 = _addcarryx_u32(0x0, x832, x834, &x843);
+  { uint32_t x846; uint8_t x847 = _addcarryx_u32(x844, x835, x837, &x846);
+  { uint32_t x849; uint8_t x850 = _addcarryx_u32(x847, x838, 0x0, &x849);
+  { 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, &x856);
+  { uint32_t x859; uint8_t x860 = _addcarryx_u32(x857, x810, x846, &x859);
+  { uint32_t x862; uint8_t x863 = _addcarryx_u32(x860, x813, x849, &x862);
+  { uint32_t x865; uint8_t x866 = _addcarryx_u32(x863, x816, x850, &x865);
+  { uint32_t x868; uint8_t x869 = _addcarryx_u32(x866, x819, x851, &x868);
+  { uint32_t x871; uint8_t x872 = _addcarryx_u32(x869, x822, x804, &x871);
+  { uint32_t x874; uint8_t x875 = _addcarryx_u32(x872, x825, x840, &x874);
+  { uint32_t x877; uint8_t x878 = _addcarryx_u32(x875, x828, x841, &x877);
+  { uint8_t x879 = (x878 + x829);
+  { uint32_t x882;  uint32_t x881 = _mulx_u32(x16, x19, &x882);
+  { uint32_t x885;  uint32_t x884 = _mulx_u32(x16, x21, &x885);
+  { uint32_t x888;  uint32_t x887 = _mulx_u32(x16, x23, &x888);
+  { uint32_t x891;  uint32_t x890 = _mulx_u32(x16, x25, &x891);
+  { uint32_t x894;  uint32_t x893 = _mulx_u32(x16, x27, &x894);
+  { uint32_t x897;  uint32_t x896 = _mulx_u32(x16, x29, &x897);
+  { uint32_t x900;  uint32_t x899 = _mulx_u32(x16, x31, &x900);
+  { uint32_t x903;  uint32_t x902 = _mulx_u32(x16, x30, &x903);
+  { uint32_t x905; uint8_t x906 = _addcarryx_u32(0x0, x882, x884, &x905);
+  { uint32_t x908; uint8_t x909 = _addcarryx_u32(x906, x885, x887, &x908);
+  { uint32_t x911; uint8_t x912 = _addcarryx_u32(x909, x888, x890, &x911);
+  { uint32_t x914; uint8_t x915 = _addcarryx_u32(x912, x891, x893, &x914);
+  { uint32_t x917; uint8_t x918 = _addcarryx_u32(x915, x894, x896, &x917);
+  { uint32_t x920; uint8_t x921 = _addcarryx_u32(x918, x897, x899, &x920);
+  { uint32_t x923; uint8_t x924 = _addcarryx_u32(x921, x900, x902, &x923);
+  { uint32_t x926; uint8_t _ = _addcarryx_u32(0x0, x924, x903, &x926);
+  { uint32_t x929; uint8_t x930 = _addcarryx_u32(0x0, x856, x881, &x929);
+  { uint32_t x932; uint8_t x933 = _addcarryx_u32(x930, x859, x905, &x932);
+  { uint32_t x935; uint8_t x936 = _addcarryx_u32(x933, x862, x908, &x935);
+  { uint32_t x938; uint8_t x939 = _addcarryx_u32(x936, x865, x911, &x938);
+  { uint32_t x941; uint8_t x942 = _addcarryx_u32(x939, x868, x914, &x941);
+  { uint32_t x944; uint8_t x945 = _addcarryx_u32(x942, x871, x917, &x944);
+  { uint32_t x947; uint8_t x948 = _addcarryx_u32(x945, x874, x920, &x947);
+  { uint32_t x950; uint8_t x951 = _addcarryx_u32(x948, x877, x923, &x950);
+  { uint32_t x953; uint8_t x954 = _addcarryx_u32(x951, x879, x926, &x953);
+  { uint32_t x957;  uint32_t x956 = _mulx_u32(x929, 0xffffffff, &x957);
+  { uint32_t x960;  uint32_t x959 = _mulx_u32(x929, 0xffffffff, &x960);
+  { uint32_t x963;  uint32_t x962 = _mulx_u32(x929, 0xffffffff, &x963);
+  { uint32_t x966;  uint32_t x965 = _mulx_u32(x929, 0xffffffff, &x966);
+  { uint32_t x968; uint8_t x969 = _addcarryx_u32(0x0, x957, x959, &x968);
+  { uint32_t x971; uint8_t x972 = _addcarryx_u32(x969, x960, x962, &x971);
+  { uint32_t x974; uint8_t x975 = _addcarryx_u32(x972, x963, 0x0, &x974);
+  { 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, &x981);
+  { uint32_t x984; uint8_t x985 = _addcarryx_u32(x982, x935, x971, &x984);
+  { uint32_t x987; uint8_t x988 = _addcarryx_u32(x985, x938, x974, &x987);
+  { uint32_t x990; uint8_t x991 = _addcarryx_u32(x988, x941, x975, &x990);
+  { uint32_t x993; uint8_t x994 = _addcarryx_u32(x991, x944, x976, &x993);
+  { uint32_t x996; uint8_t x997 = _addcarryx_u32(x994, x947, x929, &x996);
+  { uint32_t x999; uint8_t x1000 = _addcarryx_u32(x997, x950, x965, &x999);
+  { uint32_t x1002; uint8_t x1003 = _addcarryx_u32(x1000, x953, x966, &x1002);
+  { uint8_t x1004 = (x1003 + x954);
+  { uint32_t x1006; uint8_t x1007 = _subborrow_u32(0x0, x981, 0xffffffff, &x1006);
+  { uint32_t x1009; uint8_t x1010 = _subborrow_u32(x1007, x984, 0xffffffff, &x1009);
+  { uint32_t x1012; uint8_t x1013 = _subborrow_u32(x1010, x987, 0xffffffff, &x1012);
+  { uint32_t x1015; uint8_t x1016 = _subborrow_u32(x1013, x990, 0x0, &x1015);
+  { uint32_t x1018; uint8_t x1019 = _subborrow_u32(x1016, x993, 0x0, &x1018);
+  { uint32_t x1021; uint8_t x1022 = _subborrow_u32(x1019, x996, 0x0, &x1021);
+  { uint32_t x1024; uint8_t x1025 = _subborrow_u32(x1022, x999, 0x1, &x1024);
+  { uint32_t x1027; uint8_t x1028 = _subborrow_u32(x1025, x1002, 0xffffffff, &x1027);
+  { 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);
+  out[0] = x1039;
+  out[1] = x1038;
+  out[2] = x1037;
+  out[3] = x1036;
+  out[4] = x1035;
+  out[5] = x1034;
+  out[6] = x1033;
+  out[7] = x1032;
+  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femulDisplay.log b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femulDisplay.log
new file mode 100644
index 000000000..c7c748f7f
--- /dev/null
+++ b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1_8limbs/femulDisplay.log
@@ -0,0 +1,359 @@
+λ 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)
diff --git a/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femul.c b/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femul.c
new file mode 100644
index 000000000..958e08911
--- /dev/null
+++ b/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femul.c
@@ -0,0 +1,443 @@
+static void femul(uint64_t out[8], const uint64_t in1[8], const uint64_t in2[8]) {
+  { const uint64_t x16 = in1[7];
+  { const uint64_t x17 = in1[6];
+  { const uint64_t x15 = in1[5];
+  { const uint64_t x13 = in1[4];
+  { const uint64_t x11 = in1[3];
+  { const uint64_t x9 = in1[2];
+  { const uint64_t x7 = in1[1];
+  { const uint64_t x5 = in1[0];
+  { const uint64_t x30 = in2[7];
+  { const uint64_t x31 = in2[6];
+  { const uint64_t x29 = in2[5];
+  { const uint64_t x27 = in2[4];
+  { const uint64_t x25 = in2[3];
+  { const uint64_t x23 = in2[2];
+  { const uint64_t x21 = in2[1];
+  { const uint64_t x19 = in2[0];
+  { uint64_t x34;  uint64_t x33 = _mulx_u64(x5, x19, &x34);
+  { uint64_t x37;  uint64_t x36 = _mulx_u64(x5, x21, &x37);
+  { uint64_t x40;  uint64_t x39 = _mulx_u64(x5, x23, &x40);
+  { uint64_t x43;  uint64_t x42 = _mulx_u64(x5, x25, &x43);
+  { uint64_t x46;  uint64_t x45 = _mulx_u64(x5, x27, &x46);
+  { uint64_t x49;  uint64_t x48 = _mulx_u64(x5, x29, &x49);
+  { uint64_t x52;  uint64_t x51 = _mulx_u64(x5, x31, &x52);
+  { uint64_t x55;  uint64_t x54 = _mulx_u64(x5, x30, &x55);
+  { uint64_t x57; uint8_t x58 = _addcarryx_u64(0x0, x34, x36, &x57);
+  { uint64_t x60; uint8_t x61 = _addcarryx_u64(x58, x37, x39, &x60);
+  { uint64_t x63; uint8_t x64 = _addcarryx_u64(x61, x40, x42, &x63);
+  { uint64_t x66; uint8_t x67 = _addcarryx_u64(x64, x43, x45, &x66);
+  { uint64_t x69; uint8_t x70 = _addcarryx_u64(x67, x46, x48, &x69);
+  { uint64_t x72; uint8_t x73 = _addcarryx_u64(x70, x49, x51, &x72);
+  { uint64_t x75; uint8_t x76 = _addcarryx_u64(x73, x52, x54, &x75);
+  { uint64_t x78; uint8_t _ = _addcarryx_u64(0x0, x76, x55, &x78);
+  { uint64_t x82;  uint64_t x81 = _mulx_u64(x33, 0xffffffffffffffffL, &x82);
+  { uint64_t x85;  uint64_t x84 = _mulx_u64(x33, 0xffffffffffffffffL, &x85);
+  { uint64_t x88;  uint64_t x87 = _mulx_u64(x33, 0xffffffffffffffffL, &x88);
+  { uint64_t x91;  uint64_t x90 = _mulx_u64(x33, 0xffffffffffffffffL, &x91);
+  { uint64_t x94;  uint64_t x93 = _mulx_u64(x33, 0xffffffffffffffffL, &x94);
+  { uint64_t x97;  uint64_t x96 = _mulx_u64(x33, 0xffffffffffffffffL, &x97);
+  { uint64_t x100;  uint64_t x99 = _mulx_u64(x33, 0xffffffffffffffffL, &x100);
+  { uint64_t x103;  uint64_t x102 = _mulx_u64(x33, 0xfe14ffffffffffffL, &x103);
+  { uint64_t x105; uint8_t x106 = _addcarryx_u64(0x0, x82, x84, &x105);
+  { uint64_t x108; uint8_t x109 = _addcarryx_u64(x106, x85, x87, &x108);
+  { uint64_t x111; uint8_t x112 = _addcarryx_u64(x109, x88, x90, &x111);
+  { uint64_t x114; uint8_t x115 = _addcarryx_u64(x112, x91, x93, &x114);
+  { uint64_t x117; uint8_t x118 = _addcarryx_u64(x115, x94, x96, &x117);
+  { uint64_t x120; uint8_t x121 = _addcarryx_u64(x118, x97, x99, &x120);
+  { uint64_t x123; uint8_t x124 = _addcarryx_u64(x121, x100, x102, &x123);
+  { uint64_t x126; uint8_t _ = _addcarryx_u64(0x0, x124, x103, &x126);
+  { uint64_t _; uint8_t x130 = _addcarryx_u64(0x0, x33, x81, &_);
+  { uint64_t x132; uint8_t x133 = _addcarryx_u64(x130, x57, x105, &x132);
+  { uint64_t x135; uint8_t x136 = _addcarryx_u64(x133, x60, x108, &x135);
+  { uint64_t x138; uint8_t x139 = _addcarryx_u64(x136, x63, x111, &x138);
+  { uint64_t x141; uint8_t x142 = _addcarryx_u64(x139, x66, x114, &x141);
+  { uint64_t x144; uint8_t x145 = _addcarryx_u64(x142, x69, x117, &x144);
+  { uint64_t x147; uint8_t x148 = _addcarryx_u64(x145, x72, x120, &x147);
+  { uint64_t x150; uint8_t x151 = _addcarryx_u64(x148, x75, x123, &x150);
+  { uint64_t x153; uint8_t x154 = _addcarryx_u64(x151, x78, x126, &x153);
+  { uint8_t x155 = (x154 + 0x0);
+  { uint64_t x158;  uint64_t x157 = _mulx_u64(x7, x19, &x158);
+  { uint64_t x161;  uint64_t x160 = _mulx_u64(x7, x21, &x161);
+  { uint64_t x164;  uint64_t x163 = _mulx_u64(x7, x23, &x164);
+  { uint64_t x167;  uint64_t x166 = _mulx_u64(x7, x25, &x167);
+  { uint64_t x170;  uint64_t x169 = _mulx_u64(x7, x27, &x170);
+  { uint64_t x173;  uint64_t x172 = _mulx_u64(x7, x29, &x173);
+  { uint64_t x176;  uint64_t x175 = _mulx_u64(x7, x31, &x176);
+  { uint64_t x179;  uint64_t x178 = _mulx_u64(x7, x30, &x179);
+  { uint64_t x181; uint8_t x182 = _addcarryx_u64(0x0, x158, x160, &x181);
+  { uint64_t x184; uint8_t x185 = _addcarryx_u64(x182, x161, x163, &x184);
+  { uint64_t x187; uint8_t x188 = _addcarryx_u64(x185, x164, x166, &x187);
+  { uint64_t x190; uint8_t x191 = _addcarryx_u64(x188, x167, x169, &x190);
+  { uint64_t x193; uint8_t x194 = _addcarryx_u64(x191, x170, x172, &x193);
+  { uint64_t x196; uint8_t x197 = _addcarryx_u64(x194, x173, x175, &x196);
+  { uint64_t x199; uint8_t x200 = _addcarryx_u64(x197, x176, x178, &x199);
+  { uint64_t x202; uint8_t _ = _addcarryx_u64(0x0, x200, x179, &x202);
+  { uint64_t x205; uint8_t x206 = _addcarryx_u64(0x0, x132, x157, &x205);
+  { uint64_t x208; uint8_t x209 = _addcarryx_u64(x206, x135, x181, &x208);
+  { uint64_t x211; uint8_t x212 = _addcarryx_u64(x209, x138, x184, &x211);
+  { uint64_t x214; uint8_t x215 = _addcarryx_u64(x212, x141, x187, &x214);
+  { uint64_t x217; uint8_t x218 = _addcarryx_u64(x215, x144, x190, &x217);
+  { uint64_t x220; uint8_t x221 = _addcarryx_u64(x218, x147, x193, &x220);
+  { uint64_t x223; uint8_t x224 = _addcarryx_u64(x221, x150, x196, &x223);
+  { uint64_t x226; uint8_t x227 = _addcarryx_u64(x224, x153, x199, &x226);
+  { uint64_t x229; uint8_t x230 = _addcarryx_u64(x227, x155, x202, &x229);
+  { uint64_t x233;  uint64_t x232 = _mulx_u64(x205, 0xffffffffffffffffL, &x233);
+  { uint64_t x236;  uint64_t x235 = _mulx_u64(x205, 0xffffffffffffffffL, &x236);
+  { uint64_t x239;  uint64_t x238 = _mulx_u64(x205, 0xffffffffffffffffL, &x239);
+  { uint64_t x242;  uint64_t x241 = _mulx_u64(x205, 0xffffffffffffffffL, &x242);
+  { uint64_t x245;  uint64_t x244 = _mulx_u64(x205, 0xffffffffffffffffL, &x245);
+  { uint64_t x248;  uint64_t x247 = _mulx_u64(x205, 0xffffffffffffffffL, &x248);
+  { uint64_t x251;  uint64_t x250 = _mulx_u64(x205, 0xffffffffffffffffL, &x251);
+  { uint64_t x254;  uint64_t x253 = _mulx_u64(x205, 0xfe14ffffffffffffL, &x254);
+  { uint64_t x256; uint8_t x257 = _addcarryx_u64(0x0, x233, x235, &x256);
+  { uint64_t x259; uint8_t x260 = _addcarryx_u64(x257, x236, x238, &x259);
+  { uint64_t x262; uint8_t x263 = _addcarryx_u64(x260, x239, x241, &x262);
+  { uint64_t x265; uint8_t x266 = _addcarryx_u64(x263, x242, x244, &x265);
+  { uint64_t x268; uint8_t x269 = _addcarryx_u64(x266, x245, x247, &x268);
+  { uint64_t x271; uint8_t x272 = _addcarryx_u64(x269, x248, x250, &x271);
+  { uint64_t x274; uint8_t x275 = _addcarryx_u64(x272, x251, x253, &x274);
+  { uint64_t x277; uint8_t _ = _addcarryx_u64(0x0, x275, x254, &x277);
+  { uint64_t _; uint8_t x281 = _addcarryx_u64(0x0, x205, x232, &_);
+  { uint64_t x283; uint8_t x284 = _addcarryx_u64(x281, x208, x256, &x283);
+  { uint64_t x286; uint8_t x287 = _addcarryx_u64(x284, x211, x259, &x286);
+  { uint64_t x289; uint8_t x290 = _addcarryx_u64(x287, x214, x262, &x289);
+  { uint64_t x292; uint8_t x293 = _addcarryx_u64(x290, x217, x265, &x292);
+  { uint64_t x295; uint8_t x296 = _addcarryx_u64(x293, x220, x268, &x295);
+  { uint64_t x298; uint8_t x299 = _addcarryx_u64(x296, x223, x271, &x298);
+  { uint64_t x301; uint8_t x302 = _addcarryx_u64(x299, x226, x274, &x301);
+  { uint64_t x304; uint8_t x305 = _addcarryx_u64(x302, x229, x277, &x304);
+  { uint8_t x306 = (x305 + x230);
+  { uint64_t x309;  uint64_t x308 = _mulx_u64(x9, x19, &x309);
+  { uint64_t x312;  uint64_t x311 = _mulx_u64(x9, x21, &x312);
+  { uint64_t x315;  uint64_t x314 = _mulx_u64(x9, x23, &x315);
+  { uint64_t x318;  uint64_t x317 = _mulx_u64(x9, x25, &x318);
+  { uint64_t x321;  uint64_t x320 = _mulx_u64(x9, x27, &x321);
+  { uint64_t x324;  uint64_t x323 = _mulx_u64(x9, x29, &x324);
+  { uint64_t x327;  uint64_t x326 = _mulx_u64(x9, x31, &x327);
+  { uint64_t x330;  uint64_t x329 = _mulx_u64(x9, x30, &x330);
+  { uint64_t x332; uint8_t x333 = _addcarryx_u64(0x0, x309, x311, &x332);
+  { uint64_t x335; uint8_t x336 = _addcarryx_u64(x333, x312, x314, &x335);
+  { uint64_t x338; uint8_t x339 = _addcarryx_u64(x336, x315, x317, &x338);
+  { uint64_t x341; uint8_t x342 = _addcarryx_u64(x339, x318, x320, &x341);
+  { uint64_t x344; uint8_t x345 = _addcarryx_u64(x342, x321, x323, &x344);
+  { uint64_t x347; uint8_t x348 = _addcarryx_u64(x345, x324, x326, &x347);
+  { uint64_t x350; uint8_t x351 = _addcarryx_u64(x348, x327, x329, &x350);
+  { uint64_t x353; uint8_t _ = _addcarryx_u64(0x0, x351, x330, &x353);
+  { uint64_t x356; uint8_t x357 = _addcarryx_u64(0x0, x283, x308, &x356);
+  { uint64_t x359; uint8_t x360 = _addcarryx_u64(x357, x286, x332, &x359);
+  { uint64_t x362; uint8_t x363 = _addcarryx_u64(x360, x289, x335, &x362);
+  { uint64_t x365; uint8_t x366 = _addcarryx_u64(x363, x292, x338, &x365);
+  { uint64_t x368; uint8_t x369 = _addcarryx_u64(x366, x295, x341, &x368);
+  { uint64_t x371; uint8_t x372 = _addcarryx_u64(x369, x298, x344, &x371);
+  { uint64_t x374; uint8_t x375 = _addcarryx_u64(x372, x301, x347, &x374);
+  { uint64_t x377; uint8_t x378 = _addcarryx_u64(x375, x304, x350, &x377);
+  { uint64_t x380; uint8_t x381 = _addcarryx_u64(x378, x306, x353, &x380);
+  { uint64_t x384;  uint64_t x383 = _mulx_u64(x356, 0xffffffffffffffffL, &x384);
+  { uint64_t x387;  uint64_t x386 = _mulx_u64(x356, 0xffffffffffffffffL, &x387);
+  { uint64_t x390;  uint64_t x389 = _mulx_u64(x356, 0xffffffffffffffffL, &x390);
+  { uint64_t x393;  uint64_t x392 = _mulx_u64(x356, 0xffffffffffffffffL, &x393);
+  { uint64_t x396;  uint64_t x395 = _mulx_u64(x356, 0xffffffffffffffffL, &x396);
+  { uint64_t x399;  uint64_t x398 = _mulx_u64(x356, 0xffffffffffffffffL, &x399);
+  { uint64_t x402;  uint64_t x401 = _mulx_u64(x356, 0xffffffffffffffffL, &x402);
+  { uint64_t x405;  uint64_t x404 = _mulx_u64(x356, 0xfe14ffffffffffffL, &x405);
+  { uint64_t x407; uint8_t x408 = _addcarryx_u64(0x0, x384, x386, &x407);
+  { uint64_t x410; uint8_t x411 = _addcarryx_u64(x408, x387, x389, &x410);
+  { uint64_t x413; uint8_t x414 = _addcarryx_u64(x411, x390, x392, &x413);
+  { uint64_t x416; uint8_t x417 = _addcarryx_u64(x414, x393, x395, &x416);
+  { uint64_t x419; uint8_t x420 = _addcarryx_u64(x417, x396, x398, &x419);
+  { uint64_t x422; uint8_t x423 = _addcarryx_u64(x420, x399, x401, &x422);
+  { uint64_t x425; uint8_t x426 = _addcarryx_u64(x423, x402, x404, &x425);
+  { uint64_t x428; uint8_t _ = _addcarryx_u64(0x0, x426, x405, &x428);
+  { uint64_t _; uint8_t x432 = _addcarryx_u64(0x0, x356, x383, &_);
+  { uint64_t x434; uint8_t x435 = _addcarryx_u64(x432, x359, x407, &x434);
+  { uint64_t x437; uint8_t x438 = _addcarryx_u64(x435, x362, x410, &x437);
+  { uint64_t x440; uint8_t x441 = _addcarryx_u64(x438, x365, x413, &x440);
+  { uint64_t x443; uint8_t x444 = _addcarryx_u64(x441, x368, x416, &x443);
+  { uint64_t x446; uint8_t x447 = _addcarryx_u64(x444, x371, x419, &x446);
+  { uint64_t x449; uint8_t x450 = _addcarryx_u64(x447, x374, x422, &x449);
+  { uint64_t x452; uint8_t x453 = _addcarryx_u64(x450, x377, x425, &x452);
+  { uint64_t x455; uint8_t x456 = _addcarryx_u64(x453, x380, x428, &x455);
+  { uint8_t x457 = (x456 + x381);
+  { uint64_t x460;  uint64_t x459 = _mulx_u64(x11, x19, &x460);
+  { uint64_t x463;  uint64_t x462 = _mulx_u64(x11, x21, &x463);
+  { uint64_t x466;  uint64_t x465 = _mulx_u64(x11, x23, &x466);
+  { uint64_t x469;  uint64_t x468 = _mulx_u64(x11, x25, &x469);
+  { uint64_t x472;  uint64_t x471 = _mulx_u64(x11, x27, &x472);
+  { uint64_t x475;  uint64_t x474 = _mulx_u64(x11, x29, &x475);
+  { uint64_t x478;  uint64_t x477 = _mulx_u64(x11, x31, &x478);
+  { uint64_t x481;  uint64_t x480 = _mulx_u64(x11, x30, &x481);
+  { uint64_t x483; uint8_t x484 = _addcarryx_u64(0x0, x460, x462, &x483);
+  { uint64_t x486; uint8_t x487 = _addcarryx_u64(x484, x463, x465, &x486);
+  { uint64_t x489; uint8_t x490 = _addcarryx_u64(x487, x466, x468, &x489);
+  { uint64_t x492; uint8_t x493 = _addcarryx_u64(x490, x469, x471, &x492);
+  { uint64_t x495; uint8_t x496 = _addcarryx_u64(x493, x472, x474, &x495);
+  { uint64_t x498; uint8_t x499 = _addcarryx_u64(x496, x475, x477, &x498);
+  { uint64_t x501; uint8_t x502 = _addcarryx_u64(x499, x478, x480, &x501);
+  { uint64_t x504; uint8_t _ = _addcarryx_u64(0x0, x502, x481, &x504);
+  { uint64_t x507; uint8_t x508 = _addcarryx_u64(0x0, x434, x459, &x507);
+  { uint64_t x510; uint8_t x511 = _addcarryx_u64(x508, x437, x483, &x510);
+  { uint64_t x513; uint8_t x514 = _addcarryx_u64(x511, x440, x486, &x513);
+  { uint64_t x516; uint8_t x517 = _addcarryx_u64(x514, x443, x489, &x516);
+  { uint64_t x519; uint8_t x520 = _addcarryx_u64(x517, x446, x492, &x519);
+  { uint64_t x522; uint8_t x523 = _addcarryx_u64(x520, x449, x495, &x522);
+  { uint64_t x525; uint8_t x526 = _addcarryx_u64(x523, x452, x498, &x525);
+  { uint64_t x528; uint8_t x529 = _addcarryx_u64(x526, x455, x501, &x528);
+  { uint64_t x531; uint8_t x532 = _addcarryx_u64(x529, x457, x504, &x531);
+  { uint64_t x535;  uint64_t x534 = _mulx_u64(x507, 0xffffffffffffffffL, &x535);
+  { uint64_t x538;  uint64_t x537 = _mulx_u64(x507, 0xffffffffffffffffL, &x538);
+  { uint64_t x541;  uint64_t x540 = _mulx_u64(x507, 0xffffffffffffffffL, &x541);
+  { uint64_t x544;  uint64_t x543 = _mulx_u64(x507, 0xffffffffffffffffL, &x544);
+  { uint64_t x547;  uint64_t x546 = _mulx_u64(x507, 0xffffffffffffffffL, &x547);
+  { uint64_t x550;  uint64_t x549 = _mulx_u64(x507, 0xffffffffffffffffL, &x550);
+  { uint64_t x553;  uint64_t x552 = _mulx_u64(x507, 0xffffffffffffffffL, &x553);
+  { uint64_t x556;  uint64_t x555 = _mulx_u64(x507, 0xfe14ffffffffffffL, &x556);
+  { uint64_t x558; uint8_t x559 = _addcarryx_u64(0x0, x535, x537, &x558);
+  { uint64_t x561; uint8_t x562 = _addcarryx_u64(x559, x538, x540, &x561);
+  { uint64_t x564; uint8_t x565 = _addcarryx_u64(x562, x541, x543, &x564);
+  { uint64_t x567; uint8_t x568 = _addcarryx_u64(x565, x544, x546, &x567);
+  { uint64_t x570; uint8_t x571 = _addcarryx_u64(x568, x547, x549, &x570);
+  { uint64_t x573; uint8_t x574 = _addcarryx_u64(x571, x550, x552, &x573);
+  { uint64_t x576; uint8_t x577 = _addcarryx_u64(x574, x553, x555, &x576);
+  { uint64_t x579; uint8_t _ = _addcarryx_u64(0x0, x577, x556, &x579);
+  { uint64_t _; uint8_t x583 = _addcarryx_u64(0x0, x507, x534, &_);
+  { uint64_t x585; uint8_t x586 = _addcarryx_u64(x583, x510, x558, &x585);
+  { uint64_t x588; uint8_t x589 = _addcarryx_u64(x586, x513, x561, &x588);
+  { uint64_t x591; uint8_t x592 = _addcarryx_u64(x589, x516, x564, &x591);
+  { uint64_t x594; uint8_t x595 = _addcarryx_u64(x592, x519, x567, &x594);
+  { uint64_t x597; uint8_t x598 = _addcarryx_u64(x595, x522, x570, &x597);
+  { uint64_t x600; uint8_t x601 = _addcarryx_u64(x598, x525, x573, &x600);
+  { uint64_t x603; uint8_t x604 = _addcarryx_u64(x601, x528, x576, &x603);
+  { uint64_t x606; uint8_t x607 = _addcarryx_u64(x604, x531, x579, &x606);
+  { uint8_t x608 = (x607 + x532);
+  { uint64_t x611;  uint64_t x610 = _mulx_u64(x13, x19, &x611);
+  { uint64_t x614;  uint64_t x613 = _mulx_u64(x13, x21, &x614);
+  { uint64_t x617;  uint64_t x616 = _mulx_u64(x13, x23, &x617);
+  { uint64_t x620;  uint64_t x619 = _mulx_u64(x13, x25, &x620);
+  { uint64_t x623;  uint64_t x622 = _mulx_u64(x13, x27, &x623);
+  { uint64_t x626;  uint64_t x625 = _mulx_u64(x13, x29, &x626);
+  { uint64_t x629;  uint64_t x628 = _mulx_u64(x13, x31, &x629);
+  { uint64_t x632;  uint64_t x631 = _mulx_u64(x13, x30, &x632);
+  { uint64_t x634; uint8_t x635 = _addcarryx_u64(0x0, x611, x613, &x634);
+  { uint64_t x637; uint8_t x638 = _addcarryx_u64(x635, x614, x616, &x637);
+  { uint64_t x640; uint8_t x641 = _addcarryx_u64(x638, x617, x619, &x640);
+  { uint64_t x643; uint8_t x644 = _addcarryx_u64(x641, x620, x622, &x643);
+  { uint64_t x646; uint8_t x647 = _addcarryx_u64(x644, x623, x625, &x646);
+  { uint64_t x649; uint8_t x650 = _addcarryx_u64(x647, x626, x628, &x649);
+  { uint64_t x652; uint8_t x653 = _addcarryx_u64(x650, x629, x631, &x652);
+  { uint64_t x655; uint8_t _ = _addcarryx_u64(0x0, x653, x632, &x655);
+  { uint64_t x658; uint8_t x659 = _addcarryx_u64(0x0, x585, x610, &x658);
+  { uint64_t x661; uint8_t x662 = _addcarryx_u64(x659, x588, x634, &x661);
+  { uint64_t x664; uint8_t x665 = _addcarryx_u64(x662, x591, x637, &x664);
+  { uint64_t x667; uint8_t x668 = _addcarryx_u64(x665, x594, x640, &x667);
+  { uint64_t x670; uint8_t x671 = _addcarryx_u64(x668, x597, x643, &x670);
+  { uint64_t x673; uint8_t x674 = _addcarryx_u64(x671, x600, x646, &x673);
+  { uint64_t x676; uint8_t x677 = _addcarryx_u64(x674, x603, x649, &x676);
+  { uint64_t x679; uint8_t x680 = _addcarryx_u64(x677, x606, x652, &x679);
+  { uint64_t x682; uint8_t x683 = _addcarryx_u64(x680, x608, x655, &x682);
+  { uint64_t x686;  uint64_t x685 = _mulx_u64(x658, 0xffffffffffffffffL, &x686);
+  { uint64_t x689;  uint64_t x688 = _mulx_u64(x658, 0xffffffffffffffffL, &x689);
+  { uint64_t x692;  uint64_t x691 = _mulx_u64(x658, 0xffffffffffffffffL, &x692);
+  { uint64_t x695;  uint64_t x694 = _mulx_u64(x658, 0xffffffffffffffffL, &x695);
+  { uint64_t x698;  uint64_t x697 = _mulx_u64(x658, 0xffffffffffffffffL, &x698);
+  { uint64_t x701;  uint64_t x700 = _mulx_u64(x658, 0xffffffffffffffffL, &x701);
+  { uint64_t x704;  uint64_t x703 = _mulx_u64(x658, 0xffffffffffffffffL, &x704);
+  { uint64_t x707;  uint64_t x706 = _mulx_u64(x658, 0xfe14ffffffffffffL, &x707);
+  { uint64_t x709; uint8_t x710 = _addcarryx_u64(0x0, x686, x688, &x709);
+  { uint64_t x712; uint8_t x713 = _addcarryx_u64(x710, x689, x691, &x712);
+  { uint64_t x715; uint8_t x716 = _addcarryx_u64(x713, x692, x694, &x715);
+  { uint64_t x718; uint8_t x719 = _addcarryx_u64(x716, x695, x697, &x718);
+  { uint64_t x721; uint8_t x722 = _addcarryx_u64(x719, x698, x700, &x721);
+  { uint64_t x724; uint8_t x725 = _addcarryx_u64(x722, x701, x703, &x724);
+  { uint64_t x727; uint8_t x728 = _addcarryx_u64(x725, x704, x706, &x727);
+  { uint64_t x730; uint8_t _ = _addcarryx_u64(0x0, x728, x707, &x730);
+  { uint64_t _; uint8_t x734 = _addcarryx_u64(0x0, x658, x685, &_);
+  { uint64_t x736; uint8_t x737 = _addcarryx_u64(x734, x661, x709, &x736);
+  { uint64_t x739; uint8_t x740 = _addcarryx_u64(x737, x664, x712, &x739);
+  { uint64_t x742; uint8_t x743 = _addcarryx_u64(x740, x667, x715, &x742);
+  { uint64_t x745; uint8_t x746 = _addcarryx_u64(x743, x670, x718, &x745);
+  { uint64_t x748; uint8_t x749 = _addcarryx_u64(x746, x673, x721, &x748);
+  { uint64_t x751; uint8_t x752 = _addcarryx_u64(x749, x676, x724, &x751);
+  { uint64_t x754; uint8_t x755 = _addcarryx_u64(x752, x679, x727, &x754);
+  { uint64_t x757; uint8_t x758 = _addcarryx_u64(x755, x682, x730, &x757);
+  { uint8_t x759 = (x758 + x683);
+  { uint64_t x762;  uint64_t x761 = _mulx_u64(x15, x19, &x762);
+  { uint64_t x765;  uint64_t x764 = _mulx_u64(x15, x21, &x765);
+  { uint64_t x768;  uint64_t x767 = _mulx_u64(x15, x23, &x768);
+  { uint64_t x771;  uint64_t x770 = _mulx_u64(x15, x25, &x771);
+  { uint64_t x774;  uint64_t x773 = _mulx_u64(x15, x27, &x774);
+  { uint64_t x777;  uint64_t x776 = _mulx_u64(x15, x29, &x777);
+  { uint64_t x780;  uint64_t x779 = _mulx_u64(x15, x31, &x780);
+  { uint64_t x783;  uint64_t x782 = _mulx_u64(x15, x30, &x783);
+  { uint64_t x785; uint8_t x786 = _addcarryx_u64(0x0, x762, x764, &x785);
+  { uint64_t x788; uint8_t x789 = _addcarryx_u64(x786, x765, x767, &x788);
+  { uint64_t x791; uint8_t x792 = _addcarryx_u64(x789, x768, x770, &x791);
+  { uint64_t x794; uint8_t x795 = _addcarryx_u64(x792, x771, x773, &x794);
+  { uint64_t x797; uint8_t x798 = _addcarryx_u64(x795, x774, x776, &x797);
+  { uint64_t x800; uint8_t x801 = _addcarryx_u64(x798, x777, x779, &x800);
+  { uint64_t x803; uint8_t x804 = _addcarryx_u64(x801, x780, x782, &x803);
+  { uint64_t x806; uint8_t _ = _addcarryx_u64(0x0, x804, x783, &x806);
+  { uint64_t x809; uint8_t x810 = _addcarryx_u64(0x0, x736, x761, &x809);
+  { uint64_t x812; uint8_t x813 = _addcarryx_u64(x810, x739, x785, &x812);
+  { uint64_t x815; uint8_t x816 = _addcarryx_u64(x813, x742, x788, &x815);
+  { uint64_t x818; uint8_t x819 = _addcarryx_u64(x816, x745, x791, &x818);
+  { uint64_t x821; uint8_t x822 = _addcarryx_u64(x819, x748, x794, &x821);
+  { uint64_t x824; uint8_t x825 = _addcarryx_u64(x822, x751, x797, &x824);
+  { uint64_t x827; uint8_t x828 = _addcarryx_u64(x825, x754, x800, &x827);
+  { uint64_t x830; uint8_t x831 = _addcarryx_u64(x828, x757, x803, &x830);
+  { uint64_t x833; uint8_t x834 = _addcarryx_u64(x831, x759, x806, &x833);
+  { uint64_t x837;  uint64_t x836 = _mulx_u64(x809, 0xffffffffffffffffL, &x837);
+  { uint64_t x840;  uint64_t x839 = _mulx_u64(x809, 0xffffffffffffffffL, &x840);
+  { uint64_t x843;  uint64_t x842 = _mulx_u64(x809, 0xffffffffffffffffL, &x843);
+  { uint64_t x846;  uint64_t x845 = _mulx_u64(x809, 0xffffffffffffffffL, &x846);
+  { uint64_t x849;  uint64_t x848 = _mulx_u64(x809, 0xffffffffffffffffL, &x849);
+  { uint64_t x852;  uint64_t x851 = _mulx_u64(x809, 0xffffffffffffffffL, &x852);
+  { uint64_t x855;  uint64_t x854 = _mulx_u64(x809, 0xffffffffffffffffL, &x855);
+  { uint64_t x858;  uint64_t x857 = _mulx_u64(x809, 0xfe14ffffffffffffL, &x858);
+  { uint64_t x860; uint8_t x861 = _addcarryx_u64(0x0, x837, x839, &x860);
+  { uint64_t x863; uint8_t x864 = _addcarryx_u64(x861, x840, x842, &x863);
+  { uint64_t x866; uint8_t x867 = _addcarryx_u64(x864, x843, x845, &x866);
+  { uint64_t x869; uint8_t x870 = _addcarryx_u64(x867, x846, x848, &x869);
+  { uint64_t x872; uint8_t x873 = _addcarryx_u64(x870, x849, x851, &x872);
+  { uint64_t x875; uint8_t x876 = _addcarryx_u64(x873, x852, x854, &x875);
+  { uint64_t x878; uint8_t x879 = _addcarryx_u64(x876, x855, x857, &x878);
+  { uint64_t x881; uint8_t _ = _addcarryx_u64(0x0, x879, x858, &x881);
+  { uint64_t _; uint8_t x885 = _addcarryx_u64(0x0, x809, x836, &_);
+  { uint64_t x887; uint8_t x888 = _addcarryx_u64(x885, x812, x860, &x887);
+  { uint64_t x890; uint8_t x891 = _addcarryx_u64(x888, x815, x863, &x890);
+  { uint64_t x893; uint8_t x894 = _addcarryx_u64(x891, x818, x866, &x893);
+  { uint64_t x896; uint8_t x897 = _addcarryx_u64(x894, x821, x869, &x896);
+  { uint64_t x899; uint8_t x900 = _addcarryx_u64(x897, x824, x872, &x899);
+  { uint64_t x902; uint8_t x903 = _addcarryx_u64(x900, x827, x875, &x902);
+  { uint64_t x905; uint8_t x906 = _addcarryx_u64(x903, x830, x878, &x905);
+  { uint64_t x908; uint8_t x909 = _addcarryx_u64(x906, x833, x881, &x908);
+  { uint8_t x910 = (x909 + x834);
+  { uint64_t x913;  uint64_t x912 = _mulx_u64(x17, x19, &x913);
+  { uint64_t x916;  uint64_t x915 = _mulx_u64(x17, x21, &x916);
+  { uint64_t x919;  uint64_t x918 = _mulx_u64(x17, x23, &x919);
+  { uint64_t x922;  uint64_t x921 = _mulx_u64(x17, x25, &x922);
+  { uint64_t x925;  uint64_t x924 = _mulx_u64(x17, x27, &x925);
+  { uint64_t x928;  uint64_t x927 = _mulx_u64(x17, x29, &x928);
+  { uint64_t x931;  uint64_t x930 = _mulx_u64(x17, x31, &x931);
+  { uint64_t x934;  uint64_t x933 = _mulx_u64(x17, x30, &x934);
+  { uint64_t x936; uint8_t x937 = _addcarryx_u64(0x0, x913, x915, &x936);
+  { uint64_t x939; uint8_t x940 = _addcarryx_u64(x937, x916, x918, &x939);
+  { uint64_t x942; uint8_t x943 = _addcarryx_u64(x940, x919, x921, &x942);
+  { uint64_t x945; uint8_t x946 = _addcarryx_u64(x943, x922, x924, &x945);
+  { uint64_t x948; uint8_t x949 = _addcarryx_u64(x946, x925, x927, &x948);
+  { uint64_t x951; uint8_t x952 = _addcarryx_u64(x949, x928, x930, &x951);
+  { uint64_t x954; uint8_t x955 = _addcarryx_u64(x952, x931, x933, &x954);
+  { uint64_t x957; uint8_t _ = _addcarryx_u64(0x0, x955, x934, &x957);
+  { uint64_t x960; uint8_t x961 = _addcarryx_u64(0x0, x887, x912, &x960);
+  { uint64_t x963; uint8_t x964 = _addcarryx_u64(x961, x890, x936, &x963);
+  { uint64_t x966; uint8_t x967 = _addcarryx_u64(x964, x893, x939, &x966);
+  { uint64_t x969; uint8_t x970 = _addcarryx_u64(x967, x896, x942, &x969);
+  { uint64_t x972; uint8_t x973 = _addcarryx_u64(x970, x899, x945, &x972);
+  { uint64_t x975; uint8_t x976 = _addcarryx_u64(x973, x902, x948, &x975);
+  { uint64_t x978; uint8_t x979 = _addcarryx_u64(x976, x905, x951, &x978);
+  { uint64_t x981; uint8_t x982 = _addcarryx_u64(x979, x908, x954, &x981);
+  { uint64_t x984; uint8_t x985 = _addcarryx_u64(x982, x910, x957, &x984);
+  { uint64_t x988;  uint64_t x987 = _mulx_u64(x960, 0xffffffffffffffffL, &x988);
+  { uint64_t x991;  uint64_t x990 = _mulx_u64(x960, 0xffffffffffffffffL, &x991);
+  { uint64_t x994;  uint64_t x993 = _mulx_u64(x960, 0xffffffffffffffffL, &x994);
+  { uint64_t x997;  uint64_t x996 = _mulx_u64(x960, 0xffffffffffffffffL, &x997);
+  { uint64_t x1000;  uint64_t x999 = _mulx_u64(x960, 0xffffffffffffffffL, &x1000);
+  { uint64_t x1003;  uint64_t x1002 = _mulx_u64(x960, 0xffffffffffffffffL, &x1003);
+  { uint64_t x1006;  uint64_t x1005 = _mulx_u64(x960, 0xffffffffffffffffL, &x1006);
+  { uint64_t x1009;  uint64_t x1008 = _mulx_u64(x960, 0xfe14ffffffffffffL, &x1009);
+  { uint64_t x1011; uint8_t x1012 = _addcarryx_u64(0x0, x988, x990, &x1011);
+  { uint64_t x1014; uint8_t x1015 = _addcarryx_u64(x1012, x991, x993, &x1014);
+  { uint64_t x1017; uint8_t x1018 = _addcarryx_u64(x1015, x994, x996, &x1017);
+  { uint64_t x1020; uint8_t x1021 = _addcarryx_u64(x1018, x997, x999, &x1020);
+  { uint64_t x1023; uint8_t x1024 = _addcarryx_u64(x1021, x1000, x1002, &x1023);
+  { uint64_t x1026; uint8_t x1027 = _addcarryx_u64(x1024, x1003, x1005, &x1026);
+  { uint64_t x1029; uint8_t x1030 = _addcarryx_u64(x1027, x1006, x1008, &x1029);
+  { uint64_t x1032; uint8_t _ = _addcarryx_u64(0x0, x1030, x1009, &x1032);
+  { uint64_t _; uint8_t x1036 = _addcarryx_u64(0x0, x960, x987, &_);
+  { uint64_t x1038; uint8_t x1039 = _addcarryx_u64(x1036, x963, x1011, &x1038);
+  { uint64_t x1041; uint8_t x1042 = _addcarryx_u64(x1039, x966, x1014, &x1041);
+  { uint64_t x1044; uint8_t x1045 = _addcarryx_u64(x1042, x969, x1017, &x1044);
+  { uint64_t x1047; uint8_t x1048 = _addcarryx_u64(x1045, x972, x1020, &x1047);
+  { uint64_t x1050; uint8_t x1051 = _addcarryx_u64(x1048, x975, x1023, &x1050);
+  { uint64_t x1053; uint8_t x1054 = _addcarryx_u64(x1051, x978, x1026, &x1053);
+  { uint64_t x1056; uint8_t x1057 = _addcarryx_u64(x1054, x981, x1029, &x1056);
+  { uint64_t x1059; uint8_t x1060 = _addcarryx_u64(x1057, x984, x1032, &x1059);
+  { uint8_t x1061 = (x1060 + x985);
+  { uint64_t x1064;  uint64_t x1063 = _mulx_u64(x16, x19, &x1064);
+  { uint64_t x1067;  uint64_t x1066 = _mulx_u64(x16, x21, &x1067);
+  { uint64_t x1070;  uint64_t x1069 = _mulx_u64(x16, x23, &x1070);
+  { uint64_t x1073;  uint64_t x1072 = _mulx_u64(x16, x25, &x1073);
+  { uint64_t x1076;  uint64_t x1075 = _mulx_u64(x16, x27, &x1076);
+  { uint64_t x1079;  uint64_t x1078 = _mulx_u64(x16, x29, &x1079);
+  { uint64_t x1082;  uint64_t x1081 = _mulx_u64(x16, x31, &x1082);
+  { uint64_t x1085;  uint64_t x1084 = _mulx_u64(x16, x30, &x1085);
+  { uint64_t x1087; uint8_t x1088 = _addcarryx_u64(0x0, x1064, x1066, &x1087);
+  { uint64_t x1090; uint8_t x1091 = _addcarryx_u64(x1088, x1067, x1069, &x1090);
+  { uint64_t x1093; uint8_t x1094 = _addcarryx_u64(x1091, x1070, x1072, &x1093);
+  { uint64_t x1096; uint8_t x1097 = _addcarryx_u64(x1094, x1073, x1075, &x1096);
+  { uint64_t x1099; uint8_t x1100 = _addcarryx_u64(x1097, x1076, x1078, &x1099);
+  { uint64_t x1102; uint8_t x1103 = _addcarryx_u64(x1100, x1079, x1081, &x1102);
+  { uint64_t x1105; uint8_t x1106 = _addcarryx_u64(x1103, x1082, x1084, &x1105);
+  { uint64_t x1108; uint8_t _ = _addcarryx_u64(0x0, x1106, x1085, &x1108);
+  { uint64_t x1111; uint8_t x1112 = _addcarryx_u64(0x0, x1038, x1063, &x1111);
+  { uint64_t x1114; uint8_t x1115 = _addcarryx_u64(x1112, x1041, x1087, &x1114);
+  { uint64_t x1117; uint8_t x1118 = _addcarryx_u64(x1115, x1044, x1090, &x1117);
+  { uint64_t x1120; uint8_t x1121 = _addcarryx_u64(x1118, x1047, x1093, &x1120);
+  { uint64_t x1123; uint8_t x1124 = _addcarryx_u64(x1121, x1050, x1096, &x1123);
+  { uint64_t x1126; uint8_t x1127 = _addcarryx_u64(x1124, x1053, x1099, &x1126);
+  { uint64_t x1129; uint8_t x1130 = _addcarryx_u64(x1127, x1056, x1102, &x1129);
+  { uint64_t x1132; uint8_t x1133 = _addcarryx_u64(x1130, x1059, x1105, &x1132);
+  { uint64_t x1135; uint8_t x1136 = _addcarryx_u64(x1133, x1061, x1108, &x1135);
+  { uint64_t x1139;  uint64_t x1138 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1139);
+  { uint64_t x1142;  uint64_t x1141 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1142);
+  { uint64_t x1145;  uint64_t x1144 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1145);
+  { uint64_t x1148;  uint64_t x1147 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1148);
+  { uint64_t x1151;  uint64_t x1150 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1151);
+  { uint64_t x1154;  uint64_t x1153 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1154);
+  { uint64_t x1157;  uint64_t x1156 = _mulx_u64(x1111, 0xffffffffffffffffL, &x1157);
+  { uint64_t x1160;  uint64_t x1159 = _mulx_u64(x1111, 0xfe14ffffffffffffL, &x1160);
+  { uint64_t x1162; uint8_t x1163 = _addcarryx_u64(0x0, x1139, x1141, &x1162);
+  { uint64_t x1165; uint8_t x1166 = _addcarryx_u64(x1163, x1142, x1144, &x1165);
+  { uint64_t x1168; uint8_t x1169 = _addcarryx_u64(x1166, x1145, x1147, &x1168);
+  { uint64_t x1171; uint8_t x1172 = _addcarryx_u64(x1169, x1148, x1150, &x1171);
+  { uint64_t x1174; uint8_t x1175 = _addcarryx_u64(x1172, x1151, x1153, &x1174);
+  { uint64_t x1177; uint8_t x1178 = _addcarryx_u64(x1175, x1154, x1156, &x1177);
+  { uint64_t x1180; uint8_t x1181 = _addcarryx_u64(x1178, x1157, x1159, &x1180);
+  { uint64_t x1183; uint8_t _ = _addcarryx_u64(0x0, x1181, x1160, &x1183);
+  { uint64_t _; uint8_t x1187 = _addcarryx_u64(0x0, x1111, x1138, &_);
+  { uint64_t x1189; uint8_t x1190 = _addcarryx_u64(x1187, x1114, x1162, &x1189);
+  { uint64_t x1192; uint8_t x1193 = _addcarryx_u64(x1190, x1117, x1165, &x1192);
+  { uint64_t x1195; uint8_t x1196 = _addcarryx_u64(x1193, x1120, x1168, &x1195);
+  { uint64_t x1198; uint8_t x1199 = _addcarryx_u64(x1196, x1123, x1171, &x1198);
+  { uint64_t x1201; uint8_t x1202 = _addcarryx_u64(x1199, x1126, x1174, &x1201);
+  { uint64_t x1204; uint8_t x1205 = _addcarryx_u64(x1202, x1129, x1177, &x1204);
+  { uint64_t x1207; uint8_t x1208 = _addcarryx_u64(x1205, x1132, x1180, &x1207);
+  { uint64_t x1210; uint8_t x1211 = _addcarryx_u64(x1208, x1135, x1183, &x1210);
+  { uint8_t x1212 = (x1211 + x1136);
+  { uint64_t x1214; uint8_t x1215 = _subborrow_u64(0x0, x1189, 0xffffffffffffffffL, &x1214);
+  { uint64_t x1217; uint8_t x1218 = _subborrow_u64(x1215, x1192, 0xffffffffffffffffL, &x1217);
+  { uint64_t x1220; uint8_t x1221 = _subborrow_u64(x1218, x1195, 0xffffffffffffffffL, &x1220);
+  { uint64_t x1223; uint8_t x1224 = _subborrow_u64(x1221, x1198, 0xffffffffffffffffL, &x1223);
+  { uint64_t x1226; uint8_t x1227 = _subborrow_u64(x1224, x1201, 0xffffffffffffffffL, &x1226);
+  { uint64_t x1229; uint8_t x1230 = _subborrow_u64(x1227, x1204, 0xffffffffffffffffL, &x1229);
+  { uint64_t x1232; uint8_t x1233 = _subborrow_u64(x1230, x1207, 0xffffffffffffffffL, &x1232);
+  { uint64_t x1235; uint8_t x1236 = _subborrow_u64(x1233, x1210, 0xfe14ffffffffffffL, &x1235);
+  { 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);
+  out[0] = x1247;
+  out[1] = x1246;
+  out[2] = x1245;
+  out[3] = x1244;
+  out[4] = x1243;
+  out[5] = x1242;
+  out[6] = x1241;
+  out[7] = x1240;
+  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femulDisplay.log b/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femulDisplay.log
new file mode 100644
index 000000000..aca3dfe9b
--- /dev/null
+++ b/src/Specific/montgomery64_2e512m491x2e496m1_8limbs/femulDisplay.log
@@ -0,0 +1,423 @@
+λ 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)
author	Andres Erbsen <andreser@google.com>	2017-11-15 20:04:11 +0000
committer	Andres Erbsen <andreser@google.com>	2017-11-15 20:04:11 +0000
commit	ba11f2c1999e845180da3ea770e3c8309aa18c60 (patch)
tree	95bb6bdc59f81aa29f63a5e51baebcdb62c40281 /src
parent	fc4765b347fa561b7ba6e909ce771788848861ef (diff)