test: fuzz non atomic bridging #31

0xteddybear · 2024-08-22T16:49:44Z

No description provided.

packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol

simon-something

noooice

…tions the same

doable since it also handles SIGINTs gracefully

…ncies

I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when calling the MockL2ToL2CrossDomainMessenger for the first time

0xDiscotech

The way you handled the complexity is truly amazing.
Just left few small comments and a couple question, but looking very good so far!

0xDiscotech · 2024-08-30T15:24:08Z

packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol

+        for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
+            uint256 totalSupply = 0;


Suggested change

for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {

uint256 totalSupply = 0;

for (uint256 deploySaltIndex; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {

uint256 totalSupply;

0xDiscotech · 2024-08-30T15:24:27Z

packages/contracts-bedrock/test/properties/medusa/properties/Protocol.t.sol

+        for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
+            uint256 totalSupply = 0;


Suggested change

for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {

uint256 totalSupply = 0;

for (uint256 deploySaltIndex; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {

uint256 totalSupply;

0xDiscotech · 2024-08-30T15:27:54Z

packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol

+    function relayMessageFromQueue(uint256 rawIndex) public {
+        uint256 index = rawIndex % _messageQueue.length;
+        CrossChainMessage memory message = _messageQueue[index];
+        _messageQueue[index] = _messageQueue[_messageQueue.length - 1];


Missing check _length > 0 here so it doesn't revert due an underflow when subtracting 1?

Actually, I think that check should go on the first line, since if 0, the modulo operation will revert

medusa (and foundry, most of the time) ignore reverts in invariant tests, and only consider assert(false), aka Panic(0x01), as test failures. That's why we try and catch on function calls where we want to fail the test if it reverts: because otherwise it is ignored.

coverage reports are then used to know if tests are reverting too early and leaving assertions or state transitions uncovered. There are many other places throughout the campaign where execution might return early due to a revert, and many places where we explicitly revert instead of returning because it's easier :D

Oh amazing, good to know :)

0xDiscotech · 2024-08-30T15:36:27Z

packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol

+            );
+        } catch {
+            // 7
+            assert(false);


couldn't it fail when the length of relayed messages is 0 and then we need to check that if it failed was for that reason?

in that case the revert will be internal to this contract and not easy to try/catch, but we can safely ignore it in that case and medusa will re-try more often the call combinations where relays happen after queueing messages, since that leads to more coverage

0xDiscotech · 2024-08-30T15:47:33Z

packages/contracts-bedrock/test/properties/medusa/fuzz/Protocol.guided.t.sol

+    /// @custom:property relayERC20 increases sender's balance in the destination chain exactly by the input amount
+    /// @custom:property-id 7
+    /// @custom:property calls to relayERC20 always succeed as long as the cross-domain caller is valid
+    function fuzz_RelayERC20(uint256 messageIndex) external {


nit

Suggested change

function fuzz_RelayERC20(uint256 messageIndex) external {

function fuzz_RelayERC20(uint256 messageIndex) external {

* 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

…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 <agusnduha@gmail.com> Co-authored-by: 0xng <ng@defi.sucks> Co-authored-by: teddy <teddy@defi.sucks> * 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 <131301107+0xDiscotech@users.noreply.github.com> Co-authored-by: agusduha <agusnduha@gmail.com> Co-authored-by: 0xng <ng@defi.sucks>

0xteddybear force-pushed the test/non-atomic-bridging branch from 04bcb7d to e6e715e Compare August 23, 2024 00:04

0xteddybear marked this pull request as ready for review August 23, 2024 00:19

simon-something reviewed Aug 23, 2024

View reviewed changes

packages/contracts-bedrock/test/properties/helpers/MockL2ToL2CrossDomainMessenger.t.sol Show resolved Hide resolved

simon-something approved these changes Aug 23, 2024

View reviewed changes

0xteddybear force-pushed the test/superc20-tob-properties branch from 85c1548 to 3b1af6c Compare August 23, 2024 18:36

0xteddybear force-pushed the test/non-atomic-bridging branch from d952a14 to ec3ae67 Compare August 23, 2024 18:47

0xteddybear requested a review from simon-something August 23, 2024 18:48

0xteddybear changed the base branch from test/superc20-tob-properties to test/state-transitions August 26, 2024 13:01

0xteddybear force-pushed the test/non-atomic-bridging branch 2 times, most recently from 7993afa to 1760e4a Compare August 29, 2024 15:12

0xteddybear added 11 commits August 29, 2024 19:28

test: changed mocked messenger ABI for message sending but kept asser…

f32a0d1

…tions the same

docs: add new properties 26&27

03ba03c

test: queue cross-chain messages and test related properties

643b70e

test: relay random messages from queue and check associated invariants

f99bdfe

chore: rename bridge->senderc20 method for consistency with relayerc20

5d4ba04

test: not-yet-deployed supertokens can get funds sent to them

023fb00

chore: medusa runs forever by default

c53fb6a

doable since it also handles SIGINTs gracefully

chore: document the reason behind relay zero and send zero inconsiste…

86d61de

…ncies

fix: feedback from doc

71d9c01

fix: walk around possible medusa issue

e0cd4be

I'm getting an 'unknown opcode 0x4e' in ProtocolAtomic constructor when calling the MockL2ToL2CrossDomainMessenger for the first time

test: unguided handler for sendERC20

c40737d

0xteddybear force-pushed the test/non-atomic-bridging branch from 1760e4a to c40737d Compare August 29, 2024 23:03

0xteddybear changed the base branch from test/state-transitions to feat/invariant-testing August 30, 2024 02:50

0xteddybear requested a review from 0xDiscotech August 30, 2024 14:22

0xDiscotech reviewed Aug 30, 2024

View reviewed changes

fix: feedback from disco

85d9b76

0xteddybear requested a review from 0xDiscotech September 2, 2024 14:36

0xDiscotech approved these changes Sep 2, 2024

View reviewed changes

0xteddybear merged commit 553deb9 into feat/invariant-testing Sep 2, 2024
3 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

test: fuzz non atomic bridging #31

test: fuzz non atomic bridging #31

0xteddybear commented Aug 22, 2024

simon-something left a comment

0xDiscotech left a comment

0xDiscotech Aug 30, 2024

0xDiscotech Aug 30, 2024

0xDiscotech Aug 30, 2024

0xDiscotech Aug 30, 2024

0xteddybear Aug 30, 2024

0xDiscotech Sep 2, 2024

0xDiscotech Aug 30, 2024

0xteddybear Aug 30, 2024

0xDiscotech Aug 30, 2024

		for (uint256 deploySaltIndex = 0; deploySaltIndex < ghost_totalSupplyAcrossChains.length(); deploySaltIndex++) {
		uint256 totalSupply = 0;

	function fuzz_RelayERC20(uint256 messageIndex) external {
	function fuzz_RelayERC20(uint256 messageIndex) external {

test: fuzz non atomic bridging #31

test: fuzz non atomic bridging #31

Conversation

0xteddybear commented Aug 22, 2024

simon-something left a comment

Choose a reason for hiding this comment

0xDiscotech left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment