amadan
spec: move-any-app rev 6, part 1: protocol answers to joint round 2
Written against claim rev 4 (a3c86fa5). Operation-scoped generations within holder.location and a restore contract (R2-1); the start check compares the claim's generation (R2-8); recovery probes run on current inputs (R2-5); every move transition is one record CAS that the claim follows, any actor writing the claim half (record/claim ordering, K4); the deadline enforces the stop-to-open promise (N15); staging signs at the check (model 18); the straggler sweep (model 17); CC15 to CC19; the secrets key on every flagship box. The model chapter (§14.2) follows in part 2.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+289
−73
docs/superpowers/specs/2026-10-02-move-any-app-design.md+289 −73
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 8f4f8c29a..77dd35b87 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,9 +1,43 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| -**Date:** 2026-10-02 |
| -**Revision:** 5. |
| +**Date:** 2026-10-03 |
| +**Revision:** 6. |
| + |
| +- **Rev 6** answers joint Astra round 2 (`CODEX-FINDINGS-JOINT-R2.md`, |
| + df41156c; cited "J2-…"), whose three verdicts were "not ready", and is |
| + written against **claim spec rev 4** (a3c86fa5 on |
| + `design-replica-ownership`), which answers the claim-side findings. Rev 6: |
| + - **rebuilds the model to encode exactly what the specs say** |
| + (§14.2): restore and the start check no stronger than §5.1; |
| + record-first transitions split from their claim halves, with crash |
| + points between; independent processes for the host guard; a door |
| + listing with O1 and O2; creates and purges as concurrent console |
| + plans over two hostnames; requests that complete after `H`; a final |
| + oracle that only reads; and a mutation harness that counts only a |
| + parsed invariant violation as a detection (J2-R2-9, J2-R2-10); |
| + - specifies this spec's share of J2-R2-1: **operation-scoped |
| + generations** within the claim's `holder.location`, a restore |
| + contract that reads only the generation the claim names, and a |
| + **straggler sweep** for what lands after `H` (§5.1, §6.4); |
| + - fixes J2-R2-5: a recovery probe runs on the inputs it renders now, |
| + not the move's pinned ones (§7.6, §7.7); |
| + - fixes J2-R2-8: the start check also requires the generation the claim |
| + expects, so the third admission fence the model relied on is now |
| + specified (§5.1); |
| + - makes the record and the claim consistent: every move transition is |
| + one record CAS, and the claim follows it; any actor may write the |
| + claim half, which the record fully determines (§7.5, §19 K4); |
| + - makes the cut promise the enforced deadline (§7.4, T11); |
| + - records that `CARLOS_SECRETS_KEY` is on every flagship box and config |
| + sync is armed in every region (§1.2, §15); |
| + - lists CC15 to CC19 for platform-1e (§19.4). |
| + |
| + Rev 6's changes are marked "(J2-…)" for the review's findings and |
| + "(model N)" for the stricter model's. |
| -- **Rev 5** is written against **claim spec rev 3** (8b5bccb2 on |
| +Earlier revisions: |
| + |
| +- **Rev 5** (4ec3282b) was written against **claim spec rev 3** (8b5bccb2 on |
| `design-replica-ownership`), which adopted CC1 to CC13. It answers the |
| coordinator's round on rev 4: |
| - the model (§14.2) is extended until it exercises every rule rev 4 |
| @@ -82,8 +116,9 @@ branch `design-nearest-region`. |
| 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`, |
| - **rev 3 at 8b5bccb2** on `design-replica-ownership`. Rev 5 is written |
| - against rev 3; rev 4 was written against rev 2 (cf3a7861). |
| + **rev 4 at a3c86fa5** on `design-replica-ownership`. Rev 6 is written |
| + against rev 4; rev 5 against rev 3 (8b5bccb2); rev 4 against rev 2 |
| + (cf3a7861). |
| Citations are to this worktree at 7edd4b33 unless they name another branch |
| or repo. |
| @@ -132,7 +167,7 @@ traffic is undone automatically (§7.8); after the target opens, R4 stands. |
| ### 0.4 The host lifecycle claim |
| -From claim spec rev 3 (§2 to §10 there), the parts this spec relies on: |
| +From claim spec rev 4 (§2 to §10 there), the parts this spec relies on: |
| - **The object** `control/hosts/<host>.json`, rewritten whole by CAS: a |
| per-write revision `gen` (not a data generation, J-D2); a `holder`; |
| @@ -149,7 +184,12 @@ From claim spec rev 3 (§2 to §10 there), the parts this spec relies on: |
| already-admitted work is drained (`hostguard`). Rev 3 limits C3's |
| "late completion is harmless" to the operation's own version-bound |
| calls, and covers the replication exception with a late-completion |
| - horizon (§6.2a there). |
| + horizon (§6.2a there). Rev 4 adds **C3a: no storage location is shared |
| + between incarnations.** `holder.location` is |
| + `instances/<host>/<incarnation>/` for a new incarnation and |
| + `instances/<host>/` for an adopted legacy host, set with the holder and |
| + immutable while it holds; restore reads only that location, plus this |
| + spec's generation within it, from the same fresh admission read. |
| - **Op kinds** (§4 there): `moving`, `landing` and `reverting`/`restoring` |
| belong to this spec. One operation runs at a time. |
| - **Mechanisms:** stop evidence from system state, with every probe |
| @@ -157,21 +197,26 @@ From claim spec rev 3 (§2 to §10 there), the parts this spec relies on: |
| per-retirement destinations keyed `<relative key>@<source versionId>` |
| (§6.2); the late-completion horizon `H` and the per-region `quiet_after` |
| that survives `free` (§6.2a); local retirement for both layouts (§6.3); |
| - the host guard (§6.4); door reads pinned to versions (§6.5); execution |
| + the host guard, an exclusive `flock` shared by every OS process that |
| + writes host state, with a fresh claim read under it (§6.4); door |
| + listings that read the claim twice, O1 and O2 (§6.5); execution |
| leases for liveness, and declare-lost by compute fencing only (§7); one |
| - `claim.Adopt` routine with discovery parks (§9); the purge journal |
| - `reserved → adopted → claimed → torn-down → retired → done` (§5.3); the |
| - floor on every executable restore path (§10). |
| + `claim.Adopt` routine whose discovery parks every other region and every |
| + other box (§9); app admission registration, closed and drained by purge |
| + (§5.1, §5.3); `cancelled_creates` (§5.1); the purge journal |
| + `reserved → adopted → claimed → torn-down → retired → done` (§5.3); park |
| + manifests with separate archive and deletion sets (§6.2); 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 C1 to C7. **Execution holder** below |
| means the claim's `op.exec` (rev 2 made it a first-class field, as rev 3 |
| asked). |
| -Rev 4's model (§14.2) required thirteen changes to claim rev 2, CC1 to |
| -CC13; claim rev 3 adopted all of them (§19.4 maps each to its section |
| -there). Rev 5's model requires one more, CC14 (§19.4): until platform-1e |
| -adopts it, this spec states it as the behaviour it relies on. |
| +Rev 4's model required CC1 to CC13 of claim rev 2, and claim rev 3 |
| +adopted them; rev 5's CC14 is in claim rev 3.1 and rev 4. Rev 6's stricter |
| +model requires CC15 to CC19 (§19.4). Until platform-1e adopts them, this |
| +spec states each as the behaviour it relies on. |
| ## 1. What happened in production |
| @@ -200,8 +245,12 @@ set" (`internal/host/agent.go:884`). Both config loops return at once |
| (`agent.go:881-886`, `:1279`), the fast converge skips its config leg |
| (`agent.go:1812`), and the spawn treats a missing config file as empty |
| (`backend_exec.go:1146-1149`). Paul approved distributing the key to every |
| -region box (ops, in progress). The fingerprint every box publishes (§10) |
| -verifies it, and T2 refuses any target without it. |
| +region box. **Done (2026-10-03): the key is on all four flagship boxes, |
| +and config sync is armed in every region.** The fingerprint every box |
| +publishes (§10) still verifies it per box, and T2 still refuses any |
| +target without it: a new or rebuilt box can lack it again. With config |
| +sync live everywhere, bundle updates now reach a box during a move, which |
| +is why J2-R2-5's case is real (§7.6). |
| ### 1.3 Finding 3: the rehearsal proved nothing |
| @@ -310,14 +359,51 @@ model, and where each lives: |
| ## 5. The handoff protocol |
| -### 5.1 Generations and markers (codex R2-6, R2-9) |
| +### 5.1 Generations, markers and the restore contract (codex R2-6, R2-9, J2-R2-1, J2-R2-8) |
| -A generation is named in three markers. None is a record field. |
| +**Location and generation.** Claim C3a gives each incarnation its own |
| +replica location, `holder.location`: `instances/<host>/<incarnation>/`, |
| +or `instances/<host>/` for an adopted legacy host. Within it, every |
| +installed state of the database is a **generation**, named by the |
| +operation that installed it: the origin generation (`""`, written by the |
| +host's own replication from its first wake), then one per committed move, |
| +per push, and per dirty rollback. Each generation has its own key prefix: |
| + |
| +| generation | replica objects | |
| +|---|---| |
| +| origin | `<location>` itself, the layout litestream writes today (`<location>ltx…`, a legacy host's existing objects) | |
| +| an operation `op` | `<location>g-<op id>/…`: the installed snapshot and every LTX object replicated on top of it | |
| + |
| +The claim names the current one, **`holder.generation`** (CC18): written |
| +by the commit's claim CAS (§7.9), by a push's probe CAS (F7), and by a |
| +dirty rollback's source probe (§7.8). Restore reads it from the same fresh |
| +admission read as `holder.location` (claim C3a). |
| + |
| +**The restore contract (J2-R2-1).** A restore reads `holder.location`, |
| +generation `holder.generation`, in the box's own bucket, and nothing else. |
| +It replays **every** replica object of that generation, current and |
| +noncurrent, as litestream replays every LTX file of a generation. It never |
| +picks "the newest object under the prefix". So: |
| + |
| +- a request that completes late can only add an object to **its own** |
| + generation. A late install copy repeats the sealed snapshot; a late LTX |
| + PUT from an old executor lands in a generation the claim no longer |
| + names. Neither is ever restored into the current state; |
| +- the claim moves to a new generation only after that generation is fully |
| + installed and probed, so a restore never meets a half-written one; |
| +- what lands in a dead generation after its retirement is residue, not |
| + data: the straggler sweep (§6.4) retires it. |
| + |
| +The model drops the contract (restoring the newest object under the |
| +location instead) and loses acknowledged writes (§14.2.5). |
| + |
| +**Markers.** A generation is named in three markers. None is a record |
| +field. |
| | marker | where | written | content | |
| |---|---|---|---| |
| -| `generation.json` | `instances/<host>/generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6) | `{"op","incarnation","host","box","installed_at","manifest_sha256"}` | |
| -| `<dbPath>.gen` | beside the local database | after a restore completes, from `generation.json` | `{"op","incarnation"}` | |
| +| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6) | `{"op","incarnation","host","box","installed_at","manifest_sha256"}` | |
| +| `<dbPath>.gen` | beside the local database | after a restore completes | `{"op","incarnation","location"}` | |
| | `.files-gen` | inside the files directory | **last**, after files, `<host>.env`, timers and the carried registry columns are all durable (§7.6) | `{"op","incarnation"}` | |
| All three are **protocol metadata**: excluded from the archive, from every |
| @@ -325,18 +411,28 @@ content digest, and from F4's definition of the files directory (§6.1). |
| Absent everywhere means origin. The claim's `gen` is a per-write version |
| (claim spec §2), not a generation, so it never appears in a marker. |
| -**The start check (INV-4).** Before every spawn (`Start`, `Seed`, |
| -`ProbeWake`), the activator requires `<dbPath>.gen`, `.files-gen` (when |
| -the files directory exists) and the box's own `instances/<host>/generation.json` |
| -to name the same op and incarnation, and the incarnation to be the claim's |
| -holder (claim spec C4). Absent in all three is origin. A marker that |
| -merely exists proves nothing (codex R2-6). A mismatch refuses the wake |
| -with a member-safe reason and pages. The bucket read rides the wake's |
| -existing lease round trip to the same prefix. |
| - |
| -A warm local database whose `<dbPath>.gen` differs from the bucket's |
| -`generation.json` is from an earlier stay on this box. The activator parks |
| -it (§6.3) and restores cold. This replaces "staging wins" |
| +**The start check (INV-4, J2-R2-8).** Before every spawn (`Start`, `Seed`, |
| +`ProbeWake`), the activator requires: |
| + |
| +1. the box's own `<location>generation.json` (absent is origin) to name |
| + **the generation the claim expects**: `holder.generation` for an |
| + ordinary wake, or, for a probe, the generation the probing operation is |
| + installing (the move id, the rollback id, the push id); and its |
| + incarnation to be the holder's; |
| +2. `.files-gen`, when the files directory exists, to name the same |
| + generation and incarnation; |
| +3. `<dbPath>.gen` to name the same generation and location. A warm |
| + database that does not is from an earlier stay on this box: the |
| + activator parks it (§6.3) and restores cold. |
| + |
| +Rev 5's check compared the three markers with each other only. Astra |
| +showed (J2-R2-8) that after a commit, before the source is retired, the |
| +source's own three markers still agree with each other, so the "third |
| +fence" the model reported in rev 5 did not exist in the text: the model's |
| +check was stronger than the spec. Rule 1 makes it exist. A mismatch |
| +refuses the wake with a member-safe reason and pages. A marker that merely |
| +exists proves nothing (codex R2-6). The bucket read rides the wake's |
| +existing lease round trip to the same prefix. This replaces "staging wins" |
| (`backend_exec.go:1581-1588`); `promoteStagedReplica` is deleted (M15). |
| ### 5.2 Holds |
| @@ -512,9 +608,15 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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 |
| +- **What a move parks is its location, not the host namespace.** The |
| + landing's park of an earlier stay, the source's park after commit, a |
| + rolled-back target's park and a push's park all name `holder.location` |
| + in their own region (C3a); staging parks name `moves/<host>/<op id>/`. |
| +- **Exact versions (joint N1, J2-R2-6).** The snapshot takes every version |
| + under the location, noncurrent included. The manifest records two sets |
| + (claim §6.2): the **archive set**, every non-marker version, copied by |
| + `versionId`; and the **deletion set**, every version, delete markers |
| + included, which is what a retry replays, by `VersionId`. The model replaces version deletes with bare-key deletes |
| (delete markers on a versioned bucket) and finds parks that never |
| finish, in 2,325 of 3,000 seeds (rev 5). |
| - **The live lock is not data (joint N6).** The parker takes the location's |
| @@ -541,6 +643,34 @@ 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). |
| +**The straggler sweep (J2-R2-1, CC15, model 17).** S3's signature limit |
| +bounds when a request is accepted, not when it completes (claim C3a), so a |
| +request accepted before a retirement's horizon listing can still land |
| +after it. Within one incarnation the restore contract (§5.1) makes such a |
| +straggler harmless to data. It is still residue, in a region the instance |
| +left, in a dead generation, or under a freed host, and no later retirement |
| +of that location may ever run. So each region's box sweeps: |
| + |
| +- **when:** only while the host is **at rest**: the claim free, or |
| + `serving` with no operation and no obligation. It re-reads the claim on |
| + every step and abandons the sweep the moment that stops being true; |
| +- **what:** everything under `instances/<host>/` and `moves/<host>/` in its |
| + own bucket except the **live set**: in the executor's region, |
| + `holder.location`'s current generation and `generation.json`; everywhere, |
| + the parkers' own `lock.json`. Under a free host the live set is empty; |
| +- **how:** as a retirement event of its own, with the park's machinery: |
| + snapshot, archive set copied, manifest, deletion set replayed by version |
| + id, under `parked/sweep/<host>/<sweep id>/`. Every delete names a |
| + snapshot version, so nothing written after the snapshot is touched, even |
| + if an operation starts mid-sweep. |
| + |
| +A periodic listing per host and region is the cost (rate: once a day, and |
| +after each operation's release). The horizon of §6.2a stays: it is what |
| +makes INV-10 hold **when an operation ends**, for every request that |
| +completes within `H`; the sweep covers only what completes after it. The |
| +model checks both: INV-10 at every release and free, excepting only |
| +versions created after `H`, and INV-10 everywhere at the end of the run. |
| + |
| ## 7. The move |
| ### 7.1 Request and refusals |
| @@ -629,17 +759,29 @@ further rules: |
| 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. |
| -- **Sign only before `SafeUntil` (model 14).** A staging writer checks its |
| - lease's `SafeUntil` immediately before it signs each request, after any |
| - pause, and drops the request if the time has passed. Revalidating at the |
| - start of the round is not enough: a goroutine that revalidated and then |
| - paused can sign long after its lease ended, and the horizon below no |
| - longer bounds its write. |
| +- **Sign only before `SafeUntil`, and sign at the check (model 14, |
| + model 18).** A staging writer checks its lease's `SafeUntil` immediately |
| + before it signs each request, after any pause, and drops the request if |
| + the time has passed. Revalidating at the start of the round is not |
| + enough: a goroutine that revalidated and then paused can sign long after |
| + its lease ended. **The signature is computed at that check**, with the |
| + check's time as its `X-Amz-Date`, and never recomputed: a pause between |
| + the check and the send, even a whole-VM freeze that no in-process bound |
| + can promise against, then ends in S3 refusing the request once its |
| + signature is older than the signature-age limit (403 |
| + `RequestTimeTooSkewed`, verified, §15 step 8). `SafeUntil` therefore |
| + leaves room for the signature's whole valid life: `SafeUntil = Until − |
| + clock skew − 15 min`. Rev 5's rule signed at send time; the stricter |
| + model freezes a box between a passed check and the send, and the write |
| + lands after the staging cleanup (1 seed in 100,000; CC19, §19.4). |
| - **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. That bound holds only because of the rule above: a request is |
| - signed before `SafeUntil` and lands within `H` of signing. |
| + signed at a check made before `SafeUntil − 15 min`, and S3 accepts it |
| + only within 15 minutes of that, so it is accepted before `Until` and |
| + completes within `H` of acceptance, or it is a straggler that completes |
| + later, which only the straggler sweep can retire (§6.4). |
| All three are proven by the model (§14.2.5). A staging round's goroutine |
| can pause between revalidation and signing (one round in three), past its |
| @@ -686,7 +828,7 @@ placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`: |
| | 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) | |
| | 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. **Defence in depth (model, rev 5):** under claim rev 3 no state reaches it, because every retirement acknowledges only after its own horizon and CC11 refuses a move over a pending chore; the model drops T12 and no cut ever waits (§14.2.5). It stays, because it costs one comparison and guards any future path that acknowledges early | |
| -| 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) | |
| +| 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, each with its own settle** (three times 30 s plus 20 s) + the open (`open_budget`, 5 s) (joint N15, J2-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 |
| @@ -714,14 +856,20 @@ 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) | | |
| -**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 |
| +**One absolute deadline, equal to the promise (joint N15, J2-N15).** The |
| +M2 promise is the window from the source's stop to the target's open. |
| +Admission writes `cut_deadline = cut_at + cut_budget − open_budget` into |
| +the move journal. Every phase before the commit checks it, on the source |
| +and on the target alike, and **the commit is a record CAS conditional on |
| +`now ≤ cut_deadline`** (§7.9): that CAS is the decision, and the claim |
| +follows it unconditionally, so the deadline cannot be passed between the |
| +two writes. After the commit the target is authoritative and its open is a |
| +local conditional update on its own box, bounded by `open_budget`; an open |
| +that overruns it is reported against the promise, but nothing is rolled |
| +back after a commit. Exceeding the deadline before the commit starts |
| +recovery: `reverting` before the flip, a rollback after it. Rev 5 bounded |
| +the commit and called that the promise; the promise was stop to open |
| +(J2-N15). 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 |
| @@ -751,15 +899,54 @@ journal. Fifteen minutes of failed probes: `stuck`, held. |
| `timers_sha256` at `stopped`, before any phase that can fail, so every |
| recovery has a baseline. |
| -### 7.5 The flip |
| +### 7.5 The flip, and how the claim follows the record (J2: record/claim ordering) |
| -One CAS on the record, guarded by move id, incarnation and |
| -`cut_phase = archived`, followed by the claim CAS (§19 K4). If the record |
| -CAS lands and the claim CAS does not (a crash between them), the source's |
| -restart finds `flipped` in the record and completes the claim CAS; until |
| -then nobody holds the execution right, which is safe. The source row stays |
| -held (`moving`); reconcile keeps it because the claim names this box as a |
| -participant (§9.6). |
| +**Every move transition is one record CAS, and the claim follows it.** |
| +The record carries the move's journal, so the record CAS is the decision: |
| +the flip (`archived` → `flipped`), the commit (`probed` → `committed`, |
| +§7.9) and a rollback (`landing` → `rolling_back`, §7.8) are each one CAS on |
| +the record, guarded by move id and incarnation. The commit and a rollback |
| +CAS the same field, so exactly one wins. The claim half is a second CAS |
| +that the record fully determines: the op id, the claim's prior kind and |
| +phase, and its new kind, phase and execution holder: |
| + |
| +| record transition | claim CAS that follows | execution holder | |
| +|---|---|---| |
| +| `flipped` | `moving`/`sealed` → `landing`, `landing_phase = checking` | `none` → target, citing the source's evidence (`stopped-source.json`) | |
| +| `committed` | `landing` → phase `committed`, `holder.generation = move id`, plus the obligations of §7.9 | unchanged (target) | |
| +| `rolling_back` | `landing` → `restoring` under the same op id, `rollback.id` from the record | unchanged until the target's evidence (§7.8) | |
| + |
| +**Any actor that reads both objects and sees the record ahead writes the |
| +claim half**: the actor that wrote the record, on its next step; the other |
| +participant; or the console's recovery pass (claim C2's recovery owner for |
| +this state). The CAS is conditional on the op id and the prior claim |
| +state, so two actors racing to write it cannot both succeed, and neither |
| +can write anything the record did not decide. Until it lands, the claim |
| +still names the previous state: after the flip nobody holds the execution |
| +right (the source gave it up at `stopped`, K3); after the commit the target |
| +is not yet admitted to serve; after a rollback decision the target is still |
| +the executor and must still give evidence. Each is safe. |
| + |
| +This replaces rev 5's wording, in which §7.5 had the source complete the |
| +handoff while K4 reserved it to the receiving participant (J2-D7). K4 now |
| +says the execution holder changes only in the claim CAS that mirrors a |
| +record transition, citing the evidence that transition names (§19 K4). |
| + |
| +The model writes the record half and the claim half as separate steps, |
| +with crashes, console loss and the recovery pass between them (§14.2.2). |
| + |
| +The source row stays held (`moving`); reconcile keeps it because the claim |
| +names this box as a participant (§9.6). |
| + |
| +**The close is the other way round.** Releasing to `serving` is a claim |
| +CAS first (§19 K8), then the record CAS that clears `move` and names the |
| +executor's region; the recovery pass finishes the second half after a |
| +crash. Until it lands, the record still carries a finished `move`, which |
| +admits nothing. |
| + |
| +**Late record writes.** Every move write to the record is a conditional |
| +CAS. One that completes after its client gave up either still matches, |
| +and repeats a decision already taken, or fails on the ETag. |
| ### 7.6 Landing and install (codex 5, 13, R2-6) |
| @@ -771,12 +958,12 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12). |
| | phase | action | done when | replay | |
| |---|---|---|---| |
| | `checking` | read `stopped-source.json`; require the claim's `op.kind = landing` with this move id and execution holder = this box; require this box in `touched.boxes` (CAS-add before any local write); read `move.json` and require its incarnation; acquire the lease on `instances/<host>/` in its own bucket (claim spec C3) and hold it through `published` | | replayable | |
| -| `parking` | bucket-park whatever is at `instances/<host>/` in its own bucket into `superseded/<move id>/<host>/` (an earlier stay) | the park manifest exists **and** every named key is deleted | replayable by #199's rule (manifest present: skip copy, delete the rest) | |
| -| `copying` | per-key copy of `replica/` into `instances/<host>/`, verifying each size; then write the install manifest `instances/<host>/install-<move id>.json` (every key and size) | the install manifest exists | replayable: staging is immutable after the flip, the destination was emptied by `parking`, and the copy never deletes | |
| -| `published` | write `instances/<host>/generation.json` with op, incarnation and the install manifest's sha256 | `generation.json` names this move | replayable | |
| +| `parking` | bucket-park whatever is at `holder.location` in its own bucket into `superseded/<move id>/<host>/` (an earlier stay of this incarnation) | the park manifest exists **and** its deletion set is deleted | replayable by the claim's rule (manifest present: replay the deletion set) | |
| +| `copying` | per-key copy of `replica/`, by the sealed `versionId`s, into this move's own generation, `<location>g-<move id>/`, verifying each size; then write the install manifest `<location>g-<move id>/install.json` (every key and size) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the copy never deletes. A copy that completes late lands in this generation again (§5.1) | |
| +| `published` | write `<location>generation.json` with op, incarnation and the install manifest's sha256 | `generation.json` names this move | replayable | |
| | `local` | local-park any warm database (with `<dbPath>.gen`), files directory and `<host>.env` into `.parked/superseded-<move id>/`; extract the archive's files; write `<host>.env` from the archive; `ReplaceTimers` from the snapshot (§9.4); set `Replication` and `NextDue`; remove the host's restore-verification entry (§6.3); fsync all; **then** write `.files-gen` | `.files-gen` names this op and incarnation, and the journal records each sub-step | each sub-step is idempotent and journaled; `.files-gen` is written last, so its presence vouches for all of them (codex R2-6) | |
| -| `configured` | render through §9.1; the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move") | |
| -| `restored` | restore cold from `instances/<host>` (generation `<move id>`), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` | |
| +| `configured` | render through §9.1; the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move"), and the source's recovery then runs on the new bundle (§7.7, J2-R2-5) | |
| +| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` | |
| | `probing` | the probe (§7.7) | | **never replays an earlier phase** (INV-7); a crash restarts only the probe | |
| | `probed` | probe passed | | | |
| @@ -797,7 +984,18 @@ only while the claim names this box as execution holder: |
| 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; |
| + restart. **The landing probe** requires the input versions pinned at |
| + admission (`move.inputs`) and the executable. **A recovery probe** (the |
| + source's pre-flip revert and its rollback recovery, §7.4, §7.8) requires |
| + the inputs it rendered itself, now, and records them in the journal |
| + (`recovery.inputs`); it is not bound to `move.inputs` (J2-R2-5). Rev 5 |
| + bound every probe to the pinned inputs: a bundle published after |
| + admission rolled the landing back and then failed every recovery probe |
| + forever, because recovery renders the current bundle. The pin exists so |
| + the target runs what the source ran (T3); on the source itself, the |
| + current bundle is what it would run had there been no move. A bundle |
| + that is itself broken fails the recovery probe as it would fail any |
| + wake: `stuck`, held, and paged; |
| - 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; |
| @@ -878,10 +1076,12 @@ runs anywhere. It converges when the target returns (INV-3). |
| ### 7.9 Commit and finalization (codex 6) |
| -1. **Commit** (target): record CAS `probed` → `committed`, then the claim: |
| - phase `committed`, plus two obligations in the same claim write, |
| - `park-superseded` for the source box and region and `park-superseded` |
| - for the target's staging (§19.3). |
| +1. **Commit** (target): record CAS `probed` → `committed`, conditional on |
| + `now ≤ cut_deadline` (§7.4); then the claim follows (§7.5): phase |
| + `committed`, `holder.generation = move id`, plus the obligations in |
| + the same claim write, `park-superseded` for the source's location in |
| + its region and box, and `park-staging` for the target's staging |
| + (§19.3). |
| 2. **Open** (target): conditional open on `hold_op = move id`; CAS |
| `opened_at`. From here the target serves; the claim's `landing` op with |
| phase `committed` admits it (§19 K6). |
| @@ -939,6 +1139,10 @@ runs anywhere. It converges when the target returns (INV-3). |
| 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. |
| + "After `committed`" means after the **record's** commit CAS, whether or |
| + not the claim has followed it yet (§7.5). Before the commit the verb's |
| + rollback is the same record CAS as any other rollback, so it cannot |
| + race a commit. |
| 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 |
| @@ -1538,10 +1742,11 @@ region that lost. |
| ## 15. Rollout and gates |
| -1. **Ops (in progress):** `CARLOS_SECRETS_KEY` on every region box. |
| +1. **Ops (done, 2026-10-03):** `CARLOS_SECRETS_KEY` on every flagship |
| + box; config sync armed in every region. |
| 2. **Release with `secrets_key_fp`.** Verify every box against the console. |
| 3. **The host lifecycle claim** (claim spec §10) ships and every box and |
| - console honours it: claim rev 3, with CC14 (§19.4) adopted. |
| + console honours it: claim rev 4, with CC15 to CC19 (§19.4) 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. |
| @@ -1636,7 +1841,7 @@ The db door refuses on every move kind (claim spec §8). |
| | **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). | |
| +| **K4 Execution handoff** | From `none` to a participant, only in the claim CAS that mirrors a record transition (§7.5) or a recovery CAS that cites evidence, never directly from one box to another: at the flip (to the target, citing the source's `stopped-source.json`), at source recovery (to the source, citing the target's `stopped-target.json`), and at `reverting` (the source, citing its own evidence). Who writes the CAS does not matter, because the record and the cited evidence fully determine it (J2-D7). | |
| | **K5 Revalidation** | Before each destructive step the actor re-reads the claim and requires op id, kind, phase and `exec` to be what the step expects (claim spec C3); it holds the lease of every location it writes, acting before `SafeUntil`, with the exception in §19.3 D4. A staging writer checks `SafeUntil` immediately before it signs each request, after any pause (§7.3, model 14). | |
| | **K6 Wake admission** | `doWake` reads the claim fresh (claim spec §8) and applies K1. A box that reads a claim whose `exec` does not name it kills that host's process tree (§5.3 step 1) before anything else. | |
| | **K7 Other operations** | Delete, purge, park and push start only from `serving` (claim spec §4); while a move op holds the claim they are refused. Create requires free or absent. | |
| @@ -1699,6 +1904,17 @@ included now (model 15). |
| |---|---|---| |
| | **CC14** | **Staging residency rests on `SafeUntil`.** C3's closing paragraph says correctness no longer depends on the clock and pause assumption, because every destructive request is version-bound. Cross-region staging is the exception: a staging PUT creates a version, and the moves spec's staging horizon (`seal time + staging TTL + H`, §7.3) bounds only requests signed before the lease's `SafeUntil`. State that every request under the staging-work lease checks `SafeUntil` immediately before it is signed, after any pause, and that §3.1's margin must cover clock skew plus the longest pause between that check and the signature | model 14: staging residue in a region the instance left, or in the serving region (`sign-before-safeuntil`, §14.2.5) | |
| +**Rev 6's requests, against claim rev 4 (a3c86fa5).** The stricter model |
| +(§14.2) needs each of these; the mutation column is in §14.2.5. |
| + |
| +| id | change to claim rev 4 | why (model) | |
| +|---|---|---| |
| +| **CC15** | **An owner for stragglers that complete after `H`.** C3a says a straggler "is found and parked by the next retirement listing of that location". A freed incarnation's location never has another retirement, and neither does a dead generation inside a serving location. Name the owner: each region's box sweeps the host namespace in its own bucket while the host is at rest (free, or serving with no operation and no obligation), parking everything outside the live set as a retirement event of its own, and abandoning the sweep the moment the host leaves rest (moves §6.4) | model 17: with requests that complete up to 11 `H` late, residue under a freed host and in dead generations that nothing ever retires (`straggler-sweep`) | |
| +| **CC16** | **A create registration is a lease, and purge's drain knows when it is dead.** §5.1 step 0 removes a registration only at `serving` or cancel. A console that crashes between registering and the claim CAS leaves a registration nothing removes, and every later purge of the app waits on it forever. Give each registration an expiry; a create checks it immediately before its claim CAS (the §3.1 margin applies); purge's drain removes a registration only once it has expired **and** that host's claim does not name the create. Expiry alone is not enough: a create that claimed before the expiry is still in flight after it | model 19: purges that never finish (`registration-recovery`, 894 / 3,000); and, with expiry alone, a second host serving after purge tore down its store | |
| +| **CC17** | **An orphan record has no deadline.** §5.1 removes a cancelled create's late record only until `cancelled_creates.until`. A record PUT has no completion bound either (C3a's own lesson), and a late record blocks every recreate of the host. Treat a record whose incarnation is in `retired_incarnations` as an orphan whenever it lands, and delete it with `DeleteIfMatch`; `cancelled_creates` then only needs to name the record key | model 20: a record landing after `until` (`orphan-no-deadline`) | |
| +| **CC18** | **Name `holder.generation`.** C3a says restore reads "the moves spec's generation within it, taken from the claim". Add the field to §2's schema: written by the commit's claim CAS of a move, by a push's probe CAS, and by a dirty rollback's source probe; origin is `""`. The start check (moves §5.1) compares markers against it | J2-R2-8: the third admission fence exists only if the claim names the generation | |
| +| **CC19** | **CC14, amended: sign at the check.** "Check `SafeUntil` immediately before every request signature" still leaves the pause between the signature and the send, and a whole-VM freeze can stretch that without bound. Compute the signature at the check, with the check's time as `X-Amz-Date`, never recompute it, and set `SafeUntil = Until − skew − 15 min`: S3 then refuses the request once the pause outlives the signature | model 18: a box frozen between a passed check and the send lands staging after the cleanup (`sign-at-check`, 1 / 100,000) | |
| + |
| **Not a change, a note for platform-1e (model, rev 5).** Under rev 3 the |
| install wait on `quiet_after` never bites: every retirement acknowledges |
| only after its own `evidence time + H`, so the `quiet_after` it writes has |