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

Pass-2 (GLM 5.3) verification of the `flsl` (find-LAST-set, `long`) member
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/flsl.c` has no entry in `sys/conf/files`
   (libkern block 2195–2237; `grep -c` = 0 on host **and** guest).
   Every kernel TU gets `flsl` as `static __inline` from
   `sys/cpu/x86_64/include/cpufunc.h:290-296` (`HAVE_INLINE_FLSL`,
   `bsrq`-based).
2. **Cannot compile in-kernel as committed**: `#include <sys/libkern.h>`
   (flsl.c:32) pulls `libkern.h:51 → systm.h:50 → machine/cpufunc.h`, and
   the out-of-line definition at flsl.c:37-47 collides with the
   `static __inline flsl`: gcc 8.3 `error: redefinition of 'flsl'`
   (`dead_compile_flsl.log`, kernel-style `-nostdinc -D_KERNEL` compile).
3. **Latent body is arithmetically perfect**: verbatim body vs the live
   cpufunc.h inline (bsrq asm copied verbatim) and vs `64 - __builtin_clzl`:
   58,454,211 structure-complete cases (0, ~0, sign word, all 64 single
   bits, exhaustive low-22 and top-22 patterns, MSB-position sweep ×1024,
   50M randoms) — **0 mismatches** (`run.log` T2).
4. **Fix validated at compile level**: `fix.diff` = `#if
   !defined(HAVE_INLINE_FLSL)` gate. Gated file compiles kernel-style and
   defines **no** global `flsl` symbol on x86_64. Deletion equally valid.

## 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: flsl.c cannot compile in-kernel as committed: ... error: redefinition of 'flsl'
T2 flsl :   58454211 cases,          0 mism vs live-inline,          0 mism vs clz-ref
HARNESS-PASS: ...
FIXCOMPILE-OK: gated flsl.c compiles kernel-style; global flsl symbols in object: 0
```

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