Research proof index

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

Merkle binding: from two distinct leaf values x ≠ y that produce the same putative root at the same leaf index under (possibly different) sibling proofs, the constructive search findCollision returns some. Note that idx is shared , this is binding at a fixed position. The distinct-position case requires walking down both paths to the lowest comm...

The KZG scheme satisfies evaluation binding provided t-SDH holds.

Transition 2: a successful extended binding run maps to a successful t-SDH instance.

Transition 1: extending the binding game output preserves the event.

The algebraic core of evaluation binding: two valid KZG openings of the same commitment at the same point, but to different values, yield a t-SDH solution with challenge c = -query. This lemma is intentionally isolated from the probabilistic (game-based) binding game. The proof of binding_cond_le_t_sdh_cond only needs to extract hsrs and the two `ve...