carlos / platform Public

spec: move-any-app rev 7.1 on claim rev 5.1 (CC20, CC21, model 29) (#175)

Written against claim rev 5.1 (64eec93b), which adopted CC20 as written
and CC21 as a purge fence on the host claim. The model (93bf5edb,
45e16b1d) encodes the fence, a creator paused between its re-read and its
claim CAS, and the conditional generation.json marker, and finds CC22:
the creator's claim CAS must be If-Match the ETag it read when it
registered, or a fence placed and released during the pause lets it
through.

Results on this model: 30,000 and 100,000 seeds clean. 67 rules: 51
caught alone (purge-claim-fence 25 / 3,000, fence-etag 19 / 3,000,
generation-conditional 2 / 100,000, declare-lost-compute now 1 / 100,000
alone), 12 in stated combinations, 2 liveness, 1 unreachable, and
lost-return-park unexercised (0 / 300,000; 1 / 100,000 on rev 7). The
re-read alone (purge-claim-fence + fence-etag dropped) is caught 287 /
30,000. expected-outcomes.txt follows: declare-lost-compute is no longer
an expected miss, lost-return-park is.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

claude 3 weeks ago 4267350ef7d5322b134cf6049005751769041461 parent 45e16b1

2 files changed, +218 −76

docs/superpowers/specs/2026-10-02-move-any-app-design.md +216 −74
internal/sim/hostlife/expected-outcomes.txt +2 −2

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 16cf185a2..120e359bf 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,29 @@

# Move any app or instance to another region: Phase 1, a safe single-instance move

**Date:** 2026-10-03

-**Revision:** 7.

-- **Rev 7** is written against **claim spec rev 5** (4a458a9c on

+**Revision:** 7.1.

+- **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

+ **purge fence** on the host claim instead of the creator-side check

+ rev 7 proposed: S3 cannot condition one object's write on another's

+ version. The model encodes the fence, a biased schedule that pauses a

+ creator between its registration re-read and its claim CAS, and finds

+ one more condition the fence needs: the creator's claim CAS must be

+ conditional on the claim ETag it read **when it registered** (CC22),

+ or a fence placed and released while it slept lets it through

+ (§14.2.5, §19.4). It also fixes a moves-side fault the 100,000-seed run

+ surfaced: `generation.json` is a reused key, and an earlier push's PUT

+ completing late put an older generation back and left recovery stuck;

+ the marker is now written If-Match the one it supersedes (model 29,

+ §5.1). Results: 30,000 and 100,000 seeds clean; 67 rules, 51 caught

+ alone (the fence and the ETag condition among them), 12 in stated

+ combinations, the re-read alone shown insufficient (287 / 30,000), and

+ `declare-lost-compute` now caught alone (§14.2.5). The mutation harness

+ runs one prebuilt test binary under `$TMPDIR`, with no copies of the

+ source (§14.2.1).

+- **Rev 7** was written against **claim spec rev 5** (4a458a9c on

`design-replica-ownership`), which adopted CC15 to CC19. It:

- closes the model's last gap: a **biased schedule** beside the uniform

one recreates a host where it last served while the previous

@@ -130,8 +150,8 @@ 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 at 4a458a9c** on `design-replica-ownership`. Rev 7 is written

- against rev 5; rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3

+ **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

(8b5bccb2); rev 4 against rev 2 (cf3a7861).

Citations are to this worktree at 7edd4b33 unless they name another branch

@@ -181,7 +201,7 @@ traffic is undone automatically (§7.8); after the target opens, R4 stands.

### 0.4 The host lifecycle claim

-From claim spec rev 5 (§2 to §10 there), the parts this spec relies on:

+From claim spec rev 5.1 (§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`;

@@ -216,8 +236,9 @@ From claim spec rev 5 (§2 to §10 there), the parts this spec relies on:

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 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

+ other box (§9); app admission registration, closed and drained by purge,

+ which fences a drained registration's host claim before removing it

+ (§5.1, §5.3, CC21); `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).

@@ -229,7 +250,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. Rev 7's model requires CC20 and CC21 (§19.4).

+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).

Until platform-1e adopts them, this spec states each as the behaviour it

relies on.

@@ -417,10 +439,20 @@ field.

|---|---|---|---|

-| `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"}` |

+| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"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"}` |

+`generation.json` is the one reused key a generation writes: everything

+else lives under the generation's own prefix. Without the condition, an

+earlier publication that completes late puts an older generation back:

+the claim names the new generation, the bucket names the old one, and

+every wake and recovery probe refuses: the start check compares the

+markers with the claim's generation and refuses forever (model 29; the

+model finds it after a push in 2 seeds of 100,000, §14.2.5). With the

+condition the late write fails with 412 (claim §13 rows 5 and 6), and

+the later generation stays.

All three are **protocol metadata**: excluded from the archive, from every

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

@@ -673,8 +705,8 @@ holds off any new operation over that region until it acknowledges (CC11),

and every delete names a snapshot version, so nothing written later is

touched.

-**This spec adds `moves/<host>/` (CC20).** Claim rev 5's list leaves out

-staging. A staging request accepted before its lease ended can complete

+**`moves/<host>/` too (CC20, in claim rev 5.1).** Claim rev 5's list left

+out staging. A staging request accepted before its lease ended can complete

after the staging cleanup, and after the move's release nothing lists

`moves/<host>/<move id>/` again. The sweep also parks everything under

`moves/<host>/` while no operation runs, when no move is staging there.

@@ -1207,7 +1239,19 @@ the target's park and records an IAM violation on every abort.

through, and the stalled purge then tore down the new incarnation's

store. The reservation records the purge's phase; recovery drives those

phases in order; only the purge's own completion removes it, never

- `free`.

+ `free`. **The purge fence (claim rev 5.1, CC21):** a creating console

+ can renew its registration, pause, and resume after purge's drain has

+ removed that registration as expired. S3 cannot make the creator's claim

+ 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).

- **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`

