test(core): split the Era handoff Loom model into offer / accept / cancel

[dshbox-dev]

Closes #247

Summary

The ER-07 handoff model in crates/cordis-core/tests/loom_era.rs used to CAS WAITING -> DELIVERED in one step. Production (FiberHandle::era_swap) sends an EraHandoff whose EraHandoffGuard stays armed inside the offered message until EraHandoff::accept disarms it. That gives production an offered-but-not-accepted state, which the old model did not have.

• Model: a HandoffGuard value with a Drop (EraHandoffGuard, Option::take single-use) moves inside an EraOffer (EraHandoff) through a reduced oneshot slot, a loom Mutex<OfferSlot> that holds the stored offer and a receiver-dropped flag. The mutex stands in for the oneshot's send-to-receive synchronization. Tokio's oneshot internals are trusted, not modeled, and the model contains no unsafe. The oracle facts use Relaxed and are read only after the joins. (Changed in e1eb528 after maintainer review; the first revision copied Tokio's state word into an UnsafeCell.)
• Actions:
  • offer: let _ = send.send(Ok(offer)). A refused offer is dropped while still armed.
  • accept: one poll of receive.await followed by handoff.accept() in the same poll.
  • cancel: the receiver is dropped. This can land before the offer (the sender gets the offer back) or after it (the receiver releases the unaccepted offer).
• Assertions: every terminal state has exactly one owner.
  • Accepted: 0 framework cleanups.
  • Cancelled before the offer: exactly 1 guard cleanup.
  • Cancelled after the offer but before accept: exactly 1 guard cleanup.
  • The outcome must agree with the send result.
  • The positive test also asserts that all three outcomes are reached across the explored schedules.
• Negative controls:
  • offered_but_unaccepted_handoff_without_guard_cleanup_is_detected (new) treats a successful send as delivery. It fails with offered but unaccepted successor must be cleaned exactly once by its armed guard.
  • cancelled_handoff_without_framework_cleanup_is_detected is unchanged in name and message. It now disarms a refused offer.
  • cancellation_reclaiming_an_already_handed_off_successor_is_detected is re-targeted to after accept. Its message is now accepted successor cannot retain framework cleanup ownership.
• Bounds: era_model is unchanged (max_threads = 3, max_branches = 64). No test was renamed, and CI does not select any loom_era test by name.
• Docs:
  • docs/lifecycle-concurrency-modeling.md: removed the "Era offer/accept window" entry from the not-represented list, reworded the Phase 3 ER-07 handoff note and the controls bullet that follows it, and changed "twelve" to "thirteen" Era tests. The ready() bullets and LC-06 text, which Loom: model ready() publication sequence in ReadyHistoryModel (LC-06) #248 is editing, are untouched.
  • docs/lifecycle-concurrency-review-guide.md: added the new control to the ER-07 row and updated the Era test count.
• No production code or public API change.

Gates (ci/gates.sh t247)

PASS: toolchain, fmt, clippy, vocab, doc. The test, examples and latest gates were not run locally for this test/doc-only change. cargo clippy --release -p cordis-core --features loom-tests --test loom_era reports nothing for the test file.

Loom timings (local, CI commands)

• cargo test --locked --release -p cordis-core --features loom-tests --test loom_era: 13 passed. The tests take 0.20 s, or about 0.4 s wall with the build already done (re-measured at e1eb528).
• ... --test loom_inertia: 16 passed. The tests take 11.2 s, or about 14.2 s wall.

Both are well inside the 15-minute Loom job timeout.

🤖 Generated with Claude Code