sync: upstream eb4db2b (statechart skill, #741)

.github/upstream-sha

@@ -1 +1 @@
-88d47514b82e7c44f00f2b2a72ff6dd12158038c
+eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10

.github/workflows/lint.yml

@@ -76,6 +76,8 @@ jobs:
       - name: pr-recap sketch tests
         working-directory: skills/pr-recap/scripts/sketch
         run: bun run test
+      - name: statechart script tests
+        run: node --test tests/skills/statechart/scripts/test/*.test.mjs
   worktree-audit:
     runs-on: ubuntu-latest
     steps:

PORTING.md

@@ -47,6 +47,7 @@ Upstream is the source of truth for the workflows themselves. This file records
 
 - **documentation-impact** (`skills/documentation-impact/`) is a port addition for authoring and independently reviewing documentation affected by a change. Preserve its auto-invocable metadata, `tools/skill-trigger-cases.json` entry, README and guide entries, central Poteto completion trigger, and Babysit and Shipping readiness hooks during sync. Preserve its canonical author result rules. The pass covers local work without a PR and binds any required independent review verdict to the examined artifact and documentation context. Visual tools remain optional. Keep model selection and lifecycle orchestration in the calling workflow.
 - **pr-recap** (`skills/pr-recap/`) is a port addition that posts one reviewer recap comment per pull request: a two-sentence story, one hand-drawn sketch rendered by the bundled Bun tool in `scripts/sketch` and attached with `gh`, a "Not covered" line, and a collapsed details block. `skills/pr-recap/CREDITS.md` carries the MIT notices for the six skills its rules adapt and the OFL notice for the vendored Excalifont subset. On sync, keep the skill, its trigger row, the **Recap** paragraph in Opening a PR, the sketch tests in `tests/skills/pr-recap/`, and their `lint.yml`, `tools/gate-check.sh`, and Dependabot entries.
+- **statechart** (`skills/statechart/`) keeps upstream's scripts. Its tests live in `tests/skills/statechart/scripts/test/`, per the tests-out-of-`skills/` rule. Upstream runs them in a `validate-plugins.yml` step. Here they run in the `statechart script tests` step of the `lint.yml` skills job and in the `statechart node tests` line of the `gate-check.sh` test tier, both as `node --test` over `*.test.mjs`. CI uses the runner's preinstalled Node, because `tools/test_repository_hardening.py` bans `setup-node`. On sync, carry upstream changes to that step into both places.
 - **deslop** (`skills/deslop/`) is a port addition that replaces cursor-team-kit's `/deslop` with a pstack-owned code cleanup pass: nineteen numbered rules over the branch's changed hunks, a test run that proves behavior unchanged, and a report. `skills/deslop/CREDITS.md` ships inside the skill directory so the MIT notices travel with every `npx skills` copy. On sync, keep the skill, its trigger row in `tools/skill-trigger-cases.json`, the README and guide entries, poteto-mode's Before every commit or amend trigger, the deslop lines in Opening a PR, both autopilot playbooks, and the multi-phase checklist, step 5's hand-off to the no-comments skill and its Report line, and the ledger promises `deslop-available-for-code`, `opening-a-pr-deslops-diff`, `deslop-cleans-code-slop`, and `deslop-hands-unsettled-comments-to-no-comments`. Upstream never writes `skills/deslop/`; if it ever does, keep whichever version has the rule table.
 - **Gated publish** (port addition, 2026-10). In a repository that gates pushes through no-mistakes, Opening a PR's **Gated publish** section routes every publish, PR creation, restack, and retarget through the no-mistakes CLI, sends work-in-progress snapshots to `refs/pstack/wip/<branch>` or the repository's own agent ref convention, and hands sandbox work to the host. On sync, keep that section, the gated pointers in Babysit, Shipping, Autopilot-full, Autopilot-stack, Orchestrate, and the multi-phase checklist, the guide paragraph in `docs/guide/06-verify-and-ship.md`, the `no-mistakes` line in `tools/cross-suite-foreign.txt`, and the `opening-a-pr-gated-publish-*` ledger promises with the `open-pr-gated-run` case.
 - **Gate checks** (port addition, 2026-10). [README contributor checks](./README.md#contributor-checks) owns the tier commands, interpreter selection, and CI boundary. On sync, keep `.no-mistakes.yaml`, `tools/gate-check.sh`, the `gate-lint` and `gate-test` mise tasks, and the concurrency blocks in `lint.yml` and `skill-checks.yml`. Assign each new upstream check to one script tier or keep it CI-only, and update the README boundary when that changes.
@@ -246,7 +247,7 @@ Before checking the PR, the runner independently reads the committed promise led
 6. Hold any cut that upstream justifies by one model's behavior until it meets the bar in **Single-model upstream cuts**.
 7. Run `git add -A`, then run each check below, even after a sync that changes no skill directory. Run `git add -A` again before each rerun after a fix. One fix can expose the next failure, so rerun until each remaining failure is pre-existing or recorded for human judgment. The skill-reference spelling lint reads only tracked files, so it misses a new skill that is not staged. `skill-ci check` needs no staging, because its PII scan reads untracked files that git does not ignore and skips deleted tracked files. Failure signal: any nonzero exit. Fix the port, not the check, and say in the PR body what each failure was. A check can already fail on `main`. To find out which failures are pre-existing, compare individual failing tests and their messages, not exit codes or `PASS`/`FAIL` tier lines. One tier line can hide a new failing test behind a test that already fails on `main`. Fetch `origin main` immediately before creating the baseline. After a successful fetch, pin it with `main_sha="$(git rev-parse --verify 'FETCH_HEAD^{commit}')"`. Create a separate worktree outside the checkout with `main_wt="$(mktemp -d)"`, then `git worktree add --detach "${main_wt:?}" "${main_sha:?}"`, so the uncommitted sync work stays in place and `git add -A` never stages it. Check each command's exit status and output before continuing. Run the same checks in a subshell that enters `"${main_wt:?}"`, then remove the baseline with `git worktree remove "${main_wt:?}"`. Retain a removal refusal. In a fresh shell, recover the candidate baseline path from `git worktree list --porcelain`. Re-fetch with `git fetch origin main` and, only after success, pin the fetched commit with `main_sha="$(git rev-parse --verify 'FETCH_HEAD^{commit}')"`. Check that resolution succeeded. Compare the candidate baseline HEAD to this fetched pin and verify its clean state before assigning `main_wt` and using it. A failed fetch, missing or mismatched pin, or trunk move holds the old candidate. You may create a new disposable baseline from the new pin. A path or candidate HEAD alone does not identify a valid baseline. Do not delete an unknown old tree. An empty or unverified path stops the comparison. A failure is pre-existing only when the same test or check fails on `main` with the same message, apart from the checkout path. List each pre-existing failure in the PR body and continue. Fix every other failure, except the ones the audit bullet below lets you record for human judgment. The `ledger.py audit --upstream-ref upstream/main` check never qualifies as pre-existing, because `main` can lack the incoming guide classifications. The audit bullet below governs its failures, including the human-judgment route.
    - `tools/gate-check.sh lint`
-   - `tools/gate-check.sh test`. It needs Bun. `tools/gate-check.sh` picks its own Python, and `PSTACK_GATE_PYTHON` overrides it, as `README.md` describes. On a host with mise shims on `PATH`, put the real `bun` and `rg` ahead of the shims, and say in the PR body which tools ran. #166 tracks one pinned entry point per test tier.
+   - `tools/gate-check.sh test`. It needs Bun and Node. `tools/gate-check.sh` picks its own Python, and `PSTACK_GATE_PYTHON` overrides it, as `README.md` describes. On a host with mise shims on `PATH`, put the real `bun` and `rg` ahead of the shims, and say in the PR body which tools ran. #166 tracks one pinned entry point per test tier.
    - `python3 evals/promises/ledger.py audit --upstream-ref upstream/main`. An "unclassified upstream unit" is a guide sentence that upstream added or reworded. An unclassified or stale port unit is guide text that this sync changed, such as a count or a link from step 5. Classify it in `evals/promises/ledger.json` per `evals/promises/README.md`, and bind each new promise to a quote, a test, or a case. Port the sentence into `docs/guide` with the substitution map, unless you classify it `cursor-only` with its reason or `substituted` with the port units that replace it. A "quote no longer in" line names a guide promise whose skill text the sync rewrote. Keep the promise true, change the guide and the ledger together, or record the change for human judgment in the PR body. A quote recorded for human judgment can leave other checks failing that `main` passes. These are the lint tier's `promise ledger` check and the `AuditTest` cases in `evals/promises/test_ledger.py`, such as `test_the_committed_ledger_audits_clean`. These local failures may remain only when the complete listed set of held quotes explains every remaining cause. List each quote and each affected check in the PR body. Any unrelated failure blocks this local exception. Recording the hold waives neither authoritative CI nor no-mistakes Lint. Keep gated publication pending when the configured gate cannot accept the gap through its supported authority. Do not bypass or weaken checks. When you reword a guide sentence that ports an upstream unit, point that unit's `ported_as` at the new unit. List every ledger change in the PR body under "Guide promises".
    - `skill-ci check`
 8. After a sync that changes a live promise's owner files, rerun that promise's cases on all four harnesses with `evals/promises/live.py run`. When the runner lacks a harness, list the cases that did not run in the report and PR body as needing judgment. Render the matrix with `live.py report` and save it as `evals/promises/results/<date>.md`. Record the final skills revision evaluated, the matrix, the baseline comparison, and explicit judgments for missing cases or harnesses. These are report contents, not a fixed format; the local runner checks report presence only, not format or meaning. Save and commit the report even when some cases cannot run. Compare it with the newest earlier file there, if one exists, or state that no earlier baseline exists. Read that file's "Comparison baseline" section first. `2026-10-03.md` measures the tree before its own fixes, so compare against its "Fixed in this stack" rows, and run a full screen on the current tree before treating any other row as a baseline.

README.md

@@ -151,6 +151,7 @@ the full rules and playbooks live in [`skills/poteto-mode/SKILL.md`](./skills/po
 | [`/maintain-verification-skill`](./skills/maintain-verification-skill/SKILL.md) | your verify skill's feature map has drifted from the app. source wave + one live pass, at most one PR of proven corrections. |
 | [`/create-formal-verification-skill`](./skills/create-formal-verification-skill/SKILL.md) | tests can't reach the case that breaks a race, retry, state machine, parser, or unsafe code. verifies one property with the tool that fits and generates a project-local skill to recheck it on every change. |
 | [`/maintain-formal-verification-skill`](./skills/maintain-formal-verification-skill/SKILL.md) | code your formal verification covers has changed since it was last checked. updates the model, harness, or properties to match the code, reruns, and says whether each failure is drift in the verification or a bug in the code. |
+| [`/statechart`](./skills/statechart/SKILL.md) | someone who owns the behavior needs to see it, not read a spec. draws what the user sees as a mermaid statechart generated from a tla+ model, marks each state works, still wrong, or fixed by your open pr, and draws each bug tlc finds as a numbered path. also turns an agreed chart into a tla+ skeleton, or audits the code against an existing spec. |
 | [`/spec-probes`](./skills/spec-probes/SKILL.md) | (port addition) you're writing a spec, acceptance criteria, or tickets. surfaces the data-shape edges and the must-nevers before any code exists. |
 | [`/verify-commands`](./skills/verify-commands/SKILL.md) | (port addition) you're writing or reviewing a completion check, or reporting an upgrade, deployment, migration, or install as successful. catches the shapes that pass green while measuring nothing. |
 | [`/documentation-impact`](./skills/documentation-impact/SKILL.md) | (port addition) a change may affect user, operator, or developer instructions. updates affected docs or independently reviews them, including an evidenced no-change result. |
@@ -292,7 +293,7 @@ to set it up, point your agent at [`FOR_AGENTS.md`](./automations/benny/FOR_AGEN
 
 ## contributor checks
 
-CI uses Python 3.12 and Bun 1.4.0. For the git hooks, create the local virtual environment in the main checkout, install the `skill-ci` command, and install the hooks. The gate selects its interpreter separately, as described below.
+CI uses Python 3.12, Bun 1.4.0, and the runner's preinstalled Node. For the git hooks, create the local virtual environment in the main checkout, install the `skill-ci` command, and install the hooks. The gate selects its interpreter separately, as described below.
 
 ```sh
 python3 -m venv .venv
@@ -307,11 +308,13 @@ tools/gate-check.sh lint
 tools/gate-check.sh test
 ```
 
-The `lint` tier checks cross-suite references, the [mode entry byte budget](./skills/pstack-harness/references/skill-retention.md), personal home paths, the generated subagent bundle, the promise ledger, the shipped models config, and skill reference spelling (`tools/test_skill_references.py`). The skill reference spelling scope and exceptions are documented in [PORTING.md](./PORTING.md#substitution-map). `skill-ci check` runs the shared skill checks, as described below. The `test` tier runs the tools, promise, and setup-pstack unit suites. It installs the poteto-mode and pr-recap sketch dependencies with their frozen lockfiles, runs both Bun test suites, and runs poteto-mode's typecheck. Each check belongs to one tier, except skill reference spelling and the repository mode entry byte-budget check, which the tools unit suite also runs. The script runs every check in the selected tier, prints a PASS or FAIL line for each, and exits nonzero if any check fails. Unit suites and Bun tests must report tests, not a zero-test success.
+The `lint` tier checks cross-suite references, the [mode entry byte budget](./skills/pstack-harness/references/skill-retention.md), personal home paths, the generated subagent bundle, the promise ledger, the shipped models config, and skill reference spelling (`tools/test_skill_references.py`). The skill reference spelling scope and exceptions are documented in [PORTING.md](./PORTING.md#substitution-map). `skill-ci check` runs the shared skill checks, as described below. The `test` tier runs the tools, promise, and setup-pstack unit suites. It installs the poteto-mode and pr-recap sketch dependencies with their frozen lockfiles, runs both Bun test suites and poteto-mode's typecheck, then runs the statechart script tests with `node --test`. Each check belongs to one tier, except skill reference spelling and the repository mode entry byte-budget check, which the tools unit suite also runs. The script runs every check in the selected tier, prints a PASS or FAIL line for each, and exits nonzero if any check fails. Unit suites and Bun tests must report tests, not a zero-test success.
+
+The statechart suite skips TLC-dependent tests when `TLA2TOOLS` is unset or points to a missing file. Run `node skills/statechart/scripts/statechart.mjs --help` for TLC setup requirements.
 
 `python3 tools/check-personal-paths.py` scans the names and current contents of every Git-tracked file for concrete account names below `/Users/<account>` or `/home/<account>`. It scans symlink target spelling without following the link, skips contents containing NUL bytes as binary, and decodes other bytes with UTF-8 replacement. Filenames are checked even for binary files. Exact file-scoped content exceptions cover existing synthetic fixtures. An unused exception fails the default working-tree check used by the gate and CI. Index and pushed-tip modes suppress exact known synthetic matches without requiring every fixture to exist in each snapshot. Diagnostics redact account names and identify the file and line without printing source contents. Line 0 identifies a filename finding. Exit 1 means a personal path was found. Exit 2 means file acquisition or exception validation failed, or no tracked text files were inspected. A successful scan exits 0 and reports the number of tracked text files checked. Pre-push exits 0 without scanning when Git supplies no nondeleted local tips. The required CI `skills` job runs this checker explicitly, alongside the shared skill-ci checks.
 
-The script needs neither mise nor the main checkout's `.venv`. It selects `PSTACK_GATE_PYTHON` when set to a Python executable, then `$HOME/.local/share/mise/installs/python/3.14.7/bin/python3.14`, then `uv` on PATH with Python 3.12. This gate runner choice uses the environment's `HOME`. The native evaluators derive their confined runtime paths from the operating system account database, as documented in [the promise suite README](./evals/promises/README.md#run-the-model-free-checks). The native version pin is deliberate because Python 3.12 fails the native fsmonitor control on the reviewed host. The test tier also needs Bun, `rg`, `jq`, `gh`, and `openssl` on `PATH`. `mise run gate-lint` and `mise run gate-test` wrap the same script.
+The script needs neither mise nor the main checkout's `.venv`. It selects `PSTACK_GATE_PYTHON` when set to a Python executable, then `$HOME/.local/share/mise/installs/python/3.14.7/bin/python3.14`, then `uv` on PATH with Python 3.12. This gate runner choice uses the environment's `HOME`. The native evaluators derive their confined runtime paths from the operating system account database, as documented in [the promise suite README](./evals/promises/README.md#run-the-model-free-checks). The native version pin is deliberate because Python 3.12 fails the native fsmonitor control on the reviewed host. The test tier also needs Bun, Node, `rg`, `jq`, `gh`, and `openssl` on `PATH`. `mise run gate-lint` and `mise run gate-test` wrap the same script.
 
 `.no-mistakes.yaml` runs the `lint` tier and then `skill-ci check` as the gate's Lint step. It leaves the Test step to the pipeline's targeted checks, because no-mistakes reserves `commands.test` for targeted validation of the change, not a full suite that mirrors CI. Run the `test` tier yourself before a large change. GitHub CI remains authoritative and additionally runs the Docker oracle and maintained canon suites, the npx installation probe, and the Linux worktree-audit job. Those checks stay outside the local gate tiers. CI cancels superseded pull-request runs of `lint.yml` and `skill-checks.yml`; pushes to main never cancel. The gate fills PR bodies from `.github/pull_request_template.md` through `pr.template`, omits intent from them, keeps a minimal appendix with the risk line and head attestation, and protects `.github/workflows/**` and `.github/rulesets/**` from automatic repairs.