Hold 0005's mid-playback sequence as what the queue and the session do (#35)

[iderex]

The issue this belongs to

#35. The last section says which of its conditions this reaches, which is none of the three as written, and what it does reach instead.

What changed

src/session/mid_playback.rs is the sequence docs/decisions/0005-the-session-model.md fixes for a token that dies mid-playback, as what the queue and the session do at each step. 0034's counter in src/session/renewal.rs, 0047's queue in src/server/write_queue.rs and 0057's report in src/playback/report.rs were all in the tree as values, and nothing joined them: a position report the server rejected had no answer, and the sequence 0005 names #35 for existed only as a sentence.

git rev-parse origin/a-token-that-dies-mid-playback-35
540972595a9acd7dba56b51376ec339e75a6f834

git show origin/a-token-that-dies-mid-playback-35:src/session/mid_playback.rs | grep -n '^pub enum \|^pub fn \|^pub(crate) const \|^const '
85:const REPORTING_SUSPENDED: EventName = EventName::declared("session.reporting-suspended");
95:pub(crate) const POSITIONS_HELD: FieldName = FieldName::carried_whole("positions-held");
106:pub enum WhatARejectedReportDoes {
137:pub enum WhatTheOutcomeDoesToPlayback {
191:const fn forced_sign_out() -> LocalHalf {
210:pub fn a_report_was_rejected(
246:pub fn the_renewal_ended(

Four things the module holds, each because the convenient shape is wrong in a way nothing would report.

A rejected report is held where it is, in every case, and the type is what holds it. a_report_was_rejected takes the queue by shared reference, so the path that answers a rejection cannot remove an entry from it. The report that was due when the rejection arrived was the head, it stays the head, and the drain stops there, which is 0047's own rule for an entry that could not be delivered. 0005: nothing in the queue is discarded because of an authentication failure, because the failure says nothing about whether the positions are correct.

Nothing here can fail a call the client did not make. Neither answer type carries a value of 0004's vocabulary, so there is no cancellation to deliver and no outcome to arrive on a call nobody made. 0005 says the client hears nothing except through diagnostics at that moment, and that is the one route out.

A fresh token reports the current position through the queue, so it is one report and not two. The report goes through 0047's coalescing, replaces the entry the rejection left at the head, and keeps that entry's place in the order, so the drain resumes exactly where it stopped and the position reached during the renewal arrives once. src/playback/report.rs gains the occasion that report is made on and the one call that makes it; the interval is left where it was, as for a seek.

A refusal keeps every report, signs the session out by the forced act, and tells the client once. The event is session.reporting-suspended at failure, carrying how many positions are held under a field name treated as carried whole, which 0071 lists a count among. 0005: the queue belongs to the session, and a person who signs in again gets those positions reported in order before anything else. A silence keeps every report and moves nothing, which is 0034's half the natural code gets wrong.

The other files register the module where every landing registers one: src/session/mod.rs, the crate's thread assertions in src/lib.rs, the same assertions asked from outside in tests/thread_statements.rs, the coverage surface in .github/coverage/pinned-surface, the new field name in 0071's statement in src/lifecycle/mod.rs, and the list tests/the_rule_as_data_names_every_field.rs holds that statement against.

The means is the one the tree already carries, which is the check ## Choosing the means asks for: a value joining three values that already exist, in the language 0011 measured and chose, and every case asserts against the queue's, the counter's and the sink's own answers rather than against a second apparatus.

What failure it prevents

The current position reported around the queue after a renewal. It reads as the smaller change, and it delivers the held report and the current one as two writes for one item, the first of them stale, on the one path 0047 was built for.

A queue emptied because a renewal was refused. The session is over, so clearing what it held reads as tidy, and it discards the positions from a train journey at the moment they are least recoverable. 0005 refuses it by name.

A session signed out, or a client alarmed, because a renewal got no answer. 0034 says this is the half decided wrongly by reflex: a silence is not a refusal, and the damage is not the failed call but a token that is gone.

Evidence

The module's own cases, at the commit above:

cargo test --locked --lib session::mid_playback
test result: ok. 8 passed; 0 failed; 0 ignored; 0 measured; 547 filtered out; finished in 0.00s

The whole suite, which is one of the two commands the README names:

cargo test --locked
test result: ok. 555 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s
test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.19s
test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s
test result: ok. 11 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s
test result: ok. 28 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.19s
test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s
test result: ok. 124 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.22s

The other one, and the legs that run without a network:

cargo build --locked --all-targets
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 7.93s

bash .github/lint/lint.sh check
Every lint the groups above carry was refused, outside the register printed with it.

bash .github/format/format.sh check
Every tracked source file above is written the way the formatter would write it.

bash .github/invariants/invariants.sh check
Every rule above was applied to its subject and refused nothing.

bash .github/doc-paths/doc-paths.sh check
Every path these documents name resolves against the tracked set.

bash .github/excluded-targets/excluded-targets.sh check
Every target the ordinary command leaves out compiles.

The coverage leg, read off the runner rather than this machine. Run by hand here, bash .github/coverage/coverage.sh check measured nothing at all on this Windows machine, reporting actual -% (0 line(s), 0 missed) and refusing on it, so the local run is not evidence in either direction and the runner's is what stands:

gh run view 33730947400 --repo Flowfin/core --log | grep -E 'bar +[0-9]|actual +[0-9]|room +[0-9]'
      bar    96.5% of lines on the pinned surface
      actual 97.69% (9145 line(s), 211 missed)
      room   113 more uncovered line(s) on this surface before the bar is crossed

The size of the change:

git diff --shortstat origin/main...origin/a-token-that-dies-mid-playback-35
 8 files changed, 769 insertions(+), 3 deletions(-)

What a guard here refuses, and the proof it bites

Four guards, each watched failing on the version of the mistake it is against, each restored afterwards, and the restored file compared byte for byte against the kept copy. Every run below is cargo test --locked --lib session::mid_playback, and the deliberate violation is the edit named above each run.

The current position after a fresh token goes through the queue. The violation answers the queue's own value without asking it:

-            let what_the_queue_did = reporting.report_after_a_renewal(current, queue);
+            let what_the_queue_did = WhatTheEnqueueDid::Added;

test session::mid_playback::tests::a_fresh_token_reports_the_current_position_in_place_and_the_drain_resumes ... FAILED
  left: CurrentPositionReportedAndTheDrainResumes(Added)
 right: CurrentPositionReportedAndTheDrainResumes(ReplacedInPlace)
test result: FAILED. 7 passed; 1 failed; 0 ignored; 0 measured; 547 filtered out; finished in 0.00s

A refusal keeps every report. The violation empties the queue before saying so, which is the tidy version of the failure 0005 refuses:

+            while queue.after_it_was_delivered().is_some() {}

test session::mid_playback::tests::a_refused_renewal_keeps_every_report_and_says_so_once ... FAILED
  left: []
 right: [(1, "the-film", Ticks { ticks: 100000000 }), (2, "the-episode", Ticks { ticks: 0 })]
test result: FAILED. 7 passed; 1 failed; 0 ignored; 0 measured; 547 filtered out; finished in 0.00s

A silence tells the client nothing. The violation reports a silence as if the session had ended:

+            say_positions_are_held(queue, diagnostics);

test session::mid_playback::tests::a_silent_renewal_leaves_the_session_and_the_queue_exactly_as_they_were ... FAILED
test session::mid_playback::tests::an_outcome_when_nothing_was_running_changes_nothing ... FAILED
test result: FAILED. 6 passed; 2 failed; 0 ignored; 0 measured; 547 filtered out; finished in 0.00s

A server with no renewal route ends the session and the client is told. The violation ends it silently:

-            say_positions_are_held(queue, diagnostics);

test session::mid_playback::tests::a_server_with_no_renewal_route_signs_out_at_the_first_rejection_and_holds_every_report ... FAILED
  left: []
 right: [("session.reporting-suspended", Some(2))]
test result: FAILED. 7 passed; 1 failed; 0 ignored; 0 measured; 547 filtered out; finished in 0.00s

The guard that holds the rejected report in place is not one of the four, and that is said rather than left to be assumed: it is the signature of a_report_was_rejected, and the one-change neighbour that removes an entry there does not compile. A case asserts the queue is unchanged across every rejection anyway, so a later widening of that signature meets a red run rather than a green one.

What this does not cover

None of #35's three conditions as written. A test that plays through a token death against the fake server, proves the position reached during the outage arrives after renewal, and proves nothing is reported twice is a run with a stream, a drain and a renewal request in flight, and nothing in this tree sends a byte: the transport is #27, and #27 now names #291 and #292 as what its socket waits on. What this reaches is the shape those conditions will be asserted through, and the comment of 2026-08-11 on #35 already says the first condition cannot be a proof about a stream the core never holds.

Nothing is durable. The queue lives as long as the value does, which src/server/write_queue.rs says of itself, so a restart between the rejection and the renewal is not something this can be asked about.

Nothing runs a drain. The module answers that the drain stops, waits or resumes, and nothing consults that answer, because there is no drain.

Nothing here observes the position reached after the token died. 0005 guarantees the last one observed before the rejection and bounds the gap by 0057's cadence, and this claims nothing about the gap.

The sign-out is answered and not performed. LocalHalf is what 0114's local half looks like once done; no token is dropped from memory because there is none, and no store is called.

Nobody other than me has read the change. There was no second reader available for it, and the evidence above stands in place of one.