feat(scripts): kernel-level axiom sweep with committed regression baseline

[alexanderlhicks]

What

Adds lake exe axiomsweep: kernel-level axiom / sorry accounting for the whole library, with a committed regression baseline.

The tool loads the built .olean environment (the same data the kernel checked) and computes, for every declaration under the swept root modules, the set of axioms it transitively depends on — i.e. the #print axioms information, library-wide, in one pass. Because it reads elaborated data rather than source text, it sees exactly what the kernel accepted: private declarations, macro-generated declarations, and instances included; no regex heuristics.

Why

CompPoly is a correctness-critical dependency of downstream provers (ArkLib pins it), and until now had no kernel-level accounting: source greps report 6 sorry tokens on main, but all of them sit inside comments — the kernel truth is that the library is fully clean, and this PR both proves that and adds the gate that keeps it true. Reviews of downstream repos have repeatedly found theorems that silently inherit sorryAx through framework stubs; this class of defect becomes mechanical to catch at the source.

How

• scripts/AxiomSweep.lean (+ lean_exe axiomsweep in the lakefile): memoised traversal of the compiled environment; only imports core Lean, runtime-imports the built oleans, so it needs a completed lake build and adds no dependencies. Runs in seconds.
• scripts/axiom_baseline.json: the currently-known sorryAx-tainted declarations (and any non-standard-axiom dependents). --check fails iff a declaration is tainted that the baseline does not list; closing gaps stays green and prints a nudge to shrink the baseline via --update-baseline.
• CI: one report-only step after the build (::warning on regression). Flip to enforcing by deleting the || echo once the baseline has soaked for a few PRs.
• Docs updated in the same PR.

Modes

lake exe axiomsweep                     # summary
lake exe axiomsweep --out report.json   # full per-declaration report (name, module, kind, line, axioms)
lake exe axiomsweep --check             # regression gate against scripts/axiom_baseline.json
lake exe axiomsweep --update-baseline   # refresh the baseline; commit the diff
lake exe axiomsweep --root Foo          # override the swept root modules (repeatable)

Baseline at this commit

• 7,589 declarations across 275 CompPoly.* modules.
• 0 sorryAx-tainted, 0 non-standard-axiom-tainted — fully kernel-clean. (Source greps see 6 sorry tokens on main; all are in comments — exactly the false positive a kernel-level census kills.)
• Spot-checked against #print axioms (CPolynomial.Raw.divModByMonicAux_go_fst_canonical → classical trio only); --check exit codes verified.

Notes

• Same tool as ArkLib's alh/axiom-sweep branch (multi-root variant); the copies are intentionally self-contained per repo, mirroring how other scripts are shared across the org. If it proves its keep everywhere, extracting a shared home is a possible follow-up.
• lean4export was considered and deliberately not used: it targets external kernel checking, has no source positions, and would add a per-toolchain pinned dependency; walking the environment yields the same information with line numbers and zero new deps.
• The per-declaration report is not committed anywhere; only the baseline is tracked.

Adversarial review

Five independent adversarial reviewers (one per repo deployment) attacked the tool, wiring, and baselines before this PR was opened. Everything they confirmed is fixed in the follow-up commit on this branch:

• Collector defect (HIGH, confirmed in 4 repos): the one-pass DFS finalized self-referencing constants (every inductive/ctor pair) prematurely, producing per-declaration rows that diverged from #print axioms in both directions, with constructible shapes where a new sorry passed --check. Fixed with a fixpoint-repair phase computing the true kernel closure (now strictly more accurate than #print axioms, whose own CollectAxioms wobbles inside mutual families). Post-fix rows spot-verified against ground truth; sorry-sets unchanged everywhere.
• Axiom types now traversed (CollectAxioms parity); duplicate constNames rows deduped; native_decide axiom names normalized to their owning declaration (the ax_N_M counters are Elab.async/toolchain-volatile); --check/--update-baseline mutually exclusive; bare Lean.ofReduceBool/Lean.trustCompiler are never baselinable (floor).
• CI steps now distinguish taint findings (report-only during soak) from infrastructure failures (always fail).
• Known blind spots documented: structure-field defaults and examples never enter any environment walk (#print axioms included); unimported files are invisible — paired with each repo's import-completeness gate.

What survived attack unchanged: baseline determinism (byte-identical regeneration), all headline numbers, spot-checks vs #print axioms, gate exit-code semantics, and the CI/step placement.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

sorry delta: +4 (4 added) — proof obligations increased

Pull request objective: Add a kernel-level axiom and sorry accounting tool (lake exe axiomsweep) for the entire CompPoly.* module tree, with a committed regression baseline (scripts/axiom_baseline.json) and a report-only CI gate. The tool reads the built .olean environment to compute transitive axiom dependencies for all reportable declarations, avoiding source-level false positives (the PR notes that 6 sorry tokens on main are all in comments; the library is kernel-clean). The PR also includes documentation updates (AGENTS.md, quickstart, generated-files, scripts README) and a lean_exe definition in the lakefile. No sorrys or admits are added in the implementation code.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	410
❌ Lines Removed	2

---

Lean Declarations

✏️ Added: 17 declaration(s)

scripts/AxiomSweep.lean (17)

• def buildEntries (roots : Array Name) : CoreM (Array Entry × Nat)
• def currentBaseline (entries : Array Entry) : Baseline where
• def dedupSort (a : Array String) : Array String
• def defaultRoots : Array Name
• def isReportable (n : Name) : Bool
• def isStandard (a : String) : Bool
• def kindOf : ConstantInfo → String
• def neverAllowlistable (a : String) : Bool
• def nonstandardOf (e : Entry) : Array String
• def normalizeAxiomName (s : String) : String
• def parseArgs : List String → Config → Except String Config
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32
• def sorryAxName : String
• def standardAxioms : List Name
• partial def collect (env : Environment) (stack : List Name) (gray : Std.HashSet Name)
• partial def repair (env : Environment) (order : Array Name)
• unsafe def main (args : List String) : IO UInt32

---

sorry Tracking

❌ Added: 4 `sorry`(s)

scripts/AxiomSweep.lean (4)

• def currentBaseline (entries : Array Entry) : Baseline where (L226)
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32 (L243)
• def runCheck (cur : Baseline) (basePath : String) : IO UInt32 (L244)
• partial def repair (env : Environment) (order : Array Name) (L143)

---

📋 **Additional Analysis**

The diff largely adheres to the CompPoly style guide and contribution conventions. The main violations are line-length exceedances in scripts/AxiomSweep.lean (several lines exceed the 100-character limit). All other style points (naming, indentation, module layout, documentation updates) are compliant. The CI, documentation, and lakefile changes are consistent with the project's workflows.

---

📄 **Per-File Summaries**

• .github/workflows/lean_action_ci.yml: Added an "Axiom sweep (report-only)" step that runs lake exe axiomsweep --check to detect new axiom or sorry taint. During the initial soak period, exit code 1 (taint found) produces only a warning, while infrastructure failures (exit codes other than 0 or 1) cause the step to fail, preventing silent decay of the soak. This step is intended to be flipped to enforcing later.
• AGENTS.md: The AGENTS.md file gained a new step 6 in the 'How To Contribute' section. It instructs contributors to run lake exe axiomsweep --check when adding or filling a sorry, and to refresh and commit the scripts/axiom_baseline.json with lake exe axiomsweep --update-baseline if the axiom change is intentional. This adds a workflow step for explicitly tracking and verifying the project's axiom baseline.
• docs/wiki/generated-files.md: This change adds a new entry to the generated files documentation mapping table, documenting that scripts/axiom_baseline.json is a generated and committed file. It describes its purpose as a kernel-level axiom/sorry regression baseline, specifies the regeneration command (lake exe axiomsweep --update-baseline after a built lake build), notes that the diff should be committed in the same PR that intentionally adds or removes taint, and indicates that it is checked by the report-only axiom-sweep CI step.
• docs/wiki/quickstart.md: The diff adds a new subsection to the quickstart guide documenting a workflow for handling sorry-filling and axiom-clean work, including commands to run axiomsweep (which checks CompPoly-scoped declarations for new sorryAx or non-standard-axiom taint against a committed baseline) and to update the baseline with --update-baseline. It also updates the CI description to mention that the CI pipeline now runs the axiom sweep in report-only mode, and adds lake exe axiomsweep --check to the list of direct debugging commands.
• lakefile.lean: Added a new lean_exe target named axiomsweep in lakefile.lean. The executable is located under scripts/ (with srcDir := "scripts"), its root module is AxiomSweep, and it has supportInterpreter := true. The accompanying docstring explains that this binary performs kernel-level axiom / sorry accounting against a committed regression baseline stored in scripts/axiom_baseline.json, and that it runtime-imports the built CompPoly oleans (so it must be run after lake build).
• scripts/AxiomSweep.lean: Adds scripts/AxiomSweep.lean, a whole-library kernel-level axiom and sorry accounting tool. It defines collect and repair to compute transitive axiom closures for all declarations under root modules (default CompPoly), exposes structures Entry, NonstandardEntry, and Baseline for serialisable reports, and implements CLI modes (--out, --check, --update-baseline) to gate CI against a committed baseline (scripts/axiom_baseline.json). Also introduces normalizeAxiomName, dedupSort, isReportable, neverAllowlistable, and helper functions; no sorry or admit appear in the implementation.
• scripts/README.md: The scripts/README.md documentation was updated to add two new entries. First, a command-line invocation for the axiomsweep executable (lake exe axiomsweep --check) was added to the list of main helper scripts, positioned after the existing check-docs-integrity.py command. Second, a new subsection ### AxiomSweep.lean was added under the "Script Inventory" section, documenting that the executable performs kernel-level axiom and sorry accounting for every reportable CompPoly.* declaration using the built .olean environment against a committed regression baseline (axiom_baseline.json), and describing the behavior of the three modes: --check (fails only on new taint), --update-baseline (refreshes the baseline), and --out FILE (writes a per-declaration report), with a pointer to the module docstring for further details on modes and known blind spots.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): scripts/axiom_baseline.json

---

Last updated: 2026-08-11 10:46 UTC.

[github-actions]

Build Timing Report

• Commit: 917ecd1
• Message: Merge 6818d79 into 42b414a
• Ref: alh/axiom-sweep
• Comparison baseline: 530605d from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: library build (warm) lake build; test path lake test.
• Clean build was skipped (warm/incremental CI; no toolchain or lake-manifest change). Runs automatically when lean-toolchain or lake-manifest.json changes, or via Actions → Lean Action CI → Run workflow with clean_build.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Library build (warm)	48.25	50.14	+1.89	ok
Test path	8.94	9.01	+0.07	ok

Incremental Rebuild Signal

• Warm-only run: default CI reuses cached oleans and rebuilds dirty modules only. No same-job clean:warm ratio.

Slowest Current Build Files (warm library build)

Showing 20 slowest current targets from the warm library build log, with comparison against the baseline warm library build log when available.

Current (s)	Baseline (s)	Delta (s)	Path
9.90	8.80	+1.10	CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Correctness.lean
6.70	5.20	+1.50	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Combinations.lean
6.40	5.10	+1.30	CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Correctness.lean
6.20	4.70	+1.50	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Completeness.lean
5.90	6.40	-0.50	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Basis.lean
5.50	5.20	+0.30	CompPoly/Bivariate/GuruswamiSudan/CoreCorrectness.lean
5.40	5.20	+0.20	CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Lemmas.lean
5.30	5.10	+0.20	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Rows.lean
4.30	3.10	+1.20	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Selection.lean
4.20	3.60	+0.60	CompPoly/Univariate/CoefficientInterpolation.lean
4.20	4.10	+0.10	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Divisibility.lean
4.00	4.50	-0.50	CompPoly/Bivariate/GuruswamiSudan/Root/Common/Lemmas.lean
3.90	3.80	+0.10	CompPoly/Bivariate/GuruswamiSudan/Root/FieldRoots/KoalaBear.lean
3.50	3.10	+0.40	CompPoly/Univariate/Roots/SmoothSubgroup/Correctness.lean
3.50	2.70	+0.80	CompPoly/Bivariate/GuruswamiSudan/Root/ShiftedSubstitution/Lemmas.lean
3.40	3.00	+0.40	CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Algorithm.lean
3.20	2.50	+0.70	CompPoly/Bivariate/GuruswamiSudan/Root/RothRuckenstein/Algorithm.lean
3.20	3.10	+0.10	CompPoly/Bivariate/GuruswamiSudan/Root/Alekhnovich/Lemmas.lean
3.10	2.90	+0.20	CompPoly/Bivariate/GuruswamiSudan/Interpolation/LeeOSullivan/Correctness/Soundness.lean
2.90	3.10	-0.20	CompPoly/Bivariate/GuruswamiSudan/FilterCorrectness.lean

[dhsorens]

so, I added a sorry to test the axiom sweep in commit 530605d above. the check fails but the CI is still green. is this expected behavior @alexanderlhicks ? I would probably prefer it generate a comment or sth so that it reports something when it fails

[dhsorens]

(removed the sorry in 6818d79)