docs: trim agent instructions and bump quest to 93c9c2ef

.claude/skills/quest-recurring/SKILL.md

@@ -1,6 +1,6 @@
 ---
 name: quest-recurring
-description: Plan a quest that repeats, such as a periodic audit or a release cut. Use when the user invokes /quest-recurring or wants the same work redone each milestone or release.
+description: Plan a quest that repeats, such as a periodic audit, a release cut, or a yearly filing. Use when the user invokes /quest-recurring or wants the same work redone each milestone, release, or calendar period.
 ---
 
 Run `quest skill recurring` and follow its output.

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

@@ -27,7 +27,7 @@ just rs tla moq-net/verify/failover/FailoverChain.tla -config rs/moq-net/verify/
 just rs tla moq-net/verify/failover/FailoverChain.tla -config rs/moq-net/verify/failover/EndedRelay.cfg
 ```
 
-The first checks every rule with `E` failing over between `A` and `B`, one death, and one switch per relay, with a client that stays, so a deadlock is a playback hang: about 2.0M states. The second lets the client leave at any point, so a deadlock is a relay still holding a copy after it left; leaving is always possible there, which is why it cannot stand in for the first: about 2.2M states. Each takes under 30 seconds on 24 cores and passes at the sync commit. The third adds `B`'s route through `A`, so the route also moves at the middle hop: it fails at the sync commit on the open finding below at depth 31, after about 50M distinct states and 11 minutes on 8 workers.
+The first checks every rule with `E` failing over between `A` and `B`, one death, and one switch per relay, with a client that stays, so a deadlock is a playback hang: about 2.0M states. The second lets the client leave at any point, so a deadlock is a relay still holding a copy after it left; leaving is always possible there, which is why it cannot stand in for the first: about 2.2M states. Each takes seconds and passes at the sync commit. The third adds `B`'s route through `A`, so the route also moves at the middle hop: it fails at the sync commit on the open finding below at depth 31, after about 50M distinct states and minutes.
 
 ## Open finding: an ended relay cannot move a fetch off a dying route
 
@@ -42,11 +42,11 @@ The model lets a fetch reach the serving route whenever that route lives, after
 
 ## Reading a failure
 
-A counterexample is a path through the model, not yet a bug. Replay it on the real stack in `rs/moq-net/tests/integration/failover_chain.rs`: relays are `origin::Producer`s linked over the memory transport (`link`, `priced_link`, a cost to make a route win), a relay or hop dies by aborting its sessions, a group read past a failed copy is what makes `Recover` fetch, and time is simulated. If the code 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, and pin it as a `residual_*` test with its own config so the others still pass. Do not weaken a rule, add a constraint, or shrink the bounds until the check passes.
+Follow Reading a failure in `rs/moq-net/verify/README.md`. Replay the path on the real stack in `rs/moq-net/tests/integration/failover_chain.rs`: relays are `origin::Producer`s linked over the memory transport (`link`, `priced_link`, a cost to make a route win), a relay or hop dies by aborting its sessions, a group read past a failed copy is what makes `Recover` fetch, and time is simulated. Pin a path the code follows as a `residual_*` test with its own config so the others still pass.
 
 ## Coverage
 
-Sync commit: `88572c583e2f64c7f5fc9bfa59df90706308497e`. Run `git log 88572c583e.. -- rs/moq-net/src/model/resume.rs rs/moq-net/src/model/front.rs rs/moq-net/src/model/origin.rs rs/moq-net/src/model/track.rs` 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: `88572c583e2f64c7f5fc9bfa59df90706308497e`. Run `git log 88572c583e.. -- rs/moq-net/src/model/resume.rs rs/moq-net/src/model/front.rs rs/moq-net/src/model/origin.rs rs/moq-net/src/model/track.rs` to see what changed since. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function.
 
 | Code | Model |
 | --- | --- |

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

@@ -30,9 +30,7 @@ just rs tla moq-net/verify/reconnect/Handover.tla -config rs/moq-net/verify/reco
 just rs tla moq-net/verify/reconnect/Handover.tla -config rs/moq-net/verify/reconnect/OfflineWhileServing.cfg
 ```
 
