feat: superc20 kontrol tests #36
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
- used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants
previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down
Chore: setup medusa + 1 basic fuzz scenario
* feat: introduce OptimismSuperchainERC20 * fix: contract fixes * feat: add snapshots and semver * test: add supports interface tests * test: add invariant test * feat: add parameters to the RelayERC20 event * fix: typo * fix: from param description * fix: event signature and interface pragma * feat: add initializer * feat: use unstructured storage and OZ v5 * feat: update superchain erc20 interfaces * fix: adapt storage to ERC7201 * test: add initializable OZ v5 test * fix: invariant docs * fix: ERC165 implementation * test: improve superc20 invariant (#11) * fix: gas snapshot * chore: configure medusa with basic supERC20 self-bridging - used --foundry-compile-all to ensure the test contract under `test/properties` is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation) - set src,test,script to test/properties/medusa to not waste time compiling contracts that are not required for the medusa campaign - used an atomic bridge, which doesnt allow for testing of several of the proposed invariants * fix: delete dead code * test: give the fuzzer a head start * feat: create suite for sybolic tests with halmos * test: setup and 3 properties with symbolic tests * chore: remove todo comment * docs: fix properties order * test: document & implement assertions 22, 23 and 24 * fix: fixes from self-review * test: guide the fuzzer a little bit less previously: initial mint, bound on transfer amount: 146625 calls in 200s now: no initial mint, no bound on transfer amount: 176835 calls in 200s it doesn't seem to slow the fuzzer down * feat: add property for burn * refactor: remove symbolic address on mint property * refactor: order the tests based on the property id * feat: checkpoint * chore: set xdomain sender on failing test * chore: enhance mocks * Revert "Merge branch 'chore/setup-medusa' into feat/halmos-symbolic-tests" This reverts commit 945d6b6, reversing changes made to 5dcb3a8. * refactor: remove symbolic addresses to make all of the test work * chore: remove console logs * feat: add properties file * chore: polish * refactor: enhance test on property 7 using direct try catch (now works) * fix: review comments * refactor: add symbolic addresses on test functions * feat: create halmos toml * chore: polish test contract and mock * chore: update property * refactor: move symbolic folder into properties one * feat: create advanced tests helper contract * refactor: enhance tests using symbolic addresses instead of concrete ones * chore: remove 0 property natspec * feat: add halmos profile and just script * chore: rename symbolic folder to halmos * feat: add halmos commands to justfile * chore: reorder assertions on one test * refactor: complete test property seven * chore: mark properties as completed * chore: add halmos-cheatcodes dependency * chore: rename advancedtest->halmosbase * chore: minimize mocked messenger * chore: delete empty halmos file * chore: revert changes to medusa.json * docs: update changes to PROPERTIES.md from base branch * test: sendERC20 destination fix * chore: natspec fixes --------- Co-authored-by: agusduha <[email protected]> Co-authored-by: 0xng <[email protected]> Co-authored-by: teddy <[email protected]>
* refactor: allow for atomicity on mock messenger * refactor: cross domain sender logic on mock messenger * refactor: l2 to l2 caller and messenge sender logic * chore: remove assumes for removed checks on mock messenger
The changes are no longer needed since with the constructor args flag it works This reverts commit 2934238.
* feat: create temporary file to debug symoblic tests with foundry
0xDiscotech
changed the base branch from
feat/add-crosschain-properties
to
feat/symbolic-testing
packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol
Outdated
Show resolved
Hide resolved
packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol
Outdated
Show resolved
Hide resolved
packages/contracts-bedrock/test/properties/FoundryDebugSymbolic.t.sol
Outdated
Show resolved
Hide resolved
packages/contracts-bedrock/test/properties/kontrol/OptimismSuperchainERC20.k.sol
Outdated
Show resolved
Hide resolved
| /// @custom:property-id 14 | ||
| /// @custom:property Supertoken total supply starts at zero | ||
| function prove_totalSupplyStartsAtZero() public { | ||
| setUpInlined(); |
There was a problem hiding this comment.
shoudn't we us a "regular" setup for this property tho (ie deploy the contract here, with symb constructor args, instead of the state diff? I don't really see what we'd test here otherwise, this sounds like a single branch)
There was a problem hiding this comment.
I don't get which is the difference, if we already rely on the setup for the other properties, why not for this one?
The property says the total supply should start at zero, and I'm testing that after the state diff setup.
I'm open to change my mind ofc
There was a problem hiding this comment.
We use these concrete values in the state which is replayed:
So this test is solely based on the deployment with concrete value, and only assess one single case -> I agree it shouldn't change much of the underlying logic, but if we want to test the initial state, shouldn't these concrete values be symbolic instead (ie catching a bug where total supply > 0 if decimals is 10**123)?
packages/contracts-bedrock/test/properties/kontrol/helpers/MockL2ToL2Messenger.sol
Outdated
Show resolved
Hide resolved
packages/contracts-bedrock/test/properties/kontrol/helpers/RecordStateDiff.sol
Show resolved
Hide resolved
0xDiscotech
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Failing proofs:
8:prove_sendERC20ZeroCall9:prove_relayERC20ZeroCall