ci: model-sync checks (models track the code)

.github/workflows/model-sync.yml

@@ -0,0 +1,43 @@
+name: Model sync
+
+# Models track the code: a PR that changes code a TLA+ model covers
+# (verification/model-map.toml) updates the model in the same PR, and every
+# lifecycle trace event the code records is replayed by its trace spec, and
+# every model is checked against real runs (or explicitly allowlisted).
+# See docs/TESTING.md (verification layers) and verification/tla/README.md.
+on:
+  pull_request:
+    branches: ["main"]
+    # labeled/unlabeled/edited: adding `no-model-change` or the
+    # `Model: no change because ...` line re-runs the check.
+    types: [opened, synchronize, reopened, labeled, unlabeled, edited, ready_for_review]
+  merge_group:
+  push:
+    branches: ["main"]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: model-sync-${{ github.event.pull_request.number || github.sha }}
+  cancel-in-progress: true
+
+jobs:
+  model-sync:
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: Self-tests
+        run: python3 -m unittest scripts/tests/test_model_sync.py
+      - name: Every trace event is mapped
+        run: python3 scripts/check-model-sync.py events
+      - name: Every model is trace-validated (or allowlisted), coverage floors hold
+        run: python3 scripts/check-model-sync.py models
+      # On merge_group and push the script passes: the pull_request run
+      # already enforced it (labels are not visible in the merge queue).
+      - name: Modelled code changes update their model
+        if: github.event_name != 'push'
+        run: python3 scripts/check-model-sync.py paths

CHANGELOG.md

@@ -26,6 +26,13 @@
   console in every binary, targeted at 0.9) with tiers and target versions, and the OTP features Spawned will
   not add as non-goals; the comparison is in
   `docs/research/otp-elixir-gleam.md`.
+- CI: model-sync checks. A `model-sync` job fails a PR that changes code a TLA+
+  model covers (`verification/model-map.toml`) without touching that model,
+  unless it carries the `no-model-change` label and a `Model: no change because
+  <reason>` line. Every lifecycle trace event kind must map to a trace-spec
+  action; every model must be trace-validated or allowlisted as TLC-only with
+  a tracking item (Coordinator, Lifecycle, DeferredReplies, DeferredJobs);
+  per-model trace coverage has a floor that may only go up.
 - Tests: coverage follow-ups. `restart_modes_distinguish_normal_shutdown_and_panic`
   now sends a real `Normal` exit; a per-PR `MCSupervisionTemporary` TLC
   configuration makes `TemporaryStartsOnce` non-vacuous, with a negative

ROADMAP.md

@@ -318,6 +318,16 @@ without each other's findings), containing:
    benchmark against main; anything costly is opt-in.
 8. **A client mapping:** the Ethrex and Ethlambda call sites it changes.
 