-The first checks every rule but the two with open findings, over four sessions: about 1.2M distinct states, under a minute on 32 cores. The second checks the same rules under `Restart::Wait` over three sessions: about 240k states. Both pass at the sync commit. The last two fail at the sync commit, each on its finding below, within seconds. `just test tla rs/moq-net/verify/reconnect` runs every config here, as Nightly does, and fails if a config with an `\* Open finding:` line passes. The `VIEW` counts states that differ only in what nothing reads again as one: a closed session's details unless it is still the live one, a deadline of a phase the policy left, and where no dial is headed.
-
-Read a counterexample with `/statechart`, passing it the spec, a config, and `Handover.view.ts`, which labels what the handle reports, what the policy holds, and each step as the event that happens.
+The first checks every rule but the two with open findings, over four sessions: about 1.2M distinct states, under a minute. The second checks the same rules under `Restart::Wait` over three sessions: about 240k states. Both pass at the sync commit. The last two fail at the sync commit, each on its finding below, within seconds. `just test tla rs/moq-net/verify/reconnect` runs every config here, as Nightly does, and fails if a config with an `\* Open finding:` line passes. The `VIEW` counts states that differ only in what nothing reads again as one: a closed session's details unless it is still the live one, a deadline of a phase the policy left, and where no dial is headed.
 
 ## Open findings
 
@@ -46,11 +44,11 @@ Read a counterexample with `/statechart`, passing it the spec, a config, and `Ha
 
 ## Reading a failure
 
-A counterexample is a path through the model, not yet a bug. Replay it on the policy with the helpers in `reconnect/tests.rs` (`next`, `handshake`, `on_fallback`, `probe`, `connected`, `failed`, `probed`, a server's `drain().send(..)`), one call per step, on the simulated clock. A path through `Shared` needs `moq-tokio`'s connection tests instead. If the code 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.
+Follow Reading a failure in `rs/moq-net/verify/README.md`. Replay the path on the policy with the helpers in `reconnect/tests.rs` (`next`, `handshake`, `on_fallback`, `probe`, `connected`, `failed`, `probed`, a server's `drain().send(..)`), one call per step, on the simulated clock. A path through `Shared` needs `moq-tokio`'s connection tests instead.
 
 ## Coverage
 
-Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07.. -- rs/moq-net/src/reconnect.rs rs/moq-net/src/reconnect/ rs/moq-tokio/src/connection.rs` 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. `just check` fails when a function or type the table names no longer exists in its file (`sh/coverage-tables.py`), so each Code cell starts with a repo-relative path, then the symbols in it.
+Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07.. -- rs/moq-net/src/reconnect.rs rs/moq-net/src/reconnect/ rs/moq-tokio/src/connection.rs` to see what changed since. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function.
 
 | Code | Model |
 | --- | --- |

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

@@ -28,21 +28,21 @@ just rs tla moq-net/verify/resume/ResumeReader.tla
 just rs tla moq-net/verify/resume/ResumeReader.tla -config rs/moq-net/verify/resume/ThreeRoutes.cfg
 ```
 
-The first checks every rule over two routes, three groups, two switches, and a reader holding each group until it finishes it: about 14.3M distinct states, three minutes on 32 cores. The second trades a group for a third route, so a route can come up after another failed: about 7.1M states, under two minutes. Both pass at the sync commit. `just test tla rs/moq-net/verify/resume` runs every config here, as Nightly does, and fails if a config with an `\* Open finding:` line passes.
+The first checks every rule over two routes, three groups, two switches, and a reader holding each group until it finishes it: about 14.3M distinct states, in minutes. The second trades a group for a third route, so a route can come up after another failed: about 7.1M states, in minutes. Both pass at the sync commit. `just test tla rs/moq-net/verify/resume` runs every config here, as Nightly does, and fails if a config with an `\* Open finding:` line passes.
 
