fix(statechart): resolve the mise ceiling folder and run the TLC tests on macOS

PORTING.md

@@ -47,7 +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. Its refresh trigger in `skills/poteto-mode/references/task-triggers.md` and the `threads-only` sentence in step 1 of `skills/poteto-mode/playbooks/babysit.md` are also port additions, so keep that line and that sentence when a sync rewrites them.
-- **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.
+- **statechart** (`skills/statechart/`) keeps upstream's scripts, except for the `tlc-tools.mjs` edit below. Its tests live in `tests/skills/statechart/scripts/test/`, because test files sit under the root `tests/` tree at their `skills/` path, a rule the fork-only CI and tooling entry below states. 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. `statechart.test.mjs` has seven edits that upstream lacks, and its `.mmd` fixtures match upstream's. Two are older. The #297 port moved the file to `tests/`, so its imports and its `scripts` constant point at `../../../../../skills/statechart/scripts/`. Since the #304 sync, the `copyPath` test uses `/srv/u/Count.tla` where upstream puts the same file under `/home/`, because `tools/check-personal-paths.py` reports any `/home/<name>/` path and so fails the lint tier and CI. The other five come from #308, port edits (2026-10) that also change `tlc-tools.mjs`. There, `findTlc` resolves its empty folder before it names that folder in `MISE_CEILING_PATHS`, and the printed install command uses `$(pwd -P)`. mise compares the ceiling with its resolved cwd, so a TMPDIR under a symlink let it read an untrusted `mise.toml` above. In the test file, the `installCommand` helper uses `$(pwd -P)` to match the script, and three tests compare that text with the script's output. TMPDIR is resolved before any folder is made, because a run's cwd is resolved and the `/var` link on macOS made printed folders absolute. The real-mise ceiling test reaches TMPDIR through a symlink. A `findTlc` test runs the fake mise under a `locked = true` `mise.toml` above a TMPDIR reached through a symlink, so CI, which has no mise and skips the real-mise test, still checks the ceiling. The rename shim has `#ifdef __APPLE__` blocks that replace `mkdir` and `rename` through `__interpose` entries, because macOS ignores `LD_PRELOAD`. In the same edit, `failingRenames` became an environment object that the rename tests spread (`...failingRenames`), `LD_PRELOAD` on Linux and `DYLD_INSERT_LIBRARIES` on darwin. The readlink shim for the PID-namespace test stays Linux-only, because macOS has no `unshare` and the test skips there. On sync, keep these seven edits where upstream rewrites those lines, and drop each one that upstream adopts.
 - **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.

skills/statechart/scripts/tlc-tools.mjs

