Skip to main content

🦏 Sc_rollup_PVM_sem.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Alpha_context.

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].
Module input.
  Record record : Set := Build {
    inbox_level : Alpha_context.Raw_level.t;
    message_counter : Z.t;
    payload : string;
  }.
  Definition with_inbox_level inbox_level (r : record) :=
    Build inbox_level r.(message_counter) r.(payload).
  Definition with_message_counter message_counter (r : record) :=
    Build r.(inbox_level) message_counter r.(payload).
  Definition with_payload payload (r : record) :=
    Build r.(inbox_level) r.(message_counter) payload.
End input.
Definition input := input.record.

Module S.
  Record signature {state proof context : Set} : Set := {
    
The state of the PVM denotes a state of the rollup.
    state := state;
    
During interactive rejection games, a player may need to provide a proof that a given execution step is valid.
    proof := proof;
    proof_encoding : Data_encoding.t proof;
    
A state is initialized in a given context.
    context := context;
    
A commitment hash characterized the contents of the state.
[proof_start_state proof] returns the initial state hash of the [proof] execution step.
    proof_start_state : proof hash;
    
[proof_stop_state proof] returns the final state hash of the [proof] execution step.
    proof_stop_state : proof hash;
    
[state_hash state] returns a compressed representation of [state].
    state_hash : state hash;
    
[initial_state context] is the state of the PVM before booting. It must be such that [state_hash state = Commitment_hash.zero]. Any [context] should be enough to create an initial state.
    initial_state : context string state;
    
[is_input_state state] returns [Some (level, counter)] if [state] is waiting for the input message that comes next to the message numbered [counter] in the inbox of a given [level].
    is_input_state : state option (Alpha_context.Raw_level.t × Z.t);
    
[set_input level n msg state] sets [msg] in [state] as the next message to be processed. This input message is assumed to be the number [n] in the inbox messages at the given [level]. The input message must be the message next to the previous message processed by the rollup.
    set_input : input state state;
    
[eval s0] returns a state [s1] resulting from the execution of an atomic step of the rollup at state [s0].
    eval : state state;
    
[verify_proof input proof] returns [true] iff the [proof] is valid. If the state is an input state, [input] is the hash of the input message externally provided to the evaluation function.
    verify_proof : option input proof bool;
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _ _}.