[unbalancedparentheses]

Models track the code: a PR that changes modelled behaviour updates the TLA+ model in the same PR. Two mechanical checks enforce it, in a new model-sync job (.github/workflows/model-sync.yml, a new file; no existing workflow changed).

1. Paths (scripts/check-model-sync.py paths). verification/model-map.toml maps code to the models covering it (Lifecycle: actor loops, actor_cleanup, link, monitor, child_handle, mailbox*; Supervision/Cohorts/NestedSupervision: supervision.rs, supervision/**; Coordinator: system.rs; DeferredReplies/DeferredJobs: reply/**, */jobs.rs; lifecycle_trace.rs → every traced model). A PR changing a mapped file without touching any covering model (model, MC configs, *Ind, coverage or trace modules) fails, unless:

• the change is comments only or only inside a #[cfg(test)] mod (anything the script cannot classify needs the waiver);
• the PR has the no-model-change label AND a body line Model: no change because <reason>.

It passes on merge_group (the PR run enforced it). It re-runs on labeled/unlabeled/edited.

2. Trace events (scripts/check-model-sync.py events). Every action string the code passes to Event::new/Event::sup/TreeEvent::new (and, once #240 lands, LifeEvent/JobEvent/reply events, pre-configured) must be an e.a = "..." arm of its trace spec, or declared translated (trace_check.py must mention it) or rejected (Unmodelled). It also fails on non-literal action names, an unconfigured *Event struct, or a cohort filter list (COHORT_EVENTS, cohort_trace.rs) that differs from TraceCohorts.tla. Warnings: spec arms no code emits; model Next actions no trace spec takes (except declared unlogged ones: WindowExpire, Deliver). The events are &'static str, not an enum, and the mapping lives in TLA+, so this is a source scan rather than an exhaustive match. Turning them into an enum would rewrite supervision.rs, which conflicts with #240.

3. Models checked against real runs (check-model-sync.py models). Every model in verification/tla needs a map entry and trace validation, meaning a Trace*.tla that trace_check.py runs and that recorded events reach. Otherwise it needs a tlc_only allowlist entry with reason and tracking. TLC-only today: Coordinator (abstract fault model, no events recorded), Lifecycle, DeferredReplies and DeferredJobs (their trace validation is on #240; a warning asks to drop the entries once it merges) and DynamicSupervisor (pre-allowlisted for #245).

4. Coverage floors. coverage_floor per trace-validated model is the number of action keys in coverage-baseline.json: Supervision 36/40, Cohorts 40/46, Nested 11/11. The existing tla job fails when a baseline key is lost. This check fails when the baseline shrinks below the floor, so coverage only grows.

Checked against the #240 and #245 trees with this map unchanged: events and models pass on both. On #240, paths flags system.rs (Coordinator unchanged).

Self-tests: scripts/tests/test_model_sync.py (27 tests: injected unmapped, branch and non-literal events, an unconfigured struct, filter drift, a ghost arm warning; path failures and passes on a temp git repo, covering comment-only and test-module changes, the label and reason pair, merge_group and an Actions event payload). Runs under Python 3.9 (a TOML subset fallback) and in the feature-check unittest discovery.

Docs: TESTING (verification layers row + "Model sync"), verification/tla/README.md, ROADMAP "Verification rule".

model-sync is a required-check candidate. It is not added to the ruleset.

Model: no change because this PR only adds CI checks and docs.

[github-actions]

🤖 Codex Code Review

• [P2] Test-only exemption permits production changes — check-model-sync.py:317. Changed lines are classified independently against each revision’s test-module ranges. Removing #[cfg(test)], or wrapping existing production code in a test module, passes as “tests only.” Both cases change production behavior without requiring a model update or waiver. Require the module’s test-only status to remain unchanged before exempting its contents.

• [P2] Partially dynamic event names bypass validation — check-model-sync.py:466. Collecting literals anywhere within an argument misses dynamic branches. For example, Event::new(if x { "Close" } else { action }, ...) passes even when action contains an unmapped event name. Reject expressions whose possible action values cannot all be established.

All 27 existing self-tests pass; both gaps were reproduced separately.

---

Automated review by OpenAI Codex · gpt-6.1-sol · custom prompt

[github-actions]

🤖 Gemini Code Review

Overall, this is a well-structured and well-tested addition for keeping the TLA+ models, trace specs, and Rust implementation in sync.

A few minor issues and edge cases found in the script and docs:

scripts/check-model-sync.py

1. trace_validation counts translated targets even when their source event is never emitted (lines 597–599)
   In check_events (lines 507–509), translated target actions are only added to produced if the source event is actually emitted by the Rust code (if action in emitted and isinstance(how, dict):).
   In trace_validation, how.get("into", []) is added to emitted unconditionally:

   for action, how in t.get("translated", {}).items():
       if action in emitted and isinstance(how, dict):
           emitted.update(how.get("into", []))

   Without the action in emitted check, once a struct like LifeEvent is defined in lifecycle_trace.rs, Send -> ["Request", "Enqueue"] would make trace_validation report TraceLifecycle.tla as validated by recorded events even if no code emits LifeEvent yet.

2. --base branch divergence vs git show in exempt_change (lines 287–289, 360)
   In check_paths:

   base = args.base or git(root, "merge-base", "origin/main", head).strip()

   When --base is omitted, base is resolved to the merge-base commit. However, if a user passes --base main (or --base origin/main) after main has advanced past the branch point, git diff f"{base}...{head}" diffs against merge-base(base, head), whereas show(root, base, path) reads the file at base. If main modified lines above #[cfg(test)], old_tests line numbers in exempt_change can be offset from the - hunk line numbers in the diff.
   Resolving merge-base even when args.base is provided avoids this mismatch:

   base = git(root, "merge-base", args.base or "origin/main", head).strip()

3. Potential infinite loop in rust_mask on unclosed escaped char literal (lines 210–213)

   elif c == "'":
       if src.startswith("\\", i + 1):
           j = src.find("'", i + 3)
           blank(i + 1, j)
           i = j + 1

   If src.find("'", i + 3) returns -1 (e.g., '\_ in a lifetime/macro token or malformed input), i becomes 0 and loops forever. Guarding with j = n if j < 0 else j (as done for comments and raw strings above) prevents this.

Documentation

4. docs/TESTING.md (line 1132) & scripts/tests/test_model_sync.py (line 1)
   • docs/TESTING.md:1132 states: "The model-sync job (.github/workflows/model-sync.yml) checks two things mechanically." followed by four bullet points (Paths, Trace events, Models checked against real runs, Coverage floors).
   • scripts/tests/test_model_sync.py:1 similarly refers to (both checks) in the module docstring, though it now tests all three subcommands (paths, events, models).

---

Automated review by Gemini · gemini-4-argon · custom prompt

[github-actions]

🤖 Claude Code Review

PR #260 review: model-sync CI check

This PR adds no Rust runtime code, so actor lifecycle and concurrency concerns don't apply. My review covers the Python checker, the map, and the workflow. Overall it is well structured: the checks fail closed when the script cannot tell, there are negative-control tests, and it uses only the standard library. I found a few correctness gaps.

Correctness

1. trace_validation stops at the first matching trace spec (scripts/check-model-sync.py, end of the for spec_path in sorted(...) loop)

        return None, f"{rel} exists but no recorded event reaches it"

This return sits inside the loop. If the alphabetically first Trace*.tla that EXTENDS a model has no mapped events, the model fails even when a later spec validates it. The same early return happens on "... trace_check.py never runs it".

• Fix: record the failure reason and continue. Return None, reason only after the loop finishes.

2. Action arguments that mix literals and non-literals pass silently (check_events, the literals = [...] block)

The check collects every string literal anywhere in the argument span. Two cases slip through:

• Event::new(if c { "Close" } else { name }, ..) passes, because "Close" is found and name is ignored.
• Event::new(helper("Close"), ..) treats "Close" as the action, even though helper decides the real action.

A stricter check would accept only argument spans whose masked text, with literals and if/else/match/{}/| stripped, contains no identifiers. Alternatively, reject any span containing a (. Please add a negative test for each case.

3. Deleting #[cfg(test)] is treated as an exempt change (exempt_change / test_module_lines)

Removing only the attribute line produces a single - line. That line falls inside the old test-module range, so the change is classified as tests. Yet it moves the whole module into the production build. Possible fixes:

• treat any changed line that matches #[cfg(test)] itself as non-exempt; or
• require the module's opening line to fall in a test range on both sides.

4. Coverage floor counts every baseline entry, not action keys (check_models, covered = len(baseline.get(key, [])))

The docs and the map comment say the floor is the number of A|... action keys. If coverage-baseline.json also stores state or transition keys, the count is wrong. Use sum(1 for k in baseline.get(key, []) if k.startswith("A|")), or document that the baseline holds only action keys.

5. False positives in the struct-literal check (check_events, the \b%s\s*\{ scan)

Destructuring outside lifecycle_trace.rs matches action\s*[:,}] and is reported as "sets the action directly". Examples:

• let Event { action, .. } = ev;
• matches!(e, Event { action: "X", .. })

Also, -> Event { (a function returning Event) is not excluded by the 8-character lookbehind. That case only misfires if the body contains a bare a,, so it is low risk, but still fragile.

Weaknesses in what the check enforces

• Comment-only model edits satisfy the check, while comment-only code edits are exempt. Adding \* updated to Lifecycle.tla (exactly what test_code_change_with_model_passes does) clears any code change. I'd at least document this asymmetry. Better: run the same comment/whitespace exemption logic on the model side, so a comment-only model diff does not count as an update.
• Any single covering model is enough. lifecycle_trace.rs maps to six models and supervision.rs to three. A Cohorts-semantics change in supervision.rs passes with a touch to Supervision.tla only. This matches the documented rule, but it is weaker than "models track the code" implies. Consider requiring every covering model, or splitting the mappings more finely.
• concurrency/src/supervision/** maps only to NestedSupervision. If OneForOne or cohort logic ever moves into submodules there, Supervision and Cohorts lose coverage silently. Consider adding the glob to those two entries.
• "Checked against real runs" overstates what models verifies. It checks three things: a spec is mentioned by name (substring) in trace_check.py, its arms appear as literals in emitter calls, and EXTENDS matches. It does not check that traces are recorded or replayed in CI. Please tone down the wording in the docs, or add a check that the tla workflow actually invokes trace_check.py.

Robustness

• check_events, filters: if f["file"] is missing, (root / f["file"]).read_text() raises FileNotFoundError and prints a traceback. Report it as an error, the same way missing specs are handled.
• check_paths: if origin/main is absent (local runs, shallow clones), git merge-base origin/main fails with a bare CalledProcessError. Catch it and suggest --base.
• parse_toml: the if m.end() == m.start(): i += 1 branch is dead, since the first alternative always consumes \n. A trailing comment line without a final newline fails to parse. Allow (?:\n|$) in the first alternative.
• check_models: allowlisted = [... if models.get(m, {}).get("tlc_only") and m in tlc_only] is redundant; m in tlc_only alone is enough.
• check_events: trace_check.py is re-read on every [[trace]] iteration. Hoist the read out of the loop.

Workflow

model-sync.yml is fine:

• permissions: contents: read.
• The PR body is read from GITHUB_EVENT_PATH, never interpolated into shell, so there is no injection risk.
• fetch-depth: 0 makes origin/main available for the merge-base.

The merge_group bypass is only sound if model-sync is a required check on PRs. Please confirm that in the branch protection settings, or say so in the docs.

Docs

TESTING.md, README.md and model-map.toml hardcode future state ("with PR #240", "once PR #245 lands"). This text will go stale. The tlc_only.tracking fields are the right place for it; I'd keep the prose generic.

Suggested tests

• Removing #[cfg(test)] must fail.
• A mixed literal/non-literal action (if c { "A" } else { x }) must fail.
• A model with two Trace*.tla specs where the first is unmapped.

---

Automated review by Claude · claude-opus-5-5 · custom prompt

[github-actions]

🤖 DeepSeek Code Review

The PR mostly adds CI/scripts for model sync. The overall approach is reasonable, but the Python scanner has a few correctness issues worth fixing before relying on this in CI.

1. trace_validation can falsely mark a model as trace-validated.
   In scripts/check-model-sync.py, inside trace_validation (around the loop over translated), you do:

   for how in t.get("translated", {}).values():
       if isinstance(how, dict):
           emitted.update(how.get("into", []))

   This adds into target actions to emitted regardless of whether the corresponding translated source action was actually emitted. A spec could be considered validated by an action raised from a translated into even when no real event reaches it.
   Fix: only add targets when the source action is emitted, mirroring check_events:

   for action, how in t.get("translated", {}).items():
       if action in emitted and isinstance(how, dict):
           emitted.update(how.get("into", []))

2. exempt_change misses block comments.
   In exempt_change (around the text.startswith("//") check), comment-only changes are only recognized if the changed line starts with //. Rust block comments /* ... */ and their interior lines will be treated as non-comment changes and fail the check incorrectly.
   Suggested: use rust_mask/a comment-aware lexer for the diff lines, or explicitly handle lines inside /* ... */ blocks.

3. call_argument doesn’t handle generics/turbofish.
   call_argument splits arguments on commas at depth 0 but ignores <...>. Expressions like foo::<A, B>() contain a comma that will be mistaken for an argument separator, leading to false “cannot tell which action” errors. This is safe to tolerate now if no emitter call uses generics, but it’s a likely future false positive.

4. Event struct detection reads lifecycle_trace.rs unmasked.
   In check_events, structs = set(re.findall(r"pub struct (\w*Event)\b", trace_rs)) uses raw source. A commented-out struct such as // pub struct BogusEvent would be treated as a real struct and trigger a spurious missing [[trace]] error. Use the masked source for this extraction, or at least strip comments first.

5. Test typo in scripts/tests/test_model_sync.py.
   test_unmapped_event_in_a_branch_fails injects:

   'inlet _ = Event::new(if x { "Close" } else { "BogusBranch" }, 0, "");'

   inlet is invalid Rust. The scanner still finds Event::new, so the test passes, but it doesn’t exercise valid Rust input. Fix to let _ = Event::new(...).

6. trace_validation spec invocation check is substring-based.
   Around if spec_path.name not in check_py, a mention of the spec name in a comment or string in trace_check.py would satisfy the check even if the spec is never actually executed. Consider parsing the relevant command lines or Python AST for the actual list of run specs.

Overall this is a useful enforcement layer, but fixing the trace_validation and comment-exemption issues is important before the check becomes required.

---

Automated review by DeepSeek · deepseek-v4-pro · custom prompt

[github-actions]

🤖 Grok Code Review

The model-sync gate is well tested and fail-closed in the common cases. It does not touch actor runtime code, so lifecycle, ordering, and cancellation concerns do not apply. A few holes let the check pass while models still drift, and one scanner bug can hang the job.

Bypass / correctness

1. The map can opt itself out in the same PR. paths trusts verification/model-map.toml as edited on the head. Dropping a path from code (or shrinking a glob) makes that file uncovered, so a behaviour change no longer requires a model update or the waiver. coverage_floor has the same shape: check_models only compares the baseline to the floor in the same commit, and the error text says a reason is required to lower it, but nothing checks that. Require the no-model-change waiver (or fail) when code globs shrink or coverage_floor drops versus the base.

2. One touched model waives every model that covers the file (check_paths, the touched.intersection(covering) check). supervision.rs and lifecycle_trace.rs are shared. Updating only TraceSupervision.tla marks a supervision.rs change ok for Cohorts and NestedSupervision as well. The toml comment says “at least one”, but that undercuts “models track the code” on the files that matter most. Require every covering model’s files to change, or split shared files out of the multi-model code lists.

3. Direct Event { action: ... } construction in lifecycle_trace.rs is invisible (check_events, the rel == "concurrency/src/lifecycle_trace.rs" skip). That is exactly where emitters live, so a new helper that sets action itself is never checked. Scan that file too; only skip the struct / impl definitions.

4. trace_validation returns on the first Trace*.tla that EXTENDS the model (the return None, ... after the per-spec loop, and the “never runs it” return). A later spec that actually replays events is ignored. Collect every extending spec and succeed if any is run and reached. spec_path.name not in check_py is also a substring test, so a comment mentioning the filename counts as “runs it”.

5. rust_mask can infinite-loop on an unclosed escaped char literal:

    elif c == "'":
        if src.startswith("\\", i + 1):
            j = src.find("'", i + 3)
            blank(i + 1, j)
            i = j + 1

find returns -1, then i = 0. A syntax-error PR hangs until the 5-minute timeout. If j < 0, stop at n.

Smaller gaps

• Comment exemption (exempt_change, text.startswith("//")) ignores /* */ lines, so block-comment edits fail closed and need a waiver. Fine if documented; otherwise treat block-comment lines as comments after a mask.
• pub struct (\w*Event) is matched on raw lifecycle_trace.rs, so a commented-out struct fails events. Run that scan on the masked source.
• Filter windows are taken from raw text (end = '\)' / \];). A ) or ]; inside a string ends the window early.
• Workflow comment says merge-queue and push both skip the paths gate, but the if only excludes push (.github/workflows/model-sync.yml ~39–42). The script no-ops on merge_group, so this is consistent only by accident. Pass github.event.pull_request.base.sha as --base instead of merge-base origin/main, so the base does not depend on actions/checkout ref layout.

Tests cover the happy path, waiver, placeholder reason, and coverage-floor regression well. Add cases for a shrunk code glob, a shared file with only one of several models updated, and an action literal built inside lifecycle_trace.rs.

---

Automated review by Grok (xAI) · grok-4.7 · custom prompt

[github-actions]

🤖 Kimi Code Review

Findings

• #[cfg(test)] changes can be incorrectly exempted — scripts/check-model-sync.py:259-268, 283-321. Adding #[cfg(test)] to an existing production module is classified as “tests only” because the added attribute falls inside new_tests; removing it similarly falls inside old_tests. Both change production behavior without requiring a model update or waiver. Only exempt attribute/module-boundary changes when the entire test module is being added or removed, and add regression tests for these two cases.

• Translated events can fabricate trace validation — scripts/check-model-sync.py:590-601. trace_validation() unconditionally adds every translation’s into actions to emitted, even when the source action was never emitted. For example, the configured Send -> Request/Enqueue translation can make a model appear trace-validated despite no Send events existing. Mirror check_events() and only add targets when action in emitted.

• A model with multiple trace specs can be falsely rejected — scripts/check-model-sync.py:582-583, 602. trace_validation() returns immediately when the first matching Trace*.tla is not run by trace_check.py or has no reachable events, instead of examining later specs. Use continue, retaining diagnostics if no spec ultimately validates the model.

• Shorthand struct construction bypasses the event-action check — scripts/check-model-sync.py:471-478. The regex recognizes action: and action }, but not the common shorthand Event { action, .. }. Such construction can therefore emit an unchecked, non-literal action without an error. Include comma as a valid following token and add a negative control for shorthand construction.

• Coverage floors are not actually monotonic — scripts/check-model-sync.py:632-644. The check only compares the current baseline length against the current, PR-modifiable coverage_floor; lowering both in the same PR passes. This contradicts the “may only go up” documentation. Either compare the floor with its base-branch value, possibly with an explicit waiver, or document that decreases rely on manual review.

---

Automated review by Kimi (Moonshot AI) · kimi-k3.1-pro · custom prompt