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

The life cycle of the PVM is as follows. It starts its execution from an initial_state. The initial state is specialized at origination with a boot_sector, using the install_boot_sector function. The resulting state is call the “genesis” of the rollup.

Afterwards, 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.

state_hash state returns a compressed representation of state.

initial_state context is the initial state of the PVM, before its specialization with a given boot_sector.

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

install_boot_sector state boot_sector specializes the initial state of a PVM using a dedicated boot_sector, submitted at the origination of the rollup.

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 input state sets input in state as the next input to be processed. This must answer the input_request from is_input_state state.

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

verify_proof input p checks the proof p with input input and returns the input_request before the evaluation of the proof. See the doc-string for the proof type.

verify_proof input p fails when the proof is invalid in regards to the given input.

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.

verify_origination_proof proof boot_sector verifies a proof supposedly generated by produce_origination_proof.

produce_origination_proof context boot_sector produces a proof p covering the specialization of a PVM, from the initial_state up to the genesis state wherein the boot_sector has been installed.

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.