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

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, Regula.Checker.Policy.checked_executionFailures, executionRule_injective, RegulaPolicy.boundaryFailures_toolchain, RegulaPolicy.project_boundary_reported and RegulaPolicy.checked_toolchainBase; an accepted run satisfies RegulaPolicy.BoundaryOK. Extracting the execution closure from compiler IR and observing module origins are operational.