module arch.system.types.commitmenttree;

import prelude open;
import arch.node.types.crypto open;
import arch.system.types.commitment open;

Commitment Trees¶

Purpose¶

Commitment trees are a tree-like data structure that stores commitments and provide a way to efficiently store, retrieve those commitments, and verify their inclusion in the tree.

Commitment trees are part of the state in the system.

CommitmentTreeOps¶

The CommitmentTreeOps trait defines the stateless operations that a tree that stores commitments must implement.

The CommitmentTreeOps type has the following type parameters:

• A : The type of the data that is being committed.
• Tree : The type of the tree that stores the commitments.
• P : The type of the path that is used to navigate through the tree.

trait
type CommitmentTreeOps A (Tree : Type -> Type) P :=
  mkCommitmentTreeOps@{
    hashRoot : Tree A -> Digest;
    add : A -> Tree A -> Pair (Tree A) P;
    read : P -> Tree A -> Option (Commitment A);
    verify : P -> Commitment A -> Tree A -> Bool;
  };

An instance of CommitmentTreeOps¶

We now define an instance of a CommitmentTreeOps for the CTree type. Trees of this type can be used as default cryptographic accumulators.

The CTree type is defined as a specialised MTree, a general type of tree that can be used as a cryptographic accumulator.

MTree¶

A MTree is a data structure that accumulates the output related to the values of its children in the node merge. In the leaves, we store the some particular data.

type MTree A B :=
  | mkMTreeLeaf@{
      value : A;
    }
  | mkMTreeNode@{
      merge : B;
      left : MTree A B;
      right : MTree A B;
    };

CTree¶

Trees of type CTree are specialised MTree where the leaf nodes store Commitment values and the internal nodes store hashes, precisely. These hashes, Digest values, in the internal nodes represent the combined hash of their child nodes.

CTree (A : Type) : Type := MTree (Commitment A) Digest;

Let us now define the treeHash function which computes the hash of a CTree.

treeHash {A} (tree : CTree A) : Digest :=
  case tree of
    | mkMTreeLeaf@{value := c} := TODO
    | mkMTreeNode@{merge := digest} := digest;

To retrieve commitments from a CTree, we need to define a path which is a sequence of directions used to navigate through the tree.

PathDir¶

A path is a sequence of PathDir values used to navigate through a tree such as a CTree by specifying the direction to take at each node.

type PathDir :=
  | PathDirLeft
  | PathDirRight;

CTreePath¶

A CTreePath is a sequence of PathDir values used to navigate through a CTree.

CTreePath : Type := List PathDir;

CommitmentTree¶

CommitmentTree (A : Type) : Type := CommitmentTreeOps A CTree PathDir;