amadan
spec: move-any-app rev 7.18, joint round 17's two P3s
R17-1: INV-23 checks every reference a scoped park archives or deletes, fresh or replayed, whatever rules are on; the operations' own parks are scoped; TestForeignManifestReplayRefused. R17-2: the scope grammar's moves/<host> form is used by a delete's staging park (§5.2) and by an at-rest sweep, each while no operation stages there (claim rev 6.26, 98b45332). Round 17 was clean: A, B and C ready for moves Phase 1 implementation planning. No rule change; the gate alone (300 seeds and a 3,000-seed check, clean); model 9c417aaa; code main 67547f5.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+72
−9
docs/superpowers/specs/2026-10-02-move-any-app-design.md+72 −9
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 318a24138..e2588c24e 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,25 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-06 |
| -**Revision:** 7.17. |
| +**Revision:** 7.18. |
| + |
| +- **Rev 7.18** folds in **joint round 17**'s two P3s |
| + (`CODEX-FINDINGS-JOINT-R17.md`, cited "R17-n"); the round was **clean**, |
| + A, B and C ready for moves Phase 1 implementation planning, after |
| + seventeen rounds. Claim rev 6.26 (98b45332) fixes R17-2 on its side; |
| + the code is main at 67547f5. **R17-1:** the model's INV-23 now checks |
| + scope membership for every reference a scoped park archives or |
| + deletes, in the manifest it builds and in a persisted manifest it |
| + replays, whatever rules are on; an out-of-scope reference is a |
| + violation and is never acted on (rev 7.17 checked candidate keys, and |
| + only with the confinement rule off); the operations' own parks run |
| + under a scope of `holder.location`; `TestForeignManifestReplayRefused` |
| + replays a manifest naming another incarnation's key under a valid |
| + scope. **R17-2:** the scope grammar's `moves/<host>` form is used by a |
| + delete's park of the staging namespace (§5.2) and by an at-rest sweep, |
| + each while no operation stages there, as claim rev 6.26 says. No rule |
| + change (107 rules; 73 witnesses): the gate alone, per §14.2.1; the |
| + mutation tables stand at rev 7.17's. |
| - **Rev 7.17** answers **joint round 16** (`CODEX-FINDINGS-JOINT-R16.md`, |
| cited "R16-n") and is written against **claim spec rev 6.24** |
| @@ -2094,8 +2112,9 @@ box-local map that the restart cleared; witness |
| `wParkScopeSurvivesRestart`). **`location`** is exactly one of |
| `instances/<host>`, `instances/<host>/<incarnation>`, `moves/<host>/<op |
| id>` (a move's staging or a rollback's return lane, the op id with no |
| -`/`) or `moves/<host>` (the staging sweep only, while no operation |
| -stages there), nothing else and no trailing `/` (the model's INV-23 |
| +`/`) or `moves/<host>` (used by a delete's park of the staging namespace, |
| +§5.2, and by an at-rest sweep, each while no operation stages there; |
| +claim rev 6.26, R17-2), nothing else and no trailing `/` (the model's INV-23 |
| checks every scope against that grammar). **`incarnation`** names the |
| archive: the location's own, the staging op's holder incarnation, or, |
| for a free host's `moves/<host>` sweep, the newest retired incarnation. |
| @@ -2164,8 +2183,10 @@ its listing is confined to the scope's namespace (an `instances/…` |
| scope never lists or parks anything under `moves/`, the legacy |
| `instances/<host>` scope excludes child incarnations, a staging lane's |
| scope only its own lane), and every key a chore would archive must be a |
| -member of its scope (the model's INV-23 checks membership on the |
| -manifest's sources, not only the location's syntax; rev 7.16 scoped the |
| +member of its scope (the model's INV-23 checks membership for every |
| +reference a park archives or deletes, in the manifest it builds and in a |
| +persisted manifest it replays, whatever rules are on, and an out-of-scope |
| +reference is never acted on, R17-1; rev 7.16 scoped the |
| whole `instances/<host>/` listing as `instances/<host>` under the |
| serving incarnation and archived a deleted incarnation's late object |
| from there; witness `wSweepScopeMembership`). The same confinement |
| @@ -3011,7 +3032,8 @@ this text wins. |
| R16-2): the sweep's chores are grouped by location, each with its |
| archive incarnation; an `instances/…` scope never touches `moves/` |
| and the legacy `instances/<host>` scope excludes child incarnations; |
| - INV-23 checks membership for every key a chore archives. |
| + INV-23 checks membership for every reference a chore archives or |
| + deletes, fresh or replayed from a persisted manifest (R17-1). |
| A free host's at-rest sweep is a holderless `parking` op with |
| `intent.park_sweep`, no exec and no holder, which blocks the successor |
| create until `FreeAfterPark` frees the claim in its last |
| @@ -3419,8 +3441,10 @@ but produced no witness output as an ERROR, never as "none" (R3-6). |
| `TestInterruptedCleanReturn`, the run walk across regions (§5.1 step 9, |
| rev 7.14), `TestJoinHolderlessSweep`, two regions' residue under one |
| holderless op (§6.4, rev 7.15), `TestLegacyLostTargetReturn`, the legacy |
| -identity through a lost-target return, and `TestStagingSurvivesLegacyPark`, |
| -sealed staging beside a legacy instance park (rev 7.17). |
| +identity through a lost-target return, `TestStagingSurvivesLegacyPark`, |
| +sealed staging beside a legacy instance park (rev 7.17), and |
| +`TestForeignManifestReplayRefused`, a persisted manifest naming another |
| +incarnation's key refused under a valid scope (rev 7.18). |
| **Rev 7.6: the pinned libraries, observed.** `internal/sim/litestreamfacts/` |
| is a second test-only package: it drives litestream v0.5.14 and |
| @@ -3946,6 +3970,24 @@ readiness, and same-operation lease identities. |
| review's 3 GiB workload is reproduced (108.68 s with three passes at one |
| rate, 124.04 s with the fourth) and refused by rev 7.7's arithmetic. |
| +**Rev 7.18: joint round 17 (R17-1).** `parkStep` and `parkDepth` take |
| +the chore's scope; `member(scope, id, what, ref)` is INV-23's second |
| +half, checked for every reference the fresh manifest would archive or |
| +delete and for every reference of a replayed persisted manifest, with no |
| +rule gating; an out-of-scope reference is a violation, excluded from the |
| +sets and never deleted. The rule `scope-membership` keeps the listing's |
| +confinement as the implementation; the candidate-key check that ran only |
| +with the rule off is gone. The operations' own parks (a landing's |
| +install park of the target region's earlier stay, a dirty return's and a |
| +push's) run under `opScope(c, prefix)`, `holder.location` with the |
| +holder's incarnation, confined by `confine(prefix)`. |
| +`TestForeignManifestReplayRefused`: incarnation 2 serving, a persisted |
| +manifest at a sweep chore's destination naming a late object of |
| +incarnation 1 under the chore's valid `instances/<host>/2` scope; one |
| +step of the chore refuses it with INV-23 and the object survives (a |
| +later at-rest sweep may park it under incarnation 1's own scope, which is |
| +the right chore). No rule changed, so the gate alone was run (§14.2.1). |
| + |
| **Rev 7.17: joint round 16 and claim rev 6.24.** |
| - **Scope membership (R16-2).** `scopeOf(k)` is the scope location a |
| @@ -4815,6 +4857,10 @@ 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 7.18** changed no rule and ran the gate only (§14.2.1): 300 seeds, |
| +zero violations, plus a 3,000-seed check, zero violations; the numbers |
| +below are rev 7.17's, on model b9e97783. |
| + |
| **Rev 7.17, on the final model (joint round 16, claim rev 6.24: scope |
| membership, the legacy identity, the narrowed born-covered): 30,000 |
| seeds, zero violations** (84 s; no 100,000-seed run under the |
| @@ -5286,7 +5332,7 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| #### 14.2.5 Mutation results |
| Every rule was dropped in turn, with the one prebuilt binary of §14.2.1, |
| -on the final rev 7.17 model (b9e97783), with the strict classification, |
| +on the final rev 7.17 model (b9e97783; rev 7.18 changed no rule and ran no sweep, §14.2.1), with the strict classification, |
| **in two ways**: the **random sweep**, 3,000 seeds each (the 30,000- and |
| 100,000-seed sweeps of earlier revisions are not run under the evidence |
| policy of §14.2.1, Paul 2026-10-06; their columns say so); and |
| @@ -6159,6 +6205,11 @@ although the seal carries every write; the admitted writer's start |
| agent loop; and the model's C2 already binds every CAS to `op.id`, so |
| the `admit-bind-op` witness needs both rules off. |
| +**Claim rev 6.26 (98b45332), after joint round 17: R17-2 fixed on the |
| +claim's side.** `moves/<host>` is used by a delete's park of the staging |
| +namespace (§5.2) and by an at-rest sweep, each while no operation stages |
| +there; §6.4 here says the same. No notes. |
| + |
| **Claim rev 6.24 (0b821896), after joint round 16, and rev 6.25 |
| (413b12cb), which answers the four notes below: note 1 agreed and now |
| §5.2 (a delete's `park-replica` per touched region is scoped to |
| @@ -6766,6 +6817,18 @@ answers the rest and reruns every number. |
| | R6-5 (P3) replayed anchor bytes differ (the encoder's `time.Now()`) | the encoding inputs, timestamp included, are journaled in the install manifest before the PUTs and a replay reuses a current object (§5.1 step 2, §7.6 `building`); `TestFact_R6_5_AnchorReplayBytes` shows identical bytes for identical inputs and different bytes one millisecond apart | |
| | fidelity: compaction deleted the newest level-0 file, creating anchor-required cold restores the library would not | compaction keeps the newest input (§14.2.2); time-based level-0 retention stays deferred (§14.2.6) | |
| +### 22.24 Joint round 17 (claim 413b12cb, moves rev 7.17 39904c84, model b9e97783, merged code 67547f5) |
| + |
| +**Clean.** A, B and C ready for moves Phase 1 implementation planning; |
| +no P1 or P2; two P3s, folded in by rev 7.18. Claim rev 6.26 (98b45332) |
| +fixes R17-2 on its side. |
| + |
| +| finding | rev 7.18 | |
| +|---|---| |
| +| R17-1 (P3) INV-23 checked candidate keys only with the confinement rule off; actual archive and delete references, and a replayed persisted manifest, were not independently checked | `member` checks every archive and delete reference, fresh and replayed, whatever rules are on; an out-of-scope reference is a violation and is never acted on; the operations' own parks are scoped; `TestForeignManifestReplayRefused` (§6.4, §7.14 item 9, §14.2.2) | |
| +| R17-2 (P3) the scope grammar said `moves/<host>` was sweep-only while §5.2's delete needs it | the grammar names both users, each while no operation stages there, as claim rev 6.26 does (§6.4) | |
| +| the named integration requirements (delete wiring, archive destinations, the pull door's move kinds, evidence timestamps, `quiet_after`) | carried into Phase 1 planning, not spec changes | |
| + |
| ### 22.23 Joint round 16 (claim 876d6908, moves rev 7.16 6f2a93c9, model 6bfae153, merged code 7f403a77) |
| Round 16 found R15-1 resolved, no P1 and three P2s: two in the merged |