From 79cbf574d513442e25107b5816f96cd74b43f4cf Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Tue, 10 Nov 2026 17:07:46 -0800 Subject: [PATCH 01/17] chore(quest): claim quest/m2/cluster-routing/routes/echo-order.md Quest-Claim: 3905a4a2b202fe9e From 81c0698295b51fc6c3d8b654f2ce96ee78e0c724 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Tue, 10 Nov 2026 17:26:19 -0800 Subject: [PATCH 02/17] test(net): an echo arrives behind the echoer's routes in the route model and Sim The model and Sim carry each ROUTE_END echo on the FIFO behind the echoer's routes. NoCountToInfinity now holds and joins RouteHandoff.cfg, and the residual count-to-infinity test becomes one that the metric never passes the longest loop-free path. Co-Authored-By: Claude Opus 5.5 --- .claude/skills/verify-route/SKILL.md | 15 +++-- quest/m2/cluster-routing/routes/README.md | 6 +- rs/moq-net/src/route/tests/handoff.rs | 13 ++--- rs/moq-net/src/route/tests/mod.rs | 48 +++------------- rs/moq-net/src/route/tests/routing.rs | 59 ++++++++++---------- rs/moq-net/verify/route/CountToInfinity.cfg | 20 ------- rs/moq-net/verify/route/RouteHandoff.cfg | 2 +- rs/moq-net/verify/route/RouteHandoff.tla | 46 +++++++-------- rs/moq-net/verify/route/RouteHandoff.view.ts | 9 +-- 9 files changed, 79 insertions(+), 139 deletions(-) delete mode 100644 rs/moq-net/verify/route/CountToInfinity.cfg diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index d2a2a815011..90cb4383c0f 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.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, ROUTE_REQUEST, and echoes share one FIFO per direction, so an echo arrives behind every route its sender sent before it. TLC checks every ordering of those messages in a triangle of the origin and two relays, under the bounds in the config. ## Rules @@ -28,20 +28,19 @@ The constraint `Bounded` stops exploring one hop past `NoCountToInfinity`, so a ```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 ``` -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. +It checks every rule: about 1.2M distinct states, under a minute on 24 cores. 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. -## Open finding: an overtaking echo counts to infinity +## Open finding: the echo's stream -`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`. +`NoCountToInfinity` holds only because an echo arrives behind every route its sender sent before it: otherwise it can overtake an advertisement the echoer derived from this node's, and the node, its distance already drained, accepts it as a fresh, longer route (`an_echo_never_overtakes_the_echoers_routes` in `route/tests/routing.rs`). The model and `Sim` carry the echo that way, but `node.rs` still sends it back on the stream the ROUTE_END came on, apart from the echoer's routes, until [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) moves it. ## 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. +A counterexample is a path through the model, not yet a bug. Replay it on the router with `Sim` (`hold`, `deliver`, `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 @@ -53,10 +52,10 @@ Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07 | `mod.rs` `certified`, `prune`, `adopted` | `Certified`, `Prune`, `Adopted` | | `mod.rs` `update`, `record`, `advertise`, `requests` | `Update`, `Record`, `Plan`, `Requests` | | `mod.rs` `show`, `shown_now` | `Events`, `ShownNow` | -| `mod.rs` `route`, `batch`, `request`, `echo` | `OnRoute`, `OnBatch`, `OnRequest`, `Deliver`, `DeliverAck` | +| `mod.rs` `route`, `batch`, `request`, `echo` | `OnRoute`, `OnBatch`, `OnRequest`, `Deliver`, `DeliverEcho` | | `mod.rs` `connect`, `peer_interest`, `disconnect`, `collect`, `change` | `Connect`, `Opened`, `Disconnect`, `Closed`, `Collect`, `ChangeClaim` | | `view.rs` `View::merge`, `View::restrict` | `Merge`, `Certify` | -| `tests/mod.rs` `Sim` queues and `revivals`, `false_ends` | `q`, `acks`, `revivals`, `falseEnds` | +| `tests/mod.rs` `Sim` queues and `revivals`, `false_ends` | `q`, `revivals`, `falseEnds` | ## Not covered diff --git a/quest/m2/cluster-routing/routes/README.md b/quest/m2/cluster-routing/routes/README.md index e77823753b9..5aca880554d 100644 --- a/quest/m2/cluster-routing/routes/README.md +++ b/quest/m2/cluster-routing/routes/README.md @@ -179,8 +179,10 @@ the bullets below are the contract it carries. - Loop freedom is Babel's feasibility condition (RFC 8966) keyed by node: accept a route if its seqno is newer, or equal with a metric below the feasibility distance. Only the origin advances its seqno. Retraction is - ROUTE_HOLD or ROUTE_END. The route model found a count to infinity - (2026-11-10): an echo can overtake a route derived from the echoed one; + ROUTE_HOLD or ROUTE_END. Draining a distance relies on each ROUTE_END + echo arriving behind every route the echoer sent before it: an echo that + overtakes a route derived from the echoed one counts to infinity (the + route model, 2026-11-10); [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) orders it. - Starvation recovery is Babel's seqno request (RFC 8966 s3.8, decided 2026-10-12). A node whose routes to an origin are all infeasible sends diff --git a/rs/moq-net/src/route/tests/handoff.rs b/rs/moq-net/src/route/tests/handoff.rs index f76629eeadc..64715bbc06b 100644 --- a/rs/moq-net/src/route/tests/handoff.rs +++ b/rs/moq-net/src/route/tests/handoff.rs @@ -1215,18 +1215,13 @@ fn churn(rng: &mut XorShift) -> Sim { sim.reconnect(first + origin); } _ => { - // Echoed ROUTE_ENDs interleave freely with the echoing node's routes. for _ in 0..rng.next(6) { - let busy: Vec<(bool, usize, usize)> = (sim.busy().into_iter().map(|(from, to)| (false, from, to))) - .chain(sim.busy_acks().into_iter().map(|(from, to)| (true, from, to))) - .collect(); + let busy = sim.busy(); if busy.is_empty() { break; } - match busy[rng.next(busy.len() as u64) as usize] { - (false, from, to) => sim.deliver(from, to), - (true, from, to) => sim.deliver_ack(from, to), - }; + let (from, to) = busy[rng.next(busy.len() as u64) as usize]; + sim.deliver(from, to); } } } @@ -1429,7 +1424,7 @@ fn a_restarted_floorless_route_drops_what_it_no_longer_carries() { assert!(sim.run()); sim.unannounce(origin, "live/a/x"); assert!(sim.run()); - while sim.deliver_ack(z, x) {} + while sim.deliver(z, x) {} sim.connect(x, local); assert!(sim.run()); sim.release(z, x); diff --git a/rs/moq-net/src/route/tests/mod.rs b/rs/moq-net/src/route/tests/mod.rs index f3060404833..dcdf0ecaeee 100644 --- a/rs/moq-net/src/route/tests/mod.rs +++ b/rs/moq-net/src/route/tests/mod.rs @@ -104,6 +104,10 @@ enum Msg { id: Id, seqno: Seqno, }, + /// The echo of a ROUTE_END, behind every route its sender sent before it. + Echo { + id: Id, + }, } #[derive(Clone, Debug, PartialEq, Eq)] @@ -149,8 +153,6 @@ pub(super) struct Sim { grants: BTreeSet<&'static str>, up: BTreeSet<(Node, Node)>, queues: BTreeMap<(Node, Node), VecDeque>, - /// Echoed ROUTE_ENDs: unordered against the echoing node's own routes. - acks: BTreeMap<(Node, Node), VecDeque>, held: BTreeSet<(Node, Node)>, history: BTreeMap>, /// Every request sent, to spot a repeat. @@ -171,7 +173,6 @@ impl Sim { grants: BTreeSet::new(), up: BTreeSet::new(), queues: BTreeMap::new(), - acks: BTreeMap::new(), held: BTreeSet::new(), history: BTreeMap::new(), requested: BTreeSet::new(), @@ -242,7 +243,6 @@ impl Sim { self.up.remove(&Self::pair(a, b)); for (x, y) in [(a, b), (b, a)] { self.queues.remove(&(x, y)); - self.acks.remove(&(x, y)); self.held.remove(&(x, y)); self.nodes[y].disconnect(x); } @@ -397,42 +397,19 @@ impl Sim { interest, } => router.batch(from, id, changes, floor, interest), Msg::Request { id, seqno } => router.request(from, id, seqno), + Msg::Echo { id } => router.echo(from, id), } self.stats.delivered += 1; self.flush(); true } - /// Deliver one echoed ROUTE_END from `from` to `to`, even if held. - pub fn deliver_ack(&mut self, from: Node, to: Node) -> bool { - let Some(id) = self.acks.get_mut(&(from, to)).and_then(VecDeque::pop_front) else { - return false; - }; - self.nodes[to].echo(from, id); - self.stats.delivered += 1; - self.flush(); - true - } - pub fn queued(&self, from: Node, to: Node) -> usize { self.queues.get(&(from, to)).map_or(0, VecDeque::len) } - pub fn queued_acks(&self, from: Node, to: Node) -> usize { - self.acks.get(&(from, to)).map_or(0, VecDeque::len) - } - pub fn busy(&self) -> Vec<(Node, Node)> { - Self::nonempty(&self.queues) - } - - pub fn busy_acks(&self) -> Vec<(Node, Node)> { - Self::nonempty(&self.acks) - } - - fn nonempty(queues: &BTreeMap<(Node, Node), VecDeque>) -> Vec<(Node, Node)> { - queues - .iter() + (self.queues.iter()) .filter(|(_, queue)| !queue.is_empty()) .map(|(key, _)| *key) .collect() @@ -447,20 +424,12 @@ impl Sim { pub fn settle(&mut self, rounds: usize) -> bool { for _ in 0..rounds { let ready: Vec<(Node, Node)> = self.busy().into_iter().filter(|key| !self.held.contains(key)).collect(); - let acks: Vec<(Node, Node)> = self - .busy_acks() - .into_iter() - .filter(|key| !self.held.contains(key)) - .collect(); - if ready.is_empty() && acks.is_empty() { + if ready.is_empty() { return true; } for (from, to) in ready { self.deliver(from, to); } - for (from, to) in acks { - self.deliver_ack(from, to); - } } false } @@ -497,8 +466,7 @@ impl Sim { } Out::Echo { to, id } => { self.stats.route_msgs += 1; - self.acks.entry((node, to)).or_default().push_back(id); - continue; + (to, Msg::Echo { id }) } }; self.queues.entry((node, to)).or_default().push_back(msg); diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index 29f44971e61..a8dffa5cd15 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -152,7 +152,7 @@ fn collection_keeps_the_feasibility_distance_against_a_queued_echo() { sim.release(b, c); sim.release(c, b); assert!(sim.run()); - assert!(sim.queued_acks(leaf, b) > 0, "the leaf's echo waits"); + assert!(sim.queued(leaf, b) > 0, "the leaf's echo waits"); assert!(sim.remembers(b, 7), "the leaf may still hold b's advertisement"); sim.release(leaf, b); assert!(sim.run()); @@ -947,17 +947,14 @@ fn a_fresh_uncertified_claim_waits_on_an_older_floor() { } } -/// Pins a count to infinity that `verify/route/RouteHandoff.tla` found. An echo -/// travels apart from the echoing node's routes, so it can overtake an -/// advertisement that node derived from this one's. b learned its route from a -/// and advertised it back, then ended it on a's ROUTE_END. Its echo arrives -/// first, so a drains its feasibility distance and accepts b's stale -/// advertisement as a fresh, longer route to an origin neither reaches through -/// the other. With every echo overtaking, the two relays count up without end. -/// A fix keeps a's distance until that advertisement can no longer arrive: -/// then a refuses it and the route is gone. +/// An echo travels behind every route its sender sent before it, so it never +/// overtakes an advertisement the echoing node derived from this one's. b +/// learned its route from a and advertised it back, then ended it on a's +/// ROUTE_END. a refuses that advertisement while its feasibility distance +/// stands, and drains the distance only on the echo behind it, so neither relay +/// selects a route longer than a loop-free path to the origin. #[test] -fn residual_an_overtaking_echo_counts_to_infinity() { +fn an_echo_never_overtakes_the_echoers_routes() { let (origin, a, b) = (0, 1, 2); let mut sim = Sim::new(3); sim.join(origin, a, 1); @@ -973,27 +970,27 @@ fn residual_an_overtaking_echo_counts_to_infinity() { sim.disconnect(origin, a); assert!(sim.run()); assert!(!sim.holds(b, 7), "b let go on a's ROUTE_END"); - assert!(sim.deliver_ack(b, a), "b's echo overtakes its own advertisement"); - assert!(!sim.remembers(a, 7), "a drained its distance"); + assert!(sim.queued(b, a) > 1, "b's advertisement, then its echo"); + while sim.queued(b, a) > 1 { + sim.deliver(b, a); + assert!(sim.remembers(a, 7), "a keeps its distance until the echo"); + assert!(sim.route(a, 7).is_none(), "a refuses b's stale advertisement"); + } assert!(sim.deliver(b, a)); - assert_eq!( - sim.route(a, 7).map(|route| (route.next, route.metric)), - Some((Some(b), 3)) - ); - - // Each round, the relay that just drained accepts the other's stale route. - for round in 0..6 { - let (from, to) = if round % 2 == 0 { (b, a) } else { (a, b) }; - let mut peak = 0; - while sim.deliver(from, to) { - peak = peak.max(sim.route(to, 7).map_or(0, |route| route.metric)); + assert!(!sim.remembers(a, 7), "the echo drained a's distance"); + + // The longest loop-free path to the origin is through the other relay. + sim.release(origin, b); + sim.release(b, a); + loop { + for node in [a, b] { + assert!(sim.route(node, 7).is_none_or(|route| route.metric <= 2)); } - // The origin echoes b's ends, and echoes overtake every route still waiting. - while sim.deliver(b, origin) {} - while [(a, b), (b, a), (origin, b)] - .into_iter() - .any(|(x, y)| sim.deliver_ack(x, y)) - {} - assert_eq!(peak, 3 + round, "round {round}"); + let busy = sim.busy(); + let Some(&(from, to)) = busy.first() else { + break; + }; + sim.deliver(from, to); } + assert_eq!(next(&sim, a, 7), Some(b)); } diff --git a/rs/moq-net/verify/route/CountToInfinity.cfg b/rs/moq-net/verify/route/CountToInfinity.cfg deleted file mode 100644 index 5995cad17b8..00000000000 --- a/rs/moq-net/verify/route/CountToInfinity.cfg +++ /dev/null @@ -1,20 +0,0 @@ -\* The open count-to-infinity finding, checked apart so RouteHandoff.cfg still -\* checks every other rule. Once it holds, move NoCountToInfinity into -\* RouteHandoff.cfg and delete this file. -CONSTANTS - Nodes = {0, 1, 2} - Origin = 0 - Leaves = {} - Links = {{0, 1}, {0, 2}, {1, 2}} - Claims = {"x"} - MaxRev = 2 - MaxFlaps = 2 - MaxCollects = 1 - -SPECIFICATION Spec - -INVARIANTS - NoCountToInfinity - -CONSTRAINT - Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.cfg b/rs/moq-net/verify/route/RouteHandoff.cfg index d6020df9941..a4c2358fe36 100644 --- a/rs/moq-net/verify/route/RouteHandoff.cfg +++ b/rs/moq-net/verify/route/RouteHandoff.cfg @@ -1,6 +1,5 @@ \* An origin (0) and two relays (1, 2) in a triangle, so a relay can fail \* over through the other and Babel's feasibility decides whether it may. -\* NoCountToInfinity lives in CountToInfinity.cfg while its finding is open. CONSTANTS Nodes = {0, 1, 2} Origin = 0 @@ -21,6 +20,7 @@ INVARIANTS NoRegression LoopFree QuietIsSettled + NoCountToInfinity CONSTRAINT Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.tla b/rs/moq-net/verify/route/RouteHandoff.tla index ccca07819cc..e4cd03ed873 100644 --- a/rs/moq-net/verify/route/RouteHandoff.tla +++ b/rs/moq-net/verify/route/RouteHandoff.tla @@ -7,9 +7,9 @@ (* `request`, `echo`, `collect`, `connect`/`peer_interest`, `disconnect`, *) (* `announce`/`unannounce`) is one atomic step that ends in `update`, as *) (* in the code. Messages travel as the Sim queues them: ROUTE, batches, *) -(* and ROUTE_REQUEST on one FIFO per direction, echoed ROUTE_ENDs on their *) -(* own queue. A session opens and closes atomically, dropping what was in *) -(* flight. *) +(* ROUTE_REQUEST, and echoed ROUTE_ENDs on one FIFO per direction, so an *) +(* echo arrives behind every route its sender sent before it. A session *) +(* opens and closes atomically, dropping what was in flight. *) (* *) (* Scope: every node watches the root, links cost 1 with equal priority, *) (* no scoped grants, no GOAWAY, and the origin keeps its identity. Claims *) @@ -55,11 +55,11 @@ NotShown == [item |-> None, avail |-> FALSE] RouteMsg(reach) == [type |-> "route", reach |-> reach, view |-> NoView, seq |-> 0] BatchMsg(view) == [type |-> "batch", reach |-> NoReach, view |-> view, seq |-> 0] RequestMsg(seq) == [type |-> "request", reach |-> NoReach, view |-> NoView, seq |-> seq] +EchoMsg == [type |-> "echo", reach |-> NoReach, view |-> NoView, seq |-> 0] VARIABLES up, \* open sessions (`Sim::up`) q, \* q[<>]: ROUTE, batches, and ROUTE_REQUEST from m to n, in order - acks, \* acks[<>]: echoed ROUTE_ENDs from m to n rev, \* the origin's claim revision (`Origin::view.floors[""]`) own, \* the origin's claims (`Origin::view.items`) seqno, \* the origin's route seqno (`Origin::seqno`) @@ -72,7 +72,7 @@ VARIABLES flaps, collects -vars == <> \* The origin's view and seqno. @@ -249,7 +249,8 @@ Update(n, s0, ov, ups, eb) == IN [s |-> [s5 EXCEPT !.shown = now], out |-> out, ev |-> ev] \* The origin ignores every ROUTE and batch it hears for its own identity, so -\* only ROUTE_REQUEST and ROUTE_END (which it echoes) are queued toward it. +\* only ROUTE_REQUEST, ROUTE_END (which it echoes), and echoes are queued +\* toward it. \* Dropping the rest changes no behavior and keeps the state space small. Heeded(d, m) == d[2] # Origin \/ m.type = "request" \/ (m.type = "route" /\ m.reach.kind = "none") @@ -288,7 +289,6 @@ InitNode == [ Init == /\ up = Links /\ q = [d \in Dirs |-> <<>>] - /\ acks = [d \in Dirs |-> 0] /\ rev = 0 /\ own = NoItems /\ seqno = 0 @@ -311,7 +311,7 @@ ChangeClaim(c, item) == /\ own' = own1 /\ hist' = Append(hist, own1) /\ Commit([n \in {Origin} |-> Update(Origin, st[Origin], ov1, up, ended[Origin])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> \* A new claim, or new attributes for one, under a fresh revision. Announce(c) == rev < MaxRev /\ ChangeClaim(c, rev + 1) @@ -364,8 +364,10 @@ Deliver(d) == LET m == d[1] n == d[2] msg == Head(q[d]) - q0 == [q EXCEPT ![d] = Tail(@)] isEnd == msg.type = "route" /\ msg.reach.kind = "none" + \* Every ROUTE_END is echoed once applied, ahead of what the update sends. + q0 == [q EXCEPT ![d] = Tail(@), + ![<>] = IF isEnd THEN Append(@, EchoMsg) ELSE @] \* Only the origin advances its seqno to answer a request. ov1 == IF n = Origin /\ msg.type = "request" THEN [OV EXCEPT !.seq = Max(seqno, msg.seq)] ELSE OV @@ -378,8 +380,7 @@ Deliver(d) == [] msg.type = "batch" -> OnBatch(st[n], m, msg.view) [] OTHER -> OnRequest(st[n], m, msg.seq) IN /\ q[d] # <<>> - \* Every ROUTE_END is echoed once applied. - /\ acks' = IF isEnd THEN [acks EXCEPT ![<>] = @ + 1] ELSE acks + /\ msg.type # "echo" /\ seqno' = ov1.seq /\ IF skip THEN /\ q' = q0 @@ -387,16 +388,18 @@ Deliver(d) == ELSE Commit([x \in {n} |-> Update(n, s1, ov1, up, ended[n])], q0) /\ UNCHANGED <> -\* `echo`: an echoed ROUTE_END comes back (`Sim::deliver_ack`). -DeliverAck(d) == +\* `echo`: an echoed ROUTE_END comes back, behind the echoer's earlier routes. +DeliverEcho(d) == LET m == d[1] n == d[2] - IN /\ acks[d] > 0 - /\ acks' = [acks EXCEPT ![d] = @ - 1] + q0 == [q EXCEPT ![d] = Tail(@)] + IN /\ q[d] # <<>> + /\ Head(q[d]).type = "echo" /\ IF st[n].unacked[m] = 0 - THEN UNCHANGED <> + THEN /\ q' = q0 + /\ UNCHANGED <> ELSE Commit([x \in {n} |-> - Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n])], q) + Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n])], q0) /\ UNCHANGED <> ----------------------------------------------------------------------------- @@ -424,7 +427,7 @@ Connect(l) == /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x IN Update(x, Opened(st[x], y), OV, up1, ended[x])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> Disconnect(l) == LET up1 == up \ {l} @@ -433,7 +436,6 @@ Disconnect(l) == /\ flaps < MaxFlaps /\ up' = up1 /\ flaps' = flaps + 1 - /\ acks' = [d \in Dirs |-> IF {d[1], d[2]} = l THEN 0 ELSE acks[d]] /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x IN Update(x, Closed(st[x], y), OV, up1, ended[x])], q0) @@ -450,9 +452,9 @@ Collect(n) == !.heard = [m \in Nodes |-> NoHeard], !.pending = NoPending], OV, up, [c \in Claims |-> None])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> -Quiet == \A d \in Dirs : q[d] = <<>> /\ acks[d] = 0 +Quiet == \A d \in Dirs : q[d] = <<>> \* Nothing is in flight and no more churn is allowed: the run is over. Done == @@ -462,7 +464,7 @@ Done == Next == \/ \E c \in Claims : Announce(c) \/ Unannounce(c) - \/ \E d \in Dirs : Deliver(d) \/ DeliverAck(d) + \/ \E d \in Dirs : Deliver(d) \/ DeliverEcho(d) \/ \E l \in Links : Connect(l) \/ Disconnect(l) \/ \E n \in Relays : Collect(n) \/ Done diff --git a/rs/moq-net/verify/route/RouteHandoff.view.ts b/rs/moq-net/verify/route/RouteHandoff.view.ts index e02b18361bc..e80d280f2f7 100644 --- a/rs/moq-net/verify/route/RouteHandoff.view.ts +++ b/rs/moq-net/verify/route/RouteHandoff.view.ts @@ -11,7 +11,6 @@ type Msg = { type: string; reach: { kind: string; seq: number; met: number } }; type Vars = { st: Record; q: Record>; - acks: Record; up: number[][]; own: Record; }; @@ -81,15 +80,13 @@ export const step = (action: string, from: Vars, to: Vars) => { } case "Collect": return "a relay with no route collects its state"; - case "DeliverAck": { - const [m, n] = ends(Object.keys(from.acks).find((k) => to.acks[k] < from.acks[k])); - return `${name(m)}'s echo of a route end reaches ${name(n)}`; - } - case "Deliver": { + case "Deliver": + case "DeliverEcho": { const d = Object.keys(from.q).find((k) => len(to.q[k]) === len(from.q[k]) - 1); const [m, n] = ends(d); const msg = from.q[d ?? ""]?.["1"]; if (!msg) return "a message arrives"; + if (msg.type === "echo") return `${name(m)}'s echo of a route end reaches ${name(n)}`; if (msg.type === "batch") return `${name(m)}'s claims reach ${name(n)}`; const what = msg.type === "request" From 7eb1bfecbfb174c932914377192648fc97112794 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 00:18:48 -0800 Subject: [PATCH 03/17] Revert "test(net): an echo arrives behind the echoer's routes in the route model and Sim" This reverts commit 81c0698295b51fc6c3d8b654f2ce96ee78e0c724. --- .claude/skills/verify-route/SKILL.md | 15 ++--- quest/m2/cluster-routing/routes/README.md | 6 +- rs/moq-net/src/route/tests/handoff.rs | 13 +++-- rs/moq-net/src/route/tests/mod.rs | 48 +++++++++++++--- rs/moq-net/src/route/tests/routing.rs | 59 ++++++++++---------- rs/moq-net/verify/route/CountToInfinity.cfg | 20 +++++++ rs/moq-net/verify/route/RouteHandoff.cfg | 2 +- rs/moq-net/verify/route/RouteHandoff.tla | 46 ++++++++------- rs/moq-net/verify/route/RouteHandoff.view.ts | 9 ++- 9 files changed, 139 insertions(+), 79 deletions(-) create mode 100644 rs/moq-net/verify/route/CountToInfinity.cfg diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index 90cb4383c0f..d2a2a815011 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.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, ROUTE_REQUEST, and echoes share one FIFO per direction, so an echo arrives behind every route its sender sent before it. 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. TLC checks every ordering of those messages in a triangle of the origin and two relays, under the bounds in the config. ## Rules @@ -28,19 +28,20 @@ The constraint `Bounded` stops exploring one hop past `NoCountToInfinity`, so a ```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 ``` -It checks every rule: about 1.2M distinct states, under a minute on 24 cores. +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. 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. -## Open finding: the echo's stream +## Open finding: an overtaking echo counts to infinity -`NoCountToInfinity` holds only because an echo arrives behind every route its sender sent before it: otherwise it can overtake an advertisement the echoer derived from this node's, and the node, its distance already drained, accepts it as a fresh, longer route (`an_echo_never_overtakes_the_echoers_routes` in `route/tests/routing.rs`). The model and `Sim` carry the echo that way, but `node.rs` still sends it back on the stream the ROUTE_END came on, apart from the echoer's routes, until [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) moves it. +`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`. ## Reading a failure -A counterexample is a path through the model, not yet a bug. Replay it on the router with `Sim` (`hold`, `deliver`, `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. +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 @@ -52,10 +53,10 @@ Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07 | `mod.rs` `certified`, `prune`, `adopted` | `Certified`, `Prune`, `Adopted` | | `mod.rs` `update`, `record`, `advertise`, `requests` | `Update`, `Record`, `Plan`, `Requests` | | `mod.rs` `show`, `shown_now` | `Events`, `ShownNow` | -| `mod.rs` `route`, `batch`, `request`, `echo` | `OnRoute`, `OnBatch`, `OnRequest`, `Deliver`, `DeliverEcho` | +| `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` | | `view.rs` `View::merge`, `View::restrict` | `Merge`, `Certify` | -| `tests/mod.rs` `Sim` queues and `revivals`, `false_ends` | `q`, `revivals`, `falseEnds` | +| `tests/mod.rs` `Sim` queues and `revivals`, `false_ends` | `q`, `acks`, `revivals`, `falseEnds` | ## Not covered diff --git a/quest/m2/cluster-routing/routes/README.md b/quest/m2/cluster-routing/routes/README.md index 5aca880554d..e77823753b9 100644 --- a/quest/m2/cluster-routing/routes/README.md +++ b/quest/m2/cluster-routing/routes/README.md @@ -179,10 +179,8 @@ the bullets below are the contract it carries. - Loop freedom is Babel's feasibility condition (RFC 8966) keyed by node: accept a route if its seqno is newer, or equal with a metric below the feasibility distance. Only the origin advances its seqno. Retraction is - ROUTE_HOLD or ROUTE_END. Draining a distance relies on each ROUTE_END - echo arriving behind every route the echoer sent before it: an echo that - overtakes a route derived from the echoed one counts to infinity (the - route model, 2026-11-10); + ROUTE_HOLD or ROUTE_END. The route model found a count to infinity + (2026-11-10): an echo can overtake a route derived from the echoed one; [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) orders it. - Starvation recovery is Babel's seqno request (RFC 8966 s3.8, decided 2026-10-12). A node whose routes to an origin are all infeasible sends diff --git a/rs/moq-net/src/route/tests/handoff.rs b/rs/moq-net/src/route/tests/handoff.rs index 64715bbc06b..f76629eeadc 100644 --- a/rs/moq-net/src/route/tests/handoff.rs +++ b/rs/moq-net/src/route/tests/handoff.rs @@ -1215,13 +1215,18 @@ fn churn(rng: &mut XorShift) -> Sim { sim.reconnect(first + origin); } _ => { + // Echoed ROUTE_ENDs interleave freely with the echoing node's routes. for _ in 0..rng.next(6) { - let busy = sim.busy(); + let busy: Vec<(bool, usize, usize)> = (sim.busy().into_iter().map(|(from, to)| (false, from, to))) + .chain(sim.busy_acks().into_iter().map(|(from, to)| (true, from, to))) + .collect(); if busy.is_empty() { break; } - let (from, to) = busy[rng.next(busy.len() as u64) as usize]; - sim.deliver(from, to); + match busy[rng.next(busy.len() as u64) as usize] { + (false, from, to) => sim.deliver(from, to), + (true, from, to) => sim.deliver_ack(from, to), + }; } } } @@ -1424,7 +1429,7 @@ fn a_restarted_floorless_route_drops_what_it_no_longer_carries() { assert!(sim.run()); sim.unannounce(origin, "live/a/x"); assert!(sim.run()); - while sim.deliver(z, x) {} + while sim.deliver_ack(z, x) {} sim.connect(x, local); assert!(sim.run()); sim.release(z, x); diff --git a/rs/moq-net/src/route/tests/mod.rs b/rs/moq-net/src/route/tests/mod.rs index dcdf0ecaeee..f3060404833 100644 --- a/rs/moq-net/src/route/tests/mod.rs +++ b/rs/moq-net/src/route/tests/mod.rs @@ -104,10 +104,6 @@ enum Msg { id: Id, seqno: Seqno, }, - /// The echo of a ROUTE_END, behind every route its sender sent before it. - Echo { - id: Id, - }, } #[derive(Clone, Debug, PartialEq, Eq)] @@ -153,6 +149,8 @@ pub(super) struct Sim { grants: BTreeSet<&'static str>, up: BTreeSet<(Node, Node)>, queues: BTreeMap<(Node, Node), VecDeque>, + /// Echoed ROUTE_ENDs: unordered against the echoing node's own routes. + acks: BTreeMap<(Node, Node), VecDeque>, held: BTreeSet<(Node, Node)>, history: BTreeMap>, /// Every request sent, to spot a repeat. @@ -173,6 +171,7 @@ impl Sim { grants: BTreeSet::new(), up: BTreeSet::new(), queues: BTreeMap::new(), + acks: BTreeMap::new(), held: BTreeSet::new(), history: BTreeMap::new(), requested: BTreeSet::new(), @@ -243,6 +242,7 @@ impl Sim { self.up.remove(&Self::pair(a, b)); for (x, y) in [(a, b), (b, a)] { self.queues.remove(&(x, y)); + self.acks.remove(&(x, y)); self.held.remove(&(x, y)); self.nodes[y].disconnect(x); } @@ -397,19 +397,42 @@ impl Sim { interest, } => router.batch(from, id, changes, floor, interest), Msg::Request { id, seqno } => router.request(from, id, seqno), - Msg::Echo { id } => router.echo(from, id), } self.stats.delivered += 1; self.flush(); true } + /// Deliver one echoed ROUTE_END from `from` to `to`, even if held. + pub fn deliver_ack(&mut self, from: Node, to: Node) -> bool { + let Some(id) = self.acks.get_mut(&(from, to)).and_then(VecDeque::pop_front) else { + return false; + }; + self.nodes[to].echo(from, id); + self.stats.delivered += 1; + self.flush(); + true + } + pub fn queued(&self, from: Node, to: Node) -> usize { self.queues.get(&(from, to)).map_or(0, VecDeque::len) } + pub fn queued_acks(&self, from: Node, to: Node) -> usize { + self.acks.get(&(from, to)).map_or(0, VecDeque::len) + } + pub fn busy(&self) -> Vec<(Node, Node)> { - (self.queues.iter()) + Self::nonempty(&self.queues) + } + + pub fn busy_acks(&self) -> Vec<(Node, Node)> { + Self::nonempty(&self.acks) + } + + fn nonempty(queues: &BTreeMap<(Node, Node), VecDeque>) -> Vec<(Node, Node)> { + queues + .iter() .filter(|(_, queue)| !queue.is_empty()) .map(|(key, _)| *key) .collect() @@ -424,12 +447,20 @@ impl Sim { pub fn settle(&mut self, rounds: usize) -> bool { for _ in 0..rounds { let ready: Vec<(Node, Node)> = self.busy().into_iter().filter(|key| !self.held.contains(key)).collect(); - if ready.is_empty() { + let acks: Vec<(Node, Node)> = self + .busy_acks() + .into_iter() + .filter(|key| !self.held.contains(key)) + .collect(); + if ready.is_empty() && acks.is_empty() { return true; } for (from, to) in ready { self.deliver(from, to); } + for (from, to) in acks { + self.deliver_ack(from, to); + } } false } @@ -466,7 +497,8 @@ impl Sim { } Out::Echo { to, id } => { self.stats.route_msgs += 1; - (to, Msg::Echo { id }) + self.acks.entry((node, to)).or_default().push_back(id); + continue; } }; self.queues.entry((node, to)).or_default().push_back(msg); diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index a8dffa5cd15..29f44971e61 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -152,7 +152,7 @@ fn collection_keeps_the_feasibility_distance_against_a_queued_echo() { sim.release(b, c); sim.release(c, b); assert!(sim.run()); - assert!(sim.queued(leaf, b) > 0, "the leaf's echo waits"); + assert!(sim.queued_acks(leaf, b) > 0, "the leaf's echo waits"); assert!(sim.remembers(b, 7), "the leaf may still hold b's advertisement"); sim.release(leaf, b); assert!(sim.run()); @@ -947,14 +947,17 @@ fn a_fresh_uncertified_claim_waits_on_an_older_floor() { } } -/// An echo travels behind every route its sender sent before it, so it never -/// overtakes an advertisement the echoing node derived from this one's. b -/// learned its route from a and advertised it back, then ended it on a's -/// ROUTE_END. a refuses that advertisement while its feasibility distance -/// stands, and drains the distance only on the echo behind it, so neither relay -/// selects a route longer than a loop-free path to the origin. +/// Pins a count to infinity that `verify/route/RouteHandoff.tla` found. An echo +/// travels apart from the echoing node's routes, so it can overtake an +/// advertisement that node derived from this one's. b learned its route from a +/// and advertised it back, then ended it on a's ROUTE_END. Its echo arrives +/// first, so a drains its feasibility distance and accepts b's stale +/// advertisement as a fresh, longer route to an origin neither reaches through +/// the other. With every echo overtaking, the two relays count up without end. +/// A fix keeps a's distance until that advertisement can no longer arrive: +/// then a refuses it and the route is gone. #[test] -fn an_echo_never_overtakes_the_echoers_routes() { +fn residual_an_overtaking_echo_counts_to_infinity() { let (origin, a, b) = (0, 1, 2); let mut sim = Sim::new(3); sim.join(origin, a, 1); @@ -970,27 +973,27 @@ fn an_echo_never_overtakes_the_echoers_routes() { sim.disconnect(origin, a); assert!(sim.run()); assert!(!sim.holds(b, 7), "b let go on a's ROUTE_END"); - assert!(sim.queued(b, a) > 1, "b's advertisement, then its echo"); - while sim.queued(b, a) > 1 { - sim.deliver(b, a); - assert!(sim.remembers(a, 7), "a keeps its distance until the echo"); - assert!(sim.route(a, 7).is_none(), "a refuses b's stale advertisement"); - } + assert!(sim.deliver_ack(b, a), "b's echo overtakes its own advertisement"); + assert!(!sim.remembers(a, 7), "a drained its distance"); assert!(sim.deliver(b, a)); - assert!(!sim.remembers(a, 7), "the echo drained a's distance"); - - // The longest loop-free path to the origin is through the other relay. - sim.release(origin, b); - sim.release(b, a); - loop { - for node in [a, b] { - assert!(sim.route(node, 7).is_none_or(|route| route.metric <= 2)); + assert_eq!( + sim.route(a, 7).map(|route| (route.next, route.metric)), + Some((Some(b), 3)) + ); + + // Each round, the relay that just drained accepts the other's stale route. + for round in 0..6 { + let (from, to) = if round % 2 == 0 { (b, a) } else { (a, b) }; + let mut peak = 0; + while sim.deliver(from, to) { + peak = peak.max(sim.route(to, 7).map_or(0, |route| route.metric)); } - let busy = sim.busy(); - let Some(&(from, to)) = busy.first() else { - break; - }; - sim.deliver(from, to); + // The origin echoes b's ends, and echoes overtake every route still waiting. + while sim.deliver(b, origin) {} + while [(a, b), (b, a), (origin, b)] + .into_iter() + .any(|(x, y)| sim.deliver_ack(x, y)) + {} + assert_eq!(peak, 3 + round, "round {round}"); } - assert_eq!(next(&sim, a, 7), Some(b)); } diff --git a/rs/moq-net/verify/route/CountToInfinity.cfg b/rs/moq-net/verify/route/CountToInfinity.cfg new file mode 100644 index 00000000000..5995cad17b8 --- /dev/null +++ b/rs/moq-net/verify/route/CountToInfinity.cfg @@ -0,0 +1,20 @@ +\* The open count-to-infinity finding, checked apart so RouteHandoff.cfg still +\* checks every other rule. Once it holds, move NoCountToInfinity into +\* RouteHandoff.cfg and delete this file. +CONSTANTS + Nodes = {0, 1, 2} + Origin = 0 + Leaves = {} + Links = {{0, 1}, {0, 2}, {1, 2}} + Claims = {"x"} + MaxRev = 2 + MaxFlaps = 2 + MaxCollects = 1 + +SPECIFICATION Spec + +INVARIANTS + NoCountToInfinity + +CONSTRAINT + Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.cfg b/rs/moq-net/verify/route/RouteHandoff.cfg index a4c2358fe36..d6020df9941 100644 --- a/rs/moq-net/verify/route/RouteHandoff.cfg +++ b/rs/moq-net/verify/route/RouteHandoff.cfg @@ -1,5 +1,6 @@ \* An origin (0) and two relays (1, 2) in a triangle, so a relay can fail \* over through the other and Babel's feasibility decides whether it may. +\* NoCountToInfinity lives in CountToInfinity.cfg while its finding is open. CONSTANTS Nodes = {0, 1, 2} Origin = 0 @@ -20,7 +21,6 @@ INVARIANTS NoRegression LoopFree QuietIsSettled - NoCountToInfinity CONSTRAINT Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.tla b/rs/moq-net/verify/route/RouteHandoff.tla index e4cd03ed873..ccca07819cc 100644 --- a/rs/moq-net/verify/route/RouteHandoff.tla +++ b/rs/moq-net/verify/route/RouteHandoff.tla @@ -7,9 +7,9 @@ (* `request`, `echo`, `collect`, `connect`/`peer_interest`, `disconnect`, *) (* `announce`/`unannounce`) is one atomic step that ends in `update`, as *) (* in the code. Messages travel as the Sim queues them: ROUTE, batches, *) -(* ROUTE_REQUEST, and echoed ROUTE_ENDs on one FIFO per direction, so an *) -(* echo arrives behind every route its sender sent before it. A session *) -(* opens and closes atomically, dropping what was in flight. *) +(* and ROUTE_REQUEST on one FIFO per direction, echoed ROUTE_ENDs on their *) +(* own queue. A session opens and closes atomically, dropping what was in *) +(* flight. *) (* *) (* Scope: every node watches the root, links cost 1 with equal priority, *) (* no scoped grants, no GOAWAY, and the origin keeps its identity. Claims *) @@ -55,11 +55,11 @@ NotShown == [item |-> None, avail |-> FALSE] RouteMsg(reach) == [type |-> "route", reach |-> reach, view |-> NoView, seq |-> 0] BatchMsg(view) == [type |-> "batch", reach |-> NoReach, view |-> view, seq |-> 0] RequestMsg(seq) == [type |-> "request", reach |-> NoReach, view |-> NoView, seq |-> seq] -EchoMsg == [type |-> "echo", reach |-> NoReach, view |-> NoView, seq |-> 0] VARIABLES up, \* open sessions (`Sim::up`) q, \* q[<>]: ROUTE, batches, and ROUTE_REQUEST from m to n, in order + acks, \* acks[<>]: echoed ROUTE_ENDs from m to n rev, \* the origin's claim revision (`Origin::view.floors[""]`) own, \* the origin's claims (`Origin::view.items`) seqno, \* the origin's route seqno (`Origin::seqno`) @@ -72,7 +72,7 @@ VARIABLES flaps, collects -vars == <> \* The origin's view and seqno. @@ -249,8 +249,7 @@ Update(n, s0, ov, ups, eb) == IN [s |-> [s5 EXCEPT !.shown = now], out |-> out, ev |-> ev] \* The origin ignores every ROUTE and batch it hears for its own identity, so -\* only ROUTE_REQUEST, ROUTE_END (which it echoes), and echoes are queued -\* toward it. +\* only ROUTE_REQUEST and ROUTE_END (which it echoes) are queued toward it. \* Dropping the rest changes no behavior and keeps the state space small. Heeded(d, m) == d[2] # Origin \/ m.type = "request" \/ (m.type = "route" /\ m.reach.kind = "none") @@ -289,6 +288,7 @@ InitNode == [ Init == /\ up = Links /\ q = [d \in Dirs |-> <<>>] + /\ acks = [d \in Dirs |-> 0] /\ rev = 0 /\ own = NoItems /\ seqno = 0 @@ -311,7 +311,7 @@ ChangeClaim(c, item) == /\ own' = own1 /\ hist' = Append(hist, own1) /\ Commit([n \in {Origin} |-> Update(Origin, st[Origin], ov1, up, ended[Origin])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> \* A new claim, or new attributes for one, under a fresh revision. Announce(c) == rev < MaxRev /\ ChangeClaim(c, rev + 1) @@ -364,10 +364,8 @@ Deliver(d) == LET m == d[1] n == d[2] msg == Head(q[d]) + q0 == [q EXCEPT ![d] = Tail(@)] isEnd == msg.type = "route" /\ msg.reach.kind = "none" - \* Every ROUTE_END is echoed once applied, ahead of what the update sends. - q0 == [q EXCEPT ![d] = Tail(@), - ![<>] = IF isEnd THEN Append(@, EchoMsg) ELSE @] \* Only the origin advances its seqno to answer a request. ov1 == IF n = Origin /\ msg.type = "request" THEN [OV EXCEPT !.seq = Max(seqno, msg.seq)] ELSE OV @@ -380,7 +378,8 @@ Deliver(d) == [] msg.type = "batch" -> OnBatch(st[n], m, msg.view) [] OTHER -> OnRequest(st[n], m, msg.seq) IN /\ q[d] # <<>> - /\ msg.type # "echo" + \* Every ROUTE_END is echoed once applied. + /\ acks' = IF isEnd THEN [acks EXCEPT ![<>] = @ + 1] ELSE acks /\ seqno' = ov1.seq /\ IF skip THEN /\ q' = q0 @@ -388,18 +387,16 @@ Deliver(d) == ELSE Commit([x \in {n} |-> Update(n, s1, ov1, up, ended[n])], q0) /\ UNCHANGED <> -\* `echo`: an echoed ROUTE_END comes back, behind the echoer's earlier routes. -DeliverEcho(d) == +\* `echo`: an echoed ROUTE_END comes back (`Sim::deliver_ack`). +DeliverAck(d) == LET m == d[1] n == d[2] - q0 == [q EXCEPT ![d] = Tail(@)] - IN /\ q[d] # <<>> - /\ Head(q[d]).type = "echo" + IN /\ acks[d] > 0 + /\ acks' = [acks EXCEPT ![d] = @ - 1] /\ IF st[n].unacked[m] = 0 - THEN /\ q' = q0 - /\ UNCHANGED <> + THEN UNCHANGED <> ELSE Commit([x \in {n} |-> - Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n])], q0) + Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n])], q) /\ UNCHANGED <> ----------------------------------------------------------------------------- @@ -427,7 +424,7 @@ Connect(l) == /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x IN Update(x, Opened(st[x], y), OV, up1, ended[x])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> Disconnect(l) == LET up1 == up \ {l} @@ -436,6 +433,7 @@ Disconnect(l) == /\ flaps < MaxFlaps /\ up' = up1 /\ flaps' = flaps + 1 + /\ acks' = [d \in Dirs |-> IF {d[1], d[2]} = l THEN 0 ELSE acks[d]] /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x IN Update(x, Closed(st[x], y), OV, up1, ended[x])], q0) @@ -452,9 +450,9 @@ Collect(n) == !.heard = [m \in Nodes |-> NoHeard], !.pending = NoPending], OV, up, [c \in Claims |-> None])], q) - /\ UNCHANGED <> + /\ UNCHANGED <> -Quiet == \A d \in Dirs : q[d] = <<>> +Quiet == \A d \in Dirs : q[d] = <<>> /\ acks[d] = 0 \* Nothing is in flight and no more churn is allowed: the run is over. Done == @@ -464,7 +462,7 @@ Done == Next == \/ \E c \in Claims : Announce(c) \/ Unannounce(c) - \/ \E d \in Dirs : Deliver(d) \/ DeliverEcho(d) + \/ \E d \in Dirs : Deliver(d) \/ DeliverAck(d) \/ \E l \in Links : Connect(l) \/ Disconnect(l) \/ \E n \in Relays : Collect(n) \/ Done diff --git a/rs/moq-net/verify/route/RouteHandoff.view.ts b/rs/moq-net/verify/route/RouteHandoff.view.ts index e80d280f2f7..e02b18361bc 100644 --- a/rs/moq-net/verify/route/RouteHandoff.view.ts +++ b/rs/moq-net/verify/route/RouteHandoff.view.ts @@ -11,6 +11,7 @@ type Msg = { type: string; reach: { kind: string; seq: number; met: number } }; type Vars = { st: Record; q: Record>; + acks: Record; up: number[][]; own: Record; }; @@ -80,13 +81,15 @@ export const step = (action: string, from: Vars, to: Vars) => { } case "Collect": return "a relay with no route collects its state"; - case "Deliver": - case "DeliverEcho": { + case "DeliverAck": { + const [m, n] = ends(Object.keys(from.acks).find((k) => to.acks[k] < from.acks[k])); + return `${name(m)}'s echo of a route end reaches ${name(n)}`; + } + case "Deliver": { const d = Object.keys(from.q).find((k) => len(to.q[k]) === len(from.q[k]) - 1); const [m, n] = ends(d); const msg = from.q[d ?? ""]?.["1"]; if (!msg) return "a message arrives"; - if (msg.type === "echo") return `${name(m)}'s echo of a route end reaches ${name(n)}`; if (msg.type === "batch") return `${name(m)}'s claims reach ${name(n)}`; const what = msg.type === "request" From e1c9e2c90391fabc5f438c5c6a3790f97ca59b6b Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 01:49:16 -0800 Subject: [PATCH 04/17] fix(net)!: a lite-07 route names the relays it crossed, and is never feasible where it has been A node dropped its feasibility distance once every neighbour echoed its ROUTE_END, then took back a copy of its own route that a third relay still held, and the relays counted to infinity. ROUTE_START and ROUTE_UPDATE now carry the hops a route crossed. A route whose hops name the receiver is never feasible there, and one that crossed as many relays as a route may is unreachable. Co-Authored-By: Claude --- rs/moq-net/src/fuzz.rs | 1 + rs/moq-net/src/lite/announce.rs | 26 ++- rs/moq-net/src/lite/subscriber.rs | 1 + rs/moq-net/src/lite/subscriber/routed.rs | 31 +-- rs/moq-net/src/route/mod.rs | 117 ++++++---- rs/moq-net/src/route/node.rs | 4 +- rs/moq-net/src/route/tests/mod.rs | 19 +- rs/moq-net/src/route/tests/routing.rs | 271 ++++++++++++++++++++--- 8 files changed, 379 insertions(+), 91 deletions(-) diff --git a/rs/moq-net/src/fuzz.rs b/rs/moq-net/src/fuzz.rs index 4cbcf800809..2ae7e49fa73 100644 --- a/rs/moq-net/src/fuzz.rs +++ b/rs/moq-net/src/fuzz.rs @@ -677,6 +677,7 @@ impl RouteRelay { seqno: 0, metric: 0, down_only: false, + hops: [].into(), }; let receive = (0..streams) .map(|_| { diff --git a/rs/moq-net/src/lite/announce.rs b/rs/moq-net/src/lite/announce.rs index d23df0e92e9..a8fb5ce0a97 100644 --- a/rs/moq-net/src/lite/announce.rs +++ b/rs/moq-net/src/lite/announce.rs @@ -114,15 +114,23 @@ pub enum AnnounceBroadcast { Floor { id: u64, revision: Option }, } -/// Encode a seqno, metric, and down-only bit. No origin advertises the last seqno, -/// which would leave no room for the successor a ROUTE_REQUEST names. +/// Encode a seqno, metric, down-only bit, and the hops the route crossed. No origin +/// advertises the last seqno, which would leave no room for the successor a +/// ROUTE_REQUEST names. fn encode_advert(w: &mut Encoder<'_>, advert: &Advert) -> Result<(), EncodeError> { if advert.seqno == route::MAX { return Err(EncodeError::InvalidState); } + if advert.hops.len() > route::MAX_HOPS { + return Err(EncodeError::TooMany); + } w.varint(advert.seqno)?; w.varint(advert.metric)?; w.bool(advert.down_only); + w.varint(advert.hops.len() as u64)?; + for hop in advert.hops.iter() { + w.varint(*hop)?; + } Ok(()) } @@ -131,10 +139,18 @@ fn decode_advert(r: &mut Decoder<'_>) -> Result { if seqno == route::MAX { return Err(DecodeError::InvalidValue); } + let metric = r.varint()?; + let down_only = r.bool()?; + let count = r.varint()?; + if count > route::MAX_HOPS as u64 { + return Err(DecodeError::TooMany); + } + let hops = (0..count).map(|_| r.varint()).collect::>()?; Ok(Advert { seqno, - metric: r.varint()?, - down_only: r.bool()?, + metric, + down_only, + hops, }) } @@ -1541,6 +1557,7 @@ mod tests { seqno, metric, down_only, + hops: [].into(), } } @@ -1691,6 +1708,7 @@ mod tests { w.varint(seqno).unwrap(); w.varint(metric).unwrap(); w.u8(down_only); + w.varint(0u64).unwrap(); } }; let malformed = [ diff --git a/rs/moq-net/src/lite/subscriber.rs b/rs/moq-net/src/lite/subscriber.rs index ab10fbfd8a2..d7f59210608 100644 --- a/rs/moq-net/src/lite/subscriber.rs +++ b/rs/moq-net/src/lite/subscriber.rs @@ -9024,6 +9024,7 @@ mod tests { seqno: 0, metric: 0, down_only: false, + hops: [].into(), }; lite::AnnounceBroadcast::RouteStart { node, advert } .encode(w, Version::Lite07) diff --git a/rs/moq-net/src/lite/subscriber/routed.rs b/rs/moq-net/src/lite/subscriber/routed.rs index 41a55264a6a..b450439c8c4 100644 --- a/rs/moq-net/src/lite/subscriber/routed.rs +++ b/rs/moq-net/src/lite/subscriber/routed.rs @@ -585,11 +585,14 @@ mod tests { use crate::lite::{AnnounceBroadcast as Msg, AnnounceDecoder, PathRef, test_transport::SinkSession}; use crate::{Instance, Path, auth::Permit, origin::Cost, route::Advert}; - const ADVERT: Advert = Advert { - seqno: 0, - metric: 0, - down_only: false, - }; + fn advert() -> Advert { + Advert { + seqno: 0, + metric: 0, + down_only: false, + hops: [].into(), + } + } fn start(path: &'static str) -> Msg { Msg::Active { @@ -631,7 +634,7 @@ mod tests { }; let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; for msg in [route, start("live/a/public/x"), start("live/a/private/y"), floor] { routed.receive(&prefix, msg, &mut decoder).unwrap(); @@ -670,7 +673,7 @@ mod tests { }; let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; for msg in [ route, @@ -713,7 +716,7 @@ mod tests { }; let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; for msg in [route, start("live/a/public/x"), start("live/a/private/y"), floor] { routed.receive(&prefix, msg, &mut decoder).unwrap(); @@ -749,7 +752,7 @@ mod tests { }; let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; for msg in [route, start("live/a/public/x"), start("live/a/private/y"), floor] { routed.receive(&prefix, msg, &mut decoder).unwrap(); @@ -779,14 +782,14 @@ mod tests { let waiter = kio::Waiter::noop(); for (id, node) in [(0, 7), (1, 8)] { - let route = Msg::RouteStart { node, advert: ADVERT }; + let route = Msg::RouteStart { node, advert: advert() }; routed.receive(&prefix, route, &mut decoder).unwrap(); routed.receive(&prefix, Msg::RouteEnd { id }, &mut decoder).unwrap(); routed.poll(&subscriber, &mut writer, &waiter).unwrap(); } let route = Msg::RouteStart { node: 9, - advert: ADVERT, + advert: advert(), }; assert!( routed.receive(&prefix, route, &mut decoder).is_err(), @@ -807,7 +810,7 @@ mod tests { let prefix = Path::empty(); let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; routed.receive(&prefix, route, decoder)?; for path in paths { @@ -905,7 +908,7 @@ mod tests { let waiter = kio::Waiter::noop(); let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; routed.receive(&prefix, route, &mut decoder).unwrap(); let downstream = (subscriber.origin.route_node()) @@ -954,7 +957,7 @@ mod tests { }; let route = Msg::RouteStart { node: 7, - advert: ADVERT, + advert: advert(), }; for msg in [route, start("room/host"), floor] { routed.receive(&prefix, msg, &mut decoder).unwrap(); diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index 6a74dacea35..91fa5ee7ec2 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -150,16 +150,22 @@ pub(crate) fn qualifier(key: [u8; 32]) -> Arc Id + Send + Sync> { }) } +/// The most relays a route crosses: the longest hop list a message carries. +pub(crate) const MAX_HOPS: usize = 32; + /// What a node advertises for one identity. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub(crate) struct Advert { pub seqno: Seqno, pub metric: Metric, pub down_only: bool, + /// The relays the route crossed, by the hop id each names itself with, in order + /// from the origin node. The sender is last, and the origin node is left out. + pub hops: Arc<[Id]>, } /// A ROUTE's state on a stream. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub(crate) enum Reach { /// A usable route. Finite(Advert), @@ -239,11 +245,14 @@ pub(crate) struct Event { } /// A route a node holds from one neighbor. -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Debug)] struct Entry { /// The last finite advertisement. advert: Advert, held: bool, + /// Its hops name this node: a copy of a route this node sent, come back. It is + /// never feasible, which the distance alone cannot say once this node forgot it. + crossed: bool, } /// A seqno request a node keeps until a route at least that new is selected or @@ -387,6 +396,11 @@ pub(crate) struct Retained { } pub(crate) struct Router { + /// How this node names itself in the hops of a route it forwards. A rotation + /// leaves it alone, so a route that crossed this node always says so. + hop: Id, + /// The most relays a route this node uses may cross, itself included. + pub max_hops: usize, neighbors: BTreeMap, origins: BTreeMap>, rx: BTreeMap>, @@ -446,9 +460,12 @@ pub(crate) enum Error { } impl Router { - /// A node with no sessions, minting rotated identities from `seed`. - pub fn new(seed: u64) -> Self { + /// A node with no sessions, naming itself `hop` in the routes it forwards and + /// minting rotated identities from `seed`. + pub fn new(hop: Id, seed: u64) -> Self { Self { + hop, + max_hops: MAX_HOPS, neighbors: BTreeMap::new(), origins: BTreeMap::new(), rx: BTreeMap::new(), @@ -755,7 +772,8 @@ impl Router { return; } // Echo every ROUTE_END once applied, filed or refused. - if reach.is_none() { + let ended = reach.is_none(); + if ended { self.out.push(Out::Echo { to: from, id: named }); } let Some(id) = self.key(from, named) else { @@ -770,7 +788,13 @@ impl Router { let routes = self.rx.entry(id).or_default(); match reach { Some(Reach::Finite(advert)) => { - routes.insert(from, Entry { advert, held: false }); + let crossed = advert.hops.contains(&self.hop); + let entry = Entry { + advert, + held: false, + crossed, + }; + routes.insert(from, entry); } Some(Reach::Held) => { if let Some(entry) = routes.get_mut(&from) { @@ -789,7 +813,7 @@ impl Router { // last view only for what it certified. An uncertified claim lives only // while the stream carries it, and the restart's batch names only what it // still carries, so one kept here would never be withdrawn. - if reach.is_none() + if ended && let Some(heard) = self.heard.get_mut(&(id, from)) { let raw = std::mem::take(&mut heard.raw); @@ -1010,11 +1034,11 @@ impl Router { type Rank = (bool, Reverse, Metric, N); let mut best: Option<(Rank, Selected)> = None; for (&next, entry) in self.rx.get(&id)? { - if entry.held || !self.feasible(id, entry.advert) { + if entry.held || !self.feasible(id, entry) { continue; } let peer = &self.neighbors[&next]; - let Some(metric) = add(entry.advert.metric, peer.link.cost) else { + let Some(metric) = self.through(next, entry) else { continue; }; let rank = (peer.draining, Reverse(peer.link.priority), metric, next); @@ -1039,8 +1063,8 @@ impl Router { return Vec::new(); } (self.rx.get(&id).into_iter().flatten()) - .filter(|(_, entry)| !entry.held && self.feasible(id, entry.advert)) - .filter_map(|(&next, entry)| Some((next, add(entry.advert.metric, self.neighbors[&next].link.cost)?))) + .filter(|(_, entry)| !entry.held && self.feasible(id, entry)) + .filter_map(|(&next, entry)| Some((next, self.through(next, entry)?))) .collect() } @@ -1174,22 +1198,35 @@ impl Router { self.filed.get(&(id, next)).copied().unwrap_or(id) } - /// Babel's feasibility condition against this node's feasibility distance. - fn feasible(&self, id: Id, advert: Advert) -> bool { - match self.fd.get(&id) { - None => true, - Some(&(seqno, metric)) => advert.seqno > seqno || (advert.seqno == seqno && advert.metric < metric), + /// Babel's feasibility condition against this node's feasibility distance, and + /// never a route that crossed this node. + fn feasible(&self, id: Id, entry: &Entry) -> bool { + let advert = &entry.advert; + !entry.crossed + && match self.fd.get(&id) { + None => true, + Some(&(seqno, metric)) => advert.seqno > seqno || (advert.seqno == seqno && advert.metric < metric), + } + } + + /// This node's metric through `entry`, the route `next` sent, or `None` when it is + /// unreachable, never saturated: the metric overflows, or the route already + /// crossed as many relays as one may. + fn through(&self, next: N, entry: &Entry) -> Option { + if entry.advert.hops.len() >= self.max_hops { + return None; } + entry.advert.metric.checked_add(self.neighbors[&next].link.cost) } - /// The usable but infeasible routes for `id`, with their metrics. + /// The usable but infeasible routes for `id`, with their metrics: the ones a newer + /// seqno would lift past this node's distance. With no distance kept there are + /// none, since the only routes refused then are its own, come back. fn infeasible(&self, id: Id) -> impl Iterator + '_ { - self.rx - .get(&id) - .into_iter() - .flatten() - .filter(move |(_, entry)| !entry.held && !self.feasible(id, entry.advert)) - .filter_map(move |(&next, entry)| Some((add(entry.advert.metric, self.neighbors[&next].link.cost)?, next))) + let kept = self.fd.contains_key(&id); + (self.rx.get(&id).into_iter().flatten()) + .filter(move |(_, entry)| kept && !entry.held && !self.feasible(id, entry)) + .filter_map(move |(&next, entry)| Some((self.through(next, entry)?, next))) } /// Where this node sends a request for `id`: its feasible route's next hop, @@ -1235,7 +1272,7 @@ impl Router { /// Whether `entry`'s last finite advertisement from `next` is feasible here /// and reachable across the link, as selection requires of a usable route. fn reachable(&self, id: Id, next: N, entry: &Entry) -> bool { - self.feasible(id, entry.advert) && add(entry.advert.metric, self.neighbors[&next].link.cost).is_some() + self.feasible(id, entry) && self.through(next, entry).is_some() } /// The regions of `id` that this node's certifiers certify, those whose @@ -1603,6 +1640,13 @@ impl Router { /// changed among the dirty claims, unless any could have. fn advertise(&mut self, id: Id, peers: &[N], ctx: &Ctx, dirty: &Dirty) { let selected = self.selected(id); + // The selected route's hops, then this node; its own route crossed no relay. + let hops: Arc<[Id]> = match selected.and_then(|route| route.next) { + Some(next) => (self.rx[&id][&next].advert.hops.iter().copied()) + .chain([self.hop]) + .collect(), + None => Arc::default(), + }; let floors = self.adopted_floors(id).cloned().unwrap_or_default(); // Built only for a stream sent a whole snapshot, once per interest. let mut adopted: Option> = None; @@ -1612,7 +1656,7 @@ impl Router { for &to in peers { let peer = &self.neighbors[&to]; let serves = self.serves(peer, id); - let was = self.sent.get(&(id, to)).copied(); + let was = self.sent.get(&(id, to)).cloned(); if !serves && was.is_none() { continue; } @@ -1621,6 +1665,7 @@ impl Router { seqno: route.seqno, metric: route.metric, down_only: route.down_only, + hops: hops.clone(), })), None if serves && ctx.live && was.is_some() => Some(Reach::Held), _ => None, @@ -1630,7 +1675,7 @@ impl Router { let reach = reach.filter(|_| was.is_some() || !self.unacked.contains_key(&(id, to))); let watch = peer.watch.as_ref().expect("a watching peer"); let sent = self.sent_views.get(&(id, to)); - let (changes, meets) = match (reach, sent) { + let (changes, meets) = match (&reach, sent) { (None, _) => (Vec::new(), false), // A stream holding nothing that the route still does not meet. (Some(_), None) if !self.meets(id, ctx, watch) => (Vec::new(), false), @@ -1687,11 +1732,13 @@ impl Router { for (to, was, reach, meets, changes, floors, watch) in plans { let key = (id, to); + let (reaching, started) = (reach.is_some(), was.is_some()); let send = reach.filter(|_| meets); + let sending = send.is_some(); if let Some(send) = send - && was != Some(send) + && was.as_ref() != Some(&send) { - self.sent.insert(key, send); + self.sent.insert(key, send.clone()); self.out.push(Out::Route { to, id, @@ -1699,7 +1746,7 @@ impl Router { }); } // A batch goes while the route does, the last one just before its ROUTE_END. - if send.is_some() || reach.is_some() && was.is_some() && self.sent_views.contains_key(&key) { + if sending || reaching && started && self.sent_views.contains_key(&key) { let sent = self.sent_views.entry(key).or_default(); let floor = sent.floor(&watch); sent.apply(changes.clone(), floors); @@ -1714,8 +1761,8 @@ impl Router { } } // Announcements ride on the route and end with it. - if send.is_none() { - if was.is_some() { + if !sending { + if started { *self.unacked.entry(key).or_default() += 1; self.sent.remove(&key); self.out.push(Out::Route { to, id, reach: None }); @@ -1944,9 +1991,3 @@ impl Router { }); } } - -/// `metric` plus a strictly positive link `cost`, or `None` when it overflows: an -/// overflowed route is unreachable, never saturated. -fn add(metric: Metric, cost: Metric) -> Option { - metric.checked_add(cost) -} diff --git a/rs/moq-net/src/route/node.rs b/rs/moq-net/src/route/node.rs index c17fc75ddbc..0a99d15c2d6 100644 --- a/rs/moq-net/src/route/node.rs +++ b/rs/moq-net/src/route/node.rs @@ -405,7 +405,7 @@ impl Node { id != 0 && id & QUALIFIED == 0, "a declared identity is non-zero and unqualified" ); - let mut router = Router::new(seed); + let mut router = Router::new(id, seed); router.originate(id, 0); Self { state: Arc::new(Mutex::new(State { @@ -1203,6 +1203,7 @@ mod tests { seqno, metric: 0, down_only: false, + hops: [].into(), })) }; for origin in 10..110 { @@ -1326,6 +1327,7 @@ mod tests { seqno: 0, metric: 0, down_only: false, + hops: [].into(), }; receive.route(1, Some(Reach::Finite(advert))); receive.batch(1, vec![(p("live/x"), Some(claim(&instance, 0)))], Some(1)); diff --git a/rs/moq-net/src/route/tests/mod.rs b/rs/moq-net/src/route/tests/mod.rs index f3060404833..561c6e4dd50 100644 --- a/rs/moq-net/src/route/tests/mod.rs +++ b/rs/moq-net/src/route/tests/mod.rs @@ -53,6 +53,11 @@ fn fnv(label: &str, ids: &[u64]) -> u64 { hash } +/// How `node` names itself in a route's hops, fresh for each restart like its process. +pub(super) fn hop(node: Node, restarts: u32) -> Id { + 1_000 * (u64::from(restarts) + 1) + node as u64 +} + /// One side's configuration of a link. #[derive(Clone, Copy, Debug)] pub(super) struct SimLink { @@ -162,7 +167,7 @@ pub(super) struct Sim { impl Sim { pub fn new(nodes: usize) -> Self { Self { - nodes: (0..nodes).map(|node| Router::new(node as u64 + 1)).collect(), + nodes: (0..nodes).map(|node| Router::new(hop(node, 0), node as u64 + 1)).collect(), leaf: vec![false; nodes], watch: vec![Path::empty(); nodes], restarts: vec![0; nodes], @@ -257,7 +262,9 @@ impl Sim { } self.restarts[node] += 1; self.declared[node] = None; - self.nodes[node] = Router::new(fnv("restart", &[node as u64, u64::from(self.restarts[node])])); + let restarts = self.restarts[node]; + let seed = fnv("restart", &[node as u64, u64::from(restarts)]); + self.nodes[node] = Router::new(hop(node, restarts), seed); let watch = self.watch[node].clone(); self.nodes[node].watch(watch); self.flush(); @@ -471,6 +478,14 @@ impl Sim { for out in self.nodes[node].drain() { let (to, msg) = match out { Out::Route { to, id, reach } => { + // A route names every relay it crossed once, the sender last. + if let Some(Reach::Finite(advert)) = &reach { + let own = self.nodes[node].origins.contains_key(&id); + let me = hop(node, self.restarts[node]); + assert_eq!(advert.hops.last().copied(), (!own).then_some(me), "node {node}'s hops for {id}"); + let named: BTreeSet = advert.hops.iter().copied().collect(); + assert_eq!(named.len(), advert.hops.len(), "node {node} sent {id} round a loop"); + } self.stats.route_msgs += 1; (to, Msg::Route { id, reach }) } diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index 29f44971e61..41b21da5d46 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -293,7 +293,7 @@ fn sweep_forgetting_distances() { /// zero-cost link is refused when it is configured. #[test] fn zero_cost_links_are_refused() { - let mut router: Router = Router::new(1); + let mut router: Router = Router::new(99, 1); let link = Link { cost: 0, ..Link::default() @@ -775,7 +775,7 @@ fn an_unanswerable_request_stops() { #[test] fn a_newer_request_raises_the_pending_one() { let (up, a, b) = (0, 1, 2); - let mut relay = Router::::new(9); + let mut relay = Router::::new(99, 9); for neighbor in [up, a, b] { relay.connect(neighbor, Link::default()).unwrap(); } @@ -783,6 +783,7 @@ fn a_newer_request_raises_the_pending_one() { seqno: 0, metric: 1, down_only: false, + hops: [].into(), }; relay.route(up, 7, Some(Reach::Finite(advert))); relay.drain(); @@ -870,6 +871,7 @@ fn an_overflowing_route_neither_certifies_nor_holds() { seqno: 0, metric, down_only: false, + hops: [].into(), })) }; let item = Item { @@ -883,7 +885,7 @@ fn an_overflowing_route_neither_certifies_nor_holds() { ..Link::default() }; - let mut router: Router = Router::new(1); + let mut router: Router = Router::new(99, 1); router.connect(near, Link::default()).unwrap(); router.connect(far, far_link.clone()).unwrap(); router.asks(near, p("live/a")).unwrap(); @@ -899,7 +901,7 @@ fn an_overflowing_route_neither_certifies_nor_holds() { "only the unreachable route certifies it" ); - let mut router: Router = Router::new(1); + let mut router: Router = Router::new(99, 1); router.connect(far, far_link).unwrap(); router.route(far, 7, finite(1)); router.batch(far, 7, vec![(p("live/x"), Some(item))], Some(1), 0); @@ -921,6 +923,7 @@ fn a_fresh_uncertified_claim_waits_on_an_older_floor() { seqno: 0, metric, down_only: false, + hops: [].into(), })) }; let item = Item { @@ -930,7 +933,7 @@ fn a_fresh_uncertified_claim_waits_on_an_older_floor() { }; let (certifier, carrier) = (1, 2); for refresh in [true, false] { - let mut router: Router = Router::new(1); + let mut router: Router = Router::new(99, 1); router.connect(certifier, Link::default()).unwrap(); router.connect(carrier, Link::default()).unwrap(); router.route(certifier, 7, finite(1)); @@ -947,23 +950,20 @@ fn a_fresh_uncertified_claim_waits_on_an_older_floor() { } } -/// Pins a count to infinity that `verify/route/RouteHandoff.tla` found. An echo -/// travels apart from the echoing node's routes, so it can overtake an -/// advertisement that node derived from this one's. b learned its route from a -/// and advertised it back, then ended it on a's ROUTE_END. Its echo arrives -/// first, so a drains its feasibility distance and accepts b's stale -/// advertisement as a fresh, longer route to an origin neither reaches through -/// the other. With every echo overtaking, the two relays count up without end. -/// A fix keeps a's distance until that advertisement can no longer arrive: -/// then a refuses it and the route is gone. +/// An echo travels apart from the echoing node's routes, so it can overtake a +/// route that node derived from this one's. b learned its route from a and sent it +/// back, then ended it on a's ROUTE_END. Its echo arrives first, so a drops its +/// feasibility distance, and b's old route arrives looking like a fresh, longer one +/// to an origin neither reaches. Its hops name a, so a refuses it, where two relays +/// once counted up without end. #[test] -fn residual_an_overtaking_echo_counts_to_infinity() { +fn a_route_that_crossed_a_node_is_refused_once_its_distance_is_gone() { let (origin, a, b) = (0, 1, 2); let mut sim = Sim::new(3); sim.join(origin, a, 1); sim.join(origin, b, 1); sim.join(a, b, 1); - // b hears the origin only through a, and b's advertisement to a waits. + // b hears the origin only through a, and b's route to a waits. sim.hold(origin, b); sim.hold(b, a); originate(&mut sim, origin, 7, 0); @@ -973,27 +973,234 @@ fn residual_an_overtaking_echo_counts_to_infinity() { sim.disconnect(origin, a); assert!(sim.run()); assert!(!sim.holds(b, 7), "b let go on a's ROUTE_END"); - assert!(sim.deliver_ack(b, a), "b's echo overtakes its own advertisement"); - assert!(!sim.remembers(a, 7), "a drained its distance"); + assert!(sim.deliver_ack(b, a), "b's echo overtakes its own route"); + assert!(!sim.remembers(a, 7), "a dropped its distance"); assert!(sim.deliver(b, a)); + assert!(sim.holds(a, 7), "b's route stays open until b ends it"); + assert!(sim.route(a, 7).is_none(), "a refuses its own route, come back"); + assert!(!sim.starved(a, 7), "with no distance, no seqno would help"); + assert_eq!(sim.shows(a, 7, ""), None); + + // b still reaches the origin, and a takes the route b learns there. + sim.release(b, a); + sim.release(origin, b); + assert!(sim.run()); assert_eq!( sim.route(a, 7).map(|route| (route.next, route.metric)), - Some((Some(b), 3)) + Some((Some(b), 2)) ); +} + +/// The origin sits behind relay a, in a triangle with b and c. An echo proves only +/// that nothing derived is in flight on its own link: here c's copy of a's route +/// waits on its way to b while both echo a's ROUTE_END, so a drops its distance, and +/// then b takes c's copy and offers it to a. It crossed a, so a refuses it and the +/// copies die out, where the three relays once handed it round at a growing metric. +#[test] +fn a_route_handed_round_a_triangle_is_refused_where_it_began() { + let (origin, a, b, c) = (0, 1, 2, 3); + let mut sim = Sim::new(4); + sim.join(origin, a, 1); + sim.join(a, b, 2); + sim.join(a, c, 1); + sim.join(b, c, 2); + for (from, to) in [(c, b), (b, c), (b, a), (c, a)] { + sim.hold(from, to); + } + originate(&mut sim, origin, 7, 0); + assert!(sim.run()); + assert_eq!(sim.route(b, 7).map(|route| route.metric), Some(3)); - // Each round, the relay that just drained accepts the other's stale route. - for round in 0..6 { - let (from, to) = if round % 2 == 0 { (b, a) } else { (a, b) }; - let mut peak = 0; - while sim.deliver(from, to) { - peak = peak.max(sim.route(to, 7).map_or(0, |route| route.metric)); + sim.disconnect(origin, a); + assert!(sim.run()); + assert!(!sim.holds(b, 7) && !sim.holds(c, 7), "both let go on a's ROUTE_END"); + assert!(sim.deliver_ack(b, a) && sim.deliver_ack(c, a)); + assert!(!sim.remembers(a, 7), "every neighbor echoed, so a dropped its distance"); + + // c's copy, sent before the end, is shorter than what b advertised: feasible there. + assert!(sim.deliver(c, b)); + assert_eq!(sim.route(b, 7).map(|route| (route.next, route.metric)), Some((Some(c), 4))); + + // b may offer it to a once a echoes the ROUTE_END b sent it. + let mut peak = 0; + for _ in 0..100 { + for (from, to) in [(b, a), (c, a), (a, b), (a, c)] { + sim.deliver(from, to); + sim.deliver_ack(from, to); + peak = peak.max(sim.route(a, 7).map_or(0, |route| route.metric)); + } + } + assert_eq!(peak, 0, "a never takes back a route that crossed it"); + + for (from, to) in [(c, b), (b, c), (b, a), (c, a)] { + sim.release(from, to); + } + assert!(sim.run()); + for node in [a, b, c] { + assert!(!sim.holds(node, 7), "node {node}"); + assert!(!sim.remembers(node, 7), "node {node}"); + } +} + +/// A scoped peer hands a relay's own route back under the key the relay files that +/// peer's identities by. The hops are never qualified, so the relay still finds +/// itself in them and refuses the copy. +#[test] +fn a_route_that_returns_through_a_scoped_peer_is_refused() { + let (origin, relay, peer) = (0, 1, 2); + let mut sim = Sim::new(3); + sim.join(origin, relay, 1); + sim.link(relay, peer, SimLink::cost(1).grant(LOCAL), SimLink::cost(1)); + sim.originate(origin, 7, 0); + sim.announce(origin, "local/x", 0, None); + assert!(sim.run()); + let key = qualified(LOCAL.subject, 7); + assert_eq!(next(&sim, peer, 7), Some(relay)); + assert!(sim.holds(relay, key), "the peer sent the route back"); + assert!(sim.route(relay, key).is_none(), "it crossed the relay"); + assert_eq!(sim.shows(relay, key, "local/x"), None); + + sim.disconnect(origin, relay); + assert!(sim.run()); + assert!(!sim.holds(relay, key) && !sim.holds(peer, 7)); +} + +/// A route that already crossed as many relays as one may goes no further: the +/// next relay cannot add itself, so it is unreachable there, not waiting on a seqno. +#[test] +fn a_route_stops_at_the_hop_limit() { + let mut sim = Sim::new(5); + for node in 0..5 { + sim.nodes[node].max_hops = 2; + } + for node in 0..4 { + sim.join(node, node + 1, 1); + } + originate(&mut sim, 0, 7, 0); + assert!(sim.run()); + assert_eq!(sim.route(2, 7).map(|route| route.metric), Some(2), "crossed 1, and 2 makes two"); + assert!(sim.route(3, 7).is_none(), "2's route crossed two relays already"); + assert!(sim.holds(3, 7) && !sim.starved(3, 7)); + assert!(!sim.holds(4, 7), "3 has nothing to send on"); +} + +/// The cost of the longest loop-free path from `from` through nodes not yet `seen`, +/// each hop charged at the receiver's side of the link. +fn longest(sim: &Sim, from: Node, seen: &mut Vec) -> Metric { + seen.push(from); + let mut best = 0; + for to in 0..sim.links.len() { + if let Some(link) = sim.links[to][from] + && !seen.contains(&to) + { + best = best.max(link.cost + longest(sim, to, seen)); + } + } + seen.pop(); + best +} + +/// Random meshes with the origin behind a relay deliver every message and echo in a +/// random order while links flap and relays collect. A route names the relays it +/// crossed, so no relay ever selects one longer than a loop-free path: a node that +/// forgot the origin cannot take back a copy of its own old route. +#[test] +fn sweep_no_route_outgrows_a_loop_free_path() { + let mut rng = XorShift(0x0bad_c0de); + let (mut flaps, mut collected, mut cut) = (0, 0, 0); + for case in 0..400 { + let relays = 3 + rng.next(3) as usize; + let origin = relays; + let mut sim = Sim::new(relays + 1); + let mut links = Vec::new(); + for a in 0..relays { + for b in a + 1..relays { + if b == a + 1 || rng.chance(50) { + sim.join(a, b, 1 + rng.next(3)); + links.push((a, b)); + } + } + } + // The origin's links come first, so they flap most. + for _ in 0..1 + rng.next(2) { + let relay = rng.next(relays as u64) as usize; + if !sim.connected(origin, relay) { + sim.join(origin, relay, 1 + rng.next(2)); + links.insert(0, (origin, relay)); + } + } + let bound = longest(&sim, origin, &mut Vec::new()); + originate(&mut sim, origin, 7, 0); + + let check = |sim: &Sim, step: usize| { + for node in 0..relays { + let metric = sim.route(node, 7).map_or(0, |route| route.metric); + assert!( + metric <= bound, + "case {case} step {step}: node {node} selected a route of {metric}, past {bound}" + ); + } + assert_loop_free(sim, relays + 1, 7); + }; + for step in 0..300 { + match rng.next(40) { + 0 | 1 => { + let pick = match rng.chance(60) { + true => 0, + false => rng.next(links.len() as u64) as usize, + }; + let (a, b) = links[pick]; + match sim.connected(a, b) { + true => sim.disconnect(a, b), + false => sim.connect(a, b), + } + flaps += 1; + } + 2 => { + let node = rng.next(relays as u64) as usize; + if !sim.holds(node, 7) { + sim.collect(node, 7); + collected += 1; + } + } + 3 => sim.bump(origin), + _ => { + let (busy, acks) = (sim.busy(), sim.busy_acks()); + let pick = rng.next((busy.len() + acks.len()).max(1) as u64) as usize; + if let Some(&(from, to)) = busy.get(pick) { + sim.deliver(from, to); + } else if let Some(&(from, to)) = acks.get(pick - busy.len()) { + sim.deliver_ack(from, to); + } + } + } + check(&sim, step); + } + assert!(sim.run(), "case {case} never settles"); + check(&sim, usize::MAX); + + // Quiet: a relay the origin still reaches routes to it, and every other one + // holds nothing, its distance included. + let mut reached = vec![origin]; + let mut next = 0; + while let Some(&at) = reached.get(next) { + next += 1; + for peer in 0..=relays { + if sim.links[at][peer].is_some() && sim.connected(at, peer) && !reached.contains(&peer) { + reached.push(peer); + } + } + } + cut += usize::from(reached.len() <= relays); + for node in 0..relays { + match reached.contains(&node) { + true => assert!(sim.route(node, 7).is_some(), "case {case}: node {node} lost its route"), + false => { + assert!(!sim.holds(node, 7), "case {case}: node {node} holds a dead route"); + assert!(!sim.remembers(node, 7), "case {case}: node {node} keeps a dead distance"); + } + } } - // The origin echoes b's ends, and echoes overtake every route still waiting. - while sim.deliver(b, origin) {} - while [(a, b), (b, a), (origin, b)] - .into_iter() - .any(|(x, y)| sim.deliver_ack(x, y)) - {} - assert_eq!(peak, 3 + round, "round {round}"); } + assert!(flaps > 0 && collected > 0 && cut > 0, "{flaps} flaps, {collected} collects, {cut} cut"); } From f7b47f1eed201b1f5339beb3073f06cbd5f1bc6e Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 03:10:10 -0800 Subject: [PATCH 05/17] fix(net)!: the origin names itself in a route's hops, and a crossed route is infeasible A route that crossed the receiver is infeasible rather than ignored, so a relay whose neighbours all route through it still holds its claims while one of them finds another way. With no distance kept nothing waits on a seqno. The origin starts the hops with its own, so a rotated identity's route is refused where it began. The origin's hop limit bounds a route's hops. The route model carries hops and link costs, checks that every route names a loop-free path at its cost, and gains two configs with the origin behind a triangle. The draft, the cluster doc, the verify-route skill, and the routes epic describe the hops, and the quest is done. Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 29 ++- doc/bin/relay/cluster.md | 22 ++- drafts/draft-lcurley-moq-lite.md | 34 +++- quest/m1/route-inductive.md | 6 +- quest/m1/route-mesh-model.md | 5 +- quest/m2/cluster-routing/routes/README.md | 34 ++-- quest/m2/cluster-routing/routes/echo-order.md | 173 ------------------ .../m2/cluster-routing/routes/interest-set.md | 13 +- quest/m2/cluster-routing/routes/js.md | 2 +- .../m2/cluster-routing/routes/route-stream.md | 11 +- rs/moq-net/src/fuzz.rs | 6 +- rs/moq-net/src/lite/announce.rs | 46 ++++- rs/moq-net/src/lite/publisher/routed.rs | 16 +- rs/moq-net/src/lite/subscriber/routed.rs | 6 +- rs/moq-net/src/model/origin.rs | 5 +- rs/moq-net/src/route/mod.rs | 28 ++- rs/moq-net/src/route/node.rs | 12 +- rs/moq-net/src/route/tests/mod.rs | 24 ++- rs/moq-net/src/route/tests/routing.rs | 94 ++++++++-- rs/moq-net/verify/route/Behind.cfg | 26 +++ rs/moq-net/verify/route/BehindDear.cfg | 25 +++ rs/moq-net/verify/route/CountToInfinity.cfg | 20 -- rs/moq-net/verify/route/RouteHandoff.cfg | 7 +- rs/moq-net/verify/route/RouteHandoff.tla | 127 ++++++++----- rs/moq-net/verify/route/RouteHandoff.view.ts | 33 ++-- 25 files changed, 424 insertions(+), 380 deletions(-) delete mode 100644 quest/m2/cluster-routing/routes/echo-order.md create mode 100644 rs/moq-net/verify/route/Behind.cfg create mode 100644 rs/moq-net/verify/route/BehindDear.cfg delete mode 100644 rs/moq-net/verify/route/CountToInfinity.cfg diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index d2a2a815011..d4723f21f13 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.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,24 +20,33 @@ 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 | TRIANGLE | +| `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,462,496 | -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 @@ -45,11 +54,11 @@ A counterexample is a path through the model, not yet a bug. Replay it on the ro ## 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: `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 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`, `through`, `selected`, `infeasible`, `recoverable`, `live`, `certifiers` | `Feasible`, `Crossed`, `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` `show`, `shown_now` | `Events`, `ShownNow` | @@ -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, GOAWAY, link priority, costs other than 1 and 2, the hop limit, 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. diff --git a/doc/bin/relay/cluster.md b/doc/bin/relay/cluster.md index d17024b76ce..e00dd0ac9cc 100644 --- a/doc/bin/relay/cluster.md +++ b/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 @@ -109,10 +111,10 @@ 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 -own hop even when its peer appends it on receipt. Older versions and peers +moq-lite-03 and later, and moq-transport drafts 18 through 22 when the MoQ +Cluster extension is negotiated. On moq-lite-07-wip it bounds the nodes a route +crosses, the publishing node and this relay included. 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. ## Upstream links @@ -182,7 +184,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 @@ -281,7 +284,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. diff --git a/drafts/draft-lcurley-moq-lite.md b/drafts/draft-lcurley-moq-lite.md index f026f67e54a..ce21b0162ed 100644 --- a/drafts/draft-lcurley-moq-lite.md +++ b/drafts/draft-lcurley-moq-lite.md @@ -407,7 +407,7 @@ The subscriber creates the stream with an ANNOUNCE_REQUEST message. The publisher replies with a single ANNOUNCE_OK message followed by the matching routes and claims and any future changes: - ROUTE_START: the publisher reaches an origin node. -- ROUTE_UPDATE: a route's seqno, metric, or down-only bit changed. +- ROUTE_UPDATE: a route's seqno, metric, down-only bit, or hops changed. - ROUTE_HOLD: the publisher has no usable route but holds it while it recovers. - ROUTE_END: the publisher let go of a route and every claim under it. - ANNOUNCE_START: a matching claim of a route's origin node. @@ -492,8 +492,15 @@ A receiver adds the session's link cost (see [Cost Parameter](#cost-parameter)) Each link adds at least 1, so a route's metric strictly increases away from its origin. A metric that overflows 64 bits makes the route unusable. +A route carries its Hops: the Hop ID of every node it crossed, the origin node first and the sender last. +A Hop ID is a non-zero 64-bit value a node names itself with for as long as its process runs, such as the Node ID it started with; a rotation does not change it. +A node sending its selected route appends its own Hop ID to the Hops it received, and an origin's own route starts with its Hop ID alone. +A relay forwards the other entries unchanged and never qualifies them. +A route that arrives with 32 Hops is unusable. + A node keeps a feasibility distance per Node ID: the highest Seqno of any route it advertised, and the lowest metric it advertised at that Seqno, as in [RFC8966] Section 3.5.1. -A route is feasible when no feasibility distance is kept for its Node ID yet, when its Seqno is greater than the distance's, or when its Seqno is equal and its advertised Metric is lower. +A route whose Hops name the receiver is never feasible there: it is a copy of a route the receiver sent. +Any other route is feasible when no feasibility distance is kept for its Node ID yet, when its Seqno is greater than the distance's, or when its Seqno is equal and its advertised Metric is lower. A node selects, per Node ID, among its feasible routes that are not held: a session that has not received a GOAWAY, then the highest local priority, then the lowest metric. It MUST NOT select an infeasible route, and a distance only ever falls within a Seqno, so advertising a longer route never raises it. A node MAY mark a session upstream. @@ -504,18 +511,19 @@ A node that does not forward, such as a client, sends only its own route, and ho An origin advances its Seqno whenever its own set of sessions changes. It never advertises a Seqno or Revision of 2^64-1: a change that would reach it instead rotates its Node ID, ending the old route everywhere and announcing its claims again under the new one. -A node with no usable route to an origin node holds it while it can still recover: while every route it has to the node is infeasible, or a peer holds a route whose last advertisement is feasible here. +A node with no usable route to an origin node holds it while it can still recover: while it keeps a feasibility distance for the node and a route it has to the node is infeasible, or a peer holds a route whose last advertisement is feasible here. A held route travels as a ROUTE_HOLD, and its claims stay shown but unavailable until a ROUTE_UPDATE makes it usable again. Otherwise the node lets go, sending ROUTE_END wherever it advertised the route, and its claims go offline. Neither proves that the origin withdrew its claims. -A node whose routes to an origin node are all infeasible sends a ROUTE_REQUEST with its distance's Seqno plus 1 to the peer whose route it would select were it feasible. +A node that keeps a feasibility distance for an origin node, and whose routes to it are all infeasible, sends a ROUTE_REQUEST with its distance's Seqno plus 1 to the peer whose route it would select were it feasible. A node holding a selected route at least that new answers by advertising it, and the origin answers by raising its Seqno to at least the requested one; a request for 2^64-1 rotates the origin's Node ID. Any other node forwards the request to the peer whose route it would select, even the requester. Every node keeps one pending request per origin node, its own or forwarded, at the highest Seqno requested, dropping requests no newer, until it selects a route at least that new or has no route left, and sends it again whenever its Seqno rises or that peer changes. The receiver of a ROUTE_END echoes it back on the same stream once it dropped the route. -A node drops a feasibility distance once it neither selects nor advertises the route and every ROUTE_END it sent for it was echoed; a closed session counts as an echo. +A node drops a feasibility distance once no peer's route to the node is left open, it advertises none, and every ROUTE_END it sent for it was echoed; a closed session counts as an echo. +No peer then routes through the node, and its Hops refuse any copy of its own route that still returns. A SUBSCRIBE, FETCH, TRACK, TRACKS, or DATAGRAMS request names the origin node that serves it. A subscriber that names 0 lets the publisher select one (see [Resolution](#resolution)), and a relay forwarding a request names the origin node it selected or was given. @@ -1143,6 +1151,8 @@ ROUTE_START Message { Seqno (i), Metric (i), Down Only (8), + Hop Count (i), + Hop ID (i) ..., } ~~~ @@ -1164,6 +1174,13 @@ The publisher's metric to the origin node, 0 when it is the origin. 1 if the route is down-only (see [Routing](#routing)), 0 otherwise. Any other value is a PROTOCOL_VIOLATION. +**Hop Count**: +The number of Hop IDs that follow. +More than 32 is a PROTOCOL_VIOLATION. + +**Hop ID**: +The route's Hops (see [Routing](#routing)), in order, the publisher's own last. + ## ROUTE_UPDATE {#route-update} A publisher sends a ROUTE_UPDATE message when a route it sent changes, referencing its Route ID. @@ -1176,6 +1193,8 @@ ROUTE_UPDATE Message { Seqno (i), Metric (i), Down Only (8), + Hop Count (i), + Hop ID (i) ..., } ~~~ @@ -1185,14 +1204,14 @@ Set to 0x7 to indicate a ROUTE_UPDATE message. **Route ID**: The ordinal implicitly assigned by a prior ROUTE_START on this stream. -**Seqno**, **Metric**, and **Down Only**: +**Seqno**, **Metric**, **Down Only**, **Hop Count**, and **Hop ID**: As defined for [ROUTE_START](#route-start), replacing the route's. A ROUTE_UPDATE for a held route makes it usable again. ## ROUTE_HOLD {#route-hold} A publisher sends a ROUTE_HOLD message when it has no usable route to the origin node but still holds the route and its claims while it recovers (see [Routing](#routing)), referencing its Route ID. -The receiver keeps the route's last Seqno, Metric, and Down Only, and does not select it until a ROUTE_UPDATE. +The receiver keeps the route's last Seqno, Metric, Down Only, and Hops, and does not select it until a ROUTE_UPDATE. ~~~ ROUTE_HOLD Message { @@ -2230,6 +2249,7 @@ The `Message Length` describes the payload size on the wire. - A receiver mints an Instance for each announcement a session of an earlier version delivers, and a `Minted` field beside every Instance (ANNOUNCE_START, ANNOUNCE_RESTART, TRACK, TRACKS, SUBSCRIBE, FETCH, and DATAGRAMS) says whether a receiver minted it, so no Instance text is reserved for minting. - Added announce compression: ANNOUNCE_START gains `Path Base` and `Path Keep` to copy the head of a live claim's suffix. - Split routing into two layers on the Announce Stream. ROUTE_START (0x6), ROUTE_UPDATE (0x7), and ROUTE_END (0x8) advertise how the publisher reaches an origin node, named by a Node ID, with a seqno, an additive metric, and a down-only bit, and loops are prevented by Babel's feasibility condition. Every ANNOUNCE_START names its route's Route ID in place of the Hop ID list, so a link change sends one ROUTE_UPDATE per origin rather than an update per claim. Removed the Hop ID list and ANNOUNCE_OK's Hop ID, and replaced the SETUP Hop parameter (0x5) with a [Node ID parameter](#node-id-parameter), so an endpoint that reaches itself detects it at setup. +- Added Hops to ROUTE_START and ROUTE_UPDATE: the Hop ID of every node the route crossed, at most 32. A route whose Hops name the receiver is never feasible there, so a node that dropped its feasibility distance cannot take back a copy of its own route. - Added ROUTE_HOLD (0xB), which holds a route while it recovers; ROUTE_END lets it go. Neither withdraws the origin's claims, and the subscriber echoes every ROUTE_END back. - Added ROUTE_REQUEST (0xA), sent by the subscriber on the Announce Stream to ask for a route with a newer seqno when every route it has is infeasible. - Added ANNOUNCE_FLOOR (0x9), closing each batch of a route's claims with the origin Revision at which the stream's claims across the requested prefix are certified plus one, or 0 to certify nothing, so a stale copy never revives a claim whose withdrawal a newer one delivered. A floor certifies only the claims its own request shows. diff --git a/quest/m1/route-inductive.md b/quest/m1/route-inductive.md index 91dcece786b..ac1efca1f11 100644 --- a/quest/m1/route-inductive.md +++ b/quest/m1/route-inductive.md @@ -36,9 +36,9 @@ stay constants the config states. Say both bounds in the `verify-route` skill. replay it on `route::tests::Sim` as the skill says before calling it a bug. - Apalache needs type annotations. Add them to the spec TLC already checks, so both tools read one file and neither drifts. -- `NoCountToInfinity` stays out until - [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) lands; expect - the search for the invariant to find that path again. +- `NoCountToInfinity` follows from `SimplePaths`, which is inductive on its + own: every route sent adds its sender to hops that did not name it + ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)). Start there. - Run it through the `tla` recipes with Apalache from the flake. If five relays does not fit Nightly, record the largest mesh that does and its time. diff --git a/quest/m1/route-mesh-model.md b/quest/m1/route-mesh-model.md index cc0e93fc9b5..3b7fef840ec 100644 --- a/quest/m1/route-mesh-model.md +++ b/quest/m1/route-mesh-model.md @@ -27,9 +27,8 @@ are routing's confidence gates for finalizing lite-07. - Keep explicit-state runs tractable with `SYMMETRY` over interchangeable relays; run larger meshes with TLC's random simulation in Nightly ([nightly models](/quest/m1/model-checks-nightly.md)). -- Count to infinity stays in its own open-finding config until - [the echo fix](/quest/m2/cluster-routing/routes/echo-order.md) lands, so - the other rules still run on larger meshes. +- Check `SimplePaths` and `NoCountToInfinity` on every mesh: a route names + the nodes it crossed since [moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487). Replay every counterexample on `route::tests::Sim` before calling it a bug, as the `verify-route` skill says, and pin confirmed ones as `residual_*` tests. diff --git a/quest/m2/cluster-routing/routes/README.md b/quest/m2/cluster-routing/routes/README.md index 5ca33d6e685..10827756b46 100644 --- a/quest/m2/cluster-routing/routes/README.md +++ b/quest/m2/cluster-routing/routes/README.md @@ -40,7 +40,7 @@ The items below were decided 2026-11-10 (maintainer, /quest-plan on lite-07 rout 22. ✅ **A side's interest is a set of prefixes edited in place.** The live set never nests, and one edit may swap prefixes for a wider or narrower one without re-sending what both cover ([the interest set](/quest/m2/cluster-routing/routes/interest-set.md)). A token-scope change is such an edit, with one prefix per region of the scope. This supersedes items 16 and 17, and the handoff contract's "An interest change opens a new stream" below, once the route stream lands. 23. ✅ Asked what a floor covers with several prefixes on one stream: **one prefix, named by its id.** This amends item 10: the floor is still a marker and never a region list. Rejected: a floor over the whole set. 24. ✅ Asked how a side learns a newly added prefix's initial set is complete: **SYNCED per prefix, naming its id**, plus one marker per edit where it takes effect for both sides. Rejected: one SYNCED per edit, counted in order. -25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the relays it crossed, and a node never uses a route that names itself** ([the fix](/quest/m2/cluster-routing/routes/echo-order.md), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. +25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the nodes it crossed, and a node never uses a route that names itself** ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. As built: such a route is infeasible rather than ignored, so a relay whose neighbours all route through it still holds its claims while one of them finds another way; the origin names itself too, so a rotated identity's route is refused where it began; and a node names itself by a Hop ID that a rotation leaves alone. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. The route layer's core landed in @@ -144,11 +144,13 @@ the bullets below are the contract it carries. `reconnect_without_restart_needs_a_seqno_advance`). A random identity alone does not keep a dead incarnation away. What bounds it is ordered sessions, state scoped to the session that delivered it, never advertising an - unreachable route, and keeping the feasibility distance until every - ROUTE_END it sent is echoed back: a collected incarnation then reappears - only from a - message already in flight on a live session, which delivers the retraction - next (`collected_incarnation_returns_only_while_its_retraction_is_in_flight`). + unreachable route, keeping the feasibility distance until every + ROUTE_END it sent is echoed back, and the hops each route carries, which + refuse a copy of a route this node sent once the distance is gone: a + collected incarnation then reappears only from a message already in flight + on a live session that never crossed this node, which delivers the + retraction next + (`collected_incarnation_returns_only_while_its_retraction_is_in_flight`). `cluster.id` stops naming a routing identity. - Decided 2026-10-14: every identity a scoped connection sends is qualified: filed under a key the receiver derives, rather than its bare @@ -193,9 +195,9 @@ the bullets below are the contract it carries. ROUTE_HOLD or ROUTE_END. The route model found a count to infinity (2026-11-10): an echo can overtake a route derived from the echoed one, and even in order a per-neighbour echo misses a derived copy held by a - third relay; [the fix](/quest/m2/cluster-routing/routes/echo-order.md) - adds the relays a route crossed, and a node refuses one naming itself - (Plan item 25). + third relay. Each route therefore names the nodes it crossed, and one + naming the receiver is never feasible there (Plan item 25, + `sweep_no_route_outgrows_a_loop_free_path`). - Starvation recovery is Babel's seqno request (RFC 8966 s3.8, decided 2026-10-12). A node whose routes to an origin are all infeasible sends ROUTE_REQUEST for that origin, with its feasibility seqno plus one, to the @@ -389,9 +391,11 @@ loss never reports an END: feasibility distance once it also advertises the identity nowhere and every neighbour has echoed each ROUTE_END it sent, or closed. Until then an advertisement derived from its own can still wait on some session, and - accepting it loops; once all echoes are back no node holds its - advertisement, so dropping the distance is as safe as a fresh node joining - (`collection_keeps_the_feasibility_distance_against_a_queued_echo`). The + accepting it loops; once all echoes are back no neighbour routes through + it (`collection_keeps_the_feasibility_distance_against_a_queued_echo`), + and a copy a third node still holds names this node in its hops, so it is + refused when it returns + (`a_route_handed_round_a_triangle_is_refused_where_it_began`). The echo is per neighbour, not a diffusing computation: every other node keeps its own distance. A stale route accepted after the drain dead-ends at a node that let go, like any collected incarnation. @@ -485,7 +489,11 @@ Decided with the maintainer 2026-10-16, from the handoff proof: every step, and leaves no distance for a dead identity; dropping the distance before the echoes return fails the queued echo fixture, and dropping it at no entry loops where the echoed condition never does - (`sweep_forgetting_distances`). Rejected: keeping the distance forever, + (`sweep_forgetting_distances`). Revised 2026-11-10 (Plan item 25): the + echo is not enough alone, since a third node can hold a copy derived from + the advertisement and hand it back after the drain. Each route names the + nodes it crossed and is never feasible where it has been + (`sweep_no_route_outgrows_a_loop_free_path`). Rejected: keeping the distance forever, which grows with publisher churn times uptime on every relay that saw an identity, about 16 bytes each, until a restart; and Babel's source GC timer, which assumes stale echoes are gone by then rather than proving it. diff --git a/quest/m2/cluster-routing/routes/echo-order.md b/quest/m2/cluster-routing/routes/echo-order.md deleted file mode 100644 index 6a4a16b7018..00000000000 --- a/quest/m2/cluster-routing/routes/echo-order.md +++ /dev/null @@ -1,173 +0,0 @@ -# [L] A node never takes back a route that crossed it - -## Goal - -A lite-07 route names the relays it crossed, and a node never uses a route -that names itself. A node that has forgotten an identity therefore cannot -take back a copy of its own old route, however long that copy was in flight -and whatever sessions closed meanwhile. The router, `route::tests::Sim`, the -route model, and the draft agree on the rule, and TLC finds no count to -infinity on meshes where the origin sits behind a relay, with unit and with -unequal link costs, with the echo travelling as it does on today's streams. -A dead publisher goes offline everywhere and routing goes quiet. - -## Plan - -Found 2026-11-10 by the route model ([moq-dev/moq#8447](https://github.com/moq-dev/moq/pull/8447)): -`rs/moq-net/verify/route/CountToInfinity.cfg` breaks `NoCountToInfinity` in -9 steps with no partition. A node drops its feasibility distance once every -neighbour echoed its ROUTE_END (`update` in `route/mod.rs`). But the echo -rides the announce stream the node answers, while the neighbour's own routes -ride the stream the node asked for (`route/node.rs`), so the echo can -overtake an older route the neighbour derived from the node's. - -Found the same day, a /quest-plan on lite-07 routing: **putting the echo in -order is not enough.** With the echo behind the echoer's routes, as -[moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487) has it in the -model and `Sim`, the model still counts to infinity once the origin is not -adjacent to every relay. An echo proves only that nothing derived is in -flight on that one link; a derived copy can sit at a third relay and arrive -over two hops. The shortest case, an origin behind relay A with A, B, and C -in a triangle and unequal costs: - -1. The origin announces. A advertises to B and C, and B and C to each other. -2. The origin's session closes. A sends ROUTE_END to B and C. -3. B and C each apply it and echo. Their earlier ROUTEs to each other are - still queued. -4. A has both echoes and drops its distance. -5. B receives C's old ROUTE, which is feasible there, selects it, and - advertises it to A, which accepts it. -6. The route laps A, C, B, A, each relay draining and accepting again, and - the metric climbs without bound. - -#8487's triangle passes because its origin is one of the three nodes and -drops what it hears for its own identity. - -Decided 2026-11-10 (maintainer, the same /quest-plan), asked how a relay -safely forgets a publisher that is gone: a relay acknowledges a ROUTE_END -only when its own downstream has. **Superseded the same day, after the model -ran it.** That rule needed three sub-rules, each forced by a counterexample -(a held route counts as routing through the sender; a holding node defers -until the hold resolves; a deferred echo waits only on the ROUTE_ENDs -outstanding when it was deferred). It then passed with one flap and failed -with two: a closed session counts as that neighbour's echo while its last -advertisement is still in flight, so a relay takes back one stale copy of -its own route. The copy stayed within two laps, but no rule that works by -proving "nothing is left" survives a session that closes before answering. -It also makes an upstream wait on its whole subtree before it may -re-advertise, and lets a peer that withholds its echo stall that upstream. - -Decided 2026-11-10 (maintainer, the same /quest-plan, with the model results -in hand): ✅ **each route names the relays it crossed, and a node never uses -a route that names itself.** Feasibility still selects routes and still -stops hunting; the list is only a refusal, and it covers the one case -feasibility cannot, a node that no longer remembers. It is one list per -origin route, not the per-claim Hop ID list lite-07 removed, so a link -change still sends one ROUTE_UPDATE per origin, and the Rendezvous Hash and -per-broadcast choices among neighbours are unaffected: a node keeps one -entry per origin per neighbour as today. The echo and the drain rule stay -exactly as they are. Rejected: the deferred echo above; never dropping the -distance, about 16 bytes per publisher ever seen, which a peer can grow on -purpose; a timer as in RFC 8966, whose safety rests on stale messages being -gone by then; and making only relays origin nodes, rejected again. - -What the model showed, all in -`rs/moq-net/verify/route/DRAIN.md` on the branch -`route-drain-counterexamples` (`5e7e3eb434`), which also holds the model -with all three variants behind switches, per-link costs, the configs that -reproduce each result, and four `Sim` replays of the original count: - -- With the list, the triangle passes at full bounds, and the origin behind - a triangle passes with two flaps at unit cost and at four unequal cost - sets. The same holds with the echo free to overtake its sender's other - messages, which is today's wire; without the list that ordering counts to - infinity in 11 states. -- The echo cannot go: with the list and no echo, a node forgets while a - neighbour still routes through its advertisement, and `LoopFree` fails in - 944 states. -- A self-naming route is kept as an unusable entry until it ends. Dropping - it outright lets collection run while the neighbour's route is still open. -- Not run: full bounds on the 4-relay shapes, any 5-relay shape, and the - runs listed there as stopped. No message count was measured. - -So this lands on today's Announce Streams and does not wait for -[the route stream](/quest/m2/cluster-routing/routes/route-stream.md), which -later puts the echo in order by construction. A recommendation the -maintainer has not confirmed; say so in the PR. - -Work, model first: - -- In `RouteHandoff.tla`, keep the echo on its own queue as on `main`, add - the list and a cost per link, add the origin behind a triangle (unit and - unequal costs) to the checked configs, and turn `NoCountToInfinity` on in - every config. Delete `CountToInfinity.cfg` as an open finding. If - [moq-dev/moq#8479](https://github.com/moq-dev/moq/pull/8479) has landed, - that includes its line, ring, and chord, with costs; if not, whichever - lands second adapts. -- **The list's one cost is unmeasured, so measure it before the router.** - An upstream path change at equal metric now sends a ROUTE_UPDATE to - everyone downstream, where today it stops. Run the list against #8479's - announce budget (4 routing messages per session direction per external - change) on its meshes. If it breaks the budget or brings hunting back, - stop and report it rather than raising the budget. -- Say what stays unexplored. Run TLC one config at a time on the recipe's - settings; the 4-relay shapes with the origin inside a cycle did not finish - in 40 minutes on a loaded host. -- Router: an advertisement and a route entry carry the list; `route` marks - an entry that names this node; `selected`, the infeasible set, and the - certifiers skip it, so it never holds a route or asks for a seqno; a node - appends its own Node ID when it advertises. Turn the four replays and the - two-flap trace into tests that the metric never passes the longest - loop-free path. -- Wire, for the implementer to confirm or improve; list each departure in - the PR. ROUTE_START and ROUTE_UPDATE gain a count and that many Node IDs, - in order from the origin, the sender last and the origin itself left out. - List entries are never qualified: a relay files a scoped peer's origin - Node ID under a qualified one as today, and carries the list's entries on - as received, each a bare Node ID. A relay cannot compute another relay's - qualification, so a qualified entry could never match the node it names. - A scoped peer can then add or drop entries only on routes filed under its - own qualified identities, which harms nothing but those routes, and a lap - through it is still stopped by refusing to requalify a qualified identity - (`scoped_connections_cannot_requalify_a_qualified_identity`). The model - has no scoped grants, so cover this in `Sim` with a route that crosses a - relay, a scoped peer, and the same relay again. A list longer than a - fixed limit makes the route unusable; reuse lite-06's hop limit unless - there is a reason not to. A node that forwards declares a Node ID, since - it has to name itself. -- Draft: the two messages, Routing (a route that names the receiver, that - list entries are never qualified, and that forgetting is safe because of - the list, not because of the echo alone), the Node ID Parameter, which - today says an endpoint that originates no routes omits it and must now - say a node that forwards sends it, and the lite-07 changelog. `js/net` has no route layer yet, so - [its quest](/quest/m2/cluster-routing/routes/js.md) decodes the list and - sends an empty one for its own route. -- Update the `verify-route` skill's open finding, coverage, and sync - commit, and the three places in the epic that say the echo alone makes - forgetting safe: the loop-freedom bullet, decision 6, and the handoff - contract's bullet on dropping the distance ("as safe as a fresh node - joining"). -- [moq-dev/moq#8457](https://github.com/moq-dev/moq/pull/8457)'s cache - sweep runs on the Rust router and depends on the feasibility check; rerun - it with the list if it has landed. -- Run `just check`, `just test interop --all`, and `just drafts check`. - -#8487 holds this quest's branch with the echo moved behind the echoer's -routes in the model and `Sim`. That change is no longer needed here and -belongs to the route stream; start again from `main`'s model. - -Rollout: lite-07 is `-wip`, so relays pinned to `main` roll together, as -each earlier lite-07 wire change did. - -Caused by: [moq-dev/moq#7676](https://github.com/moq-dev/moq/pull/7676), -whose drain rule assumed a per-neighbour echo proves no derived route -remains, and [moq-dev/moq#8023](https://github.com/moq-dev/moq/pull/8023), -which put the echo on the answering stream. - -Public API: none. Wire: lite-07-wip, a hop list on ROUTE_START and -ROUTE_UPDATE. - -## Related - -- [Each side says everything about routing on one stream](/quest/m2/cluster-routing/routes/route-stream.md) - puts the echo in order later; this does not wait for it -- [js/net route layer](/quest/m2/cluster-routing/routes/js.md) - decodes the list in JS diff --git a/quest/m2/cluster-routing/routes/interest-set.md b/quest/m2/cluster-routing/routes/interest-set.md index d346d049493..ba70d6921fe 100644 --- a/quest/m2/cluster-routing/routes/interest-set.md +++ b/quest/m2/cluster-routing/routes/interest-set.md @@ -67,11 +67,10 @@ The edit rule those three imply, to prove rather than assume: Work: -- Start from the model and `Sim` with per-link costs and the hop list - ([the fix](/quest/m2/cluster-routing/routes/echo-order.md)), and move the - echo from its own queue onto the neighbour's FIFO, as - [moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487) did: with one - stream per side nothing overtakes anything. +- Start from the model and `Sim` with link costs and hops + ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)), and move the echo from its own queue onto the neighbour's FIFO, as + that PR's first commit (`81c0698295`) did: with one stream per side nothing + overtakes anything. - Give the model at least two prefixes and edits in flight: add, remove, widen, narrow, and an edit that crosses a claim change, a route change, a ROUTE_END, and its echo. The model fixes interest at the root today, so @@ -98,7 +97,3 @@ one key, which `Sim` and the tests use, so this changes no behaviour on its own. Public API: none (the router is crate-private). Wire: none. - -## Required - -- [A node never takes back a route that crossed it](/quest/m2/cluster-routing/routes/echo-order.md) - the model, `Sim`, and router with per-link costs and the hop list, which this builds on diff --git a/quest/m2/cluster-routing/routes/js.md b/quest/m2/cluster-routing/routes/js.md index 70f2ffbabc7..5f9a931d8e5 100644 --- a/quest/m2/cluster-routing/routes/js.md +++ b/quest/m2/cluster-routing/routes/js.md @@ -18,7 +18,7 @@ Decided 2026-10-27 (maintainer), from the cheapest one; fix it with the route-selection rework here. - Feed the availability API (`RouteInfo.available` and the `offline` route kind) from the route layer. - Rust/JS interop covers the route messages, the floor marker, and the echo. -- Decode the hop list on ROUTE_START and ROUTE_UPDATE and send an empty one for the tab's own route, once [the fix](/quest/m2/cluster-routing/routes/echo-order.md) adds it. A tab forwards nothing, so it never appends itself; the [browser mesh](/quest/m5/browser-mesh.md) does. +- Decode the Hops on ROUTE_START and ROUTE_UPDATE, and send the tab's own route with its own Hop ID alone, the Node ID it starts with. A tab forwards nothing, so it adds itself to no other route; the [browser mesh](/quest/m5/browser-mesh.md) does. - Encode lite-07's Route ID (ANNOUNCE_START) and Node ID (every TRACK, TRACKS, SUBSCRIBE, FETCH, and DATAGRAMS request, 0 when the publisher selects the node) as Rust does, and pin `js/net/src/lite/announce.test.ts`'s goldens to `lite::compress`'s `GOLDEN` and `JS_LITERAL`. - Leave the temporary Lite-06 Chain Setup Parameter unsent: JS translates nothing, so it keeps no chain, and a Rust peer sends the chain only to a peer that offers it. - Restore the native JS lite-07 lanes. Decided 2026-11-06 (maintainer, diff --git a/quest/m2/cluster-routing/routes/route-stream.md b/quest/m2/cluster-routing/routes/route-stream.md index d1046676ef9..4f557833dfa 100644 --- a/quest/m2/cluster-routing/routes/route-stream.md +++ b/quest/m2/cluster-routing/routes/route-stream.md @@ -18,12 +18,11 @@ Decided 2026-11-10 (maintainer, /quest-plan on lite-07 routing). Why: today a side's requests ride the streams it opened and its answers ride the streams its peer opened, and QUIC orders no stream against another. The -first count to infinity [the fix](/quest/m2/cluster-routing/routes/echo-order.md) -records is one message overtaking another across that split, and the router -keys each stream as its own neighbour (`route/node.rs`), where the model and -`Sim` have one neighbour per session. That fix no longer rests on this: the -hop list it adds holds with the echo unordered, so it lands first, on -today's streams. This removes the ordering hazard as a class and makes a +first count to infinity the route model found is one message overtaking +another across that split, and the router keys each stream as its own +neighbour (`route/node.rs`), where the model and `Sim` have one neighbour per +session. The fix does not rest on this: the hops a route carries +([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)) hold with the echo unordered, on today's streams. This removes the ordering hazard as a class and makes a token-scope change an edit. Settled: diff --git a/rs/moq-net/src/fuzz.rs b/rs/moq-net/src/fuzz.rs index 2ae7e49fa73..8a898a377c5 100644 --- a/rs/moq-net/src/fuzz.rs +++ b/rs/moq-net/src/fuzz.rs @@ -682,7 +682,7 @@ impl RouteRelay { let receive = (0..streams) .map(|_| { let receive = node.receive(crate::route::Link::default(), Path::empty()).unwrap(); - receive.route(Self::ORIGIN, Some(crate::route::Reach::Finite(advert))); + receive.route(Self::ORIGIN, Some(crate::route::Reach::Finite(advert.clone()))); let snapshot = (0..claims) .map(|i| (Self::path(i), Some(Self::claim(&instance, 0)))) .collect(); @@ -1590,8 +1590,8 @@ const TYPED_LITE_SEEDS: &[(u8, &[u8])] = &[ (23, &[4, 0]), (30, &[7, 0, 0, 0, 0, 0, 0, 0]), (27, &[0, 3, 0, 0, 0]), - (5, &[6, 4, 1, 0, 1, 0]), - (5, &[7, 4, 0, 1, 2, 0]), + (5, &[6, 6, 1, 0, 1, 0, 1, 1]), + (5, &[7, 6, 0, 1, 2, 0, 1, 1]), (5, &[8, 1, 0]), (5, &[9, 2, 0, 1]), (5, &[11, 1, 0]), diff --git a/rs/moq-net/src/lite/announce.rs b/rs/moq-net/src/lite/announce.rs index a8fb5ce0a97..717b10fb14f 100644 --- a/rs/moq-net/src/lite/announce.rs +++ b/rs/moq-net/src/lite/announce.rs @@ -116,14 +116,11 @@ pub enum AnnounceBroadcast { /// Encode a seqno, metric, down-only bit, and the hops the route crossed. No origin /// advertises the last seqno, which would leave no room for the successor a -/// ROUTE_REQUEST names. +/// ROUTE_REQUEST names, and no relay forwards a route that crossed too many. fn encode_advert(w: &mut Encoder<'_>, advert: &Advert) -> Result<(), EncodeError> { - if advert.seqno == route::MAX { + if advert.seqno == route::MAX || advert.hops.len() > route::MAX_HOPS { return Err(EncodeError::InvalidState); } - if advert.hops.len() > route::MAX_HOPS { - return Err(EncodeError::TooMany); - } w.varint(advert.seqno)?; w.varint(advert.metric)?; w.bool(advert.down_only); @@ -1599,6 +1596,20 @@ mod tests { id: 0, advert: advert(42, 0, true), }, + AnnounceBroadcast::RouteStart { + node: 7, + advert: Advert { + hops: [5, route::MAX, 9].into(), + ..advert(1, 3, false) + }, + }, + AnnounceBroadcast::RouteUpdate { + id: 1, + advert: Advert { + hops: (1..=route::MAX_HOPS as u64).collect(), + ..advert(1, 40, false) + }, + }, AnnounceBroadcast::RouteHold { id: 3 }, AnnounceBroadcast::RouteEnd { id: 0 }, AnnounceBroadcast::Floor { @@ -1690,6 +1701,13 @@ mod tests { id: 0, advert: advert(route::MAX, 1, false), }, + AnnounceBroadcast::RouteUpdate { + id: 0, + advert: Advert { + hops: (0..=route::MAX_HOPS as u64).collect(), + ..advert(0, 1, false) + }, + }, // The last revision has no room for the offset. AnnounceBroadcast::Floor { id: 0, @@ -1711,7 +1729,25 @@ mod tests { w.varint(0u64).unwrap(); } }; + // A route with `count` hops, naming `named` of them. + let hops = |count: u64, named: u64| { + move |w: &mut Encoder<'_>| { + for field in [1, 0, 1] { + w.varint(field as u64).unwrap(); + } + w.u8(0); + w.varint(count).unwrap(); + for hop in 0..named { + w.varint(hop + 1).unwrap(); + } + } + }; + let over = route::MAX_HOPS as u64 + 1; let malformed = [ + // More hops than a route may cross, hops missing, and one too many. + forge(ROUTE_START, hops(over, over)), + forge(ROUTE_START, hops(2, 1)), + forge(ROUTE_START, hops(1, 2)), forge(ROUTE_START, advert(0, 0, 1, 0)), forge(ROUTE_START, advert(1, route::MAX, 1, 0)), forge(ROUTE_START, advert(1, 0, 1, 2)), diff --git a/rs/moq-net/src/lite/publisher/routed.rs b/rs/moq-net/src/lite/publisher/routed.rs index 3e4fd8f5fbf..bcfa3ce0812 100644 --- a/rs/moq-net/src/lite/publisher/routed.rs +++ b/rs/moq-net/src/lite/publisher/routed.rs @@ -49,7 +49,7 @@ struct Sent { impl Sent { fn reach(&self) -> Option { - self.reach.values().next().copied() + self.reach.values().next().cloned() } /// The node's claim at `path` is now `claim`, which `link` may withhold. @@ -345,12 +345,12 @@ impl Answer { let Some(sent) = self.routes.get_mut(&id) else { // Held only follows a route the node sent, and an end of one it did not is moot. // The peer is sent the route with its first claim shown. - if let Some(reach @ route::Reach::Finite(advert)) = reach { + if let Some(route::Reach::Finite(advert)) = reach { let sent = Sent { wire: None, - advert, + advert: advert.clone(), shown: 0, - reach: BTreeMap::from([(source, reach)]), + reach: BTreeMap::from([(source, route::Reach::Finite(advert))]), claims: BTreeMap::new(), withheld: 0, floor: None, @@ -407,14 +407,14 @@ impl Answer { .get_mut(&id) .expect("a route stands while a source carries it"); let after = sent.reach(); - if let Some(route::Reach::Finite(advert)) = after { - sent.advert = advert; + if let Some(route::Reach::Finite(advert)) = &after { + sent.advert = advert.clone(); } let Some(wire) = sent.wire else { return Ok(()); }; match after { - _ if after == before => {} + after if after == before => {} Some(route::Reach::Finite(advert)) => stream.writer.buffer(&Msg::RouteUpdate { id: wire, advert })?, Some(route::Reach::Held) => stream.writer.buffer(&Msg::RouteHold { id: wire })?, None => unreachable!("a route stands while a source carries it"), @@ -436,7 +436,7 @@ impl Answer { self.next_route += 1; stream.writer.buffer(&Msg::RouteStart { node: id, - advert: sent.advert, + advert: sent.advert.clone(), })?; if sent.reach() == Some(route::Reach::Held) { stream.writer.buffer(&Msg::RouteHold { id: wire })?; diff --git a/rs/moq-net/src/lite/subscriber/routed.rs b/rs/moq-net/src/lite/subscriber/routed.rs index b450439c8c4..8d3f7847fc8 100644 --- a/rs/moq-net/src/lite/subscriber/routed.rs +++ b/rs/moq-net/src/lite/subscriber/routed.rs @@ -174,7 +174,7 @@ impl Routed { id, WireRoute { node, - reach, + reach: reach.clone(), claims: BTreeMap::new(), pending: BTreeMap::new(), committed: None, @@ -264,7 +264,7 @@ impl Routed { fn reach(&mut self, id: u64, reach: route::Reach) -> Result<(), Error> { let route = self.routes.get_mut(&id).ok_or(Error::ProtocolViolation)?; - route.reach = reach; + route.reach = reach.clone(); self.stream.route(route.node, Some(reach)); Ok(()) } @@ -347,7 +347,7 @@ impl Routed { ids.sort_unstable(); for id in &ids { let route = &self.routes[id]; - stream.route(route.node, Some(route.reach)); + stream.route(route.node, Some(route.reach.clone())); } let certifies = self.certifies(); for id in &ids { diff --git a/rs/moq-net/src/model/origin.rs b/rs/moq-net/src/model/origin.rs index 5a92caf7f47..d70fcf982a6 100644 --- a/rs/moq-net/src/model/origin.rs +++ b/rs/moq-net/src/model/origin.rs @@ -98,7 +98,8 @@ impl Hop { #[non_exhaustive] pub struct Config { /// The origin's identity on every wire: the hop id appended to broadcast hop chains - /// for loop detection, and the route identity it declares on moq-lite-07. Random by + /// for loop detection, and the route identity it declares on moq-lite-07, which also + /// names it in the hops of each route it forwards there. Random by /// default, so each process is a fresh identity; one reused across a restart has its /// lite-07 routes refused until a seqno request lifts them past the old process's. pub hop: NonZeroU64, @@ -7356,7 +7357,7 @@ impl Consumer { timers: self.timers.clone(), }; // Built before taking the lock, since opening a cursor takes it. - let node = crate::route::Node::origin(self.hop()); + let node = crate::route::Node::origin(self.hop(), self.max_hops); let claims = OwnClaims { routes: own(false).routes(), downstream: own(true).routes(), diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index 91fa5ee7ec2..059eedf2c16 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -150,7 +150,8 @@ pub(crate) fn qualifier(key: [u8; 32]) -> Arc Id + Send + Sync> { }) } -/// The most relays a route crosses: the longest hop list a message carries. +/// The most nodes a route crosses, its origin included: the longest hop list a +/// message carries. pub(crate) const MAX_HOPS: usize = 32; /// What a node advertises for one identity. @@ -159,8 +160,8 @@ pub(crate) struct Advert { pub seqno: Seqno, pub metric: Metric, pub down_only: bool, - /// The relays the route crossed, by the hop id each names itself with, in order - /// from the origin node. The sender is last, and the origin node is left out. + /// The nodes the route crossed, by the hop id each names itself with: the origin + /// node first and the sender last. pub hops: Arc<[Id]>, } @@ -399,7 +400,7 @@ pub(crate) struct Router { /// How this node names itself in the hops of a route it forwards. A rotation /// leaves it alone, so a route that crossed this node always says so. hop: Id, - /// The most relays a route this node uses may cross, itself included. + /// The most nodes a route this node uses may cross, its origin and this node included. pub max_hops: usize, neighbors: BTreeMap, origins: BTreeMap>, @@ -813,9 +814,7 @@ impl Router { // last view only for what it certified. An uncertified claim lives only // while the stream carries it, and the restart's batch names only what it // still carries, so one kept here would never be withdrawn. - if ended - && let Some(heard) = self.heard.get_mut(&(id, from)) - { + if ended && let Some(heard) = self.heard.get_mut(&(id, from)) { let raw = std::mem::take(&mut heard.raw); let kept = heard.kept.get_or_insert(raw); let floors = &kept.floors; @@ -1211,7 +1210,7 @@ impl Router { /// This node's metric through `entry`, the route `next` sent, or `None` when it is /// unreachable, never saturated: the metric overflows, or the route already - /// crossed as many relays as one may. + /// crossed as many nodes as one may. fn through(&self, next: N, entry: &Entry) -> Option { if entry.advert.hops.len() >= self.max_hops { return None; @@ -1640,13 +1639,12 @@ impl Router { /// changed among the dirty claims, unless any could have. fn advertise(&mut self, id: Id, peers: &[N], ctx: &Ctx, dirty: &Dirty) { let selected = self.selected(id); - // The selected route's hops, then this node; its own route crossed no relay. - let hops: Arc<[Id]> = match selected.and_then(|route| route.next) { - Some(next) => (self.rx[&id][&next].advert.hops.iter().copied()) - .chain([self.hop]) - .collect(), - None => Arc::default(), - }; + // The selected route's hops, then this node: its own route starts with it. + let through = selected.and_then(|route| route.next); + let hops: Arc<[Id]> = (through.iter()) + .flat_map(|next| self.rx[&id][next].advert.hops.iter().copied()) + .chain([self.hop]) + .collect(); let floors = self.adopted_floors(id).cloned().unwrap_or_default(); // Built only for a stream sent a whole snapshot, once per interest. let mut adopted: Option> = None; diff --git a/rs/moq-net/src/route/node.rs b/rs/moq-net/src/route/node.rs index 0a99d15c2d6..c4585f0e917 100644 --- a/rs/moq-net/src/route/node.rs +++ b/rs/moq-net/src/route/node.rs @@ -399,7 +399,8 @@ impl Home { } impl Node { - /// A node declaring a fresh identity, `seed` keying its rotation. + /// A node declaring a fresh identity, which also names it in the hops of the routes + /// it forwards, `seed` keying its rotation. pub fn new(id: Id, seed: u64) -> Self { debug_assert!( id != 0 && id & QUALIFIED == 0, @@ -420,11 +421,14 @@ impl Node { /// A node declaring the origin's hop id, so the origin has one identity on every /// wire. A declared identity is never qualified, so an id carrying that marker - /// loses it, or is replaced by a random one if nothing is left. - pub fn origin(hop: std::num::NonZeroU64) -> Self { + /// loses it, or is replaced by a random one if nothing is left. It uses no route + /// that crossed `max_hops` relays, which it could not add itself to. + pub fn origin(hop: std::num::NonZeroU64, max_hops: std::num::NonZeroUsize) -> Self { let mut rng = kio::clock::rng(); let id = declared_for(hop).unwrap_or_else(|| rng.random_range(1..=GENERATED)); - Self::new(id, rng.random()) + let node = Self::new(id, rng.random()); + node.lock().router.max_hops = max_hops.get(); + node } fn lock(&self) -> Locked<'_> { diff --git a/rs/moq-net/src/route/tests/mod.rs b/rs/moq-net/src/route/tests/mod.rs index 561c6e4dd50..f5b49f89f4a 100644 --- a/rs/moq-net/src/route/tests/mod.rs +++ b/rs/moq-net/src/route/tests/mod.rs @@ -128,6 +128,8 @@ pub(super) struct SimEvent { #[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] pub(super) struct Stats { pub route_msgs: usize, + /// Route messages that changed nothing but the hops: what naming them costs. + pub hop_updates: usize, pub claim_msgs: usize, pub claim_items: usize, pub requests: usize, @@ -160,6 +162,8 @@ pub(super) struct Sim { history: BTreeMap>, /// Every request sent, to spot a repeat. requested: BTreeSet<(Node, Node, Id, Seqno)>, + /// The last finite route each node sent each neighbor, to spot a change of hops alone. + routed: BTreeMap<(Node, Node, Id), Advert>, pub stats: Stats, pub events: Vec, } @@ -167,7 +171,9 @@ pub(super) struct Sim { impl Sim { pub fn new(nodes: usize) -> Self { Self { - nodes: (0..nodes).map(|node| Router::new(hop(node, 0), node as u64 + 1)).collect(), + nodes: (0..nodes) + .map(|node| Router::new(hop(node, 0), node as u64 + 1)) + .collect(), leaf: vec![false; nodes], watch: vec![Path::empty(); nodes], restarts: vec![0; nodes], @@ -180,6 +186,7 @@ impl Sim { held: BTreeSet::new(), history: BTreeMap::new(), requested: BTreeSet::new(), + routed: BTreeMap::new(), stats: Stats::default(), events: Vec::new(), } @@ -478,13 +485,22 @@ impl Sim { for out in self.nodes[node].drain() { let (to, msg) = match out { Out::Route { to, id, reach } => { - // A route names every relay it crossed once, the sender last. + // A route names every node it crossed once, the sender last. if let Some(Reach::Finite(advert)) = &reach { - let own = self.nodes[node].origins.contains_key(&id); let me = hop(node, self.restarts[node]); - assert_eq!(advert.hops.last().copied(), (!own).then_some(me), "node {node}'s hops for {id}"); + assert_eq!(advert.hops.last(), Some(&me), "node {node}'s hops for {id}"); let named: BTreeSet = advert.hops.iter().copied().collect(); assert_eq!(named.len(), advert.hops.len(), "node {node} sent {id} round a loop"); + let was = self.routed.insert((node, to, id), advert.clone()); + let same = |was: Advert| { + Advert { + hops: advert.hops.clone(), + ..was + } == *advert + }; + self.stats.hop_updates += usize::from(was.is_some_and(same)); + } else { + self.routed.remove(&(node, to, id)); } self.stats.route_msgs += 1; (to, Msg::Route { id, reach }) diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index 41b21da5d46..c28687e4829 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -1019,7 +1019,10 @@ fn a_route_handed_round_a_triangle_is_refused_where_it_began() { // c's copy, sent before the end, is shorter than what b advertised: feasible there. assert!(sim.deliver(c, b)); - assert_eq!(sim.route(b, 7).map(|route| (route.next, route.metric)), Some((Some(c), 4))); + assert_eq!( + sim.route(b, 7).map(|route| (route.next, route.metric)), + Some((Some(c), 4)) + ); // b may offer it to a once a echoes the ROUTE_END b sent it. let mut peak = 0; @@ -1042,6 +1045,33 @@ fn a_route_handed_round_a_triangle_is_refused_where_it_began() { } } +/// An origin names itself in its route's hops like any relay, so once it rotated +/// to a fresh identity and forgot the old one, a copy of the old route is still +/// refused where it began. +#[test] +fn a_retired_identitys_route_is_refused_by_the_node_that_originated_it() { + let (origin, b) = (0, 1); + let mut sim = Sim::new(2); + sim.join(origin, b, 1); + sim.hold(b, origin); + originate(&mut sim, origin, 7, MAX - 1); + assert!(sim.run()); + assert_eq!(next(&sim, b, 7), Some(origin)); + + sim.bump(origin); + assert_ne!(sim.proven(origin), 7, "the last seqno rotates the identity"); + assert!(sim.run()); + assert!(sim.deliver_ack(b, origin), "b's echo overtakes its own route"); + assert!(!sim.remembers(origin, 7)); + assert!(sim.deliver(b, origin)); + assert!(sim.holds(origin, 7), "b's copy of the old route arrived"); + assert!(sim.route(origin, 7).is_none(), "it crossed the node that began it"); + + sim.release(b, origin); + assert!(sim.run()); + assert!(!sim.holds(origin, 7) && !sim.remembers(origin, 7)); +} + /// A scoped peer hands a relay's own route back under the key the relay files that /// peer's identities by. The hops are never qualified, so the relay still finds /// itself in them and refuses the copy. @@ -1065,21 +1095,25 @@ fn a_route_that_returns_through_a_scoped_peer_is_refused() { assert!(!sim.holds(relay, key) && !sim.holds(peer, 7)); } -/// A route that already crossed as many relays as one may goes no further: the -/// next relay cannot add itself, so it is unreachable there, not waiting on a seqno. +/// A route that already crossed as many nodes as one may goes no further: the next +/// relay cannot add itself, so it is unreachable there, not waiting on a seqno. #[test] fn a_route_stops_at_the_hop_limit() { let mut sim = Sim::new(5); for node in 0..5 { - sim.nodes[node].max_hops = 2; + sim.nodes[node].max_hops = 3; } for node in 0..4 { sim.join(node, node + 1, 1); } originate(&mut sim, 0, 7, 0); assert!(sim.run()); - assert_eq!(sim.route(2, 7).map(|route| route.metric), Some(2), "crossed 1, and 2 makes two"); - assert!(sim.route(3, 7).is_none(), "2's route crossed two relays already"); + assert_eq!( + sim.route(2, 7).map(|route| route.metric), + Some(2), + "the origin, 1, and 2 make three" + ); + assert!(sim.route(3, 7).is_none(), "2's route crossed three nodes already"); assert!(sim.holds(3, 7) && !sim.starved(3, 7)); assert!(!sim.holds(4, 7), "3 has nothing to send on"); } @@ -1101,14 +1135,15 @@ fn longest(sim: &Sim, from: Node, seen: &mut Vec) -> Metric { } /// Random meshes with the origin behind a relay deliver every message and echo in a -/// random order while links flap and relays collect. A route names the relays it -/// crossed, so no relay ever selects one longer than a loop-free path: a node that -/// forgot the origin cannot take back a copy of its own old route. +/// random order while links flap and relays restart and collect. A route names the +/// relays it crossed, so no relay ever selects one longer than a loop-free path: a +/// node that forgot the origin cannot take back a copy of its own old route. Without +/// the hops this finds a count to infinity within a dozen cases. #[test] fn sweep_no_route_outgrows_a_loop_free_path() { let mut rng = XorShift(0x0bad_c0de); - let (mut flaps, mut collected, mut cut) = (0, 0, 0); - for case in 0..400 { + let (mut flaps, mut collected, mut cut, mut restarts) = (0, 0, 0, 0); + for case in 0..200 { let relays = 3 + rng.next(3) as usize; let origin = relays; let mut sim = Sim::new(relays + 1); @@ -1129,10 +1164,11 @@ fn sweep_no_route_outgrows_a_loop_free_path() { links.insert(0, (origin, relay)); } } - let bound = longest(&sim, origin, &mut Vec::new()); + // A restart is a new relay as far as hops go, which a route may cross once more. + let mut bound = longest(&sim, origin, &mut Vec::new()); originate(&mut sim, origin, 7, 0); - let check = |sim: &Sim, step: usize| { + let check = |sim: &Sim, step: usize, bound: Metric| { for node in 0..relays { let metric = sim.route(node, 7).map_or(0, |route| route.metric); assert!( @@ -1164,6 +1200,13 @@ fn sweep_no_route_outgrows_a_loop_free_path() { } } 3 => sim.bump(origin), + 4 if case % 4 == 0 && rng.chance(25) => { + let node = rng.next(relays as u64) as usize; + sim.kill(node); + sim.reconnect(node); + bound += 3 * relays as Metric; + restarts += 1; + } _ => { let (busy, acks) = (sim.busy(), sim.busy_acks()); let pick = rng.next((busy.len() + acks.len()).max(1) as u64) as usize; @@ -1174,13 +1217,13 @@ fn sweep_no_route_outgrows_a_loop_free_path() { } } } - check(&sim, step); + check(&sim, step, bound); } assert!(sim.run(), "case {case} never settles"); - check(&sim, usize::MAX); + check(&sim, usize::MAX, bound); - // Quiet: a relay the origin still reaches routes to it, and every other one - // holds nothing, its distance included. + // Quiet: a relay the origin still reaches routes to it and shows its claim, and + // every other one holds nothing, its distance included. No request is left. let mut reached = vec![origin]; let mut next = 0; while let Some(&at) = reached.get(next) { @@ -1194,13 +1237,24 @@ fn sweep_no_route_outgrows_a_loop_free_path() { cut += usize::from(reached.len() <= relays); for node in 0..relays { match reached.contains(&node) { - true => assert!(sim.route(node, 7).is_some(), "case {case}: node {node} lost its route"), + true => { + assert!(sim.route(node, 7).is_some(), "case {case}: node {node} lost its route"); + assert_eq!(sim.shows(node, 7, ""), Some(true), "case {case}: node {node}"); + } false => { assert!(!sim.holds(node, 7), "case {case}: node {node} holds a dead route"); - assert!(!sim.remembers(node, 7), "case {case}: node {node} keeps a dead distance"); + assert!( + !sim.remembers(node, 7), + "case {case}: node {node} keeps a dead distance" + ); + assert_eq!(sim.shows(node, 7, ""), None, "case {case}: node {node}"); } } } + assert_eq!(sim.retained().pending, 0, "case {case}"); } - assert!(flaps > 0 && collected > 0 && cut > 0, "{flaps} flaps, {collected} collects, {cut} cut"); + assert!( + flaps > 0 && collected > 0 && cut > 0 && restarts > 0, + "{flaps} flaps, {collected} collects, {cut} cut, {restarts} restarts" + ); } diff --git a/rs/moq-net/verify/route/Behind.cfg b/rs/moq-net/verify/route/Behind.cfg new file mode 100644 index 00000000000..5fcb950f9ab --- /dev/null +++ b/rs/moq-net/verify/route/Behind.cfg @@ -0,0 +1,26 @@ +\* The origin (0) behind relay 1, which sits in a triangle with relays 2 and 3. +\* Relay 1 can drop its distance while 2 or 3 still holds a copy of its route, +\* which only the hops refuse once it comes back. +CONSTANTS + Nodes = {0, 1, 2, 3} + Origin = 0 + Leaves = {} + Links = {{0, 1}, {1, 2}, {1, 3}, {2, 3}} + Dear = {} + Claims = {"x"} + MaxRev = 1 + MaxFlaps = 1 + MaxCollects = 0 + +SPECIFICATION Spec + +INVARIANTS + Truthful + AllCertified + NoRevival + NoFalseEnd + NoRegression + LoopFree + SimplePaths + NoCountToInfinity + QuietIsSettled diff --git a/rs/moq-net/verify/route/BehindDear.cfg b/rs/moq-net/verify/route/BehindDear.cfg new file mode 100644 index 00000000000..4c89ba2967a --- /dev/null +++ b/rs/moq-net/verify/route/BehindDear.cfg @@ -0,0 +1,25 @@ +\* Behind.cfg with unequal costs: relay 3 is nearer the origin than relay 2, so +\* 3's copy of relay 1's route is feasible at 2 after 1 ended it. +CONSTANTS + Nodes = {0, 1, 2, 3} + Origin = 0 + Leaves = {} + Links = {{0, 1}, {1, 2}, {1, 3}, {2, 3}} + Dear = {{1, 2}, {2, 3}} + Claims = {"x"} + MaxRev = 1 + MaxFlaps = 1 + MaxCollects = 0 + +SPECIFICATION Spec + +INVARIANTS + Truthful + AllCertified + NoRevival + NoFalseEnd + NoRegression + LoopFree + SimplePaths + NoCountToInfinity + QuietIsSettled diff --git a/rs/moq-net/verify/route/CountToInfinity.cfg b/rs/moq-net/verify/route/CountToInfinity.cfg deleted file mode 100644 index 5995cad17b8..00000000000 --- a/rs/moq-net/verify/route/CountToInfinity.cfg +++ /dev/null @@ -1,20 +0,0 @@ -\* The open count-to-infinity finding, checked apart so RouteHandoff.cfg still -\* checks every other rule. Once it holds, move NoCountToInfinity into -\* RouteHandoff.cfg and delete this file. -CONSTANTS - Nodes = {0, 1, 2} - Origin = 0 - Leaves = {} - Links = {{0, 1}, {0, 2}, {1, 2}} - Claims = {"x"} - MaxRev = 2 - MaxFlaps = 2 - MaxCollects = 1 - -SPECIFICATION Spec - -INVARIANTS - NoCountToInfinity - -CONSTRAINT - Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.cfg b/rs/moq-net/verify/route/RouteHandoff.cfg index d6020df9941..a549143adab 100644 --- a/rs/moq-net/verify/route/RouteHandoff.cfg +++ b/rs/moq-net/verify/route/RouteHandoff.cfg @@ -1,11 +1,11 @@ \* An origin (0) and two relays (1, 2) in a triangle, so a relay can fail \* over through the other and Babel's feasibility decides whether it may. -\* NoCountToInfinity lives in CountToInfinity.cfg while its finding is open. CONSTANTS Nodes = {0, 1, 2} Origin = 0 Leaves = {} Links = {{0, 1}, {0, 2}, {1, 2}} + Dear = {} Claims = {"x"} MaxRev = 2 MaxFlaps = 2 @@ -20,7 +20,6 @@ INVARIANTS NoFalseEnd NoRegression LoopFree + SimplePaths + NoCountToInfinity QuietIsSettled - -CONSTRAINT - Bounded diff --git a/rs/moq-net/verify/route/RouteHandoff.tla b/rs/moq-net/verify/route/RouteHandoff.tla index ccca07819cc..31e8ef0f63a 100644 --- a/rs/moq-net/verify/route/RouteHandoff.tla +++ b/rs/moq-net/verify/route/RouteHandoff.tla @@ -11,10 +11,11 @@ (* own queue. A session opens and closes atomically, dropping what was in *) (* flight. *) (* *) -(* Scope: every node watches the root, links cost 1 with equal priority, *) -(* no scoped grants, no GOAWAY, and the origin keeps its identity. Claims *) -(* are exact paths, and a claim's attributes are the revision that last *) -(* set them, standing in for a fresh Instance per announce. *) +(* Scope: every node watches the root, links have equal priority, no *) +(* scoped grants, no GOAWAY, no hop limit, and the origin keeps its *) +(* identity. Claims are exact paths, and a claim's attributes are the *) +(* revision that last set them, standing in for a fresh Instance per *) +(* announce. *) (***************************************************************************) EXTENDS Integers, Sequences, FiniteSets @@ -23,6 +24,7 @@ CONSTANTS Origin, \* the node that declares the identity Leaves, \* nodes that send only identities they serve (`Sim::leaf`) Links, \* sessions, as 2-element sets of nodes + Dear, \* the links that add 2 to a metric; the rest add 1 (`Link::cost`) Claims, \* claim paths MaxRev, \* the origin's claim changes MaxFlaps, \* session opens and closes @@ -30,6 +32,8 @@ CONSTANTS Relays == Nodes \ {Origin} +Cost == [l \in Links |-> IF l \in Dear THEN 2 ELSE 1] + \* A claim's attributes: the revision that last set it, or None when absent. None == -1 \* A view's floor: a revision, None for no floor, or Absent for no view at all. @@ -39,13 +43,14 @@ NoItems == [c \in Claims |-> None] EmptyView == [floor |-> None, items |-> NoItems] NoView == [floor |-> Absent, items |-> NoItems] -\* `Reach` as sent on a stream: nothing, `Finite(Advert)`, or `Held`. -NoReach == [kind |-> "none", seq |-> 0, met |-> 0] -HeldReach == [kind |-> "held", seq |-> 0, met |-> 0] -Finite(seq, met) == [kind |-> "fin", seq |-> seq, met |-> met] +\* `Reach` as sent on a stream: nothing, `Finite(Advert)`, or `Held`. `hops` is +\* the nodes the route crossed, the origin first and the sender last. +NoReach == [kind |-> "none", seq |-> 0, met |-> 0, hops |-> <<>>] +HeldReach == [kind |-> "held", seq |-> 0, met |-> 0, hops |-> <<>>] +Finite(seq, met, hops) == [kind |-> "fin", seq |-> seq, met |-> met, hops |-> hops] \* `rx` entry, `fd`, `heard`, and `pending` when absent. -NoEntry == [on |-> FALSE, seq |-> 0, met |-> 0, held |-> FALSE] +NoEntry == [on |-> FALSE, seq |-> 0, met |-> 0, held |-> FALSE, hops |-> <<>>] NoFd == [on |-> FALSE, seq |-> 0, met |-> 0] NoHeard == [on |-> FALSE, raw |-> EmptyView, kept |-> NoView, ended |-> FALSE] NoPending == [on |-> FALSE, seq |-> 0, from |-> {}, asked |-> None] @@ -85,31 +90,41 @@ Peers(n, ups) == {m \in Nodes : {n, m} \in ups} Serves(n) == n = Origin \/ n \notin Leaves ----------------------------------------------------------------------------- -(* Route selection on one node's state `s` (mod.rs: `feasible`, `selected`, *) -(* `infeasible`, `recoverable`, `live`, `certifiers`). Every link costs 1. *) +(* Route selection on node `n`'s state `s` (mod.rs: `feasible`, `selected`, *) +(* `infeasible`, `recoverable`, `live`, `certifiers`). *) + +\* `Entry::crossed`: the route's hops name this node. +Crossed(n, e) == \E i \in DOMAIN e.hops : e.hops[i] = n + +Feasible(n, s, e) == + /\ ~Crossed(n, e) + /\ ~s.fd.on \/ e.seq > s.fd.seq \/ (e.seq = s.fd.seq /\ e.met < s.fd.met) -Feasible(s, e) == - ~s.fd.on \/ e.seq > s.fd.seq \/ (e.seq = s.fd.seq /\ e.met < s.fd.met) +UsableSet(n, s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ Feasible(n, s, s.rx[m])} +\* With no distance kept, no route waits on a seqno. +InfeasibleSet(n, s) == + {m \in Nodes : s.fd.on /\ s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(n, s, s.rx[m])} +Certifiers(n, s) == {m \in Nodes : s.rx[m].on /\ Feasible(n, s, s.rx[m])} +Recoverable(n, s) == \E m \in Certifiers(n, s) : s.rx[m].held -UsableSet(s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ Feasible(s, s.rx[m])} -InfeasibleSet(s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(s, s.rx[m])} -Certifiers(s) == {m \in Nodes : s.rx[m].on /\ Feasible(s, s.rx[m])} -Recoverable(s) == \E m \in Certifiers(s) : s.rx[m].held +\* This node's metric through the route `m` sent. +Through(n, s, m) == s.rx[m].met + Cost[{n, m}] \* The lowest metric, then the lowest key: `selected`'s rank with equal priority. -Best(s, S) == +Best(n, s, S) == CHOOSE m \in S : \A k \in S : - s.rx[m].met < s.rx[k].met \/ (s.rx[m].met = s.rx[k].met /\ m <= k) + Through(n, s, m) < Through(n, s, k) \/ (Through(n, s, m) = Through(n, s, k) /\ m <= k) -NoSel == [on |-> FALSE, next |-> None, seq |-> 0, met |-> 0] +NoSel == [on |-> FALSE, next |-> None, seq |-> 0, met |-> 0, hops |-> <<>>] Selected(n, s, ov) == - IF n = Origin THEN [on |-> TRUE, next |-> None, seq |-> ov.seq, met |-> 0] - ELSE IF UsableSet(s) = {} THEN NoSel - ELSE LET m == Best(s, UsableSet(s)) - IN [on |-> TRUE, next |-> m, seq |-> s.rx[m].seq, met |-> s.rx[m].met + 1] + IF n = Origin THEN [on |-> TRUE, next |-> None, seq |-> ov.seq, met |-> 0, hops |-> <>] + ELSE IF UsableSet(n, s) = {} THEN NoSel + ELSE LET m == Best(n, s, UsableSet(n, s)) + IN [on |-> TRUE, next |-> m, seq |-> s.rx[m].seq, met |-> Through(n, s, m), + hops |-> Append(s.rx[m].hops, n)] Live(n, s) == - n = Origin \/ UsableSet(s) # {} \/ InfeasibleSet(s) # {} \/ Recoverable(s) + n = Origin \/ UsableSet(n, s) # {} \/ InfeasibleSet(n, s) # {} \/ Recoverable(n, s) \* `Heard::view`: what it certified before its route ended, else the raw view. HeardView(h) == IF h.kept.floor # Absent THEN h.kept ELSE h.raw @@ -117,9 +132,9 @@ HeardView(h) == IF h.kept.floor # Absent THEN h.kept ELSE h.raw \* `certified(id, held)` at the root interest: `ok` is FALSE where the code \* returns None (no route, or a certifier has not answered), and `root` says \* whether any counted certifier's view has a floor over the root. -Certified(s, held) == - [ok |-> (\E m \in Nodes : s.rx[m].on) /\ \A m \in Certifiers(s) : s.heard[m].on, - root |-> \E m \in Certifiers(s) : +Certified(n, s, held) == + [ok |-> (\E m \in Nodes : s.rx[m].on) /\ \A m \in Certifiers(n, s) : s.heard[m].on, + root |-> \E m \in Certifiers(n, s) : (held \/ ~s.rx[m].held) /\ HeardView(s.heard[m]).floor >= 0] \* The view the node shows and forwards (`adopted`). Only certified claims @@ -142,7 +157,7 @@ HasItems(v) == \E c \in Claims : v.items[c] # None \* `prune` at the root interest: once no certifier's view has a floor, the \* merged view is let go and rebuilt empty. Prune(n, s, ov) == - LET c == Certified(s, TRUE) IN + LET c == Certified(n, s, TRUE) IN IF n # Origin /\ Selected(n, s, ov).on /\ c.ok /\ s.view.floor >= 0 /\ ~c.root THEN [s EXCEPT !.view = EmptyView] ELSE s @@ -150,7 +165,7 @@ Prune(n, s, ov) == \* What `advertise` decides for one peer. Plan(n, s, m, sel, live, av, ov) == LET was == s.sent[m] - reach0 == IF sel.on /\ Serves(n) THEN Finite(sel.seq, sel.met) + reach0 == IF sel.on /\ Serves(n) THEN Finite(sel.seq, sel.met, sel.hops) ELSE IF ~sel.on /\ Serves(n) /\ live /\ was.kind # "none" THEN HeldReach ELSE NoReach \* A route starts again only once its last end was echoed. @@ -183,7 +198,7 @@ Record(n, s, sel, av, ups) == Requests(n, s, sel) == IF n = Origin THEN [pending |-> NoPending, to |-> None, seq |-> 0] ELSE - LET starved == ~sel.on /\ InfeasibleSet(s) # {} + LET starved == ~sel.on /\ InfeasibleSet(n, s) # {} want == s.fd.seq + 1 p0 == s.pending p1 == IF ~starved THEN p0 @@ -191,8 +206,8 @@ Requests(n, s, sel) == ELSE IF p0.seq < want THEN [p0 EXCEPT !.seq = want, !.asked = None] ELSE p0 answered == sel.on /\ sel.seq >= p1.seq - hasTarget == sel.on \/ InfeasibleSet(s) # {} - target == IF sel.on THEN sel.next ELSE Best(s, InfeasibleSet(s)) + hasTarget == sel.on \/ InfeasibleSet(n, s) # {} + target == IF sel.on THEN sel.next ELSE Best(n, s, InfeasibleSet(n, s)) IN IF ~p1.on THEN [pending |-> p1, to |-> None, seq |-> 0] ELSE IF answered \/ (p1.from = {} /\ ~starved) \/ ~hasTarget THEN [pending |-> NoPending, to |-> None, seq |-> 0] @@ -202,7 +217,7 @@ Requests(n, s, sel) == \* `shown_now`: how the reader sees each claim. ShownNow(n, s, sel, live, ov) == - LET serving == Certified(s, FALSE) + LET serving == Certified(n, s, FALSE) avail == sel.on /\ (n = Origin \/ ~serving.ok \/ serving.root) v == Adopted(n, s, ov) IN [c \in Claims |-> @@ -211,7 +226,7 @@ ShownNow(n, s, sel, live, ov) == \* `show`: the reader's events, as changes to `ended` and the counters. \* A claim leaving while live and certified is an END, else it went offline. Events(n, s, old, now, live, ov, eb) == - LET c0 == Certified(s, TRUE) + LET c0 == Certified(n, s, TRUE) uncertified == (c0.ok /\ ~c0.root) \/ (n # Origin /\ s.view.floor < 0) isEnd(c) == old[c].item # None /\ now[c].item = None /\ live /\ ~uncertified isStart(c) == old[c].item = None /\ now[c].item # None @@ -329,8 +344,8 @@ Certify(v) == IF v.floor >= 0 THEN v ELSE [floor |-> v.floor, items |-> NoItems] OnRoute(s, from, reach) == LET h == s.heard[from] rx1 == CASE reach.kind = "fin" -> - [s.rx EXCEPT ![from] = [on |-> TRUE, seq |-> reach.seq, - met |-> reach.met, held |-> FALSE]] + [s.rx EXCEPT ![from] = [on |-> TRUE, seq |-> reach.seq, met |-> reach.met, + held |-> FALSE, hops |-> reach.hops]] [] reach.kind = "held" -> IF s.rx[from].on THEN [s.rx EXCEPT ![from].held = TRUE] ELSE s.rx [] OTHER -> [s.rx EXCEPT ![from] = NoEntry] @@ -504,18 +519,40 @@ Hop(n, k) == IF k = 0 THEN n ELSE Hop(NextHop(n), k - 1) \* Following selected next hops from any relay never cycles. LoopFree == \A n \in Relays : Hop(n, Cardinality(Nodes)) \notin Relays -\* Every link costs 1, so a loop-free path to the origin has at most this metric. -Longest == Cardinality(Nodes) - 1 +\* The loop-free paths from the origin over the configured links, each as the +\* nodes it crosses in order, and what each costs its last node. +RECURSIVE Extend(_, _) +Extend(P, k) == + IF k = 0 THEN P + ELSE Extend(P \cup {Append(p, n) : p \in P, n \in Relays}, k - 1) +Last(p) == p[Len(p)] +RECURSIVE Along(_) +Along(p) == + IF Len(p) = 1 THEN 0 + ELSE LET before == SubSeq(p, 1, Len(p) - 1) + IN Along(before) + Cost[{Last(before), Last(p)}] +Paths == + {p \in Extend({<>}, Cardinality(Relays)) : + /\ \A i, j \in DOMAIN p : i # j => p[i] # p[j] + /\ \A i \in DOMAIN p : i > 1 => {p[i - 1], p[i]} \in Links} + +\* A route's hops are a loop-free path from the origin to its sender, and its +\* metric is that path's cost. Every route sent adds its sender to hops that did +\* not name it, so this holds of every route held or in flight, whatever any +\* node forgot. +IsPath(from, r) == r.hops \in Paths /\ Last(r.hops) = from /\ r.met = Along(r.hops) +SimplePaths == + /\ \A n, m \in Nodes : st[n].rx[m].on => IsPath(m, st[n].rx[m]) + /\ \A d \in Dirs : \A i \in DOMAIN q[d] : + q[d][i].type = "route" /\ q[d][i].reach.kind = "fin" => IsPath(d[1], q[d][i].reach) \* No relay selects a route longer than any loop-free path: a longer one is a -\* stale route counting up as it bounces between relays (Babel's feasibility -\* condition exists to rule this out). +\* stale route counting up as it bounces between relays. It follows from +\* SimplePaths, since no node selects a route that crossed it. +Longest == LET costs == {Along(p) : p \in Paths} + IN CHOOSE c \in costs : \A k \in costs : k <= c NoCountToInfinity == \A n \in Relays : Selected(n, st[n], OV).met <= Longest -\* Explore one step past NoCountToInfinity and no further, so a count to -\* infinity is reported rather than explored forever. -Bounded == \A n, m \in Nodes : st[n].rx[m].met <= Longest - \* Nodes the origin reaches over open sessions, through nodes that forward. RECURSIVE Grow(_, _) Grow(R, k) == IF k = 0 THEN R diff --git a/rs/moq-net/verify/route/RouteHandoff.view.ts b/rs/moq-net/verify/route/RouteHandoff.view.ts index e02b18361bc..fe1b07be528 100644 --- a/rs/moq-net/verify/route/RouteHandoff.view.ts +++ b/rs/moq-net/verify/route/RouteHandoff.view.ts @@ -1,13 +1,14 @@ // Labels for `/statechart` on RouteHandoff.tla: each relay's route and what its // reader shows, and each step as the message that arrives. -type Entry = { on: boolean; seq: number; met: number; held: boolean }; +// A sequence such as `hops` is keyed from 1. +type Entry = { on: boolean; seq: number; met: number; held: boolean; hops: Record }; type Node = { rx: Record; fd: { on: boolean; seq: number; met: number }; shown: Record; }; -type Msg = { type: string; reach: { kind: string; seq: number; met: number } }; +type Msg = { type: string; reach: { kind: string; seq: number; met: number; hops: Record } }; type Vars = { st: Record; q: Record>; @@ -19,20 +20,26 @@ type Vars = { const ORIGIN = "0"; const name = (n: string | number) => (String(n) === ORIGIN ? "the origin" : `relay ${n}`); -const feasible = (s: Node, e: Entry) => !s.fd.on || e.seq > s.fd.seq || (e.seq === s.fd.seq && e.met < s.fd.met); +const hops = (e: { hops: Record }) => Object.keys(e.hops).length; -// `selected`: the usable feasible route with the lowest metric, then key. -const selected = (s: Node) => { - let best: [string, number] | null = null; +// Never a route that crossed node `n`, then Babel's condition. +const feasible = (n: string, s: Node, e: Entry) => + !Object.values(e.hops).some((hop) => String(hop) === n) && + (!s.fd.on || e.seq > s.fd.seq || (e.seq === s.fd.seq && e.met < s.fd.met)); + +// `selected` where every link costs the same: the usable feasible route with the +// lowest metric, then key, and the hops to the origin through it. +const selected = (n: string, s: Node) => { + let best: [string, number, number] | null = null; for (const [m, e] of Object.entries(s.rx)) { - if (!e.on || e.held || !feasible(s, e)) continue; - if (best === null || e.met + 1 < best[1]) best = [m, e.met + 1]; + if (!e.on || e.held || !feasible(n, s, e)) continue; + if (best === null || e.met < best[2]) best = [m, hops(e), e.met]; } return best; }; -const relay = (s: Node) => { - const route = selected(s); +const relay = (n: string, s: Node) => { + const route = selected(n, s); const shows = Object.values(s.shown).some((x) => x.item >= 0); const held = Object.values(s.rx).some((e) => e.on); const how = route @@ -54,8 +61,8 @@ export const title = "One origin identity across a triangle of relays"; export const state = (v: Vars) => ({ Sessions: sessions(v), - "Relay 1": relay(v.st["1"]), - "Relay 2": relay(v.st["2"]), + "Relay 1": relay("1", v.st["1"]), + "Relay 2": relay("2", v.st["2"]), }); const len = (s: Record | undefined) => (s ? Object.keys(s).length : 0); @@ -100,7 +107,7 @@ export const step = (action: string, from: Vars, to: Vars) => { ? "hold" : String(m) === ORIGIN ? "route" - : `route (${msg.reach.met} hop${msg.reach.met === 1 ? "" : "s"})`; + : `route (${hops(msg.reach) - 1} hop${hops(msg.reach) === 2 ? "" : "s"})`; return `${name(m)}'s ${what} reaches ${name(n)}`; } default: From 0f66e70ec26f1de2f8e781c7cfcb635d30b86377 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 03:32:33 -0800 Subject: [PATCH 06/17] refactor(net): advertise compares a route against what was sent without cloning it Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 4 ++-- rs/moq-net/src/route/mod.rs | 23 ++++++++++++----------- rs/moq-net/src/route/node.rs | 2 +- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index d4723f21f13..f6da8adad03 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -35,7 +35,7 @@ just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/rout | Config | Mesh | Bounds | Distinct states | | --- | --- | --- | --- | -| `RouteHandoff.cfg` | The origin and two relays in a triangle. | 2 claim changes, 2 session changes, 1 collection | TRIANGLE | +| `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,462,496 | @@ -54,7 +54,7 @@ A counterexample is a path through the model, not yet a bug. Replay it on the ro ## 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 every config, and move the sync commit forward only once the model describes the code at the new commit. +Sync commit: `f7b47f1eed201b1f5339beb3073f06cbd5f1bc6e`. Run `git log f7b47f1eed.. -- 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 | | --- | --- | diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index 059eedf2c16..118c2eec251 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -1218,9 +1218,10 @@ impl Router { entry.advert.metric.checked_add(self.neighbors[&next].link.cost) } - /// The usable but infeasible routes for `id`, with their metrics: the ones a newer - /// seqno would lift past this node's distance. With no distance kept there are - /// none, since the only routes refused then are its own, come back. + /// The usable but infeasible routes for `id`, with their metrics: while it has + /// one, this node holds the identity and asks for a newer seqno. With no distance + /// kept there are none, since the only routes refused then are its own, come back, + /// which no seqno makes feasible. fn infeasible(&self, id: Id) -> impl Iterator + '_ { let kept = self.fd.contains_key(&id); (self.rx.get(&id).into_iter().flatten()) @@ -1654,8 +1655,8 @@ impl Router { for &to in peers { let peer = &self.neighbors[&to]; let serves = self.serves(peer, id); - let was = self.sent.get(&(id, to)).cloned(); - if !serves && was.is_none() { + let started = self.sent.contains_key(&(id, to)); + if !serves && !started { continue; } let reach = match selected { @@ -1665,12 +1666,12 @@ impl Router { down_only: route.down_only, hops: hops.clone(), })), - None if serves && ctx.live && was.is_some() => Some(Reach::Held), + None if serves && ctx.live && started => Some(Reach::Held), _ => None, }; // A route starts again only once the neighbor echoed its last end there, so // one that withholds echoes holds at most one end per identity. - let reach = reach.filter(|_| was.is_some() || !self.unacked.contains_key(&(id, to))); + let reach = reach.filter(|_| started || !self.unacked.contains_key(&(id, to))); let watch = peer.watch.as_ref().expect("a watching peer"); let sent = self.sent_views.get(&(id, to)); let (changes, meets) = match (&reach, sent) { @@ -1725,16 +1726,16 @@ impl Router { check.apply(changes.clone(), floors.clone()); assert_eq!(check, adopted.present(watch), "incremental presentation to {to:?}"); } - plans.push((to, was, reach, meets, changes, floors, watch.clone())); + plans.push((to, started, reach, meets, changes, floors, watch.clone())); } - for (to, was, reach, meets, changes, floors, watch) in plans { + for (to, started, reach, meets, changes, floors, watch) in plans { let key = (id, to); - let (reaching, started) = (reach.is_some(), was.is_some()); + let reaching = reach.is_some(); let send = reach.filter(|_| meets); let sending = send.is_some(); if let Some(send) = send - && was.as_ref() != Some(&send) + && self.sent.get(&key) != Some(&send) { self.sent.insert(key, send.clone()); self.out.push(Out::Route { diff --git a/rs/moq-net/src/route/node.rs b/rs/moq-net/src/route/node.rs index c4585f0e917..4fd31d708ed 100644 --- a/rs/moq-net/src/route/node.rs +++ b/rs/moq-net/src/route/node.rs @@ -422,7 +422,7 @@ impl Node { /// A node declaring the origin's hop id, so the origin has one identity on every /// wire. A declared identity is never qualified, so an id carrying that marker /// loses it, or is replaced by a random one if nothing is left. It uses no route - /// that crossed `max_hops` relays, which it could not add itself to. + /// that crossed `max_hops` nodes, which it could not add itself to. pub fn origin(hop: std::num::NonZeroU64, max_hops: std::num::NonZeroUsize) -> Self { let mut rng = kio::clock::rng(); let id = declared_for(hop).unwrap_or_else(|| rng.random_range(1..=GENERATED)); From c07c64d774d70a2129f0a100eda32a89f985040f Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 03:32:42 -0800 Subject: [PATCH 07/17] docs(skill): verify-route syncs to the hops commit Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index f6da8adad03..a1732a2fef2 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -54,7 +54,7 @@ A counterexample is a path through the model, not yet a bug. Replay it on the ro ## Coverage -Sync commit: `f7b47f1eed201b1f5339beb3073f06cbd5f1bc6e`. Run `git log f7b47f1eed.. -- 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. +Sync commit: `0f66e70ec26f1de2f8e781c7cfcb635d30b86377`. Run `git log 0f66e70ec2.. -- 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 | | --- | --- | From a4ad41faf7ea9402f7ea3d4a582efc21c752e805 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 03:33:04 -0800 Subject: [PATCH 08/17] docs(skill): verify-route names a sync commit that main holds Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index a1732a2fef2..097d99fd118 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -54,7 +54,7 @@ A counterexample is a path through the model, not yet a bug. Replay it on the ro ## Coverage -Sync commit: `0f66e70ec26f1de2f8e781c7cfcb635d30b86377`. Run `git log 0f66e70ec2.. -- 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. +Sync commit: `52fa6b2f0ece29c44bfa2459ec93fc54b4b48221`, plus the change that added a route's hops ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)). Run `git log 52fa6b2f0e.. -- 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 | | --- | --- | From 5509169265c8d428d86078c18c79c2c20481d81c Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 06:27:40 -0800 Subject: [PATCH 09/17] fix(net): a crossed route is never selected, and is waited on only while it extends what this node sent An independent review found that counting every crossed route as infeasible left a relay starved for good on a copy of its own route that a scoped peer handed back under a qualified key, and made it ask the origin for a seqno that could not help. Babel's feasibility condition is as it was. A node never selects or certifies through a route that crossed it, and counts one among its infeasible routes only while its hops extend those of the route the node last sent for that identity: its sender then routes through the node and moves once the node lets go. The hop limit is the wire's 32 alone, since a lower one hides a shorter path behind a cheaper long one and lite-07 has no path hunting to cut off. prune takes back the view of a certifier that returns. A relay let go of what only that neighbour certified while its route was infeasible, and kept nothing of it once the neighbour certified again, since merging happened only when a batch arrived. A change of hops alone reached that window. Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- drafts/draft-lcurley-moq-lite.md | 13 ++-- rs/moq-net/src/model/origin.rs | 2 +- rs/moq-net/src/route/mod.rs | 76 ++++++++++++++------- rs/moq-net/src/route/node.rs | 9 +-- rs/moq-net/src/route/tests/handoff.rs | 41 ++++++++++++ rs/moq-net/src/route/tests/routing.rs | 84 ++++++++++++++++++++---- rs/moq-net/verify/route/RouteHandoff.tla | 28 +++++--- 8 files changed, 195 insertions(+), 60 deletions(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index 097d99fd118..f96a956fc77 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -58,7 +58,7 @@ Sync commit: `52fa6b2f0ece29c44bfa2459ec93fc54b4b48221`, plus the change that ad | Code (`rs/moq-net/src/route/`) | Model | | --- | --- | -| `mod.rs` `feasible`, `Entry::crossed`, `through`, `selected`, `infeasible`, `recoverable`, `live`, `certifiers` | `Feasible`, `Crossed`, `Through`, `Selected`, `InfeasibleSet`, `Recoverable`, `Live`, `Certifiers` | +| `mod.rs` `feasible`, `Entry::crossed`, `eligible`, `through`, `selected`, `infeasible`, `advertised`, `recoverable`, `live`, `certifiers` | `Feasible`, `Crossed`, `Eligible`, `Through`, `Selected`, `InfeasibleSet`, `adv` and `Extends`, `Recoverable`, `Live`, `Certifiers` | | `mod.rs` `certified`, `prune`, `adopted` | `Certified`, `Prune`, `Adopted` | | `mod.rs` `update`, `record`, `advertise`, `requests` | `Update`, `Record`, `Plan`, `Requests` | | `mod.rs` `show`, `shown_now` | `Events`, `ShownNow` | diff --git a/drafts/draft-lcurley-moq-lite.md b/drafts/draft-lcurley-moq-lite.md index ce21b0162ed..814649e62eb 100644 --- a/drafts/draft-lcurley-moq-lite.md +++ b/drafts/draft-lcurley-moq-lite.md @@ -499,10 +499,11 @@ A relay forwards the other entries unchanged and never qualifies them. A route that arrives with 32 Hops is unusable. A node keeps a feasibility distance per Node ID: the highest Seqno of any route it advertised, and the lowest metric it advertised at that Seqno, as in [RFC8966] Section 3.5.1. -A route whose Hops name the receiver is never feasible there: it is a copy of a route the receiver sent. -Any other route is feasible when no feasibility distance is kept for its Node ID yet, when its Seqno is greater than the distance's, or when its Seqno is equal and its advertised Metric is lower. +A route is feasible when no feasibility distance is kept for its Node ID yet, when its Seqno is greater than the distance's, or when its Seqno is equal and its advertised Metric is lower. A node selects, per Node ID, among its feasible routes that are not held: a session that has not received a GOAWAY, then the highest local priority, then the lowest metric. It MUST NOT select an infeasible route, and a distance only ever falls within a Seqno, so advertising a longer route never raises it. +It MUST NOT select a route whose Hops name it either, feasible or not: that is a copy of a route the node sent, which no distance refuses once the node dropped it. +Such a route counts among the node's routes below only while it is infeasible and its Hops begin with those of the route the node last sent to that origin node: its sender then routes through the node, and moves once it hears the node has no route. A node MAY mark a session upstream. A route is down-only when it arrived on an upstream session or with its Down Only bit set; a node sends a down-only route with the bit set, and never on an upstream session. @@ -511,19 +512,19 @@ A node that does not forward, such as a client, sends only its own route, and ho An origin advances its Seqno whenever its own set of sessions changes. It never advertises a Seqno or Revision of 2^64-1: a change that would reach it instead rotates its Node ID, ending the old route everywhere and announcing its claims again under the new one. -A node with no usable route to an origin node holds it while it can still recover: while it keeps a feasibility distance for the node and a route it has to the node is infeasible, or a peer holds a route whose last advertisement is feasible here. +A node with no usable route to an origin node holds it while it can still recover: while every route it has to the node is infeasible, or a peer holds a route whose last advertisement is feasible here. A held route travels as a ROUTE_HOLD, and its claims stay shown but unavailable until a ROUTE_UPDATE makes it usable again. Otherwise the node lets go, sending ROUTE_END wherever it advertised the route, and its claims go offline. Neither proves that the origin withdrew its claims. -A node that keeps a feasibility distance for an origin node, and whose routes to it are all infeasible, sends a ROUTE_REQUEST with its distance's Seqno plus 1 to the peer whose route it would select were it feasible. +A node whose routes to an origin node are all infeasible sends a ROUTE_REQUEST with its distance's Seqno plus 1 to the peer whose route it would select were it feasible. A node holding a selected route at least that new answers by advertising it, and the origin answers by raising its Seqno to at least the requested one; a request for 2^64-1 rotates the origin's Node ID. Any other node forwards the request to the peer whose route it would select, even the requester. Every node keeps one pending request per origin node, its own or forwarded, at the highest Seqno requested, dropping requests no newer, until it selects a route at least that new or has no route left, and sends it again whenever its Seqno rises or that peer changes. The receiver of a ROUTE_END echoes it back on the same stream once it dropped the route. A node drops a feasibility distance once no peer's route to the node is left open, it advertises none, and every ROUTE_END it sent for it was echoed; a closed session counts as an echo. -No peer then routes through the node, and its Hops refuse any copy of its own route that still returns. +No peer then routes through the node, and the Hops refuse any copy of its own route that still returns. A SUBSCRIBE, FETCH, TRACK, TRACKS, or DATAGRAMS request names the origin node that serves it. A subscriber that names 0 lets the publisher select one (see [Resolution](#resolution)), and a relay forwarding a request names the origin node it selected or was given. @@ -2249,7 +2250,7 @@ The `Message Length` describes the payload size on the wire. - A receiver mints an Instance for each announcement a session of an earlier version delivers, and a `Minted` field beside every Instance (ANNOUNCE_START, ANNOUNCE_RESTART, TRACK, TRACKS, SUBSCRIBE, FETCH, and DATAGRAMS) says whether a receiver minted it, so no Instance text is reserved for minting. - Added announce compression: ANNOUNCE_START gains `Path Base` and `Path Keep` to copy the head of a live claim's suffix. - Split routing into two layers on the Announce Stream. ROUTE_START (0x6), ROUTE_UPDATE (0x7), and ROUTE_END (0x8) advertise how the publisher reaches an origin node, named by a Node ID, with a seqno, an additive metric, and a down-only bit, and loops are prevented by Babel's feasibility condition. Every ANNOUNCE_START names its route's Route ID in place of the Hop ID list, so a link change sends one ROUTE_UPDATE per origin rather than an update per claim. Removed the Hop ID list and ANNOUNCE_OK's Hop ID, and replaced the SETUP Hop parameter (0x5) with a [Node ID parameter](#node-id-parameter), so an endpoint that reaches itself detects it at setup. -- Added Hops to ROUTE_START and ROUTE_UPDATE: the Hop ID of every node the route crossed, at most 32. A route whose Hops name the receiver is never feasible there, so a node that dropped its feasibility distance cannot take back a copy of its own route. +- Added Hops to ROUTE_START and ROUTE_UPDATE: the Hop ID of every node the route crossed, at most 32. A node never selects a route whose Hops name it, so one that dropped its feasibility distance cannot take back a copy of its own route. - Added ROUTE_HOLD (0xB), which holds a route while it recovers; ROUTE_END lets it go. Neither withdraws the origin's claims, and the subscriber echoes every ROUTE_END back. - Added ROUTE_REQUEST (0xA), sent by the subscriber on the Announce Stream to ask for a route with a newer seqno when every route it has is infeasible. - Added ANNOUNCE_FLOOR (0x9), closing each batch of a route's claims with the origin Revision at which the stream's claims across the requested prefix are certified plus one, or 0 to certify nothing, so a stale copy never revives a claim whose withdrawal a newer one delivered. A floor certifies only the claims its own request shows. diff --git a/rs/moq-net/src/model/origin.rs b/rs/moq-net/src/model/origin.rs index d70fcf982a6..28ae3089b40 100644 --- a/rs/moq-net/src/model/origin.rs +++ b/rs/moq-net/src/model/origin.rs @@ -7357,7 +7357,7 @@ impl Consumer { timers: self.timers.clone(), }; // Built before taking the lock, since opening a cursor takes it. - let node = crate::route::Node::origin(self.hop(), self.max_hops); + let node = crate::route::Node::origin(self.hop()); let claims = OwnClaims { routes: own(false).routes(), downstream: own(true).routes(), diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index 118c2eec251..b3f5e251570 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -251,8 +251,8 @@ struct Entry { /// The last finite advertisement. advert: Advert, held: bool, - /// Its hops name this node: a copy of a route this node sent, come back. It is - /// never feasible, which the distance alone cannot say once this node forgot it. + /// Its hops name this node: a copy of a route this node sent, come back. This + /// node never uses it, which the distance alone cannot ensure once it is gone. crossed: bool, } @@ -400,8 +400,6 @@ pub(crate) struct Router { /// How this node names itself in the hops of a route it forwards. A rotation /// leaves it alone, so a route that crossed this node always says so. hop: Id, - /// The most nodes a route this node uses may cross, its origin and this node included. - pub max_hops: usize, neighbors: BTreeMap, origins: BTreeMap>, rx: BTreeMap>, @@ -411,6 +409,9 @@ pub(crate) struct Router { filed: BTreeMap<(Id, N), Id>, /// Babel's feasibility distance per identity. fd: BTreeMap, + /// The hops of the route this node last sent for an identity, kept as long as its + /// distance: a route that extends them came through this node's own. + advertised: BTreeMap>, sent: BTreeMap<(Id, N), Reach>, /// ROUTE_ENDs sent to each neighbor and not yet echoed back. Until they all /// return, a neighbor may still hold this node's advertisement, so the @@ -466,12 +467,12 @@ impl Router { pub fn new(hop: Id, seed: u64) -> Self { Self { hop, - max_hops: MAX_HOPS, neighbors: BTreeMap::new(), origins: BTreeMap::new(), rx: BTreeMap::new(), filed: BTreeMap::new(), fd: BTreeMap::new(), + advertised: BTreeMap::new(), sent: BTreeMap::new(), unacked: BTreeMap::new(), pending: BTreeMap::new(), @@ -1033,7 +1034,7 @@ impl Router { type Rank = (bool, Reverse, Metric, N); let mut best: Option<(Rank, Selected)> = None; for (&next, entry) in self.rx.get(&id)? { - if entry.held || !self.feasible(id, entry) { + if entry.held || !self.eligible(id, entry) { continue; } let peer = &self.neighbors[&next]; @@ -1062,7 +1063,7 @@ impl Router { return Vec::new(); } (self.rx.get(&id).into_iter().flatten()) - .filter(|(_, entry)| !entry.held && self.feasible(id, entry)) + .filter(|(_, entry)| !entry.held && self.eligible(id, entry)) .filter_map(|(&next, entry)| Some((next, self.through(next, entry)?))) .collect() } @@ -1197,35 +1198,41 @@ impl Router { self.filed.get(&(id, next)).copied().unwrap_or(id) } - /// Babel's feasibility condition against this node's feasibility distance, and - /// never a route that crossed this node. - fn feasible(&self, id: Id, entry: &Entry) -> bool { - let advert = &entry.advert; - !entry.crossed - && match self.fd.get(&id) { - None => true, - Some(&(seqno, metric)) => advert.seqno > seqno || (advert.seqno == seqno && advert.metric < metric), - } + /// Babel's feasibility condition against this node's feasibility distance. + fn feasible(&self, id: Id, advert: &Advert) -> bool { + match self.fd.get(&id) { + None => true, + Some(&(seqno, metric)) => advert.seqno > seqno || (advert.seqno == seqno && advert.metric < metric), + } + } + + /// Whether this node may select or certify through `entry`: a feasible route that + /// did not cross it. One that crossed it and is feasible all the same is no route + /// at all, since no seqno would change where it has been. + fn eligible(&self, id: Id, entry: &Entry) -> bool { + !entry.crossed && self.feasible(id, &entry.advert) } /// This node's metric through `entry`, the route `next` sent, or `None` when it is /// unreachable, never saturated: the metric overflows, or the route already /// crossed as many nodes as one may. fn through(&self, next: N, entry: &Entry) -> Option { - if entry.advert.hops.len() >= self.max_hops { + if entry.advert.hops.len() >= MAX_HOPS { return None; } entry.advert.metric.checked_add(self.neighbors[&next].link.cost) } - /// The usable but infeasible routes for `id`, with their metrics: while it has - /// one, this node holds the identity and asks for a newer seqno. With no distance - /// kept there are none, since the only routes refused then are its own, come back, - /// which no seqno makes feasible. + /// The usable but infeasible routes for `id`, with their metrics: this node holds + /// the identity while it has one. A route that crossed this node counts only if it + /// extends the route this node last sent, since its sender then routes through this + /// node and moves once it hears this node has none. Any other one that crossed it + /// stays as it is whatever this node does, and waiting on it would never end. fn infeasible(&self, id: Id) -> impl Iterator + '_ { - let kept = self.fd.contains_key(&id); + let sent = self.advertised.get(&id); (self.rx.get(&id).into_iter().flatten()) - .filter(move |(_, entry)| kept && !entry.held && !self.feasible(id, entry)) + .filter(move |(_, entry)| !entry.held && !self.feasible(id, &entry.advert)) + .filter(move |(_, entry)| !entry.crossed || sent.is_some_and(|sent| entry.advert.hops.starts_with(sent))) .filter_map(move |(&next, entry)| Some((self.through(next, entry)?, next))) } @@ -1272,7 +1279,7 @@ impl Router { /// Whether `entry`'s last finite advertisement from `next` is feasible here /// and reachable across the link, as selection requires of a usable route. fn reachable(&self, id: Id, next: N, entry: &Entry) -> bool { - self.feasible(id, entry) && self.through(next, entry).is_some() + self.eligible(id, entry) && self.through(next, entry).is_some() } /// The regions of `id` that this node's certifiers certify, those whose @@ -1303,6 +1310,23 @@ impl Router { let Some(regions) = self.certified(id, true) else { return; }; + // A certifier whose view the merged one lags was not one when its regions were + // let go below, and sends nothing more now it certifies again: take its view back. + let merged = self.views.get(&id); + let lags = |view: &View| { + (view.floors.iter()).any(|(region, &rev)| merged.and_then(|merged| merged.as_of(region)) < Some(rev)) + }; + let back: Vec = (self.certifiers(id).into_iter()) + .filter(|next| lags(self.heard[&(id, *next)].view())) + .collect(); + if !back.is_empty() { + let merged = self.views.entry(id).or_default(); + for next in back { + merged.merge(self.heard[&(id, next)].view()); + } + self.resync(id); + self.mark_all(id); + } let Some(merged) = self.views.get(&id) else { return; }; @@ -1496,6 +1520,7 @@ impl Router { && Self::of(&self.unacked, id).next().is_none() { self.fd.remove(&id); + self.advertised.remove(&id); } self.requests(id); self.show(id, &ctx, &dirty); @@ -1737,6 +1762,9 @@ impl Router { if let Some(send) = send && self.sent.get(&key) != Some(&send) { + if let Reach::Finite(advert) = &send { + self.advertised.insert(id, advert.hops.clone()); + } self.sent.insert(key, send.clone()); self.out.push(Out::Route { to, diff --git a/rs/moq-net/src/route/node.rs b/rs/moq-net/src/route/node.rs index 4fd31d708ed..0280a251a70 100644 --- a/rs/moq-net/src/route/node.rs +++ b/rs/moq-net/src/route/node.rs @@ -421,14 +421,11 @@ impl Node { /// A node declaring the origin's hop id, so the origin has one identity on every /// wire. A declared identity is never qualified, so an id carrying that marker - /// loses it, or is replaced by a random one if nothing is left. It uses no route - /// that crossed `max_hops` nodes, which it could not add itself to. - pub fn origin(hop: std::num::NonZeroU64, max_hops: std::num::NonZeroUsize) -> Self { + /// loses it, or is replaced by a random one if nothing is left. + pub fn origin(hop: std::num::NonZeroU64) -> Self { let mut rng = kio::clock::rng(); let id = declared_for(hop).unwrap_or_else(|| rng.random_range(1..=GENERATED)); - let node = Self::new(id, rng.random()); - node.lock().router.max_hops = max_hops.get(); - node + Self::new(id, rng.random()) } fn lock(&self) -> Locked<'_> { diff --git a/rs/moq-net/src/route/tests/handoff.rs b/rs/moq-net/src/route/tests/handoff.rs index f76629eeadc..946428c3f35 100644 --- a/rs/moq-net/src/route/tests/handoff.rs +++ b/rs/moq-net/src/route/tests/handoff.rs @@ -1439,3 +1439,44 @@ fn a_restarted_floorless_route_drops_what_it_no_longer_carries() { assert_eq!(revivals(&sim.events), 0); sim.check().unwrap(); } + +/// Relay 4 hears origin 7's claims from relay 0, which certifies them all, and from +/// relay 3, which asked only for `b`. While 0's route is infeasible for a moment, 3 +/// is the only certifier, and 4 lets go of what 3 does not certify. Once 0 certifies +/// again, 4 takes back what 0 still carries, though 0 sends nothing more. +#[test] +fn a_certifier_that_returns_brings_back_what_it_certifies() { + let (origin, other) = (6, 7); + let mut sim = Sim::new(8); + sim.join(other, 4, 1); + sim.join(other, 5, 1); + sim.join(origin, 3, 1); + sim.join(origin, 2, 1); + sim.join(0, 1, 1); + sim.link(0, 2, SimLink::cost(3), SimLink::cost(1)); + sim.join(0, 3, 1); + sim.join(0, 4, 1); + sim.link(1, 2, SimLink::cost(2), SimLink::cost(1)); + sim.join(2, 3, 1); + sim.join(2, 5, 1); + sim.link(3, 4, SimLink::cost(1), SimLink::cost(2)); + sim.originate(origin, 7, 0); + sim.announce(origin, "", 0, None); + sim.originate(other, 8, 0); + sim.announce(other, "", 0, None); + sim.watch(3, "b"); + assert!(sim.run()); + assert_eq!(sim.shows(4, 7, ""), Some(true)); + + let before = sim.events.len(); + sim.disconnect(origin, 3); + assert!(sim.run()); + let let_go = (sim.events[before..].iter()).any(|event| (event.node, event.id, event.kind) == (4, 7, Kind::Offline)); + assert!(let_go, "relay 4 let the claim go while only relay 3 certified"); + assert_eq!(sim.shows(4, 7, ""), Some(true), "and took it back from relay 0"); + sim.disconnect(2, 3); + assert!(sim.run()); + assert_eq!(sim.shows(4, 7, ""), Some(true)); + assert_eq!(false_ends(&sim.events), 0); + sim.check().unwrap(); +} diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index c28687e4829..87c908a43ff 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -978,7 +978,7 @@ fn a_route_that_crossed_a_node_is_refused_once_its_distance_is_gone() { assert!(sim.deliver(b, a)); assert!(sim.holds(a, 7), "b's route stays open until b ends it"); assert!(sim.route(a, 7).is_none(), "a refuses its own route, come back"); - assert!(!sim.starved(a, 7), "with no distance, no seqno would help"); + assert!(!sim.starved(a, 7), "no seqno would help"); assert_eq!(sim.shows(a, 7, ""), None); // b still reaches the origin, and a takes the route b learns there. @@ -1099,23 +1099,79 @@ fn a_route_that_returns_through_a_scoped_peer_is_refused() { /// relay cannot add itself, so it is unreachable there, not waiting on a seqno. #[test] fn a_route_stops_at_the_hop_limit() { - let mut sim = Sim::new(5); - for node in 0..5 { - sim.nodes[node].max_hops = 3; - } - for node in 0..4 { + let last = MAX_HOPS + 1; + let mut sim = Sim::new(last + 1); + for node in 0..last { sim.join(node, node + 1, 1); } originate(&mut sim, 0, 7, 0); assert!(sim.run()); - assert_eq!( - sim.route(2, 7).map(|route| route.metric), - Some(2), - "the origin, 1, and 2 make three" - ); - assert!(sim.route(3, 7).is_none(), "2's route crossed three nodes already"); - assert!(sim.holds(3, 7) && !sim.starved(3, 7)); - assert!(!sim.holds(4, 7), "3 has nothing to send on"); + let full = last - 2; + assert_eq!(sim.route(full, 7).map(|route| route.metric), Some(full as Metric)); + assert!(sim.route(full + 1, 7).is_none(), "the route crossed as many nodes as one may"); + assert!(sim.holds(full + 1, 7) && !sim.starved(full + 1, 7)); + assert!(!sim.holds(last, 7), "nothing is sent on"); +} + +/// A relay sends the origin's route to a peer that files it under a qualified key +/// and hands it back. While the peer got there by another relay the copy is a route +/// like any other; once the peer takes this relay's own, the copy has crossed it. No +/// seqno changes that, so the relay lets the key go without asking for one. +#[test] +fn a_scoped_copy_that_crossed_a_relay_asks_for_no_seqno() { + let (origin, near, far, cdn) = (0, 1, 2, 3); + let mut sim = Sim::new(4); + sim.join(origin, near, 1); + sim.join(origin, far, 1); + sim.link(near, cdn, SimLink::cost(1), SimLink::cost(1).grant(LOCAL)); + sim.link(far, cdn, SimLink::cost(1), SimLink::cost(2).grant(LOCAL)); + // The peer hears the far relay first. + sim.hold(near, cdn); + sim.originate(origin, 7, 0); + sim.announce(origin, "local/x", 0, None); + assert!(sim.run()); + let key = qualified(LOCAL.subject, 7); + assert_eq!(next(&sim, cdn, key), Some(far)); + assert_eq!(next(&sim, near, key), Some(cdn)); + + sim.release(near, cdn); + assert!(sim.run()); + assert_eq!(next(&sim, cdn, key), Some(near), "the peer took the shorter route"); + assert!(sim.route(near, key).is_none(), "which crossed the near relay"); + assert!(!sim.starved(near, key)); + assert_eq!(sim.seqno(origin), 0, "nothing failed, so nothing was asked"); + assert_eq!(sim.retained().pending, 0); + assert_eq!(sim.shows(near, 7, "local/x"), Some(true)); +} + +/// The same copy, arriving at a metric the relay's distance refuses: the peer had +/// the origin through the far relay, and falls back on the near one's route when +/// that goes. The copy is infeasible, but it extends nothing the near relay sent +/// under the key, so the peer will never move off it: the relay does not wait. +#[test] +fn a_scoped_copy_that_crossed_a_relay_is_not_waited_on() { + let (origin, near, far, cdn) = (0, 1, 2, 3); + let mut sim = Sim::new(4); + sim.join(origin, near, 5); + sim.join(origin, far, 1); + // The near relay is nearer the origin than the peer, so its route is feasible there. + sim.link(near, cdn, SimLink::cost(1), SimLink::cost(3).grant(LOCAL)); + sim.link(far, cdn, SimLink::cost(1), SimLink::cost(5).grant(LOCAL)); + sim.originate(origin, 7, 0); + sim.announce(origin, "local/x", 0, None); + assert!(sim.run()); + let key = qualified(LOCAL.subject, 7); + assert_eq!(next(&sim, cdn, key), Some(far)); + assert_eq!(sim.route(near, key).map(|route| route.metric), Some(7)); + + sim.disconnect(far, cdn); + assert!(sim.run()); + assert_eq!(sim.route(cdn, key).map(|route| (route.next, route.metric)), Some((Some(near), 8))); + assert!(sim.holds(near, key) && sim.route(near, key).is_none()); + assert!(!sim.starved(near, key), "the peer's route stands whatever the relay does"); + assert_eq!(sim.seqno(origin), 0); + assert_eq!(sim.retained().pending, 0); + assert_eq!(sim.shows(near, 7, "local/x"), Some(true)); } /// The cost of the longest loop-free path from `from` through nodes not yet `seen`, diff --git a/rs/moq-net/verify/route/RouteHandoff.tla b/rs/moq-net/verify/route/RouteHandoff.tla index 31e8ef0f63a..ce5d43ecc21 100644 --- a/rs/moq-net/verify/route/RouteHandoff.tla +++ b/rs/moq-net/verify/route/RouteHandoff.tla @@ -96,15 +96,23 @@ Serves(n) == n = Origin \/ n \notin Leaves \* `Entry::crossed`: the route's hops name this node. Crossed(n, e) == \E i \in DOMAIN e.hops : e.hops[i] = n -Feasible(n, s, e) == - /\ ~Crossed(n, e) - /\ ~s.fd.on \/ e.seq > s.fd.seq \/ (e.seq = s.fd.seq /\ e.met < s.fd.met) +Feasible(s, e) == + ~s.fd.on \/ e.seq > s.fd.seq \/ (e.seq = s.fd.seq /\ e.met < s.fd.met) -UsableSet(n, s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ Feasible(n, s, s.rx[m])} -\* With no distance kept, no route waits on a seqno. +\* `eligible`: a node selects and certifies only through a feasible route that +\* did not cross it. +Eligible(n, s, e) == ~Crossed(n, e) /\ Feasible(s, e) + +\* Whether hops `h` extend `a`, the hops of the route this node last sent. +Extends(a, h) == a # <<>> /\ Len(a) <= Len(h) /\ SubSeq(h, 1, Len(a)) = a + +UsableSet(n, s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ Eligible(n, s, s.rx[m])} +\* `infeasible`: a crossed route counts only while it extends the route this +\* node last sent, so its sender moves once it hears this node has none. InfeasibleSet(n, s) == - {m \in Nodes : s.fd.on /\ s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(n, s, s.rx[m])} -Certifiers(n, s) == {m \in Nodes : s.rx[m].on /\ Feasible(n, s, s.rx[m])} + {m \in Nodes : /\ s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(s, s.rx[m]) + /\ ~Crossed(n, s.rx[m]) \/ Extends(s.adv, s.rx[m].hops)} +Certifiers(n, s) == {m \in Nodes : s.rx[m].on /\ Eligible(n, s, s.rx[m])} Recoverable(n, s) == \E m \in Certifiers(n, s) : s.rx[m].held \* This node's metric through the route `m` sent. @@ -246,14 +254,17 @@ Update(n, s0, ov, ups, eb) == live == Live(n, s2) av == Adopted(n, s2, ov) plans == [m \in Peers(n, ups) |-> Plan(n, s2, m, sel, live, av, ov)] + \* `advertised`: the hops of the last route this node started or changed anywhere. + sends == \E m \in Peers(n, ups) : plans[m].sent.kind = "fin" /\ plans[m].sent # s2.sent[m] s3 == [s2 EXCEPT + !.adv = IF sends THEN sel.hops ELSE @, !.sent = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].sent ELSE s2.sent[m]], !.sentV = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].sentV ELSE s2.sentV[m]], !.unacked = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].unacked ELSE s2.unacked[m]]] \* Drop the feasibility distance once nothing routes, advertises, or awaits an echo. drained == n # Origin /\ \A m \in Nodes : ~s3.rx[m].on /\ s3.sent[m].kind = "none" /\ s3.unacked[m] = 0 - s4 == IF drained THEN [s3 EXCEPT !.fd = NoFd] ELSE s3 + s4 == IF drained THEN [s3 EXCEPT !.fd = NoFd, !.adv = <<>>] ELSE s3 req == Requests(n, s4, sel) s5 == [s4 EXCEPT !.pending = req.pending] now == ShownNow(n, s5, sel, live, ov) @@ -291,6 +302,7 @@ Commit(rs, q0) == InitNode == [ rx |-> [m \in Nodes |-> NoEntry], fd |-> NoFd, + adv |-> <<>>, heard |-> [m \in Nodes |-> NoHeard], view |-> NoView, sent |-> [m \in Nodes |-> NoReach], From 4b26eeda00ce755aa2a676345d4f557622df2db3 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 06:41:39 -0800 Subject: [PATCH 10/17] test(net): the route sweep scopes a quarter of its meshes, and the docs follow the rule as built Co-Authored-By: Claude --- doc/bin/relay/cluster.md | 9 +++--- quest/m2/cluster-routing/routes/README.md | 14 ++++++--- rs/moq-net/src/model/origin.rs | 3 +- rs/moq-net/src/route/tests/routing.rs | 37 ++++++++++++++++++++--- 4 files changed, 48 insertions(+), 15 deletions(-) diff --git a/doc/bin/relay/cluster.md b/doc/bin/relay/cluster.md index f19465e6f44..b0ea559f5b3 100644 --- a/doc/bin/relay/cluster.md +++ b/doc/bin/relay/cluster.md @@ -111,10 +111,11 @@ max_hops = 6 ``` The same setting is `--cluster-max-hops` or `MOQ_CLUSTER_MAX_HOPS`. It covers -moq-lite-03 and later, and moq-transport drafts 18 through 22 when the MoQ -Cluster extension is negotiated. On moq-lite-07-wip it bounds the nodes a route -crosses, the publishing node and this relay included. A forwarded path counts -this relay's own hop even when its peer appends it on receipt. Older versions and peers +moq-lite-03 through moq-lite-06 and moq-transport drafts 18 through 22 when +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. ## Upstream links diff --git a/quest/m2/cluster-routing/routes/README.md b/quest/m2/cluster-routing/routes/README.md index 10827756b46..f8eb9597a85 100644 --- a/quest/m2/cluster-routing/routes/README.md +++ b/quest/m2/cluster-routing/routes/README.md @@ -40,7 +40,7 @@ The items below were decided 2026-11-10 (maintainer, /quest-plan on lite-07 rout 22. ✅ **A side's interest is a set of prefixes edited in place.** The live set never nests, and one edit may swap prefixes for a wider or narrower one without re-sending what both cover ([the interest set](/quest/m2/cluster-routing/routes/interest-set.md)). A token-scope change is such an edit, with one prefix per region of the scope. This supersedes items 16 and 17, and the handoff contract's "An interest change opens a new stream" below, once the route stream lands. 23. ✅ Asked what a floor covers with several prefixes on one stream: **one prefix, named by its id.** This amends item 10: the floor is still a marker and never a region list. Rejected: a floor over the whole set. 24. ✅ Asked how a side learns a newly added prefix's initial set is complete: **SYNCED per prefix, naming its id**, plus one marker per edit where it takes effect for both sides. Rejected: one SYNCED per edit, counted in order. -25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the nodes it crossed, and a node never uses a route that names itself** ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. As built: such a route is infeasible rather than ignored, so a relay whose neighbours all route through it still holds its claims while one of them finds another way; the origin names itself too, so a rotated identity's route is refused where it began; and a node names itself by a Hop ID that a rotation leaves alone. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. +25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the nodes it crossed, and a node never uses a route that names itself** ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. As built: Babel's feasibility condition is unchanged, and a node never selects or certifies through such a route. It still counts as infeasible, so the node holds its claims, only while its hops extend those of the route the node last sent: a relay whose neighbours all route through it then waits while one of them finds another way, and does not wait on a copy that a scoped peer hands back under a qualified key, which never moves. The origin names itself too, so a rotated identity's route is refused where it began, and a node names itself by a Hop ID that a rotation leaves alone. The hop limit is the wire's 32 and no lower. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. The route layer's core landed in @@ -195,8 +195,8 @@ the bullets below are the contract it carries. ROUTE_HOLD or ROUTE_END. The route model found a count to infinity (2026-11-10): an echo can overtake a route derived from the echoed one, and even in order a per-neighbour echo misses a derived copy held by a - third relay. Each route therefore names the nodes it crossed, and one - naming the receiver is never feasible there (Plan item 25, + third relay. Each route therefore names the nodes it crossed, and a node + never selects one that names itself (Plan item 25, `sweep_no_route_outgrows_a_loop_free_path`). - Starvation recovery is Babel's seqno request (RFC 8966 s3.8, decided 2026-10-12). A node whose routes to an origin are all infeasible sends @@ -351,7 +351,11 @@ loss never reports an END: delivered (`a_lost_scope_keeps_newer_knowledge_where_still_certified`). Otherwise a wildcard above both was last learned through the lost floor and is unknown at the kept floors' revision, so the view is rebuilt from the - neighbours' last views, a collection of that region. A sender sends a + neighbours' last views, a collection of that region. A neighbour whose + route becomes feasible again certifies again with the view it last sent, + which the node takes back: it sends nothing more, and a region let go + meanwhile would otherwise stay gone + (`a_certifier_that_returns_brings_back_what_it_certifies`). A sender sends a route on a stream only while the route meets the stream's interest (Plan item 15): it starts the route before its first claim in or covering the interest, and when the last such claim goes it sends a floor certifying the @@ -492,7 +496,7 @@ Decided with the maintainer 2026-10-16, from the handoff proof: (`sweep_forgetting_distances`). Revised 2026-11-10 (Plan item 25): the echo is not enough alone, since a third node can hold a copy derived from the advertisement and hand it back after the drain. Each route names the - nodes it crossed and is never feasible where it has been + nodes it crossed, and a node never selects one that names itself (`sweep_no_route_outgrows_a_loop_free_path`). Rejected: keeping the distance forever, which grows with publisher churn times uptime on every relay that saw an identity, about 16 bytes each, until a restart; and Babel's source GC diff --git a/rs/moq-net/src/model/origin.rs b/rs/moq-net/src/model/origin.rs index de3aec4d4e0..ef34fe00695 100644 --- a/rs/moq-net/src/model/origin.rs +++ b/rs/moq-net/src/model/origin.rs @@ -115,7 +115,8 @@ pub struct Config { /// moq-transport. A forwarded path counts this origin's own hop too, including /// when the receiving peer reconstructs that hop from the announce handshake. /// Protocols without a hop path cannot reveal or bound the depth they hide. No wire - /// carries a path longer than 32, so a larger value acts as 32. + /// carries a path longer than 32, so a larger value acts as 32, and a moq-lite-07 + /// route's own hops stop there whatever this is. pub max_hops: NonZeroUsize, /// The cache pool broadcasts under this origin charge their groups into. It flows diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index d778308de71..34297c25141 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -1111,7 +1111,10 @@ fn a_route_stops_at_the_hop_limit() { assert!(sim.run()); let full = last - 2; assert_eq!(sim.route(full, 7).map(|route| route.metric), Some(full as Metric)); - assert!(sim.route(full + 1, 7).is_none(), "the route crossed as many nodes as one may"); + assert!( + sim.route(full + 1, 7).is_none(), + "the route crossed as many nodes as one may" + ); assert!(sim.holds(full + 1, 7) && !sim.starved(full + 1, 7)); assert!(!sim.holds(last, 7), "nothing is sent on"); } @@ -1169,9 +1172,15 @@ fn a_scoped_copy_that_crossed_a_relay_is_not_waited_on() { sim.disconnect(far, cdn); assert!(sim.run()); - assert_eq!(sim.route(cdn, key).map(|route| (route.next, route.metric)), Some((Some(near), 8))); + assert_eq!( + sim.route(cdn, key).map(|route| (route.next, route.metric)), + Some((Some(near), 8)) + ); assert!(sim.holds(near, key) && sim.route(near, key).is_none()); - assert!(!sim.starved(near, key), "the peer's route stands whatever the relay does"); + assert!( + !sim.starved(near, key), + "the peer's route stands whatever the relay does" + ); assert_eq!(sim.seqno(origin), 0); assert_eq!(sim.retained().pending, 0); assert_eq!(sim.shows(near, 7, "local/x"), Some(true)); @@ -1197,7 +1206,9 @@ fn longest(sim: &Sim, from: Node, seen: &mut Vec) -> Metric { /// random order while links flap and relays restart and collect. A route names the /// relays it crossed, so no relay ever selects one longer than a loop-free path: a /// node that forgot the origin cannot take back a copy of its own old route. Without -/// the hops this finds a count to infinity within a dozen cases. +/// the hops this finds a count to infinity within a dozen cases. Every fourth mesh +/// scopes some relays under a grant, which hands a relay its own route back under a +/// qualified key: nothing may wait on that copy once the mesh is quiet. #[test] fn sweep_no_route_outgrows_a_loop_free_path() { let mut rng = XorShift(0x0bad_c0de); @@ -1205,12 +1216,21 @@ fn sweep_no_route_outgrows_a_loop_free_path() { for case in 0..200 { let relays = 3 + rng.next(3) as usize; let origin = relays; + let scoped = case % 4 == 1; let mut sim = Sim::new(relays + 1); let mut links = Vec::new(); for a in 0..relays { for b in a + 1..relays { if b == a + 1 || rng.chance(50) { - sim.join(a, b, 1 + rng.next(3)); + let side = SimLink::cost(1 + rng.next(3)); + let grant = Grant { + subject: ["ga", "gb"][rng.next(2) as usize], + scope: "", + }; + match scoped && rng.chance(30) { + true => sim.link(a, b, side.grant(grant), side), + false => sim.link(a, b, side, side), + } links.push((a, b)); } } @@ -1295,6 +1315,13 @@ fn sweep_no_route_outgrows_a_loop_free_path() { } cut += usize::from(reached.len() <= relays); for node in 0..relays { + for &id in sim.nodes[node].rx.keys() { + assert!(!sim.starved(node, id), "case {case}: node {node} waits on {id}"); + } + // A scoped link files the origin under another key past it. + if scoped { + continue; + } match reached.contains(&node) { true => { assert!(sim.route(node, 7).is_some(), "case {case}: node {node} lost its route"); From f1fbea679cacd888c7fbe64cf1e81e781e48cf43 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 06:41:50 -0800 Subject: [PATCH 11/17] docs(skill): verify-route syncs to main with the route RTT Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index bef59f5e24d..f08441da0bc 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -54,7 +54,7 @@ A counterexample is a path through the model, not yet a bug. Replay it on the ro ## Coverage -Sync commit: `52fa6b2f0ece29c44bfa2459ec93fc54b4b48221`, plus the change that added a route's hops ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487)). Run `git log 52fa6b2f0e.. -- 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. +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 | | --- | --- | From cceb0194ff6b3477aab2d2679ad84824a9b80089 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 06:42:02 -0800 Subject: [PATCH 12/17] docs(skill): verify-route leaves out the route RTT Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index f08441da0bc..dd562717683 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -69,4 +69,4 @@ Sync commit: `c916855d163ff5641ad18cfb8e14b76dababd99a`, plus the change that ad ## 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 and 2, the hop limit, 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. +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 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. From a9a38520d62509261495dad13e4de861fa703b92 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 06:48:52 -0800 Subject: [PATCH 13/17] docs(skill): verify-route records the final state counts Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index dd562717683..e3c0ef553e6 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -37,7 +37,7 @@ just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/rout | --- | --- | --- | --- | | `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,462,496 | +| `BehindDear.cfg` | The same, with relay 3 nearer the origin than relay 2. | 1 claim change, 1 session change | 5,297,593 | All three pass at the sync commit. Each takes minutes on 4 workers, so run them last. First run what answers in seconds: From 9e07f609af36fa37ae1d4965d46bc4d9b550e18d Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 08:29:27 -0800 Subject: [PATCH 14/17] fix(net): a crossed route is waited on like any other, and the prune merge-back goes A second adversarial review found the merge-back worse than what it fixed: a neighbour that is feasible for one message during a seqno advance had its view taken back, which flapped a relay's claims on every advance and kept a static mesh with two narrowed interests asking for seqnos for good. prune is as on main again. A change of a route's hops or RTT alone no longer prunes: it moves no certifier, and pruning there acted on one this node's own distance had set aside, which is how a change of hops alone lost a claim. A crossed route under a plain identity always came through this node's own route to that identity, so it counts as infeasible like any other, as on main. Only under a qualified key must it extend what this node last sent, which a relay restart no longer defeats. Co-Authored-By: Claude --- rs/moq-net/src/route/mod.rs | 62 +++++++++++++++------------ rs/moq-net/src/route/tests/handoff.rs | 41 ------------------ rs/moq-net/src/route/tests/routing.rs | 29 +++++++++++++ 3 files changed, 64 insertions(+), 68 deletions(-) diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index b57fd515354..5c7914f711d 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -424,8 +424,8 @@ pub(crate) struct Router { filed: BTreeMap<(Id, N), Id>, /// Babel's feasibility distance per identity. fd: BTreeMap, - /// The hops of the route this node last sent for an identity, kept as long as its - /// distance: a route that extends them came through this node's own. + /// The hops of the route this node last sent under a qualified key, kept as long + /// as its distance: a route that extends them came through this node's own. advertised: BTreeMap>, sent: BTreeMap<(Id, N), Reach>, /// ROUTE_ENDs sent to each neighbor and not yet echoed back. Until they all @@ -819,9 +819,17 @@ impl Router { }; } let routes = self.rx.entry(id).or_default(); + // Whether only the route's hops or RTT changed, which moves no route here. + let mut same = false; match reach { Some(Reach::Finite(advert)) => { let crossed = advert.hops.contains(&self.hop); + same = routes.get(&from).is_some_and(|was| { + let (old, new) = (&was.advert, &advert); + !was.held + && was.crossed == crossed + && (old.seqno, old.metric, old.down_only) == (new.seqno, new.metric, new.down_only) + }); let entry = Entry { advert, held: false, @@ -855,7 +863,7 @@ impl Router { // What it drops lay outside every floor, so nothing it differed in. heard.ended = true; } - self.update([id]); + self.recompute([id], !same); } /// A batch of announcement changes for `named` from `from`, closed by its @@ -1268,15 +1276,21 @@ impl Router { } /// The usable but infeasible routes for `id`, with their metrics: this node holds - /// the identity while it has one. A route that crossed this node counts only if it - /// extends the route this node last sent, since its sender then routes through this - /// node and moves once it hears this node has none. Any other one that crossed it - /// stays as it is whatever this node does, and waiting on it would never end. + /// the identity while it has one. One that crossed this node counts like any other: + /// its sender routes through this node, and moves once it hears this node has no + /// route. Under a qualified key that holds only if the route extends the one this + /// node last sent under the key. Otherwise a relay past this node derived the key + /// from this node's route to another identity, which stands whatever happens to + /// this one, and waiting on it would never end. fn infeasible(&self, id: Id) -> impl Iterator + '_ { let sent = self.advertised.get(&id); + let derived = move |entry: &Entry| match id & QUALIFIED { + 0 => true, + _ => sent.is_some_and(|sent| entry.advert.hops.starts_with(sent)), + }; (self.rx.get(&id).into_iter().flatten()) .filter(move |(_, entry)| !entry.held && !self.feasible(id, &entry.advert)) - .filter(move |(_, entry)| !entry.crossed || sent.is_some_and(|sent| entry.advert.hops.starts_with(sent))) + .filter(move |(_, entry)| !entry.crossed || derived(entry)) .filter_map(move |(&next, entry)| Some((self.metric(next, entry)?, next))) } @@ -1354,23 +1368,6 @@ impl Router { let Some(regions) = self.certified(id, true) else { return; }; - // A certifier whose view the merged one lags was not one when its regions were - // let go below, and sends nothing more now it certifies again: take its view back. - let merged = self.views.get(&id); - let lags = |view: &View| { - (view.floors.iter()).any(|(region, &rev)| merged.and_then(|merged| merged.as_of(region)) < Some(rev)) - }; - let back: Vec = (self.certifiers(id).into_iter()) - .filter(|next| lags(self.heard[&(id, *next)].view())) - .collect(); - if !back.is_empty() { - let merged = self.views.entry(id).or_default(); - for next in back { - merged.merge(self.heard[&(id, next)].view()); - } - self.resync(id); - self.mark_all(id); - } let Some(merged) = self.views.get(&id) else { return; }; @@ -1533,6 +1530,13 @@ impl Router { /// this node advertises, what each neighbor is sent, its seqno request, and /// what the reader sees. fn update(&mut self, ids: impl IntoIterator) { + self.recompute(ids, true); + } + + /// [`Self::update`], letting go of what no neighbor certifies only when `prune`. A + /// neighbor's change of hops or RTT alone moves no certifier, so it lets go of + /// nothing: only a message that could have cost a region its certifier does. + fn recompute(&mut self, ids: impl IntoIterator, prune: bool) { let peers: Vec = self .neighbors .iter() @@ -1548,7 +1552,9 @@ impl Router { self.changed.entry(id).or_default(); } for id in ids { - self.prune(id); + if prune { + self.prune(id); + } self.record(id, &peers); let ctx = self.ctx(id, self.selected(id)); let mut dirty = self.dirty.remove(&id).unwrap_or_default(); @@ -1807,7 +1813,9 @@ impl Router { if let Some(send) = send && self.sent.get(&key) != Some(&send) { - if let Reach::Finite(advert) = &send { + if id & QUALIFIED != 0 + && let Reach::Finite(advert) = &send + { self.advertised.insert(id, advert.hops.clone()); } self.sent.insert(key, send.clone()); diff --git a/rs/moq-net/src/route/tests/handoff.rs b/rs/moq-net/src/route/tests/handoff.rs index 946428c3f35..f76629eeadc 100644 --- a/rs/moq-net/src/route/tests/handoff.rs +++ b/rs/moq-net/src/route/tests/handoff.rs @@ -1439,44 +1439,3 @@ fn a_restarted_floorless_route_drops_what_it_no_longer_carries() { assert_eq!(revivals(&sim.events), 0); sim.check().unwrap(); } - -/// Relay 4 hears origin 7's claims from relay 0, which certifies them all, and from -/// relay 3, which asked only for `b`. While 0's route is infeasible for a moment, 3 -/// is the only certifier, and 4 lets go of what 3 does not certify. Once 0 certifies -/// again, 4 takes back what 0 still carries, though 0 sends nothing more. -#[test] -fn a_certifier_that_returns_brings_back_what_it_certifies() { - let (origin, other) = (6, 7); - let mut sim = Sim::new(8); - sim.join(other, 4, 1); - sim.join(other, 5, 1); - sim.join(origin, 3, 1); - sim.join(origin, 2, 1); - sim.join(0, 1, 1); - sim.link(0, 2, SimLink::cost(3), SimLink::cost(1)); - sim.join(0, 3, 1); - sim.join(0, 4, 1); - sim.link(1, 2, SimLink::cost(2), SimLink::cost(1)); - sim.join(2, 3, 1); - sim.join(2, 5, 1); - sim.link(3, 4, SimLink::cost(1), SimLink::cost(2)); - sim.originate(origin, 7, 0); - sim.announce(origin, "", 0, None); - sim.originate(other, 8, 0); - sim.announce(other, "", 0, None); - sim.watch(3, "b"); - assert!(sim.run()); - assert_eq!(sim.shows(4, 7, ""), Some(true)); - - let before = sim.events.len(); - sim.disconnect(origin, 3); - assert!(sim.run()); - let let_go = (sim.events[before..].iter()).any(|event| (event.node, event.id, event.kind) == (4, 7, Kind::Offline)); - assert!(let_go, "relay 4 let the claim go while only relay 3 certified"); - assert_eq!(sim.shows(4, 7, ""), Some(true), "and took it back from relay 0"); - sim.disconnect(2, 3); - assert!(sim.run()); - assert_eq!(sim.shows(4, 7, ""), Some(true)); - assert_eq!(false_ends(&sim.events), 0); - sim.check().unwrap(); -} diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index 34297c25141..37659e27d8a 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -1344,3 +1344,32 @@ fn sweep_no_route_outgrows_a_loop_free_path() { "{flaps} flaps, {collected} collects, {cut} cut, {restarts} restarts" ); } + +/// A relay restarts with no memory and hands node 4 a reflection of the route 4 sent +/// before its last one. It crossed 4 and is infeasible there, so 4 waits on it like +/// any infeasible route, and its readers see the claim unavailable, never gone. +#[test] +fn a_relay_restart_keeps_the_claim_unavailable() { + let origin = 6; + let mut sim = Sim::new(7); + sim.join(origin, 1, 1); + sim.join(1, 3, 1); + sim.link(1, 4, SimLink::cost(1), SimLink::cost(2)); + sim.link(1, 5, SimLink::cost(1).priority(1), SimLink::cost(3).priority(-1)); + sim.join(3, 4, 1); + sim.join(4, 5, 1); + originate(&mut sim, origin, 7, 0); + assert!(sim.run()); + + let before = sim.events.len(); + sim.kill(1); + sim.reconnect(1); + assert!(sim.run()); + for node in [4, 5] { + let seen: Vec = (sim.events[before..].iter()) + .filter(|event| event.node == node) + .map(|event| event.kind) + .collect(); + assert_eq!(seen, [Kind::Unavailable, Kind::Available], "node {node}"); + } +} From 0b84b207928f89dd64b5cf326068643eb4a8b171 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 08:49:01 -0800 Subject: [PATCH 15/17] docs: the model, draft, skill, and epic follow the rule as built Co-Authored-By: Claude --- .claude/skills/verify-route/SKILL.md | 8 ++-- drafts/draft-lcurley-moq-lite.md | 3 +- quest/m2/cluster-routing/routes/README.md | 8 +--- rs/moq-net/verify/route/RouteHandoff.tla | 47 +++++++++++------------ 4 files changed, 30 insertions(+), 36 deletions(-) diff --git a/.claude/skills/verify-route/SKILL.md b/.claude/skills/verify-route/SKILL.md index e3c0ef553e6..5771104341a 100644 --- a/.claude/skills/verify-route/SKILL.md +++ b/.claude/skills/verify-route/SKILL.md @@ -37,7 +37,7 @@ just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/rout | --- | --- | --- | --- | | `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,297,593 | +| `BehindDear.cfg` | The same, with relay 3 nearer the origin than relay 2. | 1 claim change, 1 session change | 5,377,597 | All three pass at the sync commit. Each takes minutes on 4 workers, so run them last. First run what answers in seconds: @@ -58,9 +58,9 @@ Sync commit: `c916855d163ff5641ad18cfb8e14b76dababd99a`, plus the change that ad | Code (`rs/moq-net/src/route/`) | Model | | --- | --- | -| `mod.rs` `feasible`, `Entry::crossed`, `eligible`, `metric`, `selected`, `infeasible`, `advertised`, `recoverable`, `live`, `certifiers` | `Feasible`, `Crossed`, `Eligible`, `Through`, `Selected`, `InfeasibleSet`, `adv` and `Extends`, `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` | @@ -69,4 +69,4 @@ Sync commit: `c916855d163ff5641ad18cfb8e14b76dababd99a`, plus the change that ad ## 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 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. +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. diff --git a/drafts/draft-lcurley-moq-lite.md b/drafts/draft-lcurley-moq-lite.md index e4a61ebaaa0..4cac9f93a4e 100644 --- a/drafts/draft-lcurley-moq-lite.md +++ b/drafts/draft-lcurley-moq-lite.md @@ -515,7 +515,8 @@ A route is feasible when no feasibility distance is kept for its Node ID yet, wh A node selects, per Node ID, among its feasible routes that are not held: a session that has not received a GOAWAY, then the highest local priority, then the lowest metric. It MUST NOT select an infeasible route, and a distance only ever falls within a Seqno, so advertising a longer route never raises it. It MUST NOT select a route whose Hops name it either, feasible or not: that is a copy of a route the node sent, which no distance refuses once the node dropped it. -Such a route counts among the node's routes below only while it is infeasible and its Hops begin with those of the route the node last sent to that origin node: its sender then routes through the node, and moves once it hears the node has no route. +Such a route counts below as an infeasible route where the feasibility condition refuses it, and as no route where it does not: its sender routes through the node, and moves once it hears the node has no route. +Under a qualified Node ID it counts only if its Hops also begin with those of the route the node last sent under that Node ID: otherwise a relay past the node derived the Node ID from the node's route under another, and that copy stands whatever the node does. A node MAY mark a session upstream. A route is down-only when it arrived on an upstream session or with its down-only flag set; a node sends a down-only route with the flag set, and never on an upstream session. diff --git a/quest/m2/cluster-routing/routes/README.md b/quest/m2/cluster-routing/routes/README.md index f8eb9597a85..80a4fb11698 100644 --- a/quest/m2/cluster-routing/routes/README.md +++ b/quest/m2/cluster-routing/routes/README.md @@ -40,7 +40,7 @@ The items below were decided 2026-11-10 (maintainer, /quest-plan on lite-07 rout 22. ✅ **A side's interest is a set of prefixes edited in place.** The live set never nests, and one edit may swap prefixes for a wider or narrower one without re-sending what both cover ([the interest set](/quest/m2/cluster-routing/routes/interest-set.md)). A token-scope change is such an edit, with one prefix per region of the scope. This supersedes items 16 and 17, and the handoff contract's "An interest change opens a new stream" below, once the route stream lands. 23. ✅ Asked what a floor covers with several prefixes on one stream: **one prefix, named by its id.** This amends item 10: the floor is still a marker and never a region list. Rejected: a floor over the whole set. 24. ✅ Asked how a side learns a newly added prefix's initial set is complete: **SYNCED per prefix, naming its id**, plus one marker per edit where it takes effect for both sides. Rejected: one SYNCED per edit, counted in order. -25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the nodes it crossed, and a node never uses a route that names itself** ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. As built: Babel's feasibility condition is unchanged, and a node never selects or certifies through such a route. It still counts as infeasible, so the node holds its claims, only while its hops extend those of the route the node last sent: a relay whose neighbours all route through it then waits while one of them finds another way, and does not wait on a copy that a scoped peer hands back under a qualified key, which never moves. The origin names itself too, so a rotated identity's route is refused where it began, and a node names itself by a Hop ID that a rotation leaves alone. The hop limit is the wire's 32 and no lower. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. +25. ✅ Asked how a relay safely forgets a publisher that is gone, after the model showed a per-neighbour echo is not enough once the origin sits behind a relay: **each route names the nodes it crossed, and a node never uses a route that names itself** ([moq-dev/moq#8487](https://github.com/moq-dev/moq/pull/8487), which holds the counterexamples and the model results). Feasibility still selects routes; the list is one per origin route, not the per-claim Hop ID list item 6 removed, and the echo and the drain rule stay as they are. As built: Babel's feasibility condition is unchanged, and a node never selects or certifies through such a route. Where the condition refuses it, it still counts as infeasible, so a relay whose neighbours all route through it holds its claims while one of them finds another way. Under a qualified key it counts only while its hops extend those of the route the node last sent under that key: a copy that a scoped peer hands back under a key derived from the node's own route never moves, so nothing waits on it. The origin names itself too, so a rotated identity's route is refused where it began, and a node names itself by a Hop ID that a rotation leaves alone. The hop limit is the wire's 32 and no lower. A change of hops or RTT alone lets go of no region. This supersedes the claim, in the handoff contract and in decision 6 below, that the echo alone makes forgetting safe. First decided as a relay echoing a ROUTE_END only once its own downstream had; the model ran that the same day and it fails when a session closes before answering. Rejected: that deferred echo; never dropping the distance; a timer; relays as the only origin nodes. The route layer's core landed in @@ -351,11 +351,7 @@ loss never reports an END: delivered (`a_lost_scope_keeps_newer_knowledge_where_still_certified`). Otherwise a wildcard above both was last learned through the lost floor and is unknown at the kept floors' revision, so the view is rebuilt from the - neighbours' last views, a collection of that region. A neighbour whose - route becomes feasible again certifies again with the view it last sent, - which the node takes back: it sends nothing more, and a region let go - meanwhile would otherwise stay gone - (`a_certifier_that_returns_brings_back_what_it_certifies`). A sender sends a + neighbours' last views, a collection of that region. A sender sends a route on a stream only while the route meets the stream's interest (Plan item 15): it starts the route before its first claim in or covering the interest, and when the last such claim goes it sends a floor certifying the diff --git a/rs/moq-net/verify/route/RouteHandoff.tla b/rs/moq-net/verify/route/RouteHandoff.tla index ce5d43ecc21..93a75174bce 100644 --- a/rs/moq-net/verify/route/RouteHandoff.tla +++ b/rs/moq-net/verify/route/RouteHandoff.tla @@ -103,15 +103,10 @@ Feasible(s, e) == \* did not cross it. Eligible(n, s, e) == ~Crossed(n, e) /\ Feasible(s, e) -\* Whether hops `h` extend `a`, the hops of the route this node last sent. -Extends(a, h) == a # <<>> /\ Len(a) <= Len(h) /\ SubSeq(h, 1, Len(a)) = a - UsableSet(n, s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ Eligible(n, s, s.rx[m])} -\* `infeasible`: a crossed route counts only while it extends the route this -\* node last sent, so its sender moves once it hears this node has none. -InfeasibleSet(n, s) == - {m \in Nodes : /\ s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(s, s.rx[m]) - /\ ~Crossed(n, s.rx[m]) \/ Extends(s.adv, s.rx[m].hops)} +\* `infeasible`: a route that crossed this node counts like any other. No key +\* is qualified here, so its sender routes through this node's own route. +InfeasibleSet(s) == {m \in Nodes : s.rx[m].on /\ ~s.rx[m].held /\ ~Feasible(s, s.rx[m])} Certifiers(n, s) == {m \in Nodes : s.rx[m].on /\ Eligible(n, s, s.rx[m])} Recoverable(n, s) == \E m \in Certifiers(n, s) : s.rx[m].held @@ -132,7 +127,7 @@ Selected(n, s, ov) == hops |-> Append(s.rx[m].hops, n)] Live(n, s) == - n = Origin \/ UsableSet(n, s) # {} \/ InfeasibleSet(n, s) # {} \/ Recoverable(n, s) + n = Origin \/ UsableSet(n, s) # {} \/ InfeasibleSet(s) # {} \/ Recoverable(n, s) \* `Heard::view`: what it certified before its route ended, else the raw view. HeardView(h) == IF h.kept.floor # Absent THEN h.kept ELSE h.raw @@ -206,7 +201,7 @@ Record(n, s, sel, av, ups) == Requests(n, s, sel) == IF n = Origin THEN [pending |-> NoPending, to |-> None, seq |-> 0] ELSE - LET starved == ~sel.on /\ InfeasibleSet(n, s) # {} + LET starved == ~sel.on /\ InfeasibleSet(s) # {} want == s.fd.seq + 1 p0 == s.pending p1 == IF ~starved THEN p0 @@ -214,8 +209,8 @@ Requests(n, s, sel) == ELSE IF p0.seq < want THEN [p0 EXCEPT !.seq = want, !.asked = None] ELSE p0 answered == sel.on /\ sel.seq >= p1.seq - hasTarget == sel.on \/ InfeasibleSet(n, s) # {} - target == IF sel.on THEN sel.next ELSE Best(n, s, InfeasibleSet(n, s)) + hasTarget == sel.on \/ InfeasibleSet(s) # {} + target == IF sel.on THEN sel.next ELSE Best(n, s, InfeasibleSet(s)) IN IF ~p1.on THEN [pending |-> p1, to |-> None, seq |-> 0] ELSE IF answered \/ (p1.from = {} /\ ~starved) \/ ~hasTarget THEN [pending |-> NoPending, to |-> None, seq |-> 0] @@ -246,25 +241,22 @@ Events(n, s, old, now, live, ov, eb) == \* `update` on node n's state `s0`, with the origin's view `ov`, the open \* sessions `ups`, and `eb`, the items n's reader saw END for. A prune forgets. -Update(n, s0, ov, ups, eb) == - LET s1 == Prune(n, s0, ov) +Update(n, s0, ov, ups, eb, prune) == + LET s1 == IF prune THEN Prune(n, s0, ov) ELSE s0 eb1 == IF s1 # s0 THEN [c \in Claims |-> None] ELSE eb sel == Selected(n, s1, ov) s2 == Record(n, s1, sel, Adopted(n, s1, ov), ups) live == Live(n, s2) av == Adopted(n, s2, ov) plans == [m \in Peers(n, ups) |-> Plan(n, s2, m, sel, live, av, ov)] - \* `advertised`: the hops of the last route this node started or changed anywhere. - sends == \E m \in Peers(n, ups) : plans[m].sent.kind = "fin" /\ plans[m].sent # s2.sent[m] s3 == [s2 EXCEPT - !.adv = IF sends THEN sel.hops ELSE @, !.sent = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].sent ELSE s2.sent[m]], !.sentV = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].sentV ELSE s2.sentV[m]], !.unacked = [m \in Nodes |-> IF m \in Peers(n, ups) THEN plans[m].unacked ELSE s2.unacked[m]]] \* Drop the feasibility distance once nothing routes, advertises, or awaits an echo. drained == n # Origin /\ \A m \in Nodes : ~s3.rx[m].on /\ s3.sent[m].kind = "none" /\ s3.unacked[m] = 0 - s4 == IF drained THEN [s3 EXCEPT !.fd = NoFd, !.adv = <<>>] ELSE s3 + s4 == IF drained THEN [s3 EXCEPT !.fd = NoFd] ELSE s3 req == Requests(n, s4, sel) s5 == [s4 EXCEPT !.pending = req.pending] now == ShownNow(n, s5, sel, live, ov) @@ -302,7 +294,6 @@ Commit(rs, q0) == InitNode == [ rx |-> [m \in Nodes |-> NoEntry], fd |-> NoFd, - adv |-> <<>>, heard |-> [m \in Nodes |-> NoHeard], view |-> NoView, sent |-> [m \in Nodes |-> NoReach], @@ -337,7 +328,7 @@ ChangeClaim(c, item) == IN /\ rev' = rev + 1 /\ own' = own1 /\ hist' = Append(hist, own1) - /\ Commit([n \in {Origin} |-> Update(Origin, st[Origin], ov1, up, ended[Origin])], q) + /\ Commit([n \in {Origin} |-> Update(Origin, st[Origin], ov1, up, ended[Origin], TRUE)], q) /\ UNCHANGED <> \* A new claim, or new attributes for one, under a fresh revision. @@ -399,6 +390,12 @@ Deliver(d) == sel == Selected(n, st[n], OV) \* Already advertised to the requester: `request` returns before `update`. skip == n # Origin /\ msg.type = "request" /\ sel.on /\ sel.seq >= msg.seq + \* Only the route's hops changed: `route` then lets go of nothing. + was == st[n].rx[m] + same == /\ msg.type = "route" /\ msg.reach.kind = "fin" + /\ was.on /\ ~was.held + /\ was.seq = msg.reach.seq /\ was.met = msg.reach.met + /\ Crossed(n, was) = Crossed(n, msg.reach) \* The origin's own identity merges nothing it hears. s1 == IF n = Origin THEN st[n] ELSE CASE msg.type = "route" -> OnRoute(st[n], m, msg.reach) @@ -411,7 +408,7 @@ Deliver(d) == /\ IF skip THEN /\ q' = q0 /\ UNCHANGED <> - ELSE Commit([x \in {n} |-> Update(n, s1, ov1, up, ended[n])], q0) + ELSE Commit([x \in {n} |-> Update(n, s1, ov1, up, ended[n], ~same)], q0) /\ UNCHANGED <> \* `echo`: an echoed ROUTE_END comes back (`Sim::deliver_ack`). @@ -423,7 +420,7 @@ DeliverAck(d) == /\ IF st[n].unacked[m] = 0 THEN UNCHANGED <> ELSE Commit([x \in {n} |-> - Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n])], q) + Update(n, [st[n] EXCEPT !.unacked[m] = @ - 1], OV, up, ended[n], TRUE)], q) /\ UNCHANGED <> ----------------------------------------------------------------------------- @@ -450,7 +447,7 @@ Connect(l) == /\ flaps' = flaps + 1 /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x - IN Update(x, Opened(st[x], y), OV, up1, ended[x])], q) + IN Update(x, Opened(st[x], y), OV, up1, ended[x], TRUE)], q) /\ UNCHANGED <> Disconnect(l) == @@ -463,7 +460,7 @@ Disconnect(l) == /\ acks' = [d \in Dirs |-> IF {d[1], d[2]} = l THEN 0 ELSE acks[d]] /\ Commit([x \in l |-> LET y == CHOOSE y \in l : y # x - IN Update(x, Closed(st[x], y), OV, up1, ended[x])], q0) + IN Update(x, Closed(st[x], y), OV, up1, ended[x], TRUE)], q0) /\ UNCHANGED <> \* `collect`, allowed once the node holds no route (`Sim::holds`). It @@ -476,7 +473,7 @@ Collect(n) == Update(n, [st[n] EXCEPT !.view = NoView, !.heard = [m \in Nodes |-> NoHeard], !.pending = NoPending], - OV, up, [c \in Claims |-> None])], q) + OV, up, [c \in Claims |-> None], TRUE)], q) /\ UNCHANGED <> Quiet == \A d \in Dirs : q[d] = <<>> /\ acks[d] = 0 From c3d7a3e925f1d78288449662298bb69b4a5cf5ed Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 09:02:05 -0800 Subject: [PATCH 16/17] fix(net): a route that grows to the hop limit prunes like any that stops certifying Co-Authored-By: Claude --- rs/moq-net/src/route/mod.rs | 5 ++- rs/moq-net/src/route/tests/routing.rs | 45 +++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 1 deletion(-) diff --git a/rs/moq-net/src/route/mod.rs b/rs/moq-net/src/route/mod.rs index 5c7914f711d..576b86528c4 100644 --- a/rs/moq-net/src/route/mod.rs +++ b/rs/moq-net/src/route/mod.rs @@ -819,15 +819,18 @@ impl Router { }; } let routes = self.rx.entry(id).or_default(); - // Whether only the route's hops or RTT changed, which moves no route here. + // Whether only the route's hops or RTT changed, and not whether this node may + // use it: that moves no route here. let mut same = false; match reach { Some(Reach::Finite(advert)) => { let crossed = advert.hops.contains(&self.hop); + let full = |advert: &Advert| advert.hops.len() >= MAX_HOPS; same = routes.get(&from).is_some_and(|was| { let (old, new) = (&was.advert, &advert); !was.held && was.crossed == crossed + && full(old) == full(new) && (old.seqno, old.metric, old.down_only) == (new.seqno, new.metric, new.down_only) }); let entry = Entry { diff --git a/rs/moq-net/src/route/tests/routing.rs b/rs/moq-net/src/route/tests/routing.rs index 37659e27d8a..51a770b03e0 100644 --- a/rs/moq-net/src/route/tests/routing.rs +++ b/rs/moq-net/src/route/tests/routing.rs @@ -913,6 +913,51 @@ fn an_overflowing_route_neither_certifies_nor_holds() { assert_eq!(router.shows(7, &p("live/x")), None); } +/// A route grows to the hop limit with nothing else about it changed, so its sender +/// stops certifying. What only that neighbor certified is let go at once, though a +/// change of hops alone otherwise lets go of nothing. +#[test] +fn a_route_grown_to_the_hop_limit_certifies_nothing() { + let finite = |hops: usize| { + Some(Reach::Finite(Advert { + seqno: 0, + metric: 1, + down_only: false, + rtt: None, + hops: (1..=hops as Id).collect(), + })) + }; + let item = Item { + seed: 0, + epoch: None, + since: 1, + }; + let (narrow, wide) = (1, 2); + let mut router: Router = Router::new(99, 1); + router.connect(narrow, Link::default()).unwrap(); + router.connect(wide, Link::default()).unwrap(); + router.asks(narrow, p("live/a")).unwrap(); + router.route(narrow, 7, finite(2)); + router.batch(narrow, 7, vec![(p("live/a/x"), Some(item))], Some(1), 0); + router.route(wide, 7, finite(MAX_HOPS - 2)); + router.batch(wide, 7, vec![(p("live/b/y"), Some(item))], Some(1), 0); + assert_eq!(router.shows(7, &p("live/b/y")), Some(true)); + + router.route(wide, 7, finite(MAX_HOPS - 1)); + assert_eq!( + router.shows(7, &p("live/b/y")), + Some(true), + "one hop more moves nothing" + ); + router.route(wide, 7, finite(MAX_HOPS)); + assert_eq!( + router.shows(7, &p("live/b/y")), + None, + "the route crossed as many nodes as one may" + ); + assert_eq!(router.shows(7, &p("live/a/x")), Some(true)); +} + /// A fresh claim arrives only on a stream that certifies nothing, while an /// older floor on another stream proves it absent. The merge rule trusts the /// floor, so the claim stays hidden until the certifying neighbor refreshes From 587c135ede01891d2fb5ced0d5eb1620683ac483 Mon Sep 17 00:00:00 2001 From: Luke Curley Date: Wed, 11 Nov 2026 09:06:55 -0800 Subject: [PATCH 17/17] test(net): a change of hops alone lets go of no claim Co-Authored-By: Claude --- rs/moq-net/src/route/tests/handoff.rs | 38 +++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/rs/moq-net/src/route/tests/handoff.rs b/rs/moq-net/src/route/tests/handoff.rs index f76629eeadc..1db1d141593 100644 --- a/rs/moq-net/src/route/tests/handoff.rs +++ b/rs/moq-net/src/route/tests/handoff.rs @@ -1439,3 +1439,41 @@ fn a_restarted_floorless_route_drops_what_it_no_longer_carries() { assert_eq!(revivals(&sim.events), 0); sim.check().unwrap(); } + +/// Relay 4 hears origin 7's claims from relay 0, which certifies them all, and from +/// relay 3, which asked only for `b`. While 4's own distance sets 0 aside, 0 moves +/// between two equal routes and says so. That change of hops moves no certifier, so +/// 4 lets go of nothing, where pruning on it lost the root claim for good. +#[test] +fn a_change_of_hops_alone_lets_go_of_no_claim() { + let (origin, other) = (6, 7); + let mut sim = Sim::new(8); + sim.join(other, 4, 1); + sim.join(other, 5, 1); + sim.join(origin, 3, 1); + sim.join(origin, 2, 1); + sim.join(0, 1, 1); + sim.link(0, 2, SimLink::cost(3), SimLink::cost(1)); + sim.join(0, 3, 1); + sim.join(0, 4, 1); + sim.link(1, 2, SimLink::cost(2), SimLink::cost(1)); + sim.join(2, 3, 1); + sim.join(2, 5, 1); + sim.link(3, 4, SimLink::cost(1), SimLink::cost(2)); + sim.originate(origin, 7, 0); + sim.announce(origin, "", 0, None); + sim.originate(other, 8, 0); + sim.announce(other, "", 0, None); + sim.watch(3, "b"); + assert!(sim.run()); + assert_eq!(sim.shows(4, 7, ""), Some(true)); + + let hops = sim.stats.hop_updates; + sim.disconnect(origin, 3); + assert!(sim.run()); + assert!(sim.stats.hop_updates > hops, "a route changed its hops alone"); + assert_eq!(sim.shows(4, 7, ""), Some(true)); + sim.disconnect(2, 3); + assert!(sim.run()); + assert_eq!(sim.shows(4, 7, ""), Some(true)); +}