make display (new conditional_sub)

2 files changed, 24 insertions, 6 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256Display.log b/src/Specific/IntegrationTestMontgomeryP256Display.log
index 7b514df9e..a7c2cccae 100644
--- a/src/Specific/IntegrationTestMontgomeryP256Display.log
+++ b/src/Specific/IntegrationTestMontgomeryP256Display.log
@@ -86,7 +86,7 @@ Interp-η
  uint64_t x256, uint8_t x257 = addcarryx_u64(x254, x219, x241);
  uint64_t x259, uint8_t x260 = addcarryx_u64(x257, x222, x244);
  uint64_t x262, uint8_t x263 = addcarryx_u64(x260, x225, x247);
- uint64_t x265, uint8_t _ = addcarryx_u64(x263, x227, x250);
+ uint64_t x265, uint8_t x266 = addcarryx_u64(x263, x227, x250);
  uint64_t x268, uint64_t x269 = mulx_u64(x253, 0xffffffffffffffffL);
  uint64_t x271, uint64_t x272 = mulx_u64(x253, 0xffffffff);
  uint64_t x274, uint64_t x275 = mulx_u64(x253, 0xffffffff00000001L);
@@ -98,7 +98,18 @@ Interp-η
  uint64_t x292, uint8_t x293 = addcarryx_u64(x290, x256, x277);
  uint64_t x295, uint8_t x296 = addcarryx_u64(x293, x259, x280);
  uint64_t x298, uint8_t x299 = addcarryx_u64(x296, x262, x283);
- uint64_t x301, uint8_t _ = addcarryx_u64(x299, x265, x286);
- (Return x301, Return x298, Return x295, Return x292))
+ uint64_t x301, uint8_t x302 = addcarryx_u64(x299, x265, x286);
+ uint8_t x303 = x302 + x266;
+ uint64_t x304 = (uint64_t) (x303 == 0 ? 0x0 : 0xffffffffffffffffL);
+ uint64_t x306, uint8_t x307 = subborrow_u64(0x0, x292, x304 & 0xffffffffffffffffL);
+ ℤ x308 = 0x0 -ℤ x307;
+ uint64_t x310, uint8_t x311 = subborrow_u64(0x0, x295, x304 & 0xffffffff);
+ uint64_t x313, ℤ x314 = Op (Syntax.AddWithGetCarry 64 (Syntax.TWord 3) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x308, Return x310);
+ ℤ x315 = x314 -ℤ x311;
+ uint64_t x317, ℤ x318 = Op (Syntax.AddWithGetCarry 64 Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 3) (Syntax.TWord 6) Syntax.TZ) (Return x315, Return x298, 0x0);
+ uint64_t x320, ℤ _ = Op (Syntax.SubWithGetBorrow 64 (Syntax.TWord 3) (Syntax.TWord 7) (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, 0x10000000000000000L * x303, x304 & 0xffffffff00000001L);
+ uint64_t x323, uint8_t _ = addcarryx_u64(0x0, x301, x320);
+ uint64_t x326, ℤ _ = Op (Syntax.AddWithGetCarry 64 (Syntax.TWord 3) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x318, Return x323);
+ (Return x326, Return x317, Return x313, Return x306))
 (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/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
index 78b711c82..b477fb4b6 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128Display.log
+++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.log
@@ -20,7 +20,7 @@ Interp-η
  uint128_t x54, uint8_t _ = addcarryx_u128(0x0, x52, x49);
  uint128_t x57, uint8_t x58 = addcarryx_u128(0x0, x39, x45);
  uint128_t x60, uint8_t x61 = addcarryx_u128(x58, x42, x51);
- uint128_t x63, uint8_t _ = addcarryx_u128(x61, x43, x54);
+ uint128_t x63, uint8_t x64 = addcarryx_u128(x61, x43, x54);
  uint128_t x66, uint128_t _ = mulx_u128(x57, 0x1000000000000000000000001L);
  uint128_t x69, uint128_t x70 = mulx_u128(x66, 0xffffffffffffffffffffffffL);
  uint128_t x72, uint128_t x73 = mulx_u128(x66, 0xffffffff000000010000000000000000L);
@@ -28,7 +28,14 @@ Interp-η
  uint128_t x78, uint8_t _ = addcarryx_u128(0x0, x76, x73);
  uint128_t _, uint8_t x82 = addcarryx_u128(0x0, x57, x69);
  uint128_t x84, uint8_t x85 = addcarryx_u128(x82, x60, x75);
- uint128_t x87, uint8_t _ = addcarryx_u128(x85, x63, x78);
- (Return x87, Return x84))
+ uint128_t x87, uint8_t x88 = addcarryx_u128(x85, x63, x78);
+ uint8_t x89 = x88 + x64;
+ uint128_t x90 = (uint128_t) (x89 == 0 ? 0x0 : 0xffffffffffffffffffffffffffffffffL);
+ uint128_t x92, uint8_t x93 = subborrow_u128(0x0, x84, x90 & 0xffffffffffffffffffffffffL);
+ ℤ x94 = 0x0 -ℤ x93;
+ uint128_t x96, ℤ _ = Op (Syntax.SubWithGetBorrow 128 (Syntax.TWord 3) (Syntax.TWord 8) (Syntax.TWord 7) (Syntax.TWord 7) Syntax.TZ) (0x0, Const 340282366920938463463374607431768211456 * x89, x90 & 0xffffffff000000010000000000000000L);
+ uint128_t x99, uint8_t _ = addcarryx_u128(0x0, x87, x96);
+ uint128_t x102, ℤ _ = Op (Syntax.AddWithGetCarry 128 (Syntax.TWord 3) Syntax.TZ (Syntax.TWord 7) (Syntax.TWord 7) Syntax.TZ) (0x0, Return x94, Return x99);
+ (Return x102, Return x92))
 (x, x0)%core
      : word128 * word128 → word128 * word128 → ReturnType (uint128_t * uint128_t)