Checked example🔗

import Lean
/-! # Identity

Identity and its extensionally equal replacement. -/
/-- 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
run_cmd pure ()

identity: identity: replacement history unavailable: FAIL: unsupported replacement-history evaluators: #[command: Lean.Elab.Command.elabRunCmd (Lean.runCmd)]

  ⋯ 6 unchanged lines
  /-- 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
- run_cmd pure ()

import Lean
/-! # Identity

Identity and its extensionally equal replacement. -/
/-- 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

The correction removes a no-effect run_cmd metaprogramming command that prevents history authentication; the reference, replacement and correspondence theorem are unchanged.

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

How to fix it🔗

1. Remove metaprogramming commands from modules whose implemented_by history must be authenticated, or move them elsewhere.

2. Ensure every dependency's compiled code is available in the build.

3. Break cycles consisting only of replacement edges.

Why it matters🔗

An execution account that silently skipped an unresolved path would overstate what the compiled program is known to run.

What triggers it🔗

For every owned executable root the checker follows retained compiler edges, logical value dependencies, csimp candidates, observed implemented_by choices and partial helpers. Anything it cannot resolve or classify is reported with applicability execution-unresolved and impact incomplete, in both report and checked execution modes.

Replacement history is reconstructed by fresh re-elaboration; metaprogramming commands such as run_cmd, run_elab or module-local elaborators make it unavailable.

A path through the Lean toolchain's own origin-checked Init, Std or Lean modules does not need that history: a toolchain replacement is followed through the current target its compiled module records, as part of the toolchain's trusted base, so no toolchain replacement is reported as unresolved for missing history.

What a passing result establishes🔗

Every path in each owned executable root's conservative closure was resolved and classified; an unresolved path is incomplete and never accepted.

It does not establish:

• That the conservative closure is the program's actual runtime call graph: candidates and historical choices overapproximate it, and a safe program can be rejected.

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

Configuration and exceptions🔗

No execution mode waives an unresolved path.

Limitations and unsupported cases🔗

This page's example is a diagnostic demonstration: the violating run is INCOMPLETE by design and is not accepted negative evidence. Its corrected counterpart passed a completed positive check.

The editor does not analyze execution: it reports neither this rule nor a pending notice for it. Only lake lint, axiomGate (including --file) and the build-lint policy target do.

Sources🔗

Normative clauses

standard §7.6 Classify Lean Computation Mechanisms Exactly

Checklist rows

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

Detector, policy and proof sources

lean/Regula/Probe.lean, lean/RegulaCore/Policy.lean, lean/Regula/Checker/RuleDiagnostics.lean

Proved linkage

RegulaPolicy.executionFailureRecords_empty_iff, Regula.Checker.Policy.checked_executionFailures and executionRule_injective. Extracting the execution closure from compiler IR is operational.