fix(net)!: a lite-07 route names the nodes it crossed, and is never feasible where it has been

.claude/skills/verify-route/SKILL.md

@@ -5,7 +5,7 @@ description: Model-check the lite-07 route layer (`rs/moq-net/src/route/`) with
 
 # Verify the route layer
 
-`rs/moq-net/verify/route/RouteHandoff.tla` models one origin identity in `route::Router` as `route::tests::Sim` drives it: every router entry point is one atomic step ending in `update`, ROUTE, batches, and ROUTE_REQUEST share one FIFO per direction, and echoes travel on their own queue. TLC checks every ordering of those messages in a triangle of the origin and two relays, under the bounds in the config.
+`rs/moq-net/verify/route/RouteHandoff.tla` models one origin identity in `route::Router` as `route::tests::Sim` drives it: every router entry point is one atomic step ending in `update`, ROUTE, batches, and ROUTE_REQUEST share one FIFO per direction, and echoes travel on their own queue, free to overtake. TLC checks every ordering of those messages on the mesh and bounds each config names.
 
 ## Rules
 
@@ -20,38 +20,47 @@ Each rule is an INVARIANT; the harm says why it matters.
 | `NoRegression` | A reader never sees an UPDATE to an older item. | A stale announcement replaces a newer one. |
 | `LoopFree` | Selected next hops never cycle. | Requests loop between relays. |
 | `QuietIsSettled` | Once nothing is in flight, each relay reaching the origin shows its claims, available, and routes only while it has any; each cut-off relay shows nothing and keeps no route, distance, or request. | Routing never converges, or a dead origin stays shown. |
+| `SimplePaths` | Every route held or in flight names a loop-free path from the origin to its sender, at that path's cost. | A node took back a route that crossed it, the first step of a count to infinity. |
 | `NoCountToInfinity` | No relay selects a route longer than a loop-free path. | Stale routes bounce between relays with no bound. |
 
-The constraint `Bounded` stops exploring one hop past `NoCountToInfinity`, so a count to infinity shows up there instead of running TLC forever.
+`SimplePaths` needs no search to believe: a node sends a route only after adding itself to hops that did not name it. It holds whatever a node forgot, which is why `NoCountToInfinity` no longer rests on the echo.
 
 ## Run
 
 ```sh
 just rs tla moq-net/verify/route/RouteHandoff.tla
-just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/CountToInfinity.cfg
+just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/Behind.cfg
+just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/BehindDear.cfg
 ```
 
-The first checks every rule but `NoCountToInfinity`: about 3.7M states, two minutes on 32 cores, and it passes at the sync commit. The second fails at the sync commit on the open finding below.
+| Config | Mesh | Bounds | Distinct states |
+| --- | --- | --- | --- |
+| `RouteHandoff.cfg` | The origin and two relays in a triangle. | 2 claim changes, 2 session changes, 1 collection | 3,545,311 |
+| `Behind.cfg` | The origin behind relay 1, which sits in a triangle with relays 2 and 3. | 1 claim change, 1 session change | 3,033,111 |
+| `BehindDear.cfg` | The same, with relay 3 nearer the origin than relay 2. | 1 claim change, 1 session change | 5,377,597 |
 
-Read a counterexample with `/statechart`, passing it the spec, a config, and `RouteHandoff.view.ts`, which labels each relay's route and each step as the message that arrives. It gives the shortest path to each broken rule in those words.
+All three pass at the sync commit. Each takes minutes on 4 workers, so run them last. First run what answers in seconds:
 
-## Open finding: an overtaking echo counts to infinity
+- `just rs test -p moq-net --lib -E 'test(/route::/)'`. `sweep_no_route_outgrows_a_loop_free_path` delivers every message and echo in a random order on random meshes with unequal costs, flaps, restarts, and collections, and checks the metric bound, loop freedom, and the quiet state. Raise its case count for a wider search: 40,000 cases run in 15 seconds in release.
+- TLC's simulation mode on the config in question, which samples deep runs the exhaustive bounds do not reach: add `-simulate num=3000 -depth 80`.
 
