Merkelizing inbox for smart-contract rollups.
Overview
The inbox of a smart-contract rollup denotes the incoming messages of the rollup. This inbox is the source of truth about what operations are being published and have an effect on the rollup state. As such, the inbox completely determines the state of the rollup. Hence, if two claims disagree about the state of the rollup, there are only two possibilities: either these two claims correspond to two distinct interpretations of the same inbox ; or, these two claims differ on their views about the contents of the inbox itself. Sc_rollup_PVM_sem is meant to arbitrate the first kind of conflicts while Sc_rollup_inbox focuses on the second kind of conflicts.
Inbox messages
A message is a chunk of bytes. Messages are indexed using natural numbers and the level they are introduced.
A message is said to be *consumed* when its processing has been cemented, that is, when no refutation about its insertion can happen anymore because the commitment that describes the effect of this message on the state is cemented. A message is said to be *available* (for dispute) if it is not consumed.
A message processed by the rollup can be consumed or available. A message unprocessed by the rollup is always available.
The number of available messages is bounded by Constants_storage.sc_rollup_max_available_messages. When an inbox reaches the maximum number of available messages, the inbox is said to be full and cannot accept more messages. This limitation is meant to ensure that Merkle proofs about the inbox contents have a bounded size. (See next section.)
Merkelization of the inbox
As for the state of the Sc_rollup_PVM_sem, the layer 1 does not have to store the entire inbox but only a compressed form (typically a low number of hashes) that witnesses its contents, so that the protocol can check the validity of a proof about its contents. This saves space in the context of the layer 1 and is sufficient for the layer 1 to provide a source of truth about the contents of the inbox at the current level.
A level-indexed chain of inboxes
By design, inboxes are logically indexed by Tezos levels. This is required to have a simple way to decide if two commitments are in conflict. (See Sc_rollup_storage.)
A commitment included in the block at level L describes the effect of the messages of the inboxes with a level between a starting level L_0 and a stopping level L_1, both strictly inferior to L. The level L_0 must be the inbox level of its parent commitment.
To be valid, a commitment needs to prove that it is reading messages from an inbox which is consistent with the inbox at level L stored in the layer 1 context. So, it should be possible at any time to build a proof that a given inbox is a previous version at level L_1 of the inbox found at level L: these are called inclusion proofs.
Clients
This module is meant to be used both by the protocol and by the rollup node in order to maintain consistent inboxes on both sides. These two clients slightly differ on the amount of information they store about the inbox.
On the one hand, to reduce the space consumption of rollups on the chain storage, the protocol only stores metadata about the inbox. The messages of the current level are kept in memory during block validation only (See Raw_context.Sc_rollup_in_memory_inbox). By contrast, the messages of the previous levels are not kept in the context at all. They can be retrieved from the chain history though. However, being absent from the context, they are not accessible to the protocol.
On the other hand, the rollup node must keep a more precise inbox to be able to produce Merkle proofs about the content of specific messages, at least during the refutation period.
To cope with the discrepancy of requirements in terms of inbox storage while preserving a consistent Merkelization between the protocol and the rollup node, this module exposes the hashing schemes used to merkelize the inbox as a functor parameterized by the exact context where Merkle trees are stored.
include module type of V1 with type t = V1.t
The type of the inbox for a smart-contract rollup as stored by the protocol in the context. Values that inhabit this type only act as fingerprint for inboxes.
Inbox contents is represented using Raw_context.TREE.trees. (See below.)
val equal : t -> t -> boolempty level is an inbox started at some given level with no message at all.
inbox_level inbox returns the maximum level of message insertion in inbox or its initial level.
number_of_available_messages inbox returns the number of messages that can be consumed in inbox.
val number_of_messages_during_commitment_period : t -> int64number_of_messages_during_commitment_period inbox returns the number of messages added in the inbox since the beginning of the current commitment period.
start_new_commitment_period inbox level marks the beginning of a new commitment period at some level.
starting_level_of_current_commitment_period inbox returns the level at the beginning of a current commitment period.
consume_n_messages n inbox returns an inbox where n messages have been consumed, or None if there are strictly less than n messages available in inbox.
The following operations are subject to cross-validation between rollup nodes and the layer 1.
module type TREE = sig ... endThis validation is based on a standardized Merkelization scheme. The definition of this scheme is independent from the exact data model of the context but it depends on the Tree arity and internal hashing scheme.
include MerkelizedOperations
with type tree = Tezos_protocol_environment_014_PtKathma.Context.tree
The type for the Merkle trees used in this module.
A merkelized sequence of messages.
The history is a merkelized sequence of messages, one per level. The history is typically used by the rollup node to produce inclusion proofs. The protocol only manipulates an empty history as it does not remember previous messages and only keeps a witness of the latest state of the history.
val history_at_genesis : bound:int64 -> historyThe beginning of the history is an empty sequence of messages. Fail with Invalid_bound_on_history if bound is not strictly positive.
add_external_messages history inbox level payloads messages inserts a list of payloads as new messages in the messages of the current level of the inbox. This function returns the new sequence of messages as well as updated inbox and history.
If the inbox's level is older than level, the inbox is updated so that the messages of the levels older than level are archived. To archive a sequence of messages for a given level, we push it at the end of the history and update the witness of this history in the inbox. The inbox's messages for the current level are also emptied to insert the payloads in a fresh sequence of messages for level.
This function fails if level is older than inbox's level.
add_messages_no_history inbox level payloads messages behaves as add_external_messages except that it does not remember the inbox history.
get_message messages idx returns Some message if the sequence of messages has a more than idx messages and message is at position idx in this sequence. Returns None otherwise.
get_message_payload messages idx returns Some payload if the sequence of messages has a more than idx messages, message is at position idx in this sequence, and is defined by payload. Returns None otherwise.
Given a inbox A at some level L and another inbox B at some level L' >= L, an inclusion_proof guarantees that A is an older version of B.
To be more precise, an inclusion_proof guarantees that the previous levels messages of A are included in the previous levels messages of B. The current messages of A and B are not considered.
The size of this proof is O(log_basis (L' - L)).
number_of_proof_steps proof returns the length of proof.
produce_inclusion_proof history inboxA inboxB exploits history to produce a self-contained proof that inboxA is an older version of inboxB.
verify_inclusion_proof proof inboxA inboxA returns true iff proof is a minimal and valid proof that inboxA is included in inboxB.
module Proof : sig ... endThe Proof module wraps the more specific proof types provided earlier in this file into the inbox proof as it is required by a refutation.