feat: Inductive Merkle Trees with completeness theorem

[BoltonBailey]

Define Merkle trees over an indexed inductive binary tree data type.

A reference for Merkle trees can be found in chapter IV of the SNARGs book. Note though, that this development generalizes to arbitrary binary tree structures.

The potential benefits of this are:

• We can commit to non-power-of-two sized tree with non-perfectly balanced Merkle trees
• The code is written in a more functional than one that uses Vector,
• We perhaps avoid things like needing API in VCVio for monadic operations over vectors.

This PR includes:

• A low level file defining and providing API for indexed binary Merkle trees
• Definitions of the basic Merkle tree primitives for single-leaf proofs in the OracleComp monad
• The same primitives as pure functions with the hash passed explicitly
• Completeness theorem for single-leaf proofs
  • Currently depends on sorries relating randomOracle to runWithOracle. Not sure if VCVio is undergoing a change that will change what we need here.

I am marking this as ready for review, despite the presence of sorrys, since all the sorries are either not critical, or about VCVio definitions. Reviewers, please let me know if:

• Any sorries really ought to be finished before merging
• The PR should be split somehow

[alexanderlhicks]

/review

External:
https://github.com/hash-based-snargs-book/hash-based-snargs-book/blob/main/snargs-book.pdf

Internal:

Comments:

[alexanderlhicks]

Is there a good reference for inductive Merkle trees we could use here? Or specific comments?
@quangvdao @BoltonBailey

[github-actions]

🤖 AI Review (with external context)\n\nGenerating AI review...

Thank you for submitting this pull request. This is a substantial and well-structured contribution toward formalizing Merkle trees. The inductive approach using a Skeleton is powerful, and the separation of the generic BinaryTree definitions from the InductiveMerkleTree logic is excellent. The code is clearly a work in progress with many sorry placeholders, but it lays a solid foundation.

Here is a review of the changes with suggestions for improvement.

High-Level Summary

This pull request introduces a formalization of binary trees and an inductive implementation of Merkle trees built upon them. Key features include:

• A generic, inductively defined binary tree structure (BinaryTree.lean).
• An implementation of Merkle tree logic (build, prove, verify) using OracleComp for the hash function (InductiveMerkleTree.lean).
• The beginnings of correctness proofs, notably a completeness theorem.
• Utility files for handling QueryCache (QueryCacheToSet.lean).

The overall direction is excellent, but several areas need refinement, particularly in the binary tree indexing and navigation logic, as well as completing the many sorry'd proofs.

Code Review and Suggestions

ArkLib/CommitmentScheme/Junk.lean

This file appears to contain commented-out scratch code. It should be removed before merging.

(Edited comment from Bolton: Yes, I realize this, I will delete it before I un-draft, but for now I have committed it because these functions seemed like they would be useful at one point and I want to keep a pointer to them in case they turn out to be useful.)

ArkLib/CommitmentScheme/QueryCacheToSet.lean

This is a nice utility.

• The proof for QueryCache.toSet_eq_iff is sorry'd. Given [Subsingleton ι], this should be provable, as the cache for the unique oracle index i is the only component. Completing this would be great.

  -- ArkLib/CommitmentScheme/QueryCacheToSet.lean:32
  @[simp]
  theorem QueryCache.toSet_eq_iff {ι : Type} [Subsingleton ι] {spec : OracleSpec ι}
      (i : ι) (cache1 cache2 : spec.QueryCache) :
      QueryCache.toSet i cache1 = QueryCache.toSet i cache2 ↔ cache1 = cache2 := by
    constructor
    · intro h
      -- The proof here is sorried. It can be completed.
      ext i' d
      have : i' = i := Subsingleton.elim _ _
      subst this
      unfold QueryCache.toSet at h
      simp only [Set.ext_iff, Set.mem_setOf_eq] at h
      exact (h (d, ·)).trans (Option.ext_iff)
    · intro h_eq
      subst h_eq
      rfl

