Purpose

The goal here is to describe the expected behaviour of a DisputeGame.sol smart contract in a way that facilitates the security analysis found below. This is important to Optimism; it is also important for us, as we plan to write a formal verification of the dispute protocol.

The explicit description also hopefully serves as an implementation guide.

Originally, we believed Arbitrum implemented a different protocol, where "machine state roots" were laid out as the leaves of a Merkle tree in advance. More recently, we realized that Arbitrum implemented the same protocol, with some additional Arbitrum-specific logic. So, this document may also serve as an informal specification of the core logic of Arbitrum's bisection protocol.

Context

Suppose Alice & Bob wish to use Layer 1 to dispute some abstract state transition S -> S', but verifying the transition S -> S' is very expensive. A DisputeGame enables this by breaking S->S' into a sequence of smaller state transitions S_0 -> S_1, S_1 ->S_2, ..., S_{n-1} -> S_n, where

• S_0 = S
• S_n = S'
• each S_i -> S_{i+1} transition is possible to be verified on-chain.

It then "dissects" the sequence of smaller state transitions, coercing Alice or Bob to commit to a transition S_i -> S_{i+1} that can be directly invalidated on-chain.

The DisputeGame contract may be used in multiple places of the overall Optimism dispute protocol; therefore, it will be engineered to support at least the following cases:

1. Given an execution trace generated by a single transaction from a starting state root, dispute the validity of the resulting state root by narrowing down to a sequential pair of machine states M_i, M_{i+1}, and directly validating or invalidating the M_i -> M_{i+1} transition through a SingleStepVerifier.
2. Given a state root R, a list of transactions [tx1, tx2, ..., txn], and a final state root R', construct an array of state roots r where r[0] = R, and r[k] is constructed by applying tx_k to state root r[k-1]. Dispute the transition from r[0] to r[n] by pointing to a single (allegedly) invalid transition r[k] -> r[k+1], and running the dispute game a second time to determine the validity of this transition.

We can imagine some function progress which acts as a "source of truth" that defines a "correct sequence of bytes32 values":