The state of the PVM denotes a state of the rollup.

We classify states into two categories: "internal states" do not require any external information to be executed while "input states" are waiting for some information from the inbox to be executable.

A state is initialized in a given context. A context represents the executable environment needed by the state to exist. Typically, the rollup node storage can be part of this context to allow the PVM state to be persistent.

A hash characterizes the contents of a state.

During interactive refutation games, a player may need to provide a proof that a given execution step is valid. The PVM implementation is responsible for ensuring that this proof type has the correct semantics:

A proof p has four parameters:

start_hash := proof_start_state p stop_hash := proof_stop_state p input_requested := proof_input_requested p input_given := proof_input_given p

The following predicate must hold of a valid proof:

exists start_state, stop_state. (state_hash start_state == start_hash) AND (Option.map state_hash stop_state == stop_hash) AND (is_input_state start_state == input_requested) AND (match (input_given, input_requested) with | (None, No_input_required) -> eval start_state == stop_state | (None, Initial) -> stop_state == None | (None, First_after (l, n)) -> stop_state == None | (Some input, No_input_required) -> true | (Some input, Initial) -> set_input input_given start_state == stop_state | (Some input, First_after (l, n)) -> set_input input_given start_state == stop_state)

In natural language---the two hash parameters start_hash and stop_hash must have actual state values (or possibly None in the case of stop_hash) of which they are the hashes. The input_requested parameter must be the correct request from the start_hash, given according to is_input_state. Finally there are four possibilities of input_requested and input_given.

• if no input is required, or given, the proof is a simple eval step ;
• if input was required but not given, the stop_hash must be None (the machine is blocked) ;
• if no input was required but some was given, this makes no sense and it doesn't matter if the proof is valid or invalid (this case will be ruled out by the inbox proof anyway) ;
• finally, if input was required and given, the proof is a set_input step.

proofs are embedded in L1 refutation game operations using proof_encoding. Given that the size of L1 operations are limited, it is of *critical* importance to make sure that no execution step of the PVM can generate proofs that do not fit in L1 operations when encoded. If such a proof existed, the rollup could get stuck.

proof_start_state proof returns the initial state hash of the proof execution step.

proof_stop_state proof returns the final state hash of the proof execution step.

proof_input_requested proof returns the input_request status of the start state of the proof, as given by is_input_state. This must match with the inbox proof to complete a valid refutation game proof.

proof_input_given proof returns the input, if any, provided to the start state of the proof using the set_input function. If None, the proof is an eval step instead, or the machine is blocked because the inbox is fully read. This must match with the inbox proof to complete a valid refutation game proof.

state_hash state returns a compressed representation of state.

initial_state context boot_sector is the initial state of the PVM, which is a pure function of boot_sector.

The context argument is required for technical reasons and does not impact the result.

is_input_state state returns the input expectations of the state---does it need input, and if so, how far through the inbox has it read so far?

set_input (level, n, msg) state sets msg in state as the next message to be processed. This input message is assumed to be the number n in the inbox messages at the given level. The input message must be the message next to the previous message processed by the rollup.

eval s0 returns a state s1 resulting from the execution of an atomic step of the rollup at state s0.

This checks the proof. See the doc-string for the proof type.

produce_proof ctxt input_given state should return a proof for the PVM step starting from state, if possible. This may fail for a few reasons:

• the input_given doesn't match the expectations of state ;
• the context for this instance of the PVM doesn't have access to enough of the state to build the proof.

The following type is inhabited by the proofs that a given output is part of the outbox of a given state.

output_proof_encoding encoding value for output_proofs.

output_of_output_proof proof returns the output that is referred to in proof's statement.

state_of_output_proof proof returns the state hash that is referred to in proof's statement.

verify_output_proof output_proof returns true iff proof is a valid witness that its output is part of its state's outbox.

produce_output_proof ctxt state output returns a proof that witnesses the fact that output is part of state's outbox.