fix(vdisplay): the three hardest FFI calls were exempt from the crate's own unsafe-proof rule

`#![deny(clippy::undocumented_unsafe_blocks)]` cannot see an unsafe operation that
sits directly in an `unsafe fn` body — in edition 2021 `unsafe_op_in_unsafe_fn` is
allow-by-default, so a bare call inside such a body needs no block and therefore
carries no proof. The file headers claim "every unsafe block carries a SAFETY
proof", and that was true; it just did not cover the calls that needed it most.

Turning the lint on named exactly three: `DeviceIoControl` and the `ioctl` wrapper
in pf_vdisplay.rs — the whole host<->driver control channel — and
`restore_displays_ccd` in manager.rs, the call the teardown path depends on to give
the operator their physical panels back. Each now carries a real proof, and `ioctl`
and `set_render_adapter` grew the `# Safety` heading their callers were owed.

Also teaches scripts/wincheck.sh to cover pf-vdisplay, which is what let the above
be compile-verified rather than reasoned: the crate's Windows half is ~3,400 lines
that Linux CI never compiles. That needed a stub pf-encode (the real one drags
ffmpeg-sys, and the admission gate calls exactly one predicate from it) and
CompositorPref on the stub core. Verified non-vacuous with a planted type error.

pf-win-display's half of the same lint is a separate change — it flags 62 further
operations, and they want proofs written one at a time, not in bulk.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-07-28 19:45:11 +02:00
co-authored by Claude Opus 5
parent 9b38b6a22d
commit 995cac5d03
4 changed files with 115 additions and 24 deletions
+59 -7
View File
@@ -21,13 +21,19 @@
# Both enter the graph through `punktfunk-core`'s `quic` feature. Stubbing opus with a fake
# `opus.pc` gets past audiopus but not ring.
#
# The whole Windows capture stack uses exactly TWO items from punktfunk-core — `quic::HdrMeta` and
# `Mode`, both plain data (re-verify with:
# `grep -rho 'punktfunk_core::[A-Za-z_:]*' crates/pf-capture/src crates/pf-frame/src crates/pf-win-display/src | sort -u`).
# So this script generates a ~30-line stub core carrying just those, and rustls/ring/opus never
# The whole Windows capture stack uses exactly FOUR items from punktfunk-core — `quic::HdrMeta`,
# `Mode`, `CompositorPref` and its `as_str`, all plain data (re-verify with:
# `grep -rho 'punktfunk_core::[A-Za-z_:]*' crates/pf-{capture,frame,win-display,vdisplay}/src | sort -u`).
# So this script generates a ~50-line stub core carrying just those, and rustls/ring/opus never
# enter the graph at all. Every path dep that is NOT a generated member points at the REAL crate by
# absolute path, so their own relative deps and `version.workspace` inheritance still resolve.
#
# pf-encode is stubbed for the same reason and needs the same care: pf-vdisplay's admission gate
# calls exactly ONE item from it (`can_open_another_session`, admission.rs), but the real crate
# drags ffmpeg-sys — whose build script wants a Windows FFmpeg tree this box does not have. The
# stub is a `cfg(windows) -> bool`; if admission ever consults a second encoder fact, mirror it
# here or the cross-check stops covering that call.
#
# Note: `cargo fmt` needs none of this — rustfmt follows `mod`/`#[path]` without evaluating cfg, so
# it already reaches Windows-only files. Mechanical edits can be normalised with plain `cargo fmt`.
set -euo pipefail
@@ -40,8 +46,8 @@ TARGET=x86_64-pc-windows-msvc
# dep naming one of these must stay RELATIVE (resolving to the generated member); anything else is
# rewritten to the real crate. Getting that backwards silently drags the real punktfunk-core — and
# with it ring and opus — back in through pf-frame, which is the entire thing this avoids.
MEMBERS_RE='punktfunk-core|pf-frame|pf-win-display|pf-capture'
REAL_MEMBERS=(pf-frame pf-win-display pf-capture)
MEMBERS_RE='punktfunk-core|pf-encode|pf-frame|pf-win-display|pf-capture|pf-vdisplay'
REAL_MEMBERS=(pf-frame pf-win-display pf-capture pf-vdisplay)
cmd="${1:-clippy}"
[ $# -gt 0 ] && shift
@@ -71,7 +77,7 @@ mkdir -p "$OUT"
echo '# GENERATED by scripts/wincheck.sh — do not edit; re-run the script.'
echo '[workspace]'
echo 'resolver = "2"'
echo 'members = ["punktfunk-core", "pf-frame", "pf-win-display", "pf-capture"]'
echo 'members = ["punktfunk-core", "pf-encode", "pf-frame", "pf-win-display", "pf-capture", "pf-vdisplay"]'
echo
echo '[workspace.package]'
sed -n '/^\[workspace\.package\]/,/^$/p' "$REPO/Cargo.toml" | sed '1d;/^$/d'
@@ -108,6 +114,30 @@ pub struct Mode {
pub refresh_hz: u32,
}
/// Mirrors `punktfunk_core::CompositorPref` (config.rs). pf-vdisplay matches on every variant and
/// calls `as_str`, so both the variant set and the strings must stay in step with the real enum.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Default)]
pub enum CompositorPref {
#[default]
Auto,
Kwin,
Wlroots,
Mutter,
Gamescope,
}
impl CompositorPref {
pub fn as_str(self) -> &'static str {
match self {
CompositorPref::Auto => "auto",
CompositorPref::Kwin => "kwin",
CompositorPref::Wlroots => "wlroots",
CompositorPref::Mutter => "mutter",
CompositorPref::Gamescope => "gamescope",
}
}
}
pub mod quic {
/// Mirrors `punktfunk_core::quic::HdrMeta`.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Default)]
@@ -122,6 +152,28 @@ pub mod quic {
}
EOF
mkdir -p "$OUT/pf-encode/src"
cat > "$OUT/pf-encode/Cargo.toml" <<'EOF'
# GENERATED by scripts/wincheck.sh — a STUB, not the real crate.
[package]
name = "pf-encode"
version.workspace = true
edition = "2021"
rust-version.workspace = true
EOF
cat > "$OUT/pf-encode/src/lib.rs" <<'EOF'
//! GENERATED by scripts/wincheck.sh — a STUB of pf-encode carrying only the one item pf-vdisplay's
//! admission gate uses. The real crate pulls ffmpeg-sys, whose build script needs a Windows FFmpeg
//! tree; nothing in the display path needs the encoder itself, only this predicate.
/// Mirrors `pf_encode::can_open_another_session` (lib.rs, `#[cfg(target_os = "windows")]`).
#[cfg(target_os = "windows")]
pub fn can_open_another_session() -> bool {
true
}
EOF
for name in "${REAL_MEMBERS[@]}"; do
mkdir -p "$OUT/$name"
# Park the member paths behind a sentinel first: a plain self-substitution would be a no-op and