unsafe escape unsafe 修飾で totality / カーネル検査を回避

Error message

Lean itself emits no error. This is a policy-level detection: any unsafe def, unsafe theorem, or use of unsafeCast in the project is flagged as a pre-check.

Lean 4's unsafe keyword exists to interoperate with FFI and low-level primitives that the kernel cannot verify. Uses include unsafeCast (arbitrary type coercion), unsafe def (skip termination check), and unsafe theorem (skip kernel re-check of the proof term). Each of these is legitimate in its niche. None of them belong in an algebraic library that advertises kernel-checked totality — every use is a hole punched in the very guarantee LeanDFumt trades on.

Minimal reproduction

-- File: BadUnsafe.lean
import LeanDFumt

namespace LeanDFumt

/-- Non-terminating recursion — Lean would normally reject this,
    but `unsafe` silences the termination check. -/
unsafe def force_neg : DFUMT8 → DFUMT8
  | a => force_neg (DFUMT8.neg a)

/-- `unsafeCast` — an arbitrary bit-pattern reinterpretation. -/
unsafe def cast_to_TRUE (n : Nat) : DFUMT8 := unsafeCast n

/-- Theorem that trusts the unsafe cast, closed by native_decide. -/
unsafe theorem cast_zero_is_TRUE : cast_to_TRUE 0 = .TRUE := by
  native_decide

end LeanDFumt

Build output: clean. The file compiles, and downstream code that imports the module sees cast_zero_is_TRUE as if it were an ordinary theorem — unless it also carries the unsafe attribute forward (which most callers do not audit).

Why it matters

LeanDFumt's Basic.lean declares inductive DFUMT8 as a finite, decidable type with total operations. Every theorem in Theorems.lean depends on that totality. Introducing an unsafe def anywhere in the library breaks the property downstream users implicitly assume: that every function terminates and every theorem was checked by the Lean kernel.

unsafeCast is particularly hazardous because it does not merely widen the trust root — it invalidates the type system's own soundness locally. A downstream decide on a value produced by unsafeCast can report anything.

Fix

Delete the unsafe modifier and rewrite the definition or proof to satisfy the kernel. For a pattern-matched recursion on DFUMT8, structural recursion always suffices — the type has eight constructors and no self-reference:

-- Safe replacement, no `unsafe`:
def double_neg : DFUMT8 → DFUMT8
  | a => DFUMT8.neg (DFUMT8.neg a)

theorem double_neg_id (a : DFUMT8) : double_neg a = a := by
  cases a <;> decide

If the code genuinely requires FFI or low-level access — e.g., a hardware oracle for the Rei-AIOS numeric anchor — it belongs in a separate module that is opted out of the algebraic-core target, with a written justification and an isolated theorem surface (analogous to the AxiomWhitelist.lean pattern for axiom bypass).

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file containing unsafe declarations compiles and verify() returns VALID on any downstream theorem. Enforcement in v0 is a pre-check that runs before the file reaches verify(): parse each declaration and reject the file if any carries the unsafe modifier or calls unsafeCast in its body. Rejected files never enter stats(), keeping decision_rate an honest measure of what was checked under the safe-only discipline.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "unsafe") enumerates every declaration in the project whose Lean.ConstantInfo.isUnsafe flag is set, plus every body that references unsafeCast in its expression tree. The result includes both the offending declaration and the theorems that transitively depend on it, so a downstream user can see which of their own claims are undermined by an upstream unsafe definition. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also