amadan
spec: move-any-app rev 7.5: joint round 4, claim rev 6.2 encoded (#175)
Written against claim rev 6.2 (30d572c4). R4-1: the restore contract
is one implementable contract: the sealed transfer is a verified final
snapshot, generation.json names it by key, version, TXID and checksum,
and the restore is litestream v0.5.14's planner from that snapshot,
overlap allowed, failing closed on a missing snapshot, a gap or a
checksum mismatch; the content comparison is gone; §7.6 produces what
the restore consumes. R4-2: installation stamps as claim rev 6.2 states
them, op ids opaque. R4-3: the live set is {authoritative region,
location, generation} with a phase table naming the authoritative
region; claim §6.2a cited for the sweep-side rule. R4-4: retirement
under the purge's own claim, encoded. Q2: the absent-claim branch is
explicit. The random generator's marker-hold and targeted-freeze
schedules, the retention fixture and two successful-move oracles let
the sweep catch generation-conditional, declare-lost-compute and
sweep-namespace alone; the three-rule door combination is reported as
not minimal.
The model (5de710b2, e08c5fd0) encodes all of it. Results: 30,000 and
100,000 seeds clean; 75 rules, 60 caught alone, 12 in stated
combinations, 2 liveness, 1 unreachable, none unexercised. §22.11 has
every disposition.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+459
−226
docs/superpowers/specs/2026-10-02-move-any-app-design.md+459 −226
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 02866d4cd..1cf1ffaa4 100644 |
| --- a/docs/superpowers/specs/2026-10-02-move-any-app-design.md |
| +++ b/docs/superpowers/specs/2026-10-02-move-any-app-design.md |
| @@ -1,7 +1,36 @@ |
| # Move any app or instance to another region: Phase 1, a safe single-instance move |
| **Date:** 2026-10-03 |
| -**Revision:** 7.4. |
| +**Revision:** 7.5. |
| + |
| +- **Rev 7.5** answers the moves side of **joint round 4** |
| + (`CODEX-FINDINGS-JOINT-R4.md`, cited "R4-n") and is written against |
| + **claim spec rev 6.2** (30d572c4), which answers the claim side (R4-2 |
| + installation stamps, R4-3 the region-qualified live set, R4-4 |
| + retirement under purge) and the moves session's three questions (rev |
| + 6.1, 79a5243c); §22.11 has every disposition. **R4-1 (P1):** the restore |
| + contract is one implementable contract (§5.1): the sealed transfer is a |
| + verified final snapshot, `generation.json` names it by key, version, |
| + TXID and checksum, and the restore is litestream v0.5.14's planner from |
| + that snapshot, overlap allowed, failing closed on a missing snapshot, a |
| + gap or a checksum mismatch; §7.6 produces what the restore consumes. |
| + The model's databases are key-value maps with inserts, updates and |
| + deletes, its replica objects are LTX files with ranges, page images, |
| + checksums and compaction, and its restore is the planner, so a |
| + compacted continuation and a genuine gap each have a witness |
| + (`restore-overlap`, `restore-gap-closed`). **R4-2:** installation stamps |
| + as claim rev 6.2 states them, the op counter gone (§6.4); a stale writer |
| + across a retire-and-reinstall is the new witness (`fence-stamp`). |
| + **R4-3:** the live set is `{authoritative region, location, |
| + generation}`, with a phase table naming the authoritative region |
| + (§5.1), and a witness for an old regional PUT after adoption |
| + (`live-set-region`). **R4-4:** retirement under the purge's own claim, |
| + encoded. The random generator gains marker-hold and targeted-freeze |
| + schedules, a retention fixture and two successful-move oracles, so |
| + `generation-conditional`, `declare-lost-compute` and `sweep-namespace` |
| + are now caught by the sweep as well. Results: 30,000 and 100,000 seeds |
| + clean; 75 rules, 60 caught alone, 12 in stated combinations, 2 |
| + liveness, 1 unreachable, none unexercised (§14.2.5). |
| - **Rev 7.4** answers the moves side of **joint round 3** |
| (`CODEX-FINDINGS-JOINT-R3.md`, cited "R3-n") and is written against |
| @@ -221,8 +250,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 6 at 3ea3f90c** on `design-replica-ownership`. Rev 7.4 is |
| - written against rev 6; rev 7.2 and 7.3 against rev 5.2 (465fee96); rev 7.1 against rev 5.1 (64eec93b); rev 7 |
| + **rev 6.2 at 30d572c4** on `design-replica-ownership`. Rev 7.5 is |
| + written against rev 6.2; rev 7.4 against rev 6 (3ea3f90c); rev 7.2 and 7.3 against rev 5.2 (465fee96); rev 7.1 against rev 5.1 (64eec93b); rev 7 |
| against rev 5 (4a458a9c); rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3 |
| (8b5bccb2); rev 4 against rev 2 (cf3a7861). |
| @@ -325,7 +354,10 @@ adopted them; rev 5's CC14 is in claim rev 3.1 and rev 4; rev 6's CC15 to |
| CC19 are in claim rev 5, rev 7's CC20 and CC21 in claim rev 5.1 (CC21 |
| as a purge fence), and rev 7.1's CC22 in claim rev 5.2, with C5a (§19.4). |
| Claim rev 6 (3ea3f90c) answers the claim side of joint round 3 (R3-2, |
| -R3-3, R3-4) with no request from this spec; rev 7.4 encodes it (§6.4, |
| +R3-3, R3-4) with no request from this spec; rev 7.4 encodes it. Claim rev |
| +6.2 (30d572c4) answers joint round 4's claim side (R4-2 installation |
| +stamps, R4-3 the region-qualified live set, R4-4 retirement under purge) |
| +and the moves session's three questions; rev 7.5 encodes it (§5.1, §6.4, |
| §14.2.2, §19.4). |
| Until platform-1e adopts them, this spec states each as the behaviour it |
| relies on. |
| @@ -491,78 +523,111 @@ by the commit's claim CAS (§7.9), by a push's probe CAS (F7), and by a |
| dirty rollback's source probe (§7.8). Restore reads it from the same fresh |
| admission read as `holder.location` (claim C3a). |
| -**The restore contract (J2-R2-1; R3-1).** A restore reads |
| +**The restore contract (J2-R2-1; R3-1; R4-1).** A restore reads |
| `holder.location`, generation `holder.generation`, in the box's own |
| bucket, and nothing else. It never picks "the newest object under the |
| -prefix". Rev 7.3 said it "replays every replica object of that generation, |
| -current and noncurrent", which is not an algorithm (R3-1): a generation |
| -can hold the installed snapshot, later replication, a duplicate of the |
| -snapshot from a copy that completed late, and an LTX PUT that completed |
| -after a later one. **The algorithm:** |
| - |
| -1. **The snapshot is immutable and named.** `generation.json` records the |
| - installed snapshot's `versionId` and its TXID (`snapshot_version`, |
| - `snapshot_txid`), taken from the install manifest. The restore opens |
| - exactly that version. A second `base` version under the generation (a |
| - late copy) is never read. |
| -2. **Continuation is by TXID.** Every LTX object in the generation carries |
| - its transaction range `[min, max]` in its key, as litestream writes |
| - them. The restore takes, in TXID order, the objects whose `min` is |
| - `snapshot_txid + 1` and then each next contiguous range, opening each |
| - by the `versionId` the listing returned (noncurrent versions included, |
| - so a key a later PUT overwrote still contributes its version). |
| -3. **Duplicates and older checkpoints are skipped.** A version whose |
| - range the chain already covers is either a duplicate (identical |
| - content, by its checksum) or an older checkpoint of the same |
| - transactions; either way it adds nothing and is skipped. |
| -4. **A conflict refuses.** A version whose range overlaps the chain but |
| - whose content differs from what the chain holds at those TXIDs is a |
| - conflict: the restore stops with a member-safe reason and pages. It |
| - never guesses which history is right; under this spec no such |
| - version can exist within one generation, because one executor writes |
| - a generation (INV-1) and every other write lands in its own generation. |
| -5. **A gap ends the chain.** The restore stops at the first missing TXID |
| - and reports the gap. Litestream does not advance past a failed upload, |
| - so a gap within a generation means a replica object was lost, which |
| - this spec treats as a lost checkpoint (INV-2's RPO line, §14.2.3). |
| +prefix". Rev 7.4's algorithm required each next LTX object to start at |
| +`current TXID + 1`, which is not how LTX works (R4-1): compaction merges |
| +files into one covering `[Min of first, Max of last]` whose page images |
| +are the state at `Max`, deletes the inputs, and so leaves overlapping |
| +ranges and no individual intermediate objects. A snapshot ending at 100 |
| +with one current continuation `[91, 110]` is a healthy replica; rev 7.4 |
| +would have refused it, or restored through 100 and let a move commit |
| +without transactions 101 to 110. Rev 7.5 takes **one implementable |
| +contract: the sealed transfer is a verified final snapshot, and the |
| +restore is litestream's own planner over that snapshot and the |
| +generation's later files**, exactly as `litestream` v0.5.14 and |
| +`superfly/ltx` v0.5.1, the versions this repository pins, behave. |
| + |
| +1. **The sealed transfer is a snapshot.** At the cut, after the final |
| + checkpoint, the source writes a snapshot of the stopped database: one |
| + LTX file at litestream's snapshot level (9), `MinTXID = 1`, `MaxTXID = |
| + N`, every page, with its `PostApplyChecksum`. It seals that object by |
| + key and `versionId` (`seal.db`, §7.4). Nothing else of the replica is |
| + transferred: not the level-0 and level-1 files, which the snapshot |
| + subsumes. `N` is the **required final TXID** of the transfer. |
| +2. **The install copies the snapshot into the generation**, by |
| + `versionId`, to `<location>g-<move id>/ltx/9/<1>-<N>.ltx` (litestream's |
| + layout under the generation prefix), verifying its size and its |
| + trailer checksum, and records in the install manifest the key, the |
| + `versionId` the copy created, `N` and the checksum (§7.6 `copying`). |
| +3. **`generation.json` names the snapshot**: `snapshot_key`, |
| + `snapshot_version`, `snapshot_txid = N`, `snapshot_checksum`. These |
| + are the snapshot identity; a second `base` version under the |
| + generation, from a copy that completed late, is never read. |
| +4. **The restore is litestream's planner** (`replica.go` |
| + `CalcRestorePlan`), with one substitution: the snapshot it starts from |
| + is the one `generation.json` names, opened by `versionId`, not "the |
| + latest snapshot under the prefix". From `current = N` it takes, among |
| + the generation's current files at every level, the file with |
| + `MinTXID ≤ current + 1` and `MaxTXID > current` (overlap allowed: |
| + `ltx.IsContiguous`), preferring the highest `MaxTXID`, then the lowest |
| + `MinTXID`, then the higher level, applies it, sets `current = |
| + MaxTXID`, and repeats until nothing extends the range. A compacted |
| + `[91, 110]` over a snapshot at 100 is taken: its pages are the state |
| + at 110, so applying them over the state at 100 is exact. Files are |
| + taken from the current listing, as litestream lists them; nothing |
| + reads noncurrent LTX versions, because compaction's deletes make the |
| + superseded files noncurrent on purpose. |
| +5. **Fail closed.** The restore refuses, with a member-safe reason and a |
| + page, and never produces a database, when: the snapshot version is |
| + missing or its `MaxTXID` is not `snapshot_txid`; a current file starts |
| + beyond `current + 1` once nothing extends the range (litestream's |
| + "non-contiguous ltx files": a gap); or the database checksum after the |
| + last applied file is not that file's `PostApplyChecksum`. "Compare |
| + content at those TXIDs" is gone: compacted objects do not retain |
| + intermediate states, and the checksum is the validation LTX provides. |
| + A restore that falls short of `snapshot_txid` is a refusal, not a |
| + result. |
| +6. **What a gap means.** Litestream does not advance past a failed |
| + upload, and a timed-out upload is retried before the next range, so a |
| + gap in a generation's current listing is a lost or not-yet-landed |
| + object, never a healthy replica. The refusal holds until the object |
| + lands, or pages an operator. |
| So: |
| - a request that completes late can only add an object to **its own** |
| generation. A late install copy repeats the sealed snapshot (another |
| - `base` version, never opened); a late LTX PUT from an old executor lands |
| - in a generation the claim no longer names. Neither is ever restored |
| - into the current state; |
| + version, never opened); a late LTX PUT from an old executor lands in a |
| + generation the claim no longer names. Neither is ever restored into the |
| + current state; |
| - the claim moves to a new generation only after that generation is fully |
| installed and probed, so a restore never meets a half-written one; |
| - what lands in a dead generation after its retirement is residue, not |
| data: the straggler sweep (§6.4) retires it. |
| **Against litestream.** `lease.Restore` (`internal/lease/lease.go:404`) |
| -delegates to litestream, whose S3 client opens LTX keys without a |
| -`VersionId` and plans a transaction range from the keys it lists. Phase 1 |
| -needs two changes there: the snapshot opened by `versionId`, and the |
| -listing taken with versions so an overwritten key's older version is |
| -still a candidate for step 2. Both are implementation work in the restore |
| -plan (§15 step 8 verifies the S3 behaviour they rely on; rows 2, 3 and |
| -10 of claim §13). Until then a restore from a generation with a reused |
| -LTX key could miss the version a late PUT overwrote. |
| - |
| -**In the model** (§14.2.2) a history is an ordered list of transaction |
| -ids and every LTX object carries the whole history up to its checkpoint, |
| -so step 2 reads "a version continues the chain if its history extends |
| -it", step 3 "is a prefix of it", and step 4 "is neither". Rev 7.3's model |
| -took the union of every version's writes, which no restore can implement |
| -and which hid any conflict; the model drops the contract |
| -(`restore-by-generation`: the newest object under the location) and loses |
| -acknowledged writes (§14.2.5). |
| +delegates to `Replica.Restore`, whose planner lists each level without |
| +versions and opens LTX files by key. Phase 1 needs two changes there: the |
| +snapshot opened by the `versionId` `generation.json` names, and the plan |
| +rooted at that snapshot rather than the latest one listed. The rest of |
| +the planner, overlap rule, preference order and the non-contiguous error |
| +included, is used as it is. The repository's compaction ladder |
| +(`lease.go:55`: levels 0 to 3) is what produces the overlapping ranges |
| +step 4 handles. §15 step 8 verifies the S3 behaviour (claim §13 rows 2, |
| +3 and 10). |
| + |
| +**In the model** (§14.2.2) a database is a map of keys to values; |
| +transactions insert, update and delete; an LTX file carries its range, |
| +the final image of every key it touches and the checksum after `Max`; |
| +compaction merges three level-0 files into a level-1 file and deletes the |
| +inputs; a snapshot is the file `[1, TX]` with every page. The restore is |
| +step 4 and step 5 as written. The model drops the contract |
| +(`restore-by-generation`: the newest object under the location) and |
| +loses acknowledged writes; it drops the overlap rule (`restore-overlap`: |
| +rev 7.4's `min == current + 1`) and loses a compacted continuation; it |
| +drops the gap refusal (`restore-gap-closed`) and wakes a host without |
| +durable transactions (§14.2.5). Rev 7.4's model carried a full |
| +transaction history in every object, which no LTX file has, and so could |
| +not show any of this (R4-1). |
| **Markers.** A generation is named in three markers. None is a record |
| field. |
| | marker | where | written | content | |
| |---|---|---|---| |
| -| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256","snapshot_version","snapshot_txid"}`: the last two name the installed snapshot's `versionId` and TXID, which the restore starts from (R3-1) | |
| +| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256","snapshot_key","snapshot_version","snapshot_txid","snapshot_checksum"}`: the snapshot identity the restore starts from (R3-1, R4-1) | |
| | `<dbPath>.gen` | beside the local database | after a restore completes | `{"op","incarnation","location"}` | |
| | `.files-gen` | inside the files directory | **last**, after files, `<host>.env`, timers and the carried registry columns are all durable (§7.6) | `{"op","incarnation"}` | |
| @@ -581,6 +646,25 @@ content digest, and from F4's definition of the files directory (§6.1). |
| Absent everywhere means origin. The claim's `gen` is a per-write version |
| (claim spec §2), not a generation, so it never appears in a marker. |
| +**The authoritative region (claim rev 6.2 §6.2a, R4-3).** The live set is |
| +`{authoritative region, holder.location, holder.generation}` plus the |
| +versions this spec names for the generation (the snapshot version in |
| +`generation.json`, noncurrent included). Objects of the generation are |
| +live only in the authoritative region's bucket; a matching key in any |
| +other region is residue, and the sweep parks it. The authoritative region |
| +is the region of the holder's current installation: |
| + |
| +| claim state | authoritative region for `holder.generation` | |
| +|---|---| |
| +| `serving`, `pushing` | `op.exec`'s region | |
| +| `moving` (before the flip), `reverting` | the source's region | |
| +| `landing` (after the flip, before the commit) | the source's region: `holder.generation` is still the pre-move generation, and the target's new generation is not yet named | |
| +| `landing` after the commit, until the claim releases | the target's region | |
| +| `restoring`, clean | the source's region | |
| +| `restoring`, dirty, until the source's probe names the return generation | the source's region | |
| +| `restoring`, dirty, after the source's probe | the source's region, for the return generation | |
| +| `creating`, `deleting`, `parking`, `purging`, free | none: nothing is live | |
| + |
| **The start check (INV-4, J2-R2-8).** Before every spawn (`Start`, `Seed`, |
| `ProbeWake`), the activator requires: |
| @@ -807,23 +891,32 @@ Phase 1 uses the claim spec's park (§6.2 there) and local retirement |
| 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. **The marker is scoped to an installation** (claim rev 6 §6.4, |
| - R3-3): `{incarnation, op id of the installation being retired}`. It |
| - refuses a writer carrying that incarnation and an operation at or |
| - before the retired one. A later **new installation** of the same |
| - incarnation on this box, a move back to a region the instance left, |
| - replaces the marker under the guard, in the landing's `checking` phase, |
| - conditional on a fresh claim read showing the new operation current and |
| - this box its target; the marker then names the new op, and the retired |
| - installation's workers, carrying the old op, stay refused. Every |
| - host-guard writer (config sync, release adoption) records the operation |
| - it validated under when it selects a row, and the guard compares that |
| - with the marker. Rev 7.3's marker fenced the whole incarnation, and the |
| - model's move back never passed its probe: it timed out and rolled back, |
| - which a green sweep did not distinguish from success. The model now |
| - requires a successful UK→US→UK round trip as an unmutated witness |
| - (§14.2.5, `fence-by-installation`). How operations are ordered in |
| - production is a question for the claim spec (§19.4). |
| + refused. **Installation stamps** (claim rev 6.2 §6.4, R3-3, R4-2): an |
| + installation's stamp is the claim `gen` captured at the CAS that made it |
| + current on this box (a create's serving CAS, a landing's flip), kept |
| + for as long as the installation exists, serving included. Each box |
| + keeps, under the guard, a record per host incarnation: |
| + `{active_stamp | none, retired_stamps}`. Every host-state writer |
| + (config sync, release adoption, the activator's admission) carries |
| + `{incarnation, stamp}` from the record it read under the guard when it |
| + selected its work, and is admitted only if its stamp **equals** the |
| + active stamp; a lower stamp, a retired stamp, or any stamp while the |
| + active stamp is `none` is refused. Retirement moves the active stamp |
| + into the retired set and sets `none`. A new installation of the same |
| + incarnation, a move back to a region the instance left, sets the active |
| + stamp to its own captured stamp in the landing's `checking` phase, under |
| + the guard, after a fresh claim read shows its operation current and |
| + this box the landing participant. Op ids are opaque and never compared |
| + (claim rev 6.2 Q1). Rev 7.4's marker compared operations by an order |
| + the production system does not have and admitted its own installation |
| + only by a `- 1` in the model (R4-2); rev 7.3's marker fenced the whole |
| + incarnation, and the move back never passed its probe. The model keeps |
| + the stamp record exactly as claim rev 6.2 states it, requires the |
| + UK→US→UK round trip to serve on UK again unmutated, records a landing |
| + probe refused by its own installation record as a violation, and shows |
| + a stale config pass admitted across a retire-and-reinstall only when |
| + the stamp check and the host guard's fresh check are both gone |
| + (§14.2.5, `fence-by-installation`, `fence-stamp`). |
| No park destination is an ancestor of a live prefix (codex 8). **A park is |
| its own journaled phase**, complete before any install into the vacated |
| @@ -846,11 +939,23 @@ error; a child prefix of 64 hex characters is an incarnation location, |
| residue unless it is `holder.location`; a level directory directly under |
| the host prefix is the legacy location, residue unless `holder.location` |
| is the host prefix itself; and within `holder.location`, every generation |
| -other than `holder.generation` is residue. The version `generation.json` |
| -names as the snapshot (§5.1) is in the live set and is never touched. The |
| -model keeps the real cap and shows a replication PUT of an incarnation 33 |
| -recreates old landing after the list forgot it (`sweep-namespace`, |
| -§14.2.5). Being an obligation, it |
| +other than `holder.generation` is residue. **The live set is |
| +region-qualified** (claim rev 6.2 §6.2a, R4-3): `{authoritative region, |
| +holder.location, holder.generation}` plus the versions §5.1 names for the |
| +generation, the snapshot version `generation.json` names included, is |
| +protected in the authoritative region's bucket only (the table in §5.1); |
| +a matching key in any other region is residue and is parked, so a |
| +replica PUT for a legacy host serving in UK that lands in US after US's |
| +retirement is parked, not exempted. Claim §6.2a owns the sweep-side rule: |
| +the sweep never parks or deletes an object version in the live set, never |
| +touches the version `generation.json` names, never treats the marker as |
| +residue, reads the live set under the same fresh claim observation it |
| +uses for everything else, and touches nothing in a location whose marker |
| +disagrees with `holder.generation`, raising an alert instead. The model |
| +keeps the real cap and shows a replication PUT of an incarnation 33 |
| +recreates old landing after the list forgot it (`sweep-namespace`), and |
| +an old US PUT for a legacy host serving in UK parked only when the live |
| +set is region-qualified (`live-set-region`, §14.2.5). Being an obligation, it |
| holds off any new operation over that region until it acknowledges (CC11), |
| and every delete names a snapshot version, so nothing written later is |
| touched. |
| @@ -1159,11 +1264,11 @@ journaled in `<DataDir>/.moves/<host>/<move id>/` (F12). |
| |---|---|---|---| |
| | `checking` | read `stopped-source.json`; require the claim's `op.kind = landing` with this move id and execution holder = this box; require this box in `touched.boxes` (CAS-add before any local write); read `move.json` and require its incarnation; acquire the lease on `instances/<host>/` in its own bucket (claim spec C3) and hold it through `published` | | replayable | |
| | `parking` | bucket-park whatever is at `holder.location` in its own bucket into `superseded/<move id>/<host>/` (an earlier stay of this incarnation) | the park manifest exists **and** its deletion set is deleted | replayable by the claim's rule (manifest present: replay the deletion set) | |
| -| `copying` | per-key copy of `replica/`, by the sealed `versionId`s, into this move's own generation, `<location>g-<move id>/`, verifying each size; then write the install manifest `<location>g-<move id>/install.json` (every key and size) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the copy never deletes. A copy that completes late lands in this generation again (§5.1) | |
| -| `published` | write `<location>generation.json` with op, incarnation and the install manifest's sha256 | `generation.json` names this move | replayable | |
| +| `copying` | copy the **sealed snapshot** (`seal.db`: one level-9 LTX file `[1, N]`, by `versionId`, §5.1 step 1) into this move's own generation at `<location>g-<move id>/ltx/9/<1>-<N>.ltx`, verifying its size and trailer checksum; then write the install manifest `<location>g-<move id>/install.json` with the snapshot's key, the `versionId` the copy created, `N` and the checksum (R4-1) | the install manifest exists | replayable: staging is immutable after the flip, the generation is new, and the copy never deletes. A copy that completes late lands in this generation again as another version, which nothing reads (§5.1) | |
| +| `published` | write `<location>generation.json` with op, incarnation, the install manifest's sha256 and the snapshot identity: `snapshot_key`, `snapshot_version`, `snapshot_txid`, `snapshot_checksum` (§5.1) | `generation.json` names this move | replayable | |
| | `local` | local-park any warm database (with `<dbPath>.gen`), files directory and `<host>.env` into `.parked/superseded-<move id>/`; extract the archive's files; write `<host>.env` from the archive; `ReplaceTimers` from the snapshot (§9.4); set `Replication` and `NextDue`; remove the host's restore-verification entry (§6.3); fsync all; **then** write `.files-gen` | `.files-gen` names this op and incarnation, and the journal records each sub-step | each sub-step is idempotent and journaled; `.files-gen` is written last, so its presence vouches for all of them (codex R2-6) | |
| | `configured` | render through §9.1 and materialize through §9.2; **for a forward install (this landing, a push)** the move-bound ack's bundle etags must equal `move.inputs` | ack matches | replayable; a mismatch is a rollback ("configuration changed during the move"), and the source's recovery then runs on the new bundle (§7.7, J2-R2-5). **A recovery install (§7.8) runs this phase on current inputs and records them; it is never gated on `move.inputs`** (R2-5) | |
| -| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` | |
| +| `restored` | restore cold from `holder.location`, generation `<move id>` (the restore contract, §5.1: the planner from the named snapshot, which at install is the snapshot alone and must reach `snapshot_txid`, or the phase fails and rolls back), write `<dbPath>.gen`, `CheckDB` (`backend_exec.go:313`), record `landing.installed_db_sha256` | | replayable until `probing` | |
| | `probing` | the probe (§7.7) | | **never replays an earlier phase** (INV-7); a crash restarts only the probe | |
| | `probed` | probe passed | | | |
| @@ -1228,7 +1333,7 @@ held** (§9.6, §19 K9): the target row is not retired by the region change |
| |---|---| |
| | `releasing` | row `releasing` with `hold_op = rollback id`; `ReconstructStopEvidence` | |
| | `released` | digests after a final checkpoint: database sha256, files plaintext, timers. **Clean** when all three equal what was installed (`landing.installed_db_sha256`, `source.files.plain`, `source.timers_sha256`) or `landing_phase` never reached `probing`; otherwise **dirty**. Write `stopped-target.json`; CAS the claim's execution holder to `none` | |
| -| `returning` (dirty only) | the handoff back: mirror its `instances/<host>` into the source bucket's `moves/<host>/<rollback id>/replica/`, seal and publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json` | |
| +| `returning` (dirty only) | the handoff back: write a snapshot of its stopped database (one level-9 LTX file `[1, N']`, §5.1 step 1) into the source bucket's `moves/<host>/<rollback id>/db`, seal it by `versionId`, publish its files archive and timers snapshot under `files/` and `timers/`, write `move.json` | |
| | `returned` (dirty only) | every artifact published | |
| | `cleaning` | only after the source records `recovered_at` (below): **bucket-park its `instances/<host>/` and its staging `moves/<host>/<move id>/` into `superseded/<move id>/<host>/`**, local-park its database, `<dbPath>.gen`, files and `<host>.env`, delete its row (conditional on `hold_op = rollback id`), clear its timers rows | |
| | `cleaned` | CAS `rollback.target_parked_at` | |
| @@ -1873,6 +1978,75 @@ only behaviour-affecting map iteration. |
| real console cannot see; the release check still omits timers and |
| unreplicated local writes; same-operation workers still share a lease |
| identity; the timing scale is unchanged. |
| + |
| +**Rev 7.5: joint round 4 and claim rev 6.2.** |
| + |
| +- **The database and its replica have LTX semantics (R4-1, |
| + `ltx_test.go`).** A database is a map of keys to values with a lineage |
| + TXID; a transaction inserts a key named by its write, or (every fifth |
| + write) updates the newest live key, or (every fifth but one) deletes |
| + the oldest, so a restore's fidelity depends on final page images, not |
| + on a list of ids. A replica object is an LTX file: a level (0, 1, or 9 |
| + for a snapshot), a transaction range, the final image of every key it |
| + touches (0 is a delete), and the database checksum after `Max`. The |
| + oracle alone knows which acknowledged writes a file covers. The |
| + serving process ships its pending transactions as one level-0 file, |
| + retries the same range widened after a timeout, and compacts three |
| + current level-0 files into one level-1 file before deleting the inputs |
| + (as `ltx.Compactor` and litestream's retention do; the versions stay |
| + noncurrent, which the park's version-exact snapshot still sees). The |
| + sealed transfer and the dirty return are snapshots of the stopped |
| + database. **Restore is litestream's planner** (§5.1 step 4) from the |
| + snapshot `generation.json` names, with the gap refusal and the |
| + checksum check (step 5). The oracle replays the incarnation's |
| + acknowledged transactions in order into the state a restore must equal: |
| + at every release and at the end a cold restore of the live generation |
| + must reach every durable write's TXID and equal that state (INV-2, |
| + cold); the serving box's own database must equal the replay of every |
| + acknowledged write, a write that never reached a database counting as |
| + the insert the application believed it made (INV-2, local). Rev 7.4's |
| + objects carried the full transaction history and could show neither a |
| + compacted continuation nor a gap. |
| +- **Installation stamps (R4-2, claim rev 6.2 §6.4).** Each box keeps |
| + `{active_stamp | none, retired_stamps}` per incarnation. A box's claim |
| + read carries the active stamp at the read; admission compares it with |
| + the active stamp now, so a stale worker's read from before a |
| + retirement is refused. Config-sync and adoption passes record the stamp |
| + they selected under and the host guard admits them only at the active |
| + stamp. A create's installation stamp is the gen that made it serving |
| + here; a landing's is the flip CAS's gen (`op.FlipGen`), set in |
| + `checking` under the guard on a fresh read. Retirement (local park, |
| + quarantine) moves the active stamp into the retired set. The op counter |
| + ordering, the `- 1`, and "an empty serving op means now" are gone. The |
| + oracle records a landing probe refused by its own installation record |
| + (INV-3, the R3-3 fault) and a host-guard write by a pass whose stamp is |
| + not the active one (INV-6). |
| +- **The live set is region-qualified (R4-3, claim rev 6.2 §6.2a).** A |
| + generation's files and marker are live only in the authoritative |
| + region's bucket; `deadGeneration` returns residue for a matching key in |
| + any other region. |
| +- **Retirement under purge (R4-4, claim rev 6.2 §5.3 step 4).** Under |
| + `deleting` and `purging` alike, the record version is recorded in |
| + `op.intent` first (`RecVer`), the record is deleted only if its version |
| + matches, and the CAS to `parking` is legal only from the same kind, |
| + with the record authoritatively gone, and, for a purge, with the purge |
| + journal at `torn-down` or later. A purged host never returns to |
| + `serving`. |
| +- **Orphan cleanup with no claim object** is explicit (claim rev 6.2 |
| + §5.1 step 5, Q2): a record with no claim is a legacy host, adopted |
| + (§9), never an orphan. |
| +- **The random generator (R4 §3).** Three additions, each drawn from the |
| + seed's RNG in half the seeds: a **marker-hold** schedule holds a |
| + `generation.json` publication until a newer marker is current, which |
| + is model 29's interleaving; a **targeted freeze** freezes the landing |
| + target in its probe or settle window and keeps it frozen until the |
| + source runs again, which is model 5's; and a **retention-boundary |
| + fixture** starts a seed with `retired_incarnations` at its cap and a |
| + replication object of an incarnation the list forgot, as a straggler. |
| + Two oracles make a rolled-back move an unaccepted terminal where it |
| + should be: the probe-fence oracle above, and the round-trip witness. |
| + These reshuffle every seed against rev 7.4; the witnesses are the |
| + stable evidence. |
| paginated listings, separate service, wall and monotonic clocks, |
| enrollment and console and updater versions, spawn separate from |
| readiness, and same-operation lease identities. |
| @@ -1974,7 +2148,28 @@ adds and one it makes stricter: |
| app is idle. Writes past the last completed checkpoint are lost by |
| design and declared so; every durable write must come back. |
| -**Rev 7.4, on the final model (claim rev 6, the restore chain, the |
| +**Rev 7.5, on the final model (claim rev 6.2: installation stamps, the |
| +region-qualified live set, retirement under purge; LTX files with |
| +compaction and litestream's restore planner; the marker-hold and |
| +targeted-freeze schedules and the retention fixture): 30,000 seeds, zero |
| +violations; 100,000 seeds, zero violations** (4 m 46 s and 15 m 03 s: |
| +page images and checksums cost about nine times rev 7.4's run time). |
| +Across the 100,000 seeds: 155,367 completed operations, among them 1,851 |
| +completed moves, 1,890 clean and 88 dirty rollbacks, 377 pre-flip |
| +reverts, 315 declared losses, 30,228 pushes, 89,170 delete-park-free |
| +cycles and 1,412 lost disks; 12,568 LTX compactions; 38,599 requests |
| +completed after `H` (the held marker publications among them); 33,549 |
| +staging signatures were refused as stale; 30,730 creates restarted on a |
| +412; 121 targets were stopped mid-return. No restore was refused for a |
| +gap or a checksum mismatch with every rule in place. Rev 7.5's first |
| +baseline run found a model fault the oracle was built for: after a cold |
| +restore the model's replicator kept position 0 and shipped a `[1, TX]` |
| +file carrying only the new pages; the planner preferred it, the checksum |
| +check refused the restore, and the oracle reported the durable writes |
| +lost (2 / 30,000, 5 / 100,000). The restored database now replicates from |
| +the TXID it reached, as litestream's `-txid` sidecar has it. |
| + |
| +**Rev 7.4, on claim rev 6 (the restore chain, the |
| installation-scoped fence, the ordered orphan cleanup, the namespace |
| sweep, public delivery): 30,000 seeds, zero violations; 100,000 seeds, |
| zero violations** (42 s and 100 s). Across the 100,000 seeds: 165,084 |
| @@ -2081,169 +2276,172 @@ Each was a failing seed first, then a rule; each rule's mutation is in |
| #### 14.2.5 Mutation results |
| Every rule was dropped in turn, with the one prebuilt binary of §14.2.1, |
| -on the final rev 7.4 model, with the strict classification, **in two |
| +on the final rev 7.5 model, with the strict classification, **in two |
| ways**: the **random sweep**, 3,000 seeds each, 30,000 for every rule not |
| caught at 3,000, 100,000 for every rule not caught at 30,000, 30,000 for |
| each combination and 100,000 for the rarest; and the rule's **witness |
| scenarios** (§14.2.2, `witness_test.go`) under the same mutation, for the |
| -25 rules that have them. A rule is caught if either catches it; |
| +29 rules that have them. A rule is caught if either catches it; |
| `mutate.sh` reports the two separately, and this section does too. The |
| -model has **71 rules**: rev 7.3's 68 plus `fence-by-installation`, |
| -`orphan-order` and `sweep-namespace` (claim rev 6). No run was an ERROR. |
| -Seed numbers reproduce any sweep line with `HOSTLIFE_SEED`; |
| -`HOSTLIFE_WITNESS=<rule>` replays a witness with its trace. Rev 7.3's |
| -counts are in the rev 7.3 spec (dc7f2a63); the orphan plans reshuffled |
| -the seeds (§14.2.3), so sweep counts moved by a few seeds while every |
| -witness verdict is unchanged. |
| +model has **75 rules**: rev 7.4's 71 plus `fence-stamp` (claim rev 6.2 |
| +§6.4), `live-set-region` (claim rev 6.2 §6.2a), `restore-overlap` and |
| +`restore-gap-closed` (§5.1). No run was an ERROR. Seed numbers reproduce |
| +any sweep line with `HOSTLIFE_SEED`; `HOSTLIFE_WITNESS=<rule>` replays a |
| +witness with its trace. Rev 7.4's counts are in the rev 7.4 spec |
| +(0e41b685); the new schedules and fixture reshuffled every seed, and the |
| +LTX model changed what many mutations break, so sweep counts moved; every |
| +witness verdict is unchanged, and three rules the sweep could not reach |
| +before are caught by it now. |
| | | rules | |
| |---|---| |
| -| caught alone by the sweep at 3,000 seeds | 48 | |
| -| caught alone by the sweep at 30,000, and by their witness | 5 (`lost-quarantine`, `markers-last`, `rollback-journal`, `seal-by-version`, `orphan-order`) | |
| -| caught alone by their witness only; the sweep misses them at 30,000 or 100,000 | 4 (`generation-conditional`, `declare-lost-compute`, `fence-by-installation`, `sweep-namespace`) | |
| -| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 11 | |
| +| caught alone by the sweep at 3,000 seeds | 53 | |
| +| caught alone by the sweep at 30,000, and by their witness | 4 (`fence-by-installation`, `orphan-order`, `rollback-journal`, `staging-quiet`) | |
| +| caught alone by the sweep at 100,000, and by its witness | 1 (`declare-lost-compute`) | |
| +| caught alone by their witness only; the sweep misses them at 30,000 | 2 (`live-set-region`, `restore-gap-closed`) | |
| +| caught only in a stated combination: the witness holds alone and under every proper subset, and violates with the partners | 12 | |
| | liveness only | 2 (`readiness-key`, `config-before-probe`) | |
| | unreachable under claim rev 5 | 1 (`readiness-quiet`) | |
| | unexercised | **0** | |
| +**What the generator changes bought (R4 §3).** `generation-conditional` |
| +was witness-only at 0 / 100,000 in rev 7.4; the marker-hold schedule |
| +makes it 13 / 3,000 and 383 / 100,000. `declare-lost-compute` was |
| +witness-only at 0 / 100,000; the targeted freeze makes it 3 / 100,000. |
| +`sweep-namespace` was witness-only at 0 / 30,000; the retention fixture |
| +makes it 88 / 3,000. `fence-by-installation` was witness-only at 0 / |
| +30,000; the probe-fence oracle makes it 2 / 30,000, because a move back |
| +that rolls back is a violation now, not a converged terminal. Two rules |
| +stay witness-only: `live-set-region` (the sweep's legacy fixture never has |
| +an old regional PUT land after discovery) and `restore-gap-closed` (no |
| +seed loses a replica object with every rule in place). |
| + |
| **The witnesses.** One scenario per rule the sweep catches rarely or only |
| -in combination, and one per rule claim rev 6 or this round added; two |
| -for `registration-check`, one per partner. "Alone" is the witness under |
| -the rule's own mutation; "with partners" under the stated combination. |
| -The gate also runs every proper subset of each combination and requires |
| -the witness to hold there, so a rule a combination names is shown |
| -necessary; each witness violates with the failure it names, not merely |
| -some invariant (R3 review). |
| +in combination, and one per rule a review round added; two for |
| +`registration-check`, one per partner. "Alone" is the witness under the |
| +rule's own mutation; "with partners" under the stated combination. The |
| +gate also runs every proper subset of each combination and requires the |
| +witness to hold there; each witness violates with the failure it names. |
| | rule | the scenario | witness alone | witness with partners | sweep alone | |
| |---|---|---|---|---| |
| -| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 0 / 100,000 | |
| -| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 3 / 3,000, 32 / 30,000, 112 / 100,000 | |
| -| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 100,000 | |
| -| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held: with compute fencing the operator refuses, and the paused box is never declared lost | with `declare-lost-compute`: **violated**, INV-1; a watchdog inside the paused agent never fences | 0 / 100,000; the pair 3 / 100,000 | |
| -| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, a database and files for a host served elsewhere | | 0 / 3,000, 12 / 30,000 | |
| -| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 0 / 3,000, 10 / 30,000 | |
| -| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore; the restart at `claimed` parks the return generation | | 0 / 3,000, 3 / 30,000 | |
| -| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale round | | 0 / 3,000, 15 / 30,000 | |
| -| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 1 / 3,000, 10 / 30,000 | |
| -| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 2 / 3,000, 14 / 30,000 | |
| -| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs; the mutation opened the row at the probe, and the edge routes on the row | **violated**: INV-5, a public request reached the landing target before the commit | | 10 / 3,000, 115 / 30,000 (rev 7.3: never alone) | |
| -| `claim-cas-opid` (C2) | a clean rollback; a second source goroutine reads the claim just before the release and stalls; the host is released, a purge claims it, the goroutine resumes | held: revalidation stops it | with `revalidate-before-effect`: **violated**, the stale release overwrites the purge and the store is torn down under a serving host | 0; the pair 1,006 / 30,000 | |
| -| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | an open from an earlier operation, paused on the source, lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every pair | all three: **violated**, INV-1, the source serves beside the target | 0 each; any pair 0 / 30,000; the triple 7 / 30,000, 19 / 100,000 | |
| -| `start-check` (INV-4) | the same, dropping the whole start check | held, and under every pair | with `exec-admission` and `hold-op-open`: **violated**, INV-1 | the triple 9 / 30,000 | |
| -| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held: the whole-tree cleanup kills the escaped descendant | with `evidence-whole-tree`: **violated**, INV-1 | 0; the pair 128 / 30,000 | |
| -| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held: discovery parked the other region at adoption | with `legacy-discovery`: **violated**, INV-10 after `free` | 0; the pair 9,092 / 30,000 | |
| -| `door-reread` (claim §6.5 O2) | a listing authorized before the delete selects after a recreate into the same location | held: with C3a the new incarnation's location differs | with `location-per-incarnation`: **violated**, a read authorized for inc 1 returns inc 2's data | 0; the pair 36 / 30,000 (8 door violations) | |
| -| `door-by-version` (claim §6.5) | a listing selects and signs before the delete; the file request opens after the recreate | held, as above | with `location-per-incarnation`: **violated**, the same; `door-reread` is not needed | 0; the pair 29 / 30,000 (2 door violations), with `door-reread` too 55 / 30,000 (27) | |
| -| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held: the fence and the ETag condition refuse the CAS, and the 412 restarts the create on a store that exists again | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated**; a host creating on a torn-down store | 0 / 30,000; the pairs 240 and 313 / 30,000 | |
| -| `fence-by-installation` (claim rev 6 §6.4, R3-3) | UK→US, then US→UK: the second landing must replace the marker UK wrote when it retired the first installation; **unmutated, the instance must serve on UK again, running** | **violated**: the move back never serves on UK (the probe is refused, the cut deadline passes, it rolls back); INV-3 at the witness's milestone | | 0 / 30,000: the sweep cannot tell a rolled-back move from a served one | |
| -| `orphan-order` (claim rev 6 §5.1 step 5, R3-2) | a cancelled create's record lands late; the recovery pass starts its cleanup and pauses after its first observation; a create of the next incarnation removes the orphan itself, claims and publishes; the paused cleanup resumes | **violated**: the cleanup, judging the new record by the stale claim, deletes the record of the incarnation the claim names | | 0 / 3,000, 2 / 30,000 | |
| -| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 is accepted and completes after 33 delete-and-recreate cycles, by which time `retired_incarnations` no longer lists 1 | **violated**: INV-10, residue the sweep never finds | | 0 / 30,000: no seed recreates 33 times | |
| -| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty; the source's recovery install must render current inputs | **violated**: `stuck`, the source could not recover | | 51 / 3,000, 506 / 30,000 | |
| +| `generation-conditional` (model 29) | push p1's first `generation.json` PUT is accepted and its response lost; the agent publishes again and p1 completes; push p2 completes; the stale PUT lands | **violated**: the marker names p1, the claim p2, and the serving box cannot start | | 13 / 3,000, 114 / 30,000, 383 / 100,000 | |
| +| `lost-return-park` (model 27) | the target writes in the settle window, the settle check fails, the target is stopped after its first return PUT and declared lost | **violated**: INV-10, the lane in the source region at the release | | 5 / 3,000, 35 / 30,000, 113 / 100,000 | |
| +| `declare-lost-compute` (model 5) | the target is frozen in its settle window and its execution lease expires; the VM resumes once the source has recovered | **violated**: INV-1, two boxes run the host | | 0 / 30,000, 3 / 100,000 | |
| +| `watchdog-independent` (§7.1) | as above, with the agent alone paused, so the application keeps running | held | with `declare-lost-compute`: **violated**, INV-1 | 0 / 100,000; the pair 1 / 30,000, 4 / 100,000 | |
| +| `lost-quarantine` (CC12) | the target is stopped while landing, declared lost, and started again with its old disk | **violated**: INV-10, local state for a host served elsewhere | | 3 / 3,000, 7 / 30,000 | |
| +| `markers-last` (R2-6) | the source has a registered timer; the target's agent crashes between extracting the files and writing the marker | **violated**: INV-2, the timer is lost | | 1 / 3,000, 6 / 30,000 | |
| +| `rollback-journal` (R2-3) | a dirty rollback; the source's agent crashes after its probe spawned the instance, which wrote and replicated into the return generation | **violated**: INV-2 on cold restore | | 0 / 3,000, 8 / 30,000 | |
| +| `seal-by-version` (J-N2) | a pre-cut staging round completes after the seal; the source wrote and replicated between them | **violated**: INV-2 on cold restore; the landing installs the stale snapshot | | 3 / 3,000, 19 / 30,000 | |
| +| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 0 / 3,000, 6 / 30,000 | |
| +| `dirty-return` (INV-2) | the target writes during its probe and is rolled back | **violated**: INV-2, the write is lost | | 8 / 3,000, 58 / 30,000 | |
| +| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 11 / 3,000, 109 / 30,000 | |
| +| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0; the pair 1,365 / 30,000 | |
| +| `exec-admission`, `hold-op-open`, `start-check-claim-gen` (J2-R2-8) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every pair | all three: **violated**, INV-1 | 0 each; any pair 0 / 30,000; the triple 11 / 30,000, 21 / 100,000 | |
| +| `start-check` (INV-4) | the same, dropping the whole start check | held, and under every pair | with `exec-admission` and `hold-op-open`: **violated**, INV-1 | the triple 11 / 30,000 | |
| +| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 0; the pair 828 / 30,000 | |
| +| `touched-incomplete` (J-N5) | a legacy host with a pre-release replica in another region is adopted, then deleted | held | with `legacy-discovery`: **violated**, INV-10 after `free` | 0; the pair 7,407 / 30,000 | |
| +| `door-reread` (claim §6.5 O2) | a listing authorized before the delete selects after a recreate into the same location | held | with `location-per-incarnation`: **violated**, a read authorized for inc 1 returns inc 2's data | 0; the pair 432 / 30,000 (196 door violations) | |
| +| `door-by-version` (claim §6.5) | a listing selects and signs before the delete; the file request opens after the recreate | held | with `location-per-incarnation`: **violated**, the same; `door-reread` is not needed | 0; the pair 385 / 30,000 (60 door violations) | |
| +| `registration-check` (CC21) | the first create of a host registers and its console pauses; a purge of the app drains the expired registration, tears the store down and finishes; the creator resumes | held | with `fence-etag`: **violated**; with `purge-claim-fence`: **violated** | 0 / 30,000; the pairs 271 and 269 / 30,000 | |
| +| `fence-by-installation` (claim rev 6.2 §6.4, R3-3) | UK→US, then US→UK; **unmutated, the instance must serve on UK again, running** | **violated**: the landing probe on UK is refused by the box's own installation record (INV-3) | | 0 / 3,000, 2 / 30,000 | |
| +| `fence-stamp` (claim rev 6.2 §6.4, R4-2) | a config-sync pass selects the row under the first installation and pauses; UK→US→UK; a new bundle is published; the pass takes the guard | held: the host guard's fresh re-validation refuses its stale bundle | with `hostguard`: **violated**, INV-6, a pass of a retired installation wrote host state | 0 / 30,000; the pair 61 / 30,000, which is `hostguard`'s own 61: the sweep does not separate them, the witness does | |
| +| `orphan-order` (claim rev 6 §5.1 step 5, R3-2) | the recovery pass's cleanup pauses after its first observation; a create removes the orphan, claims and publishes; the paused cleanup resumes | **violated**: the record of the incarnation the claim names is deleted | | 0 / 3,000, 2 / 30,000 | |
| +| `sweep-namespace` (claim rev 6 §6.2a, R3-4) | a replication PUT of incarnation 1 completes after 33 recreates dropped it from `retired_incarnations` | **violated**: INV-10, residue the sweep never finds | | 88 / 3,000, 866 / 30,000 (the retention fixture) | |
| +| `live-set-region` (claim rev 6.2 §6.2a, R4-3) | a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after | **violated**: INV-10, residue the US sweep exempts by key alone | | 0 / 30,000 | |
| +| `restore-overlap` (§5.1, R4-1) | a generation's snapshot ends at TXID 11; the only continuation is a compacted file `[10, 15]`; the disk is lost and the host wakes cold | **violated**: INV-2, the wake loses four acknowledged writes (rev 7.4's `min == current + 1` discards the file) | | 27 / 3,000, 186 / 30,000 | |
| +| `restore-gap-closed` (§5.1, R4-1) | the same generation with `[12, 12]` missing and `[13, 13]` current | **violated**: a restore across the gap returns a database at TXID 11 | | 0 / 30,000 | |
| +| `recovery-current-inputs` (§7.7, §7.8; R2-5) | a bundle is published after admission; the target writes; the rollback is dirty | **violated**: `stuck` | | 47 / 3,000, 488 / 30,000 | |
| **The purge fence, the ETag condition and C5a.** `purge-claim-fence` |
| -(CC21) is caught alone by the sweep: 26 / 3,000, 266 / 30,000. |
| -`fence-etag` (CC22): 18 / 3,000, 195 / 30,000. `claim-never-deleted` |
| -(C5a): 8 / 3,000, 77 / 30,000 (54 of the 77 on the main host while |
| -`creating`, 23 on the second host). `registration-check`, the creator's |
| -re-read, is not caught alone by the sweep at 3,000 or 30,000 seeds, and |
| -its witness holds alone: with the fence and the ETag condition in place a |
| -drained registration always means a changed claim ETag, so the CAS fails |
| -whether or not the creator re-reads. The re-read alone, which is what |
| -rev 7's CC21 asked for, is shown insufficient in the combination table |
| -(`purge-claim-fence` + `fence-etag`, 307 / 30,000). |
| +(CC21) is caught alone by the sweep: 29 / 3,000, 240 / 30,000. |
| +`fence-etag` (CC22): 24 / 3,000, 223 / 30,000. `claim-never-deleted` |
| +(C5a): 5 / 3,000, 46 / 30,000. `registration-check` is not caught alone |
| +by the sweep at 3,000 or 30,000 seeds, and its witness holds alone; the |
| +re-read alone is shown insufficient (`purge-claim-fence` + `fence-etag`, |
| +331 / 30,000). |
| **Rev 6's unexercised three, now caught (the biased schedule, §14.2.2).** |
| | rule | result | what the model finds | |
| |---|---|---| |
| -| `location-per-incarnation` (claim C3a) | **caught alone**: 3 / 3,000, 29 / 30,000 | an incarnation's database holds writes of the previous incarnation: a replication PUT accepted before the delete completes after the recreate into the shared location, and the new incarnation's restore replays it; the cold-restore check at a later release and the start check both see it. With the restore chain (R3-1) the same PUT can also make the chain refuse a conflicting history: the sweep reports it as `stuck` | |
| -| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 36 / 30,000, of which 8 are door violations; witness violated | a listing authorized for the old incarnation selects, after the recreate, the new incarnation's object in the shared location, and signs it | |
| -| `door-by-version` (claim §6.5) | with `location-per-incarnation`: 29 / 30,000, of which 2 are door violations, and with `door-reread` as well 55 / 30,000 (27); witness violated with C3a alone | a handle signed before the delete opens the location's current object after the recreate | |
| +| `location-per-incarnation` (claim C3a) | **caught alone**: 31 / 3,000, 385 / 30,000 | with the shared location, the planner takes the previous incarnation's files (highest `MaxTXID` wins), and the cold restore equals neither incarnation's acknowledged writes; the C3a and door oracles see the rest | |
| +| `door-reread` (claim §6.5 O2) | with `location-per-incarnation`: 432 / 30,000, of which 196 are door violations; witness violated | a listing authorized for the old incarnation selects the new incarnation's object | |
| +| `door-by-version` (claim §6.5) | with `location-per-incarnation`: 385 / 30,000, of which 60 are door violations; witness violated with C3a alone | a handle signed before the delete opens the key's current object after the recreate | |
| -Neither door rule can be violated while C3a holds, under any schedule: a |
| -listing selects only under O1's location, and no later incarnation ever |
| -writes there. They are defence in depth behind C3a, and each is shown |
| -load-bearing once C3a is dropped, by its witness and by the sweep. |
| +The three-rule combination `door-by-version` + `door-reread` + |
| +`location-per-incarnation` that rev 7.4 also reported is **not a minimal |
| +combination** (R4 §3): each door rule's two-rule pair with C3a already |
| +fails, so the three-rule row is a wider set and inherits no claim that its |
| +proper subsets hold. It is no longer run. |
| -**Caught alone: 57 of 71** (48 by the sweep at 3,000; 5 by the sweep at |
| -30,000 and by their witness, marked †; 4 by their witness alone, marked |
| -‡, with the sweep's count beside). |
| +**Caught alone: 60 of 75** (53 by the sweep at 3,000; 4 by the sweep at |
| +30,000 and by their witness, marked †; 1 at 100,000 and by its witness, |
| +marked ††; 2 by their witness alone, marked ‡). |
| | rule | seeds failing | | rule | seeds failing | |
| |---|---|---|---|---| |
| -| `recovery-pass` | 2,501 / 3,000 | | `fresh-incarnation` | 41 / 3,000 | |
| -| `legacy-discovery` | 569 / 3,000 | | `location-per-incarnation` | 3 / 3,000 | |
| -| `park-by-version` | 2,063 / 3,000 | | `park-all-versions` | 677 / 3,000 | |
| -| `park-skip-lock` | 2,869 / 3,000 | | `retirement-ids` | 283 / 3,000 | |
| -| `quiet-before-ack` | 184 / 3,000 | | `straggler-sweep` | 133 / 3,000 | |
| -| `sweep-staging` | 42 / 3,000 | | `restore-by-generation` | 2 / 3,000 | |
| -| `hostguard` | 5 / 3,000 | | `purge-reserve-first` | 2,279 / 3,000 | |
| -| `purge-adopts` | 10 / 3,000 | | `purge-journal` | 1,969 / 3,000 | |
| -| `admission-registration` | 36 / 3,000 | | `registration-recovery` | 1,957 / 3,000 | |
| -| `purge-claim-fence` | 26 / 3,000 | | `fence-etag` | 18 / 3,000 | |
| -| `claim-never-deleted` | 8 / 3,000 | | `cancelled-creates` | 373 / 3,000 | |
| -| `orphan-no-deadline` | 60 / 3,000 | | `orphan-order` † | 2 / 30,000 | |
| -| `evidence-whole-tree` | 2 / 3,000 | | `evidence-from-state` | 2,778 / 3,000 | |
| -| `floor-boot-recovery` | 2,538 / 3,000 | | `participant-rows` | 4 / 3,000 | |
| -| `revalidate-before-effect` | 18 / 3,000 | | `sign-before-safeuntil` | 14 / 3,000 | |
| -| `sign-at-check` | 11 / 3,000 | | `sdk-no-resign` | 11 / 3,000 | |
| -| `lost-quarantine` † | 12 / 30,000 | | `cut-deadline` | 10 / 3,000 | |
| -| `revert-journal` | 17 / 3,000 | | `rollback-journal` † | 3 / 30,000 | |
| -| `dirty-return` | 2 / 3,000 | | `commit-before-open` | 10 / 3,000 | |
| -| `lost-return-park` | 3 / 3,000 | | `target-park` | 42 / 3,000 | |
| -| `abort-target-owner` | 1,061 / 3,000 | | `timer-freeze` | 6 / 3,000 | |
| -| `timer-canonical` | 3 / 3,000 | | `markers-last` † | 10 / 30,000 | |
| -| `source-readiness` | 7 / 3,000 | | `seal-by-version` † | 15 / 30,000 | |
| -| `staging-quiet` | 1 / 3,000 | | `fresh-admission` | 16 / 3,000 | |
| -| `stale-hold-release` | 2 / 3,000 | | `obligations-block-ops` | 22 / 3,000 | |
| -| `claim-op-exclusive` | 157 / 3,000 | | `recovery-current-inputs` | 51 / 3,000 | |
| -| `files-carried` | 79 / 3,000 | | `generation-conditional` ‡ | witness; sweep 0 / 100,000 | |
| -| `declare-lost-compute` ‡ | witness; sweep 0 / 100,000 | | `fence-by-installation` ‡ | witness; sweep 0 / 30,000 | |
| -| `sweep-namespace` ‡ | witness; sweep 0 / 30,000 | | | | |
| - |
| -`fence-by-installation` and `sweep-namespace` are liveness and |
| -long-horizon properties the sweep cannot reach: a rolled-back move back |
| -converges like a served one, and no seed recreates a host 33 times. Their |
| -witnesses are the evidence, and the first is also the unmutated |
| -round-trip test claim rev 6 asks for. |
| - |
| -**Caught only in a combination: 11 rules.** Each partner's own count, on |
| +| `recovery-pass` | 2,465 / 3,000 | | `fresh-incarnation` | 52 / 3,000 | |
| +| `legacy-discovery` | 384 / 3,000 | | `location-per-incarnation` | 31 / 3,000 | |
| +| `park-by-version` | 2,522 / 3,000 | | `park-all-versions` | 574 / 3,000 | |
| +| `park-skip-lock` | 2,721 / 3,000 | | `retirement-ids` | 333 / 3,000 | |
| +| `quiet-before-ack` | 211 / 3,000 | | `straggler-sweep` | 781 / 3,000 | |
| +| `sweep-staging` | 51 / 3,000 | | `sweep-namespace` | 88 / 3,000 | |
| +| `restore-by-generation` | 189 / 3,000 | | `restore-overlap` | 27 / 3,000 | |
| +| `restore-gap-closed` ‡ | witness; sweep 0 / 30,000 | | `hostguard` | 9 / 3,000 | |
| +| `purge-reserve-first` | 2,167 / 3,000 | | `purge-adopts` | 7 / 3,000 | |
| +| `purge-journal` | 1,883 / 3,000 | | `admission-registration` | 40 / 3,000 | |
| +| `registration-recovery` | 2,117 / 3,000 | | `purge-claim-fence` | 29 / 3,000 | |
| +| `fence-etag` | 24 / 3,000 | | `claim-never-deleted` | 5 / 3,000 | |
| +| `cancelled-creates` | 374 / 3,000 | | `orphan-no-deadline` | 50 / 3,000 | |
| +| `orphan-order` † | 2 / 30,000 | | `evidence-whole-tree` | 67 / 3,000 | |
| +| `evidence-from-state` | 2,614 / 3,000 | | `floor-boot-recovery` | 2,519 / 3,000 | |
| +| `participant-rows` | 3 / 3,000 | | `revalidate-before-effect` | 78 / 3,000 | |
| +| `sign-before-safeuntil` | 20 / 3,000 | | `sign-at-check` | 14 / 3,000 | |
| +| `sdk-no-resign` | 14 / 3,000 | | `lost-quarantine` | 3 / 3,000 | |
| +| `declare-lost-compute` †† | 3 / 100,000 | | `cut-deadline` | 13 / 3,000 | |
| +| `revert-journal` | 13 / 3,000 | | `rollback-journal` † | 8 / 30,000 | |
| +| `dirty-return` | 8 / 3,000 | | `commit-before-open` | 11 / 3,000 | |
| +| `lost-return-park` | 5 / 3,000 | | `target-park` | 52 / 3,000 | |
| +| `abort-target-owner` | 940 / 3,000 | | `timer-freeze` | 4 / 3,000 | |
| +| `timer-canonical` | 7 / 3,000 | | `markers-last` | 1 / 3,000 | |
| +| `source-readiness` | 11 / 3,000 | | `seal-by-version` | 3 / 3,000 | |
| +| `staging-quiet` † | 6 / 30,000 | | `fresh-admission` | 16 / 3,000 | |
| +| `stale-hold-release` | 5 / 3,000 | | `obligations-block-ops` | 20 / 3,000 | |
| +| `claim-op-exclusive` | 79 / 3,000 | | `recovery-current-inputs` | 47 / 3,000 | |
| +| `files-carried` | 77 / 3,000 | | `generation-conditional` | 13 / 3,000 | |
| +| `fence-by-installation` † | 2 / 30,000 | | `live-set-region` ‡ | witness; sweep 0 / 30,000 | |
| + |
| +**Caught only in a combination: 12 rules.** Each partner's own count, on |
| the same seeds, shows what the combination adds; the witness column is |
| -the rule's witness under the combination, having held under every |
| -proper subset in the gate. |
| +the rule's witness under the combination, having held under every proper |
| +subset in the gate. |
| | combination | sweep | partners alone (sweep) | witness | what the model finds | |
| |---|---|---|---|---| |
| -| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 307 / 30,000 | `purge-claim-fence` 266, `fence-etag` 195, `registration-check` 0 | (the two `registration-check` rows below) | the creator pauses after its re-read; purge drains, tears down and finishes; the CAS from free succeeds: a store destroyed under a creating or serving host. The re-read is not a fence | |
| -| `registration-check` + `purge-claim-fence` | 313 / 30,000 | `purge-claim-fence` 266 | violated | the same, without the re-read's early stops | |
| -| `registration-check` + `fence-etag` | 240 / 30,000 | `fence-etag` 195 | violated | the same: the fence alone cannot refuse a creator that resumes after its release | |
| -| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 19 / 100,000 (7 / 30,000) | every pair 0 / 30,000 | violated | two writers, Astra's J2-R2-8 trace (rev 6) | |
| -| `exec-admission` + `hold-op-open` + `start-check` | 9 / 30,000 | (above) | violated | the same, dropping the whole start check | |
| -| `door-reread` + `location-per-incarnation` | 36 / 30,000 | `location-per-incarnation` 29 | violated | door reads of another incarnation's data (8) | |
| -| `door-by-version` + `location-per-incarnation` | 29 / 30,000 | `location-per-incarnation` 29 | violated | door reads of another incarnation's data (2): the sweep rarely stalls a signed handle across a recreate; the witness does it every time | |
| -| `door-by-version` + `door-reread` + `location-per-incarnation` | 55 / 30,000 | `door-reread` + `location` 36 | violated | more door violations (27 against 8) | |
| -| `claim-cas-opid` + `revalidate-before-effect` | 1,006 / 30,000 | `revalidate-before-effect` 197 | violated | a stale purge step destroys a store; the witness's stale release overwrites a purge | |
| -| `strict-spawn` + `evidence-whole-tree` | 128 / 30,000 | `evidence-whole-tree` 11 | violated | two writers | |
| -| `touched-incomplete` + `legacy-discovery` | 9,092 / 30,000 | `legacy-discovery` 6,037 | violated | a freed host's residue | |
| -| `declare-lost-compute` + `watchdog-independent` | 3 / 100,000 | `declare-lost-compute` 0 / 100,000 (its witness alone: violated), `watchdog-independent` 0 / 100,000 | violated | two writers after a paused or frozen target resumes | |
| - |
| -`commit-before-open` + `dirty-return` (124 / 30,000) is no longer a |
| -combination the model needs: `commit-before-open` is caught alone by |
| -INV-5 (115 / 30,000 and its witness), and the pair's extra seeds are |
| -`dirty-return`'s. |
| +| `purge-claim-fence` + `fence-etag` (**the re-read alone**, rev 7's CC21 as proposed) | 331 / 30,000 | `purge-claim-fence` 240, `fence-etag` 223, `registration-check` 0 | (the two `registration-check` rows below) | a store destroyed under a creating or serving host | |
| +| `registration-check` + `purge-claim-fence` | 269 / 30,000 | `purge-claim-fence` 240 | violated | the same | |
| +| `registration-check` + `fence-etag` | 271 / 30,000 | `fence-etag` 223 | violated | the same | |
| +| `exec-admission` + `hold-op-open` + `start-check-claim-gen` | 21 / 100,000 (11 / 30,000) | every pair 0 / 30,000 | violated | two writers, Astra's J2-R2-8 trace | |
| +| `exec-admission` + `hold-op-open` + `start-check` | 11 / 30,000 | (above) | violated | the same, dropping the whole start check | |
| +| `door-reread` + `location-per-incarnation` | 432 / 30,000 | `location-per-incarnation` 385 | violated | door reads of another incarnation's data (196) | |
| +| `door-by-version` + `location-per-incarnation` | 385 / 30,000 | `location-per-incarnation` 385 | violated | door reads of another incarnation's data (60); the sweep count is the partner's, the witness is the evidence | |
| +| `claim-cas-opid` + `revalidate-before-effect` | 1,365 / 30,000 | `revalidate-before-effect` 610 | violated | a stale step destroys a store | |
| +| `strict-spawn` + `evidence-whole-tree` | 828 / 30,000 | `evidence-whole-tree` 504 | violated | two writers | |
| +| `touched-incomplete` + `legacy-discovery` | 7,407 / 30,000 | `legacy-discovery` 3,814 | violated | a freed host's residue | |
| +| `declare-lost-compute` + `watchdog-independent` | 1 / 30,000, 4 / 100,000 | `declare-lost-compute` 3 / 100,000, `watchdog-independent` 0 / 100,000 | violated | two writers after a paused or frozen target resumes | |
| +| `fence-stamp` + `hostguard` | 61 / 30,000 | `hostguard` 61, `fence-stamp` 0 | violated | a stale pass writes host state for a retired installation (INV-6); in the sweep every seed is `hostguard`'s, and the witness is what shows the stamp load-bearing | |
| **Liveness only: 2.** `readiness-key` (T2) and `config-before-probe`. |
| They have no witness: neither can violate an invariant. |
| **Unreachable: `readiness-quiet` (T12).** Every retirement acknowledges |
| -only after its own horizon, and CC11 holds; the biased schedules do not |
| -change that, because they delay only data writes, never an |
| -acknowledgement. No witness: there is no interleaving to force. |
| +only after its own horizon, and CC11 holds. No witness: there is no |
| +interleaving to force. |
| **Seeds:** 300 in the gate, with every witness under every subset (about |
| a second); the 30,000- and 100,000-seed baselines, this sweep and the |
| -witnesses are the evidence for rev 7.4. |
| +witnesses are the evidence for rev 7.5. |
| #### 14.2.6 What the model does not prove |
| @@ -2267,22 +2465,24 @@ witnesses are the evidence for rev 7.4. |
| 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). |
| -- **Restore fidelity (R3-1).** The model's transactions are append-only |
| - ids; a history is an ordered list, and a conflict is a history that is |
| - neither an extension nor a prefix of the chain. Updates, deletes and |
| - the content of a transaction are not modelled, so the chain proves |
| - that no two histories are ever merged and that every durable write |
| - stays reachable, which is what the proofs use; it does not validate |
| - litestream's LTX planning against updates and deletes. That is |
| - implementation work against the real restore (§5.1, §15 step 8). |
| -- **Observation boundaries not taken in rev 7.4** (R3 review): the |
| - target's cleanup is queued at its release, not after the source's |
| +- **Restore fidelity (R3-1, R4-1).** The model's LTX files have ranges, |
| + final page images, checksums and compaction, and its restore is |
| + litestream's planner (§5.1), so a compacted continuation, a gap and a |
| + stale image are all representable and each has a witness. What the |
| + model's pages are not is bytes: a key's image is one integer, a |
| + checksum is a digest of the whole state, and page size, WAL salts and |
| + the lock page are absent. The claim it supports is that the planner as |
| + specified restores exactly the acknowledged transactions up to the |
| + TXID it reaches and refuses otherwise; byte-level LTX decoding is |
| + validated against the real restore (§15 step 8). |
| +- **Observation boundaries not taken in rev 7.4 or 7.5** (R3 review): |
| + the target's cleanup is queued at its release, not after the source's |
| `recovered_at` (§7.8); a create refuses while a record PUT is pending |
| on the server, which a real console cannot see; the release check runs |
| the cold-restore oracle only, not the local and timer acknowledgement |
| check, so a later delete could erase evidence of an earlier loss; two |
| - workers of one operation share a lease identity; the local-exclusion |
| - passes carry an operation sequence now but no release version. |
| + workers of one operation share a lease identity; the passes carry an |
| + installation stamp now but no release version. |
| - **Adversarial scheduling is partial.** Paused opens, door reads, |
| staging signers and an earlier incarnation's replica writes wake at the |
| worst moment the model knows of; everything else wakes at random. The |
| @@ -2531,13 +2731,27 @@ model encodes that text (§14.2.2) and gives C5a its own mutation |
| spec.** Rev 6 answers R3-2 (orphan cleanup in a fixed order: record, then |
| the claim fresh, then `DeleteIfMatch`), R3-3 (the installation-scoped |
| retired marker) and R3-4 (the sweep discovers locations from the |
| -namespace; `retired_incarnations` is anti-reuse only). Rev 7.4 encodes |
| -all three (§6.4, §14.2.2) and asks platform-1e three questions, in |
| -`moves-claim-questions.md`: how operations are ordered for "at or |
| -before" in production (the model uses its op counter); whether §5.1 step |
| -5 presupposes a claim object exists (a record with no claim is a legacy |
| -host to adopt, §9); and which spec owns the statement that a sweep never |
| -touches the version `generation.json` names. |
| +namespace; `retired_incarnations` is anti-reuse only). Rev 7.4 encoded |
| +all three and asked platform-1e three questions. |
| + |
| +**Claim rev 6.2 (30d572c4), after joint round 4: no request from this |
| +spec.** Rev 6.1 (79a5243c) answered the three questions: operations are |
| +ordered by claim `gen`, op ids opaque; a record with no claim object is a |
| +legacy host, never an orphan; the claim owns the sweep-side rule for the |
| +live set and this spec owns generation-specific live-object selection. |
| +Rev 6.2 then took joint round 4's claim side: **installation stamps** |
| +(§6.4 there: the stamp is the claim `gen` captured at the CAS that made |
| +the installation current, a writer is admitted only at the active stamp, |
| +retirement sets `none`, a reinstall sets its own stamp under the guard), |
| +the **region-qualified live set** (§6.2a there: `{authoritative region, |
| +holder.location, holder.generation}` plus the versions this spec supplies, |
| +protected in the authoritative region only; the authoritative region is |
| +`op.exec`'s while serving, or what this spec's phase table names, §5.1), |
| +and **retirement under purge** (§5.3 step 4 there: the record version in |
| +`op.intent`, `DeleteIfMatch`, `purging → parking` only with the record |
| +gone and the journal at `torn-down`; a purged host never returns to |
| +`serving`). Rev 7.5 encodes all of it (§5.1, §6.4, §14.2.2) and raises no |
| +new claim question (`moves-claim-questions.md`, rev 7.5 heading). |
| **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 |
| @@ -2794,3 +3008,22 @@ Astra's verdicts were "not ready" for all three artifacts. Claim rev 6 |
| | witnesses accept any violation; `reach` turns a missed milestone into INV-3; subsets not run | every witness names its failure and must violate with it; a missed milestone is INV-3 only where the milestone is the property (the round trip); the gate runs every proper subset of each combination and requires the witness to hold there (§14.2.1) | |
| | `commit-before-open` wrongly among "caught" | it now has its own violation (INV-5) and witness; the pair is retired | |
| | model fidelity: restore, admission, cross-object atomicity, local exclusion, same-operation workers, oracle, late creates, cleanup ordering, timing | restore and public admission taken (above); passes carry an operation sequence (R2-3, partly); the rest is listed as not taken in §14.2.6, each with what it hides | |
| + |
| +### 22.11 Joint round 4 (claim 3ea3f90c, moves rev 7.4 0e41b685, model 0e41b685) |
| + |
| +Astra's verdicts were "not ready" for all three artifacts, on narrower |
| +grounds: the production fence contract, executable restore semantics, and |
| +two lifecycle transitions. Claim rev 6.1 (79a5243c) answered the moves |
| +session's three questions; claim rev 6.2 (30d572c4) took R4-2, the claim |
| +half of R4-3, and R4-4. Rev 7.5 answers the moves side and encodes rev 6.2. |
| + |
| +| finding | rev 7.5 | |
| +|---|---| |
| +| R4-1 (P1) the restore can discard a valid compacted continuation; "compare content at those TXIDs" is undefined for compacted objects | one implementable contract (§5.1): the sealed transfer is a verified final snapshot, `generation.json` names it by key, version, TXID and checksum, the restore is litestream v0.5.14's planner from that snapshot (overlap allowed, highest max first), and it fails closed on a missing snapshot, a gap or a checksum mismatch; the content comparison is gone; §7.6's `copying` produces the snapshot the restore consumes; §7.8's return is a snapshot too. The model's LTX files have ranges, page images, checksums and compaction, with updates and deletes; two witnesses: a compacted `[10,15]` over a snapshot at 11 restores through 15 (rev 7.4's rule discards it and loses four writes), and a genuine gap refuses (§14.2.5) | |
| +| R4-2 (P2) the replacement fence rejects its own installation if read literally; the op counter and "empty op means now" have no production contract | claim rev 6.2's installation stamps, encoded exactly (§6.4, §14.2.2): the active stamp is the claim gen captured at the installing CAS, writers are admitted only at equality, retirement sets none, a reinstall sets its own stamp on a fresh read; `- 1` and the counter are gone, op ids are opaque; a stale config pass across UK→US→UK is the new witness (`fence-stamp`), admitted only when the stamp check and the host guard's fresh check are both gone; the probe-fence oracle makes a fenced landing a violation in the sweep too | |
| +| R4-3 (P2) the sweep exempts the current generation in the wrong region | the live set is `{authoritative region, location, generation}` plus the versions this spec names, protected in the authoritative region only; the phase table names the authoritative region for every claim state (§5.1); claim §6.2a is cited for the sweep-side rule; `deadGeneration` checks the region for every key; witness: an old US replication PUT for a legacy host serving in UK (`live-set-region`) | |
| +| R4-4 (P2) purge invokes a retirement whose entry condition it invalidated | claim rev 6.2 §5.3 step 4, encoded: `deleteSteps` records the record version in `op.intent`, deletes conditionally, and moves `purging → parking` only with the record gone and the journal at `torn-down`; a purged host never returns to `serving` (§14.2.2) | |
| +| Q2: orphan cleanup with no claim | the branch is explicit in the model and in §19.4: a record with no claim object is a legacy host, never an orphan (claim rev 6.2 §5.1 step 5) | |
| +| §3: the random generator lacks marker and freeze schedules, a successful-move assertion and a retention fixture | all four added (§14.2.2): the marker-hold and targeted-freeze schedules, the retention-boundary fixture, and two oracles that refuse a rolled-back move as a terminal where it should have served; `generation-conditional`, `sweep-namespace` and `restore-overlap` are caught by the sweep alone now (§14.2.5) | |
| +| §3: the three-rule door combination is not minimal | the results table says so: `door-by-version` + `location-per-incarnation` is the minimal pair and the three-rule row is reported as a wider combination whose two-rule subsets already fail (§14.2.5) | |
| +| §3: ids-only restoration is a fidelity gap | closed with R4-1: transactions update and delete, and the oracle compares states, not id sets (§14.2.6 says what a page is not) | |