Proving and Challenge Protocol

This document details the mechanisms for proving correct execution and resolving disputes in the Rollup Protocol. It explains how the system separates ordinary execution from proving, transforms WASM into a specialized proving format (WAVM), and employs interactive fraud proofs to resolve disputes efficiently.

1. Separating execution from proving

One of the key challenges in designing a practical Rollup system is balancing fast, ordinary execution with the need for reliable proofs of that execution. Nitro addresses this challenge by using the same source code for both purposes but compiling it to different targets:

• Execution compilation:
  • The Nitro node software is compiled with the ordinary Go compiler into native code for the target architecture.
  • This native binary is distributed as source code and as a Docker image, making it deployable on various nodes.
• Proving compilation:
  • For proving, only the portion of the code that is the State Transition Function (STF) gets compiled by the Go compiler into WebAssembly (WASM).
  • The generated WASM code transforms into a specialized format called WAVM.
  • In any dispute regarding the STF, the WAVM code is referenced to resolve the correct result.

2. WAVM: A specialized proving format

WAVM is a modified version of WASM designed to meet the needs of fraud proofs. The following features describe it:

• Portability and Structure:
  • WASM was selected because it is portable, well-specified, and supported by robust tools.
• Modifications made in WAVM:
  • Removal of unused features:
    • WAVM removes some WASM features that the Go compiler never generates. The transformation phase ensures these features are absent.
  • Restrictions on certain features:
    • Floating-point instructions: WAVM does not contain floating-point instructions. Instead, any floating-point operations get replaced by calls to the Berkeley SoftFloat library.
      • Rationale: Using software floating-point libraries reduces the risk of incompatibilities between different architecture.
  • Nested control flow:
    • WAVM flattens control flow constructs by converting them into jump instructions.
  • Variable-time instructions: -Some instructions in WASM may take a variable amount of time to execute. WAVM transforms these into constructs with fixed-cost instructions to simplify proving.
  • Additional opcodes for blockchain interaction:
    • WAVM adds new opcodes to enable the code to interact with the blockchain environment.
    • For example, new instructions allow the WAVM code to read and write the chain's global state, retrieve the next message from the chain's inbox, or signal a successful end to the STF execution.

3. ReadPreImage and the hash oracle trick

An interesting instruction in WAVM is ReadPreImage, which the "hash oracle trick" uses. This mechanism works as follows:

• Functionality of ReadPreImage:
  • Input: A hash H and an offset I.
  • Output: The word of data at offset I in the preimage of H along with the number of bytes written (zero if I is at or beyond the end).
• Constraints for safety:
  • Generating a preimage for an arbitrary hash is infeasible. Therefore, the instruction is allowed only when:
    • The preimage is publicly known
    • The preimage's size is known to be less than a fixed upper bound (approximately 110 kbytes).
• Usage examples in Nitro:
  • State tree access:
    • Nitro's state tree is stored offchain as a Merkle tree, with nodes indexed by their Merkle hashes.
    • The STF only stores the root hash but can retrieve any node's contents using ReadPreImage.
  • Block headers:
    • The instruction fetches recent publicly known child chain block headers of bounded size.

Historical Note

This "hash oracle trick" originates from the original Arbitrum design, where the Merkle hash of a data structure is stored and full contents are retrievable on demand.

4. Resolving disputes using interactive fraud proofs

Disputes resolution in optimistic Rollups is a critical design decision. The protocol must decide which execution version is correct when two parties disagree.

4.1 Overview of dispute resolution

• Optimistic Rollups:
  • Assume that assertions about execution are correct unless challenged.
• Dispute Resolution Options:
  • Interactive proving:
    • Parties engage in a challenge game to narrow down the dispute executed steps.
  • Re-executing transactions:
    • The parent chain re-executes transactions, checking each state transition.

note

Zero-knowledge Rollups avoid the dispute situation by directly proving correctness via ZK proofs.

4.2 Interactive proving

Arbitrum favors interactive proving due to its efficiency and flexibility.

