chore: move Merkle tree files

[BoltonBailey]

I am trying to port over some of my changes from Verified-zkEVM/ArkLib#144

To start with, this change moves Merkle tree content to dedicated folder, with subfolders for different versions with different tree structure. It also moves the completeness theorems on the inductive side into its own file separate from the the defs, in anticipation of more different files for the main theorems about security properties.

[github-actions]

🤖 PR Summary

Refactoring

• Restructured the Merkle tree implementation into modular Inductive and Vector subfolders.
• Decoupled inductive Merkle tree definitions in Inductive/Defs.lean from completeness proofs, migrating functional_completeness and monadic completeness theorems to Inductive/Completeness.lean.
• Updated VCVio.lean with granular module references to reflect the new file organization.

Mathematical Formalization

• Isolated functional_completeness and completeness theorems verifying that honestly generated Merkle proofs match their roots.
• Note: No sorry or admit placeholders were found in the modified files.

Infrastructure / CI

• Updated GitHub Action workflows to trigger documentation generation on pull requests and expand review permissions for first-time contributors.
• Note: These CI updates were identified in the code changes but are not explicitly mentioned in the PR title or body.

---

Statistics

Metric	Count
📝 Files Changed	6
✅ Lines Added	103
❌ Lines Removed	69

---

Lean Declarations

✏️ **Removed:** 2 declaration(s)

• theorem functional_completeness {s : Skeleton} in VCVio/CryptoFoundations/MerkleTree/Inductive/Defs.lean
• theorem completeness [DecidableEq α] [SampleableType α] {s} in VCVio/CryptoFoundations/MerkleTree/Inductive/Defs.lean

✏️ **Added:** 2 declaration(s)

• theorem functional_completeness {s : Skeleton} in VCVio/CryptoFoundations/MerkleTree/Inductive/Completeness.lean
• theorem completeness [DecidableEq α] [SampleableType α] {s} in VCVio/CryptoFoundations/MerkleTree/Inductive/Completeness.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

All changes adhere to the style guide.

---

📄 **Per-File Summaries**

• .github/workflows/agent-docs.yml: The update adds a pull request trigger to the Agent Docs workflow, ensuring that documentation tasks are automatically executed and verified during the code review process.
• .github/workflows/review.yml: This update expands the review workflow's trigger conditions to include pull requests authored by first-time contributors. Previously, the workflow logic only permitted execution for project owners, members, and collaborators.
• VCVio.lean: The changes in VCVio.lean refactor the Merkle tree library imports by replacing broad module references with more specific sub-modules for inductive and vector-based Merkle tree definitions and completeness proofs.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Completeness.lean: This new file establishes the completeness of inductive Merkle trees by proving that honestly generated proofs always verify against honestly built roots. It introduces the functional_completeness theorem using induction on leaf indices and the completeness theorem for the monadic API, without any sorry placeholders.
• VCVio/CryptoFoundations/MerkleTree/Inductive/Defs.lean: This change renames the file to Defs.lean as part of a refactoring to separate core definitions from proofs. It removes the functional_completeness and completeness theorems, narrowing the file's scope to inductive Merkle tree structures and their verification functions.
• VCVio/CryptoFoundations/MerkleTree/Vector/Basic.lean: This change reorganizes the library structure by moving the Merkle Tree implementation to a more specific directory for vector-based constructions. The file content is unchanged, meaning no new theorems, definitions, or proofs were added or modified.

---

Last updated: 2026-04-28 02:59 UTC.

[dtumad]

Looks good to me, thanks. By the way, the question a couple weeks ago about IsQueryBound led to a definition IsQueryBoundP that may be more useful for this use case if you still need that functionality.