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.

A theorem that supplies such a proof counts only from a module whose declarations the audit replayed through Lean's kernel (the root package's, or a path dependency's in its Git work tree) or from an origin-checked toolchain module. A theorem of a dependency the audit does not own supplies no evidence: only that dependency's build vouches for it.

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 modules that the project imports but does not own, static or at runtime, are likewise not roots of their own: the account covers only those that an existing root reaches, through the constant that the action initializes. Those of owned modules are executable roots (RG3001).

• 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/RegulaPolicy/ExecutionWalk.lean, lean/RegulaPolicy/StackWalk.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. RegulaPolicy.DefeqComparison.ofAttempt_checked_iff and ofAttempt_negative_iff: a definitional comparison is checked exactly when the attempt recorded the kernel's admission of the proof with Standard-Logical axioms, and trusted exactly when it recorded the kernel's refusal or an admission with a different axiom; an error while it records the answer, also after an admission, leaves it unresolved. RegulaPolicy.ExecutionWalk.checked_walk decides the walk over the records of the probe. Root discovery, the kernel's answer, reading each record from compiler IR and observing module origins are operational, and no theorem states that RegulaPolicy.ExecutionWalk.assemble builds the correct account from the visits.