# DF-2303 — latent negative-length bcopy in fwohci_arcv split-header pullup

## What this is
Verification pack for finding DF-2303 (`sys/bus/firewire/fwohci.c:2729-2735`).
Low / speculative, latent memory-corruption landmine. Claim: in the
split-header reassembly path, `rlen` is recomputed as
`sizeof(pktbuf) - rlen` (fwohci.c:2732); if the previous-buffer fragment
exceeded sizeof(pktbuf)=16 the new rlen goes negative and the diagnostic
at 2733-2734 does NOT skip the following `bcopy(db_tr->buf, p, rlen)`
(fwohci.c:2735), whose negative int becomes a huge size_t.

## Verdict (short)
NOT REPRODUCIBLE FROM PACKET INPUT — and the battery proves it; the
landmine itself is REAL and catastrophic when the state is injected:

* (A) Reachability battery (run.log): every header straddle the real
  parser can produce was driven through the REAL fwohci_arcv
  split-header path (firewire_debug on, "rlen=%d, offset=%d" printed
  by the real code at fwohci.c:2721-2723):
    WREQB (16B hdr): F = 4, 8, 12 -> rlen_old = 4/8/12
    WRES  (12B hdr): F = 4, 8     -> rlen_old = 4/8
  All rlen_new = 16 - rlen_old in [4,12] > 0. No "why rlen < 0".
  Guest up after all runs.
* (B) Impossible-state injection (run2303b.log, panic.txt): with
  buf_offset forced to -(4096-24) (rlen_old = 24 > 16 — a state no
  packet stream can produce), the real code printed "why rlen < 0"
  and the very next bcopy hit the stack guard page:
  `panic: vm_fault: fault on stack guard` with memmove in the trace —
  the negative-length bcopy is a live stack-smash primitive.

## Why rlen_old > 16 is unreachable (line-accurate invariant)
1. buf_offset becomes negative ONLY at fwohci.c:2762
   (`buf_offset = -buf_offset`), immediately after fwohci_arcv_swap
   returned -hlen (hlen > len) for a parse at position X in buffer N
   (buf_offset = ld - buf = X at that point, set by fwohci.c:2800).
2. At out: (fwohci.c:2855) if resCount != 0, line 2871 OVERWRITES
   buf_offset with a positive value, destroying the split state — so
   the split-header branch (2712ff) is entered only when resCount
   was 0, i.e. the buffer was full and len at the failing parse was
   psize - X = rlen_old.
3. The parse failed with hlen > len, and hlen = tinfo[tcode].hdr_len
   <= 16 for every tcode arcv_swap accepts (fwohci.c:2601-2617);
   therefore rlen_old < hlen <= 16 whenever the state survives.
   Additionally every AR packet consumes a multiple of 4 bytes
   (12/16-byte headers + 4-byte trailer + quadlet-rounded payloads)
   and fwohci_arcv_swap has no STREAM case (tcode 0xa rejected,
   "Unknown tcode 10"), so F is quadlet-aligned: the battery set
   {4,8,12} is the complete reachable space for a 4096-byte buffer.

The battery mechanically confirms each element of the invariant
("split header" print, "rlen=F, offset=-X" print, clean completion).

## Fix
fix.diff turns the diagnostic into a guard (drop + goto out). A/B
validated: the SAME injected state on the fixed kernel prints the
drop message and survives instead of panicking.

## Reachability honesty
As filed: latent/unreachable today. The finding text itself says
"currently unreachable ... latent landmine if control flow changes" —
this verification upgrades that claim from speculation to mechanical
proof (battery + invariant + demonstrated consequence).