amadan
spec: move-any-app rev 4, checked against the executable model (#175)
Answers the joint Astra review (CODEX-FINDINGS-JOINT-R1.md): adopts the adjudicated D1, D3-D8 and I-7 text, takes the staging-work lease in place of rev 3's exception, and fixes the moves-owned findings: sealing staging by version and retiring it after its writers' horizon (N2), a journaled pre-flip recovery that never re-verifies after its probe (N11), a target-owned abort park (N13), a canonical timers digest against the runner's own prune (N14), and one absolute cut deadline that binds every phase before the commit (N15). Written against claim spec rev 2. The model (internal/sim/hostlife) runs 30,000 seeds clean and found 13 faults beyond the review (§14.2.4), among them late replication PUTs landing after a park verified empty, declare-lost on lease expiry under a whole-VM pause, purge missing unclaimed legacy hosts, and a recovery pass that let a stalled purge destroy a new incarnation's store. §19.4 lists the 13 claim changes the model requires, for platform-1e. §14.2.5 records every mutation result, including the 8 rules the model does not yet exercise.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+597
−183
docs/superpowers/specs/2026-10-02-move-any-app-design.md+597 −183
diff --git a/docs/superpowers/specs/2026-10-02-move-any-app-design.md b/docs/superpowers/specs/2026-10-02-move-any-app-design.md| index 492c62423..c91d18fb5 100644 |
| --- a/docs/superpowers/specs/2026-10-02-move-any-app-design.md |
| +++ b/docs/superpowers/specs/2026-10-02-move-any-app-design.md |
| @@ -1,7 +1,26 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-02 |
| -**Revision:** 3. |
| +**Revision:** 4. |
| + |
| +- **Rev 4** is the first revision checked against an **executable model** |
| + instead of a prose round. The joint Astra review of the claim spec (rev 1) |
| + and this spec (rev 3), `CODEX-FINDINGS-JOINT-R1.md` (4316db73), found 12 |
| + new P1s and 3 P2s, and recommended a joint simulation before planning. |
| + Rev 4: |
| + - builds the model: `internal/sim/hostlife/`, a test-only Go package |
| + (§14.2). It encodes claim spec rev 2 (cf3a7861) and this spec, with the |
| + real IAM split, late S3 completion, crashes, partitions, whole-VM |
| + pauses, destroyed and restarted boxes, and old executables. It runs |
| + 30,000 seeds clean, and a mutation harness drops each rule in turn; |
| + - adopts the joint review's adjudicated text for D1, D3 to D8 and I-7, |
| + and answers the findings this spec owns: N2, N11, N13, N14, N15, and the |
| + moves side of the others. Changes are marked "(joint N)"; |
| + - fixes what the model found beyond the review, marked "(model N)" |
| + (§14.2.4); |
| + - lists the claim changes the model requires (§19.3), for platform-1e. |
| + |
| +Earlier revisions: |
| - **Rev 1** (e41c4fef) went to Astra (GPT-6, via codex): 12 P1, 7 P2, 1 P3, |
| "not ready". The findings are in `CODEX-FINDINGS-MOVES-R1.md` (9fbf4afe). |
| @@ -39,8 +58,9 @@ branch `design-nearest-region`. |
| review for the same reason as round 2's P1s; the claim spec supersedes it |
| from its §2 onward (tombstones become the claim's `deleting` and |
| `parking` operations). |
| -- The claim spec, `docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` |
| - at 653ad4b1 on `design-replica-ownership`. |
| +- The claim spec, `docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`, |
| + **rev 2 at cf3a7861** on `design-replica-ownership`. Rev 4 is written |
| + against rev 2. |
| Citations are to this worktree at 7edd4b33 unless they name another branch |
| or repo. |
| @@ -89,29 +109,37 @@ traffic is undone automatically (§7.8); after the target opens, R4 stands. |
| ### 0.4 The host lifecycle claim |
| -From the claim spec (§2 to §9 there), the parts this spec relies on: |
| +From claim spec rev 2 (§2 to §10 there), the parts this spec relies on: |
| - **The object** `control/hosts/<host>.json`, rewritten whole by CAS: a |
| - per-write version `gen`; a `holder` (family, record key, incarnation); an |
| - `op` (`kind`, `id`, `phase`, `journal`); `touched` regions and boxes, |
| - appended **before** the first write there; and `obligations[]`, durable |
| - chores that must finish before the host can become free. |
| -- **Its invariants:** C1 one holder; C2 claim before record on create, |
| - `DeleteIfMatch` under the claim on delete; C3 destructive steps only by |
| - the current op id, holding the location's lease, before `SafeUntil` |
| - (§3.1 there states the clock assumption); C4 admission reads the claim |
| - fresh; C5 revocation needs stop evidence; C6 a read error never acts. |
| + per-write revision `gen` (not a data generation, J-D2); a `holder`; |
| + `op` with `kind`, `id`, `phase`, `intent` (written in the start CAS), |
| + `journal`, `exec` and `participants`; `touched` (with `complete`); |
| + `inventory`; `obligations[]`; the `lost` quarantine; and |
| + `retired_incarnations`. |
| +- **Its invariants:** C1 one holder; C2 intent before effect, a recovery |
| + owner for every state, every CAS conditional on `op.id` as well as the |
| + ETag; C3 storage mutated only by the current operation and only on |
| + **exact object versions**, with a shared staging-work lease for |
| + cross-region staging; C4 fresh admission; C5 revocation needs stop |
| + evidence or a lost-box fence; C6 a read error never acts; C7 |
| + already-admitted work is drained (`hostguard`). |
| - **Op kinds** (§4 there): `moving`, `landing` and `reverting`/`restoring` |
| - belong to this spec, including the admission rule for each phase. One |
| - operation runs at a time, so a delete and a move refuse each other. |
| -- **Stop evidence** (§6 there) recomputed from system state. |
| -- **Retained participant rows** (§8 there) and the protocol floor (§9 |
| - there, which reuses §11's object). |
| + belong to this spec. One operation runs at a time. |
| +- **Mechanisms:** stop evidence from system state (§6.1), parking by exact |
| + version into per-retirement destinations (§6.2), local retirement for both |
| + layouts (§6.3), the host guard (§6.4), door reads pinned to versions |
| + (§6.5), execution leases and declare-lost (§7), the floor on every |
| + executable restore path (§10). |
| This spec's rules for using the claim are K1 to K13 in §19, named "K" so |
| -they never read as the claim spec's own C1 to C6. Where this spec needs |
| -the claim spec to change, §19.3 says so. "Execution holder" below means |
| -the claim's `op.journal.exec` (K1). |
| +they never read as the claim spec's C1 to C7. **Execution holder** below |
| +means the claim's `op.exec` (rev 2 made it a first-class field, as rev 3 |
| +asked). |
| + |
| +The model (§14.2) found that several claim rev 2 rules need changing. |
| +§19.3 lists them; until platform-1e adopts them, this spec states each as |
| +the behaviour it relies on. |
| ## 1. What happened in production |
| @@ -206,9 +234,9 @@ Stated first, designed to, and proved by the simulation in §14.2. |
| holds even when the crashed activator has lost all memory (codex R2-2). |
| The exception is a box that never returns, handled by M16 (§7.10). |
| - **INV-4 Files match the database.** Every start, on any box, uses a files |
| - directory whose generation equals its database's generation, which |
| - equals the generation the claim says is installed on that box. Otherwise |
| - the start is refused (§5.1). |
| + directory whose generation equals its database's generation, and the |
| + generation installed in the box's own bucket. Otherwise the start is |
| + refused (§5.1). |
| Supporting invariants: |
| @@ -230,6 +258,23 @@ Supporting invariants: |
| directory) on any box or bucket except the one the claim names as |
| current. Everything else is parked under the operation id (codex R2-5). |
| +**What the model checks (§14.2).** The coordinator's list for the joint |
| +model, and where each lives: |
| + |
| +| invariant | checked | here | |
| +|---|---|---| |
| +| at most one writer per host, across regions | after every step | INV-1 | |
| +| no acknowledged write lost (database writes and registered timers), except a declared loss | at the end, on the serving box's local state **and** on a cold restore from the bucket | INV-2 | |
| +| no recreated host sees a previous incarnation's database, key or config | at every spawn | INV-4, C1 | |
| +| no live-namespace residue after an operation ends | at the end, every bucket and box | INV-10 | |
| +| claim and record agree after recovery | at the end | C2 | |
| +| every crash converges with no human, except declared loss (M16) | at the end: the run must reach a quiescent state | INV-3 | |
| +| an app store exists while its host is held for anything but delete | after every step | claim §5.3 | |
| +| a door read returns only the incarnation it authorized | at every open | claim §6.5 | |
| +| a commit happens within the cut budget | at the commit | INV-9 | |
| +| no IAM violation | at every request | M17 | |
| +| no stuck recovery | after every step | INV-3 | |
| + |
| ## 5. The handoff protocol |
| ### 5.1 Generations and markers (codex R2-6, R2-9) |
| @@ -287,11 +332,25 @@ Round 2 showed two gaps: a flat child's descendant that outlives it |
| (`childProc.Stop` waits for the main process only, `backend_exec.go:1502-1543`), |
| and evidence that cannot be produced after an agent restart, because |
| `FenceAndStop` returns `ErrStopUnproven` when it has neither an entry nor a |
| -remembered stop history (`maintenance.go:90-100`). The claim spec §6 |
| -defines evidence the same way this section does, from system state; this |
| -section adds the strict-spawn and stray-process conditions it still lacks |
| -(§19.3 D3). Rev 3 defines evidence |
| -from **durable, observable state**, never from memory. |
| +remembered stop history (`maintenance.go:90-100`). Evidence comes from |
| +**durable, observable state**, never from memory. Claim spec rev 2 §6.1 |
| +adopts the joint review's D3 text, and this section follows it (joint D3): |
| + |
| +> 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. |
| + |
| +and |
| + |
| +> 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. |
| + |
| +`PrepareStrict` refuses a populated group (`internal/cgroup/strict_linux.go:206`), |
| +so the cleanup-only operation is a separate call, `cgroup.ReopenAndDrain`. |
| **Every spawn under a move is strict.** Flat children already run in a |
| per-host cgroup, `carlos-exec@<host>` under the agent's delegated subtree |
| @@ -347,6 +406,17 @@ and timers digests. It then CASes the claim's execution holder to `none` |
| (§19 K3). The next holder reads the evidence and the claim before it starts |
| anything. |
| +**Evidence also starts a clock (model 1).** Ordinary replication is the one |
| +storage write claim C3 does not bind to a version: the serving process's |
| +litestream PUTs go to reused keys (litestream v0.5.14 `LTXFilePath`, names by TXID range, |
| +restarting at 1 for a new lineage). A PUT signed before the evidence can |
| +still complete afterwards. So every retirement of a location that a |
| +replicator wrote acknowledges only after a verification listing taken |
| +later than `evidence time + H`, where H is the late-completion horizon |
| +(S3 refuses a request whose signature is more than 15 minutes old, so H is |
| +15 minutes plus the longest request). The model drops this rule and finds |
| +residue in a freed host's namespace. |
| + |
| ## 6. State inventory |
| ### 6.1 Files on a box (codex R2-9) |
| @@ -397,21 +467,44 @@ The `timers` table (`registry.go:565-579`) is carried as a snapshot (§9.4). |
| ### 6.4 Parking |
| -Phase 1 reuses #199's park helpers with an operation-scoped destination: |
| - |
| -- **bucket park:** per-key copy, then a manifest of every key and size, |
| - then delete the keys named in the manifest (#199 §3.3). Never |
| - `MirrorPrefix`, which deletes destination-only objects |
| - (`internal/lease/mirror.go:222`). |
| -- **local park:** `rename` into `<DataDir>/.parked/<name>/<host>/` (#199 |
| - §3.4). |
| - |
| -Destinations are `superseded/<op id>/<host>/` and |
| -`.parked/superseded-<op id>/<host>/`. An op id is unique, so no two parks |
| -collide and no park destination is an ancestor of a live prefix (codex 8). |
| -**A park is its own journaled phase**, completed (manifest written and |
| -every named key deleted) before any install into the vacated namespace |
| -begins (codex R2-6). |
| +Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| +(§6.3 there), with the move's own destinations: |
| + |
| +- **One destination per retirement event (joint D5, N7).** Superseded data |
| + goes to `superseded/<op id>/<host>/<retirement id>/{instances,moves}/`, |
| + and local state to `.parked/superseded-<op id>/<host>/<retirement id>/`. |
| + The landing's park of an earlier stay, a failed target's cleanup, the |
| + source's retirement after commit and each staging retirement are |
| + separate events with separate manifests, even inside one operation. The |
| + model drops the retirement ids and the park never finishes: the second |
| + event finds the first event's immutable manifest and stops on unlisted |
| + keys. |
| +- **Exact versions (joint N1).** The snapshot takes every version under the |
| + location, noncurrent included; copies name `versionId`; deletes name |
| + `VersionId`. The model replaces version deletes with bare-key deletes |
| + (delete markers on a versioned bucket) and finds parks that never |
| + finish, in 2,311 of 3,000 seeds. |
| +- **The live lock is not data (joint N6).** The parker takes the location's |
| + replica lease first, and renews its own `lock.json` while it works. That |
| + key is excluded from the snapshot, the manifest and the emptiness check, |
| + and released by the parker's own version after the completion CAS. The |
| + model includes the lock and the park never finishes. |
| +- **Progress accumulates (model 2).** A copy's destination key carries the |
| + source version id, so a retry skips copies that landed and the manifest is |
| + written once every copy exists. Restarting the snapshot from scratch on |
| + every retry, with many versions and late completions, does not converge |
| + in the model. |
| +- **Verify after the horizon (model 1).** A park acknowledges only after a |
| + final listing taken after `max(evidence time, the region's quiet time) + |
| + H` is empty (§5.3). Anything found then is parked as a further retirement |
| + event. |
| +- **Local retirement** takes the host guard and writes a retired marker |
| + first (claim C7), so a stale background write for that incarnation is |
| + refused. |
| + |
| +No park destination is an ancestor of a live prefix (codex 8). **A park is |
| +its own journaled phase**, complete before any install into the vacated |
| +namespace begins (codex R2-6). |
| ## 7. The move |
| @@ -483,6 +576,34 @@ a snapshot or `move.json`. Landing installs only `replica/` into |
| `instances/<host>/` (§7.6). Receipts are `move-receipts/<host>/<move id>.json` |
| in the source bucket. |
| +**The staging-work lease, sealing and draining (joint D4, N2).** M17's |
| +push-only grant stays: the source can put and delete in the target's |
| +`moves/*` but cannot read it, so it cannot hold the target's `lock.json`. |
| +Exclusion between staging writers uses the claim's shared staging-work |
| +lease in the deployment bucket, keyed by target region and host (claim C3). |
| +Every round, the final round and every staging retirement take it first, |
| +then revalidate the claim's op id and phase. That is enough for two workers |
| +of one operation (a restarted agent beside a stalled one), but a lease |
| +cannot fence a request already signed, so staging safety rests on two |
| +further rules: |
| + |
| +- **Seal by version.** Each PUT's response carries the new object's |
| + `VersionId`. The final round records the exact versions of |
| + `replica/…`, `files/…` and `timers/…` in the claim's op journal: the |
| + **seal**. Landing copies those versions by `versionId` and nothing else. |
| + A stale round that lands later creates a newer version, which the seal |
| + does not name, or a delete marker, which a copy by `versionId` ignores. |
| + So nothing has to be drained for correctness. |
| +- **Retire staging after its writers' horizon.** Staging is retired (by |
| + the target-region box, §7.11) only after `seal time + staging-lease TTL + |
| + H`, when no writer that held the lease can still have a request in |
| + flight. |
| + |
| +The model exercises the stale second worker and catches the revalidation |
| +rule (§14.2.5). It does not, even at 30,000 seeds, produce a staging write |
| +that lands after the seal, so the seal and the staging horizon are **not |
| +yet proven by the model**; §14.2.5 records the gap. |
| + |
| **Snapshot rounds (source).** Each round the source builds the files |
| archive (§8) when the plaintext digest changes, and publishes its **launch |
| report** `moves/<acct>/<app>/<host>/<move id>/source.json`: every variable |
| @@ -508,12 +629,17 @@ placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`: |
| | T8 one owner | exactly one hosting box publishes the target placement | |
| | T9 claim | the claim is `moving` with this move id, its holder is the record's incarnation, and this region and box are in `touched` (added by CAS before the first staging write, claim spec §2) | |
| | T10 return lane | this box can put and delete `moves/_lane/<move id>` in the source's bucket (M17) | |
| -| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + install copy (replica size at the measured in-bucket copy rate) + restore (replica size at the measured restore rate) + render + one probe attempt (30 s + the 20 s settle). The estimate is recorded per phase as `cut_budget_s` | |
| +| T12 quiet region | the claim's `quiet_after` for the target region (CC1) has passed, so the landing's park of an earlier stay never waits inside the cut window. A move back into a region the instance left within H waits at `ready`, not mid-cut | |
| +| T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + install copy (replica size at the measured in-bucket copy rate) + restore (replica size at the measured restore rate) + render + **every permitted probe attempt** (three times 30 s, plus the 20 s settle) (joint N15). The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) | |
| **Source readiness.** S1: a probe request (§7.7) to the readiness path on |
| the instance as it runs today answers 200 to 399 from its own process |
| (codex 14); an app that fails is refused with "declare `moves.ready_path`". |
| -S2: its next spawn is strict (§5.3). |
| +S2: its next spawn is strict (§5.3). **S1 is load-bearing (model 3):** a |
| +source box that cannot run the instance now (in the model, one without |
| +`CARLOS_SECRETS_KEY`, finding 2b's state) can be cut, and its pre-flip |
| +recovery then never passes its probe. The model drops S1 and finds moves |
| +stuck in `reverting`. |
| `ready` requires a round at most the 16 MiB bar, a passing target report |
| and source readiness, each under 10 minutes old. |
| @@ -532,30 +658,38 @@ Each phase is written to `cut_phase` before its side effects. |
| | `archived` | source | build the final archive from the stopped directory, seal, write create-only to `move-snapshots/`, record both digests, copy into `files/` | over the cap, a special file, or its budget: `reverting` | |
| | `flipped` | source, the flip CAS | `region = to`, `state = landing`, `landing_deadline`; and the claim: `op.kind = landing`, execution holder = target (§19 K4) | | |
| -Every phase's budget comes from `cut_budget_s`. Exceeding a phase's budget |
| -starts its recovery; the recovery's own deadlines (`reverting` 15 min, |
| -`landing_deadline` 10 min) are separate from the promised window (codex |
| -R2-10). The source does not purge its database or files at the cut; |
| -finalization parks them (§7.9). |
| - |
| -**`reverting` (pre-flip recovery, codex 4).** The record still names the |
| -source. The source CASes the claim to `op.kind = reverting` with itself as |
| -execution holder, switches the row to `restoring` with |
| -`hold_op = move id`, and then: |
| - |
| -- **from `stopping`:** stop evidence was never obtained, so something may |
| - still run. The source keeps computing evidence (§5.3) and starts nothing |
| - until it has it. There is no files baseline to check, because the move |
| - has not touched the files; the app's own last writes stand. If evidence |
| - stays unobtainable for 15 minutes (a stray process), `stuck`, held, |
| - paged; |
| -- **from `stopped`, `staged` or `archived`:** it checks its files and timers |
| - against the digests it recorded at `stopped` (rev 2 used the archive |
| - digest, which did not exist yet when `staged` failed: codex R2, R1-4 |
| - disposition). |
| - |
| -It then probes (§7.7), opens with the conditional write, and CASes the |
| -record to `aborting`. Fifteen minutes of failed probes: `stuck`, held. |
| +**One absolute deadline (joint N15).** Admission writes |
| +`cut_deadline = cut_at + the whole budget` into the op journal. Every |
| +phase before the commit checks it, on the source and on the target alike; |
| +the commit CAS itself is conditional on `now ≤ cut_deadline`. Exceeding it |
| +starts recovery: `reverting` before the flip, a rollback after it. The |
| +deadline bounds the **commit**, which is what the M2 promise is about: |
| +after the commit the target is authoritative, and its open waits only on |
| +its own box. The recovery's own deadlines (`reverting` 15 min, the release |
| +deadline 15 min) are separate from the promised window (codex R2-10). |
| +Rev 3 checked the deadline only while probing; the model found commits far |
| +past the budget after slow installs, and finds them again when the deadline |
| +is dropped. The source does not purge its |
| +database or files at the cut; finalization parks them (§7.9). |
| + |
| +**`reverting` (pre-flip recovery, codex 4, joint N11).** The record still |
| +names the source. The source CASes the claim to `op.kind = reverting` with |
| +itself as execution holder, holds the row as `restoring` with |
| +`hold_op = move id`, and runs a **journaled** recovery, |
| +`op.journal.rev_phase`: |
| + |
| +| phase | action | replay | |
| +|---|---|---| |
| +| `evidence` | entered from `stopping`: evidence was never obtained, so something may still run. Compute it (§5.3) and start nothing until it holds. No files baseline is checked, because the move has not touched the files | replayable | |
| +| `verify` | entered from `stopped`, `staged` or `archived`: check files and timers against the digests recorded at `stopped` | replayable **until `probing` is journaled** | |
| +| `probing` | render held config and materialize the release (§7.7), then probe | restarts only the probe. **Never re-runs `verify`**: the probe's process may have written, and those writes are now the authoritative state (INV-2) | |
| +| `probed` | conditional open on `hold_op = move id` | replayable | |
| +| `opened` | the claim waits for the staging obligation (§7.11), then releases to `serving` | | |
| + |
| +Rev 3 compared digests again on re-entry, so a crash after the recovery |
| +probe had written left the move stuck on a "mismatch" that was really the |
| +app's own work (joint N11). The model reproduces that when it drops the |
| +journal. Fifteen minutes of failed probes: `stuck`, held. |
| **Source digests at `stopped`.** The source records `files.plain` (§8.3) and |
| `timers_sha256` at `stopped`, before any phase that can fail, so every |
| @@ -598,6 +732,16 @@ rollback (§7.8). |
| `ProbeWake(host, op)`, legal only on a row held with `hold_op = op` and |
| only while the claim names this box as execution holder: |
| +- **first, render held config and materialize the release** (`RenderHeld`, |
| + `MaterializeHeld`, §9.1, §9.2), for every kind of probe: the landing, the |
| + source's pre-flip and rollback recoveries, and a push (model 4). Config |
| + sync and adoption skip held rows, so an instance created shortly before |
| + the operation began may never have been rendered. In the model, pushes |
| + and reverts of such an instance never pass their probe until this rule is |
| + applied to every probe; |
| +- **check the actual launch environment at spawn** (joint N8): recompose it |
| + exactly as the spawn will, including inherited agent variables after any |
| + restart, and require the pinned input versions and executable; |
| - a strict spawn (§5.3), with `CARLOS_MOVE_PROBE=1` (advisory); |
| - the answer must come from the spawned tree: the socket peer's |
| credentials (`SO_PEERCRED`) name a process in the host's cgroup; |
| @@ -704,30 +848,62 @@ runs anywhere. It converges when the target returns (INV-3). |
| resolve --host <h> --retry` reruns the recovery's `probing` phase. |
| - **`--declare-lost <box>` (M16)**, operator-only. `carlos move resolve |
| --host <h> --declare-lost <box>` is the move-facing form of the claim |
| - spec's `carlos ops host resolve <host> --declare-lost <box>` (§4 there), |
| - which removes the box's local obligations; for a move it also does the |
| - following, with Astra's round-2 conditions: |
| - - **refused after `committed`**, and refused unless the named box is the |
| - exact participant that owes the missing evidence for this move; |
| - - **execution fencing is established independently first:** the verb |
| - CASes the claim's execution holder away from the lost box to `none`, |
| - with a `lost` entry naming it. Every box checks the claim before any |
| - spawn (§19 K6) and, on reading a claim that does not name it, kills the |
| - host's tree (§5.3 step 1) before doing anything else. So a box that was |
| - only partitioned cannot resume writing when it returns; |
| - - **recover durable data first:** if the target had reached `returned`, |
| - the dirty return is used and nothing is lost; if the source is the |
| - lost box, the verb is refused (its copy is the only authority); |
| - - otherwise it proceeds as a clean rollback, after a confirmation that |
| - names the box, the flip time, and that anything the target wrote since |
| - then is lost (M-C18). |
| + spec's `carlos ops host resolve <host> --declare-lost <box>` (§7.2 |
| + there). The joint review's D6 text governs it (joint D6, N3): |
| + |
| + > A claim CAS is bookkeeping, not 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. |
| + |
| + **This spec takes the first branch only: compute fencing (model 5).** The |
| + verb requires the operator's cloud credentials to show the box `stopped` |
| + or `terminated`, verified through the cloud API by the CLI. An expired |
| + execution lease is not enough, even with the self-fencing watchdog: a |
| + whole-VM pause stops the watchdog with everything else, and on resume the |
| + application can write before the watchdog fires. The model allows the |
| + lease-expiry branch and finds two writers when a frozen target resumes |
| + beside the recovered source (1 seed in 30,000; 2 when the watchdog also |
| + runs inside the agent, so an agent pause defeats it too). The lease stays useful for liveness: a |
| + partitioned or hung participant fences itself. |
| + |
| + It is legal in exactly these states, and refused otherwise: |
| + - **the target owes stop evidence** (landing, or a rollback before the |
| + target released): it proceeds as a clean rollback, after a |
| + confirmation naming the box, the flip time, and that the target's |
| + writes since then are lost (M-C18); |
| + - **the target released dirty but had not returned its writes** (model |
| + 6): the same, and the confirmation says so. Rev 3 missed this state; |
| + the model finds a move waiting forever on a return that a destroyed box |
| + can never send; |
| + - **a destroyed box owes only local chores** (`park-local`): the |
| + obligation is removed and nothing else changes. This one is legal |
| + after commit, because no data authority is involved (model 6); |
| + - refused after `committed` in the first two states, refused for the |
| + source, refused for any box that is not that exact participant. |
| + |
| + The box goes on `lost`. **A returning box is quarantined** (claim §7.2): |
| + before anything else it retires every local artifact for the host under |
| + the host guard, and only then can an operator `--readmit` it. The model |
| + starts stopped boxes again after they were declared lost; without the |
| + quarantine they would keep stale local state for the host. |
| ### 7.11 Abort |
| Legal in `preparing`, `ready`, and `cutting` with `cut_phase = requested` |
| -(CAS). The source parks `moves/<host>/<move id>/` and its snapshots into |
| -`superseded/<move id>/` (unreferenced, so a failed park is retried, never |
| -dangerous), clears `move`, and releases the claim to `serving`. |
| +(CAS). A move whose readiness never comes aborts itself after a bound, so |
| +an unreachable target never needs a human. |
| + |
| +**Who retires what (joint N13).** The source cannot read the target's |
| +`moves/*` and cannot write the target's `superseded/` (M17 grants it Put, |
| +Delete and prefix-scoped List on `moves/*` only), so it cannot park target |
| +staging. Abort therefore adds a `park-staging` obligation **owned by the |
| +target region's box**, not before the staging horizon of §7.3. The source |
| +parks its own snapshots. The claim stays `moving` until every obligation |
| +has acknowledged, then releases to `serving`. The model gives the source |
| +the target's park and records an IAM violation on every abort. |
| ### 7.12 Deletes and parks under the claim |
| @@ -736,6 +912,19 @@ dangerous), clears `move`, and releases the claim to `serving`. |
| they cannot start while a move op holds it (§19 K7). A purge of an app |
| with a moving instance waits. An operator who must delete aborts first, |
| or waits for the commit or rollback to finish. |
| +- **App purge (joint N9, model 7, 8).** Claim §5.3 reserves the app first, |
| + then claims every host, then tears down stores. The model found two more |
| + rules it needs. **Purge adopts first:** a legacy host of the app with a |
| + record but no claim yet is invisible to a purge that looks only at |
| + claims, so the purge tore down a store under a serving instance; purge |
| + must run the one adoption routine (claim §9) for every unclaimed record of |
| + the app before deciding. **The reservation is the purge's journal:** the |
| + console's recovery pass finished a stalled purge's delete and freed the |
| + host, `free` dropped the reservation, a create for the same app went |
| + through, and the stalled purge then tore down the new incarnation's |
| + store. The reservation records the purge's phase; recovery drives those |
| + phases in order; only the purge's own completion removes it, never |
| + `free`. |
| - **Recreate during a move** cannot happen: create requires the claim free |
| or absent (claim spec C2). |
| - **A delete after a move** parks every region in `touched.regions` |
| @@ -843,6 +1032,21 @@ version)` stages exactly the pinned release (`move.inputs.release`). |
| inserts in one transaction, preserving `next_at`, `due_at`, `attempts` |
| and `registration`. `UpsertTimer` resets them on rearm |
| (`internal/registry/timers.go:46-55`), so it is not used here. |
| +- **The runner's own prune (joint N14).** A second actor deletes timer |
| + rows: the runner's daily sweep (`internal/schedule/runner.go:260`), whose |
| + `PruneTimers` removes aged completed once-timers even for a live host |
| + (`internal/registry/timers.go:183`). It cannot be frozen without stalling |
| + every other host, so the **snapshot is canonical instead**: the timers |
| + digest covers active rows and their bookkeeping, and excludes disposable |
| + history (completed once-timers). Pruning history therefore never changes |
| + the digest a clean recovery compares. The model includes history in the |
| + digest and finds clean rollbacks stuck on a "mismatch" the runner caused; |
| + it lets a held row's refused deliveries advance bookkeeping and finds the |
| + same. |
| +- **Carried timers are acknowledged state.** A once-timer the app |
| + registered is a write the app was told succeeded. The model counts it as |
| + one for INV-2, and finds timers lost when the files marker is written |
| + before the timers are imported (R2-6). |
| - Declared schedules converge again once the claim returns to `serving`. |
| ### 9.5 Edge |
| @@ -889,9 +1093,17 @@ reach it through its config bundle, opened with the box's |
| console are at or above it, and every box is claim-aware (§19 K10). |
| - Before the first production move the deployment writes |
| `control/moves-protocol.json` `{"min": 1, "min_release": "vX.Y.Z"}`, |
| - create-only. `carlos system apply` and `carlos system rollback` refuse a |
| - release below it, and any downgrade on a box that is a participant in a |
| - claim held as `moving`. The console roll recipe states the same floor. |
| + create-only. **Every path that activates an executable** refuses a |
| + release below it: `carlos system apply`, explicit rollback, and |
| + **automatic boot recovery** of `carlos.prev` (`internal/host/systemapply.go:901`, |
| + restoring through `:817`), which validates `.prev` and any outstanding |
| + update journal before activating (joint N12; claim §10). Any downgrade of |
| + a box that is a participant in a held operation is refused. The console |
| + roll recipe states the same floor. The model lets a reboot restore an old |
| + executable and fails in 2,651 of 3,000 seeds, mostly as parks an old |
| + executable can never let finish. |
| +- **The floor is published before any protected production rehearsal** |
| + (joint N12). Rev 3's rollout order had it the other way round (§15). |
| ## 12. The operator surface (M16, M18) |
| @@ -942,47 +1154,190 @@ with a forked descendant that closes its descriptors and outlives its |
| parent; the start check; `RenderHeld`, `MaterializeHeld`, `ReplaceTimers`; |
| reconcile keeping participant rows. |
| -### 14.2 The randomized crash simulation |
| - |
| -A Go test that drives the **real** transition functions and worker phase |
| -functions through injected interfaces, at the granularity of **individual |
| -side effects**, never whole phases (codex R2, simulation note). Actors: |
| -console, the claim, source and target agents, the deadline sweep, and the |
| -application's process tree on whichever box runs it. |
| - |
| -The model contains: |
| - |
| -- the app's own background work, writing the database and an external |
| - ledger while running, including during probes and source recovery; |
| -- **descendants that outlive the main process** (codex R2-1); |
| -- **activator restarts with empty memory** (codex R2-2); |
| -- stalled workers whose children keep running; |
| -- scheduler deliveries in flight across the hold; |
| -- config, adoption, edge reloads with `RetireExcept`, reconcile mints and |
| - removals, **including reconcile running before the target's release** |
| - (codex R2-4); |
| -- versioned buckets; |
| -- forged evidence and reports with a wrong op id or incarnation; |
| -- delete and recreate attempts at every step, and **after a rollback** |
| - (codex R2-5); |
| -- **crashes between a marker's publication and the next write** (codex |
| - R2-6); |
| -- downgrades to a pre-floor binary. |
| - |
| -Assertions: INV-1 and INV-5 after every step; INV-2, INV-3, INV-4, INV-7, |
| -INV-8, INV-9 and INV-10 at the end of every run. 2,000 seeds in the gate; |
| -200,000 nightly. |
| - |
| -**Mutation checks** (each must fail within the gate's seeds): start on a |
| -deadline without evidence; accept evidence while a descendant lives; treat |
| -a missing entry as stopped; open before commit; open without the `hold_op` |
| -condition; discard target writes; reinstall during source recovery after |
| -its probe; let reconcile retire the target row before release; skip the |
| -target's replica park on rollback; write `.files-gen` before the timers; |
| -replay install after `probing`; skip the start check; let the runner |
| -advance a held row; mirror over `files/`; re-seal on replay; skip the |
| -pinned-input check at admission; skip the protocol floor; let a delete |
| -proceed while the claim is `moving`. |
| +### 14.2 The executable joint model |
| + |
| +Built for rev 4, as the coordinator directed and the joint review |
| +recommended: `internal/sim/hostlife/`, a deterministic randomized Go |
| +simulation. **It is test-only**: every file is a `_test.go` file, so |
| +`go build ./...` never sees it, and it imports only the standard library. |
| +It encodes claim spec rev 2 (cf3a7861) and this spec as they would be |
| +implemented, and every rule is a named, mutable guard (`rules_test.go`). |
| + |
| +#### 14.2.1 Running it |
| + |
| +``` |
| +go test ./internal/sim/hostlife/ # the gate: 300 seeds, about a second |
| +HOSTLIFE_SEEDS=30000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v -timeout 60m |
| +HOSTLIFE_SEED=1796 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v # one seed, full trace |
| +``` |
| + |
| +Mutation checks run in a scratch copy of the tree, never in place: |
| +`internal/sim/hostlife/mutate.sh <seeds> [rule | a,b ...]` copies `go.mod`, |
| +`go.sum` and the package to a scratch directory per rule, sets |
| +`var mutated = "<rule>"` (or `"a,b"` for a pair), runs the seeds, reports |
| +CAUGHT or MISSED, and deletes the copy. Rules run in parallel. |
| + |
| +#### 14.2.2 What it models |
| + |
| +- **State.** The claim object (CAS on its revision, op id conditions), |
| + records, the console's purge reservations and app stores, three |
| + regions' **versioned** data buckets, and each box's registry row, local |
| + database, files directory, `config.env`, live link, timers, processes, |
| + retired markers and execution-lease file. |
| +- **The real permission split.** A box has full rights on its own bucket; |
| + on another region's bucket only Put, bare Delete and CopyObject **into** |
| + `moves/*` from its own bucket. No Get, no version listing, no version |
| + delete. Every request is checked; a violation is an invariant failure. |
| +- **Late S3 completion.** A request completes at once (70%) or is |
| + "submitted, client cancelled, completed later", within a long-tailed |
| + horizon, after the issuer has moved on, crashed or been replaced. |
| +- **Box faults.** Agent crash (flat children die with the service, nested |
| + ones survive, memory is lost), reboot, whole-VM freeze, agent-only |
| + pause, partition from the control bucket, clock skew, destruction (a |
| + stopped instance) followed by either replacement or a restart with the |
| + old disk, and boot recovery to an old executable. |
| +- **The application.** Main processes and descendants (strict or escaped) |
| + that write the database and register once-timers on their own, so |
| + writes happen during probes and recoveries. |
| +- **Actors.** Create, delete, purge (store teardown included), push, the |
| + db door (authorize, stall, open), wake, idle stop, replication, |
| + reconcile (with legacy adoption), config sync and release adoption |
| + (each with a decision taken now and acted on later), the timer runner |
| + (delivery and its own prune), the self-fencing watchdog, the move worker |
| + (all of §7), rollback (clean and dirty), abort, a stalled second worker |
| + replaying an old read, the console's claim-recovery pass, and an |
| + operator (declare-lost, readmit). |
| +- **Two phases per seed.** 2,000 chaos steps with user operations and |
| + faults, then up to 6,000 calm steps: faults linger for a while (so the |
| + operator meets a frozen or partitioned participant), then heal; stopped |
| + boxes return or are replaced; ops gives every box its secrets key. |
| + |
| +#### 14.2.3 Invariants and results |
| + |
| +The invariants are the table at the end of §4. Each run must also reach a |
| +quiescent state: claim at rest, no obligations, record agreeing, the |
| +serving box able to start, and nothing left anywhere else. |
| + |
| +**30,000 seeds: zero violations** on the final model (101 s). Across those |
| +seeds: 772 completed moves, 784 clean rollbacks, 54 dirty rollbacks, 294 |
| +pre-flip reverts, 153 declared losses, 11,063 aborts (mostly targets |
| +without a secrets key, which T2 refuses until ops installs one), 19,735 |
| +pushes and 50,752 delete-park-free cycles. |
| + |
| +#### 14.2.4 Faults the model found beyond the joint review |
| + |
| +Each was a failing seed first, then a rule; each rule's mutation is in |
| +§14.2.5. |
| + |
| +| id | fault | fix | owner | |
| +|---|---|---|---| |
| +| model 1 | A replicator's PUT signed before stop evidence landed after a park had verified the prefix empty, leaving residue in a freed host's namespace. Claim C3's "late completion is harmless" does not hold for its own replication exception | verify after `evidence + H` (§5.3, §6.4) | claim | |
| +| model 2 | A park that restarts its snapshot on every retry never finishes with many versions and late completions | destinations keyed by source version; skip copies that landed (§6.4) | claim | |
| +| model 3 | A source that cannot run the instance (no secrets key) was cut, and its pre-flip recovery could never pass | S1 is a hard gate (§7.3) | moves | |
| +| model 4 | Pushes and reverts of an instance created just before the operation never passed their probe: the passes skip held rows | every probe renders held config and materializes the release (§7.7) | moves, push | |
| +| model 5 | Declare-lost on an expired execution lease let a frozen target resume beside the recovered source | compute fencing only (§7.10) | claim | |
| +| model 6 | A target that released dirty and was destroyed before returning left the move waiting forever; a destroyed box owing only local chores blocked release | declare-lost covers both (§7.10) | claim, moves | |
| +| model 7 | A purge that looked only at claims missed an unclaimed legacy record of the app and tore down its store while it served | purge adopts first (§7.12) | claim | |
| +| model 8 | The recovery pass freed a purged host, `free` dropped the reservation, a create slipped in, and the stalled purge destroyed the new store | the reservation is the purge's journal (§7.12) | claim | |
| +| model 9 | A stale local execution-lease file kept self-fencing a box after its operation ended | a fresh read with no operation ends the fence | claim | |
| +| model 10 | An adopted legacy host kept pre-rollout residue in other regions for as long as it served | discovery parks at adoption; `touched.complete` after (§19.4) | claim | |
| +| model 11 | The purge path adopted without discovery | one adoption routine for every actor | claim | |
| +| model 12 | A hold left behind by a finished operation (a revert re-held its row after opening) blocked serving | reconcile releases a hold whose operation ended | claim | |
| +| model 13 | The cut deadline, checked only while probing, let slow installs commit far past the budget | every phase before the commit (§7.4) | moves | |
| + |
| +#### 14.2.5 Mutation results |
| + |
| +Every rule was dropped in turn, in a scratch copy, on one model version: |
| +3,000 seeds each, then 30,000 seeds for every rule not caught at 3,000, |
| +then pairs for rules that looked like double protection. The full |
| +harness output is summarized here; seed numbers reproduce any line with |
| +`HOSTLIFE_SEED`. |
| + |
| +**Caught alone: 30 of 48 rules.** |
| + |
| +| rule | seeds failing | what the model finds | |
| +|---|---|---| |
| +| `recovery-pass` (claim C2, §8) | 1,474 / 3,000 | creates and deletes stranded mid-operation never converge | |
| +| `fresh-incarnation` (claim §5.1, R3-12) | 467 / 3,000 | a reused identity meets its own retired marker; the host never serves again | |
| +| `legacy-discovery` (CC4) | 10 / 3,000 | legacy residue in a region the host does not serve | |
| +| `park-by-version` (claim C3, J-N1) | 2,311 / 3,000 | parks never finish | |
| +| `park-all-versions` (claim §6.2) | 572 / 3,000 | parks never finish (older versions resurface) | |
| +| `park-skip-lock` (claim §6.2, J-N6) | 3,000 / 3,000 | parks never finish (the parker's own lock) | |
| +| `retirement-ids` (claim §6.2, J-D5, J-N7) | 214 / 3,000 | parks never finish (one manifest, two events) | |
| +| `quiet-before-ack` (CC1) | 16 / 3,000 | residue after a park, from late replication PUTs | |
| +| `hostguard` (claim C7, J-N8) | 30 / 3,000 | an instance starts with another incarnation's `config.env` | |
| +| `purge-reserve-first` (claim §5.3, J-N9) | 2,300 / 3,000 | stores destroyed under held hosts | |
| +| `purge-adopts` (CC6) | 17 / 3,000 | a store destroyed under a serving legacy host | |
| +| `purge-journal` (CC7) | 6 / 3,000 | a new incarnation's store destroyed by a stalled purge | |
| +| `door-by-version` (claim §6.5, J-N10) | 1 / 3,000 | a door read returns another incarnation's data | |
| +| `evidence-whole-tree` (claim §6.1, J-D3) | 5 / 3,000 | two writers; lost writes | |
| +| `evidence-from-state` (claim §6.1, R2-2) | 2,999 / 3,000 | evidence never comes after an agent restart | |
| +| `floor-boot-recovery` (claim §10, J-N12) | 2,651 / 3,000 | old executables break parks and admission | |
| +| `participant-rows` (claim §2, R2-4) | 10 / 3,000 | source recovery stuck | |
| +| `revalidate-before-effect` (claim C3, J-N2) | 40 / 3,000 | a stalled worker's effects lose acknowledged writes | |
| +| `declare-lost-compute` (CC5, J-D6, J-N3) | 1 / 30,000 | two writers after a frozen target resumes | |
| +| `lost-quarantine` (claim §7.2, CC12) | 2 / 30,000 | a returning box keeps stale local state | |
| +| `cut-deadline` (§7.4, J-N15) | 60 / 3,000 | commits past the budget | |
| +| `revert-journal` (§7.4, J-N11) | 28 / 3,000 | pre-flip recovery stuck on its own writes | |
| +| `rollback-journal` (§7.8, R2-3) | 9 / 30,000 | rollback recovery stuck | |
| +| `dirty-return` (§7.8, INV-2) | 2 / 3,000 | the target's acknowledged writes lost | |
| +| `target-park` (§7.8, R2-5) | 8 / 3,000 | a rolled-back target's replica left live | |
| +| `abort-target-owner` (§7.11, J-N13) | 1,084 / 3,000 | IAM violations | |
| +| `timer-freeze` (§9.4, J-N14) | 10 / 3,000 | clean recovery stuck | |
| +| `timer-canonical` (§9.4, J-N14) | 6 / 3,000 | clean recovery stuck | |
| +| `markers-last` (§7.6, R2-6) | 1 / 3,000 | an acknowledged timer lost | |
| +| `source-readiness` (§7.3, S1) | 14 / 3,000 | pre-flip recovery stuck | |
| + |
| +**Caught only in pairs: 8 rules (double protection).** Each is covered by |
| +its partner; both stay, because the model cannot prove that the partner |
| +holds in every real case. |
| + |
| +| pair | seeds failing (30,000) | what the model finds | |
| +|---|---|---| |
| +| `files-carried` + `start-check` | 1,102 | **the kpmg outage**: the app mints a new `instance.key` over data sealed with the old one | |
| +| `strict-spawn` + `evidence-whole-tree` | 313 | two writers | |
| +| `restore-lineage-filter` + `quiet-before-ack` | 207 | residue | |
| +| `touched-incomplete` + `legacy-discovery` | 5,305 | a freed host's residue | |
| +| `commit-before-open` + `dirty-return` | 10 | lost writes | |
| +| `watchdog-independent` + `declare-lost-compute` | 2 | two writers | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 1,062 (against 40 per 3,000 for revalidation alone) | a stale purge step destroys a store; the op-id condition is the second line behind revalidation | |
| + |
| +**Liveness rules: 2.** `readiness-key` (T2) and `config-before-probe` |
| +cannot break a safety invariant: without them a target that cannot render |
| +config fails its probe and rolls back. They exist to avoid a pointless |
| +cut, and the model confirms that is all they do. |
| + |
| +**Not exercised by the model: 8 rules, the model's known gaps.** |
| + |
| +| rule | why not | next step | |
| +|---|---|---| |
| +| `seal-by-version`, `staging-quiet` (J-N2) | no seed lands a staging write after the seal, even at 30,000 seeds with a fat staging tail; dropping both together is not caught either | add a staging writer that re-signs after the seal from a stale read past its lease, then require both rules to be caught | |
| +| `exec-admission`, `fresh-admission` | the model's row holds and per-role admission table already refuse what these refuse; dropping both is not caught | model a second consumer of the claim that does not consult the row (the db door, a sibling box's edge) | |
| +| `hold-op-open`, `stale-hold-release` | no stale opener survives once the revert fix was in; stale holds no longer arise | add an open retried by a stalled worker after release | |
| +| `obligations-block-ops` (CC11) | one worker per box serializes obligations and roles, which hides the race | split the obligation runner from the role worker | |
| +| `claim-op-exclusive` | caught once in an earlier model version (1 / 30,000), not in the final one: a delete mid-move stays safe under the quiet horizon | keep as a product rule; widen the delete actor | |
| + |
| +**Seeds:** 300 in the gate (about a second); the 30,000-seed baseline and |
| +the sweep are the evidence for this revision. The harness is committed; |
| +its scratch copies are not. |
| + |
| +#### 14.2.6 What the model does not prove |
| + |
| +- **It is a model.** It checks the protocol, not the code that will |
| + implement it. Its S3 is a versioned map with the documented semantics |
| + (copy and delete by version id, delete markers, conditional writes on |
| + the claim); the AWS behaviour it relies on must be checked against the |
| + real service before planning, as the paid-launch work learned ("a fake |
| + provider is never proof"). |
| +- **Granularity.** One host, three regions, one box per region. One step |
| + is atomic, so "revalidate immediately before the effect" is modelled as |
| + revalidating at the start of the step. |
| +- **Clock and pause assumptions** (claim §3.1) are modelled only as skew; |
| + correctness never depends on them except through the late-completion |
| + horizon H, which S3's signature-age limit bounds. |
| +- **Not modelled:** placement (`placing`), sidecars, nested-to-flat path |
| + translation beyond the files directory, the db door's multi-console |
| + drain, and app moves (F5). |
| ### 14.3 Cross-version |
| @@ -1009,13 +1364,22 @@ region that lost. |
| 1. **Ops (in progress):** `CARLOS_SECRETS_KEY` on every region box. |
| 2. **Release with `secrets_key_fp`.** Verify every box against the console. |
| -3. **The host lifecycle claim** (claim spec §9) ships and every box and |
| - console honours it, with §19.3's differences settled. |
| +3. **The host lifecycle claim** (claim spec §10) ships and every box and |
| + console honours it, with §19.4's changes adopted. |
| 4. **Phase 1 release, dormant.** Consoles first, then every box. |
| 5. **Infra (M17, approved):** every region's `sibling_staging_arns` lists |
| every other region's data bucket. Applied per deployment as scoped work. |
| -6. **Rehearsals** in §14.4's order; each gates the next. |
| -7. **Write `control/moves-protocol.json`** before the first production move. |
| + **Plus** the versioned-object grants claim §6.2 and §6.5 need |
| + (`s3:ListBucketVersions`, `s3:GetObjectVersion`, `s3:DeleteObjectVersion` |
| + on each box's own bucket; `s3:GetObjectVersion` for the console). |
| +6. **Write `control/moves-protocol.json`** (§11) **before any protected |
| + production rehearsal** (joint N12). Rev 3 had this after the |
| + rehearsals. |
| +7. **Rehearsals** in §14.4's order; each gates the next. |
| +8. **Before planning:** the AWS behaviours the model assumes (copy and |
| + delete by `versionId`, delete-marker semantics, conditional writes on the |
| + claim, the signature-age limit behind H) are checked against the real |
| + service in a scoped sandbox (§14.2.6). |
| ## 16. Follow-on specs |
| @@ -1033,21 +1397,20 @@ No design here, only what each must satisfy. |
| ## 17. Interface points with #199 and the claim spec |
| -The claim spec supersedes #199 rev 3 from its §2 onward, so most of rev 2's |
| -#199 interface points now go through the claim (§19). |
| +The claim spec supersedes #199 rev 3 from its §2 onward. Against claim rev 2: |
| | id | point | status | |
| |---|---|---| |
| -| I-1 | **Incarnation**, including the zero-CreatedAt legacy identity | agreed: one `provision.Incarnation` (claim spec §2) | |
| -| I-2 | **Where an incarnation's data lives** | agreed: `touched.regions` and `touched.boxes`, appended before the first write (claim spec §2); every move write site adds first (T9, §7.6 `checking`) | |
| -| I-3 | **Parking `moves/<host>/`** | agreed: the claim's delete park copies `instances/` and `moves/` as separate subtrees (claim spec §5 step 4.3), and a delete cannot run during a move, so a live move's staging is never swept | |
| -| I-4 | **Park helpers and namespaces** | agreed in shape; the destination for a move's superseded data is `superseded/<op id>/`, never `parked/<incarnation>/` (§19.3 D5) | |
| -| I-5 | **Recreate** | agreed: create requires the claim free or absent (claim spec C2) | |
| -| I-6 | **Stale or orphan row retirement** | agreed: participant rows retained (claim spec §8); §9.6 | |
| -| I-7 | **Flat files** | **open**: the claim spec's local park inventory (§5 step 4.4) names the working directory for nested rows; it should take the flat `<DataDir>/<host>/` too, as this spec defines it (§6.1), or a recreated flat host inherits an `instance.key` | |
| -| I-8 | **`generation.json`, `install-<op>.json`, `lock.json`** | agreed: copied like any other key; `lock.json` deleted last by its own holder | |
| -| I-9 | **Destructive steps** | agreed: serialized by the claim and the location's lease (claim spec C3), with the cross-region exception in §19.3 D4 | |
| -| I-10 | **Push** | agreed: F7, on §5 and the claim's `pushing` op | |
| +| I-1 | **Incarnation**, including the zero-CreatedAt legacy identity | agreed: one `provision.Incarnation` (claim §2); fresh `CreatedAt` on create and `retired_incarnations` (claim §5.1, R3-12). The model reuses an identity when the rule is dropped and finds hosts that can never be admitted again | |
| +| I-2 | **Where an incarnation's data lives** | agreed: `touched`, appended before the first write (claim §2); every move write site adds first (K12) | |
| +| I-3 | **Parking `moves/<host>/`** | agreed: parks keep `instances/` and `moves/` as separate subtrees (claim §6.2) and a delete cannot run during a move | |
| +| I-4 | **Park destinations** | agreed: one destination and manifest per retirement event (claim §6.2, joint D5); `superseded/<op>/…` for move retirements | |
| +| I-5 | **Recreate** | agreed: create requires the claim free or absent (claim C2) | |
| +| I-6 | **Participant rows** | agreed: retained while an operation lists them (claim §2 obligations, K9) | |
| +| I-7 | **Flat files** | agreed: claim §6.3 retires the flat `<DataDir>/<host>/`, the sibling env files and markers (joint I-7) | |
| +| I-8 | **`generation.json`, `install-<op>.json`, `lock.json`** | agreed, with CC3: the parker's own renewed lock is excluded everywhere | |
| +| I-9 | **Destructive steps** | agreed: exact versions plus the staging-work lease (claim C3), with CC1's horizon for the replication exception | |
| +| I-10 | **Push** | agreed: later, on §5's handoff and the claim's `pushing` op; it needs CC13 | |
| ## 18. Questions for Paul |
| @@ -1077,7 +1440,7 @@ The db door refuses on every move kind (claim spec §8). |
| | id | rule | |
| |---|---| |
| -| **K1 Execution holder** | The move keeps `op.journal.exec` = a box label or `none`, and `op.journal.participants` = {source box, target box}. Admission (claim spec C4) for a move kind is the table in §19.1 **and** `exec` naming this box. | |
| +| **K1 Execution holder** | The move keeps `op.exec` = a box label or `none`, and `op.participants` = {source box, target box}. Admission (claim spec C4) for a move kind is the table in §19.1 **and** `exec` naming this box. | |
| | **K2 Acquire** | The request door CASes `serving` → `moving` only when the holder incarnation equals the record's and no other op holds the claim; it sets op id, participants and `exec` = source box. | |
| | **K3 Execution to none** | A participant that has written stop evidence for this op id (§5.3) may CAS `exec` from itself to `none`. Nobody moves `exec` from one box to another directly. | |
| | **K4 Execution handoff** | From `none` to a participant, by that participant, citing the previous holder's evidence object for this op id: at the flip (to target), at source recovery (to source), and at `reverting` (the source, citing its own evidence). | |
| @@ -1091,39 +1454,41 @@ The db door refuses on every move kind (claim spec §8). |
| | **K12 Touched** | Every move write site CAS-adds its region or box to `touched` before its first write: the source adds the target region before the first staging round; the target adds its box at `checking`; a dirty return adds nothing new (the source region and box are already there). | |
| | **K13 Evidence durability** | Evidence objects are create-only per (op id, role) in the deployment bucket, recomputable from system state after a restart (§5.3), and referenced from the claim journal, never inlined. | |
| -### 19.3 Where this spec asks the claim spec to change |
| +### 19.3 Rev 3's requests, against claim rev 2 |
| -| id | claim spec says | moves need | why | |
| -|---|---|---|---| |
| -| D1 | admission is "`op.kind` permits serving" (§3 C4, §8) | admission for a move kind is per box and per phase, from `op.journal.exec` and the §19.1 table | the source serves during `moving` until the cut, the target only from `committed`; a kind-level answer cannot say which box | |
| -| D2 | `gen` increments on every write (§2) | nothing; this spec names generations by op id (§5.1) | rev 3's requirement for a per-handoff counter is **withdrawn** | |
| -| D3 | evidence is an empty per-host cgroup, no live lease, no open replicator (§6) | also: (a) every spawn of a host under a lifecycle op is **strict** (`cgroup.PrepareStrict`), and a non-strict pre-move child is stopped before the cut; (b) the agent's own cgroup holds no process but the agent; (c) no process holds the database open | `cgroup.Manager.Start` falls back to spawning **unaccounted** in the agent's cgroup, or to a PID move that leaves already-forked grandchildren behind (`internal/cgroup/cgroup.go:225-252`). In either case the per-host cgroup reads `populated 0` while a descendant still writes (round 2, R2-1) | |
| -| D4 | destructive steps hold the replica lease of every location written (C3) | an exception for a **per-op prefix written only by that op**: `moves/<host>/<op id>/` in another region's bucket | the source writes staging cross-region with push-only IAM (Put, Delete, prefix-scoped List, no Get: `infra/modules/region-host/main.tf:217-227`, M17), so it cannot read `lock.json` there and cannot take a lease. Exclusion there comes from the op id in the key, the claim's revalidation, and the target never reading staging until the flip | |
| -| D5 | rollback adds a `park-replica` obligation for the target region (§5) | an obligation kind `park-superseded {region or box, op id}` with destination `superseded/<op id>/<host>/` | `park-replica` parks into `parked/<incarnation>/<host>/`, and "a manifest that is present is never rewritten". The incarnation is still live; if it later moves back to that region and is deleted, the delete's park finds the rollback's manifest, skips the copy, and then stops on unlisted keys. A per-op destination never collides | |
| -| D6 | `--declare-lost` removes the box's `park-local` obligations and its `touched.boxes` entry (§4) | also: append the box to `op.journal.lost`; a box in `lost` never CAS-adds itself back to `touched` and never spawns the host until the claim is released; refused after commit; refused if the lost box is the source | `doWake` CAS-adds a missing box to `touched` (§8 there). A box that was only partitioned would re-add itself on return and wake, beside the source | |
| -| D7 | moving "ends in `serving`, or `reverting`" (§4) | `moving` → `landing` at the flip, `landing` → `restoring` at a rollback, `restoring` → `serving` | the full transition set of §19.1 | |
| -| D8 | obligations block only "free" (§2) | nothing; the move itself waits for its own obligations before releasing (K8) | recorded so both specs agree on who waits | |
| - |
| -### 19.4 Joint simulation (claim spec §10) |
| - |
| -§14.2's simulation is built to run with the claim's model, not beside it: |
| - |
| -- **One claim model.** The claim object, its CAS, `touched`, obligations, |
| - leases with `SafeUntil` and the clock assumption of claim spec §3.1 come |
| - from the claim spec's model. This spec's actors use only its interface: |
| - read, CAS, lease acquire and renew. |
| -- **Shared actors.** Delete-park, create, reconcile, wake and the db door |
| - are the claim spec's actors; source, target, the deadline sweep and the |
| - application process tree are this spec's. Every actor exposes the same |
| - `Step(rng) (effect, done)` contract at side-effect granularity. |
| -- **Shared fault menu.** Crash with memory loss, stall, partition (a box |
| - that keeps running but cannot reach the buckets), surviving descendants, |
| - versioned objects, forged objects, old binaries. |
| -- **Union of invariants.** The claim spec's C1 to C6 and this spec's INV-1 |
| - to INV-10, asserted together after every step and at the end of every |
| - run. |
| -- **Union of mutations.** Each spec's mutation list runs against the joint |
| - model; the gate passes only if every mutation from both lists is caught. |
| +| id | status in claim rev 2 | here | |
| +|---|---|---| |
| +| D1 admission per box and phase | adopted (C4, joint text) | K1, §19.1 | |
| +| D2 no per-handoff counter | adopted (`gen` is a revision) | §5.1 | |
| +| D3 strict spawn, whole-tree evidence | adopted (§6.1, joint text) | §5.3 | |
| +| D4 cross-region staging exclusion | replaced, as the review ruled: a shared staging-work lease (C3); sealing and draining are this spec's | §7.3 | |
| +| D5 per-event retirement destinations | adopted (§6.2) | §6.4 | |
| +| D6 declare-lost | adopted with an execution-lease branch; **this spec drops that branch** (model 5) | §7.10, CC5 | |
| +| D7 move-kind transitions | adopted (§4, joint text) | §19.1 | |
| +| D8 who waits for obligations | adopted (§2) | K8 | |
| +| I-7 flat local inventory | adopted (§6.3) | §6.1 | |
| + |
| +### 19.4 Claim changes the model requires (for platform-1e) |
| + |
| +This spec does not edit the claim spec. Each change below is what the |
| +model needed for its invariants to hold; the mutation column says what the |
| +model finds when the rule is dropped (§14.2.5). |
| + |
| +| id | change to claim rev 2 | why (model) | |
| +|---|---|---| |
| +| **CC1** | **A late-completion horizon on every retirement.** C3's "late completion is harmless" holds only for version-bound calls. Ordinary replication, the C3 exception, is plain PUTs to reused LTX names. A park acknowledges only after a verification listing taken later than `evidence time + H` (H = S3's 15-minute signature-age limit plus the longest request), and parks anything found then as a further retirement event. Persist a per-region `quiet_after` in the claim (kept across `free`, like `retired_incarnations`) and make any install into that region's namespace wait for it | model 1: residue in a freed host's namespace | |
| +| **CC2** | **Park progress accumulates.** §6.2 step 7 restarts at step 2 when no manifest exists. Key each copy's destination by source key and `versionId`, skip copies that already landed, and write the manifest once every copy exists | model 2: parks that never finish | |
| +| **CC3** | **The parker's own lock (J-N6) is renewed while it works**, so "excluded from the snapshot" must also mean excluded from the emptiness check and the straggler re-listing | the park never finishes when the lock is counted | |
| +| **CC4** | **Discovery at adoption.** Adopting a legacy host (§9) adds a `park-replica` obligation for every region other than the record's (that data cannot be the live lineage), and `touched.complete` becomes true once they acknowledge. §5.2 step 3's "every region at delete" then remains as a fallback | model 10: legacy residue for as long as the host serves | |
| +| **CC5** | **Declare-lost requires compute fencing.** Drop §7.2's lease-expiry branch: a whole-VM pause stops the self-fencing watchdog too, and on resume the app can write before it fires. Keep the lease for liveness. Cover two more states: a target that gave evidence and released dirty but never returned its writes; and a destroyed box that owes only `park-local` (legal after commit) | model 5, model 6 | |
| +| **CC6** | **Purge adopts first.** Before deciding which hosts the app holds, run the one adoption routine for every unclaimed record of the app | model 7 | |
| +| **CC7** | **The purge reservation is the purge's journal.** It records the purge's phase; the recovery pass drives those phases in order; only the purge's completion removes it, never `free` | model 8 | |
| +| **CC8** | **One adoption routine for every adopting actor**, discovery included | model 11 | |
| +| **CC9** | **A fresh read with no operation ends a self-fence** (§7.1): a box clears its local execution-lease file when the claim shows it is not a participant | model 9 | |
| +| **CC10** | **Reconcile releases a stale hold**: a held row whose `hold_op` is not the claim's operation, on the box the claim names as executor of a `serving` host, is opened | model 12 | |
| +| **CC11** | **No operation starts over a pending chore in its locations**: the start CAS from `serving` fails if an obligation names a region or box the operation will write | model gap: not exercised (§14.2.5) | |
| +| **CC12** | **A quarantined box retires its own state.** §7.2 says a box on `lost` is refused "until its old state has been retired"; name the actor: the returning box itself, under the host guard, before anything else | the returning box otherwise keeps stale local state | |
| +| **CC13** | **Every probe renders held config** (`RenderHeld`, `MaterializeHeld`) before spawning, including a future push's | model 4 | |
| ## 20. Copy (pending copy review) |
| @@ -1207,3 +1572,52 @@ other-region obligation disappears because a delete cannot run mid-move |
| including "require #199's epoch" now read as M14's single landing path. |
| Rev 2's §18 question is M16, with Astra's three conditions built in |
| (§7.10). |
| + |
| +### 22.3 Joint round 1 (claim 653ad4b1 with moves rev 3 6e4d3a0e) |
| + |
| +Round 2 items the joint review left partly resolved: |
| + |
| +| item | rev 4 | |
| +|---|---| |
| +| R2-8 delayed config and adoption work, inherited environment at the actual spawn | the host guard (claim C7) refuses a stale background write; the probe recomposes the launch environment at spawn (§7.7). The model's `hostguard` mutation is caught | |
| +| R2-10 one probe budgeted, three allowed | T11 budgets every attempt; one absolute `cut_deadline` binds every phase before the commit (§7.3, §7.4). The `cut-deadline` mutation is caught | |
| +| timers: the runner's own prune | canonical digest that excludes disposable history (§9.4). The `timer-canonical` and `timer-freeze` mutations are caught | |
| + |
| +Adjudicated interfaces: |
| + |
| +| item | rev 4 | |
| +|---|---| |
| +| D1 | adopted, exact text in claim rev 2 C4; §19.1 governs every spawn, Seed, probe retry and recovery | |
| +| D2 | adopted; markers carry op id and incarnation, never the claim revision (§5.1) | |
| +| D3 | adopted, exact text quoted in §5.3, with the cleanup-only `ReopenAndDrain` | |
| +| D4 | the staging-work lease replaces rev 3's exception; sealing by version and the staging horizon are this spec's (§7.3) | |
| +| D5 | per-event retirement destinations (§6.4); `retirement-ids` mutation caught (parks never finish) | |
| +| D6 | exact text quoted in §7.10; this spec takes only the compute-fencing branch (CC5) | |
| +| D7 | adopted in §19.1 and claim §4; one writer per transition (K4) | |
| +| D8 | adopted (K8) | |
| +| I-7 | adopted (claim §6.3; §17) | |
| + |
| +New findings: |
| + |
| +| # | finding | owner | rev 4 | |
| +|---|---|---|---| |
| +| N1 | late server-side completion | claim, with moves | exact-version deletes and copies (claim C3, §6.4); **plus CC1**: the replication exception is not version-bound, so retirements verify after the horizon. Mutations `park-by-version`, `park-all-versions` and `quiet-before-ack` are caught | |
| +| N2 | delayed staging round corrupts sealed staging | moves | staging-work lease; revalidation under it; seal by version; staging retired after its writers' horizon (§7.3). The stalled-worker actor exercises it; `revalidate-before-effect` is caught. See §14.2.5 for `seal-by-version` | |
| +| N3 | declare-lost starts a second writer | claim, with moves | compute fencing only (§7.10, CC5) | |
| +| N4 | unjournaled claim and record gaps | claim | intent in the start CAS and a recovery owner per state (claim C2, §8); the model's `recovery-pass` mutation is caught in about half of all seeds | |
| +| N5 | lazy legacy adoption | claim | `touched.complete` (claim §9) **plus CC4** discovery at adoption; `legacy-discovery` caught | |
| +| N6 | parking a live lock | claim | lock excluded (claim §6.2) **plus CC3**; `park-skip-lock` caught | |
| +| N7 | one move reuses its own manifest | claim, with moves | retirement ids (§6.4); caught | |
| +| N8 | in-flight config and adoption writers | claim | host guard (claim §6.4), placement as an op; `hostguard` caught | |
| +| N9 | purge destroys the store first | claim | reservation first (claim §5.3) **plus CC6, CC7**; `purge-reserve-first`, `purge-adopts`, `purge-journal` caught | |
| +| N10 | stalled door reads | claim | reads pinned to versions (claim §6.5); `door-by-version` caught | |
| +| N11 | pre-flip recovery rejects its own writes | moves | journaled `rev_phase`, never re-verify after `probing` (§7.4); `revert-journal` caught | |
| +| N12 | automatic boot recovery to an old executable | claim, with moves | the floor on every restore path, published before rehearsals (§11, §15); `floor-boot-recovery` caught in most seeds | |
| +| N13 | abort parks remote staging without permission | moves | a target-owned obligation (§7.11); `abort-target-owner` caught as IAM violations | |
| +| N14 | the runner's prune bypasses the freeze | moves | canonical digest (§9.4); caught | |
| +| N15 | no single enforceable budget | moves | absolute `cut_deadline` (§7.4); caught | |
| +| R3-12 | fresh incarnation | claim | claim §5.1 and `retired_incarnations`; `fresh-incarnation` caught | |
| + |
| +The joint review's verdict was "not ready" for both specs and asked for |
| +the expanded simulation before planning. That simulation now exists and |
| +passes; the claim changes it requires are §19.4. |