make display

8 files changed, 36 insertions, 52 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
index ff714ff16..5a9182d47 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128Display.log
+++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
@@ -32,10 +32,9 @@ Interp-η
  uint8_t x89 = x88 + x64;
  uint128_t x91, uint8_t x92 = subborrow_u128(0x0, x84, 0xffffffffffffffffffffffffL);
  uint128_t x94, uint8_t x95 = subborrow_u128(x92, x87, 0xffffffff000000010000000000000000L);
- ℤ x96 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x95);
- uint128_t _, ℤ x99 = addcarryx_u128ℤ(0x0, x96, x89);
- uint128_t x100 = x99 == 0 ? x94 : x87;
- uint128_t x101 = x99 == 0 ? x91 : x84;
- return (x100, x101))
+ uint128_t _, uint8_t x98 = subborrow_u128(x95, x89, 0x0);
+ uint128_t x99 = x98 == 0 ? x94 : x87;
+ uint128_t x100 = x98 == 0 ? x91 : x84;
+ return (x99, x100))
 (x, x0)%core
      : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log
index ea170fc85..3c1716a73 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log
@@ -6,10 +6,9 @@ Interp-η
  uint128_t x12, uint8_t x13 = addcarryx_u128(x10, x4, x6);
  uint128_t x15, uint8_t x16 = subborrow_u128(0x0, x9, 0xffffffffffffffffffffffffL);
  uint128_t x18, uint8_t x19 = subborrow_u128(x16, x12, 0xffffffff000000010000000000000000L);
- ℤ x20 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x19);
- uint128_t _, ℤ x23 = addcarryx_u128ℤ(0x0, x20, x13);
- uint128_t x24 = x23 == 0 ? x18 : x12;
- uint128_t x25 = x23 == 0 ? x15 : x9;
- return (x24, x25))
+ uint128_t _, uint8_t x22 = subborrow_u128(x19, x13, 0x0);
+ uint128_t x23 = x22 == 0 ? x18 : x12;
+ uint128_t x24 = x22 == 0 ? x15 : x9;
+ return (x23, x24))
 (x, x0)%core
      : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log
index 4e8fe5a50..50c41e1af 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log
@@ -6,12 +6,9 @@ Interp-η
  uint128_t x7, uint8_t x8 = subborrow_u128(x5, 0x0, x1);
  uint128_t x9 = (uint128_t) (x8 == 0 ? 0x0 : 0xffffffffffffffffffffffffffffffffL);
  uint128_t x10 = x9 & 0xffffffffffffffffffffffffL;
- uint128_t x12, uint8_t x13 = addcarryx_u128(0x0, x4, x10);
+ uint128_t x12, uint8_t x13 = subborrow_u128(0x0, x4, x10);
  uint128_t x14 = x9 & 0xffffffff000000010000000000000000L;
- uint256_t x15 = 0x100000000000000000000000000000000L * x8;
- ℤ x16 = Op (Syntax.Opp (Syntax.TWord 8) Syntax.TZ) (Return x15);
- uint128_t x18, ℤ _ = addcarryx_u128ℤ(x7, x16, x14);
- uint128_t x21, uint8_t _ = addcarryx_u128(0x0, x13, x18);
- (Return x21, Return x12))
+ uint128_t x16, uint8_t _ = subborrow_u128(x13, x7, x14);
+ (Return x16, Return x12))
 x
      : word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log
index 576f0c6be..07579501c 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log
@@ -6,12 +6,9 @@ Interp-η
  uint128_t x12, uint8_t x13 = subborrow_u128(x10, x4, x6);
  uint128_t x14 = (uint128_t) (x13 == 0 ? 0x0 : 0xffffffffffffffffffffffffffffffffL);
  uint128_t x15 = x14 & 0xffffffffffffffffffffffffL;
- uint128_t x17, uint8_t x18 = addcarryx_u128(0x0, x9, x15);
+ uint128_t x17, uint8_t x18 = subborrow_u128(0x0, x9, x15);
  uint128_t x19 = x14 & 0xffffffff000000010000000000000000L;
- uint256_t x20 = 0x100000000000000000000000000000000L * x13;
- ℤ x21 = Op (Syntax.Opp (Syntax.TWord 8) Syntax.TZ) (Return x20);
- uint128_t x23, ℤ _ = addcarryx_u128ℤ(x12, x21, x19);
- uint128_t x26, uint8_t _ = addcarryx_u128(0x0, x18, x23);
- (Return x26, Return x17))
+ uint128_t x21, uint8_t _ = subborrow_u128(x18, x12, x19);
+ (Return x21, Return x17))
 (x, x0)%core
      : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log
index 3c47f3fc9..1dc1b7ba3 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log
@@ -104,12 +104,11 @@ Interp-η
  uint64_t x308, uint8_t x309 = subborrow_u64(x306, x295, 0xffffffff);
  uint64_t x311, uint8_t x312 = subborrow_u64(x309, x298, 0x0);
  uint64_t x314, uint8_t x315 = subborrow_u64(x312, x301, 0xffffffff00000001L);
