#277 Add machine-checked proofs for critical arithmetic paths

Summary by cubic

Adds machine-checked proofs across key arithmetic paths (sendmsg cmsg walk, FUSE reply frames, initial stack layout, netlink TLVs, sockaddr reshape, signal frame placement, GVA) and gates them in CI with a mutation test suite. Also tightens process management, path handling, and memory sync behavior.

• New Features

  • Proved headers and targets: src/core/stack-math.h (verify-stack), src/syscall/cmsg-math.h (verify-cmsg), src/syscall/fuse-math.h (verify-fuse), src/syscall/netlink-math.h (verify-netlink), src/syscall/sigframe-math.h (verify-sigframe), src/syscall/sockaddr-math.h (verify-sockaddr), src/core/gva-math.h (verify-gva).
  • GVA call-site checks: runtime contract asserts behind -DELFUSE_CONTRACT_ASSERT plus tests/test-gva-contracts.c; make check-contracts builds and runs them.
  • CI: proofs are gating (make verify) and verify-mutants runs per target; adds ACSL coverage, plain-char signedness, and mutant-matrix sync checks; trims prover timeout for mutants.
  • Wire ABI split: syscall/linux-wire.h (errno/flags/structs/FD table) and syscall/linux-limits.h (size limits) separated from syscall/abi.h (dispatch only).

• Bug Fixes

  • Netlink: fixed receive hang from uint32 wrap; TLV walks now proved and use aligned span math.
  • Process management: guard host PID reuse by matching (host_pid, guest_pid) after relock; shrink proc table when fully idle; treat host_reap_pending as live.
  • FUSE: clamp negotiated max_write by max_pages; switch node-ref lookups to an open-addressed hash.
  • msync: defer fsync outside mmap_lock on duped fds; size scratch arrays under lock.
  • Paths and I/O: add path_tr_nofollow(); route no-sysroot fast path through tx.host_path; table-driven /proc virtual dirs; report real read(2) errors during sysroot probing; fix double-negated errno in slab restore.
  • Fork IPC: close received host fds when a guest_fd is out of range.