initialize env pollution initialize ブロックで環境を書き換えている

Error message

Lean itself emits no error. This is a policy-level detection: any top-level initialize block outside the project's whitelist is flagged as a pre-check.

Lean 4's initialize blocks run at module load time. They are the standard mechanism for registering language extensions, attribute handlers, simp sets, and elaboration hooks. Everything that runs there executes before a downstream file's first declaration is elaborated, and the changes persist for the rest of the compilation. An attacker who can inject an initialize block into an imported module can, for example, add a fake simp lemma that rewrites False to True, and every subsequent by simp in the pipeline will silently trust it.

Minimal reproduction

-- File: BadInit.lean
import LeanDFumt
import Lean

namespace LeanDFumt

/-- Register a fabricated simp lemma at load time. Every downstream
    `by simp` sees it. -/
initialize
  Lean.Elab.Command.liftTermElabM do
    let stx ← `(theorem contradictory_true : False = True := by admit)
    Lean.Elab.Command.elabCommand stx

end LeanDFumt

-- File: Downstream.lean
import LeanDFumt.BadInit

example : False := by
  have h : False = True := contradictory_true
  rw [h]
  trivial      -- passes; the polluted simp set says True = True

Build output: clean for the initialise site (the admit is buried inside the runtime meta-program, not the source), and clean for the downstream file — which now imports a proof of False.

The reproduction above is deliberately schematic. Real environment-mutation attacks are more subtle — quietly registered attributes, injected elaboration hooks, side-effectful IO that touches the file system at compile time. The point is that none of them surface at any single verify() call: the fault is in the load-time context, not in the checked expression.

Why it matters

LeanDFumt's Basic.lean, Theorems.lean, and PropEmbedding.lean declare no initialize blocks. Every proof is discharged by decide, native_decide, or rfl — tactics that depend only on the kernel and the declared bodies. Introducing an initialize block into the algebraic core widens the trust root to include every side effect executed at module load, which is impossible to review at the theorem's site.

A downstream user of LeanDFumt has no way to know their by simp tactic depends on load-time pollution; the #print axioms command reports only the kernel axioms the theorem consumes, not the run-time environment mutations that shaped those axioms. This is the one attack surface where the usual post-compile audit (axiom bypass's #print axioms, Classical.choice smuggled's axiom inspection) is silent by design.

Fix

Delete the initialize block. The three modules that make up LeanDFumt do not need one, and every claim they make is discharged without load-time machinery. If an algorithm genuinely requires an extension (e.g., a custom notation package for D-FUMT₈ operators beyond the scoped notation already used), isolate it in a dedicated module opted out of the algebraic-core target:

# lakefile.toml
[[lean_lib]]
name = "LeanDFumtNotation"    # optional extension module
# default_target = false      # not in `lake build` default set

The whitelist for initialize blocks in LeanDFumt is currently empty; the library is load-time-immutable.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not detectable through verify(). This is the fundamental limitation: verify() checks a single expression against the environment it was handed, and if that environment has already been polluted at load time, the VALID verdict is a truthful report of a corrupt baseline. Enforcement in v0 is a pre-check that runs before the file is loaded at all: parse each source file for initialize blocks and reject the file if any appears outside a project-declared whitelist. The whitelist must be maintained by hand — this is one place where "reject unless explicitly allowed" is the only safe default.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "initialize_block") enumerates every top-level initialize declaration in the project and classifies each by the environment fragment it mutates (attribute table, simp set, elaboration hook, filesystem IO). This classification lets a downstream user judge severity without reading the block's body. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also