feat: vector based merkle tree and proofs

[FawadHa1der]

@quangvdao this is related https://github.com/Verified-zkEVM/ArkLib/issues/4 I am not sure if vector based merkletree proofs are still required or not.

[github-actions]

🤖 Gemini PR Summary

This PR implements vector-based Merkle trees and proof generation within the ArkLib commitment scheme. The primary objective is to transition toward purely functional tree operations, facilitating formal proofs of functional completeness.

Features

• Functional Merkle Tree Operations: Introduced purely functional versions of core Merkle tree operations to support formal verification efforts.
• Vector-Based Proof Generation: Implemented new logic for generating Merkle proofs based on vectors, addressing requirements linked to issue Definition & Security Proofs for Merkle Trees #4.

Refactoring

• MerkleTree Logic: Refactored the existing proof generation logic in ArkLib/CommitmentScheme/MerkleTree.lean to integrate the new functional approach and improve consistency.

Fixes

• No specific bug fixes were noted in this PR.

Documentation

• No dedicated documentation files were modified, though the PR references technical requirements in issue Definition & Security Proofs for Merkle Trees #4.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	205
❌ Lines Removed	13

---

Lean Declarations

❌ **Added:** 10 declaration(s)

• def siblingIndex {n : ℕ} (i : Fin (2 ^ (n + 1))) : Fin (2 ^ (n + 1)) in ArkLib/CommitmentScheme/MerkleTree.lean
• def getPutativeRoot_with_hash {n : ℕ} (i : Fin (2 ^ n)) (leaf : α) (proof : List.Vector α n) in ArkLib/CommitmentScheme/MerkleTree.lean
• theorem functional_completeness {n : ℕ} (leaves : List.Vector α (2 ^ n)) (i : Fin (2 ^ n)) in ArkLib/CommitmentScheme/MerkleTree.lean
• lemma runWithOracle_listVector_mmap_query (f : (spec α).FunctionType) {m : ℕ} in ArkLib/CommitmentScheme/MerkleTree.lean
• lemma runWithOracle_query (f : (spec α).FunctionType) (x : α × α) : in ArkLib/CommitmentScheme/MerkleTree.lean
• lemma runWithOracle_buildMerkleTree (f : (spec α).FunctionType) (n : ℕ) in ArkLib/CommitmentScheme/MerkleTree.lean
• def buildMerkleTree_with_hash (n : ℕ) (leaves : List.Vector α (2 ^ n)) (hashFn : α × α → α) : in ArkLib/CommitmentScheme/MerkleTree.lean
• lemma runWithOracle_getPutativeRoot (f : (spec α).FunctionType) {n : ℕ} (i : Fin (2 ^ n)) in ArkLib/CommitmentScheme/MerkleTree.lean
• def buildLayer_with_hash (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (hashFn : α × α → α) : in ArkLib/CommitmentScheme/MerkleTree.lean
• lemma runWithOracle_buildLayer (f : (spec α).FunctionType) (n : ℕ) in ArkLib/CommitmentScheme/MerkleTree.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following lines violate the style guide:

• Lines 133, 134: fun j : Fin m => and let j' : Fin n := — Quote: m, n, k, ... : Natural numbers (where i, j, k are reserved for integers).
• Line 154: def siblingIndex {n : ℕ} (i : Fin (2 ^ (n + 1))) — Quote: m, n, k, ... : Natural numbers (where i, j, k are reserved for integers).
• Line 219: Empty line — Quote: Avoid empty lines *inside* definitions or proofs. (The docstring is part of the definition).
• Line 249: def buildLayer_with_hash — Quote: Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime).
• Line 254: := by rwa [pow_succ] at leaves — Quote: Place by at the end of the line preceding the tactic block. Indent the tactic block.
• Line 260: def buildMerkleTree_with_hash — Quote: Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime).
• Line 275: def getPutativeRoot_with_hash {n : ℕ} (i : Fin (2 ^ n)) — Quote: Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime). and m, n, k, ... : Natural numbers.
• Line 292: lemma runWithOracle_query — Quote: Every definition and major theorem should have a docstring.
• Line 298: lemma runWithOracle_listVector_mmap_query — Quote: Every definition and major theorem should have a docstring.
• Line 310: lemma runWithOracle_buildLayer — Quote: Every definition and major theorem should have a docstring.
• Line 322: lemma runWithOracle_buildMerkleTree — Quote: Every definition and major theorem should have a docstring.
• Line 333: lemma runWithOracle_getPutativeRoot ... (i : Fin (2 ^ n)) — Quote: Every definition and major theorem should have a docstring. and m, n, k, ... : Natural numbers.
• Line 349: (i : Fin (2 ^ n)) — Quote: m, n, k, ... : Natural numbers.
• Line 404 (approximate): (i := ⟨i.val / 2, by omega⟩) — Quote: Place by at the end of the line preceding the tactic block. Indent the tactic block.

