[dshbox-dev]

Closes #248

Summary

• ReadyHistoryModel (crates/cordis-core/tests/loom_inertia.rs) now packs the Fiber state with its total publication sequence into one SeqCst word. This mirrors StatePublication's single mutex: publish is one read-modify-write, including production's no-op for an unchanged state, and observe is one load. try_ready_acceptance follows production ready()'s order: observe (state, sequence), the idle / committed-recheck test, the sequence recheck, then the answer. Each model step cites the production lines it maps.
• New restart history (ready_answer_survives_a_complete_racing_restart_pass): one restart-like pass (claim -> publish transient Loading -> publish stable Active -> release) races one ready actor. The whole pass can land between ready's state read and its idle recheck. The Layer-C counterpart is ready_transient_state_racing_complete_restart_never_panics.
• Oracle (assert_ready_answer_had_quiescent_point): a ready answer is stale unless the answered publication was current at a point inside the invocation [I, R] where the Fiber was quiescent. Each publication's quiescent window [q, e) must meet [I, R]. The e > I side is exact: the answer's sequence must be at least the sequence read at invocation. For q <= R, the restart records the final publication's bit before its releasing CAS, so the window it records can only be wider than the real one. A transient answer is checked first and fails with its own message.
• New negative control (ready_without_sequence_recheck_is_detected): the same history without the sequence recheck. It fails with should_panic(expected = "stale ready answer: transient state escaped ready"), which is the oracle's own message. Loom finds the schedule from the Tokio regression. As a temporary probe that is not committed, I disabled the transient check; the window check alone then rejected the same answer (StatePublication { state: 2, sequence: 1 } was not current at any quiescent point inside the invocation).
• The existing ready_return_has_a_quiescent_linearization_point / ready_that_treats_idle_as_quiescent_is_detected keep their oracle and still pass and fail as before.
• Where production waits or loops (busy slot, outstanding recheck, sequence mismatch), the model returns no answer. Retry and waiting stay in Phase 2. Unloading and Loading are collapsed into one transient publication.
• lc06_model bounds are unchanged (max_threads = 3, max_branches = 64, no permutation/duration cap). The two_mutator section and two_mutations_preserve_revision_inspection_coverage are untouched.
• Docs: in lifecycle-concurrency-modeling.md, the Loom: model ready() publication sequence in ReadyHistoryModel (LC-06) #248 entry is removed from the not-represented list, the LC-06 section describes both histories, and the Phase 1 scenarios bounds sentence now says "models". This PR does not touch the Era offer/accept bullet or the ER-07 note (Loom: split Era handoff into offer / accept / cancel-after-offer #247). In lifecycle-concurrency-review-guide.md, the LC-06 row now covers the sequence recheck, the new model and negative control, and ready_transient_state_racing_complete_restart_never_panics.

Test/model and docs only. No production code or public API change.

Gates (ci/gates.sh t248)

Gate	Result
toolchain	PASS
fmt	PASS
clippy	PASS
vocab	PASS
doc	PASS

I did not run the test, examples and latest gates locally. I also ran cargo clippy -p cordis-core --features loom-tests --test loom_inertia, because the workspace clippy gate skips this feature-gated test. It reported no warnings in the test. The lib has an existing for_fiber dead-code warning that shows up only under this feature build.

Loom (as the CI Loom job runs it: cargo test --locked --release -p cordis-core --features loom-tests --test ...)

Target	Result	Local wall time (after compile)
loom_era	12 passed	~1.8 s
loom_inertia	18 passed	~21–25 s (origin/main on the same machine: ~12.4 s)

Running each new or changed LC-06 test on its own: ready_answer_survives_a_complete_racing_restart_pass ~5.1–5.6 s, ready_return_has_a_quiescent_linearization_point ~2.4–3.0 s, ready_without_sequence_recheck_is_detected ~0.4 s. This is well inside the 15-minute Loom job budget.

🤖 Generated with Claude Code