feat(MerkleTree): add batch openings with completeness and uniqueness for inductive Merkle trees

[Abraxas1010]

Summary

This PR adds batch openings for the inductive Merkle tree construction — opening several leaves of one tree against a single root with one deduplicated piece of authentication data — together with completeness and (injective-hash) uniqueness theorems. It addresses the next open checkbox of Verified-zkEVM/ArkLib#4 ("Prove completeness of Merkle commitments — Batch-index"), and is the vector-commitment operation used by the query phase of IOP-based systems (FRI/STIR/WHIR) and the BCS transform.

Design

• A batch is specified by a selector sel : LeafData Bool s (reusing the existing tree vocabulary; no new index machinery).
• BatchProof α sel is an inductive family that mirrors the tree but is pruned at unselected subtrees: a subtree with no selected leaf contributes exactly one hash (its root); a node with selected leaves on both sides contributes none. Malformed proofs are unrepresentable by typing, in the same spirit as the depth-indexed List.Vector of generateProof; the family is provably uninhabited on selectors that open nothing (BatchProof.anySelected_of_batchProof).
  • opening a single leaf recovers the information content of the single-index copath;
  • opening all leaves yields a proof carrying no hashes at all;
  • shared copath nodes are never duplicated.
• The API mirrors the single-index one exactly: functional layer (getPutativeBatchRootWithHash) + monadic layer (getPutativeBatchRoot, verifyBatchProof) connected by a simulateQ reduction lemma.

Main results

Theorem	Statement	#print axioms
functional_batch_completeness	honest batch proof + true selected values recompute the root, for every selector opening ≥ 1 leaf, under any hash	[propext, Quot.sound]
batch_completeness	Pr[verify = true] = 1 under the random oracle (reduces through simulateQ, exactly like the single-index completeness)	[propext, Classical.choice, Quot.sound]
getPutativeBatchRootWithHash_unique	with Function.Injective2 h, same selector + same putative root ⟹ identical claimed values and identical authentication data (batch analogue of Uniqueness.lean)	[propext]

Scope honesty

