[kixelated]

Finishes quest/m1/route-mesh-model.md: the route model (rs/moq-net/verify/route/RouteHandoff.tla) now checks an announce budget and convergence on meshes bigger than the triangle, including clients.

Changes

• Budget: the spec counts the ROUTE, batch, ROUTE_REQUEST, and echo messages sent from one quiet point to the next (burst), and the external changes made in that span (churn): claim changes, session opens and closes, collections. Budget == burst <= 4 * |Dirs| * (1 + |Claims|) * churn: 4 messages each way over each session per route identity and per claim, the same budget mesh_sweep.rs (from moq-dev/moq#8477) holds the implementation to, with the model's one identity.
• Convergence: Converges == <>[](Quiet /\ Settled) under LiveSpec (fairness: something in flight is eventually delivered). Since burst is part of the state, Budget already rules out a delivery cycle that never goes quiet, so Line.cfg is the only config that runs the liveness checker.
• Meshes: Line.cfg (origin, 3 relays, a watching client), Ring.cfg (origin and 3 relays), and Chord.cfg (a publishing client on a ring of 5 relays with a chord, plus 2 watching clients, 2 claims; random simulation only). Every config, including main's Behind.cfg and BehindDear.cfg, checks SimplePaths, NoCountToInfinity, and Budget. Paths now grows only along links and through forwarding nodes, so a client ends a path and the 8-node chord stays cheap to enumerate. RouteHandoff.view.ts labels any mesh.
• Nightly: sh/tla.sh passes a config's \* Simulate: line to TLC, so Chord.cfg runs as random simulation. The budget counters make the triangle, BehindDear.cfg, and Ring.cfg take 40 to 60 minutes each on 4 workers (about 46,000 CPU-seconds for the route configs together), which one 4-core leg cannot fit in 120 minutes. Each of those three now gets its own leg, a route leg takes the rest of the directory, and the TLA+ job's cap rises to 180 minutes, since Nightly still runs TLC 1.7.4 on Java 8 until moq-dev/moq#8499 lands.
• Skill and quests: verify-route documents the new rules, configs, and runtimes, and moves the sync commit to caa3dd8926 (the last change under route/, which touched only node.rs, whose seqno bump on a closed link the model leaves out). The quest file is deleted and its links removed. route-inductive no longer requires it.

Checks

TLC 1.8.0 on Java 21, -workers 4, nice -n 19, 4 GB heap (the setup moq-dev/moq#8499 moves the recipes to), on a 24-core host loaded by other sessions, at the merged head.

Config	Result
RouteHandoff.cfg (triangle)	pass, 24,192,399 distinct states, 39 min
Behind.cfg	pass, 9,384,796 distinct, 25 min
BehindDear.cfg	pass, 17,863,476 distinct, 61 min
Line.cfg (+ Converges)	pass, 1,543,073 distinct, 13 min
Ring.cfg	pass, 18,437,833 distinct, 61 min
Chord.cfg -simulate num=1000 -depth 600	pass, 4,000 behaviours, 4.6M states, 9 min

just check: pass. quest check: pass. sh/tla.sh on a small copy of Chord.cfg (simulated) and on js/publish/verify/Publish.cfg (exhaustive): pass. The spec and configs are unchanged by the last merge of main.

Decisions

Maintainer, via the /quest-iterate brief, 2026-11-11:

• ✅ Accept the two-identity reduction (rejected: a second origin identity in the spec, run in simulation).

• ✅ Drop the follow-up to measure TLC worker scaling on JDK 25; moq-dev/moq#8499 owns TLC speed. This PR's just rs tla / just js tla recipe change (JDK 25, 8 workers) is dropped in favour of chore: TLC runs on Java 21 at low priority, and plan two faster-checking spikes #8499 (rejected: keeping a second recipe change here).

• Budget: ✅ the model uses mesh_sweep.rs's message budget, so both state one budget (rejected: restoring the model's tighter budget and tightening the sweep to match). Decided 2026-11-11 by the maintainer at the merge pick, which also accepted the nightly split into four route jobs at a 180-minute cap.

Choices made without asking

• Two origin identities are covered by reduction, not a second identity in the state. Router keys all state by identity and updates an identity from its own state only. So each identity's messages, read on their own, form a run of the one-identity model, and a shared FIFO only removes orderings. Instead, the configs place the origin at the end of a line, inside a ring, behind a triangle, and on a client off a ring.
• The model states the sweep's budget. The quest's plan says the model and mesh_sweep.rs state one budget or change both. The model's own earlier budget (4 per direction per change, with no per-claim term) was tighter: the triangle's worst change used 20 of 24. The shared one is looser by the claim term, a factor of 2 to 3 here; a count to infinity still grows past any constant.
• No SYMMETRY. Selection breaks ties by neighbour key, so no two relays are interchangeable. Only watching clients on the same relay are, and one client per relay covers them.
• Exhaustive runs stop at 4-relay meshes with one flap. The 5-relay meshes run only as random simulation (Chord.cfg, whose flaps can cut the ring into a line).
• Fairness is on "some delivery happens", written out as []<>Quiet \/ []<><<Delivery>>_vars. With WF_vars(...), TLC's ENABLED check never finished. This assumption is weaker than per-queue fairness, so it checks at least as much.
• burst and churn grow every config's state space (the triangle from 3.5M to 24M distinct), since the counters are state. That is the cost of Budget also implying convergence.

Public API: none. Wire: none.

Models

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

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-sol, high effort
• Session: 01a1cd2c-b03a-7c40-9b3f-b6f0321ad3f3, round 3
• Head: 3f3a771
• Base: origin/main at 4262a06
• Score: 10/10, The incremental diff restores the coverage mapping and introduces no actionable defects on source review; builds and tests were not run, as instructed.
• Findings: none
• The last round's findings, at 4256b39:
  • Fixed: medium, .claude/skills/verify-route/SKILL.md:74: Restore the route coverage table removed during the merge; The head restores all eight coverage rows with repository-relative paths, retains the Sim::leaf/Stats row, and removes the duplicate sync paragraph.

(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

[pullfrog]

✅ No new issues found.

Reviewed changes

Reviewed the full diff at 3f3a771 and checked the load-bearing claims against the code and tooling rather than the description alone.

• Budget accounting — burst/churn, Sent, External/Internal, and PerChange. Every send site is counted exactly once (ChangeClaim, Connect, Disconnect, Collect via External(Sent(rs)); Deliver both branches plus the ROUTE_END echo; DeliverAck both branches), and External resets both counters only when the pre-state is Quiet, which is correct because burst then counts a finished burst.
• Budget matches the sweep — 4 * Cardinality(Dirs) * (1 + Cardinality(Claims)) expands to 8 * sessions * (1 + claims), the same formula as mesh_sweep.rs's budget() with one identity.
• Converges only in Line.cfg — the argument that Budget implies convergence holds: after the last change churn is fixed, so sends are bounded, deliveries consume queued messages and acks, and a run that never quiets would exceed PerChange * churn. Fairness is not vacuous (a behavior that starves delivery satisfies neither disjunct).
• Extend/Paths — restricting growth to Links and to Serves(Last(p)) is correct, not a weakening: a route's hops only ever extend from a serving node, and Paths always contains <<Origin>>, so SimplePaths and Longest stay non-vacuous while client-terminated paths are excluded.
• New configs — Line, Ring, and Chord nodes, links, Leaves, and bounds were checked node by node against their comments, and their bounds match the SKILL timing table.
• sh/tla.sh — read -ra simulate clears the array on an empty read (so Chord.cfg's flags cannot leak into later configs), the sed pattern matches only a real \* Simulate: line, only Chord.cfg carries one, and the empty-array expansion is fine on the bash 4+ the script already requires (mapfile).
• Nightly matrix — ran the route leg's real git ls-files --cached --others --exclude-standard -- rs/moq-net/verify/route ':!…RouteHandoff.cfg' ':!…BehindDear.cfg' ':!…Ring.cfg': it yields exactly Behind.cfg, Chord.cfg, Line.cfg. The per-config legs resolve to their one spec, the file parses as YAML, and ${{ matrix.paths }} splits into the four pathspecs as intended.
• Docs and quests — python3 sh/coverage-tables.py passes with the new Sim::leaf/Stats row, and a repo-wide grep finds no dangling route-mesh-model link after the quest deletion.

Two notes that need no action: the route leg still bundles Behind.cfg (25 min) with Line (13) and Chord (9), and the runtimes were measured on TLC 1.8.0/JDK 21 while Nightly is on 1.7.4/Java 8 — the 180-minute cap is the intended margin for that. Separately, git log caa3dd8926..HEAD -- rs/moq-net/src/route/ currently returns #8514, which only added Sim::shows assertions in route/tests/routing.rs, so no covered symbol changed and the sync commit still describes the model's match.

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