feat(test): fuzzed and symbolic tests

.gitignore

@@ -19,3 +19,6 @@ broadcast/*/*/*
 
 # Out dir
 out
+
+# echidna corpuses
+**/corpuses/*

.solhintignore

@@ -1,2 +1,3 @@
 test/smock/*
 test/manual-smock/*
+test/invariants/*

foundry.toml

@@ -9,15 +9,16 @@ multiline_func_header = 'params_first'
 sort_imports = true
 
 [profile.default]
-solc_version = '0.8.25'
+solc_version = '0.8.23'
 libs = ["node_modules", "lib"]
 optimizer_runs = 500
 evm_version = 'cancun'
 fs_permissions = [{ access = "read-write", path = ".forge-snapshots/"}]
 # 2018: function can be view, so far only caused by mocks
 # 2394: solc insists on reporting on every transient storage use
 # 5574, 3860: bytecode size limit, so far only caused by test contracts
-ignored_error_codes = [2018, 2394, 5574, 3860]
+# 1858: Some imports don't have the license identifier
+ignored_error_codes = [2018, 2394, 5574, 3860, 1878]
 deny_warnings = true
 
 [profile.optimized]

package.json

@@ -40,6 +40,7 @@
   },
   "dependencies": {
     "@cowprotocol/contracts": "github:cowprotocol/contracts.git#a10f40788a",
+    "@crytic/properties": "https://github.com/crytic/properties.git",
     "@openzeppelin/contracts": "5.0.2",
     "composable-cow": "github:cowprotocol/composable-cow.git#24d556b",
     "solmate": "github:transmissions11/solmate#c892309"
@@ -50,7 +51,8 @@
     "@defi-wonderland/natspec-smells": "1.1.3",
     "@defi-wonderland/smock-foundry": "1.5.0",
     "forge-gas-snapshot": "github:marktoda/forge-gas-snapshot#9161f7c",
-    "forge-std": "github:foundry-rs/forge-std#5475f85",
+    "forge-std": "github:foundry-rs/forge-std#1.8.2",
+    "halmos-cheatcodes": "github:a16z/halmos-cheatcodes#c0d8655",
     "husky": ">=8",
     "lint-staged": ">=10",
     "solhint-community": "4.0.0",

remappings.txt

@@ -5,6 +5,8 @@ solmate/=node_modules/solmate/src
 @cowprotocol/=node_modules/@cowprotocol/contracts/src/contracts
 cowprotocol/=node_modules/@cowprotocol/contracts/src/
 @composable-cow/=node_modules/composable-cow/
+halmos-cheatcodes=node_modules/halmos-cheatcodes
+@crytic/=node_modules/@crytic/
 
 contracts/=src/contracts
 interfaces/=src/interfaces

script/DeployBCoWFactory.s.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BCoWFactory} from 'contracts/BCoWFactory.sol';
 import {Script} from 'forge-std/Script.sol';

script/DeployBFactory.s.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BFactory} from 'contracts/BFactory.sol';
 import {Script} from 'forge-std/Script.sol';

script/Params.s.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 contract Params {
   struct BFactoryDeploymentParams {

src/contracts/BCoWConst.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 /**
  * @title BCoWConst

src/contracts/BCoWFactory.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BCoWPool} from './BCoWPool.sol';
 import {BFactory} from './BFactory.sol';

src/contracts/BCoWPool.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 /*
 

src/contracts/BConst.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 /**
  * @title BConst

src/contracts/BFactory.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BPool} from './BPool.sol';
 import {SafeERC20} from '@openzeppelin/contracts/token/ERC20/utils/SafeERC20.sol';

src/contracts/BMath.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BConst} from './BConst.sol';
 import {BNum} from './BNum.sol';

src/contracts/BNum.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BConst} from './BConst.sol';
 

src/contracts/BPool.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BMath} from './BMath.sol';
 import {BToken} from './BToken.sol';
@@ -30,6 +30,10 @@ contract BPool is BToken, BMath, IBPool {
   /// @dev Sum of all token weights
   uint256 internal _totalWeight;
 
+  /// TEST TEST TEST TEST TEST TEST TEST TEST
+  bytes32 internal _reenteringMutex;
+  /// TEST TEST TEST TEST TEST TEST TEST TEST
+
   /// @dev Logs the call data
   modifier _logs_() {
     emit LOG_CALL(msg.sig, msg.sender, msg.data);
@@ -148,8 +152,8 @@ contract BPool is BToken, BMath, IBPool {
 
     _pullUnderlying(token, msg.sender, balance);
   }
-
   /// @inheritdoc IBPool
+
   function unbind(address token) external _logs_ _lock_ _controller_ _notFinalized_ {
     if (!_records[token].bound) {
       revert BPool_TokenNotBound();
@@ -597,9 +601,10 @@ contract BPool is BToken, BMath, IBPool {
    * be interpreted as locked
    */
   function _setLock(bytes32 value) internal virtual {
-    assembly ("memory-safe") {
-      tstore(_MUTEX_TRANSIENT_STORAGE_SLOT, value)
-    }
+    // assembly ("memory-safe") {
+    //   tstore(_MUTEX_TRANSIENT_STORAGE_SLOT, value)
+    // }
+    _reenteringMutex = value;
   }
 
   /**
@@ -670,8 +675,9 @@ contract BPool is BToken, BMath, IBPool {
    * allowing calls
    */
   function _getLock() internal view virtual returns (bytes32 value) {
-    assembly ("memory-safe") {
-      value := tload(_MUTEX_TRANSIENT_STORAGE_SLOT)
-    }
+    // assembly ("memory-safe") {
+    //   value := tload(_MUTEX_TRANSIENT_STORAGE_SLOT)
+    // }
+    value = _reenteringMutex;
   }
 }

