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 termination_by structural on a later argument); restate its recursion.

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.

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: a structural recursion on an argument other than the first one Lean's automatic choice accepts (selectable by termination_by structural), 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, or 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.

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 regenerated, safe base with Standard-Logical axioms, and Regula.Checker.Policy.partialParent_rule with subject_contract reports a partial def's helper under the partial def.