[kixelated]

Paused: the milestone audit (moq-dev/moq#8637) moved this quest to quest/m3/route-trace-validation.md, after this session's m0-m2 scope. The work is complete and validated locally; what is left is listed under Waiting and in the quest's Plan.

Summary

Every run of sweep_handoff and sweep_scoped_handoff under the path rule can be checked as a behaviour of RouteHandoff.tla (TLA+ trace validation):

• route::tests::Sim records a run as newline-delimited JSON (rs/moq-net/src/route/tests/trace.rs, on when MOQ_ROUTE_TRACE names a directory): each step is a model action with its arguments, the messages it sent, and each touched relay's route and shown claims.
• rs/moq-net/verify/route/trace/RouteTrace.tla follows a trace through the model's own actions and compares every message and state (Agrees), plus the model's rules except Stable.
• sh/tla-trace.py runs TLC per trace (reusable for the resume, reconnect, and subscribe models; rs/moq-net/verify/README.md Trace validation). test route-trace runs it in Nightly on a fresh window of 150 scenarios per sweep (MOQ_ROUTE_TRACE_FROM). sh/tla.sh skips trace/ directories.
• The model grows where the router had drifted from it: a route goes to a stream only while a claim meets it (Meets, the empty want, Withdraw), timers due together fire in one update (Timeout replaces Lift/Expire), and an ended stream forgets what it reflected (Collect prunes src, which made the model hold for a stale child the router ignores).

Decisions

All taken by the agent under /quest-afk, for the maintainer's review:

1. Restrict the sweeps, grow the model only for drift. sweep_handoff runs churn's new Shape::Model: one origin whose every claim change changes a claim, with no restart and no collection. the_rules_agree_on_every_script keeps Shape::Full, which already ran the same checks under the path rule. The client, a leaf that offers no route, is dropped from the traces with its grant and interest edits. Rejected: growing the model to several publishers, restarts, grants, and interest edits (XL, and four open PRs edit RouteHandoff.tla).
2. Nightly only. The 300 traces cost about 20 core-minutes of TLC (about 4 core-seconds each, mostly JVM start). Rejected: the merge gate.
3. Leave Stable out of the trace check and file stable-repath. Rejected: failing test route-trace until the rule changes.
4. The brief said to rebase; I merged main instead, since the repository's rules forbid rebasing.

Follow-ups

• quest/m2/cluster-routes/stable-repath.md [M]: sweep_handoff scenario 139 is accepted by the model and breaks Stable. A relay drops available claims offline when its next hop re-paths through a session it knows closed. Open decision: hold under that next hop (recommended) or narrow Stable.

Validation

• All 300 traces of the gate's scenarios (150 per sweep) pass RouteTrace.tla on the pinned TLC 1.8.0 and CommunityModules 202311011627 jars, before and after merging main. Before the three model fixes, 20 failed.
• Planted router bugs: reversing select's tie-break fails 9 traces, and a hold turned into an end fails 101, while both sweeps pass. Dropping the withdrawal batch from a DEAD report, and not forwarding an advanced floor, fail none: the sweeps never reach those paths.
• Every rs/moq-net/verify/route/*.cfg passes on the grown model with its Simulate: line. RouteHandoff.cfg now has 29,229 distinct states, down from 476,515, because routes no longer flow before a claim exists.
• just rs test -p moq-net --lib -E 'test(/route::/)': 211 passed.
• Not run: just fix and just check, and test route-trace through sh/tlc.py. This host's Nix daemon hung fetching tla2tools.jar, so TLC ran from the same jars by hand.

Impact

Public API: none. Wire: none. Test-only additions in moq-net: Sim hooks, path::Router::session (test) and due.

Waiting

• moq-dev/moq: picked up again when m3 starts. Left: just fix/just check, refresh the state-count table in .claude/skills/verify-route/SKILL.md, run just test route-trace through sh/tlc.py, /quest-review, mark ready.

Models

Size: L
Implementer: Claude Code, claude-opus-5-5, unknown effort

🤖 Generated with Claude Code

(Written by Claude Opus 5.5)

[kixelated]

Closing per the maintainer's pick (2026-11-15, /quest-complete). #8764 settled route-trace-validation the other way: the exhaustive route search takes over RouteHandoff.tla's last three rules, and the model is deleted, so trace-validating the model no longer fits the quest. The branch stays. Its drift findings (Meets/Withdraw, timers due together, and sweep_handoff scenario 139 breaking Stable, drafted as stable-repath) are inputs for whoever runs the rewritten quest.

(Written by Claude Opus 5.5)