-
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
Chore: setup medusa + 1 basic fuzz scenario #19
Conversation
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.
Amazing ser 🐻
Since this is only the setup I guess that's why you didn't write the property on the tests NATSPEC, so no problem with that but we need to include them in the future. Maybe we can leave a TODO.
} | ||
|
||
// this is a stateless check, so halmos will probably supersede it | ||
function testContractAddressDependsOnParams(DeployParams memory left, DeployParams memory right) external { |
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.
on the opUSDC campaign we used this standard for test contracts names:
function testContractAddressDependsOnParams(DeployParams memory left, DeployParams memory right) external { | |
function fuzz_contractAddressDependsOnParams(DeployParams memory left, DeployParams memory right) external { |
I think we should stick to that unless is a blocker for medusa
], | ||
"blockNumberDelayMax": 60480, | ||
"blockTimestampDelayMax": 604800, | ||
"blockGasLimit": 125000000, |
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.
on Optimism, the block gas limit is 30m
"blockGasLimit": 125000000, | |
"blockGasLimit": 30000000, |
And also, 20m is the limit of the gas that can be deposited from L1 -> L2 for a given block (jic this has some influence on some config)
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.
should we have:
- block gas limit be realistic for the deployed network (keep in mind some other things won't be, such as all contracts being deployed in the same EVM as opposed to different L2s)
- block gas limit be unrealistic, but compensate for the above and allow more calls in the same block, which could point us in the direction of an otherwise-unreachable bug?
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.
If we can try to try the tests on a realistic environment, is better for me. Otherwise, if it becomes an issue or is really complex to handle, we can increase it
bc57cf1
to
f6c3f90
Compare
d469a49
to
5514694
Compare
_; | ||
} | ||
|
||
function fuzz_DeployNewSupertoken( |
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.
Missing assertions?
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.
I can think of an assertion for property 14, but am I missing another one?
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.
I mean is ok if is not any property and you're only testing that the setup indeed works. But don't you think using a fuzz_setup
with a comment explaining this makes it more clear?
|
||
- [ ] [OptimismSuperchainERC20](https://github.com/defi-wonderland/optimism/pull/9/files#diff-810060510a8a9c06dc60cdce6782e5cafd93b638e2557307a68abe694ee86aee) | ||
- [ ] [OptimismMintableERC20Factory](https://github.com/defi-wonderland/optimism/blob/develop/packages/contracts-bedrock/src/universal/OptimismMintableERC20Factory.sol) | ||
- [ ] [SuperchsupERC20ainERC20](https://github.com/defi-wonderland/optimism/pull/8/files#diff-603fd7d5a0b2c403c0d1eee21d0ee60fb8eb72430169eaac5ec7081e01de96b8) (not yet merged) |
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.
- [ ] [SuperchsupERC20ainERC20](https://github.com/defi-wonderland/optimism/pull/8/files#diff-603fd7d5a0b2c403c0d1eee21d0ee60fb8eb72430169eaac5ec7081e01de96b8) (not yet merged) | |
- [ ] [SuperchainERC20](https://github.com/defi-wonderland/optimism/pull/8/files#diff-603fd7d5a0b2c403c0d1eee21d0ee60fb8eb72430169eaac5ec7081e01de96b8) (not yet merged) |
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.
Astonishing 🫂 🐻
/////////////////////////////////////////////////// | ||
// Helpers for cross-chain interaction mocking // | ||
/////////////////////////////////////////////////// | ||
mapping(address => bytes32) public superTokenInitDeploySalts; |
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.
NIT: named args on the mapping
import { OptimismSuperchainERC20 } from "src/L2/OptimismSuperchainERC20.sol"; | ||
import { SafeCall } from "src/libraries/SafeCall.sol"; | ||
|
||
contract MockCrossDomainMessenger { |
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.
Is not the cross domain but the L2 <-> Messenger instead. I suggest also changing the name to the file
contract MockCrossDomainMessenger { | |
contract MockL2ToL2Messenger { |
} | ||
} | ||
|
||
function fuzz_MintSupertoken(uint256 index, uint96 amount) external { |
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.
Missing NATSPEC?
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.
I think a good idea could be to split the function to have the properties test functions on one place, and the test-helpers functions in other.
Wdyt?
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.
good idea!
/// @custom:property sum of supertoken total supply across all chains is always equal to convert(legacy, super)- | ||
/// convert(super, legacy) | ||
/// @dev deliberately not a view method so medusa runs it but not the view methods defined by Test | ||
function property_totalSupplyAcrossChainsEqualsMints() external { |
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.
Maybe this?
function property_totalSupplyAcrossChainsEqualsMints() external { | |
function fuzz_totalSupplyAcrossChainsEqualsMints() external { |
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.
this is the only method so far where we manage to only do invariant checking :D
I believe it's worthwhile to give them different names, so later it's more clear if it makes sense to have separate contracts for state transitions or assertions, similar to horsefacts/WETH9
for (uint256 i = 0; i < ghost_totalSupplyAcrossChains.length(); i++) { | ||
uint256 totalSupply = 0; | ||
(bytes32 currentSalt, uint256 trackedSupply) = ghost_totalSupplyAcrossChains.at(i); | ||
for (uint256 j = 0; j < MAX_CHAINS; j++) { | ||
address supertoken = MESSENGER.superTokenAddresses(j, currentSalt); | ||
if (supertoken != address(0)) { | ||
totalSupply += OptimismSuperchainERC20(supertoken).totalSupply(); |
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.
Could you add some comments or use another var names instead of _i
of _j
? bc is kinda difficult to understand hehe
- 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
d8ad2b1
to
ec29415
Compare
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.
It looks good overall. I would like to see the invariants divided (or at least labeled) by contract/functionality, besides type. There are four things here: the deployments of OptimismSuperchainERC20
and theOptimismSuperchainERC20Factory
; and modifications to L2StandardBridge
(convert) and OptimismMintableERC20Factory
. It's all kinda mixed
| 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 | [ ] | [ ] | |
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.
you mean symbol instead of address, right?
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.
🙈
@@ -0,0 +1,72 @@ | |||
# supertoken properties |
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.
you include invariants from liquidity migration. Wdyt about renaming this title?
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.
*and factory
| --- | --- | --- | --- | | ||
| 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 | [ ] | [ ] | |
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.
allowed legacy and allowed supertokens
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.
not every legacy nor supertoken will be allowed
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.
this was defined in SUMMARY.md
, however I realize it's not really clear from this document, so I merged them both and made sure the definitions are above
| 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 | [ ] | [ ] | |
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.
this sentence is incomplete
| 12 | supertoken total supply only increases on calls to mint() by the L2toL2StandardBridge | [ ] | [ ] | | ||
| 13 | supertoken total supply only decreases on calls to burn() by the L2toL2StandardBridge | [ ] | [ ] | | ||
| 14 | supertoken total supply starts at zero | [ ] | [ ] | | ||
| 15 | deploying a supertoken registers its remote token in the factory | [ ] | [ ] | |
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.
if you are adding invariants for the factory, you should also add uints for it, right?
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.
I read through the preliminar implementations of the factories and didn't find anything that struck me as needing an extra layer of testing on top of foundry unit tests, do you have anything in mind?
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.
mm good point. Not sure about this, but some ideas:
- Something around metadata initialization? what happens if implementation changes and adds a state variable. How should reinitialization work? We cannot overwrite to the same storage where metadata lives.
- There is only one Superchain token for a fixed set of metadata (this should be obvious from CREATE2 address deduction).
- Every Beacon Proxy deployed must implement the implementation that lives in the address indicated by the Beacon Contract (obvious from the implementation).
| --- | --- | --- | --- | | ||
| 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) | [ ] | [ ] | |
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.
total supply of what token?
| 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 | [ ] | [ ] | |
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.
<3
| --- | --- | --- | --- | | ||
| 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) | [ ] | [~] | |
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.
this repeats 19, or am I missing something?
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.
the property, from the point of view of the contracts under test, is the same one, but it will be instrumented differently (using an atomic bridge), so instead of being equal when all cross chain messages are processed, it must always be equal
If you believe the distinction should be an implementation detail of the testing contracts and readers of this document won't care much, I'm open to removing it
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.
gotcha <3
- `[~]`: partially tested/proven property | ||
- `:(`: property won't be tested due to some limitation | ||
|
||
## Unit test |
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.
you might want to include Event emissions here
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.
While I recognize the importance of emitting the events for the interop bridge, I don't see how unit tests for that in Foundry would not be sufficient, since the emission or params of it don't depend on state that medusa could push into inconsistency for example
(and I'm not sure the medusa/halmos executing environment can actually assert on event emmissions 😅)
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.
you are right
## Definitions | ||
|
||
- *legacy token:* an OptimismMintableERC20 or L2StandardERC20 token on the suprechain that has either been deployed by the factory after the liquidity migration upgrade to the latter, or has been deployed before it **but** added to factory’s `deployments` mapping as part of the upgrade. This testing campaign is not concerned with tokens on L1 or not listed in the factory’s `deployments` mapping. | ||
- *supertoken:* a SuperchainERC20 contract deployed on the Superchain |
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.
I would change this: deployed by the OptimismSuperchainERC20Factory
. Deployed in the superchain is not enough
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.
updated that + made sure we always refer to said contract by that name
| 5 | convert() burns the same amount of one token that it mints of the other | [ ] | [ ] | | ||
| id | milestone | description | halmos | medusa | | ||
| --- | --- | --- | --- | --- | | ||
| 0 | Factories | supertoken token address does not depend on the executing chain’s chainID | [ ] | [ ] | |
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.
love the new labels :)
67223b5
to
d761fa9
Compare
/// @custom:property-id 14 | ||
/// @custom:property supertoken total supply starts at zero |
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.
Ah got it. That's why you didn't use property natspec on fuzz_DeployNewSupertoken
.
Isn't better to just declare always the property natspec on the test rather than on the function?
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.
I wanted to define it closest to where it's asserted so there's less of a chance it becomes outdated. Although it's true that we usually want to know which properties are asserted on by a particular test
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.
Looking good so far ser. The assertions on the tests are correct.
But I find it quite difficult to follow and understand, mostly the setup part. Of course, this is not your fault since the system is complex by itself and we need to a multichain scenario.
But in order to improve it, could we:
- Couple helpers-setup functions and then property functions togheter?
- Divide it into a handler with actors and then another contract file just for test? (maybe is planned but out of scope for this PR)
And also, I have one specific question:
- Where are the supertoken functions being exposed to the fuzzer? I only see that you call a specific function on each test, but how can the fuzzer perform a sequence of calls before it.
destinationChainId = bound(destinationChainId, 0, MAX_CHAINS - 1); | ||
fromIndex = bound(fromIndex, 0, allSuperTokens.length - 1); | ||
OptimismSuperchainERC20 sourceToken = OptimismSuperchainERC20(allSuperTokens[fromIndex]); | ||
OptimismSuperchainERC20 destinationToken = |
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.
Don't get why the destination token address depends also on the msg.sender
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.
And also, I think in this way you're limiting the test to check balances the same address on origin and destination (msg.sender
).
IMO it should be more exhaustive if we check on different addresses as well, but it's ok if that adds even more complexity and isn't worth it
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.
In this PR I tried to get medusa running for the simplest possible (but still somewhat meaningful) test. I have #22 where I add cross-chain transfers between different accounts, which I deemed out of scope for this one since it requires an actor setup and this PR is big enough already 😁
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.
lgtm
- 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 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 fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa
- 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 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 fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa
- 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 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 fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa
…11776) * chore: configure medusa with basic supERC20 self-bridging (#19) - 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 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 fix: fixes after lovely feedback by disco docs: merge both documents and categorized properties by their milestone fix: fixes from parti's review fix: feedback from disco fix: feedback from doc refactor: separate state transitions from pure properties docs: update tested properties refactor: move all assertions into properties contract fix: move function without assertions back into handler test: only use assertion mode fix: improve justfile recipie for medusa * feat: halmos symbolic tests (#21) * 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]> * test: remaining protocol properties (#26) * test: cross-user fuzzed bridges + actor setup * test: fuzz properties 8 and 9 * test: properties 7 and 25 * fix: implement doc's feedback * test: superc20 tob properties (#27) * chore: add crytic/properties dependency * test: extend protocol properties so it also covers ToB erc20 properties * chore: small linter fixes * docs: update property list * test: handlers for remaining superc20 state transitions * fix: disable ToB properties we are not using and guide the fuzzer a bit more * fix: disable another ToB property not implemented by solady * chore: remove zero-initializations * fix: feedback from disco * chore: separate fuzz campaign tests in guided vs unguided * test: dont revert on successful unguided relay * test: add fuzzed calls to burn and mint * docs: document the separation of fuzz test functions * chore: move the properties file to its own directory * chore: consistently use fuzz_ and property_ + camelcase * chore: fix typo * chore: camelcase for handlers as well * fix: revert change that broke halmos campaign compile :D * test: fuzz non atomic bridging (#31) * test: changed mocked messenger ABI for message sending but kept assertions the same * docs: add new properties 26&27 * test: queue cross-chain messages and test related properties * test: relay random messages from queue and check associated invariants * chore: rename bridge->senderc20 method for consistency with relayerc20 * test: not-yet-deployed supertokens can get funds sent to them * chore: medusa runs forever by default doable since it also handles SIGINTs gracefully * chore: document the reason behind relay zero and send zero inconsistencies * fix: feedback from doc * fix: walk around possible medusa issue I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when calling the MockL2ToL2CrossDomainMessenger for the first time * test: unguided handler for sendERC20 * fix: feedback from disco * chore: remove halmos testsuite * chore: foundry migration (#40) * chore: track assertion failures this is so foundry's invariant contract can check that an assertion returned false in the handler, while still allowing `fail_on_revert = false` so we can still take full advantage of medusa's fuzzer & coverage reports * fix: explicitly skip duplicate supertoken deployments * chore: remove duplicated PROPERTIES.md file * chore: expose data to foundry's external invariant checker * test: run medusa fuzzing campaign from within foundry * fix: eagerly check for duplicate deployments * fix: feedback from doc * chore: shoehorn medusa campaign into foundry dir structure * chore: remove PROPERTIES.md file * chore: delete medusa config * docs: limited support for subdirectories in test/invariant * chore: rename contracts to be more sneaky about medusa * docs: rewrite invariant docs in a way compliant with autogen scripts * chore: fixes from rebase * fix: cleanup superc20 invariants (#46) * chore: revert modifications from medusa campaign * docs: extra docs on why ForTest contract is required * doc: add list of all supertoken properties * chore: run forge fmt * ci: allow for testfiles to be deleted * fix: run doc autogen script after rebase --------- Co-authored-by: Disco <[email protected]> Co-authored-by: agusduha <[email protected]> Co-authored-by: 0xng <[email protected]>
test/properties
is compiled (otherwise it is not compiled and medusa crashes when it can't find it's compiled representation)questions
assert
in property_* methods by a return? I opted to not do that for consistency (since all other properties are actually checked with asserts)to figure out what I could so far see of the first item I ran a benchmark (from an empty corpus):
no initial mint, no bound on transfer amount: 176835 calls in 200s, 713 lines covered
initial mint, bound on transfer amount: 146625 calls in 200s, 643 lines covered
(you're not allowed make fun of my 'puter after running this on an ARM chip, btw)
Is offtopic for this PR (will take care of it in the next one)
CLOSES FUZZ-28
CLOSES FUZZ-29
CLOSES FUZZ-30