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

**Status: reproduced (impact: none — dead code, Info-severity hygiene finding).
Confidence: certain. Attempts: 5. All claims machine-demonstrated on the
DragonFly guest (uname in `env.txt`; guest sources cksum-identical to the
audit tree: ffs.c 3349697062 1930 / ffsl.c 1444671719 1875 / strcmp.c
180206468 2066).**

## The claim, and how each part was proven

1. **`ffs.c` is not compiled into any DragonFly kernel or module.**
   - `sys/conf/files` libkern block (lines 2195–2237) has no `ffs.c` entry
     (nor `ffsl.c`/`flsl.c`/`flsll.c`). Verified on host and guest
     (`grep -c "libkern/ffs.c" /usr/src/sys/conf/files` → `0`, `env.txt`).
   - `sys/cpu/` contains only `x86_64` — the only supported platform — and
     every kernel TU gets `ffs` as `static __inline` from
     `sys/cpu/x86_64/include/cpufunc.h:266-273`
     (`#define HAVE_INLINE_FFS` + `__builtin_ffs`).
   - Empirical: `cc -O2 -nostdinc -I/usr/src/sys -c /usr/src/sys/libkern/ffs.c`
     → `ffs.c:33:10: fatal error: string.h: No such file or directory`
     (`dead_compile.log`; kernel uses `-nostdinc`, `sys/conf/kern.pre.mk:61`).
     The file cannot even be compiled in-kernel as committed.
2. **The latent body is arithmetically perfect.** Full-domain sweep of all
   2^32 masks: verbatim kernel `ffs.c` body (renamed `-Dffs=k_ffs`,
   compiled -O2, called through a volatile function pointer) vs
   `__builtin_ffs` == the live cpufunc.h inline: **0 / 4,294,967,296
   mismatches** (`run.log` T1). This simultaneously clears every arithmetic
   candidate: `mask == 0 → 0` (ffs.c:43-44), the negative/INT_MIN inputs
   (returns 32), the implementation-defined `mask >>= 1` signed right shift
   (ffs.c:46) — output-identical on the kernel toolchain gcc 8.3, because
   the loop only ever inspects the low bit and terminates at the lowest set
   bit, so arithmetic vs logical refill is unobservable. `ffsl.c` twin
   (which uses an explicitly unsigned shift, ffsl.c:44): 50,002,088 cases,
   0 mismatches (T2). No `ffsll` exists anywhere in the kernel (zero
   definitions, zero callers).
3. **Compiler-builtin interplay.** There is no loop-idiom → self-call or
   builtin-substitution hazard: the out-of-line body is dead, and the live
   inline is the builtin by construction (`cpufunc.h:271`). The only real
   interplay landmine is the reverse one, demonstrated in
   `fix_compile.log`: an out-of-line `ffs` **cannot coexist** with
   `cpufunc.h`'s `static __inline ffs` in one TU — so re-adding
   `libkern/ffs.c` to `conf/files` would break the x86_64 build twice over
   (missing `string.h`, then inline/outline collision).
4. **Consumer census (why this is Info, not higher).** 102 live `ffs(` call
   sites in-tree (excluding contrib): all resolve to the inline; none
   passes a 64-bit argument that would truncate (the census grep for
   64-bit-shaped operands produced only already-32-bit expressions:
   `msdosfs_fat.c:764/782` u_int bitmaps, drm 32-bit register masks,
   `am7990.c:169/173` int ring counts). 64-bit bit-scans correctly use
   `ffsl`. Guard-page class is vacuous for `ffs` — no memory operands.
5. **Fix.** `fix.diff`: `#include <string.h>` → `#include <sys/libkern.h>`
   + FreeBSD-style `#if !defined(HAVE_INLINE_FFS)` gate around the body.
   Baseline (unfixed) reproduced: kernel-style compile fails
   (`DEADPROOF-OK` record). Patched: compiles kernel-style, body correctly
   compiles away on x86_64 (`FIX2COMPILE-OK`, `fix2_compile.log`; the
   guest-validated `f_ffs2.c` is byte-identical to the diff's result).
   Deletion of the file is the equally-valid alternative fix (maintainer's
   choice); the diff is the conservative variant.

## 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
(precedent: DF-5700 bcmp.c, same class) plus the machine-checked
latent-correctness proof that closes the file's arithmetic questions
permanently.

## Rig honesty notes (all intermediate artifacts kept)

- `run.1.log`: first run had a harness bug — the guard-page fault cases
  (G3/G4) reused the page buffer left by G2 (…`'A',NUL` at the edge), so
  the walk mismatched in-bounds instead of reaching the guard. Fixed by
  re-arming the page; final `run.log` shows SIGSEGV for both kernel body
  and libc.
- `run.2.log`: second run had a dead-code-elimination artifact in the
  libc control (`(void)strcmp(...)` with unused result is elided by gcc
  -O2). Fixed by consuming the result; final run shows libc faulting
  identically to the kernel body.
- `p2_harness_v1.c`: the initial harness source, kept for the record.
- `fix_compile.log`: the naive-fix failure (inline collision) — evidence
  that the *correct* fix must include the `HAVE_INLINE_FFS` gate.

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

(No fix.diff for this item: documented recommendation only - see Fix above.)