chore: fuzz sym fixes

src/contracts/BCoWPool.sol

@@ -145,7 +145,7 @@ contract BCoWPool is IERC1271, IBCoWPool, BPool, BCoWConst {
    * @dev Grants infinite approval to the vault relayer for all tokens in the
    * pool after the finalization of the setup. Also emits COWAMMPoolCreated() event.
    */
-  function _afterFinalize() internal override {
+  function _afterFinalize() internal virtual override {
     uint256 tokensLength = _tokens.length;
     for (uint256 i; i < tokensLength; i++) {
       IERC20(_tokens[i]).forceApprove(VAULT_RELAYER, type(uint256).max);

src/contracts/BFactory.sol

@@ -42,7 +42,7 @@ contract BFactory is IBFactory {
   }
 
   /// @inheritdoc IBFactory
-  function collect(IBPool bPool) external {
+  function collect(IBPool bPool) external virtual {
     if (msg.sender != _bDao) {
       revert BFactory_NotBDao();
     }

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/fuzz/BToken.t.sol

@@ -47,7 +47,7 @@ contract FuzzBToken is CryticERC20ExternalBasicProperties, EchidnaTest {
   }
 }
 
-contract CryticTokenMock is BToken, PropertiesConstants {
+contract CryticTokenMock is BToken('Balancer Pool Token', 'BPT'), PropertiesConstants {
   bool public isMintableOrBurnable;
   uint256 public initialSupply;
 

test/invariants/fuzz/Protocol.t.sol

@@ -32,6 +32,9 @@ contract FuzzProtocol is EchidnaTest {
   uint256 ghost_bptBurned;
   mapping(FuzzERC20 => uint256) ghost_amountDirectlyTransfered;
 
+  string constant ERC20_SYMBOL = 'BPT';
+  string constant ERC20_NAME = 'Balancer Pool Token';
+
   constructor() {
     solutionSettler = address(new MockSettler());
 
@@ -40,7 +43,7 @@ contract FuzzProtocol is EchidnaTest {
     bmath = new BMath();
     bnum = new BNum();
 
-    pool = IBCoWPool(address(factory.newBPool()));
+    pool = IBCoWPool(address(factory.newBPool('Balancer Pool Token', 'BPT')));
 
     // first 4 tokens bound to the finalized pool
     for (uint256 i; i < 4; i++) {
@@ -119,7 +122,7 @@ contract FuzzProtocol is EchidnaTest {
     hevm.prank(currentCaller);
 
     // Action
-    try factory.newBPool() returns (IBPool _newPool) {
+    try factory.newBPool(ERC20_NAME, ERC20_SYMBOL) returns (IBPool _newPool) {
       // Postcondition
       assert(address(_newPool).code.length > 0);
       assert(factory.isBPool(address(_newPool)));
@@ -147,7 +150,6 @@ contract FuzzProtocol is EchidnaTest {
     }
   }
 
-  /* TODO: re-enable this test after fixing the hevm issue with SafeTransfer library
   /// @custom:property-id 3
   /// @custom:property BFactory should always be able to transfer the BToken to the BDao, if called by it
   function fuzz_alwaysCollect() public agentOrDeployer {
@@ -168,7 +170,6 @@ contract FuzzProtocol is EchidnaTest {
       assert(_currentBDao != currentCaller);
     }
   }
-  */
 
   /// @custom:property-id 4
   /// @custom:property the amount received can never be less than min amount out
@@ -341,7 +342,7 @@ contract FuzzProtocol is EchidnaTest {
   /// @custom:property total weight can be up to 50e18
   function fuzz_totalWeightMax(uint256 _numberTokens, uint256[8] calldata _weights) public {
     // Precondition
-    IBPool _pool = IBPool(address(factory.newBPool()));
+    IBPool _pool = IBPool(address(factory.newBPool(ERC20_NAME, ERC20_SYMBOL)));
 
     _numberTokens = clamp(_numberTokens, bconst.MIN_BOUND_TOKENS(), bconst.MAX_BOUND_TOKENS());
 
@@ -419,83 +420,6 @@ contract FuzzProtocol is EchidnaTest {
     assert(ghost_bptMinted - ghost_bptBurned == pool.totalSupply());
   }
 
-  /* NOTE: deprecated calcSingleOutGivenPoolIn
-  /// @custom:property-id 17
-  /// @custom:property a direct token transfer can never reduce the underlying amount of a given token per BPT
-  function fuzz_directTransfer(
-    uint256 _amountPoolToken,
-    uint256 _amountToTransfer,
-    uint256 _tokenIdx
-  ) public agentOrDeployer {
-    _tokenIdx = clamp(_tokenIdx, 0, tokens.length - 1);
-    FuzzERC20 _token = tokens[_tokenIdx];
-
-    uint256 _redeemedAmountBeforeTransfer = bmath.calcSingleOutGivenPoolIn(
-      _token.balanceOf(address(pool)),
-      pool.getDenormalizedWeight(address(_token)),
-      pool.totalSupply(),
-      pool.getTotalDenormalizedWeight(),
-      _amountPoolToken,
-      bconst.MIN_FEE()
-    );
-
-    _token.mint(address(this), _amountToTransfer);
-    // Action
-    _token.transfer(address(pool), _amountToTransfer);
-
-    // Postcondition
-    uint256 _redeemedAmountAfter = bmath.calcSingleOutGivenPoolIn(
-      _token.balanceOf(address(pool)),
-      pool.getDenormalizedWeight(address(_token)),
-      pool.totalSupply(),
-      pool.getTotalDenormalizedWeight(),
-      _amountPoolToken,
-      bconst.MIN_FEE()
-    );
-
-    assert(_redeemedAmountAfter >= _redeemedAmountBeforeTransfer);
-
-    ghost_amountDirectlyTransfered[_token] += _amountToTransfer;
-  }
-
-  /// @custom:property-id 18
-  /// @custom:property the amount of underlying token when exiting should always be the amount calculated in bmath
-  function fuzz_correctBPTBurnAmount(uint256 _amountPoolToken) public agentOrDeployer {
-    _amountPoolToken = clamp(_amountPoolToken, 0, pool.balanceOf(currentCaller));
-
-    uint256[] memory _amountsToReceive = new uint256[](4);
-    uint256[] memory _previousBalances = new uint256[](4);
-
-    for (uint256 i; i < tokens.length; i++) {
-      FuzzERC20 _token = tokens[i];
-
-      _amountsToReceive[i] = bmath.calcSingleOutGivenPoolIn(
-        _token.balanceOf(address(pool)),
-        pool.getDenormalizedWeight(address(_token)),
-        pool.totalSupply(),
-        pool.getTotalDenormalizedWeight(),
-        _amountPoolToken,
-        bconst.MIN_FEE()
-      );
-
-      _previousBalances[i] = _token.balanceOf(currentCaller);
-    }
-
-    hevm.prank(currentCaller);
-    pool.approve(address(pool), _amountPoolToken);
-
-    hevm.prank(currentCaller);
-
-    // Action
-    pool.exitPool(_amountPoolToken, new uint256[](4));
-
-    // PostCondition
-    for (uint256 i; i < tokens.length; i++) {
-      assert(tokens[i].balanceOf(currentCaller) == _previousBalances[i] + _amountsToReceive[i]);
-    }
-  }
-  */
-
   /// @custom:property-id 20
   /// @custom:property bounding and unbounding token can only be done on a non-finalized pool, by the controller
   function fuzz_boundOnlyNotFinalized() public agentOrDeployer {

test/invariants/helpers/BCoWFactoryForTest.sol

@@ -3,12 +3,24 @@ pragma solidity 0.8.25;
 
 import {BCoWPoolForTest} from './BCoWPoolForTest.sol';
 import {BCoWFactory} from 'contracts/BCoWFactory.sol';
+
+import {BFactory} from 'contracts/BFactory.sol';
+import {IBFactory} from 'interfaces/IBFactory.sol';
 import {IBPool} from 'interfaces/IBPool.sol';
 
 contract BCoWFactoryForTest is BCoWFactory {
   constructor(address cowSolutionSettler, bytes32 appData) BCoWFactory(cowSolutionSettler, appData) {}
 
-  function _newBPool() internal virtual override returns (IBPool bCoWPool) {
+  function _newBPool(string memory, string memory) internal virtual override returns (IBPool bCoWPool) {
     bCoWPool = new BCoWPoolForTest(SOLUTION_SETTLER, APP_DATA);
   }
+
+  /// @dev workaround for hevm not supporting mcopy
+  function collect(IBPool bPool) external override(BFactory, IBFactory) {
+    if (msg.sender != _bDao) {
+      revert BFactory_NotBDao();
+    }
+    uint256 collected = bPool.balanceOf(address(this));
+    bPool.transfer(_bDao, collected);
+  }
 }

test/invariants/helpers/BCoWPoolForTest.sol

@@ -2,10 +2,12 @@
 pragma solidity 0.8.25;
 
 import {IERC20} from '@openzeppelin/contracts/token/ERC20/IERC20.sol';
+
 import {BCoWPool} from 'contracts/BCoWPool.sol';
+import {IBCoWFactory} from 'interfaces/IBCoWFactory.sol';
 
 contract BCoWPoolForTest is BCoWPool {
-  constructor(address cowSolutionSettler, bytes32 appData) BCoWPool(cowSolutionSettler, appData) {}
+  constructor(address cowSolutionSettler, bytes32 appData) BCoWPool(cowSolutionSettler, appData, 'name', 'symbol') {}
 
   bytes32 private _reenteringMutex;
 
@@ -28,4 +30,17 @@ contract BCoWPoolForTest is BCoWPool {
   function _pushUnderlying(address token, address to, uint256 amount) internal override {
     IERC20(token).transfer(to, amount);
   }
+
+  /// @dev workaround for hevm not supporting mcopy
+  function _afterFinalize() internal override {
+    uint256 tokensLength = _tokens.length;
+    for (uint256 i; i < tokensLength; i++) {
+      IERC20(_tokens[i]).approve(VAULT_RELAYER, type(uint256).max);
+    }
+
+    try IBCoWFactory(FACTORY).logBCoWPool() {}
+    catch {
+      emit IBCoWFactory.COWAMMPoolCreated(address(this));
+    }
+  }
 }

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

test/invariants/symbolic/Protocol.t.sol

@@ -3,33 +3,32 @@ pragma solidity 0.8.25;
 
 import {FuzzERC20, HalmosTest} from '../helpers/AdvancedTestsUtils.sol';
 
+import {BCoWFactoryForTest as BCoWFactory} from '../helpers/BCoWFactoryForTest.sol';
 import {MockSettler} from '../helpers/MockSettler.sol';
-import {BCoWFactory, BCoWPool, IBPool} from 'contracts/BCoWFactory.sol';
+import {IBCoWPool} from 'interfaces/IBCoWPool.sol';
+import {IBPool} from 'interfaces/IBPool.sol';
 
 import {BConst} from 'contracts/BConst.sol';
-import {BMath} from 'contracts/BMath.sol';
 import {BToken} from 'contracts/BToken.sol';
 
 contract HalmosBalancer is HalmosTest {
   // System under test
   BCoWFactory factory;
   BConst bconst;
-  BMath bmath;
 
   address solutionSettler;
   bytes32 appData;
 
   FuzzERC20[] tokens;
-  BCoWPool pool;
+  IBCoWPool pool;
 
   address currentCaller = svm.createAddress('currentCaller');
 
   constructor() {
     solutionSettler = address(new MockSettler());
     factory = new BCoWFactory(solutionSettler, appData);
     bconst = new BConst();
-    bmath = new BMath();
-    pool = BCoWPool(address(factory.newBPool()));
+    pool = IBCoWPool(address(factory.newBPool('Balancer Pool Token', 'BPT')));
 
     // max bound token is 8
     for (uint256 i; i < 5; i++) {
@@ -63,7 +62,7 @@ contract HalmosBalancer is HalmosTest {
     vm.prank(_caller);
 
     // Action
-    try factory.newBPool() returns (IBPool _newPool) {
+    try factory.newBPool('Balancer Pool Token', 'BPT') returns (IBPool _newPool) {
       // Postcondition
       assert(address(_newPool).code.length > 0);
       assert(factory.isBPool(address(_newPool)));
@@ -112,7 +111,7 @@ contract HalmosBalancer is HalmosTest {
   /// @dev Only 2 tokens are used, to avoid hitting the limit in loop unrolling
   function check_totalWeightMax(uint256[2] calldata _weights) public {
     // Precondition
-    BCoWPool _pool = BCoWPool(address(factory.newBPool()));
+    IBCoWPool _pool = IBCoWPool(address(factory.newBPool('Balancer Pool Token', 'BPT')));
 
     uint256 _totalWeight = 0;
 
@@ -179,7 +178,7 @@ contract HalmosBalancer is HalmosTest {
   /// @custom:property a non-finalized pool can only be finalized when the controller calls finalize()
   function check_poolFinalizedByController() public {
     // Precondition
-    IBPool _nonFinalizedPool = factory.newBPool();
+    IBPool _nonFinalizedPool = factory.newBPool('Balancer Pool Token', 'BPT');
 
     vm.prank(_nonFinalizedPool.getController());
 
@@ -209,7 +208,7 @@ contract HalmosBalancer is HalmosTest {
   /// @custom:property bounding and unbounding token can only be done on a non-finalized pool, by the controller
   function check_boundOnlyNotFinalized() public {
     // Precondition
-    IBPool _nonFinalizedPool = factory.newBPool();
+    IBPool _nonFinalizedPool = factory.newBPool('Balancer Pool Token', 'BPT');
 
     address _callerBind = svm.createAddress('callerBind');
     address _callerUnbind = svm.createAddress('callerUnbind');