Support Nary=4, draft version #31

JustXxx · 2024-06-03T16:24:43Z

Test:
forge test --mc FaultDisputeGameN_Test --mt test_step_duplicateStep_reverts -vvv

qizhou · 2024-06-20T00:12:45Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

@@ -88,7 +91,7 @@ contract FaultDisputeGame is IFaultDisputeGame, Clone, ISemver {
    bool internal initialized;

    /// @notice Bits of N-ary search
-    uint256 nBits;


You can change nBits to immutable to reduce gas cost.

qizhou · 2024-06-20T00:16:06Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

+    }
+
+    function getClaim(ClaimData memory _data) public pure returns (Claim claim_) {
+        // claim + offset


I think we should add a TODO here to integrate libDA in future.

blockchaindevsh · 2024-06-22T00:50:28Z

Is there a summary for the PR?

blockchaindevsh · 2024-06-22T00:54:06Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

        uint256 nextPositionDepth = nextPosition.depth();

        // INVARIANT: A defense can never be made against the root claim of either the output root game or any
        //            of the execution trace bisection subgames. This is because the root claim commits to the
        //            entire state. Therefore, the only valid defense is to do nothing if it is agreed with.
-        if ((_challengeIndex == 0 || nextPositionDepth == SPLIT_DEPTH + 2) && !_isAttack) {
+        if ((_challengeIndex == 0 || nextPositionDepth == SPLIT_DEPTH + 2 * N_BITS) && 0 != _attackBranch) {


I've 2 questions here:

Should the condition be (1 << N_BITS) - 1 != _attackBranch ?

Why is the 2 * N_BITS necessary here?

From my understanding:

should be attachBranch !=0, because the root claim (which only lies in the first branch) can't be defended

because the depth definition using 2-ary depth

The root is that the root claim of a block transition is a sub claim of a block-level-output claim at depth SPLIT_DEPTH. Since a block-level-output claim at depth SPLIT_DEPTH has only one sub-claim, i.e., the root claim, the following claims at SPLIT_DEPTH + 2 can only attack the root claim (_attackBranch must be 0).

blockchaindevsh · 2024-06-22T01:01:37Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

        uint8 vmStatus = uint8(_rootClaim.raw()[0]);

-        if (_isAttack || disputed.position.depth() % 2 == SPLIT_DEPTH % 2) {
+        if ((0 != _attackBranch) || (disputedPos.depth() / N_BITS) % 2 == (SPLIT_DEPTH / N_BITS) % 2) {


_isAttack should correspond to (1 << N_BITS) - 1 != _attackBranch?

Have the same concern

Develop

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

qizhou · 2024-06-24T01:22:05Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

@@ -887,10 +911,11 @@ contract FaultDisputeGame is IFaultDisputeGame, Clone, ISemver {
        // If the move is a defense, the disputed output could have been made by either party. In this case, we
        // need to search for the parent output to determine what the expected status byte should be.
        Position disputedLeafPos = Position.wrap(_parentPos.raw() + 1);


I believe this line is incorrect for Nary > 2 cases - the purpose is to find the position of the post claim hash and thus it should be _parentPos.raw() + _attackBranch.

qizhou · 2024-06-24T01:56:43Z

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol

@@ -960,14 +983,13 @@ contract FaultDisputeGame is IFaultDisputeGame, Clone, ISemver {
        // Walk up the DAG until the ancestor's depth is equal to the split depth.
        uint256 currentDepth;


This function (_findStartingAndDisputedOutputs) should also be updated. Especially for line 1002, wasAttack should be replaced by attachBranch and then use the parameter to find the starting and disputed outputs accordingly.

…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]>

support Nary=4, draft version

bce9859

JustXxx requested a review from qizhou June 3, 2024 16:24

This was referenced Jun 4, 2024

EthStorage Devs Meeting #83 Agenda ethstorage/pm#91

Closed

QKC/OP Devs Meeting #4 Agenda ethstorage/pm#92

Closed

billxu added 2 commits June 11, 2024 00:11

Support Nary=4

031ccdd

Remove redundant code

4a7affb

JustXxx mentioned this pull request Jun 11, 2024

EthStorage Devs Meeting #84 Agenda ethstorage/pm#93

Closed

qizhou requested review from zhiqiangxu and dajuguan June 14, 2024 00:40

Assuming that SPLIT_DEPTH and MAX_GAME_DEPTH must be multiples of nBits

b656edb

qizhou reviewed Jun 20, 2024

View reviewed changes

Rewrite the _findTraceAncestor function

4d9b734

blockchaindevsh reviewed Jun 22, 2024

View reviewed changes

JustXxx mentioned this pull request Jun 22, 2024

QKC/OP Devs Meeting #6 Agenda ethstorage/pm#97

Closed

JustXxx and others added 2 commits June 23, 2024 23:05

Merge pull request #11 from ethstorage/develop

01089c5

Develop

remove old version code

dee83c0

github-advanced-security bot found potential problems Jun 23, 2024

View reviewed changes

packages/contracts-bedrock/src/dispute/FaultDisputeGameN.sol Dismissed Show dismissed Hide dismissed

JustXxx merged commit b37e73d into ethstorage:develop Jun 23, 2024
2 checks passed

qizhou reviewed Jun 24, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support Nary=4, draft version #31

Support Nary=4, draft version #31

JustXxx commented Jun 3, 2024 •

edited

Loading

qizhou Jun 20, 2024

qizhou Jun 20, 2024

blockchaindevsh commented Jun 22, 2024

blockchaindevsh Jun 22, 2024 •

edited

Loading

dajuguan Jun 24, 2024 •

edited

Loading

qizhou Jun 24, 2024

blockchaindevsh Jun 22, 2024 •

edited

Loading

dajuguan Jun 24, 2024 •

edited

Loading

qizhou Jun 24, 2024

qizhou Jun 24, 2024 •

edited

Loading

		@@ -960,14 +983,13 @@ contract FaultDisputeGame is IFaultDisputeGame, Clone, ISemver {
		// Walk up the DAG until the ancestor's depth is equal to the split depth.
		uint256 currentDepth;

Support Nary=4, draft version #31

Support Nary=4, draft version #31

Conversation

JustXxx commented Jun 3, 2024 • edited Loading

qizhou Jun 20, 2024

Choose a reason for hiding this comment

qizhou Jun 20, 2024

Choose a reason for hiding this comment

blockchaindevsh commented Jun 22, 2024

blockchaindevsh Jun 22, 2024 • edited Loading

Choose a reason for hiding this comment

dajuguan Jun 24, 2024 • edited Loading

Choose a reason for hiding this comment

qizhou Jun 24, 2024

Choose a reason for hiding this comment

blockchaindevsh Jun 22, 2024 • edited Loading

Choose a reason for hiding this comment

dajuguan Jun 24, 2024 • edited Loading

Choose a reason for hiding this comment

qizhou Jun 24, 2024

Choose a reason for hiding this comment

qizhou Jun 24, 2024 • edited Loading

Choose a reason for hiding this comment

JustXxx commented Jun 3, 2024 •

edited

Loading

blockchaindevsh Jun 22, 2024 •

edited

Loading

dajuguan Jun 24, 2024 •

edited

Loading

blockchaindevsh Jun 22, 2024 •

edited

Loading

dajuguan Jun 24, 2024 •

edited

Loading

qizhou Jun 24, 2024 •

edited

Loading