aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Specific/montgomery32_2e130m5/femulDisplay.log10
-rw-r--r--src/Specific/montgomery32_2e165m25/femulDisplay.log12
-rw-r--r--src/Specific/montgomery32_2e166m5/femulDisplay.log12
-rw-r--r--src/Specific/montgomery64_2e130m5/femul.c6
-rw-r--r--src/Specific/montgomery64_2e130m5/femulDisplay.log6
-rw-r--r--src/Specific/solinas32_2e510m290x2e496m1/fesubDisplay.log2
-rw-r--r--src/Specific/solinas32_2e512m491x2e496m1/fesubDisplay.log2
7 files changed, 25 insertions, 25 deletions
diff --git a/src/Specific/montgomery32_2e130m5/femulDisplay.log b/src/Specific/montgomery32_2e130m5/femulDisplay.log
index 9e8f3f1f7..7d2e6f3bf 100644
--- a/src/Specific/montgomery32_2e130m5/femulDisplay.log
+++ b/src/Specific/montgomery32_2e130m5/femulDisplay.log
@@ -17,7 +17,7 @@ Interp-η
uint32_t x57, uint32_t x58 = mulx_u32(x51, 0xffffffff);
uint32_t x60, uint32_t x61 = mulx_u32(x51, 0xffffffff);
uint32_t x63, uint32_t x64 = mulx_u32(x51, 0xffffffff);
- uint32_t x66, uint8_t x67 = (uint8_t)mulx_u32(x51, 0x3);
+ uint32_t x66, uint8_t x67 = mulx_u32_out_u8(x51, 0x3);
uint32_t x69, uint8_t x70 = addcarryx_u32(0x0, x55, x57);
uint32_t x72, uint8_t x73 = addcarryx_u32(x70, x58, x60);
uint32_t x75, uint8_t x76 = addcarryx_u32(x73, x61, x63);
@@ -50,7 +50,7 @@ Interp-η
uint32_t x154, uint32_t x155 = mulx_u32(x148, 0xffffffff);
uint32_t x157, uint32_t x158 = mulx_u32(x148, 0xffffffff);
uint32_t x160, uint32_t x161 = mulx_u32(x148, 0xffffffff);
- uint32_t x163, uint8_t x164 = (uint8_t)mulx_u32(x148, 0x3);
+ uint32_t x163, uint8_t x164 = mulx_u32_out_u8(x148, 0x3);
uint32_t x166, uint8_t x167 = addcarryx_u32(0x0, x152, x154);
uint32_t x169, uint8_t x170 = addcarryx_u32(x167, x155, x157);
uint32_t x172, uint8_t x173 = addcarryx_u32(x170, x158, x160);
@@ -84,7 +84,7 @@ Interp-η
uint32_t x252, uint32_t x253 = mulx_u32(x246, 0xffffffff);
uint32_t x255, uint32_t x256 = mulx_u32(x246, 0xffffffff);
uint32_t x258, uint32_t x259 = mulx_u32(x246, 0xffffffff);
- uint32_t x261, uint8_t x262 = (uint8_t)mulx_u32(x246, 0x3);
+ uint32_t x261, uint8_t x262 = mulx_u32_out_u8(x246, 0x3);
uint32_t x264, uint8_t x265 = addcarryx_u32(0x0, x250, x252);
uint32_t x267, uint8_t x268 = addcarryx_u32(x265, x253, x255);
uint32_t x270, uint8_t x271 = addcarryx_u32(x268, x256, x258);
@@ -118,7 +118,7 @@ Interp-η
uint32_t x350, uint32_t x351 = mulx_u32(x344, 0xffffffff);
uint32_t x353, uint32_t x354 = mulx_u32(x344, 0xffffffff);
uint32_t x356, uint32_t x357 = mulx_u32(x344, 0xffffffff);
- uint32_t x359, uint8_t x360 = (uint8_t)mulx_u32(x344, 0x3);
+ uint32_t x359, uint8_t x360 = mulx_u32_out_u8(x344, 0x3);
uint32_t x362, uint8_t x363 = addcarryx_u32(0x0, x348, x350);
uint32_t x365, uint8_t x366 = addcarryx_u32(x363, x351, x353);
uint32_t x368, uint8_t x369 = addcarryx_u32(x366, x354, x356);
@@ -152,7 +152,7 @@ Interp-η
uint32_t x448, uint32_t x449 = mulx_u32(x442, 0xffffffff);
uint32_t x451, uint32_t x452 = mulx_u32(x442, 0xffffffff);
uint32_t x454, uint32_t x455 = mulx_u32(x442, 0xffffffff);
- uint32_t x457, uint8_t x458 = (uint8_t)mulx_u32(x442, 0x3);
+ uint32_t x457, uint8_t x458 = mulx_u32_out_u8(x442, 0x3);
uint32_t x460, uint8_t x461 = addcarryx_u32(0x0, x446, x448);
uint32_t x463, uint8_t x464 = addcarryx_u32(x461, x449, x451);
uint32_t x466, uint8_t x467 = addcarryx_u32(x464, x452, x454);
diff --git a/src/Specific/montgomery32_2e165m25/femulDisplay.log b/src/Specific/montgomery32_2e165m25/femulDisplay.log
index e15727cb3..b47d7d467 100644
--- a/src/Specific/montgomery32_2e165m25/femulDisplay.log
+++ b/src/Specific/montgomery32_2e165m25/femulDisplay.log
@@ -20,7 +20,7 @@ Interp-η
uint32_t x70, uint32_t x71 = mulx_u32(x61, 0xffffffff);
uint32_t x73, uint32_t x74 = mulx_u32(x61, 0xffffffff);
uint32_t x76, uint32_t x77 = mulx_u32(x61, 0xffffffff);
- uint32_t x79, uint8_t x80 = (uint8_t)mulx_u32(x61, 0x1f);
+ uint32_t x79, uint8_t x80 = mulx_u32_out_u8(x61, 0x1f);
uint32_t x82, uint8_t x83 = addcarryx_u32(0x0, x65, x67);
uint32_t x85, uint8_t x86 = addcarryx_u32(x83, x68, x70);
uint32_t x88, uint8_t x89 = addcarryx_u32(x86, x71, x73);
@@ -59,7 +59,7 @@ Interp-η
uint32_t x185, uint32_t x186 = mulx_u32(x176, 0xffffffff);
uint32_t x188, uint32_t x189 = mulx_u32(x176, 0xffffffff);
uint32_t x191, uint32_t x192 = mulx_u32(x176, 0xffffffff);
- uint32_t x194, uint8_t x195 = (uint8_t)mulx_u32(x176, 0x1f);
+ uint32_t x194, uint8_t x195 = mulx_u32_out_u8(x176, 0x1f);
uint32_t x197, uint8_t x198 = addcarryx_u32(0x0, x180, x182);
uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x183, x185);
uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x186, x188);
@@ -99,7 +99,7 @@ Interp-η
uint32_t x301, uint32_t x302 = mulx_u32(x292, 0xffffffff);
uint32_t x304, uint32_t x305 = mulx_u32(x292, 0xffffffff);
uint32_t x307, uint32_t x308 = mulx_u32(x292, 0xffffffff);
- uint32_t x310, uint8_t x311 = (uint8_t)mulx_u32(x292, 0x1f);
+ uint32_t x310, uint8_t x311 = mulx_u32_out_u8(x292, 0x1f);
uint32_t x313, uint8_t x314 = addcarryx_u32(0x0, x296, x298);
uint32_t x316, uint8_t x317 = addcarryx_u32(x314, x299, x301);
uint32_t x319, uint8_t x320 = addcarryx_u32(x317, x302, x304);
@@ -139,7 +139,7 @@ Interp-η
uint32_t x417, uint32_t x418 = mulx_u32(x408, 0xffffffff);
uint32_t x420, uint32_t x421 = mulx_u32(x408, 0xffffffff);
uint32_t x423, uint32_t x424 = mulx_u32(x408, 0xffffffff);
- uint32_t x426, uint8_t x427 = (uint8_t)mulx_u32(x408, 0x1f);
+ uint32_t x426, uint8_t x427 = mulx_u32_out_u8(x408, 0x1f);
uint32_t x429, uint8_t x430 = addcarryx_u32(0x0, x412, x414);
uint32_t x432, uint8_t x433 = addcarryx_u32(x430, x415, x417);
uint32_t x435, uint8_t x436 = addcarryx_u32(x433, x418, x420);
@@ -179,7 +179,7 @@ Interp-η
uint32_t x533, uint32_t x534 = mulx_u32(x524, 0xffffffff);
uint32_t x536, uint32_t x537 = mulx_u32(x524, 0xffffffff);
uint32_t x539, uint32_t x540 = mulx_u32(x524, 0xffffffff);
- uint32_t x542, uint8_t x543 = (uint8_t)mulx_u32(x524, 0x1f);
+ uint32_t x542, uint8_t x543 = mulx_u32_out_u8(x524, 0x1f);
uint32_t x545, uint8_t x546 = addcarryx_u32(0x0, x528, x530);
uint32_t x548, uint8_t x549 = addcarryx_u32(x546, x531, x533);
uint32_t x551, uint8_t x552 = addcarryx_u32(x549, x534, x536);
@@ -219,7 +219,7 @@ Interp-η
uint32_t x649, uint32_t x650 = mulx_u32(x640, 0xffffffff);
uint32_t x652, uint32_t x653 = mulx_u32(x640, 0xffffffff);
uint32_t x655, uint32_t x656 = mulx_u32(x640, 0xffffffff);
- uint32_t x658, uint8_t x659 = (uint8_t)mulx_u32(x640, 0x1f);
+ uint32_t x658, uint8_t x659 = mulx_u32_out_u8(x640, 0x1f);
uint32_t x661, uint8_t x662 = addcarryx_u32(0x0, x644, x646);
uint32_t x664, uint8_t x665 = addcarryx_u32(x662, x647, x649);
uint32_t x667, uint8_t x668 = addcarryx_u32(x665, x650, x652);
diff --git a/src/Specific/montgomery32_2e166m5/femulDisplay.log b/src/Specific/montgomery32_2e166m5/femulDisplay.log
index 349e64a9d..a26de0769 100644
--- a/src/Specific/montgomery32_2e166m5/femulDisplay.log
+++ b/src/Specific/montgomery32_2e166m5/femulDisplay.log
@@ -20,7 +20,7 @@ Interp-η
uint32_t x70, uint32_t x71 = mulx_u32(x61, 0xffffffff);
uint32_t x73, uint32_t x74 = mulx_u32(x61, 0xffffffff);
uint32_t x76, uint32_t x77 = mulx_u32(x61, 0xffffffff);
- uint32_t x79, uint8_t x80 = (uint8_t)mulx_u32(x61, 0x3f);
+ uint32_t x79, uint8_t x80 = mulx_u32_out_u8(x61, 0x3f);
uint32_t x82, uint8_t x83 = addcarryx_u32(0x0, x65, x67);
uint32_t x85, uint8_t x86 = addcarryx_u32(x83, x68, x70);
uint32_t x88, uint8_t x89 = addcarryx_u32(x86, x71, x73);
@@ -59,7 +59,7 @@ Interp-η
uint32_t x185, uint32_t x186 = mulx_u32(x176, 0xffffffff);
uint32_t x188, uint32_t x189 = mulx_u32(x176, 0xffffffff);
uint32_t x191, uint32_t x192 = mulx_u32(x176, 0xffffffff);
- uint32_t x194, uint8_t x195 = (uint8_t)mulx_u32(x176, 0x3f);
+ uint32_t x194, uint8_t x195 = mulx_u32_out_u8(x176, 0x3f);
uint32_t x197, uint8_t x198 = addcarryx_u32(0x0, x180, x182);
uint32_t x200, uint8_t x201 = addcarryx_u32(x198, x183, x185);
uint32_t x203, uint8_t x204 = addcarryx_u32(x201, x186, x188);
@@ -99,7 +99,7 @@ Interp-η
uint32_t x301, uint32_t x302 = mulx_u32(x292, 0xffffffff);
uint32_t x304, uint32_t x305 = mulx_u32(x292, 0xffffffff);
uint32_t x307, uint32_t x308 = mulx_u32(x292, 0xffffffff);
- uint32_t x310, uint8_t x311 = (uint8_t)mulx_u32(x292, 0x3f);
+ uint32_t x310, uint8_t x311 = mulx_u32_out_u8(x292, 0x3f);
uint32_t x313, uint8_t x314 = addcarryx_u32(0x0, x296, x298);
uint32_t x316, uint8_t x317 = addcarryx_u32(x314, x299, x301);
uint32_t x319, uint8_t x320 = addcarryx_u32(x317, x302, x304);
@@ -139,7 +139,7 @@ Interp-η
uint32_t x417, uint32_t x418 = mulx_u32(x408, 0xffffffff);
uint32_t x420, uint32_t x421 = mulx_u32(x408, 0xffffffff);
uint32_t x423, uint32_t x424 = mulx_u32(x408, 0xffffffff);
- uint32_t x426, uint8_t x427 = (uint8_t)mulx_u32(x408, 0x3f);
+ uint32_t x426, uint8_t x427 = mulx_u32_out_u8(x408, 0x3f);
uint32_t x429, uint8_t x430 = addcarryx_u32(0x0, x412, x414);
uint32_t x432, uint8_t x433 = addcarryx_u32(x430, x415, x417);
uint32_t x435, uint8_t x436 = addcarryx_u32(x433, x418, x420);
@@ -179,7 +179,7 @@ Interp-η
uint32_t x533, uint32_t x534 = mulx_u32(x524, 0xffffffff);
uint32_t x536, uint32_t x537 = mulx_u32(x524, 0xffffffff);
uint32_t x539, uint32_t x540 = mulx_u32(x524, 0xffffffff);
- uint32_t x542, uint8_t x543 = (uint8_t)mulx_u32(x524, 0x3f);
+ uint32_t x542, uint8_t x543 = mulx_u32_out_u8(x524, 0x3f);
uint32_t x545, uint8_t x546 = addcarryx_u32(0x0, x528, x530);
uint32_t x548, uint8_t x549 = addcarryx_u32(x546, x531, x533);
uint32_t x551, uint8_t x552 = addcarryx_u32(x549, x534, x536);
@@ -219,7 +219,7 @@ Interp-η
uint32_t x649, uint32_t x650 = mulx_u32(x640, 0xffffffff);
uint32_t x652, uint32_t x653 = mulx_u32(x640, 0xffffffff);
uint32_t x655, uint32_t x656 = mulx_u32(x640, 0xffffffff);
- uint32_t x658, uint8_t x659 = (uint8_t)mulx_u32(x640, 0x3f);
+ uint32_t x658, uint8_t x659 = mulx_u32_out_u8(x640, 0x3f);
uint32_t x661, uint8_t x662 = addcarryx_u32(0x0, x644, x646);
uint32_t x664, uint8_t x665 = addcarryx_u32(x662, x647, x649);
uint32_t x667, uint8_t x668 = addcarryx_u32(x665, x650, x652);
diff --git a/src/Specific/montgomery64_2e130m5/femul.c b/src/Specific/montgomery64_2e130m5/femul.c
index 9d8a8a50f..90e702349 100644
--- a/src/Specific/montgomery64_2e130m5/femul.c
+++ b/src/Specific/montgomery64_2e130m5/femul.c
@@ -14,7 +14,7 @@ static void femul(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3])
{ uint64_t _; uint64_t x31 = _mulx_u64(x13, 0xcccccccccccccccdL, &_);
{ uint64_t x35; uint64_t x34 = _mulx_u64(x31, 0xfffffffffffffffbL, &x35);
{ uint64_t x38; uint64_t x37 = _mulx_u64(x31, 0xffffffffffffffffL, &x38);
- { uint8_t x41; uint64_t x40 = (uint8_t)_mulx_u64(x31, 0x3, &x41);
+ { uint8_t x41; uint64_t x40 = _mulx_u64_out_u8(x31, 0x3, &x41);
{ uint64_t x43; uint8_t x44 = _addcarryx_u64(0x0, x35, x37, &x43);
{ uint64_t x46; uint8_t x47 = _addcarryx_u64(x44, x38, x40, &x46);
{ uint8_t x48 = (x47 + x41);
@@ -35,7 +35,7 @@ static void femul(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3])
{ uint64_t _; uint64_t x92 = _mulx_u64(x80, 0xcccccccccccccccdL, &_);
{ uint64_t x96; uint64_t x95 = _mulx_u64(x92, 0xfffffffffffffffbL, &x96);
{ uint64_t x99; uint64_t x98 = _mulx_u64(x92, 0xffffffffffffffffL, &x99);
- { uint8_t x102; uint64_t x101 = (uint8_t)_mulx_u64(x92, 0x3, &x102);
+ { uint8_t x102; uint64_t x101 = _mulx_u64_out_u8(x92, 0x3, &x102);
{ uint64_t x104; uint8_t x105 = _addcarryx_u64(0x0, x96, x98, &x104);
{ uint64_t x107; uint8_t x108 = _addcarryx_u64(x105, x99, x101, &x107);
{ uint8_t x109 = (x108 + x102);
@@ -57,7 +57,7 @@ static void femul(uint64_t out[3], const uint64_t in1[3], const uint64_t in2[3])
{ uint64_t _; uint64_t x154 = _mulx_u64(x142, 0xcccccccccccccccdL, &_);
{ uint64_t x158; uint64_t x157 = _mulx_u64(x154, 0xfffffffffffffffbL, &x158);
{ uint64_t x161; uint64_t x160 = _mulx_u64(x154, 0xffffffffffffffffL, &x161);
- { uint8_t x164; uint64_t x163 = (uint8_t)_mulx_u64(x154, 0x3, &x164);
+ { uint8_t x164; uint64_t x163 = _mulx_u64_out_u8(x154, 0x3, &x164);
{ uint64_t x166; uint8_t x167 = _addcarryx_u64(0x0, x158, x160, &x166);
{ uint64_t x169; uint8_t x170 = _addcarryx_u64(x167, x161, x163, &x169);
{ uint8_t x171 = (x170 + x164);
diff --git a/src/Specific/montgomery64_2e130m5/femulDisplay.log b/src/Specific/montgomery64_2e130m5/femulDisplay.log
index d232d59bb..fd9b3aba5 100644
--- a/src/Specific/montgomery64_2e130m5/femulDisplay.log
+++ b/src/Specific/montgomery64_2e130m5/femulDisplay.log
@@ -11,7 +11,7 @@ Interp-η
uint64_t x31, uint64_t _ = mulx_u64(x13, 0xcccccccccccccccdL);
uint64_t x34, uint64_t x35 = mulx_u64(x31, 0xfffffffffffffffbL);
uint64_t x37, uint64_t x38 = mulx_u64(x31, 0xffffffffffffffffL);
- uint64_t x40, uint8_t x41 = (uint8_t)mulx_u64(x31, 0x3);
+ uint64_t x40, uint8_t x41 = mulx_u64_out_u8(x31, 0x3);
uint64_t x43, uint8_t x44 = addcarryx_u64(0x0, x35, x37);
uint64_t x46, uint8_t x47 = addcarryx_u64(x44, x38, x40);
uint8_t x48 = (x47 + x41);
@@ -32,7 +32,7 @@ Interp-η
uint64_t x92, uint64_t _ = mulx_u64(x80, 0xcccccccccccccccdL);
uint64_t x95, uint64_t x96 = mulx_u64(x92, 0xfffffffffffffffbL);
uint64_t x98, uint64_t x99 = mulx_u64(x92, 0xffffffffffffffffL);
- uint64_t x101, uint8_t x102 = (uint8_t)mulx_u64(x92, 0x3);
+ uint64_t x101, uint8_t x102 = mulx_u64_out_u8(x92, 0x3);
uint64_t x104, uint8_t x105 = addcarryx_u64(0x0, x96, x98);
uint64_t x107, uint8_t x108 = addcarryx_u64(x105, x99, x101);
uint8_t x109 = (x108 + x102);
@@ -54,7 +54,7 @@ Interp-η
uint64_t x154, uint64_t _ = mulx_u64(x142, 0xcccccccccccccccdL);
uint64_t x157, uint64_t x158 = mulx_u64(x154, 0xfffffffffffffffbL);
uint64_t x160, uint64_t x161 = mulx_u64(x154, 0xffffffffffffffffL);
- uint64_t x163, uint8_t x164 = (uint8_t)mulx_u64(x154, 0x3);
+ uint64_t x163, uint8_t x164 = mulx_u64_out_u8(x154, 0x3);
uint64_t x166, uint8_t x167 = addcarryx_u64(0x0, x158, x160);
uint64_t x169, uint8_t x170 = addcarryx_u64(x167, x161, x163);
uint8_t x171 = (x170 + x164);
diff --git a/src/Specific/solinas32_2e510m290x2e496m1/fesubDisplay.log b/src/Specific/solinas32_2e510m290x2e496m1/fesubDisplay.log
index 079973512..318927f69 100644
--- a/src/Specific/solinas32_2e510m290x2e496m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e510m290x2e496m1/fesubDisplay.log
@@ -2,6 +2,6 @@
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x48, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x94, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53, x51))%core,
- (((Const 4120062 + x48) - x94), ((0x3ffffe + x49) - x95), ((0x3ffffe + x47) - x93), ((0x7ffffe + x45) - x91), ((0x3ffffe + x43) - x89), ((0x3ffffe + x41) - x87), ((0x3ffffe + x39) - x85), ((0x7ffffe + x37) - x83), ((0x3ffffe + x35) - x81), ((0x3ffffe + x33) - x79), ((0x3ffffe + x31) - x77), ((0x7ffffe + x29) - x75), ((0x3ffffe + x27) - x73), ((0x3ffffe + x25) - x71), ((0x3ffffe + x23) - x69), ((0x7ffffe + x21) - x67), ((0x3ffffe + x19) - x65), ((0x3ffffe + x17) - x63), ((0x3ffffe + x15) - x61), ((0x7ffffe + x13) - x59), ((0x3ffffe + x11) - x57), ((0x3ffffe + x9) - x55), ((0x3ffffe + x7) - x53), ((0x7ffffe + x5) - x51)))
+ (((0x3eddfe + x48) - x94), ((0x3ffffe + x49) - x95), ((0x3ffffe + x47) - x93), ((0x7ffffe + x45) - x91), ((0x3ffffe + x43) - x89), ((0x3ffffe + x41) - x87), ((0x3ffffe + x39) - x85), ((0x7ffffe + x37) - x83), ((0x3ffffe + x35) - x81), ((0x3ffffe + x33) - x79), ((0x3ffffe + x31) - x77), ((0x7ffffe + x29) - x75), ((0x3ffffe + x27) - x73), ((0x3ffffe + x25) - x71), ((0x3ffffe + x23) - x69), ((0x7ffffe + x21) - x67), ((0x3ffffe + x19) - x65), ((0x3ffffe + x17) - x63), ((0x3ffffe + x15) - x61), ((0x7ffffe + x13) - x59), ((0x3ffffe + x11) - x57), ((0x3ffffe + x9) - x55), ((0x3ffffe + x7) - x53), ((0x7ffffe + x5) - x51)))
(x, x0)%core
: word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
diff --git a/src/Specific/solinas32_2e512m491x2e496m1/fesubDisplay.log b/src/Specific/solinas32_2e512m491x2e496m1/fesubDisplay.log
index 6290cc5b7..70d35506c 100644
--- a/src/Specific/solinas32_2e512m491x2e496m1/fesubDisplay.log
+++ b/src/Specific/solinas32_2e512m491x2e496m1/fesubDisplay.log
@@ -2,6 +2,6 @@
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x48, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x94, x95, x93, x91, x89, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53, x51))%core,
- (((Const 4162878 + x48) - x94), ((0x3ffffe + x49) - x95), ((0x7ffffe + x47) - x93), ((0x3ffffe + x45) - x91), ((0x3ffffe + x43) - x89), ((0x7ffffe + x41) - x87), ((0x3ffffe + x39) - x85), ((0x3ffffe + x37) - x83), ((0x7ffffe + x35) - x81), ((0x3ffffe + x33) - x79), ((0x3ffffe + x31) - x77), ((0x7ffffe + x29) - x75), ((0x3ffffe + x27) - x73), ((0x3ffffe + x25) - x71), ((0x7ffffe + x23) - x69), ((0x3ffffe + x21) - x67), ((0x3ffffe + x19) - x65), ((0x7ffffe + x17) - x63), ((0x3ffffe + x15) - x61), ((0x3ffffe + x13) - x59), ((0x7ffffe + x11) - x57), ((0x3ffffe + x9) - x55), ((0x3ffffe + x7) - x53), ((0x7ffffe + x5) - x51)))
+ (((0x3f853e + x48) - x94), ((0x3ffffe + x49) - x95), ((0x7ffffe + x47) - x93), ((0x3ffffe + x45) - x91), ((0x3ffffe + x43) - x89), ((0x7ffffe + x41) - x87), ((0x3ffffe + x39) - x85), ((0x3ffffe + x37) - x83), ((0x7ffffe + x35) - x81), ((0x3ffffe + x33) - x79), ((0x3ffffe + x31) - x77), ((0x7ffffe + x29) - x75), ((0x3ffffe + x27) - x73), ((0x3ffffe + x25) - x71), ((0x7ffffe + x23) - x69), ((0x3ffffe + x21) - x67), ((0x3ffffe + x19) - x65), ((0x7ffffe + x17) - x63), ((0x3ffffe + x15) - x61), ((0x3ffffe + x13) - x59), ((0x7ffffe + x11) - x57), ((0x3ffffe + x9) - x55), ((0x3ffffe + x7) - x53), ((0x7ffffe + x5) - x51)))
(x, x0)%core
: word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)