Extending Trees

[larskuhtz]

Implement extension of trees without recreating the tree from scratch.

Each subtree that is a full binary tree is immutable and won't change. Full binary subtrees are ordered in memory, with the larger trees coming before smaller trees. There is always at most one tree of each size. The set of full subtrees forms an immutable prefix in memory.

When extending a tree a suffix of at most a logarithmic number of nodes has to be updates. In concrete the nodes that form the path from the smallest full subtree to the root of the tree, or, equivalently, the roots of unbalanced subtrees.

This means that a tree can be extended efficiently by just changing and extending a suffix of logarithmic size of the tree.

Moreover old trees can easily recovered from the extended tree by computing a logarithmic number of nodes. Old versions of the tree can therefore be recomputed efficiently and thus there no need to keep the updated nodes around in memory. (This is related to the implementation of consistency proofs.)