- ℤ x316 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x315);
- uint64_t _, ℤ x319 = addcarryx_u64ℤ(0x0, x316, x303);
- uint64_t x320 = x319 == 0 ? x314 : x301;
- uint64_t x321 = x319 == 0 ? x311 : x298;
- uint64_t x322 = x319 == 0 ? x308 : x295;
- uint64_t x323 = x319 == 0 ? x305 : x292;
- return (x320, x321, x322, x323))
+ uint64_t _, uint8_t x318 = subborrow_u64(x315, x303, 0x0);
+ uint64_t x319 = x318 == 0 ? x314 : x301;
+ uint64_t x320 = x318 == 0 ? x311 : x298;
+ uint64_t x321 = x318 == 0 ? x308 : x295;
+ uint64_t x322 = x318 == 0 ? x305 : x292;
+ return (x319, x320, x321, x322))
 (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/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log
index 0f46e27f6..e6498cf83 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log
@@ -10,12 +10,11 @@ Interp-η
  uint64_t x32, uint8_t x33 = subborrow_u64(x30, x20, 0xffffffff);
  uint64_t x35, uint8_t x36 = subborrow_u64(x33, x23, 0x0);
  uint64_t x38, uint8_t x39 = subborrow_u64(x36, x26, 0xffffffff00000001L);
- ℤ x40 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x39);
- uint64_t _, ℤ x43 = addcarryx_u64ℤ(0x0, x40, x27);
- uint64_t x44 = x43 == 0 ? x38 : x26;
- uint64_t x45 = x43 == 0 ? x35 : x23;
- uint64_t x46 = x43 == 0 ? x32 : x20;
- uint64_t x47 = x43 == 0 ? x29 : x17;
- return (x44, x45, x46, x47))
+ uint64_t _, uint8_t x42 = subborrow_u64(x39, x27, 0x0);
+ uint64_t x43 = x42 == 0 ? x38 : x26;
+ uint64_t x44 = x42 == 0 ? x35 : x23;
+ uint64_t x45 = x42 == 0 ? x32 : x20;
+ uint64_t x46 = x42 == 0 ? x29 : x17;
+ return (x43, x44, x45, x46))
 (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/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log
index 0b94a81ce..b76a34a56 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log
@@ -8,15 +8,12 @@ Interp-η
  uint64_t x17, uint8_t x18 = subborrow_u64(x15, 0x0, x5);
  uint64_t x19 = (uint64_t) (x18 == 0 ? 0x0 : 0xffffffffffffffffL);
  uint64_t x20 = x19 & 0xffffffffffffffffL;
- uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x8, x20);
+ uint64_t x22, uint8_t x23 = subborrow_u64(0x0, x8, x20);
  uint64_t x24 = x19 & 0xffffffff;
- uint64_t x26, uint8_t x27 = addcarryx_u64(x23, x11, x24);
- uint64_t x29, uint8_t x30 = addcarryx_u64(x27, x14, 0x0);
+ uint64_t x26, uint8_t x27 = subborrow_u64(x23, x11, x24);
+ uint64_t x29, uint8_t x30 = subborrow_u64(x27, x14, 0x0);
  uint64_t x31 = x19 & 0xffffffff00000001L;
- uint128_t x32 = 0x10000000000000000L * x18;
- ℤ x33 = Op (Syntax.Opp (Syntax.TWord 7) Syntax.TZ) (Return x32);
- uint64_t x35, ℤ _ = addcarryx_u64ℤ(x17, x33, x31);
- uint64_t x38, uint8_t _ = addcarryx_u64(0x0, x30, x35);
- (Return x38, Return x29, Return x26, Return x22))
+ uint64_t x33, uint8_t _ = subborrow_u64(x30, x17, x31);
+ (Return x33, Return x29, Return x26, Return x22))
 x
      : word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log
index 9b301c678..de068350b 100644
--- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log
@@ -8,15 +8,12 @@ Interp-η
  uint64_t x26, uint8_t x27 = subborrow_u64(x24, x8, x14);
  uint64_t x28 = (uint64_t) (x27 == 0 ? 0x0 : 0xffffffffffffffffL);
  uint64_t x29 = x28 & 0xffffffffffffffffL;
- uint64_t x31, uint8_t x32 = addcarryx_u64(0x0, x17, x29);
+ uint64_t x31, uint8_t x32 = subborrow_u64(0x0, x17, x29);
  uint64_t x33 = x28 & 0xffffffff;
- uint64_t x35, uint8_t x36 = addcarryx_u64(x32, x20, x33);
- uint64_t x38, uint8_t x39 = addcarryx_u64(x36, x23, 0x0);
+ uint64_t x35, uint8_t x36 = subborrow_u64(x32, x20, x33);
+ uint64_t x38, uint8_t x39 = subborrow_u64(x36, x23, 0x0);
  uint64_t x40 = x28 & 0xffffffff00000001L;
- uint128_t x41 = 0x10000000000000000L * x27;
- ℤ x42 = Op (Syntax.Opp (Syntax.TWord 7) Syntax.TZ) (Return x41);
- uint64_t x44, ℤ _ = addcarryx_u64ℤ(x26, x42, x40);
- uint64_t x47, uint8_t _ = addcarryx_u64(0x0, x39, x44);
- (Return x47, Return x38, Return x35, Return x31))
+ uint64_t x42, uint8_t _ = subborrow_u64(x39, x26, x40);
+ (Return x42, Return x38, Return x35, Return x31))
 (x, x0)%core
      : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)