Challenges: Interactive Fraud Proofs

This document attempts to give an account of BoLD, Arbitrum's new all-vs-all challenge protocol, in terms that might be familiar to people used to studying Arbitrum's previous, 1-vs-1 challenge protocol. For another explanation of BoLD's concepts, refer to Gentle Introduction, Technical deep dive, or the BoLD Research whitepaper.

Suppose the Rollup chain looks like this:

Assertions 93 and 95 are siblings (they both have 92 as predecessor). Alice is bonded on 93 and Bob is bonded on 95.

At this point we know that Alice and Bob disagree about the correctness of assertion 93, with Alice committed to 93 being correct and Bob committed to 93 being incorrect. (Bob is bonded on 95, and 95 implicitly claims that 92 is the last correct assertion before it, which implies that 93 must be incorrect.)

Whenever two (or more) proposers are bonded on sibling assertions, a challenge begins between all of them. (There can only be one bonder per assertion, but multiple assertions may participate in a challenge.) The Rollup protocol will record and referee the challenge, eventually declaring a winner and confiscating the losers' bonds. This will cause the losers to be removed as proposers.

The challenge is a game in which two or more parties make moves in an attempt to defend the correctness of assertions they (or their allies) have staked on, with an Ethereum contract as the referee. The goal of the system is to determine which assertion corresponds to the correct execution.

The game will operate in two phases: Bisection, followed by one-step proof. Bisection will narrow down the size of the dispute until it is a dispute about just one instruction of execution. Then the one-step proof will determine who is right about that one instruction.

We’ll describe the bisection part of the protocol twice. First, we’ll give a simplified version which is easier to understand. Then we’ll describe some ways in which the real version differs from the simplified one. For an even more thorough explanation, please see the BoLD research whitepaper.

Bisection Protocol: Simplified Version

