docs(host): prove every unsafe block in the Linux FFI files + gate them (unsafe-proof program 2/N)

Continues the structural unsafe-proof program (every unsafe carries a documented
proof of soundness; the file gains #![deny(clippy::undocumented_unsafe_blocks)]
so it stays proven). This batch covers all 10 remaining pure-Linux files
(104 blocks), each proof stating the REAL invariant — not boilerplate:

  zerocopy/cuda.rs (26)   leaked process-lifetime libcuda fn-ptr table; opaque
                          CUcontext never dereferenced; free-exactly-once via the
                          Arc<Mutex<PoolInner>> ownership graph; dmabuf fd take/close split
  zerocopy/egl.rs (18)    eglGetProcAddress'd procs with the GL context current;
                          EGLImage liveness; the two-call modifier-query bounds
  zerocopy/vulkan.rs (4)  copy-bounds arithmetic (src_size>=span); Send = thread
                          confinement to the punktfunk-pipewire thread
  dmabuf_fence.rs (4)     poll/ioctl/close fd liveness + ownership
  capture/linux/mod.rs (16)  spa_data repr(transparent) cast; null-checked spa
                          derefs; single-loop-thread buffer ownership until requeue
  inject/linux/gamepad.rs (10)  uinput ioctl request-number ↔ struct-size match
                          (static-asserted); InputEventRaw no-padding for the byte cast
  encode/linux/vaapi.rs (15) + encode/linux/mod.rs (9)  ffmpeg object ownership/
                          free ladders; VAAPI/DRM graph; Send = single-thread transfer
  inject/linux/wlr.rs (2), vdisplay/linux/kwin.rs (1)

No memory-unsafety SUSPECT blocks were found — the unsafe is sound. The vaapi
agent did flag two real AVBufferRef *leaks* (not UB) in DmabufInner::open; marked
inline with NOTE(leak) and addressed in a follow-up.

Verified: cargo clippy -p punktfunk-host --all-targets -- -D warnings is clean
(each file's deny gate hard-errors on any undocumented block).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-06-26 09:00:30 +00:00
parent 22359f5dc8
commit ba68a98873
10 changed files with 631 additions and 6 deletions
@@ -15,6 +15,8 @@
//! the KWin session's environment.
#![allow(clippy::all, dead_code, non_camel_case_types, non_snake_case, unused)]
// Every `unsafe` block in this file carries a `// SAFETY:` proof; enforce it (unsafe-proof program).
#![deny(clippy::undocumented_unsafe_blocks)]
use super::{Mode, VirtualDisplay, VirtualOutput};
use anyhow::{anyhow, bail, Context, Result};
@@ -495,6 +497,11 @@ fn run(
events: libc::POLLIN,
revents: 0,
};
// SAFETY: `&mut pfd` points at a single live, fully-initialized `libc::pollfd` on the stack, and
// the count `1` matches that one-element array, so `poll` reads `fd`/`events` and writes `revents`
// strictly within `pfd`. `pfd.fd` is the Wayland connection's fd, valid because `conn` (and the
// `prepare_read` guard) are alive across the call. `poll` blocks up to 200 ms and writes only
// `revents`; `pfd` outlives the synchronous call and aliases nothing (a fresh local).
let r = unsafe { libc::poll(&mut pfd, 1, 200) };
if r > 0 && (pfd.revents & libc::POLLIN) != 0 {
let _ = guard.read();