Module Raw_context.Proof

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

This is expected to be used as follows:

type step = string

The type for file and directory names.

type value = bytes

The type for values.

type index = int

The type of indices for inodes' children.

The type for hashes.

type 'a inode = {
  1. length : int;
  2. proofs : (index * 'a) list;
}

The type for (internal) inode proofs.

These proofs encode large directories into a tree-like structure. This reflects irmin-pack's way of representing nodes and computing hashes (tree-like representations for nodes scales better than flat representations).

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 Tree.length and Tree.list ~offset ~length in an efficient way.

In proofs with version.is_binary = false, an inode at depth 0 has a length of at least 257. Below that threshold a Node tag is used in tree. That threshold is 3 when version.is_binary = true.

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.

In proofs with version.is_binary = true, inodes have at most 2 proofs (indexed 0 or 1).

In proofs with version.is_binary = false, inodes have at most 32 proofs (indexed from 0 to 31).

type 'a inode_extender = {
  1. length : int;
  2. segment : index 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 lenght l and final proof p.

type tree =
  1. | Value of value
  2. | Blinded_value of hash
  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.

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.

In proofs with version.is_binary = true, the length of ls is at most 2.

In proofs with version.is_binary = false, the length of ls is at most 256.

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.

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

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 similar to trees' Node.

Inode_tree i is similar to tree's Inode.

Inode_extender e is similar to trees' Extender.

type kinded_hash = [
  1. | `Value of hash
  2. | `Node of hash
]

The type for kinded hashes.

module Stream : sig ... end

Stream proofs represent an explicit traversal of a Merle tree proof. Every element (a node, a value, or a shallow pointer) met is first "compressed" by shallowing its children and then recorded in the proof.

type stream = Stream.t
type 'a t = {
  1. version : int;
  2. before : kinded_hash;
  3. after : kinded_hash;
  4. state : 'a;
}

The type for proofs of kind 'a.

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.

version p is the proof version, it packs several informations.

is_stream discriminates between the stream proofs and the tree proofs.

is_binary discriminates between proofs emitted from Mavryk_context(_memory).Context_binary and Mavryk_context(_memory).Context.

It will also help discriminate between the data encoding techniques used.

The version is meant to be decoded and encoded using the Mavryk_context_helpers.Context.decode_proof_version and Mavryk_context_helpers.Context.encode_proof_version.