amadan
seeded spec rev 7: answer Astra round 6 (abort tears down the seed's own store before releasing the hostname)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+62
−12
docs/superpowers/specs/2026-10-08-seeded-instances-design.md+47 −12docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R6.md+15 −0
CI cancelled — superseded by a newer push — run details
diff --git a/docs/superpowers/specs/2026-10-08-seeded-instances-design.md b/docs/superpowers/specs/2026-10-08-seeded-instances-design.md| index 1a9b6b0af..cf0699235 100644 |
| --- a/docs/superpowers/specs/2026-10-08-seeded-instances-design.md |
| +++ b/docs/superpowers/specs/2026-10-08-seeded-instances-design.md |
| @@ -1,6 +1,6 @@ |
| # Instances that start from a database: `--from` (#260) and the import door (#261) |
| -**Status:** rev 6, 2026-10-08. Rev 3 answered round 2 (§12), rev 4 round 3 (§13), rev 5 round 4 (§14), and rev 6 round 5 (§15). Paul approved rev 1 (c66792a3). Rev 2 |
| +**Status:** rev 7, 2026-10-08. Rev 3 answered round 2 (§12), rev 4 round 3 (§13), rev 5 round 4 (§14), rev 6 round 5 (§15), and rev 7 round 6 (§16). Paul approved rev 1 (c66792a3). Rev 2 |
| answers Astra's round 1 (`CODEX-FINDINGS-RUN-AND-SEEDED-R1.md`; findings |
| 8 to 20 are this spec's). Each change is marked **(codex N)**, and §11 lists |
| the dispositions. |
| @@ -115,6 +115,9 @@ type SeedSource struct { |
| | `--from` | `reserving` → `ready` → `placed` | |
| | import | `awaiting-upload` → `uploaded` → `ready` → `swapped` → `placed` → `committed` | |
| +Either kind can also be abandoned. Its record then goes `aborted` → |
| +`rolled-back`, and is deleted (§5.6). |
| + |
| An import can also leave the path: |
| - `refused`: the box would not swap; `Reason` says why. |
| @@ -126,7 +129,8 @@ other per-record handling: |
| | State | Reconcile | |
| |---|---| |
| -| `aborted` | runs the idempotent rollback (§5.6), or with no journal row deletes `seeds/<host>/<id>/` and the record | |
| +| `aborted` | runs the idempotent rollback (§5.6), or, with no journal row, deletes `seeds/<host>/<id>/` and CASes the record to `rolled-back` | |
| +| `rolled-back` | skips the record; the console finishes it (§5.6) | |
| | `reserving`, `awaiting-upload`, `uploaded`, `refused` | skips the record; nothing is minted | |
| | `ready` | mints (`--from`) or swaps (import) | |
| | `swapped`, `placed`, `committed` | ordinary handling, plus the import gate (§5.4) while not `committed` | |
| @@ -480,12 +484,29 @@ delete` is the verb then. |
| `DELETE …/instances/{host}` on a record whose seed is an import that isn't |
| `committed` answers 409, "abort the import instead". The only exceptions |
| are `awaiting-upload`, `uploaded` and `refused`, where no box has |
| -swapped, so the console deletes the record and `seeds/<host>/<id>/` itself. |
| - |
| -**The record is kept until the box has rolled back.** An `aborted` record |
| -stays in the bucket until the owning box deletes it at the end of the |
| -rollback below. A box that never swapped (there's no journal row for this |
| -seed `ID`) only deletes `seeds/<host>/<id>/` and the record. |
| +swapped, so the console moves the record straight to `rolled-back`, deletes |
| +`seeds/<host>/<id>/`, and finishes as below. |
| + |
| +**The record is kept until everything is clean.** An `aborted` record |
| +stays in the bucket while the box rolls back. The box then CASes it to |
| +`rolled-back`, never deleting it. A box that never swapped (there's no |
| +journal row for this seed `ID`) deletes `seeds/<host>/<id>/` and does the |
| +same CAS. |
| + |
| +**The console finishes** (codex R6-1). For a `rolled-back` record, the |
| +console's abort handler, or failing that its deadline sweep: |
| + |
| +1. **Tears down the private store this seed created**, if there is one. |
| + The store record for the derived environment is torn down with the |
| + existing `objstore.TeardownIn` (`walk.go:559-566`), but only if its |
| + grant names this seed `ID` (§4 Storage). A store without that `ID` was |
| + there before the seed, and is never touched. |
| +2. **Deletes the record** by CAS, if it still names this seed `ID`. |
| + |
| +The record holds the hostname until the store is gone, so a re-import of |
| +the same host can't meet the leftover store that §4 would refuse. The same |
| +finish runs for a `--from` that fails after creating its store, from its |
| +`aborted` record (§4 step 7). |
| **Rollback.** Reconcile runs it for any journal row whose import is |
| abandoned, meaning any of these: |
| @@ -537,14 +558,15 @@ journal's state says where to resume after a restart: |
| 6. **Clean the bucket.** Delete the host's `instances/` replica, if any, |
| and `seeds/<host>/<id>/` for this seed `ID` only. |
| 7. **Delete the journal row.** |
| -8. **Delete the record**, by CAS, if it still names this seed `ID`. It |
| - goes last (codex R4-1). Until then the aborted record holds the |
| +8. **CAS the record to `rolled-back`**, if it still names this seed `ID`. |
| + The console finishes from there (store teardown, then record delete). |
| + The record goes last of all (codex R4-1, R6-1). Until then it holds the |
| hostname, and `CreateRecord`'s create-only write refuses a new import or |
| `--from` for that host (`provision.go:845`). So no second seed can |
| arrive while this one's cleanup is still running. A crash after step 7 |
| leaves an `aborted` record with no journal row, and §3.2's no-journal |
| - path (delete this seed's snapshot, then the record) finishes the job |
| - idempotently. |
| + path (delete this seed's snapshot, then the CAS) finishes the box's |
| + part idempotently. |
| **After a restart in `cleanup-pending`,** the box resumes at step 6. Its |
| deletes are scoped to this seed `ID`, and the record still holds the |
| @@ -785,6 +807,13 @@ into the code. |
| - on an app with private storage, `--environment` refused and an existing |
| store for the derived environment refused, except a retry of the same |
| seed `ID`; the source's store and bindings unchanged; |
| + - abort and then re-import with private storage on, both before upload |
| + and after the swap. The seed's store is torn down and the re-import |
| + succeeds. A store whose grant names another seed `ID`, or none, is |
| + never torn down. A crash between the teardown and the record delete |
| + resumes; |
| + - a failed `--from` after store provisioning: the store is torn down and |
| + the host can be created again; |
| - restored size from the last LTX header, and the 413; |
| - the shared reservation pool across restores and spools, its 507, and |
| release on every path; |
| @@ -881,3 +910,9 @@ remaining imports wait for §3.4's claim algorithm. |
| | Finding | Disposition | |
| |---|---| |
| | R5-1 (P1) create doesn't guarantee an empty private store | **Accepted.** §4 Storage: with private storage, both seed doors refuse an explicit environment, use the derived one, and refuse an existing store unless it was created by the same seed `ID` | |
| + |
| +## 16. Round 6 dispositions |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| R6-1 (P2) abort leaves a store that blocks re-import | **Accepted.** §5.6: the box ends at `rolled-back`; the console tears down the store only if its grant names this seed `ID`, then deletes the record, which holds the hostname until then. The same applies to a failed `--from` | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R6.md b/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R6.md| new file mode 100644 |
| index 000000000..be5cb346a |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R6.md |
| @@ -0,0 +1,15 @@ |
| +| Round-5 finding | Disposition at `0ef3e715` | |
| +|---|---| |
| +| R5-1 — Creation does not guarantee an empty private store | **Fixed at spec level.** §4 applies the derived-environment rule to both doors, refuses existing stores, and permits reuse only when the grant names the same seed ID. | |
| + |
| +1. **P2 — Seeded §§4, 5.6: abort leaves a private store that blocks re-import.** |
| + |
| + Begin import A for an app with private storage, then abort—even before uploading. Section 5.6 deletes the snapshot and instance record but leaves A’s store. Import B at the same hostname derives the same environment, receives a new seed ID, and is therefore refused by §4. The same problem follows a failed `--from` creation after store provisioning. |
| + |
| + Storage provisioning is a separate operation ([instanceprivatestore.go:250](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/console/instanceprivatestore.go:250)). Deleting the instance record removes only that object ([provision.go:1844](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/provision.go:1844)); removing an environment’s store requires the separate teardown operation ([walk.go:559](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/objstore/walk.go:559)). Thus successful rollback does not restore the ability to retry the conversion. |
| + |
| + **Fix:** assign durable cleanup of seed-created stores to the console’s abort recovery, including failures before swap. Guard cleanup by seed ID and binding ownership, preserve pre-existing stores and bindings, and retain the reservation until cleanup finishes. Test abort followed by re-import with private storage enabled. |
| + |
| +Seeded instances: **revise**. |
| + |
| +`carlos run`: **accept**, carried forward from round 4; not re-reviewed. |
| \ No newline at end of file |