Checked example🔗

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
unsafe def identity (n : Nat) : Nat := n

identity (def) [unsafe] type=Nat → Nat axioms=[] -> kernel-only

  /-! # Identity
  
  Identity on natural numbers. -/
  /-- The identity function on natural numbers. -/
- unsafe def identity (n : Nat) : Nat := n
+ def identity (n : Nat) : Nat := n

/-! # Identity

Identity on natural numbers. -/
/-- The identity function on natural numbers. -/
def identity (n : Nat) : Nat := n

The correction keeps identity's domain and body and removes the unnecessary unsafe marker.

Checked by a fresh single-file audit of <example>/Fixture.lean (axiomGate --file, claim kernel-only, execution checked): violating run rejected, corrected run completed.

How to fix it🔗

1. Remove an unnecessary unsafe marker.

2. Replace partial def by a definition with structural recursion or a termination_by measure and decreasing_by proof; the finding names the partial def itself. A finding naming the ._unsafe_rec helper of a safe definition means the checker did not regenerate its base or check its recursion equation (standard §7.4 lists the unsupported forms, such as a wf_preprocess rule registered outside the Lean toolchain); restate its recursion without that form.

3. Deriving BEq, Hashable, Repr or Ord on a nested or mutual inductive (Ord on any recursive one) generates a partial def, reported under its generated name (such as instBEqT.beq); write that instance by structural recursion instead.

4. If the computation must stay unsafe or partial, move it to a separate, unclaimed dependency package; a claimed module cannot import an excluded module of its own package (RG2004). Where a claimed executable reaches it, it is reported as a trusted unsafe-computation or partial-computation boundary, which fails under checked execution (RG3002).

Why it matters🔗

A positive proof surface must consist of kernel-checked definitions. Unsafe and partial code can be executed, but it cannot serve as logical evidence, and reasoning about it silently depends on its runtime behavior.

What triggers it🔗

Authored unsafe and partial declarations are escape hatches: an unsafe declaration is checked only in Lean's unsafe mode, cannot be used by safe declarations or proofs and is not replayed as logical evidence, and a partial definition has no termination proof. They are rejected with applicability escape-hatch.

One exception is the range-less partial helper Lean generates for a safe, termination-checked recursive def (structural or well-founded recursion, a where or mutual definition, a recursive abbrev, or a derived DecidableEq, BEq, Hashable or Repr function on a recursive inductive that is neither nested nor mutual). It is admitted by exact match (standard §7.4): rerunning Lean's recursion compiler on the helper's recursion, with only the toolchain's own preprocessing rules and the checker's built-in syntax handlers, regenerates the observed base, up to compilation erasure, the base's axioms are within Standard-Logical, and Lean's kernel checks the recursion equation of each helper of the group: with the helper's value fun xs => body and every helper of the group replaced by its base f, the theorem ∀ xs, f xs = body, in the inspected environment, by a proof that uses no axiom outside Standard-Logical. The checker builds that statement from the helper's value and gives it to the kernel itself. A proof to try is taken from a constant named f.eq_def, whoever declared it, from the theorem Lean realizes for f or for the regenerated definition, or from reflexivity where the result is a proof, with every constant the search adds put back as its value; the kernel checks it against the checker's statement, and nothing else about it is consulted. The regeneration selects what is compared and no longer carries the claim about values: a base that the regeneration reproduces through matcher metadata or through below and brecOn declarations the audited module wrote is rejected where it does not satisfy the equation. Which code added the helper does not matter, and neither do declaration order, a nested proof shared with an earlier declaration, a proof written as a tactic block or as a term, or whether a public definition of a module file is exposed: the comparison uses no name of a theorem Lean abstracts from a nested proof. Nor, for the forms standard §7.4 lists, does it matter which definitions were irreducible where the definition was elaborated (attribute [local irreducible], attribute [irreducible] afterwards, unseal): the regeneration runs a second time with no definition irreducible (each given the status its declaration shows), and the comparison takes a match that passes a variable through as the match that uses it directly, where Lean's kernel checks that the two are equal for that matcher. Nor does the reducibility status matter that a function the definition calls had where it was compiled, where that differs from the status at the end of the audit, whatever module declares the function and whether a global attribute given afterwards or a local one made the difference (reducible, instance_reducible, implicit_reducible, semireducible or irreducible): where neither regeneration reproduces the base, the checker runs the two decisions Lean's recursion compilers take below default transparency (which parameters are fixed, and which toolchain wf_preprocess rule rewrites the body), records which definitions they ask about, and regenerates under the statuses that change them, first under the assignment the observed base selects by the parameters it keeps fixed and the mentions of a function it keeps. Where none of those reproduces the base, it regenerates under the statuses a global attribute can have replaced on the definitions of the helper's own module that the helper reaches. An assignment only selects which regeneration runs. The limitations below state what this leaves out. The regeneration and the comparison run with Lean's smart unfolding off, so no declaration named g._sunfold is read for the unfolding of g.

