Merkle Opening Uniqueness

When the hash function is injective (Function.Injective2 h), any two openings at the same leaf index that produce the same putative root must agree on both the leaf value and the authentication path. This is the deterministic analog of extractability: the Merkle root uniquely determines the committed value at each position.

Combined with getPutativeRootWithHash_binding from Binding.lean, this gives a complete picture of Merkle commitment security:

• Binding (no CR needed): same index, distinct values → hash collision.
• Uniqueness (injective hash): same index, same root → identical opening.

The distinct-index case is not a binding violation — two different leaf positions producing the same root is normal Merkle tree operation.

Main Results

• getPutativeRootWithHash_unique — opening uniqueness under injective hash
• getPutativeRootWithHash_roots_ne_of_ne — contrapositive: distinct values at the same index produce distinct roots

References

• Justin Thaler. Proofs, Arguments, and Zero-Knowledge. §7.3.2.2 (Merkle-tree string commitment binding property)
• Vitalik Buterin. Binding.lean (PR #384) — same-index collision extraction

theorem InductiveMerkleTree.getPutativeRootWithHash_unique {α : Type u_1} (h : α → α → α) (hinj : Function.Injective2 h) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) (heq : getPutativeRootWithHash idx x proof₁ h = getPutativeRootWithHash idx y proof₂ h) : x = y ∧ proof₁ = proof₂

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. The inductive hypothesis then gives agreement on the leaf value and the remaining proof elements.

theorem InductiveMerkleTree.getPutativeRootWithHash_roots_ne_of_ne {α : Type u_1} (h : α → α → α) (hinj : Function.Injective2 h) {s : BinaryTree.Skeleton} (idx : BinaryTree.SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) (hne : x ≠ y) : getPutativeRootWithHash idx x proof₁ h ≠ getPutativeRootWithHash idx y proof₂ h

Contrapositive of uniqueness: with an injective hash, distinct leaf values at the same index always produce distinct roots, regardless of the authentication paths used.