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_sig 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 messages in a commitment period is bounded by Constants_storage.sc_rollup_max_number_of_messages_per_commitment_period. When an inbox reaches the maximum number of messages in the commitment period, 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_sig, 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.
module Hash : sig ... endinclude 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 -> boolinbox_level inbox returns the maximum level of message insertion in inbox or its initial level.
A history_proof is a Skip_list.cell that stores multiple hashes. Skip_list.content history_proof gives the hash of the level tree for this cell, while Skip_list.back_pointers
history_proof is an array of hashes of earlier history_proofs in the inbox.
On the one hand, we think of this type as representing the whole Merkle structure of an inbox at a given level---it is the part of t above that can actually be used to prove things (it cannot be forged by a malicious node because it much match the hash stored by the L1).
On the other hand, we think of this type as representing a single proof-step back through the history of the inbox; given a hash that appears at some point later in the inbox this type proves that that hash points to this particular combination of a level tree and further back-pointers.
In terms of size, this type is a small set of hashes; one for the current level tree and `O(log2(ix))` in the back-pointers, where ix is the index of the cell in the skip list. That is, ix is the number of non-empty levels between now and the origination level of the rollup.
A History.t is basically a lookup table of history_proofs. We need this if we want to produce inbox proofs because it allows us to dereference the 'pointer' hashes in any of the history_proofs. This deref function is passed to Skip_list.back_path or Skip_list.search to allow these functions to construct valid paths back through the skip list.
old_levels_messages inbox returns the skip list of the inbox history. How much data there actually is depends on the context---in the L1 most of the history is forgotten and just a root hash of the skip list is kept.
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.
val refresh_commitment_period :
commitment_period:int32 ->
level:Raw_level_repr.t ->
t ->
trefresh_commitment_period ~commitment_period ~level inbox updates inbox to take into account the commitment_period: this resets a counter for the number of messages in a given commitment period (which is limited).
val current_level_hash : t -> Hash.tThis extracts the current level hash from the inbox. Note: the current level hash is stored lazily as fun () -> ..., and this function will call that function. So don't use this if you want to preserve the laziness.
The following operations are subject to cross-validation between rollup nodes and the layer 1.
module type P = 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 Merkelized_operations
with type tree = Tezos_protocol_environment_015_PtLimaPt.Context.tree
and type inbox_context = Tezos_protocol_environment_015_PtLimaPt.Context.t
The type for the Merkle trees used in this module.
The context used by the trees.
Standard hashing function used for trees in this module.
Initialise a new level. new_level_tree ctxt level is a merkle tree with no messages yet, but has the level stored so we can check that in proofs.
add_messages ctxt history inbox level payloads level_tree inserts a list of payloads as new messages in the level_tree of the current level of the inbox. This function returns the new level tree as well as updated inbox and history.
If the inbox's level is older than level, the inbox is updated so that the level trees of the levels older than level are archived. To archive a level_tree 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 level tree for the current level is emptied to insert the payloads in a fresh level_tree for level.
This function fails if level is older than inbox's level.
add_messages_no_history ctxt inbox level payloads level_tree behaves as add_external_messages except that it does not remember the inbox history.
get_message_payload level_tree idx returns Some payload if the level_tree has more than idx messages, and payload is at position idx. Returns None otherwise.
form_history_proof ctxt history inbox level_tree creates the skip list structure that includes the current inbox level, while also updating the history and making sure the level_tree has been committed to the ctxt.
This is used in archive_if_needed to produce the old_levels_messages value for the next level of the inbox. It is also needed if you want to produce a fully-up-to-date skip list for proof production. Just taking the skip list stored in the inbox at old_levels_messages will not include the current level (and that current level could be quite far back in terms of blocks if the inbox hasn't been added to for a while).
This is similar to form_history_proof except that it is just to be used on the protocol side because it doesn't ensure the history is remembered or the trees are committed in the context. Used at the beginning of a refutation game to create the snapshot against which proofs in that game must be valid.
This will however produce a history_proof with exactly the same hash as the one produced by form_history_proof, run on a node with a complete inbox_context.
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 level_trees of A are included in the previous levels level_trees of B. The current level_tree 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.
verify_inclusion_proof proof a b returns true iff proof is a minimal and valid proof that a is included in b.
An inbox proof has three parameters:
- the
starting_point, of type Raw_level_repr.t * Z.t, specifying a location in the inbox ;
- the
message, of type Sc_rollup_PVM_sig.input option ;
- and a reference
snapshot inbox.
A valid inbox proof implies the following semantics: beginning at starting_point and reading forward through snapshot, the first message you reach will be message.
Usually this is fairly simple because there will actually be a message at the location specified by starting_point. But in some cases starting_point is past the last message within a level, and then the inbox proof must prove that and also provide another proof about the message at the beginning of the next non-empty level.
See the docstring for the proof type for details of proof semantics.
verify_proof starting_point inbox proof will return the third parameter of the proof, message, iff the proof is valid.
produce_proof ctxt history inbox (level, counter) creates an inbox proof proving the first message after the index counter at location level. This will fail if the ctxt given doesn't have sufficient data (it needs to be run on an inbox_context with the full history).
empty ctxt level is an inbox started at some given level with no message at all.