The separate constructor-index exception requires an owned safe inductive and safe base, the kernel-generated eliminator, exact constructor-index alternatives, and the closed getObjTagNat wrapper with matching types, levels and metadata. It retains unsafe and runtime-replacement boundaries with trusted execution correspondence.

A partial def is an opaque declaration that Lean runs through its generated helper. The finding names the partial def, at its source range, not the helper; this includes the partial def functions that deriving BEq, Hashable, Repr or Ord generates for a nested or mutual inductive (and deriving Ord for any recursive one).

A helper of a safe definition that the regeneration does not reproduce, or for whose recursion equation the checker finds no proof the kernel accepts, is reported under the helper's name (see the limitations below); its definition may be correct.

Required proof shape🔗

A total replacement keeps the same domain and result type; if it changes behavior, state and prove the relation to the intended function.

What a passing result establishes🔗

No authored unsafe or partial declaration is on the claimed surface. Every admitted recursion helper is Lean's compilation of a safe definition: its base, of the same module and type, is what Lean's own recursion compiler regenerates from the helper's recursion, up to compilation erasure, and is kernel-checked with Standard-Logical axioms. Lean's kernel has checked, with Standard-Logical axioms, that the base satisfies the recursion equation of each helper of the group, whatever matcher metadata, below and brecOn declarations, _sunfold declarations or reducibility statuses the audited module wrote. From that equation it is argued, not kernel-checked, that whenever the helper returns, it returns the base's value: by induction on the helper's evaluation, each recursive call that returns having returned the base's value.

Every admitted constructor-index wrapper has the recorded structural relation to its owned safe parent and base. This observation does not prove native correspondence.

It does not establish:

• That unsafe or partial code elsewhere is logically unsound; the rule concerns evidence, not a claim that such code is wrong.

• That a recursion helper terminates whenever the base does. Lean compiles the base from a body its wf_preprocess rules rewrote and the helper from the original, and Lean documents that a rewrite can remove a subterm the compiled code still evaluates or delay one under a binder; a toolchain rule can, through a reducible definition that ignores an argument. The helper's termination trusts that preprocessing, as every well-founded definition Lean accepts does.

• That the regeneration observation is truthful or that a helper's compiled code matches its value; these rest on the pinned Lean toolchain and on Regula's own unproved regeneration comparison. The claim about values does not rest on the regeneration: it rests on the kernel-checked recursion equation, on the compiled code running the helper's value, and on the argument from the equation to the values, for which there is no theorem.

• Termination proofs' adequacy for cost claims.

It leaves these review obligations open: R-QUALIFY, R-COST, R-INTENT.

Configuration and exceptions🔗

partial_fixpoint helpers are not covered by the recursive-helper exception.

Limitations and unsupported cases🔗

A helper is not admitted where the regeneration does not reproduce its base. The regeneration is given the helper's value and its base's termination argument, and it reruns Lean's structural and well-founded compilers in the environment the audit inspects (at the end of the audit), and there again with no definition irreducible, and in both under the reducibility assignments it searches, with Lean's default options and the toolchain's own rules, not with the options, rules and attributes in force where the definition was compiled. The forms known to fall outside are a partial_fixpoint definition, a base compiled through a fixpoint combinator other than WellFounded.fix and WellFounded.Nat.fix, a base whose compilation used a wf_preprocess rule registered outside the Lean toolchain, one elaborated with set_option wf.preprocess false or with a toolchain rule removed by attribute [-wf_preprocess] when a rule so disabled would have rewritten its body, or one whose compilation depended on a reducibility status the search does not find. Lean reads a status with its recording put aside while it reduces the discriminant of a match below default transparency; the search asks again in an environment where no definition unfolds for its status, so such a status is found, of whichever module and whatever it was. A wf_preprocess rule that applies only where several functions unfold together is found by following the first of them through the functions Lean then newly asks about. The argument of standard §7.4 leaves out a status Lean reads with no recording and outside a match (where it tests whether a type is a class, and where instance resolution meets a reducible head it did not unfold in a term with a metavariable), which only the statuses a global attribute can have replaced on the definitions of the helper's own module reach, and a rule that needs several functions of which none, unfolded, makes Lean ask about another once more than before. Neither was observed to reject a definition Lean accepts. Give such a function its reducibility where it is declared. Otherwise a definition for which the only difference is that ordinary (semireducible) definitions are irreducible at one of the two points (attribute [local irreducible], attribute [irreducible] after the definition, unseal), or that an abbrev is irreducible at the end of the audit, is admitted.

