Module Tezos_raw_protocol_013_PtJakart.Sc_rollup_PVM_semSource

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).