diff options
Diffstat (limited to 'src/Specific')
33 files changed, 33 insertions, 33 deletions
diff --git a/src/Specific/solinas32_2e130m5/fesubDisplay.log b/src/Specific/solinas32_2e130m5/fesubDisplay.log index f5e24bedf..1250af0b6 100644 --- a/src/Specific/solinas32_2e130m5/fesubDisplay.log +++ b/src/Specific/solinas32_2e130m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((0x7fffffe + x10) - x18), ((0x7fffffe + x11) - x19), ((0x7fffffe + x9) - x17), ((0x7fffffe + x7) - x15), ((Const 134217718 + x5) - x13))) + (((0x7fffffe + x10) - x18), ((0x7fffffe + x11) - x19), ((0x7fffffe + x9) - x17), ((0x7fffffe + x7) - x15), ((0x7fffff6 + x5) - x13))) (x, x0)%core : word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas32_2e150m3/fesubDisplay.log b/src/Specific/solinas32_2e150m3/fesubDisplay.log index 135560b1b..33ae90fdf 100644 --- a/src/Specific/solinas32_2e150m3/fesubDisplay.log +++ b/src/Specific/solinas32_2e150m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((Const 2147483646 + x10) - x18), ((Const 2147483646 + x11) - x19), ((Const 2147483646 + x9) - x17), ((Const 2147483646 + x7) - x15), ((Const 2147483642 + x5) - x13))) + (((0x7ffffffe + x10) - x18), ((0x7ffffffe + x11) - x19), ((0x7ffffffe + x9) - x17), ((0x7ffffffe + x7) - x15), ((0x7ffffffa + x5) - x13))) (x, x0)%core : word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t) diff --git a/src/Specific/solinas64_2e127m1/fesubDisplay.log b/src/Specific/solinas64_2e127m1/fesubDisplay.log index d75d25535..f9746a1ad 100644 --- a/src/Specific/solinas64_2e127m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e127m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 8796093022206 + x6) - x10), ((Const 8796093022206 + x7) - x11), ((Const 17592186044414 + x5) - x9))) + (((0x7fffffffffe + x6) - x10), ((0x7fffffffffe + x7) - x11), ((0xffffffffffe + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e129m25/fesubDisplay.log b/src/Specific/solinas64_2e129m25/fesubDisplay.log index 153df42c2..d5762eae8 100644 --- a/src/Specific/solinas64_2e129m25/fesubDisplay.log +++ b/src/Specific/solinas64_2e129m25/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 17592186044414 + x6) - x10), ((Const 17592186044414 + x7) - x11), ((Const 17592186044366 + x5) - x9))) + (((0xffffffffffe + x6) - x10), ((0xffffffffffe + x7) - x11), ((0xfffffffffce + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e130m5/fesubDisplay.log b/src/Specific/solinas64_2e130m5/fesubDisplay.log index 70a105f3a..3496fca22 100644 --- a/src/Specific/solinas64_2e130m5/fesubDisplay.log +++ b/src/Specific/solinas64_2e130m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 17592186044414 + x6) - x10), ((Const 17592186044414 + x7) - x11), ((Const 35184372088822 + x5) - x9))) + (((0xffffffffffe + x6) - x10), ((0xffffffffffe + x7) - x11), ((0x1ffffffffff6 + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e137m13/fesubDisplay.log b/src/Specific/solinas64_2e137m13/fesubDisplay.log index d6a451175..c007b2271 100644 --- a/src/Specific/solinas64_2e137m13/fesubDisplay.log +++ b/src/Specific/solinas64_2e137m13/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 34359738366 + x8) - x14), ((Const 34359738366 + x9) - x15), ((Const 34359738366 + x7) - x13), ((Const 68719476710 + x5) - x11))) + (((0x7fffffffe + x8) - x14), ((0x7fffffffe + x9) - x15), ((0x7fffffffe + x7) - x13), ((0xfffffffe6 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e140m27/fesubDisplay.log b/src/Specific/solinas64_2e140m27/fesubDisplay.log index e5ded268f..a4d489ec2 100644 --- a/src/Specific/solinas64_2e140m27/fesubDisplay.log +++ b/src/Specific/solinas64_2e140m27/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 68719476734 + x8) - x14), ((Const 68719476734 + x9) - x15), ((Const 68719476734 + x7) - x13), ((Const 68719476682 + x5) - x11))) + (((0xffffffffe + x8) - x14), ((0xffffffffe + x9) - x15), ((0xffffffffe + x7) - x13), ((0xfffffffca + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e141m9/fesubDisplay.log b/src/Specific/solinas64_2e141m9/fesubDisplay.log index b47ac81d4..18bf8250e 100644 --- a/src/Specific/solinas64_2e141m9/fesubDisplay.log +++ b/src/Specific/solinas64_2e141m9/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 281474976710654 + x6) - x10), ((Const 281474976710654 + x7) - x11), ((Const 281474976710638 + x5) - x9))) + (((0xfffffffffffe + x6) - x10), ((0xfffffffffffe + x7) - x11), ((0xffffffffffee + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e150m3/fesubDisplay.log b/src/Specific/solinas64_2e150m3/fesubDisplay.log index 8c977fe6b..5506e17af 100644 --- a/src/Specific/solinas64_2e150m3/fesubDisplay.log +++ b/src/Specific/solinas64_2e150m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 2251799813685246 + x6) - x10), ((Const 2251799813685246 + x7) - x11), ((Const 2251799813685242 + x5) - x9))) + (((0x7fffffffffffe + x6) - x10), ((0x7fffffffffffe + x7) - x11), ((0x7fffffffffffa + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e150m5/fesubDisplay.log b/src/Specific/solinas64_2e150m5/fesubDisplay.log index 2a6d10e3c..d4a7f1c68 100644 --- a/src/Specific/solinas64_2e150m5/fesubDisplay.log +++ b/src/Specific/solinas64_2e150m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 2251799813685246 + x6) - x10), ((Const 2251799813685246 + x7) - x11), ((Const 2251799813685238 + x5) - x9))) + (((0x7fffffffffffe + x6) - x10), ((0x7fffffffffffe + x7) - x11), ((0x7fffffffffff6 + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e152m17/fesubDisplay.log b/src/Specific/solinas64_2e152m17/fesubDisplay.log index fa8ed8270..7ab073e38 100644 --- a/src/Specific/solinas64_2e152m17/fesubDisplay.log +++ b/src/Specific/solinas64_2e152m17/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 549755813886 + x8) - x14), ((Const 549755813886 + x9) - x15), ((Const 549755813886 + x7) - x13), ((Const 549755813854 + x5) - x11))) + (((0x7ffffffffe + x8) - x14), ((0x7ffffffffe + x9) - x15), ((0x7ffffffffe + x7) - x13), ((0x7fffffffde + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e158m15/fesubDisplay.log b/src/Specific/solinas64_2e158m15/fesubDisplay.log index 28107c90f..3c4c7efb2 100644 --- a/src/Specific/solinas64_2e158m15/fesubDisplay.log +++ b/src/Specific/solinas64_2e158m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 1099511627774 + x8) - x14), ((Const 2199023255550 + x9) - x15), ((Const 1099511627774 + x7) - x13), ((Const 2199023255522 + x5) - x11))) + (((0xfffffffffe + x8) - x14), ((0x1fffffffffe + x9) - x15), ((0xfffffffffe + x7) - x13), ((0x1ffffffffe2 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e165m25/fesubDisplay.log b/src/Specific/solinas64_2e165m25/fesubDisplay.log index 09ed125f0..8e2ee812b 100644 --- a/src/Specific/solinas64_2e165m25/fesubDisplay.log +++ b/src/Specific/solinas64_2e165m25/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((0xfffffffffffffe + x6) - x10), ((0xfffffffffffffe + x7) - x11), ((Const 72057594037927886 + x5) - x9))) + (((0xfffffffffffffe + x6) - x10), ((0xfffffffffffffe + x7) - x11), ((0xffffffffffffce + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e166m5/fesubDisplay.log b/src/Specific/solinas64_2e166m5/fesubDisplay.log index 3a20d4dbf..3b42dfd84 100644 --- a/src/Specific/solinas64_2e166m5/fesubDisplay.log +++ b/src/Specific/solinas64_2e166m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((0xfffffffffffffe + x6) - x10), ((0xfffffffffffffe + x7) - x11), ((Const 144115188075855862 + x5) - x9))) + (((0xfffffffffffffe + x6) - x10), ((0xfffffffffffffe + x7) - x11), ((0x1fffffffffffff6 + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e171m19/fesubDisplay.log b/src/Specific/solinas64_2e171m19/fesubDisplay.log index a092985c8..c6120f7d9 100644 --- a/src/Specific/solinas64_2e171m19/fesubDisplay.log +++ b/src/Specific/solinas64_2e171m19/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 288230376151711742 + x6) - x10), ((Const 288230376151711742 + x7) - x11), ((Const 288230376151711706 + x5) - x9))) + (((0x3fffffffffffffe + x6) - x10), ((0x3fffffffffffffe + x7) - x11), ((0x3ffffffffffffda + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e174m17/fesubDisplay.log b/src/Specific/solinas64_2e174m17/fesubDisplay.log index dcc4852c9..747607a6c 100644 --- a/src/Specific/solinas64_2e174m17/fesubDisplay.log +++ b/src/Specific/solinas64_2e174m17/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 576460752303423486 + x6) - x10), ((Const 576460752303423486 + x7) - x11), ((Const 576460752303423454 + x5) - x9))) + (((0x7fffffffffffffe + x6) - x10), ((0x7fffffffffffffe + x7) - x11), ((0x7ffffffffffffde + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e174m3/fesubDisplay.log b/src/Specific/solinas64_2e174m3/fesubDisplay.log index 55f1c63c8..6fbc51ba6 100644 --- a/src/Specific/solinas64_2e174m3/fesubDisplay.log +++ b/src/Specific/solinas64_2e174m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x6, x7, x5, (x10, x11, x9))%core, - (((Const 576460752303423486 + x6) - x10), ((Const 576460752303423486 + x7) - x11), ((Const 576460752303423482 + x5) - x9))) + (((0x7fffffffffffffe + x6) - x10), ((0x7fffffffffffffe + x7) - x11), ((0x7fffffffffffffa + x5) - x9))) (x, x0)%core : word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e189m25/fesubDisplay.log b/src/Specific/solinas64_2e189m25/fesubDisplay.log index d916d0327..f67ee56fe 100644 --- a/src/Specific/solinas64_2e189m25/fesubDisplay.log +++ b/src/Specific/solinas64_2e189m25/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 281474976710654 + x8) - x14), ((Const 281474976710654 + x9) - x15), ((Const 281474976710654 + x7) - x13), ((Const 562949953421262 + x5) - x11))) + (((0xfffffffffffe + x8) - x14), ((0xfffffffffffe + x9) - x15), ((0xfffffffffffe + x7) - x13), ((0x1ffffffffffce + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e190m11/fesubDisplay.log b/src/Specific/solinas64_2e190m11/fesubDisplay.log index 0acc401d0..05c4a769d 100644 --- a/src/Specific/solinas64_2e190m11/fesubDisplay.log +++ b/src/Specific/solinas64_2e190m11/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 281474976710654 + x8) - x14), ((Const 562949953421310 + x9) - x15), ((Const 281474976710654 + x7) - x13), ((Const 562949953421290 + x5) - x11))) + (((0xfffffffffffe + x8) - x14), ((0x1fffffffffffe + x9) - x15), ((0xfffffffffffe + x7) - x13), ((0x1ffffffffffea + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e191m19/fesubDisplay.log b/src/Specific/solinas64_2e191m19/fesubDisplay.log index ca0c2dcf9..5aac62de5 100644 --- a/src/Specific/solinas64_2e191m19/fesubDisplay.log +++ b/src/Specific/solinas64_2e191m19/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core, - (((Const 549755813886 + x10) - x18), ((Const 549755813886 + x11) - x19), ((Const 549755813886 + x9) - x17), ((Const 549755813886 + x7) - x15), ((Const 1099511627738 + x5) - x13))) + (((0x7ffffffffe + x10) - x18), ((0x7ffffffffe + x11) - x19), ((0x7ffffffffe + x9) - x17), ((0x7ffffffffe + x7) - x15), ((0xffffffffda + 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_2e192m2e64m1/fesubDisplay.log b/src/Specific/solinas64_2e192m2e64m1/fesubDisplay.log index 00506e7de..2a60218c6 100644 --- a/src/Specific/solinas64_2e192m2e64m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e192m2e64m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 562949953421310 + x8) - x14), ((Const 562949953421310 + x9) - x15), ((Const 562949953290238 + x7) - x13), ((Const 562949953421310 + x5) - x11))) + (((0x1fffffffffffe + x8) - x14), ((0x1fffffffffffe + x9) - x15), ((0x1fffffffdfffe + x7) - x13), ((0x1fffffffffffe + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e194m33/fesubDisplay.log b/src/Specific/solinas64_2e194m33/fesubDisplay.log index 606d06032..7240009c0 100644 --- a/src/Specific/solinas64_2e194m33/fesubDisplay.log +++ b/src/Specific/solinas64_2e194m33/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 562949953421310 + x8) - x14), ((Const 1125899906842622 + x9) - x15), ((Const 562949953421310 + x7) - x13), ((Const 1125899906842558 + x5) - x11))) + (((0x1fffffffffffe + x8) - x14), ((0x3fffffffffffe + x9) - x15), ((0x1fffffffffffe + x7) - x13), ((0x3ffffffffffbe + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e196m15/fesubDisplay.log b/src/Specific/solinas64_2e196m15/fesubDisplay.log index 0314e70e1..146b4988d 100644 --- a/src/Specific/solinas64_2e196m15/fesubDisplay.log +++ b/src/Specific/solinas64_2e196m15/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 1125899906842622 + x8) - x14), ((Const 1125899906842622 + x9) - x15), ((Const 1125899906842622 + x7) - x13), ((Const 1125899906842594 + x5) - x11))) + (((0x3fffffffffffe + x8) - x14), ((0x3fffffffffffe + x9) - x15), ((0x3fffffffffffe + x7) - x13), ((0x3ffffffffffe2 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e198m17/fesubDisplay.log b/src/Specific/solinas64_2e198m17/fesubDisplay.log index 5e49eb374..0454cd477 100644 --- a/src/Specific/solinas64_2e198m17/fesubDisplay.log +++ b/src/Specific/solinas64_2e198m17/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 1125899906842622 + x8) - x14), ((Const 2251799813685246 + x9) - x15), ((Const 1125899906842622 + x7) - x13), ((Const 2251799813685214 + x5) - x11))) + (((0x3fffffffffffe + x8) - x14), ((0x7fffffffffffe + x9) - x15), ((0x3fffffffffffe + x7) - x13), ((0x7ffffffffffde + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e205m45x2e198m1/fesubDisplay.log b/src/Specific/solinas64_2e205m45x2e198m1/fesubDisplay.log index 7d329c1bb..c4a4577cd 100644 --- a/src/Specific/solinas64_2e205m45x2e198m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e205m45x2e198m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 2920302883373054 + x8) - x14), ((0xffffffffffffe + x9) - x15), ((0xffffffffffffe + x7) - x13), ((Const 9007199254740990 + x5) - x11))) + (((0xa5ffffffffffe + x8) - x14), ((0xffffffffffffe + x9) - x15), ((0xffffffffffffe + x7) - x13), ((0x1ffffffffffffe + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e206m5/fesubDisplay.log b/src/Specific/solinas64_2e206m5/fesubDisplay.log index 445c7da96..81bcc88f2 100644 --- a/src/Specific/solinas64_2e206m5/fesubDisplay.log +++ b/src/Specific/solinas64_2e206m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0xffffffffffffe + x8) - x14), ((Const 9007199254740990 + x9) - x15), ((0xffffffffffffe + x7) - x13), ((Const 9007199254740982 + x5) - x11))) + (((0xffffffffffffe + x8) - x14), ((0x1ffffffffffffe + x9) - x15), ((0xffffffffffffe + x7) - x13), ((0x1ffffffffffff6 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e212m29/fesubDisplay.log b/src/Specific/solinas64_2e212m29/fesubDisplay.log index e88b91ff1..d08123189 100644 --- a/src/Specific/solinas64_2e212m29/fesubDisplay.log +++ b/src/Specific/solinas64_2e212m29/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0x3ffffffffffffe + x8) - x14), ((0x3ffffffffffffe + x9) - x15), ((0x3ffffffffffffe + x7) - x13), ((Const 18014398509481926 + x5) - x11))) + (((0x3ffffffffffffe + x8) - x14), ((0x3ffffffffffffe + x9) - x15), ((0x3ffffffffffffe + x7) - x13), ((0x3fffffffffffc6 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e213m3/fesubDisplay.log b/src/Specific/solinas64_2e213m3/fesubDisplay.log index 026fa6f15..82e0dfabe 100644 --- a/src/Specific/solinas64_2e213m3/fesubDisplay.log +++ b/src/Specific/solinas64_2e213m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0x3ffffffffffffe + x8) - x14), ((0x3ffffffffffffe + x9) - x15), ((0x3ffffffffffffe + x7) - x13), ((Const 36028797018963962 + x5) - x11))) + (((0x3ffffffffffffe + x8) - x14), ((0x3ffffffffffffe + x9) - x15), ((0x3ffffffffffffe + x7) - x13), ((0x7ffffffffffffa + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e216m2e108m1/fesubDisplay.log b/src/Specific/solinas64_2e216m2e108m1/fesubDisplay.log index e0a155a5a..00f2ffde6 100644 --- a/src/Specific/solinas64_2e216m2e108m1/fesubDisplay.log +++ b/src/Specific/solinas64_2e216m2e108m1/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 36028797018963966 + x8) - x14), ((Const 36028797018963964 + x9) - x15), ((Const 36028797018963966 + x7) - x13), ((Const 36028797018963966 + x5) - x11))) + (((0x7ffffffffffffe + x8) - x14), ((0x7ffffffffffffc + x9) - x15), ((0x7ffffffffffffe + x7) - x13), ((0x7ffffffffffffe + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e221m3/fesubDisplay.log b/src/Specific/solinas64_2e221m3/fesubDisplay.log index c2867843f..f1c4eacf9 100644 --- a/src/Specific/solinas64_2e221m3/fesubDisplay.log +++ b/src/Specific/solinas64_2e221m3/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0xfffffffffffffe + x8) - x14), ((0xfffffffffffffe + x9) - x15), ((0xfffffffffffffe + x7) - x13), ((Const 144115188075855866 + x5) - x11))) + (((0xfffffffffffffe + x8) - x14), ((0xfffffffffffffe + x9) - x15), ((0xfffffffffffffe + x7) - x13), ((0x1fffffffffffffa + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e222m117/fesubDisplay.log b/src/Specific/solinas64_2e222m117/fesubDisplay.log index 304edaf24..eb74f7a0d 100644 --- a/src/Specific/solinas64_2e222m117/fesubDisplay.log +++ b/src/Specific/solinas64_2e222m117/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0xfffffffffffffe + x8) - x14), ((0x1fffffffffffffe + x9) - x15), ((0xfffffffffffffe + x7) - x13), ((Const 144115188075855638 + x5) - x11))) + (((0xfffffffffffffe + x8) - x14), ((0x1fffffffffffffe + x9) - x15), ((0xfffffffffffffe + x7) - x13), ((0x1ffffffffffff16 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e226m5/fesubDisplay.log b/src/Specific/solinas64_2e226m5/fesubDisplay.log index 381e827c8..f0f83e6da 100644 --- a/src/Specific/solinas64_2e226m5/fesubDisplay.log +++ b/src/Specific/solinas64_2e226m5/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((0x1fffffffffffffe + x8) - x14), ((Const 288230376151711742 + x9) - x15), ((0x1fffffffffffffe + x7) - x13), ((Const 288230376151711734 + x5) - x11))) + (((0x1fffffffffffffe + x8) - x14), ((0x3fffffffffffffe + x9) - x15), ((0x1fffffffffffffe + x7) - x13), ((0x3fffffffffffff6 + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/solinas64_2e230m27/fesubDisplay.log b/src/Specific/solinas64_2e230m27/fesubDisplay.log index 0705a9ed8..db7ef6c5d 100644 --- a/src/Specific/solinas64_2e230m27/fesubDisplay.log +++ b/src/Specific/solinas64_2e230m27/fesubDisplay.log @@ -2,6 +2,6 @@ Interp-η (λ var : Syntax.base_type → Type, λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core, - (((Const 288230376151711742 + x8) - x14), ((Const 576460752303423486 + x9) - x15), ((Const 288230376151711742 + x7) - x13), ((Const 576460752303423434 + x5) - x11))) + (((0x3fffffffffffffe + x8) - x14), ((0x7fffffffffffffe + x9) - x15), ((0x3fffffffffffffe + x7) - x13), ((0x7ffffffffffffca + x5) - x11))) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) |