Module Mavryk_raw_protocol_alpha.Sc_rollup_PVM_sig

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:

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.

type inbox_message = {
  1. inbox_level : Raw_level_repr.t;
  2. message_counter : Mavryk_protocol_environment_alpha.Z.t;
  3. payload : Sc_rollup_inbox_message_repr.serialized;
}
type reveal_data =
  1. | Raw_data of string
  2. | Metadata of Sc_rollup_metadata_repr.t
  3. | Dal_page of Dal_slot_repr.Page.content option
  4. | Dal_parameters of Sc_rollup_dal_parameters_repr.t
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 Sc_rollup_reveal_hash.t
  2. | Reveal_metadata
  3. | Request_dal_page of Dal_slot_repr.Page.t
  4. | Reveal_dal_parameters
    (*

    Request DAL parameters that were used for the slots published at the current inbox level.

    *)
type is_reveal_enabled = current_block_level:Raw_level_repr.t -> reveal -> bool

is_reveal_enabled is the type of a predicate that tells if a kind of reveal is activated at a certain block level.

type input_request =
  1. | No_input_required
  2. | Initial
  3. | First_after of Raw_level_repr.t * Mavryk_protocol_environment_alpha.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_metadata if the machine needs the metadata 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 : Mavryk_protocol_environment_alpha.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
module type Generic_pvm_context_sig = sig ... end