package tezos-protocol-015-PtLimaPt

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

This module introduces the semantics of Proof-generating Virtual Machines.

A PVM defines an operational semantics for some computational model. The specificity of PVMs, in comparison with standard virtual machines, is their ability to generate and to validate a *compact* proof that a given atomic execution step turned a given state into another one.

In the smart-contract rollups, PVMs are used for two purposes:

  • They allow for the externalization of rollup execution by completely specifying the operational semantics of a given rollup. This standardization of the semantics gives a unique and executable source of truth about the interpretation of smart-contract rollup inboxes, seen as a transformation of a rollup state.
  • They allow for the validation or refutation of a claim that the processing of some messages led to a given new rollup state (given an actual source of truth about the nature of these messages).

An input to a PVM is the message_counter element of an inbox at a given inbox_level and contains a given payload.

According the rollup management protocol, the payload must be obtained through Sc_rollup_inbox_message_repr.serialize which follows a documented format.

FIXME: https://gitlab.com/tezos/tezos/-/issues/3649

This type cannot be extended in a retro-compatible way. It should be put into a variant.

type inbox_message = {
  1. inbox_level : Raw_level_repr.t;
  2. message_counter : Tezos_protocol_environment_015_PtLimaPt.Z.t;
  3. payload : Sc_rollup_inbox_message_repr.serialized;
}
type reveal_data =
  1. | Raw_data of string
type input =
  1. | Inbox_message of inbox_message
  2. | Reveal of reveal_data

inbox_message_encoding encoding value for inbox_message.

val inbox_message_equal : inbox_message -> inbox_message -> bool

input_equal i1 i2 return whether i1 and i2 are equal.

val reveal_data_equal : reveal_data -> reveal_data -> bool
val input_equal : input -> input -> bool
type reveal =
  1. | Reveal_raw_data of Input_hash.t
type input_request =
  1. | No_input_required
  2. | Initial
  3. | First_after of Raw_level_repr.t * Tezos_protocol_environment_015_PtLimaPt.Z.t
  4. | Needs_reveal of reveal

The PVM's current input expectations:

  • No_input_required if the machine is busy and has no need for new input.
  • Initial if the machine has never received an input so expects the very first item in the inbox.
  • First_after (level, counter) expects whatever comes next after that position in the inbox.
  • Needs_reveal reveal if the machine reveals the existence of some data and needs this data to continue its execution.

input_request_encoding encoding value for input_request.

pp_input_request fmt i pretty prints the given input i to the formatter fmt.

val reveal_equal : reveal -> reveal -> bool
val input_request_equal : input_request -> input_request -> bool

input_request_equal i1 i2 return whether i1 and i2 are equal.

type output = {
  1. outbox_level : Raw_level_repr.t;
    (*

    The outbox level containing the message. The level corresponds to the inbox level for which the message was produced.

    *)
  2. message_index : Tezos_protocol_environment_015_PtLimaPt.Z.t;
    (*

    The message index.

    *)
  3. message : Sc_rollup_outbox_message_repr.t;
    (*

    The message itself.

    *)
}

Type that describes output values.

output_encoding encoding value for output.

pp_output fmt o pretty prints the given output o to the formatter fmt.

module type S = sig ... end
OCaml

Innovation. Community. Security.