amadan
spec: host lifecycle claim rev 2, after the joint Astra review
Adopts the review's text for D1-D3, D5-D8 and I-7, its replacement for D4, and answers N1, N3-N10, N12 and R3-12: destructive storage calls name exact object versions; intent journaled before effect with a recovery owner per state; legacy hosts park everywhere; per-retirement manifests without locks; a local host guard; app purge and placement as operations; version-pinned door reads; execution leases and lost-box quarantine; floor on boot recovery. Joint findings copied unedited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+819
−305
docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md+516 −305docs/superpowers/specs/CODEX-FINDINGS-JOINT-R1.md+303 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md| index 86fcf0347..611af3cbb 100644 |
| --- a/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| +++ b/docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md |
| @@ -1,350 +1,561 @@ |
| # The host lifecycle claim |
| -Design, 2026-10-02, rev 1. A small primitive cited by two specs: |
| +Design, 2026-10-02, **rev 2**. A small primitive cited by: |
| - **#199**, deleting an instance and parking its data: |
| `2026-10-02-replica-ownership-design.md`, which this spec supersedes |
| from §2 onward; |
| - **move-any-app**, `design-moves-any-region`: |
| `2026-10-02-move-any-app-design.md`, which owns the move operation's |
| - phases. |
| - |
| -`carlos db push` will be a third operation on it, later. |
| + phases; |
| +- later, `carlos db push`. |
| + |
| +Rev 1 (653ad4b1) went through the joint Astra review with move-any-app |
| +rev 3 (`CODEX-FINDINGS-JOINT-R1.md`, cited `J-…`), and was not ready. |
| +Rev 2 adopts the review's exact text for D1, D2, D3, D5, D6, D7, D8 and |
| +I-7, adopts its replacement for D4, and answers N1, N3 to N10, N12 and the |
| +carried-forward R3-12. The moves-only findings (N2's move side, N11, N13, |
| +N14, N15) are the moves spec's. §12 maps every finding to its section. |
| + |
| +The method changes too. The moves session is building an executable |
| +joint model: a deterministic randomized Go simulation covering every |
| +actor, the real IAM split, late S3 completion, crashes, partitions and old |
| +executables. This spec will be checked against the list of claim changes |
| +the model requires before the next review. Prose rounds alone have stopped |
| +converging. |
| ## 1. Why |
| -Three #199 designs and two move-any-app rounds failed review for the same |
| -reason. Every actor that changes a host's data acts on its own snapshot, |
| -and nothing makes them take turns: |
| +Several actors can change a host's data or admit work on it: |
| -- create; |
| -- delete and its park; |
| -- reconcile's row admission and retirement; |
| -- the move worker's rounds, landing and rollback; |
| +- create and delete; |
| +- reconcile; |
| +- moves; |
| - staging promotion; |
| - wake; |
| -- the `carlos db` pull door. |
| +- background passes (config sync, release adoption, placement); |
| +- app purge; |
| +- the pull door. |
| -The findings asked, again and again, for: |
| +Today none of them serialises with the others. |
| -- exclusive ownership held through a destructive step; |
| -- revalidation under it; |
| -- a durable list of where an incarnation's data lives; |
| -- stop evidence that survives a restart; |
| -- obligations that outlive a crash. |
| +The claim gives each host **one** record of: |
| -This spec gives a host exactly one place where all of that lives. |
| +- who is entitled to it; |
| +- what operation is running on it; |
| +- where its data lives; |
| +- what is still owed. |
| -Requirements come from #199 rev 3's findings (`own/findings3.md`) and the |
| -moves R1 and R2 findings (`CODEX-FINDINGS-MOVES-R1.md`, `-R2.md`). They |
| -are cited as `199-n`, `M1-n` and `M2-n`. |
| +Each of those actors must follow the rules below. |
| ## 2. The object |
| -One object per host, in the control (deployment) bucket: |
| - |
| - control/hosts/<host>.json |
| +`control/hosts/<host>.json` in the control (deployment) bucket. It is |
| +replaced whole with conditional writes (`If-Match` on the ETag read). |
| ```json |
| { |
| - "v": 1, |
| + "v": 2, |
| "host": "shop.bab.oncarlos.com", |
| "gen": 41, |
| "holder": { |
| - "family": "instance", // instance | sidecar |
| + "family": "instance", |
| "key": "apps/bab/jam/instances/shop.bab.oncarlos.com.json", |
| - "account": "bab", "app": "jam", "name": "", // name: sidecars only |
| - "incarnation": "<hex>", |
| - "created_at": "<record CreatedAt>" |
| + "account": "bab", "app": "jam", "name": "", |
| + "incarnation": "<hex>", "created_at": "<record CreatedAt>" |
| }, |
| "op": { |
| - "kind": "serving", // see §4 |
| - "id": "op_…", // unique per operation; "" for serving |
| - "phase": "…", // owned by the operation's spec |
| - "by": "<actor>", "started_at": "…", |
| - "journal": { } // operation-bound durable state, small |
| + "kind": "serving", |
| + "id": "", |
| + "phase": "", |
| + "intent": { }, |
| + "journal": { }, |
| + "by": "", "started_at": "", |
| + "exec": "adi-knitting", |
| + "participants": ["adi-knitting"] |
| }, |
| "touched": { |
| - "regions": ["ie", "uk"], // every bucket that ever held data for this incarnation |
| - "boxes": ["adi-knitting", "iris-clockmaking"] // every box that ever held local state |
| + "complete": true, |
| + "regions": ["ie"], |
| + "boxes": ["adi-knitting"] |
| + }, |
| + "inventory": { |
| + "adi-knitting": { "layout": "nested", "paths": ["…"] } |
| }, |
| "obligations": [ |
| - {"id": "ob_…", "kind": "park-replica", "region": "uk"}, |
| - {"id": "ob_…", "kind": "park-local", "box": "iris-clockmaking"} |
| - ] |
| + {"id": "ob_…", "op": "op_…", "kind": "park-replica", "region": "ie", |
| + "retirement": "rt_…", "owner": "region:ie"} |
| + ], |
| + "lost": [], |
| + "retired_incarnations": ["<hex>", "…"] |
| } |
| ``` |
| -These rules apply to every field: |
| - |
| -- **`gen` increases by one on every write.** It is the claim's version, |
| - and every CAS is conditional on the ETag of the read. |
| -- **`holder` is the one incarnation entitled to the host.** |
| - - It is absent only when the host is **free**. |
| - - `key` names the exact record, so a sidecar is never looked up as an |
| - instance (199-11). |
| - - `incarnation` is `provision.Incarnation`. That is |
| - `maintenanceguard.RecordIdentity` over account, app, host and |
| - CreatedAt. A record with a zero CreatedAt instead gets the |
| - domain-separated legacy identity from rev 3 §2. |
| -- **`touched` only grows** for a holder, and is cleared only when the host |
| - becomes free. A component adds its region or box with a CAS **before** |
| - its first write of that incarnation's data there. That makes "where is |
| - this incarnation's data" a durable answer (199-3, 199-9, M2-5). |
| -- **`obligations` are durable chores.** Each names who must do it. A host |
| - cannot become free while any remain (M2-3, M2-4, M2-5). |
| - |
| -The claim is small, rewritten whole, and never listed on a hot path. |
| -Readers `GET` it by host. |
| +Field rules: |
| + |
| +- **`gen`** is the revision of the whole claim and increases on every |
| + successful claim write. It is not an installed-data generation (J-D2). |
| +- **`holder`** names the exact record, so a sidecar is never looked up as |
| + an instance. It is absent only while the host is **free**. |
| +- **`op.intent`** holds the operation's reconstruction inputs. It is |
| + written in the **same CAS** that starts the operation, before any other |
| + object is touched (J-N4). |
| +- **`op.journal`** holds the operation's durable phase data. |
| +- **`op.exec`** names the one box allowed to run the host's process, or |
| + `none`. **`op.participants`** are the boxes the operation involves. Both |
| + are per box, per phase (J-D1). See §4. |
| +- **`touched.regions` and `touched.boxes`** only grow while a holder holds |
| + the host, and each is appended **before** the first write there. |
| + `touched.complete` is false for an adopted legacy host, whose history is |
| + unknown (§9, J-N5). |
| +- **`inventory`** maps each box to its local paths for the host, for both |
| + layouts (§6.3). It is persisted here, independently of any operation's |
| + journal (J-I-7). |
| +- **`obligations`** are durable chores. Each names its operation, its |
| + retirement event (§6.2) and the actor that must do it. All of them |
| + block `free`. Each operation also defines which of them block its own |
| + release to `serving`. A release keeps any obligation owned by other |
| + lifecycle work (J-D8). |
| +- **`lost`** is the quarantine list for declared-lost boxes (§7). |
| +- **`retired_incarnations`** keeps the most recent 32 incarnations that |
| + held this host. A create whose incarnation appears there is refused |
| + (R3-12). |
| ## 3. Invariants |
| -**C1. One holder.** At most one incarnation holds a host. A record whose |
| -incarnation is not the claim's holder is an **orphan**: |
| +**C1. One holder.** A record whose incarnation is not the holder is an |
| +orphan, and is never admitted anywhere. |
| -- it is never admitted; |
| -- reconcile doesn't serve it; |
| -- the door refuses it; |
| -- wake refuses it. |
| +**C2. Intent before effect, and a recovery owner for every state.** |
| -**C2. Claim before record, record before release.** |
| -- **Create** CASes the claim from free (or absent; see §7) to |
| - `{holder: new, op: serving}` **before** `CreateRecord`. |
| -- **Delete** CASes `op` to `deleting` **before** removing the record, and |
| - removes it with `release.DeleteIfMatch` on the ETag it read **under** |
| - the claim (199-4). |
| -- The holder is cleared only at the end of the park (§5). |
| +- Every operation is started by one CAS that writes `op.kind`, `op.id`, |
| + `op.intent` and the first phase. |
| +- Every later cross-object step is replayable from the claim alone. |
| +- Each op kind names its recovery owner and its replay rule for every |
| + phase (§5, §8). |
| +- Every claim CAS is conditional on `op.id` as well as on the ETag, so a |
| + stale finalizer can never clear a newer operation. |
| -**C3. Mutation under the current operation.** Any change to the host's |
| -storage is made only by the claim's current `op.id`. Steady-state |
| -replication by the admitted serving process is the one exception. The |
| -storage is: |
| +**C3. Mutation only by the current operation, and only on exact object |
| +versions.** Storage changes happen only within the claim's current |
| +operation. That storage is: |
| - `instances/<host>/` and `moves/<host>/` in any region; |
| -- `parked/`; |
| -- the local database, `.lineage`/generation markers and the working |
| - directory. |
| - |
| -Each destructive step is preceded by re-reading the claim and confirming |
| -that `gen`'s op id and phase are unchanged. The worker must also hold the |
| -replica lease of every location it writes, acquired under the claim, and |
| -act only before that lease's `SafeUntil` (§3.1). That reread does not |
| -serialise anything on its own (M2 I-9). The lease does that, and the |
| -reread proves the lease was taken for the current operation. |
| - |
| -**C4. Admission is checked fresh.** These actors read the claim directly, |
| -never from a listing snapshot (199-8): |
| - |
| -- wake; |
| -- reconcile's decision to create or keep a provisioned row; |
| -- the db door. |
| - |
| -Each admits only when the holder's incarnation equals the record's and |
| -`op.kind` permits serving (§4). Unknown or unreadable means refuse, not |
| -admit. |
| - |
| -**C5. Revocation needs stop evidence.** An operation that needs serving |
| -stopped does not trust admission checks to have caught every running |
| -process. It obtains stop evidence (§6) from every box in |
| -`touched.boxes` that may be running the host, before its first |
| -destructive step. |
| - |
| -**C6. Read errors never act.** A claim, record or listing read that fails, |
| -or that returns something malformed, makes the actor wait or refuse. It |
| -is never treated as absence (199-8, 199-15). |
| - |
| -### 3.1 Leases, time and the assumption we make |
| - |
| -S3 cannot fence a delete by a token. Exclusion over storage therefore |
| -comes from the litestream lease (`lock.json`, conditional writes), held |
| -by the operation's worker. A worker that cannot renew must stop. |
| - |
| -Every destructive call checks `now < SafeUntil` immediately before it is |
| -issued, and runs under a context whose deadline is `SafeUntil`. |
| - |
| -**Assumption, stated plainly:** box clocks are NTP-synced, process pauses |
| -are shorter than the lease's safety margin, and an in-flight S3 request |
| -that outlives its context is cancelled client-side. This is the same |
| -assumption the activator's lease already makes for replication. A design |
| -needing more needs an S3 primitive the platform doesn't have. |
| - |
| -## 4. Operation kinds |
| - |
| -| `op.kind` | Serving admitted? | Owner spec | Ends in | |
| -|---|---|---|---| |
| -| `serving` | yes, in the record's region | this | any op below | |
| -| `deleting` | no | this (§5) | `parking` | |
| -| `parking` | no | this (§5) | free | |
| -| `moving` | source: per the moves spec's phase; target: no | move-any-app | `serving`, or `reverting` | |
| -| `landing` | target only once that spec's phase allows | move-any-app | `serving` | |
| -| `reverting` / `restoring` | per that spec | move-any-app | `serving` | |
| -| `pushing` | no | later push spec | `serving` | |
| - |
| -Starting any operation CASes from `serving`. One operation runs at a |
| -time, so a delete during a move is refused until the move resolves, and |
| -the reverse (199-6). Operator recovery has its own command: |
| - |
| - carlos ops host resolve <host> [--declare-lost <box>] |
| - |
| -`--declare-lost` removes a lost box's `park-local` obligations and its |
| -entry in `touched.boxes`. Its data is gone with it. The moves spec's own |
| -restriction applies: it is refused after a move commits (M2 §18). |
| - |
| -## 5. Delete and park (#199) |
| - |
| -Run by the console's delete doors (instance and sidecar), and by |
| -`PurgeApp`, one per record, in both its console and box callers. The four |
| -other record-deleting call sites, domain detach (UI and API), attach |
| -rollback and create rollback (199-10), go through the same shared helper, |
| -`provision.RetireRecord`. |
| - |
| -1. **Begin.** CAS `op = {deleting, id}` from `serving`, refused |
| - otherwise. This box or console drains the host's open db-door streams. |
| - The door is in-process on the one console; §8 covers more than one. |
| -2. **Remove the record.** Read it, check its incarnation is the holder, |
| - then `DeleteIfMatch` with that ETag. |
| -3. **Write the obligations** and move to `parking`, in one CAS: |
| - - one `park-replica` for each region in `touched.regions`; |
| - - one `park-local` for each box in `touched.boxes`. |
| -4. **Each obligation is done by its owner**, the box in that region or |
| - that box: |
| - 1. **Stop evidence** (§6) for the host on this box. |
| - 2. **Lease.** Acquire the lease on every location it will touch: |
| - `instances/<host>/` and, separately, `moves/<host>/`. If a holder |
| - is renewing, wait. |
| - 3. **Replica park** (199-7, 199-16, M2-7): |
| - - **Destination:** `parked/<incarnation>/<host>/instances/…` and |
| - `…/moves/…`, keeping each subtree's relative keys. |
| - - **Copy and manifest:** copy each key with a source-ETag |
| - condition, and record source key, ETag, size and destination |
| - key in `manifest.json`. Write the manifest last. |
| - - **Retry:** a manifest that is present is never rewritten. |
| - - **Delete:** for each manifest entry, `HEAD` the source and |
| - delete it only if its ETag still matches. A mismatch, or a source |
| - key absent from the manifest, stops the park. The obligation |
| - stays, an alert goes up, and the claim records the conflict. |
| - - **Last:** delete this worker's own `lock.json`, conditional on |
| - its own lease body. |
| - 4. **Local park** (199-13, 199-14): |
| - - **Inventory.** The obligation carries the inventory. It was |
| - written into the claim's journal when the box first touched the |
| - host, and refreshed on any layout change: `DBPath`, layout, |
| - working directory, `.lineage`/generation markers, `-wal`, `-shm`, |
| - litestream meta. |
| - - **Move each artifact** to `<DataDir>/.parked/<incarnation>/<host>/` |
| - with a non-overwriting rename (`renameat2` `RENAME_NOREPLACE`). |
| - - **Journal and sync.** Record per-artifact progress in a journal |
| - file beside them, and fsync the directories. |
| - - **Errors.** `EXDEV`, or any other error, leaves the obligation in |
| - place. |
| - - **Verdict.** Delete this host's dbverify verdict. |
| - 5. **Finish.** CAS the obligation out of the claim, conditional on the |
| - claim still showing `parking` with this op id. |
| -5. **Free.** When `obligations` is empty, CAS the claim to free: |
| - holder, op and touched all cleared, `gen` incremented. The tombstone of |
| - rev 3 is not needed: the claim's last state before free, and each |
| - `manifest.json`, are the record of what was parked. |
| - |
| -**A rolled-back move's target replica (M2-5).** The moves spec adds a |
| -`park-replica` obligation for the target region on rollback. It stays |
| -`touched`, so a later delete finds it either way. |
| - |
| -## 6. Stop evidence that survives a restart (M2-1, M2-2) |
| - |
| -**Evidence is computed from system state, never from activator memory.** |
| -For a host on a box, it holds when all of these are true: |
| - |
| -1. **The cgroup is empty.** The per-host cgroup that every exec child is |
| - placed in (`cgroup.ExecName(host)` under the agent's delegated subtree, |
| - backend_exec.go:96) reports `populated 0` in `cgroup.events`, or |
| - doesn't exist. A unit-backed host's `carlos-app@<host>.service` |
| - cgroup is checked the same way. This covers descendants that outlive |
| - the main process (M2-1). The fence is installed first, and the check |
| - waits for empty, with the operation's own deadline. |
| -2. **No live lease.** This box holds no lease for any location of the |
| - host. If `lock.json` exists, it names another holder and that holder |
| - has expired. |
| -3. **No replicator.** No replicator for the host's database is open in |
| - this agent process. A fresh process has none, by construction. |
| - |
| -**A box without cgroup delegation** cannot produce evidence. Lifecycle |
| -operations on its hosts are refused with a reason. This covers old unit |
| -files and hosts with `Cgroups == nil`. |
| - |
| -**After a restart,** evidence is simply recomputed. "Never spawned" is |
| -the same check: an absent cgroup and no lease. The activator's in-memory |
| -`stopHistory` is an optimisation, never a requirement. `FenceAndStop` |
| -gains a path that returns evidence from system state when its memory is |
| -empty, instead of `ErrStopUnproven` (M2-2). |
| - |
| -## 7. Adoption of existing hosts (R2) |
| - |
| -Hosts that exist before this release have no claim. The first actor that |
| -needs one creates it, create-only, as `{holder: current record, op: |
| -serving, touched: {regions: [record region], boxes: [this box, if it has |
| -local state]}}`: |
| - |
| -- the owning box's reconcile; |
| -- any door. |
| - |
| -A box that later finds local state for an adopted host adds itself to |
| -`touched` before acting. |
| - |
| -**Create on a host with no claim and no record** uses the #199 stopgap's |
| -check: a replica prefix that holds data in the console's region refuses |
| -the create. Leftovers there have no recorded owner, and R2 adopts only |
| -for a **current** record. Elsewhere, the create proceeds, adopted as |
| -today. |
| - |
| -## 8. Admission points, concretely |
| - |
| -- **`doWake`, before `Acquire`** (the Classifier refusal precedent at |
| - activator.go:1090). Read the claim, and require: |
| - - holder = the row's record incarnation; |
| - - `op.kind` allows serving here; |
| - - this box is in `touched.boxes`, CAS-adding it if not. |
| - |
| - Unreadable means the wake fails, retryably. |
| -- **Reconcile row creation and keeping.** The row gains `incarnation` |
| - and `claim_gen` columns. A provisioned row whose incarnation is not the |
| - claim's holder is retired with stop evidence, whatever its account and |
| - app. This covers same-app recreation (199-1). Rows that a running |
| - operation lists as participants are retained until its obligations |
| - finish (M2-4). |
| -- **The db door.** Read the claim on the listing request, and bind the |
| - restore to `gen`. Each later file `GET` rechecks the claim through a |
| - short-lived cache, and refuses once `gen` moves (199-2). Delete step 1 |
| - also drains the door. With more than one console, step 1 must wait out |
| - the cache lifetime instead. |
| -- **Create.** §3 C2. |
| - |
| -## 9. Rollout |
| - |
| -Old binaries don't know the claim. Two rules make that safe: |
| - |
| -- **Fail closed toward old binaries.** A delete by an old console leaves |
| - the claim holding an incarnation whose record is gone. Admission |
| - refuses the host from then on, and create refuses too. The host is |
| - stuck until `carlos ops host resolve` runs. That is visible and safe: |
| - never a silent inheritance. |
| -- **Floor.** New lifecycle operations (delete-park, and moves) run only |
| - while the deployment's protocol floor, the moves spec's floor object, |
| - lists every box and console at or above this release. Below the floor |
| - they are refused, and deletes keep today's behaviour plus the stopgap. |
| - |
| -## 10. Simulation |
| - |
| -Before planning, the claim, delete-park and the moves operations get a |
| -model-level simulation in the shape of the moves spec's: random |
| -interleavings and crashes at every side effect. It covers: |
| - |
| -- surviving descendants; |
| -- empty activator memory; |
| -- two consoles; |
| -- delete during each move phase; |
| -- recreate during park; |
| -- reconcile running before release; |
| -- stale door streams. |
| - |
| -It runs at high seed counts, with mutation checks that drop each guard in |
| -turn and confirm the simulation catches it. |
| +- `parked/` and `superseded/`; |
| +- the host's local files. |
| + |
| +The serving process's ordinary replication is the one exception. |
| + |
| +Every destructive storage call names **an exact object version**: a |
| +`DeleteObject` with `VersionId`, or a `CopyObject` from |
| +`key?versionId=`. Never a bare key. Both buckets are versioned |
| +(deployment-buckets/main.tf:23, :28). A request that completes late |
| +therefore touches only the version it named, never a later incarnation's |
| +object at the same key. That makes late server-side completion harmless |
| +(J-N1). |
| + |
| +- **A bare-key delete is forbidden on these prefixes.** On a versioned |
| + bucket it creates a delete marker that would hide a successor's current |
| + object. |
| +- **Exclusion between workers of the same operation** comes from leases, |
| + which are taken before re-validating the operation and its phase: |
| + - the replica lease (`lock.json`) for a location the worker can read; |
| + - the shared **staging-work lease** in the deployment bucket, keyed by |
| + destination region and host, for cross-region staging. Both |
| + participants can reach it (J-D4). The moves spec owns staging |
| + sealing and draining. |
| + |
| +The clock and pause assumption of rev 1 §3.1 remains, but only for |
| +**liveness**: a worker that cannot renew stops. Correctness no longer |
| +depends on it, because every destructive request is bound to an exact |
| +version. |
| + |
| +**C4. Fresh admission.** Admission reads the claim directly, never from a |
| +listing snapshot. Admission checks happen at: |
| + |
| +- every spawn (wake, Seed, a probe, a recovery); |
| +- restore and any other local mutation; |
| +- reconcile's decision to create or keep a row; |
| +- a door read. |
| + |
| +Admission requires all of: |
| + |
| +- the holder's incarnation equals the record's; |
| +- `op.exec` names this box; |
| +- the operation's admission table permits this box's role in this phase. |
| + |
| +**Region equality alone never grants admission.** Ordinary wake and a |
| +recovery probe are distinct permissions (J-D1). |
| + |
| +**C5. Revocation needs stop evidence** (§6.1) from every box that may run |
| +the host, **or** a lost-box fence (§7). |
| + |
| +**C6. Read errors never act.** A failed or malformed read of a claim, |
| +record or listing means wait, or refuse. It never means absent. |
| + |
| +**C7. Already-admitted work is drained.** Any process that started work |
| +for a host before an operation began must either finish under the guard |
| +it was admitted with, or be refused at its next host-specific write. That |
| +covers background passes (§6.4) and door reads (§6.5) (J-N8, J-N10). |
| + |
| +## 4. Operation kinds and transitions |
| + |
| +| `op.kind` | Owner spec | Recovery owner | |
| +|---|---|---| |
| +| `serving` | this | none | |
| +| `creating` | this (§5.1) | the console's claim-recovery pass | |
| +| `deleting`, `parking` | this (§5.2) | the console's pass for the claim steps; each obligation's owner for its chore | |
| +| `purging` | this (§5.3) | the console's pass | |
| +| `placing` | this (§5.4) | the console's pass | |
| +| `moving`, `landing`, `reverting`, `restoring` | move-any-app | as that spec names, one writer per transition | |
| +| `pushing` | later | later | |
| + |
| +**Move-kind transitions,** as J-D7 words them: `serving → moving`; |
| +`moving → landing` or `reverting`; `landing → restoring` or, after |
| +committed finalization, `serving`; `reverting`/`restoring → serving` only |
| +after their recovery and cleanup conditions hold. A change of kind does |
| +not by itself transfer execution authority: `op.exec` changes only by a |
| +CAS that cites stop evidence or a lost-box fence. |
| + |
| +Only one operation runs at a time, and a new one starts from `serving`. |
| + |
| +## 5. This spec's operations |
| + |
| +### 5.1 Create (R3-12, J-N4) |
| + |
| +1. The console assigns `CreatedAt` = now (UTC, nanoseconds). A caller |
| + cannot supply it. `CreateRecord` and `CreateSidecarRecord` refuse a |
| + zero or caller-supplied time on this path. |
| +2. **CAS** the claim from free or absent (§9) to |
| + `{holder: new, op: {creating, id, intent: {record body, key}}}`. This |
| + is refused if the incarnation is in `retired_incarnations`, or if the |
| + app holds a purge reservation (§5.3). |
| +3. `CreateRecord`, create-only. |
| +4. **CAS** `op` to `serving` and set `exec` to the record region's box. |
| +5. **Recovery,** by the console's claim-recovery pass, which lists |
| + `control/hosts/` every few minutes and handles claims whose `op` is not |
| + `serving` and older than five minutes: |
| + - the record exists with this incarnation: do step 4; |
| + - it is authoritatively absent: CAS back to free; |
| + - anything else: wait. |
| + |
| +### 5.2 Delete and park (#199) |
| + |
| +Run by the instance and sidecar delete doors, and by |
| +`provision.RetireRecord`, which is what every other record-deleting call |
| +site now uses: |
| + |
| +- domain detach, UI and API; |
| +- attach rollback; |
| +- create rollback; |
| +- `PurgeApp`, via §5.3. |
| + |
| +1. **CAS** `op = {deleting, id, intent: {record key, record ETag}}`, |
| + from `serving` only. |
| +2. **`DeleteIfMatch`** on the record with the ETag in `intent`. This is |
| + replayable: a record that is already absent, or one whose ETag doesn't |
| + match, is checked again under C6. |
| +3. **CAS** `parking`, writing the obligations: |
| + - `park-replica` for each region in `touched.regions`; |
| + - `park-local` for each box in `touched.boxes`; |
| + - if `touched.complete` is false: **every** region and **every** box |
| + of the deployment, taken from the fleet inventory (J-N5). |
| + |
| + Each obligation gets its own retirement id. Then append the |
| + incarnation to `retired_incarnations`. |
| +4. **Each owner does its obligation** (§6). It finishes with a CAS that |
| + removes the obligation, conditional on `op.id`. |
| +5. **Free:** when no obligation remains, CAS the claim to free, clearing |
| + holder, op, touched and inventory, but keeping `retired_incarnations` |
| + and `lost`. |
| +6. **Recovery,** by the console pass: |
| + - `deleting`: do steps 2 and 3; |
| + - `parking` with no obligations left: do step 5. |
| + |
| +### 5.3 App purge (J-N9) |
| + |
| +1. **Reserve the app first.** Write `apps/<acct>/<app>/purge.json`, |
| + create-only. The create door refuses any create for an app with this |
| + reservation. |
| +2. **CAS every host claim of the app** to `{purging, id}`, from `serving`. |
| + A host under any other operation fails the purge with its reason. The |
| + ones already reserved stay reserved, and the operator retries. |
| +3. **Only then** tear down stores and email, as today (ownership.go:404), |
| + then run §5.2 for each record and remove the app prefix |
| + (`PurgeApp`). |
| +4. **The boxes' auto-purge** (domains/reconcile.go:232) runs the same |
| + steps. |
| + |
| +### 5.4 Placement (J-N8) |
| + |
| +A placement change (fleets.go:616, `SetRecordRegion` at provision.go:853) |
| +is an operation, `placing`. Its CAS from `serving` comes **before** any |
| +app, registry or record write, with the target in `intent`. The pass |
| +replays it. Moves and placements therefore exclude each other. |
| + |
| +## 6. Mechanisms |
| + |
| +### 6.1 Stop evidence (J-D3) |
| + |
| +The rule, as J-D3 words it: |
| + |
| +- every lifecycle-controlled spawn requires strict containment |
| + (`PrepareStrict`); |
| +- stop evidence requires: |
| + - a closed admission fence; |
| + - drained spawn attempts; |
| + - an empty complete process tree (the per-host cgroup's `populated 0`, |
| + and no member processes); |
| + - closed replicators; |
| + - no remaining holders of the database, WAL or SHM files (checked |
| + through `/proc/*/fd`); |
| +- an absent host cgroup is not enough where an earlier spawn could have |
| + escaped containment. |
| + |
| +Evidence is reconstructed from system state, never from activator |
| +memory. A cleanup-only operation can reopen an existing populated cgroup, |
| +identify its processes, kill and drain them, without granting any |
| +authority to spawn. `PrepareStrict` stays the empty-group spawn API. |
| + |
| +A child spawned with best-effort placement before this release is not |
| +certified as stopped just because its parent exited. Its host needs the |
| +cleanup operation first. A box without cgroup delegation cannot produce |
| +evidence, so lifecycle operations on its hosts are refused. |
| + |
| +### 6.2 Parking, by exact version (J-N1, J-N6, J-N7, J-D5) |
| + |
| +**Destination.** Each retirement event has its own destination: |
| + |
| + parked/<incarnation>/<host>/<retirement-id>/{instances,moves}/<relative key> |
| + |
| +The moves spec's equivalent is `superseded/<op>/<host>/<retirement-id>/…`. |
| +A manifest belongs to exactly one retirement event and is never reused. |
| + |
| +**Steps:** |
| + |
| +1. **Lease.** Take the replica lease on each location the owner can read. |
| +2. **Snapshot.** List the location's object versions |
| + (`ListObjectVersions`). From that listing, take every current version |
| + except the live `lock.json`. A coordination lock is never data and |
| + never enters a manifest (J-N6). |
| +3. **Copy** each current version by `versionId` to the destination. |
| +4. **Write the manifest last.** It records each entry's source key, |
| + source version id, size, and destination key and version. A manifest |
| + that already exists is never rewritten. |
| +5. **Delete** every version of each manifest key whose version id is in |
| + the snapshot, **by version id**. That includes noncurrent versions, so |
| + deleting the current one cannot resurrect an older one. A version that |
| + is not in the snapshot is left alone, which keeps a later |
| + incarnation's object at the same key safe even from a late delete. |
| +6. **Release** this worker's own `lock.json` version, conditionally, after |
| + the obligation's completion CAS. |
| +7. **Retry:** if the manifest exists, go straight to deletes of its |
| + recorded versions. If it doesn't, start again from step 2. |
| + |
| +IAM: the box needs `s3:ListBucketVersions`, `s3:GetObjectVersion` and |
| +`s3:DeleteObjectVersion` on its own data bucket. Today it has only |
| +`Get`, `Put`, `Delete` and `List` (region-host main.tf:166, :174). |
| + |
| +### 6.3 Local retirement (J-I-7, 199-13, 199-14) |
| + |
| +Retirement covers both layouts. |
| + |
| +- **A flat host:** |
| + - `<DataDir>/<host>/`; |
| + - the database and its companion artifacts; |
| + - `<host>.env`, `<host>.config.env` and `<host>-sidecar.env`; |
| + - generation and lineage markers; |
| + - any other host-bound operational state. |
| +- **A nested host:** the resolved instance directory. |
| + |
| +The inventory lives in the claim's `inventory`. A box writes its entry |
| +before it first materializes local state, and updates it on a layout |
| +change. |
| + |
| +Retirement moves each artifact under `<DataDir>/.parked/<incarnation>/ |
| +<host>/<retirement-id>/` with `RENAME_NOREPLACE`. It journals each |
| +artifact's progress, and fsyncs the directories before the completion |
| +CAS. `EXDEV`, or any other error, keeps the obligation open. An empty |
| +retirement still sends its acknowledgement, so the host cannot become free |
| +until every recorded location has acknowledged. |
| + |
| +### 6.4 The local host guard (J-N8) |
| + |
| +Every host-specific local write on a box goes through |
| +`hostguard.With(host, incarnation, opID, fn)`. Those writes are: |
| + |
| +- config sync's `<host>.config.env` (syncexec.go:1091, :1180); |
| +- release adoption's live symlink (adopt.go:1045); |
| +- env files; |
| +- the admin token; |
| +- the timer registry. |
| + |
| +The guard is a per-host in-process lock. Under it, the box re-reads the |
| +admission state it caches (C4) and refuses if the incarnation or the |
| +operation has moved on. |
| + |
| +Local retirement (§6.3) takes the same guard, then writes a retired |
| +marker for the incarnation, so any later writer for that incarnation is |
| +refused. A pass that selected a row before an operation began therefore |
| +either finishes before retirement takes the guard, or fails at its next |
| +write. |
| + |
| +The guard is local because these writers are local. The claim decides |
| +what each writer is allowed to do. |
| + |
| +### 6.5 Door reads pinned to versions (J-N10) |
| + |
| +The pull door's listing resolves each LTX coordinate to an exact object |
| +version and returns an opaque, console-signed handle. A file request |
| +names that handle, and the console opens `key?versionId=`. A handler that |
| +stalls between authorization and open can therefore only ever read the |
| +version it authorized: data the requester was entitled to when it was |
| +authorized. It can never read a later incarnation's object at the same |
| +key. The console needs `s3:GetObjectVersion`. |
| + |
| +Delete step 1 also stops accepting new door requests for the host, on |
| +every console. But safety does not depend on draining them. |
| + |
| +## 7. Lost boxes and execution fencing (J-D6, J-N3) |
| + |
| +A claim CAS is bookkeeping, not fencing. A box can be partitioned from |
| +the control bucket and still reach its data bucket and the outside world. |
| + |
| +### 7.1 Execution leases |
| + |
| +While a host is under any operation, each participant box must hold an |
| +**execution lease** for that host: |
| + |
| + control/hosts/<host>/exec/<box>.json {"op": "…", "expires": "…"} |
| + |
| +- The box renews the lease every 20 seconds, with a 90-second TTL. |
| +- If it cannot renew before `expires`, the box **self-fences**: it kills |
| + the host's process tree using the cleanup-only operation (§6.1) and |
| + refuses admission until it can read the claim again. |
| +- An operation does not leave its first phase until every participant has |
| + written its execution lease. That is how the operation knows each |
| + participant has seen it. |
| + |
| +### 7.2 Declaring a box lost |
| + |
| + carlos ops host resolve <host> --declare-lost <box> |
| + |
| +The move form, `carlos move resolve --declare-lost`, delegates to this |
| +command and keeps the move spec's restrictions: before commit only, the |
| +exact participant, the source refused, and loss confirmed explicitly. |
| + |
| +The command: |
| + |
| +- refuses unless the box's execution lease has passed its expiry plus a |
| + 60-second margin; |
| +- or, if the box never wrote one, refuses unless the operator supplies |
| + compute-fencing evidence that the CLI verifies through the cloud API, |
| + using the operator's own credentials. The console never holds EC2 |
| + rights. For example, the instance must be `stopped` or `terminated`. |
| + |
| +Only then does it remove the box's obligations and execution authority. |
| +It adds the box to `lost`, a quarantine list that survives the |
| +operation's release. A box on `lost` is refused admission for any host |
| +until its old state has been retired and an operator removes it with |
| +`--readmit`. |
| + |
| +**Cost.** This adds one renewal write per participant per 20 seconds, |
| +only while an operation is running. A host that is simply serving holds |
| +no execution leases, so a control-bucket outage cannot stop serving |
| +traffic. |
| + |
| +## 8. Recovery owners, summarised |
| + |
| +| State | Owner | Replay | |
| +|---|---|---| |
| +| `creating` | console pass | §5.1 step 5 | |
| +| `deleting` | console pass | §5.2 steps 2-3 | |
| +| `parking`, obligation open | the obligation's owner box or region | §6.2 step 7, §6.3 journal | |
| +| `parking`, none left | console pass | §5.2 step 5 | |
| +| `purging` | console pass | §5.3, from the reservation | |
| +| `placing` | console pass | §5.4, from `intent` | |
| +| move kinds | move-any-app | one writer per transition | |
| + |
| +Claims are listed only by the recovery pass, never on a hot path. |
| + |
| +## 9. Legacy hosts (R2, J-N5) |
| + |
| +A host that exists before this release gets a claim from the first actor |
| +that needs one. That claim is written create-only, with: |
| + |
| +- the current record as holder; |
| +- `touched.complete: false`; |
| +- `touched.regions` set to the record's region; |
| +- `touched.boxes` set to the box, if it has local state. |
| + |
| +Because `complete` is false, a delete parks **every** region and **every** |
| +box of the deployment (§5.2 step 3). An adopted host cannot be reused |
| +until all of them have acknowledged, even when they have nothing to park. |
| + |
| +A create on a host with no claim and no record goes through the #199 |
| +stopgap's check first. The claim is then written as `complete: true`, |
| +because the instance is new. |
| + |
| +## 10. Rollout and the version floor (J-N12) |
| + |
| +- **The floor.** Lifecycle operations run only once the protocol floor, |
| + shared with the moves spec, lists every box and console at or above |
| + this release. Below the floor they are refused, and deletes keep |
| + today's behaviour plus the stopgap. |
| +- **Every path that restores an executable** must refuse to activate a |
| + binary below the published floor. That covers `system apply`, explicit |
| + rollback, and **automatic boot recovery** restoring `carlos.prev` |
| + (systemapply.go:901, :817). It also checks `.prev` and any outstanding |
| + update journal before activating. |
| +- **Order.** The floor is published before any protected rehearsal on |
| + production. |
| +- **An old console's delete** leaves a claim whose holder's record is |
| + gone. Admission and create then refuse the host until |
| + `carlos ops host resolve` runs. That is visible and safe. |
| +- **IAM:** the versioned-object grants in §6.2 and §6.5. |
| + |
| +## 11. Simulation |
| + |
| +The joint executable model, being built by the moves session, decides |
| +whether this is ready. Its scope must include everything in J's last |
| +paragraph: |
| + |
| +- the real permission split; |
| +- late server-side completion; |
| +- claim-only operations; |
| +- discovery of legacy residue; |
| +- delayed config and adoption writes; |
| +- purge teardown; |
| +- stalled door handlers; |
| +- automatic boot recovery; |
| +- several retirement events within one operation; |
| +- partitioned participants; |
| +- descendants that outlive the main process; |
| +- empty activator memory. |
| + |
| +It runs 30k+ seeds, with mutation checks that drop each guard and confirm |
| +the model catches it. |
| + |
| +## 12. Finding map |
| + |
| +| Finding | Section | |
| +|---|---| |
| +| J-D1 | §2 `op.exec` and `op.participants`, C4, §4 | |
| +| J-D2 | §2 `gen` | |
| +| J-D3 | §6.1 | |
| +| J-D4 | C3, the staging-work lease (the moves spec owns sealing and draining) | |
| +| J-D5, J-N7 | §6.2 retirement ids | |
| +| J-D6, J-N3 | §7 | |
| +| J-D7 | §4 | |
| +| J-D8 | §2 obligations | |
| +| J-I-7 | §6.3 | |
| +| J-N1 | C3, §6.2, §6.5 (exact versions) | |
| +| J-N4 | C2, §5, §8 | |
| +| J-N5 | §9, §5.2 step 3 | |
| +| J-N6 | §6.2 step 2 | |
| +| J-N8 | C7, §5.4, §6.4 | |
| +| J-N9 | §5.3 | |
| +| J-N10 | §6.5 | |
| +| J-N12 | §10 | |
| +| R3-12 | §5.1, §2 `retired_incarnations` | |
| +| J-N2 (moves side), N11, N13, N14, N15 | move-any-app | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R1.md b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R1.md| new file mode 100644 |
| index 000000000..2b0eef410 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-JOINT-R1.md |
| @@ -0,0 +1,303 @@ |
| +**Neither spec is ready for planning.** B rev 3 resolves most of the original round-2 findings, but the combined protocol still permits concurrent writers after `declare-lost`, cannot safely exclude delayed staging work, and has several crash paths that cannot finish. |
| + |
| +I read AGENTS.md, both complete specs, and all five prior findings documents. Code references below refer to `6e4d3a0e` unless explicitly qualified. **The db-door implementation is absent from this worktree**; I checked it at `653ad4b1`. This was a static, read-only review: no files changed, tests run, or production actions taken. The requested repository-policy Opus cross-check was unavailable; these are my findings. |
| + |
| +**1. Moves round-2 dispositions** |
| + |
| +“Resolved” means the particular design defect is addressed, not that the implementation exists or the composed protocol is approved. |
| + |
| +| R2 finding | Verdict | Reason | |
| +|---|---|---| |
| +| R2-1: surviving flat-exec descendants | **Resolved in B** | §5.3 requires strict containment, empty process trees and stray-process checks; A must adopt D3. | |
| +| R2-2: stop evidence lost with activator memory | **Resolved in design** | Reconstruction now uses observable state, including never-spawned operations, rather than `stopHistory`. | |
| +| R2-3: dirty source recovery replays installation | **Resolved** | §7.8 has separate source recovery phases and prohibits reinstalling after `probing`. Pre-flip recovery has a different gap below. | |
| +| R2-4: reconcile retires rollback target | **Resolved** | Both participants remain held until release and cleanup finish. | |
| +| R2-5: rollback leaves target replica live | **Resolved as a requirement** | Target replica/staging parking is now mandatory before finalization; the park algorithm has new completion failures below. | |
| +| R2-6: premature installation markers | **Resolved** | Bucket park/copy/publication are separated; `.files-gen` follows durable env, timer and registry installation. | |
| +| R2-7: mirror deletes adjacent metadata | **Resolved** | Mirroring is confined to `replica/`; archives, timers and operation metadata are separate. | |
| +| R2-8: incomplete and unpinned launch environment | **Partly** | Composition and input versions are covered, but checking at admission/configuration does not exclude delayed config/adoption work or changed inherited environment at the actual spawn. | |
| +| R2-9: missing markers and restore verdict | **Resolved as inventory** | Markers are classified and excluded from content digests; verdict invalidation is specified. | |
| +| R2-10: incomplete cut budget | **Partly** | T11 includes the missing stages, but budgets one probe attempt while §7.7 permits three; no unambiguous end-to-end deadline constrains landing retries. | |
| + |
| +The carried-forward timer finding also remains **partly resolved**: draining delivery and freezing the converger do not cover the runner’s separate pruning path. |
| + |
| +**2. D1–D8 and I-7** |
| + |
| +**D1 — B is right: admission must identify the box and phase.** |
| + |
| +A region alone is insufficient. Wake currently refreshes a local row at [activator.go:1071](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/activator.go:1071); ordinary reconcile mints it `ready` at [reconcile.go:364](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/reconcile.go:364). Neither expresses the transfer of execution authority. |
| + |
| +Exact text: |
| + |
| +- **A §§4, 8:** “For move operations, admission requires the holder incarnation, execution holder, participant identity and phase-specific permission defined by the moves spec. Region equality alone never grants admission. Ordinary wake and recovery probe are distinct permissions.” |
| +- **B §19.1/K1:** “The admission table governs every spawn, including Seed, probe retries and recovery. The table, current holder incarnation and `exec` must all authorize the exact box. Check authorization before restore or other local mutation as well as before spawn.” |
| + |
| +**D2 — A is right; B has correctly withdrawn the disagreement.** |
| + |
| +Claim revision and installed generation serve different purposes. The existing creation identity is explicitly continuity metadata, not a database generation: [types.go:60](/home/paulca/amadan.net/carlos/platform-moves-design/internal/maintenanceguard/types.go:60). |
| + |
| +Exact text: |
| + |
| +- **A §2:** “`gen` is the revision of the whole claim and increases on every successful claim write. It is not an installed-data generation.” |
| +- **B §5.1:** “Installed generations are identified by operation id and incarnation. Claim `gen` is used only for claim concurrency and observations; it is never an installed-generation marker.” |
| + |
| +**D3 — B is right, with a required restart-recovery API distinction.** |
| + |
| +Best-effort placement can leave descendants outside the host cgroup: [cgroup.go:230](/home/paulca/amadan.net/carlos/platform-moves-design/internal/cgroup/cgroup.go:230). Also, `PrepareStrict` rejects a populated group, so it cannot itself reopen and kill a surviving group after restart: [strict_linux.go:206](/home/paulca/amadan.net/carlos/platform-moves-design/internal/cgroup/strict_linux.go:206). |
| + |
| +Exact text: |
| + |
| +- **A §6:** “All lifecycle-controlled spawns require strict containment. Stop evidence requires a closed admission fence, drained spawn attempts, an empty complete process tree, closed replicators and no remaining database/WAL/SHM holders. An absent host cgroup is insufficient where an earlier spawn could escape containment.” |
| +- **B §5.3:** “Reconstruction uses a cleanup-only operation that can reopen, identify, kill and drain an existing populated cgroup without granting spawn authority. `PrepareStrict` remains the empty-group spawn API. A pre-move best-effort child is not certified stopped by ordinary parent exit.” |
| + |
| +Apply this to delete/park as well as moves. |
| + |
| +**D4 — B is right about IAM; its proposed exception is unsafe. Neither exclusion rule works as written.** |
| + |
| +The grants are precise: |
| + |
| +| Principal | Own data bucket | Sibling `moves/*` | Sibling `instances/*` | |
| +|---|---|---|---| |
| +| Region host | Get, Put, Delete; List | Put, Delete; prefix-conditioned List | No grant through sibling staging | |
| + |
| +See [main.tf:166](/home/paulca/amadan.net/carlos/platform-moves-design/infra/modules/region-host/main.tf:166) and [main.tf:217](/home/paulca/amadan.net/carlos/platform-moves-design/infra/modules/region-host/main.tf:217). A source cannot read the destination lock. But two workers for the **same operation** share its prefix, and `MirrorPrefix` deletes destination-only keys: [mirror.go:222](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/mirror.go:222). |
| + |
| +Exact text: |
| + |
| +- **A C3:** “Cross-region staging uses a shared staging-work lease in the deployment bucket, keyed by destination region and host, accessible to both participants. Every staging writer, seal, park and abort obeys this lease. Actors acquire it before revalidating operation and phase. Per-operation naming alone is not exclusion.” |
| +- **B §19.3 D4:** “Retain M17’s push-only sibling grant. Replace the lease exception with the shared staging-work lease. Before sealing or parking staging, drain earlier rounds and their outstanding I/O. Landing consumes a sealed manifest of exact object identities, using conditional copies; no earlier round may mutate the sealed input.” |
| + |
| +The deployment-bucket grant already permits this coordination. The late-I/O requirement still needs the correction in N1 below. |
| + |
| +**D5 — B is right about separating move retirement from incarnation deletion, but operation id alone is insufficient.** |
| + |
| +The target can park an earlier stay during installation and later park this move’s failed landing during rollback. Both currently use `superseded/<move id>/<host>/`. Those are different datasets within **one** operation. A unique operation id does not separate them. |
| + |
| +The source/staging coordinates are independently derived in [movespass.go:364](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/movespass.go:364); copying supports a destination key, so the distinction can be preserved: [mirror.go:467](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/mirror.go:467). |
| + |
| +Exact text: |
| + |
| +- **A §§2, 5:** “A `park-superseded` obligation identifies operation, retirement event, location, retired generation and artifact class. Its immutable manifest belongs to that exact retirement event, not merely to the incarnation or operation.” |
| +- **B §§6.4, 7.6, 7.8, 7.9:** “Use distinct destinations beneath `superseded/<op>/<host>/<retirement-id>/`, retaining separate `instances/` and `moves/` subtrees. Initial target retirement, failed-target retirement, source retirement and staging retirement never share a manifest.” |
| + |
| +**D6 — B identifies a real omission, but neither spec supplies independent execution fencing.** |
| + |
| +Changing `exec` cannot stop a partitioned process. Existing supervision reacts to the **regional replica lease**, not a globally enforced execution grant: [activator.go:2266](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/activator.go:2266). Source and target leases cover different buckets. |
| + |
| +Exact text: |
| + |
| +- **A §4:** “Declaring a box lost does not itself establish stop evidence. Before transferring execution, resolve must obtain independently verified execution fencing of the exact box incarnation. Without that proof it retains the hold. Lost-box quarantine survives operation release and prevents readmission until its old state has been retired.” |
| +- **B §7.10/D6:** “A claim CAS is bookkeeping, not independent fencing. The resolve command must establish verified compute fencing, or an independently enforced execution-lease expiry, before reopening the source. Recover validated durable target data where available, not only an already-published return. Retain M16’s precommit restriction, exact-participant check, source refusal and explicit loss confirmation.” |
| + |
| +The command must perform this through platform interfaces; it cannot require a follow-up box command. |
| + |
| +**D7 — B is right.** |
| + |
| +The existing `MoveComplete` combines region change and clearing the old move, [provision.go:1053](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/provision.go:1053); it cannot be reused unchanged for the proposed multi-stage protocol. |
| + |
| +Exact text for **both operation tables**: |
| + |
| +> “Legal move-kind transitions are `serving → moving`; `moving → landing` or `reverting`; `landing → restoring` or, after committed finalization, `serving`; `reverting/restoring → serving` only after their recovery and cleanup conditions hold. Kind transitions do not independently transfer execution authority.” |
| + |
| +Also reconcile K4’s “by that participant” with §7.5’s source completing the target handoff after a crash. Name one authorized writer for each transition and its recovery. |
| + |
| +**D8 — Both rules are compatible; retain B’s stronger operation-specific completion condition.** |
| + |
| +Existing `MoveAbortComplete` simply clears the record, [provision.go:1043](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/provision.go:1043), so builders must not mistake that helper for the new completion contract. |
| + |
| +Exact text: |
| + |
| +- **A §2:** “All obligations block `free`. Each operation additionally defines which obligations block its release to `serving`; release preserves obligations owned by any other durable lifecycle work.” |
| +- **B K8:** “A move releases to `serving` only after every obligation it created has a durable completion acknowledgement. Record cleanup and claim release follow the crash-recoverable finalization protocol, including abort.” |
| + |
| +**I-7 — B’s explicit flat-file inventory is necessary.** |
| + |
| +Flat env files are siblings of the database, not entries in the flat files directory: [paths.go:50](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/paths.go:50). `EnsureAdminToken` deliberately preserves an existing token: [admintoken.go:104](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/admintoken.go:104). |
| + |
| +Exact text: |
| + |
| +- **A §5.4:** “Local retirement covers both layouts. For flat hosts it includes `<DataDir>/<host>/`, the database and companion artifacts, `<host>.env`, `<host>.config.env`, `<host>-sidecar.env`, generation/lineage markers and host-bound operational state. Nested inventory uses the resolved instance directory. Persist this inventory independently of the replaceable operation journal.” |
| +- **B §17 I-7:** “Agreed: A’s local retirement inventory covers flat files and sibling env files as well as nested state. A host cannot become free until every recorded location acknowledges completion, including an empty retirement.” |
| + |
| +**3. New findings** |
| + |
| +The following are additional failure traces or failures in the proposed remedies, rather than missing implementation being reported as a defect. |
| + |
| +**N1 — P1: client cancellation does not establish the storage exclusion assumed by the simulation.** |
| +**A §3.1/C3; B §19.4.** |
| + |
| +A destructive request is issued before `SafeUntil`; the client times out, the lease expires, and a successor installs new data. The old server-side request can still complete against the reused key. Checking the deadline before submission and cancelling the client does not supply a server-side ownership condition. |
| + |
| +The current delete has no condition at all: [mirror.go:493](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/mirror.go:493). The lease deadline contract itself warns that notification is not proof: [lease.go:182](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/lease.go:182). |
| + |
| +**Fix:** specify conditional/version-bound destructive operations or non-reused physical object identities that make late completion harmless. Keep clock/pause assumptions separate from server-side completion. Model “request submitted, client cancelled, server completes later”; an atomic bucket-call model cannot catch this. |
| + |
| +**N2 — P1: the D4 exception permits a delayed round to corrupt sealed staging.** |
| +**B §§7.3–7.6, 19 K5/D4; A C3.** |
| + |
| +Worker W reads the permitted phase, then pauses. Another worker finishes the final round and flips. W resumes its same-operation mirror and overwrites or deletes keys while the target copies them. Operation id and incarnation still match. |
| + |
| +The existing pass mutex is process-local, [movespass.go:238](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/movespass.go:238); destination mutation occurs later in [mirror.go:198](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/mirror.go:198) and `:228`. |
| + |
| +**Fix:** adopt D4’s shared staging lease, validation under that lease, explicit round draining and sealed object identities. Exercise two workers for the same operation, not just competing move ids. |
| + |
| +**N3 — P1: `declare-lost` can start a second writer immediately.** |
| +**A §4; B §7.10, K6/K11.** |
| + |
| +The target probe remains alive while partitioned from the control bucket. Resolve changes `exec` to `none`, then the source recovers. The target has not read the new claim and continues background writes. A future kill “when it returns” does not repair the interval with two writers. |
| + |
| +Regional replication supervision at [activator.go:2266](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/activator.go:2266) does not fence a process merely because another bucket’s claim changed. |
| + |
| +**Fix:** D6’s independent fence before source admission. Test a live target partitioned only from control-plane access, including one still able to reach its regional bucket and external systems. |
| + |
| +**N4 — P1: the claim and record have unjournaled transaction gaps.** |
| +**A C2/§5; B §§7.1, 7.5, 7.8–7.11.** |
| + |
| +Concrete crash points: |
| + |
| +- Create claims `serving`, then crashes before `CreateRecord`. |
| +- Move claims `moving`, then crashes before publishing `record.move`. |
| +- Delete removes the record, then crashes before creating park obligations. |
| +- Abort clears `move`, then crashes before releasing the claim. |
| + |
| +The current worker discovers work through records and skips `Move == nil`: [movespass.go:242](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/movespass.go:242). Neither spec defines a complete recovery owner and replay decision for all these states. “Console: stateless” is false for a claim-only accepted request without durable reconstruction inputs. |
| + |
| +**Fix:** persist operation intent and reconstruction inputs before the first cross-object side effect; define discovery and reconciliation of incomplete claims without relying on an existing record. Specify every ambiguous-write recovery and terminal ordering. A stale finalizer must never clear a newer operation. |
| + |
| +**N5 — P1: lazy legacy adoption does not establish a complete `touched` inventory.** |
| +**A §§7, 9; B §§0.4, 7.12.** |
| + |
| +Before rollout, H moved from UK to US. The old move left the UK replica; current code purges local artifacts and flips the record, [movespass.go:492](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/movespass.go:492), without retiring that source replica. |
| + |
| +A door adopts H with only US in `touched`. Delete parks US and frees the claim. Recreate H in UK; the old replica remains eligible for host-keyed restore, [backend_exec.go:300](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/backend_exec.go:300). It has no move-generation marker, so origin-marker absence does not distinguish it from legitimate origin data. |
| + |
| +**Fix:** complete legacy location discovery and retirement acknowledgement before allowing reuse. Unknown historical coverage must block reuse. A first door cannot certify global cleanliness from the current record region or the console’s own bucket. |
| + |
| +**N6 — P1: parking an active coordination lock makes ordinary retries conflict permanently.** |
| +**A §5.4.3; B §17 I-8.** |
| + |
| +The park acquires a lease and copies every key, including `lock.json`, into its immutable manifest. Renewal changes the source lock ETag. A retry acquires another lock body. The manifest comparison now fails against the worker’s own coordination state, leaving the obligation outstanding. |
| + |
| +Renewal updates the lease identity at [health.go:129](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/health.go:129). Existing mirroring explicitly excludes `lock.json` for this reason: [mirror.go:174](/home/paulca/amadan.net/carlos/platform-moves-design/internal/lease/mirror.go:174). |
| + |
| +**Fix:** exclude live coordination locks from copied data and manifest completeness checks. Release only the current lease handle, conditionally, after durable completion. A historical lock observation may be recorded as evidence, but cannot be a replayable data entry. |
| + |
| +**N7 — P1: one move can reuse its own immutable park manifest for different data.** |
| +**B §§6.4, 7.6, 7.8, 7.9; A’s borrowed park helper.** |
| + |
| +A returning host already has residue on the target. Landing parks that residue into `superseded/<move>/<host>/` and installs new data. Its probe writes, then fails. Rollback cleaning parks the new target replica into the same destination. |
| + |
| +With A’s immutable-manifest rule, cleaning encounters unlisted or changed keys and cannot finish. Overwriting the manifest instead destroys the earlier retirement record. Replica and staging retirement also need distinct mappings. |
| + |
| +**Fix:** use D5’s retirement-event ids and separate artifact subtrees. Test a move back to a previously used region followed by dirty rollback. Unique move ids alone do not cover this case. |
| + |
| +**N8 — P1: status filters do not drain config, adoption or placement work already in flight.** |
| +**A C3/§8; B §§7.3–7.6, 9.1–9.2, K9.** |
| + |
| +A config pass selects A’s ready row and renders its secrets. It stalls. A is deleted and parked; B is created at the same host. The old pass resumes and writes A’s `<host>.config.env`. B can then launch with A’s credentials. |
| + |
| +The write uses the captured route at [syncexec.go:1091](/home/paulca/amadan.net/carlos/platform-moves-design/internal/appconfig/syncexec.go:1091), culminating in the rename at `:1180`. Release adoption similarly changes a host-keyed live symlink at [adopt.go:1045](/home/paulca/amadan.net/carlos/platform-moves-design/internal/release/adopt.go:1045). Its earlier `ready` filter does not protect that later mutation. |
| + |
| +There is also a separate placement writer: [fleets.go:616](/home/paulca/amadan.net/carlos/platform-moves-design/internal/console/fleets.go:616) changes registry placement before [provision.go:853](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/provision.go:853) changes the record. |
| + |
| +**Fix:** make these actors participate in lifecycle exclusion, including draining already-admitted work. Bind host-specific writes to incarnation and operation under the same local mutation guard. Guard placement before **any** app, registry or record mutation. At actual probe spawn, revalidate the complete composed environment and pinned executable, including inherited agent variables after restart. |
| + |
| +**N9 — P1: app purge can destroy the move’s store before encountering the host claim.** |
| +**A §5; B §7.12/K7.** |
| + |
| +The proposed refusal is inside `PurgeApp`/record retirement. The console destroys app stores **before** calling that function: [ownership.go:404](/home/paulca/amadan.net/carlos/platform-moves-design/internal/console/ownership.go:404), followed by `PurgeApp` at `:442`. |
| + |
| +An app with a moving instance can therefore lose its store and credentials before purge reports that the move prevents deletion. Phase 1 permits shared app stores; deferring store migration does not make their destruction safe. |
| + |
| +**Fix:** acquire a durable app-purge reservation and the necessary host lifecycle exclusions before store/email teardown or prefix deletion. Concurrent creation must also be excluded. A read-only “no move currently exists” preflight is insufficient. |
| + |
| +**N10 — P1: waiting out the db-door cache does not drain authorized reads.** |
| +**A §§5.1, 8; B §19.1.** |
| + |
| +Console A authorizes an old-incarnation GET, then stalls before opening the object. Console B begins deletion and waits one cache lifetime. It parks, frees and recreates the host. A resumes and opens the reused LTX coordinate. |
| + |
| +At **`653ad4b1:internal/console/apidb.go:287`**, authorization precedes **`:312`**, the actual `OpenLTXFile`. Cache expiry does not revoke that admitted request or prove that it finished. |
| + |
| +**Fix:** bind reads to immutable object versions/identities, or use distributed read reservations whose completion/expiry is part of retirement. Stop accepting reads and drain them on every console before namespace reuse. Model a stalled handler between authorization and object open, not only an already-streaming response. |
| + |
| +**N11 — P1: pre-flip recovery can reject its own newly acknowledged writes after a crash.** |
| +**B §7.4 `reverting`; contrast §7.8’s corrected recovery journal.** |
| + |
| +A final staging/archive step fails. The source verifies its stopped digests and starts the recovery probe. That probe changes files and acknowledges background work. The agent crashes before opening and recording `aborting`. |
| + |
| +Recovery re-enters §7.4 and compares the changed files against the original stopped digest. It now declares a mismatch and remains stuck. Reinstalling the baseline would lose the probe’s writes. |
| + |
| +The probe runs the real writable application, through [backend_exec.go:912](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/backend_exec.go:912). |
| + |
| +**Fix:** give pre-flip recovery durable `verified → probing → recovered → opened` phases too. After entering `probing`, never reapply the old baseline check as an admission requirement or restore over recovery writes. |
| + |
| +**N12 — P1: the version floor omits an automatic path back to an old executable.** |
| +**A §9; B §§11, 14.3, 15.** |
| + |
| +B names `system apply` and explicit rollback. Boot recovery independently restores `carlos.prev`: [systemapply.go:901](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/systemapply.go:901), calling the shared restore path that copies the old binary at [systemapply.go:817](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/systemapply.go:817). |
| + |
| +A leftover apply journal can therefore restore a pre-floor executable while a host is landing or restoring unless the floor is enforced in this path too. Old reconcile then knows only the ordinary `ready` mint. |
| + |
| +Additionally, B §15 puts flagship rehearsals before floor publication, while §11 requires publication before the first production move. |
| + |
| +**Fix:** enforce the floor in every executable restoration path, including automatic recovery and boot. Validate `.prev` and outstanding update journals before activation. Publish the floor before protected production rehearsals. Define authoritative enrollment of all relevant boxes/consoles and exclusion of old writers; a version report cannot constrain an old executable that ignores the claim. |
| + |
| +**N13 — P2: abort assigns remote parking to an actor without the necessary permission.** |
| +**B §7.11; A C3.** |
| + |
| +The source is told to park target staging into `superseded/`. Under M17 it cannot read target staging and cannot write target `superseded/`; it has only sibling `moves/*` Put/Delete/List. The existing abort only deletes remote staging, [movespass.go:396](/home/paulca/amadan.net/carlos/platform-moves-design/internal/host/movespass.go:396), which explains why its existing authority was sufficient. |
| + |
| +**Fix:** make target staging retirement a durable obligation executed by the target-region actor. The source parks its own snapshots. Abort retains its claim until both acknowledge completion. Do not broaden M17 to cross-region data reads. |
| + |
| +**N14 — P2: a second timer-pruning actor bypasses the freeze.** |
| +**B §9.4/K9.** |
| + |
| +The runner performs its own daily prune at [runner.go:260](/home/paulca/amadan.net/carlos/platform-moves-design/internal/schedule/runner.go:260). `PruneTimers` removes aged completed once-timers even for an alive host: [timers.go:188](/home/paulca/amadan.net/carlos/platform-moves-design/internal/registry/timers.go:188). |
| + |
| +A held source can therefore change its timer snapshot after `stopped`, causing clean recovery’s digest comparison to fail despite no application write. Freezing only declaration convergence and delivery misses this actor. |
| + |
| +**Fix:** make both prune callers respect the operation’s timer freeze, or define a canonical snapshot that explicitly excludes disposable history. Exercise the daily runner sweep during landing and rollback. |
| + |
| +**N15 — P2: the promised cut window still lacks one enforceable budget.** |
| +**B §§7.3 T11, 7.4, 7.6–7.7.** |
| + |
| +T11 reserves one 30-second probe plus 20-second settle, while §7.7 allows three attempts and landing has a separate ten-minute deadline. Those rules permit a successful move substantially beyond an admitted 120-second window. |
| + |
| +The existing health timeout is a per-start bound, [backend_exec.go:36](/home/paulca/amadan.net/carlos/platform-moves-design/internal/activator/backend_exec.go:36), not an end-to-end move deadline. |
| + |
| +**Fix:** persist an absolute cut deadline, allocate remaining time across installation and probe attempts, and begin recovery when it is exhausted. Keep recovery’s deadline separate. State whether the estimate promises one-attempt success or includes permitted retries. |
| + |
| +There are no additional material P3 findings. |
| + |
| +**4. Verdicts** |
| + |
| +| Spec | Verdict | Planning blockers | |
| +|---|---|---| |
| +| **A: host lifecycle claim** | **Not ready** | Incomplete legacy location adoption; missing cross-object recovery; lock-bearing park manifests; stale background writers and db reads; insufficient execution/storage fencing. | |
| +| **B: move-any-app rev 3, Phase 1** | **Not ready** | Unsafe D4/D6 implementations; colliding park transactions; unjournaled pre-flip recovery; abort IAM mismatch; incomplete integration with purge, background passes and automatic executable recovery. | |
| + |
| +A also fails to carry forward the prior **R3-12 fresh-incarnation requirement** explicitly. Both creation helpers still accept caller-provided timestamps—[CreateRecord](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/provision.go:820) and [CreateSidecarRecord](/home/paulca/amadan.net/carlos/platform-moves-design/internal/provision/sidecar.go:322)—while A clears the holder on `free` and retains incarnation-keyed immutable park manifests. Reusing the old creation identity must be prohibited. This is an unresolved prior finding, not counted among the new findings. |
| + |
| +The joint simulation should use the real permission split and include late server-side completion, claim-only operations, legacy residue discovery, delayed config/adoption writes, purge teardown, distributed read reservations, automatic boot recovery, and multiple retirement events within one operation. Randomizing only the named move phases will miss these failures. |
| + |
| +M1–M18 and the reduced follow-on scope can remain unchanged. |
| + |
| +--- |
| + |
| +**FIRST PROMPT:** |
| +Joint read-only review of the host-lifecycle claim and move-any-app specs against this worktree. |
| + |
| +**WHAT:** |
| +Check prior fixes, settle the interfaces, and find composition failures. |
| + |
| +**STATUS:** |
| +Review complete. Neither spec is ready for planning. Workspace unchanged. |
| + |
| +**NEEDED:** |
| +Nothing for this review. |
| + |
| +**RECOMMENDED:** |
| +Revise the shared exclusion and recovery contracts, then run the expanded joint simulation before implementation planning. |
| + |
| +**SESSION:** |
| +Safe to close. Nothing is running; no handoff file was written because the review is read-only. |
| \ No newline at end of file |