A helper for which the definitions whose reducibility status changes a decision of Lean's recursion compilers allow more than 63 assignments of another status is tried under the assignment its observed base selects and then under the first 63 single candidate changes only. One candidate change gives one definition another status and, where it was followed through the definitions it newly asks about or paired with another definition, those definitions theirs, so it can assign statuses to several definitions. If none reproduces its base the helper is undecided, neither admitted nor rejected: the checker stops with an error that names it, and the audit is incomplete, not a violation of this rule. A helper no attempt within the bound reproduces may still be what Lean generated, so a violation would assert what the checker has not established, and the helper is not admitted either way. Fixtures.Mutations.ReducibilitySearchBoundUnsafeRecForge shows the outcome for a forged helper; the helper Lean generated for a definition of that shape is admitted under the assignment its base selects. The statuses a global attribute can have replaced on the definitions of the helper's module that it reaches, tried after those, have the same bound: where they allow more than 63 assignments only the first 63 single changes are tried, and a helper none of them reproduces is undecided in the same way (Fixtures.Mutations.ReducibilityFallbackBoundUnsafeRecForge).

A change of a function's status that leaves the preprocessed body as it was is followed through the definitions it makes Lean's preprocessing newly ask about, without their unfolding: all of them at once, less the constants a toolchain rule's left-hand side mentions, each made reducible, then those with the status that unfolds least, and then all with those constants. It is then tried together with each other definition its run asked about in that way, one at a time. The first of those paths is followed to its end; beside it one change is followed through at most 64 runs of the preprocessing. Where those are used up with a change still not run, a helper nothing reproduces is undecided, the audit incomplete and not a violation, with an error that names which bound was reached.

A helper is not admitted where the checker finds no proof of its recursion equation that the kernel accepts. It looks for one only in a constant named f.eq_def, which Lean adds with a well-founded definition, in the theorem Lean realizes for a structural definition or for the regenerated one, and in reflexivity for a definition whose type is a proposition. Who declared a candidate is not checked, only that the kernel accepts it as a proof of the checker's statement. A well-founded definition and helper that a metaprogram adds with no theorem of that name are therefore rejected although the helper computes the base (fixtures_forged_measured_bare of Fixtures.Mutations.MeasuredMatchUnsafeRecForge); such a metaprogram adds f.eq_def too, copied from Lean's theorem or proved itself.

Editor feedback may be pending until the project command completes the relevant regeneration or constructor-index comparison.

Sources🔗

Normative clauses

standard §7.4 Inventory Every Owned Declaration

Checklist rows

COMP-02, THEOREM-05, THEOREM-01, DECL-03, BUILD-01

Detector, policy and proof sources

lean/RegulaPolicy/Decision.lean, lean/Regula/Collect.lean, lean/RegulaCore/Policy.lean

Proved linkage

The shared declaration decision RegulaPolicy.declarationFailure (its first failed requirement, declarationFailure_ordered) is mapped to a rule by the injective Regula.ruleForFailure. Project, file and documentation audits run it through Regula.Checker.Policy.checked_memberRule (ruleForMember_eq); the editor runs Regula.Linter.checked_editorDecision. For the same member and request, the editor passes exactly when the project decision selects no rule or only RG1008, which the editor does not render (Regula.Checker.Policy.editor_decision_none_iff), a rule it renders is the project decision's rule (editor_decision_rule), and a pending result withholds a project rule whose failure needs generated-role evidence (editor_decision_pending). The editor's request domain is the project's without teaching (editor_request_sound, editor_request_complete). The observed declaration fields and generated-role evidence are hypotheses of these theorems. RegulaPolicy.authorizedUnsafeRecHelpers_iff characterizes the admitted recursion helpers, authorizedUnsafeRecHelpers_base gives each a recorded observation (the regeneration together with the kernel-checked recursion equation) and a safe base with Standard-Logical axioms (neither proves the observation truthful), and Regula.Checker.Policy.partialParent_rule with subject_contract reports a partial def's helper under the partial def. authorizedConstructorIndexHelpers_iff characterizes the separate constructor relation, and Roles.safetyHelpers_iff binds both families to the same inventory.