Research proof index

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.

Root preservation. The single-index opening extracted from a batch opening at any selected leaf recomputes exactly the batch opening's putative root. Consequently a batch opening that verifies against a root yields, at every selected leaf, a single-index opening that verifies against the same root.

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...

Merkle opening uniqueness. When h is injective, two openings at the same leaf index that produce the same root must agree on both the leaf value and the entire authentication path. Proof: induction on the index. At each internal node, injectivity of h forces both hash arguments to agree , the sibling (proof head) and the recursive subtree root. Th...

Log-level binding (Collision Lemma at the log level). Log-formalized analog of getPutativeRootWithHash_binding_collision: two distinct openings (x, proof₁) ≠ (y, proof₂) of the same root at the same index, both witnessed by hash chains ChainInLog in the same log, force log to contain a hash collision (two log entries with equal responses b...