Add tokio-rs/loom concurrency harnesses for Atomic, RingBuf, PriorityQueue primitives

[avrabe]

Part of the V&V coverage initiative.

Problem

gale has strong Lean proofs for concurrency primitives (proofs/lean/RingBuf.lean — 9 invariants on the index arithmetic; proofs/lean/Atomic.lean, PriorityQueue.lean, PriorityCeiling.lean). Those are mathematical proofs of the abstract models. What's missing: tokio-rs/loom permutation-checking of the actual Rust implementations under every possible thread interleaving.

This is the same technique thrum/crates/thrum-db/tests/loom_claims.rs uses today — but gale has more concurrency-critical code and no loom coverage.

Note: tokio-rs/loom is the crate loom = "..." in Cargo.toml — not this project's sibling pulseengine/loom (WASM optimizer). Disambiguate carefully.

Acceptance

• Add loom as a dev-dependency with feature-gated #[cfg(loom)] import pattern
• tokio-loom harness for Atomic primitives: compare-and-swap ordering, fence correctness
• tokio-loom harness for RingBuf: single-producer/single-consumer and multi-producer variants across every interleaving
• tokio-loom harness for PriorityQueue: concurrent push/pop cannot produce invalid heaps
• Harnesses under tests/loom_<primitive>.rs, gated with RUSTFLAGS="--cfg loom" in CI
• New CI job runs loom harnesses separately from main tests (they can be slow)
• Traceability in rivet.yaml: link loom harnesses to the Lean invariants they operationalize

Notes

• Lean proves the mathematical model; loom proves the Rust impl respects it under concurrency
• loom dramatically increases runtime — keep harnesses small and focused
• Reference implementation: thrum/crates/thrum-db/tests/loom_claims.rs