(Edited comment from Bolton: This proof doesn't seem to work, it gets the same error that I got when I tried, namely that QueryCache has no ext)

ArkLib/CommitmentScheme/BinaryTree.lean

The data structures here are well-conceived, but there are some issues with the indexing and navigation functions.

1. SkeletonInternalIndex Definition

   The definition of SkeletonInternalIndex seems incorrect. It takes SkeletonLeafIndex in its recursive constructors, which prevents indexing most internal nodes. It was likely intended to be recursive on SkeletonInternalIndex.

   // ArkLib/CommitmentScheme/BinaryTree.lean:94
   inductive SkeletonInternalIndex : Skeleton → Type
     | ofInternal {left right} : SkeletonInternalIndex (Skeleton.internal left right)
     | ofLeft {left right : Skeleton} (idxLeft : SkeletonLeafIndex left) : -- Should this be SkeletonInternalIndex?
         SkeletonInternalIndex (Skeleton.internal left right)
     | ofRight {left right : Skeleton} (idxRight : SkeletonLeafIndex right) : -- Should this be SkeletonInternalIndex?
         SkeletonInternalIndex (Skeleton.internal left right)

   Please review this definition. If it's intended to index all internal nodes, it should probably be:

   inductive SkeletonInternalIndex : Skeleton → Type where
     | ofRoot {left right} : SkeletonInternalIndex (Skeleton.internal left right)
     | ofLeft {left right : Skeleton} (idxLeft : SkeletonInternalIndex left) :
         SkeletonInternalIndex (Skeleton.internal left right)
     | ofRight {left right : Skeleton} (idxRight : SkeletonInternalIndex right) :
         SkeletonInternalIndex (Skeleton.internal left right)
   -- with SkeletonInternalIndex for Skeleton.leaf being an empty type.

   However, since this type isn't heavily used yet, it might be simpler to remove it for now if it's not needed.

(Edited comment from Bolton: Good catch! Though indeed, it might not be needed.)

2. findSibling and generateProof Logic

   The current implementation of generateProof in InductiveMerkleTree.lean relies on findUncles, which in turn relies on findSibling. The logic in findSibling appears to be flawed for its purpose and contains syntax errors.

   The recursive calls idxLeftLeft.ofLeft.findSibling are not valid Lean syntax. They should probably be (SkeletonNodeIndex.ofLeft idxLeftLeft).findSibling.

   More importantly, the recursive structure of findSibling seems incorrect for finding the siblings along the ancestor path needed for a Merkle proof.

   A much clearer way to implement generateProof would be to define it recursively, mirroring the structure of the tree and index. This would also make it easier to prove its properties. The sorry'd simp lemmas for generateProof in InductiveMerkleTree.lean already provide the perfect specification for such a recursive definition.

   Suggestion: Implement generateProof directly and remove findSibling and findUncles if they are no longer needed.

   -- In ArkLib/CommitmentScheme/InductiveMerkleTree.lean
   
   /-- Generate a Merkle proof for a leaf at a given idx
       The proof consists of the sibling hashes needed to recompute the root.
   -/
   def generateProof {s} (cache_tree : FullDataTree α s) :
       BinaryTree.SkeletonLeafIndex s → List α
     | .ofLeaf => []
     | .ofLeft idxLeft =>
       (cache_tree.getRightSubtree).getRootValue ::
         (generateProof cache_tree.getLeftSubtree idxLeft)
     | .ofRight idxRight =>
       (cache_tree.getLeftSubtree).getRootValue ::
         (generateProof cache_tree.getRightSubtree idxRight)

   This definition is simple, correct, and its simp lemmas will hold by definition, avoiding complex proofs about findSibling. You'd need to adjust cache_tree access, but FullDataTree.internal_eq can destructure it.

(Edited comment from Bolton: Not sure why it thinks there are syntax errors, and I like how the current definition makes clear the relationship to sibling evaluation, but I agree that this is much simpler, and indeed this change makes the following simp lemmas rflable, so I'll switch to it. Not sure why this isn't in the section below about the InductiveMerkleTree.lean file, perhaps it is telling me it should be moved?)

3. Incomplete Lemmas

   Many lemmas like FullDataTree.toLeafDataTree_getValueAtIndex are sorry. These should be provable with straightforward induction and would be valuable additions.

(Edited comment from Bolton: Yes, I guess this PR is still a draft)

ArkLib/CommitmentScheme/InductiveMerkleTree.lean

This file contains the core logic and is looking very promising. The main suggestions are around completing the proofs.

1. Completing sorrys in Core Theorems

   The main completeness theorem depends on several key lemmas that are incomplete, such as mem_buildMerkleTree_support_iff_v3 and putative_root_eq_merkle_tree_cache_root_of_generate_proof. Focusing on these would be the most impactful next step.

2. Making aesop Proofs More Robust

   The use of aesop is great for quickly sketching proofs. However, for core theorems, relying on it entirely can make proofs brittle. When you have time, consider expanding these into more structured proofs. For example, in putative_root_eq_merkle_tree_cache_root_of_generate_proof, the aesop calls could be broken down into more explicit apply, rw, and have steps.

3. Proof of completeness

   The completeness theorem proof sketch is good, but relies on two sorry'd steps. These should be extracted into their own lemmas for clarity.

   • The first sorry claims that membership in the support implies leaf_data_tree = merkle_tree_cache.toLeafDataTree. This is a crucial property.

     -- Suggestion:
     lemma mem_buildMerkleTree_support_implies_toLeafDataTree_eq {α : Type} [DecidableEq α] [SelectableType α]
         {s : Skeleton} (leaf_data_tree : LeafDataTree α s) (merkle_tree_cache : FullDataTree α s)
         (preexisting_cache resulting_cache)
         (h_mem : ((merkle_tree_cache, resulting_cache) ∈
           ((simulateQ randomOracle (buildMerkleTree leaf_data_tree)).run preexisting_cache).support)) :
         leaf_data_tree = merkle_tree_cache.toLeafDataTree := by
       rw [mem_buildMerkleTree_support_iff_v3] at h_mem
       -- prove it from h_mem.1
       sorry

   • The second sorry relates to the cache_subset property. This is essentially the soundness of getPutativeRoot. Proving this will likely involve completing putative_root_eq_merkle_tree_cache_root_of_generate_proof.

(Edited comment from Bolton: Yes, I've actually already done these, I just haven't committed them yet.)

4. Moving Helper Lemmas

   You've correctly noted that some helper lemmas should be moved to more general libraries. This is great practice.

Conclusion

This is a fantastic start to a formalization of Merkle trees. The approach is sound, and the code structure is clean. My recommendations focus on fixing the tree navigation logic and systematically filling in the proofs. Keep up the great work

(Edited comment from Bolton: ❤️)

[quangvdao]

@BoltonBailey How ready is this PR to be merged?

[BoltonBailey]

@BoltonBailey How ready is this PR to be merged?

The completeness theorem is finished modulo the sorries in the ToVCVio folder, but I was hesitant to work too hard on those, because I recall VCVio was undergoing a rewrite. LMK if I should prove those sorries or hold off until after the rewrite is done or what.

The sorries in ArkLib/ToMathlib/Data/IndexedBinaryTree/Equiv.lean are not important and could be removed or spun off.

[quangvdao]

I think let's just put sorry's for now and we will work on it later.

If you want, the next step is to state the (multi-instance) extractability property of Merkle trees, as found in the SNARG book. This can be in the next PR.

[alexanderlhicks]

Should we consider splitting off the ToVCVio portion of this PR and just having an equivalent PR to VCVio that will be more flexible to any changes in VCVio / fixed in VCVio if needed? That is, if there's a chance that we could otherwise end up with something in ArkLib/ToVCVio that ends up not really being appropriate for VCVio after changes to the latter.

[BoltonBailey]

Ideally that whole file/folder could just be upstreamed at once. But now that I've added to it in this PR, I'd rather that happen after this PR is merged. (I guess #83 touches this file too?)

[alexanderlhicks]

LGTM?