feat(test): fuzzed and symbolic tests

.solhintignore

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

package.json

@@ -50,7 +50,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,7 @@ 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
 
 contracts/=src/contracts
 interfaces/=src/interfaces

test/SUMMARY.md

@@ -0,0 +1,67 @@
+# Outline
+
+There are 7 files to cover (B(cow)Const are contracts containing public protocol-wide constants):
+BCoWFactory: deployer for cow pools
+BCoWPool: adding signature validation to BPool
+BFactory: deployer, approx 40sloc
+BMath: contract wrapping math logic
+BNum: contract wrapping arithmetic op
+BPool: the main contract, roughly 400sloc
+BToken: extends erc20
+
+## 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
+
+## Approach
+
+Echidna should be prioritized, then halmos should be particularly easy especially for the math libs, for which the implementations will be pretty similar.
+
+Then slither-mutate on the whole test base
+
+Setup for protocol-wide *looks* pretty simple (using the factory) - tbc
+
+## 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/invariant/AdvancedTestsUtils.sol

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.25;
+
+import {MockERC20} from 'forge-std/mocks/MockERC20.sol';
+import {SymTest} from 'halmos-cheatcodes/src/SymTest.sol';
+
+interface IHevm {
+  function prank(address) external;
+}
+
+contract FuzzERC20 is MockERC20 {
+  function mint(address _to, uint256 _amount) public {
+    _mint(_to, _amount);
+  }
+
+  function burn(address _from, uint256 _amount) public {
+    _burn(_from, _amount);
+  }
+}
+
+contract AgentsHandler {
+  uint256 internal agentsIndex;
+  address[] internal agents;
+
+  address internal currentCaller;
+
+  modifier AgentOrDeployer() {
+    uint256 _currentAgentIndex = agentsIndex;
+    currentCaller = _currentAgentIndex == 0 ? address(this) : agents[agentsIndex];
+    _;
+  }
+
+  constructor(uint256 _numAgents) {
+    for (uint256 i = 0; i < _numAgents; i++) {
+      agents.push(address(bytes20(keccak256(abi.encodePacked(i)))));
+    }
+  }
+
+  function nextAgent() public {
+    agentsIndex = (agentsIndex + 1) % agents.length;
+  }
+
+  function getCurrentAgent() public view returns (address) {
+    return agents[agentsIndex];
+  }
+}
+
+contract EchidnaTest is AgentsHandler {
+  event AssertionFailed();
+
+  IHevm hevm = IHevm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
+
+  constructor() AgentsHandler(5) {}
+
+  function clamp(uint256 _value, uint256 _min, uint256 _max) internal returns (uint256) {
+    return _min + (_value % (_max - _min));
+  }
+}
+
+contract HalmosTest is SymTest {}

test/invariant/PROPERTIES.md

@@ -0,0 +1,99 @@
+| Properties                                                                                  | Type                | Id  | Halmos | Echidna |
+| ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
+| BFactory should always be able to deploy new pools                                          | Unit                | 1   | [ ]    | [ ]     |
+| BFactory's blab should always be modifiable by the current blabs                            | Unit                | 2   | [ ]    | [ ]     |
+| BFactory should always be able to transfer the BToken to the blab, if called by it          | Unit                | 3   | [ ]    | [ ]     |
+| the amount received can never be less than min amount out                                   | Unit                | 4   | [ ]    | [ ]     |
+| the amount spent can never be greater than max amount in                                    | Unit                | 5   | [ ]    | [ ]     |
+| swap fee can only be 0 (cow pool)                                                           | Valid state         | 6   | [ ]    | [ ]     |
+| total weight can be up to 50e18                                                             | Variable transition | 7   | [ ]    | [ ]     |
+| BToken increaseApproval should increase the approval of the address by the amount           | Variable transition | 8   | [ ]    | [ ]     |
+| BToken decreaseApproval should decrease the approval to max(old-amount, 0)                  | Variable transition | 9   | [ ]    | [ ]     |
+| a pool can either be finalized or not finalized                                             | Valid state         | 10  | [ ]    | [ ]     |
+| a finalized pool cannot switch back to non-finalized                                        | State transition    | 11  | [ ]    | [ ]     |
+| a non-finalized pool can only be finalized when the controller calls finalize()             | State transition    | 12  | [ ]    | [ ]     |
+| an exact amount in should always earn the amount out calculated in bmath                    | High level          | 13  | [ ]    | [ ]     |
+| an exact amount out is earned only if the amount in calculated in bmath is transfered       | High level          | 14  | [ ]    | [ ]     |
+| there can't be any amount out for a 0 amount in                                             | High level          | 15  | [ ]    | [ ]     |
+| the pool btoken can only be minted/burned in the join and exit operations                   | High level          | 16  | [ ]    | [ ]     |
+| a direct token transfer can never reduce the underlying amount of a given token per BPT     | High level          | 17  | [ ]    | [ ]     |
+| the amount of underlying token when exiting should always be the amount calculated in bmath | High level          | 18  | [ ]    | [ ]     |
+| a swap can only happen when the pool is finalized                                           | High level          | 19  | [ ]    | [ ]     |
+| bounding and unbounding token can only be done on a non-finalized pool, by the controller   | High level          | 20  | [ ]    | [ ]     |
+| there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool        | High level          | 21  | [ ]    | [ ]     |
+| only the settler can commit a hash                                                          | High level          | 22  | [ ]    | [ ]     |
+| 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  | [ ]    | [ ]     |
+
+* ERC20 properties
+(https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
+
+# Unit 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
+0 should be identity for badd
+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
+1 should be identity for bmul
+0 should be absorbing for mul
+bmul result should always be gte a and b
+
+bdiv should be bmul reverse operation // <-- unsolved
+1 should be identity for bdiv
+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)
+
+
+bpowApprox
+
+calcOutGivenIn
+
+calcOutGivenIn should be inv with calcInGivenOut
+
+calcInGivenOut
+
+calcPoolOutGivenSingleIn
+
+calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut
+
+calcSingleInGivenPoolOut
+
+calcSingleOutGivenPoolIn
+
+calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut
+
+calcPoolInGivenSingleOut

test/invariant/fuzz/config.yaml

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

test/invariant/fuzz/external/MockSettler.sol

@@ -0,0 +1,21 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity 0.8.25;
+
+import {GPv2Interaction, GPv2Trade, IERC20, ISettlement} from 'interfaces/ISettlement.sol';
+
+contract MockSettler is ISettlement {
+  function domainSeparator() external view override returns (bytes32) {
+    return bytes32(hex'1234');
+  }
+
+  function vaultRelayer() external view override returns (address) {
+    return address(123);
+  }
+
+  function settle(
+    IERC20[] calldata tokens,
+    uint256[] calldata clearingPrices,
+    GPv2Trade.Data[] calldata trades,
+    GPv2Interaction.Data[][3] calldata interactions
+  ) external {}
+}