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