# DF-0710 PoC: sco_input infinite loop (while vs if)

## Bug
`sys/netbt/sco_socket.c:221-222` uses a `while` loop where the sibling BT
socket implementations use a one-shot `if { drop; return; }`
(`sys/netbt/l2cap_socket.c:231`, `sys/netbt/rfcomm_socket.c:241`):

```c
while (m->m_pkthdr.len > sbspace(&so->so_rcv))
    sbdroprecord(&so->so_rcv.sb);
```

If an inbound SCO packet exceeds `sco_recvspace` (4096, `sco_socket.c:81`) and
the receive buffer cannot free enough room (including the empty-buffer case),
`sbdroprecord` on an empty buffer is a no-op (`uipc_sockbuf.c:524`, `if (m)`),
`sbspace` never grows, and the loop never exits. The Bluetooth protocol thread
spins at 100% CPU forever. Pure DoS — nothing is corrupted.

## Reachability on the audit guest — UNREACHABLE LIVE
`sco_input` is driven only by `hci_sco_recv` (`sys/netbt/hci_link.c:867`),
which fires from a real Bluetooth controller's RX path. The guest has:
- no `options BLUETOOTH` in `X86_64_GENERIC` (so `sco_input` is not in the
  running kernel),
- `netbt.ko` present but not loaded,
- no Bluetooth controller (no PCI/USB BT device).

The original live PoC `sco_input_hang` therefore fails with
`socket: Protocol not supported`. The bug is reproduced instead by the
deterministic code-level harness `sco_input_logic.c`, which models the exact
kernel primitives (`sbspace` macro, `sbdroprecord` no-op-on-empty,
`sco_recvspace=4096`). See `VERDICT.md` for the full source trace and the
machine-code (netbt.ko before/after) confirmation.

## Reproduce
```
./build.sh && ./run.sh
```

## Expected
- `sco_input_logic`: 4 of 6 oversize cases print
  `BUGGY(while): iters=100000 *** WOULD LOOP FOREVER ***` while
  `FIXED (if): iters=1 (dropped packet)`; the 2 control cases (small /
  exactly-fitting packet) terminate on both. Exit 0 = bug demonstrated.
- `sco_input_hang` (live): `socket: Protocol not supported` (documents live
  unreachability).

## Fix
`fix.diff`: change `while` to `if { m_freem(m); return; }` (matches l2cap/rfcomm).
Validated by building `netbt.ko` before/after: baseline `sco_input` has a
**backward** branch `5b2: jg 581` (the loop); patched has only a **forward**
branch `635: jg 660` (one-shot drop) and no backward branch. Both compile clean
with `-Werror`.