fix(Security): pin the tree-based extractor and guard distinctShape arity - #1
Open
Eduardogbg wants to merge 18 commits into
Open
fix(Security): pin the tree-based extractor and guard distinctShape arity#1Eduardogbg wants to merge 18 commits into
Eduardogbg wants to merge 18 commits into
Conversation
Eduardogbg
force-pushed
the
fix/tree-special-sound-pinned
branch
from
July 15, 2026 07:08
2590dce to
9fe7c32
Compare
* fix(blueprint): repair LaTeX/bibtex errors breaking blueprint PDF build
The docs workflow has failed on main since ~2026-07-10. Three defects in
blueprint/src caused latexmk to exit non-zero:
- hachi_subfield.tex: math ($\cong$, $\sigma_{-1}$, ...) in section/
subsection titles reached hyperref's PDF-bookmark string, and \cong
triggered a fatal "Improper alphabetic constant". Wrapped the math in
\texorpdfstring{}{} with plain-text fallbacks.
- hachi_subfield.tex: undefined macro \inv in a lemma body. Rewrote as
standard inverse notation.
- references.bib: duplicate @misc{NOZ26} entry made bibtex error out,
leaving all citations unresolved. Removed the redundant copy.
`leanblueprint pdf` and `leanblueprint web` now both exit 0.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
* ci(docs): replace hand-rolled blueprint pipeline with docgen-action
The docs workflow built the blueprint and API docs with a bespoke
xu-cheng/texlive-action invocation, a brittle `pygraphviz==1.14` pin, and
manual deploy assembly -- a setup that has broken repeatedly.
Replace it with the maintained leanprover-community/docgen-action, the
standard used by leanblueprint's own template and mathlib-adjacent blueprint
projects. It drives doc-gen4 through the isolated `docbuild` layout doc-gen4
recommends, installs pygraphviz robustly, builds the blueprint, runs
`checkdecls`, and deploys -- all without custom plumbing.
Also:
- Add a `pull_request` trigger. The action gates deploy/upload to `push`, so
PRs now get a validation-only blueprint + checkdecls build. This would have
caught the LaTeX/bibtex regression fixed in the previous commit before it
reached main.
- ArkLib's static `home_page/` is published via `build-page: false` (no Jekyll
needed); `references` points at `blueprint/src/references.bib`.
- Document the CI flow and blueprint LaTeX gotchas in the wiki.
Note: this drops scripts/inject_nav.py's cross-page nav injection, which had
no equivalent in the standard action.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
* ci(docs): pin docs workflow actions to latest, Dependabot-trackable refs
- actions/checkout v5 -> v7 (latest; matches the rest of the repo's workflows)
- jlumbroso/free-disk-space v1.3.0 -> v1.3.1 (latest)
- leanprover/lean-action stays at v1.5.0 (latest)
- docgen-action stays SHA-pinned at current main HEAD (2026-06-07): it ships no
tags/releases, so a SHA is the only immutable, Dependabot-trackable ref.
github-actions Dependabot is already configured (.github/dependabot.yml,
monthly), and tracks both the version tags and the docgen-action SHA pin.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
* fix(blueprint): repair stale \lean{} references so checkdecls passes
The docs job now runs `lake exe checkdecls blueprint/lean_decls` via
docgen-action — a validation the old hand-rolled pipeline never ran.
It surfaced 21 `\lean{}` tags across 6 blueprint sources that no longer
resolve after VCVio/ArkLib refactors. `lean_decls` is regenerated from
these tags by `leanblueprint web` in CI, so the source .tex is the fix.
Renames / namespace fixes (declaration exists under a new name):
InterleavedCode -> Code.interleavedCodeSet
smoothCode -> ReedSolomon.smoothCode
constrainedCode -> ReedSolomon.constrainedCode
multiConstrainedCode -> ReedSolomon.multiConstrainedCode
proximityMeasure -> ProximityGap.proximityMeasure
proximityGap -> ProximityGap.proximityGap
emptySpec -> OracleSpec.emptySpec
OracleSpec.OracleQuery -> OracleQuery
OracleComp.evalDist -> evalDist
loggingOracle/cachingOracle-> OracleSpec.loggingOracle/cachingOracle
randomOracle -> OracleSpec.randomOracle
Folding.polyFold -> Polynomial.FoldingPolynomial.polyFold
Commented out (declaration removed or not yet formalized; prose kept):
singletonSpec (a notation, not a declaration)
UniPoly, MlPoly (removed from ArkLib)
CheckClaim.oracleReduction_completeness (commented out in source)
Folding.{exists_unique_bivariate,degree_bound_bivariate,fold,folding}
Verified: `lake exe checkdecls` on the repointed names resolves cleanly
against the v4.31.0 ArkLib environment.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
* CWSS protocol infrastructure * clean up * remove classical * fix merge * fix PR review
…rtial reorg of Hachi folder (Verified-zkEVM#626) * CWSS protocol infrastructure * qudaratic eq messy * clean up * remove classical * CWSSPackage for (more) readble CWSS composition * huge commit * merge * composition plan * address PR review * add paper def for relout Fig. 3 --------- Co-authored-by: Alexander Hicks <25369263+alexanderlhicks@users.noreply.github.com>
* CWSS protocol infrastructure * qudaratic eq messy * clean up * remove classical * CWSSPackage for (more) readble CWSS composition * huge commit * merge * composition plan * initial skeleton * address PR review * add paper def for relout Fig. 3 * skeleton * skeleton site * move hachi artifact * prove milestone skill * update hachi plan
* Remove old whir altogether * Fix docs
* Degree-2 folding that avoids using `log`. * Address comments
…fied-zkEVM#592) Grant the Build Timing Report job the permissions it uses: `actions: read`, `contents: read`, and `pull-requests: write`. Scope them to the `report` job and remove the redundant `issues` permission. Keep expected PR comment API failures (HTTP 403, 404, 410, 422, and 429) non-blocking while recording the status and message and preserving the rendered report in the job summary. Unexpected JavaScript errors and unexpected HTTP statuses still fail. Consolidates the permission fix from Verified-zkEVM#632.
Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
* Preliminary cleanup of RS * Some improvement to RS code file
Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
…mized for this repo) (Verified-zkEVM#666) Both AI PR workflows deploy lean4repo-utils@0.3 with default models, built up from the canonical README example and then optimized for this repo: - review: ChatOps-only (/review from a repo member), review@0.3, OPENROUTER_KEY. - summary: every-PR pull_request_target, summary@0.3, OPENROUTER_KEY. Repo-specific optimization: review restores the KB citation-join (maps changed .lean files to their cited docs/kb papers -> spec_refs); summary keeps validate_title + upstream_path ArkLib/ToMathlib/. Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Expose treeSpecialSoundWith at a concrete extractor while preserving treeSpecialSound as its existential closure, certified by treeSpecialSound_iff via Iff.rfl. Add an identity-verifier witness for the diagonal relation and guard the axiom reports for every new or changed declaration. No sorries are added.
Eduardogbg
force-pushed
the
fix/tree-special-sound-pinned
branch
from
July 30, 2026 06:11
9fe7c32 to
bb1d78d
Compare
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
5 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 former combined change has been split into two reviewable fork branches:
fix/distinct-shape-arity-guardcontains only the
{k // 2 ≤ k}guard and the correspondingSecurity/Implications.leanbridge adjustments.fix/tree-special-sound-pinned(this PR's current head) contains only the pinned-extractor refactor, its identity-verifier
non-vacuity witness, guarded axiom reports, and the prepared upstream texts.
The refreshed, project-lead-ready texts are committed on the pinning branch:
The texts lead with the unperformed work, include the current upstream hash and line
references, cite upstream PR Verified-zkEVM#602's concrete extractor construction and the existing
hkhypothesis in
Implications.lean, and quote this wave's probe, targeted-build, axiom, andsorry-delta results. No new fork PRs were opened.