# DF-5715 — sys/libkern/ffsl.c dead-file status + latent-correctness proof

Pass-2 (GLM 5.3) verification of the `ffsl` tail of the ffs/fls family
(family context established by DF-5714 for ffs.c; rig pattern identical).

## What was machine-proven on the DragonFly guest

1. **Dead file**: `libkern/ffsl.c` has no entry in `sys/conf/files`
   (libkern block 2195–2237; `grep -c` = 0 on host **and** guest). Nothing
   links it. On the only supported arch every kernel TU gets `ffsl` as
   `static __inline` from `sys/cpu/x86_64/include/cpufunc.h:274-280`
   (`HAVE_INLINE_FFSL`, `__builtin_ffsl`).
2. **Cannot compile in-kernel as committed**: its `#include <sys/libkern.h>`
   (ffsl.c:32) resolves fine (unlike ffs.c's `string.h`), but
   `libkern.h:51 → systm.h:50 → machine/cpufunc.h` brings the
   `static __inline ffsl` into the same TU, and the out-of-line definition
   at ffsl.c:37-47 collides: gcc 8.3 `error: redefinition of 'ffsl'`
   (`dead_compile_ffsl.log`, kernel-style `-nostdinc -D_KERNEL` compile
   per `kern.pre.mk:61`).
3. **Latent body is arithmetically perfect**: verbatim body vs the live
   cpufunc.h inline and vs `__builtin_ffsl`: 58,454,211 cases
   (0, ~0, sign word, all 64 single bits, exhaustive low-22 and top-22
   bit patterns, MSB-position sweep ×1024, 50M splitmix64 randoms),
   **0 mismatches** (`run.log` T1).
4. **Fix validated at compile level**: `fix.diff` = FreeBSD-style
   `#if !defined(HAVE_INLINE_FFSL)` gate. Gated file compiles kernel-style
   and defines **no** global `ffsl` symbol on x86_64 (body compiles away).
   Deletion is the equally-valid alternative.

## Reproduce

Copy this directory to the guest and, as root:

```sh
sh build.sh   # identity pin (cksum), conf/files census, verbatim renamed
              # compiles, kernel-style deadproof, fix validation
sh run.sh     # differential harness (~3 s)
```

Expected decisive lines:

```
DEADPROOF-OK: ffsl.c cannot compile in-kernel as committed: ... error: redefinition of 'ffsl'
T1 ffsl :   58454211 cases,          0 mism vs live-inline,          0 mism vs clz-ref
HARNESS-PASS: ...
FIXCOMPILE-OK: gated ffsl.c compiles kernel-style; global ffsl symbols in object: 0
```

`build.sh` expects the guest sources at `/usr/src/sys` (override with
`S=...`). Host/guest source identity: ffsl.c cksum `1444671719 1875`.