Skip to content

quest: plan lite-07's hop list on routes, one routing stream per side, and its interest set - #8495

Merged
kixelated merged 6 commits into
mainfrom
quest-plan/lite07-route-stream
Nov 11, 2026
Merged

kixelated merged 6 commits into
mainfrom
quest-plan/lite07-route-stream

Conversation

@kixelated

@kixelated kixelated commented Nov 11, 2026 •

Copy link
Copy Markdown
Collaborator

Problem

lite-07's ROUTE_END echo can overtake a route, and two relays then count to infinity (moq-dev/moq#8447). The settled fix, the echo behind the echoer's routes, assumes one stream carries those routes, but a session may hold several Announce Streams each way, so moq-dev/moq#8487 could fix only the model. This /quest-plan reopened the route layer's rules to settle that.

It also found that the reordered echo is not enough. With an origin behind a relay, the model still counts to infinity: a derived route held by a third relay comes back after every neighbour has echoed.

Approach

Quest files only. Decisions are recorded in the quests' Plans; in brief, as items 18 to 25 of the routes epic:

  • Every publisher stays an origin node, holds stay, and the newest floor wins per identity.
  • Each route names the relays it crossed, and a node never uses a route that names itself. Feasibility still selects routes; the list is one per origin route, not per claim. The echo and the drain rule stay as they are.
  • Each side says everything about routing on one unidirectional Announce Stream, whose interest is a set of prefixes edited in place: never nested, with swaps that re-send nothing both sets cover, a floor per prefix, and SYNCED per prefix. Items 16 and 17 are superseded.
  • A node bumps its seqno unprompted only when a route link changes.

The hop list replaced an earlier decision in this same plan, a relay echoing a ROUTE_END only once its own downstream had. The route model ran both. The branch route-drain-counterexamples (5e7e3eb434) holds the model with each variant behind a switch, per-link costs, the configs, four Sim replays, and every result in rs/moq-net/verify/route/DRAIN.md:

Variant Result
Echo at once (today), origin behind a triangle counts to infinity in 20 states (unequal costs) and 23 (unit)
Deferred echo, one flap passes the triangle at full bounds and the origin behind a triangle
Deferred echo, two flaps, unequal costs fails in 23 states: a closed session counts as an echo while that peer's last advertisement is in flight
Hop list, two flaps passes the origin behind a triangle at unit cost and four unequal cost sets, and the triangle at full bounds
Hop list, echo unordered as on today's wire passes the same shapes; without the list that ordering fails in 11 states
Hop list, no echo a forwarding loop in 944 states, so the echo stays

Not run: full bounds on the 4-relay shapes, any 5-relay shape, and four runs stopped at 8 to 21 million states with no violation. The list's message cost is unmeasured; the quest measures it against moq-dev/moq#8479's announce budget before touching the router.

New quests:

  • quest/m2/cluster-routing/routes/interest-set.md [L]: the edit rule proven in the TLA+ model and implemented in the router, no wire.
  • quest/m2/cluster-routing/routes/route-stream.md [XL]: the wire, the sessions, the draft, and js/net.
  • quest/m1/route-seqno-bumps.md [S]: today every announce stream open and close bumps a relay's seqno.
  • quest/m1/offline-cursor-fallback.md [S] and quest/m1/offline-js-handle.md [S]: the two unowned review findings on moq-dev/moq#8375, where a lost route reads as END.
  • quest/m5/browser-mesh.md [L]: tabs that forward for LAN peers, on the Rust-to-TypeScript port.

Edited quests:

  • echo-order.md is rewritten and retitled "A node never takes back a route that crossed it": the hop list in the model, Sim, the router, the wire, and the draft, on today's Announce Streams.
  • js.md, the P2P epic, and quest/m3/mesh/overlay.md, which gains core and edge roles in place of the non-forwarding node.

Impact

None. Quest files only.

