amadan
specs rev 3: answer Astra round 2 (run state on the record, seed identity, import journal, fenced rollback)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
3 files changed,
+384
−111
docs/superpowers/specs/2026-10-08-carlos-run-design.md+104 −40docs/superpowers/specs/2026-10-08-seeded-instances-design.md+219 −71docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R2.md+61 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-10-08-carlos-run-design.md b/docs/superpowers/specs/2026-10-08-carlos-run-design.md| index 65a5eb76f..229c7d7c3 100644 |
| --- a/docs/superpowers/specs/2026-10-08-carlos-run-design.md |
| +++ b/docs/superpowers/specs/2026-10-08-carlos-run-design.md |
| @@ -1,6 +1,6 @@ |
| # `carlos run`: a member runs an app command against one instance (#259) |
| -**Status:** rev 2, 2026-10-08. Rev 1 (c66792a3) was approved by Paul. |
| +**Status:** rev 3, 2026-10-08. Rev 3 answers round 2 (§12). Rev 1 (c66792a3) was approved by Paul. |
| Rev 2 answers Astra's round 1 (`CODEX-FINDINGS-RUN-AND-SEEDED-R1.md`; |
| findings 1 to 7 are this spec's). Each change is marked **(codex N)**, and |
| §11 lists the dispositions. |
| @@ -151,24 +151,57 @@ The console refuses, in this order, each with its own status and message: |
| - a timeout outside 1 second to 6 hours; |
| - files over the cap, or a file name that isn't a plain base name. |
| +9. The instance is an import that isn't committed yet (seeded spec §5.4): |
| + 409, "finish or abort the import first" (codex R2-2). |
| + |
| If none apply, it writes these under the app's own subtree |
| (`release.AppPrefix`, so the owner gate maps onto them and app trash and |
| purge sweep them): |
| - `runs/<id>/in/<name>` for each file; |
| -- `runs/<id>/request.json`: host, argv, timeout, the file list with sizes |
| - and sha256, the caller, and the time requested; |
| -- `runs/index.json`: the app's open runs (id, host, state, cancel flag), |
| - updated by a conditional PUT on its ETag. |
| +- `runs/<id>/request.json`: host, the record's incarnation |
| + (`hostops.Record.Incarnation`: account, app, host and `CreatedAt`), argv, |
| + timeout, the file list with sizes and sha256, the caller, and the time |
| + requested. |
| + |
| +Then it writes the run onto the **instance record** itself, in one CAS on |
| +the record's ETag (codex 1, R2-6): |
| + |
| +```go |
| +ActiveRun *RunState `json:"run,omitempty"` |
| + |
| +type RunState struct { |
| + ID string `json:"id"` |
| + State string `json:"state"` // queued | picked | cancel | done | cancelled | expired |
| + Box string `json:"box,omitempty"` |
| + BootID string `json:"boot,omitempty"` |
| + Deadline time.Time `json:"deadline"` // pickup deadline, then run deadline |
| +} |
| +``` |
| + |
| +Ordinary record writers carry `ActiveRun` through unchanged, the way they |
| +carry `Maintenance` today (`provision.go:40-42`). |
| It then bumps `control/serial`, writes the `run-start` audit row (§6), and |
| answers `202` with the run id. |
| -**Run and move are serialized at the console.** A move request for a host |
| -with an open run in `runs/index.json` is refused (409, naming the run). A |
| -run request for a moving host is refused (step 6). Both checks read the |
| -record and the index at their current ETags, and the write that wins |
| -carries the ETag it read. |
| +**One record, one CAS.** Runs, moves and imports all change the same |
| +object, so they serialize on the record's ETag: |
| + |
| +- a run is admitted only when there is no non-terminal `ActiveRun`, no |
| + move in flight, and no uncommitted import; |
| +- a move request (`provision.go:1129`) is refused while `ActiveRun` is |
| + non-terminal; |
| +- an import's abort is refused while `ActiveRun` is non-terminal, although |
| + run admission already refuses uncommitted imports. |
| + |
| +Whichever write lands first wins. The loser's CAS fails, it re-reads the |
| +record, and it refuses. |
| + |
| +Deleting and recreating the host makes a new record with no `ActiveRun`, |
| +so an old request can never run against the replacement. The box also |
| +checks that `request.json`'s incarnation matches the record before it |
| +launches (codex 3). |
| ### 5.2 Pickup on the box (codex 3) |
| @@ -177,24 +210,32 @@ an object and never acts on it (`:114`, `:165`). That's right for restart |
| and wrong here: it would drop runs queued before a box started, or before |
| it came to own a host. So pickup works like this instead: |
| -- **When the box looks.** A box reads `runs/index.json` for each app it |
| - hosts at agent start, whenever it newly owns a host's exec row, and |
| - whenever the serial moves and the index's ETag differs from the last one |
| - it read. An idle box still pays nothing beyond its serial GET. |
| -- **Which runs it takes.** It acts on every open run for a host whose exec |
| - row it owns. Every other box ignores the run. |
| -- **Taking a run.** The box writes `runs/<id>/picked.json` (box, agent boot |
| - id, time) as a **create-only** PUT (`release.Store.Put` with the |
| - create-only precondition, `store.go:767-777`). If the create fails, some |
| - box already took the run, and this one leaves it alone. |
| -- **A run this box picked but never finished.** At agent start, the box |
| - checks each open run whose `picked.json` names this box with an earlier |
| - boot id. That run's unit is gone: `BindsTo=carlos-edge.service` stopped |
| - it with the edge. The box writes its `result.json` as |
| - `interrupted: "agent restart"`. **A picked run is never executed |
| - again.** |
| -- **No pickup.** The console reports "not picked up" if `picked.json` is |
| - still missing 60 seconds after the request. |
| +- **When the box looks.** Reconcile already reads the instance records in |
| + its scope on every serial bump and at agent start, so the box reads |
| + `ActiveRun` from those same reads. A record the box has just come to own |
| + is covered by the same pass, and an idle box pays nothing extra. |
| +- **Which runs it takes.** It acts on a `queued` run only for a host whose |
| + exec row it owns. Every other box ignores it. |
| +- **Taking a run.** The box moves the run from `queued` to `picked`, with |
| + its box name, agent boot id and the run's deadline, in one CAS on the |
| + record. |
| + - If the CAS fails, the box re-reads. If the run is no longer `queued` |
| + (taken, cancelled or expired), the box leaves it alone. |
| + - Only the box whose CAS succeeded launches, and it checks the deadline |
| + and cancel state again right before launch. |
| +- **A run this box picked but never finished.** At agent start, a run |
| + marked `picked` by this box under an earlier boot id has lost its unit: |
| + `BindsTo=carlos-edge.service` stopped it with the edge. The box writes |
| + its `result.json` as `interrupted: "agent restart"` and CASes the run to |
| + `done`. **A picked run is never executed again.** |
| +- **No pickup** (codex R2-6). Sixty seconds after the request, the CLI asks |
| + the console to expire the run. The console CASes it from `queued` to |
| + `expired`, which is terminal. |
| + - If that CAS succeeds, the CLI reports "not picked up" and exits 3. An |
| + expired run can never be picked, so a box that turns up late can't |
| + run it. |
| + - If the CAS fails because a box picked the run in the meantime, the CLI |
| + goes on following it. |
| Once the box has taken the run: |
| @@ -332,13 +373,17 @@ CLI exits with: |
| When you press Ctrl-C: |
| 1. The CLI sends `POST …/runs/{id}/cancel`. |
| -2. The console sets `cancel` on the run in `runs/index.json` and bumps the |
| - serial. |
| -3. The owning box stops the unit. |
| +2. The console changes the run on the record by CAS: |
| + - `queued` becomes `cancelled`, which is terminal, so no box ever |
| + launches it (codex R2-6); |
| + - `picked` becomes `cancel`, and the console bumps the serial. |
| +3. On `cancel`, the owning box stops the unit. If it hasn't launched yet, |
| + it doesn't launch at all. |
| A second Ctrl-C exits the CLI without waiting; the cancel still happens. |
| At the run's timeout the agent stops the unit itself. All of these end in |
| -an ordinary `result.json`. |
| +an ordinary `result.json`. Once the box has written `result.json`, it CASes |
| +the run to `done`. |
| If the CLI goes away without cancelling, the run carries on to its end or |
| its timeout. `carlos run --follow <id>` attaches to an open or finished run |
| @@ -346,13 +391,18 @@ and prints every chunk not yet acknowledged. |
| ### 5.8 Cleanup |
| -- **The ack.** After a valid ack (§5.6) the console deletes `runs/<id>/` |
| - and drops the run from the index. |
| +- **The ack.** After a valid ack (§5.6), the console deletes `runs/<id>/` |
| + and clears `ActiveRun` from the record by CAS, but only if the record |
| + still names this run in a terminal state. |
| - **The console sweep.** It runs in the existing deadline-sweep loop and: |
| - deletes any run whose result is more than 24 hours old, whether or not |
| it was acknowledged; |
| - - closes any run with no result once its timeout has passed by an hour, |
| - writing the audit row's end as `lost`. |
| + - deals with any run still `picked` or `cancel` an hour past its |
| + deadline: it marks the run `done` with the audit end `lost`, and |
| + clears it. |
| + |
| + A run left in a terminal state is cleared the same way, so the next run |
| + is never blocked by one nobody acknowledged. |
| The 24-hour bucket lifecycle rule from chat is replaced by this sweep. |
| The runs live under each app's subtree, which a prefix rule can't match, |
| @@ -385,7 +435,7 @@ says to pass secrets through `--file`. |
| only executes the build the instance follows. |
| - **Box-written objects can be forged.** Any box can write anywhere in the |
| deployment bucket today (#171), so a compromised box could forge another |
| - box's `picked.json`, output or result. That is the existing |
| + box's run state, output or result. That is the existing |
| record-authority boundary, not a new one, and `run` adds no path from a |
| forged object to any action. |
| - **File names** are plain base names, checked at the console and again by |
| @@ -416,14 +466,19 @@ into the code. |
| - each refusal in §5.1, in order; |
| - the member-only rule; |
| - the audit rows; |
| - - the index CAS under two concurrent requests; |
| + - the record CAS under two concurrent run requests; |
| - the run/move serialization in both directions; |
| - cancel, ack (including a wrong `last_seq`) and the sweep. |
| - **Pickup:** |
| - only the owning box acts; |
| - a run queued before agent start is picked up; |
| - a run queued before the box owned the host is picked up; |
| - - the create-only `picked.json` with two boxes racing; |
| + - the pickup CAS with two boxes racing; |
| + - expiry winning over a late box, and a late pickup winning over expiry; |
| + - cancel before pickup never launching; |
| + - a request whose incarnation doesn't match the record being refused; |
| + - run, move and import abort racing on the record's ETag; |
| + - an uncommitted import refused at admission and again at launch; |
| - a run picked before an agent restart ends `interrupted` and is never |
| run again. |
| - **Writer lifecycle:** |
| @@ -471,8 +526,17 @@ switch. Tito's boxes need the nested layout before Doc and Vicky can use it |
| |---|---| |
| | codex 1 (P1) the hold misses stop paths | **Accepted.** §5.3: the run joins the instance's writer lifecycle, and every stop settles cmd before replication closes; run and move are serialized at the console (§5.1) | |
| | codex 2 (P2) claim-armed launch is missing | **Accepted.** §3.1: refused while claim control is armed; the work moves to #250 | |
| -| codex 3 (P2) the ETag pattern drops or replays runs | **Accepted.** §5.2: scan at start and on ownership; create-only `picked.json`; a picked run is never run again | |
| +| codex 3 (P2) the ETag pattern drops or replays runs | **Accepted.** §5.2: pickup from reconcile's record reads (at start and on ownership); a CAS from queued to picked; a picked run is never run again | |
| | codex 4 (P2) oneshot success never becomes inactive | **Accepted.** §5.4: completion is the invocation's main process exiting; the agent records the result, then stops and settles the unit | |
| | codex 5 (P2) ack can delete unread output | **Accepted.** §5.5 and §5.6: the result comes after the last chunk and names `last_seq`; the ack must match | |
| | codex 6 (P2) the long-host path | **Accepted.** §5.2 step 3: `provision.InstanceDir` | |
| | codex 7 (P3) `CARLOS_REGION` | **Accepted.** §4: `cmdVars` | |
| + |
| +## 12. Round 2 dispositions |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| R1-1, still open: run and move don't share a reservation | **Accepted.** §5.1: the run state lives on the instance record, so run, move and import abort all CAS the same ETag | |
| +| R1-3, still open: no incarnation | **Accepted.** §5.1: the request carries the record's incarnation, and recreating the host drops `ActiveRun` | |
| +| R2-2 (P1) run gets past the import gate | **Accepted.** §5.1 step 9: refused while an import is uncommitted, checked under the record CAS and again at launch | |
| +| R2-6 (P2) "not picked up" leaves a runnable request | **Accepted.** §5.2 and §5.7: queued, picked, cancel, done, cancelled and expired, all moved by CAS on the record; expired and cancelled are terminal before launch | |
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 6790974c3..0f646a63a 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 2, 2026-10-08. Paul approved rev 1 (c66792a3). Rev 2 |
| +**Status:** rev 3, 2026-10-08. Rev 3 answers round 2 (§12). 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. |
| @@ -67,10 +67,15 @@ bucket, beside the `instances/` and `moves/` prefixes. |
| it may write (`resolveReplica`'s residency rule, `apidb.go:54-71`). So |
| both doors refuse a record homed anywhere else, with the existing |
| `ErrResidency` message. |
| -- A bucket lifecycle rule on the `seeds/` prefix expires objects after 7 |
| - days, as a backstop against an import that is abandoned and never |
| - aborted. `seeds/` is a top-level prefix of the data bucket, so a prefix |
| - rule matches it. This is a change in both infrastructure repos. |
| +- **There is no lifecycle rule on `seeds/`** (codex R2-5). A `--from` |
| + instance that nobody wakes for a week still needs its snapshot. Instead, |
| + the console's deadline sweep deletes `seeds/<host>/` only in three |
| + cases: |
| + - no record names it; |
| + - the record's seed is `placed` or `committed` and has another ID; |
| + - it belongs to an import stuck in `awaiting-upload` or `uploaded` for |
| + more than 7 days, which the sweep aborts first (§5.6), a terminal |
| + transition. |
| ### 3.2 The record |
| @@ -80,6 +85,7 @@ bucket, beside the `instances/` and `moves/` prefixes. |
| Seed *SeedSource `json:"seed,omitempty"` |
| type SeedSource struct { |
| + ID string `json:"id"` // random, minted with the seed; never reused |
| Kind string `json:"kind"` // "replica" | "import" |
| From string `json:"from,omitempty"` // replica: the source host |
| TXID string `json:"txid,omitempty"` // replica: the TXID actually restored |
| @@ -107,12 +113,13 @@ An import can also leave the path: |
| - `refused`: the box would not swap; `Reason` says why. |
| - `aborted`, and then the record is deleted. |
| -**What reconcile does with each state** (codex 13). It dispatches on the |
| -seed state **before** any other per-record handling: |
| +**What reconcile does with each state** (codex 13). It reads the import |
| +journal first (§5.7). Then it dispatches on the seed state **before** any |
| +other per-record handling: |
| | State | Reconcile | |
| |---|---| |
| -| `aborted` | runs the idempotent rollback (§5.6) | |
| +| `aborted` | runs the idempotent rollback (§5.6), or with no journal row deletes `seeds/<host>/` and the record | |
| | `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` | |
| @@ -154,16 +161,26 @@ applies only to a row whose record seed is `ready`, `swapped` or `placed`: |
| 1. **Is there already data?** |
| - If the host has any replica of its own, it has been placed already. |
| Restore normally, and ignore the seed. |
| - - If there's a local database, it is the placed seed from an |
| - interrupted first wake, because placement (step 3) is an atomic |
| - rename and nothing else writes that path for a seeded row. Use it, and |
| - go to step 4. |
| + - A local database counts only with **installation evidence** (codex |
| + R2-1). Step 3 writes `<db>.seed`, which names the seed's `ID`, next to |
| + the database. If the local file's marker names the record's current |
| + seed `ID`, it is this seed, placed by an interrupted first wake: use |
| + it, and go to step 4. |
| + - Anything else is purged before step 2, through `instancefs`: |
| + - a local database with no marker, or with a marker naming another ID; |
| + - its `-wal` and `-shm` files; |
| + - litestream's local metadata. |
| + |
| + So a database left behind by an earlier, aborted import of the same |
| + host can never stand in for a new one. |
| 2. **Fetch and check.** Read `seeds/<host>/snapshot.db` into a temp file |
| inside the instance's directory. Check its length and sha256 against |
| the record, then run `lease.CheckDBContext` (integrity, and at least one |
| table). |
| -3. **Place it.** Rename the temp file onto the row's database path through |
| - `instancefs`, owned by the instance, in the nested tree. |
| +3. **Place it.** Write `<db>.seed` naming the seed `ID`, then rename the |
| + temp file onto the row's database path. Both go through `instancefs`, |
| + owned by the instance, in the nested tree. The marker is written first, |
| + so a database at that path always has its marker. |
| 4. **Replicate.** Start replication. The first upload is generation one of |
| the host's own lineage. Nothing of the source's lineage is copied. |
| 5. **Advance the state.** After the first upload succeeds, set the seed to |
| @@ -188,7 +205,7 @@ the placed local file or the snapshot. |
| ## 4. `--from`: a copy of a sibling (#260) |
| ``` |
| -carlos instances create --app <app> --host <new> --from <host> [--at <txid|time>] [--environment <env>] [--channel <c>] |
| +carlos instances create --app <app> --host <new> --from <host> [--at <txid>] [--environment <env>] [--channel <c>] |
| ``` |
| **The gate (codex 17).** The door authorizes through `cliRoute` with the |
| @@ -212,22 +229,40 @@ Both doors call it. |
| 2. Resolve the source with `resolveDBSource`. |
| 3. Refuse a source and target of different apps or accounts (409). |
| Customer data never leaves its account by this door. |
| -4. **Plan the restore (codex 18).** `RestoreTo` gains a target, its zero |
| - value meaning "latest". Litestream's restore options already carry |
| - `TXID` and `Timestamp` (litestream v0.5.14 `db.go:2823-2828`); the |
| - wrapper passes them through, and returns the TXID actually restored. |
| - An `--at` older than the replica's retained history is refused with |
| - "history before <txid/time> is no longer kept". |
| -5. **Admit the restore (codex 19).** Before downloading anything: |
| - - sum the planned LTX files' sizes from the listing (the plan already |
| - has them); |
| - - refuse with 413 if the sum is over 4 GiB; |
| - - refuse with 507 unless the console's scratch filesystem has free space |
| - of at least twice that sum plus 1 GiB. |
| - |
| - Restores are limited to one at a time per app (a semaphore) and two |
| - across the deployment; more than that is refused with 429. The restore |
| - runs under a 30-minute deadline. |
| +4. **Plan the restore (codex 18).** `RestoreTo` gains a target TXID, its |
| + zero value meaning "latest", and passes it through to litestream's |
| + `RestoreOptions.TXID` (litestream v0.5.14 `db.go:2823-2824`). It returns |
| + the TXID actually restored. An `--at` older than the replica's retained |
| + history is refused with "history before <txid> is no longer kept". |
| + |
| + **`--at <time>` is left out of this version** (codex R2-18). A |
| + timestamp restore needs each LTX file's transaction time, and the db |
| + door's client ignores `useMetadata` (`dbdoor/client.go:78`). The console |
| + listing asks for `false` (`apidb.go:273`), so a time would be matched |
| + against S3's modification time instead. Adding times means carrying |
| + metadata through both, which is its own change. |
| +5. **Admit the restore (codex 19, R2-19).** Before downloading anything: |
| + - **Work out the restored size exactly.** Read the header of the last |
| + planned LTX file, with a ranged GET of its first page. Its `Commit` |
| + (the database's page count at that TXID) times its `PageSize` is the |
| + size of the database the restore will produce. The compressed sizes |
| + of the LTX files say nothing about that. |
| + - **Refuse with 413** if the restored size is over 4 GiB. |
| + - **Reserve scratch.** Take the restored size plus the sum of the |
| + planned LTX sizes from the **scratch reservation pool**. |
| + |
| + **The scratch reservation pool.** One in-process counter in the |
| + console, shared by `--from` restores and import spools (§5.2): |
| + - the pool's capacity is the scratch filesystem's free space at console |
| + start, less 1 GiB, re-read whenever the pool is empty; |
| + - a reservation that doesn't fit is refused with 507; |
| + - reservations are released on every exit path. |
| + |
| + Restores and spools are also limited together to one at a time per app |
| + and two across the deployment, with 429 beyond that. A restore runs |
| + under a 30-minute deadline. While it runs, a watcher stats the output |
| + every second and cancels the restore if the file grows past the |
| + restored size it reserved. |
| 6. **Restore and check.** Restore with `RestoreTo` into a private 0700 |
| directory under the console's scratch, `<console data>/scratch/seeds/`. |
| Run `CheckDBContext` under the same deadline. This never reads the live |
| @@ -284,8 +319,9 @@ only its hash. The record is written with seed `awaiting-upload`. |
| ### 5.2 Upload (codex 19, codex 20) |
| `PUT …/instances/{host}/import`, streamed. Before reading the body, the |
| -console checks its scratch filesystem has free space of at least `bytes` |
| -plus 1 GiB; if not, 507. Then: |
| +console reserves `bytes` from the scratch reservation pool (§4 step 5), |
| +under the same per-app and deployment limits. If the reservation is |
| +refused, it answers 507 or 429. Then: |
| 1. It spools the body to `<console data>/scratch/seeds/<host>.db` under |
| `http.MaxBytesReader(bytes)`, hashing as it writes. |
| @@ -312,26 +348,36 @@ is down. The seed becomes `ready`, and the console bumps the serial. |
| Until the swap, the app's own row keeps answering, so the app's router must |
| answer 503 for a stopped instance. |
| -### 5.4 The swap, the gate, and commit (codex 10, 11, 12, 14, 15) |
| +### 5.4 The swap, the gate, and commit (codex 10, 11, 12, 14, 15; R2-3) |
| Reconcile on the box finds a record with seed `ready` and `Replaces` set, |
| and an existing row for the host. Today such a row is left alone ("exists |
| but is not the route this record describes", `reconcile.go:1158`, `:1287`), |
| and that stays the rule for every other case. |
| +**The journal comes first.** Before any of the predicates below, reconcile |
| +checks the box's import journal (§5.7) for the host. A journal row means |
| +this box has already swapped, so the legacy-row predicates are never |
| +applied to a row the box itself replaced (codex R2-3). |
| + |
| This one case swaps instead, in one registry transaction, only if every |
| condition holds. If any fails, the seed becomes `refused` with the |
| condition named. |
| -**The row's shape** (codex 10). Registry kinds are `instance`, `service`, |
| -`static` and `sidecar`, and the backing is a separate set of fields |
| -(`registry.go:31-40`). The row must be: |
| +**The row's shape** (codex 10, R1-10). Registry kinds are `instance`, |
| +`service`, `static` and `sidecar`, and the backing is a separate set of |
| +fields (`registry.go:31-40`). The row must be: |
| - kind `instance` or `service`; |
| -- backed by `Addr` or `Addrs`, with an empty `Socket` and no tunnel; |
| +- backed by `Addr` or `Addrs`, with an empty `Socket`; |
| - without `Provisioned` from any record; |
| - with an addr equal to `Replaces`. |
| +The row must also carry **none** of the columns `shapeMismatch` refuses |
| +adoption over (`reconcile.go:598-610`): `Backing`, `Tunnel`, `Caps`, |
| +`Platform` or `Canary`. These are box-scoped or owned by the domains pass, |
| +and no import takes them over. |
| + |
| **Ownership:** the row's app equals the record's app, and the row's account |
| is either: |
| @@ -344,33 +390,40 @@ is either: |
| `nested = true` explicitly. It doesn't use `NestedPaths(existing)`, which |
| would read the addr row as flat (`reconcile.go:1103-1107`). |
| -In the same transaction, the box (codex 14): |
| +**The swap transaction** (codex 14). In one registry transaction, the box: |
| + |
| +- writes a journal row (§5.7): the host, the seed `ID`, the **complete |
| + original row**, the record key, state `swapped`, and the time; |
| +- replaces the row with the exec row the record describes, filed under |
| + the record's account, with `ImportGate` set to the record's |
| + `VerifyHash`. |
| -- writes the **complete original row** into a new registry table, |
| - `replaced_routes` (host, the row's full JSON, record key, time); |
| -- replaces the row with the exec row the record describes, filed under the |
| - record's account, with `ImportGate` set to the record's `VerifyHash`. |
| +Then it CASes the record's seed from `ready` to `swapped`. |
| -Then it sets the seed to `swapped`. With claims off, which is the only case |
| -built here, there's no claim CAS. So the transaction is the whole swap, and |
| -a crash either leaves the addr row untouched or completes the swap (codex |
| -11). The claim-armed refusal (§3.4) covers the claim case until #250. |
| +**Crashes.** A crash before the transaction leaves the addr row untouched. |
| +A crash after it, but before the record CAS, is resumed on the next pass: |
| +the journal row names this seed `ID` and the record still says `ready`, so |
| +reconcile only redoes the record CAS (codex R2-3). |
| + |
| +With claims off, which is the only case built here, there's no claim CAS. |
| +The claim-armed refusal (§3.4) covers the claim case until #250. |
| **The import gate** (codex 15). While a row has `ImportGate` set: |
| - the edge, and the edge door, answer 503 with `Retry-After: 5` to every |
| request **except** one carrying `Carlos-Import-Verify: <token>`, whose |
| sha256 matches; |
| -- the schedule runner sends no ticks to the row. |
| +- the schedule runner sends no ticks to the row; |
| +- `carlos run` refuses it (run spec §5.1 step 9). |
| -So until commit, the only requests that reach the instance are the app's |
| -own verify requests, and nothing ordinary has been served. The first verify |
| -request wakes the instance, and §3.4 places the snapshot. |
| +So until commit, only the app's own verify requests reach the instance, and |
| +nothing ordinary has been served. The first verify request wakes the |
| +instance, and §3.4 places the snapshot. |
| **Commit.** `POST …/instances/{host}/import/commit` is a record CAS that |
| -moves the seed from `placed` to `committed`. Reconcile then clears |
| -`ImportGate` and deletes the `replaced_routes` row. Commit is refused before |
| -`placed`, because there's nothing verified yet. |
| +moves the seed from `placed` to `committed`. Commit is refused before |
| +`placed`, because nothing has been verified yet. Reconcile then clears |
| +`ImportGate` and deletes the journal row in one transaction. |
| ### 5.5 Verify |
| @@ -378,24 +431,85 @@ moves the seed from `placed` to `committed`. Reconcile then clears |
| Titogo sends its verify path through the edge with the verify header. If it |
| passes, it commits. If it fails, it aborts. |
| -### 5.6 Abort |
| +### 5.6 Abort (R2-4, R2-7) |
| `POST …/instances/{host}/import/abort` is a record CAS from any state |
| -before `committed` to `aborted`. A commit and an abort race on the |
| -record's ETag, and exactly one of them wins. After `committed`, abort is |
| -refused; `carlos instances delete` is the verb then. |
| +before `committed` to `aborted`. It is refused while the record has a |
| +non-terminal `ActiveRun`, although run admission already refuses |
| +uncommitted imports. A commit and an abort race on the record's ETag, and |
| +exactly one wins. After `committed`, abort is refused; `carlos instances |
| +delete` is the verb then. |
| + |
| +**Deleting an uncommitted import is refused** (codex R2-7). |
| +`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>/` 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>/` and the record. |
| + |
| +**Rollback.** Reconcile runs it for any journal row whose import is |
| +abandoned, meaning any of these: |
| + |
| +- the record is `aborted`; |
| +- the record's seed `ID` no longer matches the journal's; |
| +- the record is gone altogether. |
| + |
| +Rollback is driven by the journal, not the record, so it doesn't depend on |
| +the record still existing (codex R2-7). Each step is idempotent, and the |
| +journal's state says where to resume after a restart: |
| + |
| +1. **Close the gate durably.** In one transaction: |
| + - set the journal row to `rolling-back`, with a fence generation; |
| + - set the row's `ImportGate` to a closed sentinel that matches no |
| + token. |
| + |
| + From here on the edge refuses even verify requests, and that survives |
| + an agent restart. |
| +2. **Fence and stop** (codex R2-4). Call |
| + `activator.FenceAndStopIfUnfenced(host, generation)` |
| + (`internal/activator/maintenance.go:45-60`) and require complete stop |
| + evidence (`stopObservation.complete`: lease released, main and sidecar |
| + stopped and exited, replica closed). On `ErrStopUnproven` or |
| + `ErrFenceHeld`, keep the fence and try again on the next pass. After a |
| + restart, a `rolling-back` journal row re-installs the fence before |
| + anything else. |
| +3. **Remove the local data** through `instancefs`: the database, `-wal`, |
| + `-shm`, `<db>.seed` and litestream's local metadata (codex R2-1). |
| +4. **Restore the route.** In one transaction, put the journal's saved row |
| + back exactly as it was, and delete the journal row. |
| +5. **Lift the fence.** |
| +6. **Clean the bucket.** Delete the host's `instances/` replica, if any, |
| + and `seeds/<host>/`. |
| +7. **Delete the record**, by CAS, if it still names this seed `ID`. |
| + |
| +**Why abort loses nothing.** Under the gate, nothing but verify requests |
| +reached the instance, so it holds no writes the old process never saw. |
| +After step 1, not even those reach it. |
| -Reconcile's idempotent rollback for `aborted` is: |
| +### 5.7 The import journal |
| -1. **If the swap happened** (there's a `replaced_routes` row): |
| - - stop the instance; |
| - - in one transaction, put the saved row back exactly as it was, and |
| - delete the `replaced_routes` row. |
| -2. Delete the host's `instances/` replica, if any, and `seeds/<host>/`. |
| -3. Delete the record. The console does this if the box never swapped. |
| +The journal is a box-local registry table, `import_journal`, replacing rev |
| +2's `replaced_routes`. It has one row per host, with these columns: |
| -**Why abort loses nothing.** Under the gate nothing but verify requests |
| -reached the instance, so it holds no writes the old process never saw. |
| +- host; |
| +- seed `ID`; |
| +- the original row as JSON; |
| +- record key; |
| +- state: `swapped` or `rolling-back`; |
| +- fence generation; |
| +- time. |
| + |
| +Reconcile reads it **before** the bucket records, on every pass and at |
| +agent start, and acts on it per §5.4 and §5.6. |
| + |
| +A journal row is deleted only in the same transaction that clears the gate |
| +at commit, or that restores the original row at rollback. So while an |
| +import is in flight, the box always knows what it replaced, whatever has |
| +happened to the record. |
| ## 6. Who may, and what is checked |
| @@ -487,7 +601,9 @@ The swap accepts nothing wider: |
| - not a database; |
| - boxes below the seed floor; |
| - commit before placed; |
| -- abort after commit. |
| +- abort after commit; |
| +- delete of an uncommitted import (abort it instead); |
| +- abort while a run is open. |
| Some come back as the swap's refusal reasons instead: |
| @@ -528,6 +644,9 @@ into the code. |
| - **Box placement:** |
| - each failure (length, hash, `CheckDB`) fails the wake, and never falls |
| back to an empty database; |
| + - a local database whose `<db>.seed` names an earlier seed `ID` (abort, |
| + then re-import) is purged with its WAL, SHM and metadata, and the new |
| + snapshot placed; |
| - a crash after the rename but before the first upload resumes from the |
| local file; |
| - a crash before the rename retries from the snapshot; |
| @@ -538,8 +657,15 @@ into the code. |
| - the operator assignment, present, absent and mapping elsewhere; |
| - nested paths derived for the new row; |
| - the original row stored and restored exactly; |
| + - rows carrying `Backing`, `Tunnel`, `Caps`, `Platform` or `Canary` |
| + refused; |
| - `aborted` dispatched before the state filter; |
| - - an idempotent rollback across a crash between its steps. |
| + - a crash between the swap transaction and the record CAS resumes; |
| + - rollback for a record that is aborted, replaced by another seed `ID`, |
| + or deleted outright; |
| + - the rollback fence: a verify request during rollback is refused, stop |
| + evidence is required, and the fence is re-installed after a restart; |
| + - an idempotent rollback across a crash between any two of its steps. |
| - **The gate:** |
| - the edge and the door answer 503 without the token and pass with it; |
| - no ticks while gated; |
| @@ -548,8 +674,16 @@ into the code. |
| - **Console:** |
| - both doors' gates, including `instance` service credentials and |
| `db pull` still refusing them; |
| - - `--from` with `--at` by TXID and by time, and history no longer kept; |
| - - scratch admission, the semaphore and the deadline; |
| + - `--from` with `--at <txid>`, and history no longer kept; |
| + - 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; |
| + - the watcher cancelling a restore that outgrows its reservation; |
| + - the per-app and deployment limits shared by both; |
| + - delete refused for an uncommitted import, allowed before upload |
| + completes; |
| + - the seeds sweep: deletes only unreferenced or superseded snapshots, |
| + never one a live `--from` record still needs; |
| - scratch cleanup on every exit path and at start; |
| - every import state transition; |
| - hash, length and `CheckDB` refusal; |
| @@ -602,3 +736,17 @@ remaining imports wait for §3.4's claim algorithm. |
| | codex 18 (P2) `RestoreTo` can't honour `--at` | **Accepted.** §4 step 4: a target passed to litestream's TXID/Timestamp options | |
| | codex 19 (P2) scratch isn't bounded | **Accepted.** §4 step 5 and §5.2: admission from the plan's sizes, free-space checks, deadlines, cleanup on every path and at start | |
| | codex 20 (P2) multipart upload | **Accepted, differently.** §5.2: spool to scratch (which `CheckDB` needs anyway), then one `PutFrom` under the 5 GB single-PUT limit; no multipart, no new IAM action | |
| + |
| +## 12. Round 2 dispositions |
| + |
| +| Finding | Disposition | |
| +|---|---| |
| +| R1-10, still open: protected columns | **Accepted.** §5.4: a row with `Backing`, `Tunnel`, `Caps`, `Platform` or `Canary` is refused, as adoption refuses it | |
| +| R1-18, still open: timestamps | **Accepted by scope.** §4 step 4: `--at <txid>` only in this version; carrying LTX times through the db door is its own change | |
| +| R1-19, still open: scratch isn't bounded | **Accepted.** §4 step 5: restored size from the last LTX header's page count and page size; one reservation pool for restores and spools; shared limits; a watcher that cancels on overgrowth | |
| +| R2-1 (P1) re-import resurrects aborted data | **Accepted.** §3.4: a seed `ID` and a `<db>.seed` marker; a local file without a matching marker is purged; rollback removes the database, WAL, SHM, marker and metadata | |
| +| R2-2 (P1) run gets past the import gate | **Accepted.** Run spec §5.1 step 9 and §5.4 here: runs are refused on uncommitted imports, under the record CAS | |
| +| R2-3 (P2) a crash between the swap and the record CAS | **Accepted.** §5.4 and §5.7: the journal is read first, keyed by seed `ID`; a swapped-but-`ready` import resumes with the CAS | |
| +| R2-4 (P2) a verify wake during rollback | **Accepted.** §5.6: the gate is closed durably first, then `FenceAndStopIfUnfenced` with complete stop evidence; the fence is re-installed after a restart | |
| +| R2-5 (P1) the lifecycle rule deletes needed seeds | **Accepted.** §3.1: no lifecycle rule; a console sweep deletes only unreferenced or superseded snapshots, after a terminal abort for stale imports | |
| +| R2-7 (P2) delete bypasses rollback | **Accepted.** §5.6: delete is refused for an uncommitted import; rollback is driven by the journal, including when the record is gone | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R2.md b/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R2.md| new file mode 100644 |
| index 000000000..120641406 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-RUN-AND-SEEDED-R2.md |
| @@ -0,0 +1,61 @@ |
| +| Round-1 finding | Disposition at `999fc5c2` | |
| +|---|---| |
| +| 1. Run hold misses stop paths | **Not fixed.** Run §5.3 addresses stop ordering, but §5.1 still does not serialize run and move admission. Both requests can read “idle,” then successfully update different objects. Moves update the instance record ([provision.go:1129](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/provision.go:1129)); `Put` conditions only the object being written ([store.go:767](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/release/store.go:767)). Both admissions must acquire the same conditional reservation. | |
| +| 2. Claim-enabled execution prerequisite | **Fixed by scope.** Both specs explicitly refuse claim-armed boxes and defer guarded launch integration to #250. | |
| +| 3. Dropped or replayed runs | **Not fixed.** Startup scans and create-only pickup address those cases, but requests still identify only the hostname, without the requested instance incarnation. Delete/recreate before pickup can execute the old request against the replacement. Existing incarnation identity includes `CreatedAt` ([record.go:91](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/hostops/record.go:91)). Bind request, pickup and launch to that identity. | |
| +| 4. Oneshot completion | **Fixed.** Run §5.4 defines invocation-specific completion, result capture, stop and settlement. | |
| +| 5. Ack deletes unread output | **Fixed.** Run §§5.5–5.6 require durable chunks, `last_seq`, complete consumption and a matching ack. | |
| +| 6. Long-host upload paths | **Fixed.** Run §5.2 uses `provision.InstanceDir`. | |
| +| 7. Command region environment | **Fixed.** Run §4 specifies authoritative set/remove behavior in `cmdVars`. | |
| +| 8. Warm-file shortcut versus claim restore | **Fixed by scope.** Seeded §3.4 excludes claim restore from this implementation. | |
| +| 9. Operator row’s destination account | **Fixed.** Seeded §6.4 requires an operator-authored destination-account/app assignment. | |
| +| 10. Invalid addr-route predicate | **Not fixed completely.** The kind/backing vocabulary is corrected, but §5.4 still admits `Backing`, `Caps`, `Platform` and `Canary` rows. Existing adoption explicitly protects these ownership fields ([reconcile.go:598](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/reconcile.go:598)). Preserve those refusals unless an explicit transfer contract covers them. | |
| +| 11. Claim acquisition during swap | **Fixed by scope.** Claim-armed imports are refused; the proposed swap no longer acquires a claim. | |
| +| 12. Flat paths derived from legacy row | **Fixed.** Seeded §5.4 explicitly derives nested replacement paths. | |
| +| 13. Aborted state skipped | **Fixed.** Seeded §3.2 dispatches rollback before the admission filter. | |
| +| 14. Original row cannot be reconstructed | **Fixed.** Seeded §5.4 journals the complete row in the replacement transaction. | |
| +| 15. Unobservable ordinary-traffic condition | **Fixed for HTTP admission.** Seeded §5.4 supplies authenticated verification and a durable commit boundary. A separate command-path interaction appears below. | |
| +| 16. Downgrade consumes seed records | **Fixed.** Seeded §3.3 requires an armed seed floor and rollback-binary verdict before any seed record. | |
| +| 17. Service credentials rejected | **Fixed.** Seeded §4 separates seed authorization from source resolution. | |
| +| 18. Historical restore | **Not fixed for timestamps.** Passing `Timestamp` through is insufficient: `dbdoor.Client.LTXFiles` discards `useMetadata` ([client.go:78](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/dbdoor/client.go:78)), and the console listing requests `false` ([apidb.go:273](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/console/apidb.go:273)). That selects S3 modification time rather than transaction metadata ([replica_client.go:1574](/home/paulca/go/pkg/mod/github.com/benbjohnson/litestream@v0.5.14/s3/replica_client.go:1574)). Preserve transaction timestamps throughout historical planning. | |
| +| 19. Scratch bounds | **Not fixed.** LTX pages are compressed ([encoder.go:255](/home/paulca/go/pkg/mod/github.com/superfly/ltx@v0.5.1/encoder.go:255)); restored output expands to database pages ([decoder.go:235](/home/paulca/go/pkg/mod/github.com/superfly/ltx@v0.5.1/decoder.go:235)). Twice the listed object sizes does not bound scratch or establish the claimed 4-GiB database limit. Concurrent free-space checks also reserve nothing, and imports have no stated concurrency bound. Reserve aggregate scratch, bound decoded output, and include uploads in admission. | |
| +| 20. Multipart support and permissions | **Fixed.** Seeded §5.2 replaces multipart with a bounded, seekable spool and single `PutFrom`. | |
| + |
| +1. **P1 — Seeded §§3.4, 5.6: abort followed by re-import restores the aborted database.** |
| + Import snapshot A, verify it, abort, let the original process advance, then import snapshot B at the same hostname. Abort deletes the remote replica and snapshot but leaves the local database. Stopping deliberately preserves that database ([activator.go:2104](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/activator.go:2104)), and restore accepts an existing local file without restoring anything ([backend_exec.go:611](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/backend_exec.go:611)). Section 3.4 therefore treats A as an interrupted installation of B, ignores B and republishes stale data. |
| + |
| + **Fix:** bind local seed installation to a unique import identity. After proven shutdown, abort must remove that import’s database, WAL/SHM and replication metadata before allowing another import. A warm file without matching installation evidence must not suppress the new snapshot. |
| + |
| +2. **P1 — Run §5.1; seeded §§5.4–5.6: `carlos run` bypasses the import’s abort-safety gate.** |
| + After verification places the snapshot, the imported row satisfies run’s platform-exec, nested and replication conditions. Neither run admission nor pickup checks whether the import is committed. A member can successfully run a database mutation, then another member can abort and delete its replica. The command operates through the activator/control path, rather than an edge request: existing wake starts the process directly ([activator.go:1282](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/activator.go:1282)), and instance control starts its unit directly ([server.go:344](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/instancectl/server.go:344)). An HTTP verification header cannot protect this path. |
| + |
| + **Fix:** refuse runs against uncommitted imports at console admission and again at launch. Serialize this check with import state transitions so a queued run cannot cross an abort or replacement. |
| + |
| +3. **P2 — Seeded §5.4: the registry transaction does not make the complete swap crash-safe.** |
| + Crash after committing `replaced_routes` and the exec row but before setting the bucket record to `swapped`. On restart the record remains `ready`; the prescribed swap predicate encounters a provisioned, socket-backed row and marks it `refused`. The record-state table then skips it indefinitely. Existing reconcile independently reads bucket records and registry rows ([reconcile.go:824](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/reconcile.go:824), [reconcile.go:1062](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/reconcile.go:1062)); a registry transaction cannot include the later bucket write. |
| + |
| + **Fix:** consult a journal bound to the import identity before applying legacy-row predicates. Resume the bucket transition when that import’s replacement already exists. Define recovery when abort wins during this interval, retaining the abort record until local rollback is acknowledged. |
| + |
| +4. **P2 — Seeded §5.6: stopping does not exclude another verification wake during rollback.** |
| + The sequence stops the instance while its verification-enabled exec row remains installed, then restores the original row and deletes the replica. A second request carrying the valid token can wake the instance between stop completion and replacement. Ordinary stop forgets the entry ([activator.go:2373](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/activator.go:2373)); the separate maintenance API exists specifically to close admission before collecting stop evidence ([maintenance.go:45](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/maintenance.go:45)). Without that exclusion, rollback can delete replication state while a new invocation is using it. |
| + |
| + **Fix:** install an import-bound maintenance fence before stopping, reject further verification admission, and require complete stop evidence before replacement or deletion. Keep the fence through cleanup and recover it after restart. |
| + |
| +5. **P1 — Seeded §§3.1, 3.4: seven-day expiration deletes seeds that are still required.** |
| + The lifecycle rule covers every `seeds/<host>/snapshot.db`, including a successful `--from` instance that nobody wakes for seven days. Creation only mints a route ([reconcile.go:1173](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/reconcile.go:1173)); restore happens on wake ([activator.go:1180](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/activator/activator.go:1180)). Such an instance has neither local data nor its own replica when expiration removes its only accepted snapshot. Its first wake must fail permanently. |
| + |
| + **Fix:** retain snapshots while a live record still needs initial placement. Sweep abandoned imports through an explicit terminal transition; expire only objects proved unreferenced or superseded by a durable replica. |
| + |
| +6. **P2 — Run §§5.2, 5.6–5.8: a “not picked up” failure leaves an executable request behind.** |
| + At 60 seconds the CLI exits with code 3, but no state transition closes the request. A box returning at 61 seconds scans open runs and can execute it after the caller received failure. The create-only pickup precondition tests object absence, not request age or cancellation ([store.go:774](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/release/store.go:774)). Cancellation before pickup similarly needs a launch refusal, not merely “stop the unit” when no unit exists. |
| + |
| + **Fix:** define a durable queued/picked/cancelled/expired state machine. Pickup and terminal cancellation must compete on the same conditional state, with the deadline and cancellation checked before launch. A terminal pickup-timeout response must prevent later execution. |
| + |
| +7. **P2 — Seeded §§3.2, 5.6: ordinary instance deletion bypasses import rollback.** |
| + An uncommitted import remains reachable through the ordinary instance-delete endpoint ([authcli.go:683](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/console/authcli.go:683)). In the claims-off implementation, deleting a record is an object deletion ([provision.go:1844](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/provision.go:1844)); reconcile then removes its provisioned route ([reconcile.go:1386](/home/paulca/amadan.net/carlos/platform/.claude/worktrees/run-and-seeded/internal/provision/reconcile.go:1386)). No `aborted` record remains to dispatch restoration of `replaced_routes`, leaving the original route unrestored. |
| + |
| + **Fix:** route deletion of an uncommitted import through the durable abort protocol, or refuse it with the abort operation identified. Recover outstanding replacement journals independently of the continued existence of their instance records. |
| + |
| +`carlos run`: **revise**. |
| + |
| +Seeded instances: **revise**. |
| \ No newline at end of file |