feat(test): fuzzed and symbolic tests (#146)

* feat: echidna and halmos bmath bnum protocol * fix: remove tests halmos cannot handle * fix: setup cow pool * chore(wip): echidna * feat: clamp util * feat(echidna): prop and tob erc20 * test(echidna): protocol prop (part) * test(echidna): swap/join prop (part) * test(echidna): all properties * test(halmos): part * feat: summary prop md and last tests * chore: reorg * feat: more bnum pain * chore: format Co-authored-by: Weißer Hase <[email protected]> * chore: format Co-authored-by: Weißer Hase <[email protected]> * chore: typo Co-authored-by: Weißer Hase <[email protected]> * chore: typo Co-authored-by: Weißer Hase <[email protected]> * test(echidna): more bnum tests * chore: unused import * chore: more assert in protocol * feat: evm version * chore: summary * fix: direct transfer then swapExactOut case * chore: fmt * feat: shanghai in summary * fix: typo * chore: typo * chore: revert consistency * chore: summary fmt * chore: fmt * Fix/fuzz tests improvements (#178) * chore: fix linter setup * chore: update smocked files * chore: add missing spdx identifier * chore: add an npm script to run echidna tests * test: ensure SpotPriceAfterBelowSpotPriceBefore is never thrown * chore: fix natspec issues * test: ensure fuzz_joinExitPool body is runnable * chore: cleaning up fuzz (#179) * feat: creating BCoWPoolForTest to avoid modifying core contracts * fix: test:echidna script * fix: safeTransfer issue with echidna * chore: update test contract licenses * test: document property 25 * chore: remove unimplemented function --------- Co-authored-by: Weißer Hase <[email protected]> * chore: update forge snapshots * chore: update gas snapshots * chore: updating Properties document after merge * dev: improving bmath fuzz test (#184) * feat: improving bmath fuzz test * chore: updating Properties file * feat: adding min amount to test environment * test: ensure results are 0.1% from each other (#187) --------- Co-authored-by: teddy <[email protected]> * docs: update test summary (#189) * chore: fuzz sym fixes (#190) * test: deal with previously commented code * chore: pass name and symbol to ForTest contracts * fix: work around hevm not supporting mcopy * fix: remove unprovable property and replace it with two provable ones --------- Co-authored-by: Weißer Hase <[email protected]> Co-authored-by: teddy <[email protected]> Co-authored-by: Weißer Hase <[email protected]>
defi-wonderland · Aug 2, 2024 · 01e8f91 · 01e8f91
1 parent 67a6b41
commit 01e8f91
Show file tree

Hide file tree

Showing 24 changed files with 2,510 additions and 10 deletions.
diff --git a/.gitignore b/.gitignore
@@ -19,3 +19,7 @@ broadcast/*/*/*
 
 # Out dir
 out
+
+# echidna corpuses
+**/corpuses/*
+**/crytic-export/*
diff --git a/foundry.toml b/foundry.toml
@@ -17,7 +17,8 @@ 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]
+# 1878: Some imports don't have the license identifier
+ignored_error_codes = [2018, 2394, 5574, 3860, 1878]
 deny_warnings = true
 
 [profile.optimized]

diff --git a/package.json b/package.json
@@ -29,6 +29,7 @@
     "script:testnet": "forge script TestnetScript -vvvvv --rpc-url $SEPOLIA_RPC --broadcast --chain sepolia --private-key $SEPOLIA_DEPLOYER_PK --verify",
     "smock": "smock-foundry --contracts src/contracts",
     "test": "yarn test:integration && yarn test:unit",
+    "test:echidna": "find test/invariants/fuzz -regex '.*\\.t\\.sol$' |cut -d '/' -f 4 | cut -d . -f 1 |xargs -I{} echidna test/invariants/fuzz/{}.t.sol --contract Fuzz{} --config test/invariants/fuzz/{}.yaml",
     "test:integration": "forge test --ffi --match-path 'test/integration/**' -vvv --isolate",
     "test:local": "FOUNDRY_FUZZ_RUNS=100 forge test -vvv",
     "test:scaffold": "bulloak check --fix test/unit/**/*.tree && forge fmt",
@@ -42,6 +43,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",
     "cow-amm": "github:cowprotocol/cow-amm.git#6566128",
@@ -53,7 +55,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",

diff --git a/remappings.txt b/remappings.txt
@@ -7,6 +7,8 @@ cowprotocol/=node_modules/@cowprotocol/contracts/src/
 @composable-cow/=node_modules/composable-cow/
 @cow-amm/=node_modules/cow-amm/src
 lib/openzeppelin/=node_modules/@openzeppelin
+halmos-cheatcodes=node_modules/halmos-cheatcodes
+@crytic/=node_modules/@crytic/
 
 contracts/=src/contracts
 interfaces/=src/interfaces

diff --git a/src/contracts/BCoWPool.sol b/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);

diff --git a/src/contracts/BFactory.sol b/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();
     }

