forked from ethereum-optimism/optimism
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* 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]>
- Loading branch information
4 people
committed
Sep 17, 2024
1 parent
8cea351
commit 84b797e
Showing
10 changed files
with
398 additions
and
12 deletions.
There are no files selected for viewing
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| # Halmos configuration file | ||
|
|
||
| ## The version needed is `halmos 0.1.15.dev2+gc3f45dd` | ||
| ## Just running `halmos` will run the tests with the default configuration | ||
|
|
||
| [global] | ||
| # Contract to test | ||
| match-contract = "SymTest_" | ||
|
|
||
| # Path to the Forge artifacts directory | ||
| forge_build_out = "./forge-artifacts" | ||
|
|
||
|
|
||
| # Storage layout | ||
| storage_layout = "generic" |
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
Submodule halmos-cheatcodes
added at
c0d865
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,73 @@ | ||
| # supertoken properties | ||
|
|
||
| legend: | ||
|
|
||
| - `[ ]`: property not yet tested | ||
| - `**[ ]**`: property not yet tested, dev/research team has asked for extra focus on it | ||
| - `[X]`: tested/proven property | ||
| - `[~]`: partially tested/proven property | ||
| - `:(`: property won't be tested due to some limitation | ||
|
|
||
| ## Unit test | ||
|
|
||
| | id | description | halmos | medusa | | ||
| | --- | ---------------------------------------------------------------------------------- | ------ | ------ | | ||
| | 0 | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | | ||
| | 1 | supertoken token address depends on name, remote token, address and decimals | [ ] | [ ] | | ||
| | 2 | convert() should only allow converting legacy tokens to supertoken and viceversa | [ ] | [ ] | | ||
| | 3 | convert() only allows migrations between tokens representing the same remote asset | [ ] | [ ] | | ||
| | 4 | convert() only allows migrations from tokens with the same decimals | [ ] | [ ] | | ||
| | 5 | convert() burns the same amount of one token that it mints of the other | [ ] | [ ] | | ||
|
|
||
| ## Valid state | ||
|
|
||
| | id | description | halmos | medusa | | ||
| | --- | ------------------------------------------------------------------------------------------ | ------- | ------ | | ||
| | 6 | calls to sendERC20 succeed as long as caller has enough balance | [x] | [ ] | | ||
| | 7 | calls to relayERC20 always succeed as long as the sender and cross-domain caller are valid | **[~]** | [ ] | | ||
|
|
||
| ## Variable transition | ||
|
|
||
| | id | description | halmos | medusa | | ||
| | --- | ------------------------------------------------------------------------------------------------- | ------ | ------ | | ||
| | 8 | sendERC20 with a value of zero does not modify accounting | [x] | [ ] | | ||
| | 9 | relayERC20 with a value of zero does not modify accounting | [x] | [ ] | | ||
| | 10 | sendERC20 decreases the token's totalSupply in the source chain exactly by the input amount | [x] | [ ] | | ||
| | 11 | relayERC20 increases the token's totalSupply in the destination chain exactly by the input amount | [x] | [ ] | | ||
| | 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [x] | [ ] | | ||
| | 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [x] | [ ] | | ||
| | 14 | supertoken total supply starts at zero | [x] | [ ] | | ||
| | 15 | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | | ||
| | 16 | deploying an OptimismMintableERC20 registers its remote token in the factory | [ ] | [ ] | | ||
|
|
||
| ## High level | ||
|
|
||
| | id | description | halmos | medusa | | ||
| | --- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | | ||
| | 17 | only calls to convert(legacy, super) can increase a supertoken’s total supply across chains | [ ] | [ ] | | ||
| | 18 | only calls to convert(super, legacy) can decrease a supertoken’s total supply across chains | [ ] | [ ] | | ||
| | 19 | sum of total supply across all chains is always <= to convert(legacy, super)- convert(super, legacy) | [ ] | [ ] | | ||
| | 20 | tokens sendERC20-ed on a source chain to a destination chain can be relayERC20-ed on it as long as the source chain is in the dependency set of the destination chain | [ ] | [ ] | | ||
| | 21 | sum of supertoken total supply across all chains is = to convert(legacy, super)- convert(super, legacy) when all cross-chain messages are processed | [ ] | [ ] | | ||
|
|
||
| ## Atomic bridging pseudo-properties | ||
|
|
||
| As another layer of defense, the following properties are defined which assume bridging operations to be atomic (that is, the sequencer and L2Inbox and CrossDomainMessenger contracts are fully abstracted away, `sendERC20` triggering the `relayERC20` call on the same transaction) | ||
| It’s worth noting that these properties will not hold for a live system | ||
|
|
||
| | id | description | halmos | medusa | | ||
| | --- | ---------------------------------------------------------------------------------------------------------------------------------- | ------ | ------ | | ||
| | 22 | sendERC20 decreases sender balance in source chain and increases receiver balance in destination chain exactly by the input amount | [ ] | [x] | | ||
| | 23 | sendERC20 decreases total supply in source chain and increases it in destination chain exactly by the input amount | [ ] | [x] | | ||
| | 24 | sum of supertoken total supply across all chains is always equal to convert(legacy, super)- convert(super, legacy) | [ ] | [~] | | ||
|
|
||
| # Expected external interactions | ||
|
|
||
| - regular ERC20 operations between any accounts on the same chain, provided by [crytic ERC20 properties](https://github.com/crytic/properties?tab=readme-ov-file#erc20-tests) | ||
|
|
||
| # Invariant-breaking candidates (brain dump) | ||
|
|
||
| here we’ll list possible interactions that we intend the fuzzing campaign to support in order to help break invariants | ||
|
|
||
| - [ ] changing the decimals of tokens after deployment | ||
| - [ ] `convert()` ing between multiple (3+) representations of the same remote token, by having different names/symbols |
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
25 changes: 25 additions & 0 deletions
25
packages/contracts-bedrock/test/properties/halmos/MockL2ToL2Messenger.sol
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity 0.8.25; | ||
|
|
||
|
|
||
| // TODO: Try to merge to a single mocked contract used by fuzzing and symbolic invariant tests - only if possible | ||
| // and low priorty | ||
| contract MockL2ToL2Messenger { | ||
| // Setting the current cross domain sender for the check of sender address equals the supertoken address | ||
| address internal immutable CROSS_DOMAIN_SENDER; | ||
|
|
||
| constructor(address _xDomainSender) { | ||
| CROSS_DOMAIN_SENDER = _xDomainSender; | ||
| } | ||
|
|
||
| function sendMessage(uint256 , address , bytes calldata) external payable { | ||
| } | ||
|
|
||
| function crossDomainMessageSource() external view returns (uint256 _source) { | ||
| _source = block.chainid + 1; | ||
| } | ||
|
|
||
| function crossDomainMessageSender() external view returns (address _sender) { | ||
| _sender = CROSS_DOMAIN_SENDER; | ||
| } | ||
| } |
Oops, something went wrong.