Module eval 

A call-by-value evaluator for the kernel’s computational fragment — the engine behind native_decide.

Unlike normalize, which β/ι/δ-reduces by SUBSTITUTION and normalizes under binders to full normal form, this evaluates a CLOSED term to weak head normal form using an ENVIRONMENT (no substitution), stopping as soon as the head constructor is known. So deciding Eq Nat 10000 10000 is a linear environment walk, not a quadratic substitution blowup — the point of native_decide.

TRUST: native_decide trusts this evaluator to agree with the kernel’s reduction (as Lean’s native_decide trusts its compiler). It is validated by a differential test against normalize, and fail-safes to None (declining) on anything it cannot decide, but it IS part of the trusted base whenever native_decide is used.

Functions

eval_bool

Evaluate a closed Bool term to true/false, or None if it does not reduce to a Bool constructor within the fuel budget (fail-safe).

eval_bool_tree

The tree-walking interpreter decision — walks the Term each step. The fallback for eval_bool and the differential oracle the compiled path is validated against.

native_compile_bool

Compile a ground Bool decision into native closures and run it — None if the term is outside the compilable fragment (the caller falls back to the eval_bool interpreter). Semantics are IDENTICAL to eval_bool/normalize (differential-tested), so the ofReduceBool certificate native_decide builds is equally sound.

native_compile_decide

Compile a closed Bool decision to native closures and run it — None if it does not reduce to a Bool constructor (fail-safe; the caller falls back to the tree-walking interpreter). Unlike native_compile_bool, this handles the FULL computational fragment (recursion, pattern matching, definitions), so recursor-based decisions compile to native code. Its verdict is IDENTICAL to eval_bool_tree/normalize (differential-tested).

native_decide

Build a native_decide proof of prop from a Decidable prop instance inst: if the decision procedure NATIVELY evaluates to true, return the proof term of_decide_eq_true prop inst (ofReduceBool (decide prop inst) true (refl Bool true)), which the (main) kernel checks by running this evaluator via the reduceBool hook — never by re-normalizing the decision procedure. Returns None (fail-safe) when the decision is not true, so it can only ever produce proofs of genuinely-true goals.