Update display logs

3 files changed, 133 insertions, 177 deletions

diff --git a/src/Specific/solinas64_2e511m187/femulDisplay.log b/src/Specific/solinas64_2e511m187/femulDisplay.log
index 0efc67963..4b8437e91 100644
--- a/src/Specific/solinas64_2e511m187/femulDisplay.log
+++ b/src/Specific/solinas64_2e511m187/femulDisplay.log
@@ -1,68 +1,52 @@
-λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
 Interp-η
 (λ var : Syntax.base_type → Type,
- λ '(x28, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x54, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31))%core,
- uint128_t x56 = (uint128_t) x5 * x54 + ((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 + ((uint128_t) x29 * x33 + (uint128_t) x28 * x31))))))))))));
- uint128_t x57 = (uint128_t) x5 * x55 + (0x2 * ((uint128_t) x7 * x53) + ((uint128_t) x9 * x51 + (0x2 * ((uint128_t) x11 * x49) + ((uint128_t) x13 * x47 + (0x2 * ((uint128_t) x15 * x45) + ((uint128_t) x17 * x43 + (0x2 * ((uint128_t) x19 * x41) + ((uint128_t) x21 * x39 + (0x2 * ((uint128_t) x23 * x37) + ((uint128_t) x25 * x35 + (0x2 * ((uint128_t) x27 * x33) + (uint128_t) x29 * x31))))))))))) + 0xbb * (0x2 * ((uint128_t) x28 * x54));
- uint128_t x58 = (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 + ((uint128_t) x25 * x33 + (uint128_t) x27 * x31)))))))))) + 0xbb * ((uint128_t) x29 * x54 + (uint128_t) x28 * x55);
- uint128_t x59 = (uint128_t) x5 * x51 + (0x2 * ((uint128_t) x7 * x49) + ((uint128_t) x9 * x47 + (0x2 * ((uint128_t) x11 * x45) + ((uint128_t) x13 * x43 + (0x2 * ((uint128_t) x15 * x41) + ((uint128_t) x17 * x39 + (0x2 * ((uint128_t) x19 * x37) + ((uint128_t) x21 * x35 + (0x2 * ((uint128_t) x23 * x33) + (uint128_t) x25 * x31))))))))) + 0xbb * (0x2 * ((uint128_t) x27 * x54) + ((uint128_t) x29 * x55 + 0x2 * ((uint128_t) x28 * x53)));
- uint128_t x60 = (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 + ((uint128_t) x21 * x33 + (uint128_t) x23 * x31)))))))) + 0xbb * ((uint128_t) x25 * x54 + ((uint128_t) x27 * x55 + ((uint128_t) x29 * x53 + (uint128_t) x28 * x51)));
- uint128_t x61 = (uint128_t) x5 * x47 + (0x2 * ((uint128_t) x7 * x45) + ((uint128_t) x9 * x43 + (0x2 * ((uint128_t) x11 * x41) + ((uint128_t) x13 * x39 + (0x2 * ((uint128_t) x15 * x37) + ((uint128_t) x17 * x35 + (0x2 * ((uint128_t) x19 * x33) + (uint128_t) x21 * x31))))))) + 0xbb * (0x2 * ((uint128_t) x23 * x54) + ((uint128_t) x25 * x55 + (0x2 * ((uint128_t) x27 * x53) + ((uint128_t) x29 * x51 + 0x2 * ((uint128_t) x28 * x49)))));
- uint128_t x62 = (uint128_t) x5 * x45 + ((uint128_t) x7 * x43 + ((uint128_t) x9 * x41 + ((uint128_t) x11 * x39 + ((uint128_t) x13 * x37 + ((uint128_t) x15 * x35 + ((uint128_t) x17 * x33 + (uint128_t) x19 * x31)))))) + 0xbb * ((uint128_t) x21 * x54 + ((uint128_t) x23 * x55 + ((uint128_t) x25 * x53 + ((uint128_t) x27 * x51 + ((uint128_t) x29 * x49 + (uint128_t) x28 * x47)))));
- uint128_t x63 = (uint128_t) x5 * x43 + (0x2 * ((uint128_t) x7 * x41) + ((uint128_t) x9 * x39 + (0x2 * ((uint128_t) x11 * x37) + ((uint128_t) x13 * x35 + (0x2 * ((uint128_t) x15 * x33) + (uint128_t) x17 * x31))))) + 0xbb * (0x2 * ((uint128_t) x19 * x54) + ((uint128_t) x21 * x55 + (0x2 * ((uint128_t) x23 * x53) + ((uint128_t) x25 * x51 + (0x2 * ((uint128_t) x27 * x49) + ((uint128_t) x29 * x47 + 0x2 * ((uint128_t) x28 * x45)))))));
- uint128_t x64 = (uint128_t) x5 * x41 + ((uint128_t) x7 * x39 + ((uint128_t) x9 * x37 + ((uint128_t) x11 * x35 + ((uint128_t) x13 * x33 + (uint128_t) x15 * x31)))) + 0xbb * ((uint128_t) x17 * x54 + ((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) x28 * x43)))))));
- uint128_t x65 = (uint128_t) x5 * x39 + (0x2 * ((uint128_t) x7 * x37) + ((uint128_t) x9 * x35 + (0x2 * ((uint128_t) x11 * x33) + (uint128_t) x13 * x31))) + 0xbb * (0x2 * ((uint128_t) x15 * x54) + ((uint128_t) x17 * x55 + (0x2 * ((uint128_t) x19 * x53) + ((uint128_t) x21 * x51 + (0x2 * ((uint128_t) x23 * x49) + ((uint128_t) x25 * x47 + (0x2 * ((uint128_t) x27 * x45) + ((uint128_t) x29 * x43 + 0x2 * ((uint128_t) x28 * x41)))))))));
- uint128_t x66 = (uint128_t) x5 * x37 + ((uint128_t) x7 * x35 + ((uint128_t) x9 * x33 + (uint128_t) x11 * x31)) + 0xbb * ((uint128_t) x13 * x54 + ((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) x28 * x39)))))))));
- uint128_t x67 = (uint128_t) x5 * x35 + (0x2 * ((uint128_t) x7 * x33) + (uint128_t) x9 * x31) + 0xbb * (0x2 * ((uint128_t) x11 * x54) + ((uint128_t) x13 * x55 + (0x2 * ((uint128_t) x15 * x53) + ((uint128_t) x17 * x51 + (0x2 * ((uint128_t) x19 * x49) + ((uint128_t) x21 * x47 + (0x2 * ((uint128_t) x23 * x45) + ((uint128_t) x25 * x43 + (0x2 * ((uint128_t) x27 * x41) + ((uint128_t) x29 * x39 + 0x2 * ((uint128_t) x28 * x37)))))))))));
- uint128_t x68 = (uint128_t) x5 * x33 + (uint128_t) x7 * x31 + 0xbb * ((uint128_t) x9 * x54 + ((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) x28 * x35)))))))))));
- uint128_t x69 = (uint128_t) x5 * x31 + 0xbb * (0x2 * ((uint128_t) x7 * x54) + ((uint128_t) x9 * x55 + (0x2 * ((uint128_t) x11 * x53) + ((uint128_t) x13 * x51 + (0x2 * ((uint128_t) x15 * x49) + ((uint128_t) x17 * x47 + (0x2 * ((uint128_t) x19 * x45) + ((uint128_t) x21 * x43 + (0x2 * ((uint128_t) x23 * x41) + ((uint128_t) x25 * x39 + (0x2 * ((uint128_t) x27 * x37) + ((uint128_t) x29 * x35 + 0x2 * ((uint128_t) x28 * x33)))))))))))));
- uint64_t x70 = (uint64_t) (x69 >> 0x25);
- uint64_t x71 = (uint64_t) x69 & 0x1fffffffff;
- uint128_t x72 = x70 + x68;
- uint64_t x73 = (uint64_t) (x72 >> 0x24);
- uint64_t x74 = (uint64_t) x72 & 0xfffffffff;
- uint128_t x75 = x73 + x67;
- uint64_t x76 = (uint64_t) (x75 >> 0x25);
- uint64_t x77 = (uint64_t) x75 & 0x1fffffffff;
- uint128_t x78 = x76 + x66;
- uint64_t x79 = (uint64_t) (x78 >> 0x24);
- uint64_t x80 = (uint64_t) x78 & 0xfffffffff;
- uint128_t x81 = x79 + x65;
- uint64_t x82 = (uint64_t) (x81 >> 0x25);
- uint64_t x83 = (uint64_t) x81 & 0x1fffffffff;
- uint128_t x84 = x82 + x64;
- uint64_t x85 = (uint64_t) (x84 >> 0x24);
- uint64_t x86 = (uint64_t) x84 & 0xfffffffff;
- uint128_t x87 = x85 + x63;
- uint64_t x88 = (uint64_t) (x87 >> 0x25);
- uint64_t x89 = (uint64_t) x87 & 0x1fffffffff;
- uint128_t x90 = x88 + x62;
- uint64_t x91 = (uint64_t) (x90 >> 0x24);
- uint64_t x92 = (uint64_t) x90 & 0xfffffffff;
- uint128_t x93 = x91 + x61;
- uint64_t x94 = (uint64_t) (x93 >> 0x25);
- uint64_t x95 = (uint64_t) x93 & 0x1fffffffff;
- uint128_t x96 = x94 + x60;
- uint64_t x97 = (uint64_t) (x96 >> 0x24);
- uint64_t x98 = (uint64_t) x96 & 0xfffffffff;
- uint128_t x99 = x97 + x59;
- uint64_t x100 = (uint64_t) (x99 >> 0x25);
- uint64_t x101 = (uint64_t) x99 & 0x1fffffffff;
- uint128_t x102 = x100 + x58;
- uint64_t x103 = (uint64_t) (x102 >> 0x24);
- uint64_t x104 = (uint64_t) x102 & 0xfffffffff;
- uint128_t x105 = x103 + x57;
- uint64_t x106 = (uint64_t) (x105 >> 0x25);
- uint64_t x107 = (uint64_t) x105 & 0x1fffffffff;
- uint128_t x108 = x106 + x56;
- uint64_t x109 = (uint64_t) (x108 >> 0x24);
- uint64_t x110 = (uint64_t) x108 & 0xfffffffff;
- uint64_t x111 = x71 + 0xbb * x109;
- uint64_t x112 = x111 >> 0x25;
- uint64_t x113 = x111 & 0x1fffffffff;
- uint64_t x114 = x112 + x74;
- uint64_t x115 = x114 >> 0x24;
- uint64_t x116 = x114 & 0xfffffffff;
- return (Return x110, Return x107, Return x104, Return x101, Return x98, Return x95, Return x92, Return x89, Return x86, Return x83, Return x80, x115 + x77, Return x116, Return x113))
+ λ '(x20, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x38, x39, x37, x35, x33, x31, x29, x27, x25, x23))%core,
+ uint128_t x40 = (((uint128_t)x5 * x38) + ((0x2 * ((uint128_t)x7 * x39)) + ((0x2 * ((uint128_t)x9 * x37)) + ((0x2 * ((uint128_t)x11 * x35)) + ((0x2 * ((uint128_t)x13 * x33)) + ((0x2 * ((uint128_t)x15 * x31)) + ((0x2 * ((uint128_t)x17 * x29)) + ((0x2 * ((uint128_t)x19 * x27)) + ((0x2 * ((uint128_t)x21 * x25)) + ((uint128_t)x20 * x23))))))))));
+ uint128_t x41 = ((((uint128_t)x5 * x39) + ((0x2 * ((uint128_t)x7 * x37)) + ((0x2 * ((uint128_t)x9 * x35)) + ((0x2 * ((uint128_t)x11 * x33)) + ((0x2 * ((uint128_t)x13 * x31)) + ((0x2 * ((uint128_t)x15 * x29)) + ((0x2 * ((uint128_t)x17 * x27)) + ((0x2 * ((uint128_t)x19 * x25)) + ((uint128_t)x21 * x23))))))))) + (0xbb * ((uint128_t)x20 * x38)));
+ uint128_t x42 = ((((uint128_t)x5 * x37) + ((0x2 * ((uint128_t)x7 * x35)) + ((0x2 * ((uint128_t)x9 * x33)) + ((0x2 * ((uint128_t)x11 * x31)) + ((0x2 * ((uint128_t)x13 * x29)) + ((0x2 * ((uint128_t)x15 * x27)) + ((0x2 * ((uint128_t)x17 * x25)) + ((uint128_t)x19 * x23)))))))) + (0xbb * (((uint128_t)x21 * x38) + ((uint128_t)x20 * x39))));
+ uint128_t x43 = ((((uint128_t)x5 * x35) + ((0x2 * ((uint128_t)x7 * x33)) + ((0x2 * ((uint128_t)x9 * x31)) + ((0x2 * ((uint128_t)x11 * x29)) + ((0x2 * ((uint128_t)x13 * x27)) + ((0x2 * ((uint128_t)x15 * x25)) + ((uint128_t)x17 * x23))))))) + (0xbb * (((uint128_t)x19 * x38) + (((uint128_t)x21 * x39) + ((uint128_t)x20 * x37)))));
+ uint128_t x44 = ((((uint128_t)x5 * x33) + ((0x2 * ((uint128_t)x7 * x31)) + ((0x2 * ((uint128_t)x9 * x29)) + ((0x2 * ((uint128_t)x11 * x27)) + ((0x2 * ((uint128_t)x13 * x25)) + ((uint128_t)x15 * x23)))))) + (0xbb * (((uint128_t)x17 * x38) + (((uint128_t)x19 * x39) + (((uint128_t)x21 * x37) + ((uint128_t)x20 * x35))))));
+ uint128_t x45 = ((((uint128_t)x5 * x31) + ((0x2 * ((uint128_t)x7 * x29)) + ((0x2 * ((uint128_t)x9 * x27)) + ((0x2 * ((uint128_t)x11 * x25)) + ((uint128_t)x13 * x23))))) + (0xbb * (((uint128_t)x15 * x38) + (((uint128_t)x17 * x39) + (((uint128_t)x19 * x37) + (((uint128_t)x21 * x35) + ((uint128_t)x20 * x33)))))));
+ uint128_t x46 = ((((uint128_t)x5 * x29) + ((0x2 * ((uint128_t)x7 * x27)) + ((0x2 * ((uint128_t)x9 * x25)) + ((uint128_t)x11 * x23)))) + (0xbb * (((uint128_t)x13 * x38) + (((uint128_t)x15 * x39) + (((uint128_t)x17 * x37) + (((uint128_t)x19 * x35) + (((uint128_t)x21 * x33) + ((uint128_t)x20 * x31))))))));
+ uint128_t x47 = ((((uint128_t)x5 * x27) + ((0x2 * ((uint128_t)x7 * x25)) + ((uint128_t)x9 * x23))) + (0xbb * (((uint128_t)x11 * x38) + (((uint128_t)x13 * x39) + (((uint128_t)x15 * x37) + (((uint128_t)x17 * x35) + (((uint128_t)x19 * x33) + (((uint128_t)x21 * x31) + ((uint128_t)x20 * x29)))))))));
+ uint128_t x48 = ((((uint128_t)x5 * x25) + ((uint128_t)x7 * x23)) + (0xbb * (((uint128_t)x9 * x38) + (((uint128_t)x11 * x39) + (((uint128_t)x13 * x37) + (((uint128_t)x15 * x35) + (((uint128_t)x17 * x33) + (((uint128_t)x19 * x31) + (((uint128_t)x21 * x29) + ((uint128_t)x20 * x27))))))))));
+ uint128_t x49 = (((uint128_t)x5 * x23) + (0xbb * ((0x2 * ((uint128_t)x7 * x38)) + ((0x2 * ((uint128_t)x9 * x39)) + ((0x2 * ((uint128_t)x11 * x37)) + ((0x2 * ((uint128_t)x13 * x35)) + ((0x2 * ((uint128_t)x15 * x33)) + ((0x2 * ((uint128_t)x17 * x31)) + ((0x2 * ((uint128_t)x19 * x29)) + ((0x2 * ((uint128_t)x21 * x27)) + (0x2 * ((uint128_t)x20 * x25))))))))))));
+ uint128_t x50 = (x49 >> 0x34);
+ uint64_t x51 = ((uint64_t)x49 & 0xfffffffffffff);
+ uint128_t x52 = (x50 + x48);
+ uint128_t x53 = (x52 >> 0x33);
+ uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
+ uint128_t x55 = (x53 + x47);
+ uint128_t x56 = (x55 >> 0x33);
+ uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
+ uint128_t x58 = (x56 + x46);
+ uint128_t x59 = (x58 >> 0x33);
+ uint64_t x60 = ((uint64_t)x58 & 0x7ffffffffffff);
+ uint128_t x61 = (x59 + x45);
+ uint128_t x62 = (x61 >> 0x33);
+ uint64_t x63 = ((uint64_t)x61 & 0x7ffffffffffff);
+ uint128_t x64 = (x62 + x44);
+ uint128_t x65 = (x64 >> 0x33);
+ uint64_t x66 = ((uint64_t)x64 & 0x7ffffffffffff);
+ uint128_t x67 = (x65 + x43);
+ uint64_t x68 = (uint64_t) (x67 >> 0x33);
+ uint64_t x69 = ((uint64_t)x67 & 0x7ffffffffffff);
+ uint128_t x70 = (x68 + x42);
+ uint64_t x71 = (uint64_t) (x70 >> 0x33);
+ uint64_t x72 = ((uint64_t)x70 & 0x7ffffffffffff);
+ uint128_t x73 = (x71 + x41);
+ uint64_t x74 = (uint64_t) (x73 >> 0x33);
+ uint64_t x75 = ((uint64_t)x73 & 0x7ffffffffffff);
+ uint128_t x76 = (x74 + x40);
+ uint64_t x77 = (uint64_t) (x76 >> 0x33);
+ uint64_t x78 = ((uint64_t)x76 & 0x7ffffffffffff);
+ uint128_t x79 = (x51 + ((uint128_t)0xbb * x77));
+ uint64_t x80 = (uint64_t) (x79 >> 0x34);
+ uint64_t x81 = ((uint64_t)x79 & 0xfffffffffffff);
+ uint64_t x82 = (x80 + x54);
+ uint64_t x83 = (x82 >> 0x33);
+ uint64_t x84 = (x82 & 0x7ffffffffffff);
+ return (Return x78, Return x75, Return x72, Return x69, Return x66, Return x63, Return x60, (x83 + x57), Return x84, Return x81))
 (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 → 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)
