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

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

The claim, and how each part was proven

1. ffsl.c is not compiled into any DragonFly kernel or module. - sys/conf/files libkern block (lines 2195–2237) has no ffsl.c entry — nor any of the ffs/fls C family (ffs.c, fls.c, ffsl.c, flsl.c, flsll.c; census in build.log: all grep -c = 0, verified on host and guest). - sys/cpu/ contains only x86_64 — the only supported platform — and every kernel TU gets ffsl as static __inline from sys/cpu/x86_64/include/cpufunc.h:274-280 (#define HAVE_INLINE_FFSL
   • __builtin_ffsl). The prototype in sys/sys/libkern.h:105-106 is itself gated by #ifndef HAVE_INLINE_FFSL, so TUs that see cpufunc.h never even see the out-of-line prototype.
2. The file cannot compile in-kernel as committed — a different mechanism than ffs.c's string.h (DF-5714), same outcome. ffsl.c:32 includes <sys/libkern.h>, which resolves fine under -nostdinc; but libkern.h:51 → sys/systm.h:50 → machine/cpufunc.h puts the static __inline ffsl (cpufunc.h:276-280) into the same TU, and the file's own out-of-line definition (ffsl.c:37-47) then collides: ffsl.c:38:1: error: redefinition of 'ffsl' / cpufunc.h:277:1: note: previous definition (dead_compile_ffsl.log, kernel-style compile per sys/conf/kern.pre.mk:61). So re-adding the file to conf/files would break the x86_64 kernel build.
3. The latent body is arithmetically perfect. Verbatim kernel body (only the kernel-only include line stripped, identifier renamed -Dffsl=k_ffsl, called through a volatile function pointer, -O2) vs (a) the live cpufunc.h inline implementation and (b) __builtin_ffsl: 0 / 58,454,211 mismatches (run.log T1). Domain: 0, ~0, 1<<63, all 64 single-bit words, exhaustive over all words with bits in the low 22 positions (4,194,304), exhaustive over all words with bits in the top 22 positions (4,194,304), every MSB position ×1024 randoms below it, and 50,000,000 splitmix64 randoms. This clears the mask == 0 → 0 path (ffsl.c:42-43), sign-bit/negative inputs, and the unsigned-shift refill at ffsl.c:45 — for this family the output depends only on the LSB position, and the domain above covers every reachable LSB/MSB structure.
4. Consumer census (why this is Info, not higher). No in-tree .c file calls ffsl directly; its uses are inside headers (sys/dev/misc/evdev/freebsd-bitstring.h:308,361, sys/dev/drm/include/linux/bitops.h:61 via __ffsl) and all resolve to the cpufunc.h inline. Nothing references the dead object. No memory operands exist (pure register function) — guard-page/overflow classes are vacuous.
5. Fix. fix.diff: FreeBSD-style #if !defined(HAVE_INLINE_FFSL) gate around the body. Validated: gated file compiles kernel-style and the body compiles away on x86_64 — nm census shows 0 global ffsl symbols in the object (build.log "FIXCOMPILE-OK", fix_run.log). Deleting the file is the equally-valid alternative (maintainer's choice); the diff is the conservative variant, consistent with DF-5714's fix for ffs.c.

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 plus the machine-checked latent-correctness proof (precedent: DF-5714 ffs.c, DF-5700 bcmp.c, same class).

Rig honesty notes

• First shot: build.sh (identity pin, census, verbatim compiles, deadproof, fix validation) and run.sh (differential) both succeeded on the first execution; no intermediate failed artifacts exist for this pack. One host-side slip (an aborted harness draft, p2_harness_scratch.c) was scp'd along with the rig and deleted from the guest scratch before evidence capture; it never compiled and is not part of the provenance chain (attempts counted as 2: build pass, run pass).
• The harness's "live inline" reference implementations are copied verbatim from cpufunc.h (bsrl/bsrq asm from :110-126, ffsl from :276-280), so the comparison target is the exact code the running kernel uses.

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.