sync: pstack 0.15.30 (eb4db2b)

PSTACK_SYNC.md

@@ -1,6 +1,6 @@
 # pstack sync
 
-Pinned: pstack 0.15.29, commit `88d47514b82e7c44f00f2b2a72ff6dd12158038c`.
+Pinned: pstack 0.15.30, commit `eb4db2b55b2b7dec3d9282754cddf0a56bf4ff10`.
 
 Upstream: repository `cursor/plugins`, subpath `pstack/` (<https://github.com/cursor/plugins/tree/main/pstack>). Never edit pstack. `scripts/pstack_sync.py` shallow-fetches the pinned and target commits itself and reads the pin and the lists below.
 

scripts/audit_portability.py

@@ -35,7 +35,7 @@
     "comment-sicko", "control-ui", "correct", "create-formal-verification-skill", "create-verification-skill", "maintain-formal-verification-skill",
     "deslop", "dstack-config", "dstack-help", "dstack-mode",
     "how", "in-your-own-words", "interrogate", "ketchup", "maintain-verification-skill", "no-comments",
-    "recall", "reflect", "setup-dstack", "sharpen", "swarm", "tdd", "teach",
+    "recall", "reflect", "setup-dstack", "sharpen", "statechart", "swarm", "tdd", "teach",
     "technical-writing", "typescript-best-practices", "unslop", "why",
     "principle-attack-the-premise", "principle-boundary-discipline",
     "principle-build-the-lever",
@@ -457,7 +457,7 @@ def check_skill(skill_dir: Path) -> List[Finding]:
 
     package_texts: List[Tuple[Path, str]] = []
     for path in sorted(skill_dir.rglob("*")):
-        if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js"}:
+        if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js", ".mjs"}:
             continue
         text = path.read_text(encoding="utf-8")
         package_texts.append((path, text))
@@ -614,7 +614,7 @@ def check_structure() -> List[Finding]:
         "playbooks/{}.md".format(name) for name in EXCLUDED_DSTACK_PLAYBOOKS
     }
     for path in sorted(SKILLS.rglob("*")):
-        if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js"}:
+        if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js", ".mjs"}:
             continue
         text = path.read_text(encoding="utf-8")
         for reference in sorted(unsupported_references):
@@ -642,7 +642,7 @@ def check_invocation_targets(skill_dirs: Iterable[Path]) -> List[Finding]:
     findings: List[Finding] = []
     for skill_dir in skill_dirs:
         for path in sorted(skill_dir.rglob("*")):
-            if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js"}:
+            if not path.is_file() or path.suffix.lower() not in {".md", ".txt", ".json", ".py", ".sh", ".ts", ".js", ".mjs"}:
                 continue
             for line_number, line in enumerate(path.read_text(encoding="utf-8").splitlines(), 1):
                 for target in SKILL_CALL.findall(line):

skills/dstack-help/SKILL.md

@@ -14,7 +14,7 @@ Give the user the file's public copy: `https://github.com/dimitriskourg/dstack/b
 
 ## Locked keep-set
 
-55 skills, 24 principles, ten playbooks. What is out of this pack lives in [Supported scope](references/guide/06-supported-scope.md), not here.
+56 skills, 24 principles, ten playbooks. What is out of this pack lives in [Supported scope](references/guide/06-supported-scope.md), not here.
 
 ### Setup and routing
 
@@ -59,13 +59,16 @@ Name a skill directly when the user wants more or less than the playbook. Read i
 | Bring a verification skill back in line | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) |
 | Formally verify a race or invariant | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) |
 | Bring a formal verification back in line | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) |
+| Show what the user sees as a chart checked by a model | [`/statechart`](../statechart/SKILL.md) |
 | Turn a finished task into skill edits | [`/reflect`](../reflect/SKILL.md) |
 | Stop agents repeating the same mistakes | [`/correct`](../correct/SKILL.md) |
 
 Bundled so the workflow is complete: `/deslop`, `/control-ui`, `/comment-sicko`.
 
 Close calls: `/how` vs `/why` vs `/teach`; `/arena` vs `/swarm`; `/recall` vs `/ketchup` (session pickup resumes one chat or branch); `/architect` implements after it settles, add "with checkpoint" to review first.
 
+`/statechart` needs Java 11 or later and `TLA2TOOLS` set to a `tla2tools.jar`.
+
 ### Playbooks
 
 Playbooks are step lists inside `/dstack-mode`, not slash commands. The Playbooks section of [`dstack-mode`](../dstack-mode/SKILL.md) lists when each applies:

