amadan
spec: move-any-app rev 7, part 2: the gap closed, the final mutation table
The biased schedule, rev 7's results (30,000 and 100,000 seeds clean on claim rev 5), model faults 25 to 27, the 64-rule mutation table with no rule left unexercised, §7.10's return-lane park, and §22.6.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+117
−82
docs/superpowers/specs/2026-10-02-move-any-app-design.md+117 −82
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 949a8cd4c..16cf185a2 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 |
| @@ -1151,7 +1151,12 @@ runs anywhere. It converges when the target returns (INV-3). |
| - **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; |
| + can never send. **The same CAS adds a `park-staging` obligation for the |
| + return lane, `moves/<host>/<rollback id>/` in the source's region, |
| + owned by the source region's box, not before the lane's staging |
| + horizon** (model 27): the lost target may have published part of its |
| + return, and the rollback now finishes as a clean one, which parks |
| + nothing else there; |
| - **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); |
| @@ -1492,6 +1497,22 @@ the text. What changed, and what did not: |
| | mutation infrastructure errors counted as detections | strict classification (§14.2.1) | |
| | the return lane outside the lease | the return lane takes the staging-work lease of the source's region, with paused signers and the forward path's horizon (§7.8) | |
| +**Rev 7: a biased schedule beside the uniform one.** In half the seeds the |
| +scheduler aims at the interleavings C3a and the door exist for, which the |
| +uniform schedule never reached (deleting and recreating a host took longer |
| +than any straggler): |
| + |
| +- a freed host is recreated at once, in the region where it last served; |
| +- at the delete, the executor's last replication PUT is accepted and then |
| + completes at its worst moment: when another incarnation holds the host |
| + with an executor, or a create, in that region. Any other long-tail |
| + request of an earlier incarnation's replica data may complete at that |
| + moment too, within `H` or after it, and the early-completion fault |
| + leaves such requests alone; |
| +- a door listing is authorized at the delete, and stalls, before |
| + selecting or between signing and opening, until the object its key |
| + names belongs to another incarnation. |
| + |
| Not changed, and listed in §14.2.6: principal-aware reads and listings, |
| paginated listings, separate service, wall and monotonic clocks, |
| enrollment and console and updater versions, spawn separate from |
| @@ -1594,14 +1615,16 @@ adds and one it makes stricter: |
| app is idle. Writes past the last completed checkpoint are lost by |
| design and declared so; every durable write must come back. |
| -**Rev 6, on the final model: 30,000 seeds, zero violations (43 s); |
| -100,000 seeds, zero violations (144 s).** Across the 100,000 seeds: |
| -180,311 completed operations, among them 1,734 completed moves, 2,341 |
| -clean and 71 dirty rollbacks, 528 pre-flip reverts, 343 declared losses, |
| -33,614 pushes, 103,353 delete-park-free cycles and 1,430 lost disks. 14,373 |
| -requests completed after `H`; 51 staging signatures were refused as stale; |
| -33 sweeps retired stragglers. 670 landings rolled back because a config |
| -bundle was published during the move. |
| +**Rev 7, on the final model (claim rev 5, the biased schedule in half the |
| +seeds): 30,000 seeds, zero violations (28 s); 100,000 seeds, zero |
| +violations (117 s).** Across the 100,000 seeds: 180,848 completed |
| +operations, among them 1,774 completed moves, 2,277 clean and 77 dirty |
| +rollbacks, 565 pre-flip reverts, 345 declared losses, 33,722 pushes, |
| +103,652 delete-park-free cycles and 1,493 lost disks. 24,973 requests |
| +completed after `H`; 30,551 staging signatures were refused as stale |
| +(most after an SDK retry that waited out a long pause). 666 landings rolled |
| +back because a config bundle was published during the move. Rev 6's |
| +figures were 30,000 and 100,000 seeds clean on claim rev 4. |
| There are fewer completed moves than in rev 5 (3,887) for two reasons the |
| stricter model makes real: bundle publications during a move now roll it |
| @@ -1638,96 +1661,94 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| | model 22 (rev 6) | A bundle published after admission rolled the landing back, and then every recovery probe failed against the pinned inputs: stuck forever (J2-R2-5) | recovery probes run on current inputs (§7.7) | moves | |
| | model 23 (rev 6) | A staging round or a push that took its writes from the local database alone, on a box that had lost it, staged an empty snapshot and parked the durable replica | a staging round is the replica plus the final checkpoint (§7.3); a push likewise (F7) | moves, push | |
| | model 24 (rev 6) | The files directory missing on a box whose markers agree: rev 5's model refused it, rev 5's spec does not (`.files-gen` "when the files directory exists"), and the app mints a new `instance.key` | already covered: `files-carried` is now caught alone (§14.2.5); the start check is unchanged | moves | |
| +| model 25 (rev 7) | Claim rev 5's at-rest sweep lists retired locations and dead generations, both under `instances/<host>/`; a staging request completing after the move's cleanup left `moves/<host>/<move id>/` residue for good | the sweep also lists `moves/<host>/` (§6.4); CC20 | claim | |
| +| model 26 (rev 7) | With registrations renewed and drained as claim rev 5 says, a console that paused between renewing and its claim CAS resumed after the drain; the host served after its store was torn down | the create re-checks its registration as the last step before its claim CAS; CC21 | claim | |
| +| model 27 (rev 7) | A target that had begun its dirty return was declared lost; the rollback finished as a clean one and nothing parked the partial return lane in the source's region (1 seed in 100,000) | declare-lost parks the lane (§7.10) | moves | |
| #### 14.2.5 Mutation results |
| -Every rule was dropped in turn, in a scratch copy, on the final rev 6 |
| +Every rule was dropped in turn, in a scratch copy, on the final rev 7 |
| model, with the strict classification of §14.2.1: 3,000 seeds each; 30,000 |
| for every rule not caught at 3,000; 30,000 for each combination below, and |
| -100,000 for the rarest. The model has **60 rules**: rev 5's 50, less |
| -`restore-lineage-filter` (now `restore-by-generation`), plus |
| -`location-per-incarnation`, `start-check-claim-gen`, `door-reread`, |
| -`admission-registration`, `registration-recovery`, `cancelled-creates`, |
| -`orphan-no-deadline`, `straggler-sweep`, `recovery-current-inputs` and |
| -`sign-at-check`. No run was an ERROR. Seed numbers reproduce any line with |
| -`HOSTLIFE_SEED`. |
| +100,000 for the rarest. The model has **64 rules**: rev 6's 60 plus |
| +`sweep-staging` (CC20), `registration-check` (CC21), `sdk-no-resign` |
| +(claim rev 5, CC19) and `lost-return-park` (model 27). No run was an |
| +ERROR. Seed numbers reproduce any line with `HOSTLIFE_SEED`. |
| | | rules | |
| |---|---| |
| -| caught alone | 44 | |
| -| caught only in a stated combination | 10 (five pairs and two triples; one of them, `commit-before-open`, adds nothing to its partner) | |
| +| caught alone | 49 | |
| +| caught only in a stated combination | 12 | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| -| unreachable under claim rev 4 | 1 (`readiness-quiet`) | |
| -| unexercised | 3 (`location-per-incarnation`, `door-by-version`, `door-reread`) | |
| +| unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| +| unexercised | **none** (rev 6 had 3) | |
| -**Caught alone: 44 of 60.** First the rules new or changed in rev 6: |
| +**Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).** |
| -| rule | seeds failing | what the model finds | |
| +| rule | result | what the model finds | |
| |---|---|---| |
| -| `restore-by-generation` (§5.1, J2-R2-1) | 10 / 30,000 | acknowledged writes lost: the newest object under the location was a late or stale one | |
| -| `straggler-sweep` (§6.4, CC15) | 3 / 3,000 | residue nobody retires, after requests that completed past `H` | |
| -| `sign-at-check` (§7.3, CC19) | 1 / 100,000 | staging lands after its cleanup from a box frozen between check and send | |
| -| `recovery-current-inputs` (§7.7, J2-R2-5) | 69 / 3,000 | recovery stuck forever after a bundle published during the move | |
| -| `admission-registration` (claim §5.1, §5.3, J2-R2-2) | 3 / 3,000 | a second host serving after its app's store was torn down | |
| -| `registration-recovery` (CC16) | 894 / 3,000 | purges that never finish | |
| -| `cancelled-creates` (claim §5.1, J2-R2-7) | 365 / 3,000 | a late record that blocks the host forever | |
| -| `orphan-no-deadline` (CC17) | 31 / 3,000 | the same, for a record that lands after `until` | |
| -| `files-carried` (§8, the kpmg outage) | 64 / 3,000 | the app mints a new `instance.key` over sealed data. Rev 5 caught this only with `start-check`; that pairing was an artifact of rev 5's stronger start check (model 24) | |
| - |
| -and the rest, rev 5's rules on the stricter model: |
| +| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 38 / 30,000 | an incarnation's database holds writes of the previous incarnation: a replication PUT accepted before the delete completes after the recreate into the shared location, and the new incarnation's restore replays it; the cold-restore check at a later release and the start check both see it | |
| +| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 47 / 30,000, of which 22 are door violations | a listing authorized for the old incarnation selects, after the recreate, the new incarnation's object in the shared location, and signs it | |
| +| `door-by-version` (claim §6.5) | with `door-reread` and `location-per-incarnation`: 77 / 30,000, of which 51 are door violations (22 without it) | a handle signed before the delete opens the location's current object after the recreate | |
| + |
| +Neither door rule can be violated while C3a holds, under any schedule: a |
| +listing selects only under O1's location, and no later incarnation ever |
| +writes there. They are defence in depth behind C3a, and each is shown |
| +load-bearing once C3a is dropped. |
| + |
| +**Caught alone: 49 of 64.** |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `recovery-pass` | 2,512 / 3,000 | | `fresh-incarnation` | 72 / 3,000 | |
| -| `legacy-discovery` | 558 / 3,000 | | `park-by-version` | 2,200 / 3,000 | |
| -| `park-all-versions` | 745 / 3,000 | | `park-skip-lock` | 2,994 / 3,000 | |
| -| `retirement-ids` | 284 / 3,000 | | `quiet-before-ack` | 187 / 3,000 | |
| -| `hostguard` | 9 / 3,000 | | `purge-reserve-first` | 2,362 / 3,000 | |
| -| `purge-adopts` | 8 / 3,000 | | `purge-journal` | 2,149 / 3,000 | |
| -| `evidence-whole-tree` | 2 / 3,000 | | `evidence-from-state` | 2,940 / 3,000 | |
| -| `floor-boot-recovery` | 2,679 / 3,000 | | `participant-rows` | 7 / 3,000 | |
| -| `revalidate-before-effect` | 11 / 3,000 | | `lost-quarantine` | 4 / 30,000 | |
| -| `cut-deadline` | 9 / 3,000 | | `revert-journal` | 17 / 3,000 | |
| -| `rollback-journal` | 1 / 3,000 | | `dirty-return` | 1 / 3,000 | |
| -| `target-park` | 49 / 3,000 | | `abort-target-owner` | 1,129 / 3,000 | |
| -| `timer-freeze` | 10 / 3,000 | | `timer-canonical` | 2 / 3,000 | |
| -| `markers-last` | 1 / 3,000 | | `source-readiness` | 10 / 3,000 | |
| -| `seal-by-version` | 1 / 3,000 | | `staging-quiet` | 2 / 3,000 | |
| -| `sign-before-safeuntil` | 9 / 3,000 | | `fresh-admission` | 4 / 3,000 | |
| -| `stale-hold-release` | 6 / 3,000 | | `obligations-block-ops` | 22 / 3,000 | |
| -| `claim-op-exclusive` | 93 / 3,000 | | | | |
| - |
| -**Caught only in a combination: 10 rules.** Each partner's own count is |
| -in the second column, so the combination's contribution shows. |
| +| `recovery-pass` | 2,513 / 3,000 | | `fresh-incarnation` | 55 / 3,000 | |
| +| `legacy-discovery` | 627 / 3,000 | | `location-per-incarnation` | 3 / 3,000 | |
| +| `park-by-version` | 2,236 / 3,000 | | `park-all-versions` | 748 / 3,000 | |
| +| `park-skip-lock` | 2,997 / 3,000 | | `retirement-ids` | 274 / 3,000 | |
| +| `quiet-before-ack` | 188 / 3,000 | | `straggler-sweep` | 156 / 3,000 | |
| +| `sweep-staging` | 44 / 3,000 | | `restore-by-generation` | 1 / 3,000 | |
| +| `hostguard` | 16 / 3,000 | | `purge-reserve-first` | 2,383 / 3,000 | |
| +| `purge-adopts` | 13 / 3,000 | | `purge-journal` | 2,128 / 3,000 | |
| +| `admission-registration` | 4 / 3,000 | | `registration-recovery` | 880 / 3,000 | |
| +| `registration-check` | 2 / 3,000 | | `cancelled-creates` | 367 / 3,000 | |
| +| `orphan-no-deadline` | 32 / 3,000 | | `evidence-whole-tree` | 5 / 30,000 | |
| +| `evidence-from-state` | 2,934 / 3,000 | | `floor-boot-recovery` | 2,657 / 3,000 | |
| +| `participant-rows` | 2 / 3,000 | | `revalidate-before-effect` | 15 / 3,000 | |
| +| `sign-before-safeuntil` | 17 / 3,000 | | `sign-at-check` | 10 / 3,000 | |
| +| `sdk-no-resign` | 7 / 3,000 | | `lost-quarantine` | 1 / 3,000 | |
| +| `cut-deadline` | 10 / 3,000 | | `revert-journal` | 22 / 3,000 | |
| +| `rollback-journal` | 1 / 3,000 | | `dirty-return` | 5 / 30,000 | |
| +| `lost-return-park` | 1 / 100,000 | | `target-park` | 45 / 3,000 | |
| +| `abort-target-owner` | 1,150 / 3,000 | | `timer-freeze` | 2 / 3,000 | |
| +| `timer-canonical` | 1 / 3,000 | | `markers-last` | 2 / 3,000 | |
| +| `source-readiness` | 15 / 3,000 | | `seal-by-version` | 8 / 30,000 | |
| +| `staging-quiet` | 4 / 30,000 | | `fresh-admission` | 10 / 3,000 | |
| +| `stale-hold-release` | 4 / 3,000 | | `obligations-block-ops` | 18 / 3,000 | |
| +| `claim-op-exclusive` | 92 / 3,000 | | `recovery-current-inputs` | 58 / 3,000 | |
| +| `files-carried` | 65 / 3,000 | | | | |
| + |
| +**Caught only in a combination: 12 rules.** Each partner's own count, on |
| +the same seeds, shows what the combination adds. |
| | combination | fails | partners alone | what the model finds | |
| |---|---|---|---| |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 19 / 100,000 | each pair of the three: 0 / 30,000 | two writers: **Astra's J2-R2-8 trace.** With the start check as rev 5 wrote it (the third rule dropped), losing the exec check and the conditional open lets a paused open make the old source ready after the commit, and it serves beside the target. Rev 6's start check is the third fence the rev 5 model invented and the rev 5 text lacked | |
| -| `exec-admission` + `hold-op-open` + `start-check` | 4 / 30,000 | (above) | the same trace, dropping the whole start check | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,079 / 30,000 | `revalidate-before-effect` alone 162 / 30,000 | a stale purge step destroys a store | |
| -| `strict-spawn` + `evidence-whole-tree` | 133 / 30,000 | `evidence-whole-tree` alone 8 / 30,000 | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 8,670 / 30,000 | `legacy-discovery` alone 5,714 / 30,000 | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 5 / 100,000 | 0 / 100,000 each | two writers after a frozen target resumes | |
| -| `commit-before-open` + `dirty-return` | 5 / 30,000 | `dirty-return` alone 7 / 30,000 | lost writes; fewer than the partner alone (seed variation), so the model does not separate `commit-before-open` | |
| - |
| -**Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`: |
| -without them a target that cannot render config fails its probe and rolls |
| -back. |
| - |
| -**Unreachable: `readiness-quiet` (T12).** As in rev 5: every retirement |
| -acknowledges only after its own horizon, and CC11 holds. |
| - |
| -**Unexercised: 3.** `location-per-incarnation` (claim C3a) protects against |
| -a request from an old incarnation that completes after the host was |
| -deleted and recreated. In the model, deleting and recreating a host takes |
| -longer than the longest straggler (11 `H`; a 40 `H` tail was also tried), |
| -and the sweep at rest retires stragglers in between; 0 / 100,000. The door |
| -rules are subsumed by C3a, and are not caught with it dropped either |
| -(0 / 30,000 each). These are honest gaps: C3a guards a production case |
| -the model's timing does not reach, where AWS gives no completion bound. |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 19 / 100,000 | each pair of the three: 0 / 30,000 | two writers, Astra's J2-R2-8 trace (rev 6) | |
| +| `exec-admission` + `hold-op-open` + `start-check` | 12 / 30,000 | (above) | the same, dropping the whole start check | |
| +| `door-reread` + `location-per-incarnation` | 47 / 30,000 | `location-per-incarnation` 38 | door reads of another incarnation's data (22) | |
| +| `door-by-version` + `door-reread` + `location-per-incarnation` | 77 / 30,000 | `door-reread` + `location` 47 | more door violations (51 against 22) | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 1,118 / 30,000 | `revalidate-before-effect` 184 | a stale purge step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 139 / 30,000 | `evidence-whole-tree` 5 | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 8,996 / 30,000 | `legacy-discovery` 6,025 | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 7 / 100,000 | 0 / 100,000 each | two writers after a frozen target resumes | |
| +| `commit-before-open` + `dirty-return` | 4 / 30,000 | `dirty-return` 5 | lost writes; adds nothing over the partner, so the model does not separate `commit-before-open` | |
| + |
| +**Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`. |
| + |
| +**Unreachable: `readiness-quiet` (T12).** Every retirement acknowledges |
| +only after its own horizon, and CC11 holds; the biased schedule does not |
| +change that, because it delays only data writes, never an acknowledgement. |
| **Seeds:** 300 in the gate (about a second); the 30,000- and 100,000-seed |
| -baselines and this sweep are the evidence for rev 6. |
| +baselines and this sweep are the evidence for rev 7. |
| #### 14.2.6 What the model does not prove |
| @@ -1751,9 +1772,11 @@ baselines and this sweep are the evidence for rev 6. |
| budget (320), the reverse of production (over 15 minutes against 120 s). |
| Results about orderings carry over; results about which wait fits inside |
| which window do not (J2 §2). |
| -- **Adversarial scheduling is partial.** Paused opens, door reads and |
| - staging signers wake at the worst moment the model knows of; everything |
| - else wakes at random. The admission triple depends on the targeted wake. |
| +- **Adversarial scheduling is partial.** Paused opens, door reads, |
| + staging signers and an earlier incarnation's replica writes wake at the |
| + worst moment the model knows of; everything else wakes at random. The |
| + admission triple, C3a and the door rules depend on those targeted |
| + wake-ups and on the biased recreate. |
| - **Not modelled:** placement (`placing`), sidecars, nested-to-flat path |
| translation beyond the files directory, the db door's multi-console |
| drain, app moves (F5), and `open_budget` (the model's deadline is the |
| @@ -2154,3 +2177,15 @@ that revision and adds CC15 to CC19. |
| | the cut promise against the enforced deadline (N15) | moves | the deadline is the stop-to-open promise less `open_budget`, enforced on the commit's record CAS; T11 budgets every attempt's settle (§7.4) | |
| | D3, D6, I-7, N12 "partly" in the model | moves | per-artifact local parks and independent guard processes taken; spawn-in-flight, cloud fencing proof and executable activation paths remain model gaps (§14.2.6) | |
| | N5 local coverage | claim | claim rev 4 §9's local discovery, modelled with seeded local residue; `legacy-discovery` caught | |
| + |
| +### 22.6 The coordinator's round on rev 6 (claim rev 5, 4a458a9c) |
| + |
| +| request | rev 7 | |
| +|---|---| |
| +| close the never-caught gap: `location-per-incarnation`, `door-by-version`, `door-reread` | a biased schedule in half the seeds: an immediate recreate where the host last served, the old executor's last replication PUT completing at its worst moment within or past `H`, door listings racing the delete and recreate (§14.2.2). C3a is caught alone (38 / 30,000); `door-reread` with C3a dropped; `door-by-version` with both. Neither door rule can fail while C3a holds | |
| +| re-encode CC15 to CC19 as claim rev 5 states them | done: the sweep under a `park-sweep` obligation, renewed registrations with the drain rule, orphans at any time removed by the pass or by a create, `holder.generation`, signatures at the check with an SDK retry that would re-sign (§14.2.2) | |
| +| 30,000 and 100,000 seeds, the full sweep | both clean; 64 rules: 49 alone, 12 in combinations, 2 liveness, 1 unreachable, none unexercised (§14.2.5) | |
| + |
| +Found on the way: CC20 (the sweep must list `moves/<host>/`), CC21 (a |
| +create re-checks its registration right before its claim CAS), and model |
| +27 (declare-lost must park a partial return lane, §7.10). |