Research proof index

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

Running the monadic version of buildMerkleTree with an oracle function f is equivalent to running the functional version of buildMerkleTreeWithHash with the same oracle function.