Checked example🔗

/-! # Identity

The identity specification is replaced with extensionally equal code. -/
/-- The replacement code for `identity`: it computes `0 + n`. -/
def alternative (n : Nat) : Nat := 0 + n
/-- The identity on natural numbers; compiled code runs `alternative` instead. -/
@[implemented_by alternative] def identity (n : Nat) : Nat := n
/-- Spells `n` through the toolchain's `Nat.repr`. -/
def spell (n : Nat) := toString n

identity reaches identity (runtime-replacement)

  /-! # Identity
  
- The identity specification is replaced with extensionally equal code. -/
- /-- The replacement code for `identity`: it computes `0 + n`. -/
- def alternative (n : Nat) : Nat := 0 + n
- /-- The identity on natural numbers; compiled code runs `alternative` instead. -/
- @[implemented_by alternative] def identity (n : Nat) : Nat := n
+ The identity specification and replacement agree on every input. -/
+ /-- The replacement code for `identity`: it computes `0 + n`. -/
+ def alternative (n : Nat) : Nat := 0 + n
+ /-- The identity on natural numbers; compiled code runs `alternative` instead. -/
+ @[implemented_by alternative] def identity (n : Nat) : Nat := n
+ theorem correspondence (n : Nat) : identity n = alternative n := (Nat.zero_add n).symm
  /-- Spells `n` through the toolchain's `Nat.repr`. -/
  def spell (n : Nat) := toString n

/-! # Identity

The identity specification and replacement agree on every input. -/
/-- The replacement code for `identity`: it computes `0 + n`. -/
def alternative (n : Nat) : Nat := 0 + n
/-- The identity on natural numbers; compiled code runs `alternative` instead. -/
@[implemented_by alternative] def identity (n : Nat) : Nat := n
theorem correspondence (n : Nat) : identity n = alternative n := (Nat.zero_add n).symm
/-- Spells `n` through the toolchain's `Nat.repr`. -/
def spell (n : Nat) := toString n

The correction adds the missing equality between the reference and its replacement on the full natural-number domain, keeping the checked execution claim and both implementations. In both, spell runs Nat.repr, whose replacement is the Lean toolchain's own: it passes as the toolchain's trusted base, reported once.

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. State and prove theorem f_eq (x) : f x = g x (either direction, any prefix of the domain with congruence) for the full domain, including implicit and instance arguments.

2. Replace implemented_by with a proof-backed @[csimp] equality where it fits.

3. If an external boundary is intended (an extern implementation, or unsafe or partial code in an unclaimed dependency), claim report execution, where it is reported as trusted and not failed. An owned unsafe or partial declaration on a claimed surface still fails RG1006 in either mode.

Why it matters🔗

@[implemented_by g] def f makes the kernel reason about f while compiled code runs g. Without a proof relating them, theorems about f say nothing about the program's behavior.

What triggers it🔗

Each reached boundary gets a kind and a correspondence state. Under checked execution, a boundary that is trusted rather than checked is rejected with applicability execution-trusted-boundary in every root that reaches it, unless the boundary itself carries an admitted toolchain origin. Only a replacement, extern, or unsafe or partial computation can: a csimp simplification or a compiler-trusting proof axiom never does, even on a constant declared in Init.

The toolchain owns a replacement, extern, or unsafe or partial computation declared in one of its own Init, Std or Lean modules, decided by where Lean loaded that module from (the pinned toolchain's library, an observation of the probe), not by its name. Such a boundary is the toolchain's trusted base: it passes and is reported once for the whole audit, with every environment and root that reaches it, in the audit's toolchain trusted base.

A partial implementation that a trusted boundary names as the code run in its place is reported with that boundary where both are trusted and neither is the toolchain's, as one finding that names both and one counted boundary. A partial implementation is a constant of partial definition safety: the implementation a metaprogram such as Mathlib's compile_inductive% adds for a recursor, named as the target of a csimp candidate or of an implemented_by replacement, or the _unsafe_rec helper Lean generates for a partial def, named by that partial def's own boundary. A partial def named as the target of a candidate or replacement is not one: it is an opaque constant compiled through that helper, so it keeps its own finding and count, and only its helper is reported with it. A second record of one trusted boundary (the same constant, kind, replacement and toolchain origin, as two constants of one equality's type give a csimp candidate) is reported and counted with the first in the same way. The account in --json-out keeps every record, and --verbose lists the implementation under its boundary as its implementation and a later record as restated.

A correspondence is checked only when a closed proof of ∀ xs, f xs = g xs over the reference's complete elaborated domain passes kernel admission, with only standard logical axioms and no extra premises.

Required proof shape🔗

∀ xs, f.{us} xs = g.{us} xs over the reference's complete dependent domain, closed, with no additional hypotheses, admitted by the kernel. An actual domain hypothesis is legitimate; an extra premise such as False is not.

What a passing result establishes🔗

Every reached boundary of a checked surface without an admitted toolchain origin has kernel-admitted correspondence; each one without it has a failure record in every root whose account contains it (RegulaPolicy.project_boundary_reported).

Every such failure record is reported: as its boundary's own finding, or, for a partial implementation reported with the boundary that runs it, in that boundary's finding, which names it, or, for a later record of a trusted boundary, in the finding that reports the first record (RegulaPolicy.failure_reported). Every finding is a record (RegulaPolicy.executionFindings_sound), and the findings are empty exactly when the records are (RegulaPolicy.executionFindings_empty_iff).

Each toolchain-owned boundary of every environment an audit inspects is in exactly one entry of the audit's toolchain trusted base, which lists exactly the environments and roots that reach it (RegulaPolicy.checked_toolchainBase).

It does not establish:

• Correctness of the toolchain's own replacements, unsafe code and native primitives, the compiler or external code; a Lean equality does not prove external machine code. These stay trusted and reported.

• Anything about code the program selects at runtime rather than references: a constant it evaluates by name (Lean.Environment.evalConst, Lean.Meta.reduceBoolNative), a dynamic library or plugin it loads, or a process it spawns. The account is the static closure; such code is data to it, and the toolchain primitive that runs it is trusted base. The initialize and [init] actions of imported modules, static or at runtime, are likewise outside the account.

• That the executable roots are the ones the project intends to cover (R-INVARIANT).

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

Configuration and exceptions🔗

execution in the surface manifest (report or checked), or --execution checked for a single-file audit, selects the mode. report mode reports trusted boundaries without failing them; it is not a fix for a checked claim.

Limitations and unsupported cases🔗

Proof search is deliberately incomplete: a candidate whose remaining premises cannot be instantiated supplies no evidence, and the boundary stays trusted.

Sources🔗

Normative clauses

standard §7.6 Classify Lean Computation Mechanisms Exactly

Checklist rows

COMP-03, COMP-04, SCOPE-03, SCOPE-05, THEOREM-05, BUILD-01, BUILD-03

Detector, policy and proof sources

lean/Regula/Probe.lean, lean/RegulaCore/Policy.lean, website/RegulaStandard/ToolingAndMachineAudit.lean

Proved linkage

RegulaPolicy.executionFailureRecords_empty_iff, RegulaPolicy.executionFindings_empty_iff, Regula.Checker.Policy.checked_executionFailures, executionRule_injective, RegulaPolicy.boundaryFailures_toolchain, RegulaPolicy.project_boundary_reported, RegulaPolicy.failure_reported, RegulaPolicy.executionFindings_sound and RegulaPolicy.checked_toolchainBase; an accepted run satisfies RegulaPolicy.BoundaryOK. Extracting the execution closure from compiler IR and observing module origins are operational.