@@ -1466,13 +1510,19 @@ combination-only, unexercised), each with its reason. The sweep exits

nonzero on any ERROR, any unexpected MISSED, and any expected miss that is

now caught (STALE).

-Mutation checks run in a scratch copy of the tree, never in place:

-`internal/sim/hostlife/mutate.sh <seeds> [rule | a,b ...]` copies `go.mod`,

-`go.sum` and the package to a scratch directory per rule, sets

-`var mutated = "<rule>"` (or `"a,b"` for a pair, `"a,b,c"` for a triple),

-runs the seeds, reports CAUGHT or MISSED, and deletes the copy. Rules run

-in parallel. Scratch copies live under `$HOSTLIFE_SCRATCH`, by default

-`~/.cache/hostlife-sim`, never `/tmp`.

+**Rev 7.1: one binary, no copies.** Mutation checks never touch the

+source. The test binary is built once (the only step that writes the Go

+build cache); `mutate.sh` then runs it once per rule with

+`HOSTLIFE_MUTATE=<rule>` (or `a,b` for a pair, `a,b,c` for a triple), in

+parallel. It refuses a binary older than the source. Its scratch (the

+binary, each run's log, the verdicts) lives under `$TMPDIR/hostlife-sim`

+and is removed once, after the whole sweep:

+```

+go test -c -o "$TMPDIR/hostlife-sim/hostlife.test" ./internal/sim/hostlife/

+internal/sim/hostlife/mutate.sh 3000 # every rule

+internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a combination

+```

#### 14.2.2 What it models

@@ -1513,7 +1563,28 @@ than any straggler):

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,

+**Rev 7.1: the purge fence, and a creator that pauses at its worst

+moment.** The model now encodes claim rev 5.1 §5.3 step 1b: before the

+drain removes an expired registration whose host claim does not name the

+create, purge CASes that host's claim from free or absent to a fence

+`{op: {kind: purging, id}}` with no holder; a fence already held by

