# DF-5714 — sys/libkern/ffs.c is dead code (not compiled anywhere), latent body proven correct over the full 2^32 domain

## What this pack proves (all on the DragonFly guest, sources cksum-pinned to the audit tree)

1. **DEAD FILE** — `sys/libkern/ffs.c` is referenced by nothing:
   - absent from `sys/conf/files` (libkern block lines 2195–2237 lists every
     libkern file that is compiled; `ffs.c`, `ffsl.c`, `flsl.c`, `flsll.c`
     are all missing),
   - the only supported architecture is x86_64 (`sys/cpu/` contains only
     `x86_64`), where every kernel TU instead uses the
     `sys/cpu/x86_64/include/cpufunc.h:266-273` `static __inline ffs()`
     (`#define HAVE_INLINE_FFS` → `__builtin_ffs`),
   - `ffs.c:33`'s `#include <string.h>` cannot even resolve in a kernel
     build (`-nostdinc`, `sys/conf/kern.pre.mk:61`; no `sys/string.h`
     exists) — empirically demonstrated in `build.log` / `dead_compile.log`.
2. **LATENT BODY CORRECT** — the verbatim `ffs.c` body, renamed at the
   preprocessor level and compiled at -O2, matches `__builtin_ffs` (== the
   live kernel semantics via cpufunc.h) on **all 4,294,967,296 inputs,
   0 mismatches** (run.log T1). The `mask >>= 1` arithmetic-shift-on-negative
   (ffs.c:46) is implementation-defined in C but produces bit-exact results
   on the kernel toolchain (gcc 8.3), including mask=INT_MIN → 32 and the
   `mask == 0 → 0` guard (ffs.c:43-44). `ffsl.c` twin: 50,002,088
   edge/exhaustive-pair/random cases, 0 mismatches (T2). There is no
   `ffsll` in the kernel at all (zero callers, zero definitions).
3. **CONSUMER CENSUS (102 live `ffs(` call sites)** — every live caller
   consumes the cpufunc.h inline; no caller passes a 64-bit value that
   would truncate (all operands are already int/u_int width; the 64-bit
   users correctly call `ffsl`). Guard-page class N/A: `ffs.c:39-47` is
   pure register arithmetic — no pointer parameters, no dereference.
4. **FIX VALIDATED (compile level — the level at which the "bug" lives)** —
   a naive include swap is NOT enough: `cpufunc.h:269`'s `static __inline
   ffs` collides with any out-of-line definition (recorded in
   `fix_compile.log`). The final `fix.diff` (include swap +
   FreeBSD-style `#if !defined(HAVE_INLINE_FFS)` gate) compiles
   kernel-style: `FIX2COMPILE-OK` in `build.log` / `fix2_compile.log`.

## Reproduce

```
scp -r . dfbsd:/tmp/df5714/        # or: git clone of this pack
ssh dfbsd                          # root
sh /tmp/df5714/build.sh            # ~30 s: verbatim compiles + proofs
sh /tmp/df5714/run.sh              # ~26 s: T1 full-domain sweep + T2-T5
```

Expected decisive lines (see `run.log`):
```
T1 ffs full-domain: 4294967296 cases, 0 mismatches ...
T2 ffsl: 50002088 cases, 0 mismatches (vs __builtin_ffsl)
...
DEADPROOF-OK: ffs.c cannot compile in-kernel:      (build.log)
FIX2COMPILE-OK: guarded ffs.c compiles kernel-style (build.log)
HARNESS-PASS
```

The same harness also carries the **strcmp.c negative evidence** (T3/T4 —
see `../neg-evidence-strcmp-pass2/`).