-`CountToInfinity.cfg` fails. A node drops its feasibility distance once every neighbour echoed its ROUTE_END (`update` in `mod.rs`), on the reasoning that no advertisement derived from its own can then still arrive. But an echo travels apart from the echoer's own routes (the answering stream carries it, per `node.rs`), so it can overtake an advertisement that neighbour derived from this node's and sent before the end. The node then accepts that advertisement as a fresh, longer route, and two relays can count up without end while each shows the broadcast available. `residual_an_overtaking_echo_counts_to_infinity` in `route/tests/routing.rs` replays it on the router. Once it is fixed, flip that test, move `NoCountToInfinity` into `RouteHandoff.cfg`, and delete `CountToInfinity.cfg`.
+Both behind-a-triangle configs fail `SimplePaths` within seconds if `Crossed` is made false, which is the count to infinity the hops fix: a relay drops its distance once its neighbours echoed, and takes back a copy of its own route that a third relay still held.
+
+Read a counterexample with `/statechart`, passing it the spec, a config, and `RouteHandoff.view.ts`, which labels each relay's route and each step as the message that arrives. It gives the shortest path to each broken rule in those words. The view names the triangle's sessions and assumes equal costs.
 
 ## Reading a failure
 
 A counterexample is a path through the model, not yet a bug. Replay it on the router with `Sim` (`hold`, `deliver`, `deliver_ack`, `disconnect`, `collect`), one call per step. If the router does not follow the path, the model is wrong: fix the model to match the code. If it does, report the path and the rule in the code's words. Do not weaken a rule, add a constraint, or shrink the bounds until the check passes.
 
 ## Coverage
 
-Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07.. -- rs/moq-net/src/route/` to see what changed since. After a change to a covered function, mirror it in the model, rerun both configs, and move the sync commit forward only once the model describes the code at the new commit.
+Sync commit: `c916855d163ff5641ad18cfb8e14b76dababd99a`, plus the change that added a route's hops ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)). Run `git log c916855d16.. -- rs/moq-net/src/route/` to see what changed since. After a change to a covered function, mirror it in the model, rerun every config, and move the sync commit forward only once the model describes the code at the new commit.
 
 | Code (`rs/moq-net/src/route/`) | Model |
 | --- | --- |
-| `mod.rs` `feasible`, `selected`, `infeasible`, `recoverable`, `live`, `certifiers` | `Feasible`, `Selected`, `InfeasibleSet`, `Recoverable`, `Live`, `Certifiers` |
+| `mod.rs` `feasible`, `Entry::crossed`, `eligible`, `metric`, `selected`, `infeasible`, `recoverable`, `live`, `certifiers` | `Feasible`, `Crossed`, `Eligible`, `Through`, `Selected`, `InfeasibleSet`, `Recoverable`, `Live`, `Certifiers` |
 | `mod.rs` `certified`, `prune`, `adopted` | `Certified`, `Prune`, `Adopted` |
-| `mod.rs` `update`, `record`, `advertise`, `requests` | `Update`, `Record`, `Plan`, `Requests` |
+| `mod.rs` `update`, `recompute`, `record`, `advertise`, `requests` | `Update` and its `prune`, `Record`, `Plan`, `Requests` |
 | `mod.rs` `show`, `shown_now` | `Events`, `ShownNow` |
 | `mod.rs` `route`, `batch`, `request`, `echo` | `OnRoute`, `OnBatch`, `OnRequest`, `Deliver`, `DeliverAck` |
 | `mod.rs` `connect`, `peer_interest`, `disconnect`, `collect`, `change` | `Connect`, `Opened`, `Disconnect`, `Closed`, `Collect`, `ChangeClaim` |
@@ -60,4 +69,4 @@ Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07
 
 ## Not covered
 
-The model fixes every interest at the root, so it leaves out wildcards, `present`/`represent`/`retire`, interest changes, and the hidden `current` regions; prune's region bookkeeping reduces to "no certifier has a floor". It also leaves out scoped grants and qualified keys, GOAWAY, link priority, costs other than 1, upstream links, identity rotation and restart, and `node.rs`'s per-stream keys. A batch carries the sender's whole presentation, equal to applying its diff on a FIFO stream. The origin drops the ROUTEs and batches it hears for its own identity, which change nothing there. A pass covers one claim, two revisions, two session opens or closes, and one collection in that triangle. `sweep_handoff` and `sweep_scoped_handoff` still own the rest.
+The model fixes every interest at the root, so it leaves out wildcards, `present`/`represent`/`retire`, interest changes, and the hidden `current` regions; prune's region bookkeeping reduces to "no certifier has a floor". It also leaves out scoped grants and qualified keys (so `advertised`, which only they read), GOAWAY, link priority, costs other than 1 and 2, the hop limit, the informational RTT, upstream links, identity rotation and restart, and `node.rs`'s per-stream keys. A batch carries the sender's whole presentation, equal to applying its diff on a FIFO stream. The origin drops the ROUTEs and batches it hears for its own identity, which change nothing there. A pass covers one claim at the bounds in the table above, and no mesh of more than three relays. `sweep_no_route_outgrows_a_loop_free_path`, `sweep_handoff`, and `sweep_scoped_handoff` still own the rest: larger meshes, more churn, restarts, and scoped grants.

doc/bin/relay/cluster.md

@@ -16,9 +16,11 @@ same way so the cluster converges instead of flapping. Both wire protocols
 carry it: natively on moq-lite up to moq-lite-06, and via the
 [cluster extension](/draft/moq-cluster) on moq-transport.
 
-moq-lite-07-wip carries no hop list. Each publishing node declares a random
-routing identity, and relays run a distance-vector route to it, loop-free by
-Babel's feasibility condition, so every claim of one origin shares that route.
+moq-lite-07-wip carries the list once per publishing node instead of once per
+broadcast. Each publishing node declares a random routing identity, and relays
+run a distance-vector route to it, loop-free by Babel's feasibility condition,
+so every claim of one origin shares that route. The route names the relays it
+crossed, and a relay never uses one that names itself.
 The first relay a request reaches picks the origin node, by a hash of the path
 and the node's identity that every relay computes alike, and names it on the
 request so later hops follow their own route to that node. A relay running both
@@ -110,8 +112,9 @@ max_hops = 6
 
 The same setting is `--cluster-max-hops` or `MOQ_CLUSTER_MAX_HOPS`. It covers
 moq-lite-03 through moq-lite-06 and moq-transport drafts 18 through 22 when
-the MoQ Cluster extension is negotiated. moq-lite-07-wip routes carry no hop
-path, so it does not bound them. A forwarded path counts this relay's
+the MoQ Cluster extension is negotiated. A moq-lite-07-wip route crosses at
+most 32 nodes whatever this is set to: it does not hunt for paths, so a lower
+cap would only hide a short path behind a cheaper long one. A forwarded path counts this relay's
 own hop even when its peer appends it on receipt. Older versions and peers
 without hop paths hide their depth, which this setting cannot bound.
 
@@ -182,7 +185,8 @@ the same one for a given path. A publisher connected straight to the relay is
 not hashed at its own path: its newest session wins, so a publisher that
 restarts takes over from its lingering old session at once.
 
-moq-lite-07-wip carries no hop list, so both hop-list steps drop out: the first
+moq-lite-07-wip keeps its hop list on the route to a publishing node, not on
+each broadcast, so both hop-list steps drop out: the first
 relay ranks the origin nodes announcing a path the same way otherwise, and
 remaining ties hash the path with each node's routing identity. Later hops
 follow their own route to the node it picked. Routes learned over an older
@@ -295,7 +299,8 @@ decides which relays receive the cluster token.
 
 Each relay has an identity that it uses for loop detection and routing, and
 declares in SETUP on moq-lite-05 and later: a Hop ID added to each route's hop
-list, or on the opt-in `moq-lite-07-wip` a Node ID naming the route's origin. It is random on every start, so a
+list, or on the opt-in `moq-lite-07-wip` a Node ID naming the route's origin,
+which it also adds to the hops of each route it forwards. It is random on every start, so a
 restarted relay is a new node to the rest of the mesh, and there is no setting
 to pin it.