aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/montgomery32_2e166m5_6limbs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Specific/montgomery32_2e166m5_6limbs')
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/femul.c266
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/femulDisplay.log252
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/feopp.c34
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/feoppDisplay.log26
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/fesub.c40
-rw-r--r--src/Specific/montgomery32_2e166m5_6limbs/fesubDisplay.log26
6 files changed, 644 insertions, 0 deletions
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/femul.c b/src/Specific/montgomery32_2e166m5_6limbs/femul.c
new file mode 100644
index 000000000..b834472fd
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/femul.c
@@ -0,0 +1,266 @@
+static void femul(uint32_t out[6], const uint32_t in1[6], const uint32_t in2[6]) {
+ { const uint32_t x12 = 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 x22 = in2[5];
+ { const uint32_t x23 = in2[4];
+ { const uint32_t x21 = in2[3];
+ { const uint32_t x19 = in2[2];
+ { const uint32_t x17 = in2[1];
+ { const uint32_t x15 = in2[0];
+ { uint32_t x26; uint32_t x25 = _mulx_u32(x5, x15, &x26);
+ { uint32_t x29; uint32_t x28 = _mulx_u32(x5, x17, &x29);
+ { uint32_t x32; uint32_t x31 = _mulx_u32(x5, x19, &x32);
+ { uint32_t x35; uint32_t x34 = _mulx_u32(x5, x21, &x35);
+ { uint32_t x38; uint32_t x37 = _mulx_u32(x5, x23, &x38);
+ { uint32_t x41; uint32_t x40 = _mulx_u32(x5, x22, &x41);
+ { uint32_t x43; uint8_t x44 = _addcarryx_u32(0x0, x26, x28, &x43);
+ { uint32_t x46; uint8_t x47 = _addcarryx_u32(x44, x29, x31, &x46);
+ { uint32_t x49; uint8_t x50 = _addcarryx_u32(x47, x32, x34, &x49);
+ { uint32_t x52; uint8_t x53 = _addcarryx_u32(x50, x35, x37, &x52);
+ { uint32_t x55; uint8_t x56 = _addcarryx_u32(x53, x38, x40, &x55);
+ { uint32_t x58; uint8_t _ = _addcarryx_u32(0x0, x56, x41, &x58);
+ { uint32_t _; uint32_t x61 = _mulx_u32(x25, 0xcccccccd, &_);
+ { uint32_t x65; uint32_t x64 = _mulx_u32(x61, 0xfffffffb, &x65);
+ { uint32_t x68; uint32_t x67 = _mulx_u32(x61, 0xffffffff, &x68);
+ { uint32_t x71; uint32_t x70 = _mulx_u32(x61, 0xffffffff, &x71);
+ { uint32_t x74; uint32_t x73 = _mulx_u32(x61, 0xffffffff, &x74);
+ { uint32_t x77; uint32_t x76 = _mulx_u32(x61, 0xffffffff, &x77);
+ { uint8_t x80; uint32_t x79 = _mulx_u32_out_u8(x61, 0x3f, &x80);
+ { uint32_t x82; uint8_t x83 = _addcarryx_u32(0x0, x65, x67, &x82);
+ { uint32_t x85; uint8_t x86 = _addcarryx_u32(x83, x68, x70, &x85);
+ { uint32_t x88; uint8_t x89 = _addcarryx_u32(x86, x71, x73, &x88);
+ { uint32_t x91; uint8_t x92 = _addcarryx_u32(x89, x74, x76, &x91);
+ { uint32_t x94; uint8_t x95 = _addcarryx_u32(x92, x77, x79, &x94);
+ { uint8_t x96 = (x95 + x80);
+ { uint32_t _; uint8_t x99 = _addcarryx_u32(0x0, x25, x64, &_);
+ { uint32_t x101; uint8_t x102 = _addcarryx_u32(x99, x43, x82, &x101);
+ { uint32_t x104; uint8_t x105 = _addcarryx_u32(x102, x46, x85, &x104);
+ { uint32_t x107; uint8_t x108 = _addcarryx_u32(x105, x49, x88, &x107);
+ { uint32_t x110; uint8_t x111 = _addcarryx_u32(x108, x52, x91, &x110);
+ { uint32_t x113; uint8_t x114 = _addcarryx_u32(x111, x55, x94, &x113);
+ { uint32_t x116; uint8_t x117 = _addcarryx_u32(x114, x58, x96, &x116);
+ { uint32_t x120; uint32_t x119 = _mulx_u32(x7, x15, &x120);
+ { uint32_t x123; uint32_t x122 = _mulx_u32(x7, x17, &x123);
+ { uint32_t x126; uint32_t x125 = _mulx_u32(x7, x19, &x126);
+ { uint32_t x129; uint32_t x128 = _mulx_u32(x7, x21, &x129);
+ { uint32_t x132; uint32_t x131 = _mulx_u32(x7, x23, &x132);
+ { uint32_t x135; uint32_t x134 = _mulx_u32(x7, x22, &x135);
+ { uint32_t x137; uint8_t x138 = _addcarryx_u32(0x0, x120, x122, &x137);
+ { uint32_t x140; uint8_t x141 = _addcarryx_u32(x138, x123, x125, &x140);
+ { uint32_t x143; uint8_t x144 = _addcarryx_u32(x141, x126, x128, &x143);
+ { uint32_t x146; uint8_t x147 = _addcarryx_u32(x144, x129, x131, &x146);
+ { uint32_t x149; uint8_t x150 = _addcarryx_u32(x147, x132, x134, &x149);
+ { uint32_t x152; uint8_t _ = _addcarryx_u32(0x0, x150, x135, &x152);
+ { uint32_t x155; uint8_t x156 = _addcarryx_u32(0x0, x101, x119, &x155);
+ { uint32_t x158; uint8_t x159 = _addcarryx_u32(x156, x104, x137, &x158);
+ { uint32_t x161; uint8_t x162 = _addcarryx_u32(x159, x107, x140, &x161);
+ { uint32_t x164; uint8_t x165 = _addcarryx_u32(x162, x110, x143, &x164);
+ { uint32_t x167; uint8_t x168 = _addcarryx_u32(x165, x113, x146, &x167);
+ { uint32_t x170; uint8_t x171 = _addcarryx_u32(x168, x116, x149, &x170);
+ { uint32_t x173; uint8_t x174 = _addcarryx_u32(x171, x117, x152, &x173);
+ { uint32_t _; uint32_t x176 = _mulx_u32(x155, 0xcccccccd, &_);
+ { uint32_t x180; uint32_t x179 = _mulx_u32(x176, 0xfffffffb, &x180);
+ { uint32_t x183; uint32_t x182 = _mulx_u32(x176, 0xffffffff, &x183);
+ { uint32_t x186; uint32_t x185 = _mulx_u32(x176, 0xffffffff, &x186);
+ { uint32_t x189; uint32_t x188 = _mulx_u32(x176, 0xffffffff, &x189);
+ { uint32_t x192; uint32_t x191 = _mulx_u32(x176, 0xffffffff, &x192);
+ { uint8_t x195; uint32_t x194 = _mulx_u32_out_u8(x176, 0x3f, &x195);
+ { uint32_t x197; uint8_t x198 = _addcarryx_u32(0x0, x180, x182, &x197);
+ { uint32_t x200; uint8_t x201 = _addcarryx_u32(x198, x183, x185, &x200);
+ { uint32_t x203; uint8_t x204 = _addcarryx_u32(x201, x186, x188, &x203);
+ { uint32_t x206; uint8_t x207 = _addcarryx_u32(x204, x189, x191, &x206);
+ { uint32_t x209; uint8_t x210 = _addcarryx_u32(x207, x192, x194, &x209);
+ { uint8_t x211 = (x210 + x195);
+ { uint32_t _; uint8_t x214 = _addcarryx_u32(0x0, x155, x179, &_);
+ { uint32_t x216; uint8_t x217 = _addcarryx_u32(x214, x158, x197, &x216);
+ { uint32_t x219; uint8_t x220 = _addcarryx_u32(x217, x161, x200, &x219);
+ { uint32_t x222; uint8_t x223 = _addcarryx_u32(x220, x164, x203, &x222);
+ { uint32_t x225; uint8_t x226 = _addcarryx_u32(x223, x167, x206, &x225);
+ { uint32_t x228; uint8_t x229 = _addcarryx_u32(x226, x170, x209, &x228);
+ { uint32_t x231; uint8_t x232 = _addcarryx_u32(x229, x173, x211, &x231);
+ { uint8_t x233 = (x232 + x174);
+ { uint32_t x236; uint32_t x235 = _mulx_u32(x9, x15, &x236);
+ { uint32_t x239; uint32_t x238 = _mulx_u32(x9, x17, &x239);
+ { uint32_t x242; uint32_t x241 = _mulx_u32(x9, x19, &x242);
+ { uint32_t x245; uint32_t x244 = _mulx_u32(x9, x21, &x245);
+ { uint32_t x248; uint32_t x247 = _mulx_u32(x9, x23, &x248);
+ { uint32_t x251; uint32_t x250 = _mulx_u32(x9, x22, &x251);
+ { uint32_t x253; uint8_t x254 = _addcarryx_u32(0x0, x236, x238, &x253);
+ { uint32_t x256; uint8_t x257 = _addcarryx_u32(x254, x239, x241, &x256);
+ { uint32_t x259; uint8_t x260 = _addcarryx_u32(x257, x242, x244, &x259);
+ { uint32_t x262; uint8_t x263 = _addcarryx_u32(x260, x245, x247, &x262);
+ { uint32_t x265; uint8_t x266 = _addcarryx_u32(x263, x248, x250, &x265);
+ { uint32_t x268; uint8_t _ = _addcarryx_u32(0x0, x266, x251, &x268);
+ { uint32_t x271; uint8_t x272 = _addcarryx_u32(0x0, x216, x235, &x271);
+ { uint32_t x274; uint8_t x275 = _addcarryx_u32(x272, x219, x253, &x274);
+ { uint32_t x277; uint8_t x278 = _addcarryx_u32(x275, x222, x256, &x277);
+ { uint32_t x280; uint8_t x281 = _addcarryx_u32(x278, x225, x259, &x280);
+ { uint32_t x283; uint8_t x284 = _addcarryx_u32(x281, x228, x262, &x283);
+ { uint32_t x286; uint8_t x287 = _addcarryx_u32(x284, x231, x265, &x286);
+ { uint32_t x289; uint8_t x290 = _addcarryx_u32(x287, x233, x268, &x289);
+ { uint32_t _; uint32_t x292 = _mulx_u32(x271, 0xcccccccd, &_);
+ { uint32_t x296; uint32_t x295 = _mulx_u32(x292, 0xfffffffb, &x296);
+ { uint32_t x299; uint32_t x298 = _mulx_u32(x292, 0xffffffff, &x299);
+ { uint32_t x302; uint32_t x301 = _mulx_u32(x292, 0xffffffff, &x302);
+ { uint32_t x305; uint32_t x304 = _mulx_u32(x292, 0xffffffff, &x305);
+ { uint32_t x308; uint32_t x307 = _mulx_u32(x292, 0xffffffff, &x308);
+ { uint8_t x311; uint32_t x310 = _mulx_u32_out_u8(x292, 0x3f, &x311);
+ { uint32_t x313; uint8_t x314 = _addcarryx_u32(0x0, x296, x298, &x313);
+ { uint32_t x316; uint8_t x317 = _addcarryx_u32(x314, x299, x301, &x316);
+ { uint32_t x319; uint8_t x320 = _addcarryx_u32(x317, x302, x304, &x319);
+ { uint32_t x322; uint8_t x323 = _addcarryx_u32(x320, x305, x307, &x322);
+ { uint32_t x325; uint8_t x326 = _addcarryx_u32(x323, x308, x310, &x325);
+ { uint8_t x327 = (x326 + x311);
+ { uint32_t _; uint8_t x330 = _addcarryx_u32(0x0, x271, x295, &_);
+ { uint32_t x332; uint8_t x333 = _addcarryx_u32(x330, x274, x313, &x332);
+ { uint32_t x335; uint8_t x336 = _addcarryx_u32(x333, x277, x316, &x335);
+ { uint32_t x338; uint8_t x339 = _addcarryx_u32(x336, x280, x319, &x338);
+ { uint32_t x341; uint8_t x342 = _addcarryx_u32(x339, x283, x322, &x341);
+ { uint32_t x344; uint8_t x345 = _addcarryx_u32(x342, x286, x325, &x344);
+ { uint32_t x347; uint8_t x348 = _addcarryx_u32(x345, x289, x327, &x347);
+ { uint8_t x349 = (x348 + x290);
+ { uint32_t x352; uint32_t x351 = _mulx_u32(x11, x15, &x352);
+ { uint32_t x355; uint32_t x354 = _mulx_u32(x11, x17, &x355);
+ { uint32_t x358; uint32_t x357 = _mulx_u32(x11, x19, &x358);
+ { uint32_t x361; uint32_t x360 = _mulx_u32(x11, x21, &x361);
+ { uint32_t x364; uint32_t x363 = _mulx_u32(x11, x23, &x364);
+ { uint32_t x367; uint32_t x366 = _mulx_u32(x11, x22, &x367);
+ { uint32_t x369; uint8_t x370 = _addcarryx_u32(0x0, x352, x354, &x369);
+ { uint32_t x372; uint8_t x373 = _addcarryx_u32(x370, x355, x357, &x372);
+ { uint32_t x375; uint8_t x376 = _addcarryx_u32(x373, x358, x360, &x375);
+ { uint32_t x378; uint8_t x379 = _addcarryx_u32(x376, x361, x363, &x378);
+ { uint32_t x381; uint8_t x382 = _addcarryx_u32(x379, x364, x366, &x381);
+ { uint32_t x384; uint8_t _ = _addcarryx_u32(0x0, x382, x367, &x384);
+ { uint32_t x387; uint8_t x388 = _addcarryx_u32(0x0, x332, x351, &x387);
+ { uint32_t x390; uint8_t x391 = _addcarryx_u32(x388, x335, x369, &x390);
+ { uint32_t x393; uint8_t x394 = _addcarryx_u32(x391, x338, x372, &x393);
+ { uint32_t x396; uint8_t x397 = _addcarryx_u32(x394, x341, x375, &x396);
+ { uint32_t x399; uint8_t x400 = _addcarryx_u32(x397, x344, x378, &x399);
+ { uint32_t x402; uint8_t x403 = _addcarryx_u32(x400, x347, x381, &x402);
+ { uint32_t x405; uint8_t x406 = _addcarryx_u32(x403, x349, x384, &x405);
+ { uint32_t _; uint32_t x408 = _mulx_u32(x387, 0xcccccccd, &_);
+ { uint32_t x412; uint32_t x411 = _mulx_u32(x408, 0xfffffffb, &x412);
+ { uint32_t x415; uint32_t x414 = _mulx_u32(x408, 0xffffffff, &x415);
+ { uint32_t x418; uint32_t x417 = _mulx_u32(x408, 0xffffffff, &x418);
+ { uint32_t x421; uint32_t x420 = _mulx_u32(x408, 0xffffffff, &x421);
+ { uint32_t x424; uint32_t x423 = _mulx_u32(x408, 0xffffffff, &x424);
+ { uint8_t x427; uint32_t x426 = _mulx_u32_out_u8(x408, 0x3f, &x427);
+ { uint32_t x429; uint8_t x430 = _addcarryx_u32(0x0, x412, x414, &x429);
+ { uint32_t x432; uint8_t x433 = _addcarryx_u32(x430, x415, x417, &x432);
+ { uint32_t x435; uint8_t x436 = _addcarryx_u32(x433, x418, x420, &x435);
+ { uint32_t x438; uint8_t x439 = _addcarryx_u32(x436, x421, x423, &x438);
+ { uint32_t x441; uint8_t x442 = _addcarryx_u32(x439, x424, x426, &x441);
+ { uint8_t x443 = (x442 + x427);
+ { uint32_t _; uint8_t x446 = _addcarryx_u32(0x0, x387, x411, &_);
+ { uint32_t x448; uint8_t x449 = _addcarryx_u32(x446, x390, x429, &x448);
+ { uint32_t x451; uint8_t x452 = _addcarryx_u32(x449, x393, x432, &x451);
+ { uint32_t x454; uint8_t x455 = _addcarryx_u32(x452, x396, x435, &x454);
+ { uint32_t x457; uint8_t x458 = _addcarryx_u32(x455, x399, x438, &x457);
+ { uint32_t x460; uint8_t x461 = _addcarryx_u32(x458, x402, x441, &x460);
+ { uint32_t x463; uint8_t x464 = _addcarryx_u32(x461, x405, x443, &x463);
+ { uint8_t x465 = (x464 + x406);
+ { uint32_t x468; uint32_t x467 = _mulx_u32(x13, x15, &x468);
+ { uint32_t x471; uint32_t x470 = _mulx_u32(x13, x17, &x471);
+ { uint32_t x474; uint32_t x473 = _mulx_u32(x13, x19, &x474);
+ { uint32_t x477; uint32_t x476 = _mulx_u32(x13, x21, &x477);
+ { uint32_t x480; uint32_t x479 = _mulx_u32(x13, x23, &x480);
+ { uint32_t x483; uint32_t x482 = _mulx_u32(x13, x22, &x483);
+ { uint32_t x485; uint8_t x486 = _addcarryx_u32(0x0, x468, x470, &x485);
+ { uint32_t x488; uint8_t x489 = _addcarryx_u32(x486, x471, x473, &x488);
+ { uint32_t x491; uint8_t x492 = _addcarryx_u32(x489, x474, x476, &x491);
+ { uint32_t x494; uint8_t x495 = _addcarryx_u32(x492, x477, x479, &x494);
+ { uint32_t x497; uint8_t x498 = _addcarryx_u32(x495, x480, x482, &x497);
+ { uint32_t x500; uint8_t _ = _addcarryx_u32(0x0, x498, x483, &x500);
+ { uint32_t x503; uint8_t x504 = _addcarryx_u32(0x0, x448, x467, &x503);
+ { uint32_t x506; uint8_t x507 = _addcarryx_u32(x504, x451, x485, &x506);
+ { uint32_t x509; uint8_t x510 = _addcarryx_u32(x507, x454, x488, &x509);
+ { uint32_t x512; uint8_t x513 = _addcarryx_u32(x510, x457, x491, &x512);
+ { uint32_t x515; uint8_t x516 = _addcarryx_u32(x513, x460, x494, &x515);
+ { uint32_t x518; uint8_t x519 = _addcarryx_u32(x516, x463, x497, &x518);
+ { uint32_t x521; uint8_t x522 = _addcarryx_u32(x519, x465, x500, &x521);
+ { uint32_t _; uint32_t x524 = _mulx_u32(x503, 0xcccccccd, &_);
+ { uint32_t x528; uint32_t x527 = _mulx_u32(x524, 0xfffffffb, &x528);
+ { uint32_t x531; uint32_t x530 = _mulx_u32(x524, 0xffffffff, &x531);
+ { uint32_t x534; uint32_t x533 = _mulx_u32(x524, 0xffffffff, &x534);
+ { uint32_t x537; uint32_t x536 = _mulx_u32(x524, 0xffffffff, &x537);
+ { uint32_t x540; uint32_t x539 = _mulx_u32(x524, 0xffffffff, &x540);
+ { uint8_t x543; uint32_t x542 = _mulx_u32_out_u8(x524, 0x3f, &x543);
+ { uint32_t x545; uint8_t x546 = _addcarryx_u32(0x0, x528, x530, &x545);
+ { uint32_t x548; uint8_t x549 = _addcarryx_u32(x546, x531, x533, &x548);
+ { uint32_t x551; uint8_t x552 = _addcarryx_u32(x549, x534, x536, &x551);
+ { uint32_t x554; uint8_t x555 = _addcarryx_u32(x552, x537, x539, &x554);
+ { uint32_t x557; uint8_t x558 = _addcarryx_u32(x555, x540, x542, &x557);
+ { uint8_t x559 = (x558 + x543);
+ { uint32_t _; uint8_t x562 = _addcarryx_u32(0x0, x503, x527, &_);
+ { uint32_t x564; uint8_t x565 = _addcarryx_u32(x562, x506, x545, &x564);
+ { uint32_t x567; uint8_t x568 = _addcarryx_u32(x565, x509, x548, &x567);
+ { uint32_t x570; uint8_t x571 = _addcarryx_u32(x568, x512, x551, &x570);
+ { uint32_t x573; uint8_t x574 = _addcarryx_u32(x571, x515, x554, &x573);
+ { uint32_t x576; uint8_t x577 = _addcarryx_u32(x574, x518, x557, &x576);
+ { uint32_t x579; uint8_t x580 = _addcarryx_u32(x577, x521, x559, &x579);
+ { uint8_t x581 = (x580 + x522);
+ { uint32_t x584; uint32_t x583 = _mulx_u32(x12, x15, &x584);
+ { uint32_t x587; uint32_t x586 = _mulx_u32(x12, x17, &x587);
+ { uint32_t x590; uint32_t x589 = _mulx_u32(x12, x19, &x590);
+ { uint32_t x593; uint32_t x592 = _mulx_u32(x12, x21, &x593);
+ { uint32_t x596; uint32_t x595 = _mulx_u32(x12, x23, &x596);
+ { uint32_t x599; uint32_t x598 = _mulx_u32(x12, x22, &x599);
+ { uint32_t x601; uint8_t x602 = _addcarryx_u32(0x0, x584, x586, &x601);
+ { uint32_t x604; uint8_t x605 = _addcarryx_u32(x602, x587, x589, &x604);
+ { uint32_t x607; uint8_t x608 = _addcarryx_u32(x605, x590, x592, &x607);
+ { uint32_t x610; uint8_t x611 = _addcarryx_u32(x608, x593, x595, &x610);
+ { uint32_t x613; uint8_t x614 = _addcarryx_u32(x611, x596, x598, &x613);
+ { uint32_t x616; uint8_t _ = _addcarryx_u32(0x0, x614, x599, &x616);
+ { uint32_t x619; uint8_t x620 = _addcarryx_u32(0x0, x564, x583, &x619);
+ { uint32_t x622; uint8_t x623 = _addcarryx_u32(x620, x567, x601, &x622);
+ { uint32_t x625; uint8_t x626 = _addcarryx_u32(x623, x570, x604, &x625);
+ { uint32_t x628; uint8_t x629 = _addcarryx_u32(x626, x573, x607, &x628);
+ { uint32_t x631; uint8_t x632 = _addcarryx_u32(x629, x576, x610, &x631);
+ { uint32_t x634; uint8_t x635 = _addcarryx_u32(x632, x579, x613, &x634);
+ { uint32_t x637; uint8_t x638 = _addcarryx_u32(x635, x581, x616, &x637);
+ { uint32_t _; uint32_t x640 = _mulx_u32(x619, 0xcccccccd, &_);
+ { uint32_t x644; uint32_t x643 = _mulx_u32(x640, 0xfffffffb, &x644);
+ { uint32_t x647; uint32_t x646 = _mulx_u32(x640, 0xffffffff, &x647);
+ { uint32_t x650; uint32_t x649 = _mulx_u32(x640, 0xffffffff, &x650);
+ { uint32_t x653; uint32_t x652 = _mulx_u32(x640, 0xffffffff, &x653);
+ { uint32_t x656; uint32_t x655 = _mulx_u32(x640, 0xffffffff, &x656);
+ { uint8_t x659; uint32_t x658 = _mulx_u32_out_u8(x640, 0x3f, &x659);
+ { uint32_t x661; uint8_t x662 = _addcarryx_u32(0x0, x644, x646, &x661);
+ { uint32_t x664; uint8_t x665 = _addcarryx_u32(x662, x647, x649, &x664);
+ { uint32_t x667; uint8_t x668 = _addcarryx_u32(x665, x650, x652, &x667);
+ { uint32_t x670; uint8_t x671 = _addcarryx_u32(x668, x653, x655, &x670);
+ { uint32_t x673; uint8_t x674 = _addcarryx_u32(x671, x656, x658, &x673);
+ { uint8_t x675 = (x674 + x659);
+ { uint32_t _; uint8_t x678 = _addcarryx_u32(0x0, x619, x643, &_);
+ { uint32_t x680; uint8_t x681 = _addcarryx_u32(x678, x622, x661, &x680);
+ { uint32_t x683; uint8_t x684 = _addcarryx_u32(x681, x625, x664, &x683);
+ { uint32_t x686; uint8_t x687 = _addcarryx_u32(x684, x628, x667, &x686);
+ { uint32_t x689; uint8_t x690 = _addcarryx_u32(x687, x631, x670, &x689);
+ { uint32_t x692; uint8_t x693 = _addcarryx_u32(x690, x634, x673, &x692);
+ { uint32_t x695; uint8_t x696 = _addcarryx_u32(x693, x637, x675, &x695);
+ { uint8_t x697 = (x696 + x638);
+ { uint32_t x699; uint8_t x700 = _subborrow_u32(0x0, x680, 0xfffffffb, &x699);
+ { uint32_t x702; uint8_t x703 = _subborrow_u32(x700, x683, 0xffffffff, &x702);
+ { uint32_t x705; uint8_t x706 = _subborrow_u32(x703, x686, 0xffffffff, &x705);
+ { uint32_t x708; uint8_t x709 = _subborrow_u32(x706, x689, 0xffffffff, &x708);
+ { uint32_t x711; uint8_t x712 = _subborrow_u32(x709, x692, 0xffffffff, &x711);
+ { uint32_t x714; uint8_t x715 = _subborrow_u32(x712, x695, 0x3f, &x714);
+ { uint32_t _; uint8_t x718 = _subborrow_u32(x715, x697, 0x0, &_);
+ { uint32_t x719 = cmovznz32(x718, x714, x695);
+ { uint32_t x720 = cmovznz32(x718, x711, x692);
+ { uint32_t x721 = cmovznz32(x718, x708, x689);
+ { uint32_t x722 = cmovznz32(x718, x705, x686);
+ { uint32_t x723 = cmovznz32(x718, x702, x683);
+ { uint32_t x724 = cmovznz32(x718, x699, x680);
+ out[0] = x724;
+ out[1] = x723;
+ out[2] = x722;
+ out[3] = x721;
+ out[4] = x720;
+ out[5] = x719;
+ }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/femulDisplay.log b/src/Specific/montgomery32_2e166m5_6limbs/femulDisplay.log
new file mode 100644
index 000000000..7202f403c
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/femulDisplay.log
@@ -0,0 +1,252 @@
+λ x x0 : word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
+ uint32_t x25, uint32_t x26 = mulx_u32(x5, x15);
+ uint32_t x28, uint32_t x29 = mulx_u32(x5, x17);
+ uint32_t x31, uint32_t x32 = mulx_u32(x5, x19);
+ uint32_t x34, uint32_t x35 = mulx_u32(x5, x21);
+ uint32_t x37, uint32_t x38 = mulx_u32(x5, x23);
+ uint32_t x40, uint32_t x41 = mulx_u32(x5, x22);
+ uint32_t x43, uint8_t x44 = addcarryx_u32(0x0, x26, x28);
+ uint32_t x46, uint8_t x47 = addcarryx_u32(x44, x29, x31);
+ uint32_t x49, uint8_t x50 = addcarryx_u32(x47, x32, x34);
+ uint32_t x52, uint8_t x53 = addcarryx_u32(x50, x35, x37);
+ uint32_t x55, uint8_t x56 = addcarryx_u32(x53, x38, x40);
+ uint32_t x58, uint8_t _ = addcarryx_u32(0x0, x56, x41);
+ uint32_t x61, uint32_t _ = mulx_u32(x25, 0xcccccccd);
+ uint32_t x64, uint32_t x65 = mulx_u32(x61, 0xfffffffb);
+ uint32_t x67, uint32_t x68 = mulx_u32(x61, 0xffffffff);
+ uint32_t x70, uint32_t x71 = mulx_u32(x61, 0xffffffff);
+ uint32_t x73, uint32_t x74 = mulx_u32(x61, 0xffffffff);
+ uint32_t x76, uint32_t x77 = mulx_u32(x61, 0xffffffff);
+ uint32_t x79, uint8_t x80 = mulx_u32_out_u8(x61, 0x3f);
+ uint32_t x82, uint8_t x83 = addcarryx_u32(0x0, x65, x67);
+ uint32_t x85, uint8_t x86 = addcarryx_u32(x83, x68, x70);
+ uint32_t x88, uint8_t x89 = addcarryx_u32(x86, x71, x73);
+ uint32_t x91, uint8_t x92 = addcarryx_u32(x89, x74, x76);
+ uint32_t x94, uint8_t x95 = addcarryx_u32(x92, x77, x79);
+ uint8_t x96 = (x95 + x80);
+ uint32_t _, uint8_t x99 = addcarryx_u32(0x0, x25, x64);
+ uint32_t x101, uint8_t x102 = addcarryx_u32(x99, x43, x82);
+ uint32_t x104, uint8_t x105 = addcarryx_u32(x102, x46, x85);
+ uint32_t x107, uint8_t x108 = addcarryx_u32(x105, x49, x88);
+ uint32_t x110, uint8_t x111 = addcarryx_u32(x108, x52, x91);
+ uint32_t x113, uint8_t x114 = addcarryx_u32(x111, x55, x94);
+ uint32_t x116, uint8_t x117 = addcarryx_u32(x114, x58, x96);
+ uint32_t x119, uint32_t x120 = mulx_u32(x7, x15);
+ uint32_t x122, uint32_t x123 = mulx_u32(x7, x17);
+ uint32_t x125, uint32_t x126 = mulx_u32(x7, x19);
+ uint32_t x128, uint32_t x129 = mulx_u32(x7, x21);
+ uint32_t x131, uint32_t x132 = mulx_u32(x7, x23);
+ uint32_t x134, uint32_t x135 = mulx_u32(x7, x22);
+ uint32_t x137, uint8_t x138 = addcarryx_u32(0x0, x120, x122);
+ uint32_t x140, uint8_t x141 = addcarryx_u32(x138, x123, x125);
+ uint32_t x143, uint8_t x144 = addcarryx_u32(x141, x126, x128);
+ uint32_t x146, uint8_t x147 = addcarryx_u32(x144, x129, x131);
+ uint32_t x149, uint8_t x150 = addcarryx_u32(x147, x132, x134);
+ uint32_t x152, uint8_t _ = addcarryx_u32(0x0, x150, x135);
+ uint32_t x155, uint8_t x156 = addcarryx_u32(0x0, x101, x119);
+ uint32_t x158, uint8_t x159 = addcarryx_u32(x156, x104, x137);
+ uint32_t x161, uint8_t x162 = addcarryx_u32(x159, x107, x140);
+ uint32_t x164, uint8_t x165 = addcarryx_u32(x162, x110, x143);
+ uint32_t x167, uint8_t x168 = addcarryx_u32(x165, x113, x146);
+ uint32_t x170, uint8_t x171 = addcarryx_u32(x168, x116, x149);
+ uint32_t x173, uint8_t x174 = addcarryx_u32(x171, x117, x152);
+ uint32_t x176, uint32_t _ = mulx_u32(x155, 0xcccccccd);
+ uint32_t x179, uint32_t x180 = mulx_u32(x176, 0xfffffffb);
+ uint32_t x182, uint32_t x183 = mulx_u32(x176, 0xffffffff);
+ uint32_t x185, uint32_t x186 = mulx_u32(x176, 0xffffffff);
+ uint32_t x188, uint32_t x189 = mulx_u32(x176, 0xffffffff);
+ uint32_t x191, uint32_t x192 = mulx_u32(x176, 0xffffffff);
+ uint32_t x194, uint8_t x195 = mulx_u32_out_u8(x176, 0x3f);
+ uint32_t x197, uint8_t x198 = addcarryx_u32(0x0, x180, x182);
+ uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x183, x185);
+ uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x186, x188);
+ uint32_t x206, uint8_t x207 = addcarryx_u32(x204, x189, x191);
+ uint32_t x209, uint8_t x210 = addcarryx_u32(x207, x192, x194);
+ uint8_t x211 = (x210 + x195);
+ uint32_t _, uint8_t x214 = addcarryx_u32(0x0, x155, x179);
+ uint32_t x216, uint8_t x217 = addcarryx_u32(x214, x158, x197);
+ uint32_t x219, uint8_t x220 = addcarryx_u32(x217, x161, x200);
+ uint32_t x222, uint8_t x223 = addcarryx_u32(x220, x164, x203);
+ uint32_t x225, uint8_t x226 = addcarryx_u32(x223, x167, x206);
+ uint32_t x228, uint8_t x229 = addcarryx_u32(x226, x170, x209);
+ uint32_t x231, uint8_t x232 = addcarryx_u32(x229, x173, x211);
+ uint8_t x233 = (x232 + x174);
+ uint32_t x235, uint32_t x236 = mulx_u32(x9, x15);
+ uint32_t x238, uint32_t x239 = mulx_u32(x9, x17);
+ uint32_t x241, uint32_t x242 = mulx_u32(x9, x19);
+ uint32_t x244, uint32_t x245 = mulx_u32(x9, x21);
+ uint32_t x247, uint32_t x248 = mulx_u32(x9, x23);
+ uint32_t x250, uint32_t x251 = mulx_u32(x9, x22);
+ uint32_t x253, uint8_t x254 = addcarryx_u32(0x0, x236, x238);
+ uint32_t x256, uint8_t x257 = addcarryx_u32(x254, x239, x241);
+ uint32_t x259, uint8_t x260 = addcarryx_u32(x257, x242, x244);
+ uint32_t x262, uint8_t x263 = addcarryx_u32(x260, x245, x247);
+ uint32_t x265, uint8_t x266 = addcarryx_u32(x263, x248, x250);
+ uint32_t x268, uint8_t _ = addcarryx_u32(0x0, x266, x251);
+ uint32_t x271, uint8_t x272 = addcarryx_u32(0x0, x216, x235);
+ uint32_t x274, uint8_t x275 = addcarryx_u32(x272, x219, x253);
+ uint32_t x277, uint8_t x278 = addcarryx_u32(x275, x222, x256);
+ uint32_t x280, uint8_t x281 = addcarryx_u32(x278, x225, x259);
+ uint32_t x283, uint8_t x284 = addcarryx_u32(x281, x228, x262);
+ uint32_t x286, uint8_t x287 = addcarryx_u32(x284, x231, x265);
+ uint32_t x289, uint8_t x290 = addcarryx_u32(x287, x233, x268);
+ uint32_t x292, uint32_t _ = mulx_u32(x271, 0xcccccccd);
+ uint32_t x295, uint32_t x296 = mulx_u32(x292, 0xfffffffb);
+ uint32_t x298, uint32_t x299 = mulx_u32(x292, 0xffffffff);
+ uint32_t x301, uint32_t x302 = mulx_u32(x292, 0xffffffff);
+ uint32_t x304, uint32_t x305 = mulx_u32(x292, 0xffffffff);
+ uint32_t x307, uint32_t x308 = mulx_u32(x292, 0xffffffff);
+ uint32_t x310, uint8_t x311 = mulx_u32_out_u8(x292, 0x3f);
+ uint32_t x313, uint8_t x314 = addcarryx_u32(0x0, x296, x298);
+ uint32_t x316, uint8_t x317 = addcarryx_u32(x314, x299, x301);
+ uint32_t x319, uint8_t x320 = addcarryx_u32(x317, x302, x304);
+ uint32_t x322, uint8_t x323 = addcarryx_u32(x320, x305, x307);
+ uint32_t x325, uint8_t x326 = addcarryx_u32(x323, x308, x310);
+ uint8_t x327 = (x326 + x311);
+ uint32_t _, uint8_t x330 = addcarryx_u32(0x0, x271, x295);
+ uint32_t x332, uint8_t x333 = addcarryx_u32(x330, x274, x313);
+ uint32_t x335, uint8_t x336 = addcarryx_u32(x333, x277, x316);
+ uint32_t x338, uint8_t x339 = addcarryx_u32(x336, x280, x319);
+ uint32_t x341, uint8_t x342 = addcarryx_u32(x339, x283, x322);
+ uint32_t x344, uint8_t x345 = addcarryx_u32(x342, x286, x325);
+ uint32_t x347, uint8_t x348 = addcarryx_u32(x345, x289, x327);
+ uint8_t x349 = (x348 + x290);
+ uint32_t x351, uint32_t x352 = mulx_u32(x11, x15);
+ uint32_t x354, uint32_t x355 = mulx_u32(x11, x17);
+ uint32_t x357, uint32_t x358 = mulx_u32(x11, x19);
+ uint32_t x360, uint32_t x361 = mulx_u32(x11, x21);
+ uint32_t x363, uint32_t x364 = mulx_u32(x11, x23);
+ uint32_t x366, uint32_t x367 = mulx_u32(x11, x22);
+ uint32_t x369, uint8_t x370 = addcarryx_u32(0x0, x352, x354);
+ uint32_t x372, uint8_t x373 = addcarryx_u32(x370, x355, x357);
+ uint32_t x375, uint8_t x376 = addcarryx_u32(x373, x358, x360);
+ uint32_t x378, uint8_t x379 = addcarryx_u32(x376, x361, x363);
+ uint32_t x381, uint8_t x382 = addcarryx_u32(x379, x364, x366);
+ uint32_t x384, uint8_t _ = addcarryx_u32(0x0, x382, x367);
+ uint32_t x387, uint8_t x388 = addcarryx_u32(0x0, x332, x351);
+ uint32_t x390, uint8_t x391 = addcarryx_u32(x388, x335, x369);
+ uint32_t x393, uint8_t x394 = addcarryx_u32(x391, x338, x372);
+ uint32_t x396, uint8_t x397 = addcarryx_u32(x394, x341, x375);
+ uint32_t x399, uint8_t x400 = addcarryx_u32(x397, x344, x378);
+ uint32_t x402, uint8_t x403 = addcarryx_u32(x400, x347, x381);
+ uint32_t x405, uint8_t x406 = addcarryx_u32(x403, x349, x384);
+ uint32_t x408, uint32_t _ = mulx_u32(x387, 0xcccccccd);
+ uint32_t x411, uint32_t x412 = mulx_u32(x408, 0xfffffffb);
+ uint32_t x414, uint32_t x415 = mulx_u32(x408, 0xffffffff);
+ uint32_t x417, uint32_t x418 = mulx_u32(x408, 0xffffffff);
+ uint32_t x420, uint32_t x421 = mulx_u32(x408, 0xffffffff);
+ uint32_t x423, uint32_t x424 = mulx_u32(x408, 0xffffffff);
+ uint32_t x426, uint8_t x427 = mulx_u32_out_u8(x408, 0x3f);
+ uint32_t x429, uint8_t x430 = addcarryx_u32(0x0, x412, x414);
+ uint32_t x432, uint8_t x433 = addcarryx_u32(x430, x415, x417);
+ uint32_t x435, uint8_t x436 = addcarryx_u32(x433, x418, x420);
+ uint32_t x438, uint8_t x439 = addcarryx_u32(x436, x421, x423);
+ uint32_t x441, uint8_t x442 = addcarryx_u32(x439, x424, x426);
+ uint8_t x443 = (x442 + x427);
+ uint32_t _, uint8_t x446 = addcarryx_u32(0x0, x387, x411);
+ uint32_t x448, uint8_t x449 = addcarryx_u32(x446, x390, x429);
+ uint32_t x451, uint8_t x452 = addcarryx_u32(x449, x393, x432);
+ uint32_t x454, uint8_t x455 = addcarryx_u32(x452, x396, x435);
+ uint32_t x457, uint8_t x458 = addcarryx_u32(x455, x399, x438);
+ uint32_t x460, uint8_t x461 = addcarryx_u32(x458, x402, x441);
+ uint32_t x463, uint8_t x464 = addcarryx_u32(x461, x405, x443);
+ uint8_t x465 = (x464 + x406);
+ uint32_t x467, uint32_t x468 = mulx_u32(x13, x15);
+ uint32_t x470, uint32_t x471 = mulx_u32(x13, x17);
+ uint32_t x473, uint32_t x474 = mulx_u32(x13, x19);
+ uint32_t x476, uint32_t x477 = mulx_u32(x13, x21);
+ uint32_t x479, uint32_t x480 = mulx_u32(x13, x23);
+ uint32_t x482, uint32_t x483 = mulx_u32(x13, x22);
+ uint32_t x485, uint8_t x486 = addcarryx_u32(0x0, x468, x470);
+ uint32_t x488, uint8_t x489 = addcarryx_u32(x486, x471, x473);
+ uint32_t x491, uint8_t x492 = addcarryx_u32(x489, x474, x476);
+ uint32_t x494, uint8_t x495 = addcarryx_u32(x492, x477, x479);
+ uint32_t x497, uint8_t x498 = addcarryx_u32(x495, x480, x482);
+ uint32_t x500, uint8_t _ = addcarryx_u32(0x0, x498, x483);
+ uint32_t x503, uint8_t x504 = addcarryx_u32(0x0, x448, x467);
+ uint32_t x506, uint8_t x507 = addcarryx_u32(x504, x451, x485);
+ uint32_t x509, uint8_t x510 = addcarryx_u32(x507, x454, x488);
+ uint32_t x512, uint8_t x513 = addcarryx_u32(x510, x457, x491);
+ uint32_t x515, uint8_t x516 = addcarryx_u32(x513, x460, x494);
+ uint32_t x518, uint8_t x519 = addcarryx_u32(x516, x463, x497);
+ uint32_t x521, uint8_t x522 = addcarryx_u32(x519, x465, x500);
+ uint32_t x524, uint32_t _ = mulx_u32(x503, 0xcccccccd);
+ uint32_t x527, uint32_t x528 = mulx_u32(x524, 0xfffffffb);
+ uint32_t x530, uint32_t x531 = mulx_u32(x524, 0xffffffff);
+ uint32_t x533, uint32_t x534 = mulx_u32(x524, 0xffffffff);
+ uint32_t x536, uint32_t x537 = mulx_u32(x524, 0xffffffff);
+ uint32_t x539, uint32_t x540 = mulx_u32(x524, 0xffffffff);
+ uint32_t x542, uint8_t x543 = mulx_u32_out_u8(x524, 0x3f);
+ uint32_t x545, uint8_t x546 = addcarryx_u32(0x0, x528, x530);
+ uint32_t x548, uint8_t x549 = addcarryx_u32(x546, x531, x533);
+ uint32_t x551, uint8_t x552 = addcarryx_u32(x549, x534, x536);
+ uint32_t x554, uint8_t x555 = addcarryx_u32(x552, x537, x539);
+ uint32_t x557, uint8_t x558 = addcarryx_u32(x555, x540, x542);
+ uint8_t x559 = (x558 + x543);
+ uint32_t _, uint8_t x562 = addcarryx_u32(0x0, x503, x527);
+ uint32_t x564, uint8_t x565 = addcarryx_u32(x562, x506, x545);
+ uint32_t x567, uint8_t x568 = addcarryx_u32(x565, x509, x548);
+ uint32_t x570, uint8_t x571 = addcarryx_u32(x568, x512, x551);
+ uint32_t x573, uint8_t x574 = addcarryx_u32(x571, x515, x554);
+ uint32_t x576, uint8_t x577 = addcarryx_u32(x574, x518, x557);
+ uint32_t x579, uint8_t x580 = addcarryx_u32(x577, x521, x559);
+ uint8_t x581 = (x580 + x522);
+ uint32_t x583, uint32_t x584 = mulx_u32(x12, x15);
+ uint32_t x586, uint32_t x587 = mulx_u32(x12, x17);
+ uint32_t x589, uint32_t x590 = mulx_u32(x12, x19);
+ uint32_t x592, uint32_t x593 = mulx_u32(x12, x21);
+ uint32_t x595, uint32_t x596 = mulx_u32(x12, x23);
+ uint32_t x598, uint32_t x599 = mulx_u32(x12, x22);
+ uint32_t x601, uint8_t x602 = addcarryx_u32(0x0, x584, x586);
+ uint32_t x604, uint8_t x605 = addcarryx_u32(x602, x587, x589);
+ uint32_t x607, uint8_t x608 = addcarryx_u32(x605, x590, x592);
+ uint32_t x610, uint8_t x611 = addcarryx_u32(x608, x593, x595);
+ uint32_t x613, uint8_t x614 = addcarryx_u32(x611, x596, x598);
+ uint32_t x616, uint8_t _ = addcarryx_u32(0x0, x614, x599);
+ uint32_t x619, uint8_t x620 = addcarryx_u32(0x0, x564, x583);
+ uint32_t x622, uint8_t x623 = addcarryx_u32(x620, x567, x601);
+ uint32_t x625, uint8_t x626 = addcarryx_u32(x623, x570, x604);
+ uint32_t x628, uint8_t x629 = addcarryx_u32(x626, x573, x607);
+ uint32_t x631, uint8_t x632 = addcarryx_u32(x629, x576, x610);
+ uint32_t x634, uint8_t x635 = addcarryx_u32(x632, x579, x613);
+ uint32_t x637, uint8_t x638 = addcarryx_u32(x635, x581, x616);
+ uint32_t x640, uint32_t _ = mulx_u32(x619, 0xcccccccd);
+ uint32_t x643, uint32_t x644 = mulx_u32(x640, 0xfffffffb);
+ uint32_t x646, uint32_t x647 = mulx_u32(x640, 0xffffffff);
+ uint32_t x649, uint32_t x650 = mulx_u32(x640, 0xffffffff);
+ uint32_t x652, uint32_t x653 = mulx_u32(x640, 0xffffffff);
+ uint32_t x655, uint32_t x656 = mulx_u32(x640, 0xffffffff);
+ uint32_t x658, uint8_t x659 = mulx_u32_out_u8(x640, 0x3f);
+ uint32_t x661, uint8_t x662 = addcarryx_u32(0x0, x644, x646);
+ uint32_t x664, uint8_t x665 = addcarryx_u32(x662, x647, x649);
+ uint32_t x667, uint8_t x668 = addcarryx_u32(x665, x650, x652);
+ uint32_t x670, uint8_t x671 = addcarryx_u32(x668, x653, x655);
+ uint32_t x673, uint8_t x674 = addcarryx_u32(x671, x656, x658);
+ uint8_t x675 = (x674 + x659);
+ uint32_t _, uint8_t x678 = addcarryx_u32(0x0, x619, x643);
+ uint32_t x680, uint8_t x681 = addcarryx_u32(x678, x622, x661);
+ uint32_t x683, uint8_t x684 = addcarryx_u32(x681, x625, x664);
+ uint32_t x686, uint8_t x687 = addcarryx_u32(x684, x628, x667);
+ uint32_t x689, uint8_t x690 = addcarryx_u32(x687, x631, x670);
+ uint32_t x692, uint8_t x693 = addcarryx_u32(x690, x634, x673);
+ uint32_t x695, uint8_t x696 = addcarryx_u32(x693, x637, x675);
+ uint8_t x697 = (x696 + x638);
+ uint32_t x699, uint8_t x700 = subborrow_u32(0x0, x680, 0xfffffffb);
+ uint32_t x702, uint8_t x703 = subborrow_u32(x700, x683, 0xffffffff);
+ uint32_t x705, uint8_t x706 = subborrow_u32(x703, x686, 0xffffffff);
+ uint32_t x708, uint8_t x709 = subborrow_u32(x706, x689, 0xffffffff);
+ uint32_t x711, uint8_t x712 = subborrow_u32(x709, x692, 0xffffffff);
+ uint32_t x714, uint8_t x715 = subborrow_u32(x712, x695, 0x3f);
+ uint32_t _, uint8_t x718 = subborrow_u32(x715, x697, 0x0);
+ uint32_t x719 = cmovznz32(x718, x714, x695);
+ uint32_t x720 = cmovznz32(x718, x711, x692);
+ uint32_t x721 = cmovznz32(x718, x708, x689);
+ uint32_t x722 = cmovznz32(x718, x705, x686);
+ uint32_t x723 = cmovznz32(x718, x702, x683);
+ uint32_t x724 = cmovznz32(x718, x699, x680);
+ return (x719, x720, x721, x722, x723, x724))
+(x, x0)%core
+ : 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)
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/feopp.c b/src/Specific/montgomery32_2e166m5_6limbs/feopp.c
new file mode 100644
index 000000000..d9caf7596
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/feopp.c
@@ -0,0 +1,34 @@
+static void feopp(uint32_t out[6], const uint32_t in1[6]) {
+ { const uint32_t x9 = in1[5];
+ { const uint32_t x10 = in1[4];
+ { const uint32_t x8 = in1[3];
+ { const uint32_t x6 = in1[2];
+ { const uint32_t x4 = in1[1];
+ { const uint32_t x2 = in1[0];
+ { uint32_t x12; uint8_t x13 = _subborrow_u32(0x0, 0x0, x2, &x12);
+ { uint32_t x15; uint8_t x16 = _subborrow_u32(x13, 0x0, x4, &x15);
+ { uint32_t x18; uint8_t x19 = _subborrow_u32(x16, 0x0, x6, &x18);
+ { uint32_t x21; uint8_t x22 = _subborrow_u32(x19, 0x0, x8, &x21);
+ { uint32_t x24; uint8_t x25 = _subborrow_u32(x22, 0x0, x10, &x24);
+ { uint32_t x27; uint8_t x28 = _subborrow_u32(x25, 0x0, x9, &x27);
+ { uint32_t x29 = cmovznz32(x28, 0x0, 0xffffffff);
+ { uint32_t x30 = (x29 & 0xfffffffb);
+ { uint32_t x32; uint8_t x33 = _addcarryx_u32(0x0, x12, x30, &x32);
+ { uint32_t x34 = (x29 & 0xffffffff);
+ { uint32_t x36; uint8_t x37 = _addcarryx_u32(x33, x15, x34, &x36);
+ { uint32_t x38 = (x29 & 0xffffffff);
+ { uint32_t x40; uint8_t x41 = _addcarryx_u32(x37, x18, x38, &x40);
+ { uint32_t x42 = (x29 & 0xffffffff);
+ { uint32_t x44; uint8_t x45 = _addcarryx_u32(x41, x21, x42, &x44);
+ { uint32_t x46 = (x29 & 0xffffffff);
+ { uint32_t x48; uint8_t x49 = _addcarryx_u32(x45, x24, x46, &x48);
+ { uint8_t x50 = ((uint8_t)x29 & 0x3f);
+ { uint32_t x52; uint8_t _ = _addcarryx_u32(x49, x27, x50, &x52);
+ out[0] = x32;
+ out[1] = x36;
+ out[2] = x40;
+ out[3] = x44;
+ out[4] = x48;
+ out[5] = x52;
+ }}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/feoppDisplay.log b/src/Specific/montgomery32_2e166m5_6limbs/feoppDisplay.log
new file mode 100644
index 000000000..8b39a6b4e
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/feoppDisplay.log
@@ -0,0 +1,26 @@
+λ x : word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x9, x10, x8, x6, x4, x2)%core,
+ uint32_t x12, uint8_t x13 = subborrow_u32(0x0, 0x0, x2);
+ uint32_t x15, uint8_t x16 = subborrow_u32(x13, 0x0, x4);
+ uint32_t x18, uint8_t x19 = subborrow_u32(x16, 0x0, x6);
+ uint32_t x21, uint8_t x22 = subborrow_u32(x19, 0x0, x8);
+ uint32_t x24, uint8_t x25 = subborrow_u32(x22, 0x0, x10);
+ uint32_t x27, uint8_t x28 = subborrow_u32(x25, 0x0, x9);
+ uint32_t x29 = cmovznz32(x28, 0x0, 0xffffffff);
+ uint32_t x30 = (x29 & 0xfffffffb);
+ uint32_t x32, uint8_t x33 = addcarryx_u32(0x0, x12, x30);
+ uint32_t x34 = (x29 & 0xffffffff);
+ uint32_t x36, uint8_t x37 = addcarryx_u32(x33, x15, x34);
+ uint32_t x38 = (x29 & 0xffffffff);
+ uint32_t x40, uint8_t x41 = addcarryx_u32(x37, x18, x38);
+ uint32_t x42 = (x29 & 0xffffffff);
+ uint32_t x44, uint8_t x45 = addcarryx_u32(x41, x21, x42);
+ uint32_t x46 = (x29 & 0xffffffff);
+ uint32_t x48, uint8_t x49 = addcarryx_u32(x45, x24, x46);
+ uint8_t x50 = ((uint8_t)x29 & 0x3f);
+ uint32_t x52, uint8_t _ = addcarryx_u32(x49, x27, x50);
+ (Return x52, Return x48, Return x44, Return x40, Return x36, Return x32))
+x
+ : word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/fesub.c b/src/Specific/montgomery32_2e166m5_6limbs/fesub.c
new file mode 100644
index 000000000..5ce4a0e74
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/fesub.c
@@ -0,0 +1,40 @@
+static void fesub(uint32_t out[6], const uint32_t in1[6], const uint32_t in2[6]) {
+ { const uint32_t x12 = 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 x22 = in2[5];
+ { const uint32_t x23 = in2[4];
+ { const uint32_t x21 = in2[3];
+ { const uint32_t x19 = in2[2];
+ { const uint32_t x17 = in2[1];
+ { const uint32_t x15 = in2[0];
+ { uint32_t x25; uint8_t x26 = _subborrow_u32(0x0, x5, x15, &x25);
+ { uint32_t x28; uint8_t x29 = _subborrow_u32(x26, x7, x17, &x28);
+ { uint32_t x31; uint8_t x32 = _subborrow_u32(x29, x9, x19, &x31);
+ { uint32_t x34; uint8_t x35 = _subborrow_u32(x32, x11, x21, &x34);
+ { uint32_t x37; uint8_t x38 = _subborrow_u32(x35, x13, x23, &x37);
+ { uint32_t x40; uint8_t x41 = _subborrow_u32(x38, x12, x22, &x40);
+ { uint32_t x42 = cmovznz32(x41, 0x0, 0xffffffff);
+ { uint32_t x43 = (x42 & 0xfffffffb);
+ { uint32_t x45; uint8_t x46 = _addcarryx_u32(0x0, x25, x43, &x45);
+ { uint32_t x47 = (x42 & 0xffffffff);
+ { uint32_t x49; uint8_t x50 = _addcarryx_u32(x46, x28, x47, &x49);
+ { uint32_t x51 = (x42 & 0xffffffff);
+ { uint32_t x53; uint8_t x54 = _addcarryx_u32(x50, x31, x51, &x53);
+ { uint32_t x55 = (x42 & 0xffffffff);
+ { uint32_t x57; uint8_t x58 = _addcarryx_u32(x54, x34, x55, &x57);
+ { uint32_t x59 = (x42 & 0xffffffff);
+ { uint32_t x61; uint8_t x62 = _addcarryx_u32(x58, x37, x59, &x61);
+ { uint8_t x63 = ((uint8_t)x42 & 0x3f);
+ { uint32_t x65; uint8_t _ = _addcarryx_u32(x62, x40, x63, &x65);
+ out[0] = x45;
+ out[1] = x49;
+ out[2] = x53;
+ out[3] = x57;
+ out[4] = x61;
+ out[5] = x65;
+ }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery32_2e166m5_6limbs/fesubDisplay.log b/src/Specific/montgomery32_2e166m5_6limbs/fesubDisplay.log
new file mode 100644
index 000000000..5b6f35fd1
--- /dev/null
+++ b/src/Specific/montgomery32_2e166m5_6limbs/fesubDisplay.log
@@ -0,0 +1,26 @@
+λ x x0 : word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core,
+ uint32_t x25, uint8_t x26 = subborrow_u32(0x0, x5, x15);
+ uint32_t x28, uint8_t x29 = subborrow_u32(x26, x7, x17);
+ uint32_t x31, uint8_t x32 = subborrow_u32(x29, x9, x19);
+ uint32_t x34, uint8_t x35 = subborrow_u32(x32, x11, x21);
+ uint32_t x37, uint8_t x38 = subborrow_u32(x35, x13, x23);
+ uint32_t x40, uint8_t x41 = subborrow_u32(x38, x12, x22);
+ uint32_t x42 = cmovznz32(x41, 0x0, 0xffffffff);
+ uint32_t x43 = (x42 & 0xfffffffb);
+ uint32_t x45, uint8_t x46 = addcarryx_u32(0x0, x25, x43);
+ uint32_t x47 = (x42 & 0xffffffff);
+ uint32_t x49, uint8_t x50 = addcarryx_u32(x46, x28, x47);
+ uint32_t x51 = (x42 & 0xffffffff);
+ uint32_t x53, uint8_t x54 = addcarryx_u32(x50, x31, x51);
+ uint32_t x55 = (x42 & 0xffffffff);
+ uint32_t x57, uint8_t x58 = addcarryx_u32(x54, x34, x55);
+ uint32_t x59 = (x42 & 0xffffffff);
+ uint32_t x61, uint8_t x62 = addcarryx_u32(x58, x37, x59);
+ uint8_t x63 = ((uint8_t)x42 & 0x3f);
+ uint32_t x65, uint8_t _ = addcarryx_u32(x62, x40, x63);
+ (Return x65, Return x61, Return x57, Return x53, Return x49, Return x45))
+(x, x0)%core
+ : 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)