[jiangkoumo]

背景与改动

基于 main 33f1caf（对齐 upstream cursor/plugins@519d36aa），补齐以下四项跟进，未发布 npm：

1. poteto-help 措辞与索引更新：
   • 更新 statechart 这一行的新表述为上游 519d36aa 第 92 行：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（移除已废弃的 from-chart/--against 描述，避免误导）；
   • 在 /ketchup 行后补充新增的 /ketchup-video（上游第 76 行）；
   • 同步更新 docs/port-map.json reason 与 docs/skill-audit.md 表格行。
2. create-formal-verification-skill 补齐上游 #794 段落：
   • 逐字保留上游第 35 段（指导后续 agent 遇到 TLA+ 模型时使用 pstack /statechart 读取最短反例路径，按名称引用且不复制易变的机器参数）；
   • 增加 Pi 执行边界说明：正式 TLC 验证走受限的 verification_exec，画图走父 shell 的 statechart 入口，两者不互相替代，生成技能不写具体 jar 或机器路径。
3. statechart SKILL.md 阻断绕过 Pi 入口：
   • 将生成正文中残留的 "scripts/statechart.ts is TypeScript, so run it with a runtime that can execute TypeScript." 替换为显式要求使用 "node /adapters/pi/statechart/entry.mjs"，严禁直接执行原始脚本或 launcher（未配置 jar 时直接运行会导致 mise 自动下载）；
   • 在 scripts/statechart-adapter.test.mjs 增加断言并验证修前退出 1、修后退出 0。
4. docs/fidelity.md 重新生成并校验干净：
   • 重新生成为真实的 149 个文件、4753/5039 = 94.3243%，运行后工作区保持干净；
   • 包含 statechart 语料中 34 份 report.md（共 201 行，全部 100% 保真；若排除该部分，整体保真度约为 94.08%，仍高于 94% 门禁）。

验收结果（干净 clone / tmp 测试）

• npm ci --include=dev：成功安装 123 个包；
• npm test（无 TLC）：448 pass / 0 fail / 5 skip，38/38 检查通过；
• npm test（配置 TLC 1.8.0 与 Java 21）：453 pass / 0 fail / 0 skip，38/38 检查通过；
• npm run check:generate：527 项资源无漂移；
• npm run check:fidelity：4753/5039 = 94.3243%，跑完后 git status 保持干净；
• upstream/pstack/skills/statechart 407 份文件与 519d36aa 树通过 GitHub tree API 逐字节比对，mismatch 为 0，skills/statechart/scripts 相对 main 无改动。

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.