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

@@ -12,12 +12,13 @@ sort_imports = true
 solc_version = '0.8.25'
 libs = ["node_modules", "lib"]
 optimizer_runs = 500
-evm_version = 'cancun'
+evm_version = 'shanghai'
 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

src/contracts/BPool.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;
   }
 }

test/SUMMARY.md

@@ -0,0 +1,69 @@
+# Tests Summary 
+
+## Warning
+The repo is using solc 0.8.25, which compiles to the Cancun EVM version by default. Unfortunately, the hevm has no implementation of this EVM version ([or not yet](https://github.com/ethereum/hevm/issues/469#issuecomment-2220677206)).
+Solc using a mcopy opcode somewhere, the property tests are run on Shanghai for now (at least until the hevm catches up), preventing this branch to be merged with the main one.
+
+## Unit tests
+Our unit tests are covering every branches, using the branched-tree technique with [Bulloak](https://github.com/alexfertel/bulloak).
+
+## Integration tests
+Integration tests are covering various happy paths and not-so-happy paths, on a mainnet fork.
+
+## Property tests
+We identified 24 properties. We challenged these either in a long-running fuzzing campaign or via symbolic execution (for 8 chosen 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). BMath properties are currently not triggered in CI, due to various rounding errors, and should be further validated.
+
+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.
+BMath properties are currently not tested and should be refactored to quantify the rounding errors.
+
+### 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 loop unrolling boundaries in the implementation for instance).
+
+Additional properties from BNum were tested independently too (with severe limitations due to previously mentionned 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/invariants/PROPERTIES.md

@@ -0,0 +1,91 @@
+| Properties                                                                                  | Type                | Id  | Halmos | Echidna |
+| ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
+| BFactory should always be able to deploy new pools                                          | Unit                | 1   | [x]    | [x]     |
+| BFactory's blab should always be modifiable by the current blabs                            | Unit                | 2   | [x]    | [x]     |
+| BFactory should always be able to transfer the BToken to the blab, if called by it          | Unit                | 3   | [x]    | [x]     |
+| the amount received can never be less than min amount out                                   | Unit                | 4   | :(     | [x]     |
+| the amount spent can never be greater than max amount in                                    | Unit                | 5   | :(     | [x]     |
+| swap fee can only be 0 (cow pool)                                                           | Valid state         | 6   | [x]    | [x]     |
+| total weight can be up to 50e18                                                             | Variable transition | 7   | [x]    | [x]     |
+| BToken increaseApproval should increase the approval of the address by the amount*          | Variable transition | 8   | [x]    | [x]     |
+| BToken decreaseApproval should decrease the approval to max(old-amount, 0)*                 | Variable transition | 9   | [x]    | [x]     |
+| a pool can either be finalized or not finalized                                             | Valid state         | 10  |        | [x]     |
+| a finalized pool cannot switch back to non-finalized                                        | State transition    | 11  |        | [x]     |
+| a non-finalized pool can only be finalized when the controller calls finalize()             | State transition    | 12  | [x]    | [x]     |
+| an exact amount in should always earn the amount out calculated in bmath                    | High level          | 13  | :(     | [x]     |
+| an exact amount out is earned only if the amount in calculated in bmath is transfered       | High level          | 14  | :(     | [x]     |
+| there can't be any amount out for a 0 amount in                                             | High level          | 15  | :(     | [x]     |
+| the pool btoken can only be minted/burned in the join and exit operations                   | High level          | 16  |        | [x]     |
+| a direct token transfer can never reduce the underlying amount of a given token per BPT     | High level          | 17  | :(     | [x]     |
+| the amount of underlying token when exiting should always be the amount calculated in bmath | High level          | 18  | :(     | [x]     |
+| a swap can only happen when the pool is finalized                                           | High level          | 19  |        | [x]     |
+| bounding and unbounding token can only be done on a non-finalized pool, by the controller   | High level          | 20  | [x]    | [x]     |
+| there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool        | High level          | 21  |        | [x]     |
+| only the settler can commit a hash                                                          | High level          | 22  | [x]    | [x]     |
+| when a hash has been commited, only this order can be settled                               | High level          | 23  | [ ]    | [ ]     |
+| BToken should not break the ToB ERC20 properties**                                          | High level          | 24  |        | [x]     |
+
+> (*) Bundled with 24
+
+> (**) [Trail of Bits ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
+
+[ ] planed to implement and still to do
+<br>[x] implemented and tested 
+<br>:( implemented but test not passing due to an external factor (tool limitation - eg halmos max unrolling loop, etc) 
+<br>empty not implemented and will not be (design, etc)
+
+# Unit-test properties for the math libs (BNum and BMath):
+
+btoi should always return the floor(a / BONE) == (a - a%BONE) / BONE
+
+bfloor should always return (a - a % BONE)
+
+badd should be commutative
+badd should be associative
+badd should have 0 as identity
+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 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
+
+bmul should be commutative
+bmul should be associative
+bmul should be distributive
+bmul should have 1 as identity
+bmul should have 0 as absorving
+bmul result should always be gte a and b
+
+bdiv should be bmul reverse operation // <-- unsolved
+bdiv should have 1 as identity
+bdiv should revert if b is 0 // <-- impl with wrapper to have low lvl call
+bdiv result should be lte a
+
+bpowi should return 1 if exp is 0
+0 should be absorbing if base
+1 should be identity if base
+1 should be identity if exp
+bpowi should be distributive over mult of the same base x^a * x^b == x^(a+b)
+bpowi should be distributive over mult of the same exp  a^x * b^x == (a*b)^x
+power of a power should mult the exp (x^a)^b == x^(a*b)
+
+bpow should return 1 if exp is 0
+0 should be absorbing if base
+1 should be identity if base
+1 should be identity if exp
+bpow should be distributive over mult of the same base x^a * x^b == x^(a+b)
+bpow should be distributive over mult of the same exp  a^x * b^x == (a*b)^x
+power of a power should mult the exp (x^a)^b == x^(a*b)
+
+## Untested (precision issues in test settingsq)
+calcOutGivenIn should be inv with calcInGivenOut
+calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut
+calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut

test/invariants/fuzz/BMath.t.sol.invalid

@@ -0,0 +1,98 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.25;
+
+import {EchidnaTest} from '../helpers/AdvancedTestsUtils.sol';
+
+import {BMath} from 'contracts/BMath.sol';
+
+contract FuzzBMath is BMath, EchidnaTest {
+  // calcOutGivenIn should be inverse of calcInGivenOut
+  function testCalcInGivenOut_InvCalcInGivenOut(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 tokenBalanceOut,
+    uint256 tokenWeightOut,
+    uint256 tokenAmountIn,
+    uint256 swapFee
+  ) public {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    tokenWeightOut = clamp(tokenWeightOut, MIN_WEIGHT, MAX_WEIGHT);
+    tokenAmountIn = clamp(tokenAmountIn, 1 ether, 10 ether);
+    tokenBalanceOut = clamp(tokenBalanceOut, 1 ether, 10 ether);
+    tokenBalanceIn = clamp(tokenBalanceIn, 1 ether, 10 ether);
+    swapFee = clamp(swapFee, MIN_FEE, MAX_FEE);
+
+    uint256 calc_tokenAmountOut =
+      calcOutGivenIn(tokenBalanceIn, tokenWeightIn, tokenBalanceOut, tokenWeightOut, tokenAmountIn, swapFee);
+
+    uint256 calc_tokenAmountIn =
+      calcInGivenOut(tokenBalanceOut, tokenWeightOut, tokenBalanceIn, tokenWeightIn, calc_tokenAmountOut, swapFee);
+
+    assert(tokenAmountIn == calc_tokenAmountIn || tokenAmountIn > calc_tokenAmountIn ? tokenAmountIn - calc_tokenAmountIn < BONE : calc_tokenAmountIn - tokenAmountIn < BONE);
+  }
+
+  // calcInGivenOut should be inverse of calcOutGivenIn
+  function testCalcOutGivenIn_InvCalcOutGivenIn(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 tokenBalanceOut,
+    uint256 tokenWeightOut,
+    uint256 tokenAmountOut,
+    uint256 swapFee
+  ) public {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    tokenWeightOut = clamp(tokenWeightOut, MIN_WEIGHT, MAX_WEIGHT);
+
+    uint256 calc_tokenAmountIn =
+      calcInGivenOut(tokenBalanceOut, tokenWeightOut, tokenBalanceIn, tokenWeightIn, tokenAmountOut, swapFee);
+
+    uint256 calc_tokenAmountOut =
+      calcOutGivenIn(tokenBalanceIn, tokenWeightIn, tokenBalanceOut, tokenWeightOut, calc_tokenAmountIn, swapFee);
+
+    assert(tokenAmountOut == calc_tokenAmountOut);
+  }
+
+  // calcSingleInGivenPoolOut should be inverse of calcPoolOutGivenSingleIn
+  function testCalcSingleInGivenPoolOut_InvCalcPoolOutGivenSingle(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 poolSupply,
+    uint256 totalWeight,
+    uint256 tokenAmountOut,
+    uint256 swapFee
+  ) public {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    totalWeight = clamp(totalWeight, MIN_WEIGHT, MAX_TOTAL_WEIGHT);
+    tokenBalanceIn = clamp(tokenBalanceIn, 1, type(uint256).max);
+
+    uint256 calc_tokenAmountIn =
+      calcSingleInGivenPoolOut(tokenBalanceIn, tokenWeightIn, poolSupply, totalWeight, tokenAmountOut, swapFee);
+
+    uint256 calc_poolAmountOut =
+      calcPoolOutGivenSingleIn(tokenBalanceIn, tokenWeightIn, poolSupply, totalWeight, calc_tokenAmountIn, swapFee);
+
+    assert(tokenAmountOut == calc_poolAmountOut);
+  }
+
+  // calcPoolOutGivenSingleIn should be inverse of calcSingleInGivenPoolOut
+  function testCalcPoolOutGivenSingle_InvCalcSingleInGivenPoolOut(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 poolSupply,
+    uint256 totalWeight,
+    uint256 poolAmountOut,
+    uint256 swapFee
+  ) public {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    totalWeight = clamp(totalWeight, MIN_WEIGHT, MAX_TOTAL_WEIGHT);
+    tokenBalanceIn = clamp(tokenBalanceIn, 1, type(uint256).max);
+
+    uint256 calc_poolAmountIn =
+      calcPoolOutGivenSingleIn(tokenBalanceIn, tokenWeightIn, poolSupply, totalWeight, poolAmountOut, swapFee);
+
+    uint256 calc_tokenAmountOut =
+      calcSingleInGivenPoolOut(tokenBalanceIn, tokenWeightIn, poolSupply, totalWeight, calc_poolAmountIn, swapFee);
+
+    assert(poolAmountOut == calc_tokenAmountOut);
+  }
+}

test/invariants/fuzz/BMath.yaml

@@ -0,0 +1,6 @@
+# https://github.com/crytic/echidna/blob/master/tests/solidity/basic/default.yaml for more options
+testMode: assertion
+corpusDir: test/invariants/fuzz/corpuses/BMath/
+coverageFormats: ["html","lcov"]
+allContracts: true
+testLimit: 50000