+     : 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)
diff --git a/src/Specific/solinas64_2e511m187/fesquareDisplay.log b/src/Specific/solinas64_2e511m187/fesquareDisplay.log
index 486b953d2..2abb714d0 100644
--- a/src/Specific/solinas64_2e511m187/fesquareDisplay.log
+++ b/src/Specific/solinas64_2e511m187/fesquareDisplay.log
@@ -1,68 +1,52 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
 Interp-η
 (λ var : Syntax.base_type → Type,
- λ '(x25, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
- uint128_t x27 = (uint128_t) x2 * x25 + ((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) x25 * x2))))))))))));
- uint128_t x28 = (uint128_t) x2 * x26 + (0x2 * ((uint128_t) x4 * x24) + ((uint128_t) x6 * x22 + (0x2 * ((uint128_t) x8 * x20) + ((uint128_t) x10 * x18 + (0x2 * ((uint128_t) x12 * x16) + ((uint128_t) x14 * x14 + (0x2 * ((uint128_t) x16 * x12) + ((uint128_t) x18 * x10 + (0x2 * ((uint128_t) x20 * x8) + ((uint128_t) x22 * x6 + (0x2 * ((uint128_t) x24 * x4) + (uint128_t) x26 * x2))))))))))) + 0xbb * (0x2 * ((uint128_t) x25 * x25));
- uint128_t x29 = (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)))))))))) + 0xbb * ((uint128_t) x26 * x25 + (uint128_t) x25 * x26);
- uint128_t x30 = (uint128_t) x2 * x22 + (0x2 * ((uint128_t) x4 * x20) + ((uint128_t) x6 * x18 + (0x2 * ((uint128_t) x8 * x16) + ((uint128_t) x10 * x14 + (0x2 * ((uint128_t) x12 * x12) + ((uint128_t) x14 * x10 + (0x2 * ((uint128_t) x16 * x8) + ((uint128_t) x18 * x6 + (0x2 * ((uint128_t) x20 * x4) + (uint128_t) x22 * x2))))))))) + 0xbb * (0x2 * ((uint128_t) x24 * x25) + ((uint128_t) x26 * x26 + 0x2 * ((uint128_t) x25 * x24)));
- uint128_t x31 = (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)))))))) + 0xbb * ((uint128_t) x22 * x25 + ((uint128_t) x24 * x26 + ((uint128_t) x26 * x24 + (uint128_t) x25 * x22)));
- uint128_t x32 = (uint128_t) x2 * x18 + (0x2 * ((uint128_t) x4 * x16) + ((uint128_t) x6 * x14 + (0x2 * ((uint128_t) x8 * x12) + ((uint128_t) x10 * x10 + (0x2 * ((uint128_t) x12 * x8) + ((uint128_t) x14 * x6 + (0x2 * ((uint128_t) x16 * x4) + (uint128_t) x18 * x2))))))) + 0xbb * (0x2 * ((uint128_t) x20 * x25) + ((uint128_t) x22 * x26 + (0x2 * ((uint128_t) x24 * x24) + ((uint128_t) x26 * x22 + 0x2 * ((uint128_t) x25 * x20)))));
- uint128_t x33 = (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)))))) + 0xbb * ((uint128_t) x18 * x25 + ((uint128_t) x20 * x26 + ((uint128_t) x22 * x24 + ((uint128_t) x24 * x22 + ((uint128_t) x26 * x20 + (uint128_t) x25 * x18)))));
- uint128_t x34 = (uint128_t) x2 * x14 + (0x2 * ((uint128_t) x4 * x12) + ((uint128_t) x6 * x10 + (0x2 * ((uint128_t) x8 * x8) + ((uint128_t) x10 * x6 + (0x2 * ((uint128_t) x12 * x4) + (uint128_t) x14 * x2))))) + 0xbb * (0x2 * ((uint128_t) x16 * x25) + ((uint128_t) x18 * x26 + (0x2 * ((uint128_t) x20 * x24) + ((uint128_t) x22 * x22 + (0x2 * ((uint128_t) x24 * x20) + ((uint128_t) x26 * x18 + 0x2 * ((uint128_t) x25 * x16)))))));
- uint128_t x35 = (uint128_t) x2 * x12 + ((uint128_t) x4 * x10 + ((uint128_t) x6 * x8 + ((uint128_t) x8 * x6 + ((uint128_t) x10 * x4 + (uint128_t) x12 * x2)))) + 0xbb * ((uint128_t) x14 * x25 + ((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) x25 * x14)))))));
- uint128_t x36 = (uint128_t) x2 * x10 + (0x2 * ((uint128_t) x4 * x8) + ((uint128_t) x6 * x6 + (0x2 * ((uint128_t) x8 * x4) + (uint128_t) x10 * x2))) + 0xbb * (0x2 * ((uint128_t) x12 * x25) + ((uint128_t) x14 * x26 + (0x2 * ((uint128_t) x16 * x24) + ((uint128_t) x18 * x22 + (0x2 * ((uint128_t) x20 * x20) + ((uint128_t) x22 * x18 + (0x2 * ((uint128_t) x24 * x16) + ((uint128_t) x26 * x14 + 0x2 * ((uint128_t) x25 * x12)))))))));
- uint128_t x37 = (uint128_t) x2 * x8 + ((uint128_t) x4 * x6 + ((uint128_t) x6 * x4 + (uint128_t) x8 * x2)) + 0xbb * ((uint128_t) x10 * x25 + ((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) x25 * x10)))))))));
- uint128_t x38 = (uint128_t) x2 * x6 + (0x2 * ((uint128_t) x4 * x4) + (uint128_t) x6 * x2) + 0xbb * (0x2 * ((uint128_t) x8 * x25) + ((uint128_t) x10 * x26 + (0x2 * ((uint128_t) x12 * x24) + ((uint128_t) x14 * x22 + (0x2 * ((uint128_t) x16 * x20) + ((uint128_t) x18 * x18 + (0x2 * ((uint128_t) x20 * x16) + ((uint128_t) x22 * x14 + (0x2 * ((uint128_t) x24 * x12) + ((uint128_t) x26 * x10 + 0x2 * ((uint128_t) x25 * x8)))))))))));
- uint128_t x39 = (uint128_t) x2 * x4 + (uint128_t) x4 * x2 + 0xbb * ((uint128_t) x6 * x25 + ((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) x25 * x6)))))))))));
- uint128_t x40 = (uint128_t) x2 * x2 + 0xbb * (0x2 * ((uint128_t) x4 * x25) + ((uint128_t) x6 * x26 + (0x2 * ((uint128_t) x8 * x24) + ((uint128_t) x10 * x22 + (0x2 * ((uint128_t) x12 * x20) + ((uint128_t) x14 * x18 + (0x2 * ((uint128_t) x16 * x16) + ((uint128_t) x18 * x14 + (0x2 * ((uint128_t) x20 * x12) + ((uint128_t) x22 * x10 + (0x2 * ((uint128_t) x24 * x8) + ((uint128_t) x26 * x6 + 0x2 * ((uint128_t) x25 * x4)))))))))))));
- uint64_t x41 = (uint64_t) (x40 >> 0x25);
- uint64_t x42 = (uint64_t) x40 & 0x1fffffffff;
- uint128_t x43 = x41 + x39;
- uint64_t x44 = (uint64_t) (x43 >> 0x24);
- uint64_t x45 = (uint64_t) x43 & 0xfffffffff;
- uint128_t x46 = x44 + x38;
- uint64_t x47 = (uint64_t) (x46 >> 0x25);
- uint64_t x48 = (uint64_t) x46 & 0x1fffffffff;
- uint128_t x49 = x47 + x37;
- uint64_t x50 = (uint64_t) (x49 >> 0x24);
- uint64_t x51 = (uint64_t) x49 & 0xfffffffff;
- uint128_t x52 = x50 + x36;
- uint64_t x53 = (uint64_t) (x52 >> 0x25);
- uint64_t x54 = (uint64_t) x52 & 0x1fffffffff;
- uint128_t x55 = x53 + x35;
- uint64_t x56 = (uint64_t) (x55 >> 0x24);
- uint64_t x57 = (uint64_t) x55 & 0xfffffffff;
- uint128_t x58 = x56 + x34;
- uint64_t x59 = (uint64_t) (x58 >> 0x25);
- uint64_t x60 = (uint64_t) x58 & 0x1fffffffff;
- uint128_t x61 = x59 + x33;
- uint64_t x62 = (uint64_t) (x61 >> 0x24);
- uint64_t x63 = (uint64_t) x61 & 0xfffffffff;
- uint128_t x64 = x62 + x32;
- uint64_t x65 = (uint64_t) (x64 >> 0x25);
- uint64_t x66 = (uint64_t) x64 & 0x1fffffffff;
- uint128_t x67 = x65 + x31;
- uint64_t x68 = (uint64_t) (x67 >> 0x24);
- uint64_t x69 = (uint64_t) x67 & 0xfffffffff;
- uint128_t x70 = x68 + x30;
- uint64_t x71 = (uint64_t) (x70 >> 0x25);
- uint64_t x72 = (uint64_t) x70 & 0x1fffffffff;
- uint128_t x73 = x71 + x29;
- uint64_t x74 = (uint64_t) (x73 >> 0x24);
- uint64_t x75 = (uint64_t) x73 & 0xfffffffff;
- uint128_t x76 = x74 + x28;
- uint64_t x77 = (uint64_t) (x76 >> 0x25);
- uint64_t x78 = (uint64_t) x76 & 0x1fffffffff;
- uint128_t x79 = x77 + x27;
- uint64_t x80 = (uint64_t) (x79 >> 0x24);
- uint64_t x81 = (uint64_t) x79 & 0xfffffffff;
- uint64_t x82 = x42 + 0xbb * x80;
- uint64_t x83 = x82 >> 0x25;
- uint64_t x84 = x82 & 0x1fffffffff;
- uint64_t x85 = x83 + x45;
- uint64_t x86 = x85 >> 0x24;
- uint64_t x87 = x85 & 0xfffffffff;
- return (Return x81, Return x78, Return x75, Return x72, Return x69, Return x66, Return x63, Return x60, Return x57, Return x54, Return x51, x86 + x48, Return x87, Return x84))
+ λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint128_t x19 = (((uint128_t)x2 * x17) + ((0x2 * ((uint128_t)x4 * x18)) + ((0x2 * ((uint128_t)x6 * x16)) + ((0x2 * ((uint128_t)x8 * x14)) + ((0x2 * ((uint128_t)x10 * x12)) + ((0x2 * ((uint128_t)x12 * x10)) + ((0x2 * ((uint128_t)x14 * x8)) + ((0x2 * ((uint128_t)x16 * x6)) + ((0x2 * ((uint128_t)x18 * x4)) + ((uint128_t)x17 * x2))))))))));
+ uint128_t x20 = ((((uint128_t)x2 * x18) + ((0x2 * ((uint128_t)x4 * x16)) + ((0x2 * ((uint128_t)x6 * x14)) + ((0x2 * ((uint128_t)x8 * x12)) + ((0x2 * ((uint128_t)x10 * x10)) + ((0x2 * ((uint128_t)x12 * x8)) + ((0x2 * ((uint128_t)x14 * x6)) + ((0x2 * ((uint128_t)x16 * x4)) + ((uint128_t)x18 * x2))))))))) + (0xbb * ((uint128_t)x17 * x17)));
+ uint128_t x21 = ((((uint128_t)x2 * x16) + ((0x2 * ((uint128_t)x4 * x14)) + ((0x2 * ((uint128_t)x6 * x12)) + ((0x2 * ((uint128_t)x8 * x10)) + ((0x2 * ((uint128_t)x10 * x8)) + ((0x2 * ((uint128_t)x12 * x6)) + ((0x2 * ((uint128_t)x14 * x4)) + ((uint128_t)x16 * x2)))))))) + (0xbb * (((uint128_t)x18 * x17) + ((uint128_t)x17 * x18))));
+ uint128_t x22 = ((((uint128_t)x2 * x14) + ((0x2 * ((uint128_t)x4 * x12)) + ((0x2 * ((uint128_t)x6 * x10)) + ((0x2 * ((uint128_t)x8 * x8)) + ((0x2 * ((uint128_t)x10 * x6)) + ((0x2 * ((uint128_t)x12 * x4)) + ((uint128_t)x14 * x2))))))) + (0xbb * (((uint128_t)x16 * x17) + (((uint128_t)x18 * x18) + ((uint128_t)x17 * x16)))));
+ uint128_t x23 = ((((uint128_t)x2 * x12) + ((0x2 * ((uint128_t)x4 * x10)) + ((0x2 * ((uint128_t)x6 * x8)) + ((0x2 * ((uint128_t)x8 * x6)) + ((0x2 * ((uint128_t)x10 * x4)) + ((uint128_t)x12 * x2)))))) + (0xbb * (((uint128_t)x14 * x17) + (((uint128_t)x16 * x18) + (((uint128_t)x18 * x16) + ((uint128_t)x17 * x14))))));
+ uint128_t x24 = ((((uint128_t)x2 * x10) + ((0x2 * ((uint128_t)x4 * x8)) + ((0x2 * ((uint128_t)x6 * x6)) + ((0x2 * ((uint128_t)x8 * x4)) + ((uint128_t)x10 * x2))))) + (0xbb * (((uint128_t)x12 * x17) + (((uint128_t)x14 * x18) + (((uint128_t)x16 * x16) + (((uint128_t)x18 * x14) + ((uint128_t)x17 * x12)))))));
+ uint128_t x25 = ((((uint128_t)x2 * x8) + ((0x2 * ((uint128_t)x4 * x6)) + ((0x2 * ((uint128_t)x6 * x4)) + ((uint128_t)x8 * x2)))) + (0xbb * (((uint128_t)x10 * x17) + (((uint128_t)x12 * x18) + (((uint128_t)x14 * x16) + (((uint128_t)x16 * x14) + (((uint128_t)x18 * x12) + ((uint128_t)x17 * x10))))))));
+ uint128_t x26 = ((((uint128_t)x2 * x6) + ((0x2 * ((uint128_t)x4 * x4)) + ((uint128_t)x6 * x2))) + (0xbb * (((uint128_t)x8 * x17) + (((uint128_t)x10 * x18) + (((uint128_t)x12 * x16) + (((uint128_t)x14 * x14) + (((uint128_t)x16 * x12) + (((uint128_t)x18 * x10) + ((uint128_t)x17 * x8)))))))));
+ uint128_t x27 = ((((uint128_t)x2 * x4) + ((uint128_t)x4 * x2)) + (0xbb * (((uint128_t)x6 * x17) + (((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)x17 * x6))))))))));
+ uint128_t x28 = (((uint128_t)x2 * x2) + (0xbb * ((0x2 * ((uint128_t)x4 * x17)) + ((0x2 * ((uint128_t)x6 * x18)) + ((0x2 * ((uint128_t)x8 * x16)) + ((0x2 * ((uint128_t)x10 * x14)) + ((0x2 * ((uint128_t)x12 * x12)) + ((0x2 * ((uint128_t)x14 * x10)) + ((0x2 * ((uint128_t)x16 * x8)) + ((0x2 * ((uint128_t)x18 * x6)) + (0x2 * ((uint128_t)x17 * x4))))))))))));
+ uint128_t x29 = (x28 >> 0x34);
+ uint64_t x30 = ((uint64_t)x28 & 0xfffffffffffff);
+ uint128_t x31 = (x29 + x27);
+ uint128_t x32 = (x31 >> 0x33);
+ uint64_t x33 = ((uint64_t)x31 & 0x7ffffffffffff);
+ uint128_t x34 = (x32 + x26);
+ uint128_t x35 = (x34 >> 0x33);
+ uint64_t x36 = ((uint64_t)x34 & 0x7ffffffffffff);
+ uint128_t x37 = (x35 + x25);
+ uint128_t x38 = (x37 >> 0x33);
+ uint64_t x39 = ((uint64_t)x37 & 0x7ffffffffffff);
+ uint128_t x40 = (x38 + x24);
+ uint128_t x41 = (x40 >> 0x33);
+ uint64_t x42 = ((uint64_t)x40 & 0x7ffffffffffff);
+ uint128_t x43 = (x41 + x23);
+ uint128_t x44 = (x43 >> 0x33);
+ uint64_t x45 = ((uint64_t)x43 & 0x7ffffffffffff);
+ uint128_t x46 = (x44 + x22);
+ uint64_t x47 = (uint64_t) (x46 >> 0x33);
+ uint64_t x48 = ((uint64_t)x46 & 0x7ffffffffffff);
+ uint128_t x49 = (x47 + x21);
+ uint64_t x50 = (uint64_t) (x49 >> 0x33);
+ uint64_t x51 = ((uint64_t)x49 & 0x7ffffffffffff);
+ uint128_t x52 = (x50 + x20);
+ uint64_t x53 = (uint64_t) (x52 >> 0x33);
+ uint64_t x54 = ((uint64_t)x52 & 0x7ffffffffffff);
+ uint128_t x55 = (x53 + x19);
+ uint64_t x56 = (uint64_t) (x55 >> 0x33);
+ uint64_t x57 = ((uint64_t)x55 & 0x7ffffffffffff);
+ uint128_t x58 = (x30 + ((uint128_t)0xbb * x56));
+ uint64_t x59 = (uint64_t) (x58 >> 0x34);
+ uint64_t x60 = ((uint64_t)x58 & 0xfffffffffffff);
+ uint64_t x61 = (x59 + x33);
+ uint64_t x62 = (x61 >> 0x33);
+ uint64_t x63 = (x61 & 0x7ffffffffffff);
+ return (Return x57, Return x54, Return x51, Return x48, Return x45, Return x42, Return x39, (x62 + x36), Return x63, Return x60))
 x
