-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(test): fuzzed and symbolic tests #146
Changes from 26 commits
21bc497
5b1182b
bec1de2
1d0d05d
013f72f
388c657
caf3c62
b01b4e6
3753371
d12abd4
8cde0c0
0d0ca16
87a9acb
e946f09
59c2686
462c38e
68a6b59
fdd4617
cad698a
c143808
a65a9c0
350c39d
c60f5fa
c5c263f
09d332d
888ebe9
0c0e1c4
00cd7d1
ea280d9
5555afc
637aa83
42d2a04
302463c
23a8264
b3f2cf6
5abef51
a793e9d
61a0930
df49eb9
7bbb6cc
9d976ff
b101648
cd1ef62
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -19,3 +19,6 @@ broadcast/*/*/* | |
|
||
# Out dir | ||
out | ||
|
||
# echidna corpuses | ||
**/corpuses/* |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,3 @@ | ||
test/smock/* | ||
test/manual-smock/* | ||
test/invariants/* | ||
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -12,12 +12,13 @@ sort_imports = true | |
solc_version = '0.8.25' | ||
wei3erHase marked this conversation as resolved.
Show resolved
Hide resolved
|
||
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] | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. WHICH ONES??! 👀 There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. ToB properties... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. 1858 or 1878? |
||
deny_warnings = true | ||
|
||
[profile.optimized] | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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", | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this will change the deployed build... |
||
"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", | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. should this be a section? |
||
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)$ | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this expression doesn't seem to be renderable Also, perhaps expressions as blocks would be easier to read? text in inline expressions gets real small There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. true true |
||
|
||
|
||
`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]. | ||
``` |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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] | | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. wanna add it? I guess that should be fairly easy in the swap post-conditions |
||
|
||
> (*) 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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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); | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
there are not that many warnings, we could disable some rules (such as
custom-errors
) for the entire directory and add a few inline ignores (in the case ofno-empty-blocks
, for example)