package irmin

  1. Overview
  2. Docs
package irmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Tree.ProofSource

Proofs are compact representations of trees which can be shared between peers.

This is expected to be used as follows:

  • A first peer runs a function f over a tree t. While performing this computation, it 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 first peer's storage. Once done, all these informations are packed into a proof of type t that is sent to the second peer.
  • The second peer 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 context state, without having to have access to the full storage of the first peer.
Sourcetype kinded_hash = [
  1. | `Contents of hash * metadata
  2. | `Node of hash
]
Sourceval kinded_hash_t : kinded_hash Irmin.Type.t
Sourcetype 'a inode = {
  1. length : int;
  2. proofs : (int * 'a) list;
}

The type for (internal) inode proofs.

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

Invariants are dependent on the backend.

length is the total number of entries in the children of the inode. It's the size of the "flattened" version of that inode. length can be used to prove the correctness of operations such as Tree.length and Tree.list ~offset ~length in an efficient way.

proofs contains the children proofs. It is a sparse list of 'a values. These values are associated to their index in the list, and the list is kept sorted in increasing order of indices. 'a can be a concrete proof or a hash of that proof.

For irmin-pack: proofs have a length of at most Conf.entries entries. For binary trees, this boolean index is a step of the left-right sequence / decision proof corresponding to the path in that binary tree.

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

The type for inode extenders.

An extender is a compact representation of a sequence of inode which contain only one child. As for inodes, the 'a parameter can be a concrete proof or a hash of that proof.

If an inode proof contains singleton children i_0, ..., i_n such as: {length=l; proofs = [ (i_0, {proofs = ... { proofs = [ (i_n, p) ] }})]}, then it is compressed into the inode extender {length=l; segment = [i_0;..;i_n]; proof=p} sharing the same length l and final proof p.

Sourceval inode_extender_t : 'a Irmin.Type.t -> 'a inode_extender Irmin.Type.t
Sourcetype 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 proof.

Value v proves that a value v exists in the store.

Blinded_value h proves a value with hash h exists in the store.

Node ls proves that a a "flat" node containing the list of files ls exists in the store. For irmin-pack: the length of ls is at most Conf.stable_hash;

Blinded_node h proves that a node with hash h exists in the store.

Inode i proves that an inode i exists in the store.

Extender e proves that an inode extender e exist in the store.

Sourceand 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

The type for inode trees. It is a subset of tree, limited to nodes.

Blinded_inode h proves that an inode with hash h exists in the store.

Inode_values ls is simliar to trees' Node.

Inode_tree i is similar to tree's Inode.

Inode_extender e is similar to trees' Extender.

Sourceval inode_tree_t : inode_tree Irmin.Type.t
Sourcetype t

The type for Merkle proofs.

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

Sourceval v : before:kinded_hash -> after:kinded_hash -> tree -> 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.

Sourceval before : t -> kinded_hash

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

Sourceval after : t -> kinded_hash

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

Sourceval state : t -> tree

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

Sourceval to_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.