package tezos-protocol-alpha

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

This PVM is used for verification in the Protocol. produce_proof always returns None.

include Sc_rollup_PVM_sem.S with type context = Tezos_protocol_environment_alpha.Context.t with type state = Tezos_protocol_environment_alpha.Context.tree with type proof = Tezos_protocol_environment_alpha.Context.Proof.tree Tezos_protocol_environment_alpha.Context.Proof.t proof

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.

val proof_start_state : proof -> hash

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

val proof_stop_state : proof -> hash option

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

val proof_input_requested : proof -> Sc_rollup_PVM_sem.input_request

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.

val proof_input_given : proof -> Sc_rollup_PVM_sem.input option

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

val install_boot_sector : state -> string -> state Tezos_protocol_environment_alpha.Lwt.t

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 (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.

verify_proof p checks the proof p. 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.
val verify_origination_proof : proof -> string -> bool Tezos_protocol_environment_alpha.Lwt.t

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.

type output_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.

val output_of_output_proof : output_proof -> Sc_rollup_PVM_sem.output

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

val state_of_output_proof : output_proof -> hash

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

val verify_output_proof : output_proof -> bool Tezos_protocol_environment_alpha.Lwt.t

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.

module Internal_for_tests : sig ... end
val name : string

name is "wasm_2_0_0".

WebAssembly is an "evergreen" specification. We aim to track the latest major version, 2.0 at the time of writing. We use the minor version number to track changes to our fork.

val parse_boot_sector : string -> string option

parse_boot_sector s builds a boot sector from its human writable description.

val pp_boot_sector : Tezos_protocol_environment_alpha.Format.formatter -> string -> unit

pp_boot_sector fmt s prints a human readable representation of a boot sector.

get_tick state gets the total tick counter for the given PVM state.

type status =
  1. | Computing
  2. | WaitingForInputMessage

PVM status

get_status state gives you the current execution status for the PVM.