carlos / platform Public

spec: move-any-app rev 7.3: deterministic witness scenarios (#175)

The model gains one fixed, hand-scheduled witness scenario per rule the
random sweep catches rarely or only in combination (witness_test.go):
22 scenarios for 20 rules, each forcing the interleaving its rule
exists for under a quiet RNG, holding with the rules in place and
violating an invariant under the rule's mutation, alone or in the
stated combination. Witnesses never draw from a seed's RNG, so adding
one reshuffles nothing. mutate.sh runs them beside the sweep and
reports both; a rule counts as caught if either catches it.

Caught alone by their witness: generation-conditional and
declare-lost-compute (sweep 0 / 100,000 each), and the five rules the
sweep reaches only at 30,000. Held alone and violated in their
combination, the redundancy shown rather than inferred:
watchdog-independent, claim-cas-opid, commit-before-open, the admission
triple and start-check, strict-spawn, touched-incomplete, door-reread,
door-by-version (C3a alone suffices), registration-check (either
partner).

Found on the way: the purge drain iterated registrations in Go map
order, the model's one source of nondeterminism; fixed, and every
count rerun on the deterministic model. Baselines 30,000 and 100,000
seeds clean. 68 rules: 53 caught alone, 12 in stated combinations, 2
liveness, 1 unreachable, none unexercised.

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

claude 3 weeks ago dc7f2a63ac3c8b66de01c2695bdee6391e0f710c parent c856228

2 files changed, +213 −96

docs/superpowers/specs/2026-10-02-move-any-app-design.md +212 −95
internal/sim/hostlife/world_test.go +1 −1

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 5433d133a..49bf7f02e 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,28 @@

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

**Date:** 2026-10-03

-**Revision:** 7.2.

+**Revision:** 7.3.

+- **Rev 7.3** adds **deterministic witness scenarios** to the model

+ (§14.2.2, `witness_test.go`): one fixed, hand-scheduled scenario per

+ rule the random sweep catches rarely or only in combination, 22

+ scenarios for 20 rules. Each forces exactly the interleaving its rule

+ exists for, under a quiet RNG that injects nothing, holds with the

+ rules in place, and violates an invariant under the rule's mutation,

+ alone or in the stated combination. Witnesses never draw from a seed's

+ RNG, so adding one reshuffles nothing, and the whack-a-mole of rev 7.1

+ (`lost-return-park`) and rev 7.2 (`generation-conditional`) ends.

+ `mutate.sh` runs them beside the sweep and reports both; a rule counts

+ as caught if either catches it. Nine rules are caught alone by their

+ witness, `generation-conditional` and `declare-lost-compute` among

+ them, which the sweep misses at 100,000; eleven hold alone and violate

+ in their combination, which is the redundancy the combination table

+ states, shown rather than inferred (§14.2.5). Found on the way: the

+ purge drain iterated registrations in Go map order, the model's one

+ source of nondeterminism; it drains in create-id order now and two

+ runs agree exactly. Results: 30,000 and 100,000 seeds clean; 68 rules,

+ 53 caught alone, 12 in stated combinations, 2 liveness, 1 unreachable,

+ **none unexercised**.

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

@@ -1550,6 +1571,23 @@ internal/sim/hostlife/mutate.sh 3000 # every rule

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

```

+**Rev 7.3: the witnesses.** `TestWitnesses` runs in the gate: every

+witness scenario (§14.2.2) must hold. Under `HOSTLIFE_MUTATE=<rule>` it

+runs that rule's witnesses and reports each as violated or held; a

+witness that must violate under the mutation and holds fails the test.

+`mutate.sh` runs both tests for every rule and prints one verdict line

+with the two results side by side:

+```

+CAUGHT lost-quarantine: sweep 0 of 3000; witness violated

+CAUGHT fence-etag: sweep 17 of 3000 (first seed 341); witness none

+EXPECTED-MISS exec-admission: sweep 0 of 3000; witness held

+```

+A rule is caught if either catches it. A witness run that fails is an

+ERROR (the witness is broken, not the rule). `HOSTLIFE_WITNESS=<rule>`

+runs one rule's witnesses with their full trace.

#### 14.2.2 What it models

**Rev 6 (joint round 2): the model encodes the specs, nothing stronger.**

@@ -1638,6 +1676,41 @@ 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.

+**Rev 7.3: deterministic witness scenarios.** Beside the random sweep,

+`witness_test.go` holds one fixed, hand-scheduled scenario per rule the

+sweep catches rarely or only in combination (22 scenarios, 20 rules;

+§14.2.5 lists them). A witness builds a clean world (three boxes with the

+key, no fault armed, no legacy host) under a **quiet RNG**, whose every

+draw takes the branch that injects nothing: no late completion, no

+stalled signer, no duplicate, no second process. It then scripts the

+interleaving its rule exists for, one protocol step at a time: it names

+the actors of each step (a box's worker, obligation runner and reconcile,

+the console's plans in order, the recovery pass, the operator), stops a

+box, crashes an agent, freezes a VM or pauses an agent, has the

+application write, holds one S3 request until it says so (the model's

+`issue` honours a witness's hold), places a paused registry open, or

+wakes a stalled worker goroutine with an old read. Then it drives to

+quiescence and runs the same final oracle as a seed. A milestone the

+scenario cannot reach, with no violation to explain it, is recorded as

+INV-3. Witnesses never draw from a seed's RNG: the model's RNG became an

+interface so the quiet one can stand in, `moveTo` and `resumeStale` are

+callable directly, and the random path's draws are unchanged, which the

+identical 300-seed gate of the rev 7.2 binary and this one confirms.

+Each witness must hold with every rule in place (it runs in the gate) and

+violate an invariant under its rule's mutation, alone or in the stated

+combination; `HOSTLIFE_MUTATE` applies the mutation and `mutate.sh`

+reports the witness beside the sweep (§14.2.1). A witness that holds

+alone and violates with its partners is the redundancy the combination

+table states, shown rather than inferred.

+**Found on the way: the model was not deterministic.** The purge drain

+iterated an app's registrations in Go map order, so a seed with two

+registrations at a drain could differ from run to run; the same rev 7.2

+binary gave 49,743, 49,744 and 49,745 completed operations over 30,000

+seeds. It drains in create-id order now, two runs agree exactly, and the

+sweep counts in §14.2.5 are rerun on the deterministic model. It was the

+only behaviour-affecting map iteration.

paginated listings, separate service, wall and monotonic clocks,

enrollment and console and updater versions, spawn separate from

readiness, and same-operation lease identities.

@@ -1739,7 +1812,18 @@ 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.2, on the final model (claim rev 5.2: CC22 with the restart and

+**Rev 7.3, on the final model (rev 7.2's, with the deterministic purge

+drain): 30,000 seeds, zero violations; 100,000 seeds, zero violations**

+(35 s and 121 s). Across the 100,000 seeds: 165,834 completed

+operations, among them 1,613 completed moves, 2,072 clean and 96 dirty

+rollbacks, 443 pre-flip reverts, 388 declared losses, 31,682 pushes,

+95,195 delete-park-free cycles and 1,416 lost disks. 24,270 requests

+completed after `H`; 30,884 staging signatures were refused as stale;

+14,143 creates restarted on a 412; 106 targets were stopped mid-return.

+Every witness holds (22 scenarios, under a second). The rev 7.2 figures

+below differ by a few operations: the drain's map order (§14.2.2).

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

@@ -1821,137 +1905,157 @@ 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.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, 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.

+on the final rev 7.3 model, with the strict classification, and **in two

+ways** (rev 7.3): the **random sweep**, 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 and 100,000 for the rarest; and the

+rule's **witness scenarios** (§14.2.2, `witness_test.go`) under the same

+mutation, for the 20 rules that have them. A rule is caught if either

+catches it; `mutate.sh` reports the two separately, and this section

+does too. The model has **68 rules**, as in rev 7.2. No run was an ERROR.

+Seed numbers reproduce any sweep line with `HOSTLIFE_SEED`;

+`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.2's

+counts are in the rev 7.2 spec (0c6058b0); the sweep counts below differ

+from them by a few seeds because the purge drain is deterministic now

+(§14.2.2), not because any seed was reshuffled.

| | rules |

|---|---|

-| caught alone | 51 |

-| caught only in a stated combination | 13 |

+| caught alone by the sweep at 3,000 seeds | 46 |

+| caught alone by the sweep at 30,000, and by their witness | 5 (`lost-quarantine`, `markers-last`, `rollback-journal`, `seal-by-version`, `staging-quiet`) |

+| caught alone by their witness only; the sweep misses them at 100,000 | 2 (`generation-conditional`, `declare-lost-compute`) |

+| caught only in a stated combination: the witness holds alone and violates with the partners | 12 |

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

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

-| unexercised | **1** (`generation-conditional`, below; rev 7.1's was `lost-return-park`) |

+| unexercised | **0** (rev 7.2 had `generation-conditional`; rev 7.1 `lost-return-park`) |

+**The witnesses.** One scenario per rule the sweep catches rarely or only

+in combination; two for `registration-check`, one per partner. "Alone"

+is the witness under the rule's own mutation; "with partners" under the

+stated combination. Where a rule holds alone, that is the redundancy the

+combination column states: the partner is what stops the scenario when

+the rule is gone, and vice versa.

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

+| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 0 / 100,000 (0 / 300,000 on rev 7.2; 2 / 100,000 on rev 7.1) |

+| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 3 / 3,000, 32 / 30,000, 102 / 100,000 |

+| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 100,000 |

+| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held: with compute fencing the operator refuses, and the paused box is never declared lost | with `declare-lost-compute`: **violated**, INV-1; a watchdog inside the paused agent never fences | 0 / 100,000; the pair 3 / 100,000 |

+| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore; the restart at `claimed` parks the return generation | | 0 / 3,000, 4 / 30,000 |

+| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale round | | 0 / 3,000, 11 / 30,000 |

+| `commit-before-open` (INV-5) | the same scenario; the mutation opens the target's row at the probe | held: an open row admits nothing while the claim is uncommitted | with `dirty-return`: violated, and the violation is `dirty-return`'s | 0; the pair 15 / 30,000 |

+| `claim-cas-opid` (C2) | a clean rollback; a second source goroutine reads the claim just before the release and stalls; the host is released, a purge claims it, the goroutine resumes | held: revalidation stops it | with `revalidate-before-effect`: **violated**, the stale release overwrites the purge and the store is torn down under a serving host | 0; the pair 1,021 / 30,000 |

+| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | an open from an earlier operation, paused on the source, lands after the commit while the source's row is still held; a request wakes the source | held, each: `hold_op` refuses the open, or the exec check refuses the wake, or the generation check refuses the start | all three: **violated**, INV-1, the source serves beside the target | 0 each; any pair 0 / 30,000; the triple 4 / 30,000, 12 / 100,000 |

+| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held: the whole-tree cleanup kills the escaped descendant | with `evidence-whole-tree`: **violated**, INV-1, the descendant writes beside the target | 0; the pair 129 / 30,000 |

+| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held: discovery parked the other region at adoption | with `legacy-discovery`: **violated**, INV-10, the replica is residue after `free` | 0; the pair 9,092 / 30,000 |

+| `door-reread` (claim §6.5 O2) | a listing authorized before the delete selects after a recreate into the same location | held: with C3a the new incarnation's location differs, and the listing finds nothing | with `location-per-incarnation`: **violated**, a read authorized for inc 1 returns inc 2's data | 0; the pair 40 / 30,000 (10 door violations) |

+| `door-by-version` (claim §6.5) | a listing selects and signs before the delete; the file request opens after the recreate | held, as above | with `location-per-incarnation`: **violated**, the same; `door-reread` is not needed | 0; the pair 31 / 30,000 (2 door violations), with `door-reread` too 59 / 30,000 (30) |

+| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held: the fence and the ETag condition refuse the CAS, and the 412 restarts the create on a store that exists again | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated**; a host creating on a torn-down store | 0 / 30,000; the pairs 231 and 309 / 30,000 |

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

+(CC21) is caught alone by the sweep: 25 / 3,000, 260 / 30,000.

+`fence-etag` (CC22): 17 / 3,000, 189 / 30,000. `claim-never-deleted`

+(C5a): 7 / 3,000, 79 / 30,000 (54 of the 79 on the main host while

+`creating`, 25 on the second host). `registration-check`, the creator's

+re-read, is not caught alone by the sweep at 3,000 or 30,000 seeds, and

+its witness holds alone: 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`, 298 / 30,000).

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

+| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 31 / 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`: 40 / 30,000, of which 10 are door violations; witness violated | 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 `location-per-incarnation`: 31 / 30,000, of which 2 are door violations, and with `door-reread` as well 59 / 30,000 (30); witness violated with C3a alone | 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.

+load-bearing once C3a is dropped, by its witness and by the sweep.

-**Caught alone: 51 of 68.**

+**Caught alone: 53 of 68** (46 by the sweep at 3,000; 5 by the sweep at

+30,000 and by their witness, marked †; 2 by their witness alone, marked

+‡, with the sweep's count beside).

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

-| `recovery-pass` | 2,502 / 3,000 | | `fresh-incarnation` | 45 / 3,000 |

+| `recovery-pass` | 2,502 / 3,000 | | `fresh-incarnation` | 44 / 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 |

+| `park-skip-lock` | 2,878 / 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 |

+| `hostguard` | 6 / 3,000 | | `purge-reserve-first` | 2,291 / 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 |

+| `claim-never-deleted` | 7 / 3,000 | | `cancelled-creates` | 374 / 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 |

+| `evidence-from-state` | 2,793 / 3,000 | | `floor-boot-recovery` | 2,533 / 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 |

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

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

+| `abort-target-owner` | 1,066 / 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 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: 13 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) | 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 |

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

+`declare-lost-compute` was combination-only in rev 7 and rev 7.2 (0 /

+100,000 alone) and caught alone once in 100,000 in rev 7.1: a rule the

+sweep reaches by chance. Its witness freezes the target and expires its

+lease, and the mutation lets it resume beside the recovered source every

+time. `generation-conditional`'s witness holds the stale marker PUT until

+a newer marker is current, which the sweep did twice in 100,000 on rev

+7.1 and never since. Neither is in `expected-outcomes.txt` any more.

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

+the same seeds, shows what the combination adds; the witness column is

+the rule's witness under the combination.

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

+| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 298 / 30,000 | `purge-claim-fence` 260, `fence-etag` 189, `registration-check` 0 | (the two `registration-check` rows below) | 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 |

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

+They have no witness: neither can violate an invariant.

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

+only after its own horizon, and CC11 holds; the biased schedules do not

+change that, because they delay only data writes, never an

+acknowledgement. No witness: there is no interleaving to force.

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

+**Seeds:** 300 in the gate, with every witness (about a second); the

+30,000- and 100,000-seed baselines, this sweep and the witnesses are the

+evidence for rev 7.3.

#### 14.2.6 What the model does not prove

@@ -2441,4 +2545,17 @@ 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`.

+gave `lost-return-park`. Rev 7.3 ends that treatment (§22.9).

+### 22.9 The coordinator's round on rev 7.2

+| request | rev 7.3 |

+|---|---|

+| stop the whack-a-mole: each biased schedule reshuffles every seed and some rare rule drops out | deterministic witness scenarios, one per rule the sweep catches rarely or only in combination, never drawn from a seed's RNG (§14.2.2); 22 scenarios for 20 rules, each violating under its mutation (§14.2.5) |

+| cover `generation-conditional`, `lost-return-park`, `declare-lost-compute`, and every rule caught only at 30k or 100k or only in combination | all covered; `generation-conditional` and `declare-lost-compute` are caught alone by their witnesses and off the expected-miss list; the five 30,000-seed rules have witnesses that violate alone |

+| where a rule is truly redundant with a partner, the witness should show it | shown for eleven: `watchdog-independent` (behind compute fencing), `claim-cas-opid` (behind revalidation), `commit-before-open` (adds nothing over `dirty-return`), the admission triple and `start-check` (one of three fences each), `strict-spawn` (behind the whole-tree cleanup), `touched-incomplete` (behind discovery), the two door rules (behind C3a; `door-by-version` needs only C3a dropped, not `door-reread`), `registration-check` (behind the fence and the ETag condition, either one) |

+| extend `mutate.sh` and expected-outcomes so a rule counts as caught if its witness fails or the sweep catches it, reported separately | done (§14.2.1); `expected-outcomes.txt` drops the two witness-caught rules and restates the combination-only ones |

+| rerun the 30k and 100k baselines and the full sweep | both clean; the sweep rerun on the deterministic model (§14.2.3, §14.2.5) |

+Found on the way: the purge drain's map-order nondeterminism (§14.2.2),

+fixed; rev 7.2's sweep counts were subject to it by a few seeds.

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index 9b9687a43..0892dab88 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -1,7 +1,7 @@

// Package hostlife is a deterministic, randomized model of the host

// lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md,

// rev 5.2, 465fee96) and Phase 1 of move-any-app

-// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.2).

+// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.3).

// Since joint round 2 the model encodes what the specs say and nothing

// stronger: restore reads the holder's location and the generation the