Research proof index

Fischlin signing has weighted query cost at most ρ • (|Ω| • w) whenever every random-oracle query carries cost at most w.

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.