crates/spt/tests/er_briefing_presented_e2e.rs | 186 ++++++++++++++++---------- traceable-reqs.toml | 2 +- 2 files changed, 118 insertions(+), 70 deletions(-) diff --git a/crates/spt/tests/er_briefing_presented_e2e.rs b/crates/spt/tests/er_briefing_presented_e2e.rs index c01b0f4b..f4125b0a 100644 --- a/crates/spt/tests/er_briefing_presented_e2e.rs +++ b/crates/spt/tests/er_briefing_presented_e2e.rs @@ -35,4 +35,4 @@ -//! row, and must never refuse the attach — and that the retained row is -//! re-offered at the next attach. None of that had a test. Arms 4 and 5 are that -//! half, and they share one home and one daemon tree because arm 5's claim is -//! about **the very row arm 4 failed to present**, not about some later briefing. +//! row, and must never refuse the attach. Within one bring-up session the next +//! seat re-offers that same row. Across the session boundary arm 5 actually +//! crosses, the retained row is loudly superseded and the new session's own +//! briefing lands at the same attach. Arms 4 and 5 prove that full chain. @@ -47,11 +47,10 @@ -//! 5. **The retained row is re-offered at the next seat.** The same adapter name -//! is re-pointed at the binding harness and a second seat taken; -//! `settle_engine_room_seat` PRESENTS on every seat-taking attach, so the -//! re-offer is that one site firing again rather than a new mechanism. (Its -//! other half, the brief ENQUEUE, is bounded to once per session — #177 — and -//! that is why the arm reaps the daemon tree between the seats: seat 2 is a -//! genuinely fresh session, so it enqueues its own briefing too. Neither fact -//! is what this arm asserts; the retained row would be re-offered either way, -//! because presentation was never gated on this seat having enqueued.) The row -//! id captured in arm 4 must be the one that goes delivered, on -//! `native-inject`, with the session still never having declared idle. +//! 5. **A miss never leaves the next seat unbriefed.** The same adapter name is +//! re-pointed at the binding harness and a second seat taken. Within one +//! session, `settle_engine_room_seat` re-offers the retained row; that regime +//! is witnessed by the same-log seat-2 unit. This arm deliberately reaps the +//! daemon tree, so seat 2 opens a new session instead. Session scoping sweeps +//! the retained row loudly as superseded, then the new session's own briefing +//! is delivered at that attach through `native-inject`. The old row's absence, +//! the `ENGINE_ROOM_BRIEFING_SWEPT` line, the fresh row's delivery, and zero +//! pending rows together prove miss => release => retained => +//! superseded-with-delivery, never a silent loss. @@ -140 +139,3 @@ fn seed_subnet_and_code(name: &str) -> String { - let seed = rec.seed_bytes().expect("a created subnet carries a member seed"); + let seed = rec + .seed_bytes() + .expect("a created subnet carries a member seed"); @@ -259 +260,3 @@ fn code_for(subnet: &str) -> String { - let seed = rec.seed_bytes().expect("a created subnet carries a member seed"); + let seed = rec + .seed_bytes() + .expect("a created subnet carries a member seed"); @@ -355 +358,3 @@ fn reap(home: &Path, spt_bin: &Path, broker: &mut Child, brain_pid: u32, extra: - cmd.no_window().args(["daemon", "stop"]).env("SPT_HOME", home); + cmd.no_window() + .args(["daemon", "stop"]) + .env("SPT_HOME", home); @@ -374 +379,3 @@ fn run_ceremony(spt_bin: &Path, home: &Path, subnet: &str, adapter: &str) -> boo - common::output_bounded(cmd, Duration::from_secs(30)).status.success() + common::output_bounded(cmd, Duration::from_secs(30)) + .status + .success() @@ -407 +414,4 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - assert!(ceremony_ok, "PRECONDITION: the ceremony must provision the record"); + assert!( + ceremony_ok, + "PRECONDITION: the ceremony must provision the record" + ); @@ -539 +549,4 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - assert!(ceremony2_ok, "PRECONDITION: the second ceremony must provision the record"); + assert!( + ceremony2_ok, + "PRECONDITION: the second ceremony must provision the record" + ); @@ -547 +560 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // ══ ARMS 4 + 5: the MISS, and the RE-OFFER that rescues it. ══ + // ══ ARMS 4 + 5: the MISS, then a SESSION BOUNDARY. ══ @@ -551,2 +564 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // must RETAIN the row, and must never cost the operator the controls — and - // the retained row must still be delivered by the next seat-taking attach. + // must RETAIN the row, and must never cost the operator the controls. @@ -554,4 +566,4 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // Both arms share ONE home and ONE daemon tree on purpose. Arm 5's whole - // claim is that the row ARM 4 FAILED TO PRESENT is the row that later - // lands; splitting them across homes would leave arm 5 asserting only that - // some fresh briefing was delivered, which arm 1 already says. + // Both arms share ONE home on purpose, preserving the retained row across + // the daemon restart. That restart opens a new session: the old row must be + // swept loudly as superseded, and the fresh session's own briefing must land + // at the same attach. Same-session re-offer is witnessed by the broker unit. @@ -564 +576,9 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - register_harness_mode(home4.path(), &spt_bin, &mock, &xlate, adapter, "hold-unbound", 1000); + register_harness_mode( + home4.path(), + &spt_bin, + &mock, + &xlate, + adapter, + "hold-unbound", + 1000, + ); @@ -607,8 +627,5 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // a second seat. `settle_engine_room_seat` PRESENTS on every seat-taking - // attach — that call is deliberately outside the once-per-session enqueue - // bound (#177) precisely so a row a previous seat could not present is - // re-offered by the next one — so the second seat re-drives. It also - // re-briefs here, because the daemon tree is reaped below and seat 2 is - // therefore a FRESH session; on a same-session re-attach it would not. - // Either way the re-offer is that one site firing again, not a new - // mechanism, and what this arm asserts is the RETAINED row's delivery. + // a second seat. The daemon restart below opens a NEW session, so the old + // session's retained briefing is no longer true: session scoping sweeps it + // loudly, then the new session composes and delivers its own briefing at the + // same attach. This arm proves the cross-session chain, while the broker's + // same-log seat-2 unit owns the distinct same-session re-offer guarantee. @@ -635 +652,8 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - reap(home4.path(), &spt_bin, &mut broker4, brain_pid4, &[rc4_pid], id); + reap( + home4.path(), + &spt_bin, + &mut broker4, + brain_pid4, + &[rc4_pid], + id, + ); @@ -655 +679,3 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // Barrier: the RETAINED row going delivered. Not "a row" — THAT row. + // Barrier: the NEW session's own briefing going delivered. The retained + // row cannot be the barrier across a session boundary because supersession + // must remove it before the fresh briefing lands. @@ -657 +683 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - let mut redriven: Option = None; + let mut new_session_briefing: Option = None; @@ -659,8 +685,7 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - if let Some(want) = retained_id { - if let Some(row) = briefing_rows(&perch4) - .into_iter() - .find(|r| r.id == want && r.delivered) - { - redriven = Some(row); - break; - } + let rows = briefing_rows(&perch4); + if let Some(row) = rows + .into_iter() + .find(|r| Some(r.id) != retained_id && r.delivered) + { + new_session_briefing = Some(row); + break; @@ -682 +707,8 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - reap(home4.path(), &spt_bin, &mut broker5, brain_pid5, &[rc5_pid], id); + reap( + home4.path(), + &spt_bin, + &mut broker5, + brain_pid5, + &[rc5_pid], + id, + ); @@ -691,2 +723,3 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - redrive: row={redriven:?} rows={redrive_rows:?} pending={redrive_pending} \ - controllable={redrive_controllable:?} idle={redrive_idle_present}\n\ + redrive: new_session_row={new_session_briefing:?} rows={redrive_rows:?} \ + pending={redrive_pending} controllable={redrive_controllable:?} \ + idle={redrive_idle_present}\n\ @@ -696 +729,4 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - assert!(ceremony4_ok, "PRECONDITION: the miss arm's ceremony must provision the record"); + assert!( + ceremony4_ok, + "PRECONDITION: the miss arm's ceremony must provision the record" + ); @@ -754 +790 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - // CLAUSE 4, ARM 5 — the retained row is re-offered at the next seat. + // CLAUSE 4, ARM 5 — a session boundary supersedes loudly and delivers anew. @@ -766 +802,13 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - let redriven = redriven.unwrap_or_else(|| { + assert!( + !redrive_rows.iter().any(|r| Some(r.id) == retained_id), + "REQ-ER-BRIEFING-PRESENTED clause 4: at a SESSION boundary the retained row \ + (id={retained_id:?}) must be superseded, not carried into a session whose posture \ + it no longer describes.\nrows={redrive_rows:?}" + ); + assert!( + brain5_stderr.contains("ENGINE_ROOM_BRIEFING_SWEPT"), + "REQ-ER-BRIEFING-PRESENTED clause 4: supersession must be LOUD. Absence of the old \ + row without ENGINE_ROOM_BRIEFING_SWEPT would be the silent loss the original \ + identity assertion guarded against.\n{brain5_stderr}" + ); + let new_session_briefing = new_session_briefing.unwrap_or_else(|| { @@ -768,4 +816,4 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - "REQ-ER-BRIEFING-PRESENTED clause 4: the RETAINED row (id={retained_id:?}) must be \ - re-offered and delivered at the next seat-taking attach. This is the miss -> \ - release -> retained -> re-drive chain: a row that survives a miss but is never \ - picked up again is retained in name only.\nrows={redrive_rows:?}\n{brain4_stderr}" + "REQ-ER-BRIEFING-PRESENTED clause 4: the new session's own briefing must be \ + delivered at the same attach that supersedes the retained row. The cross-session \ + chain is miss -> release -> retained -> superseded-with-delivery, never merely \ + disappearance.\nrows={redrive_rows:?}\n{brain4_stderr}" @@ -775 +823 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - redriven.taken_leg.as_deref(), + new_session_briefing.taken_leg.as_deref(), @@ -777,8 +825,3 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - "the re-offer must ride the SAME native arm — `idle-inject` here would mean the \ - ordinary window rescued it, which is the behaviour #164 is replacing, not the \ - re-drive this arm claims.\nrow={redriven:?}" - ); - assert!( - !redrive_idle_present, - "the re-drive must land while the session has still never declared idle — otherwise \ - this arm proves the pre-fix idle window, exactly as arm 1 guards against" + "the new session's briefing must ride the native arm at the seat-taking attach; \ + `idle-inject` would leave the next seat initially unbriefed.\n\ + row={new_session_briefing:?}" @@ -788,2 +831,7 @@ fn the_engine_room_briefing_is_presented_before_the_first_actionable_turn() { - "after the re-offer nothing may remain pending: the retained row was carried and the \ - second seat's own briefing with it.\nrows={redrive_rows:?}" + "after loud supersession and the fresh native delivery, no briefing may remain \ + pending.\nrows={redrive_rows:?}" + ); + assert!( + !redrive_idle_present, + "the new session's briefing must land while the session has still never declared \ + idle — otherwise this arm proves only the pre-fix idle window"