# Working on Regula

This file holds every rule that binds a change to Regula, and the lessons of past defects, stated as rules. It is for anyone who changes Regula, a person or an agent, whoever they work for. [`README.md`](README.md#purpose-and-constraint) states Regula's purpose and the owner's constraint on all work, the [specification](specification/README.md) states each check and what is proved of it, and [the confirmation record](specification/confirmation.md) holds each decision of the owner's. Each rule is stated once: where another file states one, this file points to it.

## The owner's decisions

- Regula's repository holds everything that a mind working on Regula must remember: each decision of the owner's about Regula's purpose, contract, constraints and method, each rule that binds a change, and each lesson needed so as not to repeat a past defect. Record each once, in this file, the README, the specification or the confirmation record, and point to it from anywhere else ([the owner's decision of 2026-11-02](specification/confirmation.md#2026-11-02-where-regulas-memory-lives)).
- The owner states and confirms Regula's contract: its purpose, what it admits, what each verdict means, and the constraints on the work. The owner confirms a plain-word restatement of their intent, with examples and with what it leaves unsaid, and answers the forks that it does not settle. Each detail below that level is the contributors' design: record it with its reason, as decided on the owner's behalf, and never present it as the owner's.
- The confirmation record keeps one form for each decision: its date, what the owner was shown or asked, the owner's answer in the owner's words, its substance in the recorder's words, and its consequences, each marked as following from the owner's words or decided on the owner's behalf. The effect of a decision is stated where it governs work: in the README, the specification or this file.
- Record an intent as one coherent account in your own words, for a reader who saw none of the conversation, and quote only the owner's own answers. A specification, an issue or an instruction that narrows, widens or defers the owner's intent changes it: state the difference and its reason in the intent itself, or ask the owner, and never only document the omission.

## The specification first

- Revise the specification from the intent first, independently of the code, then the code. Change the specification, the proofs and the checker together when they encode the same claim. When the owner's intent is amended, re-derive each element it lists against the code, and when a definition gains a parameter or a case, re-derive each claim that uses it under the general form.
- State each value and example that the owner confirmed as a literal in the specification, over the decision that runs, never by reading the code's own tables. State what a Boolean helper means in other terms than its body, such as quantifiers, fields or equations over text. A specification written from the code shared the code's mistakes three times: a raw comparison of paths twice, and a search path taken as a project's identity once.
- Before building on a specification, prove that it is not vacuous: a subject meets it, each property can fail, it asks for progress, and a degenerate subject, such as one that refuses everything, passes everything or gives a constant, fails it. Re-derive a specification you receive, from an issue, a review or an earlier design, from the definitions it names before you build on it.
- Where another model makes a second formalization from the owner's words alone, compare it with the record and settle each difference: one below the owner's level is decided and recorded with its reason, and one at the owner's level goes to the owner. The confirmation record states each second reading and its differences.
- Prove the definitions that run against the specification. A theorem about a model written apart from the code verifies nothing about the code. A theorem about a call of Lean, Lake or the operating system states the request that the call makes, and what that system does with it is an entry of the list of assumptions.
- Prefer, in order: a type that makes an illegal state unrepresentable, a relation true by construction, an exhaustive check over a closed finite domain, a machine-checked proof, and a guard derived from the invariant. Enforce an invariant where state is admitted or written, not where it is read. Record which of these each invariant reaches, and why no higher one is available. Prefer a structural proof to an enumeration.
- Each claim is proved, measured, assumed or open, with the marks that [the specification](specification/README.md#how-to-read-this-document) defines. A measurement is an observation of the inputs it ran on. Run one only for a question that derivation cannot answer, and state why, the smallest run that answers it, its decision criterion and its budget before it runs. A measurement that infers an absence from a marker, such as a file that an initializer would write, records a positive control: a run in which the marker is known to fire. A planted library was recorded as not loaded because its marker stayed empty, while a library whose dependencies fail to bind aborts the process before any initializer runs.
- Add no test as evidence where a proof, a type or a construction settles the claim, and read a gap in tests as a missing invariant, contract or proof. A run that searches for a counterexample is a diagnostic: remove it afterwards, never keep it as a check, and close the whole class of what it finds. `.no-mistakes.yaml` declares this rule to the validation pipeline's agents.

## The trusted base

- Respect the list of assumptions, `Assumption` in `specification/RegulaSpecification/Assumptions.lean`, which `specification/README.md` describes under [the trusted base](specification/README.md#the-trusted-base), and change that list when a change changes it. Every behaviour of Lean, Lake or the operating system that a verdict relies on is an entry, with its pinned source, or is outside the contract, and the build fails for a new operation, route or premise until the list holds it. Lean, its kernel and Lake stay trusted, with a short list of behaviours of the operating system, each tied to the platforms on which it was observed ([the owner's decisions of 2026-11-02](specification/confirmation.md#2026-11-02-the-list-of-assumptions)).
- A change that adds an assumption about something the proofs do not cover gives it one disposition in its pull request: a proof that removes it; a search for a counterexample against the real system, with its budget of at most about an hour of machine time and its stop rule, the first counterexample, stated before it runs, and its result; or accepted risk, with its reason.
- Check each entry's words against each source it cites. The entry `processes` cited dyld(1) for a clause about the loader that dyld(1) contradicts, written from one measurement.
- For each way to run, list from Lake's and the operating system's source what the project controls on it: its files, its configuration, the directories on a search path, and the code that runs before or during it. A verdict's published meaning closes each, or names the assumption about the project that excludes it. The proof verdict's meaning was published with no such assumption while its start puts the project's library directory on the loader's search path.
- The claim holds only for [the named configurations](specification/README.md#the-named-configurations). Anything else is outside the contract, said so in public text, and not a defect.
- A platform joins the named configurations only once each entry that depends on the platform was observed to hold there, by the procedure of its observation on the platforms already named, with the procedure, date and result recorded, as [Ubuntu](specification/README.md#ubuntu) records them. Where a platform's behaviour differs, as the loader's does, the entry states each platform's form and cites each platform's page. An entry about the operating system cites, beside each page of a platform's manual, the lines of Lean's runtime at the pinned tag that make that call: an entry once cited `posix_spawn(2)`, which Lean's runtime does not call.
- An independent audit of Regula runs only once the claim has stopped moving, and starts by checking that the list of assumptions is complete and that each entry holds on the named configurations.

## Reading Lean, Lake and the operating system

- Read another system's behaviour from its source at the pinned version, the tag `v4.35.0` of Lean with Lake below `src/lake/`, never from its documentation, a summary or memory, and cite the lines. Follow each call to the code that decides what the claim says, into the other component when it crosses one: the entry for `lake check` said that it exports the default targets, and Lean's exporter, which it calls, leaves out each constant whose name Lean marks as internal. Re-read at that version each claim about Lean or Lake in text carried from another project. A fact about another system that a proof needs is a hypothesis, a parameter or a proof-bearing field, never an axiom.
- Narrow a claim about the outside world to a closed domain, and refuse the rest truthfully. Regula's reliances on the outside world were found one case at a time until each claim was narrowed so.
- When a value from Lean, Lake or the operating system is read as naming a subject, such as a workspace or a project, list from that system's source every setting that reaches the value, and attack the design with a subject that sets each of them to another subject's value. One refused example is no evidence of identity. Compare paths by what the operating system answers for them, never as raw text.
- When a rule reads a subject by a flag or a kind, find the key by which the owning system selects the subject, such as a name or a path, and state the rule over that key. Attack it with a member that has the key and lacks the flag, and with a forger that meets the exception, as RG1006's recursion helpers needed.
- Give each subject that a rule quantifies over a coverage condition: each claimed subject is found, or the check fails. State what each key used to compare or deduplicate encodes, and prove it injective from the owning system's rules. When Lean merges constants of one name, prove the rule's property for each claimed module's own constant and metadata in `pass_held` as well as for the merged environment in `EnvFloor`; equality of the kept proof or its erasure does not establish coverage of module-local attributes. RG1011's first loader contract missed those attributes by treating a merged theorem's name as its complete identity.
- For each parameter of a check that a caller or a project can set, such as an argument, a configuration field or a variable, find the value that makes the decided property false, then prove the property for every value or fix the parameter. A project's `lintDriverArgs` once chose what the full gate audited.
- Before stating a predicate over a list of Lake's configuration, read the order in which Lake merges it. Before treating an attribute as evidence, read the code that admits its registration. Treat a moved pin of a dependency as a changed form, and search for the old hash and for each feature gained or lost.
- A change that moves a check onto another way of obtaining its input re-derives, from the owning system's source, what each query reads under the new way. Before a specification that hands a rule to an external tool goes to the owner, run that tool once on the first project the specification applies to, and record the result as a measurement. Measure a verdict's route, with its memory and time, on a project of each kind that the contract admits, one that imports Mathlib among them, and state whether its cost grows with the claim or with everything the build imports: `lake check` replays the whole imported environment, and a proof verdict on a project that imports Mathlib did not finish on the named platform.

## Guards, refusals and fixes

- Follow the rule "Removal comes first" under [Purpose and constraint](README.md#purpose-and-constraint) in the README. A fix that adds a check, a reader or a mode is new surface that needs its own proof, and later audits faulted fixes of that kind: an extra read-back, a scanner of premises, and the removal of a guard that also stopped another route.
- A rule earns enforcement in code only when breaking it would be serious or hard to undo, such as a false verdict, an unauthorized write or a crossed trust boundary. A rule whose breach is cheap and easy to undo stays written and is listed as accepted risk. A new guard is a decision of the specification: give it its theorem, or leave the rule written and name the risk. Accepting a serious or hard-to-undo risk trades quality for cost, and that is the owner's decision.
- Define a guarded boundary by its class, every way to exit, every rejection and every operation that can fail, found through the owning system, and for a wrapper through each call into it, never by a list of the members you remember. Before building a design, try to break it: construct the input or configuration that it admits and the intent forbids, and the one that it refuses and the intent needs.
- A guard that must discover what it guards gets, before any code, a table of every input it discovers and how each is read. Attack that table with a rewrap, a comment, the guarded thing inside existing code, and the guarded thing under another configuration or platform.
- Before removing a guard or a refusal, wholly or for some inputs, derive what it refused from every route that reaches the guarded point, found through the owning system: each caller, each configuration field and each command. State in the pull request what now happens on each route: another contract refuses it, the published contract puts it outside and says what follows, or the same change fixes it. When a start test was removed for a real false refusal, a project's `lintDriverArgs` reached the full gate and gave exit 0 about another directory.
- An argument that two outputs are equal lists every input of what produces them, the producing program's own code included. Attack a bound on a sum with members that each fit and together do not, and a value spliced into a command or into another language's text with spaces, quotes and newlines. Attack a resource handed to a child process, such as a variable or a descriptor, with its own nesting and with each mechanism that shares its state. A write of several steps into a place that a reader trusts by name makes an object appear under its final name only once it is complete.
- A change that gives an identifier, a variable or an inherited environment a new meaning, or removes something its consumers inherit, first finds every reader of it by a search for its name, and covers each. A design that relies on an identifier staying unchanged names the mechanism that keeps it so, and treats a mutable one as no identifier.
- Retire a check only after accounting for what it established and landing what replaces it.

## Defects and review

- A defect is fixed only when three things are: its instance, its whole class, and the link that let the class arise undetected. Name the class by the property every member violates, find every site with one criterion over each function's whole domain, and close the class with the contract that makes it impossible: a type, a construction, a proof, or a check that fails on a new instance. Then trace why it arose, from the owner's intent through the specification, the design, the code and the checks to the author's instructions and tools, up to a link that a change can correct, and correct that link in the same change when it is in this repository. The cost rule of the previous section bounds the class, and the section "Root cause" of the pull request template asks for each part.
- A review finding blocks only when its failure would be serious or hard to undo, or when it has been observed: it happened, or a run of the code reproduced it. Every other finding is accepted risk, named in the pull request. A valid finding is a defect of the author's own process: close its class and correct its link. After the third review pass of a step, triage what remains under the cost rule.
- File a bug only when it passes the cost rule, and state what is wanted by the harm it prevents and the paths in scope, never as an absolute over an open domain. End each bug issue, and each issue that reports a failure, with a section `Retrospective`: the property that failed, the contract that should have made it impossible, the assumption that stood in for that contract, and the root cause with the change it needs; then the class, the external system if any, how it was found, and the earlier issue it repeats.
- Label each issue `bug`, `enhancement` or `documentation`, or with the repository's own category label where one fits better. `question` is not a category.
- An issue, a review or an instruction that asks for a change states the property that the change must establish, and defines each class by the criterion its members meet, with any list marked as examples. It names a mechanism only after attacking it.

## Text

- Keep documentation, docstrings, diagnostics and checker output no stronger than the exact Lean property established, and a name no stronger than its definition. Before review, check each new or invalidated sentence that cites a theorem or check against its actual statement, hypotheses, and caller; name what it leaves uncovered. When a check moves between phases, re-derive each description of the phases and their results, including Boolean parameters and success conditions. No text claims that Regula is free of bugs. Prose claimed more than the proofs three times.
- Describe a check, a theorem or a measurement by what it does, read from it, never from its name or a summary, and say whether it exists or is planned. Re-derive a sentence that counts rows, or that says a document states nothing about something, from the whole set after the last edit. A record that inventories code names each item by its path and declaration at a stated commit, never by a paraphrase of its name.
- A change that makes a statement false corrects it, wherever it is. After moving a path, changing a command, renaming or removing a declaration or changing a module's imports, search the whole repository for the old form, with a fixed-string whole-word search for each rule identifier, such as `git grep -n -F -w RG1006`. Correct every restatement of a corrected claim, found by searching for its conclusion. When the checker's output changes, search each text that describes it by the output's own words. When a method or a division of responsibility changes, search what the checker prints by the old method's words. After a merge of `main`, re-read the sentences that the branch adds against what `main` changed.
- Treat the installation source, dependency manifest, command sequence and verdict claim as one contract. Instructions for an unreleased change use the checkout containing those instructions; released instructions stay with their release. Before changing that binding to a release pin, establish that the selected revision implements the stated commands and claim, for both verdicts. A run against a path dependency establishes nothing about a separately pinned release: the cone-replay change removed `lake check` while its install instructions still selected a checker that did no replay.
- Rewording text that describes code keeps each kept passage a word-for-word subset of its original sentences, plus a stated list of substitutions, checked mechanically. Read each reworded sentence beside its original for a lost "when", "if", "only", "can", "may", binder or projected subject (such as path components versus a whole path, or examples of a closed table versus its boundary). Rewriting comments to read better made eleven of them claim more than their code.
- Public text is plain and states no superlative about Regula, not even as an aim, and its comparison with seL4 is the aim of a claim that is exact and proved. The owner's delegated agent decided this on the owner's behalf on 2026-11-02, as [the record of 2026-11-01](specification/confirmation.md#2026-11-01) says.
- `README.md` is for software engineers, both users and potential contributors, who use Lean 4 as a theorem prover and as a functional programming language and want their coding agents to write well-factored, well-designed, best-practice Lean 4 code formally proven to be free of bugs, with Regula as the linter that gives those agents feedback. Keep it concise and scannable so a reader can quickly tell whether Regula fits their work: lead with the problem Regula solves for that reader and their agent, state what Regula is second, distinguish the proved foundation shipped today from planned standards, fix guidance and rules, and keep every claim exact ([the owner's decisions of 2026-11-01](specification/confirmation.md#the-readmes-reader) and [2026-11-03](specification/confirmation.md#2026-11-03-regulas-direction-and-the-readme)).
- Public text names no private repository, tool, path, agent or personal background of any contributor, states analogies shared to orient an agent in general software-engineering and Lean 4 terms unless asked to name them, and describes a private tool or agent generically where it matters.
- A Lean file has no copyright or licence header, because `LICENSE` is the repository's one copyright and licence notice. A file started as a copy of another can carry an old header back ([the owner's decision of 2026-11-02](specification/confirmation.md#2026-11-02-the-copyright-notice)).
- Code documents itself through the names of its constructs and how they are composed. A comment is a claim that nothing checks, so it 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. A doc comment that `linter.missingDocs` requires stays, cut to the shortest true sentence ([the owner's decisions of 2026-11-02](specification/confirmation.md#2026-11-02-comments)).
- Write the specification package's doc comments in Verso, under Lean's option `doc.verso`, with the role that Lean checks, such as `{name}`, for each mention that Lean can resolve where the comment stands, so that renaming or removing what such a mention names fails the build. Keep the root package's doc comments in Markdown: RG1010 refuses `doc.verso`, which the table `options` of `lean/Regula/LanguageSet.lean` does not hold, and a code block in a Verso doc comment runs during the build (the same decisions).
- Write each GitHub issue, pull-request description and comment with one line for each paragraph and each list item.

## Lean

- State the exact elaborated theorem, quantifiers, assumptions, and transitive dependencies. Do not strengthen a Lean result into a claim about an unrelated implementation.
- Ban `sorryAx`, project logical `axiom` declarations, `sorry`, and `admit` from every proof surface. Express assumptions as parameters, hypotheses, or proof-bearing fields.
- Report exact foundation strength: Kernel-only is empty; Choice-Free permits only `propext` and `Quot.sound`; Standard-Logical also permits `Classical.choice`. Do not treat these as general software-assurance rankings.
- Distinguish logical and executable decidability, noncomputability, kernel reduction, native evaluation, `partial`, `unsafe`, runtime replacement, `extern`, and FFI wherever the distinction affects a Lean claim.
- Discover modules, declarations, and dependencies through Lean/Lake semantics, not fixed file lists or source-format regexes. Unknowns and omissions fail the affected claim. Never read a programming language's source with a reader written by hand, and never take a search that finds nothing as proof that something is absent.
- Account for machine arithmetic, serialization and the order of evaluation where a claim depends on them. Lean evaluates a call's arguments before the call, so a bound on an effect follows from that order, never from where a guard stands in the source. Distinguish a check over bounded inputs from a guarantee over all of them.

## Implementation language

- Project-owned code is Lean 4, with explicit behavioral contracts proved about the actual definitions used by callers. A translation into Lean or a successful build alone does not establish behavioral correctness.
- Do not add Python, shell or other implementation-language programs. Any shell script requires explicit operator approval.
- Use Lean/Lake APIs where available. Distinguish pure proved behavior from trusted compiler/runtime, filesystem, and process effects.
- Before writing an algorithm or a procedure, look for one in Regula, then in Lean's and Lake's own code, then in published work, and reuse it unless a stated reason, such as trust, fit or the constraint's "no frameworks", rules it out. Say in the pull request what was searched and what was decided.

## Adding a rule

A rule is a pair of modules and one line in each package's registry, so that adding or fixing a rule does not break another rule ([the owner's aim](specification/confirmation.md#2026-11-03-the-aim-of-a-module-for-each-rule)), and a pair because the checker's package cannot depend on lean-intent while each rule's formal statement is a lean-intent record ([the decision of 2026-11-03](specification/confirmation.md#2026-11-03-each-rule-a-module-of-its-own)). [The shape of a rule](specification/README.md#the-shape-of-a-rule) states what each part is.

1. Its check: `lean/Regula/Rules/RGnnnn.lean`, a `module` file that imports `Regula.Rule` and no other rule, defines each table that only this rule reads, and gives `rule : Regula.Closed.Rule`, its spelling and its check. `rule` is `@[expose]` so that the registry reads its spelling, and the check stays unexposed.
2. Its line in `Regula.Closed.registry`, in `lean/Regula/Rules.lean`, at the place its findings take in the output. `Regula.Closed.spellings_nodup` refuses a spelling that another rule, RG1010 or RG2001 has. Take a code that no check of any release has had, found with `git log -S`: releases before `v0.12.0` gave RG1007 to RG1009 and other codes to checks that no longer exist, and a code reused would name two checks.
3. Its statement and proofs: `specification/RegulaSpecification/Rules/RGnnnn.lean`, which imports `RegulaSpecification.Rule`, the rule's own check, and no other rule. It holds the violation predicate, written from the owner's intent first and in other terms than the check ([the specification first](#the-specification-first)), the intent record by `ruleRecord`, the cases (`Witnessed`) with `adequate` and `noisy_fails`, `rgN_exact`, which proves that the check reports exactly the violations, and the rule's value of `Proved`.
4. Its line in `registry`, in `specification/RegulaSpecification/Rules.lean`, at the same place. `registry_rules` refuses two registries that differ.

A table that another rule also reads goes in a core, `Regula.Rule` or `RegulaSpecification.Rule` and `RegulaSpecification.Foundation`, never in a rule's module. A rule that needs a field of the build that the closed input does not carry extends `Regula.Closed.Decl`, the loader and the specification's `Input`, which every rule reads, so its pull request says so. A rule also changes what a pass means: `allHold_iff` in `specification/RegulaSpecification/Proofs/Load.lean` stops the build until `EnvFloor` and `allHold_env` state the rule in the terms of Lean's environment, with the loader's `fitsUnshown` when the rule must hold of a constant that Lean's import replaced. Change the published text with them: the README's table of the checks and what a pass means, and the specification's section on the rule and its rows of what the owner's intent requires.

No line of `lakefile.toml` or of `RegulaSpecification.lean` names a rule's module. The library `RegulaChecker` has the root `Regula.Rules`, and the specification's library has its own name as its root, so Lake builds each module below them that an import reaches. For a change confined to one rule's pair, Lake then rebuilds only that pair, the registries and what lies downstream of them. The gate still runs every check from a clean build, and stays so by [the owner's decision of 2026-11-03](specification/confirmation.md#2026-11-03-the-local-gate).

## Changes, the gate and delivery

No package of this repository requires Mathlib. `lake build` builds the default targets, and `lake build Regula` the library that no default target imports. The specification is a package of its own: `lake build` in `specification/`, from a shell whose working directory is that directory.

The merge gate is the local gate, `lean --run lean/Regula/DiagnosticsGate.lean local`. Its steps are `localSteps` in that file. It needs the pinned toolchain and a read of lean-intent from GitHub. The no-mistakes validation pipeline runs it as its Test step on each commit that it validates, as `.no-mistakes.yaml` configures. The repository has no CI workflow. Merge requires a pass of the local gate on the reviewed head and applicable focused review. Preserve PR, signature, history, and conversation protections. Finish authorized publication, exact-head merge, and owned branch cleanup.

The pipeline reads `.no-mistakes.yaml` and the PR template from the default branch, so the paths they name, `lean/Regula/DiagnosticsGate.lean` and `lean/Regula/TestListing.lean`, move only in two steps: first a change that keeps both paths working, then one that uses the new path.

- Every delivery PR requires independent review by at least one fresh-context reviewer. Scope reading and checks to the changed claims; use distinct reviewers for materially different semantic and implementation risks.
- After repair, obtain focused independent verification of the affected claims. Reuse evidence whose relevant inputs and claims remain unchanged; rerun only invalidated checks.
- When working an issue, its acceptance criteria define the deliverable. A planning issue or an agent's review response alone is not a completed delivery.
- Complete authorized implementation, local repairs, checks, and targeted review without repeatedly requesting permission. Use existing session authorization for external actions; requiring a PR does not itself grant permission to publish, merge, or change visibility.
- Mark an issue Done only after its acceptance criteria and required review/checks pass and its completing PR is integrated. A partial PR references the issue without closing it.
- A head merges only when it contains the current tip of `main` and the gate passed on it: two stale heads broke `main` on 2026-10-29. Work that changes the gate or the pipeline runs its evidence in the checkout the gate itself uses, since a fresh clone is not one: the gate of pull request 492 passed every fresh clone and refused every change in its first real run. Work that removes a merge gate first lists each property that it enforced and what carries each afterwards.
- Each change reaches `main` as one squash merge whose commit is the pull request's title and body. Title it as a Conventional Commits header, `type(scope)!: summary`, with type `feat`, `fix`, `docs`, `refactor`, `perf`, `test`, `build`, `ci`, `chore` or `revert`, and mark a breaking change with `!` and a `BREAKING CHANGE:` footer. The types set the next version under Semantic Versioning, tagged `v<version>`: `fix` a patch, `feat` a minor, a breaking change a major, or a minor before 1.0. A change that adds only theorems or text over unchanged code is not a `feat`. Give each issue that a pull request resolves its own closing keyword, as in `Closes #1.` then `Closes #2.`. No commit names an agent as a co-author.
- The pull request's description follows `.github/pull_request_template.md`. It also lists the observations of another system that the change adds or alters, and, for a removed guard or a fixed defect, what the sections above ask for.
- A feature that logs and ignores its own errors reports at least one observed success of its main path before it is called done.
- Report the tested Lean version, the Lake modules and declaration/axiom coverage, applicable diagnostics, and failures or missing evidence.