diff options
Diffstat (limited to 'src/Specific')
27 files changed, 27 insertions, 27 deletions
diff --git a/src/Specific/solinas32_2e127m1/fesubDisplay.log b/src/Specific/solinas32_2e127m1/fesubDisplay.log index c2631a75b..6727bf155 100644 --- a/src/Specific/solinas32_2e127m1/fesubDisplay.log +++ b/src/Specific/solinas32_2e127m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((Const 4194302 + x12) - x22), ((Const 4194302 + x13) - x23), ((Const 4194302 + x11) - x21), ((Const 4194302 + x9) - x19), ((Const 4194302 + x7) - x17), ((0x7ffffe + x5) - x15))) + (((0x3ffffe + x12) - x22), ((0x3ffffe + x13) - x23), ((0x3ffffe + x11) - x21), ((0x3ffffe + x9) - x19), ((0x3ffffe + x7) - x17), ((0x7ffffe + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e129m25/fesubDisplay.log b/src/Specific/solinas32_2e129m25/fesubDisplay.log index 139dee9ce..8a85dcd49 100644 --- a/src/Specific/solinas32_2e129m25/fesubDisplay.log +++ b/src/Specific/solinas32_2e129m25/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((Const 4194302 + x12) - x22), ((0x7ffffe + x13) - x23), ((Const 4194302 + x11) - x21), ((0x7ffffe + x9) - x19), ((Const 4194302 + x7) - x17), ((Const 8388558 + x5) - x15))) + (((0x3ffffe + x12) - x22), ((0x7ffffe + x13) - x23), ((0x3ffffe + x11) - x21), ((0x7ffffe + x9) - x19), ((0x3ffffe + x7) - x17), ((0x7fffce + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e140m27/fesubDisplay.log b/src/Specific/solinas32_2e140m27/fesubDisplay.log index 1afdbb9f6..3dc0cee98 100644 --- a/src/Specific/solinas32_2e140m27/fesubDisplay.log +++ b/src/Specific/solinas32_2e140m27/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((Const 16777214 + x12) - x22), ((Const 16777214 + x13) - x23), ((Const 33554430 + x11) - x21), ((Const 16777214 + x9) - x19), ((Const 16777214 + x7) - x17), ((Const 33554378 + x5) - x15))) + (((0xfffffe + x12) - x22), ((0xfffffe + x13) - x23), ((0x1fffffe + x11) - x21), ((0xfffffe + x9) - x19), ((0xfffffe + x7) - x17), ((0x1ffffca + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e141m9/fesubDisplay.log b/src/Specific/solinas32_2e141m9/fesubDisplay.log index 053034964..45d58a6d4 100644 --- a/src/Specific/solinas32_2e141m9/fesubDisplay.log +++ b/src/Specific/solinas32_2e141m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((Const 16777214 + x12) - x22), ((Const 33554430 + x13) - x23), ((Const 16777214 + x11) - x21), ((Const 33554430 + x9) - x19), ((Const 16777214 + x7) - x17), ((Const 33554414 + x5) - x15))) + (((0xfffffe + x12) - x22), ((0x1fffffe + x13) - x23), ((0xfffffe + x11) - x21), ((0x1fffffe + x9) - x19), ((0xfffffe + x7) - x17), ((0x1ffffee + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e150m5/fesubDisplay.log b/src/Specific/solinas32_2e150m5/fesubDisplay.log index e59bfd721..1229647ea 100644 --- a/src/Specific/solinas32_2e150m5/fesubDisplay.log +++ b/src/Specific/solinas32_2e150m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x3fffffe + x12) - x22), ((0x3fffffe + x13) - x23), ((0x3fffffe + x11) - x21), ((0x3fffffe + x9) - x19), ((0x3fffffe + x7) - x17), ((Const 67108854 + x5) - x15))) + (((0x3fffffe + x12) - x22), ((0x3fffffe + x13) - x23), ((0x3fffffe + x11) - x21), ((0x3fffffe + x9) - x19), ((0x3fffffe + x7) - x17), ((0x3fffff6 + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e152m17/fesubDisplay.log b/src/Specific/solinas32_2e152m17/fesubDisplay.log index 8b374243d..535c511cc 100644 --- a/src/Specific/solinas32_2e152m17/fesubDisplay.log +++ b/src/Specific/solinas32_2e152m17/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x3fffffe + x12) - x22), ((0x3fffffe + x13) - x23), ((0x7fffffe + x11) - x21), ((0x3fffffe + x9) - x19), ((0x3fffffe + x7) - x17), ((Const 134217694 + x5) - x15))) + (((0x3fffffe + x12) - x22), ((0x3fffffe + x13) - x23), ((0x7fffffe + x11) - x21), ((0x3fffffe + x9) - x19), ((0x3fffffe + x7) - x17), ((0x7ffffde + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e158m15/fesubDisplay.log b/src/Specific/solinas32_2e158m15/fesubDisplay.log index f3bdb7577..284622c58 100644 --- a/src/Specific/solinas32_2e158m15/fesubDisplay.log +++ b/src/Specific/solinas32_2e158m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x7fffffe + x12) - x22), ((0x7fffffe + x13) - x23), ((0xffffffe + x11) - x21), ((0x7fffffe + x9) - x19), ((0x7fffffe + x7) - x17), ((Const 268435426 + x5) - x15))) + (((0x7fffffe + x12) - x22), ((0x7fffffe + x13) - x23), ((0xffffffe + x11) - x21), ((0x7fffffe + x9) - x19), ((0x7fffffe + x7) - x17), ((0xfffffe2 + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e174m3/fesubDisplay.log b/src/Specific/solinas32_2e174m3/fesubDisplay.log index 40a761b7b..1299dc361 100644 --- a/src/Specific/solinas32_2e174m3/fesubDisplay.log +++ b/src/Specific/solinas32_2e174m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x3ffffffe + x12) - x22), ((0x3ffffffe + x13) - x23), ((0x3ffffffe + x11) - x21), ((0x3ffffffe + x9) - x19), ((0x3ffffffe + x7) - x17), ((Const 1073741818 + x5) - x15))) + (((0x3ffffffe + x12) - x22), ((0x3ffffffe + x13) - x23), ((0x3ffffffe + x11) - x21), ((0x3ffffffe + x9) - x19), ((0x3ffffffe + x7) - x17), ((0x3ffffffa + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e189m25/fesubDisplay.log b/src/Specific/solinas32_2e189m25/fesubDisplay.log index 80cf383c7..74fbc0216 100644 --- a/src/Specific/solinas32_2e189m25/fesubDisplay.log +++ b/src/Specific/solinas32_2e189m25/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((0xffffffe + x14) - x26), ((0xffffffe + x15) - x27), ((0xffffffe + x13) - x25), ((0xffffffe + x11) - x23), ((0xffffffe + x9) - x21), ((0xffffffe + x7) - x19), ((Const 268435406 + x5) - x17))) + (((0xffffffe + x14) - x26), ((0xffffffe + x15) - x27), ((0xffffffe + x13) - x25), ((0xffffffe + x11) - x23), ((0xffffffe + x9) - x21), ((0xffffffe + x7) - x19), ((0xfffffce + x5) - x17))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e190m11/fesubDisplay.log b/src/Specific/solinas32_2e190m11/fesubDisplay.log index fc8c57a6c..e7a7f3328 100644 --- a/src/Specific/solinas32_2e190m11/fesubDisplay.log +++ b/src/Specific/solinas32_2e190m11/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((0xffffffe + x14) - x26), ((0xffffffe + x15) - x27), ((0xffffffe + x13) - x25), ((0xffffffe + x11) - x23), ((0xffffffe + x9) - x21), ((0xffffffe + x7) - x19), ((Const 536870890 + x5) - x17))) + (((0xffffffe + x14) - x26), ((0xffffffe + x15) - x27), ((0xffffffe + x13) - x25), ((0xffffffe + x11) - x23), ((0xffffffe + x9) - x21), ((0xffffffe + x7) - x19), ((0x1fffffea + x5) - x17))) (x, x0)%core : 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) diff --git a/src/Specific/solinas32_2e196m15/fesubDisplay.log b/src/Specific/solinas32_2e196m15/fesubDisplay.log index 08d064a06..eaf509e2c 100644 --- a/src/Specific/solinas32_2e196m15/fesubDisplay.log +++ b/src/Specific/solinas32_2e196m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((0x1ffffffe + x14) - x26), ((0x1ffffffe + x15) - x27), ((0x1ffffffe + x13) - x25), ((0x1ffffffe + x11) - x23), ((0x1ffffffe + x9) - x21), ((0x1ffffffe + x7) - x19), ((Const 536870882 + x5) - x17))) + (((0x1ffffffe + x14) - x26), ((0x1ffffffe + x15) - x27), ((0x1ffffffe + x13) - x25), ((0x1ffffffe + x11) - x23), ((0x1ffffffe + x9) - x21), ((0x1ffffffe + x7) - x19), ((0x1fffffe2 + x5) - x17))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e235m15/fesubDisplay.log b/src/Specific/solinas64_2e235m15/fesubDisplay.log index b269eef28..9d33fa7c5 100644 --- a/src/Specific/solinas64_2e235m15/fesubDisplay.log +++ b/src/Specific/solinas64_2e235m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0xfffffffffffe + x10) - x18), ((0xfffffffffffe + x11) - x19), ((0xfffffffffffe + x9) - x17), ((0xfffffffffffe + x7) - x15), ((Const 281474976710626 + x5) - x13))) + (((0xfffffffffffe + x10) - x18), ((0xfffffffffffe + x11) - x19), ((0xfffffffffffe + x9) - x17), ((0xfffffffffffe + x7) - x15), ((0xffffffffffe2 + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e243m9/fesubDisplay.log b/src/Specific/solinas64_2e243m9/fesubDisplay.log index 4b7921d1f..22e0778d0 100644 --- a/src/Specific/solinas64_2e243m9/fesubDisplay.log +++ b/src/Specific/solinas64_2e243m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x1fffffffffe + x12) - x22), ((Const 4398046511102 + x13) - x23), ((0x1fffffffffe + x11) - x21), ((Const 4398046511102 + x9) - x19), ((0x1fffffffffe + x7) - x17), ((Const 4398046511086 + x5) - x15))) + (((0x1fffffffffe + x12) - x22), ((0x3fffffffffe + x13) - x23), ((0x1fffffffffe + x11) - x21), ((0x3fffffffffe + x9) - x19), ((0x1fffffffffe + x7) - x17), ((0x3ffffffffee + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e251m9/fesubDisplay.log b/src/Specific/solinas64_2e251m9/fesubDisplay.log index 2e4cdca46..4c7bb5bfc 100644 --- a/src/Specific/solinas64_2e251m9/fesubDisplay.log +++ b/src/Specific/solinas64_2e251m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0x7fffffffffffe + x10) - x18), ((0x7fffffffffffe + x11) - x19), ((0x7fffffffffffe + x9) - x17), ((0x7fffffffffffe + x7) - x15), ((Const 4503599627370478 + x5) - x13))) + (((0x7fffffffffffe + x10) - x18), ((0x7fffffffffffe + x11) - x19), ((0x7fffffffffffe + x9) - x17), ((0x7fffffffffffe + x7) - x15), ((0xfffffffffffee + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e254m127x2e240m1/fesubDisplay.log b/src/Specific/solinas64_2e254m127x2e240m1/fesubDisplay.log index 6fec626b1..4ea659b58 100644 --- a/src/Specific/solinas64_2e254m127x2e240m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e254m127x2e240m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((Const 8727910416382 + x12) - x22), ((0x7fffffffffe + x13) - x23), ((0xffffffffffe + x11) - x21), ((0x7fffffffffe + x9) - x19), ((0x7fffffffffe + x7) - x17), ((0xffffffffffe + x5) - x15))) + (((0x7f01ffffffe + x12) - x22), ((0x7fffffffffe + x13) - x23), ((0xffffffffffe + x11) - x21), ((0x7fffffffffe + x9) - x19), ((0x7fffffffffe + x7) - x17), ((0xffffffffffe + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e255m765/fesubDisplay.log b/src/Specific/solinas64_2e255m765/fesubDisplay.log index 24c1fae40..9de59caff 100644 --- a/src/Specific/solinas64_2e255m765/fesubDisplay.log +++ b/src/Specific/solinas64_2e255m765/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((Const 4503599627368966 + x5) - x13))) + (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0xffffffffffa06 + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e256m189/fesubDisplay.log b/src/Specific/solinas64_2e256m189/fesubDisplay.log index 60812c170..7089f9abe 100644 --- a/src/Specific/solinas64_2e256m189/fesubDisplay.log +++ b/src/Specific/solinas64_2e256m189/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((Const 9007199254740614 + x5) - x13))) + (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0x1ffffffffffe86 + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e256m2e32m977/fesubDisplay.log b/src/Specific/solinas64_2e256m2e32m977/fesubDisplay.log index 619189843..993f8132c 100644 --- a/src/Specific/solinas64_2e256m2e32m977/fesubDisplay.log +++ b/src/Specific/solinas64_2e256m2e32m977/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((Const 9007190664804446 + x5) - x13))) + (((0xffffffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0x1ffffdfffff85e + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e256m88x2e240m1/fesubDisplay.log b/src/Specific/solinas64_2e256m88x2e240m1/fesubDisplay.log index 839d41e5a..1c0daea96 100644 --- a/src/Specific/solinas64_2e256m88x2e240m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e256m88x2e240m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((Const 4497552313417726 + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0x1ffffffffffffe + x5) - x13))) + (((0xffa7ffffffffe + x10) - x18), ((0xffffffffffffe + x11) - x19), ((0xffffffffffffe + x9) - x17), ((0xffffffffffffe + x7) - x15), ((0x1ffffffffffffe + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e285m9/fesubDisplay.log b/src/Specific/solinas64_2e285m9/fesubDisplay.log index a4a4ca458..4afd8dcc0 100644 --- a/src/Specific/solinas64_2e285m9/fesubDisplay.log +++ b/src/Specific/solinas64_2e285m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0x3fffffffffffffe + x10) - x18), ((0x3fffffffffffffe + x11) - x19), ((0x3fffffffffffffe + x9) - x17), ((0x3fffffffffffffe + x7) - x15), ((Const 288230376151711726 + x5) - x13))) + (((0x3fffffffffffffe + x10) - x18), ((0x3fffffffffffffe + x11) - x19), ((0x3fffffffffffffe + x9) - x17), ((0x3fffffffffffffe + x7) - x15), ((0x3ffffffffffffee + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e291m19/fesubDisplay.log b/src/Specific/solinas64_2e291m19/fesubDisplay.log index f18eddc6b..a5ea892fa 100644 --- a/src/Specific/solinas64_2e291m19/fesubDisplay.log +++ b/src/Specific/solinas64_2e291m19/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0x7fffffffffffffe + x10) - x18), ((0x7fffffffffffffe + x11) - x19), ((0x7fffffffffffffe + x9) - x17), ((0x7fffffffffffffe + x7) - x15), ((Const 1152921504606846938 + x5) - x13))) + (((0x7fffffffffffffe + x10) - x18), ((0x7fffffffffffffe + x11) - x19), ((0x7fffffffffffffe + x9) - x17), ((0x7fffffffffffffe + x7) - x15), ((0xfffffffffffffda + x5) - x13))) (x, x0)%core : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e321m9/fesubDisplay.log b/src/Specific/solinas64_2e321m9/fesubDisplay.log index 24f164c51..4d9559435 100644 --- a/src/Specific/solinas64_2e321m9/fesubDisplay.log +++ b/src/Specific/solinas64_2e321m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x3ffffffffffffe + x12) - x22), ((0x7ffffffffffffe + x13) - x23), ((0x3ffffffffffffe + x11) - x21), ((0x7ffffffffffffe + x9) - x19), ((0x3ffffffffffffe + x7) - x17), ((Const 36028797018963950 + x5) - x15))) + (((0x3ffffffffffffe + x12) - x22), ((0x7ffffffffffffe + x13) - x23), ((0x3ffffffffffffe + x11) - x21), ((0x7ffffffffffffe + x9) - x19), ((0x3ffffffffffffe + x7) - x17), ((0x7fffffffffffee + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e322m2e161m1/fesubDisplay.log b/src/Specific/solinas64_2e322m2e161m1/fesubDisplay.log index 4a32c7db8..9d6ff5060 100644 --- a/src/Specific/solinas64_2e322m2e161m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e322m2e161m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((Const 140737488355326 + x14) - x26), ((Const 140737488355326 + x15) - x27), ((Const 140737488355326 + x13) - x25), ((Const 140737471578110 + x11) - x23), ((Const 140737488355326 + x9) - x21), ((Const 140737488355326 + x7) - x19), ((Const 140737488355326 + x5) - x17))) + (((0x7ffffffffffe + x14) - x26), ((0x7ffffffffffe + x15) - x27), ((0x7ffffffffffe + x13) - x25), ((0x7ffffefffffe + x11) - x23), ((0x7ffffffffffe + x9) - x21), ((0x7ffffffffffe + x7) - x19), ((0x7ffffffffffe + x5) - x17))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e336m17/fesubDisplay.log b/src/Specific/solinas64_2e336m17/fesubDisplay.log index 8d8952b0a..6df841701 100644 --- a/src/Specific/solinas64_2e336m17/fesubDisplay.log +++ b/src/Specific/solinas64_2e336m17/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x1fffffffffffffe + x12) - x22), ((0x1fffffffffffffe + x13) - x23), ((0x1fffffffffffffe + x11) - x21), ((0x1fffffffffffffe + x9) - x19), ((0x1fffffffffffffe + x7) - x17), ((Const 144115188075855838 + x5) - x15))) + (((0x1fffffffffffffe + x12) - x22), ((0x1fffffffffffffe + x13) - x23), ((0x1fffffffffffffe + x11) - x21), ((0x1fffffffffffffe + x9) - x19), ((0x1fffffffffffffe + x7) - x17), ((0x1ffffffffffffde + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e338m15/fesubDisplay.log b/src/Specific/solinas64_2e338m15/fesubDisplay.log index 7a96b6e0f..9eb96c91d 100644 --- a/src/Specific/solinas64_2e338m15/fesubDisplay.log +++ b/src/Specific/solinas64_2e338m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x12, x13, x11, x9, x7, x5, (x22, x23, x21, x19, x17, x15))%core, - (((0x1fffffffffffffe + x12) - x22), ((0x1fffffffffffffe + x13) - x23), ((0x3fffffffffffffe + x11) - x21), ((0x1fffffffffffffe + x9) - x19), ((0x1fffffffffffffe + x7) - x17), ((Const 288230376151711714 + x5) - x15))) + (((0x1fffffffffffffe + x12) - x22), ((0x1fffffffffffffe + x13) - x23), ((0x3fffffffffffffe + x11) - x21), ((0x1fffffffffffffe + x9) - x19), ((0x1fffffffffffffe + x7) - x17), ((0x3ffffffffffffe2 + x5) - x15))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e379m19/fesubDisplay.log b/src/Specific/solinas64_2e379m19/fesubDisplay.log index 813167313..30992c3d8 100644 --- a/src/Specific/solinas64_2e379m19/fesubDisplay.log +++ b/src/Specific/solinas64_2e379m19/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((0x7ffffffffffffe + x14) - x26), ((0x7ffffffffffffe + x15) - x27), ((0x7ffffffffffffe + x13) - x25), ((0x7ffffffffffffe + x11) - x23), ((0x7ffffffffffffe + x9) - x21), ((0x7ffffffffffffe + x7) - x19), ((Const 72057594037927898 + x5) - x17))) + (((0x7ffffffffffffe + x14) - x26), ((0x7ffffffffffffe + x15) - x27), ((0x7ffffffffffffe + x13) - x25), ((0x7ffffffffffffe + x11) - x23), ((0x7ffffffffffffe + x9) - x21), ((0x7ffffffffffffe + x7) - x19), ((0xffffffffffffda + x5) - x17))) (x, x0)%core : 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) diff --git a/src/Specific/solinas64_2e413m21/fesubDisplay.log b/src/Specific/solinas64_2e413m21/fesubDisplay.log index 676193cfe..ebf049655 100644 --- a/src/Specific/solinas64_2e413m21/fesubDisplay.log +++ b/src/Specific/solinas64_2e413m21/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x14, x15, x13, x11, x9, x7, x5, (x26, x27, x25, x23, x21, x19, x17))%core, - (((0xffffffffffffffe + x14) - x26), ((0xffffffffffffffe + x15) - x27), ((0xffffffffffffffe + x13) - x25), ((0xffffffffffffffe + x11) - x23), ((0xffffffffffffffe + x9) - x21), ((0xffffffffffffffe + x7) - x19), ((Const 1152921504606846934 + x5) - x17))) + (((0xffffffffffffffe + x14) - x26), ((0xffffffffffffffe + x15) - x27), ((0xffffffffffffffe + x13) - x25), ((0xffffffffffffffe + x11) - x23), ((0xffffffffffffffe + x9) - x21), ((0xffffffffffffffe + x7) - x19), ((0xfffffffffffffd6 + x5) - x17))) (x, x0)%core : 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) |