The interactive proving process

1. Initial claim and dispute start:
   • Suppose Alice claims that the chain will produce a specific result. Bob disagrees.
2. Bisection of the dispute:
   • First round:
     • Alice posts an assertion covering N steps.
     • Bob challenges the assertion.
     • Alice then provides two sub-assertions, each covering N/2 steps.
   • Subsequent rounds:
     • Bob chooses one half to challenge, and the process repeats––halving the disputed steps until only a single instruction remains.
3. Final one-step proof:
   • Once the dispute narrows to a single execution step, the parent chain referee verifies that one-step claim.

Simplified bisection protocol

• Step-by-step breakdown:
  • Alice provides a commitment to the entire computation history.
  • She bisects her claim into two halves.
  • Bob selects the half he disputes.
  • This iteration of the bisection continues until the dispute reaches a single instruction.

Why bisection correctly identifies a cheater

1. If Alice's claim is correct:
   • Every bisection provides truthful intermediate states.
   • Bob's challenge eventually leads to a correct one-step proof, allowing Alice to win.
2. If Alice's claim is incorrect:
   • One of Alice's halves will be false at some bisection.
   • Bob can always choose the incorrect half, ultimately forcing an incorrect one-step proof that is not verifiable.
   • Thus, an honest party will always be able to challenge a dishonest claim.

4.3 Re-executing transactions (alternative approach)

• Mechanism:
  • Each transaction would include a state hash after its execution.
  • In case of a dispute, the parent chain would re-execute every transaction to verify the correctness.
• Drawbacks:
  • Requires a state claim for every transaction, increasing computational load.
  • In a dispute, the entire transaction must be re-executed onchain, leading to high gas costs.

info

Interactive proving is more efficient in optimistic and pessimistic cases, as it minimizes onchain computation and adapts to Ethereum's gas limits.

5. Interactive fraud proofs and the challenge protocol

Interactive fraud proofs form the basis for resolving proposer disputes when conflicting assertions are made.

5.1 Dispute scenario

• Example setup:
  • Suppose the Rollup chain includes assertions 93 and 95, which are siblings (both following assertion 92).
  • Alice is bonded on assertion 93, while Bob is bonded on assertion 95.
  • Bob's bonding on 95 implies that assertion 93 must be incorrect.
• Initiation of the challenge:
  • An interactive challenge is initiated automatically when two proposers place bonds on sibling assertions.
  • Multiple assertions may participate in a single challenge.
  • The protocol records and referees the challenge and eventually declares a winner, confiscating the bonds of the losing parties and removing them as proposers.

5.2 The two-phase challenge game

1. Bisection phase:
   • The goal is to narrow the dispute to a single execution step.
   • At each stage, claims are bisected into smaller segments (first over child chain blocks, then over "big steps" of 2²⁶ instructions, and finally to a single instruction).
   • The parent chain referee only checks that the moves have "the right shape" (e.g., that the bisection was performed correctly) without evaluating the correctness of execution.
2. One-step proof phase:
   • Once the dispute reduces to one instruction, any player can initiate the one-step proof.
   • The parent chain executes the disputed instruction using the proof data provided.
   • If the one-step proof is correct, the disputed edge is confirmed, and the challenges resolves.

5.3 Efficiency considerations

• Optimistic case:
  • Interactive proving allows a single assertion to cover all transactions in a block.
• Pessimistic case:
  • Only one instruction is re-executed onchain during a dispute.
• Gas limits:
  • The interactive proving model can work with higher per-transaction gas limits since most work is done offchain.
• Implementation flexibility:
  • The system only requires verification a one-step proof onchain, rather than full transaction re-execution.

5.4 ChallengeManager: The arbiter

• Role:
  • The ChallengeManager contract arbitrates the challenge game.
  • It tracks assertion histories, timers, and state commitments.
