perf(decode): adopt libdeflate's decoder architecture — tracking issue

[kim-em]

Umbrella / tracking issue: re-architect the native DEFLATE decoder along libdeflate's lines. Records what libdeflate actually does (correcting #2653's premise) and links the per-phase work, split by the lean4#14053 dependency.

Background: why #2653 didn't pan out, and what libdeflate actually does

#2653 assumed libdeflate decodes "1-2 symbols per table lookup". Both prototypes built on that premise were net-negative (closed on #2653): a lazy runtime second-lookup was −1.7%/−2.9% (canterbury/dickens), and an eager precomputed wide 2-symbol table was −31% to −53%, dominated by per-block table-build cost.

Reading libdeflate's source (lib/deflate_decompress.c, lib/decompress_template.h) shows the premise was wrong. libdeflate decodes one symbol per table lookup; its speed (multiple GB/s vs our ~143 MB/s) comes from a different, composable set of techniques:

1. Bulk word refill — a single unaligned 8-byte load OR'd into the bit buffer (REFILL_BITS_BRANCHLESS). We load one byte at a time in a ~7-iteration loop.
2. Multiple symbols per refill — the fastloop refills once (~56 bits) then decodes up to 3 literals back-to-back, no refill between them. We refill after every symbol.
3. Packed single-word entry — one u32 per entry (literal/length-base + codeword length + extra-bit count + type flags); literal fast path is a single high-bit test. We use two arrays plus separate length-base/extra lookups.
4. Canonical O(num_syms + 2^bits) build, no Huffman tree — counting sort + table-doubling fill, with subtables (array lookups) for long codes. We build a HuffTree per block, walk it per slot to build the table, and tree-walk long codes.
5. Wider root table — LITLEN_TABLEBITS = 11 vs our fastBits = 9.

