Update display logs and c files

9 files changed, 463 insertions, 0 deletions

diff --git a/src/Specific/solinas64_2e488m17/femul.c b/src/Specific/solinas64_2e488m17/femul.c
new file mode 100644
index 000000000..155b528f3
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/femul.c
@@ -0,0 +1,106 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <x86intrin.h>
+#include "liblow.h"
+
+#include "femul.h"
+
+typedef unsigned int uint128_t __attribute__((mode(TI)));
+
+#if (defined(__GNUC__) || defined(__GNUG__)) && !(defined(__clang__)||defined(__INTEL_COMPILER))
+// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
+#define _subborrow_u32 __builtin_ia32_sbb_u32
+#define _subborrow_u64 __builtin_ia32_sbb_u64
+#endif
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline femul(uint64_t* out, uint64_t x32, uint64_t x33, uint64_t x31, uint64_t x29, uint64_t x27, uint64_t x25, uint64_t x23, uint64_t x21, uint64_t x19, uint64_t x17, uint64_t x15, uint64_t x13, uint64_t x11, uint64_t x9, uint64_t x7, uint64_t x5, uint64_t x62, uint64_t x63, uint64_t x61, uint64_t x59, uint64_t x57, uint64_t x55, uint64_t x53, uint64_t x51, uint64_t x49, uint64_t x47, uint64_t x45, uint64_t x43, uint64_t x41, uint64_t x39, uint64_t x37, uint64_t x35)
+{  uint128_t x64 = (((uint128_t)x5 * x62) + (((uint128_t)x7 * x63) + (((uint128_t)x9 * x61) + (((uint128_t)x11 * x59) + (((uint128_t)x13 * x57) + (((uint128_t)x15 * x55) + (((uint128_t)x17 * x53) + (((uint128_t)x19 * x51) + (((uint128_t)x21 * x49) + (((uint128_t)x23 * x47) + (((uint128_t)x25 * x45) + (((uint128_t)x27 * x43) + (((uint128_t)x29 * x41) + (((uint128_t)x31 * x39) + (((uint128_t)x33 * x37) + ((uint128_t)x32 * x35))))))))))))))));
+{  uint128_t x65 = ((((uint128_t)x5 * x63) + (((uint128_t)0x2 * (x7 * x61)) + (((uint128_t)x9 * x59) + (((uint128_t)0x2 * (x11 * x57)) + (((uint128_t)x13 * x55) + (((uint128_t)0x2 * (x15 * x53)) + (((uint128_t)x17 * x51) + (((uint128_t)0x2 * (x19 * x49)) + (((uint128_t)x21 * x47) + (((uint128_t)0x2 * (x23 * x45)) + (((uint128_t)x25 * x43) + (((uint128_t)0x2 * (x27 * x41)) + (((uint128_t)x29 * x39) + (((uint128_t)0x2 * (x31 * x37)) + ((uint128_t)x33 * x35))))))))))))))) + (0x11 * ((uint128_t)0x2 * (x32 * x62))));
+{  uint128_t x66 = ((((uint128_t)x5 * x61) + (((uint128_t)x7 * x59) + (((uint128_t)x9 * x57) + (((uint128_t)x11 * x55) + (((uint128_t)x13 * x53) + (((uint128_t)x15 * x51) + (((uint128_t)x17 * x49) + (((uint128_t)x19 * x47) + (((uint128_t)x21 * x45) + (((uint128_t)x23 * x43) + (((uint128_t)x25 * x41) + (((uint128_t)x27 * x39) + (((uint128_t)x29 * x37) + ((uint128_t)x31 * x35)))))))))))))) + (0x11 * (((uint128_t)x33 * x62) + ((uint128_t)x32 * x63))));
+{  uint128_t x67 = ((((uint128_t)x5 * x59) + (((uint128_t)0x2 * (x7 * x57)) + (((uint128_t)x9 * x55) + (((uint128_t)0x2 * (x11 * x53)) + (((uint128_t)x13 * x51) + (((uint128_t)0x2 * (x15 * x49)) + (((uint128_t)x17 * x47) + (((uint128_t)0x2 * (x19 * x45)) + (((uint128_t)x21 * x43) + (((uint128_t)0x2 * (x23 * x41)) + (((uint128_t)x25 * x39) + (((uint128_t)0x2 * (x27 * x37)) + ((uint128_t)x29 * x35))))))))))))) + (0x11 * (((uint128_t)0x2 * (x31 * x62)) + (((uint128_t)x33 * x63) + ((uint128_t)0x2 * (x32 * x61))))));
+{  uint128_t x68 = ((((uint128_t)x5 * x57) + (((uint128_t)x7 * x55) + (((uint128_t)x9 * x53) + (((uint128_t)x11 * x51) + (((uint128_t)x13 * x49) + (((uint128_t)x15 * x47) + (((uint128_t)x17 * x45) + (((uint128_t)x19 * x43) + (((uint128_t)x21 * x41) + (((uint128_t)x23 * x39) + (((uint128_t)x25 * x37) + ((uint128_t)x27 * x35)))))))))))) + (0x11 * (((uint128_t)x29 * x62) + (((uint128_t)x31 * x63) + (((uint128_t)x33 * x61) + ((uint128_t)x32 * x59))))));
+{  uint128_t x69 = ((((uint128_t)x5 * x55) + (((uint128_t)0x2 * (x7 * x53)) + (((uint128_t)x9 * x51) + (((uint128_t)0x2 * (x11 * x49)) + (((uint128_t)x13 * x47) + (((uint128_t)0x2 * (x15 * x45)) + (((uint128_t)x17 * x43) + (((uint128_t)0x2 * (x19 * x41)) + (((uint128_t)x21 * x39) + (((uint128_t)0x2 * (x23 * x37)) + ((uint128_t)x25 * x35))))))))))) + (0x11 * (((uint128_t)0x2 * (x27 * x62)) + (((uint128_t)x29 * x63) + (((uint128_t)0x2 * (x31 * x61)) + (((uint128_t)x33 * x59) + ((uint128_t)0x2 * (x32 * x57))))))));
+{  uint128_t x70 = ((((uint128_t)x5 * x53) + (((uint128_t)x7 * x51) + (((uint128_t)x9 * x49) + (((uint128_t)x11 * x47) + (((uint128_t)x13 * x45) + (((uint128_t)x15 * x43) + (((uint128_t)x17 * x41) + (((uint128_t)x19 * x39) + (((uint128_t)x21 * x37) + ((uint128_t)x23 * x35)))))))))) + (0x11 * (((uint128_t)x25 * x62) + (((uint128_t)x27 * x63) + (((uint128_t)x29 * x61) + (((uint128_t)x31 * x59) + (((uint128_t)x33 * x57) + ((uint128_t)x32 * x55))))))));
+{  uint128_t x71 = ((((uint128_t)x5 * x51) + (((uint128_t)0x2 * (x7 * x49)) + (((uint128_t)x9 * x47) + (((uint128_t)0x2 * (x11 * x45)) + (((uint128_t)x13 * x43) + (((uint128_t)0x2 * (x15 * x41)) + (((uint128_t)x17 * x39) + (((uint128_t)0x2 * (x19 * x37)) + ((uint128_t)x21 * x35))))))))) + (0x11 * (((uint128_t)0x2 * (x23 * x62)) + (((uint128_t)x25 * x63) + (((uint128_t)0x2 * (x27 * x61)) + (((uint128_t)x29 * x59) + (((uint128_t)0x2 * (x31 * x57)) + (((uint128_t)x33 * x55) + ((uint128_t)0x2 * (x32 * x53))))))))));
+{  uint128_t x72 = ((((uint128_t)x5 * x49) + (((uint128_t)x7 * x47) + (((uint128_t)x9 * x45) + (((uint128_t)x11 * x43) + (((uint128_t)x13 * x41) + (((uint128_t)x15 * x39) + (((uint128_t)x17 * x37) + ((uint128_t)x19 * x35)))))))) + (0x11 * (((uint128_t)x21 * x62) + (((uint128_t)x23 * x63) + (((uint128_t)x25 * x61) + (((uint128_t)x27 * x59) + (((uint128_t)x29 * x57) + (((uint128_t)x31 * x55) + (((uint128_t)x33 * x53) + ((uint128_t)x32 * x51))))))))));
+{  uint128_t x73 = ((((uint128_t)x5 * x47) + (((uint128_t)0x2 * (x7 * x45)) + (((uint128_t)x9 * x43) + (((uint128_t)0x2 * (x11 * x41)) + (((uint128_t)x13 * x39) + (((uint128_t)0x2 * (x15 * x37)) + ((uint128_t)x17 * x35))))))) + (0x11 * (((uint128_t)0x2 * (x19 * x62)) + (((uint128_t)x21 * x63) + (((uint128_t)0x2 * (x23 * x61)) + (((uint128_t)x25 * x59) + (((uint128_t)0x2 * (x27 * x57)) + (((uint128_t)x29 * x55) + (((uint128_t)0x2 * (x31 * x53)) + (((uint128_t)x33 * x51) + ((uint128_t)0x2 * (x32 * x49))))))))))));
+{  uint128_t x74 = ((((uint128_t)x5 * x45) + (((uint128_t)x7 * x43) + (((uint128_t)x9 * x41) + (((uint128_t)x11 * x39) + (((uint128_t)x13 * x37) + ((uint128_t)x15 * x35)))))) + (0x11 * (((uint128_t)x17 * x62) + (((uint128_t)x19 * x63) + (((uint128_t)x21 * x61) + (((uint128_t)x23 * x59) + (((uint128_t)x25 * x57) + (((uint128_t)x27 * x55) + (((uint128_t)x29 * x53) + (((uint128_t)x31 * x51) + (((uint128_t)x33 * x49) + ((uint128_t)x32 * x47))))))))))));
+{  uint128_t x75 = ((((uint128_t)x5 * x43) + (((uint128_t)0x2 * (x7 * x41)) + (((uint128_t)x9 * x39) + (((uint128_t)0x2 * (x11 * x37)) + ((uint128_t)x13 * x35))))) + (0x11 * (((uint128_t)0x2 * (x15 * x62)) + (((uint128_t)x17 * x63) + (((uint128_t)0x2 * (x19 * x61)) + (((uint128_t)x21 * x59) + (((uint128_t)0x2 * (x23 * x57)) + (((uint128_t)x25 * x55) + (((uint128_t)0x2 * (x27 * x53)) + (((uint128_t)x29 * x51) + (((uint128_t)0x2 * (x31 * x49)) + (((uint128_t)x33 * x47) + ((uint128_t)0x2 * (x32 * x45))))))))))))));
+{  uint128_t x76 = ((((uint128_t)x5 * x41) + (((uint128_t)x7 * x39) + (((uint128_t)x9 * x37) + ((uint128_t)x11 * x35)))) + (0x11 * (((uint128_t)x13 * x62) + (((uint128_t)x15 * x63) + (((uint128_t)x17 * x61) + (((uint128_t)x19 * x59) + (((uint128_t)x21 * x57) + (((uint128_t)x23 * x55) + (((uint128_t)x25 * x53) + (((uint128_t)x27 * x51) + (((uint128_t)x29 * x49) + (((uint128_t)x31 * x47) + (((uint128_t)x33 * x45) + ((uint128_t)x32 * x43))))))))))))));
+{  uint128_t x77 = ((((uint128_t)x5 * x39) + (((uint128_t)0x2 * (x7 * x37)) + ((uint128_t)x9 * x35))) + (0x11 * (((uint128_t)0x2 * (x11 * x62)) + (((uint128_t)x13 * x63) + (((uint128_t)0x2 * (x15 * x61)) + (((uint128_t)x17 * x59) + (((uint128_t)0x2 * (x19 * x57)) + (((uint128_t)x21 * x55) + (((uint128_t)0x2 * (x23 * x53)) + (((uint128_t)x25 * x51) + (((uint128_t)0x2 * (x27 * x49)) + (((uint128_t)x29 * x47) + (((uint128_t)0x2 * (x31 * x45)) + (((uint128_t)x33 * x43) + ((uint128_t)0x2 * (x32 * x41))))))))))))))));
+{  uint128_t x78 = ((((uint128_t)x5 * x37) + ((uint128_t)x7 * x35)) + (0x11 * (((uint128_t)x9 * x62) + (((uint128_t)x11 * x63) + (((uint128_t)x13 * x61) + (((uint128_t)x15 * x59) + (((uint128_t)x17 * x57) + (((uint128_t)x19 * x55) + (((uint128_t)x21 * x53) + (((uint128_t)x23 * x51) + (((uint128_t)x25 * x49) + (((uint128_t)x27 * x47) + (((uint128_t)x29 * x45) + (((uint128_t)x31 * x43) + (((uint128_t)x33 * x41) + ((uint128_t)x32 * x39))))))))))))))));
+{  uint128_t x79 = (((uint128_t)x5 * x35) + (0x11 * (((uint128_t)0x2 * (x7 * x62)) + (((uint128_t)x9 * x63) + (((uint128_t)0x2 * (x11 * x61)) + (((uint128_t)x13 * x59) + (((uint128_t)0x2 * (x15 * x57)) + (((uint128_t)x17 * x55) + (((uint128_t)0x2 * (x19 * x53)) + (((uint128_t)x21 * x51) + (((uint128_t)0x2 * (x23 * x49)) + (((uint128_t)x25 * x47) + (((uint128_t)0x2 * (x27 * x45)) + (((uint128_t)x29 * x43) + (((uint128_t)0x2 * (x31 * x41)) + (((uint128_t)x33 * x39) + ((uint128_t)0x2 * (x32 * x37))))))))))))))))));
+{  uint64_t x80 = (uint64_t) (x79 >> 0x1f);
+{  uint64_t x81 = ((uint64_t)x79 & 0x7fffffff);
+{  uint128_t x82 = (x80 + x78);
+{  uint64_t x83 = (uint64_t) (x82 >> 0x1e);
+{  uint64_t x84 = ((uint64_t)x82 & 0x3fffffff);
+{  uint128_t x85 = (x83 + x77);
+{  uint64_t x86 = (uint64_t) (x85 >> 0x1f);
+{  uint64_t x87 = ((uint64_t)x85 & 0x7fffffff);
+{  uint128_t x88 = (x86 + x76);
+{  uint64_t x89 = (uint64_t) (x88 >> 0x1e);
+{  uint64_t x90 = ((uint64_t)x88 & 0x3fffffff);
+{  uint128_t x91 = (x89 + x75);
+{  uint64_t x92 = (uint64_t) (x91 >> 0x1f);
+{  uint64_t x93 = ((uint64_t)x91 & 0x7fffffff);
+{  uint128_t x94 = (x92 + x74);
+{  uint64_t x95 = (uint64_t) (x94 >> 0x1e);
+{  uint64_t x96 = ((uint64_t)x94 & 0x3fffffff);
+{  uint128_t x97 = (x95 + x73);
+{  uint64_t x98 = (uint64_t) (x97 >> 0x1f);
+{  uint64_t x99 = ((uint64_t)x97 & 0x7fffffff);
+{  uint128_t x100 = (x98 + x72);
+{  uint64_t x101 = (uint64_t) (x100 >> 0x1e);
+{  uint64_t x102 = ((uint64_t)x100 & 0x3fffffff);
+{  uint128_t x103 = (x101 + x71);
+{  uint64_t x104 = (uint64_t) (x103 >> 0x1f);
+{  uint64_t x105 = ((uint64_t)x103 & 0x7fffffff);
+{  uint128_t x106 = (x104 + x70);
+{  uint64_t x107 = (uint64_t) (x106 >> 0x1e);
+{  uint64_t x108 = ((uint64_t)x106 & 0x3fffffff);
+{  uint128_t x109 = (x107 + x69);
+{  uint64_t x110 = (uint64_t) (x109 >> 0x1f);
+{  uint64_t x111 = ((uint64_t)x109 & 0x7fffffff);
+{  uint128_t x112 = (x110 + x68);
+{  uint64_t x113 = (uint64_t) (x112 >> 0x1e);
+{  uint64_t x114 = ((uint64_t)x112 & 0x3fffffff);
+{  uint128_t x115 = (x113 + x67);
+{  uint64_t x116 = (uint64_t) (x115 >> 0x1f);
+{  uint64_t x117 = ((uint64_t)x115 & 0x7fffffff);
+{  uint128_t x118 = (x116 + x66);
+{  uint64_t x119 = (uint64_t) (x118 >> 0x1e);
+{  uint64_t x120 = ((uint64_t)x118 & 0x3fffffff);
+{  uint128_t x121 = (x119 + x65);
+{  uint64_t x122 = (uint64_t) (x121 >> 0x1f);
+{  uint64_t x123 = ((uint64_t)x121 & 0x7fffffff);
+{  uint128_t x124 = (x122 + x64);
+{  uint64_t x125 = (uint64_t) (x124 >> 0x1e);
+{  uint64_t x126 = ((uint64_t)x124 & 0x3fffffff);
+{  uint64_t x127 = (x81 + (0x11 * x125));
+{  uint64_t x128 = (x127 >> 0x1f);
+{  uint64_t x129 = (x127 & 0x7fffffff);
+{  uint64_t x130 = (x128 + x84);
+{  uint64_t x131 = (x130 >> 0x1e);
+{  uint64_t x132 = (x130 & 0x3fffffff);
+out[0] = x126;
+out[1] = x123;
+out[2] = x120;
+out[3] = x117;
+out[4] = x114;
+out[5] = x111;
+out[6] = x108;
+out[7] = x105;
+out[8] = x102;
+out[9] = x99;
+out[10] = x96;
+out[11] = x93;
+out[12] = x90;
+out[13] = x131 + x87;
+out[14] = x132;
+out[15] = x129;
+}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+// caller: uint64_t out[16];
diff --git a/src/Specific/solinas64_2e488m17/femul.h b/src/Specific/solinas64_2e488m17/femul.h
new file mode 100644
index 000000000..c4089fc7d
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/femul.h
@@ -0,0 +1,6 @@
+#include <stdint.h>
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline femul(uint64_t* out, uint64_t x32, uint64_t x33, uint64_t x31, uint64_t x29, uint64_t x27, uint64_t x25, uint64_t x23, uint64_t x21, uint64_t x19, uint64_t x17, uint64_t x15, uint64_t x13, uint64_t x11, uint64_t x9, uint64_t x7, uint64_t x5, uint64_t x62, uint64_t x63, uint64_t x61, uint64_t x59, uint64_t x57, uint64_t x55, uint64_t x53, uint64_t x51, uint64_t x49, uint64_t x47, uint64_t x45, uint64_t x43, uint64_t x41, uint64_t x39, uint64_t x37, uint64_t x35);
diff --git a/src/Specific/solinas64_2e488m17/femulDisplay.log b/src/Specific/solinas64_2e488m17/femulDisplay.log
new file mode 100644
index 000000000..1a52d2920
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/femulDisplay.log
@@ -0,0 +1,76 @@
+λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x32, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x62, x63, x61, x59, x57, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35))%core,
+ uint128_t x64 = (((uint128_t)x5 * x62) + (((uint128_t)x7 * x63) + (((uint128_t)x9 * x61) + (((uint128_t)x11 * x59) + (((uint128_t)x13 * x57) + (((uint128_t)x15 * x55) + (((uint128_t)x17 * x53) + (((uint128_t)x19 * x51) + (((uint128_t)x21 * x49) + (((uint128_t)x23 * x47) + (((uint128_t)x25 * x45) + (((uint128_t)x27 * x43) + (((uint128_t)x29 * x41) + (((uint128_t)x31 * x39) + (((uint128_t)x33 * x37) + ((uint128_t)x32 * x35))))))))))))))));
+ uint128_t x65 = ((((uint128_t)x5 * x63) + (((uint128_t)0x2 * (x7 * x61)) + (((uint128_t)x9 * x59) + (((uint128_t)0x2 * (x11 * x57)) + (((uint128_t)x13 * x55) + (((uint128_t)0x2 * (x15 * x53)) + (((uint128_t)x17 * x51) + (((uint128_t)0x2 * (x19 * x49)) + (((uint128_t)x21 * x47) + (((uint128_t)0x2 * (x23 * x45)) + (((uint128_t)x25 * x43) + (((uint128_t)0x2 * (x27 * x41)) + (((uint128_t)x29 * x39) + (((uint128_t)0x2 * (x31 * x37)) + ((uint128_t)x33 * x35))))))))))))))) + (0x11 * ((uint128_t)0x2 * (x32 * x62))));
+ uint128_t x66 = ((((uint128_t)x5 * x61) + (((uint128_t)x7 * x59) + (((uint128_t)x9 * x57) + (((uint128_t)x11 * x55) + (((uint128_t)x13 * x53) + (((uint128_t)x15 * x51) + (((uint128_t)x17 * x49) + (((uint128_t)x19 * x47) + (((uint128_t)x21 * x45) + (((uint128_t)x23 * x43) + (((uint128_t)x25 * x41) + (((uint128_t)x27 * x39) + (((uint128_t)x29 * x37) + ((uint128_t)x31 * x35)))))))))))))) + (0x11 * (((uint128_t)x33 * x62) + ((uint128_t)x32 * x63))));
+ uint128_t x67 = ((((uint128_t)x5 * x59) + (((uint128_t)0x2 * (x7 * x57)) + (((uint128_t)x9 * x55) + (((uint128_t)0x2 * (x11 * x53)) + (((uint128_t)x13 * x51) + (((uint128_t)0x2 * (x15 * x49)) + (((uint128_t)x17 * x47) + (((uint128_t)0x2 * (x19 * x45)) + (((uint128_t)x21 * x43) + (((uint128_t)0x2 * (x23 * x41)) + (((uint128_t)x25 * x39) + (((uint128_t)0x2 * (x27 * x37)) + ((uint128_t)x29 * x35))))))))))))) + (0x11 * (((uint128_t)0x2 * (x31 * x62)) + (((uint128_t)x33 * x63) + ((uint128_t)0x2 * (x32 * x61))))));
+ uint128_t x68 = ((((uint128_t)x5 * x57) + (((uint128_t)x7 * x55) + (((uint128_t)x9 * x53) + (((uint128_t)x11 * x51) + (((uint128_t)x13 * x49) + (((uint128_t)x15 * x47) + (((uint128_t)x17 * x45) + (((uint128_t)x19 * x43) + (((uint128_t)x21 * x41) + (((uint128_t)x23 * x39) + (((uint128_t)x25 * x37) + ((uint128_t)x27 * x35)))))))))))) + (0x11 * (((uint128_t)x29 * x62) + (((uint128_t)x31 * x63) + (((uint128_t)x33 * x61) + ((uint128_t)x32 * x59))))));
+ uint128_t x69 = ((((uint128_t)x5 * x55) + (((uint128_t)0x2 * (x7 * x53)) + (((uint128_t)x9 * x51) + (((uint128_t)0x2 * (x11 * x49)) + (((uint128_t)x13 * x47) + (((uint128_t)0x2 * (x15 * x45)) + (((uint128_t)x17 * x43) + (((uint128_t)0x2 * (x19 * x41)) + (((uint128_t)x21 * x39) + (((uint128_t)0x2 * (x23 * x37)) + ((uint128_t)x25 * x35))))))))))) + (0x11 * (((uint128_t)0x2 * (x27 * x62)) + (((uint128_t)x29 * x63) + (((uint128_t)0x2 * (x31 * x61)) + (((uint128_t)x33 * x59) + ((uint128_t)0x2 * (x32 * x57))))))));
+ uint128_t x70 = ((((uint128_t)x5 * x53) + (((uint128_t)x7 * x51) + (((uint128_t)x9 * x49) + (((uint128_t)x11 * x47) + (((uint128_t)x13 * x45) + (((uint128_t)x15 * x43) + (((uint128_t)x17 * x41) + (((uint128_t)x19 * x39) + (((uint128_t)x21 * x37) + ((uint128_t)x23 * x35)))))))))) + (0x11 * (((uint128_t)x25 * x62) + (((uint128_t)x27 * x63) + (((uint128_t)x29 * x61) + (((uint128_t)x31 * x59) + (((uint128_t)x33 * x57) + ((uint128_t)x32 * x55))))))));
+ uint128_t x71 = ((((uint128_t)x5 * x51) + (((uint128_t)0x2 * (x7 * x49)) + (((uint128_t)x9 * x47) + (((uint128_t)0x2 * (x11 * x45)) + (((uint128_t)x13 * x43) + (((uint128_t)0x2 * (x15 * x41)) + (((uint128_t)x17 * x39) + (((uint128_t)0x2 * (x19 * x37)) + ((uint128_t)x21 * x35))))))))) + (0x11 * (((uint128_t)0x2 * (x23 * x62)) + (((uint128_t)x25 * x63) + (((uint128_t)0x2 * (x27 * x61)) + (((uint128_t)x29 * x59) + (((uint128_t)0x2 * (x31 * x57)) + (((uint128_t)x33 * x55) + ((uint128_t)0x2 * (x32 * x53))))))))));
+ uint128_t x72 = ((((uint128_t)x5 * x49) + (((uint128_t)x7 * x47) + (((uint128_t)x9 * x45) + (((uint128_t)x11 * x43) + (((uint128_t)x13 * x41) + (((uint128_t)x15 * x39) + (((uint128_t)x17 * x37) + ((uint128_t)x19 * x35)))))))) + (0x11 * (((uint128_t)x21 * x62) + (((uint128_t)x23 * x63) + (((uint128_t)x25 * x61) + (((uint128_t)x27 * x59) + (((uint128_t)x29 * x57) + (((uint128_t)x31 * x55) + (((uint128_t)x33 * x53) + ((uint128_t)x32 * x51))))))))));
+ uint128_t x73 = ((((uint128_t)x5 * x47) + (((uint128_t)0x2 * (x7 * x45)) + (((uint128_t)x9 * x43) + (((uint128_t)0x2 * (x11 * x41)) + (((uint128_t)x13 * x39) + (((uint128_t)0x2 * (x15 * x37)) + ((uint128_t)x17 * x35))))))) + (0x11 * (((uint128_t)0x2 * (x19 * x62)) + (((uint128_t)x21 * x63) + (((uint128_t)0x2 * (x23 * x61)) + (((uint128_t)x25 * x59) + (((uint128_t)0x2 * (x27 * x57)) + (((uint128_t)x29 * x55) + (((uint128_t)0x2 * (x31 * x53)) + (((uint128_t)x33 * x51) + ((uint128_t)0x2 * (x32 * x49))))))))))));
+ uint128_t x74 = ((((uint128_t)x5 * x45) + (((uint128_t)x7 * x43) + (((uint128_t)x9 * x41) + (((uint128_t)x11 * x39) + (((uint128_t)x13 * x37) + ((uint128_t)x15 * x35)))))) + (0x11 * (((uint128_t)x17 * x62) + (((uint128_t)x19 * x63) + (((uint128_t)x21 * x61) + (((uint128_t)x23 * x59) + (((uint128_t)x25 * x57) + (((uint128_t)x27 * x55) + (((uint128_t)x29 * x53) + (((uint128_t)x31 * x51) + (((uint128_t)x33 * x49) + ((uint128_t)x32 * x47))))))))))));
+ uint128_t x75 = ((((uint128_t)x5 * x43) + (((uint128_t)0x2 * (x7 * x41)) + (((uint128_t)x9 * x39) + (((uint128_t)0x2 * (x11 * x37)) + ((uint128_t)x13 * x35))))) + (0x11 * (((uint128_t)0x2 * (x15 * x62)) + (((uint128_t)x17 * x63) + (((uint128_t)0x2 * (x19 * x61)) + (((uint128_t)x21 * x59) + (((uint128_t)0x2 * (x23 * x57)) + (((uint128_t)x25 * x55) + (((uint128_t)0x2 * (x27 * x53)) + (((uint128_t)x29 * x51) + (((uint128_t)0x2 * (x31 * x49)) + (((uint128_t)x33 * x47) + ((uint128_t)0x2 * (x32 * x45))))))))))))));
+ uint128_t x76 = ((((uint128_t)x5 * x41) + (((uint128_t)x7 * x39) + (((uint128_t)x9 * x37) + ((uint128_t)x11 * x35)))) + (0x11 * (((uint128_t)x13 * x62) + (((uint128_t)x15 * x63) + (((uint128_t)x17 * x61) + (((uint128_t)x19 * x59) + (((uint128_t)x21 * x57) + (((uint128_t)x23 * x55) + (((uint128_t)x25 * x53) + (((uint128_t)x27 * x51) + (((uint128_t)x29 * x49) + (((uint128_t)x31 * x47) + (((uint128_t)x33 * x45) + ((uint128_t)x32 * x43))))))))))))));
+ uint128_t x77 = ((((uint128_t)x5 * x39) + (((uint128_t)0x2 * (x7 * x37)) + ((uint128_t)x9 * x35))) + (0x11 * (((uint128_t)0x2 * (x11 * x62)) + (((uint128_t)x13 * x63) + (((uint128_t)0x2 * (x15 * x61)) + (((uint128_t)x17 * x59) + (((uint128_t)0x2 * (x19 * x57)) + (((uint128_t)x21 * x55) + (((uint128_t)0x2 * (x23 * x53)) + (((uint128_t)x25 * x51) + (((uint128_t)0x2 * (x27 * x49)) + (((uint128_t)x29 * x47) + (((uint128_t)0x2 * (x31 * x45)) + (((uint128_t)x33 * x43) + ((uint128_t)0x2 * (x32 * x41))))))))))))))));
+ uint128_t x78 = ((((uint128_t)x5 * x37) + ((uint128_t)x7 * x35)) + (0x11 * (((uint128_t)x9 * x62) + (((uint128_t)x11 * x63) + (((uint128_t)x13 * x61) + (((uint128_t)x15 * x59) + (((uint128_t)x17 * x57) + (((uint128_t)x19 * x55) + (((uint128_t)x21 * x53) + (((uint128_t)x23 * x51) + (((uint128_t)x25 * x49) + (((uint128_t)x27 * x47) + (((uint128_t)x29 * x45) + (((uint128_t)x31 * x43) + (((uint128_t)x33 * x41) + ((uint128_t)x32 * x39))))))))))))))));
+ uint128_t x79 = (((uint128_t)x5 * x35) + (0x11 * (((uint128_t)0x2 * (x7 * x62)) + (((uint128_t)x9 * x63) + (((uint128_t)0x2 * (x11 * x61)) + (((uint128_t)x13 * x59) + (((uint128_t)0x2 * (x15 * x57)) + (((uint128_t)x17 * x55) + (((uint128_t)0x2 * (x19 * x53)) + (((uint128_t)x21 * x51) + (((uint128_t)0x2 * (x23 * x49)) + (((uint128_t)x25 * x47) + (((uint128_t)0x2 * (x27 * x45)) + (((uint128_t)x29 * x43) + (((uint128_t)0x2 * (x31 * x41)) + (((uint128_t)x33 * x39) + ((uint128_t)0x2 * (x32 * x37))))))))))))))))));
+ uint64_t x80 = (uint64_t) (x79 >> 0x1f);
+ uint64_t x81 = ((uint64_t)x79 & 0x7fffffff);
+ uint128_t x82 = (x80 + x78);
+ uint64_t x83 = (uint64_t) (x82 >> 0x1e);
+ uint64_t x84 = ((uint64_t)x82 & 0x3fffffff);
+ uint128_t x85 = (x83 + x77);
+ uint64_t x86 = (uint64_t) (x85 >> 0x1f);
+ uint64_t x87 = ((uint64_t)x85 & 0x7fffffff);
+ uint128_t x88 = (x86 + x76);
+ uint64_t x89 = (uint64_t) (x88 >> 0x1e);
+ uint64_t x90 = ((uint64_t)x88 & 0x3fffffff);
+ uint128_t x91 = (x89 + x75);
+ uint64_t x92 = (uint64_t) (x91 >> 0x1f);
+ uint64_t x93 = ((uint64_t)x91 & 0x7fffffff);
+ uint128_t x94 = (x92 + x74);
+ uint64_t x95 = (uint64_t) (x94 >> 0x1e);
+ uint64_t x96 = ((uint64_t)x94 & 0x3fffffff);
+ uint128_t x97 = (x95 + x73);
+ uint64_t x98 = (uint64_t) (x97 >> 0x1f);
+ uint64_t x99 = ((uint64_t)x97 & 0x7fffffff);
+ uint128_t x100 = (x98 + x72);
+ uint64_t x101 = (uint64_t) (x100 >> 0x1e);
+ uint64_t x102 = ((uint64_t)x100 & 0x3fffffff);
+ uint128_t x103 = (x101 + x71);
+ uint64_t x104 = (uint64_t) (x103 >> 0x1f);
+ uint64_t x105 = ((uint64_t)x103 & 0x7fffffff);
+ uint128_t x106 = (x104 + x70);
+ uint64_t x107 = (uint64_t) (x106 >> 0x1e);
+ uint64_t x108 = ((uint64_t)x106 & 0x3fffffff);
+ uint128_t x109 = (x107 + x69);
+ uint64_t x110 = (uint64_t) (x109 >> 0x1f);
+ uint64_t x111 = ((uint64_t)x109 & 0x7fffffff);
+ uint128_t x112 = (x110 + x68);
+ uint64_t x113 = (uint64_t) (x112 >> 0x1e);
+ uint64_t x114 = ((uint64_t)x112 & 0x3fffffff);
+ uint128_t x115 = (x113 + x67);
+ uint64_t x116 = (uint64_t) (x115 >> 0x1f);
+ uint64_t x117 = ((uint64_t)x115 & 0x7fffffff);
+ uint128_t x118 = (x116 + x66);
+ uint64_t x119 = (uint64_t) (x118 >> 0x1e);
+ uint64_t x120 = ((uint64_t)x118 & 0x3fffffff);
+ uint128_t x121 = (x119 + x65);
+ uint64_t x122 = (uint64_t) (x121 >> 0x1f);
+ uint64_t x123 = ((uint64_t)x121 & 0x7fffffff);
+ uint128_t x124 = (x122 + x64);
+ uint64_t x125 = (uint64_t) (x124 >> 0x1e);
+ uint64_t x126 = ((uint64_t)x124 & 0x3fffffff);
+ uint64_t x127 = (x81 + (0x11 * x125));
+ uint64_t x128 = (x127 >> 0x1f);
+ uint64_t x129 = (x127 & 0x7fffffff);
+ uint64_t x130 = (x128 + x84);
+ uint64_t x131 = (x130 >> 0x1e);
+ uint64_t x132 = (x130 & 0x3fffffff);
+ return (Return x126, Return x123, Return x120, Return x117, Return x114, Return x111, Return x108, Return x105, Return x102, Return x99, Return x96, Return x93, Return x90, (x131 + x87), Return x132, Return x129))
+(x, x0)%core
+     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e488m17/fesquare.c b/src/Specific/solinas64_2e488m17/fesquare.c
new file mode 100644
index 000000000..ff95eaf88
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/fesquare.c
@@ -0,0 +1,106 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <x86intrin.h>
+#include "liblow.h"
+
+#include "fesquare.h"
+
+typedef unsigned int uint128_t __attribute__((mode(TI)));
+
+#if (defined(__GNUC__) || defined(__GNUG__)) && !(defined(__clang__)||defined(__INTEL_COMPILER))
+// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
+#define _subborrow_u32 __builtin_ia32_sbb_u32
+#define _subborrow_u64 __builtin_ia32_sbb_u64
+#endif
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline fesquare(uint64_t* out, uint64_t x29, uint64_t x30, uint64_t x28, uint64_t x26, uint64_t x24, uint64_t x22, uint64_t x20, uint64_t x18, uint64_t x16, uint64_t x14, uint64_t x12, uint64_t x10, uint64_t x8, uint64_t x6, uint64_t x4, uint64_t x2)
+{  uint128_t x31 = (((uint128_t)x2 * x29) + (((uint128_t)x4 * x30) + (((uint128_t)x6 * x28) + (((uint128_t)x8 * x26) + (((uint128_t)x10 * x24) + (((uint128_t)x12 * x22) + (((uint128_t)x14 * x20) + (((uint128_t)x16 * x18) + (((uint128_t)x18 * x16) + (((uint128_t)x20 * x14) + (((uint128_t)x22 * x12) + (((uint128_t)x24 * x10) + (((uint128_t)x26 * x8) + (((uint128_t)x28 * x6) + (((uint128_t)x30 * x4) + ((uint128_t)x29 * x2))))))))))))))));
+{  uint128_t x32 = ((((uint128_t)x2 * x30) + (((uint128_t)0x2 * (x4 * x28)) + (((uint128_t)x6 * x26) + (((uint128_t)0x2 * (x8 * x24)) + (((uint128_t)x10 * x22) + (((uint128_t)0x2 * (x12 * x20)) + (((uint128_t)x14 * x18) + (((uint128_t)0x2 * (x16 * x16)) + (((uint128_t)x18 * x14) + (((uint128_t)0x2 * (x20 * x12)) + (((uint128_t)x22 * x10) + (((uint128_t)0x2 * (x24 * x8)) + (((uint128_t)x26 * x6) + (((uint128_t)0x2 * (x28 * x4)) + ((uint128_t)x30 * x2))))))))))))))) + (0x11 * ((uint128_t)0x2 * (x29 * x29))));
+{  uint128_t x33 = ((((uint128_t)x2 * x28) + (((uint128_t)x4 * x26) + (((uint128_t)x6 * x24) + (((uint128_t)x8 * x22) + (((uint128_t)x10 * x20) + (((uint128_t)x12 * x18) + (((uint128_t)x14 * x16) + (((uint128_t)x16 * x14) + (((uint128_t)x18 * x12) + (((uint128_t)x20 * x10) + (((uint128_t)x22 * x8) + (((uint128_t)x24 * x6) + (((uint128_t)x26 * x4) + ((uint128_t)x28 * x2)))))))))))))) + (0x11 * (((uint128_t)x30 * x29) + ((uint128_t)x29 * x30))));
+{  uint128_t x34 = ((((uint128_t)x2 * x26) + (((uint128_t)0x2 * (x4 * x24)) + (((uint128_t)x6 * x22) + (((uint128_t)0x2 * (x8 * x20)) + (((uint128_t)x10 * x18) + (((uint128_t)0x2 * (x12 * x16)) + (((uint128_t)x14 * x14) + (((uint128_t)0x2 * (x16 * x12)) + (((uint128_t)x18 * x10) + (((uint128_t)0x2 * (x20 * x8)) + (((uint128_t)x22 * x6) + (((uint128_t)0x2 * (x24 * x4)) + ((uint128_t)x26 * x2))))))))))))) + (0x11 * (((uint128_t)0x2 * (x28 * x29)) + (((uint128_t)x30 * x30) + ((uint128_t)0x2 * (x29 * x28))))));
+{  uint128_t x35 = ((((uint128_t)x2 * x24) + (((uint128_t)x4 * x22) + (((uint128_t)x6 * x20) + (((uint128_t)x8 * x18) + (((uint128_t)x10 * x16) + (((uint128_t)x12 * x14) + (((uint128_t)x14 * x12) + (((uint128_t)x16 * x10) + (((uint128_t)x18 * x8) + (((uint128_t)x20 * x6) + (((uint128_t)x22 * x4) + ((uint128_t)x24 * x2)))))))))))) + (0x11 * (((uint128_t)x26 * x29) + (((uint128_t)x28 * x30) + (((uint128_t)x30 * x28) + ((uint128_t)x29 * x26))))));
+{  uint128_t x36 = ((((uint128_t)x2 * x22) + (((uint128_t)0x2 * (x4 * x20)) + (((uint128_t)x6 * x18) + (((uint128_t)0x2 * (x8 * x16)) + (((uint128_t)x10 * x14) + (((uint128_t)0x2 * (x12 * x12)) + (((uint128_t)x14 * x10) + (((uint128_t)0x2 * (x16 * x8)) + (((uint128_t)x18 * x6) + (((uint128_t)0x2 * (x20 * x4)) + ((uint128_t)x22 * x2))))))))))) + (0x11 * (((uint128_t)0x2 * (x24 * x29)) + (((uint128_t)x26 * x30) + (((uint128_t)0x2 * (x28 * x28)) + (((uint128_t)x30 * x26) + ((uint128_t)0x2 * (x29 * x24))))))));
+{  uint128_t x37 = ((((uint128_t)x2 * x20) + (((uint128_t)x4 * x18) + (((uint128_t)x6 * x16) + (((uint128_t)x8 * x14) + (((uint128_t)x10 * x12) + (((uint128_t)x12 * x10) + (((uint128_t)x14 * x8) + (((uint128_t)x16 * x6) + (((uint128_t)x18 * x4) + ((uint128_t)x20 * x2)))))))))) + (0x11 * (((uint128_t)x22 * x29) + (((uint128_t)x24 * x30) + (((uint128_t)x26 * x28) + (((uint128_t)x28 * x26) + (((uint128_t)x30 * x24) + ((uint128_t)x29 * x22))))))));
+{  uint128_t x38 = ((((uint128_t)x2 * x18) + (((uint128_t)0x2 * (x4 * x16)) + (((uint128_t)x6 * x14) + (((uint128_t)0x2 * (x8 * x12)) + (((uint128_t)x10 * x10) + (((uint128_t)0x2 * (x12 * x8)) + (((uint128_t)x14 * x6) + (((uint128_t)0x2 * (x16 * x4)) + ((uint128_t)x18 * x2))))))))) + (0x11 * (((uint128_t)0x2 * (x20 * x29)) + (((uint128_t)x22 * x30) + (((uint128_t)0x2 * (x24 * x28)) + (((uint128_t)x26 * x26) + (((uint128_t)0x2 * (x28 * x24)) + (((uint128_t)x30 * x22) + ((uint128_t)0x2 * (x29 * x20))))))))));
+{  uint128_t x39 = ((((uint128_t)x2 * x16) + (((uint128_t)x4 * x14) + (((uint128_t)x6 * x12) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + (((uint128_t)x12 * x6) + (((uint128_t)x14 * x4) + ((uint128_t)x16 * x2)))))))) + (0x11 * (((uint128_t)x18 * x29) + (((uint128_t)x20 * x30) + (((uint128_t)x22 * x28) + (((uint128_t)x24 * x26) + (((uint128_t)x26 * x24) + (((uint128_t)x28 * x22) + (((uint128_t)x30 * x20) + ((uint128_t)x29 * x18))))))))));
+{  uint128_t x40 = ((((uint128_t)x2 * x14) + (((uint128_t)0x2 * (x4 * x12)) + (((uint128_t)x6 * x10) + (((uint128_t)0x2 * (x8 * x8)) + (((uint128_t)x10 * x6) + (((uint128_t)0x2 * (x12 * x4)) + ((uint128_t)x14 * x2))))))) + (0x11 * (((uint128_t)0x2 * (x16 * x29)) + (((uint128_t)x18 * x30) + (((uint128_t)0x2 * (x20 * x28)) + (((uint128_t)x22 * x26) + (((uint128_t)0x2 * (x24 * x24)) + (((uint128_t)x26 * x22) + (((uint128_t)0x2 * (x28 * x20)) + (((uint128_t)x30 * x18) + ((uint128_t)0x2 * (x29 * x16))))))))))));
+{  uint128_t x41 = ((((uint128_t)x2 * x12) + (((uint128_t)x4 * x10) + (((uint128_t)x6 * x8) + (((uint128_t)x8 * x6) + (((uint128_t)x10 * x4) + ((uint128_t)x12 * x2)))))) + (0x11 * (((uint128_t)x14 * x29) + (((uint128_t)x16 * x30) + (((uint128_t)x18 * x28) + (((uint128_t)x20 * x26) + (((uint128_t)x22 * x24) + (((uint128_t)x24 * x22) + (((uint128_t)x26 * x20) + (((uint128_t)x28 * x18) + (((uint128_t)x30 * x16) + ((uint128_t)x29 * x14))))))))))));
+{  uint128_t x42 = ((((uint128_t)x2 * x10) + (((uint128_t)0x2 * (x4 * x8)) + (((uint128_t)x6 * x6) + (((uint128_t)0x2 * (x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x11 * (((uint128_t)0x2 * (x12 * x29)) + (((uint128_t)x14 * x30) + (((uint128_t)0x2 * (x16 * x28)) + (((uint128_t)x18 * x26) + (((uint128_t)0x2 * (x20 * x24)) + (((uint128_t)x22 * x22) + (((uint128_t)0x2 * (x24 * x20)) + (((uint128_t)x26 * x18) + (((uint128_t)0x2 * (x28 * x16)) + (((uint128_t)x30 * x14) + ((uint128_t)0x2 * (x29 * x12))))))))))))));
+{  uint128_t x43 = ((((uint128_t)x2 * x8) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x8 * x2)))) + (0x11 * (((uint128_t)x10 * x29) + (((uint128_t)x12 * x30) + (((uint128_t)x14 * x28) + (((uint128_t)x16 * x26) + (((uint128_t)x18 * x24) + (((uint128_t)x20 * x22) + (((uint128_t)x22 * x20) + (((uint128_t)x24 * x18) + (((uint128_t)x26 * x16) + (((uint128_t)x28 * x14) + (((uint128_t)x30 * x12) + ((uint128_t)x29 * x10))))))))))))));
+{  uint128_t x44 = ((((uint128_t)x2 * x6) + (((uint128_t)0x2 * (x4 * x4)) + ((uint128_t)x6 * x2))) + (0x11 * (((uint128_t)0x2 * (x8 * x29)) + (((uint128_t)x10 * x30) + (((uint128_t)0x2 * (x12 * x28)) + (((uint128_t)x14 * x26) + (((uint128_t)0x2 * (x16 * x24)) + (((uint128_t)x18 * x22) + (((uint128_t)0x2 * (x20 * x20)) + (((uint128_t)x22 * x18) + (((uint128_t)0x2 * (x24 * x16)) + (((uint128_t)x26 * x14) + (((uint128_t)0x2 * (x28 * x12)) + (((uint128_t)x30 * x10) + ((uint128_t)0x2 * (x29 * x8))))))))))))))));
+{  uint128_t x45 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x11 * (((uint128_t)x6 * x29) + (((uint128_t)x8 * x30) + (((uint128_t)x10 * x28) + (((uint128_t)x12 * x26) + (((uint128_t)x14 * x24) + (((uint128_t)x16 * x22) + (((uint128_t)x18 * x20) + (((uint128_t)x20 * x18) + (((uint128_t)x22 * x16) + (((uint128_t)x24 * x14) + (((uint128_t)x26 * x12) + (((uint128_t)x28 * x10) + (((uint128_t)x30 * x8) + ((uint128_t)x29 * x6))))))))))))))));
+{  uint128_t x46 = (((uint128_t)x2 * x2) + (0x11 * (((uint128_t)0x2 * (x4 * x29)) + (((uint128_t)x6 * x30) + (((uint128_t)0x2 * (x8 * x28)) + (((uint128_t)x10 * x26) + (((uint128_t)0x2 * (x12 * x24)) + (((uint128_t)x14 * x22) + (((uint128_t)0x2 * (x16 * x20)) + (((uint128_t)x18 * x18) + (((uint128_t)0x2 * (x20 * x16)) + (((uint128_t)x22 * x14) + (((uint128_t)0x2 * (x24 * x12)) + (((uint128_t)x26 * x10) + (((uint128_t)0x2 * (x28 * x8)) + (((uint128_t)x30 * x6) + ((uint128_t)0x2 * (x29 * x4))))))))))))))))));
+{  uint64_t x47 = (uint64_t) (x46 >> 0x1f);
+{  uint64_t x48 = ((uint64_t)x46 & 0x7fffffff);
+{  uint128_t x49 = (x47 + x45);
+{  uint64_t x50 = (uint64_t) (x49 >> 0x1e);
+{  uint64_t x51 = ((uint64_t)x49 & 0x3fffffff);
+{  uint128_t x52 = (x50 + x44);
+{  uint64_t x53 = (uint64_t) (x52 >> 0x1f);
+{  uint64_t x54 = ((uint64_t)x52 & 0x7fffffff);
+{  uint128_t x55 = (x53 + x43);
+{  uint64_t x56 = (uint64_t) (x55 >> 0x1e);
+{  uint64_t x57 = ((uint64_t)x55 & 0x3fffffff);
+{  uint128_t x58 = (x56 + x42);
+{  uint64_t x59 = (uint64_t) (x58 >> 0x1f);
+{  uint64_t x60 = ((uint64_t)x58 & 0x7fffffff);
+{  uint128_t x61 = (x59 + x41);
+{  uint64_t x62 = (uint64_t) (x61 >> 0x1e);
+{  uint64_t x63 = ((uint64_t)x61 & 0x3fffffff);
+{  uint128_t x64 = (x62 + x40);
+{  uint64_t x65 = (uint64_t) (x64 >> 0x1f);
+{  uint64_t x66 = ((uint64_t)x64 & 0x7fffffff);
+{  uint128_t x67 = (x65 + x39);
+{  uint64_t x68 = (uint64_t) (x67 >> 0x1e);
+{  uint64_t x69 = ((uint64_t)x67 & 0x3fffffff);
+{  uint128_t x70 = (x68 + x38);
+{  uint64_t x71 = (uint64_t) (x70 >> 0x1f);
+{  uint64_t x72 = ((uint64_t)x70 & 0x7fffffff);
+{  uint128_t x73 = (x71 + x37);
+{  uint64_t x74 = (uint64_t) (x73 >> 0x1e);
+{  uint64_t x75 = ((uint64_t)x73 & 0x3fffffff);
+{  uint128_t x76 = (x74 + x36);
+{  uint64_t x77 = (uint64_t) (x76 >> 0x1f);
+{  uint64_t x78 = ((uint64_t)x76 & 0x7fffffff);
+{  uint128_t x79 = (x77 + x35);
+{  uint64_t x80 = (uint64_t) (x79 >> 0x1e);
+{  uint64_t x81 = ((uint64_t)x79 & 0x3fffffff);
+{  uint128_t x82 = (x80 + x34);
+{  uint64_t x83 = (uint64_t) (x82 >> 0x1f);
+{  uint64_t x84 = ((uint64_t)x82 & 0x7fffffff);
+{  uint128_t x85 = (x83 + x33);
+{  uint64_t x86 = (uint64_t) (x85 >> 0x1e);
+{  uint64_t x87 = ((uint64_t)x85 & 0x3fffffff);
+{  uint128_t x88 = (x86 + x32);
+{  uint64_t x89 = (uint64_t) (x88 >> 0x1f);
+{  uint64_t x90 = ((uint64_t)x88 & 0x7fffffff);
+{  uint128_t x91 = (x89 + x31);
+{  uint64_t x92 = (uint64_t) (x91 >> 0x1e);
+{  uint64_t x93 = ((uint64_t)x91 & 0x3fffffff);
+{  uint64_t x94 = (x48 + (0x11 * x92));
+{  uint64_t x95 = (x94 >> 0x1f);
+{  uint64_t x96 = (x94 & 0x7fffffff);
+{  uint64_t x97 = (x95 + x51);
+{  uint64_t x98 = (x97 >> 0x1e);
+{  uint64_t x99 = (x97 & 0x3fffffff);
+out[0] = x93;
+out[1] = x90;
+out[2] = x87;
+out[3] = x84;
+out[4] = x81;
+out[5] = x78;
+out[6] = x75;
+out[7] = x72;
+out[8] = x69;
+out[9] = x66;
+out[10] = x63;
+out[11] = x60;
+out[12] = x57;
+out[13] = x98 + x54;
+out[14] = x99;
+out[15] = x96;
+}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
+// caller: uint64_t out[16];
diff --git a/src/Specific/solinas64_2e488m17/fesquare.h b/src/Specific/solinas64_2e488m17/fesquare.h
new file mode 100644
index 000000000..c86247b3d
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/fesquare.h
@@ -0,0 +1,6 @@
+#include <stdint.h>
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline fesquare(uint64_t* out, uint64_t x29, uint64_t x30, uint64_t x28, uint64_t x26, uint64_t x24, uint64_t x22, uint64_t x20, uint64_t x18, uint64_t x16, uint64_t x14, uint64_t x12, uint64_t x10, uint64_t x8, uint64_t x6, uint64_t x4, uint64_t x2);
diff --git a/src/Specific/solinas64_2e488m17/fesquareDisplay.log b/src/Specific/solinas64_2e488m17/fesquareDisplay.log
new file mode 100644
index 000000000..be98a5058
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/fesquareDisplay.log
@@ -0,0 +1,76 @@
+λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x29, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint128_t x31 = (((uint128_t)x2 * x29) + (((uint128_t)x4 * x30) + (((uint128_t)x6 * x28) + (((uint128_t)x8 * x26) + (((uint128_t)x10 * x24) + (((uint128_t)x12 * x22) + (((uint128_t)x14 * x20) + (((uint128_t)x16 * x18) + (((uint128_t)x18 * x16) + (((uint128_t)x20 * x14) + (((uint128_t)x22 * x12) + (((uint128_t)x24 * x10) + (((uint128_t)x26 * x8) + (((uint128_t)x28 * x6) + (((uint128_t)x30 * x4) + ((uint128_t)x29 * x2))))))))))))))));
+ uint128_t x32 = ((((uint128_t)x2 * x30) + (((uint128_t)0x2 * (x4 * x28)) + (((uint128_t)x6 * x26) + (((uint128_t)0x2 * (x8 * x24)) + (((uint128_t)x10 * x22) + (((uint128_t)0x2 * (x12 * x20)) + (((uint128_t)x14 * x18) + (((uint128_t)0x2 * (x16 * x16)) + (((uint128_t)x18 * x14) + (((uint128_t)0x2 * (x20 * x12)) + (((uint128_t)x22 * x10) + (((uint128_t)0x2 * (x24 * x8)) + (((uint128_t)x26 * x6) + (((uint128_t)0x2 * (x28 * x4)) + ((uint128_t)x30 * x2))))))))))))))) + (0x11 * ((uint128_t)0x2 * (x29 * x29))));
+ uint128_t x33 = ((((uint128_t)x2 * x28) + (((uint128_t)x4 * x26) + (((uint128_t)x6 * x24) + (((uint128_t)x8 * x22) + (((uint128_t)x10 * x20) + (((uint128_t)x12 * x18) + (((uint128_t)x14 * x16) + (((uint128_t)x16 * x14) + (((uint128_t)x18 * x12) + (((uint128_t)x20 * x10) + (((uint128_t)x22 * x8) + (((uint128_t)x24 * x6) + (((uint128_t)x26 * x4) + ((uint128_t)x28 * x2)))))))))))))) + (0x11 * (((uint128_t)x30 * x29) + ((uint128_t)x29 * x30))));
+ uint128_t x34 = ((((uint128_t)x2 * x26) + (((uint128_t)0x2 * (x4 * x24)) + (((uint128_t)x6 * x22) + (((uint128_t)0x2 * (x8 * x20)) + (((uint128_t)x10 * x18) + (((uint128_t)0x2 * (x12 * x16)) + (((uint128_t)x14 * x14) + (((uint128_t)0x2 * (x16 * x12)) + (((uint128_t)x18 * x10) + (((uint128_t)0x2 * (x20 * x8)) + (((uint128_t)x22 * x6) + (((uint128_t)0x2 * (x24 * x4)) + ((uint128_t)x26 * x2))))))))))))) + (0x11 * (((uint128_t)0x2 * (x28 * x29)) + (((uint128_t)x30 * x30) + ((uint128_t)0x2 * (x29 * x28))))));
+ uint128_t x35 = ((((uint128_t)x2 * x24) + (((uint128_t)x4 * x22) + (((uint128_t)x6 * x20) + (((uint128_t)x8 * x18) + (((uint128_t)x10 * x16) + (((uint128_t)x12 * x14) + (((uint128_t)x14 * x12) + (((uint128_t)x16 * x10) + (((uint128_t)x18 * x8) + (((uint128_t)x20 * x6) + (((uint128_t)x22 * x4) + ((uint128_t)x24 * x2)))))))))))) + (0x11 * (((uint128_t)x26 * x29) + (((uint128_t)x28 * x30) + (((uint128_t)x30 * x28) + ((uint128_t)x29 * x26))))));
+ uint128_t x36 = ((((uint128_t)x2 * x22) + (((uint128_t)0x2 * (x4 * x20)) + (((uint128_t)x6 * x18) + (((uint128_t)0x2 * (x8 * x16)) + (((uint128_t)x10 * x14) + (((uint128_t)0x2 * (x12 * x12)) + (((uint128_t)x14 * x10) + (((uint128_t)0x2 * (x16 * x8)) + (((uint128_t)x18 * x6) + (((uint128_t)0x2 * (x20 * x4)) + ((uint128_t)x22 * x2))))))))))) + (0x11 * (((uint128_t)0x2 * (x24 * x29)) + (((uint128_t)x26 * x30) + (((uint128_t)0x2 * (x28 * x28)) + (((uint128_t)x30 * x26) + ((uint128_t)0x2 * (x29 * x24))))))));
+ uint128_t x37 = ((((uint128_t)x2 * x20) + (((uint128_t)x4 * x18) + (((uint128_t)x6 * x16) + (((uint128_t)x8 * x14) + (((uint128_t)x10 * x12) + (((uint128_t)x12 * x10) + (((uint128_t)x14 * x8) + (((uint128_t)x16 * x6) + (((uint128_t)x18 * x4) + ((uint128_t)x20 * x2)))))))))) + (0x11 * (((uint128_t)x22 * x29) + (((uint128_t)x24 * x30) + (((uint128_t)x26 * x28) + (((uint128_t)x28 * x26) + (((uint128_t)x30 * x24) + ((uint128_t)x29 * x22))))))));
+ uint128_t x38 = ((((uint128_t)x2 * x18) + (((uint128_t)0x2 * (x4 * x16)) + (((uint128_t)x6 * x14) + (((uint128_t)0x2 * (x8 * x12)) + (((uint128_t)x10 * x10) + (((uint128_t)0x2 * (x12 * x8)) + (((uint128_t)x14 * x6) + (((uint128_t)0x2 * (x16 * x4)) + ((uint128_t)x18 * x2))))))))) + (0x11 * (((uint128_t)0x2 * (x20 * x29)) + (((uint128_t)x22 * x30) + (((uint128_t)0x2 * (x24 * x28)) + (((uint128_t)x26 * x26) + (((uint128_t)0x2 * (x28 * x24)) + (((uint128_t)x30 * x22) + ((uint128_t)0x2 * (x29 * x20))))))))));
+ uint128_t x39 = ((((uint128_t)x2 * x16) + (((uint128_t)x4 * x14) + (((uint128_t)x6 * x12) + (((uint128_t)x8 * x10) + (((uint128_t)x10 * x8) + (((uint128_t)x12 * x6) + (((uint128_t)x14 * x4) + ((uint128_t)x16 * x2)))))))) + (0x11 * (((uint128_t)x18 * x29) + (((uint128_t)x20 * x30) + (((uint128_t)x22 * x28) + (((uint128_t)x24 * x26) + (((uint128_t)x26 * x24) + (((uint128_t)x28 * x22) + (((uint128_t)x30 * x20) + ((uint128_t)x29 * x18))))))))));
+ uint128_t x40 = ((((uint128_t)x2 * x14) + (((uint128_t)0x2 * (x4 * x12)) + (((uint128_t)x6 * x10) + (((uint128_t)0x2 * (x8 * x8)) + (((uint128_t)x10 * x6) + (((uint128_t)0x2 * (x12 * x4)) + ((uint128_t)x14 * x2))))))) + (0x11 * (((uint128_t)0x2 * (x16 * x29)) + (((uint128_t)x18 * x30) + (((uint128_t)0x2 * (x20 * x28)) + (((uint128_t)x22 * x26) + (((uint128_t)0x2 * (x24 * x24)) + (((uint128_t)x26 * x22) + (((uint128_t)0x2 * (x28 * x20)) + (((uint128_t)x30 * x18) + ((uint128_t)0x2 * (x29 * x16))))))))))));
+ uint128_t x41 = ((((uint128_t)x2 * x12) + (((uint128_t)x4 * x10) + (((uint128_t)x6 * x8) + (((uint128_t)x8 * x6) + (((uint128_t)x10 * x4) + ((uint128_t)x12 * x2)))))) + (0x11 * (((uint128_t)x14 * x29) + (((uint128_t)x16 * x30) + (((uint128_t)x18 * x28) + (((uint128_t)x20 * x26) + (((uint128_t)x22 * x24) + (((uint128_t)x24 * x22) + (((uint128_t)x26 * x20) + (((uint128_t)x28 * x18) + (((uint128_t)x30 * x16) + ((uint128_t)x29 * x14))))))))))));
+ uint128_t x42 = ((((uint128_t)x2 * x10) + (((uint128_t)0x2 * (x4 * x8)) + (((uint128_t)x6 * x6) + (((uint128_t)0x2 * (x8 * x4)) + ((uint128_t)x10 * x2))))) + (0x11 * (((uint128_t)0x2 * (x12 * x29)) + (((uint128_t)x14 * x30) + (((uint128_t)0x2 * (x16 * x28)) + (((uint128_t)x18 * x26) + (((uint128_t)0x2 * (x20 * x24)) + (((uint128_t)x22 * x22) + (((uint128_t)0x2 * (x24 * x20)) + (((uint128_t)x26 * x18) + (((uint128_t)0x2 * (x28 * x16)) + (((uint128_t)x30 * x14) + ((uint128_t)0x2 * (x29 * x12))))))))))))));
+ uint128_t x43 = ((((uint128_t)x2 * x8) + (((uint128_t)x4 * x6) + (((uint128_t)x6 * x4) + ((uint128_t)x8 * x2)))) + (0x11 * (((uint128_t)x10 * x29) + (((uint128_t)x12 * x30) + (((uint128_t)x14 * x28) + (((uint128_t)x16 * x26) + (((uint128_t)x18 * x24) + (((uint128_t)x20 * x22) + (((uint128_t)x22 * x20) + (((uint128_t)x24 * x18) + (((uint128_t)x26 * x16) + (((uint128_t)x28 * x14) + (((uint128_t)x30 * x12) + ((uint128_t)x29 * x10))))))))))))));
+ uint128_t x44 = ((((uint128_t)x2 * x6) + (((uint128_t)0x2 * (x4 * x4)) + ((uint128_t)x6 * x2))) + (0x11 * (((uint128_t)0x2 * (x8 * x29)) + (((uint128_t)x10 * x30) + (((uint128_t)0x2 * (x12 * x28)) + (((uint128_t)x14 * x26) + (((uint128_t)0x2 * (x16 * x24)) + (((uint128_t)x18 * x22) + (((uint128_t)0x2 * (x20 * x20)) + (((uint128_t)x22 * x18) + (((uint128_t)0x2 * (x24 * x16)) + (((uint128_t)x26 * x14) + (((uint128_t)0x2 * (x28 * x12)) + (((uint128_t)x30 * x10) + ((uint128_t)0x2 * (x29 * x8))))))))))))))));
+ uint128_t x45 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0x11 * (((uint128_t)x6 * x29) + (((uint128_t)x8 * x30) + (((uint128_t)x10 * x28) + (((uint128_t)x12 * x26) + (((uint128_t)x14 * x24) + (((uint128_t)x16 * x22) + (((uint128_t)x18 * x20) + (((uint128_t)x20 * x18) + (((uint128_t)x22 * x16) + (((uint128_t)x24 * x14) + (((uint128_t)x26 * x12) + (((uint128_t)x28 * x10) + (((uint128_t)x30 * x8) + ((uint128_t)x29 * x6))))))))))))))));
+ uint128_t x46 = (((uint128_t)x2 * x2) + (0x11 * (((uint128_t)0x2 * (x4 * x29)) + (((uint128_t)x6 * x30) + (((uint128_t)0x2 * (x8 * x28)) + (((uint128_t)x10 * x26) + (((uint128_t)0x2 * (x12 * x24)) + (((uint128_t)x14 * x22) + (((uint128_t)0x2 * (x16 * x20)) + (((uint128_t)x18 * x18) + (((uint128_t)0x2 * (x20 * x16)) + (((uint128_t)x22 * x14) + (((uint128_t)0x2 * (x24 * x12)) + (((uint128_t)x26 * x10) + (((uint128_t)0x2 * (x28 * x8)) + (((uint128_t)x30 * x6) + ((uint128_t)0x2 * (x29 * x4))))))))))))))))));
+ uint64_t x47 = (uint64_t) (x46 >> 0x1f);
+ uint64_t x48 = ((uint64_t)x46 & 0x7fffffff);
+ uint128_t x49 = (x47 + x45);
+ uint64_t x50 = (uint64_t) (x49 >> 0x1e);
+ uint64_t x51 = ((uint64_t)x49 & 0x3fffffff);
+ uint128_t x52 = (x50 + x44);
+ uint64_t x53 = (uint64_t) (x52 >> 0x1f);
+ uint64_t x54 = ((uint64_t)x52 & 0x7fffffff);
+ uint128_t x55 = (x53 + x43);
+ uint64_t x56 = (uint64_t) (x55 >> 0x1e);
+ uint64_t x57 = ((uint64_t)x55 & 0x3fffffff);
+ uint128_t x58 = (x56 + x42);
+ uint64_t x59 = (uint64_t) (x58 >> 0x1f);
+ uint64_t x60 = ((uint64_t)x58 & 0x7fffffff);
+ uint128_t x61 = (x59 + x41);
+ uint64_t x62 = (uint64_t) (x61 >> 0x1e);
+ uint64_t x63 = ((uint64_t)x61 & 0x3fffffff);
+ uint128_t x64 = (x62 + x40);
+ uint64_t x65 = (uint64_t) (x64 >> 0x1f);
+ uint64_t x66 = ((uint64_t)x64 & 0x7fffffff);
+ uint128_t x67 = (x65 + x39);
+ uint64_t x68 = (uint64_t) (x67 >> 0x1e);
+ uint64_t x69 = ((uint64_t)x67 & 0x3fffffff);
+ uint128_t x70 = (x68 + x38);
+ uint64_t x71 = (uint64_t) (x70 >> 0x1f);
+ uint64_t x72 = ((uint64_t)x70 & 0x7fffffff);
+ uint128_t x73 = (x71 + x37);
+ uint64_t x74 = (uint64_t) (x73 >> 0x1e);
+ uint64_t x75 = ((uint64_t)x73 & 0x3fffffff);
+ uint128_t x76 = (x74 + x36);
+ uint64_t x77 = (uint64_t) (x76 >> 0x1f);
+ uint64_t x78 = ((uint64_t)x76 & 0x7fffffff);
+ uint128_t x79 = (x77 + x35);
+ uint64_t x80 = (uint64_t) (x79 >> 0x1e);
+ uint64_t x81 = ((uint64_t)x79 & 0x3fffffff);
+ uint128_t x82 = (x80 + x34);
+ uint64_t x83 = (uint64_t) (x82 >> 0x1f);
+ uint64_t x84 = ((uint64_t)x82 & 0x7fffffff);
+ uint128_t x85 = (x83 + x33);
+ uint64_t x86 = (uint64_t) (x85 >> 0x1e);
+ uint64_t x87 = ((uint64_t)x85 & 0x3fffffff);
+ uint128_t x88 = (x86 + x32);
+ uint64_t x89 = (uint64_t) (x88 >> 0x1f);
+ uint64_t x90 = ((uint64_t)x88 & 0x7fffffff);
+ uint128_t x91 = (x89 + x31);
+ uint64_t x92 = (uint64_t) (x91 >> 0x1e);
+ uint64_t x93 = ((uint64_t)x91 & 0x3fffffff);
+ uint64_t x94 = (x48 + (0x11 * x92));
+ uint64_t x95 = (x94 >> 0x1f);
+ uint64_t x96 = (x94 & 0x7fffffff);
+ uint64_t x97 = (x95 + x51);
+ uint64_t x98 = (x97 >> 0x1e);
+ uint64_t x99 = (x97 & 0x3fffffff);
+ return (Return x93, Return x90, Return x87, Return x84, Return x81, Return x78, Return x75, Return x72, Return x69, Return x66, Return x63, Return x60, Return x57, (x98 + x54), Return x99, Return x96))
+x
+     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/solinas64_2e488m17/freeze.c b/src/Specific/solinas64_2e488m17/freeze.c
new file mode 100644
index 000000000..15e32ebf7
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/freeze.c
@@ -0,0 +1,25 @@
+#include <stdint.h>
+#include <stdbool.h>
+#include <x86intrin.h>
+#include "liblow.h"
+
+#include "freeze.h"
+
+typedef unsigned int uint128_t __attribute__((mode(TI)));
+
+#if (defined(__GNUC__) || defined(__GNUG__)) && !(defined(__clang__)||defined(__INTEL_COMPILER))
+// https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81294
+#define _subborrow_u32 __builtin_ia32_sbb_u32
+#define _subborrow_u64 __builtin_ia32_sbb_u64
+#endif
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline freeze(uint64_t* out, uint64_t x29, uint64_t x30, uint64_t x28, uint64_t x26, uint64_t x24, uint64_t x22, uint64_t x20, uint64_t x18, uint64_t x16, uint64_t x14, uint64_t x12, uint64_t x10, uint64_t x8, uint64_t x6, uint64_t x4, uint64_t x2)
+out[0] = uint64_t x32;
+out[1] = uint8_t x33 = Op Syntax.SubWithGetBorrow 31 Syntax.TWord 3 Syntax.TWord 6 Syntax.TWord 6 Syntax.TWord 6 Syntax.TWord 3 0x0;
+out[2] = x2;
+out[3] = Const 2147483631;;
+}
+// caller: uint64_t out[4];
diff --git a/src/Specific/solinas64_2e488m17/freeze.h b/src/Specific/solinas64_2e488m17/freeze.h
new file mode 100644
index 000000000..a955633b6
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/freeze.h
@@ -0,0 +1,6 @@
+#include <stdint.h>
+
+#undef force_inline
+#define force_inline __attribute__((always_inline))
+
+void force_inline freeze(uint64_t* out, uint64_t x29, uint64_t x30, uint64_t x28, uint64_t x26, uint64_t x24, uint64_t x22, uint64_t x20, uint64_t x18, uint64_t x16, uint64_t x14, uint64_t x12, uint64_t x10, uint64_t x8, uint64_t x6, uint64_t x4, uint64_t x2);
diff --git a/src/Specific/solinas64_2e488m17/freezeDisplay.log b/src/Specific/solinas64_2e488m17/freezeDisplay.log
new file mode 100644
index 000000000..483ee09e1
--- /dev/null
+++ b/src/Specific/solinas64_2e488m17/freezeDisplay.log
@@ -0,0 +1,56 @@
+λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x29, x30, x28, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint64_t x32, uint8_t x33 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, Const 2147483631);
+ uint64_t x35, uint8_t x36 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x33, Return x4, 0x3fffffff);
+ uint64_t x38, uint8_t x39 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x36, Return x6, 0x7fffffff);
+ uint64_t x41, uint8_t x42 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x39, Return x8, 0x3fffffff);
+ uint64_t x44, uint8_t x45 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x42, Return x10, 0x7fffffff);
+ uint64_t x47, uint8_t x48 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x45, Return x12, 0x3fffffff);
+ uint64_t x50, uint8_t x51 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x48, Return x14, 0x7fffffff);
+ uint64_t x53, uint8_t x54 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x51, Return x16, 0x3fffffff);
+ uint64_t x56, uint8_t x57 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x54, Return x18, 0x7fffffff);
+ uint64_t x59, uint8_t x60 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x57, Return x20, 0x3fffffff);
+ uint64_t x62, uint8_t x63 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x60, Return x22, 0x7fffffff);
+ uint64_t x65, uint8_t x66 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x63, Return x24, 0x3fffffff);
+ uint64_t x68, uint8_t x69 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x66, Return x26, 0x7fffffff);
+ uint64_t x71, uint8_t x72 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x69, Return x28, 0x3fffffff);
+ uint64_t x74, uint8_t x75 = Op (Syntax.SubWithGetBorrow 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x72, Return x30, 0x7fffffff);
+ uint64_t x77, uint8_t x78 = Op (Syntax.SubWithGetBorrow 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x75, Return x29, 0x3fffffff);
+ uint64_t x79 = (uint64_t)cmovznz(x78, 0x0, 0xffffffffffffffffL);
+ uint64_t x80 = (x79 & Const 2147483631);
+ uint64_t x82, uint8_t x83 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x32, Return x80);
+ uint64_t x84 = (x79 & 0x3fffffff);
+ uint64_t x86, uint8_t x87 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x83, Return x35, Return x84);
+ uint64_t x88 = (x79 & 0x7fffffff);
+ uint64_t x90, uint8_t x91 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x87, Return x38, Return x88);
+ uint64_t x92 = (x79 & 0x3fffffff);
+ uint64_t x94, uint8_t x95 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x91, Return x41, Return x92);
+ uint64_t x96 = (x79 & 0x7fffffff);
+ uint64_t x98, uint8_t x99 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x95, Return x44, Return x96);
+ uint64_t x100 = (x79 & 0x3fffffff);
+ uint64_t x102, uint8_t x103 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x99, Return x47, Return x100);
+ uint64_t x104 = (x79 & 0x7fffffff);
+ uint64_t x106, uint8_t x107 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x103, Return x50, Return x104);
+ uint64_t x108 = (x79 & 0x3fffffff);
+ uint64_t x110, uint8_t x111 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x107, Return x53, Return x108);
+ uint64_t x112 = (x79 & 0x7fffffff);
+ uint64_t x114, uint8_t x115 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x111, Return x56, Return x112);
+ uint64_t x116 = (x79 & 0x3fffffff);
+ uint64_t x118, uint8_t x119 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x115, Return x59, Return x116);
+ uint64_t x120 = (x79 & 0x7fffffff);
+ uint64_t x122, uint8_t x123 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x119, Return x62, Return x120);
+ uint64_t x124 = (x79 & 0x3fffffff);
+ uint64_t x126, uint8_t x127 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x123, Return x65, Return x124);
+ uint64_t x128 = (x79 & 0x7fffffff);
+ uint64_t x130, uint8_t x131 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x127, Return x68, Return x128);
+ uint64_t x132 = (x79 & 0x3fffffff);
+ uint64_t x134, uint8_t x135 = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x131, Return x71, Return x132);
+ uint64_t x136 = (x79 & 0x7fffffff);
+ uint64_t x138, uint8_t x139 = Op (Syntax.AddWithGetCarry 31 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x135, Return x74, Return x136);
+ uint64_t x140 = (x79 & 0x3fffffff);
+ uint64_t x142, uint8_t _ = Op (Syntax.AddWithGetCarry 30 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x139, Return x77, Return x140);
+ (Return x142, Return x138, Return x134, Return x130, Return x126, Return x122, Return x118, Return x114, Return x110, Return x106, Return x102, Return x98, Return x94, Return x90, Return x86, Return x82))
+x
+     : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)