Files
punktfunk/crates/punktfunk-host
enricobuehler 22359f5dc8 docs(host): prove every unsafe block in drm_sync.rs + gate it (unsafe-proof program 1/N)
Start of the structural unsafe-proof program (per the "every unsafe needs a
documented proof of soundness" goal): each `unsafe` block gets an accurate
`// SAFETY:` proof of WHY it is sound, and the file gains
`#![deny(clippy::undocumented_unsafe_blocks)]` so the proof requirement is
permanently enforced (a future undocumented unsafe in this file fails CI).

drm_sync.rs (10 blocks: libc open/ioctl/clock_gettime/close + 3 in tests): each
proof states the real invariant — fd liveness/ownership, the ioctl request number
encoding the matching struct size, the `&mut req` being a live correctly-sized
`#[repr(C)]` struct, and (for the timeline ioctls) the `handles`/`points` arrays
outliving the synchronous call with `count_handles` matching their length.

The gate grows file-by-file (CI stays green; undone files don't carry the lint
yet); it promotes to a crate-root deny once every file is done. ~122 Linux blocks
+ the Windows files remain.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-26 08:35:32 +00:00
..