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.

The executable roots include the action of each initialize block, named or anonymous, and of each [init] or [builtin_init] declaration of an owned module, as Lean's initializer attributes record it, whatever its name: Lean runs that action at startup or import, where no other root need reference it.

A comparison of a replacement with its reference is decided only by the kernel's answer. A comparison that the kernel stopped before it decided, or that raised an error before it recorded the kernel's answer, is unresolved.

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.

• That the executable roots are complete: the census of roots, the initializer actions among them, is read from Lean's records of each owned module, not proved.

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/RegulaPolicy/ExecutionWalk.lean, lean/RegulaPolicy/StackWalk.lean, lean/RegulaCore/Policy.lean, lean/Regula/Checker/RuleDiagnostics.lean

Proved linkage

RegulaPolicy.executionFailureRecords_empty_iff, RegulaPolicy.executionFindings_empty_iff, RegulaPolicy.unresolved_reported, Regula.Checker.Policy.checked_executionFailures and executionRule_injective. RegulaPolicy.ExecutionWalk.checked_walk decides the walk over the records of the probe: walk_sound and walk_complete. RegulaPolicy.DefeqComparison.ofAttempt_incomplete_iff and ofAttempt_error: a comparison is incomplete, and so unresolved, exactly when the kernel stopped before it decided or the attempt raised an error. Root discovery, the kernel's answer and reading each record from the environment and compiler IR are operational, and no theorem states that RegulaPolicy.ExecutionWalk.assemble builds the correct account from the visits.