skills/dstack-help/references/guide/06-supported-scope.md

@@ -48,6 +48,7 @@ The skills below remain supported. The everyday keep-set is closed.
 - `create-formal-verification-skill`
 - `maintain-formal-verification-skill`
 - `maintain-verification-skill`
+- `statechart`
 - `tdd`
 - `typescript-best-practices`
 

skills/dstack-help/references/guide/06-verify-and-ship.md

@@ -97,6 +97,22 @@ It writes a project-local skill that tells the next agent whether a change touch
 
 The skill also records which code each check covers and the commit where the check last matched it. Merges and refactors that skip the skill can leave the check passing on a description of code that's gone. After them, run [`/maintain-formal-verification-skill`](../../../maintain-formal-verification-skill/SKILL.md). It updates the verification from the code, reruns it, shows that each updated check can still fail, and tells you whether each failure is drift in the verification or a bug in the code.
 
+## Show the behavior as a statechart
+
+A counterexample in model terms convinces you. The PM or designer who owns the behavior needs to see it in their terms. Run:
+
+```text
+/statechart what the user sees when they edit a note offline
+```
+
+[`/statechart`](../../../statechart/SKILL.md) draws a Mermaid statechart of what the user sees, generated from a TLA+ model, so the picture and the checked model can't drift apart. The reader's rules ("you never see Synced while you're offline") become invariants. Each bug TLC finds is a numbered path in the reader's words, and each state is marked works, still wrong, or fixed by your open PR. Before the hand-off, the agent reproduces each bug path in the real code, so a modeling error doesn't reach the reader as a bug.
+
+It also runs the other way. Sketch the behavior as a chart, agree on it with the reader, and the skill writes a TLA+ skeleton from it. TLC checks the agreed chart's rules before any code exists. As guards from the real code go into the spec, each place the code departs from the chart shows up as a difference for the reader to decide.
+
+When the code already has a TLA+ spec, the skill can audit the code against it. The agent models what the code does and checks that model next to the unchanged spec. The chart marks the steps where the two differ, and each rule either one breaks is a numbered path.
+
+TLC needs Java 11 or later and `TLA2TOOLS` set to a `tla2tools.jar` from a TLA+ release. Set `JAVA` if `java` is not on PATH.
+
 ## Open the PR
 
 ```text

skills/dstack-help/references/guide/10-recipes-and-pitfalls.md

@@ -82,6 +82,14 @@ The qualifiers do real work. "don't change anything yet" keeps it read-only, and
 
 The generator picks the tool from the question, proves one property, and leaves a project-local skill the next agent can rerun on every relevant change. After merges or refactors in that code, run `/maintain-formal-verification-skill`. It updates the check from the code and says whether a failure is drift or a bug.
 
+## Show the PM what the user sees
+
+```text
+/statechart what the user sees when they edit a note offline
+```
+
+[`/statechart`](../../../statechart/SKILL.md) draws a Mermaid chart from a TLA+ model, marks each state works, still wrong, or fixed, and draws each bug as a numbered path. It also turns an agreed chart into a TLA+ skeleton, or audits the code against an existing spec. It needs Java 11 or later and `TLA2TOOLS` set to a `tla2tools.jar`.
+
 ## Stop correcting the same mistake
 
 ```text

skills/dstack-help/references/recipes.md

@@ -17,6 +17,7 @@ Swap in the real paths, skills, and done checks. Informal wording works.
 - Bug: `/dstack-mode <symptom>. repro first, then fix and verify.`
 - Bug in an app: `/dstack-mode repro this with /verify-<app>. if it repros on main, fix it and show me a video as proof.`
 - Property tests rarely reach: `/create-formal-verification-skill`. After merges or refactors in that code: `/maintain-formal-verification-skill`.
+- Show a PM what the user sees, checked by a model: `/statechart what the user sees when they <action>`. Needs Java 11+ and `TLA2TOOLS` pointing at `tla2tools.jar`.
 - Bug with a cheap test: `/dstack-mode repro <bug> first. if there's a cheap test path, /tdd it. then fix and rerun.`
 - Feature: `/dstack-mode add <behavior>. <current output> stays byte-identical. verify both.`
 - Refactor: `/dstack-mode move <code> into one module, zero behavior change. record the current output first and prove it's unchanged after.`
