package tezos-protocol-013-PtJakart

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
include Sc_rollup_PVM_sem.S with type context = Tezos_protocol_environment_013_PtJakart.Context.t
type state

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

type proof

During interactive rejection games, a player may need to provide a proof that a given execution step is valid.

A state is initialized in a given context.

A commitment hash characterized the contents of the state.

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 context is the state of the PVM before booting. It must be such that state_hash state = Commitment_hash.zero. Any context should be enough to create an initial state.

is_input_state state returns Some (level, counter) if state is waiting for the input message that comes next to the message numbered counter in the inbox of a given level.

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 input proof returns true iff the proof is valid. If the state is an input state, input is the hash of the input message externally provided to the evaluation function.

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_013_PtJakart.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 states:

get_status state returns the machine status in state.

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

The machine has only two 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_013_PtJakart.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_evaluation_result : state -> bool option Tezos_protocol_environment_013_PtJakart.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_013_PtJakart.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.