From c4fbac2a69f51fbbf148d5a0163233865b0ada36 Mon Sep 17 00:00:00 2001 From: Abraxas1010 Date: Fri, 10 Jul 2026 10:40:44 -0400 Subject: [PATCH 1/6] feat(MerkleTree): add tweaked Merkle authentication paths with completeness and tweak-tagged collision binding --- VCVio.lean | 1 + .../MerkleTree/Tweaked/Basic.lean | 235 ++++++++++++++++++ 2 files changed, 236 insertions(+) create mode 100644 VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean diff --git a/VCVio.lean b/VCVio.lean index e6bf199fc..44df43f70 100644 --- a/VCVio.lean +++ b/VCVio.lean @@ -55,6 +55,7 @@ import VCVio.CryptoFoundations.MerkleTree.Inductive.Defs import VCVio.CryptoFoundations.MerkleTree.Inductive.Extractability import VCVio.CryptoFoundations.MerkleTree.Inductive.QueryBound import VCVio.CryptoFoundations.MerkleTree.Inductive.Uniqueness +import VCVio.CryptoFoundations.MerkleTree.Tweaked.Basic import VCVio.CryptoFoundations.MerkleTree.Vector.Completeness import VCVio.CryptoFoundations.MerkleTree.Vector.Defs import VCVio.CryptoFoundations.PRF diff --git a/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean new file mode 100644 index 000000000..acd9c38d8 --- /dev/null +++ b/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean @@ -0,0 +1,235 @@ +/- +Copyright (c) 2026 IAOM / Equation Capital dba Apoth3osis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Abraxas1010 (IAOM / Apoth3osis) +-/ + +import VCVio.CryptoFoundations.MerkleTree.Inductive.Defs +import VCVio.CryptoFoundations.TweakableHash + +/-! +# Tweaked Merkle Authentication Paths + +Merkle trees whose node hash is a *tweakable* hash (`TweakableHash`), with the tweak varying +by level: the internal node rooting a subtree of skeleton `s` hashes its children under the +tweak `tweakAt s.depth`. This is the tree layout used by hash-based signature schemes in the +XMSS family (including the SLH-DSA / SPHINCS+ functions `H` and the lean-Ethereum leanSig +proposal), where domain separation by level is what enables *target*-collision-resistance +assumptions in place of full collision resistance. + +Contents: + +* `buildMerkleTreeTweaked` / `getPutativeRootTweaked` — tree building and putative-root + recomputation from a leaf, an authentication path, and a leaf index, hashing each level + under its own tweak. `generateProof` from the untweaked development is reused unchanged. +* `tweaked_functional_completeness` — honestly generated paths verify. +* `TweakedCollision` and `findCollisionTweaked` — the constructive binding kernel. A + disagreement between two verifying openings is traced down the two paths and returned as a + *tweak-tagged* collision: two distinct input pairs with the same digest **under the same + tweak**. This is exactly the win condition shape of the target-collision experiments in + `VCVio.CryptoFoundations.HardnessAssumptions.MultiTarget` (SM-TCR), so binding for the + tweaked tree needs only tweak-wise target collision resistance, not full collision + resistance of a single function. +* `getPutativeRootTweaked_binding_collision` — the user-facing binding statement: distinct + leaf values verifying to the same root at the same index yield a `TweakedCollision`, + as data. + +The proofs mirror `VCVio.CryptoFoundations.MerkleTree.Inductive.{Completeness, Binding}`, +generalized from a fixed `hashFn : α → α → α` to a level-indexed family. + +## References + +- Hülsing, Rijneveld, Song, Schwabe, "Mitigating Multi-Target Attacks in Hash-Based + Signatures" +- Drake, Khovratovich, Kudinov, Wagner, "Hash-Based Multi-Signatures for Post-Quantum + Ethereum" (leanSig; CiC 2025) +-/ + +namespace TweakedMerkleTree + +open BinaryTree InductiveMerkleTree + +variable {PkSeed Tweak Y : Type} + +/-- The node hash at the level of a subtree skeleton `s`: evaluate the tweakable hash under +the tweak assigned to `s.depth`. -/ +def levelHash (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) (tweakAt : ℕ → Tweak) + (s : Skeleton) (l r : Y) : Y := + th.eval pk (tweakAt s.depth) (l, r) + +/-- Build the tweaked Merkle tree: each internal node rooting a subtree of skeleton `s` +hashes its children's roots under the tweak `tweakAt s.depth`. -/ +def buildMerkleTreeTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) : {s : Skeleton} → LeafData Y s → FullData Y s + | .leaf, .leaf v => .leaf v + | .internal sl sr, .internal l r => + let leftTree := buildMerkleTreeTweaked th pk tweakAt l + let rightTree := buildMerkleTreeTweaked th pk tweakAt r + .internal + (levelHash th pk tweakAt (.internal sl sr) leftTree.getRootValue rightTree.getRootValue) + leftTree rightTree + +/-- Recompute the putative root from a leaf value and an authentication path, hashing each +level under its own tweak. Tweaked analogue of `getPutativeRootWithHash`. -/ +def getPutativeRootTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) : {s : Skeleton} → (idx : SkeletonLeafIndex s) → (leafValue : Y) → + List.Vector Y idx.depth → Y + | .leaf, .ofLeaf, leafValue, _ => leafValue + | .internal sl sr, .ofLeft idxLeft, leafValue, proof => + levelHash th pk tweakAt (.internal sl sr) + (getPutativeRootTweaked th pk tweakAt idxLeft leafValue proof.tail) proof.head + | .internal sl sr, .ofRight idxRight, leafValue, proof => + levelHash th pk tweakAt (.internal sl sr) + proof.head (getPutativeRootTweaked th pk tweakAt idxRight leafValue proof.tail) + +/-- Completeness of tweaked Merkle paths: the honest path (generated by the untweaked +`generateProof`, which only reads cached values) recomputes the root of the honestly built +tweaked tree. -/ +theorem tweaked_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} + (idx : SkeletonLeafIndex s) (leaves : LeafData Y s) : + getPutativeRootTweaked th pk tweakAt idx (leaves.get idx) + (generateProof (buildMerkleTreeTweaked th pk tweakAt leaves) idx) + = (buildMerkleTreeTweaked th pk tweakAt leaves).getRootValue := by + induction idx with + | ofLeaf => + cases leaves with + | leaf a => rfl + | ofLeft idxLeft ih => + cases leaves with + | internal l r => + simp only [buildMerkleTreeTweaked, generateProof, getPutativeRootTweaked, + FullData.leftSubtree_internal, FullData.rightSubtree_internal, + List.Vector.head_cons, LeafData.get_internal_ofLeft, + FullData.internal_getRootValue] + exact congrArg₂ (fun a b => levelHash th pk tweakAt _ a b) (ih l) rfl + | ofRight idxRight ih => + cases leaves with + | internal l r => + simp only [buildMerkleTreeTweaked, generateProof, getPutativeRootTweaked, + FullData.leftSubtree_internal, FullData.rightSubtree_internal, + List.Vector.head_cons, LeafData.get_internal_ofRight, + FullData.internal_getRootValue] + exact congrArg₂ (fun a b => levelHash th pk tweakAt _ a b) rfl (ih r) + +/-- A tweak-tagged collision: two distinct input pairs with the same digest under the *same* +tweak. This is the win-condition shape of the target-collision experiments in +`HardnessAssumptions.MultiTarget`. -/ +def TweakedCollision (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (t : Tweak) (p₁ p₂ : Y × Y) : Prop := + p₁ ≠ p₂ ∧ th.eval pk t p₁ = th.eval pk t p₂ + +variable [DecidableEq Y] + +/-- Walk two tweaked Merkle branches with the same leaf index, looking for a tweak-tagged +hash collision. Tweaked analogue of `InductiveMerkleTree.findCollision`; the returned tweak +identifies the level (and hence the SM-TCR target) at which the collision occurs. -/ +def findCollisionTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) : {s : Skeleton} → (idx : SkeletonLeafIndex s) → + (proof₁ proof₂ : List.Vector Y idx.depth) → (x y : Y) → Option (Tweak × (Y × Y) × (Y × Y)) + | .leaf, .ofLeaf, _, _, _, _ => none + | .internal sl sr, .ofLeft idxLeft, proof₁, proof₂, x, y => + let subL1 := getPutativeRootTweaked th pk tweakAt idxLeft x proof₁.tail + let subL2 := getPutativeRootTweaked th pk tweakAt idxLeft y proof₂.tail + if (subL1, proof₁.head) = (subL2, proof₂.head) then + findCollisionTweaked th pk tweakAt idxLeft proof₁.tail proof₂.tail x y + else if th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (subL1, proof₁.head) + = th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (subL2, proof₂.head) then + some (tweakAt (Skeleton.internal sl sr).depth, (subL1, proof₁.head), (subL2, proof₂.head)) + else + none + | .internal sl sr, .ofRight idxRight, proof₁, proof₂, x, y => + let subR1 := getPutativeRootTweaked th pk tweakAt idxRight x proof₁.tail + let subR2 := getPutativeRootTweaked th pk tweakAt idxRight y proof₂.tail + if (proof₁.head, subR1) = (proof₂.head, subR2) then + findCollisionTweaked th pk tweakAt idxRight proof₁.tail proof₂.tail x y + else if th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (proof₁.head, subR1) + = th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (proof₂.head, subR2) then + some (tweakAt (Skeleton.internal sl sr).depth, (proof₁.head, subR1), (proof₂.head, subR2)) + else + none + +/-- Soundness: a tuple returned by `findCollisionTweaked` is a genuine tweak-tagged +collision. -/ +theorem findCollisionTweaked_sound (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) (t : Tweak) (p₁ p₂ : Y × Y) + (hfind : findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂)) : + TweakedCollision th pk t p₁ p₂ := by + induction idx generalizing x y t p₁ p₂ with + | ofLeaf => + simp [findCollisionTweaked] at hfind + | ofLeft idxLeft ih => + simp only [findCollisionTweaked] at hfind + split at hfind + · exact ih proof₁.tail proof₂.tail x y t p₁ p₂ hfind + · split at hfind + · rename_i hpair heqhash + simp only [Option.some.injEq, Prod.mk.injEq] at hfind + obtain ⟨ht, hp₁, hp₂⟩ := hfind + subst ht hp₁ hp₂ + exact ⟨hpair, heqhash⟩ + · simp at hfind + | ofRight idxRight ih => + simp only [findCollisionTweaked] at hfind + split at hfind + · exact ih proof₁.tail proof₂.tail x y t p₁ p₂ hfind + · split at hfind + · rename_i hpair heqhash + simp only [Option.some.injEq, Prod.mk.injEq] at hfind + obtain ⟨ht, hp₁, hp₂⟩ := hfind + subst ht hp₁ hp₂ + exact ⟨hpair, heqhash⟩ + · simp at hfind + +/-- Binding for tweaked Merkle paths: two distinct leaf values verifying to the same root at +the same leaf index (under possibly different paths) yield a tweak-tagged collision, found +by `findCollisionTweaked`. -/ +theorem getPutativeRootTweaked_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) + (hne : x ≠ y) + (heq : getPutativeRootTweaked th pk tweakAt idx x proof₁ + = getPutativeRootTweaked th pk tweakAt idx y proof₂) : + ∃ t p₁ p₂, findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂) := by + induction idx generalizing x y with + | ofLeaf => + simp only [getPutativeRootTweaked] at heq + exact absurd heq hne + | ofLeft idxLeft ih => + simp only [getPutativeRootTweaked, levelHash] at heq + by_cases hpair : + (getPutativeRootTweaked th pk tweakAt idxLeft x proof₁.tail, proof₁.head) = + (getPutativeRootTweaked th pk tweakAt idxLeft y proof₂.tail, proof₂.head) + · obtain ⟨t, p₁, p₂, hrec⟩ := + ih proof₁.tail proof₂.tail x y hne (congrArg Prod.fst hpair) + exact ⟨t, p₁, p₂, by simp only [findCollisionTweaked, if_pos hpair]; exact hrec⟩ + · exact ⟨_, _, _, by simp only [findCollisionTweaked, if_neg hpair, if_pos heq]; rfl⟩ + | ofRight idxRight ih => + simp only [getPutativeRootTweaked, levelHash] at heq + by_cases hpair : + (proof₁.head, getPutativeRootTweaked th pk tweakAt idxRight x proof₁.tail) = + (proof₂.head, getPutativeRootTweaked th pk tweakAt idxRight y proof₂.tail) + · obtain ⟨t, p₁, p₂, hrec⟩ := + ih proof₁.tail proof₂.tail x y hne (congrArg Prod.snd hpair) + exact ⟨t, p₁, p₂, by simp only [findCollisionTweaked, if_pos hpair]; exact hrec⟩ + · exact ⟨_, _, _, by simp only [findCollisionTweaked, if_neg hpair, if_pos heq]; rfl⟩ + +/-- The user-facing Collision Lemma for tweaked Merkle paths: the tuple returned by +`findCollisionTweaked` on two equivocating openings is a genuine tweak-tagged collision — +i.e. a target-collision break at the identified level's tweak. -/ +theorem getPutativeRootTweaked_binding_collision (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) + (hne : x ≠ y) + (heq : getPutativeRootTweaked th pk tweakAt idx x proof₁ + = getPutativeRootTweaked th pk tweakAt idx y proof₂) : + ∃ t p₁ p₂, + findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂) + ∧ TweakedCollision th pk t p₁ p₂ := by + obtain ⟨t, p₁, p₂, hfind⟩ := + getPutativeRootTweaked_binding th pk tweakAt idx proof₁ proof₂ x y hne heq + exact ⟨t, p₁, p₂, hfind, + findCollisionTweaked_sound th pk tweakAt idx proof₁ proof₂ x y t p₁ p₂ hfind⟩ + +end TweakedMerkleTree From 6e1d312eb639ea68382c173b0287dbcf1a77409a Mon Sep 17 00:00:00 2001 From: Richard Goodman Date: Sun, 12 Jul 2026 09:04:38 -0400 Subject: [PATCH 2/6] docs(MerkleTree/Tweaked): rescope as a level-separated same-tweak collision kernel per review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - module doc: explicit scope-and-limitations block — this is NOT the XMSS/SLH-DSA layout (tweakAt : Nat -> Tweak cannot distinguish same-depth nodes); the node-addressed engine over the inductive tree is named as the tracked follow-up architecture - the binding kernel is documented as a symmetric same-tweak collision, not an SM-TCR win; the oriented (target-fixed) reduction and the multi-target TCR game audit are named as future work; MultiTarget.TcrProblem de-wired - rebased onto current main (post-#477) --- .../MerkleTree/Tweaked/Basic.lean | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean index acd9c38d8..524312edb 100644 --- a/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean +++ b/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean @@ -12,10 +12,21 @@ import VCVio.CryptoFoundations.TweakableHash Merkle trees whose node hash is a *tweakable* hash (`TweakableHash`), with the tweak varying by level: the internal node rooting a subtree of skeleton `s` hashes its children under the -tweak `tweakAt s.depth`. This is the tree layout used by hash-based signature schemes in the -XMSS family (including the SLH-DSA / SPHINCS+ functions `H` and the lean-Ethereum leanSig -proposal), where domain separation by level is what enables *target*-collision-resistance -assumptions in place of full collision resistance. +tweak `tweakAt s.depth`. This provides per-**level** domain separation only. + +**Scope and limitations (read first).** + +* This is a *level-separated* Merkle tree, **not** the XMSS / SLH-DSA layout: those schemes + tweak by full node *address* (layer, tree, horizontal index, domain tag), and + `tweakAt : ℕ → Tweak` cannot distinguish two nodes at the same depth, whatever `Tweak` is. + The right generalization is the inductive engine over a node-addressed hash + (`nodeHash : NodeAddress s → Y → Y → Y`) with this module as its level-indexed instance; + that engine is tracked as a follow-up. +* The binding kernel below returns a **symmetric same-tweak collision** as data. This is + *not by itself* a target-collision-resistance break: TCR is directional (one endpoint must + be fixed at target-generation time, before the adversary answers). The oriented reduction + — an honestly built tree/path fixed in a commitment phase against a later adversarial + opening — is future work, as is the audit of the multi-target TCR game it should land in. Contents: @@ -23,13 +34,13 @@ Contents: recomputation from a leaf, an authentication path, and a leaf index, hashing each level under its own tweak. `generateProof` from the untweaked development is reused unchanged. * `tweaked_functional_completeness` — honestly generated paths verify. -* `TweakedCollision` and `findCollisionTweaked` — the constructive binding kernel. A - disagreement between two verifying openings is traced down the two paths and returned as a - *tweak-tagged* collision: two distinct input pairs with the same digest **under the same - tweak**. This is exactly the win condition shape of the target-collision experiments in - `VCVio.CryptoFoundations.HardnessAssumptions.MultiTarget` (SM-TCR), so binding for the - tweaked tree needs only tweak-wise target collision resistance, not full collision - resistance of a single function. +* `TweakedCollision` and `findCollisionTweaked` — the constructive same-tweak collision + kernel. A disagreement between two verifying openings is traced down the two paths and + returned as a *tweak-tagged* collision: two distinct input pairs with the same digest + **under the same tweak**. The tag localizes the collision to a single level's hash, which + is the raw material a (future, oriented) per-level target-collision reduction will + consume; see the scope note above for why this symmetric statement is deliberately not + phrased as a TCR win. * `getPutativeRootTweaked_binding_collision` — the user-facing binding statement: distinct leaf values verifying to the same root at the same index yield a `TweakedCollision`, as data. @@ -123,7 +134,7 @@ variable [DecidableEq Y] /-- Walk two tweaked Merkle branches with the same leaf index, looking for a tweak-tagged hash collision. Tweaked analogue of `InductiveMerkleTree.findCollision`; the returned tweak -identifies the level (and hence the SM-TCR target) at which the collision occurs. -/ +identifies the level at which the collision occurs. -/ def findCollisionTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) (tweakAt : ℕ → Tweak) : {s : Skeleton} → (idx : SkeletonLeafIndex s) → (proof₁ proof₂ : List.Vector Y idx.depth) → (x y : Y) → Option (Tweak × (Y × Y) × (Y × Y)) From 296ed8def8fe19e33d9b477ac155cb120f8a5c00 Mon Sep 17 00:00:00 2001 From: Richard Goodman Date: Sun, 12 Jul 2026 09:25:06 -0400 Subject: [PATCH 3/6] =?UTF-8?q?feat(MerkleTree):=20node-addressed=20Merkle?= =?UTF-8?q?=20engine=20=E2=80=94=20one=20engine,=20three=20trees?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the architectural blocker on this PR: tree building, putative-root recomputation, completeness, and constructive collision tracing are now defined and proven ONCE over nodeHash : NodeAddress s -> Y -> Y -> Y, with the address threaded by reindexing (nh ∘ .inL / .inR) at each descent. - NodeAddress: typed root-path addresses of internal nodes (full XMSS-style addressing data; subtreeDepth recovers level separation) - addressed_functional_completeness: honest paths verify, for EVERY nodeHash (non-vacuity: not closed by rfl; mutation witness: the child-swapped verifier is refuted on a concrete instance) - findCollisionAddressed(_sound/_isSome) + binding corollary: collisions as data, tagged with the ADDRESS at which they occur — the raw material for the oriented per-address target-collision reduction (follow-up, per review) - Instances: constant nodeHash provably recovers the unaddressed engine (getPutativeRootAddressed_const, populateUpAddressed_const); levelNodeHash (= the Tweaked discipline, via subtreeDepth) factors through addressedNodeHash (levelNodeHash_eq_addressed) Next on this PR per review: re-derive Tweaked/Basic as the level instance, and the sampled-target (SM-rTCR) game + oriented reduction. --- VCVio.lean | 1 + .../MerkleTree/Addressed/Basic.lean | 323 ++++++++++++++++++ 2 files changed, 324 insertions(+) create mode 100644 VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean diff --git a/VCVio.lean b/VCVio.lean index 44df43f70..3672bb816 100644 --- a/VCVio.lean +++ b/VCVio.lean @@ -55,6 +55,7 @@ import VCVio.CryptoFoundations.MerkleTree.Inductive.Defs import VCVio.CryptoFoundations.MerkleTree.Inductive.Extractability import VCVio.CryptoFoundations.MerkleTree.Inductive.QueryBound import VCVio.CryptoFoundations.MerkleTree.Inductive.Uniqueness +import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic import VCVio.CryptoFoundations.MerkleTree.Tweaked.Basic import VCVio.CryptoFoundations.MerkleTree.Vector.Completeness import VCVio.CryptoFoundations.MerkleTree.Vector.Defs diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean new file mode 100644 index 000000000..d5c95d85a --- /dev/null +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean @@ -0,0 +1,323 @@ +/- +Copyright (c) 2026 VCVio Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Richard Goodman +-/ + +import VCVio.CryptoFoundations.MerkleTree.Inductive.Binding +import VCVio.CryptoFoundations.TweakableHash + +/-! # Node-Addressed Merkle Trees: the one engine + +Merkle trees whose node hash may depend on the **full address** of the node being +hashed — the typed root-path position `NodeAddress s` — via +`nodeHash : NodeAddress s → α → α → α`. + +This is the single engine of which the ordinary tree (constant `nodeHash`), the +level-separated tree (`nodeHash` through the depth of the addressed subtree), and +XMSS/SLH-DSA-style fully-addressed trees (`nodeHash` through an arbitrary +address-to-tweak map) are instances: tree building, putative-root recomputation, +completeness, and constructive collision tracing are defined and proven **once**, +and every instance inherits them by specializing `nodeHash`. + +Design: at each recursion step into a child, the engine passes the *reindexed* hash +`fun a => nodeHash (.inL a)` (resp. `.inR`) — the address is threaded by +precomposition, so no explicit path accumulator or embedding parameter appears. + +Contents: + +* `NodeAddress` — typed addresses of **internal** nodes (only internal nodes hash); + `NodeAddress.subtreeDepth` recovers the height of the addressed subtree (the + level-separation data), and the full constructor path is the XMSS address. +* `populateUpAddressed` / `buildMerkleTreeAddressedWithHash` — cache construction. +* `getPutativeRootAddressedWithHash` — putative-root recomputation from a leaf, an + authentication path (`generateProof` is reused unchanged — proofs carry no + addresses), and a leaf index. +* `addressed_functional_completeness` — honest paths verify, for **every** `nodeHash`. +* `AddressedCollision`, `findCollisionAddressed`, `findCollisionAddressed_sound` — + the constructive collision kernel, returning the collision **as data, tagged with + the address** at which it occurs: two distinct pairs with equal hash *under that + address's hash function*. +* `getPutativeRootAddressedWithHash_binding_collision` — the user-facing binding + statement: distinct leaf values verifying to the same root at the same index yield + an address-tagged collision. + +The symmetric collision statement here is deliberately **not** phrased as a +target-collision-resistance win: TCR is directional (one endpoint fixed at +target-registration time). The oriented reduction against a sampled-target game is +the follow-up consumer of the address tag. +-/ + +namespace AddressedMerkleTree + +open List OracleSpec OracleComp BinaryTree InductiveMerkleTree + +variable {α : Type _} [DecidableEq α] + +/-- A typed address of an **internal** node of a skeleton: the path from the root. +Leaf skeletons have no addresses — only internal nodes hash. -/ +inductive NodeAddress : Skeleton → Type + /-- The root of an internal skeleton. -/ + | here {l r : Skeleton} : NodeAddress (.internal l r) + /-- An address inside the left child. -/ + | inL {l r : Skeleton} (a : NodeAddress l) : NodeAddress (.internal l r) + /-- An address inside the right child. -/ + | inR {l r : Skeleton} (a : NodeAddress r) : NodeAddress (.internal l r) + deriving DecidableEq + +namespace NodeAddress + +/-- Distance of the addressed node from the root. -/ +@[simp] +def pathDepth : {s : Skeleton} → NodeAddress s → ℕ + | _, .here => 0 + | _, .inL a => a.pathDepth + 1 + | _, .inR a => a.pathDepth + 1 + +/-- The height (`Skeleton.depth`) of the subtree rooted at the addressed node. +This is the datum a *level-separated* hash depends on. -/ +@[simp] +def subtreeDepth : {s : Skeleton} → NodeAddress s → ℕ + | .internal l r, .here => (Skeleton.internal l r).depth + | _, .inL a => a.subtreeDepth + | _, .inR a => a.subtreeDepth + +end NodeAddress + +/-- Build the full cache of a Merkle tree under an address-dependent hash: each +internal node stores `nodeHash addr leftRoot rightRoot` where `addr` is that node's +address. The address is threaded by reindexing `nodeHash` along `.inL` / `.inR`. -/ +@[simp, grind] +def populateUpAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) → + LeafData α s → FullData α s + | .leaf, _, .leaf v => .leaf v + | .internal _ _, nh, .internal dl dr => + let L := populateUpAddressed (fun a => nh (.inL a)) dl + let R := populateUpAddressed (fun a => nh (.inR a)) dr + .internal (nh .here L.getRootValue R.getRootValue) L R + +/-- Alias matching the naming of the unaddressed engine. -/ +@[simp, grind] +def buildMerkleTreeAddressedWithHash {s : Skeleton} (leaf_tree : LeafData α s) + (nodeHash : NodeAddress s → α → α → α) : FullData α s := + populateUpAddressed nodeHash leaf_tree + +/-- Recompute the putative root from a leaf value, its index, and an authentication +path, hashing each step under the address of the node being reconstituted. The +node reconstituted by the *last* step is the root (`.here`); descending into the +index reindexes the hash along the path. -/ +@[simp, grind] +def getPutativeRootAddressedWithHash : + {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) → + (idx : SkeletonLeafIndex s) → (leafValue : α) → List.Vector α idx.depth → α + | _, _, .ofLeaf, leafValue, _ => leafValue + | _, nh, .ofLeft idxLeft, leafValue, proof => + nh .here (getPutativeRootAddressedWithHash (fun a => nh (.inL a)) idxLeft + leafValue proof.tail) proof.head + | _, nh, .ofRight idxRight, leafValue, proof => + nh .here proof.head (getPutativeRootAddressedWithHash (fun a => nh (.inR a)) idxRight + leafValue proof.tail) + +/-- **Completeness of the engine**: an honestly generated authentication path +recomputes the honest root, for every address-dependent hash. -/ +theorem addressed_functional_completeness {s : Skeleton} + (idx : SkeletonLeafIndex s) (leaf_data_tree : LeafData α s) + (nodeHash : NodeAddress s → α → α → α) : + getPutativeRootAddressedWithHash nodeHash idx (leaf_data_tree.get idx) + (generateProof (buildMerkleTreeAddressedWithHash leaf_data_tree nodeHash) idx) + = (buildMerkleTreeAddressedWithHash leaf_data_tree nodeHash).getRootValue := by + induction idx with + | ofLeaf => cases leaf_data_tree; rfl + | ofLeft idxLeft ih => + cases leaf_data_tree with + | internal dl dr => + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof, + List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, + BinaryTree.FullData.getRootValue] + exact congrArg (fun z => nodeHash .here z _) (ih dl (fun a => nodeHash (.inL a))) + | ofRight idxRight ih => + cases leaf_data_tree with + | internal dl dr => + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof, + List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, + BinaryTree.FullData.getRootValue] + exact congrArg (nodeHash .here _) (ih dr (fun a => nodeHash (.inR a))) + +/-- An address-tagged collision: two *distinct* input pairs with equal digest under +the hash **at that address**. -/ +def AddressedCollision {s : Skeleton} (nodeHash : NodeAddress s → α → α → α) + (w : NodeAddress s × α × α × α × α) : Prop := + (w.2.1, w.2.2.1) ≠ (w.2.2.2.1, w.2.2.2.2) ∧ + nodeHash w.1 w.2.1 w.2.2.1 = nodeHash w.1 w.2.2.2.1 w.2.2.2.2 + +/-- Walk two verifying branches at the same leaf index looking for the level at +which they merge; return the collision **as data, tagged with its address**. -/ +def findCollisionAddressed : {s : Skeleton} → (nodeHash : NodeAddress s → α → α → α) → + (idx : SkeletonLeafIndex s) → (proof₁ proof₂ : List.Vector α idx.depth) → + (x y : α) → Option (NodeAddress s × α × α × α × α) + | _, _, .ofLeaf, _, _, _, _ => none + | _, nh, .ofLeft idxLeft, proof₁, proof₂, x, y => + let subL1 := getPutativeRootAddressedWithHash (fun a => nh (.inL a)) idxLeft x proof₁.tail + let subL2 := getPutativeRootAddressedWithHash (fun a => nh (.inL a)) idxLeft y proof₂.tail + if (subL1, proof₁.head) = (subL2, proof₂.head) then + (findCollisionAddressed (fun a => nh (.inL a)) idxLeft proof₁.tail proof₂.tail x y).map + (fun w => (.inL w.1, w.2)) + else if nh .here subL1 proof₁.head = nh .here subL2 proof₂.head then + some (.here, subL1, proof₁.head, subL2, proof₂.head) + else + none + | _, nh, .ofRight idxRight, proof₁, proof₂, x, y => + let subR1 := getPutativeRootAddressedWithHash (fun a => nh (.inR a)) idxRight x proof₁.tail + let subR2 := getPutativeRootAddressedWithHash (fun a => nh (.inR a)) idxRight y proof₂.tail + if (proof₁.head, subR1) = (proof₂.head, subR2) then + (findCollisionAddressed (fun a => nh (.inR a)) idxRight proof₁.tail proof₂.tail x y).map + (fun w => (.inR w.1, w.2)) + else if nh .here proof₁.head subR1 = nh .here proof₂.head subR2 then + some (.here, proof₁.head, subR1, proof₂.head, subR2) + else + none + +/-- **Soundness of the kernel**: anything returned is an address-tagged collision. -/ +theorem findCollisionAddressed_sound {s : Skeleton} + (nodeHash : NodeAddress s → α → α → α) (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) + (w : NodeAddress s × α × α × α × α) + (hw : findCollisionAddressed nodeHash idx proof₁ proof₂ x y = some w) : + AddressedCollision nodeHash w := by + induction idx with + | ofLeaf => simp [findCollisionAddressed] at hw + | ofLeft idxLeft ih => + rw [findCollisionAddressed] at hw + split at hw + · simp only [Option.map_eq_some_iff] at hw + obtain ⟨w', hw', rfl⟩ := hw + exact ih (fun a => nodeHash (.inL a)) proof₁.tail proof₂.tail w' hw' + · rename_i hneq + split at hw + · rename_i heq + simp only [Option.some.injEq] at hw + subst hw + exact ⟨hneq, heq⟩ + · simp at hw + | ofRight idxRight ih => + rw [findCollisionAddressed] at hw + split at hw + · simp only [Option.map_eq_some_iff] at hw + obtain ⟨w', hw', rfl⟩ := hw + exact ih (fun a => nodeHash (.inR a)) proof₁.tail proof₂.tail w' hw' + · rename_i hneq + split at hw + · rename_i heq + simp only [Option.some.injEq] at hw + subst hw + exact ⟨hneq, heq⟩ + · simp at hw + +/-- If two openings at the same index recompute the same root but the branches differ +somewhere (in leaf value or path), `findCollisionAddressed` finds a collision: the +walk only returns `none` when the two branches agree at every compared level, which +forces the leaf values to agree. -/ +theorem findCollisionAddressed_isSome {s : Skeleton} + (nodeHash : NodeAddress s → α → α → α) (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) + (hroot : getPutativeRootAddressedWithHash nodeHash idx x proof₁ + = getPutativeRootAddressedWithHash nodeHash idx y proof₂) + (hne : x ≠ y) : + (findCollisionAddressed nodeHash idx proof₁ proof₂ x y).isSome := by + induction idx with + | ofLeaf => simp [getPutativeRootAddressedWithHash] at hroot; exact absurd hroot hne + | ofLeft idxLeft ih => + rw [findCollisionAddressed] + split + · rename_i hagree + simp only [Prod.mk.injEq] at hagree + simp only [Option.isSome_map] + exact ih (fun a => nodeHash (.inL a)) proof₁.tail proof₂.tail hagree.1 + · split + · simp + · rename_i hne' + exact absurd (by simpa [getPutativeRootAddressedWithHash] using hroot) hne' + | ofRight idxRight ih => + rw [findCollisionAddressed] + split + · rename_i hagree + simp only [Prod.mk.injEq] at hagree + simp only [Option.isSome_map] + exact ih (fun a => nodeHash (.inR a)) proof₁.tail proof₂.tail hagree.2 + · split + · simp + · rename_i hne' + exact absurd (by simpa [getPutativeRootAddressedWithHash] using hroot) hne' + +/-- **Binding, user-facing**: two openings of the same index recomputing the same +root with distinct leaf values yield an address-tagged collision, as data. -/ +theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton} + (nodeHash : NodeAddress s → α → α → α) (idx : SkeletonLeafIndex s) + (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) + (hroot : getPutativeRootAddressedWithHash nodeHash idx x proof₁ + = getPutativeRootAddressedWithHash nodeHash idx y proof₂) + (hne : x ≠ y) : + ∃ w, findCollisionAddressed nodeHash idx proof₁ proof₂ x y = some w ∧ + AddressedCollision nodeHash w := by + obtain ⟨w, hw⟩ := Option.isSome_iff_exists.mp + (findCollisionAddressed_isSome nodeHash idx proof₁ proof₂ x y hroot hne) + exact ⟨w, hw, findCollisionAddressed_sound nodeHash idx proof₁ proof₂ x y w hw⟩ + +/-! ## Instances: one engine, three trees + +The three hash disciplines are specializations of `nodeHash`; the theorems above +specialize with them. The recovery theorems below are the dedup certificates: the +unaddressed engine's core functions are *definitionally subsumed* (constant +instance), and the level-separated (`Tweaked`) development factors through +`NodeAddress.subtreeDepth`. -/ + +section Instances + +/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed +putative-root computation. -/ +theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton} + (idx : SkeletonLeafIndex s) (x : α) (proof : List.Vector α idx.depth) : + getPutativeRootAddressedWithHash (s := s) (fun _ => h) idx x proof + = InductiveMerkleTree.getPutativeRootWithHash idx x proof h := by + induction idx with + | ofLeaf => rfl + | ofLeft idxLeft ih => simp [getPutativeRootAddressedWithHash, ih] + | ofRight idxRight ih => simp [getPutativeRootAddressedWithHash, ih] + +/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed cache +construction. -/ +theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton} + (ld : LeafData α s) : + populateUpAddressed (fun _ => h) ld = BinaryTree.populateUp ld h := by + induction ld with + | leaf v => rfl + | internal dl dr ihl ihr => simp [populateUpAddressed, BinaryTree.populateUp, ihl, ihr] + +/-- **Level-separated instance**: hash through the depth of the addressed subtree. +This is the discipline of the `Tweaked` development: per-level domain separation. -/ +def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} : NodeAddress s → Y → Y → Y := + fun a l r => th.eval pk (tweakAt a.subtreeDepth) (l, r) + +/-- **Fully-addressed (XMSS-style) instance**: hash through an arbitrary map out of +the full typed address — per-node domain separation. Any concrete addressing scheme +(layer, horizontal index, domain tag) factors through `tweakOf`; nothing about the +address is discarded before the user's map is applied. -/ +def addressedNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) {s : Skeleton} (tweakOf : NodeAddress s → Tweak) : + NodeAddress s → Y → Y → Y := + fun a l r => th.eval pk (tweakOf a) (l, r) + +/-- The level instance factors through the fully-addressed one — level separation is +the special case `tweakOf = tweakAt ∘ subtreeDepth`. -/ +theorem levelNodeHash_eq_addressed {PkSeed Tweak Y : Type} + (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) (tweakAt : ℕ → Tweak) + {s : Skeleton} : + levelNodeHash th pk tweakAt (s := s) + = addressedNodeHash th pk (fun a => tweakAt a.subtreeDepth) := rfl + +end Instances + +end AddressedMerkleTree From 03b7572bcf70c252bb3ad74784deb16433085995 Mon Sep 17 00:00:00 2001 From: Richard Goodman Date: Sun, 12 Jul 2026 09:35:13 -0400 Subject: [PATCH 4/6] feat(MerkleTree): oriented binding for the addressed engine; Tweaked module re-derived as the level instance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves the remaining review blockers on this PR: - findCollisionAddressed_oriented / addressed_oriented_binding: against an HONESTLY BUILT tree, an adversarial opening that verifies with a different leaf yields a collision whose FIRST endpoint is the honestly-precommitted child pair stored in the cache at the tagged address — a value fixed at build (commitment) time, before any adversarial opening exists. This is the directional (target-oriented) content the review required, exposed as data; the probabilistic game packaging consumes it separately. - Tweaked/Basic.lean is REMOVED. Its honest content is re-derived in Addressed/Level.lean as the depth-collapsed instance of the engine (buildMerkleTreeLevel/getPutativeRootLevel; level_functional_completeness and level_oriented_binding are the engine theorems at levelNodeHash) — no duplicated construction or proof remains, and no XMSS/SM-TCR claim is made anywhere. - No theorem is wired to MultiTarget.TcrProblem; per review, that game needs a sampled-randomness repair (SM-rTCR, eprint 2025/055 Def 6) before anything should reduce to it. --- VCVio.lean | 2 +- .../MerkleTree/Addressed/Basic.lean | 158 +++++++++++ .../MerkleTree/Addressed/Level.lean | 69 +++++ .../MerkleTree/Tweaked/Basic.lean | 246 ------------------ 4 files changed, 228 insertions(+), 247 deletions(-) create mode 100644 VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean delete mode 100644 VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean diff --git a/VCVio.lean b/VCVio.lean index 3672bb816..14f3435d5 100644 --- a/VCVio.lean +++ b/VCVio.lean @@ -56,7 +56,7 @@ import VCVio.CryptoFoundations.MerkleTree.Inductive.Extractability import VCVio.CryptoFoundations.MerkleTree.Inductive.QueryBound import VCVio.CryptoFoundations.MerkleTree.Inductive.Uniqueness import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic -import VCVio.CryptoFoundations.MerkleTree.Tweaked.Basic +import VCVio.CryptoFoundations.MerkleTree.Addressed.Level import VCVio.CryptoFoundations.MerkleTree.Vector.Completeness import VCVio.CryptoFoundations.MerkleTree.Vector.Defs import VCVio.CryptoFoundations.PRF diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean index d5c95d85a..687644e7d 100644 --- a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean @@ -265,6 +265,164 @@ theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton} (findCollisionAddressed_isSome nodeHash idx proof₁ proof₂ x y hroot hne) exact ⟨w, hw, findCollisionAddressed_sound nodeHash idx proof₁ proof₂ x y w hw⟩ +/-! ## Target orientation + +`findCollisionAddressed` is symmetric in its two openings. The theorems below break +the symmetry for the honest-vs-adversarial configuration: when the first opening is +the **honest** one (leaf and path generated from a built cache), the first endpoint +of the returned collision is exactly the pair of child roots **stored in the cache at +the returned address** — a value fixed by the (commitment-time) build, before any +adversarial opening exists. This is the *directional* content a target-collision +reduction needs, exposed as data; the probabilistic game packaging is deliberately +kept separate. -/ + +/-- The pair of child root values stored at an internal address of a cache. These +are the honestly-precommitted hash inputs at that node. -/ +@[simp] +def childPairAt : {s : Skeleton} → FullData α s → NodeAddress s → α × α + | _, .internal _ L R, .here => (L.getRootValue, R.getRootValue) + | _, .internal _ L R, .inL a => childPairAt L a + | _, .internal _ L R, .inR a => childPairAt R a + +/-- **Orientation**: against an honest first opening, the collision's first endpoint +is the precommitted child pair at the returned address. -/ +theorem findCollisionAddressed_oriented {s : Skeleton} + (nodeHash : NodeAddress s → α → α → α) (ld : LeafData α s) + (idx : SkeletonLeafIndex s) (y : α) (proof₂ : List.Vector α idx.depth) + (hroot : getPutativeRootAddressedWithHash nodeHash idx y proof₂ + = (buildMerkleTreeAddressedWithHash ld nodeHash).getRootValue) + (hne : ld.get idx ≠ y) : + ∃ (a : NodeAddress s) (c : α × α), + findCollisionAddressed nodeHash idx + (InductiveMerkleTree.generateProof + (buildMerkleTreeAddressedWithHash ld nodeHash) idx) proof₂ + (ld.get idx) y + = some (a, (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).1, + (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).2, + c.1, c.2) := by + induction idx with + | ofLeaf => + cases ld with + | leaf v => + simp only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash, + populateUpAddressed, FullData.getRootValue_leaf] at hroot + exact absurd hroot.symm (by simpa using hne) + | ofLeft idxLeft ih => + cases ld with + | internal dl dr => + have hsub : getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) idxLeft + (dl.get idxLeft) + (InductiveMerkleTree.generateProof + (populateUpAddressed (fun a => nodeHash (.inL a)) dl) idxLeft) + = (populateUpAddressed (fun a => nodeHash (.inL a)) dl).getRootValue := + addressed_functional_completeness idxLeft dl (fun a => nodeHash (.inL a)) + have hroot' : nodeHash .here + (getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) idxLeft y + proof₂.tail) proof₂.head + = nodeHash .here + (populateUpAddressed (fun a => nodeHash (.inL a)) dl).getRootValue + (populateUpAddressed (fun a => nodeHash (.inR a)) dr).getRootValue := by + simpa only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash, + populateUpAddressed, FullData.internal_getRootValue] using hroot + rw [findCollisionAddressed] + split + · rename_i hagree + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree + obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.inL a)) dl proof₂.tail + (show getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) idxLeft y + proof₂.tail + = (buildMerkleTreeAddressedWithHash dl (fun a => nodeHash (.inL a))).getRootValue + from hagree.1.symm) + (by simpa using hne) + refine ⟨.inL a', c, ?_⟩ + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, + BinaryTree.LeafData.get] at hwalk ⊢ + rw [hwalk] + simp [childPairAt] + · split + · refine ⟨.here, (getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) + idxLeft y proof₂.tail, proof₂.head), ?_⟩ + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, childPairAt, Option.some.injEq] + · rename_i hne2 + refine absurd ?_ hne2 + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub] + exact hroot'.symm + | ofRight idxRight ih => + cases ld with + | internal dl dr => + have hsub : getPutativeRootAddressedWithHash (fun a => nodeHash (.inR a)) idxRight + (dr.get idxRight) + (InductiveMerkleTree.generateProof + (populateUpAddressed (fun a => nodeHash (.inR a)) dr) idxRight) + = (populateUpAddressed (fun a => nodeHash (.inR a)) dr).getRootValue := + addressed_functional_completeness idxRight dr (fun a => nodeHash (.inR a)) + have hroot' : nodeHash .here proof₂.head + (getPutativeRootAddressedWithHash (fun a => nodeHash (.inR a)) idxRight y + proof₂.tail) + = nodeHash .here + (populateUpAddressed (fun a => nodeHash (.inL a)) dl).getRootValue + (populateUpAddressed (fun a => nodeHash (.inR a)) dr).getRootValue := by + simpa only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash, + populateUpAddressed, FullData.internal_getRootValue] using hroot + rw [findCollisionAddressed] + split + · rename_i hagree + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree + obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.inR a)) dr proof₂.tail + (show getPutativeRootAddressedWithHash (fun a => nodeHash (.inR a)) idxRight y + proof₂.tail + = (buildMerkleTreeAddressedWithHash dr (fun a => nodeHash (.inR a))).getRootValue + from hagree.2.symm) + (by simpa using hne) + refine ⟨.inR a', c, ?_⟩ + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, + BinaryTree.LeafData.get] at hwalk ⊢ + rw [hwalk] + simp [childPairAt] + · split + · refine ⟨.here, (proof₂.head, getPutativeRootAddressedWithHash + (fun a => nodeHash (.inR a)) idxRight y proof₂.tail), ?_⟩ + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, childPairAt, Option.some.injEq] + · rename_i hne2 + refine absurd ?_ hne2 + simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub] + exact hroot'.symm + +/-- **Oriented binding, user-facing**: an adversarial opening that verifies against an +honestly built root with a different leaf value yields a collision whose first +endpoint is the honestly-precommitted child pair at the tagged address — the +directional configuration a target-collision reduction consumes. -/ +theorem addressed_oriented_binding {s : Skeleton} + (nodeHash : NodeAddress s → α → α → α) (ld : LeafData α s) + (idx : SkeletonLeafIndex s) (y : α) (proof₂ : List.Vector α idx.depth) + (hroot : getPutativeRootAddressedWithHash nodeHash idx y proof₂ + = (buildMerkleTreeAddressedWithHash ld nodeHash).getRootValue) + (hne : ld.get idx ≠ y) : + ∃ (a : NodeAddress s) (c : α × α), + (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a) ≠ c ∧ + nodeHash a (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).1 + (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).2 + = nodeHash a c.1 c.2 := by + obtain ⟨a, c, hwalk⟩ := + findCollisionAddressed_oriented nodeHash ld idx y proof₂ hroot hne + have hcol := findCollisionAddressed_sound nodeHash idx _ proof₂ (ld.get idx) y _ hwalk + exact ⟨a, c, by simpa [AddressedCollision, Prod.ext_iff] using hcol.1, + by simpa [AddressedCollision] using hcol.2⟩ + /-! ## Instances: one engine, three trees The three hash disciplines are specializations of `nodeHash`; the theorems above diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean new file mode 100644 index 000000000..bafda983c --- /dev/null +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 VCVio Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Richard Goodman +-/ + +import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic + +/-! # Level-Separated Merkle Trees, as an instance of the addressed engine + +Per-**level** domain separation — every node at the same subtree depth hashes under +the same tweak — obtained by specializing the node-addressed engine's `nodeHash` +through `NodeAddress.subtreeDepth`. Nothing here is proven from scratch: building, +completeness, and the (oriented) collision kernel are the engine's theorems at +`levelNodeHash`. + +This is deliberately **not** the XMSS / SLH-DSA layout, which separates by full node +address; that is the engine itself (`addressedNodeHash`), of which this file is the +depth-collapsed special case (`levelNodeHash_eq_addressed`). +-/ + +namespace AddressedMerkleTree + +open BinaryTree InductiveMerkleTree + +variable {PkSeed Tweak Y : Type} [DecidableEq Y] + +/-- Build a level-separated Merkle tree: node at subtree-depth `d` hashes under +`tweakAt d`. -/ +def buildMerkleTreeLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) {s : Skeleton} (ld : LeafData Y s) : FullData Y s := + buildMerkleTreeAddressedWithHash ld (levelNodeHash th pk tweakAt) + +/-- Putative-root recomputation for the level-separated tree. -/ +def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) + (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) (leafValue : Y) + (proof : List.Vector Y idx.depth) : Y := + getPutativeRootAddressedWithHash (levelNodeHash th pk tweakAt) idx leafValue proof + +/-- Completeness for the level-separated tree — the engine's completeness at +`levelNodeHash`. -/ +theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} + (idx : SkeletonLeafIndex s) (ld : LeafData Y s) : + getPutativeRootLevel th pk tweakAt idx (ld.get idx) + (generateProof (buildMerkleTreeLevel th pk tweakAt ld) idx) + = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue := + addressed_functional_completeness idx ld (levelNodeHash th pk tweakAt) + +/-- **Oriented binding** for the level-separated tree — the engine's oriented +binding at `levelNodeHash`: an adversarial opening verifying against an honestly +built root with a different leaf yields two distinct pairs with equal digest under +the tweak of the collision's level, the first pair being the honestly-precommitted +one at the tagged address. -/ +theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y) + (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (ld : LeafData Y s) + (idx : SkeletonLeafIndex s) (y : Y) (proof₂ : List.Vector Y idx.depth) + (hroot : getPutativeRootLevel th pk tweakAt idx y proof₂ + = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue) + (hne : ld.get idx ≠ y) : + ∃ (a : NodeAddress s) (c : Y × Y), + (childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a) ≠ c ∧ + th.eval pk (tweakAt a.subtreeDepth) + ((childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).1, + (childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).2) + = th.eval pk (tweakAt a.subtreeDepth) (c.1, c.2) := + addressed_oriented_binding (levelNodeHash th pk tweakAt) ld idx y proof₂ hroot hne + +end AddressedMerkleTree diff --git a/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean deleted file mode 100644 index 524312edb..000000000 --- a/VCVio/CryptoFoundations/MerkleTree/Tweaked/Basic.lean +++ /dev/null @@ -1,246 +0,0 @@ -/- -Copyright (c) 2026 IAOM / Equation Capital dba Apoth3osis. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Abraxas1010 (IAOM / Apoth3osis) --/ - -import VCVio.CryptoFoundations.MerkleTree.Inductive.Defs -import VCVio.CryptoFoundations.TweakableHash - -/-! -# Tweaked Merkle Authentication Paths - -Merkle trees whose node hash is a *tweakable* hash (`TweakableHash`), with the tweak varying -by level: the internal node rooting a subtree of skeleton `s` hashes its children under the -tweak `tweakAt s.depth`. This provides per-**level** domain separation only. - -**Scope and limitations (read first).** - -* This is a *level-separated* Merkle tree, **not** the XMSS / SLH-DSA layout: those schemes - tweak by full node *address* (layer, tree, horizontal index, domain tag), and - `tweakAt : ℕ → Tweak` cannot distinguish two nodes at the same depth, whatever `Tweak` is. - The right generalization is the inductive engine over a node-addressed hash - (`nodeHash : NodeAddress s → Y → Y → Y`) with this module as its level-indexed instance; - that engine is tracked as a follow-up. -* The binding kernel below returns a **symmetric same-tweak collision** as data. This is - *not by itself* a target-collision-resistance break: TCR is directional (one endpoint must - be fixed at target-generation time, before the adversary answers). The oriented reduction - — an honestly built tree/path fixed in a commitment phase against a later adversarial - opening — is future work, as is the audit of the multi-target TCR game it should land in. - -Contents: - -* `buildMerkleTreeTweaked` / `getPutativeRootTweaked` — tree building and putative-root - recomputation from a leaf, an authentication path, and a leaf index, hashing each level - under its own tweak. `generateProof` from the untweaked development is reused unchanged. -* `tweaked_functional_completeness` — honestly generated paths verify. -* `TweakedCollision` and `findCollisionTweaked` — the constructive same-tweak collision - kernel. A disagreement between two verifying openings is traced down the two paths and - returned as a *tweak-tagged* collision: two distinct input pairs with the same digest - **under the same tweak**. The tag localizes the collision to a single level's hash, which - is the raw material a (future, oriented) per-level target-collision reduction will - consume; see the scope note above for why this symmetric statement is deliberately not - phrased as a TCR win. -* `getPutativeRootTweaked_binding_collision` — the user-facing binding statement: distinct - leaf values verifying to the same root at the same index yield a `TweakedCollision`, - as data. - -The proofs mirror `VCVio.CryptoFoundations.MerkleTree.Inductive.{Completeness, Binding}`, -generalized from a fixed `hashFn : α → α → α` to a level-indexed family. - -## References - -- Hülsing, Rijneveld, Song, Schwabe, "Mitigating Multi-Target Attacks in Hash-Based - Signatures" -- Drake, Khovratovich, Kudinov, Wagner, "Hash-Based Multi-Signatures for Post-Quantum - Ethereum" (leanSig; CiC 2025) --/ - -namespace TweakedMerkleTree - -open BinaryTree InductiveMerkleTree - -variable {PkSeed Tweak Y : Type} - -/-- The node hash at the level of a subtree skeleton `s`: evaluate the tweakable hash under -the tweak assigned to `s.depth`. -/ -def levelHash (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) (tweakAt : ℕ → Tweak) - (s : Skeleton) (l r : Y) : Y := - th.eval pk (tweakAt s.depth) (l, r) - -/-- Build the tweaked Merkle tree: each internal node rooting a subtree of skeleton `s` -hashes its children's roots under the tweak `tweakAt s.depth`. -/ -def buildMerkleTreeTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) - (tweakAt : ℕ → Tweak) : {s : Skeleton} → LeafData Y s → FullData Y s - | .leaf, .leaf v => .leaf v - | .internal sl sr, .internal l r => - let leftTree := buildMerkleTreeTweaked th pk tweakAt l - let rightTree := buildMerkleTreeTweaked th pk tweakAt r - .internal - (levelHash th pk tweakAt (.internal sl sr) leftTree.getRootValue rightTree.getRootValue) - leftTree rightTree - -/-- Recompute the putative root from a leaf value and an authentication path, hashing each -level under its own tweak. Tweaked analogue of `getPutativeRootWithHash`. -/ -def getPutativeRootTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) - (tweakAt : ℕ → Tweak) : {s : Skeleton} → (idx : SkeletonLeafIndex s) → (leafValue : Y) → - List.Vector Y idx.depth → Y - | .leaf, .ofLeaf, leafValue, _ => leafValue - | .internal sl sr, .ofLeft idxLeft, leafValue, proof => - levelHash th pk tweakAt (.internal sl sr) - (getPutativeRootTweaked th pk tweakAt idxLeft leafValue proof.tail) proof.head - | .internal sl sr, .ofRight idxRight, leafValue, proof => - levelHash th pk tweakAt (.internal sl sr) - proof.head (getPutativeRootTweaked th pk tweakAt idxRight leafValue proof.tail) - -/-- Completeness of tweaked Merkle paths: the honest path (generated by the untweaked -`generateProof`, which only reads cached values) recomputes the root of the honestly built -tweaked tree. -/ -theorem tweaked_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y) - (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} - (idx : SkeletonLeafIndex s) (leaves : LeafData Y s) : - getPutativeRootTweaked th pk tweakAt idx (leaves.get idx) - (generateProof (buildMerkleTreeTweaked th pk tweakAt leaves) idx) - = (buildMerkleTreeTweaked th pk tweakAt leaves).getRootValue := by - induction idx with - | ofLeaf => - cases leaves with - | leaf a => rfl - | ofLeft idxLeft ih => - cases leaves with - | internal l r => - simp only [buildMerkleTreeTweaked, generateProof, getPutativeRootTweaked, - FullData.leftSubtree_internal, FullData.rightSubtree_internal, - List.Vector.head_cons, LeafData.get_internal_ofLeft, - FullData.internal_getRootValue] - exact congrArg₂ (fun a b => levelHash th pk tweakAt _ a b) (ih l) rfl - | ofRight idxRight ih => - cases leaves with - | internal l r => - simp only [buildMerkleTreeTweaked, generateProof, getPutativeRootTweaked, - FullData.leftSubtree_internal, FullData.rightSubtree_internal, - List.Vector.head_cons, LeafData.get_internal_ofRight, - FullData.internal_getRootValue] - exact congrArg₂ (fun a b => levelHash th pk tweakAt _ a b) rfl (ih r) - -/-- A tweak-tagged collision: two distinct input pairs with the same digest under the *same* -tweak. This is the win-condition shape of the target-collision experiments in -`HardnessAssumptions.MultiTarget`. -/ -def TweakedCollision (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) - (t : Tweak) (p₁ p₂ : Y × Y) : Prop := - p₁ ≠ p₂ ∧ th.eval pk t p₁ = th.eval pk t p₂ - -variable [DecidableEq Y] - -/-- Walk two tweaked Merkle branches with the same leaf index, looking for a tweak-tagged -hash collision. Tweaked analogue of `InductiveMerkleTree.findCollision`; the returned tweak -identifies the level at which the collision occurs. -/ -def findCollisionTweaked (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) - (tweakAt : ℕ → Tweak) : {s : Skeleton} → (idx : SkeletonLeafIndex s) → - (proof₁ proof₂ : List.Vector Y idx.depth) → (x y : Y) → Option (Tweak × (Y × Y) × (Y × Y)) - | .leaf, .ofLeaf, _, _, _, _ => none - | .internal sl sr, .ofLeft idxLeft, proof₁, proof₂, x, y => - let subL1 := getPutativeRootTweaked th pk tweakAt idxLeft x proof₁.tail - let subL2 := getPutativeRootTweaked th pk tweakAt idxLeft y proof₂.tail - if (subL1, proof₁.head) = (subL2, proof₂.head) then - findCollisionTweaked th pk tweakAt idxLeft proof₁.tail proof₂.tail x y - else if th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (subL1, proof₁.head) - = th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (subL2, proof₂.head) then - some (tweakAt (Skeleton.internal sl sr).depth, (subL1, proof₁.head), (subL2, proof₂.head)) - else - none - | .internal sl sr, .ofRight idxRight, proof₁, proof₂, x, y => - let subR1 := getPutativeRootTweaked th pk tweakAt idxRight x proof₁.tail - let subR2 := getPutativeRootTweaked th pk tweakAt idxRight y proof₂.tail - if (proof₁.head, subR1) = (proof₂.head, subR2) then - findCollisionTweaked th pk tweakAt idxRight proof₁.tail proof₂.tail x y - else if th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (proof₁.head, subR1) - = th.eval pk (tweakAt (Skeleton.internal sl sr).depth) (proof₂.head, subR2) then - some (tweakAt (Skeleton.internal sl sr).depth, (proof₁.head, subR1), (proof₂.head, subR2)) - else - none - -/-- Soundness: a tuple returned by `findCollisionTweaked` is a genuine tweak-tagged -collision. -/ -theorem findCollisionTweaked_sound (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) - (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) - (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) (t : Tweak) (p₁ p₂ : Y × Y) - (hfind : findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂)) : - TweakedCollision th pk t p₁ p₂ := by - induction idx generalizing x y t p₁ p₂ with - | ofLeaf => - simp [findCollisionTweaked] at hfind - | ofLeft idxLeft ih => - simp only [findCollisionTweaked] at hfind - split at hfind - · exact ih proof₁.tail proof₂.tail x y t p₁ p₂ hfind - · split at hfind - · rename_i hpair heqhash - simp only [Option.some.injEq, Prod.mk.injEq] at hfind - obtain ⟨ht, hp₁, hp₂⟩ := hfind - subst ht hp₁ hp₂ - exact ⟨hpair, heqhash⟩ - · simp at hfind - | ofRight idxRight ih => - simp only [findCollisionTweaked] at hfind - split at hfind - · exact ih proof₁.tail proof₂.tail x y t p₁ p₂ hfind - · split at hfind - · rename_i hpair heqhash - simp only [Option.some.injEq, Prod.mk.injEq] at hfind - obtain ⟨ht, hp₁, hp₂⟩ := hfind - subst ht hp₁ hp₂ - exact ⟨hpair, heqhash⟩ - · simp at hfind - -/-- Binding for tweaked Merkle paths: two distinct leaf values verifying to the same root at -the same leaf index (under possibly different paths) yield a tweak-tagged collision, found -by `findCollisionTweaked`. -/ -theorem getPutativeRootTweaked_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y) - (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) - (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) - (hne : x ≠ y) - (heq : getPutativeRootTweaked th pk tweakAt idx x proof₁ - = getPutativeRootTweaked th pk tweakAt idx y proof₂) : - ∃ t p₁ p₂, findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂) := by - induction idx generalizing x y with - | ofLeaf => - simp only [getPutativeRootTweaked] at heq - exact absurd heq hne - | ofLeft idxLeft ih => - simp only [getPutativeRootTweaked, levelHash] at heq - by_cases hpair : - (getPutativeRootTweaked th pk tweakAt idxLeft x proof₁.tail, proof₁.head) = - (getPutativeRootTweaked th pk tweakAt idxLeft y proof₂.tail, proof₂.head) - · obtain ⟨t, p₁, p₂, hrec⟩ := - ih proof₁.tail proof₂.tail x y hne (congrArg Prod.fst hpair) - exact ⟨t, p₁, p₂, by simp only [findCollisionTweaked, if_pos hpair]; exact hrec⟩ - · exact ⟨_, _, _, by simp only [findCollisionTweaked, if_neg hpair, if_pos heq]; rfl⟩ - | ofRight idxRight ih => - simp only [getPutativeRootTweaked, levelHash] at heq - by_cases hpair : - (proof₁.head, getPutativeRootTweaked th pk tweakAt idxRight x proof₁.tail) = - (proof₂.head, getPutativeRootTweaked th pk tweakAt idxRight y proof₂.tail) - · obtain ⟨t, p₁, p₂, hrec⟩ := - ih proof₁.tail proof₂.tail x y hne (congrArg Prod.snd hpair) - exact ⟨t, p₁, p₂, by simp only [findCollisionTweaked, if_pos hpair]; exact hrec⟩ - · exact ⟨_, _, _, by simp only [findCollisionTweaked, if_neg hpair, if_pos heq]; rfl⟩ - -/-- The user-facing Collision Lemma for tweaked Merkle paths: the tuple returned by -`findCollisionTweaked` on two equivocating openings is a genuine tweak-tagged collision — -i.e. a target-collision break at the identified level's tweak. -/ -theorem getPutativeRootTweaked_binding_collision (th : TweakableHash PkSeed Tweak (Y × Y) Y) - (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) - (proof₁ proof₂ : List.Vector Y idx.depth) (x y : Y) - (hne : x ≠ y) - (heq : getPutativeRootTweaked th pk tweakAt idx x proof₁ - = getPutativeRootTweaked th pk tweakAt idx y proof₂) : - ∃ t p₁ p₂, - findCollisionTweaked th pk tweakAt idx proof₁ proof₂ x y = some (t, p₁, p₂) - ∧ TweakedCollision th pk t p₁ p₂ := by - obtain ⟨t, p₁, p₂, hfind⟩ := - getPutativeRootTweaked_binding th pk tweakAt idx proof₁ proof₂ x y hne heq - exact ⟨t, p₁, p₂, hfind, - findCollisionTweaked_sound th pk tweakAt idx proof₁ proof₂ x y t p₁ p₂ hfind⟩ - -end TweakedMerkleTree From 434b90e69d146b70a9ebb6261ffd93a4fd834aef Mon Sep 17 00:00:00 2001 From: Devon Tuma Date: Mon, 27 Jul 2026 15:18:05 -0500 Subject: [PATCH 5/6] chore(MerkleTree): resolve current import and linter failures --- VCVio.lean | 4 +- .../MerkleTree/Addressed/Basic.lean | 47 ++++++++++++------- .../MerkleTree/Addressed/Level.lean | 12 +++-- 3 files changed, 40 insertions(+), 23 deletions(-) diff --git a/VCVio.lean b/VCVio.lean index 14f3435d5..c234d558d 100644 --- a/VCVio.lean +++ b/VCVio.lean @@ -49,14 +49,14 @@ import VCVio.CryptoFoundations.KEMDEM import VCVio.CryptoFoundations.KeyEncapMech import VCVio.CryptoFoundations.MacAlg import VCVio.CryptoFoundations.MacFromPRF +import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic +import VCVio.CryptoFoundations.MerkleTree.Addressed.Level import VCVio.CryptoFoundations.MerkleTree.Inductive.Binding import VCVio.CryptoFoundations.MerkleTree.Inductive.Completeness import VCVio.CryptoFoundations.MerkleTree.Inductive.Defs import VCVio.CryptoFoundations.MerkleTree.Inductive.Extractability import VCVio.CryptoFoundations.MerkleTree.Inductive.QueryBound import VCVio.CryptoFoundations.MerkleTree.Inductive.Uniqueness -import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic -import VCVio.CryptoFoundations.MerkleTree.Addressed.Level import VCVio.CryptoFoundations.MerkleTree.Vector.Completeness import VCVio.CryptoFoundations.MerkleTree.Vector.Defs import VCVio.CryptoFoundations.PRF diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean index 687644e7d..d84b6b2bb 100644 --- a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean @@ -118,6 +118,7 @@ def getPutativeRootAddressedWithHash : nh .here proof.head (getPutativeRootAddressedWithHash (fun a => nh (.inR a)) idxRight leafValue proof.tail) +omit [DecidableEq α] in /-- **Completeness of the engine**: an honestly generated authentication path recomputes the honest root, for every address-dependent hash. -/ theorem addressed_functional_completeness {s : Skeleton} @@ -133,16 +134,14 @@ theorem addressed_functional_completeness {s : Skeleton} | internal dl dr => simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof, - List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, - BinaryTree.FullData.getRootValue] + List.Vector.head_cons, BinaryTree.LeafData.get, BinaryTree.FullData.getRootValue] exact congrArg (fun z => nodeHash .here z _) (ih dl (fun a => nodeHash (.inL a))) | ofRight idxRight ih => cases leaf_data_tree with | internal dl dr => simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof, - List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, - BinaryTree.FullData.getRootValue] + List.Vector.head_cons, BinaryTree.LeafData.get, BinaryTree.FullData.getRootValue] exact congrArg (nodeHash .here _) (ih dr (fun a => nodeHash (.inR a))) /-- An address-tagged collision: two *distinct* input pairs with equal digest under @@ -227,7 +226,9 @@ theorem findCollisionAddressed_isSome {s : Skeleton} (hne : x ≠ y) : (findCollisionAddressed nodeHash idx proof₁ proof₂ x y).isSome := by induction idx with - | ofLeaf => simp [getPutativeRootAddressedWithHash] at hroot; exact absurd hroot hne + | ofLeaf => + simp only [vector_eq_nil] at hroot + exact absurd hroot hne | ofLeft idxLeft ih => rw [findCollisionAddressed] split @@ -281,8 +282,8 @@ are the honestly-precommitted hash inputs at that node. -/ @[simp] def childPairAt : {s : Skeleton} → FullData α s → NodeAddress s → α × α | _, .internal _ L R, .here => (L.getRootValue, R.getRootValue) - | _, .internal _ L R, .inL a => childPairAt L a - | _, .internal _ L R, .inR a => childPairAt R a + | _, .internal _ L _, .inL a => childPairAt L a + | _, .internal _ _ R, .inR a => childPairAt R a /-- **Orientation**: against an honest first opening, the collision's first endpoint is the precommitted child pair at the returned address. -/ @@ -328,7 +329,8 @@ theorem findCollisionAddressed_oriented {s : Skeleton} split · rename_i hagree simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.inL a)) dl proof₂.tail (show getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) idxLeft y @@ -338,7 +340,8 @@ theorem findCollisionAddressed_oriented {s : Skeleton} (by simpa using hne) refine ⟨.inL a', c, ?_⟩ simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, BinaryTree.LeafData.get] at hwalk ⊢ rw [hwalk] simp [childPairAt] @@ -346,12 +349,14 @@ theorem findCollisionAddressed_oriented {s : Skeleton} · refine ⟨.here, (getPutativeRootAddressedWithHash (fun a => nodeHash (.inL a)) idxLeft y proof₂.tail, proof₂.head), ?_⟩ simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, - BinaryTree.LeafData.get, hsub, childPairAt, Option.some.injEq] + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, childPairAt] · rename_i hne2 refine absurd ?_ hne2 simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, hsub] exact hroot'.symm | ofRight idxRight ih => @@ -375,7 +380,8 @@ theorem findCollisionAddressed_oriented {s : Skeleton} split · rename_i hagree simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.inR a)) dr proof₂.tail (show getPutativeRootAddressedWithHash (fun a => nodeHash (.inR a)) idxRight y @@ -385,7 +391,8 @@ theorem findCollisionAddressed_oriented {s : Skeleton} (by simpa using hne) refine ⟨.inR a', c, ?_⟩ simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, BinaryTree.LeafData.get] at hwalk ⊢ rw [hwalk] simp [childPairAt] @@ -393,15 +400,18 @@ theorem findCollisionAddressed_oriented {s : Skeleton} · refine ⟨.here, (proof₂.head, getPutativeRootAddressedWithHash (fun a => nodeHash (.inR a)) idxRight y proof₂.tail), ?_⟩ simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, - BinaryTree.LeafData.get, hsub, childPairAt, Option.some.injEq] + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + BinaryTree.LeafData.get, hsub, childPairAt] · rename_i hne2 refine absurd ?_ hne2 simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed, - InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, + InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree, + SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons, BinaryTree.LeafData.get, hsub] exact hroot'.symm +omit [DecidableEq α] in /-- **Oriented binding, user-facing**: an adversarial opening that verifies against an honestly built root with a different leaf value yields a collision whose first endpoint is the honestly-precommitted child pair at the tagged address — the @@ -417,6 +427,7 @@ theorem addressed_oriented_binding {s : Skeleton} nodeHash a (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).1 (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).2 = nodeHash a c.1 c.2 := by + letI : DecidableEq α := Classical.decEq α obtain ⟨a, c, hwalk⟩ := findCollisionAddressed_oriented nodeHash ld idx y proof₂ hroot hne have hcol := findCollisionAddressed_sound nodeHash idx _ proof₂ (ld.get idx) y _ hwalk @@ -433,6 +444,7 @@ instance), and the level-separated (`Tweaked`) development factors through section Instances +omit [DecidableEq α] in /-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed putative-root computation. -/ theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton} @@ -444,6 +456,7 @@ theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton} | ofLeft idxLeft ih => simp [getPutativeRootAddressedWithHash, ih] | ofRight idxRight ih => simp [getPutativeRootAddressedWithHash, ih] +omit [DecidableEq α] in /-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed cache construction. -/ theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton} diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean index bafda983c..f848c5119 100644 --- a/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean @@ -37,6 +37,7 @@ def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSe (proof : List.Vector Y idx.depth) : Y := getPutativeRootAddressedWithHash (levelNodeHash th pk tweakAt) idx leafValue proof +omit [DecidableEq Y] in /-- Completeness for the level-separated tree — the engine's completeness at `levelNodeHash`. -/ theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y) @@ -44,9 +45,11 @@ theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) (idx : SkeletonLeafIndex s) (ld : LeafData Y s) : getPutativeRootLevel th pk tweakAt idx (ld.get idx) (generateProof (buildMerkleTreeLevel th pk tweakAt ld) idx) - = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue := - addressed_functional_completeness idx ld (levelNodeHash th pk tweakAt) + = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue := by + letI : DecidableEq Y := Classical.decEq Y + exact addressed_functional_completeness idx ld (levelNodeHash th pk tweakAt) +omit [DecidableEq Y] in /-- **Oriented binding** for the level-separated tree — the engine's oriented binding at `levelNodeHash`: an adversarial opening verifying against an honestly built root with a different leaf yields two distinct pairs with equal digest under @@ -63,7 +66,8 @@ theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y) th.eval pk (tweakAt a.subtreeDepth) ((childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).1, (childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).2) - = th.eval pk (tweakAt a.subtreeDepth) (c.1, c.2) := - addressed_oriented_binding (levelNodeHash th pk tweakAt) ld idx y proof₂ hroot hne + = th.eval pk (tweakAt a.subtreeDepth) (c.1, c.2) := by + letI : DecidableEq Y := Classical.decEq Y + exact addressed_oriented_binding (levelNodeHash th pk tweakAt) ld idx y proof₂ hroot hne end AddressedMerkleTree From f24112771aadbc39677fdaf002ec44a72d459a7f Mon Sep 17 00:00:00 2001 From: Richard Goodman Date: Tue, 28 Jul 2026 10:35:12 -0400 Subject: [PATCH 6/6] feat(MerkleTree): certify the addressed engine subsumes the unaddressed API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves the architecture question raised in review by taking the staged-parallel direction explicitly, and by upgrading the "one engine" claim from prose to proof wherever it can be discharged without touching the pre-existing upstream API. Three subsumption certificates (all `[propext]`, no new axioms): * `buildMerkleTreeAddressed_const` — the constant instance recovers `InductiveMerkleTree.buildMerkleTreeWithHash`. * `functional_completeness_of_addressed` — the unaddressed completeness theorem is *derived* from `addressed_functional_completeness` at the constant instance rather than reproved. * `findCollisionAddressed_const` — erasing the address tag from the engine's constructive collision walk yields `InductiveMerkleTree.findCollision` on the nose. This is the one that answers the "the collision engines remain parallel" objection: they are one function up to the address decoration. Prose corrected to match the code: the module header now states that the unaddressed API is *propositionally*, not definitionally, subsumed; that its definitions stand unchanged; and that the definitional migration is deliberately left to the maintainers because it would change an API load-bearing for `Inductive.Extractability`, `Inductive.Batch`, `Uniqueness` and `QueryBound`. Full `lake build VCVio` green (3007 jobs); no new `sorry`. --- .../MerkleTree/Addressed/Basic.lean | 88 ++++++++++++++++--- 1 file changed, 78 insertions(+), 10 deletions(-) diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean index d84b6b2bb..16ec5e21d 100644 --- a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean +++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean @@ -7,18 +7,35 @@ Authors: Richard Goodman import VCVio.CryptoFoundations.MerkleTree.Inductive.Binding import VCVio.CryptoFoundations.TweakableHash -/-! # Node-Addressed Merkle Trees: the one engine +/-! # Node-Addressed Merkle Trees Merkle trees whose node hash may depend on the **full address** of the node being hashed — the typed root-path position `NodeAddress s` — via `nodeHash : NodeAddress s → α → α → α`. -This is the single engine of which the ordinary tree (constant `nodeHash`), the +Tree building, putative-root recomputation, completeness, and constructive collision +tracing are defined and proven **once here**, for an arbitrary `nodeHash`. Every hash +discipline expressible as a `nodeHash` — the ordinary tree (constant), the level-separated tree (`nodeHash` through the depth of the addressed subtree), and XMSS/SLH-DSA-style fully-addressed trees (`nodeHash` through an arbitrary -address-to-tweak map) are instances: tree building, putative-root recomputation, -completeness, and constructive collision tracing are defined and proven **once**, -and every instance inherits them by specializing `nodeHash`. +address-to-tweak map) — inherits all of it by specialization. + +**Scope note (staged, deliberately).** The pre-existing unaddressed API in +`MerkleTree.Inductive` is *not* re-expressed as a wrapper around this engine: its +definitions (`getPutativeRootWithHash`, `populateUp`, `findCollision`) stand +unchanged, and this module is added alongside them. What the `Instances` section +below establishes instead is that the unaddressed API is **propositionally +subsumed** at the constant instance — its build and putative-root computations are +recovered (`populateUpAddressed_const`, `getPutativeRootAddressed_const`), its +completeness theorem is *re-derived* from this engine's rather than reproved +(`functional_completeness_of_addressed`), and its constructive collision walk is +literally this engine's walk with the address tag erased +(`findCollisionAddressed_const`). Turning that propositional subsumption into a +definitional one — redefining the unaddressed entry points as constant +specializations — would change a load-bearing upstream API consumed by +`Inductive.Extractability`, `Inductive.Batch`, `Uniqueness` and `QueryBound`, so it +is left as a follow-up for the maintainers rather than performed inside this +contribution. Design: at each recursion step into a child, the engine passes the *reindexed* hash `fun a => nodeHash (.inL a)` (resp. `.inR`) — the address is threaded by @@ -434,13 +451,20 @@ theorem addressed_oriented_binding {s : Skeleton} exact ⟨a, c, by simpa [AddressedCollision, Prod.ext_iff] using hcol.1, by simpa [AddressedCollision] using hcol.2⟩ -/-! ## Instances: one engine, three trees +/-! ## Instances: three hash disciplines, one engine The three hash disciplines are specializations of `nodeHash`; the theorems above -specialize with them. The recovery theorems below are the dedup certificates: the -unaddressed engine's core functions are *definitionally subsumed* (constant -instance), and the level-separated (`Tweaked`) development factors through -`NodeAddress.subtreeDepth`. -/ +specialize with them. The theorems below are the **subsumption certificates** for the +constant instance: they exhibit the unaddressed `MerkleTree.Inductive` API as this +engine specialized, at the level of its computations +(`populateUpAddressed_const`, `getPutativeRootAddressed_const`, +`buildMerkleTreeAddressed_const`), its completeness theorem +(`functional_completeness_of_addressed`, derived here rather than reproved) and its +constructive collision kernel (`findCollisionAddressed_const`: address erasure sends +one to the other on the nose). The subsumption is propositional, not definitional — +see the scope note in the module header. The level-separated (`Tweaked`) development +factors through `NodeAddress.subtreeDepth` and is *definitionally* an instance +(`levelNodeHash_eq_addressed` is `rfl`). -/ section Instances @@ -466,6 +490,50 @@ theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton} | leaf v => rfl | internal dl dr ihl ihr => simp [populateUpAddressed, BinaryTree.populateUp, ihl, ihr] +omit [DecidableEq α] in +/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed build. -/ +theorem buildMerkleTreeAddressed_const (h : α → α → α) {s : Skeleton} + (ld : LeafData α s) : + buildMerkleTreeAddressedWithHash ld (fun _ => h) + = InductiveMerkleTree.buildMerkleTreeWithHash ld h := + populateUpAddressed_const h ld + +omit [DecidableEq α] in +/-- **Subsumption certificate (completeness)**: the unaddressed completeness theorem +is a consequence of the engine's, at the constant instance. This is not a second +proof of completeness — it is the first one, specialized. -/ +theorem functional_completeness_of_addressed (h : α → α → α) {s : Skeleton} + (idx : SkeletonLeafIndex s) (ld : LeafData α s) : + InductiveMerkleTree.getPutativeRootWithHash idx (ld.get idx) + (InductiveMerkleTree.generateProof + (InductiveMerkleTree.buildMerkleTreeWithHash ld h) idx) h + = (InductiveMerkleTree.buildMerkleTreeWithHash ld h).getRootValue := by + rw [← buildMerkleTreeAddressed_const h ld, ← getPutativeRootAddressed_const h] + exact addressed_functional_completeness idx ld (fun _ => h) + +/-- **Subsumption certificate (collision kernel)**: erasing the address tag from the +engine's constructive collision walk yields *exactly* the unaddressed `findCollision`. +So the two collision kernels are not parallel implementations that happen to agree on +their statements — they are one function, up to the address decoration. -/ +theorem findCollisionAddressed_const (h : α → α → α) {s : Skeleton} + (idx : SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) : + (findCollisionAddressed (fun _ => h) idx proof₁ proof₂ x y).map (fun w => w.2) + = InductiveMerkleTree.findCollision h idx proof₁ proof₂ x y := by + induction idx with + | ofLeaf => rfl + | ofLeft idxLeft ih => + rw [findCollisionAddressed, InductiveMerkleTree.findCollision] + simp only [getPutativeRootAddressed_const, dite_eq_ite] + split + · rw [Option.map_map]; exact ih proof₁.tail proof₂.tail + · split <;> rfl + | ofRight idxRight ih => + rw [findCollisionAddressed, InductiveMerkleTree.findCollision] + simp only [getPutativeRootAddressed_const, dite_eq_ite] + split + · rw [Option.map_map]; exact ih proof₁.tail proof₂.tail + · split <;> rfl + /-- **Level-separated instance**: hash through the depth of the addressed subtree. This is the discipline of the `Tweaked` development: per-level domain separation. -/ def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)