feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding

[Abraxas1010]

Summary

Phase 1 of the hash-based post-quantum signature lane proposed in Verified-zkEVM/ArkLib#625: Merkle authentication paths whose node hash is the existing TweakableHash, with the tweak varying by level (tweakAt s.depth at the node rooting subtree s). This is the tree layout of the XMSS family — SLH-DSA / SPHINCS+ H, and the lean-Ethereum leanSig proposal — where per-level domain separation is exactly what lets security rest on target-collision resistance instead of full collision resistance.

Main results (#print axioms in parentheses)

• buildMerkleTreeTweaked / getPutativeRootTweaked — tweaked build and putative-root recomputation; the untweaked generateProof is reused unchanged.
• tweaked_functional_completeness (no axioms at all) — honest paths verify.
• TweakedCollision, findCollisionTweaked, findCollisionTweaked_sound, getPutativeRootTweaked_binding_collision ([propext]) — the constructive binding kernel, mirroring Inductive/Binding.lean: two distinct leaf values verifying to the same root at the same index yield a tweak-tagged collision as data — two distinct pairs with equal digest under the same tweak. The returned tweak identifies the level, i.e. the SM-TCR target: this is precisely the win-condition shape of HardnessAssumptions.MultiTarget.TcrProblem, so wiring the binding kernel into the SM-TCR game (and onward to XMSS unforgeability) needs no new collision notion.

Design notes

• Tweaks are indexed by subtree depth (ℕ → Tweak), the least structure that expresses per-level separation; an instantiation can refine to the full SLH-DSA-style address scheme by choosing Tweak.
• The module deliberately contains no probabilistic layer: it is the deterministic kernel the game-level reductions consume, in the same relationship to MultiTarget as Inductive/Binding.lean is to the ROM development.

Validation performed (not in the diff)

lake build VCVio green at 24fe01d; concrete sanity: honest roundtrip on a depth-2 tree (root 38407 recomputed from every opening), a constant-tweak build yields a different root (343 — level separation is live, not decorative); mutation check: swapping the hash argument order in the ofLeft branch makes completeness and binding fail to compile (4 errors).

Follow-ups per the #625 phasing: Winternitz/target-sum chains, XMSS correctness, unforgeability from SM-TCR, leanSig production instantiation (Poseidon2/KoalaBear). Naming and placement (MerkleTree/Tweaked/ vs a future Signatures/HashBased/) happy to move wherever maintainers prefer.

---

Contributed by The Institute for Ontological Mathematics (IAOM) / Equation Capital dba Apoth3osis.

[github-actions]

🤖 PR Summary

This PR introduces a generic addressed Merkle tree engine and a level-separated (tweaked) specialization, providing completeness and collision-binding theorems. No sorries are introduced.

---

Statistics

Metric	Count
📝 Files Changed	3
✅ Lines Added	552
❌ Lines Removed	0

---

Lean Declarations

✏️ Added: 23 declaration(s)

VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean (19)

• def AddressedCollision {s : Skeleton} (nodeHash : NodeAddress s → α → α → α)
• def addressedNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def buildMerkleTreeAddressedWithHash {s : Skeleton} (leaf_tree : LeafData α s)
• def childPairAt : {s : Skeleton} → FullData α s → NodeAddress s → α × α
• def findCollisionAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) →
• def getPutativeRootAddressedWithHash :
• def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• def pathDepth : {s : Skeleton} → NodeAddress s → ℕ
• def populateUpAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) →
• def subtreeDepth : {s : Skeleton} → NodeAddress s → ℕ
• theorem addressed_functional_completeness {s : Skeleton}
• theorem addressed_oriented_binding {s : Skeleton}
• theorem findCollisionAddressed_isSome {s : Skeleton}
• theorem findCollisionAddressed_oriented {s : Skeleton}
• theorem findCollisionAddressed_sound {s : Skeleton}
• theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton}
• theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton}
• theorem levelNodeHash_eq_addressed {PkSeed Tweak Y : Type}
• theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton}

VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean (4)