+another purge makes it wait; a claim held by anyone else needs no fence,

+because the creator's CAS from free fails against it anyway. The purge id

+is kept in the reservation, so a purge resumed by the recovery pass

+releases its own fences at `done`, and the pass leaves a holderless

+`purging` claim alone. The creator's re-read of its registration is a

+step of its own, and a new fault class, in half the seeds, pauses the

+console there, after the re-read and before the claim CAS, for 100 to

+300 steps, past the registration's 60-step expiry, so a purge can drain

+the registration, fence, tear the store down and release while it sleeps.

+The second host's claim carries an epoch that every write advances, the

+model's ETag, and the creator's CAS is conditional on the epoch (or the

+main host's claim revision) it read when it registered (CC22).

+`generation.json` is written with a conditional PUT, If-Match the version

+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).

paginated listings, separate service, wall and monotonic clocks,

enrollment and console and updater versions, spawn separate from

readiness, and same-operation lease identities.

@@ -1615,7 +1686,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, on the final model (claim rev 5, the biased schedule in half the

+**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

+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

+clean and 74 dirty rollbacks, 473 pre-flip reverts, 287 declared losses,

+31,885 pushes, 95,232 delete-park-free cycles and 1,374 lost disks. 24,294

+requests completed after `H`; 30,994 staging signatures were refused as

+stale. 564 landings rolled back because a config bundle was published

+during the move. There are fewer completed operations than rev 7's

+180,848, nearly all of the difference in delete-park-free cycles (103,652

+then): the paused creator is the one delay rev 7.1 adds, and it holds a

+create back for up to 300 steps in half the seeds.

+**Rev 7, on 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

@@ -1662,84 +1747,115 @@ Each was a failing seed first, then a rule; each rule's mutation is in

| 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 |

+| 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 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, 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 **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`.

+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

+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.

| | rules |

|---|---|

-| caught alone | 49 |

+| caught alone | 51 |

| caught only in a stated combination | 12 |

| liveness only | 2 (`readiness-key`, `config-before-probe`) |

| unreachable under claim rev 5 | 1 (`readiness-quiet`) |

-| unexercised | **none** (rev 6 had 3) |

+| 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

+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`).

**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**: 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 |

+| `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 |

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.**

+**Caught alone: 51 of 67.**

|---|---|---|---|---|

-| `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 |

+| `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 |

-| `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 | | | |

+| `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.

+`expected-outcomes.txt` lists it as unexercised, so a seed that reaches

+it again is reported.

**Caught only in a combination: 12 rules.** Each partner's own count, on

the same seeds, shows what the combination adds.

|---|---|---|---|

+| `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 |

+| `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) |

**Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`.

@@ -1748,7 +1864,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.

+baselines and this sweep are the evidence for rev 7.1.

#### 14.2.6 What the model does not prove

@@ -1809,7 +1925,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, with CC20 and CC21 (§19.4) adopted.

