Skip to content

Commit

Permalink
test(echidna): all properties
Browse files Browse the repository at this point in the history
  • Loading branch information
@simon-something
simon-something committed Jul 15, 2024
1 parent 3753371 commit d12abd4
Show file tree
Hide file tree
Showing 4 changed files with 174 additions and 69 deletions.
50 changes: 26 additions & 24 deletions test/invariants/PROPERTIES.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,30 +2,32 @@
| ------------------------------------------------------------------------------------------- | ------------------- | --- | ------ | ------- |
| 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 | [ ] | [ ] |
| 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
| 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] |

* Bundled with 24

** ERC20 properties
(https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests)

# Unit for the math libs (BNum and BMath):
Expand Down
2 changes: 1 addition & 1 deletion test/invariants/fuzz/config.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@
testMode: assertion
corpusDir: test/invariants/fuzz/corpus/
coverageFormats: ["html","lcov"]
allContracts: false
allContracts: true
30 changes: 27 additions & 3 deletions test/invariants/fuzz/external/BToken.sol
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,49 @@
pragma solidity 0.8.23;

import {EchidnaTest} from '../../AdvancedTestsUtils.sol';
import {CryticERC20ExternalBasicProperties} from
'@crytic/properties/contracts/ERC20/external/properties/ERC20ExternalBasicProperties.sol';
import {ITokenMock} from '@crytic/properties/contracts/ERC20/external/util/ITokenMock.sol';
import {PropertiesConstants} from '@crytic/properties/contracts/util/PropertiesConstants.sol';
import 'contracts/BToken.sol';

