Research proof index

Batch completeness theorem for Merkle trees: building the tree honestly, generating the batch proof for any selector opening at least one leaf, and verifying it against the tree's root succeeds with probability 1 under the random oracle. The proof reduces to functional_batch_completeness through simulateQ, exactly as the single-index completeness...

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.