model the cluster peer connection map for issue 140

[fabracht]

Summary

A TLA+ model of the QUIC peer-connection map, written as the design step for #140. No production code changes.

• models peers: HashMap<NodeId, PeerConnection>: two insert sites under the same key, so an insert replaces and drops the displaced connection's send stream, while each detached receiver task outlives the replacement
• _current reproduces today's behaviour: a dead peer stays in the map forever, so direct_peers() reports it as linked and the mesh warning goes quiet exactly when it should fire
• _naive refutes the obvious fix: removing by key when a receiver task ends drops a link whose send side still works, and on a reconnect deletes the newer entry
• _guarded refutes the compare-and-remove fix too: the guard asks whether the slot is still mine, not whether the link is dead, so it also removes a healthy connection
• conclusion recorded in the spec header: receiver exit is the wrong removal trigger, since a receiver ends whenever the remote drops its send stream, which happens on every replacement

The header also records what the model cannot settle: no async implementation can satisfy InvNoDeadLink, because a break and its cleanup are separate events; and guarded removal without a re-dial turns a stale entry into a permanently absent one, which the safety invariants cannot distinguish from a fix.

Test plan

• validate_spec parses the spec and detects all three invariants
• _current: InvNoDeadLink violated, full state space
• _naive and _naive_livedrop: InvNoLiveDrop violated
• _guarded and _guarded_livedrop: InvNoLiveDrop violated, refuting the guarded fix
• model fidelity checked against quic_transport.rs and the quinn source by two independent reviewers; RecvStream::drop calling stop() and SendStream::drop calling finish() verified directly
• cargo make test: 24 suites, 1200 passed, 0 failed

[fabracht]

Closing without merging.

A multi-reviewer audit found that the spec's documentation misdescribes the code in places, and that the committed configurations cannot reproduce the table in the spec header — TLC halts at the first violation, so the naive and guarded configs never evaluate the invariant the header reports for them, and that invariant is vacuous under the current config.

The SendBreaks action is also justified incorrectly: it is documented as modelling RecvStream::drop calling stop() on our send stream, but Drop early-returns when all_data_read is set (quinn src/recv_stream.rs:511-523), and the FIN path sets that flag, so stop() is not called on the paths the argument relies on.

Reworking it is possible — a combined connection-failure action, corrected configurations, corrected prose — but the result would still be a single-node, single-peer, safety-only model, and the questions #140 actually turns on are cross-node and liveness-shaped: contagion between two nodes' maps, oscillation without backoff, and telling a converged mesh from an emptied one. A model that answers the easy question more rigorously while staying silent on the hard one is not worth the authority a spec in this repo carries.

The one design conclusion that survives — removing by key when a receiver task ends is wrong — was reached independently from the code by several reviewers and does not need a model to stand. It is recorded on #140, along with a correction retracting the prescription this PR's header proposed.

The investigation was not wasted: it produced #143, a live framing-corruption bug in the QUIC transport, which is the more valuable finding.