feat(MerkleTree/Inductive): reduce extractability to birthday - #365
Merged
alexanderlhicks merged 108 commits intoMay 20, 2026
Merged
Conversation
![lean-agent-app[bot]](https://github.githubassets.com/images/gravatars/gravatar-user-420.png){kind=avatar}
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…io birthday Add `Collision.lean` and `Extractability.lean` for inductive Merkle trees, copied from a downstream project and adapted to VCVio: - `collisionIn` predicate (two distinct hash-oracle log entries with equal responses) and bridge `collisionIn_imp_logHasCollision` to the `OracleComp.LogHasCollision` predicate from `VCVio/OracleComp/QueryTracking/Birthday.lean`. - `collision_probability_bound` is now a thin wrapper over `probEvent_logCollision_le_birthday_total`, taking `IsTotalQueryBound oa n` and concluding `n² / (2 · |α|)`. The original `IsPerIndexQueryBound oa (fun _ => n)` hypothesis is unprovable for `spec α := (α × α) →ₒ α` (per-index `n` over `|α|²` indices does not bound total log length to `n`), so the consumer in `Extractability.lean` is updated to thread a total bound through `extractability_game_IsTotalQueryBound` (still a `sorry`, was a `sorry` under the previous per-index name as well). Slight `n²` vs `n·(n-1)` slack relative to the textbook `C(n, 2) / |α|` form comes from the union-bound step in the underlying birthday lemma. Pre-existing issues in `extractability_game` (`verifyProof`/`extractedProof` expecting `List.Vector α idx.depth` rather than `List α`) are out of scope for this PR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🤖 PR SummaryMathematical Formalization
Infrastructure and Library Foundations
Proof Status
Statistics
Lean Declarations ✏️ **Removed:** 1 declaration(s)
✏️ **Added:** 45 declaration(s)
📋 **Additional Analysis**Attribution And File Headers\n\n- Incorrect Copyright Year: The copyright headers in the new files
|
…numina/inductive-merkle-collision-bound
…numina/inductive-merkle-collision-bound
The IsTotalQueryBound.of_bind_left lemma added in this branch is not used by the Merkle extractability work; spinning it off into a standalone PR. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
BoltonBailey
marked this pull request as ready for review
May 17, 2026 02:22
alexanderlhicks
approved these changes
May 20, 2026
alexanderlhicks
enabled auto-merge (squash)
May 20, 2026 16:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR finishes the extractability proof (for the inductively structured binary Merkle trees with single-branch opening proofs).
This follows the development of the SNARGs book for the definitions, but diverges somewhat in the proof, and proves a simpler but slightly looser soundness error bound.
I made most of the initial proof with Numina's Fuse app and Claude Code, IIRC it was around 1300 lines to start. At this point I have cleaned up the proof a lot from where it was at initially, and tried to create abstractions to express theorems more succinctly. I would be open to further golfing ideas, but I would also be open to just merging this and trying to do automated refactors later.