Update display logs and c files

10 files changed, 275 insertions, 0 deletions

diff --git a/src/Specific/montgomery64_2e129m25_3limbs/feadd.c b/src/Specific/montgomery64_2e129m25_3limbs/feadd.c
new file mode 100644
index 000000000..1f4da6ce2
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/feadd.c
@@ -0,0 +1,22 @@
+static void feadd(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3]) {
+  { const uint64_t x6 = in1[2];
+  { const uint64_t x7 = in1[1];
+  { const uint64_t x5 = in1[0];
+  { const uint64_t x10 = in2[2];
+  { const uint64_t x11 = in2[1];
+  { const uint64_t x9 = in2[0];
+  { uint64_t x13; uint8_t x14 = _addcarryx_u64(0x0, x5, x9, &x13);
+  { uint64_t x16; uint8_t x17 = _addcarryx_u64(x14, x7, x11, &x16);
+  { uint64_t x19; uint8_t x20 = _addcarryx_u64(x17, x6, x10, &x19);
+  { uint64_t x22; uint8_t x23 = _subborrow_u64(0x0, x13, 0xffffffffffffffe7L, &x22);
+  { uint64_t x25; uint8_t x26 = _subborrow_u64(x23, x16, 0xffffffffffffffffL, &x25);
+  { uint64_t x28; uint8_t x29 = _subborrow_u64(x26, x19, 0x1, &x28);
+  { uint64_t _; uint8_t x32 = _subborrow_u64(x29, x20, 0x0, &_);
+  { uint64_t x33 = cmovznz64(x32, x28, x19);
+  { uint64_t x34 = cmovznz64(x32, x25, x16);
+  { uint64_t x35 = cmovznz64(x32, x22, x13);
+  out[0] = x35;
+  out[1] = x34;
+  out[2] = x33;
+  }}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/feaddDisplay.log b/src/Specific/montgomery64_2e129m25_3limbs/feaddDisplay.log
new file mode 100644
index 000000000..429f30466
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/feaddDisplay.log
@@ -0,0 +1,17 @@
+λ x x0 : word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x6, x7, x5, (x10, x11, x9))%core,
+ uint64_t x13, uint8_t x14 = addcarryx_u64(0x0, x5, x9);
+ uint64_t x16, uint8_t x17 = addcarryx_u64(x14, x7, x11);
+ uint64_t x19, uint8_t x20 = addcarryx_u64(x17, x6, x10);
+ uint64_t x22, uint8_t x23 = subborrow_u64(0x0, x13, 0xffffffffffffffe7L);
+ uint64_t x25, uint8_t x26 = subborrow_u64(x23, x16, 0xffffffffffffffffL);
+ uint64_t x28, uint8_t x29 = subborrow_u64(x26, x19, 0x1);
+ uint64_t _, uint8_t x32 = subborrow_u64(x29, x20, 0x0);
+ uint64_t x33 = cmovznz64(x32, x28, x19);
+ uint64_t x34 = cmovznz64(x32, x25, x16);
+ uint64_t x35 = cmovznz64(x32, x22, x13);
+ return (x33, x34, x35))
+(x, x0)%core
+     : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/femul.c b/src/Specific/montgomery64_2e129m25_3limbs/femul.c
new file mode 100644
index 000000000..6e245304f
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/femul.c
@@ -0,0 +1,74 @@
+static void femul(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3]) {
+  { const uint64_t x6 = in1[2];
+  { const uint64_t x7 = in1[1];
+  { const uint64_t x5 = in1[0];
+  { const uint64_t x10 = in2[2];
+  { const uint64_t x11 = in2[1];
+  { const uint64_t x9 = in2[0];
+  { uint64_t x14;  uint64_t x13 = _mulx_u64(x5, x9, &x14);
+  { uint64_t x17;  uint64_t x16 = _mulx_u64(x5, x11, &x17);
+  { uint64_t x20;  uint64_t x19 = _mulx_u64(x5, x10, &x20);
+  { uint64_t x22; uint8_t x23 = _addcarryx_u64(0x0, x14, x16, &x22);
+  { uint64_t x25; uint8_t x26 = _addcarryx_u64(x23, x17, x19, &x25);
+  { uint64_t x28; uint8_t _ = _addcarryx_u64(0x0, x26, x20, &x28);
+  { uint64_t _;  uint64_t x31 = _mulx_u64(x13, 0x8f5c28f5c28f5c29L, &_);
+  { uint64_t x35;  uint64_t x34 = _mulx_u64(x31, 0xffffffffffffffe7L, &x35);
+  { uint64_t x38;  uint64_t x37 = _mulx_u64(x31, 0xffffffffffffffffL, &x38);
+  { uint64_t x40; uint8_t x41 = _addcarryx_u64(0x0, x35, x37, &x40);
+  { uint64_t x43; uint8_t x44 = _addcarryx_u64(x41, x38, x31, &x43);
+  { uint64_t _; uint8_t x47 = _addcarryx_u64(0x0, x13, x34, &_);
+  { uint64_t x49; uint8_t x50 = _addcarryx_u64(x47, x22, x40, &x49);
+  { uint64_t x52; uint8_t x53 = _addcarryx_u64(x50, x25, x43, &x52);
+  { uint64_t x55; uint8_t x56 = _addcarryx_u64(x53, x28, x44, &x55);
+  { uint64_t x59;  uint64_t x58 = _mulx_u64(x7, x9, &x59);
+  { uint64_t x62;  uint64_t x61 = _mulx_u64(x7, x11, &x62);
+  { uint64_t x65;  uint64_t x64 = _mulx_u64(x7, x10, &x65);
+  { uint64_t x67; uint8_t x68 = _addcarryx_u64(0x0, x59, x61, &x67);
+  { uint64_t x70; uint8_t x71 = _addcarryx_u64(x68, x62, x64, &x70);
+  { uint64_t x73; uint8_t _ = _addcarryx_u64(0x0, x71, x65, &x73);
+  { uint64_t x76; uint8_t x77 = _addcarryx_u64(0x0, x49, x58, &x76);
+  { uint64_t x79; uint8_t x80 = _addcarryx_u64(x77, x52, x67, &x79);
+  { uint64_t x82; uint8_t x83 = _addcarryx_u64(x80, x55, x70, &x82);
+  { uint64_t x85; uint8_t x86 = _addcarryx_u64(x83, x56, x73, &x85);
+  { uint64_t _;  uint64_t x88 = _mulx_u64(x76, 0x8f5c28f5c28f5c29L, &_);
+  { uint64_t x92;  uint64_t x91 = _mulx_u64(x88, 0xffffffffffffffe7L, &x92);
+  { uint64_t x95;  uint64_t x94 = _mulx_u64(x88, 0xffffffffffffffffL, &x95);
+  { uint64_t x97; uint8_t x98 = _addcarryx_u64(0x0, x92, x94, &x97);
+  { uint64_t x100; uint8_t x101 = _addcarryx_u64(x98, x95, x88, &x100);
+  { uint64_t _; uint8_t x104 = _addcarryx_u64(0x0, x76, x91, &_);
+  { uint64_t x106; uint8_t x107 = _addcarryx_u64(x104, x79, x97, &x106);
+  { uint64_t x109; uint8_t x110 = _addcarryx_u64(x107, x82, x100, &x109);
+  { uint64_t x112; uint8_t x113 = _addcarryx_u64(x110, x85, x101, &x112);
+  { uint8_t x114 = (x113 + x86);
+  { uint64_t x117;  uint64_t x116 = _mulx_u64(x6, x9, &x117);
+  { uint64_t x120;  uint64_t x119 = _mulx_u64(x6, x11, &x120);
+  { uint64_t x123;  uint64_t x122 = _mulx_u64(x6, x10, &x123);
+  { uint64_t x125; uint8_t x126 = _addcarryx_u64(0x0, x117, x119, &x125);
+  { uint64_t x128; uint8_t x129 = _addcarryx_u64(x126, x120, x122, &x128);
+  { uint64_t x131; uint8_t _ = _addcarryx_u64(0x0, x129, x123, &x131);
+  { uint64_t x134; uint8_t x135 = _addcarryx_u64(0x0, x106, x116, &x134);
+  { uint64_t x137; uint8_t x138 = _addcarryx_u64(x135, x109, x125, &x137);
+  { uint64_t x140; uint8_t x141 = _addcarryx_u64(x138, x112, x128, &x140);
+  { uint64_t x143; uint8_t x144 = _addcarryx_u64(x141, x114, x131, &x143);
+  { uint64_t _;  uint64_t x146 = _mulx_u64(x134, 0x8f5c28f5c28f5c29L, &_);
+  { uint64_t x150;  uint64_t x149 = _mulx_u64(x146, 0xffffffffffffffe7L, &x150);
+  { uint64_t x153;  uint64_t x152 = _mulx_u64(x146, 0xffffffffffffffffL, &x153);
+  { uint64_t x155; uint8_t x156 = _addcarryx_u64(0x0, x150, x152, &x155);
+  { uint64_t x158; uint8_t x159 = _addcarryx_u64(x156, x153, x146, &x158);
+  { uint64_t _; uint8_t x162 = _addcarryx_u64(0x0, x134, x149, &_);
+  { uint64_t x164; uint8_t x165 = _addcarryx_u64(x162, x137, x155, &x164);
+  { uint64_t x167; uint8_t x168 = _addcarryx_u64(x165, x140, x158, &x167);
+  { uint64_t x170; uint8_t x171 = _addcarryx_u64(x168, x143, x159, &x170);
+  { uint8_t x172 = (x171 + x144);
+  { uint64_t x174; uint8_t x175 = _subborrow_u64(0x0, x164, 0xffffffffffffffe7L, &x174);
+  { uint64_t x177; uint8_t x178 = _subborrow_u64(x175, x167, 0xffffffffffffffffL, &x177);
+  { uint64_t x180; uint8_t x181 = _subborrow_u64(x178, x170, 0x1, &x180);
+  { uint64_t _; uint8_t x184 = _subborrow_u64(x181, x172, 0x0, &_);
+  { uint64_t x185 = cmovznz64(x184, x180, x170);
+  { uint64_t x186 = cmovznz64(x184, x177, x167);
+  { uint64_t x187 = cmovznz64(x184, x174, x164);
+  out[0] = x187;
+  out[1] = x186;
+  out[2] = x185;
+  }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/femulDisplay.log b/src/Specific/montgomery64_2e129m25_3limbs/femulDisplay.log
new file mode 100644
index 000000000..5e06221b0
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/femulDisplay.log
@@ -0,0 +1,69 @@
+λ x x0 : word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x6, x7, x5, (x10, x11, x9))%core,
+ uint64_t x13, uint64_t x14 = mulx_u64(x5, x9);
+ uint64_t x16, uint64_t x17 = mulx_u64(x5, x11);
+ uint64_t x19, uint64_t x20 = mulx_u64(x5, x10);
+ uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x14, x16);
+ uint64_t x25, uint8_t x26 = addcarryx_u64(x23, x17, x19);
+ uint64_t x28, uint8_t _ = addcarryx_u64(0x0, x26, x20);
+ uint64_t x31, uint64_t _ = mulx_u64(x13, 0x8f5c28f5c28f5c29L);
+ uint64_t x34, uint64_t x35 = mulx_u64(x31, 0xffffffffffffffe7L);
+ uint64_t x37, uint64_t x38 = mulx_u64(x31, 0xffffffffffffffffL);
+ uint64_t x40, uint8_t x41 = addcarryx_u64(0x0, x35, x37);
+ uint64_t x43, uint8_t x44 = addcarryx_u64(x41, x38, x31);
+ uint64_t _, uint8_t x47 = addcarryx_u64(0x0, x13, x34);
+ uint64_t x49, uint8_t x50 = addcarryx_u64(x47, x22, x40);
+ uint64_t x52, uint8_t x53 = addcarryx_u64(x50, x25, x43);
+ uint64_t x55, uint8_t x56 = addcarryx_u64(x53, x28, x44);
+ uint64_t x58, uint64_t x59 = mulx_u64(x7, x9);
+ uint64_t x61, uint64_t x62 = mulx_u64(x7, x11);
+ uint64_t x64, uint64_t x65 = mulx_u64(x7, x10);
+ uint64_t x67, uint8_t x68 = addcarryx_u64(0x0, x59, x61);
+ uint64_t x70, uint8_t x71 = addcarryx_u64(x68, x62, x64);
+ uint64_t x73, uint8_t _ = addcarryx_u64(0x0, x71, x65);
+ uint64_t x76, uint8_t x77 = addcarryx_u64(0x0, x49, x58);
+ uint64_t x79, uint8_t x80 = addcarryx_u64(x77, x52, x67);
+ uint64_t x82, uint8_t x83 = addcarryx_u64(x80, x55, x70);
+ uint64_t x85, uint8_t x86 = addcarryx_u64(x83, x56, x73);
+ uint64_t x88, uint64_t _ = mulx_u64(x76, 0x8f5c28f5c28f5c29L);
+ uint64_t x91, uint64_t x92 = mulx_u64(x88, 0xffffffffffffffe7L);
+ uint64_t x94, uint64_t x95 = mulx_u64(x88, 0xffffffffffffffffL);
+ uint64_t x97, uint8_t x98 = addcarryx_u64(0x0, x92, x94);
+ uint64_t x100, uint8_t x101 = addcarryx_u64(x98, x95, x88);
+ uint64_t _, uint8_t x104 = addcarryx_u64(0x0, x76, x91);
+ uint64_t x106, uint8_t x107 = addcarryx_u64(x104, x79, x97);
+ uint64_t x109, uint8_t x110 = addcarryx_u64(x107, x82, x100);
+ uint64_t x112, uint8_t x113 = addcarryx_u64(x110, x85, x101);
+ uint8_t x114 = (x113 + x86);
+ uint64_t x116, uint64_t x117 = mulx_u64(x6, x9);
+ uint64_t x119, uint64_t x120 = mulx_u64(x6, x11);
+ uint64_t x122, uint64_t x123 = mulx_u64(x6, x10);
+ uint64_t x125, uint8_t x126 = addcarryx_u64(0x0, x117, x119);
+ uint64_t x128, uint8_t x129 = addcarryx_u64(x126, x120, x122);
+ uint64_t x131, uint8_t _ = addcarryx_u64(0x0, x129, x123);
+ uint64_t x134, uint8_t x135 = addcarryx_u64(0x0, x106, x116);
+ uint64_t x137, uint8_t x138 = addcarryx_u64(x135, x109, x125);
+ uint64_t x140, uint8_t x141 = addcarryx_u64(x138, x112, x128);
+ uint64_t x143, uint8_t x144 = addcarryx_u64(x141, x114, x131);
+ uint64_t x146, uint64_t _ = mulx_u64(x134, 0x8f5c28f5c28f5c29L);
+ uint64_t x149, uint64_t x150 = mulx_u64(x146, 0xffffffffffffffe7L);
+ uint64_t x152, uint64_t x153 = mulx_u64(x146, 0xffffffffffffffffL);
+ uint64_t x155, uint8_t x156 = addcarryx_u64(0x0, x150, x152);
+ uint64_t x158, uint8_t x159 = addcarryx_u64(x156, x153, x146);
+ uint64_t _, uint8_t x162 = addcarryx_u64(0x0, x134, x149);
+ uint64_t x164, uint8_t x165 = addcarryx_u64(x162, x137, x155);
+ uint64_t x167, uint8_t x168 = addcarryx_u64(x165, x140, x158);
+ uint64_t x170, uint8_t x171 = addcarryx_u64(x168, x143, x159);
+ uint8_t x172 = (x171 + x144);
+ uint64_t x174, uint8_t x175 = subborrow_u64(0x0, x164, 0xffffffffffffffe7L);
+ uint64_t x177, uint8_t x178 = subborrow_u64(x175, x167, 0xffffffffffffffffL);
+ uint64_t x180, uint8_t x181 = subborrow_u64(x178, x170, 0x1);
+ uint64_t _, uint8_t x184 = subborrow_u64(x181, x172, 0x0);
+ uint64_t x185 = cmovznz64(x184, x180, x170);
+ uint64_t x186 = cmovznz64(x184, x177, x167);
+ uint64_t x187 = cmovznz64(x184, x174, x164);
+ return (x185, x186, x187))
+(x, x0)%core
+     : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/fenz.c b/src/Specific/montgomery64_2e129m25_3limbs/fenz.c
new file mode 100644
index 000000000..2632a2866
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/fenz.c
@@ -0,0 +1,9 @@
+static void fenz(ReturnType uint64_t out[1], const uint64_t in1[3]) {
+  { const uint64_t x3 = in1[2];
+  { const uint64_t x4 = in1[1];
+  { const uint64_t x2 = in1[0];
+  { uint64_t x5 = (x4 | x3);
+  { uint64_t x6 = (x2 | x5);
+  out[0] = x6;
+  }}}}}
+}
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/fenzDisplay.log b/src/Specific/montgomery64_2e129m25_3limbs/fenzDisplay.log
new file mode 100644
index 000000000..680322e0f
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/fenzDisplay.log
@@ -0,0 +1,9 @@
+λ x : word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x3, x4, x2)%core,
+ uint64_t x5 = (x4 | x3);
+ uint64_t x6 = (x2 | x5);
+ return x6)
+x
+     : word64 * word64 * word64 → ReturnType uint64_t
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/feopp.c b/src/Specific/montgomery64_2e129m25_3limbs/feopp.c
new file mode 100644
index 000000000..57985379d
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/feopp.c
@@ -0,0 +1,19 @@
+static void feopp(uint64_t out[3], const uint64_t in1[3]) {
+  { const uint64_t x3 = in1[2];
+  { const uint64_t x4 = in1[1];
+  { const uint64_t x2 = in1[0];
+  { uint64_t x6; uint8_t x7 = _subborrow_u64(0x0, 0x0, x2, &x6);
+  { uint64_t x9; uint8_t x10 = _subborrow_u64(x7, 0x0, x4, &x9);
+  { uint64_t x12; uint8_t x13 = _subborrow_u64(x10, 0x0, x3, &x12);
+  { uint64_t x14 = cmovznz64(x13, 0x0, 0xffffffffffffffffL);
+  { uint64_t x15 = (x14 & 0xffffffffffffffe7L);
+  { uint64_t x17; uint8_t x18 = _addcarryx_u64(0x0, x6, x15, &x17);
+  { uint64_t x19 = (x14 & 0xffffffffffffffffL);
+  { uint64_t x21; uint8_t x22 = _addcarryx_u64(x18, x9, x19, &x21);
+  { uint8_t x23 = ((uint8_t)x14 & 0x1);
+  { uint64_t x25; uint8_t _ = _addcarryx_u64(x22, x12, x23, &x25);
+  out[0] = x17;
+  out[1] = x21;
+  out[2] = x25;
+  }}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/feoppDisplay.log b/src/Specific/montgomery64_2e129m25_3limbs/feoppDisplay.log
new file mode 100644
index 000000000..e761bfab0
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/feoppDisplay.log
@@ -0,0 +1,17 @@
+λ x : word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x3, x4, x2)%core,
+ uint64_t x6, uint8_t x7 = subborrow_u64(0x0, 0x0, x2);
+ uint64_t x9, uint8_t x10 = subborrow_u64(x7, 0x0, x4);
+ uint64_t x12, uint8_t x13 = subborrow_u64(x10, 0x0, x3);
+ uint64_t x14 = cmovznz64(x13, 0x0, 0xffffffffffffffffL);
+ uint64_t x15 = (x14 & 0xffffffffffffffe7L);
+ uint64_t x17, uint8_t x18 = addcarryx_u64(0x0, x6, x15);
+ uint64_t x19 = (x14 & 0xffffffffffffffffL);
+ uint64_t x21, uint8_t x22 = addcarryx_u64(x18, x9, x19);
+ uint8_t x23 = ((uint8_t)x14 & 0x1);
+ uint64_t x25, uint8_t _ = addcarryx_u64(x22, x12, x23);
+ (Return x25, Return x21, Return x17))
+x
+     : word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/fesub.c b/src/Specific/montgomery64_2e129m25_3limbs/fesub.c
new file mode 100644
index 000000000..d31d91734
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/fesub.c
@@ -0,0 +1,22 @@
+static void fesub(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3]) {
+  { const uint64_t x6 = in1[2];
+  { const uint64_t x7 = in1[1];
+  { const uint64_t x5 = in1[0];
+  { const uint64_t x10 = in2[2];
+  { const uint64_t x11 = in2[1];
+  { const uint64_t x9 = in2[0];
+  { uint64_t x13; uint8_t x14 = _subborrow_u64(0x0, x5, x9, &x13);
+  { uint64_t x16; uint8_t x17 = _subborrow_u64(x14, x7, x11, &x16);
+  { uint64_t x19; uint8_t x20 = _subborrow_u64(x17, x6, x10, &x19);
+  { uint64_t x21 = cmovznz64(x20, 0x0, 0xffffffffffffffffL);
+  { uint64_t x22 = (x21 & 0xffffffffffffffe7L);
+  { uint64_t x24; uint8_t x25 = _addcarryx_u64(0x0, x13, x22, &x24);
+  { uint64_t x26 = (x21 & 0xffffffffffffffffL);
+  { uint64_t x28; uint8_t x29 = _addcarryx_u64(x25, x16, x26, &x28);
+  { uint8_t x30 = ((uint8_t)x21 & 0x1);
+  { uint64_t x32; uint8_t _ = _addcarryx_u64(x29, x19, x30, &x32);
+  out[0] = x24;
+  out[1] = x28;
+  out[2] = x32;
+  }}}}}}}}}}}}}}}}
+}
diff --git a/src/Specific/montgomery64_2e129m25_3limbs/fesubDisplay.log b/src/Specific/montgomery64_2e129m25_3limbs/fesubDisplay.log
new file mode 100644
index 000000000..b792af81b
--- /dev/null
+++ b/src/Specific/montgomery64_2e129m25_3limbs/fesubDisplay.log
@@ -0,0 +1,17 @@
+λ x x0 : word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x6, x7, x5, (x10, x11, x9))%core,
+ uint64_t x13, uint8_t x14 = subborrow_u64(0x0, x5, x9);
+ uint64_t x16, uint8_t x17 = subborrow_u64(x14, x7, x11);
+ uint64_t x19, uint8_t x20 = subborrow_u64(x17, x6, x10);
+ uint64_t x21 = cmovznz64(x20, 0x0, 0xffffffffffffffffL);
+ uint64_t x22 = (x21 & 0xffffffffffffffe7L);
+ uint64_t x24, uint8_t x25 = addcarryx_u64(0x0, x13, x22);
+ uint64_t x26 = (x21 & 0xffffffffffffffffL);
+ uint64_t x28, uint8_t x29 = addcarryx_u64(x25, x16, x26);
+ uint8_t x30 = ((uint8_t)x21 & 0x1);
+ uint64_t x32, uint8_t _ = addcarryx_u64(x29, x19, x30);
+ (Return x32, Return x28, Return x24))
+(x, x0)%core
+     : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)