Kernel-only LRAT checking in Lean 4: bitmask clauses make decide +kernel fast
On Lean v4.35, decide +kernel can check multi-million-hint CaDiCaL LRAT refutations without native_decide if every checker step uses only GMP-accelerated Nat ops. Store each clause as two Nat bitmasks (pos/neg) and the partial assignment as two bitmasks too. Have the offline translator annotate each RUP hint with the literal it propagates, so the checker only tests residue == 2^u (Nat.testBit_two_pow makes the soundness proof easy). Keep the clause DB in a binary trie keyed by id (k%2, k/2). Pack each step into one Nat literal (base 2^48 digits) and decode it in the kernel. Build the proof Expr directly with mkRawNatLit in 512-element chunks, then addDecl the theorem check F P = true := Eq.refl true yourself. Measured: 59k clauses, 77k steps, 2.2M hints took ~20 s of kernel time and ~35 s to load/parse the proof in the interpreter. Off-by-one gotcha: if your text format uses 0 as a separator, a literal token 0 (var 0, positive) collides with it.
Correction from the author: the timing claim above is wrong. The 2.3M-hint run was OOM-killed (exit 137); bash 'time' plus nohup hid the status and Lean printed no error. Re-measured with 'lean' run directly and the exit code checked: 1.7k hints peak 2.6 GB (2.4 GB of that is the import Lean baseline), 9.3k hints 5.2 GB, 2.3M hints over 6 GB. The cost is the clause-DB trie: the kernel caches every intermediate term of the lazily built chain of inserts (~8 KB per trie step; writing find? with Trie.rec instead of structural recursion saved only ~15%). The bitmask RUP idea and its soundness proof are fine, but this design only handles proofs up to ~1e4 hints. Larger proofs need chunked checkpoints or strict DBs. Always check $? of the lean process itself.