test(net): Apalache reads the route model but cannot step it

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

@@ -1,6 +1,6 @@
 ---
 name: verify-route
-description: Model-check the lite-07 route rule (`rs/moq-net/verify/route/RouteHandoff.tla`, the rule the routes epic's Plan item 27 picked, as `rs/moq-net/src/route/tests/paths.rs` prototypes it) with TLA+. Use when a change touches route paths, the DEAD message for a closed session, holds, the doubt and its timer, forgetting dead hops, routes per prefix and scoped streams, the newest-floor views, what a reader is shown, or where a request goes, or when a routing bug needs every message ordering checked rather than a random sweep.
+description: Model-check the lite-07 route rule (`rs/moq-net/verify/route/RouteHandoff.tla`, the rule the routes epic's Plan item 27 picked, as `rs/moq-net/src/route/tests/paths.rs` prototypes it) with TLA+. Use when a change touches route paths, the DEAD message for a closed session, holds, the doubt and its timer, forgetting dead hops, routes per prefix and scoped streams, the newest-floor views, what a reader is shown, or where a request goes, or when a routing bug needs every message ordering checked rather than a random sweep. Also covers `RouteClaims.tla`, the claims model with no paths that it refines, where Apalache proves the claim rules for runs of any length.
 ---
 
 # Verify the route rule
@@ -27,6 +27,12 @@ Each rule is an INVARIANT; the harm says why it matters.
 | `Budget` | From one quiet point to the next, the messages sent stay within 4 each way over each configured session per prefix and per claim, for each external change. | One change sets off announce spam, or routing never goes quiet. |
 | `RequestsLoopFree` | A request never loops. | Only `Loop.cfg` checks it, as an open finding. |
 
+## Runs of any length
+
+TLC checks bounded runs. `RouteClaims.tla` keeps only what the claim rules need, with no paths: every step, any relay's routes may come and go, and claims in flight may arrive in any order, again, or never. Each config's `RefinesClaims` checks that every step of `RouteHandoff.tla` is a step there, and its `Truthful`, `NoRevival`, `NoFalseEnd`, and `NoRegression` are this model's under that mapping. Apalache checks that `IndInv` holds at `Init` (`RouteClaimsInit.cfg`) and that every step from a state where it holds keeps it (`RouteClaims.cfg`), so those four rules hold for any number of revisions, sessions, and route changes.
+
+What stays bounded: the nodes and claims the configs name, and the two claims in flight the step check starts from. The step check keeps one relay's state with five neighbours; one relay's step stands for every relay's because relays share only the claims in flight, and what a relay sends is its own view. That argument, and that a longer history than the floors name changes nothing, are not checked. The loop rules (`SimplePaths`, `LoopsAreStale`, `StaleIsChased`) have no such proof yet: [the loop rules quest](/quest/m1/route-loops.md).
+
 No config checks a liveness property: `Spec` has no fairness, so TLC does not show that a hold ends. That one does is an argument over what TLC does check. `Budget` bounds the messages a burst sends, each delivery takes one message off a queue, and a doubt starts only at a close or a delivery, so a burst is a finite number of steps. A delivery is enabled while a queue holds a message and a timer may fire once no news about its node is in flight, so a burst left alone reaches the state with nothing in flight and no doubt. `QuietIsSettled` says no relay holds there.
 
 What the timer costs, as the configs show it: fired late, it costs only the wait, and every rule holds (`RouteHandoff.cfg`). Fired early, a stale route can return, as with no doubt at all, and nothing else breaks (`Early.cfg`, which passes without `NoStaleReturn` and fails it within seconds with it). With two failures a stale route can return whatever the timer (`Twice.cfg` drops `NoStaleReturn`), and `StaleIsChased` is the bound.
@@ -36,14 +42,15 @@ What the timer costs, as the configs show it: fired late, it costs only the wait
 ```sh
 quest gate just rs tla moq-net/verify/route/RouteHandoff.tla
 quest gate just rs tla moq-net/verify/route/RouteHandoff.tla -config rs/moq-net/verify/route/Ring.cfg
+quest gate just test tla rs/moq-net/verify/route/RouteClaims.cfg
 quest gate just test tla rs/moq-net/verify/route
 ```
 
-`just test tla rs/moq-net/verify/route` runs every config, as Nightly does, simulating each one with a `Simulate:` line and expecting `Loop.cfg` to break. Times are with `-workers 4`. `Patient` is TRUE unless the table says otherwise.
+`just test tla rs/moq-net/verify/route` runs every config, as Nightly does, simulating each one with a `Simulate:` line, checking each with an `Apalache:` line through Apalache, and expecting `Loop.cfg` to break. Every TLC config but `Loop.cfg` also checks `RefinesClaims`, which costs about two thirds more time. Times are with `-workers 4`. `Patient` is TRUE unless the table says otherwise.
 
 | Config | Mesh | Bounds | Distinct states | Run |
 | --- | --- | --- | --- | --- |
-| `RouteHandoff.cfg` | The publisher behind relay 1, in a triangle with relays 2 and 3. | 1 claim change, 1 session change | 407,240 | a minute or two |
+| `RouteHandoff.cfg` | The publisher behind relay 1, in a triangle with relays 2 and 3. | 1 claim change, 1 session change | 407,240 | five minutes |
 | `Early.cfg` | The same, with a timer that fires at any moment. | 1 claim change, 1 session change | 4,178,590 | ten minutes |
 | `Twice.cfg` | The same, where two sessions close, as when relay 1 dies. Simulated: `num` counts behaviours per worker. | 1 claim change, 2 session changes | 40,000 behaviours, 4.0M states | a few minutes |
 | `Ring.cfg` | The publisher and three relays in a ring, with a timer that fires at any moment. | 1 claim change, 1 session change | 426,409 | a minute or two |
@@ -52,6 +59,8 @@ quest gate just test tla rs/moq-net/verify/route
 | `Dead.cfg` | Two relays behind a relay whose only uplink asks for `"a"` alone, one with a dear session of its own to the publisher. Simulated. | 3 claim changes, 1 session change | 40,000 behaviours, 4.8M states | ten minutes |
 | `Blind.cfg` | A relay whose nearest neighbour asks for `"a"` alone, and a farther one knows everything. Simulated. | 2 claim changes, 1 session change | 40,000 behaviours, 4.8M states | ten minutes |
 | `Loop.cfg` | The publisher with a session to each of three relays in a triangle, all closing. Open finding: `RequestsLoopFree` breaks. | 3 session changes | 979,474 when it breaks | a few minutes |
+| `RouteClaims.cfg` | Apalache: one step of `RouteClaims.tla` from any state where `IndInv` holds, for one relay with five neighbours. | 2 claims in flight | none | twelve minutes |
+| `RouteClaimsInit.cfg` | Apalache: `IndInv` holds at `Init`, with five relays. | none | none | seconds |
 
 Run them last, one at a time. First run what answers in seconds: the prototype's tests (`just rs test -p moq-net --lib -E 'test(/route::tests::(paths|compare|copies)/)'`), then TLC's simulation mode with raised bounds in a copy of a config, such as `-simulate num=3000 -depth 150`.
 
@@ -61,7 +70,7 @@ Follow Reading a failure in `rs/moq-net/verify/README.md`. Replay the path on th
 
 ## Coverage
 
-Sync commit: `d3b6c2573a30541402d396f8080488646f673594`. Run `git log d3b6c2573a.. -- rs/moq-net/src/route/tests/paths.rs` to see what changed since. The model describes the prototype, extended with a route per prefix and with dead hops kept until their timer fires; `route::Router` does not run this rule yet. `Relay::collect` forgets a dead hop as soon as no route names it, so `NoStaleReturn` covers the rule the router is to run, not the prototype's. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function.
+Sync commit: `d3b6c2573a30541402d396f8080488646f673594`. Run `git log d3b6c2573a.. -- rs/moq-net/src/route/tests/paths.rs` to see what changed since. The model describes the prototype, extended with a route per prefix and with dead hops kept until their timer fires; `route::Router` does not run this rule yet. `Relay::collect` forgets a dead hop as soon as no route names it, so `NoStaleReturn` covers the rule the router is to run, not the prototype's. Follow Coverage in `rs/moq-net/verify/README.md` after a change to a covered function. `RouteClaims.tla` repeats `Know`, `ShownNow`, and the reader's events in `Events`: a change to them changes it too, and `RefinesClaims` fails until it does.
 
 | Code | Model |
 | --- | --- |

flake.nix

@@ -602,6 +602,10 @@
           # C++ dependency build out of the default shell and flake checks.
           moxygen = pkgs.callPackage ./nix/moxygen.nix { };
 
+          # `just rs tla` and `just rs apalache`: nixpkgs has no Apalache. Kept
+          # out of the dev shell like the TLC the recipes fetch themselves.
+          apalache = pkgs.callPackage ./nix/apalache.nix { };
+
           runner-userns-profile = import ./nix/runner/unshare.nix { inherit pkgs; };
 
           # Nightly's `just rs send-depth` proves native Send futures on it.

nix/apalache.nix

@@ -0,0 +1,39 @@
+{
+  lib,
+  stdenvNoCC,
+  fetchurl,
+  makeWrapper,
+  unzip,
+  jdk21_headless,
+}:
+# Apalache, the symbolic TLA+ model checker, which nixpkgs does not package.
+# `share/tla` holds its `Apalache.tla`, whose folds TLC also evaluates, so a
+# spec checked by both tools extends it under TLC too.
+stdenvNoCC.mkDerivation (finalAttrs: {
+  pname = "apalache";
+  version = "0.63.0";
+  src = fetchurl {
+    url = "https://github.com/apalache-mc/apalache/releases/download/v${finalAttrs.version}/apalache-${finalAttrs.version}.tgz";
+    hash = "sha256-p1bpavJJvzPNdilmeklHLLJqyCJ8SFg9oTm0FINNWd8=";
+  };
+  nativeBuildInputs = [
+    makeWrapper
+    unzip
+  ];
+  installPhase = ''
+    runHook preInstall
+    install -Dm444 lib/apalache.jar $out/lib/apalache.jar
+    install -Dm555 bin/apalache-mc $out/bin/apalache-mc
+    wrapProgram $out/bin/apalache-mc --set JAVA_HOME ${jdk21_headless} --prefix PATH : ${jdk21_headless}/bin
+    mkdir -p $out/share/tla
+    unzip -p lib/apalache.jar tla2sany/StandardModules/Apalache.tla > $out/share/tla/Apalache.tla
+    runHook postInstall
+  '';
+  meta = {
+    description = "Symbolic model checker for TLA+";
+    homepage = "https://apalache-mc.org";
+    license = lib.licenses.asl20;
+    mainProgram = "apalache-mc";
+    platforms = lib.platforms.unix;
+  };
+})

quest/m0/ci/tlc-cost.md

@@ -44,9 +44,6 @@ Decided 2026-11-12 (maintainer, /quest-plan):
   Java override in `CommunityModules-deps.jar`, which nixpkgs does not
   package: take it from a pinned release, put it on TLC's classpath in both
   recipes, and confirm TLC's startup log reports the override loaded.
-  [moq-dev/moq#8564](https://github.com/moq-dev/moq/pull/8564) rewrites
-  `SumOver` as an Apalache fold; whichever lands second keeps one fold for the
-  model.
 - ✅ Add `SYMMETRY` where sound. No config checks a `PROPERTY`, so every one
   checks safety only, which symmetry preserves. A permutation is sound only if
   it fixes every constant the config gives, such as `Links`, `Origin`, or
@@ -68,13 +65,15 @@ Decided 2026-11-12 (maintainer, /quest-plan):
   the `js/*/verify/` READMEs name single configs, and only Nightly runs
   `just test tla` over a directory.
 - Rejected: Apalache, which is no cheaper here and ran out of memory on the
-  route model ([moq-dev/moq#8564](https://github.com/moq-dev/moq/pull/8564));
+  route model ([moq-dev/moq#8564](https://github.com/moq-dev/moq/pull/8564),
+  which now runs it only on the small claims model, `RouteClaims.tla`);
   waiting for the Rust checker, which the m1 quest
   spikes and this complements.
 
-Not decided: the route-inductive work in progress adds a refinement check,
-`RefinesClaims`, to the simulated `Blind.cfg`, where every sampled trace
-re-checks it. Recommended: check a refinement on the smallest exhaustive config
+Not decided: [moq-dev/moq#8564](https://github.com/moq-dev/moq/pull/8564)
+checks a refinement, `RefinesClaims`, on every route config but `Loop.cfg`,
+simulated ones included, which costs each about two thirds more time.
+Recommended: check a refinement on the smallest exhaustive config
 that exercises it, where each distinct state is checked once, unless measuring
 shows the simulated config is cheaper.
 
@@ -90,4 +89,4 @@ Public API: none. Wire: none.
 ## Related
 
 - [A Rust TLA+ checker runs the models locally if it agrees with TLC](/quest/m1/tla-native-checker.md) - a faster engine for the same specs; its TLC baseline moves with this
-- [The route rules hold from any state, not only the runs TLC reaches](/quest/m1/route-inductive.md) - rewrites `SumOver` and adds the refinement check named above
+- [The route model's loop rules hold for runs of any length](/quest/m1/route-loops.md) - adds a second refinement check like the one named above