diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index 85aaad4821..a7fc342273 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -26,7 +26,8 @@ Current checks: - every `.lean` file under `LeanPool/`, plus `LeanPool.lean`, is reachable from `LeanPool.lean` - every content `.lean` file except `LeanPool.lean` has the exact four-line file header - content files do not contain `set_option`, `nolint` waivers, broad `import Mathlib`, `sorry`, `admit`, unchecked declarations (`axiom`, `constant`, `unsafe`, `partial`, `opaque`, `@[extern]`), or diagnostic commands (`#check`, `#print`, `#eval`, `#reduce`, `#guard_msgs`, `#lint`) -- Lake configuration does not pass forbidden option overrides, trace options, linter disables, or heartbeat overrides +- content files do not manipulate elaborator options programmatically: option-API tokens (`withOptions`, `modifyOptions`, `withRecDepth`, `withCurrHeartbeats`, `KVMap`/`Options`/`Option` setters, ...) and gated option names (`maxRecDepth`, `maxHeartbeats`, `maxSynthPendingDepth`, `linter.*`) are forbidden in code (comments are fine) — ``withOptions (fun o => o.set `maxRecDepth 100000)`` inside an elaborator is still `set_option maxRecDepth 100000` +- Lake configuration does not pass forbidden option overrides, trace options, linter disables, or heartbeat / recursion-depth overrides - the style-linter allowlist `scripts/nolints-style.txt` has no active entries - no Lean content file exceeds 10000 non-blank, non-comment code lines - no theorem/lemma proof body exceeds 200 non-blank, non-comment code lines, using the current text heuristic @@ -44,6 +45,7 @@ Current checks: - project entry modules and listed main declarations resolve in Lean - generated entry-point project cards match `LeanPool/projects.yml` - public declarations depend only on the allowed axiom set: `Classical.choice`, `propext`, and `Quot.sound` +- a Lean environment audit (run via `lake env lean --run` with extensions disabled, so project notation cannot interfere) walks **every** declaration compiled into a pool module — including elaborator auxiliaries and generated declarations the textual scans cannot see — and rejects any that references option-manipulating constants, embeds a gated option-name literal (however the `Name` was assembled), directly references an axiom-injecting constant (`sorryAx`, `ofReduceBool`, ...), or is itself an axiom declared inside a pool module (which is how `native_decide` and `addDecl`-of-an-axiom backdoors surface) The checker also has `--write-project-cards` to regenerate entry-point module docstrings from `LeanPool/projects.yml`. diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index f46016793f..6c1e4f5e22 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -56,6 +56,23 @@ FORBIDDEN_DIAGNOSTICS = re.compile( r"^\s*#(?:check|print|eval!?|reduce|guard_msgs|lint)\b" ) +# Programmatic option manipulation is semantically `set_option` (banned below) +# but invisible to that textual gate: PR #278 raised `maxRecDepth` from a +# custom elaborator via `withOptions (fun options => options.set `maxRecDepth +# (100000 : Nat))`. Two complementary layers close the gap: these patterns +# reject option-API tokens and gated option names in comment-stripped source, +# and the `_check_option_backdoors` environment audit rejects compiled +# declarations whose terms reference option-manipulating constants or embed +# gated option-name literals (catching spellings the text scan cannot see, +# e.g. names assembled from string literals). +FORBIDDEN_OPTION_APIS = re.compile( + r"\b(?:withOptions|modifyOptions|MonadWithOptions|withRecDepth" + r"|withCurrHeartbeats|elabSetOption|setOptionFromString|modifyScope" + r"|KVMap\.(?:set|insert|erase)\w*|Options\.set\w*|Option\.set(?:IfNotSet)?)\b" +) +FORBIDDEN_OPTION_NAMES = re.compile( + r"\b(?:maxRecDepth|maxHeartbeats|maxSynthPendingDepth)\b|\blinter\.[\w'.]+" +) FORBIDDEN_SOUNDNESS = re.compile( r"\b(?:axiom|constant|unsafe|partial|opaque)\b|@\[\s*extern\b" ) @@ -244,6 +261,22 @@ def _check_forbidden_lean_text(root: Path) -> list[_QualityError]: errors.append( _QualityError(path, line_number, "nolint waiver is forbidden") ) + if FORBIDDEN_OPTION_APIS.search(line): + errors.append( + _QualityError( + path, + line_number, + "programmatic option manipulation is forbidden", + ) + ) + if FORBIDDEN_OPTION_NAMES.search(line): + errors.append( + _QualityError( + path, + line_number, + "gated option name in code is forbidden", + ) + ) if re.match(r"^\s*(?:public\s+)?import\s+Mathlib\s*$", line): errors.append( _QualityError( @@ -274,6 +307,7 @@ def _check_lake_options(root: Path) -> list[_QualityError]: "heartbeat override": re.compile( r"\b(?:maxHeartbeats|synthInstance\.maxHeartbeats)\b" ), + "recursion-depth override": re.compile(r"\bmaxRecDepth\b"), "trace option": re.compile(r"\btrace\."), "autoImplicit enabled": re.compile( r"\b(?:relaxedAutoImplicit|autoImplicit)\s*=\s*true" @@ -435,6 +469,191 @@ def _qualify_name(namespace_stack: list[str], name: str) -> str: return ".".join([*namespace_stack, name]) +# Environment-level companion to FORBIDDEN_OPTION_APIS/FORBIDDEN_OPTION_NAMES: +# a standalone Lean script (same `lake env lean --run` pattern as +# scripts/exposition/Extract.lean). It imports the pool WITHOUT activating +# extensions, so project-defined notation cannot interfere with the audit, +# then walks every declaration compiled into a `LeanPool.*` module (including +# elaborator auxiliaries and generated declarations the textual declaration +# parser cannot see) and reports any that +# - references an option-manipulating constant, +# - embeds a gated option-name string literal (Lean `Name` literals compile +# to string pieces, so `` `maxRecDepth `` and `Name.mkStr1 "maxRecDepth"` +# 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 +# elaborator calling `addDecl (Declaration.axiomDecl ...)` is the same +# hole). +# Candidate constants absent from the current toolchain are skipped, so core +# renames degrade coverage rather than break the audit; the completion marker +# lets the Python side fail closed if the audit itself stops compiling. +_OPTION_AUDIT_FINDING_RE = re.compile( + r"LEANPOOL_OPTION_AUDIT\|([^|\s]+)\|([^|\s]+)\|([^\n]*)" +) +_OPTION_AUDIT_COMPLETE_MARKER = "LEANPOOL_OPTION_AUDIT_COMPLETE" +_OPTION_AUDIT_LEAN = """ +import Lean + +namespace LeanPoolQuality.OptionAudit + +open Lean + +def gatedFragments : List String := + ["maxRecDepth", "maxHeartbeats", "maxSynthPendingDepth", "linter."] + +def isGatedLiteral (s : String) : Bool := + s == "linter" + || gatedFragments.any fun fragment => (s.splitOn fragment).length > 1 + +def manipulatorCandidates : List Name := + [`Lean.MonadWithOptions.withOptions, `Lean.withOptions, `Lean.modifyOptions, + `Lean.MonadRecDepth.withRecDepth, + `Lean.withCurrHeartbeats, `Lean.Core.withCurrHeartbeats, + `Lean.KVMap.set, `Lean.KVMap.setBool, `Lean.KVMap.setNat, `Lean.KVMap.setInt, + `Lean.KVMap.setString, `Lean.KVMap.setName, `Lean.KVMap.setSyntax, + `Lean.KVMap.insert, `Lean.KVMap.insertCore, `Lean.KVMap.setEntry, + `Lean.KVMap.erase, + `Lean.Option.set, `Lean.Option.setIfNotSet, + `Lean.Options.set, `Lean.Options.setBool, `Lean.Options.setNat, + `Lean.Core.Context.mk, `Lean.Elab.Command.Scope.mk, + `Lean.Elab.Command.modifyScope, + `Lean.Elab.elabSetOption, `Lean.Elab.Command.elabSetOption, + `Lean.setOptionFromString, + `Lean.maxRecDepth, `Lean.maxHeartbeats, `maxRecDepth, `maxHeartbeats] + +def axiomInjectorCandidates : List Name := + [`sorryAx, `Lean.sorryAx, `Lean.ofReduceBool, `Lean.ofReduceNat, + `Lean.trustCompiler] + +/- Only the axiom kind is rejected: `opaque` and `partial`/`unsafe` +definitions carry kernel-checked values (and unsafe constants cannot appear +in proofs at all), and the compiler legitimately generates such companions +(`._unsafe_rec`, hygienic `ext._@...` opaques, `deriving` helpers) for +ordinary safe code. An axiom declared inside a pool module, by contrast, is +always a soundness hole — whether written via an elaborator calling `addDecl` +or generated by `native_decide`. -/ +def kindViolation? (info : ConstantInfo) : Option String := + match info with + | .axiomInfo _ => some "declares an axiom" + | _ => none + +def gatedLiteral? (e : Expr) : Option String := + match e.find? fun sub => + match sub with + | .lit (.strVal s) => isGatedLiteral s + | _ => false + with + | some (.lit (.strVal s)) => some s + | _ => none + +def auditEnv (env : Environment) : IO Unit := do + let manipulators := manipulatorCandidates.filter env.contains + let injectors := axiomInjectorCandidates.filter env.contains + let mut visited : NameSet := NameSet.empty + for (moduleName, data) in env.header.moduleNames.zip env.header.moduleData do + unless moduleName.getRoot == `LeanPool do continue + for declName in data.constNames do + unless visited.contains declName do + visited := visited.insert declName + if let some info := env.find? declName then + let exprs := info.type :: info.value?.toList + let used := exprs.foldl (fun acc e => acc ++ e.getUsedConstants) #[] + let mut details : List String := [] + let hits := manipulators.filter used.contains + unless hits.isEmpty do + let joined := ", ".intercalate (hits.map (·.toString)) + details := details.concat + s!"references forbidden option-manipulating constants: {joined}" + if let some s := exprs.findSome? gatedLiteral? then + details := details.concat + s!"embeds forbidden gated option name {repr s}" + let injectorHits := injectors.filter used.contains + unless injectorHits.isEmpty do + let joined := ", ".intercalate (injectorHits.map (·.toString)) + details := details.concat + s!"references forbidden axiom-injecting constants: {joined}" + if let some kindDetail := kindViolation? info then + details := details.concat kindDetail + unless details.isEmpty do + let joined := "; ".intercalate details + IO.println s!"LEANPOOL_OPTION_AUDIT|{moduleName}|{declName}|{joined}" + IO.println "LEANPOOL_OPTION_AUDIT_COMPLETE" + +end LeanPoolQuality.OptionAudit + +def main (args : List String) : IO UInt32 := do + let modules := if args.isEmpty then [`LeanPool] else args.map (·.toName) + Lean.initSearchPath (<- Lean.findSysroot) + let imports := modules.toArray.map fun module => ({ module } : Lean.Import) + let env <- Lean.importModules imports {} (trustLevel := 1024) + LeanPoolQuality.OptionAudit.auditEnv env + return 0 +""" + + +def _check_option_backdoors(root: Path) -> list[_QualityError]: + """Audit every declaration compiled into the pool for backdoors.""" + with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False) as temp_file: + temp_path = Path(temp_file.name) + temp_file.write(_OPTION_AUDIT_LEAN) + temp_file.flush() + + try: + try: + process = subprocess.run( + ["lake", "env", "lean", "--run", str(temp_path)], + cwd=root, + check=False, + capture_output=True, + text=True, + ) + except FileNotFoundError: + # `lake` not on PATH; surface a single advisory error rather + # than crashing the whole quality run. + return [ + _QualityError( + root / "LeanPool.lean", + 1, + "option-manipulation audit skipped: `lake` not found", + ) + ] + finally: + temp_path.unlink(missing_ok=True) + + return _parse_option_audit_output(root, process.stdout, process.stderr) + + +def _parse_option_audit_output( + root: Path, stdout: str, stderr: str +) -> list[_QualityError]: + """Turn environment-audit findings (and non-completion) into errors.""" + errors: list[_QualityError] = [] + for match in _OPTION_AUDIT_FINDING_RE.finditer(stdout): + module, declaration, detail = match.groups() + errors.append( + _QualityError( + _module_to_path(root, module), + 1, + f"{declaration} {detail.strip()}", + ) + ) + if _OPTION_AUDIT_COMPLETE_MARKER not in stdout: + snippet = stderr.strip().splitlines() + errors.append( + _QualityError( + root / "LeanPool.lean", + 1, + "option-manipulation audit did not complete: " + f"{snippet[0] if snippet else '(no stderr)'}", + ) + ) + return errors + + def _check_axioms(root: Path) -> list[_QualityError]: declarations = _parse_declarations(root) if not declarations: @@ -1066,6 +1285,7 @@ def run_checks(root: Path, *, skip_lean_axioms: bool = False) -> list[_QualityEr errors = [error for check in checks for error in check(root)] if not skip_lean_axioms: errors.extend(_check_axioms(root)) + errors.extend(_check_option_backdoors(root)) return sorted( errors, key=lambda error: (str(error.path), error.line, error.message) ) @@ -1082,7 +1302,8 @@ def _parse_args(argv: list[str]) -> argparse.Namespace: parser.add_argument( "--skip-lean-axioms", action="store_true", - help="Skip the Lean subprocess used for #print axioms.", + help="Skip the Lean subprocess used for #print axioms and the " + "option-manipulation environment audit.", ) parser.add_argument( "--write-project-cards", diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 1aabbb0030..ca856e1337 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -10,6 +10,7 @@ _axiom_audit_resolved, _Declaration, _parse_declarations, + _parse_option_audit_output, _project_card, _strip_lean_comments, _write_project_card, @@ -104,6 +105,121 @@ def test_quality_check_rejects_set_option(tmp_path: Path) -> None: assert any("set_option is forbidden" in error.message for error in errors) +def test_quality_check_rejects_programmatic_option_manipulation( + tmp_path: Path, +) -> None: + """The PR #278 bypass — `withOptions` in an elaborator — is rejected.""" + _write_minimal_repo( + tmp_path, + "elab_rules : command\n" + " | `(lrat_semantic) => do\n" + " Command.liftTermElabM do\n" + " withOptions (fun options => options.set `maxRecDepth" + " (100000 : Nat)) do\n" + " pure ()\n" + "\n" + "def hello := 1\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "programmatic option manipulation is forbidden" in error.message + for error in errors + ) + assert any( + "gated option name in code is forbidden" in error.message for error in errors + ) + + +def test_quality_check_rejects_gated_option_name_in_code(tmp_path: Path) -> None: + """Receiver-variable spellings like `opts.set` cannot slip through.""" + _write_minimal_repo( + tmp_path, + "def tweak (opts : Lean.Options) : Lean.Options :=\n" + " opts.set `maxHeartbeats 400000\n" + "\n" + "def hello := 1\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "gated option name in code is forbidden" in error.message for error in errors + ) + + +def test_quality_check_rejects_linter_option_name_in_code(tmp_path: Path) -> None: + """Backtick-quoted linter option names are programmatic waiver material.""" + _write_minimal_repo( + tmp_path, + "def waiver := `linter.unusedVariables\n\ndef hello := 1\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "gated option name in code is forbidden" in error.message for error in errors + ) + + +def test_quality_check_allows_option_names_in_comments_and_identifiers( + tmp_path: Path, +) -> None: + """Option talk in comments and names like `maxRecDepth_bound` are fine.""" + _write_minimal_repo( + tmp_path, + "-- a large `decide`; upstream increases `maxHeartbeats` to avoid timeouts\n" + "/- `withOptions` and `set_option maxRecDepth` are banned here. -/\n" + "theorem maxRecDepth_bound : 1 = 1 := rfl\n" + "\n" + "def hello := 1\n", + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert not any( + "programmatic option manipulation" in error.message for error in errors + ) + assert not any("gated option name" in error.message for error in errors) + + +def test_parse_option_audit_output_reports_findings(tmp_path: Path) -> None: + """Environment-audit findings map to the module's file with the detail.""" + stdout = ( + "LEANPOOL_OPTION_AUDIT|LeanPool.Evil.Lrat|Evil.elabRule|references " + "forbidden option-manipulating constants: " + "Lean.MonadWithOptions.withOptions; embeds forbidden gated option " + 'name "maxRecDepth"\n' + "LEANPOOL_OPTION_AUDIT_COMPLETE\n" + ) + + errors = _parse_option_audit_output(tmp_path, stdout, "") + + assert len(errors) == 1 + assert errors[0].path == tmp_path / "LeanPool" / "Evil" / "Lrat.lean" + assert ( + "Evil.elabRule references forbidden option-manipulating constants" + in errors[0].message + ) + + +def test_parse_option_audit_output_accepts_clean_run(tmp_path: Path) -> None: + """A completed audit with no findings yields no errors.""" + assert not _parse_option_audit_output( + tmp_path, "LEANPOOL_OPTION_AUDIT_COMPLETE\n", "" + ) + + +def test_parse_option_audit_output_fails_closed_without_marker(tmp_path: Path) -> None: + """A crashed or non-compiling audit must fail the run, not pass silently.""" + errors = _parse_option_audit_output(tmp_path, "", "error: script broke\nmore") + + assert len(errors) == 1 + assert "option-manipulation audit did not complete" in errors[0].message + assert "error: script broke" in errors[0].message + + def test_quality_check_rejects_nolint_attribute(tmp_path: Path) -> None: """Lean files may not waive linters with `@[nolint ...]`.""" _write_minimal_repo(