CI red for two weeks: once-cells on the solver path, and a lint that could not tell code from prose

What broke

CI has been red on main since 2026-08-16 on Check for locking primitives. The runs before
that were red too, for other reasons -- mdformat on 08-11, tests on 08-08 -- so the branch has not
been green for about two weeks and each new failure replaced an older one rather than being noticed.

The lock lint fired on three once-cells:

src/hir/check/raw.rs:    static Z3: std::sync::OnceLock<bool>      (a9612685, Vx#353 A2)
src/hir/solver.rs:       static AVAIL: OnceLock<Availability>      (d4a8b545, Vx#374)
src/hir/solver.rs:       static ALLOWED: OnceLock<bool>            (d4a8b545, Vx#374)

None of them was about solver policy. All three were memoization: do not spawn z3 --version once
per proof obligation.

Why the memo was not needed at all

Every caller reaches the solver module from the ErrorKind::NotFound arm of its OWN
Command::new("z3").spawn() -- prover.rs:46, seam.rs:217, seam.rs:334. By the time it asks
"is z3 available", the answer is already established and the OS's own error string is in hand. A
second z3 --version spawn could only confirm it, with a less accurate reason.

And require() was a no-op at all three sites: each one wrote

crate::hir::solver::require()?;
return Err(crate::hir::solver::missing_message(&e.to_string()));

so the Ok path fell through to an Err anyway. The two branches differed only in which reason
string they carried, and the fallthrough's was the better one -- it came from the real spawn rather
than from a separate probe.

raw.rs's copy was worse than redundant, in two ways. It disagreed with solver.rs -- it asked
only whether the process SPAWNED, so a z3 that started and exited non-zero counted as available
there and missing here -- and its stated reason had expired: "The prover fails OPEN without z3,
which would turn every bounds obligation into a silent yes". Vx#374 made the prover fail CLOSED two
days later, so the guard was compensating for behaviour that no longer exists.

Done

• Deleted Availability, probe(), availability() and require(). What remains is
  missing_message() and unverified_allowed(), the latter a plain environment read with nothing
  cached: it is reached only after a spawn has already failed, or once per relaxed transfer edge,
  so there is no hot path to protect.
• Deleted raw.rs::z3_available() and its guard.
• No atomics were used as a replacement. An earlier attempt did use them -- AtomicPtr for the
  probe and AtomicU8 for the flag -- and that was the wrong answer to the right complaint: it
  satisfies the lint while keeping the shared mutable state the lint exists to prevent.

Behaviour is unchanged and still pinned by tests/integration_test/solver_policy_test.rs, which
runs vxc with a stripped PATH: with_a_solver_the_obligation_is_decided,
without_a_solver_the_build_fails_rather_than_claiming_success,
opting_out_compiles_but_says_so_every_time. 494 lib and 235 integration tests pass.

New lint: process-global atomics

Banned for the same reason as locks. A compilation must be isolated, and a static a worker can
write is shared mutable state whether or not it takes a lock to reach it. A cached answer also
outlives the compilation that produced it in a long-lived process such as the LSP daemon, so
compile N+1 can read what compile N left behind.

Matched on the type names, not the word "atomic", because the word appears in prose --
/// **Atomic**: returns false and leaves the stream untouched in flatten.rs is a doc comment
about all-or-nothing lowering. That is the same false-positive class that made the lock lint fail
on a doc comment that merely NAMED a once-cell while explaining why it had been removed.

Exemptions are per line, vx-lint: allow-atomic with a reason, so a new one has to justify itself
in the diff rather than inheriting a file-wide exclusion.

Remaining holdout

src/intern_mode.rs -- four lines: the interning-mode knob, the quiet flag, and the phase-timer
array. All of it is EVAL-ONLY measurement scaffolding (the file's own header says so): which mode a
benchmark run selected, whether phase logging is on, and where the wall time went. None of it is
read by the compiler to decide what to emit, so none of it can make one compilation's output depend
on another's.

PHASE_NANOS is the one with no cheap alternative: it is accumulated from inside the parallel
regions being timed, so there is no per-worker place to put it. Removing it means per-worker
counters merged at the barrier, which is a real change to the harness that reports the scaling
numbers -- worth doing deliberately rather than as a side effect of a lint. Tracked here.

Start with src/hir/check/raw.rs, src/hir/solver.rs, prover.rs, and seam.rs, then read tests/integration_test/solver_policy_test.rs. Verify the listed solver-policy tests with a stripped PATH and inspect the lint behavior around type-name matching and per-line exemptions. Done means the obsolete availability paths and raw.rs guard are gone, process-global atomics are rejected without prose false positives, and the named tests pass.