Is it possible to build short proofs of arbitrary computations over a big list? With the use of Merkle Trees, you can prove the presence of an element of a very big list, with an amount of information logarithmic in the size of the whole tree. Merkle proofs, thus, probabilistically confirm the result of this specific fold:

isMember :: ∀ t . List t -&gt; Bool
isMember e = foldr (\ h t -&gt; h == e || t) False


My question is if the same result can be extended to arbitrary folds; or, in other words, is it possible to prove arbitrary computations about a big list using some clever trick similar to Merkle Trees?

Specifically, I want to store a huge dataset (>20 GB) on several computers, and then I want any of those nodes to make arbitrary claims about that dataset (like: the max element is 198500461354!), in such a way that other nodes can verify that claim is true without having to run max over the whole dataset themselves.
Merkle aggregation can help you compute aggregation functions over the leaf data in a Merkle tree.

The technique is described in detail in Crosby &amp; Wallach's paper on history trees [1], an append-only Merkle tree. Merkle aggregation can be used to provably compute things like $\max(\cdot,\cdot)$ functions over all leafs.

The idea is quite straightforward.
Each node can have an attribute and there's an aggregator function $\alpha(l, r)$ which takes the attributes from the two children and returns the parent's attribute. For example, the aggregator function can be $\max(\cdot,\cdot)$.

By recursively applying $\alpha(\cdot,\cdot)$ starting with the leafs, attributes can be computed or aggregated for all nodes in the tree, all the way up to the root. Furthermore, the computed attributes are hashed in the Merkle tree. Specifically, a node's hash is no longer just $H(h_l, h_r)$ but $H(h_l, a, h_r)$, where $h_l,h_r$ denote the left and right child hashes and $a$ denotes the aggregated attribute computed via $\alpha(l,r)$.

Including the attributes in the Merkle hashing enables a prover to convince a verifier that the aggregation was performed correctly. Of course, the Merkle proof is a bit different now. Specifically, a Merkle path from a leaf to the root consists not just of the hashes along the sibling path, but also of the attributes along the path and the sibling path, so as to verify the aggregation.

Hope this helps!

References

[1] "Efficient Data Structures for Tamper-Evident Logging", by Scott A. Crosby, and Dan S. Wallach