+ console honours it: claim rev 5.1, with CC22 (§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.

@@ -1983,13 +2099,28 @@ in its §12: CC15 to §6.2a's at-rest sweep; CC16 to §5.1 step 0 and §5.3

step 1b; CC17 to §5.1 step 5; CC18 to §2 `holder.generation`; CC19 to C3's

staging-work lease exception. Rev 7's model encodes that text.

-**Rev 7's requests, against claim rev 5 (4a458a9c):**

+**Rev 7's requests, against claim rev 5 (4a458a9c): both adopted in claim

+rev 5.1 (64eec93b),** which maps them in its §12: CC20 to §6.2a's at-rest

+sweep, as written; CC21 to §5.3 step 1b, differently. S3 cannot make the

+creator's claim write conditional on the registration object, so purge

+fences the **host claim** instead: before removing an expired registration

+whose host claim does not name the create, it CASes a free or absent claim

+to `{op: {kind: "purging", id: <purge id>}}` with no holder, and releases

+the fence to free at `done`. The creator's re-read of its registration

+stays as a cheap extra, not sufficient on its own. Rev 7.1's model

+encodes that text (§14.2.2), and finds the fence needs CC22.

| id | change to claim rev 5 | why (model) |

|---|---|---|

| **CC20** | **The at-rest sweep also lists `moves/<host>/`.** §6.2a's sweep lists retired incarnations' locations and dead generations, both under `instances/<host>/`. A staging request accepted before its lease ended can complete after the staging cleanup, and after the move releases nothing lists `moves/<host>/<move id>/` again. Add `moves/<host>/` to the sweep's list for a host with no operation running | model 25: staging residue that nothing ever retires (`sweep-staging`) |

| **CC21** | **A create checks its registration immediately before its claim CAS.** Renewal keeps a live create's registration from expiring, but a console that pauses between renewing and its claim CAS can resume after the drain removed the expired, unclaimed registration and purge fixed its host set; its claim CAS then succeeds, and the host serves after its store was torn down. Re-read the registration (still present, renewed within the lease) as the last step before the claim CAS, with the §3.1 margin, and abandon the create if it is gone | model 26: a host serving after its app's store was torn down (`registration-check`) |

+**Rev 7.1's request, against claim rev 5.1 (64eec93b):**

+| 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) |

**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

@@ -2188,4 +2319,15 @@ that revision and adds CC15 to CC19.

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).

+27 (declare-lost must park a partial return lane, §7.10). Claim rev 5.1's

+answer to CC20 and CC21 is in §22.7.

+### 22.7 Claim rev 5.1's answer to rev 7 (64eec93b)

+| request (rev 7) | claim rev 5.1 | rev 7.1 |

+|---|---|---|

+| CC20, the sweep lists `moves/<host>/` | adopted as written (§6.2a there) | re-encoded; `sweep-staging` stays caught alone (§14.2.5) |

+| CC21, a create re-checks its registration before its claim CAS | adopted differently (§5.3 step 1b there): S3 cannot condition one object's write on another's version, so purge **fences the host claim** before removing a drained registration, and releases it at `done`; the re-read stays as a cheap extra | re-encoded with a biased schedule that pauses the creator between the re-read and the CAS (§14.2.2). The fence is load-bearing (`purge-claim-fence`), and the re-read alone is shown insufficient (§14.2.5). The model finds the fence needs one more condition, **CC22**: the CAS is If-Match the ETag read at registration, or a fence placed and released during the pause lets the creator through (model 28, §19.4) |

+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.

diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt

index 8b4d68582..25fe92435 100644

--- a/internal/sim/hostlife/expected-outcomes.txt

+++ b/internal/sim/hostlife/expected-outcomes.txt

@@ -7,8 +7,7 @@ commit-before-open missed caught with dirty-return

config-before-probe missed liveness only: a target that cannot render config fails its probe and rolls back

readiness-key missed liveness only: T2 avoids a pointless cut

readiness-quiet missed unreachable under claim rev 4: acknowledgements wait out their own horizon and CC11 holds

-declare-lost-compute missed caught with watchdog-independent (100000 seeds)

-watchdog-independent missed caught with declare-lost-compute (100000 seeds)

+watchdog-independent missed caught with declare-lost-compute (100000 seeds); declare-lost-compute alone is 1 / 100,000 on rev 7.1

exec-admission missed one of three admission fences; caught with hold-op-open and start-check-claim-gen

hold-op-open missed one of three admission fences; caught with exec-admission and start-check-claim-gen

start-check-claim-gen missed one of three admission fences; caught with exec-admission and hold-op-open

@@ -18,3 +17,4 @@ touched-incomplete missed caught with legacy-discovery

door-reread missed subsumed by C3a: caught with location-per-incarnation

door-by-version missed subsumed by C3a: caught with door-reread and location-per-incarnation

registration-check missed a cheap extra: subsumed by purge-claim-fence and fence-etag together

+lost-return-park missed unexercised on rev 7.1: 0 / 300,000 (1 / 100,000 on rev 7, before the creator's pause reshuffled every seed)