`native_decide` and `Lean.ofReduceBool`: What the Lean 4 Kernel Trusts

How native_decide works in Lean 4, why it adds the Lean.ofReduceBool axiom, and how @[implemented_by] or @[extern] can make a theorem unsound when paired with native_decide.

1. decide versus native_decide

When you prove a decidable proposition with by decide (or rfl), Lean’s **kernel** reduces the boolean decision procedure step by step using the logical definitions in the environment. It is slow on large computations, but the trusted computing base (TCB) remains just the kernel.

When you use by native_decide, the kernel does **not** reduce the term. Instead, Lean compiles the decision procedure to native machine code (via the C compiler / LLVM interpreter), executes the binary, and—if the binary returns true—invokes the axiom Lean.ofReduceBool to assert that the kernel reduction would also have yielded true.

2. How @[implemented_by] and @[extern] break native_decide

Trusting native_decide expands the trusted computing base from the small Lean kernel to the entire Lean compiler, code generator, C runtime, and—crucially—every @[implemented_by] and @[extern] attribute reachable from the term.

In Lean 4, @[implemented_by fastFn] def specFn ... tells the compiler to replace specFn with fastFn in compiled code without proving they are equal. For ordinary kernel proofs (simp, omega, decide), @[implemented_by] is completely safe because the kernel ignores it and unfolds specFn. With native_decide, the compiled code runs fastFn while the theorem statement is about specFn:

def brokenImpl (_ : Nat) : Bool := false

@[implemented_by brokenImpl]
def alwaysTrue (_ : Nat) : Bool := true

-- The kernel unfolds `alwaysTrue 0` to `true`, while `native_decide` runs `brokenImpl 0` (`false`),
-- producing a proof of `true = false` via `Lean.ofReduceBool`.

3. How to audit native_decide in a proof repository

1. **Check #print axioms:** Any use of native_decide (even buried inside a helper lemma three imports deep) leaves Lean.ofReduceBool or Lean.ofReduceNat in the #print axioms output of the main theorem.

2. **Check the transitive call graph for @[implemented_by], @[extern], and unsafe:** If Lean.ofReduceBool is present, audit every function called by the decided expression to verify no runtime replacement attributes are used.

3. **Verify with nanoda / Comparator:** Independent kernels such as nanoda reject Lean.ofReduceBool unless explicitly configured to permit it.

Questions & Answers

Sources & References

1. Lean 4 Reference Manual — Axioms and `Lean.ofReduceBool`
2. Lean FRO — Comparator (`leanprover/comparator`)