sync: upstream pstack 519d36a (0.15.34)

.omp-plugin/marketplace.json

@@ -5,13 +5,13 @@
   },
   "metadata": {
     "description": "pstack, poteto's engineering methodology for Cursor, ported to oh-my-pi. Model and provider agnostic.",
-    "version": "0.15.32"
+    "version": "0.15.34"
   },
   "plugins": [
     {
       "name": "pstack",
-      "description": "60 skills, 23 playbooks, 24 principles, the poteto-mode pin, and two agents. Upstream cursor/plugins pstack at e73df47.",
-      "version": "0.15.32",
+      "description": "60 skills, 23 playbooks, 24 principles, the poteto-mode pin, and two agents. Upstream cursor/plugins pstack at 519d36a.",
+      "version": "0.15.34",
       "category": "development",
       "license": "MIT",
       "source": "./plugins/pstack"

omp-port/UPSTREAM

@@ -1 +1 @@
-e73df471cd4bd918367e99f3dd9c51bd53ddf5f0
+519d36aa98955bf680db01bcde5fdfba686dc901

plugins/pstack/package.json

@@ -1,6 +1,6 @@
 {
   "name": "pstack",
-  "version": "0.15.32",
+  "version": "0.15.34",
   "license": "MIT",
   "omp": {
     "extensions": [

plugins/pstack/skills/create-formal-verification-skill/SKILL.md

@@ -32,7 +32,7 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p
 
 Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders.
 
-If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/skill:statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words, and which of those violations a change fixes. When the check passes, `/skill:statechart` draws a chart of how the system moves between states. Refer to `/skill:statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts.
+If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/skill:statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words. When the check passes, `/skill:statechart` draws a chart of how the system moves between states. Refer to `/skill:statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts.
 
 ## Prove it before you hand off
 

plugins/pstack/skills/poteto-help/SKILL.md

@@ -89,7 +89,7 @@ The default answer is `/skill:poteto-mode`, which runs most of the others when i
 | Bring a verification skill and its feature map back in line with the app | [`/skill:maintain-verification-skill`](../maintain-verification-skill/SKILL.md) |
 | Formally verify a race, invariant, or other property that tests rarely reach | [`/skill:create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) |
 | Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/skill:maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) |
-| Show a PM or designer what the user sees as a chart checked by a model, with each bug drawn as a numbered path, turn an agreed chart into a TLA+ skeleton, or audit the code against its TLA+ spec | [`/skill:statechart`](../statechart/SKILL.md) |
+| Show a PM or designer what the user sees as a chart checked by a TLA+ model, with the shortest path to each state that breaks a rule | [`/skill:statechart`](../statechart/SKILL.md) |
 | Vet a performance number before reporting or acting on it | [`/skill:benchmark-checklist`](../benchmark-checklist/SKILL.md) |
 | Run a large or cross-cutting change, or one to review after stepping away | [`/skill:figure-it-out`](../figure-it-out/SKILL.md) |
 | Keep a decision log during a run, and review it afterward | [`/skill:show-me-your-work`](../show-me-your-work/SKILL.md) |

plugins/pstack/skills/statechart/references/render.md

@@ -0,0 +1,93 @@
+# Render a chart
+
+Render each `.mmd` file that you show with the npm package `[email protected]`, and give the user the SVG. Install Pele once, outside the repo. Write each SVG next to its `.mmd` file, with the same name. The API is at https://pele.run/api. Pass `{ limit: 1_000_000, outputLimit: 8_000_000, maxEdges: 10_000 }` as the options of `render`. Pele's defaults are smaller than a chart of 500 states can be. When Pele throws a `PeleError`, show the user the Mermaid text and the error.
+
+## Colors
+
+Pele ignores Mermaid `theme` and `themeVariables`. Set its `--pele-*` CSS variables on `.pele`. https://pele.run/theming lists them. The command gives each state the color class of its group, such as `class sN teal`. It marks each bad state with `class sN breaks` or `class sN mayBreak`, each state on the shortest path to a bug with `class sN bugPath`, and each state that a PROPERTY counterexample repeats forever with `class sN repeats`. Pele puts these classes on the state's node. Color the classes with CSS.
+
+The `.mmd` file has a `classDef` line for `breaks` and for `mayBreak`, so that any Mermaid viewer shows the bug marks. It has no `classDef` for the group colors, `bugPath`, or `repeats`. Pele writes each `classDef` color as a `style` attribute on the node, and a `style` attribute wins over a normal CSS rule. So the rules for the marks below use `!important`. Without it, a dark theme keeps the light mark colors. A bug mark sets the fill and the text, and `bugPath` and `repeats` set the border. Put the mark rules after the group colors, so that a mark shows over the group color.
+
+These colors are suggestions. They are the colors of the old skill. Put them in a `<style>` element at the start of each SVG. Each SVG then follows the light or dark setting of the viewer.
+
+```css
+.pele {
+  --pele-bg: #ffffff;
+  --pele-fg: #1c1c1c;
+  --pele-muted: #656565;
+  --pele-line: #808080;
+  --pele-surface: #fcfcfc;
+  --pele-surface-alt: #f1f1f1;
+  --pele-border: #c9c9c9;
+}
+.pele .blue rect { fill: #c3e0ff; }
+.pele .orange rect { fill: #f0d3bf; }
+.pele .purple rect { fill: #e3d5ff; }
+.pele .yellow rect { fill: #f0dcbf; }
+.pele .teal rect { fill: #bfe3df; }
+.pele .tan rect { fill: #e5d9ce; }
+.pele .pink rect { fill: #ffcbe6; }
+.pele .breaks rect {
+  fill: #ffecee !important;
+  stroke: #e72e3b !important;
+  stroke-width: 2.5px !important;
+}
+.pele .breaks text {
+  fill: #cd2834 !important;
+}
+.pele .mayBreak rect {
+  fill: #fff3e6 !important;
+  stroke: #e8730c !important;
+  stroke-width: 2.5px !important;
+}
+.pele .mayBreak text {
+  fill: #b85a06 !important;
+}
+.pele .bugPath rect {
+  stroke: #1680f3 !important;
+  stroke-width: 2.5px !important;
+}
+.pele .repeats rect {
+  stroke: #9b35d6 !important;
+  stroke-width: 2.5px !important;
+  stroke-dasharray: 6 3;
+}
+@media (prefers-color-scheme: dark) {
+  .pele {
+    --pele-bg: #1f1f1f;
+    --pele-fg: #f5f5f5;
+    --pele-muted: #acacac;
+    --pele-line: #939393;
+    --pele-surface: #121212;
+    --pele-surface-alt: #2c2c2c;
+    --pele-border: #4e4e4e;
+  }
+  .pele .blue rect { fill: #1b3857; }
+  .pele .orange rect { fill: #573117; }
+  .pele .purple rect { fill: #3c2e57; }
+  .pele .yellow rect { fill: #573d17; }
+  .pele .teal rect { fill: #174641; }
+  .pele .tan rect { fill: #3d3127; }
+  .pele .pink rect { fill: #57233e; }
+  .pele .breaks rect {
+    fill: #2e2021 !important;
+    stroke: #cf2b35 !important;
+  }
+  .pele .breaks text {
+    fill: #ff6463 !important;
+  }
+  .pele .mayBreak rect {
+    fill: #2e2619 !important;
+    stroke: #d0700f !important;
+  }
+  .pele .mayBreak text {
+    fill: #ffa257 !important;
+  }
+  .pele .bugPath rect {
+    stroke: #116dd2 !important;
+  }
+  .pele .repeats rect {
+    stroke: #9a3fcf !important;
+  }
+}
+```

plugins/pstack/skills/statechart/scripts/backends/cfg.ts

@@ -0,0 +1,33 @@
+import { CHART_STATES, type ConfigSection, RERUN_STATES, type Spec } from "../ir.ts";
+
+export function configText(sections: ConfigSection[], extra: string[]) {
+  const lines: string[] = [];
+  for (const s of sections) lines.push(`${s.key} ${s.tokens.join(" ")}`);
+  lines.push(...extra);
+  return lines.join("\n");
+}
+
+export const boundRun = (module: string) =>
+  [
+    `---- MODULE ChartBound ----`,
+    `EXTENDS ${module}`,
+    `ChartTLC == INSTANCE TLC`,
+    `ChartNaturals == INSTANCE Naturals`,
+    `ChartBound == ChartNaturals!<(ChartTLC!TLCGet("distinct"), ${RERUN_STATES})`,
+    `====`,
+  ].join("\n");
+
+export function chartRun({ module, variables, invariants }: Spec, tag: string) {
+  const every: string[] = [];
+  for (const name of invariants) every.push(`(IF ~${name} THEN {"${name}"} ELSE {}) \\cup `);
+  return [
+    `---- MODULE ChartRun ----`,
+    `EXTENDS ${module}`,
+    `ChartTLC == INSTANCE TLC`,
+    `ChartNaturals == INSTANCE Naturals`,
+    `ChartBudget == ChartNaturals!<=(ChartTLC!TLCGet("distinct"), ${CHART_STATES})`,
+    `ChartBroken == ${every.join("")}{}`,
+    `ChartMark == ChartBroken = {} \\/ ChartTLC!PrintT(<<"${tag}", <<${variables.join(", ")}>>, ChartBroken>>)`,
+    `====`,
+  ].join("\n");
+}

plugins/pstack/skills/statechart/scripts/backends/mermaid.ts

@@ -0,0 +1,201 @@
+import { append, byText, type Chart, type ChartState, type Region, tupleKey } from "../ir.ts";
+
+const BLANK = /\p{White_Space}/u;
+const SAFE = /^[\p{L}\p{N} !'()+,\-./=?[\]"_|@{}:\\^%<>]$/u;
+const HAZARD =
+  /:(?=:|$|\S*#)|\\(?=n)|%(?=%)|<(?=[\p{L}/!?])|_(?![\p{L}\p{N}])|(?<![\p{L}\p{N}])_/giu;
+const DIRECTION = /(direction)\s+(?=LR|RL|TB|BT)/gi;
+const DOUBLE_BRACKET = /\[(?=\[)/g;
+const C4 = /C4(?=Container|Component|Dynamic|Deployment)/g;
+const UNDRAWN = /[\0\x80-\x9f]/;
+const REWRITTEN = ["fl°", "¶ß"];
+const MARKER = /(?<=marker-end=)"/g;
+const firstOf = new Map<number, number>();
+for (const pair of REWRITTEN) {
+  const [first, second] = [...pair].map((c) => c.codePointAt(0) ?? 0);
+  firstOf.set(second, first);
+}
+const KEPT = 0;
+const BLANKED = 1;
+const DROPPED = 2;
+const CODED = 3;
+const JOINS = 4;
+const kindOf = (n: number) => {
+  const c = String.fromCodePoint(n);
+  const kind =
+    c === " "
+      ? KEPT
+      : BLANK.test(c)
+        ? BLANKED
+        : UNDRAWN.test(c)
+          ? DROPPED
+          : SAFE.test(c)
+            ? KEPT
+            : CODED;
+  return firstOf.has(n) ? kind | JOINS : kind;
+};
+const ASCII = Uint8Array.from({ length: 128 }, (_, n) => kindOf(n));
+const wide = new Map<number, number>();
+const kindAt = (n: number) => {
+  if (n < 128) return ASCII[n];
+  let kind = wide.get(n);
+  if (kind === undefined) wide.set(n, (kind = kindOf(n)));
+  return kind;
+};
+const encode = (s: string, ref: (n: number) => string) => {
+  let out = "";
+  let run = 0;
+  let last = -1;
+  for (let i = 0; i < s.length;) {
+    let n = s.charCodeAt(i);
+    let width = 1;
+    if (n >= 0xd800 && n <= 0xdfff) {
+      const low = s.charCodeAt(i + 1);
+      if (n <= 0xdbff && low >= 0xdc00 && low <= 0xdfff) {
+        n = 0x10000 + ((n - 0xd800) << 10) + (low - 0xdc00);
+        width = 2;
+      } else n = 0xfffd;
+    }
+    let kind = kindAt(n);
+    if (kind === DROPPED) {
+      out += s.slice(run, i);
+      run = i + width;
+    } else {
+      const joined = kind >= JOINS && firstOf.get(n) === last;
+      kind &= ~JOINS;
+      if (joined || kind !== KEPT) {
+        out += s.slice(run, i);
+        if (joined) out += ref(0x2060);
+        if (kind === KEPT) run = i;
+        else {
+          out += kind === BLANKED ? " " : ref(n);
+          run = i + width;
+        }
+      }
+      last = n;
+    }
+    i += width;
+  }
+  return out + s.slice(run);
+};
+const code = (s: string, ref: (n: number) => string) =>
+  encode(s, ref)
+    .replace(MARKER, `${ref(0x2060)}"`)
+    .replace(HAZARD, (c) => ref(c.charCodeAt(0)));
+const esc = (s: string, quoted = false) => {
+  const plain = code(s, (n) => `#${n};`);
+  const out = quoted ? plain.replaceAll('"', "#34;") : plain;
+  if (!out.trim()) return "#32;";
+  const turned = out.replace(DIRECTION, "$1#32;");
+  const opened = turned.includes("[[") ? turned.replace(DOUBLE_BRACKET, "#91;") : turned;
+  return opened.includes("C4") ? opened.replace(C4, "C#52;") : opened;
+};
+
+const or = (names: Iterable<string>) => [...names].sort(byText).join(" or ");
+
+const MARK_STYLES = {
+  breaks: "fill:#ffecee,stroke:#e72e3b,stroke-width:2.5px,color:#cd2834",
+  mayBreak: "fill:#fff3e6,stroke:#e8730c,stroke-width:2.5px,color:#b85a06",
+};
+
+export function mermaidLines(chart: Chart) {
+  let next = 0;
+  const marks: string[] = [];
+  const used = new Set<string>();
+  const rules = { breaks: new Set<string>(), mayBreak: new Set<string>() };
+  const region = (r: Region) => {
+    const out: string[] = [];
+    const topIds = new Map<string, string>();
+    const nestedIds = new Map<string, string>();
+    const id = (path: string[]) => {
+      const top = path.length === 1;
+      const named = top ? topIds : nestedIds;
+      const k = top ? path[0] : tupleKey(path);
+      let s = named.get(k);
+      if (s === undefined) named.set(k, (s = `s${next++}`));
+      return s;
+    };
+    const known = new Map<string[], string>();
+    const idOf = (path: string[]) => {
+      let s = known.get(path);
+      if (s === undefined) known.set(path, (s = id(path)));
+      return s;
+    };
+    const tree = (prefix: string[], indent: string, below: ChartState[]) => {
+      const heads = new Map<string, ChartState[]>();
+      for (const s of below) append(heads, s.path[prefix.length], s);
+      for (const [head, under] of heads) {
+        const path = [...prefix, head];
+        let leaf: ChartState | undefined;
+        const inner: ChartState[] = [];
+        for (const s of under)
+          if (s.path.length > path.length) inner.push(s);
+          else leaf = s;
+        if (inner.length) {
+          out.push(`${indent}state "${esc(head, true)}" as ${id(path)} {`);
+          tree(path, indent + "  ", inner);
+          out.push(`${indent}}`);
+        } else if (leaf) {
+          const sid = idOf(leaf.path);
+          out.push(`${indent}${sid}: ${esc(head)}`);
+          let mark: "breaks" | "mayBreak" | undefined =
+            leaf.breaks.length && !leaf.works ? "mayBreak" : undefined;
+          if (mark) for (const b of leaf.breaks) if (b.always) mark = "breaks";
+          if (mark) for (const b of leaf.breaks) rules[mark].add(b.rule.name);
+          const trail = [leaf.lead && "bugPath", leaf.repeats && "repeats"];
+          const color = leaf.group === undefined ? undefined : chart.colors[String(leaf.group)];
+          for (const cls of [color, mark, ...trail])
+            if (cls) {
+              used.add(cls);
+              marks.push(`  class ${sid} ${cls}`);
+            }
+        }
+      }
+    };
+    tree([], "  ", r.states);
+    for (const s of r.states) if (s.start) out.push(`  [*] --> ${idOf(s.path)}`);
+    for (const s of r.steps)
+      out.push(
+        `  ${idOf(s.from)} --> ${idOf(s.to)}: ${esc(s.label + (s.when ? ` [${s.when}]` : ""))}`,
+      );
+    return out;
+  };
+  let body: string[];
+  if (chart.regions.length > 1) {
+    body = [`  state "At the same time" as all {`];
+    for (const [i, r] of chart.regions.entries()) {
+      if (i) body.push("    --");
+      body.push(`    state "${esc(r.name, true)}" as r${i} {`);
+      for (const line of region(r)) body.push(`    ${line}`);
+      body.push("    }");
+    }
+    body.push("  }");
+  } else body = region(chart.regions[0]);
+  const legend: string[][] = [];
+  for (const entry of [
+    ...Object.entries(chart.colors),
+    [`Breaks ${or(rules.breaks)}`, "breaks"],
+    [`Breaks ${or(rules.mayBreak)} in some cases`, "mayBreak"],
+    [`Path to the ${or(chart.paths)} bug`, "bugPath"],
+    [`Repeats forever, so ${or(chart.loops)} breaks`, "repeats"],
+  ])
+    if (used.has(entry[1])) legend.push(entry);
+  const lines: string[] = [];
+  const title = chart.title && code(chart.title, (n) => `fl°°${n}¶ß`).replaceAll("<", "fl°°60¶ß");
+  if (title) lines.push("---", `title: ${JSON.stringify(title)}`, "---");
+  lines.push("stateDiagram-v2");
+  if (chart.regions.length > 1) lines.push("  direction LR");
+  if (legend.length) {
+    lines.push(`  state "Legend" as legend {`);
+    for (const [i, [text]] of legend.entries()) lines.push(`    lg${i}: ${esc(text)}`);
+    lines.push("  }");
+    for (const [i, [, cls]] of legend.entries()) lines.push(`  class lg${i} ${cls}`);
+  }
+  for (const line of body) lines.push(line);
+  for (const [cls, style] of Object.entries(MARK_STYLES))
+    if (used.has(cls)) lines.push(`  classDef ${cls} ${style}`);
+  for (const line of marks) lines.push(line);
+  return lines;
+}
+
+export const mermaid = (chart: Chart) => mermaidLines(chart).join("\n");