`Tree.Proof`

`val kinded_hash_t : kinded_hash Type.t`

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

.

`val inode_extender_t : 'a Type.t -> 'a inode_extender Type.t`

`type tree = `

`| Contents of contents * metadata` |

`| Blinded_contents of hash * metadata` |

`| Node of (step * tree) list` |

`| Blinded_node of hash` |

`| Inode of inode_tree inode` |

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

`and inode_tree = `

`| Blinded_inode of hash` |

`| Inode_values of (step * tree) list` |

`| Inode_tree of inode_tree inode` |

`| 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`

.

`val inode_tree_t : inode_tree Type.t`

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.

As stream proofs directly encode the recursive construction of the Merkle root hash is slightly simpler to implement: the verifier simply needs to hash the compressed elements lazily, without any memory or choice.

Moreover, the minimality of stream proofs is trivial to check. Once the computation has consumed the compressed elements required, it is sufficient to check that no more compressed elements remain in the proof.

However, as the compressed elements contain all the hashes of their shallow children, the size of stream proofs is larger (at least double in size in practice) than tree proofs, which only contains the hash for intermediate shallow pointers.

`type elt = `

`| Contents of contents` |

`| Node of (step * kinded_hash) list` |

`| Inode of hash inode` |

`| Inode_extender of hash inode_extender` |

The type for elements of stream proofs.

`Value v`

is a proof that the next element read in the store is the value `v`

.

`Node n`

is a proof that the next element read in the store is the node `n`

.

`Inode i`

is a proof that the next element read in the store is the inode `i`

.

`Inode_extender e`

is a proof that the next element read in the store is the node extender `e`

.

`type stream = elt Stdlib.Seq.t`

The type for stream proofs.

The sequance `e_1 ... e_n`

proves that the `e_1`

, ..., `e_n`

are read in the store in sequence.

The type for proofs of kind `'a`

(i.e. `stream`

or `proof`

).

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`

.

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