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

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

/-! # 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

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.

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 (other than origin-checked Init runtime primitives) is rejected with applicability execution-trusted-boundary.

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 non-native-runtime boundary of a checked surface has kernel-admitted correspondence.

It does not establish:

• Correctness of native-runtime primitives, the compiler or external code; a Lean equality does not prove external machine code. These stay trusted and reported.

• 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 and executionRule_injective; an accepted run satisfies RegulaPolicy.BoundaryOK. Extracting the execution closure from compiler IR is operational.