diff --git a/test/SUMMARY.md b/test/SUMMARY.md
@@ -0,0 +1,68 @@
+# 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)).
+By using `ForTest` contracts in for property tests (which avoid using transient storage and `mcopy`) we managed to make the tests run under Cancun.
+
+## 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).
+
+#### 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).
+
+### 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].
+```
diff --git a/test/invariants/.solhint.json b/test/invariants/.solhint.json
@@ -0,0 +1,13 @@
+{
+  "rules": {
+    "custom-errors": "off",
+    "no-empty-blocks":"off",
+    "reason-string": "off",
+    "reentrancy": "off",
+    "style-guide-casing": [ "warn", {
+      "ignoreVariables": true,
+      "ignorePublicFunctions": true,
+      "ignoreExternalFunctions": true
+    }]
+  }
+}
diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md
@@ -0,0 +1,94 @@
+| Properties                                                                                  | Type                | Id  | Halmos | Echidna |
+| ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
+| BFactory should always be able to deploy new pools                                          | Unit                | 1   | [x]    | [x]     |
+| BFactory's BDao should always be modifiable by the current BDao                             | Unit                | 2   | [x]    | [x]     |
+| BFactory should always be able to transfer the BToken to the BDao, 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]     |
+| 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]     |
+| BToken decreaseApproval should decrease the approval to max(old-amount, 0)*                 | Variable transition | 9   |        | [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  | :(     | #     |
+| ~~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  |        | [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]     |
+| Spot price after swap is always greater than before swap                                    | High level          | 25  |        | [x]     |
+
+> (*) Bundled with 24
+
+> (**) [Trail of Bits ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)
+
+<br>`[ ]` 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>`#` implemented but deprecated feature / property
+<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 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
+
+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)
+
+calcOutGivenIn should be inv with calcInGivenOut
+calcInGivenOut should be inv with calcOutGivenIn
+~~calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut~~
+~~calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut~~
diff --git a/test/invariants/fuzz/BMath.t.sol b/test/invariants/fuzz/BMath.t.sol
@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.25;
+
+import {EchidnaTest} from '../helpers/AdvancedTestsUtils.sol';
+import {BMath} from 'contracts/BMath.sol';
+
+contract FuzzBMath is EchidnaTest {
+  BMath bMath;
+
+  uint256 immutable MIN_WEIGHT;
+  uint256 immutable MAX_WEIGHT;
+  uint256 immutable MIN_FEE;
+  uint256 immutable MAX_FEE;
+
+  /**
+   * NOTE: These values were chosen to pass the fuzzing tests
+   * @dev Reducing BPOW_PRECISION may allow broader range of values increasing the gas cost
+   */
+  uint256 constant MAX_BALANCE = 1_000_000e18;
+  uint256 constant MIN_BALANCE = 100e18;
+  uint256 constant MIN_AMOUNT = 1e12;
+  uint256 constant TOLERANCE_PRECISION = 1e18;
+  uint256 constant MAX_TOLERANCE = 1e18 + 1e15; //0.1%
+
+  constructor() {
+    bMath = new BMath();
+
+    MIN_WEIGHT = bMath.MIN_WEIGHT();
+    MAX_WEIGHT = bMath.MAX_WEIGHT();
+    MIN_FEE = bMath.MIN_FEE();
+    MAX_FEE = bMath.MAX_FEE();
+  }
+
+  // calcOutGivenIn should be inverse of calcInGivenOut
+  function testCalcInGivenOut_InvCalcInGivenOut(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 tokenBalanceOut,
+    uint256 tokenWeightOut,
+    uint256 tokenAmountIn,
+    uint256 swapFee
+  ) public view {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    tokenWeightOut = clamp(tokenWeightOut, MIN_WEIGHT, MAX_WEIGHT);
+    tokenAmountIn = clamp(tokenAmountIn, MIN_AMOUNT, MAX_BALANCE);
+    tokenBalanceOut = clamp(tokenBalanceOut, MIN_BALANCE, MAX_BALANCE);
+    tokenBalanceIn = clamp(tokenBalanceIn, MIN_BALANCE, MAX_BALANCE);
+    swapFee = clamp(swapFee, MIN_FEE, MAX_FEE);
+
+    uint256 calc_tokenAmountOut =
+      bMath.calcOutGivenIn(tokenBalanceIn, tokenWeightIn, tokenBalanceOut, tokenWeightOut, tokenAmountIn, swapFee);
+
+    uint256 calc_tokenAmountIn =
+      bMath.calcInGivenOut(tokenBalanceIn, tokenWeightIn, tokenBalanceOut, tokenWeightOut, calc_tokenAmountOut, swapFee);
+
+    assert(
+      tokenAmountIn >= calc_tokenAmountIn
+        ? (tokenAmountIn * TOLERANCE_PRECISION / calc_tokenAmountIn) <= MAX_TOLERANCE
+        : (calc_tokenAmountIn * TOLERANCE_PRECISION / tokenAmountIn) <= MAX_TOLERANCE
+    );
+  }
+
+  // calcInGivenOut should be inverse of calcOutGivenIn
+  function testCalcOutGivenIn_InvCalcOutGivenIn(
+    uint256 tokenBalanceIn,
+    uint256 tokenWeightIn,
+    uint256 tokenBalanceOut,
+    uint256 tokenWeightOut,
+    uint256 tokenAmountOut,
+    uint256 swapFee
+  ) public view {
+    tokenWeightIn = clamp(tokenWeightIn, MIN_WEIGHT, MAX_WEIGHT);
+    tokenWeightOut = clamp(tokenWeightOut, MIN_WEIGHT, MAX_WEIGHT);
+    tokenAmountOut = clamp(tokenAmountOut, MIN_AMOUNT, MAX_BALANCE);
+    tokenBalanceOut = clamp(tokenBalanceOut, MIN_BALANCE, MAX_BALANCE);
+    tokenBalanceIn = clamp(tokenBalanceIn, MIN_BALANCE, MAX_BALANCE);
+    swapFee = clamp(swapFee, MIN_FEE, MAX_FEE);
+
+    uint256 calc_tokenAmountIn =
+      bMath.calcInGivenOut(tokenBalanceOut, tokenWeightOut, tokenBalanceIn, tokenWeightIn, tokenAmountOut, swapFee);
+
+    uint256 calc_tokenAmountOut =
+      bMath.calcOutGivenIn(tokenBalanceOut, tokenWeightOut, tokenBalanceIn, tokenWeightIn, calc_tokenAmountIn, swapFee);
+
+    assert(
+      tokenAmountOut >= calc_tokenAmountOut
+        ? (tokenAmountOut * TOLERANCE_PRECISION / calc_tokenAmountOut) <= MAX_TOLERANCE
+        : (calc_tokenAmountOut * TOLERANCE_PRECISION / tokenAmountOut) <= MAX_TOLERANCE
+    );
+  }
+}
diff --git a/test/invariants/fuzz/BMath.yaml b/test/invariants/fuzz/BMath.yaml
@@ -0,0 +1,7 @@
+# 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: false
+testLimit: 50000
+seqLen: 1