amadan
spec: move-any-app rev 5, on claim rev 3, every model gap exercised (#175)
Written against claim rev 3 (8b5bccb2), which adopted CC1 to CC13. The model now exercises rev 4's eight gaps: the seal by version and the staging horizon are proven, and rest on a rule the model found, a staging writer signs only before SafeUntil (model 14, CC14); CC11 is proven (model 15); exec-admission and hold-op-open are caught only with the start check, a triple. T12 and quiet_after's install wait cannot bite under claim rev 3 and stay as defence in depth. 30,000 and 100,000 seeds clean; the full mutation sweep is §14.2.5. §15 step 8, the real-AWS check, is done, with each result cited.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+364
−123
docs/superpowers/specs/2026-10-02-move-any-app-design.md+364 −123
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 c91d18fb5..8f4f8c29a 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,34 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-02 |
| -**Revision:** 4. |
| +**Revision:** 5. |
| + |
| +- **Rev 5** is written against **claim spec rev 3** (8b5bccb2 on |
| + `design-replica-ownership`), which adopted CC1 to CC13. It answers the |
| + coordinator's round on rev 4: |
| + - the model (§14.2) is extended until it exercises every rule rev 4 |
| + listed as a gap: stalled staging signers, paused registry writes that |
| + resume at the worst moment, an obligation runner beside the role |
| + worker, and admission from cached reads. It is re-encoded against |
| + claim rev 3, and reruns clean at 30,000 and 100,000 seeds, with the |
| + full mutation sweep (§14.2.5); |
| + - N2's second half is now proven: dropping the seal by version loses |
| + acknowledged writes, and dropping the staging horizon leaves residue. |
| + The model also found the rule both rest on: a staging writer signs |
| + only before its lease's `SafeUntil` (model 14, §7.3); |
| + - CC11 is now proven: an operation started over a pending park loses |
| + acknowledged writes (model 15); |
| + - T12 and the install wait on `quiet_after` cannot bite under claim |
| + rev 3: they are kept as defence in depth (§14.2.5); |
| + - §15 step 8 is done: every AWS behaviour the model assumes was checked |
| + against the real service; |
| + - one more claim change, CC14, goes to platform-1e (§19.4). |
| + |
| + Rev 5's changes are marked "(model N)" like rev 4's. |
| -- **Rev 4** is the first revision checked against an **executable model** |
| +Earlier revisions: |
| + |
| +- **Rev 4** (a80ff90b) was the first revision checked against an **executable model** |
| instead of a prose round. The joint Astra review of the claim spec (rev 1) |
| and this spec (rev 3), `CODEX-FINDINGS-JOINT-R1.md` (4316db73), found 12 |
| new P1s and 3 P2s, and recommended a joint simulation before planning. |
| @@ -18,9 +43,7 @@ |
| moves side of the others. Changes are marked "(joint N)"; |
| - fixes what the model found beyond the review, marked "(model N)" |
| (§14.2.4); |
| - - lists the claim changes the model requires (§19.3), for platform-1e. |
| - |
| -Earlier revisions: |
| + - lists the claim changes the model requires (§19.4), for platform-1e. |
| - **Rev 1** (e41c4fef) went to Astra (GPT-6, via codex): 12 P1, 7 P2, 1 P3, |
| "not ready". The findings are in `CODEX-FINDINGS-MOVES-R1.md` (9fbf4afe). |
| @@ -59,8 +82,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 2 at cf3a7861** on `design-replica-ownership`. Rev 4 is written |
| - against rev 2. |
| + **rev 3 at 8b5bccb2** on `design-replica-ownership`. Rev 5 is written |
| + against rev 3; rev 4 was written against rev 2 (cf3a7861). |
| Citations are to this worktree at 7edd4b33 unless they name another branch |
| or repo. |
| @@ -109,7 +132,7 @@ traffic is undone automatically (§7.8); after the target opens, R4 stands. |
| ### 0.4 The host lifecycle claim |
| -From claim spec rev 2 (§2 to §10 there), the parts this spec relies on: |
| +From claim spec rev 3 (§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`; |
| @@ -123,23 +146,32 @@ From claim spec rev 2 (§2 to §10 there), the parts this spec relies on: |
| **exact object versions**, with a shared staging-work lease for |
| cross-region staging; C4 fresh admission; C5 revocation needs stop |
| evidence or a lost-box fence; C6 a read error never acts; C7 |
| - already-admitted work is drained (`hostguard`). |
| + already-admitted work is drained (`hostguard`). Rev 3 limits C3's |
| + "late completion is harmless" to the operation's own version-bound |
| + calls, and covers the replication exception with a late-completion |
| + horizon (§6.2a there). |
| - **Op kinds** (§4 there): `moving`, `landing` and `reverting`/`restoring` |
| belong to this spec. One operation runs at a time. |
| -- **Mechanisms:** stop evidence from system state (§6.1), parking by exact |
| - version into per-retirement destinations (§6.2), local retirement for both |
| - layouts (§6.3), the host guard (§6.4), door reads pinned to versions |
| - (§6.5), execution leases and declare-lost (§7), the floor on every |
| - executable restore path (§10). |
| +- **Mechanisms:** stop evidence from system state, with every probe |
| + rendering held config (§6.1); parking by exact version into |
| + per-retirement destinations keyed `<relative key>@<source versionId>` |
| + (§6.2); the late-completion horizon `H` and the per-region `quiet_after` |
| + that survives `free` (§6.2a); local retirement for both layouts (§6.3); |
| + the host guard (§6.4); door reads pinned to versions (§6.5); execution |
| + leases for liveness, and declare-lost by compute fencing only (§7); one |
| + `claim.Adopt` routine with discovery parks (§9); the purge journal |
| + `reserved → adopted → claimed → torn-down → retired → done` (§5.3); the |
| + floor on every executable restore path (§10). |
| This spec's rules for using the claim are K1 to K13 in §19, named "K" so |
| they never read as the claim spec's C1 to C7. **Execution holder** below |
| means the claim's `op.exec` (rev 2 made it a first-class field, as rev 3 |
| asked). |
| -The model (§14.2) found that several claim rev 2 rules need changing. |
| -§19.3 lists them; until platform-1e adopts them, this spec states each as |
| -the behaviour it relies on. |
| +Rev 4's model (§14.2) required thirteen changes to claim rev 2, CC1 to |
| +CC13; claim rev 3 adopted all of them (§19.4 maps each to its section |
| +there). Rev 5's model requires one more, CC14 (§19.4): until platform-1e |
| +adopts it, this spec states it as the behaviour it relies on. |
| ## 1. What happened in production |
| @@ -272,6 +304,7 @@ model, and where each lives: |
| | an app store exists while its host is held for anything but delete | after every step | claim §5.3 | |
| | a door read returns only the incarnation it authorized | at every open | claim §6.5 | |
| | a commit happens within the cut budget | at the commit | INV-9 | |
| +| an admitted cut never waits out `quiet_after` (rev 5) | at the landing's park | INV-9, T12 | |
| | no IAM violation | at every request | M17 | |
| | no stuck recovery | after every step | INV-3 | |
| @@ -333,8 +366,8 @@ Round 2 showed two gaps: a flat child's descendant that outlives it |
| and evidence that cannot be produced after an agent restart, because |
| `FenceAndStop` returns `ErrStopUnproven` when it has neither an entry nor a |
| remembered stop history (`maintenance.go:90-100`). Evidence comes from |
| -**durable, observable state**, never from memory. Claim spec rev 2 §6.1 |
| -adopts the joint review's D3 text, and this section follows it (joint D3): |
| +**durable, observable state**, never from memory. Claim spec §6.1 (rev 2 |
| +and rev 3) adopts the joint review's D3 text, and this section follows it (joint D3): |
| > All lifecycle-controlled spawns require strict containment. Stop evidence |
| > requires a closed admission fence, drained spawn attempts, an empty |
| @@ -483,21 +516,23 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| location, noncurrent included; copies name `versionId`; deletes name |
| `VersionId`. The model replaces version deletes with bare-key deletes |
| (delete markers on a versioned bucket) and finds parks that never |
| - finish, in 2,311 of 3,000 seeds. |
| + finish, in 2,325 of 3,000 seeds (rev 5). |
| - **The live lock is not data (joint N6).** The parker takes the location's |
| replica lease first, and renews its own `lock.json` while it works. That |
| key is excluded from the snapshot, the manifest and the emptiness check, |
| and released by the parker's own version after the completion CAS. The |
| model includes the lock and the park never finishes. |
| - **Progress accumulates (model 2).** A copy's destination key carries the |
| - source version id, so a retry skips copies that landed and the manifest is |
| - written once every copy exists. Restarting the snapshot from scratch on |
| + source version id (`<relative key>@<source versionId>`, claim §6.2), so a |
| + retry skips copies that landed and the manifest is written once every |
| + copy exists. Restarting the snapshot from scratch on |
| every retry, with many versions and late completions, does not converge |
| in the model. |
| - **Verify after the horizon (model 1).** A park acknowledges only after a |
| - final listing taken after `max(evidence time, the region's quiet time) + |
| - H` is empty (§5.3). Anything found then is parked as a further retirement |
| - event. |
| + verification listing taken later than `evidence time + H` (§5.3, claim |
| + §6.2a) and, for a staging retirement, later than the staging horizon |
| + (§7.3). Anything found then is parked as a further retirement event of |
| + the same obligation, and the verification repeats. |
| - **Local retirement** takes the host guard and writes a retired marker |
| first (claim C7), so a stale background write for that incarnation is |
| refused. |
| @@ -594,15 +629,36 @@ further rules: |
| A stale round that lands later creates a newer version, which the seal |
| does not name, or a delete marker, which a copy by `versionId` ignores. |
| So nothing has to be drained for correctness. |
| +- **Sign only before `SafeUntil` (model 14).** A staging writer checks its |
| + lease's `SafeUntil` immediately before it signs each request, after any |
| + pause, and drops the request if the time has passed. Revalidating at the |
| + start of the round is not enough: a goroutine that revalidated and then |
| + paused can sign long after its lease ended, and the horizon below no |
| + longer bounds its write. |
| - **Retire staging after its writers' horizon.** Staging is retired (by |
| the target-region box, §7.11) only after `seal time + staging-lease TTL + |
| H`, when no writer that held the lease can still have a request in |
| - flight. |
| - |
| -The model exercises the stale second worker and catches the revalidation |
| -rule (§14.2.5). It does not, even at 30,000 seeds, produce a staging write |
| -that lands after the seal, so the seal and the staging horizon are **not |
| -yet proven by the model**; §14.2.5 records the gap. |
| + flight. That bound holds only because of the rule above: a request is |
| + signed before `SafeUntil` and lands within `H` of signing. |
| + |
| +All three are proven by the model (§14.2.5). A staging round's goroutine |
| +can pause between revalidation and signing (one round in three), past its |
| +lease; a cut round's lost-response retry can leave a paused duplicate |
| +(one in three). Dropping the seal by version loses acknowledged writes: |
| +the install copies a stale round's older snapshot. Dropping the staging |
| +horizon or the `SafeUntil` check leaves staging in the serving region or |
| +in a region the instance left. |
| + |
| +**Where correctness rests on the pause assumption (model 14).** Claim rev |
| +3 keeps its clock and pause assumption "only for liveness", because every |
| +destructive request is version-bound. A staging PUT is not destructive, |
| +but its residency is: the staging horizon is a bound on signing time, and |
| +the only thing that enforces it is the `SafeUntil` check, whose margin |
| +must cover the clock skew and the longest pause between check and |
| +signature. The worst case is garbage under `moves/<host>/<move id>/` |
| +(never live data, because the seal names versions), but in a region the |
| +instance left that is a residency failure. CC14 asks the claim spec to |
| +say so (§19.4). |
| **Snapshot rounds (source).** Each round the source builds the files |
| archive (§8) when the plaintext digest changes, and publishes its **launch |
| @@ -629,7 +685,7 @@ placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`: |
| | T8 one owner | exactly one hosting box publishes the target placement | |
| | T9 claim | the claim is `moving` with this move id, its holder is the record's incarnation, and this region and box are in `touched` (added by CAS before the first staging write, claim spec §2) | |
| | T10 return lane | this box can put and delete `moves/_lane/<move id>` in the source's bucket (M17) | |
| -| T12 quiet region | the claim's `quiet_after` for the target region (CC1) has passed, so the landing's park of an earlier stay never waits inside the cut window. A move back into a region the instance left within H waits at `ready`, not mid-cut | |
| +| T12 quiet region | the claim's `quiet_after` for the target region (CC1) has passed, so the landing's park of an earlier stay never waits inside the cut window. A move back into a region the instance left within H waits at `ready`, not mid-cut. **Defence in depth (model, rev 5):** under claim rev 3 no state reaches it, because every retirement acknowledges only after its own horizon and CC11 refuses a move over a pending chore; the model drops T12 and no cut ever waits (§14.2.5). It stays, because it costs one comparison and guards any future path that acknowledges early | |
| | T11 budget | the **whole** stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from measured rates: stop + final checkpoint + final mirror (at most the 16 MiB bar at the measured cross-region copy rate) + archive build and upload + install copy (replica size at the measured in-bucket copy rate) + restore (replica size at the measured restore rate) + render + **every permitted probe attempt** (three times 30 s, plus the 20 s settle) (joint N15). The estimate is recorded per phase as `cut_budget_s`, and admission sets an absolute `cut_deadline` (§7.4) | |
| **Source readiness.** S1: a probe request (§7.7) to the readiness path on |
| @@ -1100,7 +1156,7 @@ reach it through its config bundle, opened with the box's |
| update journal before activating (joint N12; claim §10). Any downgrade of |
| a box that is a participant in a held operation is refused. The console |
| roll recipe states the same floor. The model lets a reboot restore an old |
| - executable and fails in 2,651 of 3,000 seeds, mostly as parks an old |
| + executable and fails in 2,696 of 3,000 seeds (rev 5), mostly as parks an old |
| executable can never let finish. |
| - **The floor is published before any protected production rehearsal** |
| (joint N12). Rev 3's rollout order had it the other way round (§15). |
| @@ -1160,22 +1216,26 @@ Built for rev 4, as the coordinator directed and the joint review |
| recommended: `internal/sim/hostlife/`, a deterministic randomized Go |
| simulation. **It is test-only**: every file is a `_test.go` file, so |
| `go build ./...` never sees it, and it imports only the standard library. |
| -It encodes claim spec rev 2 (cf3a7861) and this spec as they would be |
| -implemented, and every rule is a named, mutable guard (`rules_test.go`). |
| +Rev 5 re-encodes it against claim spec rev 3 (8b5bccb2) and this spec as |
| +they would be implemented, and every rule is a named, mutable guard |
| +(`rules_test.go`). |
| #### 14.2.1 Running it |
| ``` |
| go test ./internal/sim/hostlife/ # the gate: 300 seeds, about a second |
| HOSTLIFE_SEEDS=30000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v -timeout 60m |
| +HOSTLIFE_SEEDS=100000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v -timeout 300m |
| HOSTLIFE_SEED=1796 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v # one seed, full trace |
| ``` |
| 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), runs the seeds, reports |
| -CAUGHT or MISSED, and deletes the copy. Rules run in parallel. |
| +`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`. |
| #### 14.2.2 What it models |
| @@ -1190,7 +1250,33 @@ CAUGHT or MISSED, and deletes the copy. Rules run in parallel. |
| delete. Every request is checked; a violation is an invariant failure. |
| - **Late S3 completion.** A request completes at once (70%) or is |
| "submitted, client cancelled, completed later", within a long-tailed |
| - horizon, after the issuer has moved on, crashed or been replaced. |
| + horizon, after the issuer has moved on, crashed or been replaced. A |
| + quarter of the long tail lands at exactly `H`, the latest S3's |
| + signature-age limit allows; staging PUTs take the long tail one time in |
| + three, other requests one in eight, because the cross-region path is the slow |
| + one. |
| +- **Paused goroutines (rev 5).** Four kinds, each killed by an agent crash |
| + or reboot, as a real goroutine is: |
| + - a **staging round** that revalidated under the staging-work lease and |
| + paused before signing (one round in three), and a **cut round's |
| + lost-response retry** whose first attempt paused (one in three). The |
| + pause runs up to `2 × staging TTL + H`, so it can outlast the lease; |
| + a frozen or paused box holds it longer. The `SafeUntil` check runs |
| + when the goroutine resumes (§7.3); |
| + - a **registry hold or open** that passed its checks and paused (one |
| + hold in 25, one open in six): mostly under 150 steps, one in four up |
| + to 2,000. Half the paused opens are woken **at the worst moment**: |
| + while a newer operation that has already committed holds the row, so |
| + that operation no longer re-asserts its hold; |
| + - a **stalled role worker** replaying an old read (rev 4's actor); |
| + - a **stalled door read**, with the same pause lengths, which resumes |
| + early at its worst moment: when its location's current object belongs |
| + to another incarnation. Rev 4's door reads never stalled for long, and |
| + rev 5's slower lifecycle hid `door-by-version` until they did. |
| +- **Obligations beside roles (rev 5).** Each box runs its obligations in a |
| + runner separate from its role worker, as the agent will, so a park can |
| + run while the same box's role work for a new operation proceeds. Rev 4's |
| + single worker serialized them and hid CC11's race. |
| - **Box faults.** Agent crash (flat children die with the service, nested |
| ones survive, memory is lost), reboot, whole-VM freeze, agent-only |
| pause, partition from the control bucket, clock skew, destruction (a |
| @@ -1211,6 +1297,21 @@ CAUGHT or MISSED, and deletes the copy. Rules run in parallel. |
| faults, then up to 6,000 calm steps: faults linger for a while (so the |
| operator meets a frozen or partitioned participant), then heal; stopped |
| boxes return or are replaced; ops gives every box its secrets key. |
| +- **Scale (rev 5).** One step is the unit of time. `H` = 60 steps; the |
| + execution lease 40, renewed within 15; the cut budget 320 (220 in rev 4); the |
| + staging-work lease 400, longer than the cut budget, as in production |
| + (rev 4 had 30, which made the staging horizon shorter than any landing |
| + and so unobservable); a move aborts if readiness has not come within |
| + 800. Moves are three times as frequent as in rev 4. |
| +- **What claim rev 3 changed in the model.** C3's harmlessness only for |
| + the operation's own version-bound calls; every retirement verifies after |
| + `evidence time + H`, and stragglers go into a further retirement event; |
| + `quiet_after` per region, kept across `free`, raised by each |
| + acknowledgement, and waited for by a create's first wake, a landing's |
| + install and a push's install; park destinations keyed by source version; |
| + one adoption routine with discovery parks; declare-lost by compute |
| + fencing only; the purge journal's phases; `RenderHeld` and |
| + `MaterializeHeld` before every probe. |
| #### 14.2.3 Invariants and results |
| @@ -1218,11 +1319,20 @@ 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. |
| -**30,000 seeds: zero violations** on the final model (101 s). Across those |
| -seeds: 772 completed moves, 784 clean rollbacks, 54 dirty rollbacks, 294 |
| -pre-flip reverts, 153 declared losses, 11,063 aborts (mostly targets |
| -without a secrets key, which T2 refuses until ops installs one), 19,735 |
| -pushes and 50,752 delete-park-free cycles. |
| +**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. |
| #### 14.2.4 Faults the model found beyond the joint review |
| @@ -1244,97 +1354,163 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| | model 11 | The purge path adopted without discovery | one adoption routine for every actor | claim | |
| | model 12 | A hold left behind by a finished operation (a revert re-held its row after opening) blocked serving | reconcile releases a hold whose operation ended | claim | |
| | model 13 | The cut deadline, checked only while probing, let slow installs commit far past the budget | every phase before the commit (§7.4) | moves | |
| +| 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 | |
| #### 14.2.5 Mutation results |
| -Every rule was dropped in turn, in a scratch copy, on one model version: |
| -3,000 seeds each, then 30,000 seeds for every rule not caught at 3,000, |
| -then pairs for rules that looked like double protection. The full |
| -harness output is summarized here; seed numbers reproduce any line with |
| +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 |
| `HOSTLIFE_SEED`. |
| -**Caught alone: 30 of 48 rules.** |
| +| | 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.** |
| | rule | seeds failing | what the model finds | |
| |---|---|---| |
| -| `recovery-pass` (claim C2, §8) | 1,474 / 3,000 | creates and deletes stranded mid-operation never converge | |
| -| `fresh-incarnation` (claim §5.1, R3-12) | 467 / 3,000 | a reused identity meets its own retired marker; the host never serves again | |
| -| `legacy-discovery` (CC4) | 10 / 3,000 | legacy residue in a region the host does not serve | |
| -| `park-by-version` (claim C3, J-N1) | 2,311 / 3,000 | parks never finish | |
| -| `park-all-versions` (claim §6.2) | 572 / 3,000 | parks never finish (older versions resurface) | |
| -| `park-skip-lock` (claim §6.2, J-N6) | 3,000 / 3,000 | parks never finish (the parker's own lock) | |
| -| `retirement-ids` (claim §6.2, J-D5, J-N7) | 214 / 3,000 | parks never finish (one manifest, two events) | |
| -| `quiet-before-ack` (CC1) | 16 / 3,000 | residue after a park, from late replication PUTs | |
| -| `hostguard` (claim C7, J-N8) | 30 / 3,000 | an instance starts with another incarnation's `config.env` | |
| -| `purge-reserve-first` (claim §5.3, J-N9) | 2,300 / 3,000 | stores destroyed under held hosts | |
| -| `purge-adopts` (CC6) | 17 / 3,000 | a store destroyed under a serving legacy host | |
| -| `purge-journal` (CC7) | 6 / 3,000 | a new incarnation's store destroyed by a stalled purge | |
| -| `door-by-version` (claim §6.5, J-N10) | 1 / 3,000 | a door read returns another incarnation's data | |
| -| `evidence-whole-tree` (claim §6.1, J-D3) | 5 / 3,000 | two writers; lost writes | |
| -| `evidence-from-state` (claim §6.1, R2-2) | 2,999 / 3,000 | evidence never comes after an agent restart | |
| -| `floor-boot-recovery` (claim §10, J-N12) | 2,651 / 3,000 | old executables break parks and admission | |
| -| `participant-rows` (claim §2, R2-4) | 10 / 3,000 | source recovery stuck | |
| -| `revalidate-before-effect` (claim C3, J-N2) | 40 / 3,000 | a stalled worker's effects lose acknowledged writes | |
| -| `declare-lost-compute` (CC5, J-D6, J-N3) | 1 / 30,000 | two writers after a frozen target resumes | |
| -| `lost-quarantine` (claim §7.2, CC12) | 2 / 30,000 | a returning box keeps stale local state | |
| -| `cut-deadline` (§7.4, J-N15) | 60 / 3,000 | commits past the budget | |
| -| `revert-journal` (§7.4, J-N11) | 28 / 3,000 | pre-flip recovery stuck on its own writes | |
| -| `rollback-journal` (§7.8, R2-3) | 9 / 30,000 | rollback recovery stuck | |
| -| `dirty-return` (§7.8, INV-2) | 2 / 3,000 | the target's acknowledged writes lost | |
| -| `target-park` (§7.8, R2-5) | 8 / 3,000 | a rolled-back target's replica left live | |
| -| `abort-target-owner` (§7.11, J-N13) | 1,084 / 3,000 | IAM violations | |
| -| `timer-freeze` (§9.4, J-N14) | 10 / 3,000 | clean recovery stuck | |
| -| `timer-canonical` (§9.4, J-N14) | 6 / 3,000 | clean recovery stuck | |
| -| `markers-last` (§7.6, R2-6) | 1 / 3,000 | an acknowledged timer lost | |
| -| `source-readiness` (§7.3, S1) | 14 / 3,000 | pre-flip recovery stuck | |
| - |
| -**Caught only in pairs: 8 rules (double protection).** Each is covered by |
| -its partner; both stay, because the model cannot prove that the partner |
| -holds in every real case. |
| - |
| -| pair | seeds failing (30,000) | 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.** |
| + |
| +| rule | seeds failing | what the model finds | |
| |---|---|---| |
| -| `files-carried` + `start-check` | 1,102 | **the kpmg outage**: the app mints a new `instance.key` over data sealed with the old one | |
| -| `strict-spawn` + `evidence-whole-tree` | 313 | two writers | |
| -| `restore-lineage-filter` + `quiet-before-ack` | 207 | residue | |
| -| `touched-incomplete` + `legacy-discovery` | 5,305 | a freed host's residue | |
| -| `commit-before-open` + `dirty-return` | 10 | lost writes | |
| -| `watchdog-independent` + `declare-lost-compute` | 2 | two writers | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,062 (against 40 per 3,000 for revalidation alone) | a stale purge step destroys a store; the op-id condition is the second line behind revalidation | |
| +| `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 | |
| +|---|---|---|---| |
| +| `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. |
| -**Not exercised by the model: 8 rules, the model's known gaps.** |
| - |
| -| rule | why not | next step | |
| -|---|---|---| |
| -| `seal-by-version`, `staging-quiet` (J-N2) | no seed lands a staging write after the seal, even at 30,000 seeds with a fat staging tail; dropping both together is not caught either | add a staging writer that re-signs after the seal from a stale read past its lease, then require both rules to be caught | |
| -| `exec-admission`, `fresh-admission` | the model's row holds and per-role admission table already refuse what these refuse; dropping both is not caught | model a second consumer of the claim that does not consult the row (the db door, a sibling box's edge) | |
| -| `hold-op-open`, `stale-hold-release` | no stale opener survives once the revert fix was in; stale holds no longer arise | add an open retried by a stalled worker after release | |
| -| `obligations-block-ops` (CC11) | one worker per box serializes obligations and roles, which hides the race | split the obligation runner from the role worker | |
| -| `claim-op-exclusive` | caught once in an earlier model version (1 / 30,000), not in the final one: a delete mid-move stays safe under the quiet horizon | keep as a product rule; widen the delete actor | |
| +**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). |
| -**Seeds:** 300 in the gate (about a second); the 30,000-seed baseline and |
| -the sweep are the evidence for this revision. The harness is committed; |
| -its scratch copies are not. |
| +**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. |
| #### 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); the AWS behaviour it relies on must be checked against the |
| - real service before planning, as the paid-launch work learned ("a fake |
| - provider is never proof"). |
| + 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 only as skew; |
| - correctness never depends on them except through the late-completion |
| - horizon H, which S3's signature-age limit bounds. |
| +- **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. |
| - **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). |
| @@ -1365,7 +1541,7 @@ region that lost. |
| 1. **Ops (in progress):** `CARLOS_SECRETS_KEY` on every region box. |
| 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, with §19.4's changes adopted. |
| + console honours it: claim rev 3, with CC14 (§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. |
| @@ -1376,10 +1552,26 @@ region that lost. |
| production rehearsal** (joint N12). Rev 3 had this after the |
| rehearsals. |
| 7. **Rehearsals** in §14.4's order; each gates the next. |
| -8. **Before planning:** the AWS behaviours the model assumes (copy and |
| - delete by `versionId`, delete-marker semantics, conditional writes on the |
| - claim, the signature-age limit behind H) are checked against the real |
| - service in a scoped sandbox (§14.2.6). |
| +8. **Done (2026-10-02, before planning):** the AWS behaviours the model |
| + assumes were checked against the real service, on a versioned |
| + general-purpose bucket (§14.2.6). Every assumption holds: |
| + - **copy by version:** `CopyObject` from `versionId=V1` returns V1's |
| + body after V2 exists; |
| + - **delete by version:** `DeleteObject --version-id V1` removes only V1; |
| + - **delete markers:** a bare delete leaves a marker, and V2 is still |
| + copyable by its `versionId` (why bare deletes are forbidden on host |
| + prefixes, and why a copy by version ignores a stale marker); |
| + - **create-only writes:** `If-None-Match: *` gets 412 on an existing key |
| + and succeeds on a new one (evidence objects, manifests, `move.json`); |
| + - **conditional writes:** `If-Match` with a wrong ETag gets 412 on both |
| + PUT and DELETE, so conditional delete works on general-purpose |
| + versioned buckets (the claim CAS, lock release); |
| + - **the signature-age limit behind `H`:** a SigV4 request signed 14 |
| + minutes earlier returns 200; one signed 16 minutes earlier returns 403 |
| + `RequestTimeTooSkewed`; |
| + - **copy receipts:** a multipart ETag becomes a single-part ETag on |
| + copy; `CopyObjectResult.ETag` equals the ETag the listing shows; a |
| + `CopySourceIfMatch` mismatch gets 412. |
| ## 16. Follow-on specs |
| @@ -1397,7 +1589,8 @@ No design here, only what each must satisfy. |
| ## 17. Interface points with #199 and the claim spec |
| -The claim spec supersedes #199 rev 3 from its §2 onward. Against claim rev 2: |
| +The claim spec supersedes #199 rev 3 from its §2 onward. Against claim rev 3 |
| +(each point held in rev 2 too): |
| | id | point | status | |
| |---|---|---| |
| @@ -1408,9 +1601,9 @@ The claim spec supersedes #199 rev 3 from its §2 onward. Against claim rev 2: |
| | I-5 | **Recreate** | agreed: create requires the claim free or absent (claim C2) | |
| | I-6 | **Participant rows** | agreed: retained while an operation lists them (claim §2 obligations, K9) | |
| | I-7 | **Flat files** | agreed: claim §6.3 retires the flat `<DataDir>/<host>/`, the sibling env files and markers (joint I-7) | |
| -| I-8 | **`generation.json`, `install-<op>.json`, `lock.json`** | agreed, with CC3: the parker's own renewed lock is excluded everywhere | |
| -| I-9 | **Destructive steps** | agreed: exact versions plus the staging-work lease (claim C3), with CC1's horizon for the replication exception | |
| -| I-10 | **Push** | agreed: later, on §5's handoff and the claim's `pushing` op; it needs CC13 | |
| +| I-8 | **`generation.json`, `install-<op>.json`, `lock.json`** | agreed: the parker's own renewed lock is excluded everywhere (CC3, claim rev 3 §6.2) | |
| +| I-9 | **Destructive steps** | agreed: exact versions plus the staging-work lease (claim C3), with the horizon for the replication exception (CC1, claim rev 3 §6.2a). Open: CC14, the staging writer's `SafeUntil` check | |
| +| I-10 | **Push** | agreed: later, on §5's handoff and the claim's `pushing` op, with every probe rendering held config (CC13, claim rev 3 §6.1). The model found the push's open must also accept a row already open (model 16) | |
| ## 18. Questions for Paul |
| @@ -1444,7 +1637,7 @@ The db door refuses on every move kind (claim spec §8). |
| | **K2 Acquire** | The request door CASes `serving` → `moving` only when the holder incarnation equals the record's and no other op holds the claim; it sets op id, participants and `exec` = source box. | |
| | **K3 Execution to none** | A participant that has written stop evidence for this op id (§5.3) may CAS `exec` from itself to `none`. Nobody moves `exec` from one box to another directly. | |
| | **K4 Execution handoff** | From `none` to a participant, by that participant, citing the previous holder's evidence object for this op id: at the flip (to target), at source recovery (to source), and at `reverting` (the source, citing its own evidence). | |
| -| **K5 Revalidation** | Before each destructive step the actor re-reads the claim and requires op id, kind, phase and `exec` to be what the step expects (claim spec C3); it holds the lease of every location it writes, acting before `SafeUntil`, with the exception in §19.3 D4. | |
| +| **K5 Revalidation** | Before each destructive step the actor re-reads the claim and requires op id, kind, phase and `exec` to be what the step expects (claim spec C3); it holds the lease of every location it writes, acting before `SafeUntil`, with the exception in §19.3 D4. A staging writer checks `SafeUntil` immediately before it signs each request, after any pause (§7.3, model 14). | |
| | **K6 Wake admission** | `doWake` reads the claim fresh (claim spec §8) and applies K1. A box that reads a claim whose `exec` does not name it kills that host's process tree (§5.3 step 1) before anything else. | |
| | **K7 Other operations** | Delete, purge, park and push start only from `serving` (claim spec §4); while a move op holds the claim they are refused. Create requires free or absent. | |
| | **K8 Release** | Only the move releases to `serving`, naming `exec` (target after `done`; source after `rolled_back` or `aborted`), and only when every obligation this op created is gone (§7.8, §7.9). | |
| @@ -1454,7 +1647,10 @@ The db door refuses on every move kind (claim spec §8). |
| | **K12 Touched** | Every move write site CAS-adds its region or box to `touched` before its first write: the source adds the target region before the first staging round; the target adds its box at `checking`; a dirty return adds nothing new (the source region and box are already there). | |
| | **K13 Evidence durability** | Evidence objects are create-only per (op id, role) in the deployment bucket, recomputable from system state after a restart (§5.3), and referenced from the claim journal, never inlined. | |
| -### 19.3 Rev 3's requests, against claim rev 2 |
| +### 19.3 Rev 3's requests, against claim rev 2 and rev 3 |
| + |
| +Each status below holds in claim rev 3 as well, except D6, which rev 3 |
| +completes. |
| | id | status in claim rev 2 | here | |
| |---|---|---| |
| @@ -1463,7 +1659,7 @@ The db door refuses on every move kind (claim spec §8). |
| | D3 strict spawn, whole-tree evidence | adopted (§6.1, joint text) | §5.3 | |
| | D4 cross-region staging exclusion | replaced, as the review ruled: a shared staging-work lease (C3); sealing and draining are this spec's | §7.3 | |
| | D5 per-event retirement destinations | adopted (§6.2) | §6.4 | |
| -| D6 declare-lost | adopted with an execution-lease branch; **this spec drops that branch** (model 5) | §7.10, CC5 | |
| +| D6 declare-lost | adopted with an execution-lease branch; this spec dropped that branch (model 5), and **claim rev 3 drops it too** (CC5): compute fencing only, the lease for liveness | §7.10, CC5 | |
| | D7 move-kind transitions | adopted (§4, joint text) | §19.1 | |
| | D8 who waits for obligations | adopted (§2) | K8 | |
| | I-7 flat local inventory | adopted (§6.3) | §6.1 | |
| @@ -1474,6 +1670,13 @@ This spec does not edit the claim spec. Each change below is what the |
| model needed for its invariants to hold; the mutation column says what the |
| model finds when the rule is dropped (§14.2.5). |
| +**CC1 to CC13 (rev 4, against claim rev 2): all adopted in claim rev 3** |
| +(8b5bccb2), which maps them in its §12: CC1 to C3, §2 `quiet_after` and |
| +§6.2a; CC2 and CC3 to §6.2; CC4 and CC8 to §9; CC5, CC9 and CC12 to §7; |
| +CC6 and CC7 to §5.3; CC10 to §8; CC11 to §4; CC13 to §6.1. Rev 5's model |
| +encodes rev 3's text; §14.2.5 gives each rule's mutation result, CC11's |
| +included now (model 15). |
| + |
| | id | change to claim rev 2 | why (model) | |
| |---|---|---| |
| | **CC1** | **A late-completion horizon on every retirement.** C3's "late completion is harmless" holds only for version-bound calls. Ordinary replication, the C3 exception, is plain PUTs to reused LTX names. A park acknowledges only after a verification listing taken later than `evidence time + H` (H = S3's 15-minute signature-age limit plus the longest request), and parks anything found then as a further retirement event. Persist a per-region `quiet_after` in the claim (kept across `free`, like `retired_incarnations`) and make any install into that region's namespace wait for it | model 1: residue in a freed host's namespace | |
| @@ -1486,10 +1689,25 @@ model finds when the rule is dropped (§14.2.5). |
| | **CC8** | **One adoption routine for every adopting actor**, discovery included | model 11 | |
| | **CC9** | **A fresh read with no operation ends a self-fence** (§7.1): a box clears its local execution-lease file when the claim shows it is not a participant | model 9 | |
| | **CC10** | **Reconcile releases a stale hold**: a held row whose `hold_op` is not the claim's operation, on the box the claim names as executor of a `serving` host, is opened | model 12 | |
| -| **CC11** | **No operation starts over a pending chore in its locations**: the start CAS from `serving` fails if an obligation names a region or box the operation will write | model gap: not exercised (§14.2.5) | |
| +| **CC11** | **No operation starts over a pending chore in its locations**: the start CAS from `serving` fails if an obligation names a region or box the operation will write | model 15 (rev 5): a move landed into a region whose park was still running, and the park retired the landing's new versions: acknowledged writes lost on cold restore, or a landing that never converges | |
| | **CC12** | **A quarantined box retires its own state.** §7.2 says a box on `lost` is refused "until its old state has been retired"; name the actor: the returning box itself, under the host guard, before anything else | the returning box otherwise keeps stale local state | |
| | **CC13** | **Every probe renders held config** (`RenderHeld`, `MaterializeHeld`) before spawning, including a future push's | model 4 | |
| +**Rev 5's request, against claim rev 3:** |
| + |
| +| id | change to claim rev 3 | why (model) | |
| +|---|---|---| |
| +| **CC14** | **Staging residency rests on `SafeUntil`.** C3's closing paragraph says correctness no longer depends on the clock and pause assumption, because every destructive request is version-bound. Cross-region staging is the exception: a staging PUT creates a version, and the moves spec's staging horizon (`seal time + staging TTL + H`, §7.3) bounds only requests signed before the lease's `SafeUntil`. State that every request under the staging-work lease checks `SafeUntil` immediately before it is signed, after any pause, and that §3.1's margin must cover clock skew plus the longest pause between that check and the signature | model 14: staging residue in a region the instance left, or in the serving region (`sign-before-safeuntil`, §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 |
| +already passed; CC11 keeps operations off regions with pending chores; and |
| +`free` needs every obligation gone. The model drops this spec's T12 |
| +(which reads `quiet_after`) and no cut ever waits. Keeping the field costs |
| +one map in the claim and guards any future path that acknowledges before |
| +its horizon; removing it is the claim authors' call. |
| + |
| ## 20. Copy (pending copy review) |
| Drafts for the operator CLI. None is approved; every string goes through the |
| @@ -1602,7 +1820,7 @@ New findings: |
| | # | finding | owner | rev 4 | |
| |---|---|---|---| |
| | N1 | late server-side completion | claim, with moves | exact-version deletes and copies (claim C3, §6.4); **plus CC1**: the replication exception is not version-bound, so retirements verify after the horizon. Mutations `park-by-version`, `park-all-versions` and `quiet-before-ack` are caught | |
| -| N2 | delayed staging round corrupts sealed staging | moves | staging-work lease; revalidation under it; seal by version; staging retired after its writers' horizon (§7.3). The stalled-worker actor exercises it; `revalidate-before-effect` is caught. See §14.2.5 for `seal-by-version` | |
| +| N2 | delayed staging round corrupts sealed staging | moves | staging-work lease; revalidation under it; seal by version; staging retired after its writers' horizon (§7.3). The stalled-worker actor exercises it; `revalidate-before-effect` is caught. **Rev 5:** the seal and the horizon are proven too (`seal-by-version` 5 / 30,000, `staging-quiet` 9 / 30,000), and both rest on a third rule the model found: sign only before `SafeUntil` (model 14, CC14) | |
| | N3 | declare-lost starts a second writer | claim, with moves | compute fencing only (§7.10, CC5) | |
| | N4 | unjournaled claim and record gaps | claim | intent in the start CAS and a recovery owner per state (claim C2, §8); the model's `recovery-pass` mutation is caught in about half of all seeds | |
| | N5 | lazy legacy adoption | claim | `touched.complete` (claim §9) **plus CC4** discovery at adoption; `legacy-discovery` caught | |
| @@ -1621,3 +1839,26 @@ New findings: |
| The joint review's verdict was "not ready" for both specs and asked for |
| the expanded simulation before planning. That simulation now exists and |
| passes; the claim changes it requires are §19.4. |
| + |
| +### 22.4 The coordinator's round on rev 4 (claim rev 3, 8b5bccb2) |
| + |
| +| request | rev 5 | |
| +|---|---| |
| +| exercise the eight rules rev 4 listed as gaps, each caught alone or in a stated pair | six caught alone; `exec-admission` and `hold-op-open` caught only together with `start-check`, a triple, 5 / 100,000, with every pair of the three at 0 / 100,000 (§14.2.5). The model's new actors: paused staging signers, paused registry writes woken at the worst moment, an obligation runner beside the role worker, admission from cached reads, stalled door reads | |
| +| seal by version and the staging horizon first (N2's remaining half) | both proven, and the rule under them found: a staging writer signs only before `SafeUntil` (model 14, §7.3, CC14) | |
| +| prove CC11 | proven: dropping it loses acknowledged writes on a cold restore (model 15) | |
| +| re-run 30,000 seeds, at least one 100,000-seed run, the full mutation sweep | 30,000 and 100,000 seeds, zero violations; the sweep is §14.2.5 | |
| +| re-encode against claim rev 3 | done (§14.2.2): C3 limited to the operation's own version-bound calls; verification after `evidence time + H`, stragglers as a further retirement event; `quiet_after` kept across `free`, installs waiting for it; destinations keyed by source version; one `claim.Adopt` with discovery parks; declare-lost by compute fencing only, the lease for liveness; the purge journal's phases; `RenderHeld` and `MaterializeHeld` before every probe | |
| +| mark §15 step 8 done with the real-AWS results | done (§15 step 8): every assumption holds | |
| + |
| +Found on the way: |
| + |
| +- **Model 16** (§14.2.4): a push's open must accept a row already open. |
| + Push is F7's; recorded there through I-10 (§17). |
| +- **`readiness-quiet` and the `quiet_after` install wait cannot bite under |
| + claim rev 3** (§14.2.5). Kept as defence in depth; noted for platform-1e |
| + (§19.4). |
| +- **`restore-lineage-filter` adds nothing the model can see** once the |
| + 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. |