Three of Phase 5's four items; 5.4 is held for a decision (see below).
`open_device` is a SAFE fn returning an `OwnedHandle`. It never had a caller
obligation — it takes no arguments and every precondition is internal — so the
`unsafe fn` it used to be pushed a proof burden onto four call sites with nothing to
prove, and handed back a raw `HANDLE` that two of them re-owned by hand with
`CloseHandle`. That shape has already leaked once in this file (the wrap-IMMEDIATELY
comment in `open` records it). Ownership is now a `Drop`, `probe()` is
`open_device().map(|_| ())`, `is_available()` is `open_device().is_ok()`, and
`CloseHandle` is no longer imported here at all.
`resolve_target_gdi` ran the same 60 × 50 ms poll three times verbatim, and the 2nd and
3rd copies documented themselves as "SAFETY: as the resolve loop above" — a pointer to
a proof rather than a proof, which rots silently the moment the block it points at
moves. One `poll_gdi_name`, one proof, and the three-stage ladder now reads as the
three stages its doc describes.
Two proofs were simply wrong, both discharged everything except the one obligation
that mattered:
* The SetupAPI detail buffer was a `Vec<u8>` (align 1) written through as
`SP_DEVICE_INTERFACE_DETAIL_DATA_W` (align 4). The SAFETY comment proved bounds and
aliasing and was silent on alignment. Now a `Vec<u64>`. Its guard also compared the
required size against `size_of::<u32>()` while stamping
`size_of::<SP_DEVICE_INTERFACE_DETAIL_DATA_W>()` into `cbSize` — checking a different
number than the one it promises the OS.
* `GetMonitorInfoW` was handed `&mut info.monitorInfo`: `cbSize` promises 104 bytes but
that pointer's provenance covers the 40-byte `MONITORINFO` prefix, so everything the
OS writes past byte 40 — which is `szDevice`, the only field the caller reads — is out
of bounds for it. A compiler may assume those bytes were untouched and fold the zeroed
initializer into the reads, i.e. return an EMPTY device name. That name is what
`panel_off_except`'s exclusion compares against, so an empty one darkens the panel it
is meant to spare. The pointer now carries the full struct's provenance.
pf_vdisplay.rs 42 -> 34 `unsafe`, manager.rs 58 -> 56. Windows runner: clippy
--all-targets clean, 48 passed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
enricobuehlerandClaude Opus 5
029979e824