-     : 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)
+     : 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)
diff --git a/src/Specific/solinas64_2e511m187/freezeDisplay.log b/src/Specific/solinas64_2e511m187/freezeDisplay.log
index c798e3559..fcccbd45b 100644
--- a/src/Specific/solinas64_2e511m187/freezeDisplay.log
+++ b/src/Specific/solinas64_2e511m187/freezeDisplay.log
@@ -1,50 +1,38 @@
-λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
+λ x : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64,
 Interp-η
 (λ var : Syntax.base_type → Type,
- λ '(x25, x26, x24, x22, x20, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
- uint64_t x28, uint8_t x29 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, 0x1fffffff45);
- uint64_t x31, uint8_t x32 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x29, Return x4, 0xfffffffff);
- uint64_t x34, uint8_t x35 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x32, Return x6, 0x1fffffffff);
- uint64_t x37, uint8_t x38 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x35, Return x8, 0xfffffffff);
- uint64_t x40, uint8_t x41 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x38, Return x10, 0x1fffffffff);
- uint64_t x43, uint8_t x44 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x41, Return x12, 0xfffffffff);
- uint64_t x46, uint8_t x47 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x44, Return x14, 0x1fffffffff);
- uint64_t x49, uint8_t x50 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x47, Return x16, 0xfffffffff);
- uint64_t x52, uint8_t x53 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x50, Return x18, 0x1fffffffff);
- uint64_t x55, uint8_t x56 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x53, Return x20, 0xfffffffff);
- uint64_t x58, uint8_t x59 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x56, Return x22, 0x1fffffffff);
- uint64_t x61, uint8_t x62 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x59, Return x24, 0xfffffffff);
- uint64_t x64, uint8_t x65 = Op (Syntax.SubWithGetBorrow 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x62, Return x26, 0x1fffffffff);
- uint64_t x67, uint8_t x68 = Op (Syntax.SubWithGetBorrow 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x65, Return x25, 0xfffffffff);
- uint64_t x69 = (uint64_t)cmovznz(x68, 0x0, 0xffffffffffffffffL);
- uint64_t x70 = x69 & 0x1fffffff45;
- uint64_t x72, uint8_t x73 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x28, Return x70);
- uint64_t x74 = x69 & 0xfffffffff;
- uint64_t x76, uint8_t x77 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x73, Return x31, Return x74);
- uint64_t x78 = x69 & 0x1fffffffff;
- uint64_t x80, uint8_t x81 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x77, Return x34, Return x78);
- uint64_t x82 = x69 & 0xfffffffff;
- uint64_t x84, uint8_t x85 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x81, Return x37, Return x82);
- uint64_t x86 = x69 & 0x1fffffffff;
- uint64_t x88, uint8_t x89 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x85, Return x40, Return x86);
- uint64_t x90 = x69 & 0xfffffffff;
- uint64_t x92, uint8_t x93 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x89, Return x43, Return x90);
- uint64_t x94 = x69 & 0x1fffffffff;
- uint64_t x96, uint8_t x97 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x93, Return x46, Return x94);
- uint64_t x98 = x69 & 0xfffffffff;
- uint64_t x100, uint8_t x101 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x97, Return x49, Return x98);
- uint64_t x102 = x69 & 0x1fffffffff;
- uint64_t x104, uint8_t x105 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x101, Return x52, Return x102);
- uint64_t x106 = x69 & 0xfffffffff;
- uint64_t x108, uint8_t x109 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x105, Return x55, Return x106);
- uint64_t x110 = x69 & 0x1fffffffff;
- uint64_t x112, uint8_t x113 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x109, Return x58, Return x110);
- uint64_t x114 = x69 & 0xfffffffff;
- uint64_t x116, uint8_t x117 = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x113, Return x61, Return x114);
- uint64_t x118 = x69 & 0x1fffffffff;
- uint64_t x120, uint8_t x121 = Op (Syntax.AddWithGetCarry 37 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x117, Return x64, Return x118);
- uint64_t x122 = x69 & 0xfffffffff;
- uint64_t x124, uint8_t _ = Op (Syntax.AddWithGetCarry 36 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (Return x121, Return x67, Return x122);
- (Return x124, Return x120, Return x116, Return x112, Return x108, Return x104, Return x100, Return x96, Return x92, Return x88, Return x84, Return x80, Return x76, Return x72))
+ λ '(x17, x18, x16, x14, x12, x10, x8, x6, x4, x2)%core,
+ uint64_t x20, uint8_t x21 = Op (Syntax.SubWithGetBorrow 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x2, Const 4503599627370309);
+ uint64_t x23, uint8_t x24 = subborrow_u51(x21, x4, 0x7ffffffffffff);
+ uint64_t x26, uint8_t x27 = subborrow_u51(x24, x6, 0x7ffffffffffff);
+ uint64_t x29, uint8_t x30 = subborrow_u51(x27, x8, 0x7ffffffffffff);
+ uint64_t x32, uint8_t x33 = subborrow_u51(x30, x10, 0x7ffffffffffff);
+ uint64_t x35, uint8_t x36 = subborrow_u51(x33, x12, 0x7ffffffffffff);
+ uint64_t x38, uint8_t x39 = subborrow_u51(x36, x14, 0x7ffffffffffff);
+ uint64_t x41, uint8_t x42 = subborrow_u51(x39, x16, 0x7ffffffffffff);
+ uint64_t x44, uint8_t x45 = subborrow_u51(x42, x18, 0x7ffffffffffff);
+ uint64_t x47, uint8_t x48 = subborrow_u51(x45, x17, 0x7ffffffffffff);
+ uint64_t x49 = (uint64_t)cmovznz(x48, 0x0, 0xffffffffffffffffL);
+ uint64_t x50 = (x49 & Const 4503599627370309);
+ uint64_t x52, uint8_t x53 = Op (Syntax.AddWithGetCarry 52 (Syntax.TWord 3) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 6) (Syntax.TWord 3)) (0x0, Return x20, Return x50);
+ uint64_t x54 = (x49 & 0x7ffffffffffff);
+ uint64_t x56, uint8_t x57 = addcarryx_u51(x53, x23, x54);
+ uint64_t x58 = (x49 & 0x7ffffffffffff);
+ uint64_t x60, uint8_t x61 = addcarryx_u51(x57, x26, x58);
+ uint64_t x62 = (x49 & 0x7ffffffffffff);
+ uint64_t x64, uint8_t x65 = addcarryx_u51(x61, x29, x62);
+ uint64_t x66 = (x49 & 0x7ffffffffffff);
+ uint64_t x68, uint8_t x69 = addcarryx_u51(x65, x32, x66);
+ uint64_t x70 = (x49 & 0x7ffffffffffff);
+ uint64_t x72, uint8_t x73 = addcarryx_u51(x69, x35, x70);
+ uint64_t x74 = (x49 & 0x7ffffffffffff);
+ uint64_t x76, uint8_t x77 = addcarryx_u51(x73, x38, x74);
+ uint64_t x78 = (x49 & 0x7ffffffffffff);
+ uint64_t x80, uint8_t x81 = addcarryx_u51(x77, x41, x78);
+ uint64_t x82 = (x49 & 0x7ffffffffffff);
+ uint64_t x84, uint8_t x85 = addcarryx_u51(x81, x44, x82);
+ uint64_t x86 = (x49 & 0x7ffffffffffff);
+ uint64_t x88, uint8_t _ = addcarryx_u51(x85, x47, x86);
+ (Return x88, Return x84, Return x80, Return x76, Return x72, Return x68, Return x64, Return x60, Return x56, Return x52))
 x
-     : 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)
+     : 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)