fix: remove unprovable property and replace it with two provable ones

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

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