---

📄 **Per-File Summaries**

• ArkLib/CommitmentScheme/MerkleTree.lean: Refactors Merkle proof generation and introduces purely functional versions of the tree operations to prove functional completeness.

---

Last updated: 2026-02-26 12:36 UTC.

[quangvdao]

Definitely this is still of interest

[FawadHa1der]

The soundness theorem is not implemented as it wasn't yet implemented in InductiveMerkleTree either. I could take a look but I imagine this would require some assumptions/knowledge about the hash functions etc.

[FawadHa1der]

oh let me look at the style guide, sorry

[FawadHa1der]

This is implemented with the help Codex/Claude combo.

[alexanderlhicks]

Hello! Thanks for the PR and sorry for the delay in getting to this. I'll be merging the 4.26 PR soon, which might break a few things, and get back to all the other PRs including this one.

[alexanderlhicks]

/review

External:

Internal:

Comments:
Please review for correctness with respect to ArkLib.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
The implementation of the Merkle Tree commitment scheme is correct, featuring a significant improvement in logic by replacing complex neighbor-finding with a simplified siblingIndex approach. Crucially, this PR resolves previous gaps in the formalization by removing sorry placeholders and rigorously proving functional completeness. The construction and verification workflows are consistent, and the code is approved for merge.

---

📄 **Review for `ArkLib/CommitmentScheme/MerkleTree.lean`**

Review of ArkLib/CommitmentScheme/MerkleTree.lean

Verdict: Correct

The changes in ArkLib/CommitmentScheme/MerkleTree.lean correctly implement the Merkle Tree commitment scheme, providing a rigorous fix to the previous sorry in the completeness proof and simplifying the neighbor-finding logic.

Analysis of Changes:

1. Refactoring of findNeighbors to siblingIndex:

   • Logic: The old findNeighbors function, which relied on complex bit-reversal logic, has been replaced by siblingIndex. The new function determines the sibling of an index i at a specific layer simply by checking the parity of i (i ^ 1).
   • Correctness: This aligns perfectly with the buildLayer function, which pairs adjacent elements at indices 2k and 2k+1. If i is even (2k), its sibling is i+1. If i is odd (2k+1), its sibling is i-1.
   • Boundaries: The arithmetic in siblingIndex is accompanied by proofs ensuring i ± 1 stays within the bounds of Fin (2^(n+1)). Specifically, the case where i is even correctly proves i + 1 < 2^(n+1) because 2^(n+1) is even for all n ≥ 0, so the maximal index 2^(n+1) - 1 must be odd.

2. generateProof and getPutativeRoot Alignment:

   • Construction: generateProof now constructs the proof bottom-up using List.Vector.cons, placing the sibling from the bottom-most layer at the head of the list.
   • Verification: getPutativeRoot consumes the proof from the head (proof.head) and recurses on the tail. This effectively "hashes up" the tree from leaves to root.
   • Consistency: The order of construction and consumption is consistent (Leaf -> Root).

3. Completeness Proofs:

   • The previous sorry in buildLayer_neverFails has been resolved by an inductive proof showing that mmap of query over a vector always succeeds in the runWithOracle semantics.
   • A functional completeness theorem functional_completeness is introduced, proving that the purely functional versions of the operations satisfy the scheme's correctness properties. This is then lifted to the probabilistic setting in completeness.
   • The logic in functional_completeness correctly handles the left/right child cases, ensuring the hash arguments are ordered correctly ((node, sibling) vs (sibling, node)).

4. Misformalization Checks:

   • Off-by-One: The indexing logic for layers (n vs n+1) and vectors (Fin (2^n)) is handled correctly via dependent matching and omega.
   • Recursion: Base cases (n=0) and recursive steps are well-defined and terminating.
   • Assumptions: The use of [DecidableEq α] is appropriate for the verification logic.

Conclusion:

The code is a correct formalization of a vector-based Merkle Tree commitment scheme. The implementation is robust, and the accompanying proofs provide high confidence in its correctness. No changes are required.

[alexanderlhicks]

If this is no longer used (or for illustration only as indicated in the comment further down), maybe we can just remove it?

[alexanderlhicks]

@FawadHa1der could you give me access to your branch? I've fixed the merge conflicts and resulting broken proofs but cannot push (otherwise I can also open another PR with you as co-author to merge this?).

(disregard the last merge commit.)