Alternatives

  • The deferred echo, decided first and then run. Rejected on the model result above. It also needed three sub-rules found by counterexample, makes an upstream wait on its whole subtree before re-advertising, and lets a peer that withholds its echo stall that upstream.
  • A relay originating the claims of peers that send no Node ID or hold a scoped grant, as it does for lite-06. Rejected twice by the maintainer: a publisher's identity is wanted for signing, for one node across several links, and because browsers will forward.
  • Never dropping the feasibility distance, or dropping it on a timer. Rejected: unbounded memory with every publisher a node; safety by timing.
  • One bidirectional Announce Stream per direction with the echo moved to the answering half (the brief's shape). Rejected: a side's messages still ride two streams.
  • A floor over the whole prefix set, and SYNCED once per edit. Rejected.

Choices made without asking

For review; each is marked a recommendation in the quest it sits in.

  • The fix lands on today's Announce Streams and does not wait for the route stream. The model passes with the echo unordered once the list is there. The maintainer was asked and has not answered.
  • The hop list's wire sketch: a count and Node IDs in order from the origin, the sender last and the origin left out; checked for the receiver's own Node ID as received, before a scoped peer's ids are qualified; lite-06's hop limit reused.
  • If the list breaks test(net): the route model checks an announce budget and convergence on meshes with clients #8479's announce budget, the quest stops and reports rather than raising the budget.
  • The work splits into the interest set (model and router) and the route stream (wire).
  • The route stream's wire sketch: the stream lasts the session and is never reopened; the echo gets its own message type; one ANNOUNCE_OK per edit marks where it takes effect; an empty set is allowed; a prefix outside the grant lists nothing rather than being refused.
  • What counts as a "route link" for the seqno bump.
  • In the overlay: a link costs the product of its two ends' costs, an edge's default cost, and an edge marking its core links upstream.
  • The reference branch route-drain-counterexamples was pushed to keep the model variants and replays; delete it once echo-order's PR carries them.

Follow-ups

Models

Size: M
Implementer: Claude Code, claude-fable-5-2, high effort

Review

Rewritten by quest review after each round.

  • Reviewer: Codex, gpt-6.1-sol, medium effort
  • Session: 01a1c8f4-9345-7b80-b9a7-9a7654913282, round 4
  • Head: 470f8e4
  • Base: origin/main at 529fa6a
  • Score: 10/10, The incremental planning changes clarify hop-list identity handling and required verification consistently with the existing qualification rules, with no actionable defects.
  • Findings: none

Checks on this head: quest check --base origin/main passed (524 documents). No other local check was run after the merge of main; the diff is quest files only.

🤖 Generated with Claude Code

(Written by Claude Fable 5 with high)

kixelated and others added 2 commits November 10, 2026 20:04
Records the 2026-11-10 /quest-plan on lite-07 routing: every publisher stays
an origin node, holds and merged floors stay, and each side says everything
about routing on one unidirectional Announce Stream whose interest is a set
of prefixes edited in place. Splits the work into the interest set (model
and router) and the route stream (wire and sessions), narrows echo-order to
its model half, and plans the seqno bump fix, two offline-not-END fixes, the
browser mesh, and core and edge roles in the mesh overlay.

Co-Authored-By: Claude <noreply@anthropic.com>
The route model still counts to infinity with the echo on the neighbour's
FIFO once the origin sits behind a relay. Records the decision (epic item
25), grows echo-order to own the sound drain in the model, Sim, and router,
and keeps per-link costs and that shape in the mesh model.

Co-Authored-By: Claude <noreply@anthropic.com>
@kixelated
kixelated marked this pull request as ready for review November 11, 2026 04:55
@coderabbitai

coderabbitai Bot commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

Explain Change →

Pre-merge checks: Inconclusive 2

Failed Failed checks: 2 inconclusive

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

Simplify code

  • Commit to this branch
  • Create a new PR
  • 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

@pullfrog pullfrog Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ℹ️ No critical issues — two plan-accuracy nits inline, one findability note below.

Reviewed changes

  • One routing stream per side — item 21 and routes/route-stream.md replace the per-request stream split with one unidirectional Announce stream per endpoint, its interest a prefix set, an echo type of its own because both sides' Route IDs then share an ID space.
  • Interest as an edited prefix set — items 22-24 and routes/interest-set.md settle per-prefix floors and SYNCED, non-nesting sets, and swaps that re-send nothing both sets cover, superseding items 16 and 17.
  • A sound route drain — item 25 and routes/echo-order.md replace the per-neighbour echo with one that waits for the echoer's own downstream, carrying the origin-behind-a-relay counterexample that motivated it.
  • Seqno bumps and two offline misreports — m1/route-seqno-bumps.md narrows the unprompted bump to a route-link change, and m1/offline-cursor-fallback.md / m1/offline-js-handle.md own the two #8375 findings where a lost route reads as END.
  • Roles and browser transit — m3/mesh/overlay.md gains core and edge roles with product link pricing, and m5/browser-mesh.md plans forwarding tabs behind the Rust-to-TypeScript port, with m4/p2p/README.md and routes/js.md updated to match.

The code references, test names, config names, and wire limits the plans cite all check out against this tree (including the Gone::End capture-change arm, the two router.bump() sites, the residual_an_overtaking_echo_counts_to_infinity 3→8 climb, and MAX_MESSAGE_SIZE).

ℹ️ Four new quests are missing from their milestone indexes

quest/m1/README.md lists 24 of its 25 children and quest/m5/README.md lists every one, so the new offline-cursor-fallback, offline-js-handle, route-seqno-bumps, and browser-mesh quests are the only gaps — and the two offline quests are linked from nowhere except each other. quest check accepts unlisted children, so this is findability only, but if the milestone ## Required list is the priority index, four one-line entries would keep it complete.

Technical details
# Missing milestone index entries

## Affected sites
- `quest/m1/README.md` — no entry for `offline-cursor-fallback.md`, `offline-js-handle.md`, or `route-seqno-bumps.md`
- `quest/m5/README.md` — no entry for `browser-mesh.md`

## Required outcome
- Each new child appears in its milestone README's `## Required` list, matching how every other child of m1 and m5 is indexed.

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

The route model ran the deferred echo: it fails when a session closes before
answering. A hop list per origin route passes the same shapes, with the echo
ordered or not, so the fix lands on today's streams.

Co-Authored-By: Claude <noreply@anthropic.com>
@kixelated kixelated changed the title quest: plan lite-07's one routing stream per side, its interest set, and a sound route drain quest: plan lite-07's hop list on routes, one routing stream per side, and its interest set Nov 11, 2026
…nce-stream

# Conflicts:
#	quest/m2/cluster-routing/routes/README.md
… browser mesh

Co-Authored-By: Claude <noreply@anthropic.com>

@pullfrog pullfrog Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Important

The hop list's own-ID check has a scoped-session hole the model does not cover, and two spec-text updates are missing from the work list.

Reviewed changes

The fix changed from a deferred echo to a hop list since the prior review:

  • A hop list per origin route — item 25 and the retitled echo-order.md now make each route name the relays it crossed, with a node never using one that names itself; the deferred echo is recorded as run and superseded, including the two-flap failure that killed it.
  • The model evidence is written down — echo-order.md cites DRAIN.md on route-drain-counterexamples (5e7e3eb43) for every shape, bound, and stopped run, and gates the list's unmeasured message cost on #8479's announce budget before touching the router.
  • Downstream plans moved with it — interest-set.md starts from the hop list before moving the echo onto one FIFO, route-stream.md records that the fix no longer depends on it, js.md decodes the list, and the epic's loop-freedom bullet states the rule.
  • Main merged in — the merge brings 529fa6ac9 up to date.

I checked the new claims against the reference branch and the tree: the DRAIN.md state counts, bounds, and "not run" list match the plan, 5e7e3eb43 is that branch's head, CountToInfinity.cfg is the open-finding config with the origin as a triangle node, MAX_HOPS is 32, and the model's origin does ignore routes for its own identity.

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

@pullfrog pullfrog Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✅ No new issues in be4049e5. The two open threads from the first review are addressed cleanly, and approval is withheld only because the three findings from the previous review are still open.

Reviewed changes

  • JS's entry point named correctly — route-stream.md and js.md now say routes() in JS and announced() in Rust, in both the goal and the code-replacement list.
  • Neighbour-key ownership settled — interest-set.md now states that route::Node keeps registering each announce stream under its own key until the route stream lands, and that only the router gains the one-key ability here (used by Sim and the tests), so "changes no behaviour on its own" holds.
  • The route stream picks it up — route-stream.md now says the same change is what makes the sessions register both directions under that key.
  • Browser mesh indexed — quest/m5/README.md lists browser-mesh.md in ## Required.

Pullfrog  | Fix it ➔ | View workflow run | Using deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) | 𝕏

