package tezos-protocol-014-PtKathma

  1. Overview
  2. Docs
package tezos-protocol-014-PtKathma
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module Context : P

Signature

include Sc_rollup_PVM_sem.S with type context = Context.Tree.t with type state = Context.tree
type state = Context.tree

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.

type context = Context.Tree.t

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.

type proof

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

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.

val name : string

name is "arith".

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_014_PtKathma.Format.formatter -> string -> unit

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

pp state returns a pretty-printer valid for state.

get_tick state returns the current tick of state.

type status =
  1. | Halted
  2. | WaitingForInputMessage
  3. | Parsing
  4. | Evaluating

The machine has three possible statuses:

get_status state returns the machine status in state.

type instruction =
  1. | IPush : int -> instruction
  2. | IAdd : instruction
  3. | IStore : string -> instruction

The machine has only three instructions.

val equal_instruction : instruction -> instruction -> bool

equal_instruction i1 i2 is true iff i1 equals i2.

pp_instruction fmt i shows a human readable representation of i.

val get_parsing_result : state -> bool option Tezos_protocol_environment_014_PtKathma.Lwt.t

get_parsing_result state is Some true if the current message is syntactically correct, Some false when it contains a syntax error, and None when the machine is not in parsing state.

get_code state returns the current code obtained by parsing the current input message.

get_stack state returns the current stack.

val get_var : state -> string -> int option Tezos_protocol_environment_014_PtKathma.Lwt.t

get_var state x returns the current value of variable x. Returns None if x does not exist.

val get_evaluation_result : state -> bool option Tezos_protocol_environment_014_PtKathma.Lwt.t

get_evaluation_result state returns Some true if the current message evaluation succeeds, Some false if it failed, and None if the evaluation has not been done yet.

val get_is_stuck : state -> string option Tezos_protocol_environment_014_PtKathma.Lwt.t

get_is_stuck state returns Some err if some internal error made the machine fail during the last evaluation step. None if no internal error occurred. When a machine is stuck, it reboots, waiting for the next message to process.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct