From 299f338df1ece254bace50d6b613685aa3628c50 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Tue, 20 Oct 2026 23:10:42 -0400 Subject: [PATCH 01/12] feat(pstack): merge Cursor pstack 0.15.26 to 0.15.29 skill content (#234) Apply scripts/upstream-merge.py from 99743e9 to 88d4751: 6 files verbatim, 3 clean merges, 3 for review. Add create-formal-verification-skill and maintain-formal-verification-skill, the ketchup, sharpen and typescript-best-practices changes, and the poteto-help routing and recipes. Resolve setup-pstack by keeping the port's step 9 and adding upstream's verification offers as steps 10 and 11. Resolve poteto-help by keeping the port's install lines, setup sentence and harness paragraph, and appending upstream's offers sentence. make-bot-ui stays absent. Co-Authored-By: Claude Opus 5.5 --- README-UPSTREAM.md | 29 +++++++--- .../create-formal-verification-skill/SKILL.md | 41 +++++++++++++ plugins/pstack/skills/ketchup/SKILL.md | 20 ++++--- .../SKILL.md | 58 +++++++++++++++++++ plugins/pstack/skills/poteto-help/SKILL.md | 9 ++- .../skills/poteto-help/references/recipes.md | 4 +- plugins/pstack/skills/setup-pstack/SKILL.md | 8 +++ plugins/pstack/skills/sharpen/SKILL.md | 13 ++++- .../skills/typescript-best-practices/SKILL.md | 2 +- .../references/patterns.md | 8 ++- 10 files changed, 168 insertions(+), 24 deletions(-) create mode 100644 plugins/pstack/skills/create-formal-verification-skill/SKILL.md create mode 100644 plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md diff --git a/README-UPSTREAM.md b/README-UPSTREAM.md index 4e8b8c2a..9fde3a06 100644 --- a/README-UPSTREAM.md +++ b/README-UPSTREAM.md @@ -4,7 +4,7 @@ i'm [poteto](https://x.com/poteto). i'm not a president or ceo, but i've worked there's a growing sense that ai writes too much slop code. i agree. i don't want to ship like a team of twenty slop artists. throughput without quality is not a goal i aspire to. if you want to go fast, go deep first. -**pstack is my answer.** these are the same skills i use everyday to ship high quality code at Cursor. this turns cursor into a real engineering team. the goal is not to maximize loc, in fact it's the opposite. pstack helps you write less, but higher quality code. +**pstack is my answer.** these are the same skills i use every day to ship high quality code at Cursor. this turns cursor into a real engineering team. the goal is not to maximize loc, in fact it's the opposite. pstack helps you write less, but higher quality code. **pstack gives you fearless parallelism.** when you can go deep on one agent and trust it to write good, verifiable code, you can truly parallelize with confidence. start multiple agents up with `poteto-mode` and trust that they'll apply rigorous engineering principles to their work. @@ -18,6 +18,17 @@ fork it. improve it. make it yours. PRs are welcome! /add-plugin pstack ``` +in claude code: + +```bash +/plugin marketplace add cursor/plugins +/plugin install pstack@cursor-plugins +``` + +claude code prefixes plugin commands and agents, so `/poteto-mode` is `/pstack:poteto-mode`. the [claude code adapter](./docs/harness/claude-code.md) maps every other cursor name. in claude code, `/pstack:setup-pstack` writes your model choices to `~/.claude/rules/pstack-models.md`, and a step that needs a cursor-only feature, such as bugbot or automations, is skipped with a one-line note. + +claude code installs a generated copy of pstack, including this readme and the guide, from [`harness/pstack/`](https://github.com/cursor/plugins/tree/main/harness/pstack) at the repository root. after you change pstack, run `node scripts/generate-pstack-harness-trees.mjs` from the repository root and commit the result. ci fails while the generated copy is out of date. + ## get started two steps: @@ -27,7 +38,7 @@ two steps: new here? the [pstack guide](./docs/guide/README.md) walks you through a first real task, from setup and prompting through verification and overnight runs. stuck, or unsure which skill fits? ask [`/poteto-help`](./skills/poteto-help/SKILL.md). -that's it. the other skills are situational; the mode skill uses them for you as needed. out of the box the mode splits work by model strength: code delegates (feature, refactoring, bug fix, perf, hillclimb) go to grok, while the hardest changes, prose, and judgment go to opus 5.5. the default panel is opus 5.5 / grok. [`/setup-pstack`](./skills/setup-pstack/SKILL.md) changes any of it. +that's it. the other skills are situational, and the mode skill uses them for you as needed. out of the box the mode splits work by model strength: code delegates (feature, refactoring, bug fix, perf, hillclimb) go to grok, while the hardest changes, prose, and judgment go to opus 5.5. the default panel is opus 5.5 / grok. [`/setup-pstack`](./skills/setup-pstack/SKILL.md) changes any of it. ## usage @@ -70,7 +81,7 @@ morning. | [shipping](./skills/poteto-mode/playbooks/shipping.md) | independently verify a green stack, then land the contiguous verified run bottom-up through github by default or origin when available. | | [autonomous run](./skills/poteto-mode/playbooks/autonomous-run.md) | drive a long task to completion without stopping. | | [orchestrate](./skills/poteto-mode/playbooks/orchestrate.md) | a standing project handed to one coordinator chat: multi-day, many stacked prs, fleets of subagents. | -| [autopilot-full](./skills/poteto-mode/playbooks/autopilot-full.md) | run independent prs to merged with one owner per pr and a root swarm verdict on each round, from the code-ready head on. | +| [autopilot-full](./skills/poteto-mode/playbooks/autopilot-full.md) | run independent prs to merged with one owner per pr. a swarm verifies each code-ready head, and every later change to the patch gets a fresh check. | | [autopilot-stack](./skills/poteto-mode/playbooks/autopilot-stack.md) | build and verify one linear base-branch stack for the operator to review and land. | | [session pickup](./skills/poteto-mode/playbooks/session-pickup.md) | resume or take over a prior agent's in-flight work. | | [pause safely](./skills/poteto-mode/playbooks/pause-safely.md) | suspend in-flight work cleanly so it can be resumed later. | @@ -90,7 +101,7 @@ when invoked it: the full rules and playbooks live in [`skills/poteto-mode/SKILL.md`](./skills/poteto-mode/SKILL.md). -to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it from the `/` menu and press option+enter (mac) or alt+enter (windows) instead of enter. that makes it a [custom mode](https://cursor.com/docs/skills), which cursor offers in the agents window and the cli. it stays in context every turn, applies itself when a playbook matches or the task needs rigor, and stays out of the way otherwise. plain enter attaches it to one message only. say so to opt out, or exit the mode to turn it off. +to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it from the `/` menu and press option+enter (mac) or alt+enter (windows) instead of enter. that makes it a [custom mode](https://cursor.com/docs/skills#using-a-skill-as-a-custom-mode), which cursor offers in the agents window and the cli. it stays in context every turn until you exit the mode. plain enter attaches it to one message only. [`/poteto-mode`](./skills/poteto-mode/SKILL.md) works extremely well with cursor's `/loop` command. you can make cursor work for many hours without sacrificing rigor. @@ -114,11 +125,11 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/poteto-mode`](./skills/poteto-mode/SKILL.md) | default entry point for any non-trivial task. | | [`/poteto-help`](./skills/poteto-help/SKILL.md) | you're new to pstack, or unsure which skill, playbook, or principle fits. finds out what you're trying to do, answers that part, and hands you a prompt to type. runs only when you type `/poteto-help`. | | [`/in-your-own-words`](./skills/in-your-own-words/SKILL.md) | you want the agent to play back your goal and the problem before it starts. runs only when you type `/in-your-own-words`. | -| [`/sharpen`](./skills/sharpen/SKILL.md) | you want a task approached the way a top expert would, aimed at what you're really after, without overspecifying it or deciding your choices for you. | +| [`/sharpen`](./skills/sharpen/SKILL.md) | you want a prompt made deeper, not bigger, before you send it: what a top professional would do that you didn't ask for, the raw material they'd start from, their methods and tools, and an outside check that the result is right. hands back the rewritten prompt and leaves your choices open. doesn't do the task. runs only when you type `/sharpen`. | | [`/how`](./skills/how/SKILL.md) | you want a walkthrough of how a subsystem works. | | [`/why`](./skills/why/SKILL.md) | you want to know why something was built this way. discovers available MCPs at run time and queries each evidence category in parallel (source control, issue tracker, long-form docs, real-time chat, infra observability, error tracking, analytics warehouse). | | [`/recall`](./skills/recall/SKILL.md) | you're starting or resuming work and want your recent context on a topic rebuilt from your own chat history and the shared record, handed back as a tight current-state brief. | -| [`/ketchup`](./skills/ketchup/SKILL.md) | you want what changed in this chat since your last message, in a few plain sentences and small visuals, with just enough context on each action item to make the call. | +| [`/ketchup`](./skills/ketchup/SKILL.md) | you want what changed in this chat since your last message, in plain words and small visuals, with every item waiting on you listed and decidable from the reply alone, even when that makes the reply long. | | [`/blast-radius`](./skills/blast-radius/SKILL.md) | you have a small-looking change and want to know what else it could break, with the one fact it's safe because of proven by running code, not asserted. | | [`/architect`](./skills/architect/SKILL.md) | you're about to write code that crosses a function boundary and want the caller's usage, types, and module shape settled first. | | [`/arena`](./skills/arena/SKILL.md) | you want N parallel attempts at the same thing, then to grab the best parts of each. | @@ -138,6 +149,8 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/show-me-your-work`](./skills/show-me-your-work/SKILL.md) | you want a reviewable decision trail. logs decisions to a tsv you can commit. | | [`/create-verification-skill`](./skills/create-verification-skill/SKILL.md) | your project has no scripted way to prove app behavior. generates a project-local verify skill with a feature map, for any language or platform. | | [`/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. | | [`/unslop`](./skills/unslop/SKILL.md) | you're cleaning up writing. removes AI tells. | | [`/bro`](./skills/bro/SKILL.md) | you want the last message restated in plain human language, no jargon. | | [`/technical-writing`](./skills/technical-writing/SKILL.md) | layered doc standard (Diátaxis + Google developer style + STE + Global English) for docs, RFCs, readmes, PR descriptions, commit messages. | @@ -245,7 +258,7 @@ a few things `poteto-mode` references but doesn't bundle: - `/deslop` and the `deslop` skill ship in the `cursor-team-kit` plugin. - `control-cli` (for CLIs and TUIs) and `control-ui` (for browser, Electron, web) ship in `cursor-team-kit` too. -- `/create-skill` is a cursor built-in. cursor also ships a built-in `/babysit`; inside `poteto-mode`, the [babysit playbook](./skills/poteto-mode/playbooks/babysit.md) supersedes it for pr-status requests. +- `/create-skill` is a cursor built-in. cursor also ships a built-in `/autopilot` that watches a pr. inside `poteto-mode`, pr-status requests go to the [babysit playbook](./skills/poteto-mode/playbooks/babysit.md) instead. install `cursor-team-kit` alongside pstack if you want the full set. @@ -267,7 +280,7 @@ when a default changes, a rule written before the change still pins the old defa pstack also ships a dormant [benny automation pack](./automations/benny/). benny triages slack issue reports, then reproduces and fixes confirmed bugs with real ui evidence. its files are not registered as slash skills. -to set it up, point cursor at [`FOR_AGENTS.md`](./automations/benny/FOR_AGENTS.md). setup copies the pack into the target repository at `.cursor/automations/benny/`, enables pstack there for shared skills, and keeps user configuration outside the copied pack. +to set it up, point cursor at [`FOR_AGENTS.md`](./automations/benny/FOR_AGENTS.md). setup copies the pack into the target repository at `.cursor/automations/benny/`, enables pstack there for shared skills, and keeps user configuration outside the copied pack. benny runs on cursor automations, so it is cursor-only. ## license diff --git a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md new file mode 100644 index 00000000..b97609fd --- /dev/null +++ b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md @@ -0,0 +1,41 @@ +--- +name: create-formal-verification-skill +description: "Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, \"model-check this race\", \"prove this invariant\", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests." +disable-model-invocation: true +--- + +# Create a formal verification skill + +A test checks the cases that someone thought to write. Formal verification checks every case in a stated scope: every order of steps in a model, every input up to a bound, or every input. This skill finds the part of the repo where that matters most, verifies one property of it, and leaves a project-local skill that lets the next agent check a change against that property. Write that skill for an agent who reads it cold, mid-change, and has never seen your work. The user must be able to trust the result and act on it without learning the verification language. + +## Choose the target from the code + +Answer from the codebase, and ask the user only what you cannot observe. If the user named an area or a bug, start there. + +A good target is a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. Choose the strongest such target in the repo, not the one that is easiest to verify. + +## Let the question choose the tool + +Pick the tool that answers the question at the lowest cost: a model checker, a proof assistant, an SMT-backed verifier, or another tool. Whether events can happen in a bad order usually suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually suits a verifier that runs on the code. If no verifier runs on this language, say so, and test the real code with generated inputs, not a hand model of the function. A property that must hold at every size, where a bound is not enough, can need a proof. Prefer a tool that the repo's developers can install and run, and tell the user why you chose it. + +## What makes it good + +- **True to the code.** Every part of the model or proof points to code that a reviewer can open. What the verification treats as one indivisible step is one indivisible step in the code. Names come from this repo. +- **Able to fail.** A check that you have never seen fail proves nothing. Show each property failing on a broken variant of the code it guards, such as a removed check or a reordered step. +- **Findings stay findings.** When the current code breaks the property, report it with the counterexample in the code's terms. Do not weaken the property or the model until it passes, and do not change product code unless the user asks. +- **Honest about scope.** Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system. +- **Readable without the tool.** State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words. +- **Cheap to rerun.** One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change. +- **Kept in step with the code.** Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look. + +## Generate the verify skill + +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. + +## Prove it before you hand off + +Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change. + +## Hand off + +Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at `/maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. diff --git a/plugins/pstack/skills/ketchup/SKILL.md b/plugins/pstack/skills/ketchup/SKILL.md index 8cd2bfd6..49e4d94c 100644 --- a/plugins/pstack/skills/ketchup/SKILL.md +++ b/plugins/pstack/skills/ketchup/SKILL.md @@ -1,12 +1,12 @@ --- name: ketchup -description: "Catch the user up on what changed in this chat since their last message, in a few plain sentences and small visuals. Give each action item just enough context to make the call. Use for /ketchup." +description: "Catch the user up on what changed in this chat since their last message, in plain words and small visuals. List every item waiting on them with what they need to decide it from the reply alone. Use for /ketchup." disable-model-invocation: true --- # Ketchup -Catch the user up on what changed in this chat since the last message they wrote before `/ketchup`, and help them understand each change, not only where it stands. Notifications and subagent results are not their messages. Assume the user remembers their last message and nothing after it. +Catch the user up on what changed in this chat since the last message they wrote before `/ketchup`, and help them understand each change, not only where it stands. Then lay out every call waiting on them so they can make it from your reply alone. Notifications and subagent results are not their messages. Assume the user remembers their last message and nothing after it. Use [`/bro`](../bro/SKILL.md)'s voice, not its task: plain words, short sentences, no jargon, like one person catching up another. Say what changed for the user, not how you did it. Say "the tests pass", not "CI is green". Leave out hashes, file paths, commands, build numbers, and test counts unless the user needs one to act. Call each PR, branch, or agent by a name the user would know, not by a label you invented. If a fact needs context to make sense, give the context or leave the fact out. @@ -14,24 +14,30 @@ Use [`/bro`](../bro/SKILL.md)'s voice, not its task: plain words, short sentence Keep this turn read-only. Make visuals only from what you already have: do not change code, start an app or a job, or post anything. Collect your own work since that message, reports from subagents, and messages from anyone else in this chat. Check the current state of each PR, CI run, or agent this chat touched. Check each number you will show against the facts it comes from, and say so when you correct one. -An action item is a decision or step only the user can take, such as a product choice, an approval, an irreversible action, or access you lack. Include any still waiting on the user, even one raised before their last message. Work you can still do yourself is not an action item. Never make up a call to fill the reply. A step the user did not ask for and the work does not need is not an action item, unless it is irreversible and waiting on the user: give it one action line, no visual, and skip what happens if the user does not answer. +An action item is a call or step only the user can take, such as a product choice, an approval, an irreversible action, or access you lack. Include any still waiting on the user, even one raised before their last message. Work you can still do yourself is not an action item. Never make up a call to fill the reply. A step the user did not ask for and the work does not need is not an action item, unless it is irreversible and waiting on the user: give it one line and no visual. + +One call can cover many items, such as each PR in a set awaiting merge. For each item, collect its link, what it changes for users, the evidence behind your pick, its risk, and your pick. Write "unknown" for a fact the call needs that you do not know. Leave out a link you do not have. ## Write the reply -Keep the whole reply well under 150 words, not counting visuals. When something is easier to grasp as a picture than as sentences, draw it: how a design or system works, a PR stack or dependency chain with each PR's state, a before and after of a fix, or options side by side. Never draw a status list or boxes with nothing connecting them. Never give a fact twice, in text or across visuals. Leave out work that changed nothing for the user. When words run short, cut from what happened before you cut from the action items. +Spend words on the calls, not on the story. Keep what happened under 100 words, not counting pictures, and shorter when less happened. Leave out work that changed nothing for the user. Give each item about 30 words. The reply grows with the number of items: two items need well under 150 words in all, not counting pictures, and thirty need far more. Never cut items or shrink them to stay under a word count: no count in place of a list, and no link in place of an item. A link can add depth, but the reply alone must be enough to decide. -Open with one sentence that says how many things need the user, or that nothing does. If nothing happened and nothing waits on the user, say so and stop. +Open with one short sentence that names what waits on the user, or says nothing does. The action items give the detail. If nothing happened and nothing waits on the user, say so and stop. Then show what happened, pictures first. Embed inline the screenshots and videos the work produced, then any diagram that explains a change. Then sum up in one short bullet per thing the user asked for: what came of it, and whether it is done, still running, failed, or not checked. Write each line the way you would say it out loud: "Search was slow from a missing index", not "Search review: done" or "Slow search: missing index". Name any bug found and fixed on the way. Each line must stay true when read alone. Never mark something done that still waits on the user, and leave out anything the action items say. Under the summary, give at most three short lines that change what the user knows or must do. Then name in one line any work left that you can do yourself. -Then list the action items as plain bullets, never as a diagram or box. Give each two lines, or one for an unasked irreversible step: the decision with your recommendation and why, then what happens if the user does not answer. Ask the call the user owns, such as merge, approve, or pick. A step you would take first goes in your recommendation. So does anything that must happen first, and anything that cannot be undone. Write "unknown" for a part you do not know. Link to the detail. +Then list the action items. Ask the call the user owns, such as merge, approve, or pick, and give your pick. A step you would take first goes in your pick. So does anything that must happen first, and anything that cannot be undone. Give the number or link of each PR, issue, or agent a call is about, also in a call between options. + +Fit the shape to the call. A call about one item is one bullet: the call, your pick, what it changes for users, the evidence behind your pick, and its risk, with the item named once. When items share a call, write the call and your pick once, then give each item its own bullet, riskiest first: its link and name, what it changes for users, the evidence behind your pick, and its risk. Name an item's pick only where it differs from the call's. Give each item's risk even when it is low, such as "Low risk: only the colors change." Say what waiting costs only when it is more than a delay, such as a deadline or lost data. -Show a choice after the list. If the screenshots above already show its options, write each option's gain and cost under its screenshot instead of drawing a new visual; otherwise, compare the options side by side, with the current state when there is one. Give every option the work weighed, each with what it gets the user and what it costs. Keep them out of the rest of the text. +For a call between options, give every option the work weighed, each with what it gets the user and what it costs, and the current state when there is one. Those costs are the call's risk, so add no separate risk line. When the screenshots above show the options, write each option's gain and cost under its screenshot. ## Visuals A visual is a picture: a screenshot, a video, a Mermaid diagram, a chart or diagram that the harness renders, or a generated image. A Markdown table is not a visual, even with before and after columns. +When something is easier to grasp as a picture than as sentences, draw it: how a design or system works, a PR stack or dependency chain with each PR's state, a before and after of a fix, or options side by side. Never draw a status list, a list of action items, or boxes with nothing connecting them. Never give a fact twice, in text or across visuals. + Keep each visual small enough to read at a glance: at most six boxes, with at most eight words in each. Write labels as plain words a person would say, not tags like "Tests: pass". A fact that needs a sentence belongs in the text, or nowhere. Embed screenshots and videos inline when the change is visible, not only as links. If a visible change has none, mark its summary line "No screenshot yet," and say there what changed on screen. Draw diagrams and charts from facts you have: a Mermaid diagram for how things connect and a rendered chart for numbers. Never invent a number, and never draw or generate a picture of a screen you did not capture. Link only artifacts that exist. diff --git a/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 00000000..5d2f7f22 --- /dev/null +++ b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,58 @@ +--- +name: maintain-formal-verification-skill +description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure is drift in the verification or a bug in the code. Use for /maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +disable-model-invocation: true +--- + +# Maintain a formal verification skill + +A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits. + +## Outcomes + +Give each check one outcome, and say which: + +- **in sync**: no change since the last sync alters what the check describes, and the check passes. +- **updated**: the code changed, the verification now describes the new code, and the check passes. +- **bug**: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift. +- **blocked**: the check could not be brought back in line or could not run. Say exactly why. + +A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it. + +## Edit scope + +Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure. + +## Pass + +1. **Find the checks.** A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at `/create-formal-verification-skill`. If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did. + +2. **Run it as it is.** Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5. + +3. **Read every change to covered code.** Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is: + - **No effect.** The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message. + - **The verification no longer describes the code.** A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change. + - **The promise changed on purpose.** The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence. + - **The promise may be broken.** The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate. + +4. **Update from the code, not from the result.** Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report. + +5. **Rerun and judge each result.** + - **Pass:** the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break. + - **Fail:** replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code. + +6. **Update the verify skill.** Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run. + +## Report + +Tell the user, for each check: + +- the outcome, and the commits that you read; +- what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence); +- the rerun result, and the break that you used to show the updated check can still fail; +- each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it; +- what the verification still does not cover, including new code that it should cover and does not. + +Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description. + +Put the verification updates in a change of their own, separate from any product fix. diff --git a/plugins/pstack/skills/poteto-help/SKILL.md b/plugins/pstack/skills/poteto-help/SKILL.md index 09ba3dbf..a3d12fd6 100644 --- a/plugins/pstack/skills/poteto-help/SKILL.md +++ b/plugins/pstack/skills/poteto-help/SKILL.md @@ -26,6 +26,7 @@ Check the state that changes the answer, and mention it only when it does: - No `pstack-models.md` in the active harness's config home means `/setup-pstack` hasn't run for this user, so every role uses its default model. Resolve the config home per [`codex-tools.md`](../poteto-mode/references/codex-tools.md#harness-config-homes). - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it records as last in sync, mention `/maintain-formal-verification-skill` if the question touches that code. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a requested effort now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -35,7 +36,7 @@ When the model rule is missing and it matters, ask whether the user wants to pic ## Get set up 1. Install. In Claude Code, run `/plugin marketplace add ericlitman/open-pstack`, then `/plugin install pstack@open-pstack`, then `/reload-plugins`. In Codex, run `codex plugin marketplace add ericlitman/open-pstack --ref main`, then `codex plugin add pstack@open-pstack`, and turn on `multi_agent` per [`codex-tools.md`](../poteto-mode/references/codex-tools.md). -2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. The sheet applies to new sessions. +2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. The sheet applies to new sessions. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. 3. Start a real task with `/poteto-mode`, a goal, and a check that can pass or fail. In Claude Code, a typed skill carries the plugin prefix, as in `/pstack:poteto-mode`. In Codex, ask for a skill by name, as in "use pstack:poteto-mode". The [README](https://github.com/ericlitman/open-pstack#readme) and [guide page 1](https://github.com/cursor/plugins/blob/main/pstack/docs/guide/01-setup.md) have the details. Offer to word their first prompt with them, per [`references/prompting.md`](references/prompting.md). @@ -64,12 +65,12 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste |---|---| | Do any non-trivial task with rigor | [`/poteto-mode`](../poteto-mode/SKILL.md) | | Check that the agent understood their goal and the problem before it starts | [`/in-your-own-words`](../in-your-own-words/SKILL.md) | -| Aim a task higher before starting: more expert, more outcome-focused, not overspecified | [`/sharpen`](../sharpen/SKILL.md) | +| Get a prompt rewritten deeper, not bigger, before sending it: what a top professional would add, their raw material and methods, and an outside check. It returns the prompt and doesn't do the task | [`/sharpen`](../sharpen/SKILL.md) | | Know how code works now, or where new code should live | [`/how`](../how/SKILL.md) | | Know why code is shaped this way, or where a number came from | [`/why`](../why/SKILL.md) | | Understand a change or subsystem, explained plainly | [`/teach`](../teach/SKILL.md) | | Catch up on their own recent work on a topic | [`/recall`](../recall/SKILL.md) | -| Catch up on what changed in this chat since their last message, in a few plain sentences and small visuals, with enough context to decide each action item | [`/ketchup`](../ketchup/SKILL.md) | +| Catch up on what changed in this chat since their last message, in plain words and small visuals, with every item waiting on them listed and decidable from the reply alone | [`/ketchup`](../ketchup/SKILL.md) | | Know what a small diff could break outside itself | [`/blast-radius`](../blast-radius/SKILL.md) | | Settle types and module shape before code that crosses a function boundary | [`/architect`](../architect/SKILL.md) | | Get several attempts at one brief, merged into the best one | [`/arena`](../arena/SKILL.md) | @@ -83,6 +84,8 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Hear the last reply again in plain words | [`/bro`](../bro/SKILL.md) | | Give agents a scripted way to drive the app and prove behavior | [`/create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | +| Formally verify a race, invariant, or other property that tests rarely reach | [`/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 | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/plugins/pstack/skills/poteto-help/references/recipes.md b/plugins/pstack/skills/poteto-help/references/recipes.md index d13da3a0..048e0750 100644 --- a/plugins/pstack/skills/poteto-help/references/recipes.md +++ b/plugins/pstack/skills/poteto-help/references/recipes.md @@ -6,7 +6,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode read . restate the underlying issue in your own words, in plain english.` - `/in-your-own-words ` -- `/sharpen ` +- `/sharpen ` - `/poteto-mode investigate why . give me what we know, what data you used, and your best hypotheses. don't change any code yet.` - `use /how to understand . then use /why to find out why it broke recently.` - `/recall my work on from last week, then read .` @@ -34,6 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/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 holds in , even when interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`. - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?` @@ -43,6 +44,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode im going to bed. in a fresh worktree off . done means . keep a decision log. don't ask me before committing. /loop until done. if you're truly stuck after a few hours, stop and write up why.` - `/show-me-your-work catch me up on what you did last night.` Read its Attention section first. +- `/ketchup` catches you up on this chat since your last message and lists every call that waits on you. - `/poteto-mode full autopilot on this queue. each item is independent.` - `/poteto-mode autopilot these changes but stack them, don't ship. i'll land the stack.` - `/reflect capture what we learned so the next run doesn't repeat it.` Approve only edits that change a future decision. diff --git a/plugins/pstack/skills/setup-pstack/SKILL.md b/plugins/pstack/skills/setup-pstack/SKILL.md index c1fd8f2a..22ca0f12 100644 --- a/plugins/pstack/skills/setup-pstack/SKILL.md +++ b/plugins/pstack/skills/setup-pstack/SKILL.md @@ -118,3 +118,11 @@ Do not copy the model sheet between harnesses without rerunning the parent-speci Before declaring setup complete, run one small read-only mixed panel from this parent: every distinct chosen descriptor, distinct output/receipt paths, and an independent cross-judge. Launch Claude-native agents and every external process in the background with retained handles, then drain them. Verify the native transcript entries and every external receipt. A structural config check or unit test is not a substitute. Report the sheet path, parent route table, requested-effort probe results, smoke results, and external elapsed/token/cost receipts. Re-running this skill re-probes and updates the same sheet. Do not claim the provider exposed hidden applied-effort observability. + +### 10. Offer a verification skill (optional) + +Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. + +### 11. Offer a formal verification skill (optional) + +Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. diff --git a/plugins/pstack/skills/sharpen/SKILL.md b/plugins/pstack/skills/sharpen/SKILL.md index 4f9bb4ab..5b4a7b10 100644 --- a/plugins/pstack/skills/sharpen/SKILL.md +++ b/plugins/pstack/skills/sharpen/SKILL.md @@ -1,7 +1,16 @@ --- name: sharpen -description: "Sharpen a task before starting: the expert approach, what the user is really after, and the right level of specification. Use for /sharpen." +description: "Make a task deeper, not bigger, then rewrite the prompt. Use for /sharpen." disable-model-invocation: true --- -Before starting, ask how a top expert would approach this task (their raw sources, their real methods, an outside check that the result is right), what the user is really after, and whether the task is over- or underspecified. Loosen constraints that don't serve the goal as readily as you add ones that do, and leave choices that are the user's to make open instead of deciding them. Fold in only what makes the work better, not bigger, but always keep one outside check that the result is right, without narrating the framing, then do the work. Don't hand back a rewritten prompt. +I want a deeper version of this task, not a bigger one. Before rewriting it, do four things: + +1. Say what a top professional in this field would do here that I'm not asking for. +2. Name the rawest material they would start from instead of what has already been digested for me. +3. Name the specific methods and tools they would use. +4. Say what, other than you or me, would show the result is right. + +Then rewrite my prompt to ask for exactly that. + +Leave choices that are mine to make open instead of deciding them. diff --git a/plugins/pstack/skills/typescript-best-practices/SKILL.md b/plugins/pstack/skills/typescript-best-practices/SKILL.md index 2bf543fb..33ebef76 100644 --- a/plugins/pstack/skills/typescript-best-practices/SKILL.md +++ b/plugins/pstack/skills/typescript-best-practices/SKILL.md @@ -11,7 +11,7 @@ Apply the **type-system-discipline** principle skill first. | Rule | Summary | |------|---------| | Discriminated unions | Model variants with a `kind` literal discriminant so impossible states can't be represented. No optional-field bags. | -| Branded types | Brand primitives with `& { readonly __brand: "X" }` so they can't be mixed up. Validate once at the boundary. | +| Branded types | Brand primitives with `& { readonly __brand: "X" }` so they can't be mixed up. Validate once at the boundary. A brand comes from a verifying type guard (`input is AgentId`), never from `as`. | | Constructive modeling | Build the shape so the illegal value can't be constructed. `[T, ...T[]]` for non-empty, `[T, T][]` for even length, `start` plus `duration` for a range. Not a runtime guard, not a wish for refinement types. | | Simplest total type | Keep `T[]` while every operation on it stays total. Strengthen to `NonEmpty` only where the loose type forces `!`, a cast, or a "should never happen" throw. | | `unknown` over `any` | External data is `unknown`. | diff --git a/plugins/pstack/skills/typescript-best-practices/references/patterns.md b/plugins/pstack/skills/typescript-best-practices/references/patterns.md index c21d876b..f8dd99b6 100644 --- a/plugins/pstack/skills/typescript-best-practices/references/patterns.md +++ b/plugins/pstack/skills/typescript-best-practices/references/patterns.md @@ -9,9 +9,13 @@ Brand primitives so they can't be mixed up. Validate once at the boundary. Downs ```ts type AgentId = string & { readonly __brand: "AgentId" }; +function isAgentId(input: string): input is AgentId { + return isUUID(input); +} + function parseAgentId(input: string): AgentId { - if (!isUUID(input)) throw new Error(`Invalid agent id: ${input}`); - return input as AgentId; + if (!isAgentId(input)) throw new Error(`Invalid agent id: ${input}`); + return input; } function focusAgent(id: AgentId): void { From 614075f5abceef0b8d22497bddb13dc55c10872a Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Tue, 20 Oct 2026 23:11:21 -0400 Subject: [PATCH 02/12] fix(pstack): keep create-formal-verification-skill model-invocable (#234) Setup's new formal verification offer invokes the skill, and disable-model-invocation blocks that route on Claude Code. Drop the flag, guard it in the routed-skill invariant, and register both formal verification skills with the verifier. Co-Authored-By: Claude Opus 5.5 --- .claude/skills/verify-open-pstack/features/registry.json | 5 +++-- .../pstack/skills/create-formal-verification-skill/SKILL.md | 1 - tests/skill-collision-repro.sh | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/registry.json b/.claude/skills/verify-open-pstack/features/registry.json index 21ad3caf..88ad664d 100644 --- a/.claude/skills/verify-open-pstack/features/registry.json +++ b/.claude/skills/verify-open-pstack/features/registry.json @@ -1,8 +1,9 @@ { "skills": [ "architect", "arena", "automate-me", "babysit", "benchmark-checklist", "blast-radius", "bro", "correct", - "create-verification-skill", "deslop", "figure-it-out", "fix-ci", "fix-merge-conflicts", - "get-pr-comments", "how", "in-your-own-words", "interrogate", "ketchup", "maintain-verification-skill", + "create-formal-verification-skill", "create-verification-skill", "deslop", "figure-it-out", + "fix-ci", "fix-merge-conflicts", "get-pr-comments", "how", "in-your-own-words", "interrogate", + "ketchup", "maintain-formal-verification-skill", "maintain-verification-skill", "make-pr-easy-to-review", "no-comments", "poteto-help", "poteto-mode", "principle-attack-the-premise", "principle-boundary-discipline", "principle-build-the-lever", "principle-encode-lessons-in-structure", "principle-exhaust-the-design-space", diff --git a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md index b97609fd..a950e12d 100644 --- a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md @@ -1,7 +1,6 @@ --- name: create-formal-verification-skill description: "Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, \"model-check this race\", \"prove this invariant\", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests." -disable-model-invocation: true --- # Create a formal verification skill diff --git a/tests/skill-collision-repro.sh b/tests/skill-collision-repro.sh index 9c31aa66..5ba4dfd4 100755 --- a/tests/skill-collision-repro.sh +++ b/tests/skill-collision-repro.sh @@ -333,7 +333,7 @@ else note "ok: excluded upstream skills stay absent" fi -routed_model_skills=(how why unslop typescript-best-practices) +routed_model_skills=(how why unslop typescript-best-practices create-formal-verification-skill) routed_model_bad="" for name in "${routed_model_skills[@]}"; do routed_skill="$plugin/skills/$name/SKILL.md" From cd3b3f35fa58351542cd01472e79cc52ef9f4b35 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Tue, 20 Oct 2026 23:12:34 -0400 Subject: [PATCH 03/12] fix(pstack): let a qualifying setup rerun keep the sheet without asking (#46) On a rerun whose sheet loads with a valid setting line, with no named change and no inconsistency or kept-predecessor choice, setup validates, prints the kept roles and efforts, probes, and writes without the step 2, 4 and 7 questions when every probe passes. The verification offers print one line each. Validation, permission checks, snapshots, readback and the smoke test still run, and a failed probe still stops without writing. Co-Authored-By: Claude Opus 5.5 --- plugins/pstack/skills/poteto-help/SKILL.md | 2 +- plugins/pstack/skills/setup-pstack/SKILL.md | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/plugins/pstack/skills/poteto-help/SKILL.md b/plugins/pstack/skills/poteto-help/SKILL.md index a3d12fd6..63610b96 100644 --- a/plugins/pstack/skills/poteto-help/SKILL.md +++ b/plugins/pstack/skills/poteto-help/SKILL.md @@ -36,7 +36,7 @@ When the model rule is missing and it matters, ask whether the user wants to pic ## Get set up 1. Install. In Claude Code, run `/plugin marketplace add ericlitman/open-pstack`, then `/plugin install pstack@open-pstack`, then `/reload-plugins`. In Codex, run `codex plugin marketplace add ericlitman/open-pstack --ref main`, then `codex plugin add pstack@open-pstack`, and turn on `multi_agent` per [`codex-tools.md`](../poteto-mode/references/codex-tools.md). -2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. The sheet applies to new sessions. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. +2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. A rerun that keeps a valid sheet and names no change asks none of these questions: it keeps the sheet's roles and efforts, probes them, and writes when every probe passes. The sheet applies to new sessions. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. On a rerun that keeps the sheet, it mentions each offer in one line instead of asking. 3. Start a real task with `/poteto-mode`, a goal, and a check that can pass or fail. In Claude Code, a typed skill carries the plugin prefix, as in `/pstack:poteto-mode`. In Codex, ask for a skill by name, as in "use pstack:poteto-mode". The [README](https://github.com/ericlitman/open-pstack#readme) and [guide page 1](https://github.com/cursor/plugins/blob/main/pstack/docs/guide/01-setup.md) have the details. Offer to word their first prompt with them, per [`references/prompting.md`](references/prompting.md). diff --git a/plugins/pstack/skills/setup-pstack/SKILL.md b/plugins/pstack/skills/setup-pstack/SKILL.md index 22ca0f12..9da5cb0a 100644 --- a/plugins/pstack/skills/setup-pstack/SKILL.md +++ b/plugins/pstack/skills/setup-pstack/SKILL.md @@ -39,7 +39,9 @@ The line `codex writer sandbox: full-access` or `codex writer sandbox: bounded` Treat the normalized values as current role-to-family assignments. Overlay those rows on the complete first-run role map, the catalog's [role defaults](../poteto-mode/references/model-catalog.md#role-defaults). Materialize any missing documented role row from that map on the next successful write. A duplicate role row is inconsistent state; report it and resolve it before probing. A row whose role is not in the role defaults, such as `how critics`, is from a retired role. Drop it and list it at confirmation. A bare host-native slug from an older sheet is also invalid because it does not say which provider owns it. A versioned Claude model that matches no matrix row, kept predecessor, or rolling alias remains inconsistent state. A value whose `(provider, model)` is a [kept predecessor](../poteto-mode/references/model-catalog.md#kept-predecessors-and-normalization) is not inconsistent state. On a rerun, propose replacing every occurrence with its family's current model at the same effort, and ask. If the operator declines, that family's model stays the kept predecessor for steps 3 to 7: probe it, render it, and write it unchanged. If the sheet is missing, seed from the role defaults, whose descriptors carry the model matrix's Default effort cells. -Then ask whether to keep these role-to-family assignments or change named roles. Keeping them is the default. Apply only role changes the operator names; never offer a reset of a customized sheet to the first-run assignments. A changed role may use any model-matrix family, `inherit-parent`, or `auto`. +A qualifying rerun is a rerun whose sheet loaded, whose loaded state has one valid setting line, on which the operator names no change, and where no inconsistency or kept-predecessor proposal needs a choice. On a qualifying rerun, validate in step 3. If that passes without resolving an inconsistency, keep the role assignments and efforts and print them instead of asking the questions in steps 2 and 4. If every step 5 probe then passes, print the step 7 table and write without step 7's confirmation. The qualifying rerun skips no validation, permission check, snapshot, readback, or the step 9 smoke test. + +Otherwise, ask whether to keep these role-to-family assignments or change named roles. Keeping them is the default. Apply only role changes the operator names; never offer a reset of a customized sheet to the first-run assignments. A changed role may use any model-matrix family, `inherit-parent`, or `auto`. If the loaded state has no setting line, ask once whether Codex writer lanes that the external runner launches should run with Codex's full-access sandbox. Say that full access lets the writer launch a browser and write dot-folders such as `.agents/`, and that it removes every sandbox limit, including filesystem confinement to the worktree. Declining is the default. Record `codex writer sandbox: full-access` on a yes and `codex writer sandbox: bounded` on a decline, so a rerun does not ask again. When the line exists, keep it unless the operator names a change, and do not ask. @@ -55,7 +57,7 @@ One distinct effort per family is the current value. A family with no non-alias ### 4. Collect one requested effort per family -Ask one effort question for each assigned family. Name each model, its current or proposed value, and the Selectable efforts from its matrix row. A family whose only selectable effort is `default` gets no effort question. Empty input keeps that value. On a first run, state the assigned families' matrix defaults before asking. On a rerun, state the parsed values without offering to reset customized role lanes. +Except on the qualifying rerun above, ask one effort question for each assigned family. Name each model, its current or proposed value, and the Selectable efforts from its matrix row. A family whose only selectable effort is `default` gets no effort question. Empty input keeps that value. On a first run, state the assigned families' matrix defaults before asking. On a rerun, state the parsed values without offering to reset customized role lanes. ### 5. Probe the requested pairs @@ -91,13 +93,13 @@ Rewrite every matrix-family descriptor to `provider:model@/pstack-models.md`, the route table for this parent, every rendered role and descriptor, and the setting line. Carry the loaded assignments into the new destination; only explicit role or effort changes and the documented normalization may change them. Ask for confirmation before writing. +Show any rolling-alias migrations as original and normalized descriptors and any retired-role rows dropped in step 2. Then show the source file read in step 2, the new destination `/pstack-models.md`, the route table for this parent, every rendered role and descriptor, and the setting line. Carry the loaded assignments into the new destination; only explicit role or effort changes and the documented normalization may change them. Ask for confirmation before writing, unless the qualifying rerun's probes all passed. Why and Reflect require the parent's live MCP surface. Keep their investigator, reviewer, and synthesizer roles on `inherit-parent` or `auto`; the bounded external runner deliberately omits ambient MCPs. `inherit-parent` and `auto` always validate, but say when they reduce a panel's provider diversity. For panel roles, one lane runs per entry. The list length is the fan-out count. `arena cross-judge pool` is a list from which Arena chooses a provider different from the parent and base candidate when possible. `swarm workers` is the default for every worker unless a race explicitly assigns another descriptor. Every non-alias role value must match `:@` and must have passed step 5. -After the operator confirms, separately check the parent's effective write permission for **both actual destinations** (the sheet and parent integration, resolved through `CODEX_HOME` when set) and any directory creation needed. Render both artifacts in memory and perform this check before the first write or directory creation. Native probes succeeding does not grant configuration-write permission. A restricted parent may still be allowed to write under `CODEX_HOME`; assess each resolved destination rather than rejecting it just because it is outside the workspace. If either destination is denied or its permission remains unknown, stop with the destination-specific explanation: leave every existing artifact byte-identical and create neither artifact on a first run. Do not test permission by overwriting a target, write only the allowed artifact, or automatically request escalation. +After the operator confirms, or the qualifying rerun's probes all pass, separately check the parent's effective write permission for **both actual destinations** (the sheet and parent integration, resolved through `CODEX_HOME` when set) and any directory creation needed. Render both artifacts in memory and perform this check before the first write or directory creation. Native probes succeeding does not grant configuration-write permission. A restricted parent may still be allowed to write under `CODEX_HOME`; assess each resolved destination rather than rejecting it just because it is outside the workspace. If either destination is denied or its permission remains unknown, stop with the destination-specific explanation: leave every existing artifact byte-identical and create neither artifact on a first run. Do not test permission by overwriting a target, write only the allowed artifact, or automatically request escalation. Only after both destinations are permitted, write the in-memory render from step 6 using step 8's snapshot and readback procedure. Never paste the role defaults as the result. They only seed step 2; selected efforts and explicit role changes always replace their values before writing. @@ -109,7 +111,7 @@ On Claude, the integration is the one `@` import line in `/CLAUDE.m On Codex, the integration is the exact sheet bytes between one `` and `` pair in `/AGENTS.md`. Replace that whole bounded block on a rerun. Insert one block at the end on first run. If either marker is missing, duplicated, or reversed, stop and report inconsistent state instead of guessing a boundary. -Snapshot every target's current bytes. Write the sheet and parent integration only after every requested pair passes and the operator confirms. Read both targets back and compare them with the in-memory render. If either write or readback fails, restore every snapshot and report the failure. An unchanged rerun must produce byte-identical sheet and integration content after normalization. +Snapshot every target's current bytes. Write the sheet and parent integration only after every requested pair passes and the operator confirms or the rerun qualifies. Read both targets back and compare them with the in-memory render. If either write or readback fails, restore every snapshot and report the failure. An unchanged rerun must produce byte-identical sheet and integration content after normalization. Do not copy the model sheet between harnesses without rerunning the parent-specific probes; route availability can differ even on the same host. @@ -121,8 +123,8 @@ Report the sheet path, parent route table, requested-effort probe results, smoke ### 10. Offer a verification skill (optional) -Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. +Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. On the qualifying rerun, mention this offer in one line instead of asking, and do not invoke the skill. ### 11. Offer a formal verification skill (optional) -Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. +Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. On the qualifying rerun, mention this offer in one line instead of asking, and do not invoke the skill. From d2ff01e0aa156ce383690d5b3818956bb9142e70 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Tue, 20 Oct 2026 23:14:16 -0400 Subject: [PATCH 04/12] feat(pstack): cover the quiet setup rerun and declined offers in the verifier (#46) Every setup prompt now declines setup's two verification offers, and first-run asserts that the fixture gained no project skill directory. keep-setting now starts from a complete sheet with the full-access line and an agreeing Codex mirror, gives no answers, and requires both files to keep their bytes with no AskUserQuestion call. keep-predecessor still covers missing-role completion. Co-Authored-By: Claude Opus 5.5 --- .../verify-open-pstack/features/recipes.ts | 27 +++++----- .../verify-open-pstack/features/setup.md | 2 +- .../scripts/catalog.test.ts | 50 ++++++++++++------- 3 files changed, 46 insertions(+), 33 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 0a83f5ed..0990de3f 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -31,6 +31,7 @@ export const CLAUDE_TOOLS = 'Skill,Read,Glob,Grep,Write,Edit,Bash,Agent,Task,Tod export const DEFAULT_ROLES: Record = { claude: 'bug-fix', codex: 'judgment and prose' }; export const ROUTE = /^([a-z][a-z0-9-]*):([A-Za-z0-9._/-]+)@([a-z]+)$/; const SETUP_DESCRIPTOR = 'claude:opus@high'; +const DECLINE_OFFERS = 'If setup offers to generate a verification skill or a formal verification skill, decline both.'; const DESCRIPTOR = /\b[a-z][a-z0-9-]*:[A-Za-z0-9._/-]+@[a-z]+/g; const SHEET_HEADER = '# pstack model configuration\n\n'; const SETTING = 'codex writer sandbox: '; @@ -415,7 +416,8 @@ const setup: Case[] = [{ const text = await readFile(sheet, 'utf8'); if (!Bun.deepEquals(roleLines(text), [...(await readCatalog(f.location)).defaults].map(([role, lanes]) => `${role}: ${lanes.join(', ')}`))) throw new Error('first-run-not-role-defaults'); bounded(text); - return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`], files: [sheet] }; + for (const skills of ['.claude/skills', '.agents/skills']) if (await lstat(join(f.dir, skills)).then(() => true, () => false)) throw new Error(`first-run-offer-accepted:${skills}`); + return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`, 'offers-declined'], files: [sheet] }; }, }]; @@ -555,25 +557,24 @@ function writerRefusal(): Case { } function keepSetting(): Case { - let expected: string[] = []; + let sheetBytes = '', mirrorBytes = ''; return { id: 'keep-setting', codexSandbox: 'danger-full-access', claudePermission: 'bypassPermissions', async prepare(f) { - const roles = [...(await readCatalog(f.location)).defaults]; - const omitted = roles.find(([, lanes]) => lanes.every(lane => !lane.includes(':')))?.[0]; - expected = roles.map(([role, lanes]) => `${role}: ${lanes.join(', ')}`).sort(); - await writeFile(join(f.configHome, 'pstack-models.md'), sheetText(roles.filter(([role]) => role !== omitted)) + `${FULL_ACCESS_SETTING}\n`); - if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); + sheetBytes = sheetText([...(await readCatalog(f.location)).defaults]) + `${FULL_ACCESS_SETTING}\n`; + mirrorBytes = `${MIRROR_BEGIN}\n${sheetBytes}${MIRROR_END}\n`; + await writeFile(join(f.configHome, 'pstack-models.md'), sheetBytes); + if (f.harness === 'codex') await writeFile(join(f.configHome, 'AGENTS.md'), mirrorBytes); }, - prompt: f => `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep every role assignment and every family's current effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, + prompt: f => `${invoke(f.harness, 'setup-pstack', `Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; - const text = await readFile(sheet, 'utf8'); - if (!Bun.deepEquals(settingLines(text), [FULL_ACCESS_SETTING])) throw new Error('setting-not-kept'); - if (!Bun.deepEquals(roleLines(text).sort(), expected)) throw new Error('keep-setting-sheet-mismatch'); - return { assertions: [...assertions, ...await mirrored(f, sheet), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; + if (record.tools.some(t => t.name === 'AskUserQuestion')) throw new Error('keep-setting-asked'); + if (await readFile(sheet, 'utf8') !== sheetBytes) throw new Error('keep-setting-sheet-changed'); + if (f.harness === 'codex' && await readFile(join(f.configHome, 'AGENTS.md'), 'utf8').catch(() => '') !== mirrorBytes) throw new Error('keep-setting-mirror-changed'); + return { assertions: [...assertions, 'no-question', 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; }, }; } @@ -687,7 +688,7 @@ export function recipe(feature: string, harness: Harness, routes: string[] = []) if (feature === 'project-skill') return [projectSkill]; if (feature === 'hook:startup') return [startupHook]; if (feature === 'runner') return runner(harness, routes); - if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup; + if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup.map(c => ({ ...c, prompt: f => `${c.prompt(f)} ${DECLINE_OFFERS}` })); if (feature === 'catalog') return catalog(harness); if (feature === 'shipped-tools') return [shippedTools]; if (feature === 'agent-preload:poteto-agent' && harness === 'claude') return [agentPreload]; diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index bc2fc7a3..05f51a41 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's role defaults with one alias role left out and the line `codex writer sandbox: full-access`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that the rewritten sheet holds that setting line exactly once and that its role lines equal the role defaults. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers. It asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, and that the Claude session made no `AskUserQuestion` call. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. Every setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index 9644c074..bbbf8347 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -291,6 +291,12 @@ test('the first-run case requires a sheet equal to the catalog role defaults', a await rejectsUnbounded(c, f, written); await writeFile(path, `# pstack model configuration\n\n${lines.slice(1).join('\n')}\n`); await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow('first-run-not-role-defaults'); + await writeFile(path, written); + for (const skills of ['.claude/skills', '.agents/skills']) { + await mkdir(join(f.dir, skills), { recursive: true }); + await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow(`first-run-offer-accepted:${skills}`); + await rm(join(f.dir, skills.split('/')[0]!), { recursive: true }); + } }); test('the configure case answers yes to full access and requires that setting with only the Opus descriptor', async () => { @@ -341,31 +347,37 @@ test('the full-access writer case quotes each browser argument for sh and encode }); for (const harness of ['claude', 'codex'] as const) { - test(`${harness}: the keep-setting case requires the setting line and every role line after a rerun`, async () => { + test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror with no question`, async () => { const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!, installed = await readCatalog(location); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); await c.prepare!(f); - if (harness === 'codex') await expect(readFile(join(f.dir, 'AGENTS.md'))).rejects.toThrow(); - else expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe('mirror\n'); const path = join(f.dir, 'pstack-models.md'), prepared = await readFile(path, 'utf8'); - expect(prepared).toEndWith('\ncodex writer sandbox: full-access\n'); - const omitted = [...installed.defaults.keys()].find(role => !prepared.includes(`\n${role}: `))!; - expect(installed.defaults.get(omitted)).toEqual(['inherit-parent']); - const rerun = prepared.replace('codex writer sandbox: full-access\n', `${omitted}: inherit-parent\ncodex writer sandbox: full-access\n`); - await writeFile(path, rerun); - if (harness === 'codex') await mirror(f, rerun); - expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions) - .toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'codex' ? ['codex-mirror'] : []), 'setting:codex writer sandbox: full-access']); - - for (const [wrong, reason] of [ - [rerun.replace('codex writer sandbox: full-access\n', ''), 'setting-not-kept'], - [rerun.replace('sandbox: full-access', 'sandbox: bounded'), 'setting-not-kept'], - [rerun.replace(/\nbug-fix: [^\n]*/, ''), 'keep-setting-sheet-mismatch'], - ]) { - await writeFile(path, wrong!); - await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow(reason); + expect(prepared).toBe(`# pstack model configuration\n\n${[...installed.defaults].map(([role, lanes]) => `${role}: ${lanes.join(', ')}`).join('\n')}\n${FULL_ACCESS}`); + const agents = harness === 'codex' ? `\n${prepared}\n` : 'mirror\n'; + expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe(agents); + expect(c.prompt(f)).not.toContain('Use these answers'); + await writeFile(path, prepared); + expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', 'no-question', 'sheet-unchanged', + ...(harness === 'codex' ? ['codex-mirror-unchanged'] : []), 'setting:codex writer sandbox: full-access']); + + const asked = record(harness, 'pstack:setup-pstack'); + asked.tools.push({ name: 'AskUserQuestion', id: 'q', input: {}, parent: null, failed: true }); + await expect(c.assert(asked, f)).rejects.toThrow('keep-setting-asked'); + for (const wrong of [prepared.replace(FULL_ACCESS, ''), prepared.replace(FULL_ACCESS, BOUNDED), prepared.replace(/\nbug-fix: [^\n]*/, ''), `${prepared}\n`]) { + await writeFile(path, wrong); + await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow('keep-setting-sheet-changed'); + } + await writeFile(path, prepared); + if (harness === 'codex') { + await writeFile(join(f.dir, 'AGENTS.md'), `notes\n${agents}`); + await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow('keep-setting-mirror-changed'); } }); + + test(`${harness}: every setup prompt declines both verification offers`, async () => { + const f = await fixture(harness); + for (const c of recipe('setup', harness)) expect(c.prompt(f)).toEndWith('If setup offers to generate a verification skill or a formal verification skill, decline both.'); + }); } const FAKE_CODEX = `#!/bin/sh From 7bca76807bac5d042501707773434f9cd4dc64d1 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Tue, 20 Oct 2026 23:16:34 -0400 Subject: [PATCH 05/12] chore: record the Cursor pstack 0.15.29 sync and release 1.16.0 (#234) UPSTREAM.md moves the sync point to 88d4751 (pstack 0.15.29), records the new exclusions and adaptations, adds the #46 ledger entry, and refreshes "Incorporate a change" from this run (#106). NOTICE.md gains a 0.15.26 to 0.15.29 provenance row, CHANGES.md a 1.16.0 section, and README.md and docs/reference.md the two formal verification skills, the new /sharpen, the version, the cursor-plugins install note and the Claude writer lane host requirement. Both manifests and the marketplace move to 1.16.0. Co-Authored-By: Claude Opus 5.5 --- .claude-plugin/marketplace.json | 2 +- CHANGES.md | 18 +++++++++- NOTICE.md | 1 + README.md | 8 +++-- UPSTREAM.md | 44 ++++++++++++++++------- docs/reference.md | 9 +++-- plugins/pstack/.claude-plugin/plugin.json | 2 +- plugins/pstack/.codex-plugin/plugin.json | 2 +- 8 files changed, 64 insertions(+), 22 deletions(-) diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 4c9f4e8e..9f37ce02 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -9,7 +9,7 @@ "name": "pstack", "source": "./plugins/pstack", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", - "version": "1.15.0", + "version": "1.16.0", "author": { "name": "Lauren Tan (original)" }, diff --git a/CHANGES.md b/CHANGES.md index 33ce1a5f..a0416069 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,12 +3,28 @@ Mergify auto-queue is live: ready PRs to main require passing verify, Unfret and exact-head live-gate, and no unresolved review thread; workflow changes require operator queueing. This port applies the Cursor → Claude Code substitutions in skill bodies. Earlier drafts left them flagged; this revision resolves them. A later pass added a Codex build that shares the same skills; see [Codex port](#codex-port) below. -## Unreleased +## 1.16.0 syncs to Cursor pstack 0.15.29 + +Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. Sixteen upstream commits since 0.15.25 touch pstack. Nine change skill content, and all nine are applied with the port adaptations below. `a968159` names two skills after their folders: the port's `poteto-mode` already complies, and `make-bot-ui` stays out. Three add upstream's own Claude Code install and a docs check, which stay out apart from their README text. Three bump only the Cursor manifests and guide, which stay out. The release also fixes #46, and ships Claude Haiku 5.5 lanes (#223), foreground waits on Claude Code (#232, #233) and the comment sweep (#218), all merged after 1.15.0. Default roles and panels are unchanged. **Claude Haiku 5.5 lanes.** The model catalog registers `claude:claude-haiku-5-5` as an exact pin, with five native agents, `pstack-haiku-5-5-low` to `pstack-haiku-5-5-max`, and efforts `low` to `max`. On a Claude Code parent an unregistered Claude model is a dropout, so this is the first way to run Haiku lanes there. The pin is optional; no role default changes. The catalog registers no `haiku` alias, because Claude Code resolves that alias to Haiku 4.5, which has no effort setting, on Bedrock, Vertex and Foundry (#223, by @jwerby). **Claude Code subagents wait in the foreground.** The generated `pstack--` agents no longer set `background: true`, which Claude Code honored over a caller's `run_in_background: false` (#233). `references/codex-tools.md` has a Waits on Claude Code section: the main session runs long commands and fan-outs in the background, and a subagent dispatches the lanes it needs in the foreground, runs `watch-pr` in the foreground with `--timeout 240` instead of `/loop`, and waits on a background task in one bounded foreground call (#232). Provider dispatch, poteto-mode, babysit step 6 and `docs/reference.md` point to that section. +**New skills.** `/create-formal-verification-skill` generates a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, with TLA+ as the default tool and a fallback when no verifier fits. `/maintain-formal-verification-skill` finds the commits that touched verified code, brings the model and properties back in line, reruns them, and says whether each failure is drift or a bug. It runs only when typed. + +**Setup offers.** After its smoke test, setup offers once each to generate a verification skill and a formal verification skill, unless the project already has one. + +**Quiet setup reruns (#46).** On a rerun whose sheet loads with one valid setting line, with no change named and no inconsistency or kept-predecessor choice, setup no longer asks to keep the roles, asks no effort per family, and writes without a confirmation when every probe passes. It prints the kept roles, efforts and table, and mentions each verification offer in one line. Validation, permission checks, snapshots, readback and the smoke test still run, and a failed probe still stops without writing. A first run, an invalid sheet, a kept-predecessor proposal or a named change still asks. + +**Changed behavior.** `/sharpen` now returns a rewritten prompt and does not do the task: it says what a top professional would add, their raw material, methods and an outside check, then rewrites the prompt to ask for that. `/ketchup` lists every item waiting on the user, so each call is decidable from the reply, and never cuts items to stay under a word count. `typescript-best-practices` makes a brand with a type guard instead of `as`. `poteto-help` routes to the two formal verification skills and adds recipes for them and `/ketchup`. + +**Comments sweep (#218).** Code this repository owns drops comments outside the keep-list in `AGENTS.md`, across the runner, the Codex transcript resolver, the startup hook, the verifier, tests and repository config. A test keeps every model pair released by 1.15.0 in place. + +**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills, every setup recipe declines both offers, `first-run` asserts that no project skill directory appears, and `keep-setting` checks a quiet rerun. + +**Not applied.** See `UPSTREAM.md`: upstream's generated Claude Code tree, its adapter, generator, plugin validator and root marketplace entry, the docs-vs-tree check, the two `poteto-help` harness paragraphs, `make-bot-ui`, and the 0.15.26 to 0.15.29 manifests and guide. Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install one of the two, because both use the `pstack:` prefix. `README-UPSTREAM.md` is the verbatim upstream README. + ## 1.15.0 runs Devin, agy and dsh lanes in any repository Open Pstack 1.15.0 keeps the Cursor pstack 0.15.25 sync. It ships PR #215, merged after 1.14.0. Default roles and panels are unchanged. diff --git a/NOTICE.md b/NOTICE.md index c40ec501..7ceac4a1 100644 --- a/NOTICE.md +++ b/NOTICE.md @@ -24,6 +24,7 @@ This plugin is a port of upstream MIT-licensed work. All upstream copyright noti | `plugins/pstack/skills/` (0.15.6 to 0.15.17 changes: `benchmark-checklist`, `correct`, `ketchup`, `poteto-help`, `principle-explain-the-number`, architect red flags, fresh subagents, hourly audit tick, PR headings, performance mantras, prompt distillation), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 978ca6e](https://github.com/cursor/plugins/tree/978ca6e9c0e012047cd5058b8e829240336e704e/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | | `plugins/pstack/skills/` (0.15.18 to 0.15.20 changes: `ketchup` before-and-after visuals, prompt cuts in `how`, `why`, poteto-mode playbooks, and four principles, the `/poteto-mode` chat as the playbook runner, `create-verification-skill` usable readiness, plan-checker fences, `watch-pr` review-thread pagination, `worktree-audit.sh -b`), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 1b6d44f](https://github.com/cursor/plugins/tree/1b6d44ff26d4e242f4e8f68c391e6d2f7ca16def/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | | `plugins/pstack/skills/` (0.15.21 to 0.15.25 changes: the `in-your-own-words` and `sharpen` skills, per-spawn effort in poteto-mode and the routed skills, one full swarm per PR in the autopilots and the multi-phase plan, the Graphite-free `orch` frontier, the `watch-pr` owner-approval gate, Origin PRs in `worktree-audit.sh`, `ketchup` visuals and length, restated principles, and prompt cuts), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 99743e9](https://github.com/cursor/plugins/tree/99743e9c151c8537cbbf1f98bb38f34ef3368453/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | +| `plugins/pstack/skills/` (0.15.26 to 0.15.29 changes: the `create-formal-verification-skill` and `maintain-formal-verification-skill` skills, setup's verification offers, `poteto-help` routing and recipes, the `sharpen` rewrite, `ketchup` waiting items, and the `typescript-best-practices` brand guard), `README-UPSTREAM.md` | [cursor/plugins/pstack @ 88d4751](https://github.com/cursor/plugins/tree/88d47514b82e7c44f00f2b2a72ff6dd12158038c/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | ## What changed in the port diff --git a/README.md b/README.md index c144e9e9..0c02a8d4 100644 --- a/README.md +++ b/README.md @@ -128,12 +128,14 @@ That is the main workflow. The other skills are there when poteto-mode needs the | `interrogate` | You want different models to try to break a design or diff. | | `create-verification-skill` | Your project has no repeatable way for an agent to prove real behavior. | | `maintain-verification-skill` | The project's verification instructions no longer match the product. | +| `create-formal-verification-skill` | A race, an invariant, or another property needs a proof that tests rarely reach. | +| `maintain-formal-verification-skill` | The code a formal verification covers has changed, and you need to know whether a failure is drift or a bug. | | `babysit` | A pull request needs CI failures and review comments handled until it is ready. | | `reflect` | A hard task is finished and its lessons should improve the next run. | | `correct` | Agents keep making the same mistake in a repository and you want a check that stops it. | | `poteto-help` | You want to know which skill, playbook, or principle fits a question. | | `in-your-own-words` | You want the agent to restate your goal and the problem before it starts. | -| `sharpen` | You want a task approached the way a top expert would, aimed at what you are really after, without overspecifying it. | +| `sharpen` | You want a prompt rewritten deeper, not bigger, before you send it. It returns the rewritten prompt and does not do the task. | Plugin skills include `pstack:` in their name. In Claude Code, invoke a native skill such as `/pstack:architect`. In Codex, ask for the skill, such as `Use pstack:architect for this design.` See the [technical reference](docs/reference.md) for the full list. @@ -170,12 +172,14 @@ This repository also keeps: ## Staying close to Lauren's pstack -Open Pstack 1.15.0 tracks pstack 0.15.25 at Cursor commit [`99743e9c151c8537cbbf1f98bb38f34ef3368453`](https://github.com/cursor/plugins/commit/99743e9c151c8537cbbf1f98bb38f34ef3368453). +Open Pstack 1.16.0 tracks pstack 0.15.29 at Cursor commit [`88d47514b82e7c44f00f2b2a72ff6dd12158038c`](https://github.com/cursor/plugins/commit/88d47514b82e7c44f00f2b2a72ff6dd12158038c). The two projects have separate version numbers. The pstack version identifies Lauren's upstream content. The Open Pstack version identifies the Claude Code and Codex package built from it. In this repository, “upstream” means Lauren's original pstack. Open Pstack does not promise instant updates. It records the exact version it follows, reviews new changes in order, and changes only what Claude Code and Codex require. New pstack behavior belongs in Lauren's project first whenever possible. +Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install only one of the two, because both use the `pstack:` prefix. + ## Contributing Fixes for Claude Code or Codex and help bringing over new pstack releases are welcome. Search [GitHub Issues](https://github.com/ericlitman/open-pstack/issues) before opening a new issue. For larger behavior changes, explain why the change belongs in Open Pstack instead of Lauren's original project. diff --git a/UPSTREAM.md b/UPSTREAM.md index 768abcf7..5d6dd9d0 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -8,15 +8,15 @@ open-pstack tracks [Cursor's pstack](https://github.com/cursor/plugins/tree/main | --- | --- | | Repository | `https://github.com/cursor/plugins.git` | | Path | `pstack/` | -| Commit | `99743e9c151c8537cbbf1f98bb38f34ef3368453` | -| Upstream version | `0.15.25` | -| open-pstack version | `1.15.0` | +| Commit | `88d47514b82e7c44f00f2b2a72ff6dd12158038c` | +| Upstream version | `0.15.29` | +| open-pstack version | `1.16.0` | -The table above is the current Cursor sync point. Open Pstack 1.10.0 imported this 0.15.25 sync, and 1.11.0 through 1.15.0 keep it. `README-UPSTREAM.md` preserves the upstream pstack README verbatim. `CHANGES.md` and `NOTICE.md` describe the adaptations and provenance. +The table above is the current Cursor sync point. Open Pstack 1.16.0 imported this 0.15.29 sync. `README-UPSTREAM.md` preserves the upstream pstack README verbatim. `CHANGES.md` and `NOTICE.md` describe the adaptations and provenance. ## Upstream-only exclusions -- Commits `799151d` and `6fecddb` add and relocate `make-bot-ui`. It depends on Cursor routines, webhook events, and UI primitives that Claude Code and Codex do not share. +- Commits `799151d` and `6fecddb` add and relocate `make-bot-ui`, and `a968159` renames it after its folder. It depends on Cursor routines, webhook events, and UI primitives that Claude Code and Codex do not share. `a968159`'s other hunk names `poteto-mode` after its folder, which the port's `poteto-mode/SKILL.md` already does. - Four `disable-model-invocation: true` lines from `73f8be4` are not applied to `how`, `why`, `unslop`, or `typescript-best-practices`. Poteto-mode invokes those skills by name, and the flag blocks that route on Claude Code. - The default-model hunks for `bug-fix`, `perf-issue`, and `hillclimb` from `23a56e2`, `889ec4b`, and `70b2dc8` are not applied. Those frequent code-writing roles stay on `codex:gpt-6.1-sol@max`. - `5bf2b15`'s setup budget question, its `# budget` line, and its step down to a lower detected effort are not applied. Setup already asks one requested effort per assigned family, and the step-down would silently lower a requested effort. @@ -33,6 +33,12 @@ The table above is the current Cursor sync point. Open Pstack 1.10.0 imported th - The root Agent Plugins v1 `pstack/plugin.json` from `e5a02f8` and its version bumps through 0.15.25 are not applied. The port keeps its current Claude manifest at `plugins/pstack/.claude-plugin/plugin.json` and Codex manifest at `plugins/pstack/.codex-plugin/plugin.json`. Agent Plugins v1 is revisited with #13. - `unslop` takes `bc697d0`'s description without its `disable-model-invocation: true` line, as for `73f8be4` above. - `pstack/.cursor-plugin/plugin.json` and `pstack/docs/guide/` are not imported. The Cursor manifest has no Claude Code or Codex consumer, and the guide shows Cursor's interface; `poteto-help` links to the guide upstream. That covers the 0.15.21 to 0.15.25 version bumps and `e5136d8`'s guide edit. +- Upstream's own Claude Code install is not applied. That covers `182f2ce`'s and `1b80080`'s generated tree under `harness/pstack/claude-code/`, `scripts/generate-pstack-harness-trees.mjs`, `scripts/validate-plugins.mjs`, the root `.claude-plugin/marketplace.json` entry, the adapter at `pstack/docs/harness/claude-code.md`, and `a968159`'s generator change. That install runs `grok-*` and `gpt-*` roles on the session's Claude model, has no Codex, and maps Cursor names at runtime from the adapter, which would be a second mapping layer on top of the port's own. `README-UPSTREAM.md` takes the README text from `182f2ce`, `1b80080` and `019a6a2` verbatim. +- `019a6a2`'s guide refresh and `scripts/check-pstack-docs.mjs` are not applied. The port does not import `pstack/docs/guide/`, so that check has nothing to compare. The same covers the guide edits in `7b353f7`, `f9be7aa` and `d457567`. +- The two harness paragraphs that `f9be7aa` puts in `poteto-help/SKILL.md`, which install upstream's Claude Code tree and describe other tools, are not applied. The port keeps its own paragraph on Claude Code and Codex. +- The 0.15.26 to 0.15.29 manifest bumps in `pstack/plugin.json` and `pstack/.cursor-plugin/plugin.json` from `0b8e952`, `0148b78` and `d457567` are not applied, as for the earlier bumps above. +- `create-formal-verification-skill` takes `4382e68` without its `disable-model-invocation: true` line, because setup's formal verification offer invokes it and the flag blocks that route on Claude Code. `tests/skill-collision-repro.sh` lists it in `routed_model_skills`. `maintain-formal-verification-skill` keeps the flag and runs only when typed. +- Setup's verification offers are steps 10 and 11 in the port, after its step 9 smoke test. The port never took upstream's step 7, "Offer a verification skill", which upstream has carried since 0.11.3. This sync restores it as step 10, and `f9be7aa`'s formal verification offer becomes step 11. Each keeps upstream's check for a project that already has one. - `poteto-agent.md` does not take `b93e811`'s search of `~/.cursor/plugins/` for poteto-mode, its highest-version rule, or its note that the skill catalog hides poteto-mode. The Claude agent preloads `pstack:poteto-mode`, the port's poteto-mode is not hidden, and Codex has no `poteto-agent` type. The agent keeps upstream's "Use the absolute path your parent gave you." ## Local port-patch ledger @@ -42,6 +48,8 @@ The table above is the current Cursor sync point. Open Pstack 1.10.0 imported th - **#157 — role pointers**: Cursor names model descriptors in the Arena, Architect, How, Interrogate, and Swarm skills, the bug-fix, feature, hillclimb, perf-issue, and refactoring playbooks, poteto-mode's delegation defaults, and setup's probe table and first-run sheet. The port replaces each with a role pointer: the role's backticked sheet label and a link to `plugins/pstack/skills/poteto-mode/references/model-catalog.md#role-defaults`, which `registry/render.ts` generates from `plugins/pstack/skills/poteto-mode/scripts/runner/registry/models.ts`. Interrogate's reviewer table and setup's probe table and example sheet are deleted. When an upstream sync changes a model slug on one of these lines, keep the port's line and put the model change in `registry/models.ts`. `runner/registry.test.ts` enforces the rule: `ROLE_POINTERS` names each file's roles, and its text scan rejects any descriptor or versioned model name in `plugins/pstack/**/*.md`, `README.md`, and `docs/reference.md` outside the generated catalog and agents. +- **#46 — quiet setup reruns**: Upstream's setup has no keep-roles, per-family effort, or write-confirmation questions, so this is a port patch. `setup-pstack/SKILL.md` states one qualifying-rerun exception before step 2's keep-roles question. On a rerun whose sheet loaded with one valid setting line, with no change named and no inconsistency or kept-predecessor proposal that needs a choice, setup validates in step 3, keeps and prints the roles and efforts instead of asking steps 2 and 4, and writes without step 7's confirmation when every step 5 probe passes. Steps 4, 7 and 8 and the offers in steps 10 and 11 each name the exception. It skips no validation, permission check, snapshot, readback, or the step 9 smoke test, and a failed probe still stops without writing. `poteto-help` says the same for reruns. The verifier's `keep-setting` case gives no answers and requires the sheet and Codex mirror to keep their bytes with no `AskUserQuestion` call. Preserve this divergence during upstream syncs. + - **#191 — landing playbooks and per-spawn effort**: `ce649c0` cuts Shipping to six steps and both autopilots to principles. The port takes the cut's rules and reasons but keeps the landing procedure from 1.3.0: Shipping keeps steps 1 to 9, Autopilot-full step 2 holds the guarded rebase and push, and Autopilot-stack step 2 holds the fork and topology rules. Those steps disarm auto-merge and merge-queue entries before verification and before any rewrite, keep the verdict head and base apart from the landing head and base, resolve the base fetch remote apart from the head push URL, bind each push to a captured SHA, and merge only through a server-enforced expected head. The named landing invariants in `tests/skill-collision-repro.sh` check those rules by step and phrase, so a sync that moves them updates the invariants in the same change. `ce649c0`'s Match the model to the job rule is taken with port adaptations: the starting level is the role's configured effort, an unlisted effort moves to the nearest effort the catalog row lists, a configured `ultra` stays, and the fast and standard speed sentences are dropped because the port's descriptors carry no speed selector. - **#232 — subagent waits in babysit**: Cursor's babysit step 6 runs `drive` and `background` under `/loop`. Claude Code subagents have no `ScheduleWakeup`, so `/loop` cannot run in them. The port adds one sentence after the `/loop` sentence that limits `/loop` to the main session and points a Claude Code subagent to `plugins/pstack/skills/poteto-mode/references/codex-tools.md#waits-on-claude-code`, which holds the wait rules. Preserve this sentence during upstream syncs. @@ -58,19 +66,29 @@ Fetch and inspect only commits that touched pstack after the recorded sync point ```shell git fetch cursor main -git log --oneline 99743e9c151c8537cbbf1f98bb38f34ef3368453..cursor/main -- pstack -git diff --stat 99743e9c151c8537cbbf1f98bb38f34ef3368453..cursor/main -- pstack +git log --oneline 88d47514b82e7c44f00f2b2a72ff6dd12158038c..cursor/main -- pstack +git diff --stat 88d47514b82e7c44f00f2b2a72ff6dd12158038c..cursor/main -- pstack ``` No output means the tracked pstack tree has not changed. This comparison does not need a polling service or generated mirror branch. ## Incorporate a change -1. Create or update a GitHub issue in `ericlitman/open-pstack` and branch from current `main`. -2. Read each upstream pstack commit in order. Bring over its intent and content, then apply only the Claude Code and Codex substitutions documented in `CHANGES.md`. -3. Keep one shared `plugins/pstack/skills/` tree. Put harness translation in the existing `codex-tools.md` and provider routing in `provider-dispatch.md`; do not fork a skill per harness. -4. Update the commit and version in this file, the affected provenance rows in `NOTICE.md`, and `README-UPSTREAM.md` when upstream changes it. -5. Run CI-equivalent checks locally, then run the installed Claude Code and Codex behavioral lanes required by the changed surface. Unit tests alone are not a release gate. -6. Merge the reviewed PR before tagging the next open-pstack release. Publish the release with `python3 scripts/release.py publish` from a clean checkout of `main`. +1. Create or update a GitHub issue in `ericlitman/open-pstack` and branch from current `main`. Pin the upstream target commit in the issue. +2. Read each upstream pstack commit in order, and record a decision for each one in the issue as a table: adopt, adapt (name the adaptation), or exclude (give the reason). Bring over each adopted commit's intent and content, then apply only the Claude Code and Codex substitutions documented in `CHANGES.md` and the adaptations in this file. +3. Run the audit and the mechanical merge from a clean checkout: + + ```shell + python3 scripts/upstream-audit.py --port HEAD --upstream > audit.json + python3 scripts/upstream-merge.py audit.json + ``` + + The merge checks out files the port never changed, merges the rest three ways, and prints counts of verbatim, clean, review and unmapped paths. It exits 1 when any path needs review. +4. Resolve each review row by hand. A conflict hunk keeps the port's adaptation and takes upstream's new intent beside it. A change to an excluded path stays out and extends that exclusion's line in this file. Each unmapped path, such as a Cursor manifest or the guide, is excluded or mapped by a decision in step 2. Record every hand resolution and every new adaptation or exclusion in this file. +5. Keep one shared `plugins/pstack/skills/` tree. Put harness translation in the existing `codex-tools.md` and provider routing in `provider-dispatch.md`; do not fork a skill per harness. +6. Add every new skill to the `skills` list in `.claude/skills/verify-open-pstack/features/registry.json`. When the sync changes what a skill with its own recipe does, such as `setup-pstack`, update that recipe in `features/recipes.ts`, its unit tests under `scripts/`, and its feature page. +7. Update the commit and version in this file, add a provenance row to `NOTICE.md`, and take `README-UPSTREAM.md` when upstream changes its README. +8. Run CI-equivalent checks locally, then run the installed Claude Code and Codex behavioral lanes required by the changed surface with `verify-open-pstack`. A sync that edits the verifier runs from the candidate head with `--self-test`. A run above the session limit needs `--wide ""`. Unit tests alone are not a release gate. +9. Merge the reviewed PR before tagging the next open-pstack release. Publish the release with `python3 scripts/release.py publish` from a clean checkout of `main`. Cursor's version and open-pstack's version are independent. Cursor's version identifies the imported content; open-pstack's version identifies the cross-harness distribution. diff --git a/docs/reference.md b/docs/reference.md index 762a0beb..94bf510a 100644 --- a/docs/reference.md +++ b/docs/reference.md @@ -2,7 +2,7 @@ This page contains the full skill, dependency, runtime, and porting reference. For the plain-English introduction and quick start, see the [main README](../README.md). -[Poteto](https://x.com/poteto)'s [pstack](https://github.com/cursor/plugins/tree/main/pstack), adapted to run in Claude Code and Codex without Cursor. One shared skill tree serves both harnesses; Grok remains available as a model-provider lane. Version 1.15.0 is synced to Cursor pstack v0.15.25 at `99743e9c151c8537cbbf1f98bb38f34ef3368453`. See [UPSTREAM.md](../UPSTREAM.md) for the exact sync contract. +[Poteto](https://x.com/poteto)'s [pstack](https://github.com/cursor/plugins/tree/main/pstack), adapted to run in Claude Code and Codex without Cursor. One shared skill tree serves both harnesses; Grok remains available as a model-provider lane. Version 1.16.0 is synced to Cursor pstack v0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. See [UPSTREAM.md](../UPSTREAM.md) for the exact sync contract. Original by Lauren Tan. This distribution builds on Michael Denyer's [pstack-claude](https://github.com/michael-denyer/pstack-claude) port and retains its history and MIT attribution. It imports seven MIT-licensed skills from [cursor-team-kit](https://github.com/cursor/plugins/tree/main/cursor-team-kit): `deslop`, `thermo-nuclear-code-quality-review`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, `what-did-i-get-done`. @@ -59,7 +59,7 @@ The marketplace install is the normal user path. Direct links are only for testi ├── plugins/pstack/ # the plugin itself │ ├── .claude-plugin/plugin.json # Claude Code manifest │ ├── .codex-plugin/plugin.json # Codex manifest (skills: ./skills/) -│ ├── skills/ # 61 skills shared by Claude Code and Codex +│ ├── skills/ # 63 skills shared by Claude Code and Codex │ │ ├── poteto-mode/references/{codex-tools,provider-dispatch}.md # tool + provider routing │ │ └── poteto-mode/scripts/ # bun/bash/node tooling: watch-pr, orch, runner, resolve-codex-transcript, check-plan.mjs, worktree-audit.sh │ ├── hooks/ # SessionStart auto-fire: injects the poteto-mode mandate (Claude Code only) @@ -110,6 +110,7 @@ Not declared as deps, but referenced in skill bodies: - **`bun`** — runs the vendored `skills/poteto-mode/scripts/` tooling (`watch-pr`, `orch`, `runner`) and the port-authored `resolve-codex-transcript` launcher. Install via [`brew install oven-sh/bun/bun`](https://bun.sh). `bootstrap.ts` installs dependencies for `watch-pr` and `orch`; the runner uses only Bun and Node built-ins, so it launches directly without an install/re-exec layer. - **`git` 2.25 or later** — the runner asks `git rev-parse --git-common-dir` for a linked worktree's shared git directory, and `worktree-audit.sh` reads `git worktree list --porcelain`. Ubuntu 20.04 LTS ships 2.25; older git is unsupported. - **Bash on Windows** — the SessionStart hook runs through `hooks/run-hook.cmd`, which looks for Git for Windows' `bash.exe` in its standard system-wide and per-user locations, then for a `bash` on `PATH` (MSYS2, Cygwin). Without one, the hook exits 0 and skips the pstack startup context, as the superpowers wrapper it comes from does. Install [Git for Windows](https://git-scm.com/download/win) to get the context. In Codex, the hook starts `C:\Windows\System32\cmd.exe` by full path, because one command must work in both PowerShell and cmd. A Windows installed outside `C:\Windows` does not run the hook. +- **macOS, Linux or WSL2 for Claude writer lanes** — Claude Code's sandbox does not run on native Windows, so a Claude writer lane needs one of these hosts. - **`node`** — runs `skills/poteto-mode/scripts/check-plan.mjs`. The checker uses only Node built-ins and does not need Bun. - **Provider CLIs** — the external runner uses the assigned subscribed CLI directly, one per provider in the [model catalog's route table](../plugins/pstack/skills/poteto-mode/references/model-catalog.md#routes). Install and authenticate only the providers present in your model sheet. Some providers run read-only lanes only. The catalog notes for OpenCode, Amp, Cursor, Devin, agy and dsh say what repository and host configuration their CLIs load into a lane. Same-provider work stays native; the runner refuses it. - **`jq` and `rg` (ripgrep)** — only for `scripts/worktree-audit.sh` (the Worktree cleanup playbook). Without them the audit still runs but blanks its PR and LAST_CHAT columns, so it warns on stderr rather than returning a table that looks complete. @@ -145,6 +146,8 @@ The table uses the short upstream names. Claude Code exposes each native skill w | `/no-comments` | strip comments before review via the `comment-sicko` subagent, then fix what it finds | | `/create-verification-skill` | generate a project-local verification skill and feature map | | `/maintain-verification-skill` | re-sync a drifted verification skill and its feature map | +| `/create-formal-verification-skill` | generate a project-local skill that formally verifies a race, invariant, or other property tests rarely reach | +| `/maintain-formal-verification-skill` | bring a formal verification back in line after the code it covers changed, and say whether each failure is drift or a bug (typed only) | | `/deslop` | deslop a diff before commit | | `/babysit` | monitor an open PR, fix CI/comments, keep it merge-ready | | `/thermo-nuclear-code-quality-review` | extremely strict maintainability audit | @@ -158,7 +161,7 @@ The table uses the short upstream names. Claude Code exposes each native skill w | `/ketchup` | catch up on everything in this session since your last message (typed only) | | `/poteto-help` | find the skill, playbook, or principle for a question about pstack (typed only) | | `/in-your-own-words` | play back your goal and the problem before work starts (typed only) | -| `/sharpen` | approach a task the way a top expert would, aimed at the real goal, without overspecifying it (typed only) | +| `/sharpen` | rewrite a prompt deeper, not bigger, before you send it; returns the rewritten prompt and does not do the task (typed only) | ## Subagents diff --git a/plugins/pstack/.claude-plugin/plugin.json b/plugins/pstack/.claude-plugin/plugin.json index 7cbd5a18..495877ea 100644 --- a/plugins/pstack/.claude-plugin/plugin.json +++ b/plugins/pstack/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "pstack", "displayName": "pstack", - "version": "1.15.0", + "version": "1.16.0", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Ported from cursor/plugins/pstack for Claude Code and Codex.", "author": { "name": "Lauren Tan" diff --git a/plugins/pstack/.codex-plugin/plugin.json b/plugins/pstack/.codex-plugin/plugin.json index 52fb4b5a..f98774aa 100644 --- a/plugins/pstack/.codex-plugin/plugin.json +++ b/plugins/pstack/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "pstack", - "version": "1.15.0", + "version": "1.16.0", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Codex port of the Claude Code plugin; skills are shared, tool names resolve via skills/poteto-mode/references/codex-tools.md.", "author": { "name": "Lauren Tan" From 96a1ffc91fc61773b9fa3a4b6830480ed19e3648 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 00:23:07 -0400 Subject: [PATCH 06/12] fix(pstack): encode dots in Claude transcript folder names (#235) recall, automate-me and the session-pickup playbook said Claude Code encodes only each / in the workspace path. It also encodes each ., so every .claude/worktrees/ session looked for a folder that does not exist. Reproduced on 2026-10-21 with the installed 1.15.0 plugin. Co-Authored-By: Claude Opus 5.5 --- CHANGES.md | 4 +++- UPSTREAM.md | 1 + plugins/pstack/skills/automate-me/SKILL.md | 2 +- plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md | 2 +- plugins/pstack/skills/recall/SKILL.md | 2 +- 5 files changed, 7 insertions(+), 4 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index a0416069..31a766d3 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,12 +5,14 @@ This port applies the Cursor → Claude Code substitutions in skill bodies. Earl ## 1.16.0 syncs to Cursor pstack 0.15.29 -Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. Sixteen upstream commits since 0.15.25 touch pstack. Nine change skill content, and all nine are applied with the port adaptations below. `a968159` names two skills after their folders: the port's `poteto-mode` already complies, and `make-bot-ui` stays out. Three add upstream's own Claude Code install and a docs check, which stay out apart from their README text. Three bump only the Cursor manifests and guide, which stay out. The release also fixes #46, and ships Claude Haiku 5.5 lanes (#223), foreground waits on Claude Code (#232, #233) and the comment sweep (#218), all merged after 1.15.0. Default roles and panels are unchanged. +Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. Sixteen upstream commits since 0.15.25 touch pstack. Nine change skill content, and all nine are applied with the port adaptations below. `a968159` names two skills after their folders: the port's `poteto-mode` already complies, and `make-bot-ui` stays out. Three add upstream's own Claude Code install and a docs check, which stay out apart from their README text. Three bump only the Cursor manifests and guide, which stay out. The release also fixes #46 and #235, and ships Claude Haiku 5.5 lanes (#223), foreground waits on Claude Code (#232, #233) and the comment sweep (#218), all merged after 1.15.0. Default roles and panels are unchanged. **Claude Haiku 5.5 lanes.** The model catalog registers `claude:claude-haiku-5-5` as an exact pin, with five native agents, `pstack-haiku-5-5-low` to `pstack-haiku-5-5-max`, and efforts `low` to `max`. On a Claude Code parent an unregistered Claude model is a dropout, so this is the first way to run Haiku lanes there. The pin is optional; no role default changes. The catalog registers no `haiku` alias, because Claude Code resolves that alias to Haiku 4.5, which has no effort setting, on Bedrock, Vertex and Foundry (#223, by @jwerby). **Claude Code subagents wait in the foreground.** The generated `pstack--` agents no longer set `background: true`, which Claude Code honored over a caller's `run_in_background: false` (#233). `references/codex-tools.md` has a Waits on Claude Code section: the main session runs long commands and fan-outs in the background, and a subagent dispatches the lanes it needs in the foreground, runs `watch-pr` in the foreground with `--timeout 240` instead of `/loop`, and waits on a background task in one bounded foreground call (#232). Provider dispatch, poteto-mode, babysit step 6 and `docs/reference.md` point to that section. +**`/recall` in worktree sessions (#235).** `recall`, `automate-me` and the session-pickup playbook now encode each `/` and each `.` of the workspace path as `-`, as Claude Code does. Before this, every session under `.claude/worktrees/` looked for a transcript folder that does not exist. + **New skills.** `/create-formal-verification-skill` generates a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, with TLA+ as the default tool and a fallback when no verifier fits. `/maintain-formal-verification-skill` finds the commits that touched verified code, brings the model and properties back in line, reruns them, and says whether each failure is drift or a bug. It runs only when typed. **Setup offers.** After its smoke test, setup offers once each to generate a verification skill and a formal verification skill, unless the project already has one. diff --git a/UPSTREAM.md b/UPSTREAM.md index 5d6dd9d0..30e5de1f 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -43,6 +43,7 @@ The table above is the current Cursor sync point. Open Pstack 1.16.0 imported th ## Local port-patch ledger +- **#235 — Claude transcript folder encoding**: the port wrote Claude Code's per-project transcript path into `recall`, `automate-me` and the `session-pickup` playbook. Claude Code encodes each `/` and each `.` in the workspace path as `-`, so a `.claude/worktrees/` session's folder holds `--claude-worktrees-`. Keep both characters in those three lines during syncs. - **#140 — Reflect transcript resolution**: Cursor's Reflect step 1 reads the `agent-transcripts/` directory its system prompt names; the port had substituted Claude Code's per-project directory, which left Codex without a lookup. The port replaces that step's body with one line that points to `plugins/pstack/skills/poteto-mode/references/codex-tools.md#active-transcripts`, and leaves the rest of `reflect/SKILL.md` unchanged. That mapping section holds the harness specifics: the Claude per-project scope, layouts, candidate and scan limits, opening-message verification, the Codex resolver call, and the 2,000-word digest fallback. The port-authored Bun resolver `plugins/pstack/skills/poteto-mode/scripts/resolve-codex-transcript.ts`, started through the `sh` launcher `resolve-codex-transcript` next to it so project Bun config and `.env` files cannot affect it, looks up the parent's known chat ID in Codex's read-only `threads` index, checks rollout scope and ownership, and prints opening-message metadata without transcript text. Preserve this divergence during upstream syncs: keep step 1 as the one-line pointer and keep the mapping section and resolver. - **#120 — harness config homes** (tracked for #105): Cursor's setup destination is `~/.cursor/rules/`. The shared port resolves nonempty `CLAUDE_CONFIG_DIR` / `CODEX_HOME`, otherwise `$HOME/.claude` / `$HOME/.codex`, once at `plugins/pstack/skills/poteto-mode/references/codex-tools.md#harness-config-homes`. `setup-pstack/SKILL.md` reuses that home for reads, sheet/integration writes, snapshots, restoration, and readback; Claude preserves the literal legacy import at the default home and renders exactly `@./pstack-models.md` for redirected homes, keeping spaces and `#` in the config-directory name out of the import line; reruns replace the one import whose target basename is `pstack-models.md`, append if absent, and stop if duplicated. Preserve this intentional divergence during upstream syncs. The named config-home invariant in `tests/skill-collision-repro.sh` rejects literal default destinations outside the legacy import, requires the literal default-home rendering and zero/one/many import rules, and verifies unset/empty/space-containing resolution without daily writes. See `CHANGES.md` for the port correction and `tests/setup-config-home-repro.sh` for redirected live-evidence preparation. The Cursor sync point is unchanged. diff --git a/plugins/pstack/skills/automate-me/SKILL.md b/plugins/pstack/skills/automate-me/SKILL.md index eb2ae680..005ff102 100644 --- a/plugins/pstack/skills/automate-me/SKILL.md +++ b/plugins/pstack/skills/automate-me/SKILL.md @@ -27,7 +27,7 @@ Update mode changes the rest of the flow: ### 1. Mine their history -Locate the active workspace's transcripts before fanning out. Claude Code stores them at `~/.claude/projects//*.jsonl`, where `` is the workspace's working directory with `/` → `-`. Use only that path. Don't glob across `~/.claude/projects/`. That crosses workspace boundaries and reads private chats from unrelated projects. +Locate the active workspace's transcripts before fanning out. Claude Code stores them at `~/.claude/projects//*.jsonl`, where `` is the workspace's working directory with each `/` and each `.` → `-`. Use only that path. Don't glob across `~/.claude/projects/`. That crosses workspace boundaries and reads private chats from unrelated projects. Survey recent agent conversations within that scope for recurring patterns. Run multiple parallel subagents across slices of history (e.g. last 2-4 weeks, split into 3 slices so each has enough material). Pick each subagent's effort for the job, per the Subagents section of the **poteto-mode** skill. Each slice mining subagent reads transcripts from the workspace-scoped path the parent provides, looks for the signals below, and returns a short structured list of patterns it saw with evidence pointers. Default signals worth hunting: diff --git a/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md b/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md index 01b8cea4..60988fb3 100644 --- a/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md +++ b/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md @@ -2,7 +2,7 @@ **You own the resume point. Read the prior trail, don't redo it.** -1. Locate the prior trail. A local transcript under Claude Code's per-project transcripts directory at `~/.claude/projects//*.jsonl` (where `` is the workspace cwd with `/` → `-`. Do not glob across other directories under `~/.claude/projects/`, that crosses workspace boundaries and reads private chats from unrelated projects), a cloud-agent URL, or a pushed branch. Read the metadata overview and last messages first, then scan back for the decision points. Parse a long transcript in a subagent and keep the reduced timeline in the main thread (the **principle-guard-the-context-window** skill). Pick each subagent's effort for the job, per the Subagents section. +1. Locate the prior trail. A local transcript under Claude Code's per-project transcripts directory at `~/.claude/projects//*.jsonl` (where `` is the workspace cwd with each `/` and each `.` → `-`. Do not glob across other directories under `~/.claude/projects/`, that crosses workspace boundaries and reads private chats from unrelated projects), a cloud-agent URL, or a pushed branch. Read the metadata overview and last messages first, then scan back for the decision points. Parse a long transcript in a subagent and keep the reduced timeline in the main thread (the **principle-guard-the-context-window** skill). Pick each subagent's effort for the job, per the Subagents section. 2. Reconstruct operational state. The branch and worktree, what already landed (`git log`, `git diff` against the base), the open todos, the decisions made. The prior trail is authoritative input. Resist the bias to re-derive it. 3. Diff done vs pending. Compare what shipped against what was planned, name the resume point, do not re-run the prior repro or redo completed work. A "let me verify from scratch" pass means you're treating the trail as untrustworthy when it's authoritative. 4. Route the remaining work to the matching playbook and pick the verdict: continue the execution, ship a finished recommendation, ratify or override a prior conclusion, or postmortem a failed run. The pickup playbook ends here. The routed playbook owns the rest. diff --git a/plugins/pstack/skills/recall/SKILL.md b/plugins/pstack/skills/recall/SKILL.md index 0baacbf4..48fcecdc 100644 --- a/plugins/pstack/skills/recall/SKILL.md +++ b/plugins/pstack/skills/recall/SKILL.md @@ -11,7 +11,7 @@ Keep it tight and on-topic. Read only what the in-scope threads need, then stop. Your context lives in two records. Your own chat history holds what you did and decided. The shared record holds everything that happened around the same code under other names: the symptoms users keep reporting, the fixes that shipped and got reverted, the errors still firing in prod. That second record is what the **why** skill searches, across source control, the issue tracker, chat and issue channels, long-form docs, and error tracking. A feature with a long bug tail keeps most of its story there, so don't reconstruct it from your transcripts alone. -Transcripts live at `~/.claude/projects//.jsonl`, where `` is the workspace path with the leading slash dropped and each "/" turned into "-" (so `/Users/you/proj` becomes `-Users-you-proj`). Every line is one chat message. +Transcripts live at `~/.claude/projects//.jsonl`, where `` is the workspace path with each "/" and each "." turned into "-" (so `/Users/you/proj` becomes `-Users-you-proj`, and `/Users/you/proj/.claude/worktrees/x` becomes `-Users-you-proj--claude-worktrees-x`). Every line is one chat message. 1. Classify, then route. One specific prior chat to resume is the `session-pickup` playbook, not this. Turning habits into a durable skill is `automate-me`. A human-readable summary of your work is a different task. Recall loads working context across recent chats before you act. If the user already gave you a full state capsule (paths, branch, the change), use it and skip the mining. 2. Lock the scope before searching. Pin the window ("recent" is a real range, default the last 7 days), the topic if named, and the workspace (default the active one. Never read another project's transcripts without being asked). State the scope back. Never quietly turn "all" into "recent N". From 5598b3a6b11a1f1672b2e67ee93a618476ad4baa Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 01:04:59 -0400 Subject: [PATCH 07/12] fix(verifier): make keep-setting prove the rerun wrote and publish only what it checks (#46) keep-setting now prepares exactly the sheet a quiet rerun keeps, so a prepared file written in the session's start millisecond satisfied written() for a session that wrote nothing. The prepared sheet and Codex mirror now carry a past mtime. The case publishes no-question for Claude only, because a Codex session asks in plain text, which the session record does not keep. Co-Authored-By: Claude Opus 5.5 --- .../skills/verify-open-pstack/features/recipes.ts | 15 ++++++++++----- .../verify-open-pstack/scripts/catalog.test.ts | 14 +++++++++++--- 2 files changed, 21 insertions(+), 8 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 0990de3f..33bb727b 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -1,5 +1,5 @@ import { Database } from 'bun:sqlite'; -import { lstat, mkdir, readFile, realpath, rm, writeFile } from 'node:fs/promises'; +import { lstat, mkdir, readFile, realpath, rm, utimes, writeFile } from 'node:fs/promises'; import { homedir } from 'node:os'; import { basename, join } from 'node:path'; import { pathToFileURL } from 'node:url'; @@ -565,16 +565,21 @@ function keepSetting(): Case { async prepare(f) { sheetBytes = sheetText([...(await readCatalog(f.location)).defaults]) + `${FULL_ACCESS_SETTING}\n`; mirrorBytes = `${MIRROR_BEGIN}\n${sheetBytes}${MIRROR_END}\n`; - await writeFile(join(f.configHome, 'pstack-models.md'), sheetBytes); - if (f.harness === 'codex') await writeFile(join(f.configHome, 'AGENTS.md'), mirrorBytes); + const prepared = new Date(Date.now() - 3_600_000), sheet = join(f.configHome, 'pstack-models.md'), mirror = join(f.configHome, 'AGENTS.md'); + await writeFile(sheet, sheetBytes); + await utimes(sheet, prepared, prepared); + if (f.harness === 'codex') { + await writeFile(mirror, mirrorBytes); + await utimes(mirror, prepared, prepared); + } }, prompt: f => `${invoke(f.harness, 'setup-pstack', `Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; - if (record.tools.some(t => t.name === 'AskUserQuestion')) throw new Error('keep-setting-asked'); + if (f.harness === 'claude' && record.tools.some(t => t.name === 'AskUserQuestion')) throw new Error('keep-setting-asked'); if (await readFile(sheet, 'utf8') !== sheetBytes) throw new Error('keep-setting-sheet-changed'); if (f.harness === 'codex' && await readFile(join(f.configHome, 'AGENTS.md'), 'utf8').catch(() => '') !== mirrorBytes) throw new Error('keep-setting-mirror-changed'); - return { assertions: [...assertions, 'no-question', 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; + return { assertions: [...assertions, ...(f.harness === 'claude' ? ['no-question'] : []), 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; }, }; } diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index bbbf8347..e438f69d 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -347,7 +347,7 @@ test('the full-access writer case quotes each browser argument for sh and encode }); for (const harness of ['claude', 'codex'] as const) { - test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror with no question`, async () => { + test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror, with no question in Claude`, async () => { const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!, installed = await readCatalog(location); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); await c.prepare!(f); @@ -357,12 +357,13 @@ for (const harness of ['claude', 'codex'] as const) { expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe(agents); expect(c.prompt(f)).not.toContain('Use these answers'); await writeFile(path, prepared); - expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', 'no-question', 'sheet-unchanged', + expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'claude' ? ['no-question'] : []), 'sheet-unchanged', ...(harness === 'codex' ? ['codex-mirror-unchanged'] : []), 'setting:codex writer sandbox: full-access']); const asked = record(harness, 'pstack:setup-pstack'); asked.tools.push({ name: 'AskUserQuestion', id: 'q', input: {}, parent: null, failed: true }); - await expect(c.assert(asked, f)).rejects.toThrow('keep-setting-asked'); + if (harness === 'claude') await expect(c.assert(asked, f)).rejects.toThrow('keep-setting-asked'); + else expect((await c.assert(asked, f)).assertions).not.toContain('no-question'); for (const wrong of [prepared.replace(FULL_ACCESS, ''), prepared.replace(FULL_ACCESS, BOUNDED), prepared.replace(/\nbug-fix: [^\n]*/, ''), `${prepared}\n`]) { await writeFile(path, wrong); await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow('keep-setting-sheet-changed'); @@ -374,6 +375,13 @@ for (const harness of ['claude', 'codex'] as const) { } }); + test(`${harness}: the keep-setting case rejects a session that wrote nothing after prepare`, async () => { + const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!; + await c.prepare!(f); + const started = Date.now(); + await expect(c.assert({ ...record(harness, 'pstack:setup-pstack'), started }, f)).rejects.toThrow('fixture-file-missing:pstack-models.md'); + }); + test(`${harness}: every setup prompt declines both verification offers`, async () => { const f = await fixture(harness); for (const c of recipe('setup', harness)) expect(c.prompt(f)).toEndWith('If setup offers to generate a verification skill or a formal verification skill, decline both.'); From 8c20d39873d1a7fb4184e601511b9cace7b1369e Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 01:48:32 -0400 Subject: [PATCH 08/12] fix(verifier): observe the quiet rerun and the formal offer's handoff (#46) keep-setting got the same "decline both offers" sentence as every setup case, so its no-question check could not fail on the offers a quiet rerun must only mention. keep-setting now gets no answers and must end with SETUP-DONE, create no skill directory, and, in Claude, attempt no AskUserQuestion. The parser keeps each session's final assistant text. A new accept-formal-offer case requires setup to load create-formal-verification-skill when the user accepts that offer. first-run's offers-declined assertion is renamed no-skill-directory. Co-Authored-By: Claude Opus 5.5 --- .../verify-open-pstack/features/recipes.ts | 52 +++++++++++++---- .../verify-open-pstack/features/setup.md | 2 +- .../scripts/catalog.test.ts | 58 +++++++++++++++---- .../scripts/harness.test.ts | 16 +++++ .../verify-open-pstack/scripts/harness.ts | 6 +- .../scripts/reflect.test.ts | 2 +- .../verify-open-pstack/scripts/runner.test.ts | 2 +- .../scripts/skill-invocation.test.ts | 2 +- .../verify-open-pstack/scripts/types.ts | 1 + .../verify-open-pstack/scripts/verify.test.ts | 2 +- 10 files changed, 114 insertions(+), 29 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 33bb727b..efd48078 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -81,6 +81,16 @@ function loaded(record: SessionRecord, skill: string): string { return 'skill-loaded'; } +function ended(record: SessionRecord, word: string, failure: string): string { + if (record.reply.trim() !== word) throw new Error(failure); + return `ended:${word}`; +} + +async function noSkillDirectory(f: Fixture, failure: string): Promise { + for (const skills of ['.claude/skills', '.agents/skills']) if (await lstat(join(f.dir, skills)).then(() => true, () => false)) throw new Error(`${failure}:${skills}`); + return 'no-skill-directory'; +} + async function written(record: SessionRecord, path: string): Promise { const info = await lstat(path).catch(() => undefined); if (!info?.isFile() || !info.size || info.mtimeMs < record.started) throw new Error(`fixture-file-missing:${basename(path)}`); @@ -406,21 +416,42 @@ const setup: Case[] = [{ id: 'first-run', codexSandbox: 'danger-full-access', claudePermission: 'bypassPermissions', - async prepare(f) { - await rm(join(f.configHome, 'pstack-models.md'), { force: true }); - if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); - }, - prompt: f => `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep the first-run role assignments and every proposed effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, + prepare: unconfigured, + prompt: firstRunPrompt, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; const text = await readFile(sheet, 'utf8'); if (!Bun.deepEquals(roleLines(text), [...(await readCatalog(f.location)).defaults].map(([role, lanes]) => `${role}: ${lanes.join(', ')}`))) throw new Error('first-run-not-role-defaults'); bounded(text); - for (const skills of ['.claude/skills', '.agents/skills']) if (await lstat(join(f.dir, skills)).then(() => true, () => false)) throw new Error(`first-run-offer-accepted:${skills}`); - return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`, 'offers-declined'], files: [sheet] }; + const declined = await noSkillDirectory(f, 'first-run-offer-accepted'); + return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`, declined], files: [sheet] }; + }, +}, { + id: 'accept-formal-offer', + codexSandbox: 'danger-full-access', + claudePermission: 'bypassPermissions', + prepare: unconfigured, + prompt: f => `${firstRunPrompt(f)} Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.`, + async assert(record) { + const assertions = [loaded(record, 'pstack:setup-pstack')]; + if (!record.skills.slice(record.skills.indexOf('pstack:setup-pstack') + 1).some(isFormalCreator)) throw new Error('skill-not-routed:create-formal-verification-skill'); + return { assertions: [...assertions, 'routed:create-formal-verification-skill', ended(record, 'ACCEPT-ROUTED', 'accept-formal-offer-did-not-finish')], files: [] }; }, }]; +const DECLINE_EXEMPT = new Set(['keep-setting', 'accept-formal-offer']); +const isFormalCreator = (skill: string): boolean => + skill === 'pstack:create-formal-verification-skill' || skill.endsWith('/create-formal-verification-skill/SKILL.md'); + +async function unconfigured(f: Fixture): Promise { + await rm(join(f.configHome, 'pstack-models.md'), { force: true }); + if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); +} + +function firstRunPrompt(f: Fixture): string { + return `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep the first-run role assignments and every proposed effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`; +} + function bounded(text: string): void { if (!Bun.deepEquals(settingLines(text), [BOUNDED_SETTING])) throw new Error('setting-not-bounded'); } @@ -573,13 +604,14 @@ function keepSetting(): Case { await utimes(mirror, prepared, prepared); } }, - prompt: f => `${invoke(f.harness, 'setup-pstack', `Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, + prompt: f => `${invoke(f.harness, 'setup-pstack', `Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub. Reply with exactly SETUP-DONE as your final message.`, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; if (f.harness === 'claude' && record.tools.some(t => t.name === 'AskUserQuestion')) throw new Error('keep-setting-asked'); if (await readFile(sheet, 'utf8') !== sheetBytes) throw new Error('keep-setting-sheet-changed'); if (f.harness === 'codex' && await readFile(join(f.configHome, 'AGENTS.md'), 'utf8').catch(() => '') !== mirrorBytes) throw new Error('keep-setting-mirror-changed'); - return { assertions: [...assertions, ...(f.harness === 'claude' ? ['no-question'] : []), 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; + const quiet = [await noSkillDirectory(f, 'keep-setting-offer-accepted'), ended(record, 'SETUP-DONE', 'keep-setting-did-not-finish')]; + return { assertions: [...assertions, ...(f.harness === 'claude' ? ['no-askuserquestion-attempt'] : []), 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), ...quiet, `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; }, }; } @@ -693,7 +725,7 @@ export function recipe(feature: string, harness: Harness, routes: string[] = []) if (feature === 'project-skill') return [projectSkill]; if (feature === 'hook:startup') return [startupHook]; if (feature === 'runner') return runner(harness, routes); - if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup.map(c => ({ ...c, prompt: f => `${c.prompt(f)} ${DECLINE_OFFERS}` })); + if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup.map(c => DECLINE_EXEMPT.has(c.id) ? c : { ...c, prompt: f => `${c.prompt(f)} ${DECLINE_OFFERS}` }); if (feature === 'catalog') return catalog(harness); if (feature === 'shipped-tools') return [shippedTools]; if (feature === 'agent-preload:poteto-agent' && harness === 'claude') return [agentPreload]; diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index 05f51a41..5f05b5b5 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers. It asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, and that the Claude session made no `AskUserQuestion` call. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. Every setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the verification-skill offer and accept the formal verification offer, and to stop as soon as the formal verification skill loads and reply with exactly `ACCEPT-ROUTED`. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex records the loaded skill by name or by its `SKILL.md` path, and either counts. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index e438f69d..6403edd7 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -16,7 +16,7 @@ async function fixture(harness: Harness): Promise { return { harness, dir, workspace, location, configHome: dir, run: command }; } const record = (harness: Harness, skill: string): SessionRecord => - ({ harness, exitCode: 0, started: Date.now() - 1000, skills: [skill], commands: [], tools: [], context: [] }); + ({ harness, exitCode: 0, started: Date.now() - 1000, skills: [skill], commands: [], tools: [], context: [], reply: '' }); const sheet = async (path: string): Promise> => new Map((await readFile(path, 'utf8')).split('\n') .filter(line => /^[a-z][^:]*: \S/.test(line)).map((line): [string, string[]] => [line.slice(0, line.indexOf(': ')), line.slice(line.indexOf(': ') + 2).split(', ')])); const setupCase = (id: string): Case => recipe('setup', 'claude').find(c => c.id === id)!; @@ -287,7 +287,7 @@ test('the first-run case requires a sheet equal to the catalog role defaults', a await writeFile(path, written); await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow('codex-mirror-mismatch'); await mirror(f, written); - expect((await c.assert(record('codex', 'pstack:setup-pstack'), f)).assertions).toContain('sheet:role-defaults'); + expect((await c.assert(record('codex', 'pstack:setup-pstack'), f)).assertions).toEqual(expect.arrayContaining(['sheet:role-defaults', 'no-skill-directory'])); await rejectsUnbounded(c, f, written); await writeFile(path, `# pstack model configuration\n\n${lines.slice(1).join('\n')}\n`); await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow('first-run-not-role-defaults'); @@ -347,7 +347,7 @@ test('the full-access writer case quotes each browser argument for sh and encode }); for (const harness of ['claude', 'codex'] as const) { - test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror, with no question in Claude`, async () => { + test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror, SETUP-DONE, and no question in Claude`, async () => { const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!, installed = await readCatalog(location); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); await c.prepare!(f); @@ -356,22 +356,33 @@ for (const harness of ['claude', 'codex'] as const) { const agents = harness === 'codex' ? `\n${prepared}\n` : 'mirror\n'; expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe(agents); expect(c.prompt(f)).not.toContain('Use these answers'); + expect(c.prompt(f)).not.toContain('decline'); + expect(c.prompt(f)).toEndWith('Reply with exactly SETUP-DONE as your final message.'); await writeFile(path, prepared); - expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'claude' ? ['no-question'] : []), 'sheet-unchanged', - ...(harness === 'codex' ? ['codex-mirror-unchanged'] : []), 'setting:codex writer sandbox: full-access']); + const done = (): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), reply: '\nSETUP-DONE\n' }); + expect((await c.assert(done(), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'claude' ? ['no-askuserquestion-attempt'] : []), 'sheet-unchanged', + ...(harness === 'codex' ? ['codex-mirror-unchanged'] : []), 'no-skill-directory', 'ended:SETUP-DONE', 'setting:codex writer sandbox: full-access']); - const asked = record(harness, 'pstack:setup-pstack'); + for (const reply of ['Want a project-local verification skill? I can generate one with /create-verification-skill.', '']) { + await expect(c.assert({ ...done(), reply }, f)).rejects.toThrow('keep-setting-did-not-finish'); + } + const asked = done(); asked.tools.push({ name: 'AskUserQuestion', id: 'q', input: {}, parent: null, failed: true }); if (harness === 'claude') await expect(c.assert(asked, f)).rejects.toThrow('keep-setting-asked'); - else expect((await c.assert(asked, f)).assertions).not.toContain('no-question'); + else expect((await c.assert(asked, f)).assertions).not.toContain('no-askuserquestion-attempt'); + for (const skills of ['.claude/skills', '.agents/skills']) { + await mkdir(join(f.dir, skills), { recursive: true }); + await expect(c.assert(done(), f)).rejects.toThrow(`keep-setting-offer-accepted:${skills}`); + await rm(join(f.dir, skills.split('/')[0]!), { recursive: true }); + } for (const wrong of [prepared.replace(FULL_ACCESS, ''), prepared.replace(FULL_ACCESS, BOUNDED), prepared.replace(/\nbug-fix: [^\n]*/, ''), `${prepared}\n`]) { await writeFile(path, wrong); - await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow('keep-setting-sheet-changed'); + await expect(c.assert(done(), f)).rejects.toThrow('keep-setting-sheet-changed'); } await writeFile(path, prepared); if (harness === 'codex') { await writeFile(join(f.dir, 'AGENTS.md'), `notes\n${agents}`); - await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow('keep-setting-mirror-changed'); + await expect(c.assert(done(), f)).rejects.toThrow('keep-setting-mirror-changed'); } }); @@ -382,9 +393,32 @@ for (const harness of ['claude', 'codex'] as const) { await expect(c.assert({ ...record(harness, 'pstack:setup-pstack'), started }, f)).rejects.toThrow('fixture-file-missing:pstack-models.md'); }); - test(`${harness}: every setup prompt declines both verification offers`, async () => { - const f = await fixture(harness); - for (const c of recipe('setup', harness)) expect(c.prompt(f)).toEndWith('If setup offers to generate a verification skill or a formal verification skill, decline both.'); + test(`${harness}: every setup prompt but keep-setting and accept-formal-offer declines both verification offers`, async () => { + const f = await fixture(harness), decline = 'If setup offers to generate a verification skill or a formal verification skill, decline both.'; + const cases = recipe('setup', harness); + expect(cases.map(c => c.id)).toEqual(['configure', 'consume', 'keep-predecessor', 'new-families', 'read-only-provider', 'writer-refusal', 'keep-setting', 'first-run', 'accept-formal-offer']); + for (const c of cases) { + if (['keep-setting', 'accept-formal-offer'].includes(c.id)) expect(c.prompt(f)).not.toContain(decline); + else expect(c.prompt(f)).toEndWith(decline); + } + }); + + test(`${harness}: the accept-formal-offer case requires setup to load the formal verification creator and end with ACCEPT-ROUTED`, async () => { + const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'accept-formal-offer')!; + await writeFile(join(f.dir, 'pstack-models.md'), 'stale\n'); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); + await c.prepare!(f); + await expect(readFile(join(f.dir, 'pstack-models.md'))).rejects.toThrow(); + if (harness === 'codex') await expect(readFile(join(f.dir, 'AGENTS.md'))).rejects.toThrow(); + expect(c.prompt(f)).toContain('Keep the first-run role assignments and every proposed effort. I confirm every write.'); + expect(c.prompt(f)).toEndWith('Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.'); + const creator = harness === 'claude' ? 'pstack:create-formal-verification-skill' : '/plugins/pstack/skills/create-formal-verification-skill/SKILL.md'; + const routed = (skills: string[], reply = 'ACCEPT-ROUTED'): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), skills, reply }); + expect((await c.assert(routed(['pstack:setup-pstack', creator]), f)).assertions) + .toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); + for (const skills of [['pstack:setup-pstack'], [creator, 'pstack:setup-pstack'], ['pstack:setup-pstack', 'pstack:create-verification-skill']]) { + await expect(c.assert(routed(skills), f)).rejects.toThrow('skill-not-routed:create-formal-verification-skill'); + } + await expect(c.assert(routed(['pstack:setup-pstack', creator], 'Want a formal verification skill?'), f)).rejects.toThrow('accept-formal-offer-did-not-finish'); }); } diff --git a/.claude/skills/verify-open-pstack/scripts/harness.test.ts b/.claude/skills/verify-open-pstack/scripts/harness.test.ts index f6a4adb6..5eaad1b8 100644 --- a/.claude/skills/verify-open-pstack/scripts/harness.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/harness.test.ts @@ -336,12 +336,28 @@ describe('headless recipes', () => { { type: 'item.completed', item: { id: 'item_3', type: 'agent_message', text: 'I ran it.' } }, ].map(event => JSON.stringify(event)).join('\n'); const record = parseSession('codex', stream, 0, 0); + expect(record.reply).toBe('I ran it.'); expect(record.commands).toEqual(['true']); expect(record.tools).toEqual([ { name: 'command', id: 'item_1', input: { command: 'true' }, result: 'out\n', parent: null, failed: false }, { name: 'command', id: 'item_2', input: { command: 'false' }, result: '', parent: null, failed: true }, ]); }); + test('each harness keeps the final assistant text as the reply, or empty text when there is none', () => { + expect(parseSession('claude', lines([ + { type: 'result', subtype: 'success', is_error: false, result: 'Early.' }, + { type: 'assistant', message: { content: [{ type: 'text', text: 'Not the result.' }] } }, + { type: 'result', subtype: 'success', is_error: false, result: 'SETUP-DONE' }, + ]), 0, 0).reply).toBe('SETUP-DONE'); + expect(parseSession('claude', lines([{ type: 'assistant', message: { content: [{ type: 'text', text: 'No result.' }] } }]), 0, 0).reply).toBe(''); + expect(parseSession('codex', lines([ + { type: 'item.completed', item: { id: 'item_0', type: 'agent_message', text: 'First.' } }, + { type: 'item.completed', item: { id: 'item_1', type: 'agent_message', text: 'ACCEPT-ROUTED' } }, + { type: 'item.completed', item: { id: 'item_2', type: 'command_execution', command: 'true', aggregated_output: '', exit_code: 0 } }, + { type: 'item.started', item: { id: 'item_3', type: 'agent_message', text: 'Unfinished.' } }, + ]), 0, 0).reply).toBe('ACCEPT-ROUTED'); + expect(parseSession('codex', lines([{ type: 'item.completed', item: { id: 'item_0', type: 'command_execution', command: 'true', exit_code: 0 } }]), 0, 0).reply).toBe(''); + }); test('missing or unsupported recipes fail before any session starts', async () => { const { root, installation } = await candidate('codex'); for (const [feature, reason] of [['mystery', 'missing-recipe:codex/mystery'], ['assets:codex', 'unsupported-native-consumer']]) { diff --git a/.claude/skills/verify-open-pstack/scripts/harness.ts b/.claude/skills/verify-open-pstack/scripts/harness.ts index 537206e4..b6ea2453 100644 --- a/.claude/skills/verify-open-pstack/scripts/harness.ts +++ b/.claude/skills/verify-open-pstack/scripts/harness.ts @@ -39,7 +39,8 @@ export function parseSession(harness: Harness, text: string, exitCode: number, s .flatMap(e => [...(e.message.content as string).matchAll(/\/([^<\s]+)<\/command-name>/g)].map(m => m[1]!)); const context = stream.filter(e => e.type === 'system' && e.subtype === 'hook_response' && e.hook_event === 'SessionStart' && e.exit_code === 0 && e.outcome === 'success' && typeof e.stdout === 'string').map(e => e.stdout as string); - return { harness, exitCode, started, context, + const result = stream.findLast(e => e.type === 'result')?.result; + return { harness, exitCode, started, context, reply: typeof result === 'string' ? result : '', skills: [...commands, ...uses.filter(u => u.name === 'Skill' && typeof u.input?.skill === 'string').map(u => u.input.skill as string)], commands: uses.filter(u => u.name === 'Bash' && typeof u.input?.command === 'string').map(u => u.input.command as string), tools: stream.filter(e => e.type === 'assistant' && Array.isArray(e.message?.content)).flatMap(e => (e.message.content as Event[]).filter(b => b.type === 'tool_use') @@ -58,7 +59,8 @@ export function parseSession(harness: Harness, text: string, exitCode: number, s .map(([, name, path]) => path!.includes('/plugins/cache/open-pstack/pstack/') ? name! : path!); const tools = items.filter(i => i.type === 'command_execution' && typeof i.command === 'string').map(i => ({ name: 'command', id: String(i.id), input: { command: i.command as string }, result: typeof i.aggregated_output === 'string' ? i.aggregated_output : undefined, parent: null, failed: i.exit_code !== 0 })); - return { harness, exitCode, started, skills, commands, tools, context }; + const reply = items.findLast(i => i.type === 'agent_message')?.text; + return { harness, exitCode, started, skills, commands, tools, context, reply: typeof reply === 'string' ? reply : '' }; } export async function codexInstallation(output: string, home: string, expected: string): Promise { const result = JSON.parse(output); diff --git a/.claude/skills/verify-open-pstack/scripts/reflect.test.ts b/.claude/skills/verify-open-pstack/scripts/reflect.test.ts index 57713e50..757c1c5c 100644 --- a/.claude/skills/verify-open-pstack/scripts/reflect.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/reflect.test.ts @@ -52,7 +52,7 @@ async function simulatedRecord(f: Fixture, available: boolean): Promise { diff --git a/.claude/skills/verify-open-pstack/scripts/runner.test.ts b/.claude/skills/verify-open-pstack/scripts/runner.test.ts index deb6cb5e..e15d7959 100644 --- a/.claude/skills/verify-open-pstack/scripts/runner.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/runner.test.ts @@ -37,7 +37,7 @@ test('the runner recipe adds one linked-worktree writer case for a Codex parent const writer = recipe('runner', 'codex')[1]!; await writer.prepare!(f); const record: SessionRecord = { harness: 'codex', exitCode: 0, started: Date.now() - 1000, skills: ['pstack:poteto-mode'], tools: [], - commands: [await launch(f, writer.prompt(f))], context: [] }; + commands: [await launch(f, writer.prompt(f))], context: [], reply: '' }; expect((await writer.assert(record, f)).assertions).toEqual(['runner-ran', 'receipt-complete', 'shared-git-denied', 'file:WRITTEN.md']); diff --git a/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts b/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts index 8a187ffb..a7966594 100644 --- a/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts @@ -15,7 +15,7 @@ async function waitingSession(harness: Harness): Promise<{ f: Fixture; c: Case; const f = { harness, dir, workspace: dir, location: dir, configHome: dir, run: command }; const c = recipe(`skill-invocation:${skill}`, harness)[0]!; await c.prepare!(f); - const record = { harness, exitCode: 0, started: Date.now() - 1000, skills: [`pstack:${skill}`], commands: [], tools: [], context: [] }; + const record = { harness, exitCode: 0, started: Date.now() - 1000, skills: [`pstack:${skill}`], commands: [], tools: [], context: [], reply: '' }; await writeFile(join(dir, 'result.md'), 'Waiting for you to approve inspection. I did not inspect anything.'); return { f, c, record }; } diff --git a/.claude/skills/verify-open-pstack/scripts/types.ts b/.claude/skills/verify-open-pstack/scripts/types.ts index 28278857..33f96d76 100644 --- a/.claude/skills/verify-open-pstack/scripts/types.ts +++ b/.claude/skills/verify-open-pstack/scripts/types.ts @@ -52,6 +52,7 @@ export interface SessionRecord { commands: string[]; tools: { name: string; id: string; input: Record; parent: string | null; result?: string; failed: boolean }[]; context: string[]; + reply: string; } export interface Driver { preflight(receipt: Receipt): Promise; diff --git a/.claude/skills/verify-open-pstack/scripts/verify.test.ts b/.claude/skills/verify-open-pstack/scripts/verify.test.ts index ecf07c36..e5a4e013 100644 --- a/.claude/skills/verify-open-pstack/scripts/verify.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/verify.test.ts @@ -233,7 +233,7 @@ describe('exact-head evidence publication', () => { test('more than the session limit is refused before preflight unless --wide gives a reason', async () => { const limited = (...extra: string[]) => { const f = fixture(true); f.options.github.files = async () => [{ filename: 'plugins/pstack/skills/poteto-mode/references/codex-tools.md' }]; - f.options.features = ['claude:setup', 'claude:runner', 'claude:hook:startup', ...extra]; + f.options.features = ['claude:setup', 'claude:runner', ...extra]; return f; }; expect(SESSION_LIMIT).toBe(12); From 41c1323769c0399ad1e578810c913e4a7140483b Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 02:41:53 -0400 Subject: [PATCH 09/12] fix(verifier): accept Codex's read of the installed creator as setup's handoff (#234) Codex follows a skill reference by reading its SKILL.md with a shell command, so its rollout has no injected block for the formal creator. accept-formal-offer now also counts a successful read of the installed creator's SKILL.md, under this run's installation, whose output carries the creator's frontmatter. Co-Authored-By: Claude Opus 5.5 --- .../verify-open-pstack/features/recipes.ts | 13 ++++++++-- .../verify-open-pstack/features/setup.md | 2 +- .../scripts/catalog.test.ts | 24 ++++++++++++++++++- 3 files changed, 35 insertions(+), 4 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index efd48078..69ef84c0 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -432,9 +432,10 @@ const setup: Case[] = [{ claudePermission: 'bypassPermissions', prepare: unconfigured, prompt: f => `${firstRunPrompt(f)} Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.`, - async assert(record) { + async assert(record, f) { const assertions = [loaded(record, 'pstack:setup-pstack')]; - if (!record.skills.slice(record.skills.indexOf('pstack:setup-pstack') + 1).some(isFormalCreator)) throw new Error('skill-not-routed:create-formal-verification-skill'); + const injected = record.skills.slice(record.skills.indexOf('pstack:setup-pstack') + 1).some(isFormalCreator); + if (!injected && !(f.harness === 'codex' && await readInstalledCreator(record, f))) throw new Error('skill-not-routed:create-formal-verification-skill'); return { assertions: [...assertions, 'routed:create-formal-verification-skill', ended(record, 'ACCEPT-ROUTED', 'accept-formal-offer-did-not-finish')], files: [] }; }, }]; @@ -443,6 +444,14 @@ const DECLINE_EXEMPT = new Set(['keep-setting', 'accept-formal-offer']); const isFormalCreator = (skill: string): boolean => skill === 'pstack:create-formal-verification-skill' || skill.endsWith('/create-formal-verification-skill/SKILL.md'); +const CREATOR_SKILL_FILE = '/skills/create-formal-verification-skill/SKILL.md', CREATOR_NAME_LINE = 'name: create-formal-verification-skill'; +async function readInstalledCreator(record: SessionRecord, f: Fixture): Promise { + const home = await realpath(f.configHome); + const paths = [f.location + CREATOR_SKILL_FILE]; + if (f.location.startsWith(`${home}/`)) paths.push(`$CODEX_HOME${f.location.slice(home.length)}${CREATOR_SKILL_FILE}`); + return record.tools.some(t => !t.failed && paths.some(path => String(t.input.command).includes(path)) && !!t.result?.split('\n').includes(CREATOR_NAME_LINE)); +} + async function unconfigured(f: Fixture): Promise { await rm(join(f.configHome, 'pstack-models.md'), { force: true }); if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index 5f05b5b5..e38eb2a0 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the verification-skill offer and accept the formal verification offer, and to stop as soon as the formal verification skill loads and reply with exactly `ACCEPT-ROUTED`. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex records the loaded skill by name or by its `SKILL.md` path, and either counts. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the verification-skill offer and accept the formal verification offer, and to stop as soon as the formal verification skill loads and reply with exactly `ACCEPT-ROUTED`. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence may be the injected skill record, by name or by `SKILL.md` path, or a successful command that reads the installed creator's `SKILL.md` under this run's installation and whose output has the line `name: create-formal-verification-skill`. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index 6403edd7..57777e65 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -4,6 +4,7 @@ import { tmpdir } from 'node:os'; import { join, resolve } from 'node:path'; import { fileURLToPath, pathToFileURL } from 'node:url'; import { readCatalog, recipe, type Case, type Catalog, type Fixture } from '../features/recipes.ts'; +import { parseSession } from './harness.ts'; import { command } from './io.ts'; import type { Harness, SessionRecord } from './types.ts'; @@ -411,7 +412,7 @@ for (const harness of ['claude', 'codex'] as const) { if (harness === 'codex') await expect(readFile(join(f.dir, 'AGENTS.md'))).rejects.toThrow(); expect(c.prompt(f)).toContain('Keep the first-run role assignments and every proposed effort. I confirm every write.'); expect(c.prompt(f)).toEndWith('Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.'); - const creator = harness === 'claude' ? 'pstack:create-formal-verification-skill' : '/plugins/pstack/skills/create-formal-verification-skill/SKILL.md'; + const creator = 'pstack:create-formal-verification-skill'; const routed = (skills: string[], reply = 'ACCEPT-ROUTED'): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), skills, reply }); expect((await c.assert(routed(['pstack:setup-pstack', creator]), f)).assertions) .toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); @@ -422,6 +423,27 @@ for (const harness of ['claude', 'codex'] as const) { }); } +test('codex: accept-formal-offer counts a successful read of this run\'s installed creator as the handoff, and nothing weaker', async () => { + const base = await fixture('codex'), installed = join(base.dir, 'plugins/cache/open-pstack/pstack/1.16.0'), f = { ...base, location: installed }; + const c = recipe('setup', 'codex').find(c => c.id === 'accept-formal-offer')!; + const rollout = JSON.stringify({ type: 'response_item', payload: { type: 'message', role: 'user', content: [{ type: 'input_text', + text: `\npstack:setup-pstack\n${installed}/skills/setup-pstack/SKILL.md\n---\nname: setup-pstack\n---\n` }] } }); + const frontmatter = '---\nname: create-formal-verification-skill\ndescription: "Generate a project-local skill that formally verifies the code."\n---\n\n# Create a formal verification skill\n'; + const read = (path: string, output = frontmatter, exitCode = 0) => ({ type: 'item.completed', item: { id: 'item_19', type: 'command_execution', + command: `/bin/zsh -lc 'cat "${path}" '`, aggregated_output: output, exit_code: exitCode, status: exitCode ? 'failed' : 'completed' } }); + const done = { type: 'item.completed', item: { id: 'item_20', type: 'agent_message', text: 'ACCEPT-ROUTED' } }; + const session = (...events: object[]) => parseSession('codex', events.map(e => JSON.stringify(e)).join('\n'), 0, 0, rollout); + const suffix = 'skills/create-formal-verification-skill/SKILL.md', viaHome = `$CODEX_HOME/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`; + for (const path of [viaHome, join(installed, suffix)]) { + expect(session(read(path), done).skills).toEqual(['pstack:setup-pstack']); + expect((await c.assert(session(read(path), done), f)).assertions).toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); + } + for (const events of [[read(viaHome, frontmatter, 1), done], [read(`$CODEX_HOME/plugins/cache/other/pstack/1.16.0/${suffix}`), done], + [read(join(base.dir, 'elsewhere', suffix)), done], [read(viaHome, '# Create a formal verification skill\n'), done], [done]]) { + await expect(c.assert(session(...events), f)).rejects.toThrow('skill-not-routed:create-formal-verification-skill'); + } +}); + const FAKE_CODEX = `#!/bin/sh if [ "$1" = "login" ]; then echo 'Logged in using ChatGPT'; exit 0; fi cat > /dev/null From 8ba8645d1279a263766bcc13885646cfa3181f41 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 03:15:52 -0400 Subject: [PATCH 10/12] fix(verifier): let only setup's offer lead accept-formal-offer to the creator (#234) The case's prompt named the formal verification offer, so a candidate whose setup no longer offered it could still load create-formal-verification-skill from the prompt and pass as routed. The prompt now declines /create-verification-skill and accepts any other offer, and never names the formal one. CHANGES.md now says which setup cases decline the offers. Co-Authored-By: Claude Opus 5.5 --- .claude/skills/verify-open-pstack/features/recipes.ts | 2 +- .claude/skills/verify-open-pstack/features/setup.md | 2 +- .claude/skills/verify-open-pstack/scripts/catalog.test.ts | 3 ++- CHANGES.md | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 69ef84c0..67e62f89 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -431,7 +431,7 @@ const setup: Case[] = [{ codexSandbox: 'danger-full-access', claudePermission: 'bypassPermissions', prepare: unconfigured, - prompt: f => `${firstRunPrompt(f)} Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.`, + prompt: f => `${firstRunPrompt(f)} Decline the offer to run /create-verification-skill. Accept any other offer setup makes. When the skill that offer starts loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.`, async assert(record, f) { const assertions = [loaded(record, 'pstack:setup-pstack')]; const injected = record.skills.slice(record.skills.indexOf('pstack:setup-pstack') + 1).some(isFormalCreator); diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index e38eb2a0..cd248a0e 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the verification-skill offer and accept the formal verification offer, and to stop as soon as the formal verification skill loads and reply with exactly `ACCEPT-ROUTED`. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence may be the injected skill record, by name or by `SKILL.md` path, or a successful command that reads the installed creator's `SKILL.md` under this run's installation and whose output has the line `name: create-formal-verification-skill`. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the offer to run `/create-verification-skill`, accept any other offer, and stop as soon as the skill that offer starts loads, replying with exactly `ACCEPT-ROUTED`. The prompt never names the formal offer, so the creator loads only if setup offers it. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence may be the injected skill record, by name or by `SKILL.md` path, or a successful command that reads the installed creator's `SKILL.md` under this run's installation and whose output has the line `name: create-formal-verification-skill`. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index 57777e65..2e8417f3 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -411,7 +411,8 @@ for (const harness of ['claude', 'codex'] as const) { await expect(readFile(join(f.dir, 'pstack-models.md'))).rejects.toThrow(); if (harness === 'codex') await expect(readFile(join(f.dir, 'AGENTS.md'))).rejects.toThrow(); expect(c.prompt(f)).toContain('Keep the first-run role assignments and every proposed effort. I confirm every write.'); - expect(c.prompt(f)).toEndWith('Decline the verification-skill offer and accept the formal verification offer. When the formal verification skill loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.'); + expect(c.prompt(f)).not.toMatch(/formal/i); + expect(c.prompt(f)).toEndWith('Decline the offer to run /create-verification-skill. Accept any other offer setup makes. When the skill that offer starts loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.'); const creator = 'pstack:create-formal-verification-skill'; const routed = (skills: string[], reply = 'ACCEPT-ROUTED'): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), skills, reply }); expect((await c.assert(routed(['pstack:setup-pstack', creator]), f)).assertions) diff --git a/CHANGES.md b/CHANGES.md index 31a766d3..cff7f79a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -23,7 +23,7 @@ Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff **Comments sweep (#218).** Code this repository owns drops comments outside the keep-list in `AGENTS.md`, across the runner, the Codex transcript resolver, the startup hook, the verifier, tests and repository config. A test keeps every model pair released by 1.15.0 in place. -**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills, every setup recipe declines both offers, `first-run` asserts that no project skill directory appears, and `keep-setting` checks a quiet rerun. +**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills. Setup cases decline both offers, except two: `keep-setting` supplies no answers and checks a quiet rerun, and `accept-formal-offer` declines `/create-verification-skill`, accepts any other offer, and checks that setup hands off to `create-formal-verification-skill`. `first-run` asserts that no project skill directory appears. **Not applied.** See `UPSTREAM.md`: upstream's generated Claude Code tree, its adapter, generator, plugin validator and root marketplace entry, the docs-vs-tree check, the two `poteto-help` harness paragraphs, `make-bot-ui`, and the 0.15.26 to 0.15.29 manifests and guide. Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install one of the two, because both use the `pstack:` prefix. `README-UPSTREAM.md` is the verbatim upstream README. From 4ac36d85b70c1172fc39e9b60ad70fd309d562c5 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 07:25:56 -0400 Subject: [PATCH 11/12] fix(verifier): recognize Codex's creator read by its content (#234) The accept-formal-offer case matched the creator's path spelling, so a real Codex session that read it through a relative path failed as not routed. The case now counts a successful command whose output carries the installed creator's frontmatter name and description lines, whatever the path spelling. Co-Authored-By: Claude Opus 5.5 --- .../verify-open-pstack/features/recipes.ts | 10 +++---- .../verify-open-pstack/features/setup.md | 2 +- .../scripts/catalog.test.ts | 26 +++++++++++-------- 3 files changed, 21 insertions(+), 17 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 67e62f89..22b30503 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -444,12 +444,12 @@ const DECLINE_EXEMPT = new Set(['keep-setting', 'accept-formal-offer']); const isFormalCreator = (skill: string): boolean => skill === 'pstack:create-formal-verification-skill' || skill.endsWith('/create-formal-verification-skill/SKILL.md'); -const CREATOR_SKILL_FILE = '/skills/create-formal-verification-skill/SKILL.md', CREATOR_NAME_LINE = 'name: create-formal-verification-skill'; async function readInstalledCreator(record: SessionRecord, f: Fixture): Promise { - const home = await realpath(f.configHome); - const paths = [f.location + CREATOR_SKILL_FILE]; - if (f.location.startsWith(`${home}/`)) paths.push(`$CODEX_HOME${f.location.slice(home.length)}${CREATOR_SKILL_FILE}`); - return record.tools.some(t => !t.failed && paths.some(path => String(t.input.command).includes(path)) && !!t.result?.split('\n').includes(CREATOR_NAME_LINE)); + const lines = (await readFile(`${f.location}/skills/create-formal-verification-skill/SKILL.md`, 'utf8')).split('\n'); + const frontmatter = lines.slice(1, lines.indexOf('---', 1)); + const expected = ['name: ', 'description: '].map(key => frontmatter.find(line => line.startsWith(key)) ?? ''); + if (expected.includes('')) throw new Error('creator-frontmatter-incomplete'); + return record.tools.some(t => !t.failed && expected.every(line => !!t.result?.includes(line))); } async function unconfigured(f: Fixture): Promise { diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index cd248a0e..f126d3cd 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the offer to run `/create-verification-skill`, accept any other offer, and stop as soon as the skill that offer starts loads, replying with exactly `ACCEPT-ROUTED`. The prompt never names the formal offer, so the creator loads only if setup offers it. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence may be the injected skill record, by name or by `SKILL.md` path, or a successful command that reads the installed creator's `SKILL.md` under this run's installation and whose output has the line `name: create-formal-verification-skill`. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the offer to run `/create-verification-skill`, accept any other offer, and stop as soon as the skill that offer starts loads, replying with exactly `ACCEPT-ROUTED`. The prompt never names the formal offer, so the creator loads only if setup offers it. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence is the injected skill record, by name or by `SKILL.md` path, or a successful command whose output carries the installed creator's frontmatter `name:` and `description:` lines. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index 2e8417f3..3e1e13f8 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -424,23 +424,27 @@ for (const harness of ['claude', 'codex'] as const) { }); } -test('codex: accept-formal-offer counts a successful read of this run\'s installed creator as the handoff, and nothing weaker', async () => { +test('codex: accept-formal-offer counts a successful command whose output carries the installed creator\'s name and description lines', async () => { const base = await fixture('codex'), installed = join(base.dir, 'plugins/cache/open-pstack/pstack/1.16.0'), f = { ...base, location: installed }; + const suffix = 'skills/create-formal-verification-skill/SKILL.md', creator = await readFile(join(location, suffix), 'utf8'); + await mkdir(join(installed, 'skills/create-formal-verification-skill'), { recursive: true }); + await writeFile(join(installed, suffix), creator); const c = recipe('setup', 'codex').find(c => c.id === 'accept-formal-offer')!; const rollout = JSON.stringify({ type: 'response_item', payload: { type: 'message', role: 'user', content: [{ type: 'input_text', text: `\npstack:setup-pstack\n${installed}/skills/setup-pstack/SKILL.md\n---\nname: setup-pstack\n---\n` }] } }); - const frontmatter = '---\nname: create-formal-verification-skill\ndescription: "Generate a project-local skill that formally verifies the code."\n---\n\n# Create a formal verification skill\n'; - const read = (path: string, output = frontmatter, exitCode = 0) => ({ type: 'item.completed', item: { id: 'item_19', type: 'command_execution', - command: `/bin/zsh -lc 'cat "${path}" '`, aggregated_output: output, exit_code: exitCode, status: exitCode ? 'failed' : 'completed' } }); - const done = { type: 'item.completed', item: { id: 'item_20', type: 'agent_message', text: 'ACCEPT-ROUTED' } }; + const read = (cat: string, output = creator, exitCode = 0) => ({ type: 'item.completed', item: { id: 'item_21', type: 'command_execution', + command: `/bin/zsh -lc '${cat}'`, aggregated_output: output, exit_code: exitCode, status: exitCode ? 'failed' : 'completed' } }); + const done = { type: 'item.completed', item: { id: 'item_22', type: 'agent_message', text: 'ACCEPT-ROUTED' } }; const session = (...events: object[]) => parseSession('codex', events.map(e => JSON.stringify(e)).join('\n'), 0, 0, rollout); - const suffix = 'skills/create-formal-verification-skill/SKILL.md', viaHome = `$CODEX_HOME/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`; - for (const path of [viaHome, join(installed, suffix)]) { - expect(session(read(path), done).skills).toEqual(['pstack:setup-pstack']); - expect((await c.assert(session(read(path), done), f)).assertions).toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); + const relative = `cat ../../.codex/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`, numbered = creator.split('\n').map((line, i) => `${String(i + 1).padStart(6)}\t${line}`).join('\n'); + for (const event of [read(relative), read(`cat $CODEX_HOME/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`), + read(`cat "\${CODEX_HOME}/plugins/cache/open-pstack/pstack/1.16.0/${suffix}"`), read(`cat -n ${join(installed, suffix)}`, numbered)]) { + expect(session(event, done).skills).toEqual(['pstack:setup-pstack']); + expect((await c.assert(session(event, done), f)).assertions).toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); } - for (const events of [[read(viaHome, frontmatter, 1), done], [read(`$CODEX_HOME/plugins/cache/other/pstack/1.16.0/${suffix}`), done], - [read(join(base.dir, 'elsewhere', suffix)), done], [read(viaHome, '# Create a formal verification skill\n'), done], [done]]) { + const nameOnly = creator.split('\n').filter(line => !line.startsWith('description: ')).join('\n'); + const other = await readFile(join(location, 'skills/setup-pstack/SKILL.md'), 'utf8'); + for (const events of [[read(relative, creator, 1), done], [read(relative, nameOnly), done], [read('cat skills/setup-pstack/SKILL.md', other), done], [done]]) { await expect(c.assert(session(...events), f)).rejects.toThrow('skill-not-routed:create-formal-verification-skill'); } }); From dc9d157276ff9c3fdf1e4a8d3e39e714debef8b1 Mon Sep 17 00:00:00 2001 From: Eric Litman Date: Wed, 21 Oct 2026 07:52:15 -0400 Subject: [PATCH 12/12] revert(verifier): drop the setup test machinery added for #46 Restore the verifier's recipes, setup notes, parser and tests to main. This removes the accept-formal-offer case, the SETUP-DONE and ACCEPT-ROUTED sentinels, the parser's reply field, the offer-decline sentence and the extra keep-setting and first-run assertions. The registry still lists the two formal verification skills. Co-Authored-By: Claude Opus 5.5 --- .../verify-open-pstack/features/recipes.ts | 85 +++--------- .../verify-open-pstack/features/setup.md | 2 +- .../scripts/catalog.test.ts | 123 +++--------------- .../scripts/harness.test.ts | 16 --- .../verify-open-pstack/scripts/harness.ts | 6 +- .../scripts/reflect.test.ts | 2 +- .../verify-open-pstack/scripts/runner.test.ts | 2 +- .../scripts/skill-invocation.test.ts | 2 +- .../verify-open-pstack/scripts/types.ts | 1 - .../verify-open-pstack/scripts/verify.test.ts | 2 +- CHANGES.md | 2 +- 11 files changed, 48 insertions(+), 195 deletions(-) diff --git a/.claude/skills/verify-open-pstack/features/recipes.ts b/.claude/skills/verify-open-pstack/features/recipes.ts index 22b30503..0a83f5ed 100644 --- a/.claude/skills/verify-open-pstack/features/recipes.ts +++ b/.claude/skills/verify-open-pstack/features/recipes.ts @@ -1,5 +1,5 @@ import { Database } from 'bun:sqlite'; -import { lstat, mkdir, readFile, realpath, rm, utimes, writeFile } from 'node:fs/promises'; +import { lstat, mkdir, readFile, realpath, rm, writeFile } from 'node:fs/promises'; import { homedir } from 'node:os'; import { basename, join } from 'node:path'; import { pathToFileURL } from 'node:url'; @@ -31,7 +31,6 @@ export const CLAUDE_TOOLS = 'Skill,Read,Glob,Grep,Write,Edit,Bash,Agent,Task,Tod export const DEFAULT_ROLES: Record = { claude: 'bug-fix', codex: 'judgment and prose' }; export const ROUTE = /^([a-z][a-z0-9-]*):([A-Za-z0-9._/-]+)@([a-z]+)$/; const SETUP_DESCRIPTOR = 'claude:opus@high'; -const DECLINE_OFFERS = 'If setup offers to generate a verification skill or a formal verification skill, decline both.'; const DESCRIPTOR = /\b[a-z][a-z0-9-]*:[A-Za-z0-9._/-]+@[a-z]+/g; const SHEET_HEADER = '# pstack model configuration\n\n'; const SETTING = 'codex writer sandbox: '; @@ -81,16 +80,6 @@ function loaded(record: SessionRecord, skill: string): string { return 'skill-loaded'; } -function ended(record: SessionRecord, word: string, failure: string): string { - if (record.reply.trim() !== word) throw new Error(failure); - return `ended:${word}`; -} - -async function noSkillDirectory(f: Fixture, failure: string): Promise { - for (const skills of ['.claude/skills', '.agents/skills']) if (await lstat(join(f.dir, skills)).then(() => true, () => false)) throw new Error(`${failure}:${skills}`); - return 'no-skill-directory'; -} - async function written(record: SessionRecord, path: string): Promise { const info = await lstat(path).catch(() => undefined); if (!info?.isFile() || !info.size || info.mtimeMs < record.started) throw new Error(`fixture-file-missing:${basename(path)}`); @@ -416,51 +405,20 @@ const setup: Case[] = [{ id: 'first-run', codexSandbox: 'danger-full-access', claudePermission: 'bypassPermissions', - prepare: unconfigured, - prompt: firstRunPrompt, + async prepare(f) { + await rm(join(f.configHome, 'pstack-models.md'), { force: true }); + if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); + }, + prompt: f => `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep the first-run role assignments and every proposed effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; const text = await readFile(sheet, 'utf8'); if (!Bun.deepEquals(roleLines(text), [...(await readCatalog(f.location)).defaults].map(([role, lanes]) => `${role}: ${lanes.join(', ')}`))) throw new Error('first-run-not-role-defaults'); bounded(text); - const declined = await noSkillDirectory(f, 'first-run-offer-accepted'); - return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`, declined], files: [sheet] }; - }, -}, { - id: 'accept-formal-offer', - codexSandbox: 'danger-full-access', - claudePermission: 'bypassPermissions', - prepare: unconfigured, - prompt: f => `${firstRunPrompt(f)} Decline the offer to run /create-verification-skill. Accept any other offer setup makes. When the skill that offer starts loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.`, - async assert(record, f) { - const assertions = [loaded(record, 'pstack:setup-pstack')]; - const injected = record.skills.slice(record.skills.indexOf('pstack:setup-pstack') + 1).some(isFormalCreator); - if (!injected && !(f.harness === 'codex' && await readInstalledCreator(record, f))) throw new Error('skill-not-routed:create-formal-verification-skill'); - return { assertions: [...assertions, 'routed:create-formal-verification-skill', ended(record, 'ACCEPT-ROUTED', 'accept-formal-offer-did-not-finish')], files: [] }; + return { assertions: [...assertions, ...await mirrored(f, sheet), 'sheet:role-defaults', `setting:${BOUNDED_SETTING}`], files: [sheet] }; }, }]; -const DECLINE_EXEMPT = new Set(['keep-setting', 'accept-formal-offer']); -const isFormalCreator = (skill: string): boolean => - skill === 'pstack:create-formal-verification-skill' || skill.endsWith('/create-formal-verification-skill/SKILL.md'); - -async function readInstalledCreator(record: SessionRecord, f: Fixture): Promise { - const lines = (await readFile(`${f.location}/skills/create-formal-verification-skill/SKILL.md`, 'utf8')).split('\n'); - const frontmatter = lines.slice(1, lines.indexOf('---', 1)); - const expected = ['name: ', 'description: '].map(key => frontmatter.find(line => line.startsWith(key)) ?? ''); - if (expected.includes('')) throw new Error('creator-frontmatter-incomplete'); - return record.tools.some(t => !t.failed && expected.every(line => !!t.result?.includes(line))); -} - -async function unconfigured(f: Fixture): Promise { - await rm(join(f.configHome, 'pstack-models.md'), { force: true }); - if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); -} - -function firstRunPrompt(f: Fixture): string { - return `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep the first-run role assignments and every proposed effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`; -} - function bounded(text: string): void { if (!Bun.deepEquals(settingLines(text), [BOUNDED_SETTING])) throw new Error('setting-not-bounded'); } @@ -597,30 +555,25 @@ function writerRefusal(): Case { } function keepSetting(): Case { - let sheetBytes = '', mirrorBytes = ''; + let expected: string[] = []; return { id: 'keep-setting', codexSandbox: 'danger-full-access', claudePermission: 'bypassPermissions', async prepare(f) { - sheetBytes = sheetText([...(await readCatalog(f.location)).defaults]) + `${FULL_ACCESS_SETTING}\n`; - mirrorBytes = `${MIRROR_BEGIN}\n${sheetBytes}${MIRROR_END}\n`; - const prepared = new Date(Date.now() - 3_600_000), sheet = join(f.configHome, 'pstack-models.md'), mirror = join(f.configHome, 'AGENTS.md'); - await writeFile(sheet, sheetBytes); - await utimes(sheet, prepared, prepared); - if (f.harness === 'codex') { - await writeFile(mirror, mirrorBytes); - await utimes(mirror, prepared, prepared); - } + const roles = [...(await readCatalog(f.location)).defaults]; + const omitted = roles.find(([, lanes]) => lanes.every(lane => !lane.includes(':')))?.[0]; + expected = roles.map(([role, lanes]) => `${role}: ${lanes.join(', ')}`).sort(); + await writeFile(join(f.configHome, 'pstack-models.md'), sheetText(roles.filter(([role]) => role !== omitted)) + `${FULL_ACCESS_SETTING}\n`); + if (f.harness === 'codex') await rm(join(f.configHome, 'AGENTS.md'), { force: true }); }, - prompt: f => `${invoke(f.harness, 'setup-pstack', `Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub. Reply with exactly SETUP-DONE as your final message.`, + prompt: f => `${invoke(f.harness, 'setup-pstack', `Use these answers and ask nothing else. Keep every role assignment and every family's current effort. I confirm every write. Write the setup report to ${join(f.dir, 'result.md')}.`)} Do not push, post, or contact GitHub.`, async assert(record, f) { const sheet = join(f.configHome, 'pstack-models.md'), assertions = [loaded(record, 'pstack:setup-pstack'), await written(record, sheet)]; - if (f.harness === 'claude' && record.tools.some(t => t.name === 'AskUserQuestion')) throw new Error('keep-setting-asked'); - if (await readFile(sheet, 'utf8') !== sheetBytes) throw new Error('keep-setting-sheet-changed'); - if (f.harness === 'codex' && await readFile(join(f.configHome, 'AGENTS.md'), 'utf8').catch(() => '') !== mirrorBytes) throw new Error('keep-setting-mirror-changed'); - const quiet = [await noSkillDirectory(f, 'keep-setting-offer-accepted'), ended(record, 'SETUP-DONE', 'keep-setting-did-not-finish')]; - return { assertions: [...assertions, ...(f.harness === 'claude' ? ['no-askuserquestion-attempt'] : []), 'sheet-unchanged', ...(f.harness === 'codex' ? ['codex-mirror-unchanged'] : []), ...quiet, `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; + const text = await readFile(sheet, 'utf8'); + if (!Bun.deepEquals(settingLines(text), [FULL_ACCESS_SETTING])) throw new Error('setting-not-kept'); + if (!Bun.deepEquals(roleLines(text).sort(), expected)) throw new Error('keep-setting-sheet-mismatch'); + return { assertions: [...assertions, ...await mirrored(f, sheet), `setting:${FULL_ACCESS_SETTING}`], files: [sheet] }; }, }; } @@ -734,7 +687,7 @@ export function recipe(feature: string, harness: Harness, routes: string[] = []) if (feature === 'project-skill') return [projectSkill]; if (feature === 'hook:startup') return [startupHook]; if (feature === 'runner') return runner(harness, routes); - if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup.map(c => DECLINE_EXEMPT.has(c.id) ? c : { ...c, prompt: f => `${c.prompt(f)} ${DECLINE_OFFERS}` }); + if (feature === 'setup' || feature === 'skill-invocation:setup-pstack') return setup; if (feature === 'catalog') return catalog(harness); if (feature === 'shipped-tools') return [shippedTools]; if (feature === 'agent-preload:poteto-agent' && harness === 'claude') return [agentPreload]; diff --git a/.claude/skills/verify-open-pstack/features/setup.md b/.claude/skills/verify-open-pstack/features/setup.md index f126d3cd..bc2fc7a3 100644 --- a/.claude/skills/verify-open-pstack/features/setup.md +++ b/.claude/skills/verify-open-pstack/features/setup.md @@ -20,4 +20,4 @@ Claude uses the operator's normal config/login; Codex uses a run-owned home with ## Headless -The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. It runs nine cases per harness. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's complete role defaults with the line `codex writer sandbox: full-access`, and on Codex a run-owned `AGENTS.md` whose mirror agrees with that sheet. It supplies no answers, not even the sentence that declines the offers, and asks the session to reply with exactly `SETUP-DONE` as its final message. On this qualifying rerun setup must only mention its two offers. The case asserts that setup wrote the sheet, that the sheet and the Codex `AGENTS.md` keep their prepared bytes, that the fixture gained no `.claude/skills` or `.agents/skills` directory, and that the session's final assistant text, trimmed, is exactly `SETUP-DONE`. A final question fails the case. In Claude it also asserts that the session attempted no `AskUserQuestion` call, including a call that failed. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults, and that the fixture gained no `.claude/skills` or `.agents/skills` directory. A ninth, `accept-formal-offer`, prepares the fixture as `first-run` does and gives the first-run answers. It tells setup to decline the offer to run `/create-verification-skill`, accept any other offer, and stop as soon as the skill that offer starts loads, replying with exactly `ACCEPT-ROUTED`. The prompt never names the formal offer, so the creator loads only if setup offers it. It asserts that `pstack:create-formal-verification-skill` loaded after setup-pstack and that the final assistant text, trimmed, is exactly `ACCEPT-ROUTED`. Codex routing evidence is the injected skill record, by name or by `SKILL.md` path, or a successful command whose output carries the installed creator's frontmatter `name:` and `description:` lines. Every other setup prompt ends with one sentence that declines setup's offers to generate a verification skill and a formal verification skill. The parser keeps each session's final assistant text: in Claude, the last `result` event's `result`; in Codex, the text of the last completed `agent_message` item. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. +The setup recipe in `recipes.ts` serves `setup` and `skill-invocation:setup-pstack`. One session, `configure`, runs setup with explicit answers that move every model-family role to `claude:opus@high` and answer yes when setup asks whether Codex writer lanes should run with full access. Setup keeps an existing setting line without asking, so before the session the case removes any `codex writer sandbox:` line from the operator's sheet and keeps every other byte. It asserts that the written sheet holds only that descriptor and exactly one setting line, `codex writer sandbox: full-access`. A second session has `poteto-mode` report the configured route for one role. A third, `keep-predecessor`, writes a sheet whose every family lane is `grok:grok-4.6@high`, a kept predecessor, with one alias role left out, and asks setup to decline the replacement. It asserts the rewritten sheet keeps `grok:grok-4.6@high`, restores the missing role, and that the reported proposal is the family's current model from the installed catalog at the same effort. A fourth, `new-families`, writes the installed catalog's role defaults with `swarm workers` on `codex:gpt-6-luna@max`, `hardest tasks` on the registered pin `claude:claude-opus-5-5@max`, `how explainer` on the versioned `claude:claude-sonnet-5-5@max`, and `judgment and prose` on the older revision `claude:claude-opus-5@max`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line, except that the versioned revisions are written as `claude:sonnet@max` and `claude:opus@max`. A fifth, `read-only-provider`, writes the installed catalog's role defaults with the read-only role `how explorer` on `devin:swe-2@max`, a provider whose route table lists only `read-only`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that every role line of the rewritten sheet equals the prepared line. A sixth, `writer-refusal`, assigns the writer role `bug-fix` to `devin:swe-2@max` and asks setup to keep every assignment. It asserts that the sheet keeps its exact bytes, that Codex's removed mirror is not written back, and that setup's refusal names the role and the provider. A seventh, `keep-setting`, writes the installed catalog's role defaults with one alias role left out and the line `codex writer sandbox: full-access`, and asks setup to keep every assignment and effort. On Codex it removes the run-owned `AGENTS.md` mirror first. It asserts that the rewritten sheet holds that setting line exactly once and that its role lines equal the role defaults. An eighth, `first-run`, removes the sheet (and, on Codex, the run-owned `AGENTS.md` mirror) and asserts that setup writes a sheet whose role lines equal the installed catalog's role defaults. Every role-line comparison leaves out the setting line. Setup asks about full access when the sheet has no setting line, and declining is the default. So `keep-predecessor`, `new-families`, `read-only-provider` and `first-run`, which start without a setting line and take the default answers, each assert that the written sheet holds exactly one setting line, `codex writer sandbox: bounded`. A missing setting line or an unrequested `full-access` fails them. `writer-refusal` keeps its exact-bytes check: its prepared sheet has no setting line, and setup writes nothing. Every case that removes the Codex `AGENTS.md` mirror also asserts that setup wrote it back: exactly one begin marker and a newline, the rewritten sheet's exact bytes, and one end marker. The parent snapshots the daily files before the first session and restores and verifies them after the last, on success or failure. diff --git a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts index 3e1e13f8..9644c074 100644 --- a/.claude/skills/verify-open-pstack/scripts/catalog.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/catalog.test.ts @@ -4,7 +4,6 @@ import { tmpdir } from 'node:os'; import { join, resolve } from 'node:path'; import { fileURLToPath, pathToFileURL } from 'node:url'; import { readCatalog, recipe, type Case, type Catalog, type Fixture } from '../features/recipes.ts'; -import { parseSession } from './harness.ts'; import { command } from './io.ts'; import type { Harness, SessionRecord } from './types.ts'; @@ -17,7 +16,7 @@ async function fixture(harness: Harness): Promise { return { harness, dir, workspace, location, configHome: dir, run: command }; } const record = (harness: Harness, skill: string): SessionRecord => - ({ harness, exitCode: 0, started: Date.now() - 1000, skills: [skill], commands: [], tools: [], context: [], reply: '' }); + ({ harness, exitCode: 0, started: Date.now() - 1000, skills: [skill], commands: [], tools: [], context: [] }); const sheet = async (path: string): Promise> => new Map((await readFile(path, 'utf8')).split('\n') .filter(line => /^[a-z][^:]*: \S/.test(line)).map((line): [string, string[]] => [line.slice(0, line.indexOf(': ')), line.slice(line.indexOf(': ') + 2).split(', ')])); const setupCase = (id: string): Case => recipe('setup', 'claude').find(c => c.id === id)!; @@ -288,16 +287,10 @@ test('the first-run case requires a sheet equal to the catalog role defaults', a await writeFile(path, written); await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow('codex-mirror-mismatch'); await mirror(f, written); - expect((await c.assert(record('codex', 'pstack:setup-pstack'), f)).assertions).toEqual(expect.arrayContaining(['sheet:role-defaults', 'no-skill-directory'])); + expect((await c.assert(record('codex', 'pstack:setup-pstack'), f)).assertions).toContain('sheet:role-defaults'); await rejectsUnbounded(c, f, written); await writeFile(path, `# pstack model configuration\n\n${lines.slice(1).join('\n')}\n`); await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow('first-run-not-role-defaults'); - await writeFile(path, written); - for (const skills of ['.claude/skills', '.agents/skills']) { - await mkdir(join(f.dir, skills), { recursive: true }); - await expect(c.assert(record('codex', 'pstack:setup-pstack'), f)).rejects.toThrow(`first-run-offer-accepted:${skills}`); - await rm(join(f.dir, skills.split('/')[0]!), { recursive: true }); - } }); test('the configure case answers yes to full access and requires that setting with only the Opus descriptor', async () => { @@ -348,107 +341,33 @@ test('the full-access writer case quotes each browser argument for sh and encode }); for (const harness of ['claude', 'codex'] as const) { - test(`${harness}: the keep-setting case gives no answers and requires an unchanged sheet and mirror, SETUP-DONE, and no question in Claude`, async () => { + test(`${harness}: the keep-setting case requires the setting line and every role line after a rerun`, async () => { const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!, installed = await readCatalog(location); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); await c.prepare!(f); - const path = join(f.dir, 'pstack-models.md'), prepared = await readFile(path, 'utf8'); - expect(prepared).toBe(`# pstack model configuration\n\n${[...installed.defaults].map(([role, lanes]) => `${role}: ${lanes.join(', ')}`).join('\n')}\n${FULL_ACCESS}`); - const agents = harness === 'codex' ? `\n${prepared}\n` : 'mirror\n'; - expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe(agents); - expect(c.prompt(f)).not.toContain('Use these answers'); - expect(c.prompt(f)).not.toContain('decline'); - expect(c.prompt(f)).toEndWith('Reply with exactly SETUP-DONE as your final message.'); - await writeFile(path, prepared); - const done = (): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), reply: '\nSETUP-DONE\n' }); - expect((await c.assert(done(), f)).assertions).toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'claude' ? ['no-askuserquestion-attempt'] : []), 'sheet-unchanged', - ...(harness === 'codex' ? ['codex-mirror-unchanged'] : []), 'no-skill-directory', 'ended:SETUP-DONE', 'setting:codex writer sandbox: full-access']); - - for (const reply of ['Want a project-local verification skill? I can generate one with /create-verification-skill.', '']) { - await expect(c.assert({ ...done(), reply }, f)).rejects.toThrow('keep-setting-did-not-finish'); - } - const asked = done(); - asked.tools.push({ name: 'AskUserQuestion', id: 'q', input: {}, parent: null, failed: true }); - if (harness === 'claude') await expect(c.assert(asked, f)).rejects.toThrow('keep-setting-asked'); - else expect((await c.assert(asked, f)).assertions).not.toContain('no-askuserquestion-attempt'); - for (const skills of ['.claude/skills', '.agents/skills']) { - await mkdir(join(f.dir, skills), { recursive: true }); - await expect(c.assert(done(), f)).rejects.toThrow(`keep-setting-offer-accepted:${skills}`); - await rm(join(f.dir, skills.split('/')[0]!), { recursive: true }); - } - for (const wrong of [prepared.replace(FULL_ACCESS, ''), prepared.replace(FULL_ACCESS, BOUNDED), prepared.replace(/\nbug-fix: [^\n]*/, ''), `${prepared}\n`]) { - await writeFile(path, wrong); - await expect(c.assert(done(), f)).rejects.toThrow('keep-setting-sheet-changed'); - } - await writeFile(path, prepared); - if (harness === 'codex') { - await writeFile(join(f.dir, 'AGENTS.md'), `notes\n${agents}`); - await expect(c.assert(done(), f)).rejects.toThrow('keep-setting-mirror-changed'); - } - }); - - test(`${harness}: the keep-setting case rejects a session that wrote nothing after prepare`, async () => { - const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'keep-setting')!; - await c.prepare!(f); - const started = Date.now(); - await expect(c.assert({ ...record(harness, 'pstack:setup-pstack'), started }, f)).rejects.toThrow('fixture-file-missing:pstack-models.md'); - }); - - test(`${harness}: every setup prompt but keep-setting and accept-formal-offer declines both verification offers`, async () => { - const f = await fixture(harness), decline = 'If setup offers to generate a verification skill or a formal verification skill, decline both.'; - const cases = recipe('setup', harness); - expect(cases.map(c => c.id)).toEqual(['configure', 'consume', 'keep-predecessor', 'new-families', 'read-only-provider', 'writer-refusal', 'keep-setting', 'first-run', 'accept-formal-offer']); - for (const c of cases) { - if (['keep-setting', 'accept-formal-offer'].includes(c.id)) expect(c.prompt(f)).not.toContain(decline); - else expect(c.prompt(f)).toEndWith(decline); - } - }); - - test(`${harness}: the accept-formal-offer case requires setup to load the formal verification creator and end with ACCEPT-ROUTED`, async () => { - const f = await fixture(harness), c = recipe('setup', harness).find(c => c.id === 'accept-formal-offer')!; - await writeFile(join(f.dir, 'pstack-models.md'), 'stale\n'); await writeFile(join(f.dir, 'AGENTS.md'), 'mirror\n'); - await c.prepare!(f); - await expect(readFile(join(f.dir, 'pstack-models.md'))).rejects.toThrow(); if (harness === 'codex') await expect(readFile(join(f.dir, 'AGENTS.md'))).rejects.toThrow(); - expect(c.prompt(f)).toContain('Keep the first-run role assignments and every proposed effort. I confirm every write.'); - expect(c.prompt(f)).not.toMatch(/formal/i); - expect(c.prompt(f)).toEndWith('Decline the offer to run /create-verification-skill. Accept any other offer setup makes. When the skill that offer starts loads, stop at once without doing its work and reply with exactly ACCEPT-ROUTED as your final message.'); - const creator = 'pstack:create-formal-verification-skill'; - const routed = (skills: string[], reply = 'ACCEPT-ROUTED'): SessionRecord => ({ ...record(harness, 'pstack:setup-pstack'), skills, reply }); - expect((await c.assert(routed(['pstack:setup-pstack', creator]), f)).assertions) - .toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); - for (const skills of [['pstack:setup-pstack'], [creator, 'pstack:setup-pstack'], ['pstack:setup-pstack', 'pstack:create-verification-skill']]) { - await expect(c.assert(routed(skills), f)).rejects.toThrow('skill-not-routed:create-formal-verification-skill'); + else expect(await readFile(join(f.dir, 'AGENTS.md'), 'utf8')).toBe('mirror\n'); + const path = join(f.dir, 'pstack-models.md'), prepared = await readFile(path, 'utf8'); + expect(prepared).toEndWith('\ncodex writer sandbox: full-access\n'); + const omitted = [...installed.defaults.keys()].find(role => !prepared.includes(`\n${role}: `))!; + expect(installed.defaults.get(omitted)).toEqual(['inherit-parent']); + const rerun = prepared.replace('codex writer sandbox: full-access\n', `${omitted}: inherit-parent\ncodex writer sandbox: full-access\n`); + await writeFile(path, rerun); + if (harness === 'codex') await mirror(f, rerun); + expect((await c.assert(record(harness, 'pstack:setup-pstack'), f)).assertions) + .toEqual(['skill-loaded', 'file:pstack-models.md', ...(harness === 'codex' ? ['codex-mirror'] : []), 'setting:codex writer sandbox: full-access']); + + for (const [wrong, reason] of [ + [rerun.replace('codex writer sandbox: full-access\n', ''), 'setting-not-kept'], + [rerun.replace('sandbox: full-access', 'sandbox: bounded'), 'setting-not-kept'], + [rerun.replace(/\nbug-fix: [^\n]*/, ''), 'keep-setting-sheet-mismatch'], + ]) { + await writeFile(path, wrong!); + await expect(c.assert(record(harness, 'pstack:setup-pstack'), f)).rejects.toThrow(reason); } - await expect(c.assert(routed(['pstack:setup-pstack', creator], 'Want a formal verification skill?'), f)).rejects.toThrow('accept-formal-offer-did-not-finish'); }); } -test('codex: accept-formal-offer counts a successful command whose output carries the installed creator\'s name and description lines', async () => { - const base = await fixture('codex'), installed = join(base.dir, 'plugins/cache/open-pstack/pstack/1.16.0'), f = { ...base, location: installed }; - const suffix = 'skills/create-formal-verification-skill/SKILL.md', creator = await readFile(join(location, suffix), 'utf8'); - await mkdir(join(installed, 'skills/create-formal-verification-skill'), { recursive: true }); - await writeFile(join(installed, suffix), creator); - const c = recipe('setup', 'codex').find(c => c.id === 'accept-formal-offer')!; - const rollout = JSON.stringify({ type: 'response_item', payload: { type: 'message', role: 'user', content: [{ type: 'input_text', - text: `\npstack:setup-pstack\n${installed}/skills/setup-pstack/SKILL.md\n---\nname: setup-pstack\n---\n` }] } }); - const read = (cat: string, output = creator, exitCode = 0) => ({ type: 'item.completed', item: { id: 'item_21', type: 'command_execution', - command: `/bin/zsh -lc '${cat}'`, aggregated_output: output, exit_code: exitCode, status: exitCode ? 'failed' : 'completed' } }); - const done = { type: 'item.completed', item: { id: 'item_22', type: 'agent_message', text: 'ACCEPT-ROUTED' } }; - const session = (...events: object[]) => parseSession('codex', events.map(e => JSON.stringify(e)).join('\n'), 0, 0, rollout); - const relative = `cat ../../.codex/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`, numbered = creator.split('\n').map((line, i) => `${String(i + 1).padStart(6)}\t${line}`).join('\n'); - for (const event of [read(relative), read(`cat $CODEX_HOME/plugins/cache/open-pstack/pstack/1.16.0/${suffix}`), - read(`cat "\${CODEX_HOME}/plugins/cache/open-pstack/pstack/1.16.0/${suffix}"`), read(`cat -n ${join(installed, suffix)}`, numbered)]) { - expect(session(event, done).skills).toEqual(['pstack:setup-pstack']); - expect((await c.assert(session(event, done), f)).assertions).toEqual(['skill-loaded', 'routed:create-formal-verification-skill', 'ended:ACCEPT-ROUTED']); - } - const nameOnly = creator.split('\n').filter(line => !line.startsWith('description: ')).join('\n'); - const other = await readFile(join(location, 'skills/setup-pstack/SKILL.md'), 'utf8'); - for (const events of [[read(relative, creator, 1), done], [read(relative, nameOnly), done], [read('cat skills/setup-pstack/SKILL.md', other), done], [done]]) { - await expect(c.assert(session(...events), f)).rejects.toThrow('skill-not-routed:create-formal-verification-skill'); - } -}); - const FAKE_CODEX = `#!/bin/sh if [ "$1" = "login" ]; then echo 'Logged in using ChatGPT'; exit 0; fi cat > /dev/null diff --git a/.claude/skills/verify-open-pstack/scripts/harness.test.ts b/.claude/skills/verify-open-pstack/scripts/harness.test.ts index 5eaad1b8..f6a4adb6 100644 --- a/.claude/skills/verify-open-pstack/scripts/harness.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/harness.test.ts @@ -336,28 +336,12 @@ describe('headless recipes', () => { { type: 'item.completed', item: { id: 'item_3', type: 'agent_message', text: 'I ran it.' } }, ].map(event => JSON.stringify(event)).join('\n'); const record = parseSession('codex', stream, 0, 0); - expect(record.reply).toBe('I ran it.'); expect(record.commands).toEqual(['true']); expect(record.tools).toEqual([ { name: 'command', id: 'item_1', input: { command: 'true' }, result: 'out\n', parent: null, failed: false }, { name: 'command', id: 'item_2', input: { command: 'false' }, result: '', parent: null, failed: true }, ]); }); - test('each harness keeps the final assistant text as the reply, or empty text when there is none', () => { - expect(parseSession('claude', lines([ - { type: 'result', subtype: 'success', is_error: false, result: 'Early.' }, - { type: 'assistant', message: { content: [{ type: 'text', text: 'Not the result.' }] } }, - { type: 'result', subtype: 'success', is_error: false, result: 'SETUP-DONE' }, - ]), 0, 0).reply).toBe('SETUP-DONE'); - expect(parseSession('claude', lines([{ type: 'assistant', message: { content: [{ type: 'text', text: 'No result.' }] } }]), 0, 0).reply).toBe(''); - expect(parseSession('codex', lines([ - { type: 'item.completed', item: { id: 'item_0', type: 'agent_message', text: 'First.' } }, - { type: 'item.completed', item: { id: 'item_1', type: 'agent_message', text: 'ACCEPT-ROUTED' } }, - { type: 'item.completed', item: { id: 'item_2', type: 'command_execution', command: 'true', aggregated_output: '', exit_code: 0 } }, - { type: 'item.started', item: { id: 'item_3', type: 'agent_message', text: 'Unfinished.' } }, - ]), 0, 0).reply).toBe('ACCEPT-ROUTED'); - expect(parseSession('codex', lines([{ type: 'item.completed', item: { id: 'item_0', type: 'command_execution', command: 'true', exit_code: 0 } }]), 0, 0).reply).toBe(''); - }); test('missing or unsupported recipes fail before any session starts', async () => { const { root, installation } = await candidate('codex'); for (const [feature, reason] of [['mystery', 'missing-recipe:codex/mystery'], ['assets:codex', 'unsupported-native-consumer']]) { diff --git a/.claude/skills/verify-open-pstack/scripts/harness.ts b/.claude/skills/verify-open-pstack/scripts/harness.ts index b6ea2453..537206e4 100644 --- a/.claude/skills/verify-open-pstack/scripts/harness.ts +++ b/.claude/skills/verify-open-pstack/scripts/harness.ts @@ -39,8 +39,7 @@ export function parseSession(harness: Harness, text: string, exitCode: number, s .flatMap(e => [...(e.message.content as string).matchAll(/\/([^<\s]+)<\/command-name>/g)].map(m => m[1]!)); const context = stream.filter(e => e.type === 'system' && e.subtype === 'hook_response' && e.hook_event === 'SessionStart' && e.exit_code === 0 && e.outcome === 'success' && typeof e.stdout === 'string').map(e => e.stdout as string); - const result = stream.findLast(e => e.type === 'result')?.result; - return { harness, exitCode, started, context, reply: typeof result === 'string' ? result : '', + return { harness, exitCode, started, context, skills: [...commands, ...uses.filter(u => u.name === 'Skill' && typeof u.input?.skill === 'string').map(u => u.input.skill as string)], commands: uses.filter(u => u.name === 'Bash' && typeof u.input?.command === 'string').map(u => u.input.command as string), tools: stream.filter(e => e.type === 'assistant' && Array.isArray(e.message?.content)).flatMap(e => (e.message.content as Event[]).filter(b => b.type === 'tool_use') @@ -59,8 +58,7 @@ export function parseSession(harness: Harness, text: string, exitCode: number, s .map(([, name, path]) => path!.includes('/plugins/cache/open-pstack/pstack/') ? name! : path!); const tools = items.filter(i => i.type === 'command_execution' && typeof i.command === 'string').map(i => ({ name: 'command', id: String(i.id), input: { command: i.command as string }, result: typeof i.aggregated_output === 'string' ? i.aggregated_output : undefined, parent: null, failed: i.exit_code !== 0 })); - const reply = items.findLast(i => i.type === 'agent_message')?.text; - return { harness, exitCode, started, skills, commands, tools, context, reply: typeof reply === 'string' ? reply : '' }; + return { harness, exitCode, started, skills, commands, tools, context }; } export async function codexInstallation(output: string, home: string, expected: string): Promise { const result = JSON.parse(output); diff --git a/.claude/skills/verify-open-pstack/scripts/reflect.test.ts b/.claude/skills/verify-open-pstack/scripts/reflect.test.ts index 757c1c5c..57713e50 100644 --- a/.claude/skills/verify-open-pstack/scripts/reflect.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/reflect.test.ts @@ -52,7 +52,7 @@ async function simulatedRecord(f: Fixture, available: boolean): Promise { diff --git a/.claude/skills/verify-open-pstack/scripts/runner.test.ts b/.claude/skills/verify-open-pstack/scripts/runner.test.ts index e15d7959..deb6cb5e 100644 --- a/.claude/skills/verify-open-pstack/scripts/runner.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/runner.test.ts @@ -37,7 +37,7 @@ test('the runner recipe adds one linked-worktree writer case for a Codex parent const writer = recipe('runner', 'codex')[1]!; await writer.prepare!(f); const record: SessionRecord = { harness: 'codex', exitCode: 0, started: Date.now() - 1000, skills: ['pstack:poteto-mode'], tools: [], - commands: [await launch(f, writer.prompt(f))], context: [], reply: '' }; + commands: [await launch(f, writer.prompt(f))], context: [] }; expect((await writer.assert(record, f)).assertions).toEqual(['runner-ran', 'receipt-complete', 'shared-git-denied', 'file:WRITTEN.md']); diff --git a/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts b/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts index a7966594..8a187ffb 100644 --- a/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/skill-invocation.test.ts @@ -15,7 +15,7 @@ async function waitingSession(harness: Harness): Promise<{ f: Fixture; c: Case; const f = { harness, dir, workspace: dir, location: dir, configHome: dir, run: command }; const c = recipe(`skill-invocation:${skill}`, harness)[0]!; await c.prepare!(f); - const record = { harness, exitCode: 0, started: Date.now() - 1000, skills: [`pstack:${skill}`], commands: [], tools: [], context: [], reply: '' }; + const record = { harness, exitCode: 0, started: Date.now() - 1000, skills: [`pstack:${skill}`], commands: [], tools: [], context: [] }; await writeFile(join(dir, 'result.md'), 'Waiting for you to approve inspection. I did not inspect anything.'); return { f, c, record }; } diff --git a/.claude/skills/verify-open-pstack/scripts/types.ts b/.claude/skills/verify-open-pstack/scripts/types.ts index 33f96d76..28278857 100644 --- a/.claude/skills/verify-open-pstack/scripts/types.ts +++ b/.claude/skills/verify-open-pstack/scripts/types.ts @@ -52,7 +52,6 @@ export interface SessionRecord { commands: string[]; tools: { name: string; id: string; input: Record; parent: string | null; result?: string; failed: boolean }[]; context: string[]; - reply: string; } export interface Driver { preflight(receipt: Receipt): Promise; diff --git a/.claude/skills/verify-open-pstack/scripts/verify.test.ts b/.claude/skills/verify-open-pstack/scripts/verify.test.ts index e5a4e013..ecf07c36 100644 --- a/.claude/skills/verify-open-pstack/scripts/verify.test.ts +++ b/.claude/skills/verify-open-pstack/scripts/verify.test.ts @@ -233,7 +233,7 @@ describe('exact-head evidence publication', () => { test('more than the session limit is refused before preflight unless --wide gives a reason', async () => { const limited = (...extra: string[]) => { const f = fixture(true); f.options.github.files = async () => [{ filename: 'plugins/pstack/skills/poteto-mode/references/codex-tools.md' }]; - f.options.features = ['claude:setup', 'claude:runner', ...extra]; + f.options.features = ['claude:setup', 'claude:runner', 'claude:hook:startup', ...extra]; return f; }; expect(SESSION_LIMIT).toBe(12); diff --git a/CHANGES.md b/CHANGES.md index cff7f79a..c9d9a4da 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -23,7 +23,7 @@ Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff **Comments sweep (#218).** Code this repository owns drops comments outside the keep-list in `AGENTS.md`, across the runner, the Codex transcript resolver, the startup hook, the verifier, tests and repository config. A test keeps every model pair released by 1.15.0 in place. -**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills. Setup cases decline both offers, except two: `keep-setting` supplies no answers and checks a quiet rerun, and `accept-formal-offer` declines `/create-verification-skill`, accepts any other offer, and checks that setup hands off to `create-formal-verification-skill`. `first-run` asserts that no project skill directory appears. +**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills. **Not applied.** See `UPSTREAM.md`: upstream's generated Claude Code tree, its adapter, generator, plugin validator and root marketplace entry, the docs-vs-tree check, the two `poteto-help` harness paragraphs, `make-bot-ui`, and the 0.15.26 to 0.15.29 manifests and guide. Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install one of the two, because both use the `pstack:` prefix. `README-UPSTREAM.md` is the verbatim upstream README.