🤖 fix: keep a refused or failed migration pending until its command exits

[ThomasK33]

Summary

When a foreground command's move to the background is refused (a removal or archive has sealed the workspace) or fails (the record cannot be created), the bash tool aborts the command and waits at most 5 s for it to exit. Before this PR, the migration's pending entry ended with that wait, so a command whose kill took effect late ran on untracked, and the removal went on to delete its checkout. Now the pending entry stays until the command's exit actually settles. A removal or archive cleanup keeps waiting for it, and fails closed at its existing 60 s drain deadline instead of deleting the checkout.

Fixes #5522

Builds on #5575 (merged: the #5465 model and repros). This PR turns its two case-1 repros into plain tests.

Implementation

• tools/bash.ts: the migration handle was a using declaration, so it ended with the block. It is now a plain handle, ended by a small using guard unless the failed-migration path hands it to execStream.exitCode. It ends only when that promise resolves, which confirms the exit. A rejection (for example a remote transport error) does not confirm the stop, so the migration then stays pending for the session, and removal and archive of that workspace keep failing closed. The 5 s join and the tool's reply are unchanged.
• No new persisted state. The pending entry is the existing in-memory pendingAdmissions entry that cleanup() already drains (backgroundProcessManager.ts).
• Removal and archive call cleanup(ws, { failClosedAfterDrainTimeout: true }), which throws after 60 s (🤖 Background cleanup: surface failed kills and bound the pending-admission drain #5477). An unconfirmed stop therefore blocks the destructive step, as 🤖 fix: only a supervisor inside the group signals a background process group #5521 requires. Session disposal (no deadline) waits until the command's exit is confirmed. This only delays the disposal's tail steps, as an admitted spawn stuck in a runtime call already does.

Model

formal/background-processes/BgCleanup.tla: MJoinTimeout now moves the migration to "stopping", which MStopped ends only after the command exits. MigrationOwned counts "stopping" as owned. MC_cleanup_refused_join_timeout and MC_cleanup_failed_join_timeout (the forced admitted-then-failed path) now hold (EXPECT ""). A new mutant constant JoinUntracked (the code before this PR) is FALSE in every other config. Its config MC_mut_cleanup_join_untracked still violates NoLiveAfterDelete and MigrationOwned, so the model still sees the defect class.

Validation

• Test-first. On main before this PR (🤖 tests: cover #5465 background-process cases in the TLA+ model #5575), both repros ("a refused migration ..." and "a failed migration ...") fail at their target assertion, expect(early === "finished").toBe(false), with Expected: false, Received: true: the removal's cleanup has already finished while the command is alive. The first version of the plain test, run without the fix, also failed:

  Expected: "waiting"
  Received: "finished"
  (fail) #5465 case 1: ... > a refused migration keeps its command tracked until it exits
  

  With the fix, both pass as plain tests. A third test, "a migration whose exit observation fails stays pending", uses a runtime whose exitCode rejects after the kill. Without the rejection handling it fails (Expected: "waiting", Received: "finished"). Each also releases the held kill and checks that the cleanup then finishes and the PID is gone.

• formal/background-processes/check.sh (full) and FORMAL_FAST=1 exit 0.

• Bun 1.3.12: backgroundProcessesFormalRepro, bash*, backgroundProcessManager, workspaceService.archive and workspaceService.remove tests pass (403 tests). make static-check passes.

Risks

Low. The change only affects the path where a migration was refused or failed, and only lengthens how long cleanup waits for that command. A command that never exits now makes removal or archive fail after 60 s instead of deleting the checkout under it. That is the intended fail-closed behavior.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: high • Cost: $32.91

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-03T20:56:39.088584Z	7ee1ce8	New commits
🔒 Security Review	✅ Completed 2026-10-03T20:59:52.052912Z	7ee1ce8	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 01b34a8ce5

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[ThomasK33]

Review budget status for head 7ee1ce8. The PR is not merged yet.

• CI: all checks pass on this head (29 pass, 4 skipped), including the Formal background-processes job. Unresolved threads: 0. The automatic normal review on this head reacted with a thumbs-up. The security reviews found nothing in 3 rounds.
• Assessments used: 6 (3 normal and 3 security automatic reviews). Normal-review findings per round: 0, 1, 0. The round-2 finding (a rejected exitCode disposed the pending migration) was fixed with a test.
• Findings did not strictly shrink (0 then 1), so the +2 extension does not apply automatically. The final independent check would be the 7th assessment. I am pausing for the coordinator's approval before running it and merging.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: high • Cost: $32.91

[ThomasK33]

Readiness record for head 7ee1ce8:

• CI: all checks pass on this head (29 pass, 4 skipped), including the Formal background-processes job. Unresolved threads: 0.
• Local: check.sh full and FORMAL_FAST=1 exit 0. 403 targeted tests pass on Bun 1.3.12. make static-check passes.
• Review budget: 7 assessments, which are 3 normal and 3 security automatic reviews plus the final check. Normal-review findings per round: 0, 1, 0, and the security reviews found nothing. The coordinator approved the 7th slot for the final check: findings did not strictly shrink, but the one extra finding was a real defect that is now fixed with a test, and the latest round was clean.
• Final independent check (clean context, on exactly this head): "ready with tracked follow-ups". No blocker. Its follow-up is liveness when an exit is never confirmed (session disposal waits forever, and removal keeps failing until restart), tracked in 🤖 bug: a migration whose exit is never confirmed blocks its workspace's teardown until restart #5589. The pre-existing crash-window gap is 🤖 bug: a crash before a background command's child starts leaves a record that refuses workspace removal #5576.
• Decision: ready. Merging with squash, pinned to this head.

---

Generated with xum • Model: anthropic:claude-opus-5-5 • Thinking: high • Cost: $43.48