…pdate

Co-Authored-By: Claude <noreply@anthropic.com>

@pullfrog pullfrog Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ℹ️ No critical issues — one accuracy note on the final work item.

Reviewed changes

Since be4049e5 the delta is one hunk in routes/echo-order.md, settling the scoped-grant hole and the two spec-text gaps from the last review:

  • Hop-list entries are never qualified — a relay still files a scoped peer's origin under a qualified key, but forwards list entries as received, since no relay can derive another's qualification. A scoped peer can then only edit lists on routes filed under its own qualified identities, and a lap through it is still refused by the requalify rule, to be covered by a Sim case because the model has no scoped grants.
  • The draft's Node ID Parameter joins the work list — a node that only forwards must now declare a Node ID, which the SETUP text currently contradicts.
  • The handoff contract's drain bullet is named — it joins the loop-freedom bullet and decision 6 as an epic site to update.

ℹ️ The epic-update list names the wrong bullet

echo-order.md:145-149 names the loop-freedom bullet, decision 6, and the drain bullet. The loop-freedom bullet (quest/m2/cluster-routing/routes/README.md:190-198) already states the hop-list rule after 7daa3267, while the fresh-identity bullet (README.md:145-151) still argues from the echo bound: keeping the feasibility distance until every ROUTE_END is echoed leaves a collected incarnation reappearing only from an in-flight message that delivers the retraction next, which is exactly what the origin-behind-a-relay case refutes. Name that bullet instead so the implementer updates a site that still carries the refuted claim.

