design-doc.md

Draft dispute game specification

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":

• in case 1, the SingleStepVerifier defines a correct sequence of "machine state fingerprints", terminating when the transaction is fully executed.
• in case 2, the correct sequence of state root transitions is defined by
  • setting r[0] = R'
  • initializing some machine state with state root r[k-1], transaction tx_k, and running the SingleStepVerifier until a terminal state is reached with state root r_final, setting r[k] = r_final

The following description is restricted in scope to correctness requirements, and ignores liveness requirements, assuming that the sequencer & challenger each act in a timely manner. The specific incentives & timeouts are not considered in this document.

Dispute game overview

DisputeGame.sol makes the following assumptions about "boundary conditions":

1. Alice has a fixed array a of bytes32 values.
2. Bob has a fixed array b of bytes32 values.
3. a[0] == b[0] and a[m] != b[n], where m = length(a) and n = length(b)
4. m <= n (if this is not true, switch Alice ←→ Bob)

# Alice & Bob's "local views" might be:

a = [0, 1, 2.1, 3, 4, 5.1, 6, 7.1]
b = [0, 1, 2,   3, 4, 5  , 6, 7, 8, 9, 10]

# in this case, m == 8 and n == 11

The arrays a and b may or may not be correct, as defined by the relevant "source of truth" progress function. (Assumption 4 implies that at most one of a and b are correct. DisputeGame.sol relies on another component of the rollup to verify assumption 4.)

Alice might "change her mind" during the progress of the game, but this doesn't really matter: we don't care about the values of a that are not revealed on-chain, only the values of a that are revealed. Once values of a are revealed, Alice has committed to them on-chain, and there's no going back.

So, we might as well pretend that a[i] is fixed in advanced to be the value that Alice would reveal if asked to reveal a[i].

The fact that a[0] == b[0] is crucial — it implies that Alice and Bob are starting in the same state.

Gameplay

Alice and Bob take turns revealing a[i] and b[i] for prescribed indices, "dissecting" the two arrays a and b, continuing until either:

• one party forfeits
• there are two sequential values x[i], x[i+1] revealed (x is either a or b) where x[i] -> x[i+1] can be invalidated on-chain. We call this outcome "proving fraud".

We outline a DisputeGame.sol specification as well as an off-chain protocol with the following property:

• if Alice is correct, then
  • either Alice moves last and Bob forfeits
  • or Bob moves last, and Alice can prove fraud
• if Bob is correct, then
  • either Bob moves last, and Alice forfeits
  • or Alice moves last, and Bob can prove fraud

DisputeGame.sol specification

For the rest of this document, division is integer division, rounded towards 0. (All numbers are positive.)

We assume some unspecified value k, the "splitting factor". (This is not specified, because we will need empirical tests to understand eg. the gas cost of various choices of k.)

Define index(i,k,low, high) = low + i * (high - low) / k

Initialization

Two values, numSteps and values, are provided to the constructor.

• values is validated to be of length k+1
• numSteps is validated to be at least 1.
• A storage variable lastMover is set to be Alice. (Alice is taking the first move during initialization.)
• values is recorded in storage.
• A storage value consensusIndex is initialized at 0.
• A storage value disputedIndex is initialized at numSteps.
• A storage value status is set to running

enum ChallengeStatus {
    InProgress,
    DisputeFinalized,
    Forfeited
}

contract ChallengeManager {
    bytes32 root;
    uint256 k;
    uint256 disputedindex;
    uint256 consensusIndex;
    string lastMover;
    ChallengeStatus status;

    constructor(
        bytes32[] memory _values,
        uint256 _numSteps,
        string memory _lastMover,
        uint256 _k
    ) {
        state values = _values;
        require(_k > 1, 'The splitting factor must be above 1');
        require(_numSteps >= 1, 'There must be at least one element');
        require(_values.length == _k + 1, 'There must be k+1 values');

        disputedindex = _numSteps;
        lastMover = _lastMover;
        k = _k;
        consensusIndex = 0;
        status = ChallengeStatus.InProgress;
    }
}