contract EchidnaBToken is CryticERC20ExternalBasicProperties {
contract EchidnaBToken is CryticERC20ExternalBasicProperties, EchidnaTest {
constructor() {
// Deploy ERC20
token = ITokenMock(address(new CryticTokenMock()));
}

/// @custom:property-id 8
/// @custom:property BToken increaseApproval should increase the approval of the address by the amount
function fuzz_increaseApproval() public {
function fuzz_increaseApproval(uint256 _approvalToAdd) public {
// Precondition
uint256 _approvalBefore = token.allowance(USER1, USER2);

hevm.prank(USER1);

// Action
BToken(address(token)).increaseApproval(USER2, _approvalToAdd);

// Postcondition
assert(token.allowance(USER1, USER2) == _approvalBefore + _approvalToAdd);
}
/// @custom:property-id 9
/// @custom:property BToken decreaseApproval should decrease the approval to max(old-amount, 0)
function fuzz_decreaseApproval() public {}

function fuzz_decreaseApproval(uint256 _approvalToLower) public {
// Precondition
uint256 _approvalBefore = token.allowance(USER1, USER2);

hevm.prank(USER1);

// Action
BToken(address(token)).decreaseApproval(USER2, _approvalToLower);

// Postcondition
assert(
token.allowance(USER1, USER2) == (_approvalBefore > _approvalToLower ? _approvalBefore - _approvalToLower : 0)
);
}
}

contract CryticTokenMock is BToken, PropertiesConstants {
Expand Down
161 changes: 120 additions & 41 deletions test/invariants/fuzz/external/Protocol.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,39 @@ contract EchidnaBalancer is EchidnaTest {
ghost_bptMinted = pool.INIT_POOL_SUPPLY();
}

// Randomly add or remove tokens to a finalized pool
// Insure caller has enough token
function setup_joinExitPool(bool _join, uint256 _amountBpt) public AgentOrDeployer {
if (_join) {
uint256[] memory _maxAmountsIn;

_maxAmountsIn = new uint256[](4);

for (uint256 i; i < _maxAmountsIn.length; i++) {
uint256 _maxIn =
bnum.bmul_exposed(bnum.bdiv_exposed(_amountBpt, pool.totalSupply()), pool.getBalance(address(tokens[i])));
_maxAmountsIn[i] = _maxIn;

tokens[i].mint(currentCaller, _maxIn);
hevm.prank(currentCaller);
tokens[i].approve(address(pool), _maxIn);
}

hevm.prank(currentCaller);
try pool.joinPool(_amountBpt, _maxAmountsIn) {
ghost_bptMinted += _amountBpt;
} catch {}
} else {
hevm.prank(currentCaller);
pool.approve(address(pool), _amountBpt);

hevm.prank(currentCaller);
try pool.exitPool(_amountBpt, new uint256[](4)) {
ghost_bptBurned += _amountBpt;
} catch {}
}
}

/// @custom:property-id 1
/// @custom:property BFactory should always be able to deploy new pools
function fuzz_BFactoryAlwaysDeploy() public AgentOrDeployer {
Expand Down Expand Up @@ -128,14 +161,13 @@ contract EchidnaBalancer is EchidnaTest {
/// @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 fuzz_swapExactIn(
uint256 _minAmountOut,
uint256 _amountIn,
uint256 _tokenIn,
uint256 _tokenOut
) public AgentOrDeployer {
// Precondition
// Preconditions
require(pool.isFinalized());

_tokenIn = clamp(_tokenIn, 0, tokens.length - 1);
Expand Down Expand Up @@ -184,11 +216,12 @@ contract EchidnaBalancer is EchidnaTest {

/// @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 fuzz_swapExactOut(
uint256 _maxAmountIn,
uint256 _amountOut,
Expand All @@ -200,7 +233,6 @@ contract EchidnaBalancer is EchidnaTest {

_tokenIn = clamp(_tokenIn, 0, tokens.length - 1);
_tokenOut = clamp(_tokenOut, 0, tokens.length - 1);

_maxAmountIn = clamp(_maxAmountIn, 0, 10 ether);

tokens[_tokenIn].mint(currentCaller, _maxAmountIn);
Expand Down Expand Up @@ -285,6 +317,8 @@ contract EchidnaBalancer is EchidnaTest {
}
}

/// properties 8 and 9 are tested with the BToken internal tests

/// @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
Expand Down Expand Up @@ -319,53 +353,84 @@ contract EchidnaBalancer is EchidnaTest {
} catch {}
}

function setup_joinExitPool(bool _join, uint256 _amountBpt) public AgentOrDeployer {
if (_join) {
uint256[] memory _maxAmountsIn;

_maxAmountsIn = new uint256[](4);

for (uint256 i; i < _maxAmountsIn.length; i++) {
uint256 _maxIn =
bnum.bmul_exposed(bnum.bdiv_exposed(_amountBpt, pool.totalSupply()), pool.getBalance(address(tokens[i])));
_maxAmountsIn[i] = _maxIn;

tokens[i].mint(currentCaller, _maxIn);
hevm.prank(currentCaller);
tokens[i].approve(address(pool), _maxIn);
}

hevm.prank(currentCaller);
try pool.joinPool(_amountBpt, _maxAmountsIn) {
ghost_bptMinted += _amountBpt;
} catch {}
} else {
hevm.prank(currentCaller);
pool.approve(address(pool), _amountBpt);

hevm.prank(currentCaller);
try pool.exitPool(_amountBpt, new uint256[](4)) {
ghost_bptBurned += _amountBpt;
} catch {}
}
}

/// @custom:property-id 16
/// @custom:property the pool btoken can only be minted/burned in the join and exit operations
function fuzz_mintBurnBPT() public {
assert(ghost_bptMinted - ghost_bptBurned == pool.totalSupply());
}

/// @custom:property-id 17
/// @custom:property a direct token transfer can never reduce the underlying amount of a given token per BPT
function fuzz_directTransfer(uint256 _amount, uint256 _token) public AgentOrDeployer {
// Mint bpt
// get quote
// transfer token to the pool
// compare new quote
function fuzz_directTransfer(
uint256 _amountPoolToken,
uint256 _amountToTransfer,
uint256 _tokenIdx
) public AgentOrDeployer {
_tokenIdx = clamp(_tokenIdx, 0, tokens.length - 1);
FuzzERC20 _token = tokens[_tokenIdx];

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() public AgentOrDeployer {}
function correctBPTBurnAmount(uint256 _amountPoolToken) public AgentOrDeployer {
_amountPoolToken = clamp(_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);
}

hevm.prank(currentCaller);
pool.approve(address(pool), _amountPoolToken);

hevm.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
Expand Down Expand Up @@ -425,9 +490,23 @@ contract EchidnaBalancer is EchidnaTest {
}
}

/// @custom:property-id 22
/// @custom:property only the settler can commit a hash
function fuzz_settlerCommit() public AgentOrDeployer {
// Precondition
hevm.prank(currentCaller);

// Action
try pool.commit(hex'1234') {
// Postcondition
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 {
Expand Down

0 comments on commit d12abd4

Please sign in to comment.