@@ -20,8 +20,9 @@ export function findTlc() {
     if (file && !fs.existsSync(file)) throw new Error(`${name} is ${file}, which does not exist.`);
   if (TLA2TOOLS) return { jar: TLA2TOOLS, java: JAVA || "java" };
   const command = (tools) =>
-    `cd "$(mktemp -d)" && MISE_CEILING_PATHS="$PWD" mise install ${tools.map((t) => `'${t}'`).join(" ")}`;
-  const empty = fs.mkdtempSync(path.join(os.tmpdir(), "statechart-mise-"));
+    `cd "$(mktemp -d)" && MISE_CEILING_PATHS="$(pwd -P)" mise install ${tools.map((t) => `'${t}'`).join(" ")}`;
+  // mise compares the ceiling with its resolved cwd, so a TMPDIR under a symlink must be resolved.
+  const empty = fs.realpathSync(fs.mkdtempSync(path.join(os.tmpdir(), "statechart-mise-")));
   const env = { ...process.env, MISE_CEILING_PATHS: empty };
   const run = (...args) => spawnSync("mise", args, { cwd: empty, env, encoding: "utf8" });
   const mise = (...args) => {

tests/skills/statechart/scripts/test/statechart.test.mjs

@@ -8,6 +8,7 @@ import {
   mkdtempSync,
   readdirSync,
   readFileSync,
+  realpathSync,
   renameSync,
   rmSync,
   statSync,
@@ -47,6 +48,10 @@ import { ruleBook } from "../../../../../skills/statechart/scripts/rule-book.mjs
 import { copyPath } from "../../../../../skills/statechart/scripts/snapshot.mjs";
 import { findTlc, JAVA_TOOL, TLC_TOOL } from "../../../../../skills/statechart/scripts/tlc-tools.mjs";
 
+// A run's cwd is a resolved path, so the folders it names must be built from a resolved TMPDIR.
+// macOS keeps TMPDIR under /var, a link to /private/var.
+process.env.TMPDIR = realpathSync(tmpdir());
+
 const here = dirname(fileURLToPath(import.meta.url));
 const scripts = join(here, "../../../../../skills/statechart/scripts");
 const fixture = (name) => readFileSync(join(here, name), "utf8");
@@ -1452,7 +1457,7 @@ test("statechart.mjs writes the spec next to the chart, keeps it on the next run
 });
 
 const installCommand = (...tools) =>
-  `cd "$(mktemp -d)" && MISE_CEILING_PATHS="$PWD" mise install ${tools.map((t) => `'${t}'`).join(" ")}`;
+  `cd "$(mktemp -d)" && MISE_CEILING_PATHS="$(pwd -P)" mise install ${tools.map((t) => `'${t}'`).join(" ")}`;
 
 test("statechart.mjs shows mise's own error when mise fails before it can look for TLC", () => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-"));
@@ -1999,8 +2004,38 @@ test(
   },
 );
 
+test("findTlc installs TLC with mise under a mise.toml that sets locked = true above a TMPDIR reached through a symlink", () => {
+  const { at, dir, env } = outsideRepoWithoutTlc();
+  const root = dirname(dir);
+  writeFileSync(join(dir, "mise.toml"), "[settings]\nlocked = true\n");
+  mkdirSync(join(dir, "tmp"));
+  symlinkSync(dir, join(root, "link"));
+  const home = join(root, "tlaplus");
+  mkdirSync(home);
+  writeFileSync(join(home, "tla2tools.jar"), "");
+  const findTlcHere = `import { findTlc } from ${JSON.stringify(pathToFileURL(join(at, "tlc-tools.mjs")).href)};
+console.log(JSON.stringify(findTlc()));`;
+  const r = spawnSync(process.execPath, ["--input-type=module", "-e", findTlcHere], {
+    cwd: dir,
+    encoding: "utf8",
+    env: {
+      ...process.env,
+      ...env,
+      TLAPLUS_HOME: home,
+      TLC_JAVA: process.execPath,
+      TMPDIR: join(root, "link", "tmp"),
+    },
+  });
+  assert.equal(r.status, 0, r.stderr);
+  assert.equal(r.stderr, INSTALLING);
+  assert.deepEqual(JSON.parse(r.stdout), {
+    jar: join(home, "tla2tools.jar"),
+    java: process.execPath,
+  });
+});
+
 test(
-  "statechart.mjs finds TLC with the real mise when an untrusted mise.toml is next to the spec and above TMPDIR",
+  "statechart.mjs finds TLC with the real mise when an untrusted mise.toml is next to the spec and above a TMPDIR reached through a symlink",
   {
     skip:
       !tools || process.env.TLA2TOOLS
@@ -2018,7 +2053,8 @@ test(
     mkdirSync(tmp, { recursive: true });
     writeFileSync(join(dir, "mise.toml"), '[tools]\njava = "17"\n\n[env]\nSTATECHART = "1"\n');
     writeFileSync(join(dir, "upload.mmd"), fixture("upload.mmd"));
-    const env = { JAVA: "", TMPDIR: tmp };
+    symlinkSync(dir, join(root, "link"));
+    const env = { JAVA: "", TMPDIR: join(root, "link", "tmp") };
     const r = node("statechart.mjs", ["from-chart", "upload.mmd"], dir, env, at);
     assert.equal(r.status, 0, r.stderr);
     assert.equal(r.stderr, "");
@@ -6073,6 +6109,14 @@ const failRenames = `#define _GNU_SOURCE
 #include <string.h>
 #include <sys/stat.h>
 #include <unistd.h>
+#ifdef __APPLE__
+/* dyld replaces a function only through an __interpose entry, and there dlsym(RTLD_NEXT)
+   returns the replacement, so original() hands out libc's functions instead. */
+#define mkdir preloaded_mkdir
+#define rename preloaded_rename
+#define dlsym(handle, name) original(name)
+static void *original(const char *name);
+#endif
 static size_t hits;
 static int raced;
 static int removeOne(const char *path, const struct stat *s, int type, struct FTW *at) {
@@ -6158,13 +6202,26 @@ int rename(const char *from, const char *to) {
   if (renamed == 0 && named(to, "shared") && racing("when-made")) takeOver(to);
   return renamed;
 }
+#ifdef __APPLE__
+#undef mkdir
+#undef rename
+static void *original(const char *name) {
+  return strcmp(name, "mkdir") == 0 ? (void *)mkdir : (void *)rename;
+}
+__attribute__((used, section("__DATA,__interpose"))) static const void *interposed[][2] = {
+  {(const void *)preloaded_mkdir, (const void *)mkdir},
+  {(const void *)preloaded_rename, (const void *)rename},
+};
+#endif
 `;
+// macOS ignores LD_PRELOAD. Node's signature lets DYLD_INSERT_LIBRARIES load the library.
 const failingRenames = (() => {
   const dir = mkdtempSync(join(tmpdir(), "statechart-preload-"));
   writeFileSync(join(dir, "rename.c"), failRenames);
   const so = join(dir, "rename.so");
   const cc = spawnSync("cc", ["-shared", "-fPIC", "-o", so, join(dir, "rename.c"), "-ldl"]);
-  return cc.status === 0 ? so : null;
+  if (cc.status !== 0) return null;
+  return process.platform === "darwin" ? { DYLD_INSERT_LIBRARIES: so } : { LD_PRELOAD: so };
 })();
 test(
   "a run whose rename fails after it moves the output folder aside puts the folder back, or says where it is",
@@ -6178,7 +6235,7 @@ test(
     assert.equal(first.status, 0, first.stderr);
     const chart = readFileSync(join(shared, "chart.mmd"), "utf8");
     const run = (fails) =>
-      node("statechart.mjs", args, dir, { LD_PRELOAD: failingRenames, RENAME_FAILS: fails });
+      node("statechart.mjs", args, dir, { ...failingRenames, RENAME_FAILS: fails });
 
     const back = run("NI");
     assert.equal(back.status, 2, back.stderr);
@@ -6219,7 +6276,7 @@ test(
         `export const state = (v) => (v.on ? "On" : "Off");\nexport const step = () => "${label}";\n`,
       );
       const r = node("statechart.mjs", args, dir, {
-        LD_PRELOAD: failingRenames,
+        ...failingRenames,
         RENAME_CANNOT: cannot,
       });
       assert.equal(r.status, 0, r.stderr);
@@ -6238,7 +6295,7 @@ test(
     const shared = join(dir, "shared", "chart.mmd");
     const run = (anotherRun) =>
       node("statechart.mjs", ["from-spec", "Lamp.tla", "--out", "shared"], dir, {
-        LD_PRELOAD: failingRenames,
+        ...failingRenames,
         RENAME_CANNOT: "ENOSYS",
         ANOTHER_RUN: anotherRun,
       });
@@ -6268,7 +6325,7 @@ test(
     const dir = mkdtempSync(join(tmpdir(), "statechart-"));
     writeLamp(dir);
     const r = node("statechart.mjs", ["from-spec", "Lamp.tla", "--out", "shared"], dir, {
-      LD_PRELOAD: failingRenames,
+      ...failingRenames,
       RENAME_CANNOT: "ENOSYS",
       ANOTHER_RUN: "removed-during-copy",
     });
@@ -6289,7 +6346,7 @@ test(
     const dir = mkdtempSync(join(tmpdir(), "statechart-"));
     writeLamp(dir);
     const r = node("statechart.mjs", ["from-spec", "Lamp.tla", "--out", "shared"], dir, {
-      LD_PRELOAD: failingRenames,
+      ...failingRenames,
       RENAME_CANNOT: "ENOSYS",
       ANOTHER_RUN: "when-made",
     });