| index 120e359bf..5433d133a 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,29 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| |
| **Date:** 2026-10-03 |
| -**Revision:** 7.1. |
| +**Revision:** 7.2. |
| + |
| +- **Rev 7.2** is written against **claim spec rev 5.2** (465fee96), which |
| + adopted CC22: the creator's claim CAS is `If-Match` the ETag read at |
| + registration (`If-None-Match: *` when the claim was absent), a 412 |
| + restarts the create from step 0 with a new registration, the purge |
| + fence is released by writing a free claim, and a new **C5a** says a |
| + claim object is never deleted. The model encodes that text: the 412 |
| + restarts the create instead of abandoning it, and a new rule, |
| + `claim-never-deleted`, lets the mutation delete a fence that found no |
| + claim; dropped, a paused creator's `If-None-Match: *` passes again |
| + (§14.2.2, §14.2.5). Rev 7.2 also closes the gap rev 7.1 left: a |
| + **biased schedule** in half the seeds makes the target's app write in |
| + the settle window, fails the settle check, and stops the target the |
| + moment its first return PUT is out, so declare-lost meets a partial |
| + return lane. `lost-return-park` (model 27) is caught alone (3 / 3,000, |
| + 32 / 30,000), where rev 7.1 reached it in no seed of 300,000. Results: |
| + 30,000 and 100,000 seeds clean; 68 rules (§14.2.5). The reshuffle this |
| + schedule causes moves two rare rules back: `declare-lost-compute` is |
| + combination-only again (0 / 100,000 alone, 3 / 100,000 with |
| + `watchdog-independent`), and `generation-conditional` (model 29) is |
| + unexercised (0 / 300,000; 2 / 100,000 on rev 7.1), listed as such in |
| + `expected-outcomes.txt` as rev 7.1 listed `lost-return-park` (§14.2.5). |
| |
| - **Rev 7.1** is written against **claim spec rev 5.1** (64eec93b), which |
| adopted CC20 (the sweep lists `moves/<host>/`) and answered CC21 with a |
| @@ -150,8 +172,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 5.1 at 64eec93b** on `design-replica-ownership`. Rev 7.1 is |
| - written against rev 5.1; rev 7 against rev 5 (4a458a9c); rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3 |
| + **rev 5.2 at 465fee96** on `design-replica-ownership`. Rev 7.2 is |
| + written against rev 5.2; rev 7.1 against rev 5.1 (64eec93b); rev 7 |
| + against rev 5 (4a458a9c); rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3 |
| (8b5bccb2); rev 4 against rev 2 (cf3a7861). |
| |
| Citations are to this worktree at 7edd4b33 unless they name another branch |
| @@ -250,8 +273,8 @@ asked). |
| |
| 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 CC15 to |
| -CC19 are in claim rev 5, and rev 7's CC20 and CC21 in claim rev 5.1 (CC21 |
| -as a purge fence). Rev 7.1's model requires CC22 (§19.4). |
| +CC19 are in claim rev 5, rev 7's CC20 and CC21 in claim rev 5.1 (CC21 |
| +as a purge fence), and rev 7.1's CC22 in claim rev 5.2, with C5a (§19.4). |
| Until platform-1e adopts them, this spec states each as the behaviour it |
| relies on. |
| |
| @@ -1245,13 +1268,16 @@ the target's park and records an IAM violation on every abort. |
| write conditional on the registration object, so before purge removes |
| a registration whose host claim does not name the create, it CASes that |
| host's claim from free or absent to `{op: {kind: purging, id}}` with no |
| - holder, and releases it to free at `done`. The creator's CAS from free |
| - or absent then fails. The model found the fence needs one more |
| - condition: the creator's CAS must be If-Match the claim ETag it read |
| - when it registered, or a fence placed and released while it was paused |
| - lets it through (CC22, §19.4). The creator's re-read of its |
| - registration just before the CAS stays, as a cheap extra; the model |
| - shows it is not sufficient alone (§14.2.5). |
| + holder, and releases it at `done` by writing a free claim. The |
| + creator's CAS from free or absent then fails. The model found the fence |
| + needs one more condition, and claim rev 5.2 adopted it (CC22, §19.4): |
| + the creator's CAS is If-Match the claim ETag it read when it |
| + registered, or If-None-Match: * if the claim was absent then; a 412 |
| + restarts the create from step 0, with a new registration; and a claim |
| + object is never deleted (C5a there), because deleting a released fence |
| + would let the paused creator's If-None-Match: * succeed. The creator's |
| + re-read of its registration just before the CAS stays, as a cheap |
| + extra; the model shows it is not sufficient alone (§14.2.5). |
| - **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` |
| @@ -1585,6 +1611,33 @@ main host's claim revision) it read when it registered (CC22). |
| it supersedes or If-None-Match when there is none, and the model's S3 |
| answers 412 when the key's current version differs at completion, whether |
| the request completes at once or late (model 29). |
| + |
| +**Rev 7.2: CC22 as claim rev 5.2 states it, and a target stopped |
| +mid-return.** The creator's 412 no longer abandons the create: the plan |
| +drops its registration and starts again at step 0, with a new create id, |
| +a new registration and a new read of the claim, as rev 5.2 §5.1 says |
| +(never a re-read and a retried CAS alone). Over 100,000 seeds 14,136 |
| +creates restart this way, after any claim write between the registration |
| +and the CAS: a sweep's acknowledgement, another create, a fence. A purge fence |
| +records whether it found a claim at all. Its release writes a free claim |
| +(rev 5.2 §5.3, C5a); the mutation of the new rule `claim-never-deleted` |
| +deletes a fence that found no claim instead, so the host's claim is |
| +absent again, and the second host's epoch returns to 0, which is how the |
| +model spells absence there. |
| + |
| +The schedule gains a third bias, in half the seeds, for the interleaving |
| +model 27 exists for. While a landing waits out its settle window, the |
| +target's app does real work (its writes are acknowledged like any |
| +other), and the settle check then fails as it does on a `FailSettle` |
| +box, so the rollback that follows is dirty and the target owes a return. |
| +The moment the target has issued the first PUT of its return lane, |
| +accepted or still in flight, or the second with the return not yet |
| +journaled, the cloud stops the box. The target is destroyed, which is |
| +what declare-lost's compute fencing verifies, and the operator declares |
| +it lost on a later call, with part of the lane in the source's region. |
| +Rev 7's uniform schedule reached this once in 100,000 seeds and rev 7.1's |
| +never; it now happens 106 times in 100,000 seeds, and dirty rollbacks |
| +rise from the 74 per 100,000 rev 7.1 recorded to 96. |
| paginated listings, separate service, wall and monotonic clocks, |
| enrollment and console and updater versions, spawn separate from |
| readiness, and same-operation lease identities. |
| @@ -1686,8 +1739,21 @@ 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.1, on the final model (claim rev 5.1 with CC22, the purge fence, |
| -the paused creator in half the seeds, the conditional marker): 30,000 |
| +**Rev 7.2, on the final model (claim rev 5.2: CC22 with the restart and |
| +C5a; the biased schedules for the recreate, the paused creator and the |
| +target stopped mid-return): 30,000 seeds, zero violations; 100,000 |
| +seeds, zero violations** (32 s and 100 s). Across the 100,000 seeds: |
| +165,856 completed operations, among them 1,611 completed moves, 2,072 |
| +clean and 96 dirty rollbacks, 443 pre-flip reverts, 388 declared losses, |
| +31,686 pushes, 95,205 delete-park-free cycles and 1,418 lost disks. |
| +24,266 requests completed after `H`; 30,885 staging signatures were |
| +refused as stale; 14,136 creates restarted on a 412; 106 targets were |
| +stopped mid-return by the biased schedule; 175 landings failed the |
| +settle check (rev 7.1: 74 dirty rollbacks). 573 landings rolled back |
| +because a config bundle was published during the move. |
| + |
| +**Rev 7.1, on claim rev 5.1 with CC22, the purge fence, |
| +the paused creator in half the seeds, the conditional marker: 30,000 |
| seeds, zero violations; 100,000 seeds, zero violations** (73 s and 259 s, |
| with the mutation sweep running beside them). Across the 100,000 seeds: |
| 166,106 completed operations, among them 1,719 completed moves, 2,027 |
| @@ -1748,114 +1814,135 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| | 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 rev 5.1 answers with a purge fence on the host claim instead, keeping the re-read as a cheap extra (§19.4) | 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; unexercised on rev 7.1, §14.2.5) | declare-lost parks the lane (§7.10) | moves | |
| -| model 28 (rev 7.1) | With claim rev 5.1's purge fence, a creator paused across a whole purge resumed after the fence was released; its claim CAS "from free", read fresh, succeeded, for an app whose store was gone | the CAS is conditional on the claim ETag read when the create registered; CC22 | 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 on rev 7; none of 300,000 on rev 7.1; rev 7.2's biased schedule stops a returning target on purpose, and the rule is caught alone, §14.2.5) | declare-lost parks the lane (§7.10) | moves | |
| +| model 28 (rev 7.1) | With claim rev 5.1's purge fence, a creator paused across a whole purge resumed after the fence was released; its claim CAS "from free", read fresh, succeeded, for an app whose store was gone | the CAS is conditional on the claim ETag read when the create registered; CC22, adopted in claim rev 5.2 with C5a (a claim object is never deleted) | claim | |
| | model 29 (rev 7.1) | An earlier push's `generation.json` PUT completed after the later push's and put the older generation back; the claim and the bucket disagreed and recovery was stuck | `generation.json` is written If-Match the marker it supersedes (§5.1) | moves | |
| |
| #### 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.1 model, with the strict classification: 3,000 seeds |
| +on the final rev 7.2 model, with the strict classification: 3,000 seeds |
| each; 30,000 for every rule not caught at 3,000; 100,000 for every rule |
| -not caught at 30,000; 30,000 for each combination below, and 100,000 for |
| -the rarest. The model has **67 rules**: rev 7's 64 plus |
| -`purge-claim-fence` (CC21 as claim rev 5.1 states it), `fence-etag` |
| -(CC22) and `generation-conditional` (model 29). No run was an ERROR. Seed |
| -numbers reproduce any line with `HOSTLIFE_SEED`. Rev 7's counts are in |
| -the rev 7 spec (7e0c025e); where a rule's count moved, the biased |
| -creator schedule reshuffled every seed. |
| +not caught at 30,000, and 300,000 for the one not caught at 100,000; |
| +30,000 for each combination below, and 100,000 for the rarest. The model |
| +has **68 rules**: rev 7.1's 67 plus `claim-never-deleted` (claim rev 5.2 |
| +C5a). No run was an ERROR. Seed numbers reproduce any line with |
| +`HOSTLIFE_SEED`. Rev 7.1's counts are in the rev 7.1 spec (4267350e); |
| +where a rule's count moved, the third biased schedule reshuffled every |
| +seed, as the second did in rev 7.1. |
| |
| | | rules | |
| |---|---| |
| | caught alone | 51 | |
| -| caught only in a stated combination | 12 | |
| +| caught only in a stated combination | 13 | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| -| unexercised | **1** (`lost-return-park`, below; rev 7 had none) | |
| - |
| -**The purge fence and the re-read.** `purge-claim-fence` (CC21) is caught |
| -alone: 25 / 3,000, 241 / 30,000. `fence-etag` (CC22) is caught alone: 19 |
| -/ 3,000, 186 / 30,000. `registration-check`, the creator's re-read, is |
| -not caught alone at 3,000 or 30,000 seeds: with the fence and the ETag |
| +| unexercised | **1** (`generation-conditional`, below; rev 7.1's was `lost-return-park`) | |
| + |
| +**The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| +(CC21) is caught alone: 25 / 3,000, 261 / 30,000. `fence-etag` (CC22) is |
| +caught alone: 17 / 3,000, 189 / 30,000. `claim-never-deleted` (C5a) is |
| +caught alone: 7 / 3,000, 79 / 30,000: with the fence on an absent claim |
| +released by deleting the object, the paused creator's `If-None-Match: *` |
| +passes, and the host is created, or the second host serves, on a store |
| +the purge tore down (53 of the 79 on the main host while `creating`, 26 |
| +on the second host). `registration-check`, the creator's re-read, is not |
| +caught alone at 3,000 or 30,000 seeds: with the fence and the ETag |
| condition in place, a drained registration always means a changed claim |
| ETag, so the CAS fails whether or not the creator re-reads. The re-read |
| alone, which is what rev 7's CC21 asked for, is shown insufficient in the |
| combination table (`purge-claim-fence` + `fence-etag`). |
| |
| +**`lost-return-park` (model 27), now caught alone: 3 / 3,000, 32 / |
| +30,000, 102 / 100,000** (rev 7: 1 / 100,000; rev 7.1: 0 / 300,000). |
| +With the rule dropped, the biased schedule of §14.2.2 produces the trace |
| +model 27 was written for: the target is stopped after its first return |
| +PUT, the operator declares it lost, the rollback finishes as a clean |
| +one, and the move releases with `moves/<host>/<rollback id>/db` (in 10 |
| +of the 102 seeds the files object too) still in the source's region: |
| +INV-10 at the release. With the rule, the `park-staging` obligation |
| +declare-lost adds retires the lane after its horizon, and the release |
| +waits for it. `claim-never-deleted` at 100,000: 282. |
| + |
| **Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).** |
| |
| | rule | result | what the model finds | |
| |---|---|---| |
| -| `location-per-incarnation` (claim C3a) | **caught alone**: 2 / 3,000, 25 / 30,000 (rev 7: 3 and 38) | 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`: 34 / 30,000, of which 7 are door violations (rev 7: 47 and 22) | 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`: 63 / 30,000, of which 33 are door violations (7 without it; rev 7: 77 and 51) | a handle signed before the delete opens the location's current object after the recreate | |
| +| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 31 / 30,000 (rev 7.1: 2 and 25; rev 7: 3 and 38) | 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`: 40 / 30,000, of which 10 are door violations (rev 7.1: 34 and 7) | 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`: 59 / 30,000, of which 30 are door violations (10 without it; rev 7.1: 63 and 33) | 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: 51 of 67.** |
| +**Caught alone: 51 of 68.** |
| |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `recovery-pass` | 2,508 / 3,000 | | `fresh-incarnation` | 41 / 3,000 | |
| -| `legacy-discovery` | 618 / 3,000 | | `location-per-incarnation` | 2 / 3,000 | |
| -| `park-by-version` | 2,106 / 3,000 | | `park-all-versions` | 696 / 3,000 | |
| -| `park-skip-lock` | 2,881 / 3,000 | | `retirement-ids` | 295 / 3,000 | |
| -| `quiet-before-ack` | 187 / 3,000 | | `straggler-sweep` | 152 / 3,000 | |
| -| `sweep-staging` | 44 / 3,000 | | `restore-by-generation` | 22 / 30,000 | |
| -| `hostguard` | 9 / 3,000 | | `purge-reserve-first` | 2,264 / 3,000 | |
| -| `purge-adopts` | 7 / 3,000 | | `purge-journal` | 2,007 / 3,000 | |
| -| `admission-registration` | 26 / 3,000 | | `registration-recovery` | 1,954 / 3,000 | |
| -| `purge-claim-fence` | 25 / 3,000 | | `fence-etag` | 19 / 3,000 | |
| -| `cancelled-creates` | 375 / 3,000 | | `orphan-no-deadline` | 23 / 3,000 | |
| -| `evidence-whole-tree` | 2 / 3,000 | | `evidence-from-state` | 2,793 / 3,000 | |
| -| `floor-boot-recovery` | 2,512 / 3,000 | | `participant-rows` | 1 / 3,000 | |
| -| `revalidate-before-effect` | 16 / 3,000 | | `sign-before-safeuntil` | 15 / 3,000 | |
| -| `sign-at-check` | 13 / 3,000 | | `sdk-no-resign` | 13 / 3,000 | |
| -| `lost-quarantine` | 1 / 3,000 | | `declare-lost-compute` | 1 / 100,000 | |
| -| `cut-deadline` | 18 / 3,000 | | `revert-journal` | 21 / 3,000 | |
| -| `rollback-journal` | 1 / 3,000 | | `dirty-return` | 5 / 30,000 | |
| -| `target-park` | 60 / 3,000 | | `abort-target-owner` | 1,004 / 3,000 | |
| -| `timer-freeze` | 1 / 3,000 | | `timer-canonical` | 3 / 3,000 | |
| -| `markers-last` | 1 / 3,000 | | `source-readiness` | 10 / 3,000 | |
| -| `seal-by-version` | 1 / 3,000 | | `staging-quiet` | 2 / 3,000 | |
| -| `fresh-admission` | 17 / 3,000 | | `stale-hold-release` | 3 / 3,000 | |
| -| `obligations-block-ops` | 9 / 3,000 | | `claim-op-exclusive` | 83 / 3,000 | |
| -| `recovery-current-inputs` | 60 / 3,000 | | `files-carried` | 78 / 3,000 | |
| -| `generation-conditional` | 2 / 100,000 | | | | |
| - |
| -`declare-lost-compute` was combination-only in rev 7 (0 / 100,000 alone); |
| -on this model one seed in 100,000 (75975) catches it alone: INV-1, two |
| -boxes run the host at once, the two-writer trace the combination found |
| -in rev 7. `expected-outcomes.txt` no longer lists it. |
| - |
| -**Unexercised: `lost-return-park` (model 27).** Rev 7 caught it in one |
| -seed of 100,000; on this model, with every seed's schedule reshuffled by |
| -the creator's pause, no seed of 300,000 reaches a dirty return that a |
| -declare-lost interrupts before the rollback finishes. The rule stays: |
| -it answers a trace the model did produce, and §7.10 states it. |
| +| `recovery-pass` | 2,502 / 3,000 | | `fresh-incarnation` | 45 / 3,000 | |
| +| `legacy-discovery` | 569 / 3,000 | | `location-per-incarnation` | 3 / 3,000 | |
| +| `park-by-version` | 2,066 / 3,000 | | `park-all-versions` | 681 / 3,000 | |
| +| `park-skip-lock` | 2,879 / 3,000 | | `retirement-ids` | 283 / 3,000 | |
| +| `quiet-before-ack` | 192 / 3,000 | | `straggler-sweep` | 135 / 3,000 | |
| +| `sweep-staging` | 43 / 3,000 | | `restore-by-generation` | 4 / 3,000 | |
| +| `hostguard` | 6 / 3,000 | | `purge-reserve-first` | 2,292 / 3,000 | |
| +| `purge-adopts` | 10 / 3,000 | | `purge-journal` | 1,976 / 3,000 | |
| +| `admission-registration` | 39 / 3,000 | | `registration-recovery` | 1,945 / 3,000 | |
| +| `purge-claim-fence` | 25 / 3,000 | | `fence-etag` | 17 / 3,000 | |
| +| `claim-never-deleted` | 7 / 3,000 | | `cancelled-creates` | 373 / 3,000 | |
| +| `orphan-no-deadline` | 29 / 3,000 | | `evidence-whole-tree` | 2 / 3,000 | |
| +| `evidence-from-state` | 2,794 / 3,000 | | `floor-boot-recovery` | 2,534 / 3,000 | |
| +| `participant-rows` | 5 / 3,000 | | `revalidate-before-effect` | 19 / 3,000 | |
| +| `sign-before-safeuntil` | 16 / 3,000 | | `sign-at-check` | 11 / 3,000 | |
| +| `sdk-no-resign` | 11 / 3,000 | | `lost-quarantine` | 12 / 30,000 | |
| +| `cut-deadline` | 15 / 3,000 | | `revert-journal` | 17 / 3,000 | |
| +| `rollback-journal` | 4 / 30,000 | | `dirty-return` | 2 / 3,000 | |
| +| `lost-return-park` | 3 / 3,000 | | `target-park` | 44 / 3,000 | |
| +| `abort-target-owner` | 1,067 / 3,000 | | `timer-freeze` | 7 / 3,000 | |
| +| `timer-canonical` | 4 / 3,000 | | `markers-last` | 15 / 30,000 | |
| +| `source-readiness` | 8 / 3,000 | | `seal-by-version` | 11 / 30,000 | |
| +| `staging-quiet` | 10 / 30,000 | | `fresh-admission` | 17 / 3,000 | |
| +| `stale-hold-release` | 2 / 3,000 | | `obligations-block-ops` | 18 / 3,000 | |
| +| `claim-op-exclusive` | 85 / 3,000 | | `recovery-current-inputs` | 56 / 3,000 | |
| +| `files-carried` | 74 / 3,000 | | | | |
| + |
| +`dirty-return` (INV-2) moves from 5 / 30,000 to 2 / 3,000 and 20 / |
| +30,000: the biased schedule's dirty rollbacks exercise it too. |
| + |
| +`declare-lost-compute` is combination-only again, as it was in rev 7: 0 |
| +/ 3,000, 0 / 30,000, 0 / 100,000 alone on this model (rev 7.1 caught it |
| +in one seed of 100,000), and 3 / 100,000 with `watchdog-independent`. |
| +`expected-outcomes.txt` lists it as a miss again, with the combination. |
| + |
| +**Unexercised: `generation-conditional` (model 29).** Rev 7.1 caught it |
| +in two seeds of 100,000; on this model, with every seed reshuffled by the |
| +mid-return schedule, no seed of 300,000 has an earlier push's |
| +`generation.json` PUT complete after a later push's. The rule stays: it |
| +answers a trace the model did produce, and §5.1 states it. |
| `expected-outcomes.txt` lists it as unexercised, so a seed that reaches |
| -it again is reported. |
| +it again is reported. It is the next gap to close the way rev 7 closed |
| +C3a's and rev 7.2 closed model 27's: a biased schedule that holds the |
| +stale marker PUT until a newer marker is current. |
| |
| -**Caught only in a combination: 12 rules.** Each partner's own count, on |
| +**Caught only in a combination: 13 rules.** Each partner's own count, on |
| the same seeds, shows what the combination adds. |
| |
| | combination | fails | partners alone | what the model finds | |
| |---|---|---|---| |
| -| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 287 / 30,000 | `purge-claim-fence` 241, `fence-etag` 186, `registration-check` 0 | the creator pauses after its re-read; purge drains, tears down and finishes; the CAS from free succeeds: a store destroyed under a creating or serving host. The re-read is not a fence | |
| -| `registration-check` + `purge-claim-fence` | 305 / 30,000 | `purge-claim-fence` 241 | the same, without the re-read's early stops | |
| -| `registration-check` + `fence-etag` | 221 / 30,000 | `fence-etag` 186 | the same: the fence alone cannot refuse a creator that resumes after its release | |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 14 / 100,000 | `exec-admission` + `hold-op-open` 0 / 30,000; `exec-admission` + `start-check-claim-gen` 0 / 30,000; `hold-op-open` + `start-check-claim-gen` 0 / 30,000 | two writers, Astra's J2-R2-8 trace (rev 6) | |
| -| `exec-admission` + `hold-op-open` + `start-check` | 7 / 30,000 | (above) | the same, dropping the whole start check | |
| -| `door-reread` + `location-per-incarnation` | 34 / 30,000 | `location-per-incarnation` 25 | door reads of another incarnation's data (7) | |
| -| `door-by-version` + `door-reread` + `location-per-incarnation` | 63 / 30,000 | `door-reread` + `location` 34 | more door violations (33 against 7) | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,027 / 30,000 | `revalidate-before-effect` 175 | a stale purge step destroys a store | |
| -| `strict-spawn` + `evidence-whole-tree` | 145 / 30,000 | `evidence-whole-tree` 8 | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 9,012 / 30,000 | `legacy-discovery` 6,085 | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 3 / 100,000 | `declare-lost-compute` 1 / 100,000, `watchdog-independent` 0 / 100,000 | two writers after a frozen target resumes | |
| -| `commit-before-open` + `dirty-return` | 3 / 30,000 | `dirty-return` 5 | lost writes; adds nothing over the partner, so the model does not separate `commit-before-open` | |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 299 / 30,000 | `purge-claim-fence` 261, `fence-etag` 189, `registration-check` 0 | the creator pauses after its re-read; purge drains, tears down and finishes; the CAS from free succeeds: a store destroyed under a creating or serving host. The re-read is not a fence | |
| +| `registration-check` + `purge-claim-fence` | 310 / 30,000 | `purge-claim-fence` 261 | the same, without the re-read's early stops | |
| +| `registration-check` + `fence-etag` | 236 / 30,000 | `fence-etag` 189 | the same: the fence alone cannot refuse a creator that resumes after its release | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 12 / 100,000 (4 / 30,000) | `exec-admission` + `hold-op-open` 0 / 30,000; `exec-admission` + `start-check-claim-gen` 0 / 30,000; `hold-op-open` + `start-check-claim-gen` 0 / 30,000 | two writers, Astra's J2-R2-8 trace (rev 6) | |
| +| `exec-admission` + `hold-op-open` + `start-check` | 6 / 30,000 | (above) | the same, dropping the whole start check | |
| +| `door-reread` + `location-per-incarnation` | 40 / 30,000 | `location-per-incarnation` 31 | door reads of another incarnation's data (10) | |
| +| `door-by-version` + `door-reread` + `location-per-incarnation` | 59 / 30,000 | `door-reread` + `location` 40 | more door violations (30 against 10) | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 1,022 / 30,000 | `revalidate-before-effect` 206 | a stale purge step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 130 / 30,000 | `evidence-whole-tree` 11 | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 9,092 / 30,000 | `legacy-discovery` 6,037 | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 3 / 100,000 | `declare-lost-compute` 0 / 100,000, `watchdog-independent` 0 / 100,000 | two writers after a frozen target resumes | |
| +| `commit-before-open` + `dirty-return` | 15 / 30,000 | `dirty-return` 20 | 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`. |
| |
| @@ -1864,7 +1951,7 @@ 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 7.1. |
| +baselines and this sweep are the evidence for rev 7.2. |
| |
| #### 14.2.6 What the model does not prove |
| |
| @@ -1925,7 +2012,7 @@ region that lost. |
| 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 5.1, with CC22 (§19.4) adopted. |
| + console honours it: claim rev 5.2 (CC22 adopted, §19.4). |
| 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. |
| @@ -2119,7 +2206,18 @@ encodes that text (§14.2.2), and finds the fence needs CC22. |
| |
| | id | change to claim rev 5.1 | why (model) | |
| |---|---|---| |
| -| **CC22** | **The creator's claim CAS is conditional on the claim ETag it read when it registered** (`If-Match` that ETag, or `If-None-Match: *` if the claim was absent), not on a read taken just before the CAS. The fence is released at the purge's `done`; a creator paused across the whole purge resumes against a free claim again, and a CAS "from free" conditioned on a fresh read succeeds, for an app whose store is gone. Any fence placed after the creator registered, even one since released, changes the ETag, so the stale condition fails with 412 and the create is refused before any record exists. Two corollaries. The fence on an absent claim must be **released by writing a free claim, never by deleting the object**, or the paused creator's `If-None-Match: *` succeeds again. And a 412 for any reason (a sweep acknowledgement, another create) means the create starts again at §5.1 step 0, with a new registration and a new read; it never re-reads and retries the CAS alone. With this condition the creator's re-read of its registration adds nothing the model can see; it stays as a cheap extra | model 28: a host creating on a torn-down store after a fence was released (`fence-etag`); the re-read alone is shown insufficient (`purge-claim-fence` + `fence-etag`, §14.2.5) | |
| +| **CC22** | **The creator's claim CAS is conditional on the claim ETag it read when it registered** (`If-Match` that ETag, or `If-None-Match: *` if the claim was absent), not on a read taken just before the CAS. The fence is released at the purge's `done`; a creator paused across the whole purge resumes against a free claim again, and a CAS "from free" conditioned on a fresh read succeeds, for an app whose store is gone. Any fence placed after the creator registered, even one since released, changes the ETag, so the stale condition fails with 412 and the create is refused before any record exists. Two corollaries. The fence on an absent claim must be **released by writing a free claim, never by deleting the object**, or the paused creator's `If-None-Match: *` succeeds again. And a 412 for any reason (a sweep acknowledgement, another create) means the create starts again at §5.1 step 0, with a new registration and a new read; it never re-reads and retries the CAS alone. With this condition the creator's re-read of its registration adds nothing the model can see; it stays as a cheap extra | model 28: a host creating on a torn-down store after a fence was released (`fence-etag`); the re-read alone is shown insufficient (`purge-claim-fence` + `fence-etag`, §14.2.5); the deletion corollary is its own rule in rev 7.2 (`claim-never-deleted`, 7 / 3,000) | |
| + |
| +**CC22: adopted in claim rev 5.2** (465fee96), which maps it in its §12: |
| +§5.1 step 0 reads the host's claim and keeps its ETag, or notes that it |
| +is absent, before registering; step 2's CAS is `If-Match` that ETag or |
| +`If-None-Match: *`, and a 412 restarts the create from step 0 with a new |
| +registration; §5.3 releases the fence at `done` by writing a free claim, |
| +never by deleting the object; and a new **C5a** states the corollary as a |
| +rule: a claim object is never deleted, "free" is a written state, and |
| +only the very first claim for a host is created create-only. Rev 7.2's |
| +model encodes that text (§14.2.2) and gives C5a its own mutation |
| +(§14.2.5). No further claim change is requested. |
| |
| **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 |
| @@ -2331,3 +2429,16 @@ answer to CC20 and CC21 is in §22.7. |
| |
| Found on the way: model 29, `generation.json` written If-Match the |
| marker it supersedes (§5.1), a moves-side fix with no claim change. |
| + |
| +### 22.8 Claim rev 5.2's answer to rev 7.1 (465fee96) |
| + |
| +| request (rev 7.1) | claim rev 5.2 | rev 7.2 | |
| +|---|---|---| |
| +| CC22, the creator's claim CAS is If-Match the ETag read at registration | adopted as written (§5.1 steps 0 and 2 there): `If-Match` that ETag, or `If-None-Match: *` when the claim was absent; a 412 restarts the create from step 0 with a new registration. The fence release in §5.3 writes a free claim, never deletes. The deletion corollary becomes **C5a**: a claim object is never deleted; only a host's very first claim is created create-only | re-encoded: the 412 restarts the create (14,136 restarts in 100,000 seeds, after any claim write between the registration and the CAS); the fence remembers whether it found a claim; `claim-never-deleted` is a rule, and its mutation deletes a released fence that found no claim: caught alone, 7 / 3,000 and 79 / 30,000, as the paused creator's `If-None-Match: *` passing again (§14.2.5). `fence-etag` stays caught alone (17 / 3,000) | |
| +| (rev 7.1's own gap) `lost-return-park` unexercised, 0 / 300,000 | no claim change: the lane is this spec's (§7.10) | a third biased schedule stops a returning target mid-return (§14.2.2); the rule is caught alone, 3 / 3,000 and 32 / 30,000 (§14.2.5) | |
| + |
| +The reshuffle moved two rare rules: `declare-lost-compute` is |
| +combination-only again, with `watchdog-independent` (3 / 100,000), and |
| +`generation-conditional` is unexercised (0 / 300,000; 2 / 100,000 on rev |
| +7.1) and listed as such in `expected-outcomes.txt`, the treatment rev 7.1 |
| +gave `lost-return-park`. |