make display

1 files changed, 58 insertions, 0 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
new file mode 100644
index 000000000..3189c60e8
--- /dev/null
+++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
@@ -0,0 +1,58 @@
+λ x x0 : word64 * word64,
+Interp-η
+(λ var : Syntax.base_type → Type,
+ λ '(x4, x5, (x6, x7))%core,
+ uint128_t x8 = (uint128_t) x5 * x7;
+ uint64_t x9 = (uint64_t) x8 & 0xffffffffffffffffL;
+ uint64_t x10 = (uint64_t) (x8 >> 0x40);
+ uint128_t x11 = (uint128_t) x5 * x6;
+ uint64_t x12 = (uint64_t) x11 & 0xffffffffffffffffL;
+ uint64_t x13 = (uint64_t) (x11 >> 0x40);
+ uint64_t x15, bool x16 = addcarryx_u64(0x0, 0x0, x9);
+ uint64_t x18, bool x19 = addcarryx_u64(x16, x10, x12);
+ uint64_t x21, bool _ = addcarryx_u64(0x0, x19, x13);
+ uint64_t x24, bool x25 = addcarryx_u64(0x0, 0x0, x15);
+ uint64_t x27, bool x28 = addcarryx_u64(x25, 0x0, x18);
+ uint64_t x30, bool x31 = addcarryx_u64(x28, 0x0, x21);
+ uint64_t x32 = x24 & 0xffffffffffffffffL;
+ uint128_t x33 = (uint128_t) x32 * 0xffffffffffffffffL;
+ uint64_t x34 = (uint64_t) x33 & 0xffffffffffffffffL;
+ uint64_t x35 = (uint64_t) (x33 >> 0x40);
+ ℤ x36 = x32 *ℤ Const 6277101733925179126845168871924920046849447032244165148671;
+ uint64_t x37 = x36 &ℤ 0xffffffffffffffffL;
+ ℤ x38 = x36 >>ℤ 0x40;
+ uint64_t x40, bool x41 = addcarryx_u64(0x0, 0x0, x34);
+ uint64_t x43, bool x44 = addcarryx_u64(x41, x35, x37);
+ uint64_t x46, uint128_t _ = Op (Syntax.AddWithGetCarry 64 (Syntax.TWord 0) (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 7)) (0x0, Return x44, Return x38);
+ uint64_t _, bool x50 = addcarryx_u64(0x0, x24, x40);
+ uint64_t x52, bool x53 = addcarryx_u64(x50, x27, x43);
+ uint64_t x55, bool x56 = addcarryx_u64(x53, x30, x46);
+ bool x58, bool _ = Op (Syntax.AddWithGetCarry 64 (Syntax.TWord 0) (Syntax.TWord 0) (Syntax.TWord 0) (Syntax.TWord 0) (Syntax.TWord 0)) (0x0, Return x56, Return x31);
+ uint128_t x60 = (uint128_t) x4 * x7;
+ uint64_t x61 = (uint64_t) x60 & 0xffffffffffffffffL;
+ uint64_t x62 = (uint64_t) (x60 >> 0x40);
+ uint128_t x63 = (uint128_t) x4 * x6;
+ uint64_t x64 = (uint64_t) x63 & 0xffffffffffffffffL;
+ uint64_t x65 = (uint64_t) (x63 >> 0x40);
+ uint64_t x67, bool x68 = addcarryx_u64(0x0, 0x0, x61);
+ uint64_t x70, bool x71 = addcarryx_u64(x68, x62, x64);
+ uint64_t x73, bool _ = addcarryx_u64(0x0, x71, x65);
+ uint64_t x76, bool x77 = addcarryx_u64(0x0, x52, x67);
+ uint64_t x79, bool x80 = addcarryx_u64(x77, x55, x70);
+ uint64_t x82, bool _ = addcarryx_u64(x80, x58, x73);
+ uint64_t x84 = x76 & 0xffffffffffffffffL;
+ uint128_t x85 = (uint128_t) x84 * 0xffffffffffffffffL;
+ uint64_t x86 = (uint64_t) x85 & 0xffffffffffffffffL;
+ uint64_t x87 = (uint64_t) (x85 >> 0x40);
+ ℤ x88 = x84 *ℤ Const 6277101733925179126845168871924920046849447032244165148671;
+ uint64_t x89 = x88 &ℤ 0xffffffffffffffffL;
+ ℤ x90 = x88 >>ℤ 0x40;
+ uint64_t x92, bool x93 = addcarryx_u64(0x0, 0x0, x86);
+ uint64_t x95, bool x96 = addcarryx_u64(x93, x87, x89);
+ uint64_t x98, uint128_t _ = Op (Syntax.AddWithGetCarry 64 (Syntax.TWord 0) (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 7)) (0x0, Return x96, Return x90);
+ uint64_t _, bool x102 = addcarryx_u64(0x0, x76, x92);
+ uint64_t x104, bool x105 = addcarryx_u64(x102, x79, x95);
+ uint64_t x107, bool _ = addcarryx_u64(x105, x82, x98);
+ (Return x107, Return x104))
+(x, x0)%core
+     : word64 * word64 → word64 * word64 → ReturnType (uint64_t * uint64_t)