@@ -32,6 +33,7 @@ Swap in the real paths, skills, and done checks. Informal wording works.
 
 - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too.
 - `/create-formal-verification-skill prove <property> holds in <module>, even when <steps> interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`.
+- `/statechart what the user sees when they <action>`. Turn an agreed chart into a TLA+ skeleton, or audit the code against its spec.
 - `/swarm check every package under <dir> against its check script. one worker per package. one report.`
 - `/dstack-mode open the pr. small ordered commits, evidence in the description.`
 - `/dstack-mode babysit this pr. get it green.` For status only: `/dstack-mode check on pr <number>. anything outstanding?`

skills/statechart/SKILL.md

@@ -0,0 +1,36 @@
+---
+name: statechart
+description: "Draw what an app's user sees as a Mermaid statechart from a TLA+ model. States are gray if they work, red if still wrong, and green if fixed. Each bug TLC finds is a numbered path. Use for /statechart, \"show the PM the bug\", or to turn an agreed chart into a TLA+ skeleton."
+disable-model-invocation: true
+---
+
+# Statechart
+
+The chart shows what an app's user sees. A PM reads it to decide whether that behavior is right. Label each state with what is on the screen, such as "Paying". Label each step with what the user does or sees happen, such as "tap Pay" or "the charge goes through". Keep variable and action names out of labels. The scripts call this user the reader, as in `readerActions` and reader steps.
+
+Run `node <skill dir>/scripts/statechart.mjs --help` for the commands and for how to read a chart. TLC needs `TLA2TOOLS` set to a `tla2tools.jar` from a [TLA+ release](https://github.com/tlaplus/tlaplus/releases), and Java 11 or later. Set `JAVA` if `java` is not on PATH. The skill ships a checked example under `scripts/model/` and tests under `scripts/test/`. Work in a scratch folder outside the repo. The command writes its files next to its input.
+
+## Pick the direction
+
+Use `from-spec` when a TLA+ model exists or the code is concrete enough to model. Use `from-chart` when there is no model and the PM should agree on the behavior before anyone writes or changes the code.
+
+If the code already has a TLA+ spec, start from a copy of that spec. Add the variables the user sees, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as `--against`. In a new spec, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code.
+
+## Spec to chart
+
+1. Choose the chart's states. When the PM cares about something the screen does not show, such as a second charge while the screen still says "Paying", name the state "Paying, charged twice". Start with few states, and split a state only when the split separates two bugs.
+2. Write each rule the PM agrees to as one invariant, with the PM's sentence as its comment. For a rule that applies once everything settles, define `Settled == ~ENABLED System`, where `System` is the disjunction of the actions the user does not take. Report each broken rule as a bug. Never weaken a rule to make the chart pass.
+3. Run `from-spec`, then fill in the mapping file it writes. Put the labels in `state` and `step`, and list the user's actions in `readerActions` by action name. When two bugs end on the same screen through different code paths, add `cause` and make it name the code path. To color the states by what the PM cares about, such as "Toast shown", return that group from `group`. The legend names the groups, and states that break a rule still get a red border.
+4. If there is an open fix, model it from the code and pass that model as `--fixed`.
+5. Render each chart with `--png` and look at every PNG. Check that each numbered path reads in order. If a label reads like code, fix `state` or `step` and run the command again.
+6. Replay each bug's story against the real code, as a test or a live repro, one step per model action. If a bug does not reproduce, assume the model is wrong until you show otherwise. Fix the model, not the rule.
+
+## Chart to spec
+
+1. Draw the chart the PM agrees to. Use one region for each thing that changes independently, such as the connection and the sync badge. Add one `%% never` line per rule, with the PM's sentence. Draw "the app closes" as an edge to the state the user sees next.
+2. Run `from-chart`. If a rule breaks, the agreed chart has a design bug. Take the bug to the PM.
+3. Add the real code's guards and variables to the spec that `from-chart` wrote, and run `from-chart` again. For each difference it prints, ask the PM whether the code is wrong or the chart needs a correction.
+
+## Hand off
+
+Give the PM the PNG and the Mermaid source of each chart. Add one line per bug with the rule it breaks, its steps as the chart numbers them, whether it reproduced, and whether the open fix fixes it. Take every count you quote from `summary.json`. Attach `stories.md` and the command that regenerates everything. Say what the model leaves out.

skills/statechart/agents/openai.yaml

@@ -0,0 +1,5 @@
+interface:
+  display_name: "Statechart"
+  short_description: "Draw what the user sees as a checked chart"
+policy:
+  allow_implicit_invocation: false