From 0d0ca16d956032e2d42a189aac9cc4f1db2589e6 Mon Sep 17 00:00:00 2001 From: drgorillamd <83670532+drgorillamd@users.noreply.github.com> Date: Tue, 16 Jul 2024 11:41:14 +0200 Subject: [PATCH] feat: summary prop md and last tests --- test/SUMMARY.md | 46 ++-- test/invariants/PROPERTIES.md | 74 +++--- test/invariants/symbolic/BMath.t.sol | 32 --- test/invariants/symbolic/BNum.t.sol | 218 ----------------- test/invariants/symbolic/Protocol.t.sol | 298 ++++++------------------ 5 files changed, 139 insertions(+), 529 deletions(-) delete mode 100644 test/invariants/symbolic/BMath.t.sol diff --git a/test/SUMMARY.md b/test/SUMMARY.md index e37a2331..098dce15 100644 --- a/test/SUMMARY.md +++ b/test/SUMMARY.md @@ -1,13 +1,19 @@ -# Outline +# 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 | -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 @@ -16,15 +22,27 @@ Factory deploys a pool and can "collect" from the pool Pool inherit btoken (which represents a LP) and bmath Bmath uses bnum -## Approach +# 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 -Echidna should be prioritized, then halmos should be particularly easy especially for the math libs, for which the implementations will be pretty similar. +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. -Then slither-mutate on the whole test base +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. -Setup for protocol-wide *looks* pretty simple (using the factory) - tbc +## 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). -nb 14 means if token in == token out, people just give tokens to the pool, intended? +Additional properties from BNum were tested independently too (with severe limitations due to loop unrolling boundaries). ## Notes diff --git a/test/invariants/PROPERTIES.md b/test/invariants/PROPERTIES.md index 5d0377d4..96a17439 100644 --- a/test/invariants/PROPERTIES.md +++ b/test/invariants/PROPERTIES.md @@ -1,36 +1,41 @@ | Properties | Type | Id | Halmos | Echidna | | ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- | -| BFactory should always be able to deploy new pools | Unit | 1 | [ ] | [x] | -| BFactory's blab should always be modifiable by the current blabs | Unit | 2 | [ ] | [x] | -| BFactory should always be able to transfer the BToken to the blab, if called by it | Unit | 3 | [ ] | [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] | -| 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] | -| 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] | -| 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] | -| 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] | +| 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 ** ERC20 properties (https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) -# Unit for the math libs (BNum and BMath): +[ ] planed to implement and still to do +
[x] implemented and tested +
:( implemented but judged as incorrect (tool limitation, etc) +
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) @@ -79,23 +84,6 @@ 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 \ No newline at end of file +calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut \ No newline at end of file diff --git a/test/invariants/symbolic/BMath.t.sol b/test/invariants/symbolic/BMath.t.sol deleted file mode 100644 index e98f6aad..00000000 --- a/test/invariants/symbolic/BMath.t.sol +++ /dev/null @@ -1,32 +0,0 @@ -// SPDX-License-Identifier: UNLICENSED -pragma solidity 0.8.23; - -import {HalmosTest} from '../helpers/AdvancedTestsUtils.sol'; -import {BMath} from 'contracts/BMath.sol'; - -contract SymbolicBMath is BMath, HalmosTest { -// todo crashes (pow -> loop...) -// calcOutGivenIn should be inv with calcInGivenOut -// function check_calcOutGivenInEquiv() public { -// uint256 tokenBalanceIn = svm.createUint256('tokenBalanceIn'); -// uint256 tokenWeightIn = svm.createUint256('tokenWeightIn'); -// uint256 tokenBalanceOut = svm.createUint256('tokenBalanceOut'); -// uint256 tokenWeightOut = svm.createUint256('tokenWeightOut'); -// uint256 tokenAmountIn = svm.createUint256('tokenAmountIn'); -// uint256 swapFee = svm.createUint256('swapFee'); - -// vm.assume(tokenWeightIn != 0); -// vm.assume(tokenWeightOut != 0); -// vm.assume(tokenAmountIn != 0); -// vm.assume(tokenBalanceIn > BONE - swapFee); - -// uint256 tokenAmountOut = calcOutGivenIn(tokenBalanceIn, tokenWeightIn, tokenBalanceOut, tokenWeightOut, tokenAmountIn, swapFee); -// vm.assume(tokenAmountOut != tokenBalanceOut); - -// uint256 tokenAmountIn2 = calcInGivenOut(tokenBalanceOut, tokenWeightOut, tokenBalanceIn, tokenWeightIn, tokenAmountOut, swapFee); - -// assert(tokenAmountIn == tokenAmountIn2); -// } -// calcPoolOutGivenSingleIn should be inv with calcSingleInGivenPoolOut -// calcSingleOutGivenPoolIn should be inv with calcPoolInGivenSingleOut -} diff --git a/test/invariants/symbolic/BNum.t.sol b/test/invariants/symbolic/BNum.t.sol index 1d7b6c61..122f0eec 100644 --- a/test/invariants/symbolic/BNum.t.sol +++ b/test/invariants/symbolic/BNum.t.sol @@ -10,7 +10,6 @@ contract SymbolicBNum is BNum, HalmosTest { ///////////////////////////////////////////////////////////////////// // btoi should always return the floor(a / BONE) == (a - a%BONE) / BONE - // TODO: Too tightly coupled function check_btoi_alwaysFloor(uint256 _input) public pure { // action uint256 _result = btoi(_input); @@ -149,13 +148,6 @@ contract SymbolicBNum is BNum, HalmosTest { assert(_result <= _a); } - // todo - // bsub should alway revert if b > a (duplicate with previous tho) - function check_bsub_revert(uint256 _a, uint256 _b) public pure { - vm.assume(_b > _a); - //bsub(_a, _b); - } - ///////////////////////////////////////////////////////////////////// // Bnum::bsubSign // ///////////////////////////////////////////////////////////////////// @@ -210,43 +202,6 @@ contract SymbolicBNum is BNum, HalmosTest { assert(_result1 == _result2); } - //todo hangs - // bmul should be associative - function testCheck_bmul_associative(uint256 _a, uint256 _b, uint256 _c) public pure { - // precondition - if (_b != 0) vm.assume(_a < type(uint256).max / _b); // Avoid mul overflow - if (_c != 0) vm.assume(_b < type(uint256).max / _c); // Avoid mul overflow - vm.assume(_a * _b + _c / 2 < type(uint256).max); // Avoid add overflow - - vm.assume(_a >= BONE); - vm.assume(_b >= BONE); - vm.assume(_c >= BONE); - - // action - uint256 _result1 = bmul(bmul(_a, _b), _c); - uint256 _result2 = bmul(_a, bmul(_b, _c)); - - // post condition - // assert(_result1 == _result2); - assertApproxEqAbs(_result1, _result2, 10 * BONE); - } - - //todo hangs - // bmul should be distributive - // function check_bmul_distributive(uint256 _a, uint256 _b, uint256 _c) public pure { - // uint256 _result1 = bmul(_a, badd(_b, _c)); - // uint256 _result2 = badd(bmul(_a, _b), bmul(_a, _c)); - // assert(_result1 == _result2); - // } - - //todo - // 1 should be identity for bmul - // function check_bmul_identity(uint256 _a) public pure { - // vm.assume(_a < type(uint256).max / BONE); // Avoid mul overflow - // uint256 _result = bmul(_a, BONE); - // assert(_result == _a); - // } - // 0 should be absorbing for mul function check_bmul_absorbing(uint256 _a) public pure { // action @@ -256,95 +211,6 @@ contract SymbolicBNum is BNum, HalmosTest { assert(_result == 0); } - //todo hangs - // bmul result should always be gte a and b - // function check_bmul_resultGTE(uint256 _a, uint256 _b) public pure { - // vm.assume(_a != 0 && _b != 0); // Avoid absorbing - // vm.assume(_a < type(uint256).max / BONE); // Avoid mul overflow - // vm.assume(_b < type(uint256).max / BONE); // Avoid mul overflow - // vm.assume(_a * BONE + _b / 2 < type(uint256).max); // Avoid add overflow - - // uint256 _result = bmul(_a, _b); - // assert(_result >= _a); - // assert(_result >= _b); - // } - - ///////////////////////////////////////////////////////////////////// - // Bnum::bdiv // - ///////////////////////////////////////////////////////////////////// - - //todo: Halmos times out vs foundry passes - // 1 should be identity for bdiv - // function check_bdiv_identity(uint256 _a) public pure { - // vm.assume(_a < type(uint256).max / BONE); // Avoid add overflow - // uint256 _result = bdiv(_a, BONE); - // assert(_result == _a); - // } - - // uint256[] public fixtureA = [ - // BONE, - // BONE * 2, - // BONE / 2, - // BONE * 2 - 1, - // BONE * 2 + 1, - // BONE / 2 - 1, - // BONE / 2 + 1, - // BONE * 3, - // BONE * 4, - // BONE * 5, - // BONE * 6, - // BONE * 7, - // BONE * 8, - // BONE * 9, - // BONE * 10, - // type(uint256).max / 10**18, - // type(uint256).max / 10**18 - 1, - // type(uint256).max / 10**18 - 10, - // type(uint256).max / 10**18 - BONE / 2, - // type(uint256).max / 10**18 - BONE / 2 + 1, - // type(uint256).max / 10**18 - BONE / 2 - 1, - // type(uint256).max / 10**18 - BONE / 2 - 10, - // 0, - // 1, - // 2 - // ]; - - // /// forge-config: default.fuzz.runs = 1000000 - // function test_bdiv_identity(uint256 a) public pure { - // a = bound(a, 0, type(uint256).max / 10**18); - // uint256 _result = bdiv(a, BONE); - // assertEq(_result, a); - // } - - //todo - // bdiv should revert if b is 0 - // function check_bdiv_revert(uint256 _a) public pure { - // } - - //todo hangs - // bdiv result should be lte a - function test_bdiv_resultLTE(uint256 _a, uint256 _b) public pure { - vm.assume(_b != 0); - vm.assume(_a < type(uint256).max / BONE); // Avoid mul overflow - //todo: overconstrained next line? Too tightly coupled? - vm.assume(_a * BONE + _b / 2 < type(uint256).max); // Avoid add overflow - - uint256 _result = bdiv(_a, _b); - assert(_result <= _a * BONE); - assertLe(_result, _a * BONE); - } - - //todo hangs - // bdiv should be bmul reverse operation - // function check_bdiv_bmul(uint256 _a, uint256 _b) public pure { - // vm.assume(_b > 0); - // vm.assume(_a > _b); // todo: overconstrained? - - // uint256 _bdivResult = bdiv(_a, _b); - // uint256 _result = bmul(_bdivResult, _b); - // assert(_result == _a); - // } - ///////////////////////////////////////////////////////////////////// // Bnum::bpowi // ///////////////////////////////////////////////////////////////////// @@ -358,52 +224,6 @@ contract SymbolicBNum is BNum, HalmosTest { assert(_result == BONE); } - //todo echidna (loop unrolling bound hit) - // 0 should be absorbing if base - // function check_bpowi_absorbingBase(uint256 _exp) public pure { - // vm.assume(_exp != 0); // Consider 0^0 as undetermined - - // uint256 _result = bpowi(0, _exp); - // assert(_result == 0); - // } - - //todo echidna (loop unrolling bound hit) - // 1 should be identity if base - // function check_bpowi_identityBase(uint256 _exp) public pure { - // uint256 _result = bpowi(BONE, _exp); - // assert(_result == BONE); - // } - - //todo echidna (loop unrolling bound hit) - // 1 should be identity if exp - // function check_bpowi_identityExp(uint256 _base) public pure { - // uint256 _result = bpowi(_base, BONE); - // assert(_result == _base); - // } - - /** - * // bpowi should be distributive over mult of the same base x^a * x^b == x^(a+b) - * function check_bpowi_distributiveBase(uint256 _base, uint256 _a, uint256 _b) public pure { - * uint256 _result1 = bpowi(_base, badd(_a, _b)); - * uint256 _result2 = bmul(bpowi(_base, _a), bpowi(_base, _b)); - * assert(_result1 == _result2); - * } - * - * // bpowi should be distributive over mult of the same exp a^x * b^x == (a*b)^x - * function check_bpowi_distributiveExp(uint256 _a, uint256 _b, uint256 _exp) public pure { - * uint256 _result1 = bpowi(bmul(_a, _b), _exp); - * uint256 _result2 = bmul(bpowi(_a, _exp), bpowi(_b, _exp)); - * assert(_result1 == _result2); - * } - * - * // power of a power should mult the exp (x^a)^b == x^(a*b) - * function check_bpowi_powerOfPower(uint256 _base, uint256 _a, uint256 _b) public pure { - * uint256 _result1 = bpowi(bpowi(_base, _a), _b); - * uint256 _result2 = bpowi(_base, bmul(_a, _b)); - * assert(_result1 == _result2); - * } - */ - ///////////////////////////////////////////////////////////////////// // Bnum::bpow // ///////////////////////////////////////////////////////////////////// @@ -417,20 +237,6 @@ contract SymbolicBNum is BNum, HalmosTest { assert(_result == BONE); } - //todo min base is 1wei -> can never be 0 instead (echidna) - // 0 should be absorbing if base - // function check_bpow_absorbingBase(uint256 _exp) public pure { - // uint256 _result = bpow(0, _exp); - // assert(_result == 0); - // } - - //todo echidna (loop unrolling bound hit) - // 1 should be identity if base - // function check_bpow_identityBase(uint256 _exp) public pure { - // uint256 _result = bpow(BONE, _exp); - // assert(_result == BONE); - // } - // 1 should be identity if exp function check_bpow_identityExp(uint256 _base) public pure { // action @@ -439,28 +245,4 @@ contract SymbolicBNum is BNum, HalmosTest { // post condition assert(_result == _base); } - - //todo infinite loop - // bpow should be distributive over mult of the same base x^a * x^b == x^(a+b) - // function check_bpow_distributiveBase(uint256 _base, uint256 _a, uint256 _b) public pure { - // uint256 _result1 = bpow(_base, badd(_a, _b)); - // uint256 _result2 = bmul(bpow(_base, _a), bpow(_base, _b)); - // assert(_result1 == _result2); - // } - - //todo loop - // bpow should be distributive over mult of the same exp a^x * b^x == (a*b)^x - // function check_bpow_distributiveExp(uint256 _a, uint256 _b, uint256 _exp) public pure { - // uint256 _result1 = bpow(bmul(_a, _b), _exp); - // uint256 _result2 = bmul(bpow(_a, _exp), bpow(_b, _exp)); - // assert(_result1 == _result2); - // } - - // todo - // // power of a power should mult the exp (x^a)^b == x^(a*b) - // function check_bpow_powerOfPower(uint256 _base, uint256 _a, uint256 _b) public pure { - // uint256 _result1 = bpow(bpow(_base, _a), _b); - // uint256 _result2 = bpow(_base, bmul(_a, _b)); - // assert(_result1 == _result2); - // } } diff --git a/test/invariants/symbolic/Protocol.t.sol b/test/invariants/symbolic/Protocol.t.sol index bb9619e6..69c6b360 100644 --- a/test/invariants/symbolic/Protocol.t.sol +++ b/test/invariants/symbolic/Protocol.t.sol @@ -5,9 +5,11 @@ import {FuzzERC20, HalmosTest} from '../helpers/AdvancedTestsUtils.sol'; import {MockSettler} from '../helpers/MockSettler.sol'; import {BCoWFactory, BCoWPool, IBPool} from 'contracts/BCoWFactory.sol'; + import {BConst} from 'contracts/BConst.sol'; import {BMath} from 'contracts/BMath.sol'; import {BNum} from 'contracts/BNum.sol'; +import {BToken} from 'contracts/BToken.sol'; contract HalmosBalancer is HalmosTest { // System under test @@ -23,6 +25,7 @@ contract HalmosBalancer is HalmosTest { BCoWPool pool; address currentCaller = svm.createAddress('currentCaller'); + // address currentCaller = address(234); constructor() { solutionSettler = address(new MockSettler()); @@ -107,120 +110,10 @@ contract HalmosBalancer is HalmosTest { assert(_currentBLab != currentCaller); } } - - /// @custom:property-id 4 - /// @custom:property the amount received can never be less than min amount out - /// @custom:property-id 13 - /// @custom:property an exact amount in should always earn the amount out calculated in bmath - /// @custom:property-id 15 - /// @custom:property there can't be any amount out for a 0 amount in - /// @custom:property-id 19 - /// @custom:property a swap can only happen when the pool is finalized - function skipped_swapExactIn(uint256 _minAmountOut, uint256 _amountIn, uint256 _tokenIn, uint256 _tokenOut) public { - // Preconditions - vm.assume(_tokenIn < tokens.length); - vm.assume(_tokenOut < tokens.length); - vm.assume(_tokenIn != _tokenOut); // todo: dig this, it should pass without this precondition - - tokens[_tokenIn].mint(currentCaller, _amountIn); - - vm.prank(currentCaller); - tokens[_tokenIn].approve(address(pool), type(uint256).max); // approval isn't limiting - - uint256 _balanceOutBefore = tokens[_tokenOut].balanceOf(currentCaller); - - uint256 _outComputed = bmath.calcOutGivenIn( - tokens[_tokenIn].balanceOf(address(pool)), - pool.getDenormalizedWeight(address(tokens[_tokenIn])), - tokens[_tokenOut].balanceOf(address(pool)), - pool.getDenormalizedWeight(address(tokens[_tokenOut])), - _amountIn, - bconst.MIN_FEE() - ); - - vm.prank(currentCaller); - - // Action - try pool.swapExactAmountIn( - address(tokens[_tokenIn]), _amountIn, address(tokens[_tokenOut]), _minAmountOut, type(uint256).max - ) { - // Postcondition - uint256 _balanceOutAfter = tokens[_tokenOut].balanceOf(currentCaller); - - // 13 - assert(_balanceOutAfter - _balanceOutBefore == _outComputed); - - // 4 - if (_amountIn != 0) assert(_balanceOutBefore <= _balanceOutAfter + _minAmountOut); - // 15 - else assert(_balanceOutBefore == _balanceOutAfter); - - // 19 - assert(pool.isFinalized()); - } catch {} - } - - /// @custom:property-id 5 - /// @custom:property the amount spent can never be greater than max amount in - /// @custom:property-id 14 - /// @custom:property an exact amount out is earned only if the amount in calculated in bmath is transfere - /// @custom:property-id 15 - /// @custom:property there can't be any amount out for a 0 amount in - /// @custom:property-id 19 - /// @custom:property a swap can only happen when the pool is finalized - function skipped_swapExactOut(uint256 _maxAmountIn, uint256 _amountOut, uint256 _tokenIn, uint256 _tokenOut) public { - // Precondition - vm.assume(_tokenIn < tokens.length); - vm.assume(_tokenOut < tokens.length); - - tokens[_tokenIn].mint(currentCaller, _maxAmountIn); - - vm.prank(currentCaller); - tokens[_tokenIn].approve(address(pool), type(uint256).max); // approval isn't limiting - - uint256 _balanceInBefore = tokens[_tokenIn].balanceOf(currentCaller); - uint256 _balanceOutBefore = tokens[_tokenOut].balanceOf(currentCaller); - - uint256 _inComputed = bmath.calcInGivenOut( - tokens[_tokenIn].balanceOf(address(pool)), - pool.getDenormalizedWeight(address(tokens[_tokenIn])), - tokens[_tokenOut].balanceOf(address(pool)), - pool.getDenormalizedWeight(address(tokens[_tokenOut])), - _amountOut, - bconst.MIN_FEE() - ); - - vm.prank(currentCaller); - - // Action - try pool.swapExactAmountOut( - address(tokens[_tokenIn]), _maxAmountIn, address(tokens[_tokenOut]), _amountOut, type(uint256).max - ) { - // Postcondition - uint256 _balanceInAfter = tokens[_tokenIn].balanceOf(currentCaller); - uint256 _balanceOutAfter = tokens[_tokenOut].balanceOf(currentCaller); - - // 5 - assert(_balanceInBefore - _balanceInAfter <= _maxAmountIn); - - // 14 - if (_tokenIn != _tokenOut) assert(_balanceOutAfter - _balanceOutBefore == _amountOut); - else assert(_balanceOutAfter == _balanceOutBefore - _inComputed + _amountOut); - - // 15 - if (_balanceInBefore == _balanceInAfter) assert(_balanceOutBefore == _balanceOutAfter); - - // 19 - assert(pool.isFinalized()); - } catch {} - } - - /// @custom:property-id 6 - /// @custom:property swap fee can only be 0 (cow pool) - /// @custom:property-id 7 /// @custom:property total weight can be up to 50e18 /// @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())); @@ -254,15 +147,37 @@ contract HalmosBalancer is HalmosTest { } } - /// properties 8 and 9 are tested with the BToken internal tests + /// @custom:property-id 8 + /// @custom:property BToken increaseApproval should increase the approval of the address by the amount + function check_increaseApproval(uint256 _approvalToAdd, address _owner, address _spender) public { + // Precondition + uint256 _approvalBefore = pool.allowance(_owner, _spender); - /// @custom:property-id 10 - /// @custom:property a pool can either be finalized or not finalized - /// @dev included to be exhaustive/future-proof if more states are added, as rn, it - /// basically tests the tautological (a || !a) + vm.prank(_owner); - /// @custom:property-id 11 - /// @custom:property a finalized pool cannot switch back to non-finalized + // Action + BToken(address(pool)).increaseApproval(_spender, _approvalToAdd); + + // Postcondition + assert(pool.allowance(_owner, _spender) == _approvalBefore + _approvalToAdd); + } + /// @custom:property-id 9 + /// @custom:property BToken decreaseApproval should decrease the approval to max(old-amount, 0) + + function check_decreaseApproval(uint256 _approvalToLower, address _owner, address _spender) public { + // Precondition + uint256 _approvalBefore = pool.allowance(_owner, _spender); + + vm.prank(_owner); + + // Action + BToken(address(pool)).decreaseApproval(_spender, _approvalToLower); + + // Postcondition + assert( + pool.allowance(_owner, _spender) == (_approvalBefore > _approvalToLower ? _approvalBefore - _approvalToLower : 0) + ); + } /// @custom:property-id 12 /// @custom:property a non-finalized pool can only be finalized when the controller calls finalize() @@ -294,79 +209,6 @@ contract HalmosBalancer is HalmosTest { } catch {} } - /// @custom:property-id 16 - /// @custom:property the pool btoken can only be minted/burned in the join and exit operations - - /// @custom:property-id 17 - /// @custom:property a direct token transfer can never reduce the underlying amount of a given token per BPT - function skipped_directTransfer(uint256 _amountPoolToken, uint256 _amountToTransfer, uint256 _tokenIdx) public { - vm.assume(_tokenIdx < tokens.length); - - FuzzERC20 _token = tokens[2]; - - 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); - } - - /// @custom:property-id 18 - /// @custom:property the amount of underlying token when exiting should always be the amount calculated in bmath - function correctBPTBurnAmount(uint256 _amountPoolToken) public { - _amountPoolToken = bound(_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); - } - - vm.prank(currentCaller); - pool.approve(address(pool), _amountPoolToken); - - vm.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 check_boundOnlyNotFinalized() public { @@ -377,50 +219,67 @@ contract HalmosBalancer is HalmosTest { address _callerUnbind = svm.createAddress('callerUnbind'); address _callerFinalize = svm.createAddress('callerFinalize'); - for (uint256 i; i < 2; i++) { - tokens[i].mint(_callerBind, 10 ether); + // Avoid hitting the max unrolled loop limit - vm.startPrank(_callerBind); - tokens[i].approve(address(pool), 10 ether); + // Bind 3 tokens + tokens[0].mint(_callerBind, 10 ether); + tokens[1].mint(_callerBind, 10 ether); + tokens[2].mint(_callerBind, 10 ether); - uint256 _poolWeight = bconst.MAX_WEIGHT() / 5; + vm.startPrank(_callerBind); + tokens[0].approve(address(_nonFinalizedPool), 10 ether); + tokens[1].approve(address(_nonFinalizedPool), 10 ether); + tokens[2].approve(address(_nonFinalizedPool), 10 ether); - try _nonFinalizedPool.bind(address(tokens[i]), 10 ether, _poolWeight) { - assert(_callerBind == _nonFinalizedPool.getController()); - } catch { - assert(_callerBind != _nonFinalizedPool.getController()); - } + uint256 _poolWeight = bconst.MAX_WEIGHT() / 4; + uint256 _bindCount; - vm.stopPrank(); + try _nonFinalizedPool.bind(address(tokens[0]), 10 ether, _poolWeight) { + assert(_callerBind == _nonFinalizedPool.getController()); + _bindCount++; + } catch { + assert(_callerBind != _nonFinalizedPool.getController()); } - vm.prank(_callerUnbind); - try _nonFinalizedPool.unbind(address(tokens[1])) { - assert(_callerUnbind == _nonFinalizedPool.getController()); + try _nonFinalizedPool.bind(address(tokens[1]), 10 ether, _poolWeight) { + assert(_callerBind == _nonFinalizedPool.getController()); + _bindCount++; } catch { - assert(_callerUnbind != _nonFinalizedPool.getController()); + assert(_callerBind != _nonFinalizedPool.getController()); } - vm.prank(_callerFinalize); - try _nonFinalizedPool.finalize() { - assert(_callerFinalize == _nonFinalizedPool.getController()); + try _nonFinalizedPool.bind(address(tokens[2]), 10 ether, _poolWeight) { + assert(_callerBind == _nonFinalizedPool.getController()); + _bindCount++; } catch { - // assert(_callerFinalize != _nonFinalizedPool.getController()); + assert(_callerBind != _nonFinalizedPool.getController()); } vm.stopPrank(); - } - /// @custom:property-id 21 - /// @custom:property there always should be between MIN_BOUND_TOKENS and MAX_BOUND_TOKENS bound in a pool - function fuzz_minMaxBoundToken() public { - assert(pool.getNumTokens() >= bconst.MIN_BOUND_TOKENS()); - assert(pool.getNumTokens() <= bconst.MAX_BOUND_TOKENS()); + if (_bindCount == 3) { + vm.prank(_callerUnbind); + // Action + // Unbind one + try _nonFinalizedPool.unbind(address(tokens[0])) { + assert(_callerUnbind == _nonFinalizedPool.getController()); + } catch { + assert(_callerUnbind != _nonFinalizedPool.getController()); + } + } + + vm.prank(_callerFinalize); + // Action + try _nonFinalizedPool.finalize() { + assert(_callerFinalize == _nonFinalizedPool.getController()); + } catch { + assert(_callerFinalize != _nonFinalizedPool.getController() || _bindCount < 2); + } } /// @custom:property-id 22 /// @custom:property only the settler can commit a hash - function fuzz_settlerCommit() public { + function check_settlerCommit() public { // Precondition vm.prank(currentCaller); @@ -430,11 +289,6 @@ contract HalmosBalancer is HalmosTest { assert(currentCaller == solutionSettler); } catch {} } - - /// @custom:property-id 23 - /// @custom:property when a hash has been commited, only this order can be settled - /// @custom:property-not-implemented - function fuzz_settlerSettle() public {} } contract BNum_exposed is BNum {