amadan
spec: move-any-app rev 6, part 2: the strict model's results
§14.2 rewritten for the model that encodes the specs and nothing stronger: what changed against Astra's fidelity table, the stricter invariants, 30,000 and 100,000 seeds clean, the strict mutation sweep (60 rules: 44 caught alone, 10 in combinations, 2 liveness-only, 1 unreachable, 3 unexercised), model faults 17 to 24, and what the model still does not prove. §22.5: joint round 2 dispositions.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+201
−155
docs/superpowers/specs/2026-10-02-move-any-app-design.md+201 −155
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 77dd35b87..b912dc89c 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 |
| @@ -1433,6 +1433,16 @@ HOSTLIFE_SEEDS=100000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v |
| HOSTLIFE_SEED=1796 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v # one seed, full trace |
| ``` |
| +**Rev 6: strict classification (J2-R2-10).** `mutate.sh` reports CAUGHT |
| +only when the run completed and reported a seed that violated an |
| +invariant, with the seed number parsed from its output. A build failure, a |
| +panic, a timeout or unparsable output is ERROR, never a detection; every |
| +run's log is kept. `expected-outcomes.txt` beside the script declares the |
| +rules not expected to be caught alone (liveness-only, unreachable, |
| +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 |
| @@ -1443,6 +1453,33 @@ in parallel. Scratch copies live under `$HOSTLIFE_SCRATCH`, by default |
| #### 14.2.2 What it models |
| +**Rev 6 (joint round 2): the model encodes the specs, nothing stronger.** |
| +Astra's §2 listed where the rev 5 model was stronger or more atomic than |
| +the text. What changed, and what did not: |
| + |
| +| J2 fidelity point | rev 6 model | |
| +|---|---| |
| +| restore stronger than the spec (an exact base pointer, historical lineage selection) | restore reads `holder.location` and `holder.generation` and replays every object of that generation (§5.1). The mutation restores the newest object under the location | |
| +| the start check stronger than the spec (compared with the committed lineage) | the start check compares the box's own three markers with each other and, as a separate rule, with the claim's generation (§5.1); rev 5's check is the mutation | |
| +| claim transitions followed by an atomic record write | record-first flip, commit and rollback, then the claim half as a separate step, written by the actor, the other participant or the recovery pass; the close the other way round (§7.5) | |
| +| every request completes by `issue + H` | one long-tail request in 20 completes up to 11 `H` late, after publication and after retirement; the restore contract keeps them out of data, the sweep retires them (§5.1, §6.4) | |
| +| check and sign, check and local write, atomic | staging writers sign at the check and may then pause, a frozen box without bound (§7.3); host-guard writers are independent processes (`carlos-config-sync`, `carlos-adopt`) that survive an agent crash, pause before the guard and re-validate under it (claim §6.4); door listings read O1, pause, select, read O2 (claim §6.5) | |
| +| atomic `localPark` | one artifact per step, the retired marker first | |
| +| creates and purges atomic, one host | creates are console plans (register, claim, record, serve, deregister), purges close and drain admission, plans run concurrently, the console crashes between any two; a second hostname takes part in creates and purges (claim §5.1, §5.3) | |
| +| record writes synchronous | a create's record PUT can lose its response and land later, rarely very late (claim §5.1) | |
| +| config an incarnation integer | bundle versions, published at any time, pinned at admission (§7.6, §7.7) | |
| +| park manifest of current versions | archive and deletion sets (claim §6.2) | |
| +| legacy discovery never meets local residue | a legacy host's earlier move can leave a database and files on another box; adoption discovery parks them (claim §9) | |
| +| a final oracle that replicates before checking | the oracle only reads: cold-restore checks of every durable write at every release and at the end, INV-10 at every operation's end, no restored database holding another incarnation's writes (§14.2.3) | |
| +| mutation infrastructure errors counted as detections | strict classification (§14.2.1) | |
| +| the return lane outside the lease | the return lane takes the staging-work lease of the source's region, with paused signers and the forward path's horizon (§7.8) | |
| + |
| +Not changed, and listed in §14.2.6: principal-aware reads and listings, |
| +paginated listings, separate service, wall and monotonic clocks, |
| +enrollment and console and updater versions, spawn separate from |
| +readiness, and same-operation lease identities. |
| + |
| + |
| - **State.** The claim object (CAS on its revision, op id conditions), |
| records, the console's purge reservations and app stores, three |
| regions' **versioned** data buckets, and each box's registry row, local |
| @@ -1519,24 +1556,38 @@ in parallel. Scratch copies live under `$HOSTLIFE_SCRATCH`, by default |
| #### 14.2.3 Invariants and results |
| -The invariants are the table at the end of §4. Each run must also reach a |
| -quiescent state: claim at rest, no obligations, record agreeing, the |
| -serving box able to start, and nothing left anywhere else. |
| - |
| -**Rev 5, on the final model: 30,000 seeds, zero violations (23 s); 100,000 |
| -seeds, zero violations (80 s).** Across the 100,000 seeds: 199,462 |
| -completed operations, among them 3,887 completed moves, 2,858 clean |
| -rollbacks, 129 dirty rollbacks, 1,037 pre-flip reverts, 664 declared |
| -losses, 35,232 pushes and 113,792 delete-park-free cycles; and 41,863 |
| -aborts, mostly sources whose plan pass had not yet rendered `config.env` |
| -or adopted the release since their row was recreated (S1 refuses them), |
| -the rest targets without a secrets key (T2). In 2,731 install attempts the |
| -staging object was newer than the seal, because a paused round had written |
| -after it; in 249 of them it held an older snapshot. Those are the cases |
| -the seal by version exists for. |
| - |
| -Rev 4's figures (30,000 seeds, 101 s, 772 completed moves) were on a model |
| -that exercised less. |
| +The invariants are the table at the end of §4, with three checks rev 6 |
| +adds and one it makes stricter: |
| + |
| +- **INV-2, cold restore, at every release and at the end.** A restore of |
| + the claim's location and generation in the serving region, computed and |
| + never written, holds every acknowledged write that a completed replica |
| + object of that generation, or of any generation it superseded, ever |
| + held. Rev 5 wrote the serving box's database into the bucket and then |
| + restored it (J2-R2-9). |
| +- **INV-10 at every operation's end.** At each release to `serving` and |
| + each `free`, nothing outside the live set remains, except a version |
| + created by a request that completed after `H` (only the sweep can retire |
| + those) and what another pending chore owes. At the end of the run, |
| + nothing at all. |
| +- **C3a.** No database restored or started for an incarnation holds a write |
| + another incarnation acknowledged. |
| +- **A disk-loss fault** takes the serving box's database file while the |
| + app is idle. Writes past the last completed checkpoint are lost by |
| + design and declared so; every durable write must come back. |
| + |
| +**Rev 6, on the final model: 30,000 seeds, zero violations (43 s); |
| +100,000 seeds, zero violations (144 s).** Across the 100,000 seeds: |
| +180,311 completed operations, among them 1,734 completed moves, 2,341 |
| +clean and 71 dirty rollbacks, 528 pre-flip reverts, 343 declared losses, |
| +33,614 pushes, 103,353 delete-park-free cycles and 1,430 lost disks. 14,373 |
| +requests completed after `H`; 51 staging signatures were refused as stale; |
| +33 sweeps retired stragglers. 670 landings rolled back because a config |
| +bundle was published during the move. |
| + |
| +There are fewer completed moves than in rev 5 (3,887) for two reasons the |
| +stricter model makes real: bundle publications during a move now roll it |
| +back (J2-R2-5), and every transition takes two writes. |
| #### 14.2.4 Faults the model found beyond the joint review |
| @@ -1561,163 +1612,134 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| | model 14 (rev 5) | A staging round revalidated under its lease, paused, and signed after the lease ended; its PUT landed after the staging retirement had verified the prefix empty, leaving staging in the serving region or in a region the instance left | check `SafeUntil` immediately before signing (§7.3); CC14 | moves, claim | |
| | model 15 (rev 5) | With obligations run beside role work, a move started while a `park-replica` of its target region was still running; the park retired the landing's fresh versions, and a cold restore lost acknowledged writes (or the landing never converged) | CC11, already in claim rev 3 §4: now proven | claim | |
| | model 16 (rev 5) | A push whose row was already open (a reconcile acting on a cached claim had released its hold) never released: its open is conditional on its own `hold_op` and the row had none. Found under the `fresh-admission` mutation, unreachable with fresh admission; the open should be idempotent anyway | a push's open, like the landing's, accepts a row already open (F7) | push | |
| +| model 17 (rev 6) | With requests completing after `H`, residue under a freed host and in dead generations that no later retirement ever lists | the straggler sweep at rest (§6.4); CC15 | claim, moves | |
| +| model 18 (rev 6) | A box froze between a passed `SafeUntil` check and the send; signed at send time, its staging PUT was accepted after the lease and landed after the cleanup | sign at the check, `SafeUntil = Until − skew − 15 min` (§7.3); CC19 | claim, moves | |
| +| model 19 (rev 6) | A console that crashed between registering a create and its claim CAS left a registration that every later purge waited on forever; with an expiry alone, a create that had claimed before the expiry was dropped from the purge's host set and served after its store was torn down | registrations are leases, and the drain removes one only if expired and unclaimed; CC16 | claim | |
| +| model 20 (rev 6) | A create's record PUT landed after `cancelled_creates.until`, and the orphan blocked every recreate | orphan whenever its incarnation is retired; CC17 | claim | |
| +| model 21 (rev 6) | With the start check exactly as rev 5 wrote it, a paused open made the old source ready after the commit and, with the exec check also gone, it served beside the target (Astra's J2-R2-8 trace) | the start check compares the claim's generation (§5.1); CC18 | moves, claim | |
| +| model 22 (rev 6) | A bundle published after admission rolled the landing back, and then every recovery probe failed against the pinned inputs: stuck forever (J2-R2-5) | recovery probes run on current inputs (§7.7) | moves | |
| +| model 23 (rev 6) | A staging round or a push that took its writes from the local database alone, on a box that had lost it, staged an empty snapshot and parked the durable replica | a staging round is the replica plus the final checkpoint (§7.3); a push likewise (F7) | moves, push | |
| +| model 24 (rev 6) | The files directory missing on a box whose markers agree: rev 5's model refused it, rev 5's spec does not (`.files-gen` "when the files directory exists"), and the app mints a new `instance.key` | already covered: `files-carried` is now caught alone (§14.2.5); the start check is unchanged | moves | |
| #### 14.2.5 Mutation results |
| -Every rule was dropped in turn, in a scratch copy, on the final rev 5 |
| -model: 3,000 seeds each, then 30,000 seeds for every rule not caught at |
| -3,000, then 30,000 seeds for each combination below (100,000 for the |
| -triple). The model has 50 rules: rev 4's 48, plus `sign-before-safeuntil` |
| -and `readiness-quiet`. Seed numbers reproduce any line with |
| +Every rule was dropped in turn, in a scratch copy, on the final rev 6 |
| +model, with the strict classification of §14.2.1: 3,000 seeds each; 30,000 |
| +for every rule not caught at 3,000; 30,000 for each combination below, and |
| +100,000 for the rarest. The model has **60 rules**: rev 5's 50, less |
| +`restore-lineage-filter` (now `restore-by-generation`), plus |
| +`location-per-incarnation`, `start-check-claim-gen`, `door-reread`, |
| +`admission-registration`, `registration-recovery`, `cancelled-creates`, |
| +`orphan-no-deadline`, `straggler-sweep`, `recovery-current-inputs` and |
| +`sign-at-check`. No run was an ERROR. Seed numbers reproduce any line with |
| `HOSTLIFE_SEED`. |
| | | rules | |
| |---|---| |
| -| caught alone | 37 | |
| -| caught only with a stated partner | 9 (six pairs and a triple) | |
| -| caught with a partner, but adding nothing to it | 1 (`restore-lineage-filter`) | |
| -| liveness only | 2 | |
| -| unreachable under claim rev 3 | 1 (`readiness-quiet`) | |
| - |
| -**Rev 4's eight gaps, now exercised.** Each is caught by its own mutation, |
| -except the two admission and hold rules, which are caught together with |
| -the start check and with nothing less. |
| - |
| -| rule | rev 4 | rev 5 | what the model finds | |
| -|---|---|---|---| |
| -| `seal-by-version` (J-N2, §7.3) | not exercised | 5 / 30,000 | acknowledged writes lost: the install copied the current staging object, an older snapshot a paused round wrote after the seal | |
| -| `staging-quiet` (J-N2, §7.3) | not exercised | 9 / 30,000 | staging left in the serving region | |
| -| `fresh-admission` (claim C4) | not exercised | 79 / 30,000 | 77 pushes that never finish (a reconcile acting on a cached claim retired the pushing box's row); one freed host's residue; one pair of writers | |
| -| `exec-admission` (claim C4, K1) | not exercised | only in the triple below | two writers | |
| -| `hold-op-open` (§5.2) | not exercised | only in the triple below | two writers | |
| -| `stale-hold-release` (CC10) | not exercised | 37 / 30,000 | a held row blocks serving forever | |
| -| `obligations-block-ops` (CC11) | not exercised | 14 / 30,000 | **acknowledged writes lost** on a cold restore (6): a landing into a region whose park was still running; landings that never converge (8). Model 15 | |
| -| `claim-op-exclusive` (claim C2) | not exercised | 2,005 / 30,000 | operations that never converge when a delete starts over another operation (2,004); local state left for a freed host (1) | |
| - |
| -**The triple: `exec-admission` + `hold-op-open` + `start-check`.** 5 of |
| -100,000 seeds fail with two writers; each rule alone, and each pair of |
| -them, fails none of 100,000. Seed 1920: a push's paused open resumes after |
| -a later move from that box committed, and opens the old source's row, |
| -which the move held. Three independent fences stood behind that: |
| - |
| -- the conditional open refuses it, because the row's `hold_op` names the |
| - move (§5.2); |
| -- admission refuses the old source, because `op.exec` names the target |
| - (claim C4). The model's admission table names each phase's role by box, |
| - and the role is always `op.exec`, so `exec-admission` drops both; |
| -- the start check refuses its stale database, whose generation is not the |
| - committed one (INV-4). |
| - |
| -That is double protection twice over, as intended. The model cannot |
| -separate the exec check from the role column of the admission table, |
| -because in Phase 1 they never differ; a future kind whose roles are not |
| -its executor (a sidecar, F6) would need its own check. |
| - |
| -**New rules in rev 5.** |
| +| caught alone | 44 | |
| +| caught only in a stated combination | 10 (five pairs and two triples; one of them, `commit-before-open`, adds nothing to its partner) | |
| +| liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| +| unreachable under claim rev 4 | 1 (`readiness-quiet`) | |
| +| unexercised | 3 (`location-per-incarnation`, `door-by-version`, `door-reread`) | |
| -| rule | seeds failing | what the model finds | |
| -|---|---|---| |
| -| `sign-before-safeuntil` (claim C3, §7.3, model 14) | 156 / 30,000 | staging in a region the instance left (131), in the serving region (17), and in a freed host's namespace (8) | |
| -| `readiness-quiet` (T12) | 0 / 100,000 | unreachable under claim rev 3; see below | |
| - |
| -**Caught alone: 37 of 50 rules.** |
| +**Caught alone: 44 of 60.** First the rules new or changed in rev 6: |
| | rule | seeds failing | what the model finds | |
| |---|---|---| |
| -| `recovery-pass` (claim C2, §8) | 1,405 / 3,000 | creates and deletes stranded mid-operation never converge | |
| -| `fresh-incarnation` (claim §5.1, R3-12) | 100 / 3,000 | a reused identity meets its own retired marker; the host never serves again | |
| -| `legacy-discovery` (CC4) | 12 / 3,000 | legacy residue in a region the host does not serve | |
| -| `park-by-version` (claim C3, J-N1) | 2,325 / 3,000 | parks never finish | |
| -| `park-all-versions` (claim §6.2) | 926 / 3,000 | parks never finish (older versions resurface) | |
| -| `park-skip-lock` (claim §6.2, J-N6, CC3) | 3,000 / 3,000 | parks never finish (the parker's own lock) | |
| -| `retirement-ids` (claim §6.2, J-D5, J-N7) | 392 / 3,000 | parks never finish (one manifest, two events) | |
| -| `quiet-before-ack` (CC1) | 103 / 3,000 | residue after a park, from late replication PUTs | |
| -| `hostguard` (claim C7, J-N8) | 8 / 3,000 | an instance starts with another incarnation's `config.env` | |
| -| `purge-reserve-first` (claim §5.3, J-N9) | 2,113 / 3,000 | stores destroyed under held hosts | |
| -| `purge-adopts` (CC6) | 19 / 3,000 | a store destroyed under a serving legacy host | |
| -| `purge-journal` (CC7) | 5 / 30,000 | a new incarnation's store destroyed by a stalled purge | |
| -| `door-by-version` (claim §6.5, J-N10) | 25 / 30,000 | a door read returns another incarnation's data | |
| -| `evidence-whole-tree` (claim §6.1, J-D3) | 13 / 30,000 | two writers; lost writes | |
| -| `evidence-from-state` (claim §6.1, R2-2) | 2,982 / 3,000 | evidence never comes after an agent restart | |
| -| `floor-boot-recovery` (claim §10, J-N12) | 2,696 / 3,000 | old executables break parks and admission | |
| -| `participant-rows` (claim §2, R2-4) | 6 / 3,000 | source recovery stuck | |
| -| `revalidate-before-effect` (claim C3, J-N2) | 31 / 3,000 | a stalled worker's effects lose acknowledged writes | |
| -| `declare-lost-compute` (CC5, J-D6, J-N3) | 1 / 30,000 | acknowledged writes lost after a frozen target resumes | |
| -| `lost-quarantine` (claim §7, CC12) | 2 / 30,000 | a returning box keeps stale local state | |
| -| `cut-deadline` (§7.4, J-N15) | 50 / 3,000 | commits past the budget | |
| -| `revert-journal` (§7.4, J-N11) | 22 / 3,000 | pre-flip recovery stuck on its own writes | |
| -| `rollback-journal` (§7.8, R2-3) | 11 / 30,000 | rollback recovery stuck | |
| -| `dirty-return` (§7.8, INV-2) | 1 / 3,000 | the target's acknowledged writes lost | |
| -| `target-park` (§7.8, R2-5) | 11 / 3,000 | a rolled-back target's replica left live | |
| -| `abort-target-owner` (§7.11, J-N13) | 1,260 / 3,000 | IAM violations | |
| -| `timer-freeze` (§9.4, J-N14) | 4 / 3,000 | clean recovery stuck | |
| -| `timer-canonical` (§9.4, J-N14) | 4 / 3,000 | clean recovery stuck | |
| -| `markers-last` (§7.6, R2-6) | 12 / 30,000 | an acknowledged timer lost | |
| -| `source-readiness` (§7.3, S1) | 18 / 3,000 | pre-flip recovery stuck | |
| - |
| -The six rules of rev 4's gap table that are caught alone, and |
| -`sign-before-safeuntil`, complete the 37. |
| - |
| -**Caught only with a partner.** The partner's own count, on the same |
| -30,000 seeds, shows whether the combination adds anything. |
| - |
| -| combination | fails (30,000) | partner alone | what the model finds | |
| +| `restore-by-generation` (§5.1, J2-R2-1) | 10 / 30,000 | acknowledged writes lost: the newest object under the location was a late or stale one | |
| +| `straggler-sweep` (§6.4, CC15) | 3 / 3,000 | residue nobody retires, after requests that completed past `H` | |
| +| `sign-at-check` (§7.3, CC19) | 1 / 100,000 | staging lands after its cleanup from a box frozen between check and send | |
| +| `recovery-current-inputs` (§7.7, J2-R2-5) | 69 / 3,000 | recovery stuck forever after a bundle published during the move | |
| +| `admission-registration` (claim §5.1, §5.3, J2-R2-2) | 3 / 3,000 | a second host serving after its app's store was torn down | |
| +| `registration-recovery` (CC16) | 894 / 3,000 | purges that never finish | |
| +| `cancelled-creates` (claim §5.1, J2-R2-7) | 365 / 3,000 | a late record that blocks the host forever | |
| +| `orphan-no-deadline` (CC17) | 31 / 3,000 | the same, for a record that lands after `until` | |
| +| `files-carried` (§8, the kpmg outage) | 64 / 3,000 | the app mints a new `instance.key` over sealed data. Rev 5 caught this only with `start-check`; that pairing was an artifact of rev 5's stronger start check (model 24) | |
| + |
| +and the rest, rev 5's rules on the stricter model: |
| + |
| +| rule | seeds failing | | rule | seeds failing | |
| +|---|---|---|---|---| |
| +| `recovery-pass` | 2,512 / 3,000 | | `fresh-incarnation` | 72 / 3,000 | |
| +| `legacy-discovery` | 558 / 3,000 | | `park-by-version` | 2,200 / 3,000 | |
| +| `park-all-versions` | 745 / 3,000 | | `park-skip-lock` | 2,994 / 3,000 | |
| +| `retirement-ids` | 284 / 3,000 | | `quiet-before-ack` | 187 / 3,000 | |
| +| `hostguard` | 9 / 3,000 | | `purge-reserve-first` | 2,362 / 3,000 | |
| +| `purge-adopts` | 8 / 3,000 | | `purge-journal` | 2,149 / 3,000 | |
| +| `evidence-whole-tree` | 2 / 3,000 | | `evidence-from-state` | 2,940 / 3,000 | |
| +| `floor-boot-recovery` | 2,679 / 3,000 | | `participant-rows` | 7 / 3,000 | |
| +| `revalidate-before-effect` | 11 / 3,000 | | `lost-quarantine` | 4 / 30,000 | |
| +| `cut-deadline` | 9 / 3,000 | | `revert-journal` | 17 / 3,000 | |
| +| `rollback-journal` | 1 / 3,000 | | `dirty-return` | 1 / 3,000 | |
| +| `target-park` | 49 / 3,000 | | `abort-target-owner` | 1,129 / 3,000 | |
| +| `timer-freeze` | 10 / 3,000 | | `timer-canonical` | 2 / 3,000 | |
| +| `markers-last` | 1 / 3,000 | | `source-readiness` | 10 / 3,000 | |
| +| `seal-by-version` | 1 / 3,000 | | `staging-quiet` | 2 / 3,000 | |
| +| `sign-before-safeuntil` | 9 / 3,000 | | `fresh-admission` | 4 / 3,000 | |
| +| `stale-hold-release` | 6 / 3,000 | | `obligations-block-ops` | 22 / 3,000 | |
| +| `claim-op-exclusive` | 93 / 3,000 | | | | |
| + |
| +**Caught only in a combination: 10 rules.** Each partner's own count is |
| +in the second column, so the combination's contribution shows. |
| + |
| +| combination | fails | partners alone | what the model finds | |
| |---|---|---|---| |
| -| `files-carried` + `start-check` | 1,498 | 0 and 0 | **the kpmg outage**: the app mints a new `instance.key` over data sealed with the old one | |
| -| `strict-spawn` + `evidence-whole-tree` | 210 | 13 | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 5,925 | 170 | a freed host's residue | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,201 | 248 | a stale purge step destroys a store | |
| -| `watchdog-independent` + `declare-lost-compute` | 6 | 1 | two writers (the partner alone loses writes, but never runs two) | |
| -| `commit-before-open` + `dirty-return` | 8 | 6 | lost writes; a weak signal, two seeds over the partner | |
| -| `restore-lineage-filter` + `quiet-before-ack` | 1,105 | 1,105 | **nothing beyond the partner**: the same seeds fail the same way. Rev 4 reported 207 against about 160; rev 5's model makes `quiet-before-ack` fail first in every seed where the filter would matter. The filter stays as the second line behind the horizon, unproven by this model | |
| -| `exec-admission` + `hold-op-open` + `start-check` | 5 / 100,000 | 0 / 100,000 for each pair | two writers (above) | |
| - |
| -**Liveness rules: 2.** `readiness-key` (T2) and `config-before-probe` |
| -cannot break a safety invariant: without them a target that cannot render |
| -config fails its probe and rolls back. They exist to avoid a pointless |
| -cut, and the model confirms that is all they do. |
| - |
| -**Unreachable under claim rev 3: `readiness-quiet` (T12).** With it |
| -dropped, no cut waits on `quiet_after` in 100,000 seeds, and an |
| -instrumented run of 30,000 seeds finds no install of any kind (a create's |
| -first wake, a landing, a push) that waits on it either. Every retirement |
| -acknowledges only after its own `evidence time + H` (claim §6.2a), so the |
| -`quiet_after` it writes has passed by then; CC11 keeps operations off |
| -regions with pending chores; and `free` needs every obligation gone. T12 |
| -and the field stay as defence in depth (§7.3, §19.4's note). |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 19 / 100,000 | each pair of the three: 0 / 30,000 | two writers: **Astra's J2-R2-8 trace.** With the start check as rev 5 wrote it (the third rule dropped), losing the exec check and the conditional open lets a paused open make the old source ready after the commit, and it serves beside the target. Rev 6's start check is the third fence the rev 5 model invented and the rev 5 text lacked | |
| +| `exec-admission` + `hold-op-open` + `start-check` | 4 / 30,000 | (above) | the same trace, dropping the whole start check | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 1,079 / 30,000 | `revalidate-before-effect` alone 162 / 30,000 | a stale purge step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 133 / 30,000 | `evidence-whole-tree` alone 8 / 30,000 | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 8,670 / 30,000 | `legacy-discovery` alone 5,714 / 30,000 | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 5 / 100,000 | 0 / 100,000 each | two writers after a frozen target resumes | |
| +| `commit-before-open` + `dirty-return` | 5 / 30,000 | `dirty-return` alone 7 / 30,000 | lost writes; fewer than the partner alone (seed variation), so the model does not separate `commit-before-open` | |
| + |
| +**Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`: |
| +without them a target that cannot render config fails its probe and rolls |
| +back. |
| + |
| +**Unreachable: `readiness-quiet` (T12).** As in rev 5: every retirement |
| +acknowledges only after its own horizon, and CC11 holds. |
| + |
| +**Unexercised: 3.** `location-per-incarnation` (claim C3a) protects against |
| +a request from an old incarnation that completes after the host was |
| +deleted and recreated. In the model, deleting and recreating a host takes |
| +longer than the longest straggler (11 `H`; a 40 `H` tail was also tried), |
| +and the sweep at rest retires stragglers in between; 0 / 100,000. The door |
| +rules are subsumed by C3a, and are not caught with it dropped either |
| +(0 / 30,000 each). These are honest gaps: C3a guards a production case |
| +the model's timing does not reach, where AWS gives no completion bound. |
| **Seeds:** 300 in the gate (about a second); the 30,000- and 100,000-seed |
| -baselines and this sweep are the evidence for rev 5. The harness is |
| -committed; its scratch copies are not. |
| +baselines and this sweep are the evidence for rev 6. |
| #### 14.2.6 What the model does not prove |
| - **It is a model.** It checks the protocol, not the code that will |
| - implement it. Its S3 is a versioned map with the documented semantics |
| - (copy and delete by version id, delete markers, conditional writes on |
| - the claim). As the paid-launch work learned, "a fake provider is never |
| - proof": every AWS behaviour it relies on has now been checked against the |
| - real service (§15 step 8), and each held. |
| -- **Granularity.** One host, three regions, one box per region. One step |
| - is atomic, so "revalidate immediately before the effect" is modelled as |
| - revalidating at the start of the step. |
| -- **Clock and pause assumptions** (claim §3.1) are modelled as skew of |
| - at most one step and, since rev 5, as paused goroutines (§14.2.2). |
| - Correctness depends on them in two places only: the late-completion |
| - horizon `H`, which S3's signature-age limit bounds (checked, §15 step 8), |
| - and the staging writer's `SafeUntil` check, whose margin must cover the |
| - pause between check and signature (model 14, CC14). The model makes the |
| - check and the signature one atomic step; the margin is the |
| - implementation's to prove. |
| -- **Adversarial scheduling is partial.** The model wakes two kinds of |
| - paused work at the worst moment it knows of, and everything else at |
| - random. Two results depend on those targeted wake-ups: the admission |
| - triple (a paused open woken after a newer operation committed) and |
| - `door-by-version` (a stalled read woken while its location holds another |
| - incarnation's object). Worse moments it does not know of may exist. |
| + implement it. Its S3 is a versioned map with the documented semantics, |
| + every one checked against the real service (§15 step 8). |
| +- **Granularity.** One data-plane host, three regions, one box per region, |
| + and a second hostname for creates and purges only. One step is atomic, |
| + except where rev 6 splits it (§14.2.2). |
| +- **J2 fidelity points not taken in rev 6:** reads, `Head` and version |
| + listings are not checked against each principal's permissions (writes |
| + are); listings are complete, never paginated or truncated; one global |
| + clock with a fixed skew, not separate service, wall and monotonic |
| + clocks; an old executable is one Boolean, not distinct console, agent |
| + and boot-updater versions with enrollment; a spawn and its readiness |
| + answer are one event; two workers of one operation share a lease |
| + identity (only one box writes staging, and a restarted agent's |
| + goroutines die with it). Each could hide a fault; each is a next step, |
| + in that order of likely yield. |
| +- **Timing is scaled, not real.** `H` (60 steps) is shorter than the cut |
| + budget (320), the reverse of production (over 15 minutes against 120 s). |
| + Results about orderings carry over; results about which wait fits inside |
| + which window do not (J2 §2). |
| +- **Adversarial scheduling is partial.** Paused opens, door reads and |
| + staging signers wake at the worst moment the model knows of; everything |
| + else wakes at random. The admission triple depends on the targeted wake. |
| - **Not modelled:** placement (`placing`), sidecars, nested-to-flat path |
| translation beyond the files directory, the db door's multi-console |
| - drain, and app moves (F5). |
| + drain, app moves (F5), and `open_budget` (the model's deadline is the |
| + commit's). |
| ### 14.3 Cross-version |
| @@ -2078,3 +2100,27 @@ Found on the way: |
| horizon holds (§14.2.5). Rev 4 counted it as a pair; rev 5 does not. |
| - **`door-by-version` went unexercised** at 100,000 seeds until door reads |
| were given real stalls (§14.2.2); it is caught again, 25 / 30,000. |
| + |
| +### 22.5 Joint round 2 (claim bf61e6a9, moves rev 5 4ec3282b, model 7a3e94e7) |
| + |
| +`CODEX-FINDINGS-JOINT-R2.md` (df41156c). Claim-side findings went to |
| +platform-1e and are answered in claim rev 4 (a3c86fa5); rev 6 encodes |
| +that revision and adds CC15 to CC19. |
| + |
| +| finding | owner | rev 6 | |
| +|---|---|---| |
| +| §2 model fidelity | moves | the model rebuilt to encode the specs and nothing stronger (§14.2.2); the points not taken are listed (§14.2.6) | |
| +| R2-1 storage fencing at the destination and completion boundary | claim (C3a), moves | claim rev 4's per-incarnation locations; here, operation-scoped generations within a location, the restore contract, and the straggler sweep (§5.1, §6.4, CC15). The model completes requests up to 11 `H` late; `restore-by-generation` and `straggler-sweep` are caught; `location-per-incarnation` is unexercised (§14.2.5) | |
| +| R2-2 purge misses a creator past its check | claim | claim rev 4 §5.1 step 0, §5.3 step 1b, modelled with two hostnames; the model adds CC16 (registrations are leases, drained only when expired and unclaimed) | |
| +| R2-3 the host guard is per process | claim | claim rev 4 §6.4, modelled with independent processes; `hostguard` caught | |
| +| R2-4 door authorization to selection | claim | claim rev 4 §6.5 (O1, O2), modelled; subsumed by C3a in the model | |
| +| R2-5 a config update makes rollback fail forever | moves | recovery probes run on current inputs, recorded; the landing stays pinned (§7.6, §7.7); `recovery-current-inputs` caught, 69 / 3,000 | |
| +| R2-6 the park manifest cannot replay its deletion set | claim | claim rev 4 §6.2, modelled (§6.4) | |
| +| R2-7 create recovery and a late record | claim, moves | claim rev 4's `cancelled_creates`, modelled with late record PUTs; CC17 removes the deadline. The move's own record writes are conditional CASes, so a late one repeats a decision or fails (§7.5) | |
| +| R2-8 the third admission fence does not exist | moves | the start check compares the claim's generation (§5.1, CC18); the model reproduces Astra's trace with rev 5's check (§14.2.5) | |
| +| R2-9 the oracle repairs storage | moves | a read-only oracle with durable-write checks at every release (§14.2.3) | |
| +| R2-10 infrastructure errors counted as detections | moves | strict classification and expected outcomes (§14.2.1) | |
| +| record/claim ordering and handoff authority | moves | every transition one record CAS, the claim following; K4 rewritten (§7.5, §19.2) | |
| +| the cut promise against the enforced deadline (N15) | moves | the deadline is the stop-to-open promise less `open_budget`, enforced on the commit's record CAS; T11 budgets every attempt's settle (§7.4) | |
| +| D3, D6, I-7, N12 "partly" in the model | moves | per-artifact local parks and independent guard processes taken; spawn-in-flight, cloud fencing proof and executable activation paths remain model gaps (§14.2.6) | |
| +| N5 local coverage | claim | claim rev 4 §9's local discovery, modelled with seeded local residue; `legacy-discovery` caught | |