• State machine:
  • A state machine represents the challenge with several distinct phases:
    • Block challenge:
      • The challenge begins by bisecting over global states (including block hashes) to narrow down the dispute to a single block.
    • Big-step execution challenge:
      • Upon identifying the block, the execution challenge bisects a "chunk" of 2²⁶ instructions.
    • Small-step execution challenge:
      • This phase bisects the chunk until the dispute narrows to a single instruction.
    • One-step proof:
      • A final onchain one-step proof confirms the disputed instruction.
• Winning the challenge:
  • Winning is not instantaneous; a built-in time delay safeguards against erroneous challenge resolutions.
  • This delay allows time for diagnosing and correcting errors via contract upgrades if necessary.

6. One-step proof assumptions

The one-step proof (OSP) is the final arbiter of a single disputed instruction. Its design accounts for several key assumptions:

6.1 Assumptions for correct execution

• Correct cases:
  • In a challenge involving at least one honest party, the honest side will always prove a reachable case.
  • An arbitrator generates the WAVM code (from a valid WASM compile) and should not encounter unreachable cases in correct execution.

6.2 Handling unreachable cases

• Definition:
  • An unreachable case is a situation that is assumed never to arise during correct execution.
• Behavior in malicious challenges:
  • In challenges between malicious assertions, unreachable cases may occur and can be handled arbitrarily by the one-step proof.
• Safety in honest challenges:
  • An honest party never needs to prove an unreachable case.
  • If a dishonest party attempts to force an unreachable case, it will be preceded by an invalid reachable case, ensuring that the dishonest party eventually loses the challenge.

6.3 Additional safety assumptions

• WAVM code validity:
  • The WAVM code produced by the arbitrator comes from valid WASM compile. It is checked using wasm-validate from the WebAssembly Binary Toolkit (WABT).
• Inbox message size:
  • Inbox messages must be small enough (no larger than 117,964 bytes) to be fully available for proving.
• Preimage requests:
  • Preimages requested via ReadPreImage must be known and within the size limit (117,964 bytes).
  • Examples include block headers, state trie nodes, and recent child chain block headers.

7. WASM to WAVM transformation

Not all WASM instructions are mapped directly 1:1 to WAVM opcodes. The transformation design simplifies execution for proving and enables additional blockchain interactions.

7.1 Transformation process overview

• Source:
  • The Go compiler produces WASM code.
• Transformation:
  • A simple transformation stage converts the WASM code into WAVM code.
• Purpose:
  • Ensure that the WAVM code is free from unused features, restricted in its functionality where necessary, and augmented with additional opcodes for blockchain interaction.

7.2 Key differences between WASM and WAVM

• Removed features:
  • Any WASM features not generated by the Go compiler are removed.
• Restricted features:
  • Berkeley SoftFloat library calls replace floating-point instructions.
  • The nested control flow flattens into jumps.
  • Variable-time instructions transform into fixed-cost instructions.
• Added opcodes:
  • New opcodes additions for interacting with the blockchain (e.g., reading global state, fetching inbox messages, signaling completion).

7.3 Translation of specific WASM constructs

• Block and loop:
  • In WASM, blocks contain instructions and branch instructions for exiting blocks.
  • In WAVM, since instructions are flat, branch instructions are replaced with jumps to predetermined destinations.
• If and Else:
  • Translated into a block with an ArbitraryJumpIf instructions.
    • Structure example:
      • Begin block with endpoint end
      • Conditional jump to else block
      • [if-statement instructions]
      • Unconditional branch (to skip else)
      • Else block: [else-statement instructions]
      • End block
• Branch instructions (br and br_if):
  • Translated into ArbitraryJump and ArbitraryJumpIf with jump destinations known at compile time.
• Branch table (br_table):
  • Translated to a series of conditional checks for each possible branch, with a default branch if no conditions are met.
• Local.tee:
  • Implemented by duplicating the local value (using a Dup opcode) followed by a LocalSet.