src/contracts/BToken.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {ERC20} from '@openzeppelin/contracts/token/ERC20/ERC20.sol';
 

src/interfaces/IBCoWFactory.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {IBFactory} from 'interfaces/IBFactory.sol';
 

src/interfaces/IBCoWPool.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {GPv2Order} from '@cowprotocol/libraries/GPv2Order.sol';
 import {IERC1271} from '@openzeppelin/contracts/interfaces/IERC1271.sol';

src/interfaces/IBFactory.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {IBPool} from 'interfaces/IBPool.sol';
 

src/interfaces/IBPool.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0-or-later
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {IERC20} from '@openzeppelin/contracts/token/ERC20/IERC20.sol';
 

src/interfaces/ISettlement.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: GPL-3.0
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {IERC20} from '@cowprotocol/interfaces/IERC20.sol';
 import {GPv2Interaction} from '@cowprotocol/libraries/GPv2Interaction.sol';

test/SUMMARY.md

@@ -0,0 +1,88 @@
+# Tests Summary
+
+There are 9 solidity files, totalling 939 sloc.
+
+| filename                      | language | code | comment | blank | total |
+| :---------------------------- | :------- | :--- | :------ | :---- | :---- |
+| src/contracts/BCoWConst.sol   | solidity | 4    | 10      | 2     | 16    |
+| src/contracts/BCoWFactory.sol | solidity | 20   | 13      | 7     | 40    |
+| src/contracts/BCoWPool.sol    | solidity | 90   | 41      | 24    | 155   |
+| src/contracts/BConst.sol      | solidity | 23   | 29      | 9     | 61    |
+| src/contracts/BFactory.sol    | solidity | 44   | 17      | 11    | 72    |
+| src/contracts/BMath.sol       | solidity | 128  | 156     | 18    | 302   |
+| src/contracts/BNum.sol        | solidity | 133  | 40      | 28    | 201   |
+| src/contracts/BPool.sol       | solidity | 473  | 104     | 107   | 684   |
+| src/contracts/BToken.sol      | solidity | 24   | 27      | 7     | 58    |
+
+
+## Interdependencies
+BCoWFactory deploys a bcowpool
+BCoWPool is a bpool which adds signature validation
+Factory deploys a pool and can "collect" from the pool
+Pool inherit btoken (which represents a LP) and bmath
+Bmath uses bnum
+
+# Unit tests
+Current coverage is XXX % for the 9 contracts, accross XXX tests. All tests are passing. Unit tests are writtent using the branched-tree technique and Bulloak as templating tool.
+
+< TABLE >
+
+# Integration tests
+
+# Property tests
+We identified 24 properties. We challenged these either in a long-running fuzzing campaign (targeting 23 of these in XXX runs) or via symbolic execution (for 8 properties).
+
+## Fuzzing campaign
+
+We used echidna to test these 23 properties. In addition to these, another fuzzing campaign as been led against the mathematical contracts (BNum and BMath), insuring the operation properties were holding. 
+
+Limitations/future improvements
+Currently, the swap logic are tested against the swap in/out functions (and, in a similar way, liquidity management via the join/exit function). The combined equivalent (joinswapExternAmountIn, joinswapPoolAmountOut, etc) should be tested too.
+
+## Formal verification: Symbolic Execution
+We managed to test 10 properties out of the 23. Properties not tested are either not easily challenged with symbolic execution (statefullness needed) or limited by Halmos itself (hitting loops in the implementation for instance).
+
+Additional properties from BNum were tested independently too (with severe limitations due to loop unrolling boundaries).
+
+
+## Notes
+The bmath corresponding equations are:
+
+`Spot price:`
+$\text{spotPrice} = \frac{\text{tokenBalanceIn}/\text{tokenWeightIn}}{\text{tokenBalanceOut}/\text{tokenWeightOut}} \cdot \frac{1}{1 - \text{swapFee}}$
+
+
+`Out given in:`
+$\text{tokenAmountOut} = \text{tokenBalanceOut} \cdot \left( 1 - \left( \frac{\text{tokenBalanceIn}}{\text{tokenBalanceIn} + \left( \text{tokenAmountIn} \cdot \left(1 - \text{swapFee}\right)\right)} \right)^{\frac{\text{tokenWeightIn}}{\text{tokenWeightOut}}} \right)$
+
+
+`In given out:`
+$\text{tokenAmountIn} = \frac{\text{tokenBalanceIn} \cdot \left( \frac{\text{tokenBalanceOut}}{\text{tokenBalanceOut} - \text{tokenAmountOut}} \right)^{\frac{\text{tokenWeightOut}}{\text{tokenWeightIn}}} - 1}{1 - \text{swapFee}}$
+
+
+`Pool out given single in`
+$\text{poolAmountOut} = \left(\frac{\text{tokenAmountIn} \cdot \left(1 - \left(1 - \frac{\text{tokenWeightIn}}{\text{totalWeight}}\right) \cdot \text{swapFee}\right) + \text{tokenBalanceIn}}{\text{tokenBalanceIn}}\right)^{\frac{\text{tokenWeightIn}}{\text{totalWeight}}} \cdot \text{poolSupply} - \text{poolSupply}$
+
+
+`Single in given pool out`
+$\text{tokenAmountIn} = \frac{\left(\frac{\text{poolSupply} + \text{poolAmountOut}}{\text{poolSupply}}\right)^{\frac{1}{\frac{\text{weightIn}}{\text{totalWeight}}}} \cdot \text{balanceIn} - \text{balanceIn}}{\left(1 - \frac{\text{weightIn}}{\text{totalWeight}}\right) \cdot \text{swapFee}}$
+
+
+`Single out given pool in`
+$\text{tokenAmountOut} = \left( \text{tokenBalanceOut} - \left( \frac{\text{poolSupply} - \left(\text{poolAmountIn} \cdot \left(1 - \text{exitFee}\right)\right)}{\text{poolSupply}} \right)^{\frac{1}{\frac{\text{tokenWeightOut}}{\text{totalWeight}}}} \cdot \text{tokenBalanceOut} \right) \cdot \left(1 - \left(1 - \frac{\text{tokenWeightOut}}{\text{totalWeight}}\right) \cdot \text{swapFee}\right)$
+
+
+`Pool in given single out`
+$\text{poolAmountIn} = \frac{\text{poolSupply} - \left( \frac{\text{tokenBalanceOut} - \frac{\text{tokenAmountOut}}{1 - \left(1 - \frac{\text{tokenWeightOut}}{\text{totalWeight}}\right) \cdot \text{swapFee}}}{\text{tokenBalanceOut}} \right)^{\frac{\text{tokenWeightOut}}{\text{totalWeight}}} \cdot \text{poolSupply}}{1 - \text{exitFee}}$
+
+
+BNum bpow is based on exponentiation by squaring and hold true because (see dapphub dsmath): https://github.com/dapphub/ds-math/blob/e70a364787804c1ded9801ed6c27b440a86ebd32/src/math.sol#L62
+```
+    //  If n is even, then x^n = (x^2)^(n/2).
+    //  If n is odd,  then x^n = x * x^(n-1),
+    //   and applying the equation for even x gives
+    //    x^n = x * (x^2)^((n-1) / 2).
+    //
+    //  Also, EVM division is flooring and
+    //    floor[(n-1) / 2] = floor[n / 2].
+```

test/integration/BCowPool.t.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BPoolIntegrationTest} from './BPool.t.sol';
 import {GPv2TradeEncoder} from '@composable-cow/test/vendored/GPv2TradeEncoder.sol';

test/integration/BPool.t.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {IERC20} from '@cowprotocol/interfaces/IERC20.sol';
 import {BFactory} from 'contracts/BFactory.sol';

test/integration/DeploymentGas.t.sol

@@ -1,5 +1,5 @@
 // SPDX-License-Identifier: MIT
-pragma solidity 0.8.25;
+pragma solidity 0.8.23;
 
 import {BFactory} from 'contracts/BFactory.sol';