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

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

The claim, and how each part was proven

1. flsl.c is not compiled into any DragonFly kernel or module. - sys/conf/files libkern block (lines 2195–2237) has no flsl.c entry (census in build.log: grep -c = 0, host and guest). - Every kernel TU gets flsl as static __inline from sys/cpu/x86_64/include/cpufunc.h:290-296 (#define HAVE_INLINE_FLSL, body mask == 0 ? mask : (int)bsrq((u_long)mask) + 1); the prototype in sys/sys/libkern.h:111-112 is gated by #ifndef HAVE_INLINE_FLSL.
2. The file cannot compile in-kernel as committed. flsl.c:32 includes <sys/libkern.h> → libkern.h:51 → systm.h:50 → machine/cpufunc.h brings the static __inline flsl into the TU, and the out-of-line definition (flsl.c:37-47) collides: flsl.c:38:1: error: redefinition of 'flsl' / cpufunc.h:293:1: note: previous definition (dead_compile_flsl.log, kernel-style -nostdinc -D_KERNEL compile per sys/conf/kern.pre.mk:61). Re-adding the file to conf/files would break the x86_64 kernel build.
3. The latent body is arithmetically perfect — find-LAST-set semantics machine-checked. Verbatim kernel body vs (a) the live cpufunc.h inline implementation copied verbatim (bsrq asm from cpufunc.h:119-126 + the :292-296 body) and (b) the 64 - __builtin_clzl reference: 0 / 58,454,211 mismatches (run.log T2). The domain is structure-complete for the fls family (output depends only on the MSB position): 0, ~0, 1<<63, all 64 single-bit words, exhaustive low-22-bit words, exhaustive top-22-bit words, every MSB position h∈[0,64) ×1024 random words with highest set bit exactly h, and 50,000,000 splitmix64 randoms. This proves flsl(x) = index_of_highest_set_bit + 1 (= 64 - clz(x) for x≠0, 0 for x=0) for the whole 64-bit domain structure, including the loop-termination path at flsl.c:44 (mask != 1) and the unsigned refill at flsl.c:45.
4. Consumer census (why this is Info, not higher). Live consumers all resolve to the inline, none to the dead object: - sys/kern/kern_slaballoc.c:784 — i = flsl(size) inside powerof2_size() (:775-785): the size == 0 and powerof2(size) guards (:781-782) ensure flsl is only called with size ≥ 2 non-power-of-2, so the returned index ∈ [1, 63] and 1UL << i cannot shift by 64 — no misuse. - sys/dev/disk/nata/chipsets/ata-ahci.c:102, sys/sys/bitops.h:162 (ilog2 macro), sys/dev/drm/include/linux/bitops.h:79, sys/dev/drm/include/linux/log2.h:40,52. No memory operands — guard-page/overflow classes vacuous.
5. Fix. fix.diff: #if !defined(HAVE_INLINE_FLSL) gate. Validated: gated file compiles kernel-style, 0 global flsl symbols in the object on x86_64 (build.log "FIXCOMPILE-OK", fix_run.log). Deletion equally valid; consistent with DF-5714's ffs.c fix.

Why no further escalation was pursued

Pure register function, no pointers, linked nowhere — no runtime kernel behavior to attack. The pass-2 deliverable is the dead-file status plus the machine-checked find-last-set correctness proof (precedent: DF-5714, DF-5700, same class).

Rig honesty notes

• Same rig as DF-5715/DF-5717 (shared build.sh/run.sh/p2_harness.c); first-shot success, no intermediate failed artifacts. See DF-5715's VERDICT for the scratch-file note.

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.