• Return:
  • The function signature knows the number of return values:
    • A MoveFromStackToInternal opcode is added for each return value.
    • A loop uses IsStackBoundary to clean up the stack.
    • Finally, MoveFromInternalToStack opcodes are added for each return value, followed by a Return opcode.
• Floating-point instructions:
  • f32 and f64 values are bitcast to i32 and i64.
  • Cross-module calls go to the floating-point library.
  • Return values are bitcast back to floating-point types.

7.4 WAVM custom opcodes not in WASM

WAVM includes several unique opcodes that simplifying proving. They breakdown into several categories:

Invariants and Codegen internal opcodes

• General assumptions:
  • Many opcodes assume specific items on the stack (e.g., "pops an i32" means the top stack item must be an i32`).
  • WASM validation and arbitrator code generation maintain these invariants.
• Examples of custom opcodes:

Opcode	Name	Description
0x8000	EndBlock	Pops an item from the block stack.
0x8001	EndBlockIf	Peeks the top value (assumed i32) and, if non-zero, pops an item from the block stack.
0x8002	InitFrame	Pops a caller module index (i32), a caller module internals offset (i32), and a return InternalRef; creates a stack frame with these details and the locals Merkle root.
0x8003	ArbitraryJumpIf	Pops an i32; if non-zero, jumps to the program counter provided in the argument data.
0x8004	PushStackBoundary	Pushes a stack boundary marker onto the stack.
0x8005	MoveFromStackToInternal	Pops an item from the stack and pushes it to an internal stack.
0x8006	MoveFromInternalToStack	Pops an item from the internal stack and pushes it back onto the stack.
0x8007	IsStackBoundary	Pops an item from the stack; if it is a stack boundary, pushes an i32 with value 1; otherwise, 0.
0x8008	Dup	Peeks at the top stack item and pushes a duplicate.

Linking opcode

• Purpose:
  • Generated for linking modules together:
• Opcode:

Opcode	Name	Description
0x8009	CrossModuleCall	Pushes current program counter, module number, and module internals offset; splits the argument data into function index and module index; jumps to the beginning of that function.

Host calls

• Used in host call implementations:
  • They enable libraries to perform host calls and access the caller's memory.
• Examples of host call opcodes:

Opcode	Name	Description
0x800A	CallerModuleInternalCall	Pushes the current program counter, module number, and module internals offset; retrieves caller module internals offset; jumps to caller module function if valid, otherwise errors.
0x8010	GetGlobalStateBytes32	Pops a pointer and index; writes the global state bytes32 value (if all alignment and bounds checks pass) to the pointer.
0x8011	SetGlobalStateBytes32	Pops a pointer and index; reads a bytes32 value from memory and writes it into the global state.
0x8012	GetGlobalStateU64	Pops a pointer and index; writes the global state u64 value to memory (with alignment and bounds checking).
0x8013	SetGlobalStateU64	Pops a pointer and index; reads a u64 from memory and writes it into the global state.
0x8020	ReadPreImage	Pops an offset and pointer; reads a 32-byte Keccak-256 hash from memory; writes up to 32 bytes of its preimage starting from the offset; pushes the number of bytes written.
0x8021	ReadInboxMessage	Pops an offset, pointer, and i64 message number; attempts to read an inbox message; if out-of-bounds, enters a “too far” state; writes up to 32 bytes and pushes the number of bytes written.
0x8022	HaltAndSetFinished	Sets the machine status to finished, halting execution and marking it as successful.

8. WAVM floating-point implementation

Floating-point operations in WAVM are handled differently to ensure determinism and consistency:

• Implementation using Berkeley SoftFloat:
  • Instead of implementation IEEE 754-2019 directly in WAVM, floating-point instructions are replaced with calls to the Berkeley SoftFloat-3e library.
  • The soft float library is linked, and floating-point operations are implemented via cross-module calls.
• Known divergences:
  • For example, floating-point to integer truncation will saturate on overflow (instead of erroring), which is safer and more consistent with x86 behavior.
  • These divergences follow proposals (e.g., saturating opcodes) that are not yet widely adopted.

9. WAVM modules and linking

WASM's notion of modules is extended in WAVM to support multi-module programs. This extension allows:

9.1 Entrypoint module

• Definition:
  • The entry point module is the starting point of execution.
• Behavior:
  • It calls any modules' start functions if specified.
  • If then calls the main module's main function:
    • For Go:
      • Sets argv to ["js"] (to mimic the JS environment) and calls run.
    • For Rust:
      • Simply calls main with no arguments.

9.2 Library exports

• Export naming convention:
  • Libraries export function using the pattern module__name.
  • This convention allows future libraries or the main module to import these functions.
• Example:
  • The wasi-stub library provides functions that Rust imports, adhering to the WebAssembly System Interface (WASI).

9.3 WAVM guest calls

• Mechanism:
  • Libraries can call exports of the main module using the naming scheme "env" "wavm_guest_call__*".
• Usage example:
  • go-stub calls Go's resume function when queueing asynchronous events via wavm_guest_call_resume(), and retrieves the new stack pointer with wavm_guest_call_getsp().

9.4 Caller module internals call

• Purpose:
  • Each stack frame retains information about the caller module and its internals offset.
• Implementation:
  • WAVM appends four "internal" functions to each module that perform small memory load or store operations.
  • Libraries use opcodes such as wavm_caller_{load,store}{8,32} to access their caller's memory.
  • Only libraries can access their caller's memory; restrictions prevent the main module from doing so.

10. Stylus proving and fraud detection

Stylus introduces an execution path alongside the EVM, enabling smart Contract execution in WebAssembly (WASM). Given that Stylus program are fraud-proven directly rather than interpreted via Geth's EVM implementation––the proving mechanism required modifications to the standard Arbitrum proving architecture.

10.1 Proving Stylus programs

Unlike EVM-based contracts, Stylus programs are dynamically linked into the replay machine when proving fraud. This is achieved through two key opcodes:

• LinkModule: Loads the Stylus contract's WASM module into the replay machine.
• UnlinkModule: Removes the module once execution completes.

These opcodes ensure that Stylus contracts are treated as part as part of the replay machine, allowing for precise fraud-proof bisection at the WASM level.

10.2 Execution-proving separation

Stylus leverages Arbitrum's execution-proving separation, where the replay machine runs in WAVM, and disputes over Stylus transactions follow the standard interactive fraud-proof protocol (BoLD), which means:

1. A challenge initiates if a validator disputes the execution of a Stylus transaction.
2. The dispute narrows to a single WAVM opcode via the bisection protocol.
3. The One-Step Proof (OSP) mechanism extends to handle Stylus-specific operations, proving the correctness of WASM execution at the opcode level.

10.3 Internal function calls in proofs

Since Stylus programs interact with the blockchain through host I/O's, fraud proofs must ensure correct execution of cross-module calls. The following additional proving opcodes facilitate Stylus program execution:

• CrossModuleInternalCall: Allows internal functions within a Stylus module to be proven independently.
• CrossModuleForward: Ensures host I/O calls are accurately relayed through forward.wat, maintaining consistency in fraud proofs.

10.4 Error recovery and chain safety

Stylus introduces a novel Error Guard mechanism to prevent malicious programs from halting the chain. If an error occurs within a Stylus program during proving:

1. Execution reverts to the main replay machine context.
2. The replay machine resets the program's execution state using an Error Guard stack.
3. If recovery is not possible, the transaction is flagged as invalid, ensuring Stylus fraud proofs remain deterministic.

10.5 One-Step Proofs for Stylus

The One-Step Prover extends to validate Stylus-specific opcodes, which include:

• Memory operations (e.g., MemoryGrow, HeapAlloc)
• Host I/O's (e.g., storage_load_bytes32, return_data)
• Gas metering within WASM execution

By integrating these functionalities, Stylus ensures WASM contract execution can be fraud-proven like EVM transactions, while leveraging Arbitrum's existing BoLD fraud-proof architecture.