Technical details
# Epic sites that still rest on echo-alone safety

## Affected sites
- `quest/m2/cluster-routing/routes/echo-order.md:145-149` — update list names the loop-freedom bullet
- `quest/m2/cluster-routing/routes/README.md:190-198` — loop-freedom bullet, already rewritten to the hop list in `7daa3267`
- `quest/m2/cluster-routing/routes/README.md:145-151` — fresh-identity bullet, still grounds reappearance in the retained distance and the echo
- `quest/m2/cluster-routing/routes/README.md:387-394` — drain bullet, correctly named ("as safe as a fresh node joining")

## Required outcome
- The work item names every epic site that still carries the echo-alone justification, so `README.md:145-151` is not left arguing the premise the model refuted.

## Open questions for the human (optional)
- The loop-freedom bullet may still want a rewording pass; it already states the rule today.

Pullfrog  | Fix it ➔ | View workflow run | Using deepseek-v4.1-flash-1017 (free via Pullfrog for OSS) | 𝕏

@kixelated
kixelated added this pull request to the merge queue Nov 11, 2026
Merged via the queue into main with commit 52fa6b2 Nov 11, 2026
9 of 11 checks passed
@kixelated
kixelated deleted the quest-plan/lite07-route-stream branch November 11, 2026 08:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant