[kixelated]

Finishes quest/m1/failover-chain-model.md.

Problem

Each model from moq-dev/moq#8447 checks one layer alone: routing (verify-route), a front switching copies (verify-resume), and a subscription's accounting (verify-subscribe). Resume failover keeps breaking where those layers meet: a relay's front switches routes while the relay above it is resuming too, and a half-read group has to continue across both.

Approach

rs/moq-net/verify/failover/FailoverChain.tla models one track read by a client C through relay E. E starts on relay A and may fail over to relay B; both pull from the origin O. With Mesh, B may also route through A. Each layer is cut down to the steps its own model checked: a route change is one step, a switch asks the new copy from the reader's newest group or lowest gap, and a handed-out group crosses a hop unless its session dies. What the chain adds is frames. A group whose copy fails or stalls mid-read continues at the same frame (Recover): from another copy, from the serving copy, or by fetching the rest from the serving route, which asks its own upstream in turn.

Rules: CleanEndIsComplete, CleanEndIsDeclared, NoSkipWhileHeld, SettledIsWhole, and TLC's deadlock check as Settles. Settles means no hang, and once the client leaves, no relay keeps a copy. The new verify-failover skill documents them, with run times, the open findings, a Coverage table, and the scope.

• FailoverChain.cfg passes: about 2.0M states, with one death and one switch per relay. The client stays, so a deadlock there is a playback hang.
• Leave.cfg passes: about 2.2M states. The client may leave at any point, so a deadlock there is a relay still holding a copy. Each takes under 30 s on 24 cores.
• EndedRelay.cfg adds the mesh hop and fails NoSkipWhileHeld, at depth 31 after about 50M distinct states (11 min on 8 workers). B finishes its track, then its route through A dies with E's fetch for the rest of group 0 still pending. B's front no longer switches, so the fetch fails although B still reaches O directly, and E cuts the client's group short.

Mutation checks show the rules catch real breaks: dropping backfill_gaps breaks CleanEndIsComplete, disabling Recover deadlocks, and disabling a relay's park deadlocks once the client leaves.

Found on the real stack

Replaying those paths over real sessions (rs/moq-net/tests/integration/failover_chain.rs, memory transport, simulated clock) found two bugs. In both, the code falls short of what the model allows. Each is pinned as a residual_* test that passes while the bug stands. A control test, a_half_read_group_continues_through_the_new_route, runs the same path without the end and passes.

• residual_ending_the_track_fails_a_fetch_in_flight: E's fetch for the rest of group 0 is in flight through B when the publisher ends the track. B's copy, asked from group 1, completes, and B's fetch from the publisher is cancelled. E's read of group 0 then fails with NotFound, even though every relay still reaches the publisher and the publisher writes the rest.
• residual_a_fetch_from_a_completed_copy_never_leaves_the_relay: the same group, read further only after E's serving copy from B completed. Recover::poll_fetch calls fetch_group on that copy, but no FETCH goes on the wire, so the read waits out the subscriber's budget.

The mesh finding has no replay of its own yet: the real stack breaks the same rule earlier, on the first bug.

Impact

• Public API: none. Wire: none.
• Tests only: a TLA+ spec, three configs, a skill, and three integration tests (about 25 ms each).

Validation

• just check: every test passed except moq-relay config::tests::repository_configs_load. That test fails because test/audio-quality/congestion.toml on main has a field the relay config rejects (unknown field down). This branch touches neither file, so the failure predates it, and moq-dev/moq#8486 fixes it.
• The failover_chain integration tests passed 5 runs out of 5. TLC passes FailoverChain.cfg and Leave.cfg, and fails EndedRelay.cfg on its open finding.

Decisions

