package tezos-protocol-015-PtLimaPt

  1. Overview
  2. Docs
Tezos/Protocol: economic-protocol definition

Install 

dune-project
 Dependency

www.tezos.com Readme Edit opam file Versions (8)

Authors

  1. T
    Tezos devteam

Maintainers

  1. C
    contact@tezos.com

Sources

tezos-16.1.tar.gz
sha256=43723d096307603703a1a89ed1b2eb202b365f5e7824b96b0cbf813b343a6cf7
sha512=b2a637f2e965000d3d49ad85277ca24d6cb07a1a7cf2bc69d296d8b03ad78c3eaa8e21e94b9162e62c2e11649cd03bc845b2a3dafe623b91065df69d47dc8e4f

doc/tezos-protocol-015-PtLimaPt.raw/Tezos_raw_protocol_015_PtLimaPt/Sc_rollup_inbox_repr/index.html

Module Tezos_raw_protocol_015_PtLimaPt.Sc_rollup_inbox_reprSource

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.

Sourcemodule Hash : sig ... end
Sourcemodule V1 : sig ... end

Versioning, see Sc_rollup_data_version_sig.S for more information.

include Sc_rollup_data_version_sig.S with type t = V1.t
Sourcetype versioned
Sourceval of_versioned : versioned -> V1.t
Sourceval to_versioned : V1.t -> versioned
include module type of V1 with type t = V1.t
Sourcetype 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.)

Sourceval equal : t -> t -> bool
Sourceval inbox_level : t -> Raw_level_repr.t

inbox_level inbox returns the maximum level of message insertion in inbox or its initial level.

Sourcetype history_proof

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.

Sourceval equal_history_proof : history_proof -> history_proof -> bool
Sourceval old_levels_messages : t -> history_proof

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.

Sourceval number_of_messages_during_commitment_period : t -> int64

number_of_messages_during_commitment_period inbox returns the number of messages added in the inbox since the beginning of the current commitment period.

Sourceval refresh_commitment_period : commitment_period:int32 -> level:Raw_level_repr.t -> t -> t

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

Sourceval current_level_hash : t -> Hash.t

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

Sourcetype serialized_proof
Sourcemodule type Merkelized_operations = sig ... end

The following operations are subject to cross-validation between rollup nodes and the layer 1.

Sourcemodule type P = sig ... end

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

Sourceval hash_level_tree : tree -> Hash.t

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

Sourceval take_snapshot : t -> history_proof

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.

Sourcetype inclusion_proof

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

Sourceval number_of_proof_steps : inclusion_proof -> int

number_of_proof_steps proof returns the length of proof.

Sourceval verify_inclusion_proof : inclusion_proof -> history_proof -> history_proof -> bool

verify_inclusion_proof proof a b returns true iff proof is a minimal and valid proof that a is included in b.

Sourcetype proof

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.

Sourceval to_serialized_proof : proof -> serialized_proof
Sourceval of_serialized_proof : serialized_proof -> proof option

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.

Sourcemodule Internal_for_tests : sig ... end
Sourcetype inbox = t