Research proof index

Completeness theorem for Merkle trees. The proof proceeds by reducing to the functional completeness theorem by a theorem about the OracleComp monad, and then applying the functional version of the completeness theorem.

The extractability theorem for Merkle trees. Adapting from the SNARGs book Lemma 18.5.1: For any adversary 𝒜 whose committing and opening phases together obey the two-phase total query bound qb, if the game runs 𝒜.commit and 𝒜.opening, and the extractor algorithm is run on the resulting cache and root, then with probability at most κ does `𝒜...

Soundness: if findCollision returns a tuple, that tuple is a hash collision according to Collision.

A functional form of the batch completeness theorem: the honest batch proof generated from an honestly built tree, together with the true selected leaf values, recomputes the tree's root , under any hash function and any selector opening at least one leaf.

Batch opening uniqueness. When hashFn is injective, two batch openings for the same selector that produce the same putative root must agree on both the claimed selected values and the entire pruned authentication data.

getPutativeRoot makes one oracle query per level of idx, so it has total query bound idx.depth.