DF-5717 — sys/libkern/flsll.c dead-file status + latent-correctness proof

Pass-2 (GLM 5.3) verification of the flsll (find-LAST-set, long 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/flsll.c has no entry in sys/conf/files (libkern block 2195–2237; grep -c = 0 on host and guest). Every kernel TU gets flsll as static __inline from sys/cpu/x86_64/include/cpufunc.h:298-304 (HAVE_INLINE_FLSLL, delegating to flsl((long)mask)).
2. Cannot compile in-kernel as committed: #include <sys/libkern.h> (flsll.c:32) pulls libkern.h:51 → systm.h:50 → machine/cpufunc.h, and the out-of-line definition at flsll.c:37-47 collides with the static __inline flsll: gcc 8.3 error: redefinition of 'flsll' (dead_compile_flsll.log, kernel-style -nostdinc -D_KERNEL compile).
3. Latent body is arithmetically perfect: verbatim body vs the live cpufunc.h inline (verbatim copy), vs 64 - __builtin_clzll, and vs the verbatim kernel flsl twin: 58,454,211 structure-complete cases — 0 mismatches on all three axes (run.log T3).
4. Fix validated at compile level: fix.diff = #if !defined(HAVE_INLINE_FLSLL) gate. Gated file compiles kernel-style and defines no global flsll 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: flsll.c cannot compile in-kernel as committed: ... error: redefinition of 'flsll'
T3 flsll:   58454211 cases,          0 mism vs live-inline,          0 mism vs clz-ref,          0 mism vs kernel-flsl-twin
HARNESS-PASS: ...
FIXCOMPILE-OK: gated flsll.c compiles kernel-style; global flsll symbols in object: 0

build.sh expects the guest sources at /usr/src/sys (override with S=...). Host/guest source identity: flsll.c cksum 1445885582 1884.

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

The claim, and how each part was proven

1. flsll.c is not compiled into any DragonFly kernel or module. - sys/conf/files libkern block (lines 2195–2237) has no flsll.c entry (census in build.log: grep -c = 0, host and guest). - Every kernel TU gets flsll as static __inline from sys/cpu/x86_64/include/cpufunc.h:298-304 (#define HAVE_INLINE_FLSLL, body return (flsl((long)mask))); the prototype in sys/sys/libkern.h:114-115 is gated by #ifndef HAVE_INLINE_FLSLL.
2. The file cannot compile in-kernel as committed. flsll.c:32 includes <sys/libkern.h> → libkern.h:51 → systm.h:50 → machine/cpufunc.h brings the static __inline flsll into the TU, and the out-of-line definition (flsll.c:37-47) collides: flsll.c:38:1: error: redefinition of 'flsll' / cpufunc.h:301:1: note: previous definition (dead_compile_flsll.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 on long long machine-checked three ways. Verbatim kernel body vs (a) the live cpufunc.h inline implementation (verbatim copy of :300-304, i.e. flsl((long)mask) with the bsrq-based flsl), (b) the 64 - __builtin_clzll reference, and (c) the verbatim kernel flsl body itself (the twin check — on x86_64 long and long long are both 64-bit): 0 / 58,454,211 mismatches on all three axes (run.log T3). Domain is structure-complete for the fls family (0, ~0, 1<<63, all 64 single bits, exhaustive low-22 and top-22 words, every MSB position ×1024, 50M randoms). Note the dead body uses (unsigned long long)mask >> 1 (flsll.c:45) while the live inline delegates through (long) — output-identical on every tested input, as expected on LP64.
4. Consumer census (why this is Info, not higher). Live consumers: sys/vfs/tmpfs/tmpfs_vnops.c:1952 (max(32, flsll(tmp->tm_pages_max * PAGE_SIZE) + 1)) and sys/dev/drm/include/linux/log2.h:133. Both resolve to the inline; none references the dead object. No memory operands — overflow/ guard-page classes vacuous.
5. Fix. fix.diff: #if !defined(HAVE_INLINE_FLSLL) gate. Validated: gated file compiles kernel-style, 0 global flsll 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-5716 (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.