fix(core): close the proof-lint hole in punktfunk-core — the ABI contract, stated once

146 sites, 141 of them in `abi.rs`, the `extern "C"` surface `cbindgen` turns into
`punktfunk_core.h`. Writing 141 independent arguments would have been the wrong answer and would
have read like it: they are instances of ONE contract in six shapes — opaque handles reached only
through `as_mut()`/`as_ref()` (so null becomes a status, never a dereference), caller-owned
out-params (null-checked exactly where the header calls them optional), NUL-terminated-or-null C
strings through `opt_cstr`, unchanged forwarding to a versioned entry point, fixed-length output
buffers, and `addr_of!` reads.

So the contract is stated once at the top of the file, the way `pf-win-display`'s CCD contract is,
and each site says which instance it is. Two properties that hold everywhere are stated there and
not repeated 141 times: no pointer is retained past the call that received it, and every entry point
runs inside `guard`'s `catch_unwind`, so a panic becomes a status code instead of unwinding into C.

The `addr_of!` sites got a real proof rather than a shape, because that one is load-bearing and
non-obvious: it forms a raw pointer WITHOUT creating a reference precisely because the caller's
struct may be an older, smaller version, so the field must be read by offset and not through a `&`.

`transport/udp/linux.rs`'s five are genuinely individual — two `zeroed()` POD initialisations, and
the `sendmmsg`/`recvmmsg`/`CMSG` trio, where the argument worth writing down is that
`msg_controllen` is set to `CMSG_SPACE(size_of::<u16>())` and the `CmsgBuf` is 64 bytes, so the
kernel cannot write past the control buffer.

punktfunk-core now denies `undocumented_unsafe_blocks`. Verified: Linux .21 fmt + both CI clippy
steps rc=0, and — since this is the C surface and comments alone should not change it — the C ABI
harness still passes, 4 frames round-tripped byte-exact through lossy loopback.
This commit is contained in:
2026-07-29 08:48:42 +02:00
parent e1ddd49e37
commit dda9ed1aa2
3 changed files with 381 additions and 0 deletions
File diff suppressed because it is too large Load Diff
+4
View File
@@ -33,6 +33,10 @@
//! Nothing in the per-frame path touches an async runtime. `tokio`/`quinn` are gated
//! behind the off-by-default `quic` feature and used only for the control plane.
// Unsafe-proof program: every `unsafe {}` / `unsafe impl` in this crate carries a `// SAFETY:`
// proof. The bulk lives in `abi.rs`, whose sites are instances of the ABI contract stated once at
// the top of that file rather than 141 independent arguments.
#![deny(clippy::undocumented_unsafe_blocks)]
#![forbid(unsafe_op_in_unsafe_fn)]
pub mod abi;
@@ -42,6 +42,8 @@ use libc::{mmsghdr, recvmmsg, sendmmsg};
fn mmsghdrs(iovs: &mut [libc::iovec]) -> Vec<mmsghdr> {
iovs.iter_mut()
.map(|iov| {
// SAFETY: `mmsghdr` is a `repr(C)` POD of scalars and pointers, so all-zeroes is a
// valid bit pattern; every field the kernel reads is assigned right below.
let mut h: mmsghdr = unsafe { std::mem::zeroed() };
h.msg_hdr.msg_iov = iov;
h.msg_hdr.msg_iovlen = 1;
@@ -123,9 +125,15 @@ fn send_one_gso(fd: libc::c_int, buf: &[u8], gso_size: u16) -> std::io::Result<(
bytes: [u8; 64],
}
let mut control = CmsgBuf { bytes: [0u8; 64] };
// SAFETY: `msghdr` is a `repr(C)` POD of scalars and pointers, so all-zeroes is a valid bit
// pattern; every field the kernel reads is assigned below before the call.
let mut msg: libc::msghdr = unsafe { std::mem::zeroed() };
msg.msg_iov = &mut iov;
msg.msg_iovlen = 1;
// SAFETY: `control` and `iov` are locals that outlive the call. `msg_controllen` is set to
// `CMSG_SPACE(size_of::<u16>())`, which the 64-byte `CmsgBuf` covers, so the kernel cannot write
// past it; `CMSG_FIRSTHDR`/`CMSG_DATA` are the documented accessors for that buffer and the
// header they return is checked for null before it is written through.
let rc = unsafe {
msg.msg_control = control.bytes.as_mut_ptr() as *mut libc::c_void;
msg.msg_controllen = libc::CMSG_SPACE(std::mem::size_of::<u16>() as u32) as _;
@@ -162,6 +170,9 @@ pub(super) fn send_batch(t: &UdpTransport, packets: &[&[u8]]) -> std::io::Result
})
.collect();
let mut hdrs = mmsghdrs(&mut iovs);
// SAFETY: `fd` is the live socket, and `hdrs` is a local slice of `mmsghdr` whose length
// is passed alongside it; each header points at an `iov` in `iovs`, which outlives the
// call. The kernel only reads the buffers and writes each header's `msg_len`.
let n = unsafe { sendmmsg(fd, hdrs.as_mut_ptr(), hdrs.len() as libc::c_uint, 0) };
if n < 0 {
let err = std::io::Error::last_os_error();
@@ -250,6 +261,9 @@ pub(super) fn recv_batch(
})
.collect();
let mut hdrs = mmsghdrs(&mut iovs);
// SAFETY: `fd` is the live socket, and `hdrs` is a local slice of `mmsghdr` whose length is
// passed alongside it; each header points at an `iov` backed by a buffer in `bufs`, which
// outlives the call, so the kernel writes only inside those buffers.
let n = unsafe {
recvmmsg(
fd,