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 (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.

The only 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, and the base's axioms are within Standard-Logical. 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 a global reducibility attribute given after the definition (attribute [reducible], [instance_reducible], [implicit_reducible], or [irreducible] after one of those) matter when it is given to a function of the helper's own module that is not an abbrev, the change is one the search covers (from a status on which Lean's validation admits that attribute, or from reducible to irreducible), and the definitions the helper reaches allow at most 63 assignments of an earlier status: where neither regeneration reproduces the base, the checker searches the statuses such an attribute can have replaced, for the definitions of the helper's module that the helper reaches, and an assignment only selects which regeneration runs. The limitations below list the forms outside this. 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.

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 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 generated 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; whenever the helper returns, it returns the base's value.

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 the 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.

• 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 that calls a function whose status where the definition was compiled the search does not try, where that changes which parameters Lean finds fixed or which wf_preprocess rule of the toolchain applies: a status that holds only where the definition is compiled (attribute [local reducible] or a reducible function made semireducible afterwards, under set_option allowUnsafeReducibility true; attribute [local instance_reducible] or [local implicit_reducible]), an abbrev that is not reducible where the definition is compiled, a function of another module whose status changes afterwards, or a change Lean's validation does not admit, such as reducible given to an instance_reducible function (all under that option). These are limits of this release, which issue #196 keeps open (Fixtures.Mutations.KnownLimitReducibleWhereCompiled). 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 whose reached definitions allow more than 63 assignments of an earlier reducibility status is searched over the first 63 single changes only, each giving one definition one earlier status. 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. A forged helper over the bound ends the same way. Fixtures.Mutations.KnownLimitReducibilitySearchBound shows the outcome for a helper Lean generated. The bound of 63 is a limit of this release, which issue #196 keeps open.

Editor feedback may be pending until the project command completes the regeneration.

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 (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 regeneration observation 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.