native_decide bluff native_decide でカーネル検査を回避している

Error message

Lean itself emits no error. This is a policy-level detection: any use of native_decide outside the project's designated numeric-anchor module is flagged as a pre-check.

native_decide is a legitimate tactic, but it works by compiling the goal to native code and trusting the compiled binary. Unlike decide (which produces a term the Lean kernel re-checks), native_decide extends the trust root of every theorem it closes to include the native compiler, the runtime, and any @[implemented_by] attributes on transitively-called functions. This is fine for a small, audited numeric anchor. It is not fine as a general-purpose tactic under the kernel-checked discipline LeanDFumt advertises.

Minimal reproduction

-- File: BadNativeDecide.lean
import LeanDFumt

namespace LeanDFumt

-- The library provides `and_FALSE_left` as a `decide`-proved theorem.
-- An agent submits a "replacement" using native_decide — the tactic
-- looks equivalent, but the trust story changes silently.
theorem and_FALSE_left_native (a : DFUMT8) :
    and .FALSE a = .FALSE := by
  cases a <;> native_decide

end LeanDFumt

Build output: clean. Now compare the trust root:

#print axioms LeanDFumt.and_FALSE_left
-- 'LeanDFumt.and_FALSE_left' does not depend on any axioms

#print axioms LeanDFumt.and_FALSE_left_native
-- 'LeanDFumt.and_FALSE_left_native' depends on axioms:
--   Lean.ofReduceBool

Lean.ofReduceBool is the marker axiom introduced by native_decide. Its presence means "the theorem's truth was decided by native compilation, not by the Lean kernel." The two theorems above are propositionally equivalent, but only one is kernel-checked.

Why it matters

LeanDFumt's Theorems.lean uses native_decide in exactly one place — the numeric anchor toFloat_TRUE_pos, which necessarily involves Float arithmetic that the kernel cannot reduce. Every other theorem in the library is closed by decide, rfl, or cases … <;> decide. This discipline is what lets the README claim:

All proved by decide / native_decide on the finite type.

Silently expanding the use of native_decide widens the trust root without acknowledgement. An @[implemented_by native_lie] attribute anywhere in the transitive call graph would then be sufficient to make a false theorem compile.

Fix

Replace native_decide with decide wherever the goal can be reduced by the kernel — on the finite DFUMT8 type this is almost always the case:

theorem and_FALSE_left (a : DFUMT8) : and .FALSE a = .FALSE := by
  cases a <;> decide

Verify the fix by re-checking the axiom dependencies:

#print axioms LeanDFumt.and_FALSE_left
-- 'LeanDFumt.and_FALSE_left' does not depend on any axioms

If decide genuinely cannot close the goal — for example because it involves Float or another type the kernel cannot reduce — the theorem belongs in the numeric-anchor module (see Theorems.lean's toFloat_TRUE_pos), not in the algebraic core.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file that closes proofs with native_decide still compiles and verify() returns VALID. Enforcement in v0 is a two-step pre-check that runs after compilation but before the file is admitted to stats(): (a) grep for native_decide occurrences outside the designated numeric-anchor module; (b) run #print axioms <theorem> and reject the file if Lean.ofReduceBool appears in an axiom list belonging to a theorem declared outside the anchor. Rejected files never enter stats().

Post-v0 Layer 2 (planned — spec §13): locate_first_error(kind = "native_decide") traverses the elaborated declaration tree in source order and returns the position of the first native_decide tactic invocation whose enclosing module is not on the anchor whitelist. When paired with Lean.Environment introspection, this can also surface any @[implemented_by] attributes in the transitive call graph — the amplifier that turns a benign native_decide into a forgeable one. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also