feat(test): fuzzed and symbolic tests #146
Conversation
test/invariant/PROPERTIES.md
Outdated
| bfloor should always return (a - a % BONE) | ||
| badd should be commutative | ||
| badd should be associative | ||
| 0 should be identity for badd |
There was a problem hiding this comment.
badd should have 0 as identity?
| function bsub_exposed(uint256 a, uint256 b) external pure returns (uint256) { | ||
| return bsub(a, b); | ||
| } |
There was a problem hiding this comment.
i think this is unnecessary bc you're inheriting BNum
other way should be to import MockBNum from manual-smock/ that exposes all calls (with call_* naming standard)
There was a problem hiding this comment.
it's a pretty weird case: I just needed the selector
require(_b > _a);
(bool succ,) = address(this).call(abi.encodeCall(EchidnaBNum.bsub_exposed, (_a, _b)));
assert(!succ);
}
| ///////////////////////////////////////////////////////////////////// | ||
|
|
||
| // btoi should always return the floor(a / BONE) == (a - a%BONE) / BONE | ||
| // TODO: Too tightly coupled |
| // badd should never sum terms which have a sum gt uint max | ||
| function badd_overflow(uint256 _a, uint256 _b) public pure { | ||
| // precondition | ||
| // vm.assume(_a != type(uint256).max); |
| assert(_result1 == _result2); | ||
| } | ||
|
|
||
| //todo this one fails |
crytic-export/combined_solc.json
Outdated
foundry.toml
Outdated
| # 1858: Some imports don't have the license identifier | ||
| ignored_error_codes = [2018, 2394, 5574, 3860, 1878] |
There was a problem hiding this comment.
ToB properties...
There was a problem hiding this comment.
I find the lack of coverage of parts of the join flow a bit concerning, but the exitPool function is covered so perhaps there's something I'm missing? I ran
echidna test/invariants/fuzz/Protocol.t.sol --contract FuzzProtocol --config test/invariants/fuzz/Protocol.yaml
and similarly for the other test files
I agree with weiber on that we should have npm scripts or something in the readme on how to run halmos/echidna
foundry.toml
Outdated
| # 1858: Some imports don't have the license identifier | ||
| ignored_error_codes = [2018, 2394, 5574, 3860, 1878] |
test/SUMMARY.md
Outdated
|
|
||
| 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 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.
spot price before a swap should always be lower than after it|high level|25?
There was a problem hiding this comment.
wanna add it? I guess that should be fairly easy in the swap post-conditions
| @@ -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/Protocol/ | |||
There was a problem hiding this comment.
the difference between all of these .yaml seems to be the corpusDir
- could we use a single config file?
- what's the purpose behind having different corpus directories?
There was a problem hiding this comment.
if you replay a "common" directory, where they're all mixed, echidna spends some time trying "wrong" seq (ie trying to interact with non-deployed contracts) and dropping them -> check the echidna-corpus repo, different config files purpose is twofold: avoiding wasting time replaying "aberrant" seq; having flexibility when using the shell script (if one test shouldn't be an assert mode for instance, or deploy some libraries, etc)
test/SUMMARY.md
Outdated
|
|
||
|
|
||
| `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.
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
.solhintignore
Outdated
| @@ -1,2 +1,3 @@ | |||
| test/smock/* | |||
| test/manual-smock/* | |||
| test/invariants/* | |||
There was a problem hiding this comment.
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 of no-empty-blocks, for example)
|
|
||
| function clamp(uint256 _value, uint256 _min, uint256 _max) internal returns (uint256) { | ||
| if (_min > _max) { | ||
| emit AssertionFailed(); |
There was a problem hiding this comment.
why use the event here but assert(false) elsewhere?
There was a problem hiding this comment.
yeah, not super consistent, agree (this will become a std lib we can reuse, with rounding errors/approx eq, etc, maybe in echidna-corpus repo?)
test/invariants/fuzz/BToken.sol
Outdated
There was a problem hiding this comment.
should be BToken.t.sol for consistency
| _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 { | ||
| assert( | ||
| pool.isFinalized() || pool.getCurrentTokens().length > bconst.MAX_BOUND_TOKENS() | ||
| || currentCaller != pool.getController() | ||
| ); | ||
| } |
There was a problem hiding this comment.
after a run of 50k calls I'm getting no coverage on this, perhaps there's something wrong with line 80?
the calls to _{mint,push}PoolShare in join are also not covered
There was a problem hiding this comment.
- 50k is rookie number -> check echidna-corpus repo to reuse bigger corpus (I think a bit more than 10m runs rn? Still not huge, but something, looking at cloud-fuzzing very soon(tm)(c))
- you're right, bmul calls revert systematically -> I guess bptToken should have more constraints. Wanna give it a stab?
| uint256 _outRatio = bnum.bmul_exposed(tokens[_tokenOut].balanceOf(address(pool)), bconst.MAX_OUT_RATIO()); | ||
|
|
||
| assert( | ||
| _inComputed > _maxAmountIn // 5 |
There was a problem hiding this comment.
this assert seems to always short-circuit on the first condition
There was a problem hiding this comment.
why do you think so? Test fails if I remove any of the 3 conditions for me
There was a problem hiding this comment.
then it's probably related to me running only 50k calls
| 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 |
There was a problem hiding this comment.
is this a halmos/echidna thing? we should issue them
* 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]>
wei3erHase
force-pushed
the
feat/fuzz-symb-tests
branch
from
bf490bb to
42d2a04
Compare
* 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]>
* 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
| @@ -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", | |||
There was a problem hiding this comment.
this will change the deployed build...
No description provided.