Consolidate the futex syscall contract surface

Start with the four contract headers under src/proved/, the _UNPROVED entries in mk/verify.mk, and the assertions and comments in src/runtime/futex.c. Run frama-c-mcp check src/proved/futexreq.h, then make verify using the pinned .github/actions/framac toolchain. Done means the nine contracts have documented total-versus-conditional decisions, syscall-level invariants are stated, and any resulting proved fragments are registered and verified without runtime changes.

Filed to hold the place for what @jserv asked for in
https://github.com/sysprog21/elfuse/pull/350#discussion_r3913005274:

You should consolidate contracts for futex system call. See
Model Checking Futexes
and utilize frama-c-mcp to proceed.

#350 took the piece that belonged to the change in front of it — the requeue
counts, now src/proved/futexreq.h — and left the rest. This is the rest.

Where the contracts stand

Four targets cover this syscall today, 160 obligations across 9 functions, all
discharging on Frama-C 33.0 with Alt-Ergo 2.6.3 and Z3 4.16.0:

target	functions	goals
futexhash	futex_bucket_index	5
futexop	futex_op_sign_extend12, futex_op_shift_arg_mask	13
futexdeadline	futex_remaining_ns, futex_quantum_deadline, linux_timespec_is_valid, futex_uaddr_is_aligned	128
futexreq	futex_requeue_counts_valid, futex_requeue_budget	14

Each was split out for its own local reason, and each is sound. What they have
in common is the shape of what they leave out. The four _UNPROVED lines in
mk/verify.mk say the same thing in four wordings:

• futexhash: the queue walks around it stay test-covered
• futexop: the wake and requeue walks around them stay test-covered
• futexreq: the bucket walk the budget bounds stays test-covered
• futexdeadline: futex_make_deadline, which reads the guest

So the proved surface is leaf arithmetic over guest-supplied words, and the
thing every fragment defers is the same thing: the queue and bucket state the
walks maintain. src/runtime/futex.c has 14 futex_* functions and 27 sites
that answer EINVAL or EAGAIN; the contracts reach a handful of them.

That is the consolidation. Not merging four headers into one file — stating the
invariants that span them, which none of the four is positioned to state alone.

What the paper gives us, and what it does not

Worth being precise, because the two formalisms are not doing the same job.

Evrard and Donaldson, SPIN 2023, model futex-based mutex and condition
variable implementations in Promela and check safety properties with Spin.
They find bugs that affected real implementations and confirm current ones. The
models are open source and offered as a template for verifying new primitive
designs.

It is a model of the userspace protocols built on top of the futex API, not
of a kernel-side implementation of it. So it does not hand us ACSL for
futex_requeue. What it does hand us is the other half: the properties those
protocols rely on the API to hold, which is exactly the register the current
fragments are missing. A per-function WP proof cannot say "a waiter this call
enqueues is either woken or still queued when it returns"; that is a statement
about the syscall, and the paper is where the list of such statements comes
from.

Concretely that suggests two different tools for two different halves, rather
than pushing WP where it does not reach:

• WP/ACSL keeps the sequential arithmetic, as now.
• The concurrent claims — no lost wakeup, no waiter counted to no bucket, the
  published census never understating the chain — want a model, and Spin is the
  one the paper already validated for this domain.

The census invariant is not hypothetical here: futex_wake carries an
ELFUSE_CONTRACT_ASSERT block that re-reads before believing a violation,
precisely because it cannot see the chain and os_sync_waiters in one instant.
That comment is a specification written in prose in a runtime assert.

A first concrete question, already asked by the tool

frama-c-mcp check src/proved/futexreq.h returns incomplete, with
VALID_UNDER_HYP: 5 and EVA_NOT_RUN: 1.

Neither is a defect. The five are the goals holding under
futex_requeue_budget's precondition, which is what makes it a conditional
contract, and EVA has not been run because the target is WP-only. But "should
the budget contract be conditional or total" is a real design question, and the
same question exists for every fragment: futex_bucket_index is total,
futex_op_shift_arg_mask is total, futex_remaining_ns is not. Nothing today
says which of those is deliberate.

So the first pass is a survey, not a rewrite: for each of the 9 proved
functions, is the contract total or conditional, and is that a decision or an
accident?

Scope

In:

• one statement of the syscall-level invariants, sourced from the paper's
  properties and from the prose already in futex.c's asserts and comments
• a survey of the 9 existing contracts for total-vs-conditional, with the
  answers written down
• whatever new proved fragments fall out, registered the existing way
• EVA in the loop where it adds something WP alone does not

Out, unless someone asks:

• rewriting the four headers into one file for its own sake
• changing runtime behaviour; this is about what is stated, not what runs
• a Promela model in-tree, until there is a claim worth checking with one

Notes for whoever picks it up

.github/actions/framac pins the toolchain: Frama-C 33.0, Alt-Ergo 2.6.3, Z3
4.16.0, in a switch named frama-c-elfuse. Creating that switch locally with
the same pins makes make verify the same run as CI's; the whole suite is 1093
of 1093 across 23 targets in about a minute on an M-series machine.

frama-c-mcp installs into that switch and registers itself with Claude Code
and codex. Its check <file> subcommand is the part meant to be run by hand.