• def buildMerkleTreeLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
• theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y)
• theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y)

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• VCVio.lean: Added imports for two new modules, VCVio.CryptoFoundations.MerkleTree.Addressed.Basic and VCVio.CryptoFoundations.MerkleTree.Addressed.Level, which bring in definitions and results related to an addressed variant of the Merkle tree structure.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean: This new file defines the AddressedMerkleTree namespace, implementing a generic engine for Merkle trees whose node hash depends on the node's full typed address (NodeAddress s). It introduces the inductive type NodeAddress for paths to internal nodes, along with the core constructions populateUpAddressed/buildMerkleTreeAddressedWithHash (cache building) and getPutativeRootAddressedWithHash (root recomputation). The theorem addressed_functional_completeness proves that honest authentication paths verify correctly for any address-dependent hash. The kernel findCollisionAddressed produces an address-tagged collision when two openings agree on the root but differ in leaf value or path, with soundness and isSome guarantees (findCollisionAddressed_sound, findCollisionAddressed_isSome); getPutativeRootAddressedWithHash_binding_collision packages this as a user-facing binding statement. Two oriented theorems (findCollisionAddressed_oriented, addressed_oriented_binding) refine the collision to expose the honestly-precommitted child pair at the tagged address, suitable for a target-collision reduction. Finally, instances show that constant nodeHash recovers the unaddressed engine (getPutativeRootAddressed_const, populateUpAddressed_const), and the file provides levelNodeHash (via subtreeDepth) and addressedNodeHash (via an arbitrary map) to instantiate level-separated and fully-addressed (XMSS-style) trees, with levelNodeHash_eq_addressed showing the former factor through the latter.
• VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean: This new file Level.lean introduces a level-separated (per-subtree-depth) specialization of the addressed Merkle tree engine. It defines buildMerkleTreeLevel and getPutativeRootLevel that wrap the generic buildMerkleTreeAddressedWithHash and getPutativeRootAddressedWithHash with levelNodeHash. Two theorems from the engine are instantiated: level_functional_completeness (verifying that a generated proof recovers the root) and level_oriented_binding (establishing an oriented collision-binding property under the tweak of the collision's level). No sorry or admit appear in the file.

---

Last updated: 2026-07-12 13:36 UTC.

[quangvdao]

Thank you for the compact and well-structured deterministic development. The completeness and collision-tracing proofs themselves look reasonable. I am requesting changes because the current API and documentation do not yet justify the XMSS/SM-TCR interpretation, and this PR is intended to become the semantic foundation for the wider hash-signature lane.

There are three blocking issues.

1. A same-tweak collision is not by itself an SM-TCR break.

getPutativeRootTweaked_binding_collision starts from two arbitrary, potentially adversarial openings and returns distinct p₁,p₂ with

th.eval pk t p₁ = th.eval pk t p₂.

This is a symmetric same-tweak collision. Target-collision resistance is directional: one input must be fixed through the target-generation/commitment phase, and the adversary subsequently supplies the distinct colliding input. The current theorem does not establish which endpoint is the precommitted target or that it was fixed at the required time.

Please either:

• keep this as an accurately named same-tweak collision kernel, without claiming that it is already an SM-TCR win condition; and add a later oriented theorem/game reduction comparing an honestly fixed tree/path with an adversarial alternative opening; or
• establish that oriented reduction in this PR.

The first option is perfectly acceptable as a staged result. What is not acceptable is treating the symmetric collision witness as already equivalent to TCR.

2. The existing MultiTarget.TcrProblem needs an audit before being used as the target assumption.

Its f is a fixed public deterministic function, and TcrAdversary.choose is parameterized by the problem and can therefore evaluate prob.f while choosing targets. An adversary can search for a collision during choose, designate one endpoint as its target, store the other endpoint, and return it during forge. Without later challenge randomness or a post-target hidden key, this risks collapsing the stated TCR game back to ordinary collision resistance.

This also does not match the SM-rTCR game used by leanSig: that game has a target-generation oracle which samples the target randomness rather than letting the adversary choose all of it (Definition 6 of https://eprint.iacr.org/2025/055.pdf).

Before wiring the tree theorem to MultiTarget.TcrProblem, please identify the exact TCR/SM-rTCR notion required by the intended XMSS/leanSig proof and repair or replace the game accordingly. Then prove the reduction to that game, including the target orientation.

3. tweakAt : ℕ → Tweak cannot express a full XMSS/SLH-DSA node address.

Every node at the same subtree depth receives the same tweak. Choosing a richer Tweak type does not repair this, because tweakAt is only given the depth and cannot distinguish two nodes at the same level. It cannot vary the tree/layer, horizontal node index/path, or function/domain tag per node.

Please parameterize hashing by a genuine typed node address or node position, carrying at least the context needed by the intended scheme. A level-only instantiation can then be recovered as a special case. Alternatively, strictly scope this PR to a level-separated toy/general Merkle tree and remove the claim that it models the XMSS/SLH-DSA layout or can recover full addressing merely by choosing Tweak.

Architecturally, I would strongly prefer generalizing the existing inductive Merkle engine over a node-addressed hash such as

nodeHash : NodeAddress s → Y → Y → Y

rather than duplicating tree construction, putative-root computation, collision search, and binding. The ordinary tree, a level-separated tree, and the eventual XMSS tree should then be instances of one engine, with completeness and collision tracing proved once. This will also give us a sensible path to tweaked batch openings later.

Concrete signature encoding and a full XMSS unforgeability proof are not prerequisites for this PR. A deterministic, address-aware collision kernel is a good intermediate deliverable. But its statement must distinguish ordinary same-tweak collision extraction from the later directional SM-TCR reduction.

Finally, please update the branch to current main (#477 is already merged) and rerun CI after the redesign.

[Abraxas1010]

Thank you for the careful semantic review — all three blocking points are correct, and I've taken the staged option on each:

1. Same-tweak collision ≠ SM-TCR break. Agreed — the kernel is symmetric and establishes no target orientation. The module is now scoped as exactly what it proves: a same-tweak collision kernel (TweakedCollision as data, findCollisionTweaked_sound). All claims that this is already an SM-TCR win condition are removed from the docs; the oriented reduction (honestly fixed tree/path in the commitment phase vs. a subsequent adversarial opening) is named as the follow-up theorem it actually is.

2. MultiTarget.TcrProblem audit. Agreed, and de-wired: the module no longer points at MultiTarget.TcrProblem as its target assumption. Your observation that TcrAdversary.choose can evaluate the fixed public f while choosing targets — collapsing the game toward plain CR — matches my reading; the game needs sampled target randomness (SM-rTCR à la leanSig Definition 6) or a post-target key before anything should reduce to it. I'll treat that audit/repair as its own PR and only then prove the oriented reduction against the repaired game.

3. Level-only tweaks cannot express XMSS addressing. Agreed — tweakAt : ℕ → Tweak cannot distinguish same-depth nodes, and no choice of Tweak repairs that. The XMSS/SLH-DSA layout claim is removed; the module is scoped as a level-separated Merkle tree. On architecture I also agree with the stronger point: the right home for this is the existing inductive engine generalized over a node-addressed hash (nodeHash : NodeAddress s → Y → Y → Y), with ordinary, level-separated, and XMSS-addressed trees as instances of one engine — completeness and collision tracing proved once. I'd like to do that generalization as the follow-up PR (it subsumes this module; this one then either becomes the level-indexed instance or is dropped in its favor).

Branch is rebased onto current main (post-#477) with CI rerunning. If you'd rather I hold this PR and go straight to the node-addressed engine, happy to do that instead — otherwise this stands as the honestly-scoped intermediate deliverable.

[quangvdao]

Please address all the limitations instead of just acknowledging them - I will hard block on this PR until all of them are resolved and I find no remaining misformalizations

[Abraxas1010]

Understood — the limitations are now resolved in code on this branch, not acknowledged. Point by point against the three blockers:

3. Addressing (resolved). The branch now contains the architecture you specified: MerkleTree/Addressed/Basic.lean generalizes the inductive engine over nodeHash : NodeAddress s → Y → Y → Y, where NodeAddress is the typed root-path position of each internal node (the full per-node context; nothing is collapsed before the user's map is applied). Building, putative-root recomputation, completeness, and constructive collision tracing are defined and proven once; the address is threaded by reindexing (nh ∘ .inL/.inR) rather than an accumulator. The constant instance provably recovers the unaddressed engine (getPutativeRootAddressed_const, populateUpAddressed_const); full addressing is addressedNodeHash (any tweakOf : NodeAddress s → Tweak); level separation is its depth-collapsed special case (levelNodeHash_eq_addressed).

1. Orientation (resolved, deterministically). findCollisionAddressed_oriented / addressed_oriented_binding: for an honestly built tree and an adversarial opening that verifies against its root with a different leaf value, the returned collision's first endpoint is the honestly-precommitted child pair stored in the cache at the tagged address — fixed at build time, before the adversarial opening exists. So the theorem is no longer symmetric: one side is pinned to commitment-time data, per address. What I have deliberately not claimed: that this is itself a game win — it is the deterministic directional kernel a game reduction consumes.

2. The TCR game (de-wired; repair scoped). Nothing on this branch references MultiTarget.TcrProblem. I agree with your audit finding (choose can evaluate the fixed public f), and that the right target notion is SM-rTCR with oracle-sampled target randomness (leanSig, eprint 2025/055 Def. 6). One question before I write that game, since it's the piece where a wrong formalization would be costly: would you prefer the SmRTcrProblem definition + the probabilistic reduction (consuming addressed_oriented_binding) in this PR, or as its own PR against HardnessAssumptions/ where the game design can be reviewed on its own? I have the reduction plan either way; I don't want to guess the game encoding you'd accept.

Duplication (resolved). Tweaked/Basic.lean is deleted. Its honest content survives as Addressed/Level.lean — thin instantiations whose completeness and oriented binding are the engine theorems at levelNodeHash; no duplicated recursion or proof remains, and no XMSS/SLH-DSA layout claim is made anywhere on the branch.

Branch is on current main, full lake build VCVio green. The load-bearing theorems were checked non-vacuous (completeness is not closed by rfl; a child-swapped mutant verifier is refuted by decide on a concrete instance).