package tezos-protocol-015-PtLimaPt

  1. Overview
  2. Docs
package tezos-protocol-015-PtLimaPt
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.

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