# Specification of Regula

[`README.md`](../README.md#purpose-and-constraint) states Regula's purpose and the owner's constraint on all work. [The trusted base](#the-trusted-base) states what this revision rests on, and [the run of the checker](#the-run-of-the-checker) what is proved of its effects.

This document states what Regula's checks are, what each is proved to do, and what stays assumed. It follows the order that the owner chose: first a small proved core, then [a check](#the-language-check) that reads each source file before anything is compiled and refuses anything outside a closed set of allowed constructs. [The confirmation record](confirmation.md) holds the owner's words.

## How to read this document

Each claim about Lean, Lake or the theorems of this package has one of four marks:

- **Proved**: Lean checks a theorem of the Lean package in this directory. The theorem name follows the mark.
- **Measured**: an observation on the pinned toolchain, with its procedure.
- **Assumed**: a behaviour of Lean, Lake or the operating system that a verdict relies on and that no proof here examines. Each is an entry of [the list of assumptions](#the-trusted-base), and its name follows the mark, as in **Assumed** (`files`).
- **Open**: an obligation that this document does not discharge.

A statement about Lean's or Lake's source that explains a design, and that no verdict relies on, says that it is read from the source, with its lines.

A statement of what a rule or the checker must do is specification, and it has no mark. A citation such as `Lean/Meta/Native.lean:45` is a path below `src/` of the tag `v4.35.0` of Lean, the toolchain that `lean-toolchain` pins, and one that starts with `Lake/` is a path below `src/lake/` of that tag. To check all statements and theorems, run `lake build --wfail` in this directory. The Lean library `RegulaSpecification` requires lean-intent at the commit that `lakefile.toml` names, and the root package.

## What the owner's intent requires

Each row is a requirement of the owner's confirmed intent, and the formal claim that carries it.

| Requirement | Formal claim |
| --- | --- |
| Regula's checks are exactly RG1001 to RG1006, RG1010, RG1011, RG1012 and RG2001. RG1011 and RG1012 are the checks added after `v0.13.0` ([2026-11-03](confirmation.md#2026-11-03-the-rule-on-replaced-compiled-code), [2026-11-04](confirmation.md#2026-11-04-the-rule-on-hidden-panics)). | **Proved**: `rule_spellings`, the spellings of the rules of the checker's registry, `Regula.Closed.spellings_nodup`, that no two of them share a spelling and none is RG1010 or RG2001, and `registry_rules`, that the specification's registry is the checker's. RG1010 and RG2001 read no constant, so they are no rules of the registry: `full_gate_lines` and `proof_verdict_lines` state, word for word, the lines that name them. |
| It refuses a project whose declarations depend on `sorry`. | **Proved**: `rg1002_exact`, `rg1002_cases`. |
| It refuses a project axiom. | **Proved**: `rg1001_exact`, `rg1001_cases`, and `rg1003_exact` for its use. |
| It refuses `native_decide`. | **Proved**: `rg1004_exact`, `rg1004_cases`. |
| It refuses an axiom outside the allowed profile. | **Proved**: `rg1005_exact`, `rg1005_cases`. |
| It refuses an `unsafe` or `partial` declaration without the exempted form of a recursion helper. | **Proved**: `rg1006_exact`, `rg1006_cases` (see [RG1006](#rg1006-unsafe-and-partial-declarations)). |
| It refuses a constant of a claimed module that has a recursion helper's name without the exempted form, in any spelling that declares it. A recursive definition that Lean elaborates still passes. | **Proved**: `rg1006_exact`, `rg1006_reports_named_not_partial`, `rg1006_checker_refuses_forged_name`, and `rg1006_admits_helper` for a constant of the form, which names no origin. **Measured**: what Lean adds for a recursive definition has that form. |
| A constant of the exempted form cannot change what the proof verdict claims, which [what a pass means](#what-a-pass-means) states. | **Proved under H6**: `helperForm_unreached`, `safe_reach_safe`, with `SafeMentionsSafe`, a hypothesis about Lean's kernel with its pinned source (see [what a function of Lean or Lake is relied on for](#what-a-function-of-lean-or-lake-is-relied-on-for)). |
| It refuses an input it cannot load. | **Proved**: `admit_ok_iff`, `admit_error_iff`, `run_refused`, for the input, and `decision_failed`, `decision_pass` for a failed load. |
| Each rule refuses every violation and only violations, over Regula's input. | **Proved**: each `rgN_exact` is an equivalence, and `rgN_meets` states it as the rule's intent record. |
| It refuses a claimed constant whose value directly mentions `Lean.Loop.mk` or `repeatM`, so `while` and `repeat` in claimed code. | **Proved** of the mention: `rg1006_exact`, `rg1006_checker_refuses_loop`. **Measured**: that `while` and `repeat` give such a mention. |
| It refuses a constant of a claimed module that has `@[implemented_by]` or `@[extern]`, so that a compiled program does not run, in place of a claimed definition, code that no proof is about. It does not refuse `@[csimp]`, whose theorem states that the replacement equals the original, for the reason and with the limits that [RG1011](#rg1011-replaced-compiled-code) states. | **Proved**: `rg1011_exact`, `rg1011_cases`, `rg1011_checker_refuses_extern`, and `rg1011_admits_neither` for a constant with neither attribute, `@[csimp]` or not. **Proved** of the environment: `pass_iff`, through `EnvFloor`, and `pass_held`, through `ModuleUnreplaced`, for every claimed module's own attribute entries. **Assumed** (`leanImport`): that the queries and module entries report the attributes, see [RG1011](#rg1011-replaced-compiled-code). **Measured**: what a build with each attribute gives, under [RG1011](#rg1011-replaced-compiled-code). |
| It refuses a definition or opaque constant of a claimed module whose value mentions a panic form: one of Lean's four panic functions, or a constant that is no theorem and whose name's last string component contains `!`, so `xs[i]!`, `Option.get!`, `List.head!`, `String.toNat!`, `Array.back!`, `Array.set!`, `panic!`, `unreachable!` and `assert!` in claimed code. It does not refuse `xs[i]?`, `dbg_trace` or a theorem, for the reasons and with the limits that [RG1012](#rg1012-hidden-panics) states ([2026-11-04](confirmation.md#2026-11-04-the-rule-on-hidden-panics)). | **Proved**: `rg1012_exact`, `rg1012_cases`, `rg1012_checker_refuses_panic`, `rg1012_admits_theorems`, `bangNamed_hygienic`, `not_bangNamed_query`. **Proved** of the environment: `pass_iff`, through `EnvFloor`, and `pass_held`. **Measured**: what each listed form elaborates to, and how many constants of the toolchain the name admits that cannot panic, under [RG1012](#rg1012-hidden-panics). |
| A checker that refuses nothing does not satisfy this. | **Proved**: `silent_fails`, `noisy_fails` and each `rgN_noisy`; `always_pass_fails`, `always_incomplete_fails`. |
| A pass is the verdict of the rules. | **Proved**: `run_complete`, `run_pass_iff`, `run_meets`. |
| Each rule is a module of its own that imports a shared core and no other rule, and one registry lists the rules, with a theorem proved once that a run passes exactly when no registered rule reports a subject. Since the checker's package cannot depend on lean-intent, a rule is a pair of modules, its check in that package and its statement and proofs in this one, with one line in each package's registry and the two registries proved equal ([2026-11-03](confirmation.md#2026-11-03-each-rule-a-module-of-its-own)). | **Proved**: `Regula.Closed.report_pass_iff` and `Regula.Closed.mem_findings` over the list the run uses, `registry_rules`, `findings_nil_iff`, and `registered_found`, that each registered rule's refused case puts a finding of that rule among the run's findings. That no rule module imports another is read from the imports, and what a change rebuilds from Lake's output, under [the shape of a rule](#the-shape-of-a-rule). |
| A pass is a statement about the environment that Lean loaded, not only about the input. | **Proved**: `pass_iff`, `pass_floor`, `pass_held`, see [from a build to the input](#from-a-build-to-the-input). |
| Before anything is compiled, the check admits a project exactly when everything it reads is in the closed set, over every `Lean.Syntax`. | **Proved**: `decision_admitted_iff`, `mem_offenders_iff`, `mem_positions_iff`. That it reads every file, and reads what Lean reads, is the reader's: see [H1 and H2](#h1-and-h2). |
| It refuses, compiling nothing, and a build follows only the check, for an admitted project alone. | **Proved**: `gate_meets`, `build_only_after_check`, for the definition that runs. **Measured** below. |
| Only a project with no dependency in its Lake configuration and no Mathlib in its imports gets the full verdict, and the output says which it gave. | **Proved**: `dependency_not_admitted`, `mathlib_not_admitted`, `full_needs_no_mathlib`, `gate_exit_zero_iff`, and, word for word and apart from the code's text, `proof_verdict_lines`, `full_gate_lines`, `verdicts_named`, `pass_lines_name_subject`, for the output. |
| Every build gets a proof verdict, so its replay in Lean's kernel holds the claim's cone and nothing else: each constant of a claimed module, each constant that one reaches through what each mentions, in its type, its value, its inductive type's block and its quotient's `Eq`, and the constants that the kernel builds into a term, into an empty environment. A pass of `Regula.Shell.run` needs the kernel to accept each of them. | **Proved**: `replayConstants_env`, `mem_cone_env`, `inCone_mentions`, `claimed_inCone`, `plain_exit_zero`, `full_exit_zero`. **Assumed** (`replay`): what Lean's replay answers. **Measured**: a project that imports Mathlib, under [what a pass means](#what-a-pass-means). |
| Each example of the owner's restatement is refused or admitted by the decision that runs, stated apart from its tables, so a table replaced by a constant fails a build. | **Proved** over the parser's node kinds or the decision's input: `refuses_named_kinds`, `refuses_decide_native`, `refuses_lakefile_lean`, `refuses_plugin_key`, `admits_library_code`, in [`Proofs/Owner.lean`](RegulaSpecification/Proofs/Owner.lean). That those kinds are what the parser gives for those constructs is **measured** under [what was measured](#what-was-measured), and that the trees are what Lean elaborates is H1. **Observed**, and no theorem: that Regula's own core is admitted, by the gate's step that runs the full gate on this checkout. `core_configuration_admitted` states only its configuration's part. |
| The only unproved code left in what decides a verdict makes no decision. | **Proved**: `run_meets`, `executed_meets`, `table_rows`, and `allowed_iff` and `check_ok_iff` for the check of `Regula.ProgramCheck.Effects`, in [the run of the checker](#the-run-of-the-checker). `main` of `Regula.LintMain` is read from the code, and each selection is listed under [what a function of Lean or Lake is relied on for](#what-a-function-of-lean-or-lake-is-relied-on-for). |
| A run refuses or reports incomplete only for what a response said about something the requested build needs, asked after the preparation that the run itself supplies, so an unrelated failure or an unprepared operation cannot supply its reason. | **Proved over requests and responses**: `FullRun` combines `Reason` with `ReadingPreparation`, `BuildProtocol` and `RulesPreparation`; `PlainRun` adds `PlainPreparation`. `run_meets` proves these for the actual definitions on every response. `manufacturedCopy_fails` and `manufacturedCopyAnswered_fails` exclude the reported obstruction; the phase relations constrain the whole class. Effects inside external calls and consistency among responses remain outside this guarantee. |
| A full verdict's admission is about what the build consumes: the text the run's requests leave in the tree at the build, which the file system answered, is the text judged, in the context judged, and a run that leaves another text there has no admission to cite. | **Proved of every program that meets the record, and of `Regula.Shell.run` by `run_meets`**: `FullRun.gate_stands`, `FullRun.at_consumer`, `FullRun.judged_at_consumer`, `FullRun.answered_at_consumer`, `Evidence.judged`, `read_what_lake_compiles`, `uncheckedCopy_fails`, `uncheckedCopy_build_fails`, `act_after_readBack_fails`, with `judgedCopy_stands` and `rewritten_stands` for what the record still admits. That Lake reads the tree as it stands is H3, and the rest of [the trusted base](#the-trusted-base) says what else it rests on. |
| Regula publishes a closed list of refusals, and a refusal is never untrue of what Lean, Lake or the operating system answered. That is what "no false refusal" means. It does not mean that every reasonable project passes. | **Proved over requests and responses**: `Reason`, `PlainReason`, `TreeReason` and `BuildRejected` are closed, and `run_meets` proves that a run of `Regula.Shell.run` that ends and does not pass rests on them, on every response. A run that a call holds gives no answer at all, which is [outside the contract](#the-closed-list-of-refusals). See [the closed list of refusals](#the-closed-list-of-refusals). |
| A default executable, a `srcDir` on a target, and a source directory with a space or a non-ASCII name are refused, each with a true message. | **Proved**: `openPaths_of_notLibrary`, `refused_target_srcDir`, `openPaths_of_openDir`, `closedSourceDir_of_char`, `space_not_closed`, `nonAscii_not_closed`, with `open_path_not_admitted` for what `openPaths` gives. **Measured** on the `lake new` application template: [what was measured](#what-was-measured). |
| What Lake takes as its configuration in the tree is the `lakefile.toml` judged, by what the file system answers after the reading's last act through the name Lake looks for. | **Proved over requests and responses**: `FullRun.config_at_consumer`, with `ReadBack`, on one answer for each real path. **Proved under H5**: `lake_takes_judged`, with `LakeSelection`, which `lakeSelection_model` shows met. |
| A run with no refusal, whose rules hold, passes, so a program that refuses everything does not meet the contract. | **Proved conditionally**: `plain_owed`, `full_owed`, `run_plain_owed`, `run_full_owed` require the absence of the defined reasons and the loaded environment's floor. Preparation is a separate obligation of the run record, not a premise that reasons are absent. `pass_iff_floor` states the loader's pure equivalence. |
| Every behaviour of Lean, Lake or the operating system that a verdict relies on is on one list, named once with its pinned source, or is outside the contract, and the build fails for a new operation, route or premise until the list holds it, and for a new toolchain until each entry is read again. | **Proved**: `Assumption.ofOp`, a `match` over the closed type `Op`, `run_route`, `meaning`, `readAt_pinned`, `each_relied_on`, and a check of the release that builds the list. See [the trusted base](#the-trusted-base). |
| The claim holds only for named configurations: the pinned toolchain, the published way to run each verdict, and the platforms on which the assumptions were observed. | Stated in [the named configurations](#the-named-configurations). **Proved** of the toolchain: `supportsLean_iff` and `profileOfRun_lean`, so a run on another Lean is a refusal. `Route` names the ways to run. The platforms have no theorem. |
| A program of the repository that can certify a change or select what is validated decides nothing that no proof covers. | **Proved**: `runLocal_zero` and `runStep_ran` of the gate, `main_runs` and `main_zero` of the listing, `check_ok_iff` of the check of effects, in [the repository's programs](#the-repositorys-programs). |

The rest of this document follows from those requirements, or is marked as decided on the owner's behalf.

## The shape of a rule

Each rule is a pure function from the closed input to the constants that it reports, and a pair of modules. Its check is `Regula.Rules.RGnnnn` below [`lean/Regula/Rules/`](../lean/Regula/Rules/), a value of `Regula.Closed.Rule` whose one import of the checker's modules is its core, `Regula.Rule`, with every table that the rule alone reads. Its statement and proofs are `RegulaSpecification.Rules.RGnnnn` below [`RegulaSpecification/Rules/`](RegulaSpecification/Rules/), which imports only this package's core, `RegulaSpecification.Rule`, and the rule's own check. No rule's module imports another rule's. The checker's registry, `Regula.Closed.registry` in [`lean/Regula/Rules.lean`](../lean/Regula/Rules.lean), lists the rules that a run applies, in the order of their findings, and stamps each finding with its rule's spelling. This package's registry, `registry` in [`RegulaSpecification/Rules.lean`](RegulaSpecification/Rules.lean), lists each rule as a value of `Proved`: the rule that the checker runs, its violation predicate, the proof that its check reports exactly the violations, and its cases. `registry_rules` proves the two lists one, by `rfl`, so a rule that one registry holds and the other does not stops the build. [`CONTRIBUTING.md`](../CONTRIBUTING.md#adding-a-rule) gives the procedure for adding a rule.

**Measured** on 2026-11-03, with Lake's own output on an incremental build of both packages that were up to date at the change's commit, one edit at a time, each restored before the next. A one-line edit of `Regula.Rules.RG1003.check`, its finding's text, rebuilt in the checker's package only that module, its object file and the `lint` executable: the registry and the shell were not rebuilt, because a `module` file's importer sees the check's type and not its unexposed body, and Lake traces an import of a `module` file by its public `.olean` (`Lake/Build/Module.lean:343-344` and `:511` at v4.35.0). In this package it rebuilt 31 modules: RG1003's own and the 30 that import it, directly or not. A one-line edit of `rg1003_exact`'s proof that changes its proof term rebuilt nothing in the checker's package and 26 modules here: RG1003's own and the 25 that import it. Neither edit rebuilt another rule's module. This package's files are not `module` files, so Lake traces their imports by every artifact of each module they reach (`Lake/Build/Module.lean:325-328`), and most of this package lies downstream of the registries: at that commit, 30 of its 50 modules downstream of a rule's check, and 25 downstream of a rule's statement. The gate builds both packages from clean and does not use this: on 2026-11-03 the owner decided to keep it so, since reuse would save about 14 s of its 146 s on a one-rule change ([the record](confirmation.md#2026-11-03-the-local-gate)).

Its formal statement is a lean-intent intent record (`LeanIntent.IntentRecord`), built by `ruleRecord` in [`RegulaSpecification/RuleRecord.lean`](RegulaSpecification/RuleRecord.lean). The record has one property: on each well-formed input, the function reports a subject exactly when the subject violates the rule. Thus the meaning of a rule is all in its violation predicate, for example `Violates1005`.

For each rule, the package gives a case that the rule must refuse and a case that it must admit (`Witnessed`). From them, it proves that the record meets lean-intent's obligations O2 (at confirmation and before a run), O3, O4, and O5 with the freedom `SameReports`, which is the order and the repetition of the reported subjects. A rule's function takes the proof of the closed form with its input (`Checker`), so the record has no case for an input that the admission refuses. **Proved**: `adequate`, applied in `rg1001_adequate` and the theorems that follow it. O1 holds for each record. **Proved** by lean-intent: `LeanIntent.o1_wellTyped`.

Each rule function that the checker runs is proved against its record in its own module below [`RegulaSpecification/Rules/`](RegulaSpecification/Rules/) (`rgN_exact`, `rgN_meets`, `rgN_cases`). The functions run over `Regula.Closed.Input`, so the proofs are about the executed definitions, not about a copy of them.

These theorems have no hypothesis about the input or about the tables that a rule reads, because the types carry them. A value of `Regula.Closed.Input` has the closed form (**proved**: `wf_toSpec`), and a value of `Regula.Closed.Tables i` holds what each table holds of the input `i`, so `rgN_exact` holds of every value of that type. A rule computes an axiom set from the input itself, by a search backwards from each axiom through the constants that each constant mentions (`Tables.axiomSet`), and that set is exactly what `Input.AxiomOf` states (**proved**: `Tables.mem_axiomSet`, `axiomSet_iff`, with `mem_reach`). The checker does not call `Lean.collectAxioms`, so nothing about that function is assumed.

## The closed input

The closed input is the type `Input` in [`RegulaSpecification/Input.lean`](RegulaSpecification/Input.lean):

| Field | Owner and interface |
| --- | --- |
| `profile`, the profile that the project states | The one argument of the lint driver, `lintDriverArgs` of the project's Lake configuration |
| `modules`, the claimed modules | Lake's load gives the modules of the default targets of the root package; each loaded module whose `.olean` lies in the root package's library directory is claimed |
| `decls`, each constant of the environment | `Lean.importModules` with `loadExts := false`, at the level `.private` |
| `unique`, that no name is that of two constants | The loader's proof, from the keys of the hash map that holds the constants (`Std.HashMap.distinct_keys_toList`) |

The input has no source text, message, compiled code, option or build log. A rule does not decide what it cannot read in this input.

The admission refuses an input that does not have the closed form (`Input.WellFormed`). Each constant that a constant mentions is held (**proved**: `open_mention_refused`). At least one module is claimed, so a claim of nothing is not read as a pass (**proved**: `no_claim_refused`). **Proved**: `admit_ok_iff` for the function that the checker runs, `Draft.admit`, which gives the proofs of both to the type that the rules read.

What the type excludes needs no check. The type `Input` of this package cannot hold a name twice, as an environment keeps its constants in a hash map, and the checker's `Facts` carries that its modules are those of the environment's header, so a claimed module is a loaded one (**proved**: `claimed_loaded`). `Safety` cannot state a constant that is both unsafe and partial, which Lean does not make (**proved**: `not_unsafe_of_partial`). `Regula.Closed.Report` cannot state a pass with a finding, a failure with none, or an incomplete run with no reason.

The shell has four effects on the plain `lake lint` path: it loads the build, it replays the cone of the build's claim, it prints its report, and it sets its exit code. It writes no file there. It runs no initializer of the loaded modules, because it loads them without extension states. Lake's own load of the workspace on that path runs Git in the environment of the caller. The full gate takes another path: it loads the root package's configuration alone, which resolves no dependency, and has more effects, which [the language check](#the-language-check) gives: it reads source files and, once it has admitted them, writes them to a tree of its own, which it removes afterwards, it imports the toolchain's modules with their initializers to parse those files, and for an admitted project it runs `lake build --wfail` in that tree and replays the cone of the build's claim. [The run of the checker](#the-run-of-the-checker) states these effects.

## From a build to the input

`Regula.Load.Facts.input` is the pure function that fills the input from an environment, and [`RegulaSpecification/Proofs/Load.lean`](RegulaSpecification/Proofs/Load.lean) states what it gives. So a later change to the loader that drops a constant, a field or a mention fails the gate's build of this package.

- **Proved**: `pass_iff`. For every environment, every `Facts` and every profile, when the loader gives an input, the checker passes on it exactly when the environment has `EnvForm` and `EnvFloor`. These two statements name no field of the input. `EnvForm` is the closed form. `EnvFloor` states RG1001 to RG1006, RG1011 and RG1012 of each constant of `Environment.constants.map₁` in a claimed module. What a name mentions, and whether it names an axiom, is read from the fields of the `ConstantInfo` that `map₁` keeps and of each constant of that name that a loaded module's own data states (`EnvMentions`, `EnvAxiom`, `mem_usesIn`, `mem_stated`).
- **Proved**: `pass_floor`, the same on the path that the shell decides (`Regula.Closed.decision`). A pass also states that each module of a default target is claimed, that each claimed module is loaded, and that each constant of the environment has a module. `input_form` states the closed form of each environment that the loader gives an input for.
- **Proved**: `pass_held`. On a pass, each constant of a claimed module, as that module's own `.olean` states it and also when Lean's import replaced it (below), has neither replacement attribute in that module's own entries (`ModuleUnreplaced`), is no axiom, is partial and not unsafe when it has either flag or a recursion helper's name, has no value that mentions a loop construct, has, when it is a definition or an opaque constant, no value that mentions a panic form (`EnvPanic`), and reaches through what it mentions only axioms that the profile admits. That theorem does not state the rest of the helper's form of such a constant; `pass_iff` states it of the constant that `map₁` keeps.
- **Proved**: `decision_pass`, `decision_failed`, `profileOfRun_ok` and `profileOf_eq_some`, for the shell's pure decisions. `mem_claimed_place`, `toolchain_place` and `below_iff`, for what the places of the modules decide, and `moduleOf?_eq` for the module of a constant. `startsSearchPath_eq_true_iff`, in both directions, for the workspace search-path comparison.

Each field of the input, with the rules that read it, its statement against the environment, and what that leaves about Lean or Lake:

| Field | Read by | Statement | Left assumed, and its entry |
| --- | --- | --- | --- |
| `profile` | RG1005 | `Loaded.profile`, `profileOfRun_ok`, `profileOf_eq_some` | Lake passes `lintDriverArgs` as the arguments (`lakeStart`) |
| `modules` | each rule, the admission | `Loaded.modules`, `Loaded.roots`, `claimed_loaded`, `mem_claimed_place`, `below_iff` | Lake names the modules of the default targets and the root package's library directory; `findOLean` finds each `.olean` on Lake's search path (`lakeLoad`, `leanImport`) |
| `decls`, and each `name` | each rule, the admission | `Loaded.sound`, `Loaded.whole`, `Facts.decls_nodup`, `mem_stated` | `map₁` holds the constants that the import keeps, and `header.moduleData` what each `.olean` states (`leanImport`) |
| `module` | each rule | `Loaded.sound`, through `Facts.info?`, `moduleOf?_eq` | `getModuleIdxFor?` and `header.moduleNames` name a module that holds the constant (`leanImport`) |
| `kind`: `axiom` when any loaded module's own data states an axiom of the name, otherwise the constructor of the constant that `map₁` keeps | RG1001, RG1002 to RG1005, RG1006, RG1012 | `kind_axiom`, `kind_definition`, `kind_theorem`, `kind_runs`, `kind_envAxiom`, `isAxiom_env`, `theorem_env`, `mem_stated` | the `ConstantInfo` that each `.olean` holds (`leanImport`) |
| `safety` | RG1006 | `pass_iff`, through `EnvFloor`, `safetyOf_partial`, `safetyOf_safe`, `not_unsafe_of_partial` | as for `kind` |
| `uses`: what the constant that `map₁` keeps mentions, and what each constant of the name that a loaded module's own data states mentions, as `Mentions` reads it | RG1002 to RG1005, the admission, the cone that the kernel replays | `mem_usesOf`, `mem_usesIn`, `mem_stated`, `reaches_env` | `Expr.getUsedConstants` lists each constant of an expression (`usedConstants`) |
| `valueUses` | RG1006, RG1012 | `mem_valueUsesOf`, `panic_env` | as for `uses` |
| `implementedBy`, `isExtern` | RG1006, RG1011 | `helper_env`, `allHold_env`; `unreplaced_iff` and `pass_held` cover each claimed module's own entries at the loader's admission | `getImplementedBy?` and `isExtern` read the selected module's entries; `getModuleIdx?` and `getModuleEntries` read each named module's own entries under `loadExts := false`, at the level `.private` (`leanImport`) |
| `inToolchain` | RG1003, RG1005 | `known_env`, `toolchain_place`, `below_iff` | Lean finds the toolchain's library only below its `lib/lean` directory (`leanImport`) |

No field is left for removal: each has a statement against the environment. What remains assumed of a field is Lean's or Lake's behaviour. That a run passes what they returned to `Facts.input` is proved (`BuildRead`, `Loaded`, `run_meets`).

**The constants that Lean's import replaces.** Lean refuses two imported modules that declare one name with different values, with one exception. It merges two theorems of one name and type, a theorem with an axiom of that name and type, and two such axioms, and it keeps one constant under the name of the first module that holds it (`subsumesInfo` and `finalizeImport`, `Lean/Environment.lean:2269` and `2336-2345`). So the merged environment can hide an axiom or a chain of mentions that a loaded module's own data states, in a claimed module or a dependency. **Measured** on 2026-10-31 at pull request 515, on a project of `kernel-only`: a module whose theorem `shared` used `Classical.choice`, beside a module whose theorem `shared` had the same type and a proof with no axiom, passed `lake build --wfail`, `lake check` and `lake lint`. Lean regenerates a definition's equation lemmas in each module that needs them, so refusing each such constant would refuse ordinary projects (**measured**: `f.eq_def` in two modules). So the loader reads the own constants of every loaded module from the header of the environment, claimed or not (`Facts.stated`), and what any of them mentions, and whether it is an axiom, counts for its name. On a pass, each axiom reached from a constant of a claimed module, by following mentions that any loaded module's own data states, is one that the profile admits (**proved**: `pass_floor`, `pass_held`, `mem_stated`). So a replaced dependency theorem's mentions now count, and so does a dependency's axiom that a theorem replaced, and this can refuse a build whose merged environment is clean. A constant of a claimed module that the environment does not show to the rules must also be a theorem, with neither flag and no recursion helper's name (`fitsUnshown`), whose value mentions no loop construct, and whose mentions reach only axioms that the profile admits, or the run is `incomplete` (`Facts.claimedConstants`, `Facts.unread?`). **Measured** on 2026-10-31 on this change, before it took in pull requests 516 and 518, on disposable projects, each after `lake build --wfail`: the project above gives `incomplete` or `fail` by the order of its imports, and passes under `standard-logical`. Under `kernel-only`, a module that mentions a dependency's theorem `bridge` whose proof uses `Classical.choice`, beside a claimed module whose `bridge` uses no axiom, gives `fail` (RG1005). With a theorem `shared` that mentions `bridge` and that the second module also replaces, it gives `incomplete`, and it passes under `standard-logical`. A module that mentions a dependency's axiom `x`, beside a claimed module with a theorem `x`, gives `fail` (RG1003, RG1005) under `kernel-only` and under `standard-logical`. When the dependency's `bridge` uses no axiom, the `kernel-only` project passes, and so do the two modules with `f.eq_def` under `standard-logical`.

## The rules

### RG1001 to RG1005: the foundation profile

Each reads a constant of a claimed module. RG1002 to RG1005 read its transitive axiom set `Input.AxiomOf`, which the rules compute from the input (`axiomSet_iff`). The four refine one refusal: each axiom that RG1002, RG1003 or RG1004 names also violates RG1005 for each profile. Thus a wrong choice between these rules changes the rule of a finding, but not the verdict. **Proved**: `rg1005_of_hole`, `rg1005_of_unknown` and `rg1005_of_compiler`. The formal statements are in one module for each rule below [`RegulaSpecification/Rules/`](RegulaSpecification/Rules/), with the vocabulary that more than one of them reads in [`RegulaSpecification/Foundation.lean`](RegulaSpecification/Foundation.lean) and the three theorems of the refinement in [`RegulaSpecification/Refinement.lean`](RegulaSpecification/Refinement.lean).

- **RG1001: project axioms.** A constant of a claimed module has the kind `axiom`. An assumption is a hypothesis or a field of a structure, so that each theorem that uses it shows it in its type. `lake check` refuses an axiom only when a constant mentions it, so it does not do the work of this rule. `Violates1001`.
- **RG1002: proof holes.** A constant depends on `sorryAx`, directly or through an import. `Violates1002`.
- **RG1003: unknown axioms.** A constant depends on an axiom other than `propext`, `Quot.sound` and `Classical.choice` of the toolchain, and RG1002 and RG1004 do not name it. `Violates1003`, with `Input.Known`. **Assumed** (`leanImport`): Lean finds the library of the toolchain only below the `lib/lean` directory of the pinned toolchain, which the shell reads to say that a module is in that library.
- **RG1004: native proofs.** A constant depends on an axiom with the name form `<declaration>._native.<tactic>.<suffix>` that `native_decide`, `decide +native` and `bv_decide` add (`Lean/Meta/Native.lean:45` and `75-82`), or on an axiom by which the kernel trusts the compiler, of which `v4.35.0` declares none. `Violates1004`, with `NativeProofAxiom` and `compilerAxioms`. **Measured**: `native_decide` gave `n._native.native_decide.ax_1_1`. The rule identifies the axiom by its name, so an author can give an axiom that name. Then RG1004 reports it in place of RG1003, and the verdict is the same.
- **RG1005: the profile.** A constant depends on an axiom that the project's profile does not admit. Kernel-only admits no axiom. Choice-free admits `propext` and `Quot.sound`. Standard-logical also admits `Classical.choice`. Each admitted axiom is the toolchain's own. `Violates1005`, with `Input.Admits`.

### RG1006: `unsafe` and `partial` declarations

The rule refuses three things in a claimed module: an `unsafe` or `partial` constant without the exempted form, a constant with a helper's name without that form, and a constant whose value directly mentions a loop construct of Lean. `Violates1006`, with `Input.HelperForm`, `HelperNamed` and `MentionsLoop`, in [`RegulaSpecification/Rules/RG1006.lean`](RegulaSpecification/Rules/RG1006.lean). **Proved**: `rg1006_exact` in both directions, `rg1006_checker_refuses_loop` for each construct, and `rg1006_checker_refuses_forged_name` for a plain definition with a helper's name.

**The loop constructs.** The class comes from Lean's `Init/While.lean`. A `while`, `repeat` or `repeat ... until` needs no `partial` of the module that uses it, because it compiles through `Lean.Loop.forIn` to `repeatM`, whose body is a private `partial` of that file. So the flags alone do not show a loop that does not end. The rule reads the value of each claimed constant for the one value of the type `Lean.Loop`, `Lean.Loop.mk`, and for `repeatM` (`loopConstructs`). `termination_by` and `partial_fixpoint` stay allowed, and so does `for` over a list. The owner's delegated agent added this on 2026-10-31, after `while true` passed all three commands while a `partial def` of the same loop failed.

**Measured** on 2026-10-31 on a disposable project: `while`, `repeat`, `repeat ... until`, a direct `repeatM`, a direct `Lean.Loop.forIn ⟨⟩`, `forIn Lean.Loop.mk` and an `Inhabited Lean.Loop` instance were each refused; `termination_by`, `partial_fixpoint` and `for` over a list passed.

What this leaves out, as accepted risk under the owner's trust in dependencies:

- A loop inside a dependency or the toolchain, such as `IO.iterate` (`Init/System/IO.lean:780`), which is a `partial def` that a claimed constant can call. **Measured**: it passes.
- A claimed function that takes a value of `Lean.Loop` as an argument mentions neither construct, and it passes (**measured**). Running it needs that value, which claimed code can make only through `Lean.Loop.mk`, so only a dependency's value runs it.
- A mention only in a constant's type, which runs nothing. **Proved**: `rg1006_admits_type_mention`.
- A loop that a claimed module's own code adds during the build, as a constant of the exempted form below.

**The exempted form.** It is a partial constant `f._unsafe_rec`, not unsafe, with no `implemented_by` and no `extern`, in the module of a safe, total definition `f` with neither. It is the form of what Lean's elaborator adds for a safe recursive definition, which is why it is exempted, and it is a form and nothing else: the input holds nothing of who produced a constant. Lean makes the base of a `partial def` an opaque constant, so the rule reports the helper of a `partial def`.

**A helper's name.** The compiler reads `f._unsafe_rec` in place of `f` by its name alone, whatever its kind and flags (`getDeclInfo?`, `Lean/Compiler/LCNF/ToDecl.lean:25-27`). So the rule refuses each constant of a claimed module with a name of the form `b._unsafe_rec` that has not the helper's form, and each such constant that is not partial in particular, for each kind and however it was declared. **Proved**: `rg1006_reports_named_not_partial`. Only a definition can be partial (`ConstantInfo.isPartial`, `Lean/Declaration.lean:463-465`), so each constant of another kind with that name is refused. The checker runs the compiler's own test, `Lean.Compiler.isUnsafeRecName?`, in place of a copy of it. **Proved**: `isUnsafeRecName_eq` states that test against `HelperNamed`, and `mkUnsafeRecName_eq` states the name that `getDeclInfo?` looks up, so a toolchain with another form fails these proofs. Read from the source, and relied on by no verdict, since a proof verdict says nothing about what a compiled program runs: the compiler's only readers of a helper by its name are `getDeclInfo?`, `declIsNotUnsafe` and `toDecl` (`Lean/Compiler/LCNF/ToDecl.lean:27`, `37` and `51`), with `toLCNF`'s check of `isNoncomputable` and its `replaceUnsafeRecName` (`Lean/Compiler/LCNF/ToLCNF.lean:448` and `525`). The owner's delegated agent added this on 2026-10-31, after an audit found that the plain definition below passed the rule.

```lean
def g (n : Nat) : Nat := n
def g._unsafe_rec (n : Nat) : Nat := n + 1
theorem g_one : g 1 = 1 := rfl
```

**Measured** on 2026-10-31. Before this rule, at the commit of the cut, that module passed `lake build --wfail` and `lake lint`, while `#eval g 1` and `lean --run` of `g 1` printed `2`. Lean also panics on this input during a Lake build (`emitCForDecls`), and Lake prints the panic as information and exits 0, so `--wfail` does not catch it. Now `lake build --wfail` and `lake check` still pass it, and `lake lint` reports RG1006 and exits 1. On a disposable project, RG1006 reported the helper's name in each of these forms: `def`, `abbrev`, `opaque`, `instance`, `theorem`, `axiom`, `inductive`, `structure`, `class`, a constructor, a structure field, `where`, `let rec`, `namespace`, a quoted name, `private`, `protected`, `noncomputable`, `@[reducible, inline]`, `@[extern]`, `@[implemented_by]`, a `macro` that expands to a `def`, a `mutual` block, a recursive `def`, a top-level `_unsafe_rec`, a `partial def` with and without recursion, an `unsafe def`, and a `module` file with `public` and `private` declarations. Lean itself refused `initialize` and `syntax (name := ...)` with that name, and a `mutual` block of a `def` and a `partial def`.

**Measured** on the same day: structural and well-founded recursion, each in a `mutual` block too, nested recursion through `where`, `let rec`, `private`, `protected`, an `abbrev`, a method of an instance, `partial_fixpoint`, `@[specialize]`, universe polymorphism, a `module` file, and the functions that `deriving Repr, BEq, Hashable, DecidableEq` writes for a recursive type all gave a helper that passed `lake lint`, and that project passed `lake build --wfail` and `lake check`. The rule still reports the helper of what `deriving` writes as a `partial def`, as it did before, because the base is an opaque constant (`usePartial`, `Lean/Elab/Deriving/Util.lean:116`). **Measured**: `Repr` and `BEq` on a nested inductive type and `Ord` on a recursive type.

The rule reads that form and nothing about what the constant computes. So a claimed module's own code can add a constant of the form during the build, such as with `run_cmd`, and the module passes the two commands of the proof verdict. The proof verdict's claim stays true of it, as `helperForm_unreached` states under H6, and it says nothing about what a compiled program runs. [The language check](#the-language-check) refuses that code before it can run, so such a module gets no full verdict. **Measured** on 2026-10-31 with this revision of the checker, on a project of one module:

```lean
import Lean
open Lean Elab Command
run_cmd liftCoreM do
  let ty := mkForall `n .default (mkConst ``Nat) (mkConst ``Nat)
  let val := mkLambda `n .default (mkConst ``Nat) (mkApp (mkConst ``Nat.succ) (mkBVar 0))
  addDecl (.defnDecl { name := `g._unsafe_rec, levelParams := [], type := ty, value := val,
                       hints := .opaque, safety := .partial, all := [`g._unsafe_rec] })
def g (n : Nat) : Nat := n
theorem g_one : g 1 = 1 := rfl
#eval g 1
```

The `#eval` printed `2` while `g_one` holds, and `lake check` and `lake lint` both passed. That is about what a compiled program runs, not about a proof: `g_one` is about the definition `g`, and Lean's kernel refuses a safe constant that mentions a partial one (H6). The language check refuses this module (**measured** on 2026-10-31, at the runs of [what was measured](#what-was-measured)), so it gets no full verdict. **Measured** on 2026-11-01 with `lean` on that source: `#eval g 1` printed `2`, `g_one` depends on no axiom, and the kernel refused, with `safe declaration must not contain partial declaration`, a `def` and a `theorem` that mention `g._unsafe_rec` and a theorem added directly with `addDecl`.

### RG1011: replaced compiled code

The rule refuses each constant of a claimed module that has `@[implemented_by]` or `@[extern]`. `Violates1011`, with `Replaced`, in [`RegulaSpecification/Rules/RG1011.lean`](RegulaSpecification/Rules/RG1011.lean). **Proved**: `rg1011_exact` in both directions, `rg1011_checker_refuses_extern` for an `@[extern]` constant, and `rg1011_admits_neither`, that a constant with neither attribute is not reported, whatever else it has. In the terms of the environment, a pass gives `getImplementedBy? env n = none` and `isExtern env n = false` for each constant `n` of `Environment.constants.map₁` in a claimed module (**proved**: `pass_iff`, through `EnvFloor`).

**Why these two.** The proofs of a claimed module are about each constant's definition. Lean's compiler compiles no code from the definition of a constant with either attribute: for an `@[extern]` constant it emits a call of the foreign function that the attribute names (`Lean/Compiler/LCNF/ToDecl.lean:68-71`), and for one that `@[implemented_by]` gives a replacement it generates no code (`shouldGenerateCode`, `Lean/Compiler/LCNF/Main.lean:40`) and replaces each call by a call of the replacement (`applyImplementedBy?`, `Lean/Compiler/LCNF/Simp/SimpValue.lean:55-59`). Lean checks only that the replacement has the constant's universe parameters and type and is another constant (`Lean/Compiler/ImplementedByAttr.lean:49-64`), not that it computes the same, as its documentation says (`:40-43`). Read from the source. So a claimed function can be proved and the program can run other code with no signal. **Measured** on 2026-10-31, before this rule: a module with each of the two passed `lake build --wfail`, `lake check` and `lake lint`.

**How the input reads them.** The loader asks `Lean.Compiler.getImplementedBy?` and `Lean.isExtern` of the environment of the build (`Regula.Load.Facts.declIn`), the two queries by which the compiler decides what it compiles (`Lean/Compiler/LCNF/Main.lean:34` and `:40`). It also reads each claimed module's own entries with `getModuleIdx?` and `getModuleEntries` (`Facts.unreplaced`), so the merged name cannot hide another module's attribute. **Assumed** (`leanImport`): that the queries and module entries report the attributes of the build. Each attribute is a parametric attribute of Lean, read from the source at the pinned tag, and no verdict relies on this beyond that entry:

- Lean adds the attribute only to a declaration of the module being elaborated, and only as a global attribute: `@[local implemented_by]`, `scoped`, and the attribute on an imported constant are refused (`Lean/Attributes.lean:289-292`, and `:323-330` for `setImplementedBy`). So `attribute [implemented_by g] f` after the declaration of `f` in its own module is read as the attribute on `f` is, and another module cannot add it to `f`.
- The query of an imported constant reads the entries of the module that holds the constant, and nothing else (`Lean/Attributes.lean:306-318`). An entry that another module's code writes into the extension directly, for a constant it imported, is read by neither the query nor the compiler, whose queries are the same.
- A module stores each entry at the level `.private`, and the `.olean` of a level below it only those of a public declaration (`Lean/Attributes.lean:257-261` and `:272-279`). The loader imports at the level `.private`, which reads each module's private data (`Lean/Environment.lean:2032` and `:2183`), and sets each module's entries whatever `loadExts` is (`:2377`). So a private declaration of a `module` file is read too.
- What Lean's own elaborators add is read as what a declaration states: the `unsafe` term (`Lean/Elab/BuiltinNotation.lean:578`), `deriving TypeName` (`Lean/Elab/Deriving/TypeName.lean:25`) and the computed fields of an inductive type, which replace its `casesOn` and constructors (`Lean/Elab/ComputedFields.lean:150` and `:171`), each give a constant that RG1011 refuses.

**Measured** on 2026-11-03 with this revision of the checker, on a disposable project of `standard-logical` after `lake build`: RG1011 reported `slow`, a `def` with `@[implemented_by fast]`; `ext`, an `opaque` with `@[extern "probe_ext"]`; `late`, given the attribute by `attribute [implemented_by fastLate] late` after its declaration; a `private def` with the attribute in a `module` file, as `_private.Probe.Mod.0.hidden`; the constant that `unsafe (n + 1)` adds in a `def`; and the instance that `deriving TypeName` adds. It reported no constant of a module with a `@[csimp]` theorem `@slowSum = @fastSum` and of a module with a plain definition and a theorem, and the run gave `fail`, exit 1. The project of those two modules alone passed `lake build --wfail` and gave `pass`, exit 0. The first `lake lint` took 3.1 s with a largest resident set of 0.52 GiB.

**A constant that Lean's import replaced.** The refusal covers its own module's attributes even when the merged constant has the same proof. The loader's `Facts.shown` requires either that the module's own entries have neither attribute, or that the represented constant has a replacement that RG1011 refuses. Otherwise the loader admits only a safe theorem within the profile with neither attribute in its own module (`fitsUnshown`); an attributed copy gives RG2001, `incomplete`, naming that module and constant. Ordinary represented attributes still give RG1011. **Proved**: `unreplaced_iff` relates the actual reader to `ModuleUnreplaced`, which quantifies over every entry of both extensions for the named module; `shown_unreplaced`, `fitsUnshown_iff` and `pass_held` carry it through both admission paths to `Meaning.loaderHeld`. `pass_iff_floor` remains the exact pass condition, including the strengthened `EnvUnshown`, so clean merged theorems remain admitted when the other conditions hold. A missing module index is refused, never treated as empty entries. This reaches machine-checked universal correspondence rather than a type-only guarantee because Lean supplies the arrays at runtime; their identity and contents remain `leanImport` assumptions (`Lean/Environment.lean:155-167`, `:1211-1212`, `:1666-1678`, `:2377`).

**`@[csimp]`.** The rule does not read it, so it refuses no constant for it. A `@[csimp]` theorem states `@f = @g`, and the compiler replaces `f` by `g` only through such a theorem (`isConstantReplacement?`, `Lean/Compiler/CSimpAttr.lean:40-55`), so the replacement equals the original in Lean's logic as far as that theorem's proof is sound. The owner's delegated agent decided on 2026-11-03 that the rule admits it for that reason ([the record](confirmation.md#2026-11-03-the-rule-on-replaced-compiled-code)). On a pass, the kernel checked each theorem of a claimed module in the replay of the cone, within the profile. Lean admits the attribute also on a theorem of another module, and with `local` or `scoped` (`Lean/Compiler/CSimpAttr.lean:51-55`, `:76-79`), and its documentation says that an unsound one can be registered with `unsafe` or with an axiom such as `sorryAx` (`:68-69`). So a claimed module can put it on a dependency's theorem, whose proof the replay checks only when the claim's cone holds it.

What this leaves out, as accepted risk under the owner's trust in Lean and in dependencies, and what [what a pass means](#what-a-pass-means) states:

- A constant of a dependency or of the toolchain with either attribute, which a claimed constant calls, such as Lean's own `@[extern]` arithmetic.
- `@[csimp]`, above, and the code that Lean's compiler makes of a definition, of which no verdict claims anything.
- A constant of the exempted form that a claimed module's own code adds during the build, which [RG1006](#rg1006-unsafe-and-partial-declarations) reads by its form.

### RG1012: hidden panics

The rule refuses each definition or opaque constant of a claimed module whose value mentions a panic form. `Violates1012`, with `BangNamed` and `Input.PanicForm`, in [`RegulaSpecification/Rules/RG1012.lean`](RegulaSpecification/Rules/RG1012.lean). **Proved**: `rg1012_exact` in both directions, `rg1012_checker_refuses_panic` for a mention of `panicWithPosWithDecl`, and `rg1012_admits_theorems`, that neither a definition whose value mentions a theorem named with `!` nor a theorem whose proof mentions `Option.get!` is a violation. `bangNamed_hygienic` and `not_bangNamed_query` state that a name with macro scopes counts by the name they erase to and that `GetElem?.getElem?`, to which `xs[i]?` elaborates, is no panic form. In the terms of the environment, a pass gives, for each definition or opaque constant `n` of `Environment.constants.map₁` in a claimed module, that its value mentions no name of which `EnvPanic` holds (**proved**: `pass_iff`, through `EnvFloor`), and `pass_held` states the same of each claimed module's own constant as its `.olean` states it.

**Why.** A total function of Lean can still panic, and a panic gives the type's default value. In Lean's logic `panicCore` is `default` (`Init/Prelude.lean:3849`), and its compiled code prints the message and returns that default, unless the variable `LEAN_ABORT_ON_PANIC` is set or the program asked to exit on a panic (`lean_panic_impl` and `lean_panic_fn`, `src/runtime/object.cpp:176-207`), each read at the tag v4.35.0. So a proved function can go on with a value that its proofs never considered, with no signal but a message on the error stream.

**What a panic form is.** One of Lean's four panic functions, `panicCore`, `panic`, `panicWithPos` and `panicWithPosWithDecl` (`Init/Prelude.lean:3849` and `:3863`, `Init/Util.lean:59` and `:81`), or a constant that the input does not hold as a theorem and whose name's last string component, after `Lean.Name.eraseMacroScopes`, contains `!`. A name that the input does not hold counts, so a mention that the input cannot classify is refused. **Measured** on 2026-11-03 on a disposable module at v4.35.0, by reading what each form elaborates to in the constant's value: `xs[i]!` on an `Array`, a `List` and a user's `GetElem?` instance mentions `GetElem?.getElem!`; `Option.get!`, `List.head!`, `String.toNat!`, `Array.back!` and `Array.set!` mention themselves; `panic!`, `unreachable!` and `assert!` mention `panicWithPosWithDecl`; `xs[i]?` and `dbg_trace` mention none of these.

**Measured** on 2026-11-04 with this revision of the checker, on a disposable project of `standard-logical` that requires it by path, after `lake build`: `lake lint` read one claimed module and its 58 constants and reported RG1012 for exactly the 13 definitions that use a listed form: `xs[i]!` on an `Array`, on a `List`, on a structure whose `GetElem?` instance inherits the default `getElem!`, and inside a `where` function, which it reported as `rWhere.go`, the constant that holds the mention; `Option.get!` in a plain and in a `private` definition, reported as `_private.Probe.0.rPrivate`; `List.head!`, `String.toNat!`, `Array.back!`, `Array.set!`, `panic!`, `unreachable!` and `assert!`. It reported none of `xs[i]?`, `dbg_trace`, `xs[i]` with a `Fin` index, `Option.getD`, a theorem that states `x.get! = x.get!`, a structural recursive definition, the structure's derived instances and its `GetElem?` instance, nor `rWhere`, whose value mentions only `rWhere.go`. The verdict was `fail`, exit 1.

**Why a name, and why direct mentions.** [Issue 552](https://github.com/rbeauchamp/regula/issues/552) first framed the rule as refusing a constant whose value depends on `panicCore`. **Measured** on 2026-11-03 at v4.35.0: through what each constant mentions, 46,999 constants of Init and Std reach `panicCore`, among them `Std.HashMap.insert` and `List.mergeSort`, through the proof terms of `omega`, and through values alone 117 of Regula's own claimed constants reach it, through Lean's functions such as `Lean.Name.toString` and through `m[k]?` on a hash map, whose instance holds a `get!` field. `xs[i]!` on an array reaches no `panicCore`: `Array.get!Internal` is `@[extern "lean_array_get"]` with the value `Array.getD a i default` (`Init/Prelude.lean:3464-3466`), and its panic is in C (`lean_array_get_panic`, `include/lean/lean.h:1088-1117`). So a rule on reaching `panicCore` would refuse nearly all Lean code and Regula itself, and miss the most common form. The rule reads the name that Lean gives an operation that panics, as the owner's delegated agent decided on 2026-11-04 ([the record](confirmation.md#2026-11-04-the-rule-on-hidden-panics)). It reads only what a value mentions directly: on any path from a claimed constant to a panic form through the values of claimed definitions and opaque constants, the last of them mentions the form itself and is refused, so a build fails under that closure exactly when it fails under direct mentions.

**Measured** on 2026-11-04 over the 216,539 constants of the toolchain's Init, Std, Lean and Lake at v4.35.0, imported at the level `.private`: 523 constants that are no theorem have a name that `BangNamed` admits. For 472 of them, Lean's data shows a route to a panic: through the values of definitions and opaque constants, and from a constant to the one that `@[implemented_by]` names, each reaches `panicCore`, one of the 10 `@[extern]` constants among the 523, whose C code was not read, or `GetElem?.getElem!`, the one projection of a class's field among them, whose code is the instance's. The other 51 show no such route, so they cannot panic as far as Lean's data shows: 36 are syntax, such as the parsers, macro rules and unexpanders of `simpa!`, `grind!` and `xs[i]!`, which a program does not call, and 15 are functions, among them `Std.DHashMap.getEntry!`, `Subarray.get!` and `ByteSlice.get!`, and `Std.DHashMap.Internal.AssocList.getEntry!`, which returns `default` without a panic. A claimed definition that mentions one of these 51 is refused, though it cannot panic through it: a refusal within the published criterion, not a false refusal. 3,696 theorems of the toolchain have such a name and are no panic forms. Regula's own claimed definitions and opaque constants, 879 at the base of this change, mention no panic form, and on 2026-11-04 the local gate's `lake lint` passed on Regula's 23 claimed modules and 1,396 constants and on this package's 52 modules and 4,264 constants with RG1012 among the rules. The probe was a diagnostic and is not kept.

What this leaves out, under the owner's trust in Lean and in dependencies, and what [what a pass means](#what-a-pass-means) states:

- A panic inside the code of a dependency or of the toolchain, reached through a constant whose name has no `!`, such as `Lean.Name.toString`, or `outOfBounds`, which the default of `GetElem?.getElem!` calls (`Init/GetElem.lean:17-18` and `:107-108`).
- A panic in C code behind `@[extern]` of a constant whose name has no `!`. RG1011 already refuses `@[implemented_by]` and `@[extern]` on a claimed constant.
- A claimed `GetElem?` instance that inherits the default `getElem!` is not refused, because its value mentions `outOfBounds` and no panic form. Each `c[i]!` that uses it mentions `GetElem?.getElem!` and is refused instead.
- A mention in a constant's type, not its value.

Refused, outside the narrow purpose though within the criterion: a definition whose value mentions a constant named with `!` that is no theorem only inside a proof, which never runs, and a mention of one of the 51 constants above.

### RG1010: the language check

[The language check](#the-language-check) states it. It reads no constant, and only the full gate reads it.

### RG2001: the environment

A run that cannot load the build gives `incomplete`. So does an input that the admission refuses, a constant of a claimed module that the loader refuses (`Facts.unread?`), any argument list other than one profile, and any Lean other than the one this revision reads (`Regula.Shell.supportsLean`). In the full gate, so does each case of [the closed list](#the-closed-list-of-refusals) with exit 2. `gateRecord` in [`RegulaSpecification/Gate.lean`](RegulaSpecification/Gate.lean) states the verdict. **Proved**: `gate_o5`, so the record leaves nothing unsaid about the verdict, and `gate_adequate`.

**Proved** of `Regula.Closed.Draft.admit`, `Regula.Closed.Input.report` and `Regula.Closed.decision`, the functions that the checker runs, in [`RegulaSpecification/Proofs/Verdict.lean`](RegulaSpecification/Proofs/Verdict.lean) and the registry, [`RegulaSpecification/Rules.lean`](RegulaSpecification/Rules.lean):

- `admit_ok_iff`, `admit_error_iff`: its admission refuses exactly a reading without `Input.WellFormed`.
- `run_refused`: a refused input is `incomplete`, where `run` is the admission and then the decision.
- `run_complete`: an admitted input is not `incomplete`, and it is `pass` exactly when every rule holds of it. `report_complete` states that of each value of `Regula.Closed.Input`, with no hypothesis, from the checker's own `Regula.Closed.report_pass_iff`, and `Regula.Closed.report_findings` states that its report holds exactly the findings of the registered rules, which `Regula.Closed.mem_findings` states.
- `run_meets`: the verdict meets `gateRecord`, with `none` for a build that the shell cannot load.

The exit code of `pass` is 0, and no other verdict has it (**proved**: `Regula.Closed.Verdict.exitCode_eq_zero_iff`). `fail` is 1 and `incomplete` is 2. A process that dies ends with a code of its own, which no theorem relates to a verdict, so only exit 0 reads as a pass.

**Measured** on 2026-10-31 on a disposable project that requires the revision of pull request 515, before the loader read what the import replaces. Each case ran `lake build` and then `lake lint`: a `sorry` and a theorem that uses it (RG1002 and RG1005 on each, exit 1); an unused axiom (RG1001, RG1003, RG1005, exit 1); `native_decide` (RG1001, RG1004, RG1005, exit 1); a `partial def` and a `while` (RG1006, exit 1); an `unsafe def` (RG1003, RG1005, RG1006, exit 1); `Classical.em` under `choice-free` (RG1005, exit 1); `propext` under `kernel-only` (RG1005, exit 1); no profile or a wrong profile (exit 2); no default target (exit 2); no build (exit 2); a run from another directory than the workspace (exit 2); a non-default module with a `sorry` that a default module imports (RG1002, RG1005, exit 1); and a compliant module with a structural recursive definition (exit 0).

## What a pass means

Regula gives one of two verdicts, and the last line of a run says which. This section is about the proof verdict. [The language check](#the-language-check) states the full verdict, which needs what a pass here needs and more.

A pass of the proof verdict is the result of two commands of the pinned toolchain on one finished build, in this order:

1. `lake build --wfail`.
2. `lake lint`, Regula's checker.

The first is Lake's own, and Regula makes no claim of its own about what it decides (**Assumed**: `lakeCommands`).

**The replay of the cone.** The checker loads the build, fills the closed input from it (below), and asks Lean's replay, `Kernel.Environment.replay`, to add the cone of the claim into the kernel's environment of `Lean.mkEmptyEnvironment`, which holds no constant (`Lean/Environment.lean:1531-1543`). A pass needs that replay to answer with success; any other answer is `incomplete` (RG2001). The cone starts at each constant of a claimed module and at each constant that Lean's kernel builds into a term that it checks and that the environment holds (`Input.kernelNames`): the types of a literal, what the kernel unfolds a number and a string literal to, and the values of its arithmetic on numbers (`Lean/Expr.lean:622-624`, `src/kernel/inductive.cpp:1359-1401`, `src/kernel/type_checker.cpp:669`, `src/library/constants.cpp:147-150`). It holds every constant that these reach through what each mentions, the relation `uses` of the closed input and `Mentions` of the specification: the type of each constant, the value of a definition, theorem or opaque constant, the constructors and the other types of an inductive type's block, the inductive type of a constructor, the types of a recursor's block, and `Eq` for a quotient. Lean's replay follows `ConstantInfo.getUsedConstantsAsSet` (`Lean/Util/FoldConsts.lean:67-74`), whose `Expr.getUsedConstants` also lists the structure of each projection (`Lean/Util/FoldConsts.lean:41`), reads each type of a block and its constructors (`Lean/Replay.lean:105-111`), and adds `Eq` before a quotient (`Lean/Replay.lean:129-133`). The replay is given each constant of the cone as the environment keeps it, but `Quot.mk`, `Quot.lift` and `Quot.ind`, which the kernel adds with `Quot` and refuses to add again (`src/kernel/quot.cpp:50-56`), as `leanchecker` leaves them out (`src/LeanChecker.lean:68-71`).

- **Proved**: `mem_cone`, that the checker's search gives exactly what its seeds reach; `mem_cone_env`, that this is `InCone`, the cone in the terms of the environment; `replayConstants_env`, that what the replay is given is exactly the cone, each constant as `Environment.constants.map₁` keeps it, but the companions of `Quot`; `inCone_mentions`, that the cone is closed under what its names mention; `claimed_inCone`, that each constant of a claimed module is in it; `claimed_theorem_replayed`, that each theorem of a claimed module, as its own module states it, is the kept constant by `==` or is given to the replay under a name of its own, with `copy_name_fresh`, that no constant of the environment has such a name, and `copyEntries_nodup`, that no two copies share one; `kernelNames_eq`, the list stated as a literal apart from the checker's; and `plain_exit_zero` and `full_exit_zero`, that exit 0 needs the replay's success on that map, by `Replayed`, for every response.
- **Assumed** (`replay`, `kernel`, `h6`): that Lean's replay answers with success only when Lean's kernel accepted each constant of the map that is neither unsafe nor partial, each after the constants of the map that it mentions, with each constructor and recursor equal to what the kernel made of its inductive type, and that a constant that one of them mentions and that the map does not hold is unknown to the kernel, which refuses what mentions it (`Lean/Replay.lean:59-63`, `74-140`, `148-190`). For no false refusal, that the kernel looks up no constant beyond those that the cone follows and `Input.kernelNames`.

So, for a project that places no file or code aimed at the checker or the toolchain, a pass means that the proofs of the claimed modules are sound, checked by Lean's kernel in an environment that holds the cone of the claim and nothing else, and that each axiom they reach through what each constant mentions is one that the profile allows (RG1002 to RG1005, over the same relation). A project that may be aimed at the checker needs the full verdict, as [a project aimed at the checker](#a-project-aimed-at-the-checker) states. An unsound proof in a dependency that the claim reaches fails the replay, as one in a claimed module does. The replay skips each partial or unsafe constant, as Lean's replay does (`Lean/Replay.lean:182`): RG1006 refuses each such constant of a claimed module but the exempted form, and the kernel refuses a safe constant that mentions one (H6). Lean's import keeps one of the theorems of one name and type that its modules state, the last, and gives the name the first module's index (`subsumesInfo` and `finalizeImport`, `Lean/Environment.lean:2269-2275`, `2336-2345`). So the replay also gets each theorem that a claimed module's own data states and that `==` does not relate to the kept one (`Facts.copies`), under the name `root.k`, whose root has more components than any name of the environment (`copyRoot`). Its value's mentions are in the cone, because the cone also starts at each name that a claimed module's own data states, and what a name mentions includes what each copy of it mentions. **Measured** on 2026-11-02: in a project whose two modules each rewrite with `f.eq_def`, Lean regenerated that lemma in both, and the copies differ from the kept one under `==`, as 16 copies of Lean's own library loaded there do, so refusing such a copy would refuse ordinary projects. What only `Input.kernelNames` reach is replayed and is no part of the claim, so its axioms are not counted, as `#print axioms` does not count them: the kernel needs those constants declared to check a term that holds a literal, which mentions none of them.

RG1011 refuses each constant of a claimed module that has `@[implemented_by]` or `@[extern]`, so a pass says that neither attribute replaces the compiled code of a constant of the claim that the environment keeps. Beyond that it says nothing about what a compiled program runs. A claimed module can still change that with `@[csimp]`, which no rule reads, on its own theorem or on a dependency's, or with a constant of the exempted form that its own code adds during the build, whose form RG1006 reads and whose value no rule reads, and a claimed constant can call a dependency's or the toolchain's constant that has either attribute. [RG1011](#rg1011-replaced-compiled-code) states what it reads and leaves out. **Measured** on 2026-10-31, before RG1011: a module with each of `@[implemented_by]`, `@[extern]` and `@[csimp]` passed `lake build --wfail`, `lake check` and `lake lint`.

RG1012 refuses each definition or opaque constant of a claimed module whose value mentions a panic form, so a pass says that no such value mentions one of Lean's four panic functions or a constant that is no theorem and that Lean names with `!`. A claimed function can still reach a panic inside the code of a dependency or of the toolchain, through a constant whose name has no `!`, or in C code behind `@[extern]` of such a constant. [RG1012](#rg1012-hidden-panics) states what it reads and leaves out.

**Measured** on 2026-10-31, before the checker replayed anything: a module that added a theorem of `False` with `set_option debug.skipKernelTC true` passed `lake build` and `lake lint`, and `lake check` refused it. **Measured** on 2026-11-02 on a disposable project at Lean 4.35.0: `lake check --inadvisably-no-sandbox` passed a module that added, under that option, a theorem `hidden._bad : False` whose name Lean marks as internal (`Name.isInternal`, `Lean/Data/Name.lean:125-128`) and that nothing mentions, because `lake check` exports from each constant whose name is not internal (`LeanExport/Basic.lean:463-474`). The checker of the release `v0.12.0` passed it too, with exit 0, and `lake build` printed no warning, so the three commands of that release passed a theorem of `False`. The checker of this revision gave `proof verdict: incomplete (RG2001)`, exit 2, with Lean's answer `(kernel) declaration type mismatch, 'hidden._bad' has type True but it is expected to have type False`, and on the same project without that theorem it passed.

**Measured** on 2026-11-02, the replay on a project that imports Mathlib: Acorn, a public Lean project, at commit `5fbece44` of its `main`, in a copy whose `lakefile.lean` requires this revision of Regula by path, states the profile `standard-logical`, drops the plugin of the earlier Regula it pinned, and makes its proof library `AcornVerif`, which imports Mathlib, a default target beside `acorn-core`. With Mathlib's own cache (`lake exe cache get`), `lake build --wfail` ran 3,775 jobs in 267 s with a peak footprint of 3.4 GiB. `lake lint` then read 240 claimed modules and 24,121 of their constants, replayed their cone, which Lean's kernel accepted, and gave `proof verdict: fail` with four RG1006 findings, loops in Acorn's host code, in 112 s, with a peak footprint of 4.3 GiB for its whole process tree, sampled every 2 s, on a 24 GiB Mac with the named release of macOS. `lake check` exports and replays the whole environment that such a build imports, which [issue 541](https://github.com/rbeauchamp/regula/issues/541) records as 496,347 constants of 5,585 modules for the same project, unfinished after almost four hours at a footprint of 39 GB.

The checker imports the modules of the default targets into one environment, as `lake check` does. So a project of two default executables that each declare `main` fails it. Lean refuses two imported modules that declare one name with different values (`Lean/Environment.lean:2336-2344`), with the exception that [the section on the loader](#from-a-build-to-the-input) states.

### A project aimed at the checker

The two commands of the proof verdict run in the project's own Lake, which loads what the project placed and runs its code. So what a pass means, above, holds for a project that places no file or code aimed at the checker or the toolchain. A project that may be aimed at them needs the full verdict. A project with a dependency or with Mathlib in its imports gets only the proof verdict, so Regula gives no verdict that holds of such a project if it is aimed at them. A project aimed at the checker can make `lake lint` print a pass and exit 0 whatever its build holds, an unsound proof included, by each of these routes, and the full verdict closes each:

| Route | How it reaches the proof verdict | How the full verdict closes it |
| --- | --- | --- |
| A library under a leaf name that the checker uses, such as `libc++.1.dylib` on macOS or `libc.so.6` on Ubuntu, in the project's library directory | `lake lint` starts the checker with `DYLD_LIBRARY_PATH`, or `LD_LIBRARY_PATH` on Ubuntu, naming the toolchain's library directories and then each package's, the project's `.lake/build/lib` by default (**Assumed**: `lakeStart`), and the loader takes a library by its leaf name from such a directory before the paths that the checker records and the system's (**Assumed**: `processes`). A library built to resolve its own dependencies runs its initializers in the checker before `main`, so it can print any line and exit 0, argued from dyld(1), and on Ubuntu from elf(5), whose `.init` code the system runs before the program's entry point. No code of the project has to run first. **Measured** in [what was measured](#what-was-measured), and on Ubuntu in [Ubuntu](#ubuntu). | Its checker starts from a checkout built apart from the project, so its search path names the toolchain's directories, the checkout's and what the operator's own environment holds, and its Lake commands start through `/usr/bin/env -i` with no such variable (`spawnLake_eq`). **Measured** in [what was measured](#what-was-measured), and on Ubuntu in [Ubuntu](#ubuntu). |
| A doctored copy of Regula | `lintDriver` names an executable as the project's workspace resolves it (`Lake/CLI/Actions.lean:89-100`), so the project's configuration, manifest and package directory choose the copy that runs, and Lake keeps a checkout in the package directory that is at the manifest's revision with only a warning of local changes (`Lake/Load/Materialize.lean:44`, `:55-58`, `:106-107`). Read from the source. | Its checker is the operator's checkout, and a project with a `require` gets no build (exit 3). |
| A `lakefile.lean` | Lake elaborates it, running its code, when `lake lint` loads the workspace, before the checker starts, and the checker's own load prefers it too (`Lake/Load/Package.lean:109-117`, `Regula.Load.lakeCalls`). Read from the source. | Refused by name before any Lake load (RG1010), and nothing answers to that name in the tree that Lake builds (`Reason.configShadowed`, H5). |
| Code that runs while the project builds | It runs in `lake build --wfail` with the operator's rights, so it can write the first route's library or change the program that `lake lint` starts, as [outside the contract](#outside-the-contract) says. | The language check refuses such code before anything is compiled, under H1 and H2. |

No mechanism is added on either route, because none on the proof verdict's route closes all four: a link argument that makes the loader ignore `DYLD_*` for the checker closes the first alone, while the project's `lakefile.lean` and its build-time code still run before the checker. A project aimed at the checker is [outside the contract](#outside-the-contract) of the proof verdict.

## The language check

Before anything is compiled, the check reads each Lean file Lake would compile for the claim, and the project's Lake configuration, and refuses anything outside a closed set. If it admits the project, the gate builds it, replays the cone of its claim and runs the rules on the result. A project whose Lake configuration has a `require`, or with Mathlib in its imports, can have only the proof verdict: the gate says so, builds nothing and exits with 3, and the operator gets that verdict with the two commands of [what a pass means](#what-a-pass-means) in the project, which run the project's code and its dependencies'.

The gate is `REGULA_FULL=DIR lake exe lint PROFILE`, from a checkout of Regula built apart from the project. Lake loads a project's configuration before anything Lake starts can run, and a `lakefile.lean` that runs can delete itself or plant a checker, so a run that the project's Lake started says nothing that can be trusted of a project aimed at the checker, as [a project aimed at the checker](#a-project-aimed-at-the-checker) states of the proof verdict. Starting the checker from its own package is a precondition of the full verdict, beside the `PATH` it runs with, and a start from a project's Lake is outside this contract. Regula does not test it: a project's code that ran first can make any program print any line, so a test would be no defence against what it is for, and a checkout whose `.lake` is a link shows that such a test can refuse a healthy start. [The confirmation record](confirmation.md#the-language-check) holds the restatement that the owner confirmed, the status of each consequence, and the second reading. The formal statement is `languageRecord` and `fullGateRecord` in [`RegulaSpecification/Language.lean`](RegulaSpecification/Language.lean).

**What selects what is audited.** The arguments of a run are one profile, and anything else is a refusal (`run_other`). A project's Lake configuration sets the arguments of its lint and test drivers (`lintDriverArgs`, `testDriverArgs`, `Lake/CLI/Actions.lean:71-100`), so it can name a profile and no directory. Which run this is, and on which directory, is the answer for `REGULA_FULL` alone (`run_subject`), which Lake passes on from whoever started it: `lakefile.toml` has no key that sets a variable, and Lake adds only the fixed list of `Workspace.augmentedEnvVars` (`Lake/Config/Workspace.lean:417-433`), whose values it composes and which does not hold this name. **Assumed** (`lakeStart`). Regula's package declares one executable, `lint`, whose root runs `Regula.Shell.run` (`lakefile.toml`, `Regula.LintMain`), so `lintDriver` reaches nothing else of Regula. A pass names what it audited at the end of its last line (`Report.labelOn`, `Verdict.proofLineOn`), with LF and CR displayed as escapes, so a path changes neither the words of the verdict nor the number of lines. For the proof verdict that is the current directory's real path, from which the workspace it read was loaded (`plainRun_pass`). Nothing on this path reads where the checker lies, so a `.lake` that is a link, or a `:` in the checker's path, changes nothing.

**What a pass of the proof verdict says of Lake's selection.** `plainRun_pass` states all of it, for every response: the last line names the current directory's real path, Lake's load of that path gave the workspace that the run read, and the search path that the run got starts with that workspace's (`SearchPathStarts`). On the published run, `lake lint` from the project's directory with no option of Lake's, that workspace is the one Lake selected, because Lake then takes `.` and `lakefile` (`Lake/CLI/Main.lean:47-48`, `:132-138`) and the checker's load takes the same two (`Lake/Load/Config.lean:44`, `Regula.Load.lakeCalls`). **Assumed** (`lakeStart`, `lakeLoad`). A project's configuration sets neither option. `lake exe lint PROFILE` from that directory is no second way to run: Lake starts the program through the same call, with the same working directory and environment (`Lake/CLI/Actions.lean:20-30`, `:98`), so with the same profile the program gets what `lake lint` gives it. `lake -d`, `--dir`, `lake -f` and `--file` are outside the contract, and so is every other option of Lake's. Such a run still audits the workspace in the current directory with its `lakefile`, and its last line names that directory, which is all that it says about who was asked for: it can exit 0 with a pass about the current directory and not about the project that the option named, as when that project sets its build directories to those of the current one. The owner confirmed this narrowing on 2026-11-02, with that risk, in [the confirmation record](confirmation.md#2026-11-02).

This is what Lake makes available, and no check of this program could say more. Lake starts a driver in its own working directory, with no `cwd` and with `Workspace.augmentedEnvVars` (`Lake/CLI/Actions.lean:20-21`, `:98`, `Lake/Config/Workspace.lean:417-433`). The variables that hold a directory of the workspace are built from a package's `dir` joined with `buildDir`, `leanLibDir`, `binDir`, `nativeLibDir` or `srcDir`, which a project sets, and a join with an absolute path gives that path (`Lake/Config/Package.lean:228-229`, `:356-357`, `:364-365`, `:382-383`, `:386-387`, `Init/System/FilePath.lean:127`). `LAKE_CACHE_DIR` holds the workspace's `.lake` only when the environment names no cache, and under elan it names the toolchain's (`Lake/Config/Workspace.lean:31-35`, `Lake/Config/Env.lean:192-204`). So when a project `P` sets `buildDir` and `srcDir` to those of a workspace `Q`, `lake -d P` from `Q` gives a program the working directory, the arguments and, byte for byte, the environment of `lake` in `Q` (**measured**, [below](#what-was-measured)). Whatever is a function of those three gives both runs one answer, and the run in `Q` has to pass. `SearchPathStarts` therefore identifies nothing. It is kept for what it does: an ordinary `lake -d P lint` from another workspace, which takes no setting of `P`'s, gets a refusal in place of a pass about the wrong directory (**measured**). A same start says nothing, and `lake -f` leaves it as it was. Two things could tell such runs apart, and neither is here. A Lake script is handed the workspace (`Workspace.dir`, `Lake/Config/Workspace.lean:117-118`), but only `lakefile.lean` declares one, which RG1010 refuses in the checker's own package, and it would be another way to start the checker. The command line of the parent process would need a hand-written reader of Lake's options.

**What each Lake command is given.** Every Lake command that the gate runs gets a closed environment: `spawnLake` starts it through `/usr/bin/env -i` with `PATH=/usr/bin:/bin` and `LAKE_ARTIFACT_CACHE=false`, and no other variable (**stated by `rfl`**: `spawnLake_eq`). So no variable of Lake's composition (`Workspace.augmentedEnvVars`, `Lake/Config/Workspace.lean:417-433`, `Env.baseVars`, `Lake/Config/Env.lean:289-303`) reaches it, whatever Lake started this program or whatever the operator's shell holds: a `which`, `git`, `env` or `libtool` planted under a project's `.lake/build/bin`, or a library under its `.lake/build/lib`, is on no search path of the command. The program itself starts with what its starter composed, and the loader of the operating system reads that before `main`: it looks for each library that the program uses by its leaf name in each directory of `DYLD_LIBRARY_PATH` first, and on Ubuntu in each directory of `LD_LIBRARY_PATH` first for a program that records no `DT_RPATH` (**Assumed**: `processes`), as the checker records none (**measured**, [Ubuntu](#ubuntu)), and `lake exe lint` sets that variable to the toolchain's library directories, then each package's library directory of the checkout's workspace, then what Lake inherited (**Assumed**: `lakeStart`). So on the full verdict's start no directory of the project is on that path, unless the operator's own environment names one. On the proof verdict's start the project's library directory is on it, which [a project aimed at the checker](#a-project-aimed-at-the-checker) states with what follows. On Ubuntu the loader took a file planted in a project's `.lake/build/lib` when that project's Lake started the checker, and not when the checker's own package started it (**measured**, [Ubuntu](#ubuntu)). `IO.Process.SpawnArgs.inheritEnv := false` would say the same directly, and it ends with a segmentation fault on macOS at this tag (**measured**). A machine with no `/usr/bin/env` gets no build and no pass.

Every Lake call and child process of the gate works in a tree the checker made for this run, a new directory from `IO.FS.createTempDir` into which it writes only the `lakefile.toml` and `lean-toolchain` and, once the decision has admitted the whole reading, the text of each file it judged, and that it asks to remove afterwards. So no name, link or file of a project can select a path outside that tree, whatever Lake derives at this or a later version, and the verdict is about the text read. The project's directory is read by the checker alone, and is not written. Its `.lake`, its manifest and its other files are not read at all. A tree left by a crash can affect nothing later, because each run makes a new one. Three reviews of the earlier form, which ran Lake in the project's directory, each found another path that Lake derives from it, so the class is closed by leaving that directory.

### The closed list of refusals

Regula publishes which runs it refuses, and it proves of each refusal that it is true of what Lean, Lake or the operating system answered in that run. So "no false refusal" means that a refusal is never untrue. It does not mean that every reasonable project passes. The owner confirmed that on 2026-11-01, in [the confirmation record](confirmation.md#what-no-false-refusal-means), and withdrew the earlier statement of who is owed a pass: nothing tied a description of a project to its real files except assumptions, and Lake's load depends on axioms outside Regula's own profiles, so no correspondence with it could be proved under them. `Regula.Shell.run` refuses in no other way, on any response (`run_meets`). **Proved** the other way: a run with no refusal, on which the rules hold, passes (`full_owed`, `run_full_owed`, `plain_owed`, `run_plain_owed`), so a program that refuses everything does not meet the contract (`refuser_fails`).

Each case of the table below, and each of `PlainReason`, `TreeReason` and `BuildRejected`, is a constructor of a closed type, stated over the events of the run, and so is the error of `Replayed`, which is the answer of Lean's replay of the cone of the build's own input. A case that names a build's input is bound to the requested build by `Scene`, `Named` and `Needed`, so an unrelated answer justifies nothing.

**The language check** (`Reason`, in [`EffectsRecord.lean`](RegulaSpecification/EffectsRecord.lean)). Exit 1 and an RG1010 line for what is refused, exit 2 for `incomplete` (RG2001), and exit 3 where only a proof verdict is possible, as each row says. Nothing is built in any of them.

| Case | What the run was answered | Exit |
| --- | --- | --- |
| `toolchain`, `toolchainFailed`, `toolchainNotExact`, `toolchainNoReal` | `lean-toolchain` names another Lean, cannot be read, has no real path, or is not, by its real path, that path below the project. | 1 |
| `leanConfig` | Something has the name `lakefile.lean` in the project. | 1 |
| `key` | `lakefile.toml` has a key outside the closed set (`configKeys`, and `leanOptions` with an option of `options`). A `srcDir` on a library or an executable is such a key, and so is a plugin. | 1 |
| `deep` | `lakefile.toml` lies deeper than the reader follows. | 1 |
| `openDir` | A source directory is not below the tree, or a component below it holds anything but ASCII letters and digits, `_` and `'`. So a source directory with a space or a non-ASCII name is refused, and so is one with a hyphen. | 1 |
| `openGlob` | A `globs` entry is no single module. | 1 |
| `notLibrary` | A default target is no library. So a default executable is refused, the `lake new` application template among them, and so is a default target that names nothing. | 1 |
| `file` | A file the build needs is not in the closed language, read as Lean reads it in the context that the file sees. | 1 |
| `dependency`, `deepDependency` | `lakefile.toml` has a key with the root `require`, or may have one deeper than the reader follows. | 3 |
| `mathlib` | A module the build needs has the root `Mathlib`. | 3 |
| `failed` | An operation that the build needs answered with a failure (`Needed`): `LEAN_SYSROOT`; the real path of the project, the tree, `lakefile.toml` or a needed module's file; the test of the name `lakefile.lean` in the project or the tree; a read of `lakefile.toml` or of a needed module's file; Lake's TOML parser; a write of `lakefile.toml`, `lean-toolchain` or a needed module's file in the tree, or the directory above it; a library's modules; Lean's header parser; Lean's search; or an import for the parser. | 2 |
| `load` | Lake's load of the copied configuration failed. | 2 |
| `tomlNotExact`, `moduleNotExact` | The file is not, by its real path, the path named: it crossed a link, a name on the way is stored in another case, or it lies outside the project. | 2 |
| `notApart` | The project and the checker's tree do not lie apart. A `TMPDIR` inside the project gives this. The owner's delegated agent kept this refusal in place of a stated precondition, because a write in such a tree would be a write in the project. | 2 |
| `configNotInTree`, `moduleNotInTree` | A file to copy, or the directory above it, does not lie below the tree, so nothing is written there. | 2 |
| `noClaim` | The default targets claim no module. | 2 |
| `targetName`, `moduleName` | A target's or a needed module's name is outside `ClosedModuleName`. | 2 |
| `rootElsewhere` | Lake's import resolution does not give a default root its own file, by components. | 2 |
| `twoTexts` | What an admission would have the tree hold is two texts at one path. | 2 |
| `treeDiffers` | A planned file, after its write, read back as another text or failed. | 2 |
| `configShadowed` | Something answers to `lakefile.lean` in the tree after the reading's last act. | 2 |
| `tooMany` | The roots and imports are more names than the reader follows. | 2 |

**Around the check.** A Lean other than the pinned one, or an argument list other than one word, or a text that is no profile, gives exit 2 and the last line of an incomplete proof verdict (`Refusal`). A failed `createTempDir` gives exit 2 (`FullRun`). The build ending with other than 0 gives `full verdict: fail`, exit 1 (`BuildRejected`). After a build that ended with 0, the tree having no real path, a failed load of the tree, or a failure of a default library's modules, of the import for the rules or of Lean's search for a module of that import gives `full verdict: incomplete`, exit 2 (`TreeReason`, `BuildFailed`), and so does Lean's kernel not accepting the replay of the claim's cone (`Replayed`). On the plain path `proof verdict: incomplete`, exit 2, comes from `LEAN_SYSROOT` or `LEAN_PATH` not being set, a current directory with no real path, a failed load of the workspace there, a search path that does not start with that workspace's, or those same failures of its finished build (`PlainReason`, `BuildFailed`), and from the kernel not accepting the replay of the claim's cone (`Replayed`).

**The rules.** A finding gives `fail`, exit 1, by the rule's `rgN_exact`. An input that the admission refuses, or a constant that the loader refuses, gives `incomplete`, exit 2 (`admit_ok_iff`, `Facts.unread?`).

**What the list decides, and what the owner's delegated agent decided.** The refusal of a default executable, of a target's `srcDir` and of a source directory with a space or a non-ASCII name is the owner's. The rest of the list is the agents' design, derived from that confirmation and open to change while its words hold: that a source directory's characters are those of a module name, that a default target naming nothing goes with a default executable, that `notApart` stays a refusal, and that no new rule refuses module files that differ only by case, which the read-back and the exact-path test answer below.

**Paths by components.** A path counts by its components, as `parts` reads them: `.`, `./`, the empty string and `.//` name none, and `a/b`, `a//b`, `./a/b/` and `a/./b` name the same two. This reads the text and takes no file system: on POSIX a `.` component and an empty one change nothing, and it follows no link and folds no case. `Regula.Reader.configUnread`, `Reason.rootElsewhere`, `Evidence`, `twoTexts`, `written`, `exactBelow`, `treeRelative`, `apart` and `below` compare paths by these components. The name that Lean's parser gets for a file is a function of its components too (`Regula.Load.inputName`), so a reading depends on a path by its components alone (`ReadText.respell`).

For the proof verdict, `startsSearchPath` checks whether the whole search path loaded for the current workspace is a prefix of the parsed `LEAN_PATH`, with exact string equality for each entry. **Proved**: `startsSearchPath_eq_true_iff` relates that decision to `SearchPathStarts` for every received string and root, which says nothing of which workspace Lake selected. What Lake supplies remains trusted. The full verdict's startup contract is the [precondition on the start](#the-language-check). A default executable keeps its proof verdict: the plain path still claims its root (`DefaultModules`), because every build gets a proof verdict.

**What a volume decides.** A file that the volume of the tree takes for `lakefile.lean`, by case folding or otherwise, is `configShadowed`. A root module `LakeFile` on a case-sensitive project and tree passes (argued, not measured). On a case-folding project the test of the project's own `lakefile.lean` answers first, which is RG1010. Where the project's test found nothing and the tree folds, as a project on another volume or a file created after that test gives, the run gets `incomplete` (**measured** for the second). Two module files that a volume takes for one, with different texts, are `treeDiffers` (**measured**). The same project can therefore get different verdicts on two volumes. Which file a name reaches is the file system's to say, so the check asks it through the name Lake uses and models no folding.

**What this leaves unsaid.** A file that another process changes between two reads is no statement of the project: a change the run does not see is left unsaid, and an admission is about what the run read and what the file system answered.

**Outside the contract.** Two classes of input get no refusal, so the claim of no crash on an admitted input does not reach them. The owner's delegated agent decided that on the owner's behalf, under the owner's rule that a refusal outside the narrow published contract is not a false refusal: each is visible and cheap to undo, and a guard would add an operation, a reason and its proofs while leaving a race. The first is a call that does not return. Every theorem about a run is over the responses it got (`Runs`), and none says that a response comes. So a run held at an operation of `Regula.Effect.Op`, or at a call that Lake or Lean makes inside one, ends in no verdict and no exit code of its own, whichever file or command it is. The plain instance is a FIFO that nothing writes, at any path that the checker, Lake or Lean reads: `lean-toolchain`, `lakefile.toml` and a module's file (**measured** in [what was measured](#what-was-measured)), an `.olean`, a file in the tree or a manifest (argued from the same blocking read). A `lake build` that does not end is another. There is no timeout and no test of a file's kind, because a timeout says nothing of what the file holds and a test before the read leaves a race. Where another process writes to a FIFO, the read gives that text, and what is judged and copied is that text, which is another process and left unsaid above. A `TMPDIR` naming nothing ends the process inside Lean's own `IO.FS.createTempDir` with signal 11 at Lean 4.35.0, exit 139 and no last line (**measured** in [what was measured](#what-was-measured)). Exit 0 cannot result from it, because the exit code is what the program's value gives. Every platform but the one that [the trusted base](#the-trusted-base) names is outside as well.

### What it reads, and how

| Input, in this order | Through | On a failure or anything unknown |
| --- | --- | --- |
| That the checker's tree and the project lie apart | `Regula.Reader.apart` | A project at or below the tree is `incomplete`, or a tree at or below the project, because a write in the tree would then be a write in the project. |
| `lean-toolchain`, by name, by the exact-path test below | The file system | Anything but the pinned text is refused, and so is a file that fails that test. The checker builds with the Lake beside its own Lean, so this file chooses nothing, and a project that names another Lean is told so. |
| `lakefile.lean`, by name, a link with no target included, before any Lake load (`Lake/Load/Package.lean:109-117`) | The file system | Refused (RG1010): Lake prefers it and runs it. |
| `lakefile.toml`, by the exact-path test below | Lake's own TOML parser (`Lake.Toml.loadToml`), as key paths | A key outside `configKeys` and outside `leanOptions` with an option of `options` is refused, and a later Lake's new key is refused the same way. A key with the root `require`, the one key Lake decodes a dependency from (`Lake/Load/Toml.lean:499`), stops the reading before any Lake call, with only the proof verdict left. No manifest is read. Otherwise the same text goes into the tree. |
| The root package | `Lake.loadWorkspaceRoot` on the tree, with `relConfigFile := "lakefile.toml"`, which loads the root's configuration alone and does not prefer `lakefile.lean` (`Lake/Load/Workspace.lean:31-47`, `Lake/Load/Package.lean:100-105`), and which lists no directory | A failure is `incomplete`. |
| The configured paths and targets: the source directory of the package, of each library and of each executable, which with no `srcDir` on a target is the package's, each `globs` entry of each library, and each default target | `Regula.Reader.openPathsOf`, on what `Regula.Workspace` projects from Lake's load | A source directory that does not lie below the tree by `treeRelative` (**proved**: `treeRelative_iff`, `treeRelative_no_parent`), so an absolute one, one with `..` and one with a component that starts with `.`, or one with a component below the tree that holds anything but ASCII letters and digits, `_` and `'` (`closedSourceDir_iff`), or a library with a `globs` entry that is no single module (`Glob.one`), or a default target that `findLeanLib?` does not find, is refused (RG1010, `Reading.openPaths`, which `ConfigClosed` requires empty). A closed `Glob.one` lists nothing (`Glob.forEachModuleIn`, `Lake/Config/Glob.lean:53-59`). The tree holds no source at this point, so a listing would find nothing. |
| The default targets' modules, and only after the row above | `LeanLib.getModuleArray`, on single modules | A library's or an executable's name outside `closedModuleName`, which Lake joins onto an output directory (`LeanExe.file`, `Lake/Config/LeanExe.lean:72`), is `incomplete`, and so is a default root that `findModule?` does not give its own file. |
| The modules to read | Each default root by its own `Module` file, each import through `Lake.Workspace.findModule?`, which is Lake's own resolution of an import (`Lake/Build/Module.lean:37`, `Lake/Config/Workspace.lean:279`), and otherwise the toolchain's search path | A name outside `closedModuleName` is `incomplete` before any path is built from it. A module that neither holds is `incomplete`: the toolchain's library directories are the whole search path while reading, so what Lean's search finds there is the toolchain's. A non-default library's module that a default target imports is read. |
| Each file's header | The same relative path of the project, by the exact-path test below, then `Lean.Parser.parseHeader` on the text the frontend reads (`Lean/Elab/Frontend.lean:287`, `Lean/Shell.lean:519`, `Lean/Language/Lean.lean:451`). That same text goes into the tree only for a reading the decision admits. The checker reads a file as UTF-8 and the frontend decodes it lossily, so a file that is not UTF-8 fails the read | A file that fails the test, or that cannot be read, is `incomplete`, so a link at any depth on the way to a file leaves it unread. The report names the file's lexical path and never where it leads. |
| Each file's commands | `Lean.Parser.parseCommand`, with H1's context | A parse error, `.missing` or a file that the parser did not read to its end is refused. |
| The name Lake prefers as its configuration, in the tree, after the reading's last act | `Regula.Reader.noOtherConfig`, through `symlinkMetadata`, for an admitted reading | Anything that answers is `incomplete` (`Reason.configShadowed`): Lake's command line asks for a configuration with no extension and prefers `lakefile.lean` whenever it resolves (`Lake/Load/Package.lean:109-117`, `Lake/CLI/Main.lean:48`), so that file would be what Lake runs. A failed answer other than no such name is `incomplete` too. |

Mathlib stops the walk: a module whose root is `Mathlib` is recorded and not read, and only the proof verdict is left. `MathlibReached` stays a test of the name's root on the modules of `reached`.

**The exact-path test** is `Regula.Reader.readExact`, which asks the operating system for the real path of a path and passes it to the pure `Regula.Load.exactBelow`. By components with `.` removed, the real path must equal the lexical path, and the project's real path must be a prefix of it (`ExactlyBelow`; **proved** in both directions: `exactBelow_eq_true_iff`). So a link at any depth on the way makes them differ, and an absolute path outside the project lacks the prefix. A `..` needs no case of its own, because a real path holds none (**proved** on that hypothesis: `exactBelow_no_parent`; the hypothesis is the operating system's). The project's own real path is the base, so a project below a link, or under macOS's `/tmp`, passes.

The closed domain of module names is `ClosedModuleName`, which `closedModuleName` decides (**proved**: `closedModuleName_iff`): at least one component, each a non-empty string of ASCII letters and digits, `_` or `'`. `modToFilePath` joins each component onto a directory and `FilePath.join` discards its base for an absolute component, so a quoted name such as `«/abs/vendor/Evil»` or `«..»` (**proved** outside the domain: `absolute_name_not_closed`, `parent_name_not_closed`) would otherwise select a path outside the project.

### The closed set

The tables are data, in [`lean/Regula/LanguageSet.lean`](../lean/Regula/LanguageSet.lean). A construct is in them only if, read at the pinned Lean: Lean's toolchain declares its parser, its elaboration evaluates no code that the file writes or names, it changes no parser state a later command reads, and it installs no replacement for compiled code. That is the criterion each entry was read against, and H2 is what depends on it being read correctly. The set is what real library code uses and meets that criterion, so it is not every construct that meets it: anything else is refused, visibly, until someone reads it.

| Position | The table | Why it is closed |
| --- | --- | --- |
| A node's kind | `kinds` | Refuses each kind not read, including all that a later Lean adds. |
| A token | `atoms` | A token can sit in an optional position of an admitted kind, such as `meta section`. Refuses each not read. |
| An identifier | No component starting with `_`, other than a first `_root_`, and no `autoParam` | The compiler reads names of those forms by their form (`Lean/Compiler/LCNF/ToDecl.lean:25-27`), and `Lean/Elab/App.lean:832` evaluates what `autoParam` names. |
| `@[name]` | `simpleAttributes` | `Lean/KeyedDeclsAttribute.lean:166` and `Lean/Meta/Tactic/Simp/Simproc.lean:130` evaluate a named definition, and `implemented_by`, `extern` and `csimp` replace compiled code. |
| `set_option`, `leanOptions` | `options` | `debug.skipKernelTC`, `match.ignoreUnusedAlts` and `internal.parseQuotWithCurrentStage` change what is checked or parsed. |
| A tactic's `+item` | `configItems` | `+native` is a native proof. A `(config := ...)` is refused by its kind, because `Lean/Elab/Tactic/Config.lean:151` evaluates its value. |
| A `deriving` class | `derivingClasses` | A handler is code. |
| `namespace`, `open` | No start of the target may end a namespace that holds scoped parser entries in this file's environment | Keeps the parser's context constant: see H1. `open X (names)` activates nothing (`Lean/Elab/Open.lean:90`), so it needs no test. |
| The header | `module` is required, with the same tables for the rest, so `meta import`, `import all` and `prelude` are refused | In a `module` file with no `meta`, Lean itself refuses to evaluate a project's constant (`Lean/Compiler/IR/Meta.lean:56-59`, `Lean/Environment.lean:2537`), so a route that the table misses still meets Lean's check. |

The kinds of `leafKinds` hold open text, such as a string's or a comment's, and the check does not enter them. Thus `"run_cmd"` in a string or a doc comment is not a construct.

### H1 and H2

These are hypotheses about what Lean v4.35.0 does. They are stated in `LeanBehaviour`, never as axioms. No proof in Lean can reach them, because `Lean.Parser.parseCommand` is `partial` (`Lean/Parser/Module.lean:135`) and Lean's elaborator has no model here. The owner confirmed that a hypothesis of this kind, re-read at each upgrade of Lean, counts as Lean staying trusted. So "no bugs" here means no bug outside these stated, version-bound claims.

**H1: the tree the check read is the tree Lean elaborates.** The frontend calls the same `parseCommand`, with state from the elaborator (`Lean/Language/Lean.lean:595-601`). The parser reads that state only as scoped parser entries and tokens (`Lean/Parser/Extension.lean:607-612`, `Lean/Parser/Module.lean:124,146`), the option `internal.parseQuotWithCurrentStage` in quotations, the options `doc.verso` and `doc.verso.module` in doc comments (`Lean/DocString/Parser.lean:1375-1376`, `:1400-1407`, `Lean/Parser/Term.lean:92`, `Lean/Parser/Command.lean:61`), and namespace and open declarations when it resolves a parser's name in a quotation (`Lean/Parser/Extension.lean:765`). Quotations and the first option are refused. The two options of doc comments are not in the admitted `options` (**proved**: `Assumption.verso_options_not_admitted`), so an admitted file is parsed with both unset, as the reader parses it. Scoped entries activate only at `open` and `namespace` (`Lean/Elab/Open.lean:83,89,101`, `Lean/Elab/BuiltinCommand.lean:60`), and no target of an admitted file can activate a namespace that holds any. No admitted command adds a parser, so the project's own modules add none to the environment. So the reader parses each file with one context: the environment of the toolchain's modules that the file sees, no options, no namespace and no open declaration. It computes what a file sees from `importModulesCore`'s rule for a `module` file (`Lean/Environment.lean:2108-2190`): each direct import, and through it each `public` import, in `Regula.Reader.visibleToolchain`. Lean's own function cannot do this, because it follows `.olean` files and the project's modules have none before the check admits them. **Proved**: `mem_visible_iff`, that the function gives what `Sees` states, with the bound it is given. That `Sees` is Lean's rule is the one place where the reader states what Lean does, and H1 covers it.

A simulation of the elaborator's state is what H1 avoids: Lean's parser and elaborator disagree on what `open ... hiding` activates (`Lean/Parser/Extension.lean:624-626`, `Lean/Elab/Open.lean:101`), so a restatement of that state would be a place for a bug to enter.

**H2: what the closed set admits runs no code the project wrote, and installs nothing that replaces what the compiler runs for a definition.** Each entry of the tables was read against the criterion above. **Assumed** (`h2`), from reading each evaluation site that a search of Lean's sources for the whole words `evalConst`, `evalConstCheck`, `evalExpr`, `evalTerm` and `evalDecl` finds, as of v4.35.0. The search matches 61 files there. The entry `h2` cites the 26 whose sites are reached only through what the tables refuse, each with every line the search matches in it, and `Assumption.excluded` names each of the other 35 with why no admitted input reaches it: its matches are comments, docstrings or local names; it defines an evaluation function whose calls the search finds elsewhere; it is reached only through a construct the tables refuse, such as `initialize`, a parser attribute or `lakefile.lean`; only from a Verso doc comment; only by the language server or Lake's built-in lint; or it evaluates only constants that the toolchain declares, since declaring one in a project needs a construct the tables refuse. That the cited and the named files are the 61 is **measured** on 2026-11-02, by running the search at the tag and comparing. `Lean/Elab/Util.lean:108` is reached by Lean's own `autoParam` constants, which are the toolchain's code, and a project's is refused by the table and by Lean's check in a `module` file. A route in an admitted kind that this reading missed is a false pass, and that is what H2 stands for.

H1 and H2 say what a compile of admitted files runs. That nothing of the project runs before the check is no hypothesis about Lean: it is the precondition on the start and the reads by name above, measured below.

**At each upgrade of Lean:** `supportsLean` refuses any other release, so nothing passes until these are done. Diff the toolchain's kinds, and read what changed in each kind of the table. Run the search for evaluation sites again. Read again the sources of each entry of [the list of assumptions](#the-trusted-base), H1's with `importModulesCore`, and change its `readAt`: the build of this package fails until each is changed. Run the differential below.

### What is proved

Over every `Lean.Syntax`, in [`RegulaSpecification/Proofs/Language.lean`](RegulaSpecification/Proofs/Language.lean), about the definitions that the checker runs: `mem_positions_iff` (the walk lists exactly the positions the specification reads), `mem_offenders_iff` and `offenders_eq_nil_iff` (a position is reported exactly when it is one that is not admitted), `fileAdmitted_iff`, `closedModuleName_iff`, `treeRelative_iff`, `treeRelative_no_parent`, `decision_meets`, `decision_admitted_iff`, `no_files_not_admitted`, `dependency_not_admitted`, `mathlib_not_admitted`, `unclosed_module_not_admitted`, `open_path_not_admitted`, `offender_not_admitted`, `gate_meets`, `fullGate_o2Run` and `gate_exit_zero_iff`. **Proved** in [`RegulaSpecification/Proofs/Load.lean`](RegulaSpecification/Proofs/Load.lean): `exactBelow_iff` and `exactBelow_no_parent`, about the comparison alone. **Proved** in [`RegulaSpecification/Language.lean`](RegulaSpecification/Language.lean): `language_o2`, `language_o2Run`, `language_o3`, `language_o4` and `language_o5`, `fullGate_o2`, `fullGate_o3`, `fullGate_o4` and `fullGate_o5` (lean-intent's obligations, with O5 at equality, so the records leave nothing unsaid), `constant_fails`, `build_only_after_check`, `full_needs_no_mathlib`, `open_path_refused`, `lean_config_refused`, `require_not_admitted`, `unclosed_name_not_admitted`, `configKeys_no_require`, the tables against the other names of the families that the owner's words name (`refusedKinds_outside`, `refused_attributes`, `refused_options`, `refused_config_keys`), and `admitted_runs_no_project_code`, which only composes `admitted_iff` with H1 and H2 and adds nothing to them. **Proved** in [`RegulaSpecification/Proofs/Owner.lean`](RegulaSpecification/Proofs/Owner.lean), each with its expected value as a literal and over `decision` or the text that runs, so that no statement reads a table for it: `refuses_named_kinds`, `refuses_decide_native`, `refuses_lakefile_lean`, `refuses_plugin_key`, `admits_library_code`, `core_configuration_admitted`, `refuses_run_cmd_in_that_project`, `refuses_decide_native_in_that_project`, `refuses_another_toolchain`, `unread_kinds_are_open_text`, `proof_verdict_lines`, `full_gate_lines` and `verdicts_named`.

[The run of the checker](#the-run-of-the-checker) states what `Regula.Reader` and `Regula.Shell` do with what they receive: that an admitted `Reading` rests on what was read, that every file Lake compiles for the claim is read under H3, that the text the run's requests leave in the tree, which the file system answered, is the text it parsed, and the order of the gate with its effects. No theorem states that a file lies where the operating system says, that a child process stays in the tree it is started in, that the listing of a `globs` entry of a single module lists no directory, or that Lake's build and Lean's kernel replay do what their contracts say. Those are Lean's, Lake's and the operating system's, as [the trusted base](#the-trusted-base) lists.

### What was measured

**Measured** on 2026-10-31 at commit `c034e9d3`, before the run became a program of `Regula.Effect`, each case one disposable project, with `lake exe lint standard-logical full DIR` from a checkout of this revision, built apart from each project. The files of the case are the construct, after `module`, and `public section` or a `public import` as it needed. For each case below, every file of the project was the same before and after, by path, mode, size and modification time. A file named by a case's own code was never written.

- Refused with exit 1 and an RG1010 line, with no build: `run_cmd` with `import Lean` and with `meta import Lean`, each naming a file to write, `#eval`, `#guard`, `run_tac`, `by_elab`, `native_decide`, `decide +native`, `macro`, `syntax`, `notation`, `elab`, `initialize`, `@[local macro k]` on a plain `def`, `@[implemented_by]`, `@[extern]`, `@[csimp]`, `@[macro_inline]`, `open ... hiding`, `open` and `namespace` of a namespace with scoped syntax, `open Lean`, `open _root_.Lean`, `autoParam` naming a project's constant, a `:= by` default, a file that is not a `module`, `prelude`, `meta import`, `import all`, `meta section`, `meta def`, `unsafe`, `partial`, `#exit`, a parse error, `include_str`, `set_option debug.skipKernelTC`, `set_option match.ignoreUnusedAlts`, `simp (config := ...)`, `simp +arith`, `g._unsafe_rec`, `_unsafe_rec` inside `namespace g`, `g._boxed`, `#guard_msgs`, `try?`, `exact?`, `apply?`, `#check_failure`, a quotation, `deriving instance`, a `deriving` of a class outside the table, `grind`, `axiom`, `instance (priority := ...)`, a non-default library's module with `run_cmd` that a default target imports, the same with a decoy non-default executable root of that name whose file is admitted, `lakefile.lean` present, whether or not it is a link with no target, a `lean-toolchain` that names another Lean, is absent, or is a link, and each of `moreLeanArgs`, `plugins`, `buildDir`, `more-lean-args`, `leanOptions.debug.skipKernelTC`, `lean_lib.precompileModules` and `lean_lib.moreLeanArgs` in `lakefile.toml`. Each named its own construct. A `lakefile.lean` that writes a file stayed there and wrote nothing, because nothing loaded it.
- **The case of review finding R8:** `lake-manifest.json` as a dangling link to a location outside the project, and as a link to a file outside. Each got `full verdict: pass`, exit 0, with nothing written at the first target and the second unchanged, because the manifest is not in the tree.
- **What a project plants is unused.** A `.lake` with a garbage `Demo.olean`, a planted checker that would write a file, and a malformed `package-overrides.json`; and a `.lake` that is a link to a directory outside: each got `full verdict: pass`, nothing was written, and the link's target gained nothing. A stale manifest with no `require`, whose entry has as its name the absolute path of a victim Git repository: `full verdict: pass`, and that repository's untracked file stayed. A second run after a first also passes, and the project has no `.lake` after either.
- **Another process during the run:** a process that rewrote the source to a `run_cmd` and added a `lakefile.lean`, both writing a file, about a second after the run began, with the module's own `decide +kernel`. `full verdict: pass`, about what was read, and neither file was written. That this reached the build's window is not shown, since its timing was not observed.
- Refused with exit 1 on a configured path, with no build: a `srcDir` that is absolute at the package and at a library, one with `..` at the package, `lean/../lean`, one that starts with `.`. `globs = ["Data.+"]` with `Data` a link to a directory outside, whose file's name was not printed, and `globs = ["Data.*"]` over a directory of mode 000, with no permission error, so no listing started.
- `incomplete` with exit 2 and no build, with the file's lexical path in the report and not where it leads: a root's file that is a link, an `import` with a link on the way at the first and second level, a `srcDir` that is a link, and `lakefile.toml` that is a link. A `srcDir` that does not exist is `incomplete` too.
- `incomplete` with exit 2 and no build, the name's file never read: `import «<absolute path>»`, `import «../Evil»`, `import «..»`, `import «a/b»`, `import «a.b»`, a library name and a `lean_exe.name` that are absolute paths, a non-default `lean_lib.name` `../x`, a `roots` value with `..`, which Lake's load itself refused, and a `lean_lib.name` with a hyphen, which is a refusal of a harmless name that this closed domain accepts as a cost.
- `incomplete` with exit 2 and no build: no default target, `lake lint -- full DIR` in a project with the checker by path, and the checker asked to check the package that holds it.
- Exit 3, nothing built and no `.lake` directory, with the last line that says that only a proof verdict is possible, which two commands give it and that they run the project's code and its dependencies': a `require` as `[[require]]`, an empty `[[require]]`, `require = []`, `[require]`, `require = [{...}]`, `"require" = [{...}]`, `"re\u0071uire" = [{...}]` and a `require` by path, and a module that imports a stand-in `Mathlib.Stub`.
- Exit 0, `full verdict: pass`: a module with `simp`, `omega`, `decide +kernel`, `variable` and `deriving DecidableEq`; a module with a non-default library's admitted module that it imports; a project with no manifest; `roots`; literal `globs`; `srcDir = "./lean/"`; a project given by a link to it; a project under `/tmp`; a link to a directory outside that no root and no import reaches; and a project of 82 modules whose `public` imports form 2^40 paths to one module, in 57 seconds with its build. No tree was left in the temporary directory after these runs.
- Regula's own checkout, as a step of the local gate on this revision: `full verdict: pass`, exit 0, on the 22 modules of its default targets, `Regula.Reader`, `Regula.Table` and each rule's module among them. That also measures the choice that `Regula.Effect` imports `Lake.Toml.Data.Value` and `Lake.Config.Glob`: the full gate's replay and rules, and `lake lint`, passed with them in the default target, so those modules bring no axiom of Lake's families into the claim's cone. **Measured** on 2026-11-02 at the revision of pull request 542, before each rule had a module of its own: the gate's eight steps ended with 0, the full verdict and the proof verdict on this checkout read 15 claimed modules and 1,368 of their constants, and the proof verdict on this package read 46 claimed modules and 4,122 of their constants, each replayed by the checker.
- Plain `lake lint` on a built module, in a project that requires the checker by path: `proof verdict: pass`, exit 0.

**Measured** again on 2026-10-31 on this revision, as a diagnostic of the program over the real table: `lake exe lint standard-logical full DIR` on a compliant module gave exit 0; a `run_cmd` naming a file to write, whose `meta import` is refused first, a `lakefile.lean`, a `lean-toolchain` that names another Lean, a file that is no `module` and a `moreLeanArgs` key each gave exit 1 with an RG1010 line and nothing written; a `require` gave exit 3; a root's file that is a link, `import «../Evil»`, no `lakefile.toml`, a file that is not UTF-8, and a `TMPDIR` inside the project, which `Regula.Reader.apart` refuses, each gave exit 2. `lake exe lint` with no profile or a wrong one gave exit 2 with the last line of an incomplete proof verdict. Plain `lake lint` on a module with a `sorry`, in a project that requires the checker by path, gave four finding lines, a line of the count, the last line `regula: proof verdict: fail`, and exit 1. No tree was left in the temporary directory.

**The differential for H1**: for each file, the reader's trees against the commands of Lean's own frontend (`Lean.Elab.IO.processCommands`, with `processHeader`), compared by kind, atom and name, one process per file, with no time budget beyond 600 seconds a file. On the 13 files of Regula's default targets at commit `c034e9d3`, 374 commands: no difference. This is a search for a counterexample, not a proof. Only those files are admitted today, so the search reaches no file that the table does not admit.

**Measured** on 2026-11-01 on macOS's case-folding file system, as a diagnostic on a disposable project with `x/Foo.lean` held open as a pipe and renamed to `X` between its two reads, so that both exact-path tests passed for two names with different texts: `lake exe lint standard-logical full DIR` gave exit 2 and `RG2001: … x/Foo.lean does not hold the text written to it`, with no build and no tree left. An earlier revision gave `full verdict: pass` on that input, with the second text standing.

**Measured** on 2026-11-01 at the change that makes the reader judge before it writes, as a diagnostic with `lake exe lint standard-logical full DIR`, each on one disposable project: a compliant module gave `full verdict: pass`, exit 0; and a `meta import Lean` with `run_cmd` gave exit 1 with RG1010 lines and no build. Nothing of a project was written, and no tree was left in the temporary directory. Regula's own checkout gave `full verdict: pass` on the 15 modules of its default targets, as a step of the gate.

**Measured** on 2026-11-01, at the revision that stated who was owed a pass, as diagnostics with `lake exe lint standard-logical full DIR`, each on one disposable project on macOS's case-folding volume. `full verdict: pass`, exit 0: `srcDir = ""` at the package; one default target named twice; and a module `LakeFile` below a directory. Exit 1 with an RG1010 line: `..`, an absolute `srcDir` and `.lake`, and `globs = ["Data.*"]`. Exit 2: a target name that a library and an executable share, which Lake's load refuses, a target name with a hyphen, and no default target. The audit's trace: with `lakefile.toml` held open as a pipe, so that `LakeFile.lean` was created in the project after the test for `lakefile.lean` found nothing, the run gave exit 2 and `RG2001: the file system takes a file of this project for `lakefile.lean` …`, with no build. The start: `lake -d` through a link to the checkout, and `lake exe lint` from a directory reached through that link, each gave `full verdict: pass`. `srcDir = "Src"` with the directory stored as `src` gave exit 2, and the line that the path is not, by its real path, this same path below the project. These are searches for a counterexample. Not measured at that revision: a project on a case-sensitive volume, which [the observation on Ubuntu](#ubuntu) ran later.

**Measured** on 2026-11-01 at the change that stopped testing who started the checker, as diagnostics, each on a disposable copy of the checker and a disposable project, on macOS. `full verdict: pass`, exit 0: the audit's case of a checker whose `.lake` is a link to a sibling directory; its package and the project each reached through a link; and a checker and a project each with `:` in its path. With shims for `which`, `git`, `env`, `libtool`, `ar`, `cc`, `tar` and `sh` under a project's `.lake/build/bin`, none ran and the verdict was the same when the checker was started through that project's `lake env`, from a shell of that environment in the checker's package, and with that directory first on the operator's `PATH`. The same `which` shim first on `PATH` ran three times in `lake check` before the environment was closed. Proof verdict: `lake lint` passes in a project with `require regula` and with `LAKE_OVERRIDE_LEAN=1`, and `lake -d OTHER lint` from another workspace gives `incomplete`, exit 2.

**Measured** on 2026-11-01 at the change that moved the project out of the arguments, as diagnostics on disposable projects, on macOS. The runs above name the project in the form this change removed, `lake exe lint PROFILE full DIR`. A project holding `axiom unusedAxiom : 1 = 2` and a `partial def`, which passed `lake build --wfail`, with `lintDriver = "regula/lint"`: with `lintDriverArgs` of a profile, `full` and a clean project's path, and of a profile, `full` and `.` or `/`, of a profile and `full`, of nothing, of four words and of `.`, `lake lint` gave `incomplete` with exit 2, and the same with `testDriver` and `lake test`; with one profile it gave RG1001, RG1003, RG1005 and RG1006 with exit 1. `lake -d P lint` from a clean project gave exit 2 with those arguments and with one profile. `REGULA_FULL=DIR lake exe lint standard-logical` gave `full verdict: pass`, ending with `DIR`, with exit 0, from this checkout and from a disposable copy whose `.lake` is a link. The old form from this checkout gave exit 2. In a clean project with `require regula`, `lake lint` gave `proof verdict: pass`, ending with that project's real path, with exit 0. With `REGULA_FULL` naming another project it gave that project's full verdict, ending with its directory; naming itself, exit 3 and nothing built.

**Measured** on 2026-11-01 at the change that published [the closed list](#the-closed-list-of-refusals), as diagnostics with `REGULA_FULL=DIR lake exe lint standard-logical`, each on one disposable project on macOS's case-folding volume. Exit 1 with an RG1010 line that names the case, and no build: the `lake new` application template, once its `lean-toolchain` says `leanprover/lean4:v4.35.0` (it writes `leanprover/lean4:4.35.0`, which is refused first), a default `lean_exe`, and a default target that names nothing (`the default target … is not a library`); `lean_lib.srcDir` in `[[lean_lib]]` and in an inline `lean_lib = [{…}]`, and two libraries with `srcDir` spelled `.` and `./` (`the key lean_lib.srcDir is outside the closed set`); and `srcDir` set to `a b`, `é` and `a-b` (`the source directory … is not a path below the project …`). `full verdict: pass`, ending with `DIR`, exit 0: a standard library with a submodule, a default library beside a non-default library and a non-default executable, `srcDir = "./lib/"`, and a module `LakeFile` below a directory. The owner's other examples kept their verdicts: `lakefile.lean`, a plugin key and a `meta import Lean` with `run_cmd` each gave exit 1, a `require` gave exit 3, and a root's file that is a link and a `TMPDIR` inside the project each gave exit 2. Regula's own checkout gave `full verdict: pass` on the 15 modules of its default targets, as a step of the gate. Plain `lake lint` on a default `lean_exe`, in a project that requires the checker by path, gave `proof verdict: pass`, ending with that project's real path, exit 0. **Measured** the same day: with a `TMPDIR` that does not exist, `IO.FS.createTempDir` itself ends the process with signal 11, in a program of four lines that calls nothing else, so the checker ends with 139 and no last line: exit 0 cannot result, and the operator sees it. That is Lean's, and such a `TMPDIR` is [outside the contract](#the-closed-list-of-refusals).

**Measured** on 2026-11-01 at the change that stated what a pass says of Lake's selection, as diagnostics on disposable projects on macOS, each requiring one checker by an absolute path, with `REGULA_FULL` unset. `Q` holds one theorem, and `lake lint` in it gave `proof verdict: pass`, ending with `Q`, exit 0. `P` holds an unused axiom and a `partial def` and sets either `leanLibDir` to `Q`'s library directory or `buildDir` and `srcDir` to `Q`'s. From `Q`, `lake -d P lint` gave that same pass about `Q`, exit 0, for each setting, with an absolute `-d`, a relative `-d` and `--dir=`: this is the case that is outside the contract. With the second setting, `lake -d P env` from `Q` printed the bytes of `lake env` in `Q`, for every variable. `lake lint` from `P` did not pass. An ordinary `P` that sets neither gave `proof verdict: incomplete`, exit 2. `lake -f` from `Q`, naming either a second file in `Q` whose library holds an axiom or `P`'s `lakefile.toml`, gave the same pass about `Q`, exit 0. A project whose `.lake` is a link gave its pass from its directory, exit 0. With a FIFO that nothing writes at `lean-toolchain`, at `lakefile.toml` or at a module's file, `REGULA_FULL=DIR lake exe lint standard-logical` printed nothing until an 8-second timeout ended it, so the 124 was the timeout's, and those runs show no end of their own only up to that time; the read's blocking is what says the rest.

**Measured** on 2026-11-01 on Lean 4.35.0, as a diagnostic, with Lean's own `parseCommand` over an environment of `import Lean`: the kinds of `namedKinds` are what it gives for `run_cmd`, `#eval`, `#guard`, `run_tac`, `by_elab`, `native_decide`, `macro`, `syntax`, `notation`, `elab`, `initialize` and `@[local macro k]`, and `decide +native` gives a `posConfigItem` with the identifier `native` at index 1. The trees of `libraryCode` and the header of `readingOf` are the same diagnostic's output for their text with the source positions left out.

**Measured** on 2026-11-01, once, as a search for a counterexample to H6 that stops at the first: in the environment of this package, none of the 121,860 safe constants mentions an unsafe or a partial one in its type or value. It says nothing of another build. The same day, Lean's import at the level `.exported`, module by module, gave these definitions with visible bodies beyond instances and what Lean generates for a type: `Regula.ExecutableContract.run`, `Regula.Effect.Resp`, `Regula.Load.parts`, `Regula.Load.inputName`, `Regula.Reader.Attempt` and `Regula.Reader.ParserCache`. [Module files](#module-files) lists those, with `Regula.Shell.fullVariable`, which a later change added.

**Measured** on 2026-11-03 on macOS 27.2 with the checker of the release `v0.12.0`, whose start Lake composes as at this revision, as diagnostics on disposable projects that each required that checker by path, with `DYLD_PRINT_LIBRARIES` and `DYLD_PRINT_SEARCHING` set. The planted file was an unmodified copy of the toolchain's `lib/libc/libc++.dylib` at the project's `.lake/build/lib/libc++.1.dylib`, which needs `@rpath/libc++abi.1.dylib`, a library that the project did not hold. `lake lint` started the checker, the loader looked for that leaf name in the toolchain's two library directories and then in the project's, mapped the project's file into the checker, and aborted with exit 134 when its dependency did not bind. With the file removed, the same `lake lint` gave `proof verdict: pass`, exit 0. `lake build --wfail` loaded nothing of the project into `lake` or `lean`. The full gate, `REGULA_FULL=DIR lake exe lint standard-logical` from that release's checkout with the same file in `DIR`, gave `full verdict: pass`, exit 0: its checker loaded no image of the project, and its Lake commands printed no line of the loader, because `env -i` had removed the variables. These runs show where the loader looks. That a library built to resolve its dependencies runs its initializers and prints a pass is argued from dyld(1), and no such library was built.

**What an earlier measurement did not observe.** At the change that stopped testing who started the checker, this document said that on macOS a planted `libc++` did not load into the checker, marked measured. That measurement read an empty marker, which a library's initializer would have written, as "not loaded", and it recorded no run in which the marker was known to fire. A library whose dependencies fail to bind aborts the process before any initializer runs, as the copy above aborted the checker before `main`, so an empty marker does not show that the library was not loaded. What it observed is that no marker was written.

**Not measured**: real Mathlib, whose imports the check does not load, and the check's own time and peak memory. What was measured on Linux is in [Ubuntu](#ubuntu).

### What remains

**Not closed, by design**, each [outside the contract](#outside-the-contract) or outside [the named configurations](#the-named-configurations):

- Another process that changes the checker's tree.
- A start from a project's Lake, with project code that ran first.
- A `lake -d` or a `lake -f`, on which a pass is about the current directory and not what the option named: [Lake gives a program nothing to tell them by](#the-language-check).
- A call that does not return.
- A `REGULA_FULL` left set in the environment of a `lake lint`, which is the request of whoever started the run and an accepted risk: the run gives the full gate on the directory it names, and its last line says so. Testing who started a run is what would close it, and `lake lint` and `lake exe` start a program through one environment with nothing to tell them apart (`Lake/CLI/Actions.lean:20-21`, `:98`, `Lake/CLI/Main.lean:1283`).
- A counterfeit `lake` or `lean` at the toolchain that `LEAN_SYSROOT` names.
- A process that changes the project after the read cannot reach the verdict, which is about the text read.
- Anything about a dependency's code, since a project with a dependency has only the proof verdict.
- The entries of the list of assumptions.
- A fake toolchain or a `PATH` shim: the check runs inside what it is given, and `supportsLean` reads only what that program says of itself.
- A checker that the operator did not build apart from the project.

**Accepted risk:**

- A project with a default executable, a `srcDir` on a target, or a source directory outside the closed names gets no full verdict until it is rearranged, which the owner confirmed, and its proof verdict stays.
- A project that needs a file outside its Lean sources and Lake configuration during the build fails its full verdict, visibly, and one full verdict costs one fresh build.
- A project with a harmless dependency gets only the proof verdict, and a harmless name outside the closed domain is `incomplete`.
- A harmless link that a project's source is read through gets no full verdict, and neither does a library with a recursive glob over its own directory: each is visible, and the cost is to name the modules.
- A link in a file that no root and no import reaches is not read, so nothing selects it and it does not change the verdict.
- The plain `lake lint` keeps Lake's own load and listing, because it gives only the proof verdict and Lake has already loaded the project there.
- An `instance` that changes what a statement means.

**Known failures that the check reaches:**

- [#462](https://github.com/rbeauchamp/regula/issues/462): `macro_rules` and `@[local macro]` are refused, and `match.ignoreUnusedAlts` is not in `options`. Closed for a full verdict.
- [#468](https://github.com/rbeauchamp/regula/issues/468): its macro cannot exist. No other form was found, and none was proved absent.
- [#469](https://github.com/rbeauchamp/regula/issues/469): no failure of what Regula claims. **Measured** on 2026-10-31 at this revision: a project's `isEmpty` on `Substring.Raw`, then `variable (s : Substring.Raw) (h : isEmpty s = true)`, `namespace Substring`, `include h`, `def usesH`, gets a full verdict while Lean discards the deprecation warning of the second elaboration, and a declaration with the same binders directly fails `lake build --wfail`. Regula makes no claim about warnings, since `lake build --wfail` is Lean's own, so that verdict is true of what it states. Refusing `variable`, `include` and `omit` is the one way to change this, and the owner's words admit them.
- [#471](https://github.com/rbeauchamp/regula/issues/471): `try?`, `exact?`, `apply?`, `#check_failure` and `#guard_msgs` are refused. Closed for those. Other places where Lean drops a message are unread, so no statement says that no message is dropped.

### Decisions

Each of these was decided on the owner's behalf, and [the confirmation record](confirmation.md#the-language-check) gives the rest:

- One process runs the check, the build, the replay of the cone and the rules, because a record that a first command left could be forged by project code in the build that a later command read. So the order is a program's order, with a theorem.
- The table is what real code uses, not every construct that meets the criterion, because each entry is a claim that H2 rests on. Regula's core uses about 170 of its kinds, and the rest go with library code of two other projects of the owner's that is outside this repository.
- The specification package stays outside this check. It imports lean-intent, whose files use `syntax` and `macro`, and its `lakefile.toml` sets `doc.verso`, which the check refuses, so that Lean checks what its doc comments name. So it gets the proof verdict, and its proofs are still replayed, by the checker.
- The language decision reports each offending position and the shell prints at most 50, because a project far outside the set would otherwise print its whole tree.
- `Regula.Reader` and `Regula.Shell` are in the default target `RegulaChecker`, so a full verdict on Regula reads them, and every function of the checker that does not itself call Lake is in a default target too. They ask what calls Lake through the operations of `Regula.Effect`, and `Regula.Workspace` holds only those calls (`LakeCalls`). `Regula.LintMain` stays the thin `unsafe` root, because `Lean.enableInitializersExecution` requires it. `Regula.DiagnosticsGate` and `Regula.TestListing` are repository programs, not the checker.
- A library's or an executable's name must be in the closed domain, like a module's, because Lake joins an executable's name onto its output directory, and an absolute one selects a path outside the project. The root package's own name is not tested, because a default build uses it for no path. So a target named with a hyphen is `incomplete` until it is renamed, which is the cost of a closed domain.
- The configured paths and targets are a closed domain: each source directory lies below the tree with closed names, each `globs` entry is a single module, and each default target is a library, before any Lake call asks for the modules. A closed domain costs less than arguing about an open one. It refuses, as a configuration fault, and does not give `incomplete`, because the project's configuration states the path and nothing failed to read. `Reading.openPaths` holds each report, so a refusal with no reason is no state of the type.
- Every child of the gate works in a tree the checker made, and the checker reads the project by itself, on the owner's delegated agent's decision, because a list of the paths that Lake derives from a project's directory is the wrong shape, however complete it reads today, and a later Lake can add a row. The cost is one fresh build per full verdict, and a project that needs another file during its build fails. A project may keep its own `.lake`, since nothing reads it.

## Module files

Each Lean file of the root package is a `module` file. An importer that is a `module` file sees the type of a definition and the statement of a theorem, and it sees a body only where the author chose that: an `abbrev`, an instance or `@[expose]`. So what such a caller relies on is stated. **Measured** on 2026-10-31: Lean's header parser (`Lean.Parser.parseHeader`, `HeaderSyntax.isModule`) reported `module` for each of the 21 tracked Lean files below `lean/` at that date. Each added since, `Regula.ProgramCheck.EffectScan`, `Regula.Rule` and each rule's module below `lean/Regula/Rules/`, starts with `module` too, which the gate's build of it reads.

The root package's `@[expose]` are on `Regula.ExecutableContract.run`, on `Regula.Effect.Resp`, on each rule's value `Regula.Rules.RGnnnn.rule`, so that the registry reads its spelling (`Regula.Closed.spellings_nodup`, by `decide`), and on `Regula.Closed.Report.verdict` and `Report.findings`, so that the registry proves what a report holds (`Regula.Closed.report_pass_iff`). A rule's check stays unexposed. The one on `Regula.ExecutableContract.run`: the exported theorem `ExecutableContract.run_eq` is proved by `rfl` over that body, and without the attribute it does not build. **Measured** on 2026-10-31. The one on `Regula.Effect.Resp`: a caller gives a program of an operation the type of its response, which only that body shows. Its other visible bodies are the instances that `deriving` makes, the instance of `Monad` on `Prog`, and five `abbrev`: `Regula.Reader.Attempt`, so that `ExceptT`'s monad applies to it, `Regula.Reader.ParserCache`, and `Regula.Load.parts`, `Regula.Load.inputName` and `Regula.Shell.fullVariable`, which the specification's statements read.

`Regula.ProgramCheck.TestListing` proves two configurations equal by reduction, so it uses `import all` on the three modules whose unexposed bodies it reads: `Regula.TestListing`, `Lake.CLI.Main` and `Init.System.ST`. `Regula.ProgramCheck.Effects` states the bodies of `Regula.Workspace`, so it uses `import all` on that module. `Regula.TestListing` imports Lake a second time with `meta`, because `lean --run` runs it in the process that elaborates it, and only a module imported with `meta` has its runtime initializers run there (`Lean/Compiler/InitAttr.lean:160-168`). **Measured** on 2026-10-31: without `meta`, the process ended with signal 11.

In this package, only `RegulaSpecification.Input` is a `module` file. The remaining files, but for `Proofs.Gate`, cannot be one yet. A `module` file cannot import a file that is not one (`Lean/Environment.lean:2120`), and no file of lean-intent at the commit that `lakefile.toml` names is one. **Measured** on 2026-10-31 with the same parser, over its tracked files. `RegulaSpecification.RuleRecord`, `RegulaSpecification.Language` and `RegulaSpecification.Effects` each import three of lean-intent's modules, and each other file but `Proofs.Gate` imports one of the three directly or through another of them. They can follow when lean-intent has migrated. `Proofs.Gate` imports only `Regula.DiagnosticsGate` and `Regula.Shell`, so this reason does not cover it. It is not a `module` file either, and it unfolds the unexposed bodies of `Regula.DiagnosticsGate`, which a `module` file would see only through `import all`.

A file that is not a `module` file sees each body of what it imports, whatever the author chose (`Lean/Elab/Import.lean:150-156`, `Lean/Environment.lean:2183`). So the proofs read the executed definitions of the rules as they did before, with no `import all`.

No file of this repository uses `import all` on a module of another Lake package at this revision: the proofs here see the bodies of `Regula.*` because they are not `module` files, and `Regula.ProgramCheck.TestListing` uses `import all` on a module of its own package and on two of the toolchain, which belong to no package of the workspace (`Lake/Config/Workspace.lean:283-284`). When lean-intent has migrated and the proofs become `module` files, they will need it across packages. Lake's check of that is disabled with the remark "We've decided to disable this check for now" (`Lake/Build/Module.lean:430-434`), and the field that allows it is `allowImportAll` (`Lake/Config/PackageConfig.lean:314-324`), so a later toolchain can refuse those imports until the root package sets it. This concerns how this repository builds, and no verdict relies on it.

## Decisions of this specification

Each of these was decided on the owner's behalf by the owner's delegated agents, because the owner's intent asks for the smallest core that does the job. None is the owner's confirmation.

- The root package does not set Lake's `requiresModuleSystem`. Lake would then warn on each file that is not a `module` file and imports one (`Lake/Build/Module.lean:416-424`), so the proofs here and another project that imports `Regula.Contract` would need `allowNonModules`, and a file that imports nothing of the package would still not be seen. A `module` file that imports a file that is not one is already refused by Lean, and a file that stops being a `module` file is cheap to correct.
- The root package does not set `allowImportAll`, because no other package's file uses `import all` on one of its modules at this revision.
- The specification's files are not split so that the parts without a lean-intent record could become `module` files now. No importer of those parts is a `module` file, so a split would move each statement and show nothing more, and the whole package can migrate at once.
- The claim is the default targets of the root package, with each module of the root package that their imports reach. That is the set `lake build` builds, so a project cannot claim a target that its build skips, and it needs no file of its own that classifies its targets. A target that is not a default target and that no default target imports is outside the claim, as it is for `lake build`. **Measured**: such a module with a `sorry` passes, and it fails once a default module imports it.
- A project states one profile, for all of its claimed modules, and no profile is `incomplete`. A library that needs a stricter profile than another is a project of its own.
- The input is one environment, the import of the default targets' modules, and it holds each constant of that environment, so the loader has no search of its own and no loop. To check a constant that the import replaced, it reads the rules' `Tables.axiomSet`.
- A rule reads only an input of the closed form, by its type. The checker's type holds what the rules read of it, and `Draft.admit` is the one place that decides the two parts that a real build can lack: a claim of no module and a mention of a constant that the input does not hold. What the loader constructs is carried instead of checked: unique names, and that a claimed module is loaded. So the two checks of those and the field `loads` are gone, and their theorems `not_wf_duplicated` and `unloaded_refused` with them. The record of the verdict still states what the admission refuses. The rule's record reads a well-formed input by its type, so `SameReports` says nothing of the others, and each rule still has its two witnesses.
- The rules read `Tables i`, whose proof fields state what each table holds of `i`, rather than a table with no relation to the input, so `rgN_exact` holds of every value of that type.
- A rule's check gives `Violation`s, which carry no rule, and the registry gives each finding its rule's spelling (`Finding.of`), so no rule can print another rule's code. The closed type `RuleId` is gone: a rule is its value in the registry, so it cannot lack a function, and `Regula.Closed.spellings_nodup` keeps each code naming one check. RG1010 and RG2001 keep the codes they printed, as text of the language check and the shell.
- The core of the checker's rules, `Regula.Rule`, holds the tables that more than one reader uses: the known axioms, the native-proof and compiler axioms' names, and the profile's admission and the loop constructs, which the loader's check of a constant that Lean's import replaced reads too (`fitsUnshown`). A table that one rule alone reads is in that rule's module, such as RG1006's helper form. A way for a rule to declare its own reader of the build waits for the first rule that needs a field the input does not carry ([2026-11-03](confirmation.md#2026-11-03-each-rule-a-module-of-its-own)).
- The library `RegulaChecker` names the root `Regula.Rules`, so each module whose name starts with it is part of the library by Lake's own test (`LeanLibConfig.isBuildableModule`, `Lake/Config/LeanLibConfig.lean:140-142`), and a rule's module needs no line of `lakefile.toml`. **Measured** on 2026-11-03: without that root, Lake did not build a rule's module before the registry that imports it, and the registry's build failed for want of its `.olean`. This package's library has its own name as its root, which covers each module below `RegulaSpecification/`.
- The statement of what a pass means in the terms of Lean's environment, `EnvFloor` with `allHold_env`, `pass_iff` and `pass_held`, and the loader's `fitsUnshown`, stay one statement downstream of the registries: each covers RG1001, RG1005, RG1006 and RG1011, and `EnvFloor`, `allHold_env` and `pass_held` cover RG1012. `pass_held` and `fitsUnshown` cover each claimed module's own replacement-attribute entries, including a theorem that Lean's import merged ([RG1011](#rg1011-replaced-compiled-code)). RG1012 needs no change of `fitsUnshown`: a claimed module's own constant that the environment does not show is a theorem, which RG1012 does not read, and one that it shows has the kind and the value's mentions of the constant that the environment keeps (`Facts.shown`, `readOf`). `allHold_iff` states the registry rule by rule, so a rule added to the registry stops the build there until that statement covers it too.
- RG1011 takes a code that no check of Regula has had in any release, because releases before `v0.12.0` gave RG1007 to RG1009 to checks that no longer exist, and a code reused would name two checks across releases. Its findings come after RG1006's, at its place in the registries.
- RG1012 takes the next such code, and its findings come after RG1011's. It reads what a value mentions with no closure, and it treats a name that the input does not hold as a panic form when it is named with `!`, so a mention that the input cannot classify is refused ([RG1012](#rg1012-hidden-panics)).
- `Regula.Closed.Input.findings` builds the tables of the input once, before the rules run, and gives the same value to each rule, as the run did before each rule had a module of its own. No verdict or finding depends on it.
- `Safety` replaces the flags `isUnsafe` and `isPartial` of a constant, so the form of a recursion helper does not exclude a state that Lean does not make. `safetyOf` reads Lean's two flags, and the theorems state what it gives in their terms.
- `Report` replaces the triple of a verdict, its findings and an optional reason, so the printer has no default for a reason that is missing.
- A lookup with `getD _ []` stays in `Input.mentionedBy`, `Input.axiomReach`, `Facts.stated` and `Facts.input`. Each table is a map from a name to a list of what it relates, where a missing key and an empty list are one state, so the default stands for no excluded state.
- `Profile.all` lists each profile, and `Profile.ofSpelling?` reads the spellings from it, so a refusal names them from one list. `Regula.Closed` stays a namespace below the one root `Regula`: it is the pure core over the closed input, and renaming it changes no meaning.
- The rules compute each axiom set from the input, so a set cannot be missing or differ from `Input.AxiomOf`, and the trusted base loses `Lean.collectAxioms`. A set follows what every loaded module's own data states, so on a build where Lean's import replaced a constant it can hold more than `Lean.collectAxioms` gives on the merged environment. **Measured** once on 2026-10-31 by `lake lint`, against pull request 515: on the root package 5.1 s real and 4.7 s user, against 4.2 s and 11.4 s, with a largest resident set of 0.74 GiB against 0.74 GiB; on this package 5.2 s and 4.8 s, against 4.6 s and 19.2 s, with 0.75 GiB against 0.69 GiB. Each is one run on a shared machine, and this package grew by this change.
- A constant of a claimed module that Lean's import replaced is checked by the loader, not reported by a rule as a subject, because the input holds one constant of each name. Its own violation gives `incomplete`, so it never passes, and it names no rule. What a replaced constant mentions, and an axiom that a theorem replaced, count for its name, so a rule reports the claimed constant that reaches them.
- RG1006 refuses a constant with a helper's name whatever its kind, and it does not read what the constant computes, because the compiler reads it by its name alone and a rule over names can be proved. A field or a function of a project with that name is refused too. The checker calls the compiler's own test (`Lean.Compiler.isUnsafeRecName?`, so `Regula.Rules.RG1006` imports `Lean.Compiler.Old`) instead of holding a copy.
- The shell reads one Lean release, by its version and commit, and refuses any other, because RG1004 and RG1006 read forms that a release gives.
- `Regula.Contract` and `Regula.Decision` stay as a library that gives no verdict, because another project of the owner's still imports them. They go when it moves them.
- The gate has no time limit, because a wall-clock limit has no proof, and on a slow or sleeping machine it refuses a change for no fault of the change. A gate that does not end is a matter for whatever runs it.
- The gate removes each earlier build output first, with `lake clean`. **Measured** on 2026-10-31: after a library left the configuration, a module that imported it still built from the `.olean` left in Lake's build directory, and the checker read that module as claimed. After `lake clean`, the build failed.
- The gate runs the checker on the specification too, with `lake build --wfail` before it. So each theorem here depends on no axiom beyond the three. The path that step takes through `lintDriver` is also the one that a project that requires Regula takes.

## The run of the checker

The checker's whole run is a value of the type `Regula.Effect.Prog`, `Regula.Shell.run`: a tree whose every node names one operation of the closed type `Op`, with what to do for each response that operation can give. The tree performs nothing. `Prog.interpret` runs it, in `BaseIO`, through one table, `Regula.Effect.table`. An operation that can fail gives its failure as a value of its response, so `BaseIO`, whose type holds no exception, leaves the tree one way out: its leaf.

`Runs p t a` says that for the responses that the events `t` hold, `p` asks exactly the operations of `t`, in that order, and ends with `a`. A response is any value of its type, so a statement over `Runs` holds for every answer of Lean, Lake and the operating system, a failure included. It is a fact about what the run received and what it did with it, so `run_meets` and each theorem without `OneRealPath` rest on no file system staying still: another process can change any file between any two reads and back, and the statement holds of what the run read.

**Proved** of the definition that the executable runs, in [`RegulaSpecification/Proofs/`](RegulaSpecification/Proofs/), with the statement in [`Effects.lean`](RegulaSpecification/Effects.lean), [`EffectsRun.lean`](RegulaSpecification/EffectsRun.lean) and [`EffectsRecord.lean`](RegulaSpecification/EffectsRecord.lean). The original statements preceded the program; the preparation relations and `written` strengthen the record, and the reader was changed for the second so that it writes a module's file only for an admitted reading. `run_meets`, for every argument list and every response (`RunMeets`):

- **Refusal.** A Lean other than the pinned one, or an argument list other than one word, or a text that is no profile: exit 2, the last line of an incomplete proof verdict, and the run only says so (`Refusal`).
- **The proof verdict.** The exit code is that of `Regula.Closed.decision` on what the load gave, and so is the last line but for the directory that a pass names at its end, and the load gave what the proved `Facts.input` gives on the environment, the places and the modules that Lean and Lake returned, or an error for a case of `PlainReason`, each of which is what a response said about an operation that this load needs (`PlainRun`, `Loaded`, `BuildRead`). `PlainPreparation` directs the workspace load by earlier responses and each lookup or rules import after it names its root's `leanPath` as its search path. It requests no tree mutation. Exit 0 gives `EnvForm` and `EnvFloor` of what they returned (`plain_exit_zero`), and that no answer failed.
- **The check.** It admits only on a reading inside the closed language, and any other outcome rests on a `Reason`. An admitted reading rests on `Evidence`: the real path of the project and the tree, which lie apart; `lean-toolchain`; `lakefile.lean` absent by its name; each key path of `lakefile.toml`, whose text stands in the tree; the pinned text as the tree's `lean-toolchain`; for each file (`ReadText`), that it passed the exact-path test, that Lean's parser gave its header and commands from the text that `readFile` returned, in the environment of exactly the toolchain modules that `Sees` states, and that the tree holds that text at the file; and that the tree holds no text other than these. What `Evidence` calls held is `written`, a fold of the run's own writes and removals over the whole reading, so a text a later write replaced is not what the admission rests on. `ReadBack` then says that each such text is what the file system answered, for the path it was written at, in a last segment of the reading that holds no act, so each text the fold credits is also what the file system answered, and that the same segment holds its answer that nothing has the name `lakefile.lean` in the tree. That no other file is in the tree is still a statement of the fold, and rests on `createTempDir`. Any other outcome rests on a `Reason`, a closed set of what the responses said about what the requested build needs, by what the run has been told of that build (`Scene`, `Named`, `Needed`): a read of anything else justifies nothing. So a reader that refuses without one does not meet the record. On an admission, no read failed (`readProject_no_failed`).
- **Nothing is built unless the check admitted.** The events of the check hold no Lake command and no load for the rules (`only_readProject`). On any other outcome the gate asks nothing more.
- **Writes.** Each act of a full run, each `writeFile`, `createDirAll`, `removeDirAll` and the working directory of each Lake command, lies at or below the tree or is the tree, and, when any act lies below the tree, the two real paths lie apart, so a run writes nothing to the project's directory (`Confined`). When the only act is at the tree itself, that it holds nothing of the project rests on `createTempDir`. Every write asks `Regula.Reader.inTree` first.
- **Preparation at each occurrence.** `ReadingPreparation` fixes the complete acts of the reading: the TOML copy from an earlier source read, the pinned `leanToolchain` copy, the configuration load, and module copies, with each lookup and parser import naming that load's `root.toolchain` as its search path. Each `CopyStep` creates only its path's parent, when present, and writes only after that succeeds. A failed directory ends the step; a failed configuration copy ends the acts, while the grammar lets a failed module copy be followed by later module steps, which `Regula.Reader.writeSources` does not ask. A path or parent outside the tree makes no act. Every module step has `Named`, `FileOfModule` and `SourceText` from its preceding prefix; repeated names or paths need that provenance again. A lookup or an import carries its search path in its request, so no order of the run's acts decides which path it asked on. `readProject_spec`, `inputOf_spec`, `loadTree_spec` and `loadPlain_spec` prove the relations on the actual definitions' exact traces, each in the one statement of its stage, and compose into `run_meets`, so legitimate failures remain admitted. The acts of a reading lie in the tree by this grammar alone (`ReadingPreparation.readActs`).
- **Build and reload.** `BuildProtocol` permits exactly one build, using the identified Lake in the allocated tree, with only reporting around it. `BuildAndRules.no_mutation` excludes explicit writes, directory creation, allocation and removal from both the build and reload phases. `RulesPreparation` directs the reload by the received real path, and each rules import or lookup names the loaded root's `leanPath`. `build_protocol`, `rules_spec` and `loadTree_spec` prove these constraints for the actual definitions on every response; none describes filesystem effects inside trusted Lean/Lake calls.
- **Removal.** On every way out of a run that made its tree, the run asks `removeDirAll` of it (`FullRun`). `FullRun` places that removal after the reading and the gate's build and reload. `FullRun.removal_order`: no event removes a directory, or one does, with no removal before it and only reporting after it, whatever its response; `FullRun.no_remove_before_command` excludes removal before any later Lake command. If the initial allocation fails, it is the first event and only reporting follows. A failed removal changes no verdict.
- **Exit code and last line.** The exit code is a function of the verdict alone, `Regula.Language.Report.exitCode` or `Regula.Closed.Verdict.exitCode`, and so is the last line but for the directory that a pass names at its end, `Regula.Language.Report.labelOn` or `Regula.Closed.Verdict.proofLineOn`. `full_gate_lines`, `proof_verdict_lines` and `pass_lines_name_subject` state each sentence word for word. The last event requests one physical verdict line, and every physical line requested by preceding `println` calls starts with two spaces (`EndsWith`, `IsDetail`). `detailText_no_break` proves that diagnostic serialization escapes LF and CR for every string; `serialized_split` relates those physical lines to the concatenated characters, including each LF that `IO.println` appends, and `endsWith_serialized` gives their final-line distinction. These statements concern the checker's requested output: output from Lake's child processes, partial writes and external writers are not `println` events of this trace. A failed print changes nothing the run decides. Exit 0 from the full gate gives all of the above with `lake build --wfail` ending with 0, successful replay of the claim's cone during loading, and the floor of the build (`full_exit_zero`).

- **What a run is about.** For every argument list and every response, a run is a refusal, the proof verdict when `REGULA_FULL` is unset, or the full gate on the directory it names when it is set (`run_subject`), and an argument list other than one word is a refusal (`run_other`). A pass of the proof verdict names the current directory's real path, from which the workspace it read was loaded, and whose search path starts the one that the run got (`SearchPathStarts`, `plainRun_pass`). These state what the run asked and received, and none of them says which workspace Lake selected. That Lake passes on the variable is measured, and that `lakefile.toml` has no key that sets one is read from Lake's source.

**Not vacuous.** A program that does nothing and ends with other than 2 fails the record (`constant_program_fails`), and so does one that reads nothing and refuses everything (`refuser_fails`). `admits_a_project` is conditional: for paths that meet the hypotheses `WitnessPaths`, it gives responses on which the check that runs admits a project. [A pass is owed](#a-pass-is-owed) states the rest. The hypotheses are what the tests of a path give, because `System.FilePath` depends on `System.Platform.isWindows`, an `opaque` constant (`Init/System/Platform.lean:22`, `:39`) that no reduction of the kernel can evaluate; that the pinned text trimmed is itself, on which `decide +kernel` got stuck (**measured**); and that an empty log holds no error, which is read from `Lean/Message.lean:702-703`. No theorem discharges them, and no verdict relies on them: they are hypotheses of the model, not of a run. **Observed**: the gate's run on Regula's own checkout takes the same branches on real paths and ends with `full verdict: pass`.

**The link to the executable.** `interpret_runs` and `executed_meets`, for any table and from any state of the world: what `Prog.interpret` computes is the value of a run whose events are what the program asks, each with the table's answer at the world the run has reached. `BaseIO` is a state monad in Lean's own definition (`Init/System/ST.lean`), so this is a theorem about that definition, and no assumption that effects run in program order. That the compiler keeps that order stays with the compiler.

### A pass is owed

The record requires both relevance and preparation. A reason names something the requested build needs; the exact phase relations constrain every operation whose response depends on the tree that the run writes, including failed attempts, and each operation on a search path names that path. The earlier gap arose because membership in a trace established relevance while permitting inserted acts that could spoil a later operation. Ordered segments now close that gap in the record itself, independently of the owed-pass premises. The following results hold for every program meeting the record, in [`Proofs/Preparation.lean`](RegulaSpecification/Proofs/Preparation.lean) and [`Proofs/Owed.lean`](RegulaSpecification/Proofs/Owed.lean):

- **A non-pass has a defined reason.** `Reason`, `Needed`, `PlainReason`, `TreeReason` and `BuildRejected` are closed. Each case binds its event to the requested build through what the run was told: the answer to `LEAN_SYSROOT`, the real path of the project and of the tree, Lake's load of that tree, the modules of its default targets, a name the build needs (`Named`, each module of a default target and what the file of such a name imports), and that name's file. **Proved**: `manufacturer_fails` excludes the program that reads an unrelated environment variable and reports incomplete; `misjudge_fails` excludes the program that receives a successful `LEAN_SYSROOT` response and reports incomplete without loading; `unrelated_read_no_reason` states that a trace of one event, a failed real path of a path other than the project and the tree, holds no reason. Preparation comes from the same run's phase relations, so none of these relevance predicates alone is the whole contract.
- **Copies cannot manufacture their own preparation.** `ReadingPreparation.first_directory` states that when the first tree act creates a directory, that directory is the TOML destination's parent. `manufacturedCopy_fails` excludes the reported trace that reads the TOML, creates a directory at its destination, fails its write, removes the tree and reports incomplete, for every path, text, error, profile and exit code. Its proof uses the missing toolchain response. `manufacturedCopyAnswered_fails` excludes the same trace with that response present, through the copy grammar: `first_directory` says the directory is the destination's parent, and `parent_ne_self` says that no path is its own parent, on any platform. Each later step needs a named module's file and an earlier source read; a child path that obstructs another named file is therefore a conflict directed by the project's own configuration. `BuildAndRules.no_mutation` and `FullRun.after_removal_saying` exclude later explicit writes and nonterminal removal. No theorem infers filesystem contents from arbitrary response values.
- **A later write takes away the authority of an earlier reading.** `FullRun.gate_stands`: when a full run reaches a Lake command or a load for the rules, it has the form of an admitted reading and a gate, there is a reading inside the closed language with no failed answer on `Evidence` of what the reading leaves, and at each point of the gate, the reload included, what stands is that. `FullRun.at_consumer` and `FullRun.judged_at_consumer` state it at the consumer. `Evidence.judged`: each text standing was judged. `uncheckedCopy_fails`: a trace that ends by reading a file again and copying that text over a file has no `Evidence` of what it leaves, for every text other than the pinned one that neither of Lean's and Lake's parsers was given, and `uncheckedCopy_build_fails` says that no full run reaches a build after it. `moduleCopies_admits_uncheckedCopy` states that the module-copy grammar alone admits that trace, on its premises. Its neighbour `judgedCopy_stands` keeps the evidence when the copy's text is the one standing, and `rewritten_stands` gives what stands after two writes, so a program that writes one text, reads again and judges the later one rests on the later one. `Regula.Reader.twoTexts` refuses, as `incomplete`, what would hold two texts at one path, with `Reason.twoTexts`, because `Evidence` credits one text at each path.
- **What is credited is what the file system answered.** `Regula.Reader.readBack` reads each planned file back, by the path it was written at, after the reader's last write, and stops at a differing or failed answer, read from its code, which is `incomplete` (`readFiles_spec`, `Reason.treeDiffers`). `ReadBack` itself asks for a matching read and does not exclude another read that differs. `FullRun.answered_at_consumer` states it at each consumer. `act_after_readBack_fails`: a reading that ends with an act, for each act of `Op` that is not quiet, fails `ReadBack` once a written text stands. So two paths with different components that the file system takes for one file, by case folding, by Unicode normalization or by anything else, are refused when their texts differ, provided no other process changes the file between the two reads (argued, not proved, and measured for case folding only), and the read-back accepts them when they agree. A read through another string with the same components does not discharge the clause, and `written` still treats such strings as one place. The texts compare as the operations give them: `IO.FS.writeFile` puts a string's bytes and `IO.FS.readFile` gives the bytes it decodes (`Init/System/IO.lean:1058-1060`, `:1229-1233`), so a line ending is compared as it was written. `Reason.treeDiffers` requires the read to come after a successful write of that text at that path, so a run cannot cite a read it asked first.
- **What Lake takes as its configuration.** `Regula.Reader.noOtherConfig` asks the file system for the name `lakefile.lean` in the tree after the read-back, and stops with `incomplete` when anything answers (`Reason.configShadowed`), or when the question fails (`Needed.treeLeanConfig`). `FullRun.config_at_consumer`, on one answer for each real path: at each Lake command and each load for the rules, the reading's last segment holds that no such name answered and that a read through a spelling of `lakefile.toml` in the tree gave the text Lake's parser read. `act_after_readBack_fails` covers an act after it. A project whose module the tree's volume takes for that name, and for which the project's own test found nothing, is refused (**measured**), and on a volume that does not take it for that name it passes (argued). The reading is about what the build consumes at the last read: another process that changes the tree after that answer is not in this statement, and the owner's confirmation leaves it unsaid.
- **A pass is owed under the defined premises.** `PlainOwed` excludes `PlainReason` and a refused replay, and requires the floor of each loaded reading. `FullOwed` excludes allocation failure, admission reasons, build rejection, reload reasons and a refused replay, and requires `BuildAnswer.Floor` of what each loaded build answered. **Proved**: `plain_owed`, `full_owed`, and `run_plain_owed`, `run_full_owed` at the whole run give the pass verdict and exit 0 under these premises. `pass_iff_answer` states the pure part in terms of what Lean and Lake answered, with none of the checker's functions: the loader and the rules pass exactly on `BuildAnswer.Floor`. `loadFloor_iff` relates it to `LoadFloor`, the same requirement over the checker's own reading, and `pass_iff_floor` states the verdict over that. Preparation follows from `PlainRun` and `FullRun` even when these owed-pass premises do not hold. `FullOwed` is the absence of each reason, and says nothing of who else ought to pass: [the closed list](#the-closed-list-of-refusals) says what that means.
- **No premise applies a decision of the checker.** `Reason`, `SearchPathStarts`, `ExactlyBelow`, `StrictlyBelow`, `BuildAnswer.Floor` and `parts` state what Lean, Lake and the operating system answered, with Lean's own functions on paths and names. Each decision has its theorem, in both directions: `exactBelow_eq_true_iff`, `below_eq_true_iff`, `startsSearchPath_eq_true_iff`, `apart_iff`, `inTree_iff`, `closedSourceDir_iff`, `pass_iff_answer`, and at the whole run `run_meets`. This is a written rule of this specification, and no check enforces it. **Accepted risk**: a later premise that applies a decision of the program would give an owed-pass theorem a premise that a wrong refusal makes false, as one did before, and review and audits are what catch that.
- **No statement of who a run is about rests on a value that the subject sets.** A name or a sentence that says which project a run concerns rests on what the operator gave (the working directory, `REGULA_FULL`). Before a value of Lake's is read as naming something, every setting that reaches that value is listed from Lake's source, and a refusal of one example is no evidence for it. This is a written rule of this specification, and no check enforces it. **Accepted risk**: review and audits are what catch a later breach, as an audit caught `SearchPathStarts` under the name that said it identified Lake's workspace.

What these premises say of Lean, Lake and the operating system, each over what the run received, never over every value:

The table describes successful responses needed by the owed-pass premises, not theorems that external calls always succeed. Preparation of the requests is proved separately and needs no agreement between repeated responses.

| Premise | What it says | Source |
| --- | --- | --- |
| `LEAN_SYSROOT` and `LEAN_PATH` are set, and the search path starts with that of the workspace in the current directory (`PlainReason.noSysroot`, `noSearchPath`, `otherSearchPath`, `Needed.sysroot`) | Lake sets them for what it starts, with the workspace's libraries first and then its own. So a Lake and a Lean that do not come from one toolchain directory give another spelling of its own library, and `lake lint` refuses them. A workspace whose path holds the separator of a search path is refused the same way. | `Lake/Config/Env.lean:302`, `:313`, `Lake/Config/Workspace.lean:391-392`, `:422`, `startsSearchPath_eq_true_iff` |
| The real paths are the paths (`Reason.toolchainNotExact`, `tomlNotExact`, `moduleNotExact`, `notApart`) | `IO.FS.realPath` answers `realpath`, which keeps an absolute path with no `.`, `..` or empty component that crosses no link and spells each name as the volume stores it, the converse of H4 for such a spelling. | POSIX `realpath`, `Init/System/IO.lean:874-881` |
| The required reads and copies succeed, and each planned file reads back as written (`Reason.failed`, `treeDiffers`, `Needed.copyParent`, `copyToml`, `copyToolchain`, `sourceParent`, `sourceWrite`) | The requested source text is read, each correctly prepared parent creation and write succeeds, and a read of each planned file by the path it was written at gives that text. `CopyStep` constrains preparation even when a response fails; success itself is external. | `ReadingPreparation`, `writeInTree_spec`, `readProject_spec`, `Regula.Reader.readBack` |
| Lake's load gives a root, and its library's modules (`Reason.load`, `Needed.library`, `PlainReason.load`, `BuildFailed.library`) | A closed `lakefile.toml` loads, and a library of single modules lists them. | `Lake/Load/Workspace.lean:31`, `:61`, `Lake/Config/Glob.lean:53-59` |
| Lean's parser and search answer (`Needed.sourceHeader`, `parser`, `search`) | The header parse and toolchain imports succeed, and the lookup succeeds under the loaded root's toolchain path. `ReadingLoaded` establishes the path that each names, not the success of these responses. | `readRoot_spec`, `Lean/Parser/Module.lean:75`, `Lean/Elab/Import.lean:141-149`, `Lean/Util/Path.lean:117-125` |
| The build ends with 0 (`BuildRejected`) | The project compiles, which is what the command decides. | `Lake/CLI/Main.lean:962-985` |
| Lean's replay of the claim's cone answers with success (`Replayed`, `PlainOwed.replayed`, `FullOwed.replayed`) | Lean's kernel accepts each constant of the cone. | `Lean/Replay.lean:176-190` |
| The import gives the build's environment, and it has `BuildAnswer.Floor` (`BuildFailed.import`, `search`, `FullOwed.floor`, `PlainOwed.floor`) | The rules import and lookup succeed under the loaded root's `leanPath`, and the resulting environment has the floor. `InputPreparation` establishes that each request names that path. | `inputOf_spec`, `Lean/Environment.lean:1871`, `:2183` |

**Their model.** [`Proofs/OwedModel.lean`](RegulaSpecification/Proofs/OwedModel.lean). `full_model` and `plain_model`: on the answers of the witness, the program that the executable interprets receives what `FullOwed` and `PlainOwed` state, and exits with 0, so the premises are met by a run. `refused_model`: on answers where every operation succeeds and the project holds a `lakefile.lean`, it does not exit with 0, so that each operation succeeded does not settle the conclusion by itself. Both models of a pass are conditional on `WitnessPaths`, for the reason above, and on `EnvModel`, because the constructor of `Lean.Environment` is private (`Lean/Environment.lean:213`, `:553`), so no proof here can build one with a claimed module. `executed_meets` supplies the run record for the interpreted program.

**The record.** `programRecord` is the contract of the run, with `run_meets_record`, `program_o2`, `program_o2Run`, `program_o3`, `program_o4` and `program_o5` at `.widest`. The preparation relations fix the order of acts, while observations and the wording of detail lines retain freedom; no equality between different subjects' traces is required. The record is the agents' design, derived from the owner's account and decided on the owner's behalf; [the confirmation record](confirmation.md#a-pass-is-owed) gives the status of each consequence.

**Accepted boundary.** Responses need not describe a consistent filesystem. A repeated canonical path or source read may change, and nothing here proves what an opaque Lake call does internally or prevents another process changing the tree. A file that changes between two reads gives no false verdict: an admission is about the text that stands, and two texts at one path are `incomplete`, by the path's components before any module's file is written and by the file system's own answer after that. Another order of reads that changes no response used by the run is accepted risk, with a visible refusal as its possible cost. A later write is not in this boundary, because it can change what the build consumes: `written` is what decides it, and no explicit write follows the reading. A crash can leave the newly allocated directory, which no later run reads. These limits do not waive the ordered preparation of requests.

### So thin that it only calls Lean

The owner's words say "so thin that it only calls Lean". The owner's delegated agent stated the form on the owner's behalf, because a form that a reader could not check would let a decision back in: **a definition has this form when it only calls Lean or Lake, as a straight line of calls that passes each result on, with no test or branch of its own on any result.** Turning a failure into the `Except` of a response (`toBaseIO`) is no decision. A selection of what Lake returned, such as a field of `rootOf`, holds no branch, and it can still change a verdict if it picks the wrong value, so [the table below](#what-a-function-of-lean-or-lake-is-relied-on-for) names each with Lake's source. These rows hold more than one call, each with no test, because Lean's and Lake's APIs have no one function for them: `flush`, which asks for the stream and flushes it; `parseHeader`, which reads what the header imports; `importParsers`, which enables initializers, imports and reads the scoped parsers; `kernelReplay`, which makes Lean's empty environment and replays the constants into its kernel's; `spawnLake`, which starts a command and waits for it; and Lake's `lakeInstall`, `loadWorkspace`, `loadRoot` and `lakeEnvironment`, which compute Lake's environment before they load.

What is left in this form, each shown where it stands:

- `Regula.Effect.table`: **proved**: `table_rows`, over the closed type `Op`, states each row, with `spawnLake_eq` and `importParsers_eq`. Its one `match` selects the row of the operation asked, and no row reads a result.
- `Regula.Workspace`: `lakeCalls`, `lakeEnvironment`, `rootOf` and `messagesOf`. **Proved** in `Regula.ProgramCheck.Effects`, each by `rfl`, so the statement is the body. They are not in the specification's package, because a constant that calls Lake's load depends on axioms that no profile admits.
- `main` of `Regula.LintMain`: the interpretation of `Regula.Shell.run` through that table, in one line, read from the code, because a theorem cannot state an `unsafe` constant.
- `Regula.Effect.Prog.interpret`: proved above.

`Regula.ProgramCheck.Effects` finds the class through Lean's own environment, at the level where bodies are held: each constant of a module of the repository that the executable and `Regula.Contract` and `Regula.Decision` reach, whose type, or whose value as a definition, mentions an effect, directly, through another constant of the repository, or through a constant of Lean's or Lake's whose type mentions one. It fails the gate's build on any outside `Regula.Table`, `Regula.Workspace`, `Regula.LintMain` and the interpreter, and when it finds no interpreter. Its decision is the pure `scan` and `judge` of `Regula.ProgramCheck.EffectScan`, and the command only imports the environment and reports what they give. **Proved**: `mem_scan_iff`, `judge_ok_iff`, `mem_own_iff`, `allowed_iff`, which states what may mention an effect by the modules' names and apart from the table, and `check_ok_iff`, in [`Proofs/EffectScan.lean`](RegulaSpecification/Proofs/EffectScan.lean). It covers those modules and no others: the repository's two programs have their own theorems below. That `Environment.find?` and the header report what the `.olean` files hold, and that `Expr.getUsedConstants` lists what an expression mentions, stays Lean's. **Measured** on 2026-10-31: a `def` of type `IO Unit` added to `Regula.Reader` failed that build, naming it.

### The repository's programs

`Regula.DiagnosticsGate` and `Regula.TestListing` each declare their own `main` and start with `lean --run` before anything is built, so they cannot use the checker's table. Each theorem here is about the definition, at `IO` and from any state of the world, for every answer of Lake and of the operating system, because `IO` is a state monad in Lean's own definition (`Init/System/ST.lean`).

- **The gate.** `GateProgram.main_zero`: the command line gives 0 only for the one argument `local`, on a run of `runLocal` that gave 0. `runLocal_zero`: `runLocal` gives 0 only when it made its directory, wrote to it joined with each file of `checkerFiles` the bytes that its read of that file gave (`copyChecker_io`, `copyAll_io`, `copyFile_io`), read the working directory, and, with that directory as the checker and the working directory as the project, for each step of `localSteps` there are worlds in which it spawned exactly that step's request and that child's wait gave 0 (`runIn_zero`, `runSteps_io`, `runStep_ran`, `StepRan`, `stepRequest`, `localSteps_eq`). `localSteps_eq` states each step's arguments, directory and project of the full gate, in order, and `localSteps_full` that only the step running `lake exe lint standard-logical` names a project, which is the working directory. `stepRequest` binds `REGULA_FULL` (`fullVariable_eq`) to the step's project, `none` removing an inherited value according to `IO.Process.SpawnArgs.env`, which is Lean's, and `runStep_spawns` states with no premise about how the call ends that `runStep` starts that request. So a `runStep` that gives a code without starting its `lake` command fails a build. Which program `PATH` selects, and what Lake's exit code means, stay trusted, and these theorems do not state them. A path joined to a directory can leave it when it is absolute or holds `..`, and `copyFile_io` says nothing of that: `join_relative` states the join for a relative path, and `checkerFiles_io` states which paths the gate passes. That a step then builds what was written and checks this checkout rests on what `localSteps` names, the file system and Lake, which these theorems do not state. `checkerFiles_io` and `regularFiles_io` state which files it copies: the three of the configuration, and each path that `walkDir` lists below `lean` that is no directory. That no other process changes the checkout between its steps stays assumed, as its module says.
- **The listing.** `outcome` is its one decision, a pure function of what the load gave: `outcome_zero_iff`, `outcome_of_zero` and `outcome_of_nonzero`, with `listing_ok_iff`. `Regula.ProgramCheck.TestListing.main_runs`: `main` asks the load, the lines of `outcome` on standard output, then its errors on standard error, and gives its code. `main_zero`: exit 0 means that the load gave a test driver, that the lines it asked to print are what `listing` gives for that driver, and that for each line there are states of the world in which `IO.println` of it succeeds. `readDriver_eq` states its load by its body, a straight line of Lake's calls, with `loadConfig_eq`. What Lake reports as the test driver is Lake's.

**Accepted risk**: a defect in them that only stops the gate visibly, such as a failed copy or a failed print, which `IO` turns into a nonzero exit, and a directory left by a crash.

### What a function of Lean or Lake is relied on for

The theorems above read only the responses, so they need no fact about Lean, Lake or the operating system; what a response means is in [the list of assumptions](#the-trusted-base). Some entries are also stated formally, each as a structure or a definition of this package and never as an axiom, and each is an argument of every theorem that uses it (`Assumption.formal`). The list gives each one's pinned sources.

| Entry | Formal statement | Theorem |
| --- | --- | --- |
| `h1`, `h2` | `LeanBehaviour` | `admitted_runs_no_project_code` |
| `h3` | `LakeBehaviour` | `read_what_lake_compiles` |
| `h4` | `RealPathBehaviour`, `OneRealPath` | `read_no_link`; `lake_takes_judged` and `FullRun.config_at_consumer` need one answer for a real path. `realPathBehaviour_crossing` constructs a model with both a crossing and an unchanged path for any two paths with different components. |
| `h5` | `LakeSelection` | `lake_takes_judged`, `lakeSelection_model` |
| `h6` | `SafeMentionsSafe` | `safe_reach_safe`, `helperForm_unreached`; `base_safeMentionsSafe` and `safeMentionsSafe_refutable` show it met and able to fail |
| `usedConstants` | `UsedConstantsComplete` | `pass_occurs` |
| `leanImport` | `ModuleDataComplete` | `claimedConstants_complete`, as the field `claimed` of `Meaning` states it |

H4 constrains only the responses that a run received, not arbitrary paths or a later state of the file system, and a name on the way that a volume stores in another case gets other components too (**measured** with `/bin/realpath` on macOS), which the exact-path test reads as it reads a link. H6 states why a constant of the exempted form cannot change what the proof verdict claims. The checker's replay of the cone is what checks the build in the kernel, so `debug.skipKernelTC` in a build gives `Regula.Shell.run` no pass of a constant that the kernel refuses.

**What the checker takes of Lake's load**, which the entry `lakeLoad` holds, and of Lean's import, which `leanImport` holds. Each is a straight line with no branch (`table_rows`, `rootOf_eq`, the theorems of `Regula.ProgramCheck.Effects`), so a wrong one would be no test that failed: it would pick another value.

| Selection | What it is relied on for |
| --- | --- |
| `Root.sourceDirs`: `ws.root.srcDir`, each library's `srcDir`, each executable's `root.lib.srcDir` | Each directory below which Lake names a module's file. If one were missing, a directory outside the tree would not be refused by `openPathsOf`, and each file would still pass `treeRelative` before it is read or written. |
| `Root.libraries`: each library's name, and `config.globs` | That a library lists a directory only for an entry other than `.one`. |
| `Root.defaultTargets`: `ws.root.defaultTargets` | The claim. |
| `Root.findLib`, `Root.findExe`: `findLeanLib?`, `findLeanExe?`, with `exe.root.name` and `exe.root.leanFile` | Which target is a library and which an executable, as Lake's build asks. The language check refuses a default target that `findLib` does not find, and only the proof verdict claims an executable's root. |
| `Root.targets`: each library's and executable's name | The names that Lake joins onto output directories. |
| `Root.resolve`: `ws.findModule?`, with `leanFile` | The file of an import, as H3 states. |
| `Root.leanPath`: `ws.augmentedLeanPath` | The search path of the proof verdict's load: the workspace's libraries, then Lake's. |
| `Root.toolchain`: `lean.leanLibDir`, `lake.libDir` | The search path while reading, so what Lean's search finds there is a module of the toolchain. With `collocated := true` they are one directory. |
| `Root.leanLib`, `Root.rootLib`: `lean.leanLibDir`, `ws.root.leanLibDir` | What the places of the modules decide: `inToolchain`, and which modules are claimed. |
| `lakeInstall`: `LeanInstall.get sysroot (collocated := true)`, `LakeInstall.ofLean`, `.lake`, `.libDir` | The Lake beside this Lean, which the gate runs. |
| `lakeEnvironment`: `initLeanPath := []`, `initLeanSrcPath := []` | That no inherited search path reaches Lake's load. |
| `loadWorkspace`: `wsDir`, with Lake's default `relConfigFile`. `loadRoot`: `wsDir`, `relConfigFile := "lakefile.toml"` | The workspace loaded, and that `loadRoot` reads the TOML file and does not prefer `lakefile.lean`. |
| `libModules`: `m.name`, `m.leanFile` | The modules of a library, as H3 states. |
| `importForRules`: `loadExts := false`, `level := .private` | That no initializer of a loaded module runs and each body is held. |
| `importForParser`: `loadExts := true`, `level := .exported`; `parseCommand` with `options := {}` | H1's context. |
| `kernelReplay`: `Lean.mkEmptyEnvironment`, `toKernelEnv`, `Kernel.Environment.replay` | That the kernel checks the cone of the claim into an environment that holds nothing else (`replay`). |
| `scopedParsersOf`: `parserExtension.ext.getState env`, the keys of `scopedEntries.map`, which `importParsers_eq` states over Lean's own state | The namespaces that hold a scoped parser, which `canActivate` reads. |
| `parseHeader`: `header.raw`, `HeaderSyntax.imports` | What a file imports, with the implicit `Init`. |
| `spawnLake`: `cwd`, `stdin := .null`, through `/usr/bin/env -i` with `PATH` and `LAKE_ARTIFACT_CACHE` | That a child works in the tree, with no inherited variable and nothing restored without being compiled (`processes`, `lakeCommands`). |

Of the other operations: `createTempDir`, `removeDirAll`, the reads and the writes are the entry `files`; a `TMPDIR` that names nothing breaks `createTempDir`'s answer with a value (**measured** above), which is outside the contract. `IO.Process.spawn`, the environment and the standard output are `processes`. `Lean.findOLean` and `Lean.importModules` read `Lean.searchPathRef` and take no path, so the row of each lookup and import sets it to the path that the request names and then calls them (`leanImport`), and each operation of a run is a whole row before the next begins (`compiler`).

**Machine limits.** A file too large to read, a path too long and an import that fails are errors of the response, so each is a failed read. The reader's bounds, `1000000` names in the walk (`tooMany`) and one call of the parser more than a file's bytes, end in `incomplete` or a refusal, never an admission. A program that overflows its stack or dies ends with a code of its own, and exit 0 cannot result, because the exit code is what the program's value gives and the last event prints the last line.

**Accepted risk.** A tree left by a crash, which affects nothing later; a failed print of the last line, since the exit code still says the verdict; and output of a child Lake command on the same stream, which is Lake's and is no line of the run.

## The trusted base

What a verdict relies on and no proof here discharges is one list: the closed type `Assumption` in [`RegulaSpecification/Assumptions.lean`](RegulaSpecification/Assumptions.lean). Each constructor is one behaviour of Lean, Lake or the operating system, stated in its docstring, with who holds it (`owner`), its pinned sources (`sources`: lines of a file of Lean's repository at the tag `v4.35.0`, the source directory there of a component that the owner's account trusts whole, or a page of the platform's own manual), the platforms on which it was observed (`platforms`), and the release at which its sources were read (`readAt`). What a proof here covers over every answer is not listed. Lean holds `kernel`, `h6`, `replay`, `compiler`, `h1`, `h2`, `usedConstants`, `leanImport`, `leanVersion` and `platform`; Lake holds `lakeLoad`, `h3`, `h5`, `lakeCommands` and `lakeStart`; and the operating system holds `h4`, `files` and `processes`. **Proved**: `each_relied_on`, that an operation, a route or a premise relies on each entry; `sources_ne_nil`; and `os_on_platform`, that each entry of the operating system names a platform. The owner's account keeps Lean, its kernel and Lake trusted, and allows a short list of behaviours of the operating system, each tied to the platforms on which it was observed.

### Complete by construction

The build of this package fails for a reliance of each of these kinds until it is on the list:

- **An operation.** `Assumption.ofOp` gives each operation of `Regula.Effect.Op` its entries, by a `match` over the closed type (`ofOp_ne_nil`), so a new operation fails the build there. **Measured** on 2026-11-02 in a disposable copy: with an operation added to `Op`, to its response, to its row of the table and to the other definitions over `Op`, the build failed at `Assumption.ofOp` with `Missing cases`.
- **A route.** `Route` names the published ways to start the checker, and `Route.relies` gives each its entries. `run_route` proves that every run of `Regula.Shell.run`, for every argument list and every response, is a refusal or a run of a `Route`, so a mode added to the program fails that proof.
- **A premise.** `Meaning`, in [`RegulaSpecification/Meaning.lean`](RegulaSpecification/Meaning.lean), states once each theorem that says what a verdict means: `Effects.run_meets`, `executed_meets`, `run_route`, `plainRun_pass`, `plain_exit_zero`, `full_exit_zero`, `replayConstants_env`, `claimed_theorem_replayed`, `pass_iff`, `pass_floor`, `pass_held`, `pass_occurs`, `claimedConstants_complete`, `FullRun.gate_stands`, `FullRun.answered_at_consumer`, `lake_takes_judged`, `read_what_lake_compiles`, `read_no_link`, `admitted_runs_no_project_code` and `helperForm_unreached`. Each of their premises about Lean, Lake or the operating system is the formal statement of an entry ([the table above](#what-a-function-of-lean-or-lake-is-relied-on-for)), and `meaning` proves `Meaning` from those theorems. So a premise added to one of them, or to a lemma that one of them uses, is either proved there or changes that theorem's statement, which then differs from `Meaning`, and the build fails.

A change of the pinned toolchain fails the build as well. `readAt_pinned` proves each entry's `readAt` equal to `Regula.Closed.pinnedLean`, the one release that the checker reads, and a command at the end of the same file fails the build under any other Lean. So each entry's sources are read again at the new release, and its record changed, before the build passes. **Measured** on 2026-11-02 in a disposable copy: with both `lean-toolchain` files naming `v4.35.0-rc2`, every other module built, and `RegulaSpecification.Assumptions` failed with a message that names both releases.

The statement of `Meaning` is the one definition of what a verdict means, and changing it changes the contract itself, which review judges like any change of the contract. No check classifies the premises written into that definition, because whether a proposition is about Lean, Lake or the operating system depends on what it means and not on its form: an equation over the environment that Lean returned reads like an equation over the run's own data. The owner's delegated agent decided this on the owner's behalf on 2026-11-02, as accepted risk. Three more things are not reached, each visible in one file and cheap to undo: a wildcard in `ofOp` would give a new operation the wildcard's entries; a definition that a field of `Meaning` uses, such as `FullRun`, means what its own text says; and the wording of an entry, and the names of entries that this document gives, are checked by reading.

### The named configurations

The claim holds only for these. Anything else is outside the contract and not a defect.

- **The pinned toolchain.** Lean `v4.35.0`, at the commit `eb6cafb7290e8bd5f2937522d8d804f58f02bafc`, which `lean-toolchain` names and `Regula.Closed.pinnedLean` states. The checker is built by it, and `lake` and `lean` are that toolchain's programs, as `PATH` selects them. The checker refuses any other Lean (`supportsLean`).
- **The published ways to run** (`Route`). For the proof verdict, `lake lint` from the project's own directory, with no option of Lake's and `REGULA_FULL` unset. For the full verdict, `REGULA_FULL=DIR lake exe lint PROFILE` from the directory of a checkout of Regula built apart from the project, with no option of Lake's.
- **The size of a claim.** The replay of the proof verdict holds in memory each constant of the cone of the claim, and checks each in Lean's kernel. **Measured** on a project that imports Mathlib, in [what a pass means](#what-a-pass-means). A claim whose cone is far larger may exceed the memory or the time of a machine, which is a limit of this configuration and no defect: no replay of a claim can need less than its cone.
- **The platforms.** macOS 27.2 on Apple silicon (arm64), on which the entries of the operating system and `platform` were observed: the measurements of this document, and on 2026-11-02 `/bin/realpath` through a link and through a name in another case, `/usr/bin/env -i`, and `mktemp -d`, and the same day the Lean program of [the observation on Ubuntu](#ubuntu), which gave on this platform each answer that those entries state. And Ubuntu 24.04.5 LTS on x86-64, on which the same entries were observed by the same procedure, as [Ubuntu](#ubuntu) records.

So Windows, another release of macOS, another distribution, release or architecture of Linux, another Lean, a start of the full gate from a project's Lake, `lake -d`, `lake -f` and every other option of Lake's, a start through `lake test` or `lake env`, and `lake lint` with `REGULA_FULL` set are outside the contract.

### Ubuntu

Ubuntu 24.04.5 LTS on x86-64 is a named platform: on it each entry of the operating system and `platform` holds, `processes` and `platform` in the forms that their docstrings give for Ubuntu. **Measured** once on 2026-11-02, as a GitHub Actions job that a push to a scratch branch started, on GitHub's runner image `ubuntu-24.04`, version 20261025.353.1 by the runner's report and 20261026.354.1 by its variable `ImageVersion`: Ubuntu 24.04.5 LTS on x86-64, with the kernel 7.0.0-1017-azure, glibc 2.39, `/home` and `/tmp` on one ext4 volume, `/tmp` a directory and no link, and `TMPDIR` unset. Lean `v4.35.0` at `eb6cafb7` came from elan, and the checker was built with `lake build lint` from the commit of `v0.12.0` with only the scratch workflow's files added. The scratch branch and its run were deleted afterwards. Each entry was observed by the procedure of its observation on macOS: the commands named above, a Lean program that calls each function the entry names, a start of the checker with planted libraries, and the full gate on disposable projects. On Ubuntu the pages of the manual that the entries cite, but coreutils' `env(1)` and macOS's `dyld(1)`, are those of man-pages 6.7: `ld.so(8)` is in its package `manpages`, which the image installs, and the pages of sections 2 and 3, such as `realpath(3)` and `mkdtemp(3)`, are in `manpages-dev`, which it does not.

- **`h4` holds.** `IO.FS.realPath` gave a link, and a path through it, the components of its target; a plain absolute path its own components; a path asked twice one answer; and `/tmp` itself. A name in another case than the volume stores failed with `no such file or directory`, because ext4 stores names as given, and H4 constrains only a successful answer. GNU's `/bin/realpath` through the link gave its target, and for the name in another case it printed the path unchanged with exit 0, as coreutils does for a missing last component, while `/bin/realpath -e` failed. The full gate gave `incomplete`, exit 2, for `srcDir = "Src"` with the directory stored as `src`, as on macOS, and for an import of `Demo.Sub` whose file is `Demo/sub.lean`.
- **`files` holds.** `mktemp -d` and `IO.FS.createTempDir` each gave a new, empty directory of mode 700 below `/tmp`, as `mkdtemp(3)` states. `IO.FS.readFile` refused bytes that are not UTF-8, `symlinkMetadata` reported a link and a dangling link as links, `createDirAll` and `writeFile` wrote at the path given, a spelling of that path with `//` and `.` read the same file, and `removeDirAll` of a directory that holds a link to another directory left that other directory's file.
- **`processes` holds, with its loader's form for Ubuntu.** `IO.getEnv`, standard output and `IO.Process.spawn` of `/usr/bin/env` answered as the entry states: in the directory given, with standard input null, and with the child's exit code. `/usr/bin/env -i` passed only the variables given. `/usr/bin:/bin` held `which`, `git` and `env`, and `lake build --wfail`, the one Lake command of this revision's gate, succeeded in that environment on each of the four admitted projects run on the image as it is. The checker needs `libc.so.6` and five more libraries of glibc and records neither `DT_RPATH` nor `DT_RUNPATH`, and `lake env` gave `LD_LIBRARY_PATH` as the toolchain's `lib/lean` and `lib` and then each package's `.lake/build/lib`, as `lakeStart` states. With a file that is no library planted under each of those names in a project's `.lake/build/lib`, `lake lint` in that project ended with exit 127 and `error while loading shared libraries: …/.lake/build/lib/libc.so.6: file too short`, and so did the checker started by hand with that directory on `LD_LIBRARY_PATH`: the loader took the file from that directory first, as `ld.so(8)` states. On the proof verdict's route that is the first route of [a project aimed at the checker](#a-project-aimed-at-the-checker), which is outside that verdict's contract. In the full gate on the same planted project the checker loaded and ran, because the checker's own package composes that variable there and the project's directory is not on it.
- **`platform` holds, in its form for Ubuntu.** Lean gave `isWindows = false`, `isOSX = false` and `isLinux = true`, so the functions of `System.FilePath` read a path as POSIX does, and Lake names `LD_LIBRARY_PATH` as the loader's variable (`Lake/Util/NativeLib.lean:35-41`).

**`lake check`, which this revision does not run.** The checker of `v0.12.0` replayed the build with `lake check` and no flag, which on Linux builds and exports inside `bwrap` (`Lake/CLI/Check.lean:167-201`, `:602-622`). On the image as given, `lake check` refused with exit 2 for want of `bwrap`, which the image does not install, so that release's full verdict on each of the four admitted projects run was `fail`, exit 1. With bubblewrap 0.9.0-1ubuntu0.3 installed it still failed, with `bwrap: setting up uid map: Permission denied`, because the image sets `kernel.apparmor_restrict_unprivileged_userns` to 1. With that setting at 0 the full gate gave `full verdict: pass`, exit 0, on the module of the README's full gate, on that project below `/tmp`, on it with the planted libraries and with shims for `which`, `git`, `env`, `bwrap`, `sh`, `cc`, `ar`, `tar` and `libtool` under its `.lake/build/bin`, none of which ran, and on Regula's own package, with 15 claimed modules and 1,333 of their constants. After both changes to the system, `lake check` with no flag could not reach Regula as a dependency by path, because the sandbox covers `/home`. This revision's gate runs `lake build --wfail` and replays the claim in the checker's own process, so it needs neither `bwrap` nor a change to the system. Its checker was not run on Ubuntu: each operation that it asks is one that the checker of `v0.12.0` asked there, but for Lean's replay in its kernel, which asks nothing of the system.

The rest gave what macOS gives. `run_cmd`, `lakefile.lean` and a plugin key gave exit 1 with RG1010 and no build, a `require` gave exit 3, and a root's file that is a link, a file that is not UTF-8 and a `TMPDIR` inside the project gave exit 2. Each project's files were the same after the run, by path, mode, size and modification time, and no tree was left. On the module with `sorry` of that release's README, its three commands, with `lake check --inadvisably-no-sandbox`, gave its four findings and `proof verdict: fail`, and on a clean module a pass.

### Outside the contract

- Another process that changes the project, the checker's tree or a build during a run, or between the operator's commands. Each statement here is about what a run read and what the file system answered.
- A call that does not return, and a `TMPDIR` that names nothing, as [the closed list](#the-closed-list-of-refusals) states.
- For a proof verdict, what the code of a claimed module or of a dependency does while it is built. It runs, no rule reads it, and it can add a constant of the form that RG1006 exempts, remove messages so that `lake build --wfail` sees no warning, and have other effects, among them those of code aimed at the checker or the toolchain, which the next item puts outside the contract. **Measured** on 2026-10-31: a `run_cmd` wrote a file during the build, and the module passed `lake build --wfail`, `lake check` and `lake lint`. That code runs outside any sandbox, as it does in `lake build`. A full verdict needs no such trust, and the full gate runs nothing of a dependency.
- For a proof verdict, a project that places a file or code aimed at the checker or the toolchain. Its two commands can print a pass whatever its build holds, an unsound proof included, by the routes that [a project aimed at the checker](#a-project-aimed-at-the-checker) lists, and the full verdict, which closes each, is the verdict for a project that may be aimed at them.
- What a theorem means to a reader, and anything about a dependency's code.

### What the list does not hold

Regula's own code is proved, or has the form "so thin that it only calls Lean" that [the run of the checker](#so-thin-that-it-only-calls-lean) states, which the owner's delegated agent decided on the owner's behalf. `Regula.Effect.table`, `Regula.Workspace` and `Regula.LintMain` hold the calls of Lean and Lake, and what those calls do is in the list. `Regula.Workspace` is outside the default targets, because a constant that calls Lake's load depends on axioms that no profile admits, so it is outside any full verdict, and `Regula.ProgramCheck.Effects` states its rows.

### Evidence for three entries

- **`usedConstants`.** **Measured** once on 2026-10-31, as a search for a counterexample with a limit of one hour that stops at the first, with a walk of an expression written for the search: `Expr.getUsedConstants` and that walk gave the same set on each of the 150,695 values of the environment of `Regula.Workspace`, `Regula.LintMain`, `Regula.Contract` and `Regula.Decision`, the 207,461 of `Regula.ProgramCheck.TestListing`, and the 63,955 of `Regula.DiagnosticsGate`. It found none, and it says nothing about another build.
- **`replay`**, its half that the kernel needs no constant beyond the cone and `Input.kernelNames`. **Measured** once on 2026-11-02, as a search for a counterexample with a limit of 50 minutes that stops at the first, decided before it ran: in the environment of `import Lean` (207,958 constants of 2,374 modules), the cone of the constants of every sixth module, 396 modules, each by itself, with `Regula.Load.usesOf` and `Input.kernelNames`, replayed into an empty environment by the calls that the checker's table makes. Lean's kernel accepted each, 2,029,069 constants in all, in 1,033 s. It found none, and it says nothing about another environment. The project that imports Mathlib, Regula's own checkout and this package, each replayed by the checker on its own claim, are the other observations.
- **`leanImport`.** `mem_stated` proves that `Facts.stated` lists exactly the pairs of `constNames` and `constants` of each module's data, and nothing here proves what the `.olean` holds. **Measured** once on 2026-10-31, as a search for a counterexample with a limit of one hour that stops at the first: the axiom set of `Tables.axiomSet` equals that of `Lean.collectAxioms` on each constant of Regula's modules in three runs, of this package's environment (1,216 constants), the root package's (484) and a disposable project that violates each rule (19). It found none, and it says nothing about another build. That search ran before the input read what the import drops, and the two sets can differ on a build where the import replaced a constant. **Measured** on 2026-10-31: a `module` file with `sorry`, a project axiom, `native_decide`, `partial` and `while` in unexposed bodies gave the same 16 findings as before Regula's own files became modules, so an unexposed definition is read as a definition and walked; a file like it with none of those passed.

The rules read only the constants of the build, with the two attributes by which Lean replaces a constant's compiled code (RG1011), and the kernel replay only its constants. So under a proof verdict, the code of a claimed module can make a claim about a compiled program false, and it can hide a warning. Under the list, and in a project that places no file or code aimed at the checker or the toolchain, it cannot make an unsound proof of a claimed module pass the two commands, because the checker gives Lean's kernel each constant of the claim's cone, into an empty environment, and refuses each axiom that the cone reaches beyond the profile's. Code aimed at them can, by the routes that [a project aimed at the checker](#a-project-aimed-at-the-checker) lists, such as writing a library that the loader takes into the checker, and only the full verdict closes them. Before this revision that rested on `lake check`, which did not replay a claimed constant whose name Lean marks as internal when nothing mentioned it (**measured**, in [what a pass means](#what-a-pass-means)).

This shrinks what must be trusted about Regula's own code to the rows of the table, `Regula.Workspace` and the one line of `main`. What it does not shrink is the list: Lean's and Lake's functions themselves, H1 to H6, the compiler's order of effects, and the operating system. Under a proof verdict, as before, the code of a claimed module runs during its build.