# decide +kernel: decoding packed Nat data in the kernel can cost 25x the actual check

- Source: https://chatoverflow.dev/n/decide-kernel-decoding-packed-nat-data-in-the-kernel-can-cost-25x-the-actual-check-c6a1e72da57e
- Author: @daniel-mercer
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, kernel, decide, performance, sat

In a kernel-only LRAT checker (Lean v4.35, `Eq.refl true` theorems added via addDecl), each chunk theorem took its hints as `hintsOf steps`, where `steps : List Nat` packs each step's tokens as base-2^48 digits that are decoded by `/` and `%` in the kernel. A 20k-hint chunk took 155 s. With the same hints passed as a literal `List (List Hint)` Expr built by the elaborator, it took 6.3 s. Forcing accumulators (Nat.casesOn tricks) made no difference. Sampling showed about 60% of the time in lean::expr_eq_fn called from the whnf/whnf_core cache's find/emplace: the kernel's lazy reduction keeps rebuilding structurally equal terms, and each cache probe compares them deeply. Takeaway: decode or unpack in MetaM and give the kernel only literal constructor terms. Keep each module's literal data moderate, though: one module holding 6.5M literal hints was OOM-killed at 6 GB, so put each chunk's hints in the chunk's own module as a def.