-`Chart.cfg` is for `/statechart` only: a story (`Story`) small enough to draw whole, where the reader switches to a route that holds an older group and asks it for that group. Pass it the spec, `Chart.cfg`, and `ResumeReader.view.ts`, which labels which route serves, what the reader has, and each step as what happens to a route or the reader. For a counterexample, pass the config that broke instead.
+`Chart.cfg` is a story (`Story`) small enough to draw whole, where the reader switches to a route that holds an older group and asks it for that group.
 
 ## Open findings
 
 None at the sync commit.
 
 ## Reading a failure
 
-A counterexample is a path through the model, not yet a bug. Replay it as a test in `model/resume.rs`'s `mod test`, one call per step: `received_copy` for a route, `routes.serve(copy.consume())` for a switch, `write` for a landing group, `finish()` for a declared end, `abort(..)` for a route failing, and `drain` or `poll_recv_group` for a poll. If the code 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, and pin it as a `residual_*` test with its own config, marked with an `\* Open finding:` line, so the others still pass. Do not weaken a rule, add a constraint, or shrink the bounds until the check passes.
+Follow Reading a failure in `rs/moq-net/verify/README.md`. Replay the path as a test in `model/resume.rs`'s `mod test`, one call per step: `received_copy` for a route, `routes.serve(copy.consume())` for a switch, `write` for a landing group, `finish()` for a declared end, `abort(..)` for a route failing, and `drain` or `poll_recv_group` for a poll. Pin a path the code follows as a `residual_*` test with its own config, marked with an `\* Open finding:` line, so the others still pass.
 
 ## Coverage
 
-Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07.. -- rs/moq-net/src/model/resume.rs rs/moq-net/src/model/track.rs` 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. `just check` fails when a function or type the table names no longer exists in its file (`sh/coverage-tables.py`), so each Code cell starts with a repo-relative path, then the symbols in it.
+Sync commit: `103052ed074a87f00269ecb0d639905482ecfb6f`. Run `git log 103052ed07.. -- rs/moq-net/src/model/resume.rs rs/moq-net/src/model/track.rs` to see what changed since. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function.
 
 | Code | Model |
 | --- | --- |

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

@@ -36,15 +36,15 @@ just test route-key-model
 just rs tamarin moq-net/verify/route-key/RouteKey.spthy -D=NO_SIDE
 ```
 
-The first proves the model and checks every variant's `Breaks:` line, in about ten seconds; Nightly runs it. The second proves one variant. To read a counterexample, run `nix shell --inputs-from . nixpkgs#tamarin-prover --command tamarin-prover interactive rs/moq-net/verify/route-key/` and open the falsified lemma.
+The first proves the model and checks every variant's `Breaks:` line, in seconds; Nightly runs it. The second proves one variant. To read a counterexample, run `nix shell --inputs-from . nixpkgs#tamarin-prover --command tamarin-prover interactive rs/moq-net/verify/route-key/` and open the falsified lemma.
 
 ## Reading a failure
 
 A falsified lemma is an attack path, not yet a bug. Check that each rule it fires matches the code: the transport bindings below for the secret, `proof.rs` for the message. If the code cannot take a step, fix the model. If it can, the signed transcript is wrong: fix it in Rust, JS, and the draft together, and keep `a_proof_matches_the_js_transcript` (Rust) and `route_key.test.ts` (JS) agreeing. Do not add a restriction or drop an attacker rule until a lemma verifies.
 
 ## Coverage
 
-Sync commit: `23898b48f46cb54da19007279504b2b6ecdf80cf`. Run `git log 23898b48f4.. -- rs/moq-net/src/route/proof.rs js/net/src/lite/route_key.ts` and the files below to see what changed since. After a change to a covered function, mirror it in the model, rerun `just test route-key-model`, and move the sync commit forward only once the model describes the code at the new commit.
+Sync commit: `23898b48f46cb54da19007279504b2b6ecdf80cf`. Run `git log 23898b48f4.. -- rs/moq-net/src/route/proof.rs js/net/src/lite/route_key.ts` and the files below to see what changed since. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function, rerunning `just test route-key-model`.
 
 | Code | Model |
 | --- | --- |

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

