# VERDICT — DF-5715: sys/libkern/ffsl.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: ffsl.c `1444671719 1875`, flsl.c `2802750667 1878`,
flsll.c `1445885582 1884`).**

## The claim, and how each part was proven

1. **`ffsl.c` is not compiled into any DragonFly kernel or module.**
   - `sys/conf/files` libkern block (lines 2195–2237) has no `ffsl.c`
     entry — nor any of the ffs/fls C family (`ffs.c`, `fls.c`, `ffsl.c`,
     `flsl.c`, `flsll.c`; census in `build.log`: all `grep -c` = 0,
     verified on host and guest).
   - `sys/cpu/` contains only `x86_64` — the only supported platform — and
     every kernel TU gets `ffsl` as `static __inline` from
     `sys/cpu/x86_64/include/cpufunc.h:274-280` (`#define HAVE_INLINE_FFSL`
     + `__builtin_ffsl`). The prototype in `sys/sys/libkern.h:105-106` is
     itself gated by `#ifndef HAVE_INLINE_FFSL`, so TUs that see cpufunc.h
     never even see the out-of-line prototype.
2. **The file cannot compile in-kernel as committed** — a *different*
   mechanism than ffs.c's `string.h` (DF-5714), same outcome. `ffsl.c:32`
   includes `<sys/libkern.h>`, which resolves fine under `-nostdinc`;
   but `libkern.h:51 → sys/systm.h:50 → machine/cpufunc.h` puts the
   `static __inline ffsl` (cpufunc.h:276-280) into the same TU, and the
   file's own out-of-line definition (ffsl.c:37-47) then collides:
   `ffsl.c:38:1: error: redefinition of 'ffsl'` /
   `cpufunc.h:277:1: note: previous definition` (`dead_compile_ffsl.log`,
   kernel-style compile per `sys/conf/kern.pre.mk:61`). So re-adding the
   file to `conf/files` would break the x86_64 kernel build.
3. **The latent body is arithmetically perfect.** Verbatim kernel body
   (only the kernel-only include line stripped, identifier renamed
   `-Dffsl=k_ffsl`, called through a volatile function pointer, -O2) vs
   (a) the live cpufunc.h inline implementation and (b) `__builtin_ffsl`:
   **0 / 58,454,211 mismatches** (`run.log` T1). Domain: 0, ~0, `1<<63`,
   all 64 single-bit words, exhaustive over all words with bits in the low
   22 positions (4,194,304), exhaustive over all words with bits in the top
   22 positions (4,194,304), every MSB position ×1024 randoms below it,
   and 50,000,000 splitmix64 randoms. This clears the `mask == 0 → 0` path
   (ffsl.c:42-43), sign-bit/negative inputs, and the unsigned-shift refill
   at ffsl.c:45 — for this family the output depends only on the LSB
   position, and the domain above covers every reachable LSB/MSB structure.
4. **Consumer census (why this is Info, not higher).** No in-tree `.c`
   file calls `ffsl` directly; its uses are inside headers
   (`sys/dev/misc/evdev/freebsd-bitstring.h:308,361`,
   `sys/dev/drm/include/linux/bitops.h:61` via `__ffsl`) and all resolve
   to the cpufunc.h inline. Nothing references the dead object. No memory
   operands exist (pure register function) — guard-page/overflow classes
   are vacuous.
5. **Fix.** `fix.diff`: FreeBSD-style `#if !defined(HAVE_INLINE_FFSL)` gate
   around the body. Validated: gated file compiles kernel-style and the
   body compiles away on x86_64 — `nm` census shows 0 global `ffsl`
   symbols in the object (`build.log` "FIXCOMPILE-OK", `fix_run.log`).
   Deleting the file is the equally-valid alternative (maintainer's
   choice); the diff is the conservative variant, consistent with
   DF-5714's fix for ffs.c.

## Why no further escalation was pursued

No memory-safety primitive exists in this file (pure register function,
no pointers), and the file is not linked anywhere — there is no runtime
kernel behavior to attack. The pass-2 deliverable is the dead-file status
plus the machine-checked latent-correctness proof (precedent: DF-5714
ffs.c, DF-5700 bcmp.c, same class).

## Rig honesty notes

- First shot: `build.sh` (identity pin, census, verbatim compiles,
  deadproof, fix validation) and `run.sh` (differential) both succeeded
  on the first execution; no intermediate failed artifacts exist for this
  pack. One host-side slip (an aborted harness draft,
  `p2_harness_scratch.c`) was scp'd along with the rig and deleted from
  the guest scratch before evidence capture; it never compiled and is not
  part of the provenance chain (attempts counted as 2: build pass, run
  pass).
- The harness's "live inline" reference implementations are copied
  verbatim from cpufunc.h (bsrl/bsrq asm from :110-126, ffsl from
  :276-280), so the comparison target is the exact code the running
  kernel uses.

## 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.