What our bottleneck actually is (corrected after the #2669 attempt)

libdeflate's per-symbol cost is a few register ops, so amortizing the refill frequency (technique 2) is a big deal for them. Ours is not: an implementation attempt at technique 2 (#2669) regressed on every variant, because our per-symbol cost is dominated by table reads + ByteArray.push/RC + well-founded-recursion argument threading, which batching doesn't reduce — and without packed entries the per-literal "continue the batch?" test costs the same multi-read+compare that sank #2653's lazy prototype. So technique 2 is not the safe first win; it depends on technique 3 and is marginal even then.

The levers that attack our cost structure are the ones that cut per-symbol reads, per-refill cost, and per-block build: techniques 1, 3, 4.

Phases — split by the lean4#14053 dependency, measure-first at each gate

Priority, available now (no lean4#14053):

• Phase 3 — packed single-word entry → perf(decode): packed single-word decode-table entry (Phase 3 of #2668) #2670 — do this first. One read instead of two per symbol (standalone win), and the prerequisite that makes any literal-batching test a single cheap branch.
• Phase 4 — canonical O(n) build + subtables, retire the HuffTree → perf(decode): canonical O(n) table build + subtables, retire the HuffTree (Phase 4 of #2668) #2671 (heaviest proof; gate on a Phase 3 measurement).
• Phase 5 — widen the root table to ~11 bits → perf(decode): widen the root decode table to ~11 bits (Phase 5 of #2668) #2672 (depends on Phase 4).

Deferred / conditional:

• Phase 2 — multiple literals per refill → perf(decode): decode multiple literals per refill (Phase 2 of #2668) — deferred, depends on #2670 #2669 — depends on perf(decode): packed single-word decode-table entry (Phase 3 of #2668) #2670; an attempt without it regressed (see the issue for the root cause). Revisit as a small experiment after perf(decode): packed single-word decode-table entry (Phase 3 of #2668) #2670; expect marginal at best.

Blocked on lean4#14053 (wide ByteArray load accessors; open):

• Phase 1 — bulk word refill → perf(explore, needs lean4#14053): decode wide bit-refill — ugetUInt64LE in refill #2630 (already in the needs lean4#14053 family with perf(explore, needs lean4#14053): compress hash-load — ugetUInt32LE in hash3 #2629/perf(explore): BitWriter wide-store — local usetUInt64LE + pre-sized buffer (unblocked by #2707) #2631; refill is ~13.9% of decode, wide refill measured ~1.63× → est. ~5% decode). Lands when #14053 merges and the toolchain bumps.

Recommended order: #2670 (packed entry) first — it's a standalone per-symbol read reduction and unblocks everything else — then measure; #2630 (bulk refill) whenever lean4#14053 is available; then decide whether the remaining gap justifies #2671's heavy build/proof. #2669 is conditional on #2670 and low priority.

References: libdeflate lib/deflate_decompress.c (build_decode_table; entry format ~L425-500) and lib/decompress_template.h (fastloop ~L337-435). Foundations landed: #2666.

[kim-em]

Status + recommended order (after #2670/#2673 landed: +6.8% dickens / +12.5% canterbury, validating per-symbol read-reduction as our lever).

Phase 3b filed as #2674 (fold length base + extra into the packed entry — follow-up to #2673).

Recommended order:

0. Re-profile decode at current master (gate, not an issue). The symbol loop has been trimmed repeatedly (perf(decode): de-allocate the decodeSym / takeBits per-symbol success tuples (continue #2645) #2649/perf(decode): de-box the Huffman symbol table (Array (UInt16 × UInt8) -> packed word) #2650/perf(decode): drop redundant per-symbol guards from the wide-buffer decoder #2663/perf(decode): USize the goFused bit counters through the symbol loop #2664/perf(decode): packed single-word decode-table entry (Phase 3 of #2668) #2670); literal reads are near-optimal. Confirm where time goes now (output-copy was ~31% and RC/alloc ~10% in the last profile) before committing to the heaviest build. This decides whether to keep pushing the decode loop or pivot to output-copy.
1. perf(decode): fold length base + extra-bit count into the packed decode entry (Phase 3b of #2668) #2674 — length base/extra fold. Low-risk continuation of the proven read-reduction win, and it finalizes the packed-entry format (literals from perf(decode): packed single-word decode-table entry #2673 + lengths here) so the canonical build (perf(decode): canonical O(n) table build + subtables, retire the HuffTree (Phase 4 of #2668) #2671) can target the final format instead of being repacked later.
2. perf(decode): decode multiple literals per refill (Phase 2 of #2668) — deferred, depends on #2670 #2669 — multi-per-refill: quick spike, then resolve. Now unblocked by packed entries (the batch-continue test is cheap), so re-test cheaply; if still flat/negative (expected — the refill guard isn't our bottleneck), close it definitively.
3. perf(decode): canonical O(n) table build + subtables, retire the HuffTree (Phase 4 of #2668) #2671 — canonical O(n) build + retire HuffTree. The big structural bet and heaviest proof; start only if step 0 shows per-block build / walkTree is a meaningful fraction (amortized on dickens, larger on small inputs). Builds the finalized packed entry from step 1.
4. perf(decode): widen the root decode table to ~11 bits (Phase 5 of #2668) #2672 — widen root table to ~11 bits. Cheap immediately after perf(decode): canonical O(n) table build + subtables, retire the HuffTree (Phase 4 of #2668) #2671.

Parallel / external track:

• perf(explore, needs lean4#14053): decode wide bit-refill — ugetUInt64LE in refill #2630 — bulk refill lands whenever lean4#14053 merges + toolchain bump (~5% est., independent of the above).

[kim-em]

Step-0 re-profile done (post-#2670/#2673, dickens decode, self-time, longest_match/compress filtered).

symbol	self%	bucket
goFusedPU	33.5%	symbol loop (dispatch + push + inlined refill)
lean_byte_array_copy_slice + memmove + copyLoop + extract	~28%	output back-reference copy
lean_dec_ref_cold + mi_free/mi_malloc + lean_copy_sarray	~13%	RC / alloc / buffer growth
walkTree	5.0%	long-code (>9-bit) tree-walk fallback
tableEntry_go	2.0%	per-slot table-build walk

Takeaways:

• The symbol loop (33.5%) is still Review: split InflateCorrect.lean, proof improvements #1 but the packed entry already took the big literal win; further cuts need bulk refill (perf(explore, needs lean4#14053): decode wide bit-refill — ugetUInt64LE in refill #2630, blocked on lean4#14053) or multi-per-refill (perf(decode): decode multiple literals per refill (Phase 2 of #2668) — deferred, depends on #2670 #2669, marginal — the refill guard is a small part of this). Diminishing returns here until #14053.
• perf(decode): canonical O(n) table build + subtables, retire the HuffTree (Phase 4 of #2668) #2671 (canonical build + subtables) is now data-justified: it directly eliminates walkTree (5%) and tableEntry_go (2%) and the per-block HuffTree allocation (part of the ~13% RC/alloc) — a concrete ~7-10% target on dickens, larger on smaller inputs. The subtable replaces the tree walk with an array lookup; perf(decode): widen the root decode table to ~11 bits (Phase 5 of #2668) #2672 (wider root) then shrinks the remaining fallback population. This is the strongest evidence-backed next bet, and it's what the step-0 gate was for.
• Output-copy (~28%) is mostly irreducible (memmove/copy_slice must move the bytes), but copyLoop (7.4%, our worker) is addressable and is outside the perf(decode): adopt libdeflate's decoder architecture — tracking issue #2668 program — worth its own issue if we want it. lean_copy_sarray (4%) is buffer-growth realloc, already mitigated by sizeHint when the size is known (this profile mixes hinted/unhinted).

Revised order: #2674 (small warm-up) → #2671 (now justified; the structural bet) → #2672. #2669 stays low (marginal); #2630 lands with lean4#14053.