# The owner's confirmations

This file records each decision of the owner's about Regula, the confirmations of its specification among them, in the owner's words.

## 2026-11-04: the rule on hidden panics

On 2026-11-03, when the owner asked for the next, single most important rule, the owner's delegated agent named the rule on replaced compiled code ([the record below](#2026-11-03-the-rule-on-replaced-compiled-code)) and, as the runner-up, a rule against hidden panics. Lean's total functions can still reach a panic, through `xs[i]!`, `Option.get!`, `List.head!`, `String.toNat!` or `unreachable!`, and a panic gives the type's default value, in Lean's logic and in the running program, so a proved function can go on with a value that nothing proved. Coding agents reach for these forms often. The owner's direction of the same day ([the record below](#2026-11-03-regulas-direction-and-the-readme)) invites new proved checks on the foundation of `v0.13.0`, and the owner's delegated agent decided on the owner's behalf to take this rule next, as [issue 552](https://github.com/rbeauchamp/regula/issues/552). The owner was asked nothing about this rule and has not picked it, so this entry quotes no answer of the owner's.

Issue 552 first framed the rule as refusing a claimed constant whose value depends on Lean's panic primitive, `panicCore`. Measurement on the pinned toolchain showed that this cannot serve the aim: 46,999 constants of Init and Std reach `panicCore` through what each mentions, among them `Std.HashMap.insert` and `List.mergeSort` through the proof terms of `omega`, and 117 of Regula's own claimed constants reach it through the values of Lean's functions that Regula must call, so the rule would refuse nearly all Lean code and Regula itself; and `xs[i]!` on an array never reaches `panicCore`, because its panic is in C code behind `@[extern]`. So on 2026-11-04 the owner's delegated agent narrowed the rule on the owner's behalf: it refuses each 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 `!`, Lean's naming for an operation that panics when it fails, to which each listed form elaborates. Theorems are not checked, because a proof is never run. The owner has not confirmed this narrowing.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| A rule against hidden panics is the next rule, RG1012. | [RG1012](README.md#rg1012-hidden-panics) | Decided by the owner's delegated agent, under the owner's direction of 2026-11-03 that invites new proved checks. |
| It refuses each definition or opaque constant of a claimed module whose value directly mentions a panic form, one of `panicCore`, `panic`, `panicWithPos` and `panicWithPosWithDecl` or a constant that is no theorem and whose name's last string component, with its macro scopes erased, contains `!`, and nothing else. | [RG1012](README.md#rg1012-hidden-panics), `RegulaSpecification/Rules/RG1012.lean` | Decided by the owner's delegated agent on 2026-11-04, from the measurements above. |
| `rg1012_exact` proves its check exact in both directions, and it is a check module and a specification module with one line in each registry that extends the statement of what a pass means in the terms of Lean's environment (`EnvFloor`, `allHold_iff`, `pass_held`). | [Adding a rule](../CONTRIBUTING.md#adding-a-rule) | Follows from the owner's decision of 2026-10-31 that a rule stays only if it is proved, and, for the layout, from [the record below](#2026-11-03-each-rule-a-module-of-its-own). |
| A panic inside the code of a dependency or of the toolchain, reached through a constant whose name has no `!`, and one in C code behind `@[extern]` of such a constant, stay outside the rule, and the published text says so. | [RG1012](README.md#rg1012-hidden-panics), [`README.md`](../README.md#what-a-pass-means) | Decided by the owner's delegated agent, as the limit of the narrowing. |
| The README marks RG1012 as on `main` and in no release, and keeps `v0.13.0`'s eight checks as what ships today. | [`README.md`](../README.md) | Follows from the owner's direction of 2026-11-03 that public text keeps what ships today apart from what is planned. |

## 2026-11-03: the local gate

On 2026-11-03, after a design study for [issue 549](https://github.com/rbeauchamp/regula/issues/549), which asked for the local gate to re-check only what a one-rule change touches, the owner was asked whether to keep the gate as it is: every run re-checks every rule's proofs, and the gate starts clean and does not rely on Lake's input hash, because reusing build outputs would save only about 14 s of the gate's 146 s on a change to one rule. The owner answered "Keep it, close 549".

In substance: the local gate stays a clean build that runs every check and re-checks every rule's proofs on each run, and issue 549 is closed as not planned. This replaces the part of [the record below](#2026-11-03-each-rule-a-module-of-its-own) that left a fast gate for a one-rule change to issue 549.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| The gate keeps its clean step and runs every check from a clean build, without reusing build outputs through Lake's input hash. | `localSteps` in [`lean/Regula/DiagnosticsGate.lean`](../lean/Regula/DiagnosticsGate.lean) | Follows. |
| Issue 549 is closed as not planned. | [Issue 549](https://github.com/rbeauchamp/regula/issues/549) | Follows. |
| The sentences of `CONTRIBUTING.md` and the specification that gave issue 549 the work of a fast gate now say that the gate stays as it is. | [Adding a rule](../CONTRIBUTING.md#adding-a-rule), [The shape of a rule](README.md#the-shape-of-a-rule) | Decided by the owner's delegated agent, as the correction of text that the decision made false. |

## 2026-11-03: the rule on replaced compiled code

On 2026-11-03 the owner asked what the next, single most important rule for Regula is, across Lean 4 as a theorem prover and as a functional programming language. The owner's delegated agent answered that a pass of either verdict says that the proofs of the claimed modules are sound, while nothing says that the compiled program runs the definitions those proofs are about: a claimed module can give a definition `@[implemented_by]` or `@[extern]`, so that its proofs reason about one definition while the program runs other code that nothing proves, and a module with each of them was measured passing on 2026-10-31. For Lean 4 used to write programs, that is where a proved function and the code that runs can differ with no signal. The owner took that answer forward by having Regula restructured first, as [the record below](#2026-11-03-each-rule-a-module-of-its-own) states, so that this rule is the first one added in the new way ([issue 548](https://github.com/rbeauchamp/regula/issues/548)). The owner's words reached this record only through the delegated agent's account, so this entry states the decision in that account's substance and quotes none.

In substance: a rule refuses each constant of a claimed module that has `@[implemented_by]` or `@[extern]`, so that a proof about a claimed definition is about the code that runs for it, as far as those two attributes go. It is proved exact in both directions, as RG1001 to RG1006 are, stated in the README and the specification, and added as a check module and a specification module with one line in each registry.

The owner's delegated agent decided on the owner's behalf, the same day, that the rule reads these two attributes and no other, and that it admits `@[csimp]`, because its theorem proves the replacement equal to the original, a reason that the rule's specification states with the limits of that theorem. It also decided that the same change binds the input's tables once before the rules run, which review of the change of the record below had left for the next change to the rules' list. The owner has seen neither decision.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| A rule refuses each constant of a claimed module that has `@[implemented_by]` or `@[extern]`, and `rg1011_exact` proves its check exact in both directions. | [RG1011](README.md#rg1011-replaced-compiled-code), `RegulaSpecification/Rules/RG1011.lean` | Follows. |
| It is a check module and a specification module with one line in each registry, and it extends the statement of what a pass means in the terms of Lean's environment (`EnvFloor`, `allHold_iff`), as [the record below](#2026-11-03-each-rule-a-module-of-its-own) requires of a rule that changes what a pass means. | [Adding a rule](../CONTRIBUTING.md#adding-a-rule) | Follows for the modules and the registries. Extending the shared statement follows from the decision of the record below, which was decided. |
| It reads these two attributes and no other, and admits `@[csimp]`. | [RG1011](README.md#rg1011-replaced-compiled-code) | Decided by the owner's delegated agent. |
| `Regula.Closed.Input.findings` builds the input's tables once, before the rules run. | [Decisions of this specification](README.md#decisions-of-this-specification) | Decided by the owner's delegated agent. |
| Its code is RG1011, which no check has had in any release, because releases before `v0.12.0` gave RG1007 to RG1009 to checks that no longer exist. | [Decisions of this specification](README.md#decisions-of-this-specification), [Adding a rule](../CONTRIBUTING.md#adding-a-rule) | Decided by the owner's delegated agent while building the change. |
| A constant of a claimed module that Lean's import replaced is checked against that module's own replacement-attribute entries as well as the merged environment. | [RG1011](README.md#rg1011-replaced-compiled-code) | Follows from the refusal of each attributed claimed constant. This corrects the earlier delegated decision to read only the kept constant: proof erasure does not exempt a theorem from that requirement. |
| The README marks RG1011 as on `main` and in no release, and keeps `v0.13.0`'s eight checks as what ships today. | [`README.md`](../README.md) | Follows from the owner's direction of 2026-11-03 that public text keeps what ships today apart from what is planned. |

## 2026-11-03: the aim of a module for each rule

On 2026-11-03, after deciding to keep the local gate as it is ([the record above](#2026-11-03-the-local-gate)), the owner clarified what the owner had asked for in [the record below](#2026-11-03-each-rule-a-module-of-its-own): "to be clear, my intent was not necessarily to make the CI or build faster, but rather to ensure that our architecture is modular such that adding or updating a rule does not break other rules. we and other contributors should be able to easily and safely add new rules and fix existing ones (if needed)."

In substance: the aim of giving each rule a module of its own is that adding or updating a rule cannot break another rule, so that the owner and other contributors can add new rules and fix existing ones easily and safely. Faster verification was not the aim. So keeping the gate a clean build that re-checks every rule leaves the aim met: the layout keeps rules apart, and the gate's speed was never what it was for. The record below keeps its account of what the owner asked then.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| The purpose of the layout of a rule as a pair of modules, with one line in each registry, is that a rule is added or fixed without breaking another, not a faster build or gate. | [Adding a rule](../CONTRIBUTING.md#adding-a-rule) | Follows. |
| Keeping the gate as it is leaves that purpose met. | [The local gate](#2026-11-03-the-local-gate) | Follows. |

## 2026-11-03: each rule a module of its own

On 2026-11-03 the owner asked whether Regula is built so that adding a rule is self-contained and can never break another rule, so that the owner and contributors can add rules easily and safely, and so that verification need not re-run every check and proof for every rule, only those of the new or changed one. The owner's delegated agent read the code and reported that each rule was already a pure, total function of the closed input, the report the union of their findings, and the type of the rules closed and matched exhaustively, so that a rule could not change another rule's findings; but that adding a rule edited files that every rule shared (`RuleId.lean`, `Rules.lean`, `Tables.lean`, and `Input.lean` and the reader when the rule needed new data, with specification files that grouped several rules), so two additions collided, and a change to one rule rebuilt and re-proved nearly all of Regula. The owner then decided to restructure Regula before adding the next rule. The owner's words reached this record only through the delegated agent's account, so this entry states the decision in that account's substance and quotes none.

In substance: each rule is a module of its own, holding its check, its statement and its proofs, importing a shared core and no other rule, with the data that it alone reads defined by the rule itself; one small registry lists the rules, with a theorem proved once that a run passes exactly when no registered rule reports a subject; so adding a rule is new modules and a registry line, and Lake's own change tracking re-checks only what the change touches, the registry and what links them. The local gate stays the gate and still runs every check, never a hand-picked subset (a decision of the owner's of 2026-10-28). No verdict, exit code or printed finding changes for any input. The next rule, which refuses `@[implemented_by]` and `@[extern]` on constants of claimed modules (issue 548), follows as the first rule added this way, in a change of its own.

The same day, after reading the code, the owner's delegated agent decided four points on the owner's behalf, which the owner has not seen. The checker's package cannot depend on lean-intent, since a `require` there would cost Regula the full verdict on its own core, while each rule's formal statement is a lean-intent record; so a rule is a pair of modules, its check in the checker's package and its statement and proofs in the specification's, with one line in each package's registry and the two registries proved equal. The statement of what a pass means in the terms of Lean's environment stays one shared statement downstream of the registries, which a rule that changes what a pass means extends together with the published text. A way for a rule to declare its own reader of the build waits for the first rule that needs one. The gate stays a clean full build in this change, because its clean step guards against outputs of removed modules and dropping it needs a design of its own, which [issue 549](https://github.com/rbeauchamp/regula/issues/549) holds.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| Each rule's check is a module of its own below `lean/Regula/Rules/` that imports the checker's core, `Regula.Rule`, and no other rule, with each table that it alone reads. | [The shape of a rule](README.md#the-shape-of-a-rule) | Follows. |
| Each rule's statement, intent record, cases and proofs are a module of its own below `RegulaSpecification/Rules/` that imports the specification's core, `RegulaSpecification.Rule`, its own check, and no other rule. | [The shape of a rule](README.md#the-shape-of-a-rule) | Follows that the statement and proofs are the rule's own. That they are a second module, in the specification's package, is decided, for the reason above. |
| One registry in each package lists the rules, `Regula.Closed.registry` and `registry`, and `registry_rules` proves them one list; `Regula.Closed.report_pass_iff` is the theorem proved once. | [`lean/Regula/Rules.lean`](../lean/Regula/Rules.lean), [`RegulaSpecification/Rules.lean`](RegulaSpecification/Rules.lean) | Follows for the registry and its theorem. Two registries proved equal are decided. |
| Adding a rule is two new modules and one line in each registry, and `lakefile.toml` needs no line for it. | [Adding a rule](../CONTRIBUTING.md#adding-a-rule) | Follows, as amended by the decision above. That the library names the root `Regula.Rules` so that Lake builds each rule's module is decided. |
| A rule that changes what a pass means in the terms of Lean's environment also extends `EnvFloor`, `allHold_iff` and the published text, and `allHold_iff` stops the build until it does. | [Decisions of this specification](README.md#decisions-of-this-specification) | Decided. |
| A rule that needs a field of the build that the closed input does not carry extends the core input and the loader, until a rule needs its own reader. | [Decisions of this specification](README.md#decisions-of-this-specification) | Decided. |
| The gate keeps its clean full build, and a fast gate for a one-rule change, with a replacement for its clean step's guard, is issue 549. | [Issue 549](https://github.com/rbeauchamp/regula/issues/549) | Decided. |
| No verdict, exit code or printed finding changes. | Each rule's check, moved with its body unchanged, and the order of the registry | Follows. |
| The closed type `RuleId` is gone, and a finding prints the spelling that the registry gives it from its rule. | [Decisions of this specification](README.md#decisions-of-this-specification) | Decided. |

## 2026-11-03: Regula's direction and the README

On 2026-11-03, while asking for `README.md` to be rewritten so it is clear and concise rather than a dense wall of prose, the owner stated Regula's basic intent and target audience: Regula is meant to capture a strict Lean 4 engineering standard and enforce it as a linter across both Lean 4 as a theorem prover and Lean 4 as a functional programming language, giving coding agents feedback and fix guidance across soundness, totality, design, refactoring and architecture so generated code is formally verified and meets both functional and non-functional requirements, for software engineers using Lean 4 with coding agents (both potential users evaluating Regula and potential contributors). Because [the decisions of 2026-10-31](#2026-10-31) had cut Regula down to eight proved checks and [the constraint of 2026-11-01](#2026-11-01) ("Removal comes first", "One use case") read to an outside reader as if the rule set were permanently frozen, the owner's delegated agent restated that vision in plain words and asked the owner to choose between two directions: Option A, keeping the 2026-10-31 bar that no unproved rule ships while stating in `README.md` that `v0.13.0` is the proved foundation and inviting contributors to help build out a Lean 4 engineering standard, actionable fix guidance in diagnostics, and new proved functional-programming, theorem-proving and design rules on top of it; or Option B, keeping the linter permanently scoped to proof soundness, axiom profiles, totality (RG1006) and build-time isolation (RG1010). The owner answered "option A".

In substance: Regula's purpose covers both Lean 4 as a theorem prover and Lean 4 as a functional programming language, aiming over time to capture a strict Lean 4 engineering standard and enforce it as a linter that gives coding agents and the software engineers supervising them exact diagnostics and fix guidance across soundness, totality, design, refactoring and architecture so generated code meets both functional and non-functional requirements. The [2026-10-31 proof bar](#2026-10-31) and [2026-11-01 simplicity constraint](#2026-11-01) remain in full force as the admission bar for every check, fix and feature: `v0.13.0` (RG1001 to RG1006, RG1010 and RG2001) is the proved foundation, not a frozen rule set, and each new standard item, fix or check ships only once specified and proved to that bar. `README.md` speaks in general software-engineering and Lean 4 terms to engineers evaluating Regula for agent-written Lean 4 and to potential contributors, stays concise and scannable so a reader can quickly tell whether Regula fits their work, separates what `v0.13.0` ships today from what is planned, and keeps every published claim, limit, hypothesis, refusal, verdict and exit code at its full strength.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| Regula's purpose spans Lean 4 as a theorem prover and as a functional programming language, with `v0.13.0` as the proved foundation for a broader Lean 4 standard, actionable fix guidance in diagnostics, and new proved checks across soundness, totality, design, refactoring and architecture, gated by the 2026-10-31 proof bar and 2026-11-01 simplicity constraint. | [Regula](../README.md#regula), [Purpose and constraint](../README.md#purpose-and-constraint), [Work on Regula](../README.md#work-on-regula) | Follows. |
| `README.md` distinguishes what `v0.13.0` ships today (the eight proved checks, with neither fix suggestions nor a standalone design or architecture standard yet) from what is planned on that foundation. | [Regula](../README.md#regula), [Purpose and constraint](../README.md#purpose-and-constraint) | Follows, from the owner's ask for honesty and authenticity together with [Text](../CONTRIBUTING.md#text). |
| `README.md` addresses software engineers using Lean 4 with coding agents, both users and potential contributors, in concise, scannable prose using general software-engineering and Lean 4 terms rather than background from other language ecosystems, while keeping every published claim exact. | [`README.md`](../README.md), [Text](../CONTRIBUTING.md#text) | Follows, extending [the README's reader](#the-readmes-reader) of 2026-11-01. |
| Moving `Use it` directly below the opening, grouping `The checks` by area, turning the prose blocks of `Before you adopt it`, `What a pass means` and `The full gate` into labeled bullets, keeping every heading name and fenced code block unchanged, and stating the owner's direction without superlatives under [the replacement of 2026-11-02](#2026-11-01) are layout and wording choices of the rewrite. | [`README.md`](../README.md) | Decided by the owner's delegated agent. |

## 2026-11-03: a project aimed at the checker

On 2026-11-03 an investigation by the owner's delegated agent observed that under `lake lint` on macOS the dynamic loader maps into the checker a library that a project placed in its own `.lake/build/lib`, through the library path that Lake sets. So the `processes` entry was false where it said that the loader loads no library a project placed below its own directory, and the published meaning of a proof-verdict pass could not hold for a project aimed at the checker. The owner was asked whether Regula's proof verdict, and the owner's 2026-11-02 sentence as far as it covers the proof verdict, should state that it assumes the project is not attacking the checker. The owner answered "yes".

In substance: the proof verdict assumes that the project is not attacking the checker, and so does [the record of 2026-11-02](#2026-11-02) as far as it covers the proof verdict.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| A pass of the proof verdict means what the specification says only for a project that places no file or code aimed at the checker or the toolchain, and a project that may be aimed at it needs the full verdict. | [What a pass means](README.md#what-a-pass-means), [a project aimed at the checker](README.md#a-project-aimed-at-the-checker), `Route.relies` | Follows, that the proof verdict states the assumption. Its wording, the four routes it names and the full verdict as the remedy were decided by the owner's delegated agent in pull request 543. |
| The record of 2026-11-02, as far as it covers `lake lint`, holds for a project that is not aimed at the checker. | [2026-11-02](#2026-11-02) | Follows. That record keeps the words the owner confirmed and states the assumption beside them. |
| The `processes` entry states the loader's search order as its manual gives it, and `lakeStart` the library path that Lake sets. | `processes`, `lakeStart` | Decided by the owner's delegated agent in pull request 543. |
| This record is added by the change after pull request 543, which carried out the answer. | This file | Decided by the owner's delegated agent. |

## 2026-11-02: the release v0.12.0

On 2026-10-31 the owner ruled that Regula has no release until the language check stands. An independent audit of main at `f7d3bf2b`, the seventh of Regula, then found that Regula meets the owner's account within its narrowed, named contract and its 17 named assumptions, with no blocker. The contract is the one that [the specification](README.md) states at that commit, narrowed by [what no false refusal means](#what-no-false-refusal-means) and by [the entry of 2026-11-02 on `lake -d`](#2026-11-02). The configurations are [the named configurations](README.md#the-named-configurations), and the assumptions are the entries of `Assumption`, which [the trusted base](README.md#the-trusted-base) lists. The owner was shown that verdict and asked whether Regula meets the owner's intent and whether v0.12.0 should be published. The owner answered "Yes, both".

In substance: the owner judges that Regula at `f7d3bf2b` meets the owner's intent, and Regula is released as v0.12.0. The judgment rests on that audit, so it holds only as far as the audit does: for the named configurations and under the list of assumptions. It says nothing of another toolchain, another way to run or another platform, and it is no statement that Regula is free of bugs.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| Regula is released, and its release notes say that the claim holds only for the named configurations and under the list of assumptions, and what is outside the contract. | The tag `v0.12.0` and its release notes | Follows, the second part from the owner's practice of [2026-11-02](#2026-11-02-the-list-of-assumptions) that anything outside the named configurations is said to be outside the contract. |
| The version is `0.12.0`, because a breaking change before 1.0 is a minor release. | [Changes, the gate and delivery](../CONTRIBUTING.md#changes-the-gate-and-delivery) | Decided by the owner's delegated agent. The question that the owner answered named that version. |
| The tag is on the commit that adds this entry to `main`, whose only change from `f7d3bf2b` is the text that names the release: in the README, the two install instructions and the line that says which release has this form; `SECURITY.md`; the `version` of `lakefile.toml`; and this entry. No code or proof changes, and no statement of what a verdict means or of how Regula behaves. | The diff from `f7d3bf2b` to the tag | Decided by the owner's delegated agent, so that what is released is what the audit read. |
| The README tells a project to require `v0.12.0`, and the full gate to start from a clone of that tag, in place of `main`. | [Use it](../README.md#use-it), [the full gate](../README.md#the-full-gate) | Decided by the owner's delegated agent: a project that requires `main` gets whatever lands after the audit. |
| The release notes are the text of the GitHub release, and the repository keeps no changelog. | The GitHub release `v0.12.0` | Decided by the owner's delegated agent. |

## 2026-11-02: where Regula's memory lives

Regula is open source, and an agent that works for another contributor has none of the owner's private notes, instructions or skills, nor the records of the owner's delegated agent. On 2026-11-02 the owner raised this, set where Regula's memory lives, and then made the criterion exact. In substance: Regula's repository holds its cross-contributor memory, everything that any mind working on Regula must remember, whoever it works for. That is every decision of the owner's about Regula's purpose, contract, constraints and method, every working rule that binds a change to Regula, and every lesson a contributor needs so as not to repeat a past defect, each stated once, in Regula's own words, pointing rather than repeating. What only the owner's own agents need, such as how they schedule their work, stays private, and a private copy of anything else is only a copy, because two copies of one account drift apart, as comments drift from code. Four decisions of the owner's were recorded only privately until then: [the size of the full verdict](#the-size-of-the-full-verdict) and [the README's reader](#the-readmes-reader) of 2026-11-01, and the two of [the list of assumptions](#2026-11-02-the-list-of-assumptions), whose entry below this revision completes. Two more of 2026-11-02 were recorded only in descriptions of pull requests: [comments](#2026-11-02-comments) and [the copyright notice](#2026-11-02-the-copyright-notice).

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| Every rule that binds a change to Regula, and each lesson of a past defect, stated as a rule, is in one file that `AGENTS.md` points to. | [`CONTRIBUTING.md`](../CONTRIBUTING.md) | Follows. That the file is `CONTRIBUTING.md`, beside a short `AGENTS.md`, is decided: a contributor's agent reads `AGENTS.md`, and a person finds `CONTRIBUTING.md` on the forge. |
| Each decision of the owner's about Regula is in this file, in its form, with its effect stated where it governs work. | This file | Follows. That this file, which held the confirmations of the specification, holds the owner's other decisions too is decided: one record of the owner's words. |
| Regula's purpose is stated once, and the specification and `AGENTS.md` point to it. | [Purpose and constraint](../README.md#purpose-and-constraint) | Follows, with the README chosen by the owner's standing rule that a project's purpose goes in its README. |
| A rule that concerns only how the owner's agents work for the owner, such as their scheduling, the owner's machine or their delivery tooling, is not recorded here. | Nowhere in the repository | Follows for scheduling. The rest is decided: none of those rules binds a change to Regula. |

## 2026-11-02: comments

On 2026-11-02 the owner set how code is documented when agents read and write it. In substance: code documents itself through the names of its constructs and how they are composed, so that a new agent or session can understand what it means and so that comments and names cannot drift apart. A comment is a claim that nothing checks: agents read every one, and when a declaration it mentions is renamed or removed, the comment goes stale with no signal. So a comment stays only when it says what the code cannot. Pull request 535 pruned Regula's comments to that.

The owner then answered "Yes, try it" to a trial of Lean's Verso doc comments, whose code roles Lean checks while it builds. The trial found that RG1010 refuses Lean's option `doc.verso` for every project, the checker's own package included, because a code block in a Verso doc comment runs during the build and the check does not read inside doc comments, so admitting the option would change the language check. Shown this, the owner answered "Yes, specification only": the specification package uses Verso doc comments, whose names Lean checks, and the checker's package keeps Markdown. The specification package gets only the proof verdict, so nothing of the checker, its language check or a published claim changes.

| Consequence | Where | Status |
| --- | --- | --- |
| A comment stays only when it says what the code cannot: the reason for a decision and the alternative rejected, a fact about Lean, Lake or the operating system that the code relies on, cited by version and source location, a hypothesis, assumption or limit the code depends on, or a short module header saying what the module is for and what it trusts. | [Text](../CONTRIBUTING.md#text) | Follows, from the owner's amendment of the account of pull request 535, which states the list. |
| A doc comment that `linter.missingDocs` requires stays, cut to the shortest true sentence, and the linter stays on in both packages. | The same | Decided by the owner's delegated agent in pull request 535: turning the linter off would remove a check, which is the owner's call. |
| The specification package writes its doc comments in Verso, under `doc.verso`, with the role that Lean checks for each mention that Lean can resolve where the comment stands. | The same | Follows. Leaving a mention that Lean cannot resolve there as literal text is decided by the owner's delegated agent, as accepted risk: a stale one is cheap to correct. |
| The root package keeps Markdown doc comments, and RG1010 and its table `options` stay as they are. | The same | Follows. |

## 2026-11-02: the copyright notice

On 2026-11-02 the owner judged the copyright header at the top of each of Regula's 66 Lean files redundant, because `LICENSE` already carries the copyright notice and the MIT licence, and asked for the headers to be removed, which pull request 537 did. Two files written the same day were created with the old header copied from another file, which is how the rule gets lost.

| Consequence | Where | Status |
| --- | --- | --- |
| A Lean file carries no copyright or licence header, and `LICENSE` stays the repository's one copyright and licence notice, to which `lakefile.toml` and the README only point. | [Text](../CONTRIBUTING.md#text) | Follows. |
| The whole header goes, its licence pointer and authors line included. | Pull request 537 | Decided by the owner's delegated agent: both lines are as redundant as the copyright line. |

## 2026-11-02: the list of assumptions

The owner adopted three practices of seL4 for all work on Regula. In substance: every behaviour of Lake, Lean or the operating system that a verdict relies on is on one short, exhaustive list of named assumptions with its pinned source, or is outside the contract, and the build fails when a new reliance has neither; the claim holds only for named configurations, which are the pinned toolchain, the one published way to run and the platforms on which the assumptions were observed, and anything else is outside the contract, said so, and not a defect; and an independent audit runs only once the claim has stopped moving, starting by checking that the list is complete and that each assumption holds on the named configurations. An audit had found behaviours of the operating system, such as `realpath` and `/usr/bin/env`, listed under the labels of Lean, of Lake or of a decision. Asked whether the list may name behaviours of the operating system, as seL4 names hardware, the owner answered "Yes, a short list": a few such entries, each tied to the platforms on which it was observed, with Lean, its kernel and Lake trusted as before. This revision carries out the first two practices. The third binds later work, which [`CONTRIBUTING.md`](../CONTRIBUTING.md#the-trusted-base) states.

**Follows** means that the owner's words settle it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, and it is no confirmation of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| One list of assumptions, each entry named once with its owner, its pinned sources and the release at which they were read, in place of the labelled prose list and the scattered marks. | [The trusted base](README.md#the-trusted-base), `Assumption` | Follows. |
| A new operation of the checker, a new mode of the program and a new premise about Lean, Lake or the operating system of a theorem that states what a verdict means each fail the build until the list holds it. | `Assumption.ofOp`, `Route`, `run_route`, `Meaning`, `meaning` | Follows. That the theorems which state what a verdict means are those that `Meaning` restates, and that the program's modes stand for the published routes, are decided. |
| A change of the pinned toolchain fails the build until each entry is read again. | `readAt_pinned` and the check at the end of `Assumptions.lean` | Follows. |
| The named configurations: Lean `v4.35.0`; `lake lint` from the project's own directory with no option of Lake's for the proof verdict, and `REGULA_FULL=DIR lake exe lint PROFILE` from a checkout of Regula built apart from the project for the full verdict; macOS 27.2 on Apple silicon, and from a later revision Ubuntu 24.04.5 LTS on x86-64. | [The named configurations](README.md#the-named-configurations) | The toolchain and the proof verdict's way follow. The full verdict's way is decided: the owner's words name one way to run, and the owner's account keeps the full verdict, whose published start this is. The platform is decided from where the entries were observed, so Linux, on which nothing was measured then, was outside the contract. A later observation found each entry to hold on Ubuntu 24.04.5 LTS on x86-64, `processes` and `platform` in forms for that system, and that platform is named from that revision, as [Ubuntu](README.md#ubuntu) records, which the owner's delegated agent decided by the same rule. |
| No verdict, rule, refusal or proved statement changes, and no proof is replaced by an assumption; a reliance already proved over every answer stays proved and is not listed. | The diff of this revision | Decided by the owner's delegated agent, because a shorter list bought by giving up a proof would trade assurance the owner already has. |
| The entries of the operating system are `h4`, `files` and `processes`, and `platform` is Lean's, tied to the platform too. | `Assumption.owner`, `Assumption.platforms` | Decided: each behaviour of the system that a response's meaning needs is in one of them. |
| An independent audit runs only once the claim has stopped moving, and starts by checking that the list is complete and that each entry holds on the named configurations. | [The trusted base](../CONTRIBUTING.md#the-trusted-base) in `CONTRIBUTING.md` | Follows. |

## 2026-11-02

An audit of `eac81908` observed a false pass. With the working directory in a project `Q` that holds one theorem, `lake -d P lint` of a project `P` that holds a project axiom and a `partial def`, and that sets its `leanLibDir` to `Q`'s, exited 0 with a pass about `Q`. The owner's delegated agent found from Lake's source, and measured, that Lake gives a program it starts nothing that names the project chosen with `lake -d` or `lake -f` and that a project cannot set. When `P` sets `buildDir` and `srcDir` to `Q`'s, the two runs have one working directory, one argument list and, byte for byte, one environment, so no check of those three can tell them apart.

Shown this, the owner answered "Yes, as recommended" to narrowing the published contract. In substance: Regula audits the workspace in the current directory and names that directory on its last line. The one published way to run the proof verdict is `lake lint` from the project's own directory with no option of Lake's, and on that run no configuration a project can set makes an unmodified Regula report a pass about any project other than the one in that directory. `lake -d`, `lake -f` and every other option of Lake's are outside the contract, and the published text says that a run with one can exit 0 with a pass about the current directory and not about the project that the option named. The owner accepted that risk.

| Consequence | Theorem or source | Status |
| --- | --- | --- |
| A pass of the proof verdict ends its last line with the current directory's real path, and the workspace it read was loaded from that path. | `plainRun_pass` | Confirmed by the owner. |
| On `lake lint` from the project's directory with no option of Lake's, that workspace is the one Lake selected. | [Lake's source](README.md#the-language-check) | Follows from Lake's source, and no theorem proves it. It is what makes the run the owner confirmed about the project in that directory. |
| `lake -d`, `lake -f` and every other option of Lake's are outside the contract, and a run with one can exit 0 with a pass about the current directory. | [What a pass says of Lake's selection](README.md#the-language-check), and measured | Confirmed by the owner, with its risk. |
| The test that the search path the run got starts with that of the workspace in the current directory stays, under names that claim only that. | `SearchPathStarts`, `startsSearchPath_eq_true_iff`, `PlainReason.otherSearchPath` | Decided by the owner's delegated agent on the owner's behalf, as part of the option the owner accepted: without it an ordinary `lake -d P lint` from a healthy workspace `Q`, with no setting of `P`'s, prints a pass about `Q`. An audit found that its old names and text said that it identified the workspace Lake selected. |

On 2026-11-03 [the owner's answer of that day](#2026-11-03-a-project-aimed-at-the-checker) gave this record the assumption of the proof verdict: as far as it covers `lake lint`, it holds for a project that is not aimed at the checker. A project aimed at the checker can make `lake lint` print a pass whatever its build holds, by the routes that [a project aimed at the checker](README.md#a-project-aimed-at-the-checker) lists. The words above that the owner confirmed are unchanged.

## 2026-11-01

The owner added a constraint over all Regula work and confirmed the restatement that follows, which the owner's delegated agent wrote. The agent decided on the owner's behalf that the README state the restatement's superlative as an aim, because the restatement allows no superlative in public until the proofs back it, and that the constraint stays a written rule with no enforcement in code, because a violation is caught at review and is easy to undo. Neither decision is the owner's confirmation. On 2026-11-02 the owner's delegated agent replaced the first decision: public text no longer states the superlative, even as an aim, and states the comparison with seL4 as the aim of being a tool whose claim is exact and proved. That replacement is not the owner's confirmation either, and the restatement the owner confirmed stays quoted word for word below.

> Regula is meant to be to Lean linters what seL4 is to kernels: the most trusted one, because its claim is exact and proved. Simplicity is how that becomes achievable, as in LionsOS, where each component does only the minimum its use case needs.
>
> - Removal comes first: before adding or repairing anything, ask whether it can be deleted, or its input narrowed, so the need goes away.
> - Hard proofs are a warning: a proof far harder than the code it covers means the code should get simpler, not only better proved.
> - Simplicity never replaces proof: RG1001 to RG1006, the two verdicts and "no bugs" all stand.
> - One use case: one toolchain, one way to run it, a closed input, and a truthful refusal for anything else. Refusing something outside a narrow published contract is not a false refusal.
> - An seL4-style claim: exactly what is proved, for which inputs, under which listed assumptions, with no superlatives in public until the proofs back them.
> - The work follows it too: the simplest analysis that answers the question, with no frameworks.
>
> For example, this rules out adding 1,000 lines to keep an unusual folder layout working, adding a mode to avoid a refusal, or keeping a tool in the repository for one analysis. It still allows a long proof of something truly hard, such as the two-way axiom rules.

### What no false refusal means

Later on 2026-11-01 the owner answered "Yes, as recommended" to a restatement of what "no false refusal" means, which the owner's delegated agent wrote after an analysis the owner asked for. In substance: Regula stops trying to prove that a project matching a description is owed a pass, because that description was tied to real files only by assumptions. `Project.config` and `SourceFile.read` were chosen values, seven of the thirteen fields of `Answers` restated the conclusion for a case of `Reason`, and Lake's loader depends on axioms outside Regula's own profiles (10 for `Lake.loadTomlConfig`, 75 for `Lake.loadWorkspaceRoot`), so no correspondence with it can be proved under them. Instead Regula publishes a closed list of refusals. Each refusal is proved true of what Lean, Lake or the operating system answered, and a project passes when no refusal applies and the rules hold. So "no false refusal" means that a refusal is never untrue, not that every reasonable project passes, and "exit 0 exactly when" is withdrawn. Newly refused, each with a true message: a default executable, including the `lake new` application template; a `srcDir` on a target; and a source directory with a space or a non-ASCII name.

The owner kept in force that the false-pass guarantee does not weaken: what a pass rests on stays proved over the actual program with the same three axioms, and a project with no refusal, on which the rules hold, passes, so a program that refuses everything does not meet the contract. The owner's confirmed examples keep their verdicts, and H1 to H5 stay as stated hypotheses, re-read at each upgrade. Where simplicity outranks the full verdict stays open with the owner, and this revision holds on every branch of that question. The owner answered it the same day, under [the size of the full verdict](#the-size-of-the-full-verdict).

So `Project.InDomain`, `Configuration`, `Answers`, `LakeAgrees`, `DomainRun`, `domain_owed`, `reason_excluded`, `reason_classified`, `run_plain_exit_zero_iff`, `run_full_exit_zero_iff`, `plain_exit_zero_owed`, `full_exit_zero_owed`, `OwedExact` and `OneContext` are gone, and the commit `2c9524b0` holds them. The list is [in the specification](README.md#the-closed-list-of-refusals).

**Follows** means that the restatement settles it. **Decided** means that the owner's delegated agents decided it on the owner's behalf, derived from the restatement and open to change while its words hold, and it is no confirmation of the owner's.

| Consequence | Theorem or measurement | Status |
| --- | --- | --- |
| A run that does not pass rests on a case of the closed list, or on the rules, for every response. | `run_meets`, with `Reason`, `Refusal`, `PlainReason`, `TreeReason`, `BuildRejected` | Follows. |
| A run with no refusal, on which the rules hold, passes. | `plain_owed`, `full_owed`, `run_plain_owed`, `run_full_owed` | Follows. |
| A pass rests on what it rested on before. | `run_meets`, `executed_meets`, `plain_exit_zero`, `full_exit_zero`, `FullRun.gate_stands`, `FullRun.answered_at_consumer`, read with the same three axioms | Follows. |
| A default executable is refused, as RG1010, and so is a default target that names nothing. | `openPaths_of_notLibrary`, `open_path_not_admitted`, `Reason.notLibrary`, and measured | The first follows. The second is decided: `findLib` does not tell them apart, and neither claims a library. |
| A `srcDir` on a target is refused, as a key outside the closed set. | `refused_target_srcDir`, `Reason.key`, and measured | Follows. |
| A source directory with a space or a non-ASCII name is refused. | `openPaths_of_openDir`, `closedSourceDir_of_char`, `space_not_closed`, `nonAscii_not_closed`, `Reason.openDir`, and measured | Follows. |
| The characters of a source directory's names are those of a module name, so a hyphen is refused too. | `closedSourceDir_iff`, `ClosedComponent`, and measured | Decided: one criterion for every name a path is built from. The cost is a rename. |
| A default executable keeps its proof verdict. | `DefaultModules.exe`, `PlainRun`, and measured | Follows from the owner's "every build gets a proof verdict". So `Root.findExe` stays, for the proof verdict alone. |
| The read-back and the test of `lakefile.lean` in the tree stay, and no rule on case takes their place. | `ReadBack`, `FullRun.answered_at_consumer`, `FullRun.config_at_consumer`, `lake_takes_judged` | Decided: they closed an observed false pass on a case-folding volume, and the rule proposed in their place had no theorem and never ran on a case-sensitive volume. |
| A default root that Lake's resolution does not give its own file, and two texts at one path, stay `incomplete`. | `Reason.rootElsewhere`, `Reason.twoTexts`, `Evidence` | Decided: with one source directory, neither can arise from Lake's own answers, by its source. Dropping them would move that fact from a test the run makes into H3, and the owner's words keep the false-pass guarantee. One test replaces the earlier three, `twoFiles`, `twoRoots` and `importedRoot`. |
| A tree inside the project stays a refusal. | `Reason.notApart`, `apart_iff`, `Confined` | Decided: a stated precondition in its place would let a run write into the project. |
| `FullRun.config_at_consumer` needs one answer for a real path, and nothing more. | `OneRealPath` | Decided: it is the one part of the removed `OneAnswer` that a kept theorem used. |
| `reason_classified` has no replacement, so the three-way sorting of reasons is gone. | The list in the specification | Decided: each refusal still stands by itself. |
| A call that does not return, as a read of a FIFO that nothing writes at any path the checker, Lake or Lean reads, and a `TMPDIR` naming nothing are outside the contract, so the claim of no crash on an admitted input does not reach them. Neither has a guard or a timeout. | [Outside the contract](README.md#the-closed-list-of-refusals), and measured for `TMPDIR` and for a FIFO at `lean-toolchain`, `lakefile.toml` and a module's file | Decided, under the owner's rule that a refusal outside the narrow published contract is not a false refusal: each takes the operator's own act and is cheap to undo, and a guard would add an operation, a reason and its proofs while leaving a race. |

No second reading was made of this revision. The owner confirmed the restatement, and the list's other details are the agents', as the table says.

### The size of the full verdict

[What no false refusal means](#what-no-false-refusal-means) left open where simplicity outranks the full verdict. Pull request 530 then counted the full verdict's built size: 11,518 lines of specification and 1,698 of program, about 6.8 lines of specification for each line of program. Shown those numbers against about 4,300 and 1,900 without the full verdict, about 2 to 1, and the case each way, the owner answered "Yes, keep it". In substance: the full verdict stays at its built size, and simplicity does not outrank the confirmed full verdict at this size. The size remains a warning, and work that shrinks it without losing a word the owner confirmed is welcome.

| Consequence | Where | Status |
| --- | --- | --- |
| The full verdict stays, at its built size, and simplicity does not outrank it at that size. | [Purpose and constraint](../README.md#purpose-and-constraint) | Follows. |
| The size stays a warning under the constraint, and a change that shrinks it without losing a word the owner confirmed is welcome. | The same | Follows. |

### The README's reader

While the README was being rewritten on 2026-11-01, the owner, who had found its opening phrase "Regula exists to be trusted" strange, set who the README is for. In substance: a person who wants their agents to write well-factored, well-designed, best-practice Lean 4 code formally proven to be free of bugs. Regula is a linter that gives those agents feedback. That reader wonders what a new tool will do for them, so the problem it solves for them and for the agent writing their code matters more than what it is. Pull request 532 rewrote the README to that.

| Consequence | Where | Status |
| --- | --- | --- |
| The README leads with the problem that Regula solves for that person and their agent, and what Regula is comes second. | [`README.md`](../README.md), and [Text](../CONTRIBUTING.md#text) in `CONTRIBUTING.md` | Follows. |
| Its claims stay exact. | The same | Follows. |

## 2026-10-31

- **"Approve with floor"**: the owner's answer to a restatement of the owner's direction of that day, with RG1001 to RG1006 as the floor. Being free of bugs outranks every lint rule and feature, and Regula gives up what it cannot prove.
- **"B: core, then language"**: the owner's choice of the order of work. First Regula is cut to a small proved core. Then a check is added that reads each source file and refuses anything outside a fixed set of allowed constructs.

The owner made these answers knowing that they reverse consequences confirmed on 2026-10-29.

### The language check

On 2026-10-31 the owner answered "Yes, as recommended" to a restatement of what the check must do, with its cases. The words that follow are the restatement, which the owner's delegated agent wrote after reading Regula's code, the code of two other projects of the owner's and an early prototype of this check, and which the owner adopted. So the second reading below starts from words that the code influenced.

> Before anything is compiled, the check reads every Lean file Lake would compile for the claim, and the project's Lake configuration. If it passes, then while Lake builds those files no code written in the project runs, and no file installs anything that replaces what the compiler runs for a definition. So what the build contains came from Lean's own elaborators acting on source the check read. Whatever it cannot read or does not recognize is refused, including any construct a later Lean adds. An empty set of files is `incomplete`, never a pass. It leaves unsaid what a theorem's statement means to a reader, what another process does, and anything about a dependency's code.
>
> For example, it refuses `run_cmd`, `#eval`, `#guard`, `run_tac`, `by_elab`, `native_decide`, `decide +native`; `macro`, `syntax`, `notation`, `elab`, `initialize`, and `@[local macro k]` on a plain `def`; `lakefile.lean`, and a plugin in Lake's TOML. It admits Regula's own core, and library code using `simp`, `omega`, `decide +kernel`, `variable` and `deriving DecidableEq`. These examples are witnesses of the criterion, not its boundary.
>
> A hypothesis about Lean's behaviour, written in the specification and re-read at each Lean upgrade, counts as Lean staying trusted. So "no bugs" here means no bug outside stated, version-bound claims, and the hypotheses are named wherever a pass is described.
>
> A build importing Mathlib runs Mathlib's code when it imports it, so the check cannot make its promise there. Every build gets a proof verdict, meaning the proofs are sound and use allowed axioms; only a build with no Mathlib in its imports gets the full verdict. Regula's output says which it gave, so neither can be mistaken for the other.
>
> The decision itself is a pure function over the parser's output, proved in both directions against a specification written first and independently of the code. It stays only if it can be proved: if it cannot meet that bar, the result is to say so plainly, not to weaken it. The code is the model of how such code is written. No rule is weakened, and nothing is released from this change alone unless the owner's remaining conditions hold.

The owner's delegated agent amended this on 2026-10-31, on a report that a `lakefile.lean` runs when `lake lint` loads the workspace, before the check starts, so it can act and delete itself, and a full verdict could then be forged. That contradicts the purpose of the restatement. So a full verdict comes only from a checker started from outside the checked project's Lake, built independently of that project and given its path, which reads the configuration by name before any Lake load of the project, and `lake lint` inside a project gives only the proof verdict. As a consequence Regula's own program gets a full verdict on itself from a checker built beforehand from a separate copy. The same agent decided that a dependency with no Mathlib whose files fail the check, or that has a `lakefile.lean`, leaves the build at the proof verdict, and that the check's rule identity is one no released version used for another meaning. None of this is the owner's confirmation.

The owner's delegated agent amended this again on 2026-10-31, after a review found that fetching and classifying dependencies before admission let a manifest act on a path outside the project, that a Lake load with no manifest ran a dependency's configuration, and that the checker's reader lay outside what a full verdict read. A full verdict now requires a project with no dependency at all, read from its Lake configuration before any Lake load. Any `require` leaves only the proof verdict, and the checker fetches and runs nothing of a project's dependencies: it says that only a proof verdict is possible and exits with 3, and the operator gets that verdict with the three commands in the project. Of the checker, everything that does not call Lake is inside Regula's default targets and so inside its own full verdict, and what calls Lake only calls Lake and is named in the trusted base. This replaces the earlier statements of this record that Regula's own program gets a full verdict on itself, and that a dependency with no Mathlib leaves the build at the proof verdict by the check of its files: no dependency's file is read any more. This amendment is the agent's and no confirmation of the owner's. The restatement that the owner confirmed leaves unsaid anything about a dependency's code and says that every build gets a proof verdict, which the three commands still give.

The owner's delegated agent amended this a third time on 2026-10-31, after three review passes each found another path that Lake derives from a project's directory, the last a dangling `lake-manifest.json` link that Lake writes through. The agent decided that a list of derived paths is the wrong shape, however complete it reads today, since a later Lake can add a row. So every path that a child Lake command of the full gate reads or writes lies in a tree the checker made for that run, holding only regular files it read itself, and the verdict is about the files copied. The project's own directory is not written. The cost, accepted: a project that needs another file during its build fails its full verdict, visibly, and each full verdict is one fresh build.

Each consequence below has its status against that restatement. **Follows** means the restatement settles it. **Decided** means the owner's delegated agent decided it on the owner's behalf, with the reason given, and it is no confirmation of the owner's. Each theorem is in `RegulaSpecification/Language.lean` or below `RegulaSpecification/Proofs/`, but for `Report.exitCode_eq_zero_iff`, in `lean/Regula/Language.lean`.

| Consequence | Theorem or measurement | Status |
| --- | --- | --- |
| A reading is admitted exactly when its configuration is closed, everything was read, it has no `require`, Mathlib is absent, each module reached has a name in the closed domain and its file, and each file holds only what the closed set holds. | `decision_admitted_iff`, `decision_meets` | Follows, with the `require` clause and the closed domain from the second amendment. |
| An empty set of files is never admitted, and no claim is `incomplete`. | `no_files_not_admitted`, `languageRecord` | Follows. |
| Mathlib in the imports never gets the full verdict. | `mathlib_not_admitted`, `full_needs_no_mathlib` | Follows. |
| A refused or unreadable project, and one with only the proof verdict, is compiled by nothing, and a build runs only after the check. | `gate_meets`, `build_only_after_check` | Follows, and from the second amendment for the proof verdict. |
| A `lakefile.lean` never gets a full verdict, and nothing under the project's `.lake` is read. | `lean_config_refused`, `readProject_spec`, and measured | Follows from the amendments. A checker that the project's Lake started is outside the contract since the revision of 2026-11-01 under [who started the checker](#who-started-the-checker). |
| Only a pass of the full verdict exits with 0 from the full gate, and the two verdicts are distinct constructors with distinct last lines. | `gate_exit_zero_iff`, `Report.exitCode_eq_zero_iff`, `proof_verdict_lines`, `full_gate_lines`, `verdicts_named`, `pass_lines_name_subject` | Follows. The exit code 3, now for a project with only the proof verdict, is decided: a script must not read a proof verdict as a full one. |
| The check that admits everything, or refuses everything, or gives any other constant, does not meet the record. | `constant_fails` | Follows. |
| Any two decisions that meet the record are equal. | `language_o5`, `fullGate_o5` | Follows from the record, which leaves no freedom. |
| Each construct the restatement refuses by name is refused by the decision, and each it admits is admitted, stated apart from the tables. | `refuses_named_kinds`, `refuses_decide_native`, `refuses_lakefile_lean`, `refuses_plugin_key`, `admits_library_code`, and [what the build holds apart from the code](#what-the-build-holds-apart-from-the-code) | Follows. |
| Other constructs of the families the restatement names are outside the tables. | `refusedKinds_outside`, `refused_attributes`, `refused_options`, `refused_config_keys` | Decided, each read from Lean's sources. |
| A project with any `require` has only the proof verdict, and the gate builds nothing for it, as for Mathlib. | `require_not_admitted`, `dependency_not_admitted`, `fullGateRecord` | Recorded in the second amendment. Its reason: the restatement names Mathlib for a reason, that its code runs when it is imported, and that reason holds of any dependency. "Only" makes no Mathlib necessary and not sufficient. A full verdict there would be false, so this errs toward no claim. The cost, accepted: a project with a harmless dependency gets only the proof verdict. |
| A project's file is refused if it is not a `module` file. | `languageRecord`, `ModuleFile` | Decided: in a `module` file with no `meta`, Lean itself refuses to evaluate a project's constant, so a route that the table misses still meets Lean's own check. |
| Reading a project with a failure is `incomplete`, not `refused`. | `languageRecord` | Decided: both refuse to pass and compile nothing, and RG2001 already means that something could not be read. |
| An identifier with a component that starts with `_`, other than a first `_root_`, is refused, so a binder such as `_h` is too. | `ReservedName` | Decided: the compiler reads such names by their form, and the positions that declare a name are an open list. The cost is a rename. |
| `include_str`, `:= by` defaults of a binder, `open ... hiding`, `open ... renaming` and tactic configuration other than `+kernel` are refused. | `refusedKinds_outside`, `configItems` | Decided: each either reads something the check did not read or can reach an evaluation or a scoped parser. Each refusal is visible and cheap. |
| A plain `lake lint` runs no language check, and gives the proof verdict. | `Regula.Shell.run`, `PlainRun` | Follows from the amendment. One process runs the check and the build, because only such a process can say that a build followed the check: decided. |
| Regula's default targets get a full verdict on themselves, from a checker built first from a copy of these same sources, and every function of the checker that does not itself call Lake is in a default target. | `lean/Regula/DiagnosticsGate.lean`, a step of the gate; `lakefile.toml` | Follows from the second amendment, which replaces the first's statement about Regula's own program. `Regula.Workspace`, which only calls Lake, and the thin root `Regula.LintMain` stay outside it and in the trusted base. So the verdict shows that these sources are in the closed language and that compiling them again ran no project code. It does not show that the first compile, of the copy, did not: the checker's own sources are what a checker has to trust. |
| A project's `lean-toolchain` must name the pinned Lean, and the checker builds with the Lake beside its own Lean. | `ConfigClosed`, `Regula.Shell.build` | Decided: a project's file must choose nothing about which Lean runs, and a project that names another is one whose author means another. |
| A `require` in any TOML form stops the reading before any Lake call, and no manifest is read. | `RequiresDependency`, `keysOf_sound`, `keysOf_complete`, `KeyPath`, and measured | Decided in the second amendment: Lake decodes a dependency from exactly that key, so its root is the test. A manifest is no input, because it is not in the tree. |
| A module's name, and a library's or an executable's, must be in a closed domain, each file read must be by its real path exactly its own path below the project's real path, and a module is the file Lake's own import resolution names. | `ClosedModuleName`, `closedModuleName_iff`, `exactBelow_iff`, `ReadAs`, `walk_spec`, and measured | Decided: no value a project controls may select a path outside the project or the toolchain. The cost, accepted: a harmless name outside the domain is `incomplete` until it is renamed, and a file reached through a harmless link is `incomplete` until the link goes. |
| Each source directory of the package, its libraries and its executables must lie below the tree, and each `globs` entry must be a single module. The checker lists no directory. A project outside this is refused. Since [the confirmation of 2026-11-01](#what-no-false-refusal-means) the names of a source directory are closed too, and each default target is a library. | `ConfigClosed`, `open_path_refused`, `open_path_not_admitted`, `treeRelative_iff`, `openPaths_reason`, and measured | Decided: a closed domain costs less than arguing about an open one. The cost, accepted: a library with a recursive glob is refused until it names its modules. |
| Each Lake call and child process of the full gate works in the checker's tree, which holds what the checker read and the two files it wrote, and no file of the project is written. | `readProject_spec`, `Confined`, `FullRun` | Follows from the third amendment. |

**Measured** on 2026-10-31 on the first project this applies to, Regula itself at commit `c034e9d3`: a checker built from a separate copy gave `full verdict: pass` on the 13 files of Regula's default targets, as a step of the gate, and on the 15 files at the change that made the run a program. No open item depends on another external tool.

The second reading was made by Codex `gpt-6-astra` at `xhigh`, through `codex exec` with no user configuration, memory, hooks or session file, from the restatement above, the definition of `Lean.Syntax` and lean-intent's `LeanIntent/Record.lean`. These were in its prompt, after a first session could not read files inside this machine's own sandbox. Its event log records no command, and its own list of what it read names only those. Its global instruction file, the owner's standing instructions, was loaded, and it holds nothing of this record. Its subject type differs, so no comparison by theorem exists: each difference below is stated in plain words, and is unproved.

| Difference | Settlement |
| --- | --- |
| It gives the full verdict to every pass with no Mathlib, and refuses a dependency outside the closed set. This record, since the second amendment, reads no dependency's file and leaves any project with a dependency at the proof verdict, which the two commands give and the gate does not build. | Decided for this record: "every build gets a proof verdict" asks for a verdict there, and neither reading gives a false full verdict. |
| It reads "cannot read" as `refused`. This record has `incomplete`. | Decided as in the table above. |
| It makes an empty set `incomplete` even with a refused configuration. This record refuses the configuration first. | Decided: Lake's load comes after the refusal of a configuration, so the order is the order of what runs. Neither passes. |
| It names hypotheses in every pass. This record names H1 to H5 and the trusted base in the full verdict's last line, and the proof verdict's says that it says nothing about what ran. | Decided: those are what the full verdict rests on, and the proof verdict rests on none of H1 to H5. The documents name them for both. A shorter line that named H1 and H2 alone was a false statement of what the verdict rests on, and it was corrected on 2026-10-31. |
| It has an abstract `requiredAdmission` family that must have instances, and the check must pass them. This record has `goodReading`, and the gate's run of the check on Regula. | Decided: a run of the real parser shows more than an abstract family, and it is a measurement, not a proof. |

The second reading was of the restatement before the amendments, whose words are not the owner's, so it was not made again. Later reviews found what it did not read: it stated a read before compilation, and neither it nor this record's first form said where Lake's own reads and writes go.

The owner has answered no fork of this check beyond the restatement.

**The stand-ins for lean-intent's checks**, read on the forge on 2026-10-31. Issues 2, 3, 4 and 6 of rbeauchamp/lean-intent are closed, and each feature is at the commit this package pins, so no stand-in for them is needed. Issue 2: lean-intent's `Cone.checkRecord` accepted both records against the implementation's names, in a scratch run. Issue 3: each consequence above is a theorem about the record by name, so a revision that loses one fails the build, and no `Accepted` value is declared, because the owner answered a restatement and no consequence one by one. Issue 4: the record's source is what this file cites, and no rendering was shown, because the owner's attention went to the restatement. Issue 6: `Reading` holds `Lean.Syntax`, which lean-intent's degenerate class does not cover, so `constant_fails` is the check by other means that its document allows. Issue 5 is open, so this file stands in for the confirmation record, and nothing checks it against the record.

### The run of the checker

The owner's account of 2026-10-31 says that only Lean, its kernel and Lake's own behaviour stay trusted, and that Regula's own code, its loader and command-line shell included, is proved or so thin that it only calls Lean, and that a stated hypothesis about Lean's behaviour, re-read at each upgrade, counts as Lean staying trusted. The owner's delegated agent, who had read the code, then asked for that account to hold of the effects of a run: the only unproved code left in what decides a verdict makes no decision, every decision is proved over the definitions the program runs, and the verdicts keep their meanings. The owner was asked nothing new for this. So `programRecord` is the agents' design, derived from that account and decided on the owner's behalf, and no consequence below is the owner's confirmation. The author of the record had read the code before writing it, so the record's independence from the code is weakened that far.

**Follows** means that the account settles it. **Decided** means that the agent decided it on the owner's behalf, with the reason given.

| Consequence | Theorem | Status |
| --- | --- | --- |
| A run's exit code is the verdict's alone, and so is its last line but for the directory that a pass names at its end, on what the proved decisions give for what Lean, Lake and the operating system answered, for every answer. | `run_meets`, `plain_exit_zero`, `full_exit_zero` | Follows. |
| Every file Lake would compile for the claim is read, and the configuration, and the text judged is the text that stands in the tree. | `Evidence`, `ReadText`, `written`, `FullRun.at_consumer`, `read_what_lake_compiles` under H3 | Follows. |
| A failed read is never admitted, and nothing is built unless the check admitted. | `readProject_no_failed`, `only_readProject`, `FullRun` | Follows. |
| A run writes only in its tree, which lies apart from the project, and asks to remove it on every way out. | `Confined`, `FullRun` | Follows. Refusing a project and a tree that do not lie apart is decided: without it, a project at `/tmp` would hold the tree. |
| A reader that refuses without a reason does not meet the record, and for paths that meet the hypotheses `WitnessPaths` there are answers on which a project is admitted. | `Reason`, `refuser_fails`, `admits_a_project`, and [the next section](#a-pass-is-owed) | Follows from the account's "a checker that refuses nothing" and its converse. The hypotheses are decided: they rest on observation, the gate's run on real paths, because no reduction of the kernel evaluates `System.FilePath`. |
| "So thin that it only calls Lean" is a straight line of calls that passes each result on, with no test or branch of its own on any result. | `table_rows`, `Regula.ProgramCheck.Effects` | Decided by the owner's delegated agent, who amended the account's words to this after the implementer reported the rows with more than one call, with the reason in [the specification](README.md#so-thin-that-it-only-calls-lean). No row was split. Each selection of what Lake returned is named there with its source. It is no confirmation of the owner's. |
| A failed removal of the tree and a failed print change no verdict. | `FullRun`, `Regula.Reader.say` | Decided: a tree left behind affects nothing later, and the exit code still says the verdict. |
| Each line before the last starts with two spaces, and the last is a function of the verdict and, on a pass, of the directory it names at its end, so the count of findings and a reason of `incomplete` are lines of their own. | `EndsWith`, `Regula.Closed.Verdict.proofLineOn` | Decided: it makes the requirement on the last line true by construction, and no name in a project can print a verdict. It changes the output's form, and no verdict. |
| A default root that Lake's import resolution does not give its own file is `incomplete`, so a module name that two default targets hold with two files is. | `rootElsewhere`, `Compiled` | Decided: the proof that every file Lake compiles is read needs it. |

The second reading was made by Codex `gpt-6-astra` at `xhigh`, through `codex exec` with no user configuration, memory, hooks or session file, from the owner's account, the types of `Regula.Effect` and of the reading, and lean-intent's `LeanIntent/Record.lean`, in its prompt. Its event log records no command and its own list names only those three. Its global instruction file, the owner's standing instructions, was loaded, and it holds nothing of this record. It gave no Lean record: it said that the inputs do not determine one, because the rule predicates and the interpreter were not among them. So no comparison by theorem exists, and each difference is stated in plain words and is unproved.

| Difference | Settlement |
| --- | --- |
| It said that thinness concerns the interpreter, which a predicate of `run` alone cannot distinguish. | Settled by the design: `table_rows`, `executed_meets` and `Regula.ProgramCheck.Effects` state it apart from `programRecord`, whose subject is `run`. |
| It said that unconditional refusal cannot satisfy the clause that the verdicts keep their meanings. | The same reading: `Reason`, `refuser_fails`. |
| It left the exit codes, the output's text and the reading of the command line unsaid. | Decided: they keep what the specification states, with the change to the last line above. |

**The stand-ins for lean-intent's checks** are as for the language check. Issue 2: lean-intent's `Cone.checkRecord` accepted `programRecord` against `Regula.Shell.run`, `runFull`, `runPlain`, `Regula.Reader.readProject`, `walk` and `readExact`, in a scratch run on 2026-10-31. Issue 5 is open, so this file stands in for the confirmation record, and nothing checks it against the record.

[The README](../README.md#purpose-and-constraint) states the purpose, and the section "What the owner's intent requires" of [the specification](README.md) states what follows from these answers. A detail below that level is marked in the specification as decided on the owner's behalf, and it is no confirmation of the owner's.

### A pass is owed

An independent audit of main at `f63d7596` judged that this record did not yet meet the owner's account, because it let a run report incomplete on a failed answer to anything, and because programs kept for validation made decisions that no proof covered. So this revision of `programRecord` is the agents' design, derived from the account's "no false refusal" and from the account of this change, which the owner's agents wrote from the audit's report: a run refuses or reports incomplete only for a reason the requested build's own inputs and operations give, and a run in which nothing the build needs has failed, on a project the contract admits, passes. The owner was asked nothing new for this. The author of the revision had read the code before writing it, so its independence from the code is weakened that far. It was sealed by a commit before the second reading below, and the code that it is proved against did not change for it: `Regula.Shell.run`, `Regula.Reader` and `Regula.Load` are as they were.

Validation of this revision then showed that relevance alone admitted an obstructed copy. So the agents strengthened the record, deciding on the owner's behalf and deriving it from the account's "no false refusal", and the owner was asked nothing new for this either: the record constrains every occurrence of an operation that depends on the tree the run itself writes, including a failed attempt, each operation on a search path names that path, and the actual reader, loader and shell stay unchanged. The subject can choose adversarial acts, and responses are arbitrary; no consistency of a filesystem may be assumed. The mechanism is an ordered grammar of configuration copies, load and named-module copies, followed by the closed build/reload protocol and terminal removal. Module copies need earlier source reads, configuration failures end the acts, and module failures permit the walk to continue. This leaves the requirements on relevance and owed passes in force.

The grammar is a relation made true by its constructors; its linkage to the actual definitions is a universal proof over their exact traces. A type cannot establish the truth of external responses, so the proof constrains requests without promoting those responses into filesystem facts. `Op` and `Runs` supply the closed operation domain and exact sequence, and the preparation proofs compose those sequences by append and insert nothing into them. That closes the reasoning gap which previously treated path membership as readiness. Another order of reads, and another order within the closed acts that changes no response used by the run, are accepted risk with a visible refusal as their possible cost. Inconsistent responses, external changes to the tree and effects inside trusted calls remain outside the request guarantee. A crash may leave a newly allocated directory that later runs do not read.

The operation class, the arbitrary-response model, the retained legitimate failures and the unchanged program are decisions of the agents, derived from that account. `EffectsRecord.lean` states the ordered relations; `Proofs/Preparation.lean` states their consequences, and the one theorem of each stage (`readProject_spec`, `inputOf_spec`, `loadTree_spec`, `loadPlain_spec`) links them to the definitions that run.

| Consequence | Theorem | Status |
| --- | --- | --- |
| A refusal, a failure or an incomplete result rests on a response about a needed input or operation, with the preparation that the run itself supplies still in place at that occurrence. | `Reason`, `Needed`, `PlainReason`, `TreeReason`, `BuildRejected`, together with `ReadingPreparation`, `BuildProtocol`, `RulesPreparation` and `PlainPreparation`; `run_meets` links the complete record to the program. | Decided on the owner's behalf, derived from the account's "no false refusal". No relation asserts consistent external responses. |
| The reported trace that creates a directory at the TOML destination and then cites its failed write cannot meet the record; each later copy has prefix-based provenance and each lookup and import names its loaded root's search path. | `manufacturedCopy_fails`, `manufacturedCopyAnswered_fails`, `parent_ne_self`, `ReadingPreparation.first_directory`, `readProject_spec`, `inputOf_spec`, `loadTree_spec`, `loadPlain_spec` | Decided on the owner's behalf: the exclusion, the operation class and the exact segment decomposition are the agents' design, derived from the account's "no false refusal" and chosen to retain failed attempts and prevent inserted acts. |
| A run in which no reason holds, whose build ended with 0, whose replay of the claim's cone Lean's kernel accepted, and whose build has `BuildAnswer.Floor`, gives the pass verdict and exit 0, for every program that meets the record. | `plain_owed`, `full_owed`, `run_plain_owed`, `run_full_owed` | Follows. |
| The loader and the rules pass exactly on `BuildAnswer.Floor`, which names no field of the input and none of the checker's functions. | `pass_iff_answer`, `loadFloor_iff`, `pass_iff_floor` | Follows. It holds with no hypothesis. |
| A run that exits with 0 received no failed answer. | `PlainRun`, `FullRun`, by the program's `loadPlain_spec`, `loadTree_spec`, `readProject_no_failed` | Decided: it makes a pass read as what it says. A failed print or removal is no failed answer, because no verdict rests on it. |
| The bound of `tooMany` is strict and counts the roots and the imports of distinct files that the build needs. | `Reason.tooMany`, `walk_spec` | Decided: the walk stops only when more names are left than it follows, and a parse of anything else counts for nothing. |
| A dependency deeper than the reader follows may report that only a proof verdict is possible, whatever the root of its deep key. | `Reason.deepDependency` | Decided, accepted risk: it can only change exit 3 into exit 1 or back on a project that is admitted by neither, so no pass depends on it. |
| The premises are met by a run on the witness's answers, and that every operation succeeded does not settle the conclusion. | `full_model`, `plain_model`, `refused_model` | Decided. The pass models are conditional on `WitnessPaths` and `EnvModel`. |
| The check of effects, the gate's wrapper and the listing decide nothing that no proof covers. | `allowed_iff`, `check_ok_iff`, `runStep_ran`, `runLocal_zero`, `main_runs`, `main_zero` | Follows. Their programs kept their paths and what they establish. |

The second reading was made by Codex `gpt-6-astra` at `xhigh`, through `codex exec` with no user configuration, memory, hooks or session file, from the words of the account, the types of `Regula.Effect`, the events and the reading, and lean-intent's `LeanIntent/Record.lean`, in its prompt, after the record's commit. Its event log records no command, and its own list names only those three. Its global instruction file, the owner's standing instructions, was loaded, and it holds nothing of this record. It gave a record over parameters, for what is admitted, what a pass is and what the build provides, because it said that the inputs do not define them. So no comparison by theorem exists, and each difference is stated in plain words and is unproved.

| Difference | Settlement |
| --- | --- |
| Its properties read "what the build provides" and "admitted" as parameters. | The same shape: `Needed`, `Reason` and `FullOwed` define them, from the operations that a run of a build asks. |
| It said that a later failure must not justify an earlier report, so a reason is read from the prefix before the report. | The same reading: `EndsWith` makes the verdict the last event, so a reason precedes it. |
| It asked that every admitted request finish for every plan of responses, and said that the type of `Prog` gives that. | The same reading: a `Prog` is a finite tree, and `runs_with` gives a run for every function of the operation. No property is needed. |
| It said that a successful read of a violation can justify a refusal, so that a failure is not the only reason. | The same reading: the content cases of `Reason`. |
| It said that the programs kept for validation are other subjects than `run`. | Settled by the design: their theorems are apart from `programRecord`. |

**The stand-ins for lean-intent's checks** are as above. Issue 2: lean-intent's `Cone.requireIndependent` accepted this revision of `programRecord` against `Regula.Shell.run`, `runFull`, `runPlain`, `Regula.Reader.readProject`, `walk` and `readExact`, in a scratch run on 2026-10-31. Issue 5 is open, so this file stands in for the confirmation record, and nothing checks it against the record.

## 2026-10-29

- **"Confirm all"**: the owner's answer to the plain-word consequences of an earlier, larger specification, which the commit `ea69f22f` holds at `specification/README.md`. The answers of 2026-10-31 replace each consequence of it that concerns what this cut removes.

## What the build consumes

An independent audit of main at `48431e2c` judged that this record did not yet meet the owner's account: its contract of a full run let a run read a named file again and copy that new text over the tree after the check had judged an earlier one, and kept the earlier evidence. The audit proved that for every text, and it observed no false verdict of the program. It also found a published comment that said more than its theorem. The owner was asked nothing, and no owner decision came of this: the account says a contract that misses the intent is a bug, and that the property must be proved, or the verdict removed by the owner's own call. It was proved. What follows was decided by the agents on the owner's behalf, derived from that account, and none of it is the owner's confirmation.

The first statement of the property is that a full verdict's admission is about what the build consumes. The agents wrote the record first, on the words of that account, with the reader already known to its author from the audit's report, so the method's premise is weakened that far. They sealed it before reading the second reading.

| Consequence | Theorem | Status |
| --- | --- | --- |
| When a full run reaches a Lake command or a load for the rules, there is a reading inside the closed language, with no failed answer, on `Evidence` of what it leaves, and at each point of the gate that is what stands. | `FullRun.gate_stands`, `FullRun.at_consumer` | Follows. |
| Each file Lake compiles holds the text that the reading's file of its module was parsed from, under H3. | `read_what_lake_compiles` | Follows. |
| Each text standing by the run's requests is the configuration's, the pinned text, or one a file of the reading was parsed from, so the run asks no other file into the tree. | `Evidence.judged`, `Evidence` | Decided: Lake prefers a `lakefile.lean` in the tree, so a file outside the reading could run code at the build with no language check, whatever name it came under. |
| A trace that ends by copying a text other than the pinned one, which it judged nowhere, has no `Evidence` of what it leaves, and no full run reaches a build after it. | `uncheckedCopy_fails`, `uncheckedCopy_build_fails` | Follows. |
| A copy of the text already standing keeps the evidence, and after two writes what stands is the last. So a program that writes one text, reads again and judges the later one rests on the later one. | `judgedCopy_stands`, `rewritten_stands` | Follows: the later text is the one judged. |
| Two texts at one path are `incomplete`, by components before a module's file is written and by the read-back after it. | `Reason.twoTexts`, `twoTexts` | Decided: `Evidence` credits one text at each path. |
| A module's text reaches the tree only for a reading the decision admits. Each source is written once, so a path with two names is written twice with one text. | `Regula.Reader.readFiles`, `writeSources_spec`, `holds_of_leavesAs` | Decided: `FullRun` admits other orders, and the program takes this one because the property then follows from its shape and needs no invariant over a walk that writes. It rests on Lake's load and resolution reading no module's file (H3). |
| A failed write of an admitted file is `incomplete`. | `readFiles_spec`, `Needed.sourceWrite`, `Needed.sourceParent`, `Reason.moduleNotInTree` | Decided: the build could not consume what was judged. |
| A failed write counts as written, so a later `written` does not credit the text before it. | `Event.leaves` | Decided: a failed write leaves the file unknown. An admission receives no failed answer anyway. |
| Each text credited is the file system's answer for its path after the reading's last act, with no act of the reading after it. `Regula.Reader.readBack` stops at a differing or failed answer, which is `incomplete`. | `ReadBack`, `FullRun.answered_at_consumer`, `act_after_readBack_fails`, `readFiles_spec`, `Reason.treeDiffers` | Decided: a fold of requests is a model of the file system, and the pipeline's live run reproduced a full pass in which a second text had replaced the first, which the fold does not show. Observing the answer takes no assumption about which paths alias; that a read and a build through one path name one file stays trusted. It costs one read per planned entry. |
| What Lake and another process do to the tree after that answer stay out of the record. | [the trusted base](README.md#the-trusted-base) | Decided: the account keeps inconsistent responses and external changes as accepted risk. |

**The class closed.** A fact a verdict rests on about state the run's own acts can change after the fact was established, over the closed acts of `Op`, in the full run and the plain run. Found by reading `Op` and each relation that reads an event: the acts are `writeFile`, `createDirAll`, `createTempDir`, `removeDirAll` and `runLake`. A search path is no such state: each lookup and each import names its own, as the operation's argument.

| State | Fact, and its consumer | How it is closed |
| --- | --- | --- |
| A module's file | The text judged, at the build and the reload | `Evidence` of `written` (`FullRun.gate_stands`). |
| `lakefile.toml` | The text Lake's parser read, at the load, the build and the reload | `PreparedLoad` for the first load, `Evidence` of `written` for the rest (`FullRun.gate_stands`). |
| `lean-toolchain` | The pinned text, at the same | The same. |
| Any other file of the tree, such as a `lakefile.lean` | That the run asks nothing else into it | The last clause of `Evidence`. That nothing else is there rests on `createTempDir`. |
| A directory at a file's path | That a write can store it | `CopyStep` makes only a file's own parent. A file below another file is a project with two such paths, and the failed response is its reason. |
| The whole tree, by `removeDirAll` or `createTempDir` | That it still stands | `FullRun` admits one allocation first and one removal last (`FullRun.removal_order`), and `Event.leaves` reads a removal. |
| The tree, by `runLake` | The build, at the reload | `BuildProtocol` asks one build with only reporting around it, and `BuildAndRules.no_mutation` asks no write after. What the command does inside is Lake's. |
| The search path in the reading | A toolchain module's place, and the parser's environment | No state: each lookup and import of `ReadingLoaded` names the toolchain's library. |
| The search path at the rules | Where the build's modules are, and the import | No state: each lookup and import of `RulesPreparation` and `InputPreparation` names the loaded root's search path. |
| The search path in a proof verdict | The same | No state: each lookup and import of `PlainPreparation` names the loaded root's search path, and a plain run has no other act (`PlainRun`). |
| The project | What was read of it | When an act lies below the tree, the two real paths lie apart (`Confined`), and an act at the tree itself rests on `createTempDir`, so `Evidence.mono` keeps what no act of the run can change. Another process changing the project reaches only what the next read gives. |

**The second class closed.** An assumption of the record about what the file system does with the run's own writes, over the closed acts of `Op` on the tree. The plain run writes no tree and is outside it.

| Assumption | How it is closed |
| --- | --- |
| Different components name different files | Removed for planned paths: an alias between them with different texts is an answer that differs, and one with agreeing texts passes. An earlier form of this row said that a spelling no plan names is accepted risk, and that a module spelled `LakeFile` mattered only on a case-sensitive project with a case-folding tree. An audit showed that false: on one case-folding volume, with `LakeFile.lean` created in the project after the test for `lakefile.lean` found nothing, its text was judged, and Lake then took the copy in the tree as its configuration. The file has a second role that the read-back did not observe, so the run now asks the file system through Lake's own name (`ReadBack`, `Reason.configShadowed`). |
| A write that answered success stored its text | Removed: the same. |
| A failed write left what stood | Removed: `Event.leaves` counts it as written, an admission has no failed answer, and `ReadBack` sees what stands. |
| `createDirAll` changes no file's text | Removed: the read-back comes after the last `createDirAll`. A reading that ends with an act fails the clause, and a read-back after that act is the one that counts. |
| `removeDirAll` takes a file away | No admission rests on it: it is the run's last act, and `Event.leaves` reads it. |
| `createTempDir` makes an empty directory | Removed for a file the run wrote. A file the run did not write and that was there is outside what `written` credits, and Lake's reading of one rests on that call. |
| `runLake` keeps the text of the sources | Trusted: what a call of Lake does inside itself. |
| A lookup's search path has no effect on a file | It is no act on the tree, and there is no file-system state to read back: the request names the path, and what `findOLean` then answers is the response. |

`Evidence.mono` is kept, with the state fixed: it says what stays true of what was read, and `written` says what stands.

By `git diff --numstat` against `48431e2c`, with the read-back and the docstring corrections below: the three record files grew by 84 lines net, `Standing.lean` and `Written.lean` total 543, the proofs of the reader changed mostly where `readSource` and the walk lost their write and where the read-back came in, and `Reader.lean` grew by 64 lines net. `Evidence` is a state and two clauses longer, `Decided` adds `ReadBack`, and the copy grammar's rules are unchanged.

The second reading was made by Codex `gpt-6-astra` at `xhigh`, through `codex exec` with no user configuration, memory, hooks or session file, from the account above, the types of `Regula.Effect` and of the reading, and lean-intent's `LeanIntent/Record.lean`, which were in its prompt, because a nested confinement refuses its reads. It read no file. It gave a schema with the trace predicate as a parameter, and said that the types it was given do not define admission, a full build or consumption. So there is no theorem to compare, and these are differences in plain words, labelled unproved.

| Difference | Settlement |
| --- | --- |
| It said that the obligation holds when the build fails too, so a condition on a successful exit would miss a false refusal. | The same reading: `FullRun.at_consumer` holds at each command, whatever its response. |
| It said that defining consumption as the last successful write is an equivalence the types do not support. | Settled in the same direction: `written` says what the run asked, and that Lake reads what stands is H3 and the trusted base, not a claim of the record. It counts a failed write too, for the reason above. |
| It did not ask for one read, for no overwrite, or for no alias. | The same reading: the record asks for none of them, and `twoTexts` is the program's. |

No difference reached the owner's level. The stand-ins for lean-intent's checks are as for the sections above.

Three readers who did not write them read the class of a docstring whose conclusion its statement does not carry, across `Proofs/`, `lean/Regula/ProgramCheck/` and the README sentences citing them: about 730 comments. They found about 80 such sentences, each corrected in this change or, for `FullRun.at_consumer`, by a stronger statement. The worst were of the audit's shape: `treeRelative_no_parent` said that a join could not leave the directory, `below` and `exactBelow` were said to state what their names say, and `main_zero` of the listing named what `main` printed with no such link. The same reading found that `ConstantInfo.value?` gives no value of a theorem or an opaque constant, so the check of effects reads neither. The text now says that, and the check is unchanged: this change's boundary leaves it, and a value of those kinds that mentions an effect stays what it was.

### A statement of who is owed a pass, withdrawn

An independent audit of the revision `802ba3c7` reproduced two findings against the owner's account of 2026-10-31. A project with two default libraries, `srcDir` spelled `.` and `./`, was refused, and `FullOwed` was the absence of every reason, so the proofs and the program shared one mistake. And a published claim about a module spelled `LakeFile` was false, as the row above now says. The owner's delegated agent then published a statement of which projects a full verdict is owed to, `Project.InDomain`, and proved each refusal justified against it. It also decided, open to the owner's reversal, that another process is left unsaid by what the owner confirmed, and that `PATH` selecting the genuine `lake` and `lean` stays a stated premise of using the checker. On 2026-11-01 the owner [withdrew that statement](#what-no-false-refusal-means), so the commit `2c9524b0` holds it, with its consequences and its second reading. These remain, each decided on the owner's behalf:

| Consequence | Theorem or measurement | Status |
| --- | --- | --- |
| A project whose module the tree's volume takes for `lakefile.lean` is refused: as `incomplete`, when the project's own test of that name found nothing, and otherwise by that test. On a volume that does not take it so it is not refused. | `Reason.configShadowed`, `FullRun.config_at_consumer`, and measured on a case-folding volume | Follows for the refusal: Lake would run that file, which is what the owner's refusal of `lakefile.lean` is for. That the verdict can differ between volumes is decided: a rule on the name's text would have to model folding and still miss what it does not model. |
| What Lake takes as its configuration is `lakefile.toml`, given H5 and that the answer still holds at the consumer. | `FullRun.config_at_consumer`, `lake_takes_judged`, `LakeSelection` | Follows, under H5. Another process is left unsaid. |
| A `srcDir` that names a directory by another case than a volume stores gets `incomplete` on that volume, by the exact-path test. | `Reason.moduleNotExact`; read from `realpath`, and measured of `realpath` | Decided: a name's case is a way for a path to name what the file system holds otherwise, and the test takes no model of folding. The cost, accepted: its author corrects the spelling. |

### Who started the checker

An independent audit of main at `a399fbe9` judged the owner's account unmet by one blocker. A healthy project passed the full gate; then only the checker's `.lake` directory was moved to a sibling and replaced by a link to it, and the same command refused, saying that the project's Lake had built or started the checker, which was false. The program derived its own library from its real path and compared that string with Lake's spelling of the same directory. The proof could not see it, because `Answers.start` required the program's own tests to return the wanted Booleans, so the owed-pass theorem had a false premise on that run.

On 2026-11-01 the owner confirmed that Regula is meant to be to Lean linters what seL4 is to kernels, and that removal comes first: before adding or repairing anything, ask whether it can be deleted or its input narrowed so the need goes away. Refusing something outside a narrow published contract is no false refusal. The owner's delegated agent then decided, on the owner's behalf and reversibly, that Regula stops trying to detect who started the checker, replacing that agent's amendment of 2026-10-31 above: the restatement the owner confirmed names no starter, the detection was by its own account no defence against project code that ran first, and it cost about 620 lines of code and proof. Each row below is the agents' design, derived from the account, and no statement of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| Starting the checker from its own package is a precondition of the full verdict, beside `PATH`. A start from a project's Lake is outside the contract, and nothing tests it. | [The language check](README.md#the-language-check) | Decided by the owner's delegated agent, for the reason above. |
| Every Lake command the gate runs gets a closed environment, so no variable that a Lake composed reaches its lookups of a program or a library. | `spawnLake_eq`, and measured | Decided: the detection did prevent one harm, a planted `<project>/.lake/build/bin/which` that `lake check` would run, and this closes it for every start. |
| A checker or a project whose path holds `:` gets its full verdict, since nothing reads the checker's path. A workspace whose path holds `:` gets `incomplete` from `lake lint`, because its search path cannot name it. | `startsSearchPath_eq_true_iff`, and measured | Decided: a mode for that spelling would add code to avoid a truthful refusal. |
| A module that Lean's search finds on the toolchain's library is the toolchain's, with no test of its real path. | `HeldByToolchain`, `toolchainOLean_spec` | Decided: those directories are the whole search path, and a project does not control them. A module that the search names and that does not exist fails the parser's import, which is `incomplete`. |
| Each premise of an owed pass is stated by what Lean, Lake or the operating system answered. | `Reason`, `ExactlyBelow`, `StrictlyBelow`, `SearchPathStarts`, `BuildAnswer.Floor`, `parts` | Decided: `parts` and `inputNameOf` state over Lean's `FilePath` functions what the checker computes, and each decision has its theorem in `Proofs/Paths.lean`, `Proofs/Floor.lean` or `Proofs/ReaderWalk.lean`. That rule is written, and no check enforces it. |

The specification's sentence of this revision that on macOS a planted `libc++` did not load into the checker, marked measured, was false, and its measurement observed only that no marker was written: [what was measured](README.md#what-was-measured) corrects it, and [a project aimed at the checker](README.md#a-project-aimed-at-the-checker) states what follows for the proof verdict.

## What the build holds apart from the code

On 2026-11-01 the owner asked for an analysis of where the proofs stop constraining reality. It replaced the result of each definition at `2c9524b0` by a constant and rebuilt Regula and this package. 26 of 728 changes still built, among them `Verdict.proofLine` and `Language.Report.label` as the empty string and `DiagnosticsGate.runStep` as `pure default`. None was a bug seen in the program. Each showed a behaviour the owner confirmed, or a check something relied on, that no theorem constrained, because a proof whose expected value is read from the code under proof shows agreement with that code and not what the owner asked for. The owner asked that what was confirmed be stated apart from the code's own values and proved over the actual decision.

The owner's delegated agent decided, because the link from the parser's real output to the model is being investigated apart and is not settled here, that an example is stated over the parser's node kinds or the decision's input, and that one that cannot be stated so is named as observed. Everything below but that request is the agents' design, derived from it, and none of it is the owner's confirmation.

| Consequence | Theorem | Status |
| --- | --- | --- |
| Each example of the restatement, stated with literal expected values over `decision`. | `Proofs/Owner.lean` | Follows. |
| Admitting Regula's own core is observed, by the gate's run of the full gate on this checkout. Only its Lake configuration's key paths are stated. | `core_configuration_admitted` | Follows from the agent's decision above. The gate's step fails if a table loses what the core uses. |
| Each sentence of a verdict is stated word for word, so a reword is an edit of two files. | `proof_verdict_lines`, `full_gate_lines` | Decided: the owner asked that neither verdict can be mistaken for the other, and a statement of prefixes alone would let a sentence lose what it says a verdict rests on. |
| A kind added to `leafKinds` that is not open text fails a build, so that no construct can be hidden from the check that way. | `unread_kinds_are_open_text` | Decided: `Occurs` reads that table, so each theorem over it would otherwise read a table for its reach. |
| What a successful gate step is: it spawned exactly its request and carried that child's wait. | `stepRequest`, `StepRan`, `runStep_ran` | Follows. Which program `PATH` selects and what Lake's exit code means stay trusted. The message a step prints is split out as `announce`, so a reword of it is no edit of this statement. |
| The namespaces that hold a scoped parser are what Lean's own parser extension holds. | `importParsers_eq` | Decided: H1 reads that state, so the statement names it. |
| The module copies and the rules' reading hold no load, Lake command, removal or allocation. | `ModuleCopies.not_barred`, `InputPreparation.not_barred` | Decided: this document said it, and no theorem relied on the lists of allowed operations that say it. |
| What may mention an effect is stated by the modules' names, apart from the table. | `allowed_iff`, `check_ok_iff` | Decided: the check would otherwise pass whatever `allowed` said. |

An audit of `2c9524b0` by a worker of the owner's delegated agent then added three points, and the agent amended the account with them. `Proofs/Premises.lean` is gone with its prevention claim: it decided whether this package builds, over a hand-kept list and a walk limited to two namespaces, with no theorem about what it decided, and it reported success on an empty or a missing root, so it could not establish what was claimed for it. The written rule that a premise states what a system answered stays, and a later premise that breaks it is accepted risk that review and audits carry. The inventory of visible bodies is corrected. And RG1006's exception is published as a form: on 2026-10-31 the owner chose that a pass of the proof verdict means that the proofs are sound and use only allowed axioms and says nothing about what a compiled program runs, having been shown that a forged helper passes RG1006. That the input records a form and no origin, that no sentence guarantees an origin, and that the reason is `helperForm_unreached` under H6, are the agent's decisions under that choice, and no confirmation of the owner's.

**Text that only explains** stays free of a contract: a finding's detail, a line number, a usage list, a coverage summary and what the gate prints. A wrong one is cheap to undo and changes no verdict. **`main` of `Regula.LintMain`** stays in the trusted base, in one line.

**Removed**, because no consequence of this record or row of the specification relies on it: `OneSpelling`; `anonymous_not_closed`, `num_not_closed`, `uncovered`; `pure_eq`, `bind_eq`, `afterOp`, `interpret_ask`; `needed_not_loadRoot`, `BuildAnswered.mono`, `plain_refused_justified`, `full_refused_justified`; `modules_eq`, `buildRead_unique`, `lookup_of_mem_isSome`; `lakeCommands`, `LakeInvocation.commands`, `BuildProtocol.commands`; `ReadingLoad.prepend`; `writeInTree_leaves`; `argsOf_full`, `argsOf_one`; `names_toSpec`, `resolves_iff`; `refused_native` and `admitted_kinds`, which `Proofs/Owner.lean` replaces; and the field `LakeSelection.takesOne`, which no theorem read. The theorems of `Proofs/DomainCases.lean` were kept at that stage to settle the second reading of the domain. They are now removed with the domain statement under the [2026-11-01 confirmation](#what-no-false-refusal-means).

**Why it could arise.** The tables were written with the decision, and the specification imported them to state the decision. So the method's rule that a specification be independent of its code held of `languageRecord`'s predicates and not of the values they read. A check of what fails when a value changes would have shown it, and the analysis was the first. Each statement of an owner's example now holds its value.


### What selects what is audited

An analysis of Regula's past fixes that the owner asked for on 2026-11-01 observed a false pass: a project holding a project axiom and a `partial def` set `lintDriver = "regula/lint"` and `lintDriverArgs = ["standard-logical", "full", "<a clean project>"]`, and `lake lint` printed `regula: full verdict: pass`, with exit 0, naming neither project. The removal of the start test had reopened this, because that test's refusal was the only thing between the configuration's arguments and the full gate. The account the owner asks for: an unmodified Regula never reports a pass about something other than what the person running it asked about. On 2026-11-02 the owner narrowed it for the proof verdict to [the workspace in the current directory](#2026-11-02). Each row below is the agents' design, derived from that account, and no statement of the owner's.

| Consequence | Where | Status |
| --- | --- | --- |
| No argument names a project. A run takes one profile, and any other list of arguments is a refusal, with exit 2. | `run_other`, `RunMeets`, `profileOfRun` | Decided: a Lake configuration sets the arguments of `lake lint`, so this removes the route rather than guarding it, and a second executable in this package would not close it, since `lintDriver` can name any. |
| The variable `REGULA_FULL` names the project of the full gate, and it replaces the old `full DIR` form of the published run. | `run_subject`, `README.md` | Decided by the owner's delegated agent on the owner's behalf: `lakefile.toml` has no key that sets a variable, and the published run stays a start from the checker's own package on a named project. It reads nothing of where the checker lies, so it cannot refuse a `.lake` that is a link. |
| Whoever leaves `REGULA_FULL` set gets the full gate from `lake lint` too, on the directory it names, and the last line says which. | `run_subject`, `Report.labelOn` | Decided by the owner's delegated agent on the owner's behalf: a value of the variable is the request of the person who started the run. `lake lint` and `lake exe` start a program through one environment with nothing to tell them apart, so detecting a stale one would bring back a test of who started the run. A stale value is accepted risk: it takes the operator's own act and is visible on that line. |
| A pass ends its last line with what it audited: the directory named for the full verdict, and the current directory's real path for the proof verdict. Any other last line is unchanged. | `Report.labelOn`, `Verdict.proofLineOn`, `plainRun_pass` | Decided: at the end of the line, with LF and CR displayed as escapes, so a path changes neither the verdict's words nor the number of lines. |
| The local gate gives the variable to its one full-gate step and removes it from the others. | `localSteps_eq`, `localSteps_full`, `runStep_spawns`, `stepRequest`, `fullVariable_eq` | Decided: an inherited value must not turn a later `lake lint` of the gate into a verdict about another directory. |

## The form of this record

The file is not signed. Its authority is that of the commit that adds it. The owner's agents passed each answer to the author of this file on its date.