Alice (or one of her allies - for the sake of brevity we'll refer to this party as Alice) is defending the claim that starting with the state in the predecessor assertion, the state of the Virtual Machine can advance to the state specified in assertion A. Once a challenge starts, Alice has to provide a commitment to the entire history of the computation: that is, to the state after each step of execution.

Alice’s first move requires her to bisect her claims about intermediate states between the beginning (0 instructions executed) and the end (N instructions executed). So we require Alice to divide her claim in half, and post the state at the half-way point, after N/2 instructions have been executed.

Now Alice has effectively bisected her N-step Assertion into two (N/2)-step assertions. Bob (or one of his allies; for brevity, Bob) needs to do the same for his assertion, also deriving two new (N/2)-step assertions. At most one of these will be a "rival" of one of Alice's assertions. Two assertions are "rivals" if they agree on a prefix of the state history to which they commit but disagree on the rest; this is very similar to the concept of "siblings" for assertions. Whichever of the two of Alice's assertions now has a rival, Alice will proceed to defend it.

At this point we’re effectively back in the original situation: Alice having made an assertion that Bob disagrees with. But we have cut the size of the assertion in half, from N to N/2. We can apply the same method again, with Alice bisecting and Bob choosing one of the halves, to reduce the size to N/4. And we can continue bisecting, so that after a logarithmic number of rounds Alice and Bob will be disagreeing about a single step of execution. That’s where the bisection phase of the protocol ends, and Alice must make a one-step proof which will be checked by the EthBridge.

Why Bisection Correctly Identifies a Cheater

Before talking about the complexities of the real Challenge protocol, let’s stop to understand why the simplified version of the protocol is correct. Here correctness means two things: (1) if Alice’s initial claim is correct, Alice (or her ally) can always win the challenge, and (2) if Alice’s initial claim is incorrect, and there is at least one honest validator participating in the protocol, Alice and her allies never win the challenge.

To prove (1), observe that if Alice’s initial claim is correct, she can offer a truthful midpoint claim, and both of the implied half-size claims will be correct. So whichever half Bob objects to, Alice will again be in the position of defending a correct claim. At each stage of the protocol, Alice will be defending a correct claim. At the end, Alice will have a correct one-step claim to prove, so that claim will be provable and Alice can win the challenge.

To prove (2), observe that if Alice’s initial claim is incorrect, this can only be because her claimed endpoint after N steps is incorrect. Now when Alice offers her midpoint state claim, that midpoint claim is either correct or incorrect. If it’s incorrect, then Bob can force Alice to defend her first-half claim, which will be incorrect. If Alice’s midpoint state claim is correct, then her second-half claim must be incorrect, and Bob can force her to defend that. So whatever Alice does, Bob will be able to challenge an incorrect half-size claim. At each stage of the protocol, Bob can identify an incorrect claim to challenge. At the end, Alice will have an incorrect one-step claim to prove, which she will be unable to do, so Bob can win the challenge.

note

If you’re a stickler for mathematical precision, we invite you to read the BoLD research whitepaper. Formalizing these and other arguments pertaining to BoLD is quite tricky and subtle!

The real bisection protocol

The real bisection protocol is conceptually similar to the simplified one described above, but with several changes that improve efficiency or deal with necessary corner cases. Here is a list of the differences.

**Bisection over L2 blocks, then over "big steps" of many instructions, then over single instructions: **Alice's assertion is over an assertion, which asserts the result of creating some number of Layer 2 Nitro blocks. Bisection first occurs over these Layer 2 blocks, to narrow the dispute down to a dispute about a single Layer 2 Nitro block. Next, the dispute transforms into a dispute about executing a "big step" of 2^26 instructions (this intermediate level is needed to reduce the workload on the validator). At this point, the dispute transforms into a dispute about a single execution of the State Transition Function or in other words about the execution of a sequence of WAVM instructions. The protocol then executes the recursive bisection sub-protocol again, this time over WAVM instructions, to narrow the dispute to a single instruction. For details about how these "subchallenges" work, see BoLD: Technical deep dive Time Limits: The protocol can be seen as tracking a timer for each assertion, counting (essentially) how much time has passed while that assertion could be seen as the presumptive winner of the game (that is, the amount of time during which the onus is on parties opposing the assertion to act.) Think of the time allowance as being about a week. Once an assertion's timer reaches this time allowance, it can be confirmed. The time allowance is designed to give the honest parties in the protocol enough time to act, including the time needed to calculate, submit, and process moves, as well as to account for possible censorship on L1.

It should be clear that these changes don’t affect the basic correctness of the challenge protocol. They do, however, improve its efficiency and enable it to handle all of the cases that can come up in practice.

Efficiency

The challenge protocol is designed to resolve the dispute with a minimum of work required by the protocol (via its parent chain contracts) in its role as referee. The protocol needs to track information for the assertions created by parties in the challenge, including their history commitments and timers that can be used to calculate how long they have gone without a rival. The protocol doesn’t need to pay attention to whether those claims are correct in any way; it only needs to know whether Alice’s move “has the right shape”. For more information on what the protocol needs to keep track of, see BoLD: Technical deep dive

The only point where the protocol needs to evaluate a move “on the merits” is at the one-step proof, where it needs to look at Alice’s proof and determine whether the proof that was provided does indeed establish that the virtual machine moves from the before state to the claimed after state after one step of computation.

ChallengeManager

This section is a technical deep dive into the ChallengeManager and will walk through the arbitration of a challenge game in great detail. The ChallengeManager plays the role of the arbiter of challenge games. Here's a diagram of the challenge state machine:

Block challenge

The challenge begins by bisecting over global states (including block hashes). Before actual machine execution is disputed, the dispute is narrowed down to an individual block. Once the challenge has been bisected down to an individual block, challengeExecution can be called by the current responder. This operates similarly to a bisection in that the responder must provide a competing global state and machine state, but it uses that information to transition to the execution challenge phase.

"Big-Step" execution challenge

Once narrowed down to an individual block, the actual machine execution can be bisected. We begin by bisecting the machine execution until we reach a "chunk" of 2^26 WASM instructions. Once the disagreement has reached this granularity, we can proceed with a "small-step" execution challenge (see below). For more detail on why we use two levels of execution challenges ("big step" and "small-step"), see "Challenge Resolution" in the BoLD technical deep dive.

"Small-Step" Execution challenge

After reaching a "chunk" of 2^26 instructions, we begin a new challenge level, bisecting this chunk until we reach a dispute over a single instruction. Once the execution has been bisected down to an individual step, oneStepProveExecution can be called by any player to resolve the one-step dispute. That player must provide proof data to execute a step of the machine. This proof is checked on L1. If it is correct, the one-step edge to which the one-step proof is applied and considered confirmed.

Winning the challenge

Note that for the time being, winning the challenge isn't instant.

This is done as a precaution, so that if a challenge is resolved incorrectly, there is time to diagnose and fix the error with a contract upgrade.

One Step Proof Assumptions

The One Step Proof (OSP) implementation makes certain assumptions about the cases that can arise in a correct execution. This documents those assumptions about what's being executed.

If a case is "unreachable", that is, the case is assumed to never arise in correct execution, then the OSP can implement any instruction semantics in that case.

• In a challenge between malicious assertions, that start from an unreachable machine state, any case can arise. The challenge protocol must do something safe in every case. But the instruction semantics can be weird in such cases because no honest party ever needs to try to refute an assertion that starts from an unreachable state. All assertions engaging in a dispute starting from an unreachable state must be malicious, and the protocol doesn't need to care which one wins. In particular, it is OK for the onchain one-step proof contract to differ in its behavior from the node software's execution engine in this case (and only in this case).
• In a challenge with one honest party, the honest party will never need to one-step prove an unreachable case. The honest party will only assert correct executions, so it will only have to prove reachable cases.
• In a challenge with an honest party, a dishonest party could assert an execution that transitions into an unreachable case, but such an execution must include an invalid execution of a reachable case earlier in the assertion. Because a challenge involving an honest party will eventually require an OSP over the first instruction where the parties disagree, the eventual OSP will be over the earlier point of divergence, and not over the later execution from an unreachable case.

In general, some unreachable cases will be detectable by the OSP checker and some will not. For safety, the detectable unreachable cases should be defined by transition the machine into an error state, allowing governance to eventually push an upgrade to recover from the error. An undetectable unreachable case, if such a case were reached in correct execution, could lead to a security failure.

The following assumptions, together, must prevent an unreachable case from arising in correct execution.

The WAVM code is generated by Arbitrator from valid WASM

WAVM is the name of the custom instruction set similar to WASM used for proving. Arbitrator transpiles WASM code into WAVM. It also invokes wasm-validate from wabt (the WebAssembly Binary Toolkit) to ensure the input WASM is valid. WAVM produced otherwise may not be executable, as it may try to close a non-existent block, mismatch types, or do any other number of invalid things which are prevented by WASM validation.

WAVM code generated from by Arbitrator from valid WASM is assumed to never encounter an unreachable case.

Inbox messages must not be too large

The current method of inbox hashing requires the full inbox message be available for proving. That message must not be too large as to prevent it from being supplied for proving, which is enforced by the inboxes.

The current length limit is 117,964 bytes, which is 90% of the max transaction size Geth will accept, leaving 13,108 bytes for other proving data.

Requested preimages must be known and not too large

WAVM has an opcode which resolves the preimage of a Keccak-256 hash. This can only be executed if the preimage is already known to all nodes, and can only be proven if the preimage isn't too long. Violations of this assumption are undetectable by the OSP checker.

The current length limit is 117,964 bytes for the reasons mentioned above. Here's a list of which preimages may be requested by Nitro, and why they're known to all parties, and not too large:

Block headers

Nitro may request up to the last 256 L2 Block headers. The last block header is required to determine the current state, and blocks before it are required to implement the BLOCKHASH EVM instruction.

This is safe as previous block headers are a fixed size, and are known to all nodes.

State trie access

To resolve state, Nitro traverses the state trie by resolving preimages.

This is safe as validators retain archive state of unconfirmed blocks, each trie branch is of a fixed size, and the only variable sized entry in the trie is contract code, which is limited by EIP-170 to about 24KB.

WASM to WAVM

Not all WASM instructions are 1:1 with WAVM opcodes. This document lists those which are not, and explains how they're expressed in WAVM. Many of the WAVM representations use opcodes not in WASM, which are documented in wavm-custom-opcodes.

block and loop

In WASM, a block contains instructions. Branch instructions exit a fixed number of blocks, jumping to their destination. A normal block's destination is the end of the block, whereas a loop's destination is the start of the loop.

In WAVM, instructions are flat. At transpilation time, any branch instructions are replaced with jumps to the corresponding block's destination. This means that WAVM interpreters don't need to track blocks, and thus block instructions are unnecessary.

if and else

These are translated to a block with an ArbitraryJumpIf as follows:

begin block with endpoint end
  conditional jump to else
  [instructions inside if statement]
  branch
  else: [instructions inside else statement]
end

br and br_if

br and br_if are translated into ArbitraryJump and ArbitraryJumpIf respectively. The jump locations can be known at transpilation time, making blocks obsolete.

br_table

br_table is translated to a check for each possible branch in the table, and then if none of the checks hit, a branch of the default level.

Each of the non-default branches has a conditional jump to a section afterwards, containing a drop for the selector, and then a jump to the target branch.

local.tee

local.tee is translated to a WAVM Dup and then a LocalSet.

return

To translate a return, the number of return values must be known from the function signature. A WAVM MoveFromStackToInternal is added for each return value. Then, a loop checks IsStackBoundary (which implicitly pops a value) until it's true and the stack boundary has been popped. Next, a MoveFromInternalToStack is added for each return value to put the return values back on the stack. Finally, a WAVM Return is added, returning control flow to the caller.

Floating point instructions

A floating point library module must be present to translate floating point instructions. They are translated by bitcasting f32 and f64 arguments to i32s and i64s, then a cross module call to the floating point library, and finally bitcasts of any return values from i32s and i64s to f32s and f64s.

WAVM custom opcodes not in WASM

In addition to the MVP WASM specification, WAVM implements the multi value and sign extension ops WASM proposals.

WAVM also implements the following unique opcodes, which are not part of WASM nor any WASM proposal.

Invariants

Many of these opcodes have implicit invariants about what's on the stack, e.g., "Pops an i32 from the stack" assumes that the top of the stack has an i32. If these conditions are not satisfied, execution is generally not possible. These invariants are maintained by WASM validation and Arbitrator codegen. (See One Step Proof Assumptions.)

Codegen internal

These are generated when breaking down a WASM instruction that does many things into many WAVM instructions which each do one thing. For instance, a WASM local.tee is implemented in WAVM with dup and then local.set, the former of which doesn't exist in WASM.

Other times, these opcodes help out an existing WASM opcode by splitting out functionality. For instance, the WAVM return opcode by itself does not clean up the stack, but its WASM->WAVM codegen includes a loop that utilizes IsStackBoundary to perform the stack cleanup specified for WASM's return.

Opcode	Name	Description
0x8000	EndBlock	Pops an item from the block stack.
0x8001	EndBlockIf	Peeks the top value on the stack, assumed an i32. If non-zero, pops an item from the block stack.
0x8002	InitFrame	Pops a caller module index i32, then a caller module internals offset i32, and finally a return InternalRef from the stack. Creates a stack frame with the popped info and the locals merkle root in proving argument data.
0x8003	ArbitraryJumpIf	Pops an i32 from the stack. If non-zero, jumps to the program counter in the argument data.
0x8004	PushStackBoundary	Pushes a stack boundary to the stack.
0x8005	MoveFromStackToInternal	Pops an item from the stack and pushes it to the internal stack.
0x8006	MoveFromInternalToStack	Pops an item from the internal stack and pushes it to the stack.
0x8007	IsStackBoundary	Pops an item from the stack. If a stack boundary, pushes an i32 with value 1. Otherwise, pushes an i32 with value 0.
0x8008	Dup	Peeks an item from the stack and pushes another copy of that item to the stack.

The above opcodes eliminate the need for the following WASM opcodes (which are transpiled into other WAVM opcodes):

• loop
• if/else
• br_table
• local.tee

Linking

This is only generated to link modules together. Each import is replaced with a local function consisting primarily of this opcode, which handles the actual work needed to change modules.

Opcode	Name	Description
0x8009	CrossModuleCall	Pushes the current program counter, module number, and module's internals offset to the stack. Then splits its argument data into the lower 32 bits being a function index, and the upper 32 bits being a module index, and jumps to the beginning of that function.

Host calls

These are only used in the implementation of "host calls". Each of these has an equivalent host call method, which can be invoked from libraries. The exception is CallerModuleInternalCall, which is used for the implementation of all of the wavm_caller_* host calls. Those calls are documented in wavm-modules.mdx.

For these instruction descriptions, all pointers and offsets are represented as WASM i32s.

Opcode	Name	Description
0x800A	CallerModuleInternalCall	Pushes the current program counter, module number, and module's internals offset (all i32s) to the stack. Then, it retrieves the caller module internals offset from the current stack frame. If 0, errors, otherwise, jumps to the caller module at function (internals offset + opcode argument data) and instruction 0.
0x8010	GetGlobalStateBytes32	Pops a pointer and then an index from the stack. If the index is greater than or equal to the number of global state bytes32s, errors. If the pointer mod 32 is not zero, errors. If the pointer + 32 is outside the programs memory, errors. Otherwise, writes the global state bytes32 value of the specified index to the specified pointer in memory.
0x8011	SetGlobalStateBytes32	Pops a pointer and then an index from the stack. If the index is greater than or equal to the number of global state bytes32s, errors. If the pointer mod 32 is not zero, errors. If the pointer + 32 is outside the programs memory, errors. Otherwise, reads a bytes32 from the specified pointer in memory and sets the global state bytes32 value of the specified index to it.
0x8012	GetGlobalStateU64	Pops a pointer and then an index from the stack. If the index is greater than or equal to the number of global state u64s, errors. If the pointer mod 32 is not zero, errors. If the pointer + 8 is outside the programs memory, errors. Otherwise, writes the global state u32 value of the specified index to the specified pointer in memory.
0x8013	SetGlobalStateU64	Pops a pointer and then an index from the stack. If the index is greater than or equal to the number of global state u64s, errors. If the pointer mod 32 is not zero, errors. If the pointer + 8 is outside the programs memory, errors. Otherwise, reads a u64 from the specified pointer in memory and sets the global state u64 value of the specified index to it.
0x8020	ReadPreImage	Pops an offset and then a pointer from the stack. If the pointer mod 32 is not zero, errors. If the pointer + 32 is outside the programs memory, errors. Reads a 32 byte Keccak-256 hash from the specified pointer in memory. Writes up to 32 bytes of the preimage to that hash, beginning with the offset byte of the preimage. If offset is greater than or equal to the number of bytes in the preimage, writes nothing. Pushes the number of bytes written to the stack as an i32.
0x8021	ReadInboxMessage	Pops an offset, then a pointer, and then an i64 message number from the stack. If the pointer mod 32 is not zero, errors. If the pointer + 32 is outside the programs memory, errors. Attempts to read an inbox message from the inbox identifier contained in the argument data (0 for the Sequencer inbox, 1 for the Delayed Inbox) at the specified message number. If this exceeds the machine's inbox limit, enters the "too far" state. Otherwise, writes up to 32 bytes of the specified inbox message, beginning with the offset byte of the message. If offset is greater than or equal to the number of bytes in the preimage, writes nothing. Pushes the number of bytes written to the stack as an i32.
0x8022	HaltAndSetFinished	Sets the machine status to finished, halting execution and marking it as a success.

WAVM Floating point implementation

Implementing correct, consistent, and deterministic floating point operations directly in WAVM (meaning both a Rust Arbitrator implementation and Solidity OSP implementation) would be an extremely tricky endeavor. WASM specifies floating point operations as being compliant to IEEE 754-2019, which is not deterministic, and full of edge cases.

Instead, floating point operations (apart from trivial bit-casts like i32 <-> f32) are implemented using the C Berkeley SoftFloat-3e library running inside WAVM. Arbitrator links other WAVM guests against this, by replacing float point operations with cross module calls to the library.

Berkeley SoftFloat does not implement all necessary floating point operations, however. Most importantly, it does not provide a min function, despite IEEE 754-2019 specifying one. The implementation of these operations, along with the export of convenient APIs for WASM opcode implementations, are contained in bindings32.c for 32 bit integers and bindings64.c for 64 bit integers.

This ensures that floating point operations are deterministic and consistent between Arbitrator and the OSP, as they are implemented exclusively using operations already known to be deterministic and consistent. However, it does not ensure that the floating point operations are perfectly compliant to the WASM specification. Go uses floating points in its JS<->Go WASM interface, and floating points may be used outside core state transition code for imprecise computations, but the former is well exercised as used in Nitro, and the latter generally doesn't rely on details like the minimum of NaN and infinity.

Known divergences from the WASM specification

Floating point to integer truncation will saturate on overflow, instead of erroring. This is generally safer, because on x86, overflowing simply produces an undefined result. A WASM proposal exists to add new opcodes which are defined to saturate, but it's not widely adopted.

WAVM Modules

WASM natively has a notion of modules. Normally, in WASM, a module is the entire program. A .wasm file represents one module, and generally they aren't combined. An exception to this is C compiled via Clang, where wasm files are also used as object files, but its linking scheme is not supported in other languages.

In WAVM this is extended to make the executing program composed of multiple modules. These may call each other, and library modules may write to their caller's memory to return results.

The entrypoint module

The entrypoint module is where execution begins. It calls modules' start functions if specified, and then calls the main module's main function, which is language specific. For Go it sets argv to ["js"] to match the JS environment, and calls run. For Rust it calls main with no arguments.

Library exports

Libraries may export functions with the name pattern module__name, which future libraries or the main module can import as "module" "name".

For instance, this is used for wasi-stub to provide functions Rust imports according to the WebAssembly System Interface.

Floating point operations

To provide floating point operations for future libraries, the soft float library exports functions which perform floating point ops. These have the same name as the WASM instruction names, except . is replaced with _. Their type signature is also the same, except all f32s and f64s are bitcasted to i32s and i64s.

Future modules can implicitly use these by using WASM floating point operations, which are replaced at the WASM->WAVM level with bitcasts and cross module calls to these functions.

WAVM guest calls

Libraries may call the main module's exports via "env" "wavm_guest_call__*".

For instance, go-stub calls Go's resume function when queueing async events via wavm_guest_call_resume(), and then retrieves the new stack pointer with wavm_guest_call_getsp().

Caller module internals call

Every stack frame retains its caller module and its caller module's "internals offset", which is the first internal function index. WAVM appends 4 "internal" functions to each module, which perform a memory load or store of 1 or 4 bytes.

Via wavm_caller_{load,store}{8,32}, a library may access its caller's memory, which is implemented by calling these internal functions of the caller's module. Only libraries can access their caller's memory; the main module cannot.

For instance, this is used to read arguments from and write return values to the Go stack, when Go calls into go-stub.