From a5458ac450f6804c80aaab658e5817cc13e0a844 Mon Sep 17 00:00:00 2001
From: teddy <teddy@defi.sucks>
Date: Thu, 1 Aug 2024 22:03:50 -0300
Subject: [PATCH] fix: remove unprovable property and replace it with two
 provable ones

---
 test/invariants/PROPERTIES.md       |  3 ++-
 test/invariants/symbolic/BNum.t.sol | 39 +++++++++++++++++++----------
 2 files changed, 28 insertions(+), 14 deletions(-)

diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md
index 40b535ea..ff3d6ed1 100644
--- a/test/invariants/PROPERTIES.md
+++ b/test/invariants/PROPERTIES.md
@@ -49,12 +49,13 @@ badd result should always be gte its terms
 badd should never sum terms which have a sum gt uint max
 badd should have bsub as reverse operation
 
-bsub should not be commutative
 bsub should not be associative
 bsub should have 0 as identity
 bsub result should always be lte its terms
 bsub should alway revert if b > a (duplicate with previous tho)
 
+bsubSign should not be commutative sign-wise
+bsubSign should be commutative value-wise
 bsubSign result should always be negative if b > a
 bsubSign result should always be positive if a > b
 bsubSign result should always be 0 if a == b
diff --git a/test/invariants/symbolic/BNum.t.sol b/test/invariants/symbolic/BNum.t.sol
index 2f218f6f..9a4b9cd1 100644
--- a/test/invariants/symbolic/BNum.t.sol
+++ b/test/invariants/symbolic/BNum.t.sol
@@ -100,19 +100,6 @@ contract SymbolicBNum is BNum, HalmosTest {
   //                           Bnum::bsub                            //
   /////////////////////////////////////////////////////////////////////
 
-  // bsub should not be commutative
-  function check_bsub_notCommut(uint256 _a, uint256 _b) public pure {
-    // precondition
-    vm.assume(_a != _b);
-
-    // action
-    uint256 _result1 = bsub(_a, _b);
-    uint256 _result2 = bsub(_b, _a);
-
-    // post condition
-    assert(_result1 != _result2);
-  }
-
   // bsub should not be associative
   function check_bsub_notAssoc(uint256 _a, uint256 _b, uint256 _c) public pure {
     // precondition
@@ -152,6 +139,32 @@ contract SymbolicBNum is BNum, HalmosTest {
   //                         Bnum::bsubSign                          //
   /////////////////////////////////////////////////////////////////////
 
+  // bsubSign should be commutative value-wise
+  function check_bsubSign_CommutValue(uint256 _a, uint256 _b) public pure {
+    // precondition
+    vm.assume(_a != _b);
+
+    // action
+    (uint256 _result1,) = bsubSign(_a, _b);
+    (uint256 _result2,) = bsubSign(_b, _a);
+
+    // post condition
+    assert(_result1 == _result2);
+  }
+
+  // bsubSign should not be commutative sign-wise
+  function check_bsubSign_notCommutSign(uint256 _a, uint256 _b) public pure {
+    // precondition
+    vm.assume(_a != _b);
+
+    // action
+    (, bool _sign1) = bsubSign(_a, _b);
+    (, bool _sign2) = bsubSign(_b, _a);
+
+    // post condition
+    assert(_sign1 != _sign2);
+  }
+
   // bsubSign result should always be negative if b > a
   function check_bsubSign_negative(uint256 _a, uint256 _b) public pure {
     // precondition