• A group may fail while its track lives (Abort): when no other copy holds it and no fetch can reach the rest, because the front has no route, ended with its serving copy gone, or its live serving copy gave up on the group. Before, Abort needed the whole track to have failed, so NoSkipWhileHeld could never break (pullfrog's finding). ✅ make Abort match Recover::poll giving up (rejected: keep the guard and document the rules as out of reach).
• FailsOnlyUnroutable is dropped: the client's track fails only through FrontFail, whose guard is the rule, so it could not break. ✅ drop it and say so under Not covered (rejected: keep it as a tautology).

Choices made without asking

• The model's docs are a verify-failover skill, matching the four sibling models.
• The model describes the intended behavior wherever the code falls short: a fetch reaches the serving route while that route lives, after the track ended too. The two code bugs are listed under the skill's open findings rather than written into the model.
• The origin writes each group whole, and frames split only at the hops. Writing frame by frame did not finish exploring after 53M states.
• When a relay parks a track that ended, it forgets the track, so the next reader gets a fresh front. The cache is only an optimization, so the model keeps none.
• "In order" in the Goal is read as frames within a group: a resumed group never repeats or skips a frame. Groups themselves arrive in arrival order, as an unordered reader sees them.

Related

• moq-dev/moq#8476 changes how a failed fetch below a declared end settles. It touches the same area but neither finding.
• moq-dev/moq#8472 plans nightly runs and trace validation for the models, which this one should join.

Follow-ups

• Fix the two fetch bugs above: a fetch for the rest of a group survives the track ending, and is sent from a completed copy. Then replay EndedRelay.cfg's path and fix how an ended relay moves a fetch off a dying route. Recommend: plan one m1 quest for all three; they share the fetch path and the replay harness.
• EndedRelay.cfg takes 11 minutes. Recommend: no separate quest; the nightly models quest picks it up as an open-finding config.

Models

Size: L
Implementer: Claude Code, claude-opus-5-5, high effort
Implementer: Claude Code, claude-opus-5-5, medium effort (iterate, S)

🤖 Generated with Claude Code

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-sol, high effort
• Session: 01a1c852-f40c-78c0-8b58-1532e5ec8a6e, round 3
• Head: f1d0be9
• Base: origin/main at b722c56
• Score: 10/10, The incremental changes let group failures surface independently of track failure and update the documented counterexample consistently, with no new findings from source-only review; no builds or tests were run.
• Findings: none

(Written by Claude Opus 5.5 with medium)

[coderabbitai]

Pre-merge checks: 2

Failed checks: 2 inconclusive

Check name	Status	Explanation	Resolution
Title check		This assessment has not completed. The check will be retried on the next pre-merge check run.
Description check		This assessment has not completed. The check will be retried on the next pre-merge check run.

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[kixelated]

Automated review by review (OpenAI)

Reviewed 006ed54, including all nine changed files and the referenced recovery/front and integration-harness paths. No additional actionable findings.

Direction: the separate stay/leave configurations avoid letting an available unsubscribe hide a playback deadlock. Frame recovery and clean-end checks complement the existing whole-group models. The control replay and two explicitly named residual tests distinguish successful recovery from the known end-of-track fetch failures; these are documented existing defects, not fixes delivered here. The mesh counterexample remains explicitly unreplayed.

Verification limits: GitHub-only static review. No Rust tests or TLC runs performed, and reported state counts, timings, and failures were not independently reproduced. The model uses bounded, abstract routes and deadlock checks, not an unrestricted temporal-liveness proof; the documented model/code differences remain.

[pullfrog]

Important

The model's rule table claims coverage the spec does not have: FailsOnlyUnroutable and NoSkipWhileHeld are entailed by the step definitions and can never fail, in any config. The replay tests themselves are sound — 3/3 pass, stable across five simulator seeds.

Reviewed changes

I read the whole diff, ran cargo test -p moq-net --test integration --features async failover_chain (3/3 pass, 0.02 s, and again across MOQ_SIM_SEED 1/7/42/123/999), and checked the new files against the sh/text.sh gate.

• Failover chain model — FailoverChain.tla composes route, resume, and subscribe as one step each and adds frames, so a half-read group continues at the same frame from another copy or by fetching from the serving route.
• Three configs — FailoverChain.cfg (client stays, so a deadlock is a playback hang) and Leave.cfg (client may leave, so a deadlock is a retained copy) are green; EndedRelay.cfg is committed known-red on the ended-relay finding.
• Replay tests — failover_chain.rs builds P→A/B→E over the memory transport with a simulated clock, aborts the A↔E session, and pins the two fetch bugs as residual_* tests, with a control test for the same path without the track end.
• Skill — verify-failover documents the rules, run times, open findings, coverage, and scope in the shape of the four sibling models; the finished quest file and its README line are removed.

The residual_* naming, the weak is_err() assertion (AGENTS forbids matching on errors), and the 500 ms settle() all hold up: the control test discriminates the setup, the abort forces the same switch as the price change, and 30 s cannot be reached by the Old grace, so the second residual can only pass by hanging.

---

_{Reviewed the complete diff at 006ed54; 9 files, 3 commits. Tests in this run: failover_chain 3/3 across five seeds.}

  ^{｜ Fix all ➔ ｜ Fix 👍s ➔ ｜ View workflow run ｜ Using deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) ｜ 𝕏}

[kixelated]

Heads-up from moq-dev/moq#8483. It runs every TLA+ config in Nightly through just test tla. A config with a \* Open finding: line must break a rule, and every other config must pass. Whichever of the two PRs lands second, check that the markers still hold, with just test tla <verify dir>. That means a finding this PR fixes moves its rule into the passing config and drops its finding config, and a new open-finding config gets the marker.

(Written by Opus 5.5 with medium)

[kixelated]

One more from moq-dev/moq#8483. just check now runs sh/coverage-tables.py over every verify-* Coverage table. Each Code cell must start with a repo-relative path, such as `rs/moq-net/src/model/resume.rs`, followed by the symbols in that file. Each symbol must still be defined there. If this lands second, verify-failover's table needs that form.

(Written by Opus 5.5 with medium)

[pullfrog]

✅ No new issues found.

Reviewed changes

Reviewed the delta since the prior pullfrog review at 006ed54: the Abort guard, the dropped rule, and the matching doc updates.

• Abort can fail a group while its track lives — a short group now fails only when its source is dead or gave up, no other copy can continue it, and no fetch can reach the rest (the front has no route, ended with its serving copy gone, or its live serving copy gave up on the group). This mirrors Recover::poll's give-up paths and makes NoSkipWhileHeld falsifiable.
• FailsOnlyUnroutable removed — it was entailed by FrontFail's own guard in every config; the skill's Not covered section now records that the client's track fails only through that step.
• EndedRelay.cfg now fails on NoSkipWhileHeld — the mesh counterexample reports the rule instead of a deadlock, so the skill's attribution of the first residual to that rule holds.
• Docs updated to match — the Abort comment, the rules table, the open-finding text, and the run notes (depth 31, about 50M distinct states).

  ^{｜ View workflow run ｜ Using deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) ｜ 𝕏}