🤖 formal/plan-storage: model and repro gaps from the #5458 review

[ThomasK33]

Follow-ups from the Codex review of #5458 (the plan-storage TLA+ model and repros). Each one refines the model or a repro. None changes the findings #5458 reports.

1. Fork crash between registration and copy (MC_fork_race_fixed). With Crashes = TRUE and forkCopyAfterRegister, a fork can register and then crash before its copy. The fork's row is live without its plan. No invariant checks plan availability, so the fixed twin holds. Track plan presence per live row (or keep registration pending until the copy ends) before certifying the 🤖 fix: the fork plan copy runs before registration, so concurrent forks with one name keep the last copy #5175 fix ordering. Review threads: PRRT_kwDOPxxmWM6oWV5D, PRRT_kwDOPxxmWM6oWV5J.
2. Removal guard and delete are one atomic step (MC_seeded_remove, ClearGuard). deletePlanFilesOfRemovedWorkspace awaits getAllWorkspaceMetadata() and then deletePlanFilesOfMetadata() separately. A create of the same name can register between the two awaits. Split guard and delete into separate sub-steps and add a concurrent-create scenario, for removal and for a candidate clear guard. Review thread: PRRT_kwDOPxxmWM6oWV5R.
3. F6 repro varies the project path as well as the installation (🤖 fix: two Xum installations on one SSH host can share or delete each other's plan files #5174). The two-installations repro gives the other installation a different local project path. A fix that namespaces remote plans by local project path would pass it, although two installations with the same project path still collide. Hold the project path constant, vary only the installation root, and give the other installation another srcBaseDir for a separate checkout. The 🤖 fix: two Xum installations on one SSH host can share or delete each other's plan files #5174 fix PR owns this change. Review thread: PRRT_kwDOPxxmWM6oWV5V.

Refs #5458, #5175, #5174

---

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

[ThomasK33]

Item 2, code side: #5467 does not close this item. It keeps the guard and the delete as two awaits (no lock across them: the config write queue would block every config edit behind a remote rm) and states the residual window in the code and the PR body.

• A row that leaves between the lookup and the delete only keeps a file.
• A row that joins must register the clearing (or removed) workspace's name in the same plan directory while that workspace is still registered. Create and rename refuse that name in their preflight. Fork refuses it under the config write.
• So the window is reachable only by a create or rename whose preflight ran before that workspace registered the name, and whose registration write does not re-check it (🤖 fix: create has no locked re-check of the plan-directory name namespace #5181 and the rename race). Their locked re-checks close it.

The model change this item asks for (split guard and delete, add a concurrent-create scenario) stays open here.

[ThomasK33]

Item 1 (fork crash between registration and copy) is addressed in #5468. The model adds a ForkHasPlan invariant: a fork that registered and finished holds its plan, and only a fork halted between its registration and its copy may have a live row without its plan. MC_fork_race_fixed (Crashes = TRUE) holds, MC_fork_race violates it, and the new mutant MC_mut_fork_skipcopy (a fork that registers and finishes without copying) violates it. The code treats that crash state as "no plan", the same state as a fork of a source that has no plan; the PR body describes it. Items 2 and 3 remain open.

[ThomasK33]

Item 3 (the F6 repro varies the project path as well as the installation) is closed by #5469. The other installation now uses the same local project path and workspace name, another data root (nested withTempMuxRoot) and another srcBaseDir, and its plan path is resolved with its own Config. A mutant that keys the remote plan path by project id alone fails the repro at its target assertion.

[ThomasK33]

Triage by the issue coordinator (workspace workspace-64, lane for the formal batch-4 follow-ups). Classes: A = single-backend defect with a small fix; B = needs two backends, cross-process crash evidence or a mixed-version decision; C = needs a new persisted field or subsystem; D = low priority or trigger-gated; E = already fixed; M = model or repro refinement.

Item	Class	Disposition
1. Fork crash between registration and copy	E	Done by #5468 (ForkHasPlan, MC_mut_fork_skipcopy).
2. Split removal guard and delete, add a concurrent-create scenario	M	Waits for #5469, which also edits formal/plan-storage/check.sh. I will pick it up after #5469 merges.
3. F6 repro varies only the installation	E (pending)	Closed by #5469 when it merges.

---

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

[ThomasK33]

Status from the formal batch-4 lane (workspace-64), which is finishing: item 2 (split the removal guard and delete in the model, add a concurrent-create scenario) is still pending on #5469, which edits formal/plan-storage/check.sh. Item 3 closes when #5469 merges. The issue coordinator will dispatch item 2 after that.

---

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

[ThomasK33]

Picked up by the issue coordinator: workspace workspace-71, branch formal-plan-storage-5462-guard-split

Re-triage after #5611 (merged as 235980f). Classes: A = single-backend defect, small fix, no new persisted field. B = needs two backends, a crash window or mixed versions. C = new persisted field or subsystem. D = low priority. E = already fixed by #5611 (merged as 235980f), with evidence. M = model or repro refinement in formal/plan-storage.

Item	Class	Disposition
1. Fork crash between registration and copy	E	Done by #5468 (ForkHasPlan, MC_mut_fork_skipcopy), as noted above.
2. Split the removal guard and the delete, add a concurrent-create scenario	M	I am doing this now in PlanStorage.tla. Removal becomes three sub-steps in the code's order (sharing guard, delete, deregistration), and the clear guard gets its own sub-step. New scenarios: a create that races a removal, and a create that races a guarded clear. Each has a fixed twin with the create re-check (#5468), plus a mutant that deregisters before it deletes.
3. The F6 repro varies the installation only	E	#5469 was closed unmerged, but #5611 carries the same repro. In workspaceService.planStorageFormalRepro.test.ts the other installation uses the same local project path and workspace name, its own data root (nested withTempMuxRoot) and its own srcBaseDir. Its plan path comes from its own Config. I checked it with a mutant on 235980f: when getInstallationScopedPlanFilePath drops the installation ID (the path keys on the project ID alone), the repro fails at its target assertion (Expected: false, Received: true).

This PR will close the issue, because items 1 and 3 are already done.

---

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