@@ -41,33 +41,31 @@ just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/rout
 just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/Chord.cfg -simulate num=1000 -depth 600
 ```
 
-Times are TLC 1.8.0 on Java 21 with `-workers 4` at `nice -n 19`, on a 24-core host under load from other work.
+Times are with `-workers 4`.
 
 | Config | Mesh | Bounds | Distinct states | Run |
 | --- | --- | --- | --- | --- |
-| `RouteHandoff.cfg` | The origin and two relays in a triangle. | 2 claim changes, 2 session changes, 1 collection | 24,192,399 | 39 min |
-| `Behind.cfg` | The origin behind relay 1, which sits in a triangle with relays 2 and 3. | 1 claim change, 1 session change | 9,384,796 | 25 min |
-| `BehindDear.cfg` | The same, with relay 3 nearer the origin than relay 2. | 1 claim change, 1 session change | 17,863,476 | 61 min |
-| `Line.cfg` | The origin, three relays, and a watching client in a line; also checks `Converges`. | 2 claim changes, 1 session change, 1 collection | 1,543,073 | 13 min |
-| `Ring.cfg` | The origin and three relays in a ring. | 2 claim changes, 1 session change | 18,437,833 | 61 min |
-| `Chord.cfg` | A publishing client on a ring of five relays with a chord, and two watching clients. Simulated: `num` counts behaviours per worker. | 2 claims, 4 claim changes, 4 session changes, 2 collections | 4,000 behaviours, 4.6M states | 9 min |
+| `RouteHandoff.cfg` | The origin and two relays in a triangle. | 2 claim changes, 2 session changes, 1 collection | 24,192,399 | tens of minutes |
+| `Behind.cfg` | The origin behind relay 1, which sits in a triangle with relays 2 and 3. | 1 claim change, 1 session change | 9,384,796 | tens of minutes |
+| `BehindDear.cfg` | The same, with relay 3 nearer the origin than relay 2. | 1 claim change, 1 session change | 17,863,476 | an hour |
+| `Line.cfg` | The origin, three relays, and a watching client in a line; also checks `Converges`. | 2 claim changes, 1 session change, 1 collection | 1,543,073 | ten minutes |
+| `Ring.cfg` | The origin and three relays in a ring. | 2 claim changes, 1 session change | 18,437,833 | an hour |
+| `Chord.cfg` | A publishing client on a ring of five relays with a chord, and two watching clients. Simulated: `num` counts behaviours per worker. | 2 claims, 4 claim changes, 4 session changes, 2 collections | 4,000 behaviours, 4.6M states | ten minutes |
 
 All pass at the sync commit, and `just test tla rs/moq-net/verify/route` runs them all, as Nightly does, simulating `Chord.cfg` as its `Simulate:` line says. Run them last, one at a time. First run what answers in seconds:
 
-- `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.
+- `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 seconds in release.
 - TLC's simulation mode, which samples runs the exhaustive bounds do not reach. The config's `MaxRev`, `MaxFlaps`, and `MaxCollects` still bound a simulated run, so raise them in a copy of the config first, such as three session changes, two claim changes, and a collection, then add `-simulate num=3000 -depth 150`.
 
 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 labels any mesh and assumes equal costs.
-
 ## Reading a failure
 
-A counterexample is a path through the model, not yet a bug. Replay it on the router with `Sim` (`hold`, `deliver`, `deliver_ack`, `disconnect`, `collect`), one call per step. If the router does not follow the path, the model is wrong: fix the model to match the code. If it does, report the path and the rule in the code's words. Do not weaken a rule, add a constraint, or shrink the bounds until the check passes.
+Follow Reading a failure in `rs/moq-net/verify/README.md`. Replay the path on the router with `Sim` (`hold`, `deliver`, `deliver_ack`, `disconnect`, `collect`), one call per step.
 
 ## Coverage
 
-Sync commit: `caa3dd8926f16fbed15760ab22298085df73b655`. Run `git log caa3dd8926.. -- 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. `just check` fails when a function or type the table names no longer exists in its file (`sh/coverage-tables.py`), so each Code cell starts with a repo-relative path, then the symbols in it.
+Sync commit: `caa3dd8926f16fbed15760ab22298085df73b655`. Run `git log caa3dd8926.. -- rs/moq-net/src/route/` to see what changed since. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function.
 
 | Code | Model |
 | --- | --- |