package tezos-protocol-013-PtJakart
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).
type input = {inbox_level : Alpha_context.Raw_level.t;message_counter : Tezos_protocol_environment_013_PtJakart.Z.t;payload : string;
}An input to a PVM is the message_counter element of an inbox at a given inbox_level and contains a given payload.
module type S = sig ... end