Offchain protocol: Alice provides "evenly spaced" values of a through the values variable. Explicitly, she provides values = a[index(i,k,0,numSteps)] for i = 0,...,k.

Sample behaviour:

Suppose the (local) views are:
a = [0, 1, 2.1, 3, 4, 5.1, 6, 7.1]
b = [0, 1, 2,   3, 4, 5  , 6, 7, 8, 9, 10]

# Initialization; Alice commits to numSteps = 8, reveals a[0], a[3] and a[7]
# This data is now viewable on L1
a = [ 0, _, _, 3, _, _, _, 7.1 ]
b = [ _, _, _, _, _, _, _, _   ]

      lo                   hi

lo = consensusIndex
hi = disputedIndex
values = [0,3,7.1]
lastMover = Alice

Splitting

Alice and Bob alternate providing values. Since Alice was the last value provider during initialization, it's Bob's move. Bob moves by calling a function split:

split(i: number, newValues: bytes32[], mover)

On-chain behaviour:

split has the following behaviour:

1. It checks that newValues is an array of length k
2. It checks that i < k
3. It checks that newValues[k-1] != values[i+1]
4. It checks that disputedIndex - consensusIndex > k
5. It checks that mover is one of [Alice, Bob], and mover != lastMover
6. It sets consensusIndex = index(i, k, consensusIndex, disputedIndex)
7. It sets disputedIndex = index(i+1, k, consensusIndex, disputedIndex)
8. It sets values = [values[i], ...newValues]
9. It sets lastMover = mover

Off-chain protocol: The current mover

• iterates through i = 0,...,k to find the last i such that values[i] == x[index(i, k, consensusIndex, disputedIndex)], where x is their "local view".
• sets newConsensusIndex = index(i, k, consensusIndex, disputedIndex)
• sets newDisputedIndex = index(i+1, k, consensusIndex, disputedIndex)
• sets newValues = x[index(j, k, newConsensusIndex, newDisputedIndex) for j = 1,...,k])
• calls DisputeGame.split(i, newValues)

Sample behaviour:

Suppose the (local) views are:
a = [0, 1, 2.1, 3, 4, 5.1, 6, 7.1]
b = [0, 1, 2,   3, 4, 5  , 6, 7, 8, 9, 10]

# Initialization
a = [ 0, _, _, 3, _, _, _, 7.1 ]
b = [ _, _, _, _, _, _, _, _   ]
      lo                   hi

# Bob agrees with a[3] but disagrees with a[7], and calls split(1, [5,7])
a = [ 0, _, _, 3, _, _, _, 7.1 ]
b = [ _, _, _, 3, _, 5, _, 7   ]
               lo          hi

# now, the values in storage are
consensusIndex = 3
disputedIndex = 7
values = [3,5,7]
lastMover = Bob

# Alice agrees with b[3] but disagrees with b[5], and calls split(0, [4,5.1])
a = [ 0, _, _, 3, 4, 5.1, _, 7.1 ]
b = [ _, _, _, 3, _, 5,   _, 7   ]
               lo    hi

# now, the values in storage are
consensusIndex = 3
disputedIndex = 7
values = [3,4,5.1]
lastMover = Alice

Terminating the game

Detecting fraud

When disputedIndex - consensusIndex <= k, no party can call split. Instead, they must finish the game by either "forfeiting" or "pointing fraud".

In this case, Bob knows that 4 -> 5.1 is an incorrect transition

a = [ 0, _, _, 3, 4, 5.1, _, 7.1 ]
b = [ _, _, _, 3, _, 5,   _, 7   ]
               lo    hi

consensusIndex = 3
disputedIndex = 7
values = [3,4,5.1]
lastMover = Alice

So, Bob would finish the game by calling claimFraud(1).

claimFraud(i: number)

On-chain behaviour:

claimFraud(i) has the following behaviour:

• it validates that index(i+1, k, consensusIndex, disputedIndex) = index(i, k, consensusIndex, disputedIndex) + 1
• it sets the game as "terminated" in a "fraud claimed" state.

The exact behaviour is unspecified, but an external contract should be able to read:

• who the lastMover was
• that the game terminated in a "fraud claimed" state

An external contract can then use a SingleStepVerifier to prove fraud for use case (1), or launch a second dispute game for use case (2).

Off-chain protocol: If a mover knows they can prove fraud about the values[i] -> values[i+1] transition for some i, they call claimFraud(i).

Forfeiting

Suppose the game instead ended up in this state:

a = [ _, _, _, 3, _, 5.1, _, 7.1 ]
b = [ 0, _, _, 3, 4, 5,   _, 7   ]
               lo    hi

consensusIndex = 3
disputedIndex = 5
values = [3,4,5]
lastMover = Bob

On-chain behaviour:

In this case, Alice is the next mover, but she knows she won't be able to prove fraud. She should be able to finish the game by calling forfeit.

forfeit();

Perhaps Alice should be able to forfeit at any point! Therefore, forfeit should have the following behaviour:

• it sets the game as "terminated" in a "fraud claimed" state

But, to simplify the security analysis, we assume it has the following behaviour:

• it validates that disputedIndex <= consensusIndex + k
• it sets the game as "terminated" in a "fraud claimed" state

Off-chain protocol: If a mover cannot split, and recognizes that they will lose, they call forfeit.

Interface

For now, the interface is defined in Typescript, although the interface will later be converted to Solidity.

class ChallengeManager {
  public k: number;
  public consensusIndex: number = 0;

  constructor(
    public values: Bytes32[],
    public disputedIndex: number, // Set by the first mover
    public mover: string
  ) {}

  split(i: number, values: Bytes32[]): void {}

  claimFraud(i: number): void;
}

Protocol analysis

We would like to show that given a dispute where Alice and Bob disagree:

• When a player is taking a turn, the game contains a state with which a player agrees and a state with which the player disagrees.
• The game terminates (quickly).
• On termination, the dispute is correctly resolved.

The game maintains a window around a disputed transition

Claim: When the off-chain protocol is followed, the game (almost) maintains the following invariant:

• a[consensusIndex] == b[consensusIndex] and a[disputedIndex] != b[disputedIndex]

Proof:

The game is initialized in a state where a[consensusIndex] == b[consensusIndex].

It's possible that a[disputedIndex] == b[disputedIndex] at the start of the game. Ignore this possibility!

forfeit and claimFraud do not alter storage values other than the "termination status".

Consider split(i, newValues) .

When Bob is taking a turn, is it possible Bob is unable to find a value with which Bob agrees?

1. On split, consensus value is updated. values[0] is replaced with oldValues[i]
2. For the second turn (first split call): Bob must agree with at least oldValues[0] by definition of the game.
3. For the third turn or later turns (second or subsequent split calls): On the turn before, Alice set oldValues[0] to oldValues'[i] , where oldValues' were supplied by Bob on his turn. So Bob must agree with at least oldValues[0]
4. So the invariant a[consensusIndex] == b[consensusIndex] is maintained on every turn.

When Bob is taking a turn, is it possible that Bob is unable to find a value with which Bob disagrees?

