3 files changed, 164 insertions, 0 deletions
diff --git a/src/Specific/solinas32_2e256m189/femulDisplay.log b/src/Specific/solinas32_2e256m189/femulDisplay.log
new file mode 100644
index 000000000..5af81cff1
--- /dev/null
+++ b/src/Specific/solinas32_2e256m189/femulDisplay.log
@@ -0,0 +1,60 @@
+λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x24, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x46, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27))%core,
+ uint64_t x48 = (uint64_t) x5 * x46 + (0x2 * ((uint64_t) x7 * x47) + ((uint64_t) x9 * x45 + ((uint64_t) x11 * x43 + (0x2 * ((uint64_t) x13 * x41) + ((uint64_t) x15 * x39 + ((uint64_t) x17 * x37 + (0x2 * ((uint64_t) x19 * x35) + ((uint64_t) x21 * x33 + ((uint64_t) x23 * x31 + (0x2 * ((uint64_t) x25 * x29) + (uint64_t) x24 * x27))))))))));
+ uint64_t x49 = (uint64_t) x5 * x47 + ((uint64_t) x7 * x45 + ((uint64_t) x9 * x43 + ((uint64_t) x11 * x41 + ((uint64_t) x13 * x39 + ((uint64_t) x15 * x37 + ((uint64_t) x17 * x35 + ((uint64_t) x19 * x33 + ((uint64_t) x21 * x31 + ((uint64_t) x23 * x29 + (uint64_t) x25 * x27))))))))) + 0xbd * ((uint64_t) x24 * x46);
+ uint64_t x50 = (uint64_t) x5 * x45 + (0x2 * ((uint64_t) x7 * x43) + (0x2 * ((uint64_t) x9 * x41) + ((uint64_t) x11 * x39 + (0x2 * ((uint64_t) x13 * x37) + (0x2 * ((uint64_t) x15 * x35) + ((uint64_t) x17 * x33 + (0x2 * ((uint64_t) x19 * x31) + (0x2 * ((uint64_t) x21 * x29) + (uint64_t) x23 * x27)))))))) + 0xbd * (0x2 * ((uint64_t) x25 * x46) + 0x2 * ((uint64_t) x24 * x47));
+ uint64_t x51 = (uint64_t) x5 * x43 + (0x2 * ((uint64_t) x7 * x41) + ((uint64_t) x9 * x39 + ((uint64_t) x11 * x37 + (0x2 * ((uint64_t) x13 * x35) + ((uint64_t) x15 * x33 + ((uint64_t) x17 * x31 + (0x2 * ((uint64_t) x19 * x29) + (uint64_t) x21 * x27))))))) + 0xbd * ((uint64_t) x23 * x46 + (0x2 * ((uint64_t) x25 * x47) + (uint64_t) x24 * x45));
+ uint64_t x52 = (uint64_t) x5 * x41 + ((uint64_t) x7 * x39 + ((uint64_t) x9 * x37 + ((uint64_t) x11 * x35 + ((uint64_t) x13 * x33 + ((uint64_t) x15 * x31 + ((uint64_t) x17 * x29 + (uint64_t) x19 * x27)))))) + 0xbd * ((uint64_t) x21 * x46 + ((uint64_t) x23 * x47 + ((uint64_t) x25 * x45 + (uint64_t) x24 * x43)));
+ uint64_t x53 = (uint64_t) x5 * x39 + (0x2 * ((uint64_t) x7 * x37) + (0x2 * ((uint64_t) x9 * x35) + ((uint64_t) x11 * x33 + (0x2 * ((uint64_t) x13 * x31) + (0x2 * ((uint64_t) x15 * x29) + (uint64_t) x17 * x27))))) + 0xbd * (0x2 * ((uint64_t) x19 * x46) + (0x2 * ((uint64_t) x21 * x47) + ((uint64_t) x23 * x45 + (0x2 * ((uint64_t) x25 * x43) + 0x2 * ((uint64_t) x24 * x41)))));
+ uint64_t x54 = (uint64_t) x5 * x37 + (0x2 * ((uint64_t) x7 * x35) + ((uint64_t) x9 * x33 + ((uint64_t) x11 * x31 + (0x2 * ((uint64_t) x13 * x29) + (uint64_t) x15 * x27)))) + 0xbd * ((uint64_t) x17 * x46 + (0x2 * ((uint64_t) x19 * x47) + ((uint64_t) x21 * x45 + ((uint64_t) x23 * x43 + (0x2 * ((uint64_t) x25 * x41) + (uint64_t) x24 * x39)))));
+ uint64_t x55 = (uint64_t) x5 * x35 + ((uint64_t) x7 * x33 + ((uint64_t) x9 * x31 + ((uint64_t) x11 * x29 + (uint64_t) x13 * x27))) + 0xbd * ((uint64_t) x15 * x46 + ((uint64_t) x17 * x47 + ((uint64_t) x19 * x45 + ((uint64_t) x21 * x43 + ((uint64_t) x23 * x41 + ((uint64_t) x25 * x39 + (uint64_t) x24 * x37))))));
+ uint64_t x56 = (uint64_t) x5 * x33 + (0x2 * ((uint64_t) x7 * x31) + (0x2 * ((uint64_t) x9 * x29) + (uint64_t) x11 * x27)) + 0xbd * (0x2 * ((uint64_t) x13 * x46) + (0x2 * ((uint64_t) x15 * x47) + ((uint64_t) x17 * x45 + (0x2 * ((uint64_t) x19 * x43) + (0x2 * ((uint64_t) x21 * x41) + ((uint64_t) x23 * x39 + (0x2 * ((uint64_t) x25 * x37) + 0x2 * ((uint64_t) x24 * x35))))))));
+ uint64_t x57 = (uint64_t) x5 * x31 + (0x2 * ((uint64_t) x7 * x29) + (uint64_t) x9 * x27) + 0xbd * ((uint64_t) x11 * x46 + (0x2 * ((uint64_t) x13 * x47) + ((uint64_t) x15 * x45 + ((uint64_t) x17 * x43 + (0x2 * ((uint64_t) x19 * x41) + ((uint64_t) x21 * x39 + ((uint64_t) x23 * x37 + (0x2 * ((uint64_t) x25 * x35) + (uint64_t) x24 * x33))))))));
+ uint64_t x58 = (uint64_t) x5 * x29 + (uint64_t) x7 * x27 + 0xbd * ((uint64_t) x9 * x46 + ((uint64_t) x11 * x47 + ((uint64_t) x13 * x45 + ((uint64_t) x15 * x43 + ((uint64_t) x17 * x41 + ((uint64_t) x19 * x39 + ((uint64_t) x21 * x37 + ((uint64_t) x23 * x35 + ((uint64_t) x25 * x33 + (uint64_t) x24 * x31)))))))));
+ uint64_t x59 = (uint64_t) x5 * x27 + 0xbd * (0x2 * ((uint64_t) x7 * x46) + (0x2 * ((uint64_t) x9 * x47) + ((uint64_t) x11 * x45 + (0x2 * ((uint64_t) x13 * x43) + (0x2 * ((uint64_t) x15 * x41) + ((uint64_t) x17 * x39 + (0x2 * ((uint64_t) x19 * x37) + (0x2 * ((uint64_t) x21 * x35) + ((uint64_t) x23 * x33 + (0x2 * ((uint64_t) x25 * x31) + 0x2 * ((uint64_t) x24 * x29)))))))))));
+ uint64_t x60 = x59 >> 0x16;
+ uint32_t x61 = (uint32_t) x59 & 0x3fffff;
+ uint64_t x62 = x60 + x58;
+ uint64_t x63 = x62 >> 0x15;
+ uint32_t x64 = (uint32_t) x62 & 0x1fffff;
+ uint64_t x65 = x63 + x57;
+ uint64_t x66 = x65 >> 0x15;
+ uint32_t x67 = (uint32_t) x65 & 0x1fffff;
+ uint64_t x68 = x66 + x56;
+ uint64_t x69 = x68 >> 0x16;
+ uint32_t x70 = (uint32_t) x68 & 0x3fffff;
+ uint64_t x71 = x69 + x55;
+ uint64_t x72 = x71 >> 0x15;
+ uint32_t x73 = (uint32_t) x71 & 0x1fffff;
+ uint64_t x74 = x72 + x54;
+ uint64_t x75 = x74 >> 0x15;
+ uint32_t x76 = (uint32_t) x74 & 0x1fffff;
+ uint64_t x77 = x75 + x53;
+ uint32_t x78 = (uint32_t) (x77 >> 0x16);
+ uint32_t x79 = (uint32_t) x77 & 0x3fffff;
+ uint64_t x80 = x78 + x52;
+ uint32_t x81 = (uint32_t) (x80 >> 0x15);
+ uint32_t x82 = (uint32_t) x80 & 0x1fffff;
+ uint64_t x83 = x81 + x51;
+ uint32_t x84 = (uint32_t) (x83 >> 0x15);
+ uint32_t x85 = (uint32_t) x83 & 0x1fffff;
+ uint64_t x86 = x84 + x50;
+ uint32_t x87 = (uint32_t) (x86 >> 0x16);
+ uint32_t x88 = (uint32_t) x86 & 0x3fffff;
+ uint64_t x89 = x87 + x49;
+ uint32_t x90 = (uint32_t) (x89 >> 0x15);
+ uint32_t x91 = (uint32_t) x89 & 0x1fffff;
+ uint64_t x92 = x90 + x48;
+ uint32_t x93 = (uint32_t) (x92 >> 0x15);
+ uint32_t x94 = (uint32_t) x92 & 0x1fffff;
+ uint64_t x95 = x61 + (uint64_t) 0xbd * x93;
+ uint32_t x96 = (uint32_t) (x95 >> 0x16);
+ uint32_t x97 = (uint32_t) x95 & 0x3fffff;
+ uint32_t x98 = x96 + x64;
+ uint32_t x99 = x98 >> 0x15;
+ uint32_t x100 = x98 & 0x1fffff;
+ return (Return x94, Return x91, Return x88, Return x85, Return x82, Return x79, Return x76, Return x73, Return x70, x99 + x67, Return x100, Return x97))
+(x, x0)%core
+     : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * 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 * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e256m189/fesquareDisplay.log b/src/Specific/solinas32_2e256m189/fesquareDisplay.log
new file mode 100644
index 000000000..c9b917797
--- /dev/null
+++ b/src/Specific/solinas32_2e256m189/fesquareDisplay.log
@@ -0,0 +1,60 @@
+λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x21, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint64_t x23 = (uint64_t) x2 * x21 + (0x2 * ((uint64_t) x4 * x22) + ((uint64_t) x6 * x20 + ((uint64_t) x8 * x18 + (0x2 * ((uint64_t) x10 * x16) + ((uint64_t) x12 * x14 + ((uint64_t) x14 * x12 + (0x2 * ((uint64_t) x16 * x10) + ((uint64_t) x18 * x8 + ((uint64_t) x20 * x6 + (0x2 * ((uint64_t) x22 * x4) + (uint64_t) x21 * x2))))))))));
+ uint64_t x24 = (uint64_t) x2 * x22 + ((uint64_t) x4 * x20 + ((uint64_t) x6 * x18 + ((uint64_t) x8 * x16 + ((uint64_t) x10 * x14 + ((uint64_t) x12 * x12 + ((uint64_t) x14 * x10 + ((uint64_t) x16 * x8 + ((uint64_t) x18 * x6 + ((uint64_t) x20 * x4 + (uint64_t) x22 * x2))))))))) + 0xbd * ((uint64_t) x21 * x21);
+ uint64_t x25 = (uint64_t) x2 * x20 + (0x2 * ((uint64_t) x4 * x18) + (0x2 * ((uint64_t) x6 * x16) + ((uint64_t) x8 * x14 + (0x2 * ((uint64_t) x10 * x12) + (0x2 * ((uint64_t) x12 * x10) + ((uint64_t) x14 * x8 + (0x2 * ((uint64_t) x16 * x6) + (0x2 * ((uint64_t) x18 * x4) + (uint64_t) x20 * x2)))))))) + 0xbd * (0x2 * ((uint64_t) x22 * x21) + 0x2 * ((uint64_t) x21 * x22));
+ uint64_t x26 = (uint64_t) x2 * x18 + (0x2 * ((uint64_t) x4 * x16) + ((uint64_t) x6 * x14 + ((uint64_t) x8 * x12 + (0x2 * ((uint64_t) x10 * x10) + ((uint64_t) x12 * x8 + ((uint64_t) x14 * x6 + (0x2 * ((uint64_t) x16 * x4) + (uint64_t) x18 * x2))))))) + 0xbd * ((uint64_t) x20 * x21 + (0x2 * ((uint64_t) x22 * x22) + (uint64_t) x21 * x20));
+ uint64_t x27 = (uint64_t) x2 * x16 + ((uint64_t) x4 * x14 + ((uint64_t) x6 * x12 + ((uint64_t) x8 * x10 + ((uint64_t) x10 * x8 + ((uint64_t) x12 * x6 + ((uint64_t) x14 * x4 + (uint64_t) x16 * x2)))))) + 0xbd * ((uint64_t) x18 * x21 + ((uint64_t) x20 * x22 + ((uint64_t) x22 * x20 + (uint64_t) x21 * x18)));
+ uint64_t x28 = (uint64_t) x2 * x14 + (0x2 * ((uint64_t) x4 * x12) + (0x2 * ((uint64_t) x6 * x10) + ((uint64_t) x8 * x8 + (0x2 * ((uint64_t) x10 * x6) + (0x2 * ((uint64_t) x12 * x4) + (uint64_t) x14 * x2))))) + 0xbd * (0x2 * ((uint64_t) x16 * x21) + (0x2 * ((uint64_t) x18 * x22) + ((uint64_t) x20 * x20 + (0x2 * ((uint64_t) x22 * x18) + 0x2 * ((uint64_t) x21 * x16)))));
+ uint64_t x29 = (uint64_t) x2 * x12 + (0x2 * ((uint64_t) x4 * x10) + ((uint64_t) x6 * x8 + ((uint64_t) x8 * x6 + (0x2 * ((uint64_t) x10 * x4) + (uint64_t) x12 * x2)))) + 0xbd * ((uint64_t) x14 * x21 + (0x2 * ((uint64_t) x16 * x22) + ((uint64_t) x18 * x20 + ((uint64_t) x20 * x18 + (0x2 * ((uint64_t) x22 * x16) + (uint64_t) x21 * x14)))));
+ uint64_t x30 = (uint64_t) x2 * x10 + ((uint64_t) x4 * x8 + ((uint64_t) x6 * x6 + ((uint64_t) x8 * x4 + (uint64_t) x10 * x2))) + 0xbd * ((uint64_t) x12 * x21 + ((uint64_t) x14 * x22 + ((uint64_t) x16 * x20 + ((uint64_t) x18 * x18 + ((uint64_t) x20 * x16 + ((uint64_t) x22 * x14 + (uint64_t) x21 * x12))))));
+ uint64_t x31 = (uint64_t) x2 * x8 + (0x2 * ((uint64_t) x4 * x6) + (0x2 * ((uint64_t) x6 * x4) + (uint64_t) x8 * x2)) + 0xbd * (0x2 * ((uint64_t) x10 * x21) + (0x2 * ((uint64_t) x12 * x22) + ((uint64_t) x14 * x20 + (0x2 * ((uint64_t) x16 * x18) + (0x2 * ((uint64_t) x18 * x16) + ((uint64_t) x20 * x14 + (0x2 * ((uint64_t) x22 * x12) + 0x2 * ((uint64_t) x21 * x10))))))));
+ uint64_t x32 = (uint64_t) x2 * x6 + (0x2 * ((uint64_t) x4 * x4) + (uint64_t) x6 * x2) + 0xbd * ((uint64_t) x8 * x21 + (0x2 * ((uint64_t) x10 * x22) + ((uint64_t) x12 * x20 + ((uint64_t) x14 * x18 + (0x2 * ((uint64_t) x16 * x16) + ((uint64_t) x18 * x14 + ((uint64_t) x20 * x12 + (0x2 * ((uint64_t) x22 * x10) + (uint64_t) x21 * x8))))))));
+ uint64_t x33 = (uint64_t) x2 * x4 + (uint64_t) x4 * x2 + 0xbd * ((uint64_t) x6 * x21 + ((uint64_t) x8 * x22 + ((uint64_t) x10 * x20 + ((uint64_t) x12 * x18 + ((uint64_t) x14 * x16 + ((uint64_t) x16 * x14 + ((uint64_t) x18 * x12 + ((uint64_t) x20 * x10 + ((uint64_t) x22 * x8 + (uint64_t) x21 * x6)))))))));
+ uint64_t x34 = (uint64_t) x2 * x2 + 0xbd * (0x2 * ((uint64_t) x4 * x21) + (0x2 * ((uint64_t) x6 * x22) + ((uint64_t) x8 * x20 + (0x2 * ((uint64_t) x10 * x18) + (0x2 * ((uint64_t) x12 * x16) + ((uint64_t) x14 * x14 + (0x2 * ((uint64_t) x16 * x12) + (0x2 * ((uint64_t) x18 * x10) + ((uint64_t) x20 * x8 + (0x2 * ((uint64_t) x22 * x6) + 0x2 * ((uint64_t) x21 * x4)))))))))));
+ uint64_t x35 = x34 >> 0x16;
+ uint32_t x36 = (uint32_t) x34 & 0x3fffff;
+ uint64_t x37 = x35 + x33;
+ uint64_t x38 = x37 >> 0x15;
+ uint32_t x39 = (uint32_t) x37 & 0x1fffff;
+ uint64_t x40 = x38 + x32;
+ uint64_t x41 = x40 >> 0x15;
+ uint32_t x42 = (uint32_t) x40 & 0x1fffff;
+ uint64_t x43 = x41 + x31;
+ uint64_t x44 = x43 >> 0x16;
+ uint32_t x45 = (uint32_t) x43 & 0x3fffff;
+ uint64_t x46 = x44 + x30;
+ uint64_t x47 = x46 >> 0x15;
+ uint32_t x48 = (uint32_t) x46 & 0x1fffff;
+ uint64_t x49 = x47 + x29;
+ uint64_t x50 = x49 >> 0x15;
+ uint32_t x51 = (uint32_t) x49 & 0x1fffff;
+ uint64_t x52 = x50 + x28;
+ uint32_t x53 = (uint32_t) (x52 >> 0x16);
+ uint32_t x54 = (uint32_t) x52 & 0x3fffff;
+ uint64_t x55 = x53 + x27;
+ uint32_t x56 = (uint32_t) (x55 >> 0x15);
+ uint32_t x57 = (uint32_t) x55 & 0x1fffff;
+ uint64_t x58 = x56 + x26;
+ uint32_t x59 = (uint32_t) (x58 >> 0x15);
+ uint32_t x60 = (uint32_t) x58 & 0x1fffff;
+ uint64_t x61 = x59 + x25;
+ uint32_t x62 = (uint32_t) (x61 >> 0x16);
+ uint32_t x63 = (uint32_t) x61 & 0x3fffff;
+ uint64_t x64 = x62 + x24;
+ uint32_t x65 = (uint32_t) (x64 >> 0x15);
+ uint32_t x66 = (uint32_t) x64 & 0x1fffff;
+ uint64_t x67 = x65 + x23;
+ uint32_t x68 = (uint32_t) (x67 >> 0x15);
+ uint32_t x69 = (uint32_t) x67 & 0x1fffff;
+ uint64_t x70 = x36 + (uint64_t) 0xbd * x68;
+ uint32_t x71 = (uint32_t) (x70 >> 0x16);
+ uint32_t x72 = (uint32_t) x70 & 0x3fffff;
+ uint32_t x73 = x71 + x39;
+ uint32_t x74 = x73 >> 0x15;
+ uint32_t x75 = x73 & 0x1fffff;
+ return (Return x69, Return x66, Return x63, Return x60, Return x57, Return x54, Return x51, Return x48, Return x45, x74 + x42, Return x75, Return x72))
+x
+     : 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 * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e256m189/freezeDisplay.log b/src/Specific/solinas32_2e256m189/freezeDisplay.log
new file mode 100644
index 000000000..9a2478ece
--- /dev/null
+++ b/src/Specific/solinas32_2e256m189/freezeDisplay.log
@@ -0,0 +1,44 @@
+λ x : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x21, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint32_t x24, uint8_t x25 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x2, 0x3fff43);
+ uint32_t x27, uint8_t x28 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x25, Return x4, 0x1fffff);
+ uint32_t x30, uint8_t x31 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x28, Return x6, 0x1fffff);
+ uint32_t x33, uint8_t x34 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x31, Return x8, 0x3fffff);
+ uint32_t x36, uint8_t x37 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x34, Return x10, 0x1fffff);
+ uint32_t x39, uint8_t x40 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x37, Return x12, 0x1fffff);
+ uint32_t x42, uint8_t x43 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x40, Return x14, 0x3fffff);
+ uint32_t x45, uint8_t x46 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x43, Return x16, 0x1fffff);
+ uint32_t x48, uint8_t x49 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x46, Return x18, 0x1fffff);
+ uint32_t x51, uint8_t x52 = Op (Syntax.SubWithGetBorrow 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x49, Return x20, 0x3fffff);
+ uint32_t x54, uint8_t x55 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x52, Return x22, 0x1fffff);
+ uint32_t x57, uint8_t x58 = Op (Syntax.SubWithGetBorrow 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x55, Return x21, 0x1fffff);
+ uint32_t x59 = (uint32_t)cmovznz(x58, 0x0, 0xffffffff);
+ uint32_t x60 = x59 & 0x3fff43;
+ uint32_t x62, uint8_t x63 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (0x0, Return x24, Return x60);
+ uint32_t x64 = x59 & 0x1fffff;
+ uint32_t x66, uint8_t x67 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x63, Return x27, Return x64);
+ uint32_t x68 = x59 & 0x1fffff;
+ uint32_t x70, uint8_t x71 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x67, Return x30, Return x68);
+ uint32_t x72 = x59 & 0x3fffff;
+ uint32_t x74, uint8_t x75 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x71, Return x33, Return x72);
+ uint32_t x76 = x59 & 0x1fffff;
+ uint32_t x78, uint8_t x79 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x75, Return x36, Return x76);
+ uint32_t x80 = x59 & 0x1fffff;
+ uint32_t x82, uint8_t x83 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x79, Return x39, Return x80);
+ uint32_t x84 = x59 & 0x3fffff;
+ uint32_t x86, uint8_t x87 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x83, Return x42, Return x84);
+ uint32_t x88 = x59 & 0x1fffff;
+ uint32_t x90, uint8_t x91 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x87, Return x45, Return x88);
+ uint32_t x92 = x59 & 0x1fffff;
+ uint32_t x94, uint8_t x95 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x91, Return x48, Return x92);
+ uint32_t x96 = x59 & 0x3fffff;
+ uint32_t x98, uint8_t x99 = Op (Syntax.AddWithGetCarry 22 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x95, Return x51, Return x96);
+ uint32_t x100 = x59 & 0x1fffff;
+ uint32_t x102, uint8_t x103 = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x99, Return x54, Return x100);
+ uint32_t x104 = x59 & 0x1fffff;
+ uint32_t x106, uint8_t _ = Op (Syntax.AddWithGetCarry 21 (Syntax.TWord 3) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 5) (Syntax.TWord 3)) (Return x103, Return x57, Return x104);
+ (Return x106, Return x102, Return x98, Return x94, Return x90, Return x86, Return x82, Return x78, Return x74, Return x70, Return x66, Return x62))
+x
+     : 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 * uint32_t * uint32_t * uint32_t * uint32_t)