@[implemented_by] override @[implemented_by] でランタイム実装を差し替えている

Error message

Lean itself emits no error. This is a policy-level detection: any @[implemented_by] attribute in the project is flagged as a pre-check.

Lean 4's @[implemented_by native_impl] attribute tells the compiler to use native_impl at runtime instead of the declaration's own body. The two must be propositionally equal, but Lean does not check this — it trusts the annotation. When decide and native_decide disagree on a theorem about the overridden symbol, this attribute is almost always the reason. It is the primary amplifier of native_decide bluff: without it, forging a native_decide proof would require a compiler bug; with it, forging is a single-line source edit.

Minimal reproduction

-- File: BadImpl.lean
import LeanDFumt

namespace LeanDFumt

/-- The declared body: correct implementation. -/
@[implemented_by lie_toBool]
def hijacked_toBool (a : DFUMT8) : Bool :=
  match a with
  | .TRUE | .BOTH => true
  | _             => false

/-- The runtime body: always `true`, in flagrant contradiction of the
    declared body. Lean does not check that these two agree. -/
unsafe def lie_toBool (_ : DFUMT8) : Bool := true

end LeanDFumt

Build output: clean. Now watch decide and native_decide disagree on the same theorem:

-- Uses the declared body (kernel reduction):
example : LeanDFumt.hijacked_toBool .FALSE = false := by decide
-- ✓ passes

-- Uses the native override:
example : LeanDFumt.hijacked_toBool .FALSE = false := by native_decide
-- ✗ fails: 'true = false'

The native_decide failure at least surfaces the disagreement here. The dangerous case is the reverse: a native_decide proof succeeds where decide would have failed — because the native lie happens to satisfy the goal while the honest declared body does not. Both proofs pass verify() as VALID; only cross-checking the two tactics on the same goal reveals the fraud.

Why it matters

LeanDFumt's soundness rests on the assumption that #eval, decide, and native_decide agree on every DFUMT8 operation. This assumption is what lets Papers 75/76 use the same operators at compile time (in Lean proofs) and at runtime (in QuTiP-numerical anchors). An @[implemented_by] attribute anywhere in the transitive call graph invalidates the assumption — silently, at a single site, with no downstream indicator.

The attribute has legitimate uses in the standard library (System.Platform.numBits, some IO primitives) — cases where the declared body is a specification and the native impl is a faster equivalent. In an algebraic library it has none. Every operation on DFUMT8 is a pattern match on eight constructors; nothing needs a faster native path.

Fix

Delete the attribute. If the declared body is correct — as it should be — deleting the attribute makes native_decide agree with decide automatically:

-- Deleted: @[implemented_by lie_toBool]

def honest_toBool (a : DFUMT8) : Bool :=
  match a with
  | .TRUE | .BOTH => true
  | _             => false

-- Both tactics now use the same body:
example : honest_toBool .FALSE = false := by decide         -- ✓
example : honest_toBool .FALSE = false := by native_decide  -- ✓

If a native fast path is genuinely needed (LeanDFumt currently has none), the two bodies must be equal by inspection and the attribute site must be documented with a written justification. In LeanDFumt the whitelist for @[implemented_by] is currently empty; the library is native-override-free.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file with an @[implemented_by] attribute compiles and both decide and native_decide proofs return VALID — even when the two would disagree if run side-by-side. Enforcement in v0 is a pre-check that runs before the file reaches verify(): parse each declaration's attributes and reject the file if any carries @[implemented_by ...] outside a project-declared whitelist. Optional harder mode: for every declaration with the attribute, submit both a decide proof and a native_decide proof of the same trivial identity (e.g. f x = f x); a UNDECIDED / UNSUPPORTED_SYNTAX from one but not the other is a red flag.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "implemented_by") enumerates every declaration carrying the @[implemented_by] attribute and, for each pair (declared body, native impl), attempts a kernel-level convertibility check — reports each unverified pair with its source position. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also