This PR proves completeness and deterministic uniqueness only. Batch extractability (the ROM game, next checkbox of ArkLib#4) is deliberately not attempted here — happy to discuss whether the Extractability.lean machinery should be generalized to batch selectors as a follow-up, and to work on it.

Validation performed (not in the diff)

• lake build VCVio green at 24fe01d (this branch's base).
• Concrete corpus with a non-commutative hash (2a+3b+1): batch root equals tree root on a depth-2 tree opening leaves {0,3}; single-leaf batch agrees with the single-index getPutativeRootWithHash; all-leaves batch proof is hash-free by construction; nothing-selected selector is uninhabited.
• Mutation check: swapping the hash argument order in both the functional and monadic recomputation (so the simulateQ lemma still holds) makes functional_batch_completeness fail to compile — the completeness theorem is genuinely sensitive to tree order.

Naming and style are happy to move wherever the maintainers prefer.

---

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

[github-actions]

🤖 PR Summary

ℹ️ This PR modifies 1 file(s) under ToMathlib/ — consider whether a corresponding upstream PR is needed.

#1 MerkleTree: batch openings (completeness + uniqueness)

Adds batch (multi-leaf) opening support to the inductive Merkle tree construction and proves completeness and uniqueness. A batch opening authenticates several leaves against a single root with a single, deduplicated proof. This is the missing piece for the vector-commitment operation used in IOP query phases (FRI / STIR / WHIR) and the BCS transform; it addresses the next open checkbox of Verified-zkEVM/ArkLib#4.

New modules (under VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/):

• Defs.lean — core definitions: BatchProof (inductive family, pruned at unselected subtrees), SelectedValues / selectedValues, honest prover generateBatchProof, functional and monadic root recomputation (getPutativeBatchRootWithHash, getPutativeBatchRoot), verifyBatchProof, and simulateQ_getPutativeBatchRoot (bridging the two APIs).
• Completeness.lean — functional_batch_completeness (honest proof yields the correct root, by induction on the selector) and batch_completeness (monadic version, probability 1 under simulateQ).
• Uniqueness.lean — getPutativeBatchRootWithHash_unique (same selector and root ⇒ identical claimed values and proof data, assuming Injective2 hash). Contrapositive getPutativeBatchRootWithHash_batch_roots_ne_of_ne. Supporting lemmas anySelected_of_batchProof and selectedValues_eq_of_not_anySelected.
• ToSingle.lean — reduction to single-index openings: selectedValueAt, batchToSingleProof, theorem getPutativeRootWithHash_batchToSingleProof (root is preserved), and getPutativeBatchRootWithHash_binding (cross-selector binding via existing findCollision).

Existing files modified:

• Defs.lean — todo checklist updated: "Multi-leaf proofs" marked [x] with reference to Batch.Defs.

New test file:

• VCVioTest/MerkleTreeBatch.lean — concrete examples for a depth‑2 tree: singleton reduction matches generateProof, pruning shape check, all‑selected proof is hash‑free, empty selector is uninhabited, cross‑selector collision extraction.

Scope honesty: Completeness and deterministic uniqueness are proved; batch extractability (ROM game) is not attempted in this PR. No sorry or admit appear in any added or modified file.

---

Statistics

Metric	Count
📝 Files Changed	10
✅ Lines Added	822
❌ Lines Removed	1

---

Lean Declarations

✏️ Added: 60 declaration(s)

ToMathlib/Data/IndexedBinaryTree/Basic.lean (2)

• def LeafData.anySelected {s : Skeleton} : LeafData Bool s → Bool
• theorem LeafData.anySelected_of_get {s : Skeleton} {sel : LeafData Bool s}

VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Completeness.lean (2)

• theorem batch_completeness [DecidableEq α] [Inhabited α] [SampleableType α] {s : Skeleton}
• theorem functional_batch_completeness {s : Skeleton}

VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Defs.lean (7)

• def SelectedValues (α : Type u) : {s : Skeleton} → LeafData Bool s → Type u
• def generateBatchProof : {s : Skeleton} → (cache : FullData α s) → (sel : LeafData Bool s) →
• def getPutativeBatchRoot {m : Type _ → Type _} [Monad m] [HasQuery (spec α) m] :
• def getPutativeBatchRootWithHash (hashFn : α → α → α) :
• def selectedValues : {s : Skeleton} → (leaves : LeafData α s) → (sel : LeafData Bool s) →
• def verifyBatchProof {m : Type _ → Type _} [Monad m] [HasQuery (spec α) m] [DecidableEq α]
• lemma simulateQ_getPutativeBatchRoot {s : Skeleton} {sel : LeafData Bool s}

VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/ToSingle.lean (4)

• def batchToSingleProof (hashFn : α → α → α) : {s : Skeleton} → {sel : LeafData Bool s} →
• def selectedValueAt : {s : Skeleton} → {sel : LeafData Bool s} → SelectedValues α sel →
• theorem getPutativeBatchRootWithHash_binding [DecidableEq α] (hashFn : α → α → α)
• theorem getPutativeRootWithHash_batchToSingleProof (hashFn : α → α → α)

VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Uniqueness.lean (4)

• theorem BatchProof.anySelected_of_batchProof {s : Skeleton} {sel : LeafData Bool s}
• theorem getPutativeBatchRootWithHash_batch_roots_ne_of_ne
• theorem getPutativeBatchRootWithHash_unique
• theorem selectedValues_eq_of_not_anySelected {s : Skeleton} {sel : LeafData Bool s}

VCVioTest/MerkleTreeBatch.lean (41)

• def allNonempty : selectAll.anySelected = true
• def allProof : BatchProof Nat selectAll
• def bothLeftSelected : selectBoth.get pairLeftIndex = true
• def bothProof : BatchProof Nat selectBoth
• def bothValues : SelectedValues Nat selectBoth
• def cache : FullData Nat fourLeafSkeleton
• def constantHash (_left _right : Nat) : Nat
• def firstIndex : SkeletonLeafIndex fourLeafSkeleton
• def firstNonempty : selectFirst.anySelected = true
• def firstProof : BatchProof Nat selectFirst
• def firstSelected : selectFirst.get firstIndex = true
• def fourLeafSkeleton : Skeleton
• def leaves : LeafData Nat fourLeafSkeleton
• def leftProof : BatchProof Nat selectLeft
• def leftSelected : selectLeft.get pairLeftIndex = true
• def leftValues : SelectedValues Nat selectLeft
• def orderedHash (left right : Nat) : Nat
• def outerNonempty : selectOuter.anySelected = true
• def outerProof : BatchProof Nat selectOuter
• def pairLeftIndex : SkeletonLeafIndex pairSkeleton
• def pairSkeleton : Skeleton
• def putativeRootsAgree :
• def selectAll : LeafData Bool fourLeafSkeleton
• def selectBoth : LeafData Bool pairSkeleton
• def selectFirst : LeafData Bool fourLeafSkeleton
• def selectLeft : LeafData Bool pairSkeleton
• def selectNone : LeafData Bool fourLeafSkeleton
• def selectOuter : LeafData Bool fourLeafSkeleton
• def selectedValuesDiffer :
• example : IsEmpty (BatchProof Nat selectNone)
• example : cache.getRootValue = 76
• example : orderedHash 9 19 = 76
• example : orderedHash 9 19 ≠ orderedHash 19 9
• example : selectedValueAt (selectedValues leaves selectFirst) firstIndex firstSelected = 1
• example :
• example :
• example :
• example :
• example :
• example :
• example :

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

Lean Quality Signals

• ⚠️ native_decide bypasses the kernel — potential soundness concern in VCVioTest/MerkleTreeBatch.lean (L157)

---

📋 **Additional Analysis**

The diff passes all style, documentation, and workflow checks. No violations or blocking issues.

---

📄 **Per-File Summaries**

• VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Completeness.lean: Adds InductiveMerkleTree.functional_batch_completeness and InductiveMerkleTree.batch_completeness (the batch analogue of the single-index completeness theorem). functional_batch_completeness is a purely functional statement (proved by induction on sel) that for any hash function hash, selector sel with sel.anySelected = true, and leaf data leaves, getPutativeBatchRootWithHash hash (selectedValues leaves sel) (generateBatchProof (buildMerkleTreeWithHash leaves hash) sel h) equals the root of the honestly built tree. batch_completeness lifts this to the monadic random‑oracle API, showing that verifying the batch proof succeeds with probability 1 under simulateQ (by reducing to the functional lemma via simulateQ and beq_iff_eq).
• VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Defs.lean: This new file introduces batch opening definitions for the inductive Merkle tree construction. It defines the BatchProof inductive type for pruned authentication data parameterized by a LeafData Bool selector, the SelectedValues type family and selectedValues extraction function, the honest prover generateBatchProof, and two root recomputation functions—getPutativeBatchRootWithHash (functional) and getPutativeBatchRoot (monadic via the oracle query)—along with the simulateQ_getPutativeBatchRoot lemma equating them under a concrete query implementation. It also provides the batch verification function verifyBatchProof. The file is the first in a module that will be completed by separate files for completeness and uniqueness proofs.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/ToSingle.lean: This new file, ToSingle.lean, adds the core reduction from batch openings to single-index openings for the inductive Merkle tree model. It defines selectedValueAt (the claimed leaf value from a batch opening) and batchToSingleProof (the extracted single-index authentication path at a selected leaf). The theorem getPutativeRootWithHash_batchToSingleProof proves that this extracted single-index opening recomputes the batch opening's putative root, ensuring root preservation. The theorem getPutativeBatchRootWithHash_binding uses that result together with the existing findCollision kernel to establish cross-selector batch binding, strengthening prior results by allowing different selectors and an arbitrary hash function. This file provides the deterministic kernel for future extractability transfers and directly supports the binding security of batch openings.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Batch/Uniqueness.lean: This new file adds batch opening uniqueness results for Merkle trees under an injective hash assumption. It defines two supporting lemmas: BatchProof.anySelected_of_batchProof (any batch proof implies the selector has selected leaves) and selectedValues_eq_of_not_anySelected (all claimed-value tuples agree on selectors with no selected leaves). The main theorem getPutativeBatchRootWithHash_unique proves that two batch openings for the same selector that produce the same putative root must agree on both the claimed selected values and the entire pruned authentication data. Its contrapositive getPutativeBatchRootWithHash_batch_roots_ne_of_ne ensures distinct claimed-value tuples yield distinct putative roots. All definitions are in the InductiveMerkleTree namespace; no sorry or admit appear.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Defs.lean: The file header’s to-do checklist was updated: the item for “Multi-leaf proofs” is now marked as completed ([x]) and includes a reference to the newly created module VCVio.CryptoFoundations.MerkleTree.Inductive.Batch.Defs. This is a documentation-only change; no Lean declarations were added, modified, or left incomplete.
• VCVioTest/MerkleTreeBatch.lean: This new file adds the test module VCVioTest.MerkleTreeBatch that provides concrete examples exercising the behavior of batch opening proofs for a 4-leaf Merkle tree. It defines a skeleton (fourLeafSkeleton), leaf data (leaves), a non-commutative hash (orderedHash), a full cache (cache), several selectors (selectFirst, selectOuter, selectAll, selectNone), and corresponding batch proofs generated via generateBatchProof. A series of example blocks then verify key properties: the singleton reduction batchToSingleProof matches generateProof; the pruning shape of outerProof matches a specific BatchProof constructor; the all-selected allProof consists of only leaf nodes; the empty-selector selectNone yields an empty BatchProof type; and a cross-selector collision extraction example demonstrates findCollision and Collision via getPutativeBatchRootWithHash_binding. The file imports three modules from VCVio.CryptoFoundations.MerkleTree.Inductive.Batch and contains no sorry or admit.
• 4 file(s) filtered as noise (lockfiles, generated, or trivial): .github/workflows/build.yml, ToMathlib/Data/IndexedBinaryTree/Basic.lean, VCVio.lean, VCVioTest.lean

---

Last updated: 2026-07-15 12:19 UTC.

[Abraxas1010]

Fixed the file headers to follow this repo's CONTRIBUTING convention (copyright holder = credited author/organization rather than the ArkLib-style collective holder I had copied over): holder is now The Institute for Ontological Mathematics / Equation Capital dba Apoth3osis, author Abraxas1010. ./scripts/update-lib.sh reports no further update needed and lake build VCVio is green at the new head. The attribute annotations (@[simp, grind] / @[simp, grind =]) mirror the neighboring Defs.lean/Completeness.lean usage and compile warning-free — happy to adjust if a maintainer prefers a different discipline for the new declarations.

[Abraxas1010]

Pushed a second commit delivering the extractability direction promised in the PR body: BatchToSingle.lean, the deterministic reduction of batch openings to single-index openings.

• batchToSingleProof extracts, at every selected leaf, a single-index authentication path from a batch opening — reading each sibling either off the batch proof (pruned side) or by recomputing its putative batch subroot (opened side).
• getPutativeRootWithHash_batchToSingleProof (#print axioms: [propext]): the extracted opening recomputes exactly the batch putative root — so a verifying batch opening yields, at every selected leaf, a verifying single-index opening against the same root. This is the deterministic kernel for transferring the Extractability.lean game to batch openings: a batch adversary that wins at a selected leaf yields a single-index winner for the same committing phase, hence the same query log and the same extracted tree. The game-level packaging is deliberately left as the follow-up.
• getPutativeBatchRootWithHash_binding ([propext]): cross-selector batch binding — two batch openings under possibly different selectors that both select an index, claim distinct values there, and produce the same root, yield a concrete hash collision via the constructive findCollision kernel of Binding.lean. This is strictly stronger than the same-selector, injective-hash uniqueness in the first commit: arbitrary hash, collision as data.

lake build VCVio green; happy to split this commit into its own PR if you prefer smaller review units.

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

[BoltonBailey]

Thanks for the submission, I'll leave a review with more comments.

Looks like this is failing CI due to an extra import in VCVio.lean.

I think if all the file names will start with Batch, they should all just be put in a Batch/ folder and have the rest of the filenames be the same (e.g. Batch/Defs.lean and so forth).

[BoltonBailey]

Thanks, seems like an overall good contribution.

[BoltonBailey]

Seems this isn't used in this file, could it be moved to Uniqueness?

[Abraxas1010]

Done — moved to its only consumer, now Inductive/Batch/Uniqueness.lean (post folder-move).

[BoltonBailey]

if this is _root_ could it be moved to a file where the namespace is appropriate, maybe the file or folder where LeafData is defined?

[Abraxas1010]

Done — LeafData.anySelected now lives in ToMathlib/Data/IndexedBinaryTree/Basic.lean next to LeafData.get, without the _root_ prefix.

[BoltonBailey]

could this theorem be moved to the file where anySelected is defined, wherever that ends up being?

[Abraxas1010]

Done — anySelected_of_get moved to ToMathlib/Data/IndexedBinaryTree/Basic.lean, directly after the anySelected definition.

[Abraxas1010]

Thanks for the review! All three suggestions made sense — done in the latest push:

1. BatchProof.anySelected_of_batchProof — moved to BatchUniqueness.lean, which is its only consumer (and BatchUniqueness now imports just BatchDefs).
2. BinaryTree.LeafData.anySelected — moved to ToMathlib/Data/IndexedBinaryTree/Basic.lean, next to LeafData.get where the rest of the LeafData API lives (dropping the _root_ prefix accordingly).
3. BinaryTree.LeafData.anySelected_of_get — moved to the same file, directly after the anySelected definition.

While rebuilding I also noticed the branch had accidentally picked up an import VCVio.CryptoFoundations.MerkleTree.Tweaked.Basic line in VCVio.lean (from a sibling branch of mine — the file isn't part of this PR), which broke the root build; that stray line is removed in the same commit. Full lake build VCVio is green locally.

[quangvdao]

Thanks for this contribution. I did a deeper semantic pass and the core claims look sound and appropriately scoped: the pruned BatchProof representation is canonical for a nonempty selector, completeness holds for an arbitrary hash, and batchToSingleProof gives a clean deterministic reduction from every selected batch leaf to the existing single-index collision kernel. I did not find an assumption-smuggling or theorem-statement problem here.

I agree with Bolton's folder suggestion: please use

Inductive/Batch/Defs.lean
Inductive/Batch/Completeness.lean
Inductive/Batch/ToSingle.lean
Inductive/Batch/Uniqueness.lean

That will scale better when game-level batch extractability and any later batch-specific query-bound files arrive.

A few final integration points before landing:

1. Please update the branch to current main (chore: complete Lean 4.31 migration #477 is already merged) and rerun the full CI suite. The latest head only has the summary check; the earlier full run was on the version with the stray sibling-branch import.
2. Please ask Bolton for a fresh re-review. His inline threads are outdated and appear addressed, but the old requested-changes review remains on the PR.
3. Keep the extractability wording precise: BatchToSingle is the deterministic kernel for a future game-level transfer, not yet a proof of batch extractability. The game still needs to package the dynamic selector, preserve the commitment-phase extraction log, account for root recomputation/query costs, and transfer the winning event.
4. The injective-hash uniqueness theorem is useful as a structural sanity result, but the constructive collision theorem is the cryptographically meaningful binding result; please avoid presenting global Function.Injective2 as a realistic hash assumption.
5. The dense LeafData Bool s selector is reasonable internally, but ArkLib consumers will naturally have a sparse list/Finset of query indices. This need not block this PR, but please track a sparse-selector conversion/API follow-up so that the eventual FRI/STIR/WHIR consumer does not accidentally pay for or expose a full-tree selection mask.

Subject to the folder move, current-main CI, and Bolton's re-review, I think this should land.

[Abraxas1010]

All review points are now addressed on the updated branch:

• Folder move: the four files now live at Inductive/Batch/{Defs, Completeness, ToSingle, Uniqueness}.lean as suggested, with imports updated accordingly.
• anySelected home: LeafData.anySelected and anySelected_of_get were already moved to ToMathlib/Data/IndexedBinaryTree/Basic.lean (where LeafData lives) in an earlier push; BatchProof.anySelected_of_batchProof sits with the uniqueness development.
• Rebased onto current main (post-chore: complete Lean 4.31 migration #477) and the full CI suite reruns on this head — the earlier failure was the stray sibling-branch import in VCVio.lean, removed some pushes ago.
• Extractability wording: the Batch/ToSingle.lean module doc now states explicitly that it is a deterministic kernel for a future game-level transfer, not a proof of batch extractability, and names what the game-level packaging still owes (dynamic selector, commitment-phase extraction log, root-recomputation query costs, winning-event transfer).
• Function.Injective2 framing: Batch/Uniqueness.lean now says outright that global injectivity is not a realistic assumption on a compressing hash — these are structural sanity results — and points to the constructive collision theorems as the cryptographically meaningful binding statements.
• Sparse selectors: tracked as a follow-up in the Batch/Defs.lean module doc (sparse List/Finset index set → dense selector conversion API with getLeaf-level correspondence lemmas, to land before the FRI/STIR/WHIR-style consumers).

@BoltonBailey — could you take a fresh look when you get a chance? Your earlier inline threads should all be resolved on this head.

[BoltonBailey]

All of this looks good to me.

I agree with Quang that Injective2 is not ideal, but it's also used in the non-batch version of that file. Perhaps one way that could be turned into something more useful is switching to some kind of "Option Injective2" which treats the function of interest as possibly none-valued to represent non-queried pairs and proves that there is a collision in the queried values. But probably that should not be done in this PR, we could file an issue to address both files in a later PR.

[Abraxas1010]

Thanks for the re-review! Filed the Injective2 → queried-domain ("Option Injective2") refinement as #486, covering both the single-opening and batch uniqueness files for a later PR, as suggested.

With that, all three landing conditions from the earlier review are met: folder move done, full CI green on the current-main head, and Bolton's fresh approval. Nothing further pending on my side.

[quangvdao]

Maintainer follow-up completed on this branch.

What changed:

• merged current main into the PR branch;
• clarified that BatchProof is an intrinsic dependent-tree encoding of the path-pruning optimization from Building Cryptographic Proofs from Hash Functions (minimal copath frontier), while noting that a separate tuple-of-paths compression/equivalence API is not formalized here;
• added committed behavioral canaries for noncommutative left/right hash order, both pruning directions, singleton agreement with the ordinary opening API, all-selected/no-authentication-hashes, the empty-selector boundary, batchToSingleProof root preservation, and cross-selector collision extraction;
• wired the new canary module into CI;
• marked the inductive Merkle tree's multi-leaf-proof TODO complete.

Validation:

• full local lake build VCVio passed (2,925 jobs);
• generated-import, style, agent-doc, and interop-isolation checks passed locally;
• all GitHub checks are green, including the fresh full build and the new Merkle batch-opening canary step.

The sparse-selector conversion API, batch query-cost theorem, queried-domain uniqueness refinement, and game-level batch extractability remain appropriate follow-up work rather than blockers for this PR.