# VERDICT — DF-5716: sys/libkern/flsl.c dead-file status + latent-correctness proof

**Status: reproduced (impact: none — dead code, Info-severity hygiene
finding). Confidence: certain. Attempts: 2. All claims machine-demonstrated
on the DragonFly guest (uname in `env.txt`; guest source cksum-identical to
the audit tree: flsl.c `2802750667 1878`, ffsl.c `1444671719 1875`,
flsll.c `1445885582 1884`).**

## The claim, and how each part was proven

1. **`flsl.c` is not compiled into any DragonFly kernel or module.**
   - `sys/conf/files` libkern block (lines 2195–2237) has no `flsl.c`
     entry (census in `build.log`: `grep -c` = 0, host and guest).
   - Every kernel TU gets `flsl` as `static __inline` from
     `sys/cpu/x86_64/include/cpufunc.h:290-296` (`#define HAVE_INLINE_FLSL`,
     body `mask == 0 ? mask : (int)bsrq((u_long)mask) + 1`); the prototype
     in `sys/sys/libkern.h:111-112` is gated by `#ifndef HAVE_INLINE_FLSL`.
2. **The file cannot compile in-kernel as committed.** `flsl.c:32`
   includes `<sys/libkern.h>` → `libkern.h:51 → systm.h:50 →
   machine/cpufunc.h` brings the `static __inline flsl` into the TU, and
   the out-of-line definition (flsl.c:37-47) collides:
   `flsl.c:38:1: error: redefinition of 'flsl'` /
   `cpufunc.h:293:1: note: previous definition`
   (`dead_compile_flsl.log`, kernel-style `-nostdinc -D_KERNEL` compile
   per `sys/conf/kern.pre.mk:61`). Re-adding the file to `conf/files`
   would break the x86_64 kernel build.
3. **The latent body is arithmetically perfect — find-LAST-set semantics
   machine-checked.** Verbatim kernel body vs (a) the **live cpufunc.h
   inline implementation copied verbatim** (bsrq asm from cpufunc.h:119-126
   + the :292-296 body) and (b) the `64 - __builtin_clzl` reference:
   **0 / 58,454,211 mismatches** (`run.log` T2). The domain is
   structure-complete for the fls family (output depends only on the MSB
   position): 0, ~0, `1<<63`, all 64 single-bit words, exhaustive
   low-22-bit words, exhaustive top-22-bit words, every MSB position h∈[0,64)
   ×1024 random words with highest set bit exactly h, and 50,000,000
   splitmix64 randoms. This proves `flsl(x) = index_of_highest_set_bit + 1`
   (= `64 - clz(x)` for x≠0, `0` for x=0) for the whole 64-bit domain
   structure, including the loop-termination path at flsl.c:44
   (`mask != 1`) and the unsigned refill at flsl.c:45.
4. **Consumer census (why this is Info, not higher).** Live consumers all
   resolve to the inline, none to the dead object:
   - `sys/kern/kern_slaballoc.c:784` — `i = flsl(size)` inside
     `powerof2_size()` (:775-785): the `size == 0` and `powerof2(size)`
     guards (:781-782) ensure `flsl` is only called with size ≥ 2
     non-power-of-2, so the returned index ∈ [1, 63] and
     `1UL << i` cannot shift by 64 — no misuse.
   - `sys/dev/disk/nata/chipsets/ata-ahci.c:102`, `sys/sys/bitops.h:162`
     (ilog2 macro), `sys/dev/drm/include/linux/bitops.h:79`,
     `sys/dev/drm/include/linux/log2.h:40,52`.
   No memory operands — guard-page/overflow classes vacuous.
5. **Fix.** `fix.diff`: `#if !defined(HAVE_INLINE_FLSL)` gate. Validated:
   gated file compiles kernel-style, 0 global `flsl` symbols in the
   object on x86_64 (`build.log` "FIXCOMPILE-OK", `fix_run.log`).
   Deletion equally valid; consistent with DF-5714's ffs.c fix.

## Why no further escalation was pursued

Pure register function, no pointers, linked nowhere — no runtime kernel
behavior to attack. The pass-2 deliverable is the dead-file status plus
the machine-checked find-last-set correctness proof (precedent: DF-5714,
DF-5700, same class).

## Rig honesty notes

- Same rig as DF-5715/DF-5717 (shared `build.sh`/`run.sh`/`p2_harness.c`);
  first-shot success, no intermediate failed artifacts. See DF-5715's
  VERDICT for the scratch-file note.

## Fix status (batch validation)
Applied with the 36 sibling fix.diffs of this batch in findings/poc/_batch41/all_fixes.patch; single in-guest `make -j6 nativekernel KERNCONF=X86_64_GENERIC` completed RC=0 with zero errors under -Werror (full log: findings/poc/_batch41/fix_build8.log). Behavior A/B intentionally skipped for this Info-tier item.