1. On split, disputed value is updated. values[k] is replaced with newValues[k-1]. The updated value must differ from a value previously stored (by definition of the game).
2. For the second turn (first split call: Bob must disagree with at least oldValues[k] by definition of the game.
3. For the third turn or later turns (second or subsequent split calls): On the turn before, Alice set oldValues[k] to x where x != oldValues'[i]. oldValues' were supplied by Bob on his turn. So Bob must disagree with at least oldValues[k].
4. The invariant a[disputedIndex] != b[disputedIndex] is maintained on throughout the game.

The game terminates quickly

Claim: The game terminates in log_k(m) rounds, where m is the total number of states.

Proof:

1. The game starts with consensusIndex == 0 and disputedIndex == m.
2. For a turn t, consensusIndex is updated to consensusIndex = oldConsensusIndex + m*i/k^t
3. For a turn t, disputedIndex is updated to consensusIndex = oldConsensusIndex + m*(i+1)/k^t
4. So after a turn, disputedIndex - consensusIndex = m/k^t
5. The game terminates when disputedIndex - consensusIndex = m/k^t ≤ k
   1. Solving for t, log_k(m) ≤ t+1

When terminated, the dispute is correctly resolved

Claim:

• If Alice was correct
  • if Bob was the last mover, then Alice has proven fraud
  • if Alice was the last mover, then Bob cannot prove fraud
• If Bob was correct
  • if Alice was the last mover, then Bob has proven fraud
  • if Bob was the last mover, then Alice cannot prove fraud

Proof:

The game starts with a set of states provided by Alice [a_0, a_s, a_2*s ..., a_(k-1)*s, a_n]. If there is a sequence of valid transitions between a_0 and a_n that includes the intermediate states, then:

• If the game terminates, there are only valid transitions between states, and Alice is the last mover.
• On Bob's turn:
  • The states are updated to [a_i, b_i+s', b_i+2*s', ... b_i+k*s']
  • the consensus state is updated to one of Alice's, correct states.
  • the disputed state is updated to an incorrect state. b_i+k*s' must not equal to a_i+k*s'
  • intermediates states are supplied. The intermediate states are either correct states that follow the consensus state or include an incorrect state.
  • If the game terminates, then the states include an invalid transition, and Bob is the last mover.
• On Alice's next turn:
  • The states are updated to [b_i', a_i'+s", a_i'+2*s", ... a_i'+k*s"]
  • Alice sets the consensus state to the last correct, intermediate state that Bob supplied. Bob's state after the consensus state must be invalid. Alice sets the correct, disputed state. Alice sets intermediate states to valid states that lead to the correct, disputed state.
  • If the game terminates, there are only valid transitions between states, and Alice is the last mover.
• Alice's and Bob's next moves follow the same logic.

The other option is that the game starts with a set of states provided by Alice [a_0, a_s, a_2*s ..., a_(k-1)*s, a_n] where there is no sequence of valid transitions between a_0 and a_n that includes the intermediate states. The proof for this case is very similar to the proof above. The game status is equivalent to Bob's turn in the proof above with Alice and Bob's roles reversed.

Optimizations

Storage

Since storage is expensive, DisputeGame.sol should not store values. Instead, the contract should store a commitment to values, such that the next mover can prove to the contract:

• values[i] = v_0
• values[i+1] = v_1

One option is for the contract to construct a merkle tree whose leaves have values taken from values, and storing the root of this tree.

The interface would then look like the following:

enum ChallengeStatus {
    InProgress,
    FraudDetected,
    Forfeited
}

struct WitnessProof {
    bytes32 witness;
    uint256 index;
    bytes32[] nodes;
}

contract DisputeManager {
    bytes32 root;
    uint256 immutable splitFactor;
    uint256 disputedIndex;
    uint256 consensusIndex;
    string lastMover;
    ChallengeStatus public currentStatus;
    uint256 public fraudIndex;

    constructor(
        bytes32[] memory _values,
        uint256 _numSteps,
        string _lastMover,
        uint256 _splitFactor
    ) {
        root = MerkleUtils.generateRoot(_values);

    }

    function forfeit(Mover _mover) external


    function claimFraud(uint256 index, Mover _mover) external

    function split(
        WitnessProof calldata _consensusProof,
        bytes32[] calldata _hashes,
        WitnessProof calldata _disputedProof,
        Mover _mover
    ) external

split and claimFraud should validate each Witness against the stored merkleRoot, which serves as a proof that values[witness.index] == witness.value.