From 90df0a2dc8b0ae70e4f00d5a2eeb04c601effea4 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Thu, 12 May 2022 19:38:08 +0200 Subject: [PATCH] Proto,SCORU: Improve the docstring for PVM interface Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/sc_rollup_PVM_sem.ml | 94 ++++++++++++------- 1 file changed, 61 insertions(+), 33 deletions(-) diff --git a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml index 80ae218a8905..d4a855e4c7d4 100644 --- a/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml +++ b/src/proto_alpha/lib_protocol/sc_rollup_PVM_sem.ml @@ -35,15 +35,15 @@ 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. + 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). + processing of some messages led to a given new rollup state (given + an actual source of truth about the nature of these messages). *) open Alpha_context @@ -63,55 +63,83 @@ module type S = sig The state of the PVM denotes a state of the rollup. + We classify states into two categories: "internal states" do + not require any external information to be executed while + "input states" are waiting for some information from the + inbox to be executable. + *) type state - (** During interactive rejection games, a player may need to - provide a proof that a given execution step is valid. *) + (** A state is initialized in a given context. A [context] + represents the executable environment needed by the state to + exist. Typically, the rollup node storage can be part of this + context to allow the PVM state to be persistent. *) + type context + + (** A [hash] characterizes the contents of a state. *) + type hash = State_hash.t + + (** + + During interactive refutation games, a player may need to + provide a proof that a given execution step described as + a pair of a [hash] for the state before the execution step + and a [hash] for the state right after the execution step + is valid. + + The protocol only has to verify proofs. Hence, this signature + does not include a function to produce proofs. However, a + rollup node would necessarily offer a richer interface for its + own implementation of the PVM typically to be able to generate + such proofs when it participates in a refutation game. + + *) type proof + (** [proof]s are embedded in L1 refutation game operations using + [proof_encoding]. Given that the size of L1 operations are + limited, it is of *critical* importance to make sure that + no execution step of the PVM can generate proofs that do not + fit in L1 operations when encoded. If such a proof existed, + the rollup could get stuck. *) val proof_encoding : proof Data_encoding.t - (** A state is initialized in a given context. *) - type context - - (** A commitment hash characterized the contents of the state. *) - type hash = State_hash.t + (** [verify_proof input proof] returns [true] iff the [proof] is + valid. If the state related to the proof is an input state, + [input] is the inbox message provided to the evaluation + function. *) + val verify_proof : input:input option -> proof -> bool Lwt.t (** [proof_start_state proof] returns the initial state hash of the - [proof] execution step. *) + [proof] execution step. *) val proof_start_state : proof -> hash (** [proof_stop_state proof] returns the final state hash of the - [proof] execution step. *) + [proof] execution step. *) val proof_stop_state : proof -> hash (** [state_hash state] returns a compressed representation of [state]. *) val state_hash : state -> hash Lwt.t - (** [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 boot_sector] is the state of the PVM + before booting. *) val initial_state : context -> string -> state Lwt.t - (** [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] returns [Some (level, counter)] if + [state] is an input state waiting for the input message that + comes next to the message numbered [counter] in the inbox of a + given [level]. By convention, waiting for the very first message + is represented by [Some (0, -1)]. *) val is_input_state : state -> (Raw_level.t * Z.t) option Lwt.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] sets [input] in [state] as the next + input message to be processed. The input message must be the + message next to the previous message processed by the rollup + in the inbox. *) val set_input : input -> state -> state Lwt.t (** [eval s0] returns a state [s1] resulting from the - execution of an atomic step of the rollup at state [s0]. *) + execution of an atomic step of the rollup at state [s0]. *) val eval : state -> state Lwt.t - - (** [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. *) - val verify_proof : input:input option -> proof -> bool Lwt.t end -- GitLab