+Models track the code. A PR that changes modelled behaviour updates the model
+in the same PR; drift is a bug. The `model-sync` CI check enforces it: code
+mapped to a model in `verification/model-map.toml` may not change without
+that model (or the `no-model-change` label and a `Model: no change because
+<reason>` line), every lifecycle trace event must be replayed by its
+trace spec, every model must be trace-validated against real runs or
+allowlisted with a tracking item (TLC-only today: Coordinator, Lifecycle,
+DeferredReplies, DeferredJobs), and per-model trace coverage may only grow
+([model sync](docs/TESTING.md#model-sync)).
+
 **Production arm (rank 5c).** Trace validation checks test runs. After the
 Ethlambda canary, the same invariants (`AtMostOneGeneration`,
 `PublishedIsLive`, `BudgetBounded`, `ReverseShutdown`, and, once the base

docs/TESTING.md

@@ -114,6 +114,7 @@ Status of each layer. "Planned" items are tracked in the
 | Design, any size | TLAPS or Veil | An invariant that fails only for larger configurations | Planned ([verification tools](research/verification-tools.md)) |
 | Spec and code | Trace validation | The implementation doing something the model forbids | Real OneForOne, cohort and nested traces plus invalid-trace and model-mutation controls |
 | Spec and code coverage | Trace coverage (`verification/tla/trace_coverage.py`) | Model actions, states and transitions no test ever reaches | Report on every PR (actions covered by the dedicated trace tests may not regress); whole test suite weekly. See [trace coverage](#trace-coverage) |
+| Spec and code in sync | `scripts/check-model-sync.py`, `verification/model-map.toml` | A PR changing modelled code without its model; a trace event no trace spec replays; a model no real run is checked against; trace coverage going down | `model-sync` job on every PR. See [model sync](#model-sync) |
 | Primitives | Loom | Atomic and memory-ordering bugs in cancellation, ready gate and wakeups | In CI; expand to reply slots and mailbox publication versus shutdown |
 | Whole runtime, deterministic | Simulation backend for `spawned-rt::tasks` (random, PCT, bounded DFS) | Async races, replayed from a seed with virtual time | In CI (`sim` job, [simulated suites in CI](#simulated-suites-in-ci)) |
 | Resource stability | Soak tests | Memory, file descriptors, threads, tasks and registry entries growing over hours of actor churn and restarts | Planned |
@@ -1125,6 +1126,59 @@ feature that compiles a mutated line before treating it as a gap. Code inside
 `macro_rules!` bodies is not mutated at all, so keep lifecycle code out of
 single-use macros.
 
+### Model sync
+
+Models track the code: a PR that changes behaviour a TLA+ model specifies
+updates the model in the same PR, and drift is a bug. The `model-sync` job
+(`.github/workflows/model-sync.yml`) checks four things mechanically.
+
+- **Paths.** `verification/model-map.toml` maps code to the models that
+  cover it (for example `actor_cleanup.rs`, `link.rs`, `monitor.rs` and the
+  actor loops to `Lifecycle`; `supervision.rs` to `Supervision`, `Cohorts`
+  and `NestedSupervision`; `system.rs` to `Coordinator`). If a PR changes a
+  mapped file but none of its models (the model, its MC configurations,
+  inductive or coverage modules, or trace spec; a comment-only model edit
+  does not count, and one covering model is enough), the job fails. Changes to
+  comments only, or only inside a `#[cfg(test)] mod` block, are exempt (the
+  file's code outside test modules must be unchanged, so removing
+  `#[cfg(test)]` is not exempt); when the script cannot tell, it requires
+  the waiver. The waiver is the
+  `no-model-change` label AND a PR body line `Model: no change because
+  <reason>`. In the merge queue the step passes, which is sound because
+  `model-sync` is a required check on the PR.
+- **Trace events.** Every action name the code can record with the
+  `lifecycle-trace` feature (the string literal, or the literals of an
+  `if .. else` chain, passed to each emitter listed in the map, such as
+  `Event::new`, `Event::sup` and `TreeEvent::new`) must be an `e.a = "..."` arm of its trace spec, or be
+  declared in the map as translated by `trace_check.py` or rejected on
+  purpose (`Unmodelled`). A non-literal action name, an event struct with no
+  map entry, or a cohort event filter that differs from `TraceCohorts.tla`
+  fails. Warnings list spec arms no code emits and model actions no trace
+  spec takes (except those declared unlogged, such as `WindowExpire`). The
+  event names are strings, not an enum, so this is a source scan rather than
+  a compile-time `match`; the mapping it checks lives in TLA+.
+- **Models with trace validation.** Every model in `verification/tla` needs
+  a map entry and trace validation, checked statically: a `Trace*.tla` that
+  extends the model, is named in `trace_check.py`, and has arms that events
+  the code emits reach (the `tla-traces` job replays the recorded traces). A
+  model checked by TLC alone can drift from the code unnoticed, so it fails
+  unless it has a `tlc_only` allowlist entry with a reason and a tracking
+  item. `check-model-sync.py models` prints the current list.
+- **Coverage floors.** Each trace-validated model has a `coverage_floor`: the
+  action keys the dedicated trace tests cover in
+  `verification/tla/coverage-baseline.json` (Supervision 36 of 40, Cohorts
+  40 of 46, Nested 11 of 11). The `tla` job already fails when a baseline key
+  stops being covered; this check fails when the baseline shrinks below the
+  floor, so coverage only grows. Raise the floor when coverage grows.
+
+```bash
+python3 scripts/check-model-sync.py events
+python3 scripts/check-model-sync.py models                      # inventory: trace validation and coverage floors
+python3 scripts/check-model-sync.py paths                       # this branch against origin/main
+python3 scripts/check-model-sync.py paths --pr 123              # with that PR's labels and body
+python3 -m unittest scripts/tests/test_model_sync.py            # self-tests and negative controls
+```
+
 ## Planted-bug sensitivity
 
 Mutation testing breaks one operator at a time. To measure whether the stack