package irmin-layers

  1. Overview
  2. Docs

Proofs are compact representations of Irmin trees which can be shared between an Irmin node and a client.

The protocol is the following:

  • The Irmin node runs a function f over a tree t. While performing this computation, the node records: the hash of t (called before below), the hash of f t (called after below) and a subset of t which is needed to replay f without any access to the node's storage. Once done, the node packs this into a proof p and sends this to the client.
  • The client generates an initial tree t' from p and computes f t'. Once done, it compares t''s hash and f t''s hash to before and after. If they match, they know that the result state f t' is a valid state of Irmin, without having to have access to the full node's storage.
type 'a inode = {
  1. length : int;
  2. proofs : (int * 'a) list;
}

The type for (internal) inode proofs.

These proofs encode large directories into a more efficient tree-like structure.

Invariant are dependent on the backend.

length is the total number of entries in the chidren of the inode. E.g. the size of the "flattened" version of that inode. This is used by some backend (like irmin-pack) to efficiently implements paginated lists and an optimized lenght function.

For irmin-pack: proofs have a length of at most Conf.entries entries. This list can be sparse so every proof is indexed by their position between 0 ... (Conf.entries-1). For binary trees, this boolean index is a step of the left-right sequence / decision proof corresponding to the path in that binary tree.

val inode_t : 'a Irmin.Type.t -> 'a inode Irmin.Type.t
type 'a inode_extender = {
  1. length : int;
  2. segments : int list;
  3. proof : 'a;
}

The type for inode extenders.

val inode_extender_t : 'a Irmin.Type.t -> 'a inode_extender Irmin.Type.t
type tree =
  1. | Contents of contents * metadata
  2. | Blinded_contents of hash * metadata
  3. | Node of (step * tree) list
  4. | Blinded_node of hash
  5. | Inode of inode_tree inode
  6. | Extender of inode_tree inode_extender

The type for compressed and partial Merkle tree proofs.

Tree proofs do not provide any guarantee with the ordering of computations. For instance, if two effects commute, they won't be distinguishable by this kind of proofs.

Blinded_node h is a shallow pointer to a node having hash h.

Node ls is a "flat" node containing the list of files ls. The length of ls depends on the backend. For instance, it can be unbounded for most of the backends, while it is at most Conf.stable_hash entries for irmin-pack.

Inode i is an optimized representation of a node as a tree. Pointers in that trees would refer to blinded nodes, nodes or to other inodes. E.g. Blinded content nor contents is not expected to appear directly in an inodes.

Blinded_contents (h, m) is a shallow pointer to contents having hash h and metadata m.

Contents c is the contents c.

and inode_tree =
  1. | Blinded_inode of hash
  2. | Inode_values of (step * tree) list
  3. | Inode_tree of inode_tree inode
  4. | Inode_extender of inode_tree inode_extender
val tree_t : tree Irmin.Type.t
val inode_tree_t : inode_tree Irmin.Type.t
type kinded_hash = [
  1. | `Contents of hash * metadata
  2. | `Node of hash
]

The type for kinded hashes.

val kinded_hash_t : kinded_hash Irmin.Type.t
type elt =
  1. | Contents of contents
  2. | Node of (step * kinded_hash) list
  3. | Inode of hash inode
  4. | Inode_extender of hash inode_extender
val elt_t : elt Irmin.Type.t
type stream = elt Seq.t

The type for stream proofs. Stream poofs provides stronger ordering guarantees as the read effects have to happen in the exact same order and they are easier to verify.

val stream_t : stream Irmin.Type.t
type 'a t

The type for proofs.

val t : 'a Irmin.Type.t -> 'a t Irmin.Type.t
val v : before:kinded_hash -> after:kinded_hash -> 'a -> 'a t

v ~before ~after p proves that the state advanced from before to after. p's hash is before, and p contains the minimal information for the computation to reach after.

val before : 'a t -> kinded_hash

before t it the state's hash at the beginning of the computation.

val after : 'a t -> kinded_hash

after t is the state's hash at the end of the computation.

val state : 'a t -> 'a

proof t is a subset of the initial state needed to prove that the proven computation could run without performing any I/O.

val to_tree : tree t -> tree

to_tree p is the tree t representing the tree proof p. Blinded parts of the proof will raise Dangling_hash when traversed.