From db90366200726d092139f4371c027c55eb17ede5 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Sun, 25 Oct 2026 23:36:08 +0100 Subject: [PATCH 1/4] fix axiom-audit checker using Lean env rather than source parsing --- python/lean_pool/quality.py | 302 ++++++++++++++------------ python/tests/test_axiom_audit_lean.py | 112 ++++++++++ python/tests/test_quality.py | 244 ++++++++++++++++----- python/tests/test_validation_cache.py | 2 +- 4 files changed, 472 insertions(+), 188 deletions(-) create mode 100644 python/tests/test_axiom_audit_lean.py diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 7adf1cfdd9..74636bce24 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -3,6 +3,7 @@ from __future__ import annotations import argparse +import json import re import subprocess import sys @@ -419,6 +420,13 @@ def _declarations_in( rf"^\s*{DECLARATION_PREFIX}({keyword_pattern})\s+" rf"({LEAN_IDENT})(?![\w'.])" ) + # Match Lean's sectionHeader modifiers without interpreting their visibility. + # Missing an opening section makes its closing `end` pop a namespace instead. + section_pattern = re.compile( + rf"^\s*(?:@\[\s*expose\s*\]\s*)?" + rf"(?:public\s+)?(?:noncomputable\s+)?(?:meta\s+)?" + rf"section(?:\s+({LEAN_IDENT}))?\s*$" + ) for path in paths: # Track `namespace` and `section` opens together so that an # `end
` pops the section rather than the enclosing namespace. @@ -432,15 +440,24 @@ def _declarations_in( for line_number, line in enumerate(stripped.splitlines(), start=1): namespace_match = re.match(rf"^\s*namespace\s+({LEAN_IDENT})\s*$", line) if namespace_match: - scope_stack.append((True, namespace_match.group(1))) + # Lean opens one scope per name component, allowing both + # `end A.B` and `end B; end A` after `namespace A.B`. + scope_stack.extend( + (True, name) for name in namespace_match.group(1).split(".") + ) continue - section_match = re.match(rf"^\s*section(?:\s+({LEAN_IDENT}))?\s*$", line) + section_match = section_pattern.match(line) if section_match: - scope_stack.append((False, section_match.group(1))) + label = section_match.group(1) + scope_stack.extend( + (False, name) for name in (label.split(".") if label else [None]) + ) continue - if re.match(rf"^\s*end(?:\s+{LEAN_IDENT})?\s*$", line): - if scope_stack: - scope_stack.pop() + end_match = re.match(rf"^\s*end(?:\s+({LEAN_IDENT}))?\s*$", line) + if end_match: + label = end_match.group(1) + count = len(label.split(".")) if label else 1 + del scope_stack[-count:] continue match = decl_pattern.match(line) if match and not include_private and _is_private_declaration_line(line): @@ -488,10 +505,10 @@ def _qualify_name(namespace_stack: list[str], name: str) -> str: # both surface here), # - directly references an axiom-injecting constant (`sorryAx`, # `ofReduceBool`, ...), or -# - IS an axiom declared inside a pool module — this extends the -# `#print axioms` audit to declarations it cannot enumerate textually (on -# this toolchain `native_decide` compiles to a generated per-theorem -# axiom in the module, which is exactly what the kind check rejects; an +# - IS an axiom declared inside a pool module — independently of whether +# a public declaration depends on it (on this toolchain `native_decide` +# compiles to a generated per-theorem axiom in the module, which is +# exactly what the kind check rejects; an # elaborator calling `addDecl (Declaration.axiomDecl ...)` is the same # hole). # Candidate constants absent from the current toolchain are skipped, so core @@ -690,169 +707,183 @@ def _parse_option_audit_output( return errors +_AXIOM_AUDIT_PREFIX = "LEANPOOL_AXIOM_AUDIT|" +_AXIOM_AUDIT_LEAN = """ +import Lean + +open Lean Core + +def emitAxiomAudit (record : Json) : IO Unit := + IO.println s!"LEANPOOL_AXIOM_AUDIT|{record.compress}" + +def initializeAxiomCache (env : Environment) : IO Environment := do + -- collectAxioms needs its imported cache, but loadExts would also initialize + -- project extensions. Initialize only Lean's own axiom-cache extension. + let some ext := (← persistentEnvExtensionsRef.get).find? fun ext => + privateToUserName ext.name == `Lean.exportedAxiomsExt + | throw <| IO.userError "Lean's exported axiom-cache extension is unavailable" + let state := ext.toEnvExtension.getState (asyncMode := .sync) env + let imported ← ext.addImportedFn state.importedEntries { env, opts := {} } + return ext.toEnvExtension.setState (asyncMode := .sync) env + { state with state := imported } + +def auditAxioms (env : Environment) (modules : List Name) : CoreM Unit := do + let mut count := 0 + for (moduleName, data) in env.header.moduleNames.zip env.header.moduleData do + unless modules.contains moduleName do continue + for declName in data.constNames do + -- Private declarations are dependencies, not independent audit roots. + if isPrivateName declName then continue + unless env.contains declName do + throwError "missing declaration in audit environment: {declName}" + let axioms ← collectAxioms declName + let ranges ← findDeclarationRanges? declName + let line := ranges.map (·.range.pos.line) |>.getD 1 + liftM <| emitAxiomAudit <| Json.mkObj [ + ("kind", toJson "declaration"), ("module", toJson moduleName.toString), + ("name", toJson declName.toString), ("line", toJson line), + ("axioms", toJson (axioms.map Name.toString))] + count := count + 1 + liftM <| emitAxiomAudit <| Json.mkObj [ + ("kind", toJson "complete"), ("modules", toJson (modules.map Name.toString)), + ("declarations", toJson count)] + +def main : IO Unit := do + let input ← (← IO.getStdin).readToEnd + let json ← IO.ofExcept (Json.parse input) + let moduleStrings : List String ← IO.ofExcept (fromJson? json) + if moduleStrings.isEmpty then throw <| IO.userError "no modules to audit" + let modules := moduleStrings.map String.toName + Lean.initSearchPath (← Lean.findSysroot) + let imports := modules.toArray.map fun module => ({ module } : Lean.Import) + -- Load private bodies too: public declarations may depend on private helpers. + -- Do not activate project-defined extensions or execute their initializers. + let env ← Lean.importModules imports {} (trustLevel := 1024) (level := .private) + let env ← initializeAxiomCache env + for moduleName in modules do + unless env.header.moduleNames.contains moduleName do + throw <| IO.userError s!"missing module in audit environment: {moduleName}" + let _ ← CoreM.toIO (ctx := { fileName := "", fileMap := default }) + (s := { env }) (auditAxioms env modules) +""" + + def _check_axioms(root: Path) -> list[_QualityError]: - """Audit pooled declarations: allowlisted axioms only, never `sorry`.""" - return _audit_axioms( - root, - _parse_declarations(root), - [m for unit in pool_units(root) for m in unit] - if discovers_modules(root) - else "LeanPool", - ) + """Audit every non-private pool declaration, including generated declarations.""" + return _audit_axioms(root, [m for unit in pool_units(root) for m in unit]) -def _audit_axioms( - root: Path, - declarations: list[_Declaration], - import_module: str | list[str], -) -> list[_QualityError]: - """Run `#print axioms` over ``declarations`` and grade the results.""" - if not declarations: +def _audit_axioms(root: Path, modules: list[str]) -> list[_QualityError]: + """Enumerate compiled module declarations and collect their axioms in Lean.""" + if not modules: return [] - - modules = [import_module] if isinstance(import_module, str) else import_module index_path = _module_to_path(root, modules[0]) - commands = "".join(f"import {module}\n" for module in modules) + "\n".join( - f"#print axioms _root_.{declaration.name}" for declaration in declarations - ) with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: temp_path = Path(temp_file.name) - temp_file.write(commands) + temp_file.write(_AXIOM_AUDIT_LEAN) temp_file.flush() try: try: process = subprocess.run( - ["lake", "env", "lean", str(temp_path)], + ["lake", "env", "lean", "--run", str(temp_path)], cwd=root, check=False, capture_output=True, text=True, + input=json.dumps(modules), ) except FileNotFoundError: - # `lake` not on PATH; surface a single advisory error rather - # than crashing the whole quality run. return [ _QualityError( index_path, 1, - "axiom audit skipped: `lake` not found", + "axiom audit failed: `lake` not found", ) ] finally: temp_path.unlink(missing_ok=True) - errors = _parse_axiom_output(root, declarations, process.stdout) - resolved = _axiom_audit_resolved(process.stdout) - missing = [ - declaration for declaration in declarations if declaration.name not in resolved - ] - # Distinguish "Lean ran but couldn't resolve some declarations" (per-decl - # localization is useful) from "Lean failed before any #print axioms ran" - # (a single root-cause error is more useful than N copies). - if missing and not resolved and process.returncode != 0: - return errors + [ - _QualityError( - index_path, - 1, - f"axiom audit failed before any declaration was checked: " - f"{process.stderr.strip() or '(no stderr)'}", - ) - ] - errors.extend(_axiom_audit_missing(missing, process.stderr)) - return errors + return _parse_axiom_output( + root, modules, process.stdout, process.stderr, process.returncode + ) def _parse_axiom_output( root: Path, - declarations: list[_Declaration], + modules: list[str], output: str, + stderr: str = "", + returncode: int = 0, ) -> list[_QualityError]: + """Grade structured Lean results; fail closed on incomplete or invalid audits.""" errors: list[_QualityError] = [] - by_name = {declaration.name: declaration for declaration in declarations} - by_name.update( - {f"_root_.{declaration.name}": declaration for declaration in declarations} - ) - # Names may contain `'` (e.g. `foo'`); see _axiom_audit_resolved comment. - pattern = re.compile(r"^'(.+?)' depends on axioms: \[([^\]]*)\]", re.MULTILINE) - for match in pattern.finditer(output): - name = match.group(1) - if name not in by_name: - continue - declaration = by_name[name] - axioms = {item.strip() for item in match.group(2).split(",") if item.strip()} - errors.extend(_axiom_errors(declaration, name, axioms)) - return errors - - -def _axiom_errors( - declaration: _Declaration, name: str, axioms: set[str] -) -> list[_QualityError]: - """Grade one declaration's axiom set without proof-hole exceptions.""" - extra_axioms = sorted(axioms - ALLOWED_AXIOMS) - if not extra_axioms: - return [] - return [ - _QualityError( - declaration.path, - declaration.line, - f"{name} depends on unallowlisted axioms: {', '.join(extra_axioms)}", + try: + records = [ + json.loads(line.removeprefix(_AXIOM_AUDIT_PREFIX)) + for line in output.splitlines() + if line.startswith(_AXIOM_AUDIT_PREFIX) + ] + _validate_axiom_records(records, modules) + for record in records[:-1]: + extra = sorted(set(record["axioms"]) - ALLOWED_AXIOMS) + if extra: + errors.append( + _QualityError( + _module_to_path(root, record["module"]), + record["line"], + f"{record['name']} depends on unallowlisted axioms: " + f"{', '.join(extra)}", + ) + ) + except (ValueError, KeyError, TypeError) as exc: + errors.append( + _QualityError( + _module_to_path(root, modules[0]), + 1, + f"axiom audit did not complete: {exc}", + ) ) - ] - - -def _axiom_audit_resolved(stdout: str) -> set[str]: - """Return the set of declaration names that `#print axioms` resolved.""" - # `#print axioms NAME` produces one of two messages on stdout: - # 'NAME' depends on axioms: [a, b, c] - # 'NAME' does not depend on any axioms - # Both indicate the lookup resolved; only the first list is interesting - # for the trusted-axiom check, but both must count as "seen" so we don't - # emit a spurious "produced no result" for axiom-free declarations. - # - # Names may contain `'` (e.g. `foo'`), so we cannot use `[^']+` for the - # name. Use a non-greedy match anchored on `' ` (closing quote followed - # by space) — Lean always emits one space between the echoed name and - # the verb, and a name cannot end with whitespace. - pattern = re.compile( - r"^'(.+?)' (?:depends on axioms: \[|does not depend on any axioms)", - re.MULTILINE, - ) - resolved: set[str] = set() - for match in pattern.finditer(stdout): - name = match.group(1) - # Lean echoes back the qualified name we passed in; strip _root_. so it - # matches the unqualified names we collected via _parse_declarations. - if name.startswith("_root_."): - name = name[len("_root_.") :] - resolved.add(name) - return resolved - - -def _axiom_audit_missing( - missing: list[_Declaration], - stderr: str, -) -> list[_QualityError]: - """Emit one error per declaration that `#print axioms` could not resolve.""" - errors: list[_QualityError] = [] - for declaration in missing: - snippet = _stderr_snippet_for(stderr, declaration.name) - message = ( - f"axiom audit failed for {declaration.name}: {snippet}" - if snippet - else f"axiom audit produced no result for {declaration.name}" + if returncode: + detail = (stderr.strip() or output.strip() or "no diagnostics")[-2000:] + errors.append( + _QualityError( + _module_to_path(root, modules[0]), + 1, + f"axiom audit failed (exit {returncode}): {detail}", + ) ) - errors.append(_QualityError(declaration.path, declaration.line, message)) return errors -def _stderr_snippet_for(stderr: str, name: str) -> str: - """Find the most relevant stderr line mentioning `name`, or ''.""" - error_lines = [line for line in stderr.splitlines() if name in line] - for line in error_lines: - if "error" in line.lower(): - return line.strip() - return error_lines[0].strip() if error_lines else "" +def _validate_axiom_records(records: list[Any], modules: list[str]) -> None: + """Require complete coverage and well-formed, uniquely identified results.""" + if not records or not all(isinstance(record, dict) for record in records): + raise ValueError("missing completion record or invalid JSON records") + complete = records[-1] + if complete != { + "kind": "complete", + "modules": modules, + "declarations": len(records) - 1, + }: + raise ValueError("missing or inconsistent completion record") + seen: set[tuple[str, str]] = set() + for record in records[:-1]: + if ( + record.get("kind") != "declaration" + or record.get("module") not in modules + or not isinstance(record.get("name"), str) + or not record["name"] + or type(record.get("line")) is not int + or record["line"] < 1 + or not isinstance(record.get("axioms"), list) + or not all(isinstance(axiom, str) for axiom in record["axioms"]) + ): + raise ValueError("invalid declaration record") + key = (record["module"], record["name"]) + if key in seen: + raise ValueError(f"duplicate declaration record: {key}") + seen.add(key) def _load_projects_yaml( @@ -1513,12 +1544,11 @@ def _cached_pool_audits(root: Path, cache: ValidationCache) -> list[_QualityErro """Cover all pool declarations, with current static reachability checked above.""" errors: list[_QualityError] = [] for modules in pool_units(root): - paths = [_module_to_path(root, module) for module in modules] errors.extend( cache.check( "axioms", modules, - lambda: _audit_axioms(root, _declarations_in(paths), modules), + lambda: _audit_axioms(root, modules), ) ) errors.extend( diff --git a/python/tests/test_axiom_audit_lean.py b/python/tests/test_axiom_audit_lean.py new file mode 100644 index 0000000000..f087373924 --- /dev/null +++ b/python/tests/test_axiom_audit_lean.py @@ -0,0 +1,112 @@ +"""Exercise the axiom audit against real compiled legacy and module-system files.""" + +from __future__ import annotations + +import json +import os +import subprocess +from pathlib import Path +from unittest.mock import patch + +import pytest + +from lean_pool.quality import _AXIOM_AUDIT_PREFIX, _audit_axioms + + +def test_compiled_axiom_audit(tmp_path: Path) -> None: + """Audit public roots, including generated names, through private dependencies.""" + pin = (Path(__file__).resolve().parents[2] / "lean-toolchain").read_text().strip() + lake = ( + Path.home() + / ".elan/toolchains" + / pin.replace("/", "--").replace(":", "---") + / "bin/lake" + ) + if not lake.is_file(): + if os.environ.get("LEAN_POOL_REQUIRE_TEST_TOOLCHAIN") == "1": + pytest.fail("required pinned Lean toolchain unavailable") + pytest.skip("pinned Lean toolchain unavailable") + (tmp_path / "lean-toolchain").write_text(pin + "\n") + (tmp_path / "lakefile.toml").write_text( + 'name = "audit_fixture"\n' + '[[lean_lib]]\nname = "AuditModern"\n' + '[[lean_lib]]\nname = "AuditLegacy"\n' + '[[lean_lib]]\nname = "AuditLeaks"\n' + '[[lean_lib]]\nname = "AuditDependency"\n' + ) + (tmp_path / "AuditDependency.lean").write_text( + "axiom unusedImportedAxiom : False\n" + ) + (tmp_path / "AuditModern.lean").write_text( + "module\nimport Lean\nnamespace AuditModern\n" + "theorem hiddenUnused : False := by sorry\n" + "private theorem explicitlyPrivate : False := by sorry\n" + "axiom hiddenAxiom : False\n" + "public section\nnoncomputable section Local.Inner\n" + "theorem good : True := True.intro\n" + "theorem allowed (p q : Prop) (h : p ↔ q) : p = q := propext h\n" + "end Local.Inner\nend\nend AuditModern\n" + ) + (tmp_path / "AuditLegacy.lean").write_text( + "import Lean\nimport AuditDependency\nnamespace AuditLegacy\n" + 'initialize IO.eprintln "PROJECT_INITIALIZER_EXECUTED"\n' + "private theorem explicitlyPrivate : False := by sorry\n" + "theorem good : True := True.intro\n" + 'elab "makeAuditFact" : command => do\n' + " Lean.Elab.Command.elabCommand\n" + " (← `(theorem generatedFact : True := True.intro))\n" + "makeAuditFact\nend AuditLegacy\n" + ) + (tmp_path / "AuditLeaks.lean").write_text( + "module\nimport all AuditModern\nnamespace AuditLeaks\n" + "private theorem helper : False := AuditModern.hiddenUnused\n" + "public theorem leakedSorry : False := helper\n" + "public theorem leakedAxiom : False := AuditModern.hiddenAxiom\n" + "public axiom newAxiom : False\nend AuditLeaks\n" + ) + build = subprocess.run( + [str(lake), "build", "AuditModern", "AuditLegacy", "AuditLeaks"], + cwd=tmp_path, + capture_output=True, + text=True, + timeout=180, + ) + assert build.returncode == 0, build.stdout + build.stderr + processes: list[subprocess.CompletedProcess] = [] + original_run = subprocess.run + + def capture(command: list[str], **kwargs) -> subprocess.CompletedProcess: + command[0] = str(lake) + result = original_run(command, **kwargs, timeout=180) + processes.append(result) + return result + + with patch("lean_pool.quality.subprocess.run", side_effect=capture): + errors = _audit_axioms(tmp_path, ["AuditModern", "AuditLegacy", "AuditLeaks"]) + assert processes[0].returncode == 0, processes[0].stdout + processes[0].stderr + assert "PROJECT_INITIALIZER_EXECUTED" not in processes[0].stdout + assert "PROJECT_INITIALIZER_EXECUTED" not in processes[0].stderr + records = [ + json.loads(line.removeprefix(_AXIOM_AUDIT_PREFIX)) + for line in processes[0].stdout.splitlines() + if line.startswith(_AXIOM_AUDIT_PREFIX) + ] + names = {record["name"] for record in records[:-1]} + assert "AuditModern.good" in names + assert "AuditLegacy.good" in names + assert any("generatedFact" in name for name in names) + assert not any( + "hiddenUnused" in name or "explicitlyPrivate" in name for name in names + ) + assert "unusedImportedAxiom" not in names + assert len(errors) == 3, errors + by_name = {error.message.split(" depends on")[0]: error for error in errors} + assert set(by_name) == { + "AuditLeaks.leakedSorry", + "AuditLeaks.leakedAxiom", + "AuditLeaks.newAxiom", + } + assert "sorryAx" in by_name["AuditLeaks.leakedSorry"].message + assert "hiddenAxiom" in by_name["AuditLeaks.leakedAxiom"].message + assert by_name["AuditLeaks.leakedSorry"].path == tmp_path / "AuditLeaks.lean" + assert by_name["AuditLeaks.leakedSorry"].line == 5 diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 494b696542..3d4eb1fb5e 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -2,15 +2,15 @@ from __future__ import annotations +import json +import subprocess from pathlib import Path from unittest.mock import patch import pytest from lean_pool.quality import ( - _axiom_audit_missing, - _axiom_audit_resolved, - _Declaration, + _audit_axioms, _parse_axiom_output, _parse_declarations, _parse_option_audit_output, @@ -526,6 +526,84 @@ def test_quality_check_section_inside_namespace_keeps_namespace( assert "after" not in names +@pytest.mark.parametrize( + "header", + [ + f"{expose}{public}{noncomputable}{meta}section" + for expose in ("", "@[expose] ") + for public in ("", "public ") + for noncomputable in ("", "noncomputable ") + for meta in ("", "meta ") + ], +) +@pytest.mark.parametrize("label", ["", "LocalSection"]) +def test_quality_check_modified_section_keeps_namespace( + tmp_path: Path, header: str, label: str +) -> None: + """Every Lean section-header combination must balance its closing end.""" + suffix = f" {label}" if label else "" + _write_minimal_repo( + tmp_path, + "namespace Ns\n" + f"{header}{suffix}\n" + "theorem before : True := trivial\n" + "namespace Inner\n" + "theorem nested : True := trivial\n" + "end Inner\n" + f"end{suffix}\n" + "theorem after : True := trivial\n" + "end Ns\n" + "theorem outside : True := trivial\n", + ) + + names = [declaration.name for declaration in _parse_declarations(tmp_path)] + + assert names == ["Ns.before", "Ns.Inner.nested", "Ns.after", "outside"] + + +@pytest.mark.parametrize("opening", ["namespace A.B", "namespace A\nnamespace B"]) +@pytest.mark.parametrize("closing", ["end A.B", "end B\nend A"]) +def test_quality_check_dotted_namespace_scopes( + tmp_path: Path, opening: str, closing: str +) -> None: + """Dotted opens and ends represent one scope per name component.""" + _write_minimal_repo( + tmp_path, + "namespace Outer\n" + f"{opening}\n" + "theorem nested : True := trivial\n" + f"{closing}\n" + "theorem after : True := trivial\n" + "end Outer\n" + "theorem outside : True := trivial\n", + ) + + names = [declaration.name for declaration in _parse_declarations(tmp_path)] + + assert names == ["Outer.A.B.nested", "Outer.after", "outside"] + + +def test_quality_check_partial_namespace_end_and_dotted_section(tmp_path: Path) -> None: + """Ending one component preserves the rest; dotted section names also balance.""" + _write_minimal_repo( + tmp_path, + "namespace A.B\n" + "end B\n" + "section Local.Inner\n" + "theorem inside : True := trivial\n" + "end Inner\n" + "theorem middle : True := trivial\n" + "end Local\n" + "theorem after : True := trivial\n" + "end A\n" + "theorem outside : True := trivial\n", + ) + + names = [declaration.name for declaration in _parse_declarations(tmp_path)] + + assert names == ["A.inside", "A.middle", "A.after", "outside"] + + def test_quality_check_dotted_name_inside_namespace_is_qualified( tmp_path: Path, ) -> None: @@ -783,46 +861,108 @@ def test_quality_check_rejects_invalid_provenance(tmp_path: Path) -> None: assert any("invalid provenance" in error.message for error in errors) -def test_axiom_audit_resolved_parses_success_lines() -> None: - """`#print axioms` success lines populate the resolved set; _root_ stripped. +def _axiom_output( + declarations: list[dict], + modules: list[str] | None = None, +) -> str: + """Encode the environment audit's line-oriented JSON protocol.""" + modules = modules if modules is not None else ["LeanPool.Basic"] + complete = { + "kind": "complete", + "modules": modules, + "declarations": len(declarations), + } + return "".join( + "LEANPOOL_AXIOM_AUDIT|" + json.dumps(record) + "\n" + for record in [*declarations, complete] + ) - Both output forms must be recognized — the with-axioms list and the - axiom-free message that pure `def`s produce. - """ - stdout = ( - "'_root_.Foo.bar' depends on axioms: [Classical.choice, propext]\n" - "'baz' depends on axioms: []\n" - "'_root_.hello' does not depend on any axioms\n" - # Names ending in `'` are echoed by Lean as `'foo'' ...`; the parser - # must capture the prime, not stop at the embedded quote. - "'_root_.Ns.neg_one_pow_ne_zero'' does not depend on any axioms\n" - "'_root_.Ns.exp_poly_sub_prod'' depends on axioms: [propext]\n" - ) - - assert _axiom_audit_resolved(stdout) == { - "Foo.bar", - "baz", - "hello", - "Ns.neg_one_pow_ne_zero'", - "Ns.exp_poly_sub_prod'", + +def _axiom_record(name: str = "foo", axioms: list[str] | None = None) -> dict: + """Construct a declaration record with a compiler-provided source location.""" + return { + "kind": "declaration", + "module": "LeanPool.Basic", + "name": name, + "line": 12, + "axioms": axioms if axioms is not None else [], } -def test_axiom_audit_missing_attributes_stderr_to_each_declaration( - tmp_path: Path, +@pytest.mark.parametrize("name", ["foo", "Ns.foo'", "Ns.odd name|with punctuation"]) +@pytest.mark.parametrize("axioms", [[], ["propext", "Classical.choice", "Quot.sound"]]) +def test_axiom_audit_accepts_allowed_results( + tmp_path: Path, name: str, axioms: list[str] ) -> None: - """Per-declaration errors quote the matching stderr line.""" - decl_a = _Declaration(name="foo'", path=tmp_path / "A.lean", line=12, kind="lemma") - decl_b = _Declaration(name="bar", path=tmp_path / "B.lean", line=34, kind="lemma") - stderr = "/tmp/x.lean:5:0: error: unknown constant '_root_.foo''\n" + """JSON records need no Lean-name or pretty-printer parsing.""" + output = _axiom_output([_axiom_record(name, axioms)]) + assert _parse_axiom_output(tmp_path, ["LeanPool.Basic"], output) == [] - errors = _axiom_audit_missing([decl_a, decl_b], stderr) - assert len(errors) == 2 - assert errors[0].path == tmp_path / "A.lean" and errors[0].line == 12 - assert "unknown constant" in errors[0].message - assert errors[1].path == tmp_path / "B.lean" and errors[1].line == 34 - assert "produced no result" in errors[1].message +def test_axiom_audit_accepts_empty_module(tmp_path: Path) -> None: + """An explicitly completed module with no public declarations is valid.""" + assert _parse_axiom_output(tmp_path, ["LeanPool.Basic"], _axiom_output([])) == [] + + +@pytest.mark.parametrize( + "output", + [ + "", + "LEANPOOL_AXIOM_AUDIT|{broken JSON\n", + "LEANPOOL_AXIOM_AUDIT|[]\n", + _axiom_output([_axiom_record()]).splitlines()[0] + "\n", + _axiom_output([]).replace('"declarations": 0', '"declarations": 1'), + _axiom_output([], ["LeanPool.Other"]), + _axiom_output([_axiom_record(), _axiom_record()]), + _axiom_output([{**_axiom_record(), "module": "Mathlib.Other"}]), + _axiom_output([{**_axiom_record(), "line": -1}]), + _axiom_output([{**_axiom_record(), "axioms": "sorryAx"}]), + _axiom_output([{**_axiom_record(), "axioms": [None]}]), + ], +) +def test_axiom_audit_rejects_incomplete_or_invalid_output( + tmp_path: Path, output: str +) -> None: + """Malformed, partial, duplicate, or out-of-scope results fail closed.""" + errors = _parse_axiom_output(tmp_path, ["LeanPool.Basic"], output) + assert errors + assert "did not complete" in errors[0].message + + +def test_axiom_audit_rejects_nonzero_exit_with_completion(tmp_path: Path) -> None: + """A completion marker cannot conceal a subprocess failure.""" + errors = _parse_axiom_output( + tmp_path, ["LeanPool.Basic"], _axiom_output([]), "import failed", 1 + ) + assert len(errors) == 1 + assert "import failed" in errors[0].message + + +def test_axiom_audit_uses_environment_not_source_parser(tmp_path: Path) -> None: + """Only module names are passed to Lean; source declaration parsing is unused.""" + with ( + patch("lean_pool.quality._declarations_in", side_effect=AssertionError), + patch( + "lean_pool.quality.subprocess.run", + return_value=subprocess.CompletedProcess( + [], 0, _axiom_output([_axiom_record()]), "" + ), + ) as run, + ): + assert _audit_axioms(tmp_path, ["LeanPool.Basic"]) == [] + command = run.call_args.args[0] + assert command[:4] == ["lake", "env", "lean", "--run"] + assert json.loads(run.call_args.kwargs["input"]) == ["LeanPool.Basic"] + assert len(command) == 5 + assert not Path(command[4]).exists() + + +def test_axiom_audit_missing_lake_fails_closed(tmp_path: Path) -> None: + """A missing toolchain is an audit failure, not an implicit pass.""" + with patch("lean_pool.quality.subprocess.run", side_effect=FileNotFoundError): + errors = _audit_axioms(tmp_path, ["LeanPool.Basic"]) + assert len(errors) == 1 + assert "failed" in errors[0].message def test_quality_check_rejects_duplicate_slug(tmp_path: Path) -> None: @@ -957,16 +1097,15 @@ def test_quality_check_rejects_unproved_terms(tmp_path: Path, proof: str) -> Non def test_axiom_audit_rejects_sorry_axiom(tmp_path: Path) -> None: """A compiled proof hole fails even when textual checks cannot see it.""" - declaration = _Declaration( - "unfinished", tmp_path / "LeanPool/Basic.lean", 7, "theorem" - ) errors = _parse_axiom_output( tmp_path, - [declaration], - "'unfinished' depends on axioms: [propext, sorryAx]\n", + ["LeanPool.Basic"], + _axiom_output([_axiom_record("unfinished", ["propext", "sorryAx"])]), ) assert len(errors) == 1 assert "unallowlisted axioms: sorryAx" in errors[0].message + assert errors[0].path == tmp_path / "LeanPool/Basic.lean" + assert errors[0].line == 12 @pytest.mark.parametrize("name", ["unfinished", "unfinished.eq_def"]) @@ -983,18 +1122,21 @@ def test_environment_audit_rejects_proof_holes(tmp_path: Path, name: str) -> Non assert "sorryAx" in errors[0].message -@pytest.mark.parametrize("extra", ["", ",\n sorryAx", ",\n customAxiom"]) -def test_axiom_audit_reads_wrapped_lists(tmp_path: Path, extra: str) -> None: - """Lean's wrapped axiom output preserves both safe and forbidden findings.""" - declaration = _Declaration( - "Widget.long_theorem_name", tmp_path / "LeanPool/Widget.lean", 7, "theorem" - ) +@pytest.mark.parametrize("extra", [[], ["sorryAx"], ["customAxiom"]]) +def test_axiom_audit_reads_axiom_arrays(tmp_path: Path, extra: list[str]) -> None: + """Structured axiom arrays preserve both safe and forbidden findings.""" errors = _parse_axiom_output( tmp_path, - [declaration], - "'Widget.long_theorem_name' depends on axioms: [propext,\n" - f" Classical.choice,\n Quot.sound{extra}]\n", + ["LeanPool.Basic"], + _axiom_output( + [ + _axiom_record( + "Widget.long_theorem_name", + ["propext", "Classical.choice", "Quot.sound", *extra], + ) + ] + ), ) assert bool(errors) == bool(extra) if extra: - assert extra.split()[-1] in errors[0].message + assert extra[0] in errors[0].message diff --git a/python/tests/test_validation_cache.py b/python/tests/test_validation_cache.py index 2a9a6a5ed6..aa0f4df530 100644 --- a/python/tests/test_validation_cache.py +++ b/python/tests/test_validation_cache.py @@ -206,7 +206,7 @@ def test_quality_audits_cover_every_owned_module(repository: Path) -> None: patch("lean_pool.quality._run_option_audit", return_value=[]) as backdoors, ): assert _cached_pool_audits(repository, cache) == [] - assert [call.args[2] for call in axioms.call_args_list] == pool_units( + assert [call.args[1] for call in axioms.call_args_list] == pool_units( repository ) assert [ From 3eca1ade26d059edaf1e7556fbfe40c0a6d96f04 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Sun, 25 Oct 2026 23:46:33 +0100 Subject: [PATCH 2/4] remove leftover code from prev draft --- python/lean_pool/quality.py | 28 +++---------- python/tests/test_quality.py | 78 ------------------------------------ 2 files changed, 6 insertions(+), 100 deletions(-) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 74636bce24..36b5f7e45e 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -420,13 +420,6 @@ def _declarations_in( rf"^\s*{DECLARATION_PREFIX}({keyword_pattern})\s+" rf"({LEAN_IDENT})(?![\w'.])" ) - # Match Lean's sectionHeader modifiers without interpreting their visibility. - # Missing an opening section makes its closing `end` pop a namespace instead. - section_pattern = re.compile( - rf"^\s*(?:@\[\s*expose\s*\]\s*)?" - rf"(?:public\s+)?(?:noncomputable\s+)?(?:meta\s+)?" - rf"section(?:\s+({LEAN_IDENT}))?\s*$" - ) for path in paths: # Track `namespace` and `section` opens together so that an # `end
` pops the section rather than the enclosing namespace. @@ -440,24 +433,15 @@ def _declarations_in( for line_number, line in enumerate(stripped.splitlines(), start=1): namespace_match = re.match(rf"^\s*namespace\s+({LEAN_IDENT})\s*$", line) if namespace_match: - # Lean opens one scope per name component, allowing both - # `end A.B` and `end B; end A` after `namespace A.B`. - scope_stack.extend( - (True, name) for name in namespace_match.group(1).split(".") - ) + scope_stack.append((True, namespace_match.group(1))) continue - section_match = section_pattern.match(line) + section_match = re.match(rf"^\s*section(?:\s+({LEAN_IDENT}))?\s*$", line) if section_match: - label = section_match.group(1) - scope_stack.extend( - (False, name) for name in (label.split(".") if label else [None]) - ) + scope_stack.append((False, section_match.group(1))) continue - end_match = re.match(rf"^\s*end(?:\s+({LEAN_IDENT}))?\s*$", line) - if end_match: - label = end_match.group(1) - count = len(label.split(".")) if label else 1 - del scope_stack[-count:] + if re.match(rf"^\s*end(?:\s+{LEAN_IDENT})?\s*$", line): + if scope_stack: + scope_stack.pop() continue match = decl_pattern.match(line) if match and not include_private and _is_private_declaration_line(line): diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 3d4eb1fb5e..3fb7d128d6 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -526,84 +526,6 @@ def test_quality_check_section_inside_namespace_keeps_namespace( assert "after" not in names -@pytest.mark.parametrize( - "header", - [ - f"{expose}{public}{noncomputable}{meta}section" - for expose in ("", "@[expose] ") - for public in ("", "public ") - for noncomputable in ("", "noncomputable ") - for meta in ("", "meta ") - ], -) -@pytest.mark.parametrize("label", ["", "LocalSection"]) -def test_quality_check_modified_section_keeps_namespace( - tmp_path: Path, header: str, label: str -) -> None: - """Every Lean section-header combination must balance its closing end.""" - suffix = f" {label}" if label else "" - _write_minimal_repo( - tmp_path, - "namespace Ns\n" - f"{header}{suffix}\n" - "theorem before : True := trivial\n" - "namespace Inner\n" - "theorem nested : True := trivial\n" - "end Inner\n" - f"end{suffix}\n" - "theorem after : True := trivial\n" - "end Ns\n" - "theorem outside : True := trivial\n", - ) - - names = [declaration.name for declaration in _parse_declarations(tmp_path)] - - assert names == ["Ns.before", "Ns.Inner.nested", "Ns.after", "outside"] - - -@pytest.mark.parametrize("opening", ["namespace A.B", "namespace A\nnamespace B"]) -@pytest.mark.parametrize("closing", ["end A.B", "end B\nend A"]) -def test_quality_check_dotted_namespace_scopes( - tmp_path: Path, opening: str, closing: str -) -> None: - """Dotted opens and ends represent one scope per name component.""" - _write_minimal_repo( - tmp_path, - "namespace Outer\n" - f"{opening}\n" - "theorem nested : True := trivial\n" - f"{closing}\n" - "theorem after : True := trivial\n" - "end Outer\n" - "theorem outside : True := trivial\n", - ) - - names = [declaration.name for declaration in _parse_declarations(tmp_path)] - - assert names == ["Outer.A.B.nested", "Outer.after", "outside"] - - -def test_quality_check_partial_namespace_end_and_dotted_section(tmp_path: Path) -> None: - """Ending one component preserves the rest; dotted section names also balance.""" - _write_minimal_repo( - tmp_path, - "namespace A.B\n" - "end B\n" - "section Local.Inner\n" - "theorem inside : True := trivial\n" - "end Inner\n" - "theorem middle : True := trivial\n" - "end Local\n" - "theorem after : True := trivial\n" - "end A\n" - "theorem outside : True := trivial\n", - ) - - names = [declaration.name for declaration in _parse_declarations(tmp_path)] - - assert names == ["A.inside", "A.middle", "A.after", "outside"] - - def test_quality_check_dotted_name_inside_namespace_is_qualified( tmp_path: Path, ) -> None: From 0f93970f914358e5c46696e27b4512ff488a2d15 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Sun, 25 Oct 2026 23:50:22 +0100 Subject: [PATCH 3/4] move to Lean CI step --- .github/workflows/lean_action_ci.yml | 9 ++++++--- python/tests/test_ci_cache_contract.py | 21 +++++++++++++++++++++ 2 files changed, 27 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 9911b4185a..07ad15f0cf 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -258,7 +258,8 @@ jobs: run: >- uv run --project python --group test pytest -q python/tests/test_ci_pr_build.py python/tests/test_indexes.py - -k 'test_lake_' + python/tests/test_axiom_audit_lean.py + -k 'test_lake_ or test_compiled_axiom_audit' - name: Install Mathlib cache id: mathlib-cache @@ -608,7 +609,8 @@ jobs: run: >- uv run --project python --group test pytest -q python/tests/test_ci_pr_build.py python/tests/test_indexes.py - -k 'test_lake_' + python/tests/test_axiom_audit_lean.py + -k 'test_lake_ or test_compiled_axiom_audit' - name: Install Mathlib cache id: mathlib-cache @@ -882,7 +884,8 @@ jobs: run: >- uv run --project python --group test pytest -q python/tests/test_ci_pr_build.py python/tests/test_indexes.py - -k 'test_lake_' + python/tests/test_axiom_audit_lean.py + -k 'test_lake_ or test_compiled_axiom_audit' - name: Install Mathlib cache run: | diff --git a/python/tests/test_ci_cache_contract.py b/python/tests/test_ci_cache_contract.py index cbfd2c2956..0090af2e6e 100644 --- a/python/tests/test_ci_cache_contract.py +++ b/python/tests/test_ci_cache_contract.py @@ -3,6 +3,7 @@ from __future__ import annotations import os +import shlex import subprocess from pathlib import Path @@ -651,6 +652,8 @@ def test_scoped_checks_handle_large_diffs(tmp_path, filename): ("lake-manifest.json", "true", "false", True), ("python/lean_pool/ci_pr_build.py", "true", "false", True), ("python/tests/test_ci_pr_build.py", "true", "false", True), + ("python/lean_pool/quality.py", "true", "false", True), + ("python/tests/test_axiom_audit_lean.py", "true", "false", True), ('"python/lean_pool/quoted.py"', "true", "false", True), ("scripts/ProjectIndexes.lean", "true", "false", True), ("scripts/exposition/Extract.lean", "true", "false", True), @@ -695,6 +698,24 @@ def test_dependency_tracking_tests_scope( assert tracking["if"] == "needs.plan.outputs.dependency_tests == 'true'" +@pytest.mark.parametrize("job_name", ["build", "finalize", "rebase"]) +def test_pinned_lean_ci_runs_compiled_axiom_audit(job_name: str) -> None: + """The compiled axiom fixture must run rather than silently skip in CI.""" + jobs = yaml.safe_load((WORKFLOWS / "lean_action_ci.yml").read_text())["jobs"] + step = next( + step + for step in jobs[job_name]["steps"] + if step.get("name") + == "Check compiled artifact dependency tracking with pinned Lean" + ) + assert step["env"]["LEAN_POOL_REQUIRE_TEST_TOOLCHAIN"] == "1" + command = shlex.split(step["run"]) + assert "python/tests/test_axiom_audit_lean.py" in command + assert command[command.index("-k") + 1] == ( + "test_lake_ or test_compiled_axiom_audit" + ) + + def test_profiling_is_automatic_and_cache_pruning_is_scheduled() -> None: """PRs get advisory profiles while cache maintenance stays scheduled.""" profiling = yaml.safe_load((WORKFLOWS / "proof-profile.yml").read_text()) From e9e4f76a943d8502d5de02c4fbd5c0cede7dd782 Mon Sep 17 00:00:00 2001 From: David Loeffler Date: Mon, 26 Oct 2026 08:04:22 +0100 Subject: [PATCH 4/4] filter out unsafe defs (`deriving Repr` etc) --- python/lean_pool/quality.py | 9 +++++--- python/tests/test_axiom_audit_lean.py | 30 +++++++++++++++++++++++++-- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 36b5f7e45e..7f215c6ca3 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -718,8 +718,11 @@ def auditAxioms (env : Environment) (modules : List Name) : CoreM Unit := do for declName in data.constNames do -- Private declarations are dependencies, not independent audit roots. if isPrivateName declName then continue - unless env.contains declName do - throwError "missing declaration in audit environment: {declName}" + let some info := env.find? declName + | throwError "missing declaration in audit environment: {declName}" + -- Compiler-generated executable code may contain proof-erasure axioms. + -- Unsafe constants cannot be dependencies of ordinary kernel proofs. + if info.isUnsafe then continue let axioms ← collectAxioms declName let ranges ← findDeclarationRanges? declName let line := ranges.map (·.range.pos.line) |>.getD 1 @@ -753,7 +756,7 @@ def main : IO Unit := do def _check_axioms(root: Path) -> list[_QualityError]: - """Audit every non-private pool declaration, including generated declarations.""" + """Audit safe, non-private pool declarations, including generated declarations.""" return _audit_axioms(root, [m for unit in pool_units(root) for m in unit]) diff --git a/python/tests/test_axiom_audit_lean.py b/python/tests/test_axiom_audit_lean.py index f087373924..bb2a79a8ab 100644 --- a/python/tests/test_axiom_audit_lean.py +++ b/python/tests/test_axiom_audit_lean.py @@ -33,6 +33,7 @@ def test_compiled_axiom_audit(tmp_path: Path) -> None: '[[lean_lib]]\nname = "AuditLegacy"\n' '[[lean_lib]]\nname = "AuditLeaks"\n' '[[lean_lib]]\nname = "AuditDependency"\n' + '[[lean_lib]]\nname = "AuditSmuggled"\n' ) (tmp_path / "AuditDependency.lean").write_text( "axiom unusedImportedAxiom : False\n" @@ -44,6 +45,7 @@ def test_compiled_axiom_audit(tmp_path: Path) -> None: "axiom hiddenAxiom : False\n" "public section\nnoncomputable section Local.Inner\n" "theorem good : True := True.intro\n" + "unsafe def unsafeProof : False := lcProof\n" "theorem allowed (p q : Prop) (h : p ↔ q) : p = q := propext h\n" "end Local.Inner\nend\nend AuditModern\n" ) @@ -52,6 +54,7 @@ def test_compiled_axiom_audit(tmp_path: Path) -> None: 'initialize IO.eprintln "PROJECT_INITIALIZER_EXECUTED"\n' "private theorem explicitlyPrivate : False := by sorry\n" "theorem good : True := True.intro\n" + "unsafe def runtime._aux_1 : False := lcProof\n" 'elab "makeAuditFact" : command => do\n' " Lean.Elab.Command.elabCommand\n" " (← `(theorem generatedFact : True := True.intro))\n" @@ -62,7 +65,8 @@ def test_compiled_axiom_audit(tmp_path: Path) -> None: "private theorem helper : False := AuditModern.hiddenUnused\n" "public theorem leakedSorry : False := helper\n" "public theorem leakedAxiom : False := AuditModern.hiddenAxiom\n" - "public axiom newAxiom : False\nend AuditLeaks\n" + "public axiom newAxiom : False\n" + "public theorem named._aux_1 : False := helper\nend AuditLeaks\n" ) build = subprocess.run( [str(lake), "build", "AuditModern", "AuditLegacy", "AuditLeaks"], @@ -99,14 +103,36 @@ def capture(command: list[str], **kwargs) -> subprocess.CompletedProcess: "hiddenUnused" in name or "explicitlyPrivate" in name for name in names ) assert "unusedImportedAxiom" not in names - assert len(errors) == 3, errors + assert "AuditModern.unsafeProof" not in names + assert "AuditLegacy.runtime._aux_1" not in names + assert len(errors) == 4, errors by_name = {error.message.split(" depends on")[0]: error for error in errors} assert set(by_name) == { "AuditLeaks.leakedSorry", "AuditLeaks.leakedAxiom", "AuditLeaks.newAxiom", + "AuditLeaks.named._aux_1", } assert "sorryAx" in by_name["AuditLeaks.leakedSorry"].message assert "hiddenAxiom" in by_name["AuditLeaks.leakedAxiom"].message + assert "sorryAx" in by_name["AuditLeaks.named._aux_1"].message assert by_name["AuditLeaks.leakedSorry"].path == tmp_path / "AuditLeaks.lean" assert by_name["AuditLeaks.leakedSorry"].line == 5 + + # Skipping unsafe audit roots must not let one prove a safe theorem with them. + (tmp_path / "AuditSmuggled.lean").write_text( + "module\nimport AuditModern\n" + "public theorem smuggled : False := AuditModern.unsafeProof\n" + ) + rejected = subprocess.run( + [str(lake), "build", "AuditSmuggled"], + cwd=tmp_path, + capture_output=True, + text=True, + timeout=180, + ) + assert rejected.returncode != 0 + diagnostics = rejected.stdout + rejected.stderr + assert "unsafe" in diagnostics.lower() + assert "AuditModern.unsafeProof" in diagnostics + assert "AuditSmuggled.lean:3:" in diagnostics