[Vilin97]

Why

quality.py bans set_option textually, but PR #278 demonstrated a bypass: a custom elaborator calling

withOptions (fun options => options.set `maxRecDepth (100000 : Nat)) do ...

is semantically set_option maxRecDepth 100000, invisible to the textual gate. Requested by the maintainer; this PR closes that hole with two complementary layers plus coverage for adjacent backdoor classes discovered along the way.

Layer 1 — textual (fast, runs even with --skip-lean-axioms)

On comment/string-stripped content:

• programmatic option manipulation is forbidden — option-API tokens: withOptions, modifyOptions, MonadWithOptions, withRecDepth, withCurrHeartbeats, elabSetOption, setOptionFromString, modifyScope, KVMap.set*/insert*/erase*, Options.set*, Option.set(IfNotSet).
• gated option name in code is forbidden — any code occurrence of maxRecDepth / maxHeartbeats / maxSynthPendingDepth / linter.*. This catches receiver-variable spellings (options.set `` maxRecDepth``) the API list can't. Word boundaries keep maxRecDepth_bound and comment mentions legal.
• Lakefile: maxRecDepth joins the existing heartbeat ban in [leanOptions].

Layer 2 — Lean-native environment audit (_check_option_backdoors)

A standalone script run via lake env lean --run (same pattern as scripts/exposition/Extract.lean; importModules with extensions disabled, so project notation cannot interfere — importing the pool normally lets e.g. MRiscX's syntax break audit parsing). It walks every declaration compiled into a LeanPool.* module — including elab_rules auxiliaries and elaborator-generated declarations that the textual declaration parser cannot enumerate (so #print axioms never sees them) — and flags any that:

1. references an option-manipulating constant (resolved against the live env; candidates absent from the toolchain are skipped, so core renames degrade coverage instead of breaking the gate);
2. embeds a gated option-name string literal — Lean Name literals compile to string pieces, so `maxRecDepth, Name.mkStr1 "maxRecDepth", and Name.mkStr2 "linter" "…" all surface;
3. directly references an axiom-injecting constant (sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler);
4. is an axiom declared inside a pool module — on v4.32 native_decide compiles to a generated per-theorem axiom (no ofReduceBool reference anymore), and an elaborator calling addDecl (Declaration.axiomDecl …) is the same hole. Only the axiom kind is rejected: generated ._unsafe_rec / hygienic opaques / deriving helpers are sanctioned compiler output and carry kernel-checked values.

The audit fails closed: if the script stops compiling on a future toolchain, a missing completion marker is itself an error.

Validation

• Zero false positives: textual scan over all current pool sources and env audit over the entire built pool (~120 projects) both come back clean; the env audit costs ~10 s end-to-end. SetTheory (reflection tactic, registered simp attrs) and MRiscX (Hoare-logic elaborators) — the most metaprogramming-heavy projects — pass all arms.
• PR Import Erdos97ConvexOctagon: convex-octagon case of Erdős Problem 97 #278 caught: both textual rules fire on the real Lrat.lean line, and a probe module replicating its elaborator is caught in the env audit via Lean.MonadWithOptions.withOptions + Lean.Options.set + the "maxRecDepth" literal.
• Obfuscation caught: a variant assembling the option name at runtime (Name.mkSimple ("maxRec" ++ "Depth")) — invisible to any textual scan — is still caught by its Lean.KVMap.setNat reference; MonadRecDepth.withRecDepth 0 (counter reset) and native_decide's generated axiom are caught too.
• 187 pytest tests pass (7 new, incl. the verbatim PR Import Erdos97ConvexOctagon: convex-octagon case of Erdős Problem 97 #278 line); ruff check/format clean.

Residual risk (documented honestly)

An ephemeral backdoor that never persists a declaration (e.g. run_cmd driving elabCommand under withOptions) is invisible to the env audit — but its source must still spell a manipulator token or gated name, which the textual layer bans; assembling those from characters at runtime while also referencing no flagged constant would additionally have to dodge evalConst-style reflection (unusable here since unsafe is banned). The layers make the known channels fail loudly rather than prove absence; LLM review remains the judgment backstop.

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.