Module Sc_rollup_arith.Make

Parameters

Signature

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

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.

type context = Context.Tree.t

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

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 ~empty is the initial state of the PVM, before its specialization with a given boot_sector. The initial state is built on the empty state which must be provided.

val install_boot_sector : state -> string -> state Mavryk_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 ~is_reveal_enabled 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 ~is_reveal_enabled 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 ~is_reveal_enabled 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_sig.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 the output_proof's output iff the 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 check_dissection : default_number_of_sections:int -> start_chunk:Sc_rollup_dissection_chunk_repr.t -> stop_chunk:Sc_rollup_dissection_chunk_repr.t -> Sc_rollup_dissection_chunk_repr.t list -> unit Mavryk_protocol_environment_alpha.Error_monad.tzresult

check_dissection ~default_number_of_sections ~start_chunk ~stop_chunk chunks fails if the dissection encoded by the list [start_chunk] @ chunks @ [stop_chunk] does not satisfy the properties expected by the PVM.

get_current_level state returns the current level of the state, returns None if it is not possible to compute the level.

module Internal_for_tests : sig ... end
val parse_boot_sector : string -> string option

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

val pp_boot_sector : Mavryk_protocol_environment_alpha.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. | Waiting_for_input_message
  3. | Waiting_for_reveal of Sc_rollup_PVM_sig.reveal
  4. | Parsing
  5. | Evaluating

The machine has five possible statuses:

get_status ~is_reveal_enabled state returns the machine status in state.

get_outbox outbox_level state returns the outbox in state for a given outbox_level.

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