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

Date: 2026-10-06 Revision: 7.24.

• Rev 7.24 lets a move target the home region (moves into home, part 2; plan docs/superpowers/plans/2026-10-15-moves-home-region-part2.md, amadan #236). Phase 1 moves between two non-fleet placements, into home only with host claims on (§2). §7.1 refuses a target of home on a console without host claims, or a home whose box sets a region code of its own. §16 F2 records home as a target as delivered by that plan. Paul's rulings of 2026-10-15, decided: R1, home targets only under host claims; R3, --to takes the home's configured name, with no home keyword, and carlos move back stays a follow-on; R5, no protocol version bump (a home box without the new T3 fails T3 and waits, fail closed; boxes roll before consoles); R7, a home target may be the console's own box (the records and the claim are durable, so a box lost mid-landing delays recovery and loses nothing). R2(a) and R6 bind the rehearsal runbook, not this spec.
• Rev 7.23 records Paul's ruling M4 (2026-10-10, moves Plan 5 delta pre-flight after claim Plan 10): every close is record first, then the claim's release. Rev 7.22 released the claim to serving first and cleared move second (§7.5, §19 K8). Claim Plan 10's move-recovery grant closes the record first, and a serving claim with a live move record can never acquire that grant, so the two orders could not both stand. Each close (the commit's, a rollback's, a revert's, an abort's) now checks that no obligation of the op remains, CAS-clears move into last_move, and then releases. A crash between the halves leaves the record at rest and the claim still under the op with nothing owed; the box passes are driven by records with a live move and do not come back, so the console's recovery pass releases from last_move. Amended: §7.5, §7.8 finalization, §7.9 step 5, §7.11, the reverting table's opened row, §14.2.2's model row and §19 K8. The model (internal/sim/hostlife, moves Plan 5 Task 7 fix round 1) closes the same way: a box's close CASes the record (last_move), and on every third step stops before the release; the recovery pass releases from last_move (fixRecord). A new invariant, K8, fails any move's release whose record still carries the move, and a new rule, record-first-close, whose mutation is rev 7.22's claim-first close, is caught by it (1,060 / 3,000 seeds, first seed 1; no witness). The 3,000-seed sweep of every rule otherwise matches its expected outcomes. The claim-cas-opid witness is restaged: its stalled goroutine is now the source between the record's close and its release (§14.2.5).
• Rev 7.22 answers joint round 19 (CODEX-FINDINGS-JOINT-R19.md, "R19-1", the round's one finding, P2) and fixes the install manifest's keys. R19-1: rev 7.21 bound the prepared files manifest to "the holder location and generation" during local, but holder.generation still names the source's pre-move generation S until the probe's admission (§7.14, §9.4), and claim rev 6.30 binds the manifest to the prepared generation P; a manifest bound to S could never be P's baseline and an ordinary cold landing would block. §7.6 now binds the manifest, and places it, under the installation's prepared destination generation: g-<move id> for a forward landing, the prepared return generation g-<rollback id> for a dirty rollback; holder.generation is unchanged until admission. Plan 2 Task 10's local step matches. install.json keys: §7.6 names the snakecase keys claim Plan 6's `installcontract.go tags the shared moves.InstallManifest with (snapshot_txid for the Go field N`). The model encodes no manifest binding (§14.2.6); no rule changed, gate only.

• Rev 7.21 answers joint round 18 (CODEX-FINDINGS-JOINT-R18.md, cited "R18-n"; not clean: one P2, three P3s, no P1). R18-1 (P2): the first files manifest of an installation is not the session-bound publisher's, since no target session exists until probing; §7.6 now has the landing build the initial immutable files objects and a create-only prepared manifest, mirroring claim rev 6.30 (73b1b9dc) exactly: published by op.exec before any session exists, in a phase that permits installation; bound to {location, generation, op id, installation stamp}, naming exact versions, at sequence 0, never replaced, retired with its generation; the session-bound publisher starts only after the first admission, takes that manifest by exact version as its baseline and publishes from sequence 1 (region HA spec 1 §5.8's prepared-manifest build, :809, is the same rule). R18-2 (P3): §7.10's "before the flip" is stated as "the record has not entered landing", the flip's record CAS, distinct from the final commit. R18-4 (P3): M-C22 no longer promises that nothing is lost; it describes the retained remote data, the pending recovery and the declaration a restart may make (§20). R18-3 is the claim's (§11 there). The model encodes no publication timing beyond installing the files at the installation CAS, which is the prepared manifest's moment (§14.2.6); no rule changed and no sweep was run.
• Rev 7.20 aligns with claim rev 6.28 (4ffe8a0d), which adopts region HA's L1 to L20 at its sections (CODEX-ANALYSIS-REGION-HA-L1-L20.md beside it). The fence reference (§7.10, moves C7): every transition that relies on a termination fence writes op.journal["fence.<box>"] = {"enrollment","key","sha256"}; a loss.<id> intent cites the same reference; ReturnToSource accepts a fence only through it, re-verifying the record; an automatic declaration needs no quarantine revision and no operator (L4). A source terminated before the flip (§7.10): the fence converts the moving op to relocating in one CAS (exec "none", stamp and generation preserved, relocating at pinning in the source region, every obligation untouched, the lane's park-replica queued when not yet owed); in a one-box region it holds at pinning, safe but not recovered, until region HA enrolls a replacement box; the operator sees waiting for a box in <region> and one alert; after the flip the conversion is refused. This replaces rev 7.19's "the move aborts". L13 (§7.6, §8.3): the files manifest is claim C3's, §6.2a's and P6-D3's: the session-bound publisher, origin-qualified manifest references, files reachability independent of the database baseline. Scope ruling: Phase 1 is for one-box regions; a move into or out of a region with more than one eligible box is refused at the door with new copy (M-C21, pending Paul) until region HA's own model and plan cover multi-box; the model stays one box per region (§14.2.6). The model gains rule fence-converts-moving and witness wFenceConvertsMoving (§14.2.5).
• Rev 7.19 records Paul's rulings of 2026-10-06 on amadan #236 as claim rev 6.27 (989ee349) §1.1 states them, and folds in region HA's requests L14 to L17 (spec 1 rev 5.4, branch design-region-ha-rev5, 2026-10-04-region-ha-box-placement-design.md §9). New §0.5. P7, cold-only admissions: until a reviewed Litestream fix (#234) makes a clean-close certificate safe, every admission is cold, no certificate is issued, and nothing in Phase 1 depends on warm; §5.1 step 9's warm mode stays as specified future behaviour. L14 (§7.10): a target terminated mid-move is taken off the move by the termination fence, as M16's evidence, automatically, under the before-commit rules. L15 (§7.1, §7.3, §19.1): a move names its target box in the start CAS, chosen by region HA's choose(); readiness, evidence, install and recovery bind to it. L16 (§5.1, §7.6): the install is one shared routine with relocation, fed by a sealed staged replica or a pinned set of remote versions. L17 (§6.1, §8, §9.4): every installation writes a files manifest in its new generation; the archive at the cut stays; timer freezing and draining apply to relocating holds. L18 (§14.2.6): the model stays at one box per region plus replacements; the two-box extension is stated as a limit, not done here. Nothing in the protocol of rev 7.18 changes otherwise. Conflicts and claim changes these raise are listed in region-ha-conflicts.md (the coordinator's record) for platform-1e.
• Rev 7.18 folds in joint round 17's two P3s (CODEX-FINDINGS-JOINT-R17.md, cited "R17-n"); the round was clean, A, B and C ready for moves Phase 1 implementation planning, after seventeen rounds. Claim rev 6.26 (98b45332) fixes R17-2 on its side; the code is main at 67547f5. R17-1: the model's INV-23 now checks scope membership for every reference a scoped park archives or deletes, in the manifest it builds and in a persisted manifest it replays, whatever rules are on; an out-of-scope reference is a violation and is never acted on (rev 7.17 checked candidate keys, and only with the confinement rule off); the operations' own parks run under a scope of holder.location; TestForeignManifestReplayRefused replays a manifest naming another incarnation's key under a valid scope. R17-2: the scope grammar's moves/<host> form is used by a delete's park of the staging namespace (§5.2) and by an at-rest sweep, each while no operation stages there, as claim rev 6.26 says. No rule change (107 rules; 73 witnesses): the gate alone, per §14.2.1; the mutation tables stand at rev 7.17's.

• Rev 7.17 answers joint round 16 (CODEX-FINDINGS-JOINT-R16.md, cited "R16-n") and is written against claim spec rev 6.24 (0b821896: the legacy identity, scope namespaces, the narrowed born-covered) and rev 6.25 (413b12cb, which answers this revision's four notes: §5.2 now has a delete park only holder.location plus moves/<host>, never the whole host prefix, as the model does); the code the model aligns with is main at 67547f5, which carries platform-1e's R16-1 and R16-3 fixes (c7e595b, "park, hostclaim: scopes stay in their own namespace; the legacy session-0 loss identity") and the first-admission fix (a created incarnation's first admission declares nothing; note 2 was an E bug); §22.23 has every disposition. A park executes strictly within its scope (R16-2): the model's sweep groups residue by the location it belongs to, an incarnation's own, the legacy instances/<host> (never a child incarnation) or moves/<host>, and queues one chore per location with that scope and its archive incarnation; the archive names the incarnation; every scoped chore's listing is confined to its scope and INV-23 checks every key a chore would archive for membership, not only the location's syntax; the delete parks the deleted incarnation's own location and the staging namespace, never the whole host prefix. The legacy identity is session 0 (R16-3): an adopted host's pre-claim writer is {session: 0, generation: "" (@root), box: holder.writer_box}, valid in both writes_lost and additional_writes_lost; every other declaration has a session above 0, and a declaration always names a box, so a created incarnation's first admission, whose predecessor has no writer, declares nothing (INV-24); the model no longer gives adoption session 1; TestLegacyLostTargetReturn walks adopt → a move with src_covered false → a cold target admission → the target declared lost → the return declaring the target's session and the source's cut session 0. An instance park never touches staging (R16-1): TestStagingSurvivesLegacyPark. Born covered, narrowed (6.24 item 5): only an unscoped park-replica or a park scoped exactly to holder.location. Rule scope-membership (107 in all); witness wSweepScopeMembership (73 in all). Evidence under the policy of §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.

• Rev 7.16 answers joint round 15 (CODEX-FINDINGS-JOINT-R15.md, cited "R15-1") and is written against claim spec rev 6.23 (876d6908, §2's park scope: the location grammar, the archive incarnation, evidence_at always the original evidence or fencing bound, one deadline for every scope); E is merged to main as 99084d7, F merges next; §22.22 has the disposition. Every remote chore carries the claim's scope from its queuing CAS (R15-1): location exactly one of instances/<host>, instances/<host>/<incarnation>, moves/<host>/<op id> (a move's staging or a rollback's return lane) or moves/<host> (the staging sweep), no trailing / (INV-23); incarnation the location's own, the staging op's holder incarnation or, for a free host's moves/<host> sweep, the newest retired one; evidence_at the original bound, the cut's stop for the commit's source park, the release or the declaration for the target region's, the seal bound for a staging lane (the time after which no staging writer, its lease holder included, can still write: the seal plus the staging lease), the listing for a sweep, the publication for a generation chore; never the cleanup's start time. One deadline for every scope, staging included: acknowledge only after a listing later than evidence_at + H; there is no separate staging contract (rev 7.15 bound a staging park at cleanup and then kept the seal's quiet time instead, which Astra's example exposed: sealed at 100, deadline 560, a cleanup first running at 600 must acknowledge at once, not at 660). Witness wStagingScopeDeadline (delayed cleanup through an agent restart; INV-9 under the mutation); wParkScopeSurvivesRestart takes its deadline from the persisted scope. Rules unchanged (106); witnesses 72. Evidence under the policy of §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.

• Rev 7.15 answers joint round 14 (CODEX-FINDINGS-JOINT-R14.md, cited "R14-n"), against claim spec rev 6.22 (0bf2f49f) with platform-1e's answers to the six rev 7.14 notes, E f0127321 and F d7621a29, both MERGE-READY there; §22.21 has every disposition. The start restores what the run walk selected (R14-1): the open state carries the restore mode, the marker's generation through generation.json or a run generation rooted at [1, 1], so the start and the recovery oracle use one selection; witness wIntermediateBaseline (R's first upload pending at its crash, an empty R2, R's upload landing). One writes_lost plus additional_writes_lost, unique by (box, session) (R14-2): the source's cut session joins the list under its persisted identity, the separate representation is gone, one alert per declaration, INV-21; witnesses before and after the target's first admission. The horizon keeps its signature-age allowance (R14-3): the park scope persists request_limit, and every acknowledgement waits evidence_at + H with H the signature-age limit plus request_limit; a park-sweep acknowledges only after a verification listing later than that (platform-1e's answer to note 2). A running holderless sweep admits another region's chores (R14-4; TestJoinHolderlessSweep). Every remote chore runs under a persisted scope (R14-5): generation chores take theirs from the publication, staging parks bind one before their first step, INV-22. Two fidelity limits stated in §14.2.6 (occupancy by current objects; the publication's precondition and trimming aligned with E). Rules restore-selected-baseline, unique-declarations (106 in all); witnesses wIntermediateBaseline, wNoDuplicateDeclarationEarly, wNoDuplicateDeclarationLate (71 in all). Evidence under the policy of §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.

• Rev 7.14 answers joint round 13 (CODEX-FINDINGS-JOINT-R13.md, cited "R13-n") and is written against claim spec rev 6.22 (0bf2f49f, which adopts rev 7.13's seven notes in rev 6.21 and answers R13-1 to R13-3; rev 6.15 and 6.16 added the persisted park scope and the holderless sweep), the library E on feat/hostclaim-r713 at f0127321 and the generation selector F on feat/hostclaim-genselect at d7621a29; §22.20 has every disposition. The model's park state is the claim's (R13-4): every remote chore carries a persisted park scope {location, incarnation, evidence_at, request_limit}, bound in a CAS before its first step or at the sweep's queuing CAS, so a retry after an agent restart keeps the original evidence time and never restarts the horizon; a free host's at-rest sweep is a holderless parking op {kind: parking, intent: {park_sweep: "v1"}} with no exec and no holder, carrying only scoped remote chores, which blocks the successor create and frees the claim again in its last acknowledgement's CAS (FreeAfterPark); on a serving host the sweep's chores carry session:<n>; INV-20, a create never claims a host over an outstanding park. Coverage, completely (R13-2): an entry becomes covered in exactly four ways, at birth (a warm entry; an entry admitted under a pending whole-location park of its predecessor's region), by publication (which requires an entry to name the published generation and walks every entry in order, skipping covered ones), by CoverRegionPredecessors in the three whole-location-park CASes, and by CoverParkedPredecessors(region, generations) in the sweep's queuing and acknowledgement CASes, only for the generations the sweep parks. The run walk, precisely (R13-1): from holder.generation back to the marker's generation, a link whose generation keeps its objects in another region is passed over, covered or not; a link in this region must be uncovered, and a covered local generation reached as a needed baseline refuses the start and alerts; restoreCalc stays the reference and TestInterruptedCleanReturn walks R → T → S and R2 → R → T → S. additional_writes_lost (R13-3): the lost-target return's extra declarations, one per target session since the cut, unique by (box, session), each alerted. Rules persisted-park-scope, holderless-park, covered-baseline-refused (104 in all); witnesses wParkScopeSurvivesRestart, wFreeSweepVsCreate, wCoveredLocalBaseline (68 in all). Results in §14.2.3 and §14.2.5. The evidence policy (Paul, 2026-10-06; §14.2.1): each revision runs the gate and one mutation sweep at 3,000 seeds, serially and niced; baselines at 30,000 only; the 100,000-seed baseline and the 30,000- and 100,000-seed mutation sweeps run once, at a final pre-implementation checkpoint, when Paul says so. Rev 7.14's 100,000 baseline ran before the policy and is reported; its deeper sweeps were stopped and are marked not run.

• Rev 7.13 answers joint round 12 (CODEX-FINDINGS-JOINT-R12.md, cited "R12-n") and is written against claim spec rev 6.14 (dc146058, whose §6.4a has one operative subsection, "Admissions, coverage and retirement (operative, rev 6.14)", and answers R12-4 and R12-6; rev 6.13, b3825827, adopted rev 7.12's five notes) and the library E at 47426cc1 (unchanged since round 12 judged it merge-ready); §22.19 has every disposition. Coverage is regional and recorded (R12-3): every admission record carries region and predecessor_region; PublishGeneration walks the uncovered records (a predecessor holding nothing anywhere is covered with no chore, one in the publishing region gets its chore and is covered, one in another region stays uncovered with no chore, and one that is the live generation again is left uncovered too, a reading against item 5's first bullet: covered, nothing would retire it later), every cold admission publishes, a prepared generation's included, and CoverRegionPredecessors runs inside the CAS that queues a region's whole-location park: the commit's park of the source region, a rollback's park of the target region, the console's lost-target release (note 5's discharge, adopted). Two readings for the claim: a record admitted while such a park is already queued for its predecessor's region is born covered, and the sweep's CASes cover the records whose predecessors it parks. INV-17 checks, as a whole-location park completes, that no record whose predecessor was there is uncovered. The loss oracle matches the declared identity (R12-1): acknowledgements carry the writer session and generation of the process that gave them, a writes_lost record exempts the writes of the session it names and no other, the source-cut declaration stays separate, and a declared-lost target's every session since the cut is declared, certified or not (a probe session that certified and a warm continuation that did not are two, and no return lane carries either's writes); a two-session witness (INV-18). The probe deadline is checked before each start and before readiness is accepted (R12-2): an expired attempt never starts, a late readiness is not accepted, INV-19 at every probe acceptance, and TestProbeWindow walks k = 29, 30, 31. One operative rule set for admission (R12-4): §7.14 states it, mirroring claim rev 6.14's structure, and the passages that disagreed are corrected or marked history: the restore contract's "after installed and probed", the dirty-return region rows, the start table's failed-host marking (a serving wake's only; a probe never marks the host failed), the recovery limit (nine attempts, R12-5), and holder.admissions retention (conservative, no compaction). The absent-marker sweep fault has its own rule and mutant, absent-marker-origin, so wOriginSwept's evidence no longer rides on baseline-live. Rules foreign-region-uncovered, cover-at-park, session-scoped-loss, probe-window, absent-marker-origin (101 in all); witnesses wTwoSessionDeclaration, wRollbackBaselinePreserved, wCommitCoverage, wCommitInterrupted, wCommitReplayed, wProbeWindowAt (65 in all). Results in §14.2.3 and §14.2.5.

• Rev 7.12 answers joint round 11 (CODEX-FINDINGS-JOINT-R11.md, cited "R11-n") and is written against claim spec rev 6.12 (b202ea4e, which answers rev 7.11's eight notes and R11-2 to R11-5) and the library E at 34224a29; §22.18 has every disposition. holder.admissions replaces op.journal.writers: the record of admissions lives in the holder, so it survives every operation, release and new operation, trimmed to eight covered records and never an uncovered one or the current predecessor. An admission's predecessor is always the last record there (session, box, generation), never the generation an operation chose for a restore (R11-4): a clean return resets holder.generation to the source's for the restore, but the predecessor is still the target's writer (INV-16). Coverage "" | sealed | clean-return replaces BaselineCoversPredecessor: only "" with no certificate records writes_lost, and the record always names its coverage; a clean rollback with src_covered declares nothing. PublishGeneration replaces QueueGenerationRetire: the one retirement path, bound to the observed operation and phase, legal while serving and inside any operation a writer runs in (R11-5), chores with op = op.id inside an operation and session:<n> while serving, only of predecessors in holder.admissions; "" and "@root" are one origin, so nothing retires an adopted host's replica before a cold admission has published a successor (R11-2). The sweep reads an absent generation.json as the origin (R11-1), as the residue oracle does, so an unfinished admission's chain protects an adopted host's replica; witness wOriginSwept. The final oracle runs the recovery admission for real when the serving session is uncertified and judges by what it declared; an admission that cannot run is counted as an unverified prospective declaration, never exempted (R10-6). A probe attempt's five app restarts share its 30 s readiness window (§7.7): the fifth failure or the window ends the attempt and the operation counts one of its three budgeted attempts; a probe never marks the host failed. §5.1, §7.8 and the authoritative-region table carry no instruction left that assigns holder.generation outside a cold admission's CAS or the clean return (R10-3). Rule clean-return-identity (96 in all); witnesses wCleanReturnIdentity and wOriginSwept (59 in all). Results in §14.2.3 and §14.2.5.

• Rev 7.11 answers joint round 10 (CODEX-FINDINGS-JOINT-R10.md, cited "R10-n") and is written against claim spec rev 6.10 (3f916b05, with rev 6.9.1's answers to rev 7.10's readings); §22.17 has every disposition. The admitting CAS comes first (R10-1): before the purge, the restore, the app start and readiness, so nothing the app acknowledges is ever outside a writer session; a session belongs to the agent's replicator, app restarts under the same agent stay in it, a new agent process is a new session and stops a running app it finds; failed starts are governed by a retry policy (five attempts under one session with a doubling backoff from one step, then the host is marked failed and gets no new session until an operator clears it). A cold admission's generation is unfinished until generation.json names it (R10-2): its journalled predecessor stays live, no chore retires it, and the sweep never parks it; the retire chores are queued by the marker's publication; a marker lagging behind holder.generation that names the predecessor of the latest admission, or of a chain of unfinished ones, is the normal state and no alert, any other disagreement leaves the location untouched and alerts. §7.5, §7.6, §7.8 and §7.9 are rewritten around §7.14's protocol (R10-3): the commit and the probed CASes move no generation; holder.generation is always the latest admission's. The admission is API-shaped like the library's Admission (R10-4): KeepStamp only when holder.stamp > holder.session, warm with an empty NewGeneration, refused in creating, deleting, parking, purging and placing, BaselineCoversPredecessor for a seal that covers the stopped predecessor (compared against the seal's own position; the journal says baseline: sealed, no writes_lost), the empty-generation ancestor restore only for the latest journalled unfinished admission. Serving-time chores use op = "session:<n>" and an adopted host's root generation is "@root" (R10-5). Disk-loss faults exempt nothing (R10-6): every exemption comes from a durable writes_lost declaration, alert delivery is checked separately (INV-14), timers are never exempted by the database rule, and a write the remote holds is never declared lost while its writer's box is with us (INV-15). Startup PUTs are session evidence (R10-7): the first upload and the anchor enter the ledger, a retry after the client's wait makes the session uncertain for good, server completion and client response are distinct, and the bytes of a retry are the original's. The budget prices the new protocol (R10-8): a restore per probe attempt, the admission's overhead, a fresh generation's full upload on a retried probe; the 2 GiB example runs to 117.9 s and admits one attempt, the review's 2.5 GiB is refused at 131.2 s; the replication interval is the normal window a failed upload extends. Counters are structured (R10-9): the baseline logs COUNTERS {json}, the generator fails on a missing field, §14.2.3 and the change note are regenerated. Two gaps the rerun found beyond the review: a rollback is clean only when the source's own replica covered its stopped database at the seal, else the return carries the seal, whether or not the target wrote (§7.8, rule seal-return, INV-15); and a pre-flip round never forces a sync on a session whose start is unfinished. Rules admit-before-start, baseline-live, seal-return (95 in all); witnesses for the acknowledgement before admission, the parked baseline, the first-upload and anchor retries and the uncovered return (57 in all). Results in §14.2.3 and §14.2.5.

• Rev 7.10 answers joint round 9 (CODEX-FINDINGS-JOINT-R9.md, cited "R9-n") under Paul's ruling to simplify, and is written against claim spec rev 6.9 (f6180ae4); §22.16 has every disposition. A box never reuses its local database. Every admitted writer, warm or cold, in every phase, purges the local database (an error-returning purge; if it fails the writer does not start) and restores from the certified remote: warm, the same generation up to the certificate's max_txid; cold, the predecessor generation's remote. Lineage, provenance and the warm-provenance rule are gone (R9-1 closed by construction; its clean-close stale-database scenario is the witness wStaleLocalAfterClose). Warm continuation needs only the certificate for the observed session with a matching max_txid, and any op.exec box may continue (claim rev 6.8.2 reverses rev 7.9's same-box reading). holder.writer_box is set by every admission and survives operation replacement; a cold admission of an uncertified session records writes_lost {box: observed writer_box, generation, session, remote_max_txid} in its journal entry and the box alerts, so a crash with acknowledged, unuploaded writes loses them declared, never silently (R9-2). Only warm and cold survive (R9-3): a first install is a cold admission into an empty generation; holder.generation is the only authoritative generation in every kind and phase; a probe or recovery that opens replication is a cold admission that moves it; an operation's prepared generation is opened once, by its probe's cold admission, and never re-entered; a fresh generation roots at the writer's full first upload, made after the CAS and before its marker; a failed cold start leaves an empty, unpublished generation for the sweep and the next attempt is cold again. Admission happens after readiness and before any upload, and is bound to the observed op.id and op.phase, serving's "" compared literally, refused in deleting, parking, purging and creating (R9-4; INV-13). Close evidence is client-observed success for every request class, level-0, compaction, snapshot and retention, with a sticky uncertainty for a timeout or a lost response (R9-5). §14.2.5's tables are regenerated from the retained verdicts (R9-6). The spec states plainly how today's activator differs (§7.14: production keeps the warm cache and restores only when the local copy is absent; this is a behaviour change, costing a restore per wake and the unuploaded writes on a crash). Rules remote-baseline, writes-lost, admit-bind-op (92 in all); witnesses for the stale local database after a clean close, the silent loss, the stale closure during a delete, a maintenance retry and a lost response (52 in all); the whole-start-check witness is retired, subsumed by regional restores. Results in §14.2.3 and §14.2.5.

• Rev 7.9 answers joint round 8 (CODEX-FINDINGS-JOINT-R8.md, cited "R8-n") and is written against claim spec rev 6.8 (5462d293), whose rewritten §6.4a, writer sessions and epochs, answers R8-1 to R8-4, and rev 6.8.1 (a963d98d): only op.exec may open replication, in every op kind; §22.15 has every disposition. R8-1 (P1): rev 7.8's closed.json was consumed by deleting the version the writer read, which is not one-use under S3's semantics (an exact version delete removes it and exposes an older version; a delayed or replayed PUT recreates it); the certificate is now per writer session, closed/<session>.json, never deleted, and what makes it one-use is the admitting CAS that moves holder.session forward: a certificate names a dead session from then on, whatever its stamp and max_txid say. R8-2 (P1): rev 7.8 checked replication state only at an ordinary wake; every path that opens replication is an AdmitWriter now (a committed landing's serving, a restarted probe, a reverted source, an opened rollback recovery, a push's writer), and a cold admission runs inside the operation it interrupts, keeping its kind, id, journal, participants and obligations (§7.14's phase table says which box may be admitted in which phase; op.exec is handed over before any probe or landing write). R8-3 (P2): a created incarnation's first wake is a cold admission into an empty generation: no snapshot [1, 0], no anchor [0, 0] (the pinned encoder refuses a zero TXID, TestFact_R8_3_EmptyBootstrap); the app starts first and may create its database, and the first transaction's file is the first upload. R8-4 (P2): the warm database is the cold baseline only with provenance: a lineage file naming the journalled predecessor's {generation, session}, the predecessor's box being this box, and an integrity check; re-initializing a stamp record never writes lineage. R8-5 (P2): the clean close's evidence is every request of the writer's lifetime, level-0, compaction, snapshot and retention, with a sticky uncertainty flag for a timed-out original whose retry succeeded. R8-6 (P3): §14.2.5's retired-door rows separate the historical results from the current ones. Rules writer-session, admit-everywhere, exec-writer, warm-provenance, valid-ltx, close-evidence; witnesses for a dead session's certificate replayed, the collision during a committed landing's serving and during a probe restart, a non-exec writer, a warm database with a foreign lineage, an empty first wake, and a retry that succeeds while its original stays unresolved. 90 rules, 49 witnesses. The model faults this round found before the final numbers (a stalled worker replaying a finished build, the carried files untagged, a source that lost its disk during a rollback, the biased schedule's unbounded hold in the calm phase, a lost target's unfinished admission blocking the rollback, every close outside serving dropped) are in §14.2.2. Results in §14.2.3 and §14.2.5.

• Rev 7.8 answers joint round 7 (CODEX-FINDINGS-JOINT-R7.md, cited "R7-n") and is written against claim spec rev 6.6 (b10547e1), whose new §6.4a, writer epochs, answers R7-1; §22.14 has every disposition. R7-1 (P1): the hazard rev 7.7's note raised is real and now closed: litestream's level-0 PUT is unconditional and its key is prefix, level and TXID range only (TestFact_R7_1_UnconditionalPut), so a dead writer's in-flight upload for [N + 1] can replace the file the next writer uploaded for the same TXID, or make its upload loop skip it. Two writers whose uploads could overlap never share a generation (§5.1 step 9, §7.14): a writer that stops cleanly drains its uploads and writes closed.json {stamp, max_txid} once; a wake continues the generation only if that marker exists, its max_txid is the generation's remote maximum and its stamp is the box's own, and the writer consumes it as it opens; anything else is lost replication state and a cold recovery, an installing CAS into a fresh generation (new holder.generation, new holder.stamp), built under stop evidence from the warm database or the old generation restored, published, then served, with the old generation parked as a chore. Rules recovery-generation, closed-marker, close-waits; witnesses for both completion orders, the initialization/remote-position race, a stale marker, a crash before the marker, and a clean close that must wait. R7-2 (P2): the cold-restore oracle checks required writes by identity and compares the state with the replay of exactly the writes the restored files carry; the per-key mask is gone, with the review's counterexample as a witness. R7-3 (P2): every retention path keeps the newest level-0 file (newest-l0, witness with the local position ahead of the uploads). R7-4 (P2): a build is a durable intent, then acknowledged artifacts, then a completed manifest, and generation.json is published only from the completed state (§5.1 step 2, §7.6; INV-11, build-completion, witness with crashes between the steps). R7-5 (P3): the Store gate awaits each maintenance event it claims, compares row contents with updates and deletes, and forces a restore through compacted continuation files (§14.2.1). The model's full files replace the state they are applied to and carry every write they hold, which the rebuilt oracle needed. 84 rules, 42 witnesses (two rules the sweep no longer reaches at 3,000 seeds under writer epochs, evidence-whole-tree and timer-freeze, gained witnesses; the two door witnesses are retired). Results in §14.2.3 and §14.2.5.

• Rev 7.7 answers joint round 6 (CODEX-FINDINGS-JOINT-R6.md, cited "R6-n") and is written against claim spec rev 6.5 (d36adcfa), whose new invariant answers R6-4: holder.stamp always names the installation op.exec should run, so every CAS that changes op.exec writes it, a new installation's new gen or an existing installation's own stamp from the op journal; §22.13 has every disposition. Round 6 judged the claim ready for planning and found no P1. R6-1 (P2): the model's restore oracle wrote anchors into the system it checked and granted a position before the anchor PUT succeeded; the restore is now a pure calculation (restoreCalc) that every oracle uses, and the activator's initialization (restoreInit) opens replication only once the anchor PUT is acknowledged, reading the position from the listing, never from the restored TXID (§5.1 step 7; rule anchor-acked, witness: the anchor PUT held across attempted opens); every oracle asserts its purity (buckets, versions, queues, anchors, console, random draws unchanged), and every number in §14.2 is rerun. R6-2 (P2): litestreamfacts asserts exact facts and fails on any alternative (the newest level-0 file retained by identity, the next TXID exactly N + 1, every row, the original continuation gone, the rooted restore's exact refusal), and gains the missing integration gate: one anchored lineage through the production Store shape with compaction, snapshot rotation, time-based level-0 expiry, disk loss and repeated cold restores, exact positions and contents asserted (§14.2.1). R6-3 (P2): the restored phase verifies the database building produced instead of restoring it again, T11 prices regional S3 and the disk separately and the verification pass too, and the worked example is one set of numbers in the spec, the note and the test (2 GiB at 10 / 250 / 500 MiB/s: 53.6 s fixed, one attempt; §7.3, §7.6). R6-4 (P3): the return to source encoded as claim rev 6.5 states it (the flip keeps the source's stamp in the journal, the return CAS writes it back, a lost local record re-initializes from it, artifacts are tagged when the new stamp activates, retire-artifacts parks by tag; §6.4, §7.8; rule return-stamp, witness: a dirty return with a lost local record). R6-5 (P3): the anchor's encoding inputs, the header timestamp included, are persisted in the install manifest so a replayed PUT repeats identical bytes (§5.1 step 2; TestFact_R6_5_AnchorReplayBytes). Compaction in the model keeps the newest level-0 file, as litestream's retention does. 79 rules, 34 witnesses. Results in §14.2.3 and §14.2.5.

• Rev 7.6 answers the moves side of joint round 5 (CODEX-FINDINGS-JOINT-R5.md, cited "R5-n") and is written against claim spec rev 6.4 (697f0f9f), which answers the claim side of R5-4 (rev 6.3: holder.stamp, the record's initialization, two named retirements; rev 6.4: the stamp captured at work selection, retire-artifacts never moves a stamp, the legacy location's children); §22.12 has every disposition. Round 5 found that rev 7.5 described the pinned libraries from their documentation; rev 7.6 starts from their observed behaviour: internal/sim/litestreamfacts/ drives litestream v0.5.14 and superfly/ltx v0.5.1 as pinned and asserts each fact this spec relies on (§14.2.6). R5-1 (P1): a snapshot-only install restarts replication at TXID 1 (fact R5-1a) and a later cold restore loses the new writes (R5-1b); the install now writes a level-0 anchor [N, N] beside the snapshot, which the pinned open takes as its position (R5-1c, d); -txid is follow-only (R5-1e). R5-2: the pinned writers set HeaderFlagNoChecksum, so there is no post-apply checksum to compare; verification is what the format supplies, the per-file CRC-64 trailer, plus SQLite's integrity check and the required TXID (§5.1 step 5); the whole-state checksum is gone from the model. R5-3: snapshot rotation and retention are specified and modelled; the restore roots at the newest current successor snapshot of the named generation at or past the pinned one, and only at the pinned version when no successor is current (R5-3d, e). R5-4: claim rev 6.4's stamp lifecycle, encoded exactly (§6.4): holder.stamp written by every installing CAS, the local record initialized only from a fresh read under the guard, no record refuses, retire-artifacts against retire-installation, and a dirty rollback's install carries its own stamp. R5-5: the sealed snapshot is built on the target from the staged replica; T11 prices the final delta within the bar and the target's restore, snapshot and anchor at the local rate, and budget_test.go shows a 2 GiB database over 10 MiB/s admitted that way and refused as a cross-region transfer (§7.3, §7.6). R5-6: the retention fixture populates 2 to 33 and asserts the injected incarnation absent. LTX keys follow the pinned S3 client's layout, <prefix>/<level, 4 hex>/<min>-<max>.ltx. Two new rules, each with a witness (restore-anchor, root-advance). Results: 30,000 and 100,000 seeds clean; 77 rules, 63 caught alone, 11 in stated combinations, 2 liveness, 1 unreachable, none unexercised (§14.2.3, §14.2.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 claim spec rev 6 (3ea3f90c), which answers the claim side (R3-2, R3-3, R3-4); §22.10 has every disposition. On the spec: R3-1, the restore contract is an algorithm now (§5.1): generation.json names the installed snapshot by version id and TXID, and the restore replays the LTX chain that continues it, skipping what it already covers and refusing a conflict, never guessing; R2-5, a recovery install's configured phase renders current inputs and is never gated on move.inputs (§7.6, §7.8); R3-7, T11's permitted probe attempts depend on the admitted budget, and a test shows rev 7.3's formula refused every default move (§7.3, budget_test.go); claim rev 6's installation-scoped retired marker, ordered orphan cleanup and namespace sweep are taken into §6.4 and §19.4. On the model (§14.2): restore is a chain, not a union; the local fence is per installation and a deterministic UK→US→UK round trip serves on UK again; orphan cleanup is a plan with pauses; the sweep discovers locations from the namespace with the 32-entry cap modelled; a public request to a landing target before the commit is INV-5 (R3-5), which gives commit-before-open its own violation; mutate.sh fails on orchestration errors and missing witness output (R3-6); every witness names its failure and the gate proves it under every proper subset of its mutation set. Three new rules (fence-by-installation, orphan-order, sweep-namespace), each with a witness. Results: 30,000 and 100,000 seeds clean; 71 rules, 57 caught alone, 11 in stated combinations, 2 liveness, 1 unreachable, none unexercised (§14.2.5).

• Rev 7.3 adds deterministic witness scenarios to the model (§14.2.2, witness_test.go): one fixed, hand-scheduled scenario per rule the random sweep catches rarely or only in combination, 22 scenarios for 20 rules. Each forces exactly the interleaving its rule exists for, under a quiet RNG that injects nothing, holds with the rules in place, and violates an invariant under the rule's mutation, alone or in the stated combination. Witnesses never draw from a seed's RNG, so adding one reshuffles nothing, and the whack-a-mole of rev 7.1 (lost-return-park) and rev 7.2 (generation-conditional) ends. mutate.sh runs them beside the sweep and reports both; a rule counts as caught if either catches it. Nine rules are caught alone by their witness, generation-conditional and declare-lost-compute among them, which the sweep misses at 100,000; eleven hold alone and violate in their combination, which is the redundancy the combination table states, shown rather than inferred (§14.2.5). Found on the way: the purge drain iterated registrations in Go map order, the model's one source of nondeterminism; it drains in create-id order now and two runs agree exactly. Results: 30,000 and 100,000 seeds clean; 68 rules, 53 caught alone, 12 in stated combinations, 2 liveness, 1 unreachable, none unexercised.

• Rev 7.2 is written against claim spec rev 5.2 (465fee96), which adopted CC22: the creator's claim CAS is If-Match the ETag read at registration (If-None-Match: * when the claim was absent), a 412 restarts the create from step 0 with a new registration, the purge fence is released by writing a free claim, and a new C5a says a claim object is never deleted. The model encodes that text: the 412 restarts the create instead of abandoning it, and a new rule, claim-never-deleted, lets the mutation delete a fence that found no claim; dropped, a paused creator's If-None-Match: * passes again (§14.2.2, §14.2.5). Rev 7.2 also closes the gap rev 7.1 left: a biased schedule in half the seeds makes the target's app write in the settle window, fails the settle check, and stops the target the moment its first return PUT is out, so declare-lost meets a partial return lane. lost-return-park (model 27) is caught alone (3 / 3,000, 32 / 30,000), where rev 7.1 reached it in no seed of 300,000. Results: 30,000 and 100,000 seeds clean; 68 rules (§14.2.5). The reshuffle this schedule causes moves two rare rules back: declare-lost-compute is combination-only again (0 / 100,000 alone, 3 / 100,000 with watchdog-independent), and generation-conditional (model 29) is unexercised (0 / 300,000; 2 / 100,000 on rev 7.1), listed as such in expected-outcomes.txt as rev 7.1 listed lost-return-park (§14.2.5).

• Rev 7.1 is written against claim spec rev 5.1 (64eec93b), which adopted CC20 (the sweep lists moves/<host>/) and answered CC21 with a purge fence on the host claim instead of the creator-side check rev 7 proposed: S3 cannot condition one object's write on another's version. The model encodes the fence, a biased schedule that pauses a creator between its registration re-read and its claim CAS, and finds one more condition the fence needs: the creator's claim CAS must be conditional on the claim ETag it read when it registered (CC22), or a fence placed and released while it slept lets it through (§14.2.5, §19.4). It also fixes a moves-side fault the 100,000-seed run surfaced: generation.json is a reused key, and an earlier push's PUT completing late put an older generation back and left recovery stuck; the marker is now written If-Match the one it supersedes (model 29, §5.1). Results: 30,000 and 100,000 seeds clean; 67 rules, 51 caught alone (the fence and the ETag condition among them), 12 in stated combinations, the re-read alone shown insufficient (287 / 30,000), and declare-lost-compute now caught alone (§14.2.5). The mutation harness runs one prebuilt test binary under $TMPDIR, with no copies of the source (§14.2.1).

• Rev 7 was written against claim spec rev 5 (4a458a9c on design-replica-ownership), which adopted CC15 to CC19. It: - closes the model's last gap: a biased schedule beside the uniform one recreates a host where it last served while the previous incarnation's requests are still in flight, and races door listings against the delete and the recreate. location-per-incarnation (claim C3a) is now caught alone, and both door rules with it (§14.2.5); - re-encodes claim rev 5: the at-rest sweep under an obligation the sweeping box owns, registration leases, orphan records at any time, holder.generation, signatures taken at the deadline check with an SDK retry that must not re-sign; - asks for two more claim changes, CC20 and CC21 (§19.4).

Earlier revisions:

• Rev 6 (7ac666fe) answers joint Astra round 2 (CODEX-FINDINGS-JOINT-R2.md, df41156c; cited "J2-…"), whose three verdicts were "not ready", and is written against claim spec rev 4 (a3c86fa5 on design-replica-ownership), which answers the claim-side findings. Rev 6: - rebuilds the model to encode exactly what the specs say (§14.2): restore and the start check no stronger than §5.1; record-first transitions split from their claim halves, with crash points between; independent processes for the host guard; a door listing with O1 and O2; creates and purges as concurrent console plans over two hostnames; requests that complete after H; a final oracle that only reads; and a mutation harness that counts only a parsed invariant violation as a detection (J2-R2-9, J2-R2-10); - specifies this spec's share of J2-R2-1: operation-scoped generations within the claim's holder.location, a restore contract that reads only the generation the claim names, and a straggler sweep for what lands after H (§5.1, §6.4); - fixes J2-R2-5: a recovery probe runs on the inputs it renders now, not the move's pinned ones (§7.6, §7.7); - fixes J2-R2-8: the start check also requires the generation the claim expects, so the third admission fence the model relied on is now specified (§5.1); - makes the record and the claim consistent: every move transition is one record CAS, and the claim follows it; any actor may write the claim half, which the record fully determines (§7.5, §19 K4); - makes the cut promise the enforced deadline (§7.4, T11); - records that CARLOS_SECRETS_KEY is on every flagship box and config sync is armed in every region (§1.2, §15); - lists CC15 to CC19 for platform-1e (§19.4).

Rev 6's changes are marked "(J2-…)" for the review's findings and "(model N)" for the stricter model's.

• Rev 5 (4ec3282b) was 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.

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. Rev 4: - builds the model: internal/sim/hostlife/, a test-only Go package (§14.2). It encodes claim spec rev 2 (cf3a7861) and this spec, with the real IAM split, late S3 completion, crashes, partitions, whole-VM pauses, destroyed and restarted boxes, and old executables. It runs 30,000 seeds clean, and a mutation harness drops each rule in turn; - adopts the joint review's adjudicated text for D1, D3 to D8 and I-7, and answers the findings this spec owns: N2, N11, N13, N14, N15, and the 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.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).
• Rev 2 (45b77691) answered them, cut the scope to Phase 1, took Paul's rulings M4 to M15, and rebuilt on #199 rev 3. Round 2, CODEX-FINDINGS-MOVES-R2.md (e5b67514), resolved or accepted the deferral of most of round 1. It found 6 new P1s and 4 P2s: "not ready".
• Rev 3 answers round 2. Changes are marked "(codex R2-N)"; rev 2's marks "(codex N)" stay. §22 records every disposition from both rounds. Rev 3 also: - takes Paul's rulings M16 to M18 (§0.1); - builds on the host lifecycle claim that Paul ruled on 2026-10-02: one object per host, updated by CAS, that serializes delete, park, move, push, the db door and wake. It is specified in docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md (rev 1 at 653ad4b1 on design-replica-ownership; "the claim spec"). §19 says how moves use it and where this spec asks it to change.

Status: DRAFT for review. Nothing here is built. Discussion: amadan carlos/platform #175. Goal (Paul, 2026-10-02): "I want region-default AND the ability to easily move any app or instance to a different region." The region default is docs/superpowers/specs/2026-10-01-nearest-region-default-design.md on branch design-nearest-region. Builds on:

• #331, docs/superpowers/specs/2026-08-28-instance-move-design.md.
• The moves design record (the "09-24 record"), docs/superpowers/specs/2026-09-24-instance-moves-for-every-app-design.md on branch docs-instance-moves-design, with CODEX-RULINGS-INSTANCE-MOVES.md.
• On main (7edd4b33): P0 (the cut fence), P7 (the edge door), and the move-ready fix (16 MiB readiness bar, copy receipts for multipart ETags).
• #199 rev 3, docs/superpowers/specs/2026-10-02-replica-ownership-design.md at 66f1dad3 on design-replica-ownership (the "#199 spec"). It failed review for the same reason as round 2's P1s; the claim spec supersedes it 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.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).

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

0. Rulings and the shared primitive

0.1 Paul's rulings (2026-10-02). Not reopened here.

| id | ruling | where Phase 1 spends it | |---|---|---| | M1 | Who: owners move their own apps and instances, self-serve, from the console and the CLI. Operators can do the same for any account. The platform refuses unsafe moves. | Phase 1 is operator-only (§12); owners come in F1 (§16) | | M2 | Downtime: a short cut window (tens of seconds of 503), an automatic health check after the cut, and automatic rollback to the source if the target will not start. Not live migration. | §7 | | M3 | Stores move with the app. | F4; Phase 1 leaves the app store in place and refuses private stores (§7.1) | | M4 | The files the move carries are a fixed set. | §6.1 | | M5 | The files archive is capped at 256 MiB, enforced while streaming and again at the cut. | §8.1 | | M6 | Person-started moves cut automatically once ready and validated; the API default stays manual; --manual-cut exists. | §12 | | M7 | The source copy is held for 7 days after a move; owners may end the hold early. | F3 | | M8 | An app move pauses when one of its instances rolls back, and keeps the target app region. | F5 | | M9 | An app store's final copy holds every consumer at 503, behind a durable barrier covering concurrent creates. | F4, F5 | | M10 | An app with sidecars is refused an app move until sidecar moves exist. | F5 | | M11 | Target pre-warming is deferred; eligibility is gated on the measured duration of the whole cut. | §7.3 (T11) | | M12 | Rehearsal order: a probe app, then a disposable ips instance, then kpmg, each with scoped approval. | §14.4 | | M13 | Owners only, not members; the member-minted instance-token bypass is closed. | §12; F1 | | M14 | One landing path in production. | §7.6 | | M15 | A landed copy is installed into the target's instances/, never served from moves/. | §5.1, §7.6 | | M16 | An operator-only carlos move resolve --declare-lost <box>, refused after commit, proceeds as a clean rollback after a confirmation naming what is lost. | §7.10 | | M17 | The return lane is approved. Every region's sibling_staging_arns lists every other region's data bucket, with moves/* Put and Delete and prefix-conditioned List only. | §7.3 (T10), §15 | | M18 | Tito waits. Move mutations are operator-only; instance-role tokens keep only the status read. | §12 |

0.2 The 09-24 record's rulings

They bind unless M1 to M18 override them. R4 ("rollback is a move back") is narrowed by M2: a landing that fails before the target admits traffic is undone automatically (§7.8); after the target opens, R4 stands. Q5 (other accounts operator-only until #171) is consistent with Phase 1.

0.3 What #199 contributes

• Replica data stays at instances/<host> (internal/activator/activator.go:138). No record field carries storage identity, so this spec names a generation by the operation id that installed it, in object names and marker files (§5.1).
• The incarnation, provision.Incarnation(rec), including the zero-CreatedAt legacy identity, and the park helpers (copy with a manifest then delete; local rename), now specified in the claim spec §2 and §5.

0.4 The host lifecycle claim

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

• The object control/hosts/<host>.json, rewritten whole by CAS: a per-write revision gen (not a data generation, J-D2); a holder; op with kind, id, phase, intent (written in the start CAS), journal, exec and participants; touched (with complete); inventory; obligations[]; the lost quarantine; and retired_incarnations.
• Its invariants: C1 one holder; C2 intent before effect, a recovery owner for every state, every CAS conditional on op.id as well as the ETag; C3 storage mutated only by the current operation and only 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). 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). Rev 4 adds C3a: no storage location is shared between incarnations. holder.location is instances/<host>/<incarnation>/ for a new incarnation and instances/<host>/ for an adopted legacy host, set with the holder and immutable while it holds; restore reads only that location, plus this spec's generation within it, from the same fresh admission read.
• 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, 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, an exclusive flock shared by every OS process that writes host state, with a fresh claim read under it (§6.4); door listings that read the claim twice, O1 and O2 (§6.5); execution leases for liveness, and declare-lost by compute fencing only (§7); one claim.Adopt routine whose discovery parks every other region and every other box (§9); app admission registration, closed and drained by purge, which fences a drained registration's host claim before removing it (§5.1, §5.3, CC21); cancelled_creates (§5.1); the purge journal reserved → adopted → claimed → torn-down → retired → done (§5.3); park manifests with separate archive and deletion sets (§6.2); the floor on every executable restore path (§10).

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

Rev 4's model required CC1 to CC13 of claim rev 2, and claim rev 3 adopted them; rev 5's CC14 is in claim rev 3.1 and rev 4; rev 6's CC15 to CC19 are in claim rev 5, rev 7's 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. 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.

0.5 Paul's rulings of 2026-10-06 (#236; claim rev 6.27 §1.1) and region HA's requests

Claim rev 6.27 (989ee349) §1.1 records every ruling of amadan #236. The ones this spec acts on:

• P1, the floor is the first fully integrated release. §11's control/moves-protocol.json names a real release that carries the claim, the moves and the region HA code together; no placeholder tag.
• P5, record-backed placement only. A move's target is a record's region and a box the roster knows; nothing places by hand.
• P6, rename and transfer stay refused. Out of scope here as before.
• P7, cold-only admissions. Until a reviewed Litestream fix (#234) makes a clean-close certificate safe, every admission is cold: no closed/<session>.json is written, no PredecessorCertified admission is made, and no plan task depends on warm. §5.1 step 9's warm mode, the certificate ledger and KeepStamp's interaction with warm stay in this spec as the behaviour a later revision turns on; the model keeps both modes so the rule stays checked. The cost in Phase 1: every wake restores from the remote (one regional S3 read and one disk write of the database), writes a fresh generation's first upload (one disk read and one regional S3 write) and its generation.json, and PublishGeneration queues one park-generation chore for the dead predecessor per wake. T11 already prices every probe attempt as a cold admission (rev 7.11, R10-8), so the readiness budget is unchanged by P7; the per-wake chore is a claim CAS and a regional park after the horizon, outside the cut window.

Region HA (spec 1 rev 5.4, §9) asks four things of this spec, folded in as follows; the fifth, L18, is stated as a limit:

• L14 (§7.10): the termination fence is M16's evidence, automatically.
• L15 (§7.1, §7.3, §19.1): the target box is chosen in the start CAS.
• L16 (§5.1 step 2, §7.6): one install routine, two sources.
• L17 (§6.1, §8.3, §9.4): a files manifest per installation.
• L18 (§14.2.6): two boxes per region in the model is not done here.

1. What happened in production

1.1 Finding 1: busy instances never reached ready (fixed on main)

Multipart ETags never matched after CopyObject. Fixed in 2cbf6196 and 167d721b (merged as 7edd4b33): copy receipts (internal/activator/backend_exec.go:1557) and a 16 MiB readiness bar (internal/host/movespass.go:215-235, applied at :387).

1.2 Finding 2: a completed move could not start for 1h54m

kpmg.bdn.oncarlos.com (account bdn, app ips) moved IE (home) to uk, and every wake on the UK box then failed with instance not healthy within 30s (backend_exec.go:1443). Both causes are confirmed.

(a) The per-host data directory does not move. The cut mirrors the replica (movespass.go:476-490), purges database files only (backend_exec.go:1566-1575), and flips the record (movespass.go:494). The app keeps instance.key and report.token in /data/<host>/, which no platform code names. On the UK box the app minted a new key.

(b) Only the Ireland box holds CARLOS_SECRETS_KEY (codex 20). The UK, US and AU journals log "config sync loop disabled: CARLOSSECRETSKEY not set" (internal/host/agent.go:884). Both config loops return at once (agent.go:881-886, :1279), the fast converge skips its config leg (agent.go:1812), and the spawn treats a missing config file as empty (backend_exec.go:1146-1149). Paul approved distributing the key to every region box. Done (2026-10-03): the key is on all four flagship boxes, and config sync is armed in every region. The fingerprint every box publishes (§10) still verifies it per box, and T2 still refuses any target without it: a new or rebuilt box can lack it again. With config sync live everywhere, bundle updates now reach a box during a move, which is why J2-R2-5's case is real (§7.6).

1.3 Finding 3: the rehearsal proved nothing

bdf/hello has no key file, store, config or timers. §14.4 rehearses with an app shaped like ips.

1.4 Finding 4: SSM Parameter Store is regional

carloku-infrastructure region-uk.tf:61-64: nothing replicates /carlos/* between regions. §10 shows that an instance needs only the box's secrets key from it.

2. Phase 1: what it does and what it refuses

Phase 1 moves one exec-backed, hibernating kind:"instance" record between two non-fleet placements, into home only with host claims on (Ruling R1, rev 7.24), driven by an operator. It carries every piece of per-host state, proves the target can run it before the source stops, starts it on the target with no public traffic, and opens only after a commit. If the target cannot start it, the instance returns to the source automatically, carrying anything the target wrote. Phase 1 refuses everything §7.1 lists. It deletes nothing: what a move supersedes is parked under the operation's id, out of every live namespace, ready for F3's cleanup.

3. Words

• Source / target: the box serving before the move, and after. "Box" means the one box whose registry owns the route (OwnsRoute, movespass.go:180-185).
• Move id / rollback id: console-minted, unique, mv_ or rb_ plus 26 lowercase base32 characters. Each names one operation.
• Generation: one installed copy of an instance's state (database, files, timers), identified by (op id, incarnation). An instance that has never moved is in the origin generation (no markers anywhere).
• Handoff: the transfer of the execution right from one box to another, with a new generation (§5). A move is a handoff; a dirty rollback is a handoff back; a future carlos db push is a handoff on one box.
• Hold: a registry row status that admits no traffic, ticks or ordinary wakes (§5.2).
• Flip / commit / open: the CAS that sets region to the target; the CAS after which the target is authoritative; the target row becoming ready.

4. Invariants

Stated first, designed to, and proved by the simulation in §14.2.

• INV-1 One writer. At any instant at most one process tree, on any box in any region, runs the instance with write access to its database, files or store. A box starts the instance only while the claim names it as the execution holder, and the right moves only on stop evidence proving the previous holder's whole process tree is gone (§5.3). A timeout never moves it (codex 1, R2-1).
• INV-2 No lost acknowledged write. No write the instance acknowledged, to a client, a tick, its own background work or an external system, is lost by any outcome. A rollback carries back whatever the target wrote, and a source recovery never reinstalls over its own new writes (codex 2, R2-3). M16's --declare-lost is the one disclosed exception.
• INV-3 Convergence without a human. A crash of any actor (a console or agent process restart, or a box reboot) at any step leaves a state from which the move reaches a terminal outcome with no human action. This holds even when the crashed activator has lost all memory (codex R2-2). The exception is a box that never returns, handled by M16 (§7.10).
• INV-4 Files match the database. Every start, on any box, uses a files directory whose generation equals its database's generation, and the generation installed in the box's own bucket. Otherwise the start is refused (§5.1).

Supporting invariants:

• INV-5 No admission before commit. A row leaves a hold only by a conditional write naming the operation that holds it (codex 3, 6).
• INV-6 The environment that runs is the environment that was checked, from inputs whose versions were pinned at readiness (codex 14, R2-8).
• INV-7 Install is never replayed over writes, on the target or the source; and a completion marker is published only after everything it vouches for is durable (codex 5, R2-3, R2-6).
• INV-8 Phase 1 deletes nothing a recovery might need (codex 8).
• INV-9 Bounded. Every non-terminal state has a deadline after which it advances, recovers, or pages in a state that still satisfies INV-1 and INV-2. Recovery deadlines are separate from the promised cut window (codex R2-10).
• INV-10 Incarnation isolation. When a move or rollback ends, no copy of the instance's data remains in a live host namespace (instances/<host>/, moves/<host>/, the flat DB path, the files directory) on any box or bucket except the one the claim names as current. Everything else is parked under the operation id (codex R2-5).

What the model checks (§14.2). The coordinator's list for the joint model, and where each lives:

| invariant | checked | here | |---|---|---| | at most one writer per host, across regions | after every step | INV-1 | | no acknowledged write lost (database writes and registered timers), except a declared loss | at the end, on the serving box's local state and on a cold restore from the bucket | INV-2 | | no recreated host sees a previous incarnation's database, key or config | at every spawn | INV-4, C1 | | no live-namespace residue after an operation ends | at the end, every bucket and box | INV-10 | | claim and record agree after recovery | at the end | C2 | | every crash converges with no human, except declared loss (M16) | at the end: the run must reach a quiescent state | INV-3 | | 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 |

5. The handoff protocol

5.1 Generations, markers and the restore contract (codex R2-6, R2-9, J2-R2-1, J2-R2-8)

Location and generation. Claim C3a gives each incarnation its own replica location, holder.location: instances/<host>/<incarnation>/, or instances/<host>/ for an adopted legacy host. Within it, every installed state of the database is a generation, named by the operation that installed it: the origin generation ("", written by the host's own replication from its first wake), then one per committed move, per push, and per dirty rollback. Each generation has its own key prefix:

| generation | replica objects | |---|---| | origin | <location> itself, the layout litestream writes today (<location>ltx…, a legacy host's existing objects) | | an operation op | <location>g-<op id>/…: the installed snapshot, its anchor and every LTX object replicated on top of them |

Within a generation prefix the objects are litestream's, in the layout the pinned S3 client writes (s3/replica_client.go, ltx.FormatFilename): <prefix>/<level as four hex digits>/<MinTXID as sixteen hex digits>-<MaxTXID as sixteen hex digits>.ltx, so a snapshot ending at TXID 7 is 0009/0000000000000001-0000000000000007.ltx and a level-0 file for TXID 8 is 0000/0000000000000008-0000000000000008.ltx. Rev 7.5 wrote ltx/<level>/, which is not the layout (R5-6). Rev 7.6 writes the real one in this spec and in the model.

The claim names the current one, holder.generation (CC18): written only by a cold admission's AdmitWriter CAS (a landing's, a push's or a dirty rollback's probe into its prepared generation, every recovery into a fresh one, §7.14) and by a clean rollback's return CAS, which names the source's generation again for the restore (§7.8; R10-3: no commit, probed or install phase writes it). Restore reads it from the same fresh admission read as holder.location (claim C3a).

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.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 took 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. Joint round 5 showed that rev 7.5 described litestream v0.5.14 and superfly/ltx v0.5.1, the versions this repository pins, from their documentation and got three things wrong (R5-1, R5-2, R5-3). Rev 7.6 writes the contract against the libraries' observed behaviour: internal/sim/litestreamfacts/facts_test.go drives the pinned libraries with the file replica client and asserts every fact cited below as "fact R5-n"; a library upgrade that changes one fails there first (§14.2.6).

1. The sealed transfer is the staged replica at the required final TXID (R5-5). At the cut, after the final checkpoint and SyncAndWait, the source's replication position is N: the MaxTXID of its newest level-0 file. The final mirror round (staged, §7.4) copies the delta of the source's replica into staging's replica/, within the 16 MiB bar, and the seal records N and the exact versionId of every current LTX file under replica/. Nothing larger crosses the region boundary at the cut: rev 7.5 shipped a whole snapshot of the stopped database after the stop, which a 2 GiB database over a 10 MiB/s path cannot do in a 120 s window, while T11 priced only the 16 MiB delta (R5-5). N is the required final TXID of the transfer.
2. The target builds the generation's snapshot from the staged replica (§7.6 building). It restores the sealed versions with the planner of step 4, in its own region, verifying each file's trailer (ltx.Decoder.Verify: the CRC-64 FileChecksum), and requires the result to reach exactly N and to pass PRAGMA integrity_check. From that database it writes two files into the move's own generation: the snapshot, one level-9 LTX file [1, N], every page, at <location>g-<move id>/0009/<1>-<N>.ltx; and the anchor (step 7), one level-0 LTX file [N, N], every page, at <location>g-<move id>/0000/<N>-<N>.ltx. Both are written as the pinned writers write theirs: HeaderFlagNoChecksum set, pre- and post-apply checksums zero, the trailer's CRC-64 present (fact R5-2); the anchor's WALOffset is the WAL header size, which Verify requires (fact R5-1c). A build is two durable states, never one object (R7-4): first the build intent, <location>g-<move id>/build-intent.json, written before any PUT, with the encoding inputs the builder will use (the header timestamp, the page size, the commit, N) so that a replay (a restarted building) encodes identical bytes (R6-5: the bytes depend on the timestamp, TestFact_R6_5_AnchorReplayBytes); then, only once the snapshot PUT and the anchor PUT have both returned, the completed install manifest, <location>g-<move id>/install.json, with the artifacts' acknowledged identities (keys, the versionId each PUT returned, N, each file's CRC-64) and the verification results (integrity_check passed, the sha256 of the database file the build produced). Its keys are the shared moves.InstallManifest's json tags (claim Plan 6's internal/moves/install_contract.go; rev 7.22): v, op, host, snapshot_txid (the Go field N), snapshot_key, snapshot_version, snapshot_crc64, anchor_key, anchor_version, anchor_crc64, integrity_check, db_sha256, built_at. The completion predicate is the manifest's existence, never the intent's: rev 7.7 said "the install manifest records the inputs before the PUTs" and "building is done when the install manifest exists", so a crash after the inputs and before the artifacts left a manifest that satisfied the completion predicate (R7-4). A replay reads the intent, encodes the same bytes, and reuses a snapshot or anchor it finds already current under its key rather than writing again (the model's cold admission does the same, §7.14). generation.json is published only from the completed state (step 3). The cost is three passes over the database, each across regional S3 and the disk, plus a verification read, which T11 prices (§7.3).
3. generation.json names the snapshot: snapshot_key, snapshot_version, snapshot_txid = N, snapshot_crc64. These are the snapshot identity: the pinned root. A second version under the same key, from a PUT that completed late, is identical bytes and is never read.
4. The restore is litestream's planner (replica.go CalcRestorePlan, v0.5.14), rooted in the named generation and nowhere else. Its root is the newest current level-9 file of the generation whose MaxTXID ≥ snapshot_txid (a verified successor snapshot, step 8), or, when no such file is current, the pinned snapshot opened by snapshot_version. From current = root.MaxTXID it takes, among the generation's current files at levels 0 to 8, 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 and retention's deletes make the superseded files noncurrent on purpose. Rev 7.5 said "every level" and rooted at the pinned snapshot for good; after retention that root has no continuation (fact R5-3d) and the restore would have refused a healthy replica (R5-3).
5. Fail closed, by what the format supplies (R5-2). The pinned level-0 writer, snapshot writer and compactor all set HeaderFlagNoChecksum; PreApplyChecksum and PostApplyChecksum are zero in every file, and ltx.Trailer.Validate requires them to be with that flag (fact R5-2, litestream db.go:1948, db.go:2412, ltx compactor.go). There is no database checksum to compare after applying a file; rev 7.5's step 5 would have refused every healthy continuation, or been skipped. What the format supplies is per-file integrity: the trailer's CRC-64 over the file, which Decoder.Verify checks, and which SQLite's own PRAGMA integrity_check (CheckDB, backend_exec.go:313) complements over the result. The restore refuses, with a member-safe reason and a page, and never produces a database, when: no root is current and the pinned version is missing or its MaxTXID is not snapshot_txid; a file fails Verify; a current file starts beyond current + 1 once nothing extends the range (litestream's "non-contiguous ltx files": a gap); the result fails integrity_check; or, at an install, the result is not at the required final TXID. End-state checksums would need the three writers changed; Phase 1 does not change them, and the model carries none (§14.2.2).
6. What a gap means. Litestream does not advance past a failed upload, and a timed-out upload is retried with the same bytes 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.
7. The anchor: restore-to-replication initialization (R5-1). Litestream's open (db.go checkDatabaseBehindReplica) takes a fresh box's replication position from the newest remote level-0 file; a <db>-txid sidecar is read in follow mode only (fact R5-1e). A generation holding a snapshot and nothing at level 0 therefore starts replication at TXID 1: the first upload is [1, 1] (fact R5-1a), later writes land below N, and a cold restore rooted at N skips them and loses every write since the install (fact R5-1b; the R5-1 counterexample, confirmed). The remedy the pinned library supports unchanged is the anchor of step 2: a level-0 file [N, N] with every page, beside the snapshot. The open takes N as its position, the local WAL does not match it, and the next sync is a full upload at N + 1 (fact R5-1c); a cold restore afterwards holds every row (fact R5-1d). Every install of a generation writes its anchor before any process may open the database: a landing (§7.6 building), a push's install, a dirty rollback's install on the source (§7.8). The PUT must be acknowledged before replication opens, and the position is what the listing then shows (R6-1): litestream derives its position from the remote level-0 files actually present, so an anchor still in flight is no anchor, and an activator that opened on the strength of having issued the PUT would replicate from TXID 1. The activator therefore waits for the PUT's response, retrying the same bytes after its client timeout (the original may still land, identical), and only then opens; it never sets the position itself. Rev 7.6's model did (db.Pos = cur, R6-1); rev 7.7's restoreInit returns nothing until the anchor is acknowledged and reads the position from the listing (rule anchor-acked; the witness holds the anchor PUT across forty attempted opens and requires the host not to open, §14.2.5). A cold restore of a replica that has replicated since needs no anchor: the newest level-0 file is never removed by TXID- or time-based retention (fact R5-1f, asserted by identity), so a fresh box continues at exactly N + 1 (facts R5-1g, h; TestGate_AnchoredLineageThroughStore for three disk losses in a row). The wake writes one anyway whenever the restored TXID is above the newest current level-0 file, which costs nothing when it is not (the model's restore-anchor). Oracles never write one: a cold-restore check is the pure calculation of steps 4, 5 and 8 (R6-1).
8. Rotation, retention and root advancement (R5-3). Litestream writes a new snapshot [1, P] at its snapshot interval, and EnforceSnapshotRetention keeps the newest, returning minSnapshotTXID = the MaxTXID of the snapshot before the oldest kept one; the store then expires every level-1 and higher file whose MaxTXID is below it, and level 0 by time (fact R5-3a, b). After two rotations no current file continues from the pinned snapshot (fact R5-3f): a restore rooted there fails with "non-contiguous ltx files: have up to 1 but next file starts at 5" (fact R5-3d) while a restore from the newest snapshot holds every row (fact R5-3e). Protecting the pinned version alone does not protect its continuation; the root advances. A verified successor snapshot is a current level-9 file of the named generation with MaxTXID ≥ snapshot_txid that passes Verify; only the generation's own replicator writes under its prefix (C3a, and the generation name is the operation's), and a stale re-upload of a rotated snapshot is identical bytes under the same key, so the newest current one is the one litestream itself restores from. generation.json is not rewritten at rotation: the pinned root is the install's identity and the floor the successor must clear, not the only root (step 4). The sweep protects every current version under holder.generation and the pinned version (§6.4). The newest level-0 file survives every retention path (facts R5-1f to h; R7-3): compaction deletes its inputs bar the newest, and the expiry below the previous snapshot never takes the newest level-0 file, which is where a fresh box reads its position. Rev 7.7's model kept it only through compaction and expired it when the local position had run ahead of the uploads (R7-3; the model's newest-l0).
9. Writer sessions and epochs: two writers whose uploads could overlap never share a generation, every path that opens replication is admitted before its app starts, and a box never reuses its local database (claim rev 6.10 §6.4a; R7-1, R8-1 to R8-5, R9-1 to R9-5, R10-1 to R10-7). Litestream writes each file to a key built from the level and the TXID range only, and its PUT is unconditional (TestFact_R7_1_UnconditionalPut). So a writer A whose level-0 upload for [N + 1] is still in flight when A dies with its disk, and a writer B that restores the generation through N and uploads its own [N + 1], collide: if A's PUT lands last it replaces B's file and the next cold restore loses B's acknowledged writes; if it lands after B initialized its position and before B's sync, B's upload loop takes the remote [N + 1] as already uploaded and skips B's (replica.go Sync), and B's write is never replicated at all. lock.json cannot revoke a PUT S3 has accepted, and waiting for the lease to expire proves nothing about requests already signed. Claim rev 6.9 states the rule and this spec owns the data path: - AdmitWriter, one claim CAS before the app process starts (claim rev 6.10, R10-1; this reverses rev 6.8.2's order, which let an app acknowledge work before it had a session: a background worker committed and acknowledged, the app crashed before readiness, the old certificate still stood and the next warm admission purged the acknowledgement silently). The order is: the CAS; the purge and the restore of the baseline; the app start; readiness; uploads. A session belongs to the agent's replicator, not to the app process: an app that crashes or restarts while the same agent keeps replicating stays within the admitted session and is not re-admitted; a new agent process is always a new session, so an agent that restarts under a running app stops it (the replicator that was admitted died with the old agent) and its next wake is a new admission, which declares what the app acknowledged meanwhile. holder.session is the claim gen of the CAS that admitted the current writer session; holder.writer_box is the box it admitted (R9-2). Every path that opens replication makes this CAS: an ordinary wake, a committed move's target serving while the claim is still landing, a probe and a restarted probe, a reverted source, an opened rollback recovery, a push's writer (R8-2). The library's call is AdmitWriter(Admission{ObservedOpID, ObservedPhase, ObservedSession, ObservedGeneration, Box, Mode, NewGeneration, PredecessorCertified, RemoteMaxTXID, KeepStamp, Coverage, Region, PredecessorRegion}) (R10-4; Coverage since claim rev 6.12, Region and PredecessorRegion since rev 6.13, E 47426cc1), and this spec's model is shaped like it. It requires the observed op.id and op.phase (serving's "" compared literally, so a closure computed under serving fails once any operation starts), the observed holder.session and holder.generation, and op.exec to be this box, in every op kind (claim rev 6.8.1); it is refused in creating, deleting, parking, purging and placing (R9-4, R10-4): a create's first writer is admitted after CompleteCreate, under serving, and nothing writes while a placement runs. After a conflict the box re-establishes its evidence, the certificate, the exec handover, rather than re-reading alone. It writes holder.session = its resulting gen, holder.writer_box = this box, and a record in holder.admissions {session, box, generation, region, predecessor: {session, box, generation, stamp}, predecessor_region, mode, coverage, covered, writes_lost?} (claim rev 6.14 §6.4a item 1; the library's AdmissionRecord). region is where the new writer's generation keeps its objects, the admitted box's region; predecessor_region is the last record's region (before any record, the writer box's region, "" when the generation holds nothing anywhere, as after a create). The predecessor is the last record there, with its own session, box and generation; it never comes from the holder's fields, which a clean return has reset to the source's generation for the restore while the predecessor is still the target's writer (R11-4; rev 7.11 journalled the target's session and box with the source's generation, a writer that never was; INV-16). holder.admissions lives in the holder, so it survives every operation transition, release and new operation; its retention is deliberately conservative (claim rev 6.14 item 8, R12-6): covered records are trimmed from the front only, while more than eight remain, an uncovered record stops the trimming and everything behind it is kept, and there is no compaction. The admission never replaces the operation: kind, id, phase, participants, obligations and the rest of the journal are kept. - Failed starts are governed by a retry policy, never by another admission (R10-1). Within the admitted session the agent retries the app start with a doubling backoff from one step (1, 2, 4, 8, 16 steps in the model; seconds in production) up to five attempts; a start the environment is not ready for (config not rendered, the release not live) waits and counts no attempt. For a serving wake, at the fifth failure the box marks the host failed, abandons the session's start, and creates no new session for the host until an operator clears it (or a health signal does; the model's operator clears it after half a horizon). For a probe, the restarts share the probe attempt's 30 s readiness window (§7.7): the fifth failure or the window's end, whichever comes first, ends the attempt, the operation counts one of its budgeted attempts, and the host is not marked failed. Five attempts because the start's own faults (a missing key, a bad bundle) do not heal within the window and a crash loop would otherwise churn generations. The waits between attempts total 15 s (1 + 2 + 4 + 8); each attempt's own start and readiness time is on top, so five attempts are not a bound on a serving wake's duration, only on its count. An app's writes are never left in an interval without an admitted session: there is no app before the CAS, and the session stands until the next CAS. - A box never reuses its local database (R9-1). Before it starts, every admitted writer purges the local database with an error-returning purge; if the purge fails the writer does not start (a transient error: the next attempt purges again). It then restores from the certified remote baseline, under the lease, and starts the app on that; the restore is version-pinned and the planner's (steps 4 and 5). A warm database is never the baseline, whatever it holds: acknowledged writes it held that never uploaded are lost, and they are declared (below), never silently dropped. There is no lineage file and no provenance check. - Warm continuation is an admission in warm mode: legal only if closed/<holder.session>.json exists for the observed session and its max_txid equals the generation's remote maximum TXID over every level (PredecessorCertified). Any op.exec box may continue on it (claim rev 6.8.2): the certificate proves every upload of the session completed, whichever box made them. The admitting CAS moves holder.session forward, so that certificate names a dead session: a delayed, replayed or re-created certificate of any earlier session can never authorize anything again. The writer restores the same generation up to the certificate's max_txid, refusing to start on a restore that stops short of it, and reads its remote position at its first sync (litestream initializes it lazily). - Everything else is cold: no certificate for the observed session, a mismatched max_txid, any doubt. A cold admission is an installing CAS: in the same write a new holder.generation (NewGeneration) and holder.stamp = the resulting gen. The new generation is either the operation's prepared generation (a landing's or a push's g-<op id>/, built from the sealed archive with its snapshot [1, N] and anchor [N, N]; a dirty rollback's return generation), opened exactly once, by its probe, and never re-entered once it is holder.generation or an ancestor of it (a dead writer's uploads may still land in it); or a fresh id; warm passes an empty NewGeneration (R10-4). The writer restores the prepared generation from its pinned snapshot, or the predecessor generation's remote (holder.generation as observed) for a fresh one, in its own region; a fresh generation is empty until the writer's first upload, the full file [1, 1] of the restored baseline (fact R5-1c), made after the app started and before the marker; the bytes are captured once and a retry carries the same bytes (R10-7). When the observed session had no certificate and the baseline does not cover the predecessor's last acknowledged position, the CAS records writes_lost {box: holder.writer_box, generation, session, remote_max_txid} in its journal entry and the box raises an alert (R9-2): the predecessor's acknowledged writes beyond its uploads are gone with its database. When the baseline is a seal that covers the stopped predecessor (a landing's, a push's, a return's prepared generation, built from the stopped database's every page), there is nothing to declare: the admission's Coverage is sealed (claim rev 6.12, replacing rev 6.9.1's BaselineCoversPredecessor); the comparison is against the seal's own position, never a TXID from another region. A clean rollback's return with src_covered (§7.8) is covered too, clean-return: the unchanged target and the source's complete replica establish preservation, and the source's re-admission declares nothing. The coverage speaks for the target's probe session and for the source's cut session (cut.session, journalled at the stop) only: a later session of the recovered source that dies uncertified is declared like any other, and a return made clean only by a declared-lost target is not covered at all: it records writes_lost for every session the target was admitted into since the cut, certified or not (a probe session that closed cleanly and a warm continuation that died are two; the first's writes are durable only in the lost target's region, and no return lane carries either's; seed 33373 / 100,000, hidden until the session-scoped match of R12-1). Representation (claim rev 6.22 item 2, R13-3, R14-2): the admission entry carries writes_lost (one, the predecessor's session) and additional_writes_lost (a list, the other target sessions since the cut, and the source's cut session, under its persisted identity cut.session, when src_covered is false), each {box, generation, session, remote_max_txid}, unique by (box, session) across both: a target destroyed after the flip and before its first admission leaves the source's cut session as the predecessor itself, declared once (rev 7.14 declared it twice, through a separate field; INV-21); the caller supplies the list and the library records it in the admitting CAS; the admitting box raises one alert per declaration after the CAS and retries until delivered, and the console's durable loss record is the long-term copy, so trimming a covered entry never loses a declaration (the model: admissionRecord.AdditionalWritesLost, an alert each, INV-14 counts them). Only coverage "" with no certificate records writes_lost, and the record always names its coverage, certified or not. A seal built from the remote because the disk was gone (seal.from_db false, §7.4) stops at the remote's position and covers nothing beyond it: the prepared generation's admission has coverage "" and records writes_lost for the predecessor's acknowledged writes past it, as a cold admission from the remote would. The box is never inferred from op.exec. A write the host's remote holds, in any generation, is never declared lost while its writer's box is with us (INV-15): the lineage adopts the generation that holds it, a dirty return's lane, instead; a box declared lost may leave such writes behind, and so may a rollback whose target was declared lost (no return lane runs; the seal in the target's region is unreadable from the source); the record's remote_max_txid names where an operator finds them (§7.10). - Only warm and cold exist (R9-3). A first install, after a create or an adoption with nothing replicated, is a cold admission into an empty generation: no LTX file until the first committed transaction, never a zero-TXID file (TestFact_R8_3_EmptyBootstrap); the app starts first and may create its database, as the activator does today. There is no fresh, reserve, build or open transition. holder.generation is the only authoritative generation in every kind and phase: a probe or a recovery that opens replication is a cold admission that moves it, never an op-journal generation. A cold admission issues a new holder.stamp except when no writer was admitted since the current stamp was issued (holder.stamp > holder.session, the library's KeepStamp, claim rev 6.9.1): a landing's first probe after the flip keeps the stamp the flip issued and the target's record activated; a restarted probe, a push and a dirty return take a new one. - A cold admission's generation is unfinished until generation.json names it (claim rev 6.10, R10-2). Until then its baseline, the journalled predecessor, is part of the live set: no park-generation chore for it may be queued and the sweep never parks it (rev 7.10 queued the chore at the CAS, so a writer that died before its first upload could have its only baseline archived under it). The chores that retire superseded generations are queued by the marker's publication, through one PublishGeneration(observedOpID, observedPhase, observedSession, publishedGeneration, region, newID) CAS (claim rev 6.12, replacing QueueGenerationRetire): bound to the observed operation and phase like the admission, legal while serving and inside any operation a writer runs in (a restarted landing probe, a rollback's or a revert's source; R11-5), it requires holder.generation to be the published generation and an entry to name it, then walks every entry of holder.admissions in order, skipping covered ones (claim rev 6.22 item 5, R13-2; bounded by the list's length; warm entries are born covered, so it visits every uncovered cold entry): a predecessor whose predecessor_region is "" (it holds nothing anywhere) is covered with no chore; one that is the published, live generation again (a clean return's source generation, a republished lagging marker's) is left uncovered with no chore (covered, nothing would retire it once a later admission supersedes it, since that admission's predecessor is the last record and not the generation it restored from: seed 41914 / 100,000 left the source's generation as residue; rev 7.13 note 6, adopted); one whose objects are in the publishing region gets one deduplicated park-generation chore there and is covered; one whose objects are in another region stays uncovered, with no chore, and the walk goes on. The walk finds what rev 7.12 enumerated: the predecessor; behind a lagging marker, every generation of the chain of unfinished admissions between the marker's generation and the new one, and the marker's; and the predecessor of any earlier cold admission not yet covered (its writer died after its marker landed and before the CAS). Every cold admission publishes, a prepared generation's included (rev 7.12's model left a prepared generation's predecessor to the operation, R12-3): a landing's publication in the target's region leaves the source's generation uncovered, and the commit covers it (below). Its chores carry op = op.id inside an operation and op = "session:<holder.session>" while serving. Retirement happens only through it, and only of predecessors recorded in holder.admissions (R11-2). An adopted legacy host's generation is the location root itself, named by the sentinel "@root" so a chore can name it; "" and "@root" are one origin, so nothing retires the active legacy replica before a cold admission has created a successor and published it; holder.generation is "" for such a host until its first cold admission, and the adoption writes holder.writer_box as the box running the pre-release process, so the first cold admission's writes_lost names the writer whose unuploaded writes it leaves behind (R10-5, R11-3). That writer is the legacy identity (claim rev 6.24, R16-3): {session: 0, generation: "" (read as @root), box: holder.writer_box}, adoption's holder.session being 0; it is valid in both writes_lost and additional_writes_lost (a lost-target return after a move cut at session 0 declares it there), every other declaration has a session above 0, and a declaration always names a box: a created incarnation's first admission, whose predecessor has no writer (holder.writer_box empty), declares nothing (INV-24; rev 7.13 to 7.16 gave adoption session 1 and declared a boxless record for a created incarnation's first admission). Coverage, completely (claim rev 6.22 item 5, R13-2): a record is covered when its predecessor's retirement is in hand in the region that holds the predecessor's objects, and an entry becomes covered in exactly four ways, no other transition covers anything: at birth, a warm entry (its predecessor is its own generation, which nothing retires; the next cold admission's record names it and queues the chore), or an entry admitted while the claim already holds a park of the whole location in its predecessor_region: an unscoped park-replica, or a park scoped exactly to holder.location; a scoped park of an old incarnation or of a staging prefix does not count (claim rev 6.24 item 5; that park retires the predecessor: a rollback's return admitted after the release queued the target region's park, which the CAS that queued it could not see; seed 1036 / 3,000); by publication, above; by CoverRegionPredecessors(op, phase, region) in one of the three CASes that queue a whole-location park of region, every uncovered entry whose predecessor_region is region: the commit's park-superseded of the source region (§7.9), a rollback's park-superseded of the target region at the target's release (§7.8), and the console's release of a declared-lost target (§7.10), which retire those generations wholesale and so queue nothing; and by CoverParkedPredecessors(op, phase, region, generations) in the CAS that queues an at-rest park-sweep and in the CAS that acknowledges it, only the uncovered entries whose predecessor is one of the listed generations, the ones that sweep actually retires (a predecessor with a sweepable object at the queuing; one whose objects it retired on the way, at the acknowledgement): a sweep never covers a predecessor it did not park. A predecessor whose objects live in another region (a move's source generation, seen by the target's publication) is never queued into its region from here, since the rollback may still need it (seeds 1036 and 1296 / rev 7.12; witness wRollbackBaselinePreserved). INV-17: when a whole-location park of holder.location completes in a region, no record whose predecessor's objects were there is uncovered. A dead generation holding nothing yet still gets its chore in the publishing region, as does one whose objects were parked already: a dead writer's late upload or certificate may land in it within the chore's horizon. A failed cold start leaves an empty, unpublished generation; the next attempt is cold again and the marker it publishes retires it. - A marker that lags holder.generation (an absent marker is the origin "", for the sweep as for the restore, R11-1) is read through holder.admissions: when it names the predecessor of the latest admission, or the predecessor of a chain of admissions each of which died before its marker (two in a row happen: the second's purge failed after its CAS), that is the normal unfinished state, every generation of the chain and the marker's is live, and there is no alert. The run walk, in one region's bucket (claim rev 6.22 §6.2a, R13-1): the next admission follows each record's predecessor back from holder.generation to the marker's generation, newest first. A link whose generation keeps its objects in another region is passed over, covered or not: it holds nothing in this bucket, and its own region's park retires it (a clean rollback's fresh source admission R, admitted after the target region's park was queued and dead before its first upload, walks R, then the target's T in the other region, born covered under that park, then the source's S, and restores S; TestInterruptedCleanReturn walks that and R2 → R → T → S after it). A link in this region must be uncovered: a covered local generation is retired or being retired here, so reaching one as a needed baseline refuses the start and alerts (rev 7.13 read objects alone and would restore the marker's retired generation as an empty database; witness wCoveredLocalBaseline); an uncovered local link that holds an object is the baseline, the nearest such; one that holds none (a fresh generation that never uploaded) is passed over; else the marker's generation. The start restores what the walk selected (R14-1): the marker's generation through generation.json, as every ordinary restore; a run generation the walk selected rooted at [1, 1], its first full upload, never through the marker, which still names the run's baseline (rev 7.14's start selected R from R2 → R → S and then refused it because the marker named S, while the oracle restored it; the marker is never published backwards). The model's restoreCalc over the marker's generation and restoreWith rooted at [1, 1] over a selected one are the reference the selector F mirrors. An empty holder.generation for any other reason is unexplained missing data: refuse the start and alert. A holder.generation that holds objects has its marker published again (from the operation's build journal for a prepared generation, rooted at [1, 1] otherwise) and the chores queued, before anything else. Any other disagreement between the marker and the claim leaves the location untouched and alerts (§6.4). - A clean close is a one-use certificate. A writer session stopping cleanly first waits until every request it issued over its lifetime returned success to the client, within the client's wait (R8-5, R9-5, R10-7): every level-0 upload, every compaction and snapshot upload, every retention delete, and the start's own PUTs, the fresh generation's first upload and a warm restore's anchor, which enter the same ledger. A request the client timed out on, whether or not it later completed on the server (a lost response), one the server refused, and any retry after a timeout make the session uncertain for good; server completion and the client's response are distinct, and only the latter advances the start. A session whose start has not opened replication, or whose replicator died with its agent, certifies nothing. A session that can prove completion writes <location>/<generation>/closed/<session>.json {session, box, max_txid, closed_at} once (If-None-Match), then releases its lease; nothing of the host may run when it certifies (the unit stop kills the cgroup; a descendant that escaped it makes the close fail rather than wait, since its writes would be lost silently at the next purge, and the next wake is cold and declares). A certificate PUT not acknowledged within the client's wait ends the close uncertified: the PUT may still land, and a later wake that finds it may continue warm, since the drain was complete; the next wake is cold. No certificate is ever deleted or reused. Litestream's Replicator.Close drops the initial SyncAndWait error (internal/lease/lease.go), so certificate eligibility needs its own evidence, never Close's return value. An operation that takes the writer over, a push, a move's cut, a delete or a purge, drops a pending close: the generation is being replaced or parked. - Writers are bound to their generation. The replica client is constructed for the {holder.location, holder.generation, session} the writer was admitted with and refuses any key outside <location>/<generation>/: level-0 files, compaction, snapshots, retention. It never re-reads the generation, so a new admission is a new writer. A dead writer's late uploads land in the old generation, or in the current one before the session that superseded it opened; a cold successor has a new generation, and a warm successor exists only after the old session certified that every one of its requests had completed. - Conditional PUT alone would not do (R7 review): if A's file won a create-only race, B would have to detect differing bytes and fail closed; the remote-position shortcut would have to check identity; multipart completion would need the same condition; and a delete marker makes a key creatable again. Disjoint generation prefixes need none of that.

The model encodes all of it (§14.2.2): both completion orders and the race are witnesses whose late upload lands harmlessly in the dead generation with the rule and loses B's write without it; a dead session's certificate with a matching stamp and max_txid authorizes nothing; the collision during a committed landing's serving and during a probe restart is caught by the admission inside the operation; a non-exec writer is refused; a valid certificate over a stale local database restores the remote; a crash with an unuploaded write is declared; a stale closure during a delete is refused; an empty first wake and an empty install write no file; a retry that succeeds while its original stays unresolved, a maintenance retry, a lost response, a first-upload retry and an anchor retry write no certificate; a background acknowledgement right after the start, then a crash, is declared by the next admission (under rev 6.8.2's order it is purged silently); a crash before the first upload leaves the predecessor live until the marker names the new generation (with the chore at the CAS the predecessor is parked and the recovery restores nothing); a rollback whose source replica stopped short of the stopped database returns the seal. The cost is a restore at every wake, warm or cold, a full first upload per fresh cold generation (none for an empty one), three local passes for an operation's prepared generation as §7.3 prices an install, a restore per probe attempt, and a dead generation to park.

So:

• a request that completes late can only add an object to its own generation. A late snapshot or anchor PUT repeats identical bytes (another version, never opened); a late LTX PUT from an old executor, or from a dead writer of the same incarnation (step 9), lands in a generation the claim no longer names. Neither is ever restored into the current state;
• the claim moves to a new generation at its writer's cold admission, before the restore, the app start and the probe (§7.14; rev 7.12's wording here, "only after that generation is fully installed and probed", described rev 7.9's protocol and is superseded, R12-4). A restore still never meets a half-written generation: a prepared generation is complete, snapshot and anchor, before any admission opens it, and a fresh one is empty until its own writer's first upload, which is the baseline's full file and lands before the marker names the generation; a restore reads the baseline the admission names, never a generation under construction;
• 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 Replica.Restore, whose planner lists each level without versions and opens LTX files by key. Phase 1 needs three things beside it, none a change to the pinned library: the root rule of step 4 (the newest current successor snapshot of the named generation, else the pinned version opened by versionId, never another generation's or "the latest under the location"); the builder of step 2 (restore the staged versions, write the snapshot and the anchor with ltx.NewEncoder as litestreamfacts does); and the wake's anchor check of step 7. 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. internal/sim/litestreamfacts/ verifies the library behaviour this section relies on (facts R5-1 to R5-3, §14.2.6); §15 step 8 verified 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 with a lineage TXID and, separately, a replication position; transactions insert, update and delete; an LTX file carries its level, its range in replication numbering and the final image of every key it touches, and no checksum (R5-2); the serving process ships one level-0 file per sync at position + 1; compaction merges three level-0 files into a level-1 file and deletes the inputs, then rotates a snapshot [1, position] and enforces retention as step 8 states (R5-3). The restore is steps 4, 5, 7 and 8 as written: the root is the newest current successor snapshot at or past the pinned one, the position is read from the newest current level-0 file, and the anchor is written when the restored TXID is above it. 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; it drops the anchor (restore-anchor) and a snapshot-only install that wrote, replicated and lost its disk loses every write since the push; it drops root advancement (root-advance) and a host whose replica rotated four times refuses to wake (§14.2.5). Rev 7.4's model carried a full transaction history in every object, which no LTX file has; rev 7.5's carried a whole-state checksum no pinned file has and a position that litestream never derives from a snapshot (R5-1, R5-2).

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_key","snapshot_version","snapshot_txid","snapshot_crc64"}: the pinned root, the install's snapshot identity and the floor a successor snapshot must clear (R3-1, R4-1, R5-3) | | <dbPath>.gen | beside the local database | after a restore completes | the generation's name as plain text, one line: the format main already writes (hostbox.WriteGenerationMarker). It carries no incarnation and no location; the claim's holder vouches for both (Paul's ruling, moves Phase 1 Plan 3) | | .files-gen | inside the files directory | last, after files, <host>.env, timers and the carried registry columns are all durable (§7.6) | {"op","incarnation"} |

generation.json is the one reused key a generation writes: everything else lives under the generation's own prefix. Without the condition, an earlier publication that completes late puts an older generation back: the claim names the new generation, the bucket names the old one, and every wake and recovery probe refuses: the start check compares the markers with the claim's generation and refuses forever (model 29; the model finds it after a push in 2 seeds of 100,000, §14.2.5). With the condition the late write fails with 412 (claim §13 rows 5 and 6), and the later generation stays.

All three are protocol metadata: excluded from the archive, from every content digest, and from F4's definition of the files directory (§6.1). Absent everywhere means origin. The claim's gen is a per-write version (claim spec §2), not a generation, so it never appears in a marker.

The authoritative region (claim rev 6.5 §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; every current version under the generation, successor snapshots and anchors among them). 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 target's probe is admitted | the source's region: holder.generation is still the pre-move generation, and the target's prepared generation is not yet named | | landing from the target's probe's cold admission on, committed or not | the target's region: holder.generation is the generation that admission chose, the prepared one or, for a restarted probe, a fresh one restored from it (§7.14; rev 7.11's row said "before the commit", R10-3) | | restoring, clean, from the return CAS on | the source's region: the return CAS named the source's generation again for the restore, and the source's re-admission moves to a fresh generation there | | restoring, dirty, until the source's probe is admitted | the target's region, for holder.generation, which is still the target's last admission: a dirty return resets nothing (only a clean return's CAS names the source's generation again), and the generation stays the target's until the source's probe is admitted. In practice nothing is live there: the target stopped, and the target region's whole-location park is queued at the release with the records whose predecessors are there covered in that CAS (§7.8). The return generation is built in the source's region but not yet named (rev 7.12's row assigned the pre-move generation here, before any source admission, R12-4) | | restoring, dirty, from the source's probe's cold admission on | the source's region, for the return generation, which that admission named; its record's predecessor is the target's writer, in the target's region, born covered under the target region's park | | 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:

1. the box's own <location>generation.json (absent is origin) to name the generation the claim expects: holder.generation, as the admission's CAS left it, for every start; a probe's first admission publishes the operation's prepared generation (the move id, the rollback id, the push id) and a restarted probe's a fresh generation restored from it (§7.14; rev 7.11's clause named the prepared generation for every probe, R10-3); a lagging marker is read through holder.admissions (§5.1 step 9); and its incarnation to be the holder's;
2. .files-gen, when the files directory exists, to name the holder's incarnation and either holder.generation or its cold predecessor (the newest cold admission into holder.generation, warm self-links skipped), which is the prepared generation a restarted probe was restored from; no older generation counts;
3. <dbPath>.gen to name the same generation, exactly: the plain name carries no location, which the claim's holder.location vouches for. A warm database that does not is from an earlier stay on this box: the activator parks it (§6.3) and restores cold.

Rev 5's check compared the three markers with each other only. Astra showed (J2-R2-8) that after a commit, before the source is retired, the source's own three markers still agree with each other, so the "third fence" the model reported in rev 5 did not exist in the text: the model's check was stronger than the spec. Rule 1 makes it exist. A mismatch refuses the wake with a member-safe reason and pages. A marker that merely exists proves nothing (codex R2-6). The bucket read rides the wake's existing lease round trip to the same prefix. This replaces "staging wins" (backend_exec.go:1581-1588); promoteStagedReplica is deleted (M15).

5.2 Holds

A hold status is one the edge does not serve (internal/edge/edge.go:595), ticks refuse (activator.go:2785-2789), and no ordinary wake reaches: moving (source), landing (target), restoring (source, recovering), releasing (target, during a rollback). The routes table gains an additive column, hold_op, set whenever a hold is written. Leaving a hold is one conditional statement:

UPDATE routes SET status='ready', hold_op='' WHERE host=? AND hold_op=?

A late write from a finished operation matches nothing (codex 6). Reconcile mints held rows for every participant the claim names and never mints ready while the claim holds a move operation (moving, reverting, landing before the commit, or restoring) (§9.6, §19 K9).

5.3 Stop evidence (codex 1, R2-1, R2-2)

The execution right moves only on stop evidence. Rev 2 relied on the activator's in-memory FenceAndStop (internal/activator/maintenance.go:50). Round 2 showed two gaps: a flat child's descendant that outlives it (childProc.Stop waits for the main process only, backend_exec.go:1502-1543), 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 §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 > complete process tree, closed replicators and no remaining database/WAL/SHM > holders. An absent host cgroup is insufficient where an earlier spawn > could escape containment.

and

> Reconstruction uses a cleanup-only operation that can reopen, identify, > kill and drain an existing populated cgroup without granting spawn > authority. PrepareStrict remains the empty-group spawn API. A pre-move > best-effort child is not certified stopped by ordinary parent exit.

PrepareStrict refuses a populated group (internal/cgroup/strict_linux.go:206), so the cleanup-only operation is a separate call, cgroup.ReopenAndDrain.

Every spawn under a move is strict. Flat children already run in a per-host cgroup, carlos-exec@<host> under the agent's delegated subtree (internal/cgroup/cgroup.go:37, :243; Delegate= in internal/host/units/carlos-edge.service), but placement is best-effort: a failed placement spawns "unaccounted" in the agent's own cgroup (cgroup.go:248-252). The strict path exists (internal/cgroup/strict_linux.go: PrepareStrict, Populated, KillAndEmpty). Under a move, every spawn of the host (the source's recovery, the target's probe, and the source's ordinary wakes while the claim says moving) uses PrepareStrict and refuses to spawn if it cannot. A nested child already runs in its own carlos-instance@<iid> unit.

The source's pre-move child. Its cgroup placement was best-effort. The source's readiness (§7.3, S2) therefore requires its current or next child to be strict: before ready, it stops an awake non-strict child (an ordinary idle stop) so the next wake is strict.

Evidence is ReconstructStopEvidence(host), a new activator call that reads only the box's current state, so it gives the same answer after an agent restart as before:

1. Kill and drain the tree. Flat: write cgroup.kill on carlos-exec@<host> and wait until cgroup.events says populated 0 (KillAndEmpty). Nested: stop carlos-instance@<iid> (and its seed and sidecar units) through the instance-control channel and require each unit inactive and its cgroup unpopulated.
2. No stray process. The agent's own cgroup (cgroup.procs of the service's leaf) holds only the agent's own process. A strict spawn never leaves anything there; anything else is unattributable and refuses evidence with an alert.
3. No open database. No process on the box holds the instance's database, WAL or SHM open (a scan of /proc/*/fd for the paths, restricted to the carlos uid).
4. Lease released. The host's lock.json lease (internal/lease/lease.go:86) is absent, released, or expired by more than the lease's renewal margin.
5. Replica final. After 1 to 4, a final checkpoint of the local database (if any) into the box's own instances/<host>, and its sha256.

A durably never-spawned operation. If the box's journal for the operation shows no spawn was ever attempted (the target's landing_phase before probing), steps 1 to 4 still run: an empty tree proves the same thing whether or not a spawn happened. "No entry in memory" is never evidence on its own (codex R2-2).

The box writes the result to the deployment bucket at moves/<acct>/<app>/<host>/<op id>/stopped-<role>.json: box label, incarnation, the claim gen it read, each step's observation, and the database, files and timers digests. It then CASes the claim's execution holder to none (§19 K3). The next holder reads the evidence and the claim before it starts anything.

Evidence also starts a clock (model 1). Ordinary replication is the one storage write claim C3 does not bind to a version: the serving process's litestream PUTs go to reused keys (litestream v0.5.14 LTXFilePath, names by TXID range, restarting at 1 for a new lineage). A PUT signed before the evidence can still complete afterwards. So every retirement of a location that a replicator wrote acknowledges only after a verification listing taken later than evidence time + H, where H is the late-completion horizon (S3 refuses a request whose signature is more than 15 minutes old, so H is 15 minutes plus the longest request). The model drops this rule and finds residue in a freed host's namespace.

6. State inventory

6.1 Files on a box (codex R2-9)

| # | state | where | disposition | |---|---|---|---| | F1 | SQLite DB, WAL, SHM | <DataDir>/<host>.db (provision.go:1219) or nested InstanceDir/<host>.db | carried as the replica; installed as a generation (§7.6) | | F2 | litestream meta dirs | <db>-litestream, .activator-<db>-litestream (backend_exec.go:1570-1571) | rebuilt on restore | | F3 | <dbPath>.gen | beside the DB | protocol marker (§5.1); local-parked with the database, flat or nested | | F4 | files directory | flat: strings.TrimSuffix(dbPath, ".db") = <DataDir>/<host>/; nested: every entry in InstanceDir except F1 to F3, F5 to F11 and #199's markers | carried (§8), excluding .files-gen | | F5 | .files-gen | inside F4 | protocol marker (§5.1), never archived or digested | | F6 | <host>.env | paths.go:50; CARLOS_ADMIN_TOKEN (admintoken.go:115) and operator overrides | carried in the archive, as its own entry | | F7 | <host>.config.env | syncexec.go:71-76 | rendered for the held row (§9.1), pinned by T3 | | F8 | <host>-sidecar.env | paths.go:51 | refused (§7.1) | | F9 | launch files, sockets, log sockets, exit records | provision.go:1282-1294 | rewritten per start | | F10 | quarantined restore <db>.corrupt | backend_exec.go:313-324 | local-parked with the database | | F11 | layout journal | <DataDir>/layout/<host>.json (provision.go:1303) | the cut waits while present (movespass.go:447) | | F12 | operation journals | <DataDir>/.moves/<host>/<op id>/ (new) | protocol state for this box's phases (§7.6, §7.8); parked at finalization |

6.2 Registry state (codex 16)

Every routes column (internal/registry/registry.go:34):

| column(s) | class | Phase 1 | |---|---|---| | Host, Slug, Kind, App, Account, Region, Channel, Environment, Hibernate, StatusNamed, Steering, Gate, Seed | reproduced | from the record by routeFor (internal/provision/reconcile.go:364-376) | | Socket, DBPath | reproduced | derived for the target row's layout; Phase 1 lands flat (routeFor mints flat) | | Provisioned | reproduced | true | | Status, hold_op (new) | protocol | §5.2 | | Replication | carried | box-local (registry.go:138-145, reconcile.go:1100-1113) | | NextDue | carried | the app's own next wake, probed at stop (activator.go:2019-2030) | | Version, PrevVersion | reset | materialized for the held row (§9.2) | | LastError, DNSStatus, DNSCheckedAt, CertExpiresAt, CreatedAt | reset | recomputed by their passes | | Caps, Unit, Backing (unit), Platform, Tunnel, FleetBox, Pool, Canary, Addr, Addrs, Health | refused if set | not the platform's to move | | Replica, Replicas | refused | a replica, or a home with replicas (Q2) | | IdleSeconds, MaxRunSeconds, Args | n/a | sidecar columns |

The timers table (registry.go:565-579) is carried as a snapshot (§9.4).

6.3 Other host-keyed state (codex R2-9)

| state | where | disposition | |---|---|---| | restore-verification verdict | control/restore-verify.json, hosts[<host>] (internal/dbverify/dbverify.go:10, :33) | the host's entry is removed at every install (landing and dirty rollback), so an earlier generation's "ok" never vouches for a new one; the next drill writes a fresh verdict | | config ack | control/config-ack/<box>/<host>.json (internal/appconfig/configack.go:111-118) | move-bound acks (§9.1); the source's parked at finalization | | copy receipts | move-receipts/<host>/<op id>.json (source bucket) | keyed by operation | | snapshots | move-snapshots/<host>/<op id>/ (source bucket) | §8.3 |

6.4 Parking

Phase 1 uses the claim spec's park (§6.2 there) and local retirement (§6.3 there), with the move's own destinations:

• One destination per retirement event (joint D5, N7). Superseded data goes to superseded/<op id>/<host>/<retirement id>/{instances,moves}/, and local state to .parked/superseded-<op id>/<host>/<retirement id>/. The landing's park of an earlier stay, a failed target's cleanup, the source's retirement after commit and each staging retirement are separate events with separate manifests, even inside one operation. The model drops the retirement ids and the park never finishes: the second event finds the first event's immutable manifest and stops on unlisted keys.
• What a move parks is its location, not the host namespace. The landing's park of an earlier stay, the source's park after commit, a rolled-back target's park and a push's park all name holder.location in their own region (C3a); staging parks name moves/<host>/<op id>/.
• Exact versions (joint N1, J2-R2-6). The snapshot takes every version under the location, noncurrent included. The manifest records two sets (claim §6.2): the archive set, every non-marker version, copied by versionId; and the deletion set, every version, delete markers included, which is what a retry replays, by VersionId. The model replaces version deletes with bare-key deletes (delete markers on a versioned bucket) and finds parks that never 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 (<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 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. Installation stamps (claim rev 6.5 §6.4, R3-3, R4-2, R5-4): an installation's stamp is the claim gen produced by the CAS that made it current, and that CAS writes it into holder.stamp (claim rev 6.5 §2), so the claim is the durable record of every installation's stamp and the recovery source for every box. The CASes that install, and so write holder.stamp, are: a create's serving CAS (claim §5.1 step 4); adoption (claim §9); a landing's flip (§7.5); a push's probe CAS (F7); a dirty rollback's source probe CAS (§7.8); a reinstall after quarantine. A dirty rollback installs a new generation and never keeps its predecessor's stamp (rev 7.5's model did, R5-4). The stamp is 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}. Initialization (claim rev 6.5 §6.4): a box creates or refreshes its record only from a fresh claim read under the guard, only when that read names it op.exec or the landing participant (the phase table, §5.1), setting active_stamp = holder.stamp: a create's first wake, adoption on the serving box after the adoption CAS, a landing in its checking phase, a box whose record was lost, on restart. Rev 7.5's model initialized the record from the claim revision at reconciliation, which intervening claim writes change (R5-4). No local record: refuse. Every host-state writer (config sync, release adoption, the activator's admission) carries {incarnation, stamp} captured from the box's local record when it selected its work (claim rev 6.5's answer 1: the fresh claim read under the guard is still required, for the incarnation, the operation and the config and release identity, but the stamp is the selection's), and is admitted only if its stamp equals the active stamp; a lower stamp, a retired stamp, any stamp while the active stamp is none, and any stamp while the box has no record, are refused (rev 7.5's model admitted a writer when no record existed, R5-4). Two retirements, named at every call (claim rev 6.5 §6.4): retire-artifacts(S) parks the local artifacts tagged with stamp S and moves no stamp: neither active_stamp nor retired_stamps changes (rev 6.3 had it add S to the retired set; rev 6.4's answer 2 withdraws that). It parks by tag: every local artifact carries the stamp of the installation that produced it (claim §6.3's inventory), retire-artifacts(S) parks the ones tagged S and leaves the rest, and a caller that expected another tag has made a mistake the model records (R6-4). Where the files directory is carried into the new generation (a push, F7; a landing's restored phase; the activator's park of a warm database before a cold restore) the retirement is of the database alone. It is what a landing that has activated its own stamp in checking uses in local to park its predecessor's database, files and <host>.env, what the activator uses on a warm database from an earlier stay, and what a dirty rollback's install uses on the source, whose pre-move stamp is still active at that point. Only two things move a stamp: activation, which puts the old active_stamp, if any, into retired_stamps and then sets the new one (so the dirty rollback's pre-move stamp retires when its probe CAS's new stamp activates), and retire-installation, which moves active_stamp into retired_stamps, sets none and parks every artifact; it is the local park at a delete, a move away (the source's finalization, §7.9), a rolled-back target's cleaning and quarantine (CC12). Nothing calls retire-installation to clean up a predecessor: rev 7.5's §7.6 reused the general local park in local, which read literally retires the installation checking had just activated and refuses its own probe (R5-4). A cold admission is an installing CAS too (claim rev 6.9 §6.4a; §5.1 step 9, §7.14): it writes a new holder.generation, a new holder.stamp and holder.writer_box in one write, with the predecessor's {session, box, generation, stamp} journalled in the same write; the box's record activates the new stamp from its next fresh read, and the carried files are retagged with it at the CAS, whether or not the start completes (the first rev 7.9 model left the files under the dead writer's stamp, and the next dirty install parked an artifact of a retired stamp, seed 453 / 30,000; rev 7.10's first model retagged them only at the start, seed 62 / 300); the restored database carries it; the dead writer's stamp retires with it. The purge of the local database that precedes every restore (§5.1 step 9) is not a retirement event: it deletes a file no installation will run again. There is no lineage file (rev 7.10). The admission's writer opens the new generation without a certificate of its own; its clean close writes the first one. The return to source (claim rev 6.5, R6-4). holder.stamp always names the installation op.exec should run, so every CAS that changes op.exec writes holder.stamp in the same write: a CAS that makes a new installation current writes the gen it produces; a CAS that makes an existing installation current again writes that installation's own stamp, taken from the op journal. The flip records the source's pre-move stamp S in the journal (op.source_stamp) as it writes the target's F; a rollback's return CAS (§7.8 claimed: op.exec back to the source) writes holder.stamp = S, never F. The source's initialization then finds holder.stamp equal to its active_stamp and changes nothing; a source whose local record was lost (a reboot) re-initializes to S from the same fresh read. A dirty rollback's install runs under S, its artifacts tagged S; the probe CAS issues R with holder.generation, and activation of R tags the generation's artifacts R and retires S. F was only ever active on the target and retires there (retire-installation at cleaning). Rev 7.6's model returned execution with holder.stamp still F, so the source activated the target's installation and tagged its artifacts F (R6-4); rev 7.7 encodes rev 6.5 and records any activation of a stamp the claim issued for another box as INV-6 (return-stamp, with a witness whose source has lost its record, §14.2.5). Op ids are opaque and never compared (claim rev 6.1 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.5 states it (every installing CAS writes holder.stamp, initRecord under the guard, refusal without a record, activation the only move of the old stamp, retire-artifacts a named no-op on the record), 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 namespace begins (codex R2-6).

The straggler sweep (J2-R2-1, CC15, model 17; claim rev 5 §6.2a). S3's signature limit bounds when a request is accepted, not when it completes (claim C3a), so a request accepted before a retirement's horizon listing can still land after it. Within one incarnation the restore contract (§5.1) makes such a straggler harmless to data. It is still residue, and no later retirement of that location may ever run. Claim rev 5's at-rest sweep owns it: for a host with no operation running, each region's box lists the host's namespace and parks what is not live, as a further retirement event, under a park-sweep obligation the sweeping box owns. The chore carries a persisted park scope (claim rev 6.23 §2; R13-4, R14-5, R15-1): {location, incarnation, evidence_at, request_limit}, written at the queuing CAS, so every retry, an agent restart's included, uses the same location, archive incarnation and original evidence time; a retry's own clock is never evidence, and a restart never starts the horizon again (rev 7.13's model kept the evidence time in a box-local map that the restart cleared; witness wParkScopeSurvivesRestart). location is exactly one of instances/<host>, instances/<host>/<incarnation>, moves/<host>/<op id> (a move's staging or a rollback's return lane, the op id with no /) or moves/<host> (used by a delete's park of the staging namespace, §5.2, and by an at-rest sweep, each while no operation stages there; claim rev 6.26, R17-2), nothing else and no trailing / (the model's INV-23 checks every scope against that grammar). incarnation names the archive: the location's own, the staging op's holder incarnation, or, for a free host's moves/<host> sweep, the newest retired incarnation. evidence_at is always the original evidence or fencing bound, never the cleanup's start time: the cut's stop evidence for the commit's park of the source region; the release's stop, or the declaration's fenced_at, for the target region's; a staging lane's own seal bound, the time after which no staging writer, its lease holder included, can still write (the seal plus the staging lease), persisted when the lane is sealed or fenced; the sweeping box's complete listing for a sweep; the publication that supersedes a generation for a generation chore. A chore queued without a scope (a delete's or an adoption's park-replica, whose CAS has no evidence time yet) binds one in a CAS before its first step runs, once its stop evidence is in hand, and never again; INV-22, no remote chore runs a step unscoped. One deadline for every scope (R15-1): acknowledge only after a verification listing later than evidence_at + H, with H = the signature-age limit plus request_limit (claim §6.2a, §2: 15 minutes plus 120 s in production; sigAgeH + requestLimitH = horizonH in the model, 45 + 15 = 60 steps). There is no separate staging contract: rev 7.15 bound a staging park at cleanup and then kept the seal's quiet time instead of that bound, so a lane sealed at step 100, deadline 560, whose cleanup first ran at 600 would have waited until 660 (witness wStagingScopeDeadline: the cleanup acknowledges at once, through an agent restart, since the persisted deadline has passed). Rev 7.14 wrote evidence_at + request_limit here, dropping the signature-age allowance (R14-3). The sweep parks at once and acknowledges, with its straggler pass, only after a verification listing later than evidence_at + H (platform-1e's answer to rev 7.14 note 2: a park-sweep is a retirement event and is not exempt from the horizon). On a serving host the chore's op is session:<holder.session>, as for PublishGeneration. On a free host (no holder) the sweep is a holderless sweep (claim rev 6.15 §6.2a): one CAS sets op = {kind: parking, id: <new op id>, intent: {park_sweep: "v1"}} with no exec and no holder and queues only scoped remote chores owned by that op; it is the only holderless claim that may carry obligations, so it blocks free's successor create while it runs (the create waits, it is not refused), and its last acknowledgement frees the claim again in the same CAS (FreeAfterPark), keeping quiet_after (witness wFreeSweepVsCreate; INV-20: a create never claims a host while a park of its namespace is outstanding). Another region's sweep while the op runs joins it with its own scoped chores under the same op id (R14-4, platform-1e's preferred reading of rev 7.14 note 1; TestJoinHolderlessSweep has two regions' residue parked under one op and one FreeAfterPark); any other operation running suppresses new sweeps; the console's recovery pass leaves the op to its runners and only replays FreeAfterPark for one whose chores are all acknowledged. It discovers locations from the namespace itself (claim rev 6 §6.2a, R3-4), not from retired_incarnations, which is capped at 32 entries and exists only to stop an incarnation being reused: it lists instances/<host>/ with delimiter /, every page, refusing on a listing 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. What it finds is grouped by the location it belongs to (claim rev 6.24 §2, R16-2): each incarnation location its own, the legacy instances/<host> (a level directory or generation directly under the host prefix, never a child incarnation), moves/<host> for staging residue; one chore per location, scoped to that location with its archive incarnation (the location's own; the holder's for the legacy location or the staging sweep; the newest retired on a free host), and the archive is written under that incarnation. A park executes strictly within its scope: its listing is confined to the scope's namespace (an instances/… scope never lists or parks anything under moves/, the legacy instances/<host> scope excludes child incarnations, a staging lane's scope only its own lane), and every key a chore would archive must be a member of its scope (the model's INV-23 checks membership for every reference a park archives or deletes, in the manifest it builds and in a persisted manifest it replays, whatever rules are on, and an out-of-scope reference is never acted on, R17-1; rev 7.16 scoped the whole instances/<host>/ listing as instances/<host> under the serving incarnation and archived a deleted incarnation's late object from there; witness wSweepScopeMembership). The same confinement governs a delete's parks, which cover the deleted incarnation's own location and the staging namespace, never the whole host prefix (claim rev 6.25 §5.2); an older incarnation's residue is this sweep's. The live set is region-qualified (claim rev 6.5 §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); within holder.generation every current version is live, the successor snapshots and the anchor among them (§5.1 steps 7 and 8); and, in claim rev 6.4 §6.2a's words, a child prefix that is not an incarnation id (64 hex) belongs to the host prefix's own location: a level directory 0000 to 0009 or a generation prefix g-<op id>/ directly under the host prefix is the legacy location's, never an incarnation location (the model's locationOf; rev 7.6's first baseline misread g-<op>/ under a legacy host as an incarnation and swept the live generation, caught in 2 seeds of 3,000); 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, except for the one disagreement that is normal (claim rev 6.10, R10-2): a marker that names the journalled predecessor of the latest admission, or of a chain of admissions each of which died before its marker, while holder.generation is ahead of it; then every generation of the chain and the marker's are live, protected, and no alert is raised (§5.1 step 9). 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.

moves/<host>/ too (CC20, in claim rev 5.1). Claim rev 5's list left out staging. A staging request accepted before its lease ended can complete after the staging cleanup, and after the move's release nothing lists moves/<host>/<move id>/ again. The sweep also parks everything under moves/<host>/ while no operation runs, when no move is staging there. The model drops this and leaves staging residue for good (§14.2.5).

A periodic listing per host and region is the cost (rate: once a day, and after each operation's release). The horizon of §6.2a stays: it is what makes INV-10 hold when an operation ends, for every request that completes within H; the sweep covers only what completes after it. The model checks both: INV-10 at every release and free, excepting only versions created after H, and INV-10 everywhere at the end of the run.

7. The move

7.1 Request and refusals

POST /api/cli/apps/{account}/{app}/instances/{host}/move {"region":"uk","cut":"auto"|"manual"}, operator-only (§12). The door CASes the claim from serving (holder = this incarnation, execution holder = the source box) to moving with op id = the move id (§19 K2). The target box is named in that CAS (region HA L15, ruled H12): the door computes region HA's choose(eligibleBoxes(region, pool), app) (spec 1 §5.2: prefer a box running no instance of the app, then the most headroom, then the SHA-256 tie-break) over the roster and the edges snapshot. Phase 1 scope (rev 7.20): a move into or out of a region with more than one eligible box is refused at the door, with M-C21, until region HA's own model and plan cover multi-box regions; so in Phase 1 choose() always names the region's one box, and the source is the one box of its region. The refusal is a scope rule, not a safety rule: the protocol below is written for any target box the start CAS names. The choice is made once and recorded as op.participants[1] and op.intent.target; readiness (T8, T9), evidence, install and recovery bind to that box, and nothing substitutes another box: a target that cannot complete is replaced only by an explicit fenced transition (§7.10, L14), never by recovery picking a new one (P5-D2, A1-10). It is refused (400 or 409, with the sentence), and every box step re-checks:

• not exec-backed kind:"instance", addr-backed, pooled, fleet-placed, non-hibernating (internal/console/apiinstancemove.go:53-72);
• a replica (:187-190, provision.go:978-980), or a home with replicas (new);
• a target of home on a console without host claims, or a home whose box sets a region code of its own (apiinstancemove.go:203-209; F2, rev 7.24, Ruling R1), the current region, or one outside the manifest's regions (apiinstances.go:1797). A home target is named by the home's configured name; there is no home keyword (Ruling R3);
• a source <host>-sidecar.env, or any refused registry column (§6.2);
• a private store bound to the instance's environment (codex 12; F4);
• the claim not serving, or any box in either region below the protocol floor (§11).

7.2 Record fields

Additive under move (provision.go:907-917). The claim carries the cross-operation serialization (§19); the record carries this move's phase journal, because only a move reads it.

"move": {
  "id": "mv_…", "incarnation": "…", "from": "", "to": "uk", "cut": "auto",
  "state": "landing", "requested_by": "…", "requested_at": "…", "updated_at": "…",
  "ready_at": "…",
  "inputs": {"bundle_etags": {"…": "…"}, "overlay_etag": "…", "release": "…",
             "files_plain": "sha256:…", "env_report": "sha256:…"},
  "cut_phase": "flipped", "cut_at": "…", "cut_budget_s": 95,
  "source": {"replication": "stream", "next_due": 0, "db_sha256": "…",
             "files": {"plain": "sha256:…", "sealed": "sha256:…", "bytes": 1824, "entries": 4},
             "timers_sha256": "…", "evidence": "…/stopped-source.json"},
  "flipped_at": "…", "landing_deadline": "…",
  "landing_phase": "probing", "landing": {"installed_db_sha256": "…"},
  "committed_at": "…", "opened_at": "…", "source_parked_at": "…",
  "rollback": {"id": "rb_…", "requested_at": "…", "reason": "…",
               "target_phase": "returned", "dirty": true, "evidence": "…",
               "source_phase": "probing", "recovered_at": "…", "opened_at": "…",
               "target_parked_at": "…", "release_deadline": "…"},
  "reason": "…"
}

Every box transition is a CAS on the record guarded by move.id and move.incarnation, and revalidates the claim's op id, kind and phase first (§19 K5).

7.3 Preparing and readiness

Staging layout (codex R2-7). Each artifact class has its own subprefix under moves/<host>/<move id>/ in the target bucket:

| subprefix | content | writer | |---|---|---| | replica/ | the mirrored litestream replica; the only subtree MirrorPrefix touches | source rounds | | files/ | sealed archive and manifest | source | | timers/ | the timers snapshot | source | | move.json (outside every subtree) | {"move_id","incarnation","host","from","to"}, create-only | source, before the first round |

MirrorPrefix runs on replica/ only, so it can never delete an archive, a snapshot or move.json. Landing installs only replica/ into instances/<host>/ (§7.6). Receipts are move-receipts/<host>/<move id>.json in the source bucket.

The staging-work lease, sealing and draining (joint D4, N2). M17's push-only grant stays: the source can put and delete in the target's moves/* but cannot read it, so it cannot hold the target's lock.json. Exclusion between staging writers uses the claim's shared staging-work lease in the deployment bucket, keyed by target region and host (claim C3). Every round, the final round and every staging retirement take it first, then revalidate the claim's op id and phase. That is enough for two workers of one operation (a restarted agent beside a stalled one), but a lease cannot fence a request already signed, so staging safety rests on two further rules:

• Seal by version. Each PUT's response carries the new object's VersionId. The final round records the exact versions of replica/…, files/… and timers/… in the claim's op journal: the seal. Landing copies those versions by versionId and nothing else. 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, and sign at the check (model 14, model 18). 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. The signature is computed at that check, with the check's time as its X-Amz-Date, and never recomputed, including by the SDK's automatic retry, which must resend the original signature (claim rev 5, CC19): a pause between the check and the send, even a whole-VM freeze that no in-process bound can promise against, then ends in S3 refusing the request once its signature is older than the signature-age limit (403 RequestTimeTooSkewed, verified, §15 step 8). SafeUntil therefore leaves room for the signature's whole valid life: SafeUntil = Until − clock skew − 15 min. Rev 5's rule signed at send time; the stricter model freezes a box between a passed check and the send, and the write lands after the staging cleanup (1 seed in 100,000; CC19, §19.4).
• 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. That bound holds only because of the rule above: a request is signed at a check made before SafeUntil − 15 min, and S3 accepts it only within 15 minutes of that, so it is accepted before Until and completes within H of acceptance, or it is a straggler that completes later, which only the straggler sweep can retire (§6.4).

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 report moves/<acct>/<app>/<host>/<move id>/source.json: every variable of the composed launch environment its next spawn would get, which is childEnv (backend_exec.go:1158-1196) over instanceEnv (:1135-1153) plus the agent-owned variables (:975-993), including the non-CARLOS_* variables childEnv inherits from the agent (codex R2-8). Each value is reported as an HMAC-SHA256 under a key derived (HKDF) from CARLOS_SECRETS_KEY, so the report reveals names and equality only.

Readiness report (target). For every record whose move.to is its placement, the target writes moves/<acct>/<app>/<host>/<move id>/target.json:

| check | passes when | |---|---| | T1 protocol | this box is at or above the protocol floor (§11) (codex 7) | | T2 secrets key | this box publishes secrets_key_fp equal to the console's (§10) | | T3 environment | the target composes the environment it would launch with for a flat held row on this box (rendered bundle through §9.1, the carried <host>.env from the newest archive, the agent-owned variables, and its own inherited agent variables), and every source variable matches by HMAC, with these classes: region (CARLOS_REGION): must differ as expected; layout (CARLOS_CONTROL_SOCKET, CARLOS_PURGE): must be present iff the flat layout provides it, value not compared; box (an allow-list of host-specific inherited variables such as INVOCATION_ID, JOURNAL_STREAM): not compared; everything else: equal. A <host>.env variable that shadows a rendered one is reported. The report records the input versions it used: every bundle etag, the overlay etag, the archive's plaintext digest, the release version and the launch report's digest (codex R2-8) | | T4 storage | for each store bound in that composed environment (internal/objstore/objstore.go:214-218), with its credentials: list one key, put, get and delete .carlos-move-probe/<move id> | | T5 archive | the newest archive opens with this box's key, matches its manifest, has no special file, and is under the cap | | T6 disk | free space (readDiskFrac, internal/host/probes.go:209) covers twice the replica, plus the archive, plus 2 GiB, and stays under 85% | | T7 release (amendment, 2026-10-12) | the pinned release materializes for the held row (§9.2). With host claims on, T7 stages the pinned release into the shared version store and verifies it there (D3's admit, §4.1's authorization, the stage bound to its digest and D3's bind on the staged bytes) but does not publish live/<host>: a moving claim grants no held write, and the link is this host's file. The publication moves to the landing's configured, under its held-release selection (§9.2). With host claims off, T7 is unchanged. A target that cannot write its version store under the claim reports that the release is not staged yet, because there is no root stage pass to relay it to. Paul ruled it on 2026-10-12 (Q2.1 of the moves pre-flight after claim Plan 12), so that a move can become ready while host claims are on | | 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. 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 | | T13 landing armed (amendment, 2026-10-11) | the target box reports that it can land the move and roll it back (landingArmed and rollbackTargetArmed); a report without the check counts as unarmed. The source also refuses to start the cut unless its own recovery is armed (recoverySourceArmed), checked at requested before the staging lease and again at admitted before the stop; a refusal returns the move to ready with the reason shown and is never stuck. Paul ruled it on 2026-10-11 so that the switch is not the only guard against a cut nothing can land. An old source ignores T13, so every box runs a release with it before moves are enabled | | T11 budget | the whole stop-to-open estimate fits the operator's cut window (default 120 s) (codex R2-10, M11), from three measured rates, the cross-region copy path, regional S3 (reads and writes from a box in the bucket's region) and the box's disk: stop + final checkpoint and SyncAndWait + final mirror (at most the 16 MiB bar at the cross-region rate) + archive build and upload + the target's build (§7.6 building, R5-5, R6-3): the restore of the staged replica (the whole database read from regional S3 and written to disk), the snapshot write and the anchor write (each the whole database read from disk and written to regional S3) + the verification of the built database (§7.6 restored: one disk read for its sha256) + render + the probe attempts the window permits, each with its own settle + the open (open_budget, 5 s) (joint N15, J2-N15). Rev 7.5 made the sealed transfer a snapshot of the stopped database and still priced the cross-region copy at the 16 MiB bar: a 2 GiB database over a 10 MiB/s path needs about 205 s for that copy alone, so T11 admitted a move the deadline then rolled back (R5-5). Rev 7.6 built the snapshot on the target and priced three passes at one local rate, then restored the generation cold a fourth time in restored without pricing it: the review's 3 GiB at 200 MiB/s with one probe came to 108.68 s priced and 124.04 s run (R6-3). Rev 7.7 verifies the built database instead of restoring it again and prices every byte moved. Rev 7.11 prices the probe's own protocol (R10-8): every probe attempt is a cold admission that purges the built database and restores the prepared generation again before the app starts (one regional S3 read and one disk write of the whole database), plus the admission's overhead (the CAS, the purge, generation.json: 2 s), the probe and its settle; every attempt after the first is a fresh generation whose first upload is the whole database again (one disk read and one regional S3 write). Rev 7.10 priced the previous protocol, three build passes, a verification and the probe alone, so the review's 2.5 GiB at the example rates was admitted at 113.8 s against the 120 s window and would have run to 131.2 s (129.2 s before the admission's overhead). The worked example, the same in this spec, the change note and budget_test.go: 2 GiB at 10 MiB/s across regions, 250 MiB/s to regional S3, 500 MiB/s on disk gives 53.6 s of fixed costs (restore 12.3, snapshot 12.3, anchor 12.3, verify 4.1, the rest 12.6), a first attempt of 64.3 s (restore 12.3, admission 2, probe 30, settle 20), 117.9 s in all, and admits one attempt by 2.1 s; a second attempt would add 76.6 s; the cross-region snapshot transfer (204.8 s) is refused by the same arithmetic, so is the review's 3 GiB workload at 200 MiB/s (rev 7.6's arithmetic admitted it), and so is 2.5 GiB. The permitted attempts depend on the budget (R3-7): the attempts admitted are those whose summed costs fit the window after the fixed costs, attempt(1) = restore + admission + 30 s + 20 s, attempt(i > 1) = attempt(1) + full upload, at most three, and the instance is eligible only if that is at least one; the probe loop (§7.7) runs at most that many. Rev 7.3 required all three attempts to fit, 150 s of probing against a 120 s default window, so no default move was ever eligible; budget_test.go (§14.2) states the arithmetic and shows a tiny instance admitted with two attempts, the boundary at 70 s of fixed costs, and never more than three. 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 the instance as it runs today answers 200 to 399 from its own process (codex 14); an app that fails is refused with "declare moves.ready_path". S2: its next spawn is strict (§5.3). S1 is load-bearing (model 3): a source box that cannot run the instance now (in the model, one without CARLOS_SECRETS_KEY, finding 2b's state) can be cut, and its pre-flip recovery then never passes its probe. The model drops S1 and finds moves stuck in reverting.

ready requires a round at most the 16 MiB bar, a passing target report and source readiness, each under 10 minutes old.

7.4 The cut, journaled (codex 4, R2-8, R2-10)

Each phase is written to cut_phase before its side effects.

| phase | entered by | action | failure and recovery | |---|---|---|---| | requested | cut door or the source (auto-cut), CAS ready → cutting | none | | | admitted | source CAS, stamping cut_at | only if the report and source readiness are fresh and every pinned input version (move.inputs) still matches the current bundle etags, overlay etag, release and launch report; otherwise CAS back to ready so the checks rerun (codex R2-8) | abort is legal until admitted and refused after; both CAS the same field | | stopping | source | row moving, hold_op = move id; ReconstructStopEvidence (§5.3) | its budget, then reverting | | stopped | source | final checkpoint and SyncAndWait, so the replica holds every acknowledged transaction; record the required final TXID N, the MaxTXID of the newest level-0 file (§5.1 step 1); read Replication and NextDue; snapshot the timers rows to move-snapshots/<host>/<move id>/timers.json and …/timers/ in staging; write stopped-source.json with N; CAS the claim's execution holder to none (§19 K3) | | | staged | source | byte-final mirror round into replica/, within the bar; the seal: N and the versionId of every current LTX file under replica/, of files/… and timers/…, in the op journal (§7.3), and src_covered (rev 7.11): whether the source's own replica of holder.generation reached the stopped database's position with no pending write, which decides a rollback's clean return (§7.8); and from_db: whether the seal was built from the stopped database itself, which decides whether the landing's admission has anything to declare (§5.1 step 9). A round never forces a sync on a session whose start has not opened replication (§7.14): it mirrors the remote as it stands | 3 deferred rounds or its budget: reverting | | archived | source | build the final archive from the stopped directory, seal, write create-only to move-snapshots/, record both digests, copy into files/ | over the cap, a special file, or its budget: reverting | | flipped | source, the flip CAS | region = to, state = landing, landing_deadline; and the claim: op.kind = landing, execution holder = target (§19 K4) | |

One absolute deadline, equal to the promise (joint N15, J2-N15). The M2 promise is the window from the source's stop to the target's open. Admission writes cut_deadline = cut_at + cut_budget − open_budget into the move journal. Every phase before the commit checks it, on the source and on the target alike, and the commit is a record CAS conditional on now ≤ cut_deadline (§7.9): that CAS is the decision, and the claim follows it unconditionally, so the deadline cannot be passed between the two writes. After the commit the target is authoritative and its open is a local conditional update on its own box, bounded by open_budget; an open that overruns it is reported against the promise, but nothing is rolled back after a commit. Exceeding the deadline before the commit starts recovery: reverting before the flip, a rollback after it. Rev 5 bounded the commit and called that the promise; the promise was stop to open (J2-N15). The recovery's own deadlines (reverting 15 min, the release deadline 15 min) are separate from the promised window (codex R2-10). Rev 3 checked the deadline only while probing; the model found commits far past the budget after slow installs, and finds them again when the deadline is dropped. The source does not purge its database or files at the cut; finalization parks them (§7.9).

reverting (pre-flip recovery, codex 4, joint N11). The record still names the source. The source CASes the claim to op.kind = reverting with itself as execution holder, holds the row as restoring with hold_op = move id, and runs a journaled recovery, op.journal.rev_phase:

| phase | action | replay | |---|---|---| | evidence | entered from stopping: evidence was never obtained, so something may still run. Compute it (§5.3) and start nothing until it holds. No files baseline is checked, because the move has not touched the files | replayable | | verify | entered from stopped, staged or archived: check files and timers against the digests recorded at stopped | replayable until probing is journaled | | probing | render held config and materialize the release (§7.7), then probe | restarts only the probe. Never re-runs verify: the probe's process may have written, and those writes are now the authoritative state (INV-2) | | probed | conditional open on hold_op = move id | replayable | | opened | the claim waits for the staging obligation (§7.11); then the record clears (last_move = rolled_back) and the claim releases to serving (record first, §7.5) | |

Rev 3 compared digests again on re-entry, so a crash after the recovery probe had written left the move stuck on a "mismatch" that was really the app's own work (joint N11). The model reproduces that when it drops the journal. Fifteen minutes of failed probes: stuck, held.

Source digests at stopped. The source records files.plain (§8.3) and timers_sha256 at stopped, before any phase that can fail, so every recovery has a baseline.

7.5 The flip, and how the claim follows the record (J2: record/claim ordering)

Every move transition is one record CAS, and the claim follows it. The record carries the move's journal, so the record CAS is the decision: the flip (archived → flipped), the commit (probed → committed, §7.9) and a rollback (landing → rolling_back, §7.8) are each one CAS on the record, guarded by move id and incarnation. The commit and a rollback CAS the same field, so exactly one wins. The claim half is a second CAS that the record fully determines: the op id, the claim's prior kind and phase, and its new kind, phase and execution holder:

| record transition | claim CAS that follows | execution holder | |---|---|---| | flipped | moving/sealed → landing, landing_phase = checking | none → target, citing the source's evidence (stopped-source.json) | | committed | landing → phase committed, plus the obligations of §7.9; holder.generation is not touched: it is the generation the latest admission chose, the target's probe (§7.14), and a commit that wrote the prepared generation back would put an obsolete one into authority after a restarted probe (R10-3) | unchanged (target) | | rolling_back | landing → restoring under the same op id, rollback.id from the record; holder.generation untouched here too | unchanged until the target's evidence (§7.8) |

Any actor that reads both objects and sees the record ahead writes the claim half: the actor that wrote the record, on its next step; the other participant; or the console's recovery pass (claim C2's recovery owner for this state). The CAS is conditional on the op id and the prior claim state, so two actors racing to write it cannot both succeed, and neither can write anything the record did not decide. Until it lands, the claim still names the previous state: after the flip nobody holds the execution right (the source gave it up at stopped, K3); after the commit the target is not yet admitted to serve; after a rollback decision the target is still the executor and must still give evidence. Each is safe.

This replaces rev 5's wording, in which §7.5 had the source complete the handoff while K4 reserved it to the receiving participant (J2-D7). K4 now says the execution holder changes only in the claim CAS that mirrors a record transition, citing the evidence that transition names (§19 K4).

The model writes the record half and the claim half as separate steps, with crashes, console loss and the recovery pass between them (§14.2.2).

The source row stays held (moving); reconcile keeps it because the claim names this box as a participant (§9.6).

The close is record first too (rev 7.23, Paul's ruling M4). The actor that closes first checks that no obligation this op created remains, then CASes the record: move is cleared and last_move names the move and its outcome (done, rolled_back or aborted). The claim's release to serving (§19 K8) is the second CAS, determined by last_move: the op id, its kind and phase, and the executor the outcome names. Until it lands, the claim still holds the op, so nothing else starts on the host. After a crash between the two, no box revisits the host (the box passes are driven by records with a live move), and the console's recovery pass writes the release from last_move. Rev 7.22 had this the other way round, claim first; claim Plan 10's recovery grant can act only while the claim holds the move op, so a claim released over a live move could never be finished by it.

Late record writes. Every move write to the record is a conditional CAS. One that completes after its client gave up either still matches, and repeats a decision already taken, or fails on the ETag.

7.6 Landing and install (codex 5, 13, R2-6)

The target's reconcile mints the row held as landing with hold_op = move id (§9.6). The target's worker runs these phases. Each is written to landing_phase before its side effects, and its local work is journaled in <DataDir>/.moves/<host>/<move id>/ (F12).

| phase | action | done when | replay | |---|---|---|---| | 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; under the host guard, from that fresh read, set the local record's active_stamp = holder.stamp, the stamp the flip CAS wrote (claim rev 6.5 §6.4, §6.4 here); 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) | | building | build the generation from the staged replica (§5.1 step 2, R5-5): restore the sealed versions under replica/ with the planner into the generation's database file, verifying each file's CRC-64 trailer, requiring exactly N and PRAGMA integrity_check; write the snapshot [1, N] to <location>g-<move id>/0009/<1>-<N>.ltx and the anchor [N, N] to <location>g-<move id>/0000/<N>-<N>.ltx (§5.1 step 7); in this order (R7-4, §5.1 step 2): the build intent <location>g-<move id>/build-intent.json with the encoding inputs (the header timestamp, page size, commit, N), before any PUT; the snapshot PUT, acknowledged; the anchor PUT, acknowledged; then the completed install manifest <location>g-<move id>/install.json with the snapshot's key, the versionId each PUT returned, N, each CRC-64, integrity_check's result and the sha256 of the database file the build produced (R4-1, R5-1, R5-2, R6-5) | the completed install manifest exists; the intent alone is not completion | replayable at every boundary: staging is immutable after the flip, the generation is new, and the build never deletes. A replay reads the intent, encodes identical bytes, and reuses a snapshot or anchor it finds current under its key; a crash after the intent, after either PUT, or before the manifest leaves no completion, so published never runs; a PUT that completes late lands in this generation again as another version of identical bytes, which nothing reads (§5.1). The model journals the same states (install-copy, install-anchor, published) and refuses, as INV-11, a generation.json naming a snapshot or anchor that has not landed | | published | the build is complete and recorded; generation.json is not written here (R10-3; rev 7.9 wrote it): the probe's cold admission publishes it, with op, incarnation, the install manifest's sha256 and the snapshot identity (snapshot_key, snapshot_version, snapshot_txid, snapshot_crc64, §5.1), after its CAS and before replication opens (§7.14) | the journal records the phase | replayable | | local | retire-artifacts (claim rev 6.5 §6.4, §6.4 here: never retire-installation, which would retire the stamp checking activated) any warm database (with <dbPath>.gen), files directory and <host>.env of an earlier stay 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 | verify the database building produced (R6-3): its sha256 equals the manifest's, CheckDB (backend_exec.go:313) passes, and <dbPath>.gen is written naming this generation and location; record landing.installed_db_sha256. No second cold restore: the file was built by the planner over the sealed versions on this box and verified at N, and a cold restore from the generation would yield the same pages by construction (the snapshot is every page of that file). The anchor's PUT was acknowledged in building, so litestream's open reads position N from the listing and replication starts at N + 1 (§5.1 step 7); a building replayed after a crash rebuilds and the sha256 is checked again | | replayable until probing; a sha256 or CheckDB mismatch is a rollback | | probing | the probe (§7.7) | | never replays an earlier phase (INV-7); a crash restarts only the probe | | probed | probe passed | | |

Any failure from checking to probing, or landing_deadline, triggers a rollback (§7.8).

One install routine, two sources (region HA L16; rev 7.19). building and published are one routine shared with region HA's relocation (spec 1 §5.8): its input is a pinned set of remote versions (key, version id, level, TXID range) plus the required final TXID, and its output is the prepared generation's snapshot, anchor, build intent and completed install manifest exactly as above. A move feeds it the seal's replica/ versions and N; a relocation feeds it the versions genselect.SelectPrepared or the generation's current listing pins and that listing's maximum TXID. The anchor rule, the two durable states, the replay rule and the marker rule are the routine's, so both callers get them once. Every installation writes a files manifest in its new generation (L17, §8.3; claim rev 6.28 C3, §6.2a, P6-D3; rev 7.21 after R18-1): the first manifest is not the session-bound publisher's, because no target writer session exists until probing (claim C3 binds that publisher to an admitted {location, generation, session}). It is the prepared manifest, as claim rev 6.30 (73b1b9dc) states the rule and region HA spec 1 §5.8's remote build (:809) uses it: before any session exists, op.exec may publish an installation's initial files state in a phase that permits installation: a move's local, a relocation's installing, or region HA's prepared build. That state is create-only content objects plus one create-only prepared manifest: in local, after the archive is extracted and verified, the target writes the installed files, <host>.env and the wake state (the timers snapshot, NextDue, Replication) as region HA §5.6's immutable objects under <location>files/<P>/objects/ and then the one manifest <location>files/<P>/manifest.json, bound to {location, P, op id, installation stamp} where P is the installation's prepared destination generation, never holder.generation (rev 7.22, R19-1): g-<move id> for a forward landing, the prepared return generation g-<rollback id> for a dirty rollback (§7.12), the same name the install manifest and the generation prefix of §5.1 use. holder.generation still names the source's pre-move generation S until the probe's cold admission moves it (§7.14, §9.4) and is not changed by local; a manifest bound to or filed under S could never be P's baseline, so the first landing admission would block (claim rev 6.30 requires the prepared generation). The binding's other members are the move id (or rollback id), the holder location and the flip's stamp. The manifest is published naming exact versions, with sequence 0, never replaced, and retired with its generation; it is journalled in the op journal like the install manifest, before .files-gen is written, and a replay reuses the objects it finds by digest and the manifest by key (create-only, so a late second write fails). The session-bound publisher starts only after the first admission (the probe's, §7.14): it takes that manifest by exact version as its baseline and publishes from sequence 1; until then nothing but the install writes under files/<generation>/. Manifest entries carry origin-qualified references (claim P6-D3): an object is named by its own incarnation location and region, so copying a manifest into a new generation never reinterprets its references, and a cross-region landing's prepared manifest names destination-local objects it materialized and verified from the sealed archive. Files reachability is independent of the database baseline: a cold admission establishes its files manifest from the newest valid manifest in the admitted predecessor chain, read by exact version, before the app starts; missing or malformed manifest data is never an empty-files bootstrap. The archive at the cut stays as the sealed transfer and the rollback's evidence.

7.7 The probe (codex 14)

ProbeWake(host, op), legal only on a row held with hold_op = op and only while the claim names this box as execution holder:

• first, render held config and materialize the release (RenderHeld, MaterializeHeld, §9.1, §9.2), for every kind of probe: the landing, the source's pre-flip and rollback recoveries, and a push (model 4). Config sync and adoption skip held rows, so an instance created shortly before the operation began may never have been rendered. In the model, pushes and reverts of such an instance never pass their probe until this rule is applied to every probe;
• check the actual launch environment at spawn (joint N8): recompose it exactly as the spawn will, including inherited agent variables after any restart. The landing probe requires the input versions pinned at admission (move.inputs) and the executable. A recovery probe (the source's pre-flip revert and its rollback recovery, §7.4, §7.8) requires the inputs it rendered itself, now, and records them in the journal (recovery.inputs); it is not bound to move.inputs (J2-R2-5). Rev 5 bound every probe to the pinned inputs: a bundle published after admission rolled the landing back and then failed every recovery probe forever, because recovery renders the current bundle. The pin exists so the target runs what the source ran (T3); on the source itself, the current bundle is what it would run had there been no move. A bundle that is itself broken fails the recovery probe as it would fail any wake: stuck, held, and paged;
• a strict spawn (§5.3), with CARLOS_MOVE_PROBE=1 (advisory);
• the answer must come from the spawned tree: the socket peer's credentials (SO_PEERCRED) name a process in the host's cgroup;
• the readiness path (moves.ready_path from the instances manifest, / otherwise) answers 200 to 399 within 30 s (backend_exec.go:36);
• a 20 s settle, the process still running, and a second request;
• up to three attempts for a landing, and never more than T11 admitted for this budget (§7.3, R3-7); a recovery probe (a revert's or a rollback's source) has nine before stuck (§7.8, §7.10; R12-5). One attempt is one cold admission (§7.14): its app may be restarted under the retry policy of §5.1 step 9 within the attempt's 30 s readiness window, which runs from the first start (the waits total 15 s, each start's own time is on top), and the fifth failure or the window's end, whichever comes first, ends the attempt; the next attempt, if the budget allows one, is a new cold admission into a fresh generation restored from the dead attempt's. The deadline is checked before each start and before readiness is accepted (R12-2): an attempt whose window passed while the agent was paused, or between a failed start and its retry, does not start the app at all (rev 7.12 checked only while the environment was unready or after a failed start, so a successful start after the window made an expired attempt the probed writer); an app that answers readiness at or after the deadline is stopped and the attempt fails; and the probe's acceptance checks the attempt it accepts answered within its window (INV-19). At the boundary, readiness k steps after the attempt's first start: k = 29 is accepted, k = 30 fails before the start, k = 31 fails at the deadline with the environment still unready (TestProbeWindow). A probe never marks the host failed; the operation's rollback (or stuck) is its outcome. The budget's attempts and the policy's five restarts are different things: at most three (or nine) admissions, each with at most five starts inside 30 s. The absolute cut_deadline (§7.4) still bounds the whole.

The probe's activator entry is held: RetireExcept (internal/edge/edge.go:924, activator.go:2624) keeps it, and the edge never admits a request to it (codex 13).

7.8 Rollback (codex 1, 2, 3, R2-3, R2-4, R2-5)

Triggers: a landing failure (the target), or landing_deadline (the source or the console's sweep). Both are a record CAS landing → rolling_back, guarded by move id; the commit is a CAS from probed on the same record, so exactly one wins. The CAS sets region = from, rollback.id, reason, release_deadline = now + 15 min, and the claim moves to op.kind = restoring under the same op id, with the execution holder still the target until its evidence arrives. Both boxes stay participants, so reconcile keeps both rows held (§9.6, §19 K9): the target row is not retired by the region change (codex R2-4).

Target release, journaled as rollback.target_phase:

| phase | action | |---|---| | 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, and the seal recorded src_covered (§7.4: the source's own replica reached its stopped database's position); otherwise dirty. Rev 7.11 adds the second condition (rule seal-return, INV-15): when the source's final upload was still in flight at the stop, the seal holds a write the source's replica does not, and a clean return would restore the source without it, declaring lost a write the staging and the landing's built generation hold. Write stopped-target.json; CAS the claim's execution holder to none | | returning (dirty only) | the handoff back: after a final checkpoint and SyncAndWait, write a snapshot of its stopped database (one level-9 LTX file [1, N'], every page, as the pinned writers write it, §5.1 step 2) into the source bucket's moves/<host>/<rollback id>/replica/0009/<1>-<N'>.ltx, seal it by versionId with N', publish its files archive and timers snapshot under files/ and timers/, write move.json. A target that never restored a database (dirty only for want of src_covered) returns the staged seal as it was given, pinned by the versions the cut journalled, and the staged files and timers with it. The return is under the release deadline (15 min), not the cut window, so the whole snapshot crosses the region here | | 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 |

The cleaning phase is what leaves no copy of the incarnation in the target's live namespace, so a later delete and recreate there cannot restore it (codex R2-5, INV-10). It waits for the source's recovery because, until then, a source failure might need the target's state again.

Source recovery, journaled as rollback.source_phase and in <DataDir>/.moves/<host>/<rollback id>/ (codex R2-3):

| phase | action | replay | |---|---|---| | waiting | until released (clean) or returned (dirty) and the claim's execution holder is none | | | claimed | CAS the claim: op.kind = restoring, execution holder = this box, citing the target's evidence (§19 K4), and holder.stamp = op.source_stamp, the source installation's own stamp the flip journaled (claim rev 6.5: a CAS that makes an existing installation current again writes that installation's stamp; R6-4); clean, with src_covered: holder.generation = op.journal.src_gen, the source's generation again, for the restore. The predecessor of the source's re-admission is still the target's writer, the last record of holder.admissions (claim rev 6.12, R11-4), and its coverage is clean-return: nothing is declared. The source's fresh read then matches its record, or re-initializes a lost one, to S | | | restoring | row restoring, hold_op = rollback id | replayable | | clean: verified | files and timers digests equal its stopped digests (a mismatch is stuck, INV-4); its warm database's <dbPath>.gen equals its pre-move generation | replayable | | dirty: parking, building, published, local, configured, restored | the target's install phases of §7.6, on the source, from moves/<host>/<rollback id>/ (building restores the returned snapshot, requires N', and writes the rollback generation's snapshot and anchor), with destination superseded/<rollback id>/<host>/ for what it supersedes, with two differences: configured and the release materialization run on the inputs the source renders now, recorded as recovery.inputs, and are never gated on move.inputs (§7.7, J2-R2-5); and the stamps: the install runs under the source's pre-move installation S, which the claimed CAS wrote back into holder.stamp and which stays active; local runs retire-artifacts(S) on the pre-move database, tagged S, which moves no stamp (a leftover tagged with a retired stamp, left by a cold admission that issued its stamp and then failed its purge, is parked too, rev 7.11); the return generation's database and files are tagged S as they are installed; the probe's cold admission (§7.14), which names the return generation in holder.generation, issues the new holder.stamp R in the same write (KeepStamp false: a writer was admitted since S was issued), and the source's fresh read under the guard activates R before the open, tagging the return generation's artifacts R and retiring S then (claim rev 6.5 §6.4: a dirty rollback installs a new generation and never keeps its predecessor's stamp, R5-4, R6-4; rev 7.5's model kept it, rev 7.6's activated the target's; rev 7.11's row still said the probed CAS wrote them, R10-3). Rev 7.3 said "exactly" and so inherited the landing's configured gate: a bundle published after admission, a target that wrote, and a dirty rollback would then have failed before the recovery probe (R2-5). The model's recovery-current-inputs witness is that case (§14.2.5) | as §7.6 | | probing | the probe, an AdmitWriter (§7.14): dirty, cold into the return generation from its pinned seal (baseline: sealed, no writes_lost); clean, warm or cold into the source's own generation, which the return CAS named again | never replays an earlier phase: once its recovery process has started, its own new writes are authoritative (INV-2, INV-7); a probe that dies before its session opened replication, or in its settle, is restarted, a new admission | | probed | the phase CAS alone: holder.generation and holder.stamp moved at the probe's cold admission (§7.14; a dirty return's generation and its new stamp, claim rev 6.5 §2 and 6.9 §6.4a), and the probed CAS writes neither (R10-3; rev 7.10's row still named the return generation here). Dirty: the return lane's park-staging chore is queued now | | | recovered | CAS rollback.recovered_at | | | opened | the conditional open on hold_op = rollback id; CAS rollback.opened_at | |

Obligations. The target's released CAS also adds to the claim, in the same write, a park-superseded obligation for the target box and region (its replica, staging and local state; destination superseded/<move id>/<host>/), which its cleaning phase discharges, and in the same write runs CoverRegionPredecessors for the target region (claim rev 6.14 item 6, R12-3): every record whose predecessor's objects are the target's (a restarted probe's record names the dead probe's generation there) is covered, with no chore, since the park retires the whole location. The console's release of a declared-lost target (§7.10) queues the same park and covers the same way. The source's return admission comes after this CAS, so its record, whose predecessor is the target's writer, is born covered under the park the claim already holds (§5.1 step 9). A dirty source recovery adds one for its own region and box for what its install supersedes. These are the claim spec's durable chores (§2 there); §19.3 asks for the kind.

Finalization: when recovered_at, opened_at and target_parked_at are all stamped, and no obligation this op created remains, whichever actor stamps last writes the terminal log event (rolled_back, with every timing, digest and reason), CAS-clears move, and then releases the claim to serving (§19 K8; record first, §7.5). Until then move and the claim stay, so nothing else can start on the host (codex 6). The source serves from opened on; the held claim blocks only other operations.

Nine failed recovery probe attempts (three times the landing's budget of three; probeTries*3 in the model): stuck, held (§7.10). Rev 7.12's sentence here said three, against its own model description (R12-5).

Waiting. If release_deadline passes with no target evidence, the move stays in rolling_back ("waiting for uk to release"), paged, safe: nothing runs anywhere. It converges when the target returns (INV-3).

7.9 Commit and finalization (codex 6)

1. Commit (target): record CAS probed → committed, conditional on now ≤ cut_deadline (§7.4). The commit is also refused once a rollback reason is recorded, and it is bounded by the earlier of cut_deadline and landing_deadline (§7.8 makes the second a rollback trigger; Plan 2 ruling P2-deadline). Then the claim follows (§7.5): phase committed, plus the obligations in the same claim write, park-superseded for the source's location in its region and box, and park-staging for the target's staging (§19.3). holder.generation is not written (R10-3): it is whatever the latest admission chose, the prepared generation g-<move id>/ when the first probe passed, a fresh generation restored from it when a probe was restarted (§7.14). Rev 7.9's commit wrote move id here; after a restarted probe that had acknowledged writes into its fresh generation, that put the obsolete prepared generation back into authority and the next restore lost them.
2. Open (target): conditional open on hold_op = move id; CAS opened_at. From here the target serves on the session its probe was admitted with; the claim's landing op with phase committed admits its later wakes as AdmitWriters like serving's (§19 K6, §7.14).
3. Source park (source, holding the lease on its own instances/<host>/, claim spec C3): bucket-park its instances/<host>/ into superseded/<move id>/<host>/; local-park its database (with <dbPath>.gen), files, <host>.env, quarantine and journals; delete its row (conditional on hold_op = move id) and its timers rows; CAS source_parked_at and remove its obligation.
4. Target staging park (target, holding the lease on its own moves/<host>/): moves/<host>/<move id>/ into superseded/<move id>/<host>/; remove its obligation.
5. Close (when both obligations are gone): terminal log event done; CAS-clear move (last_move = done); then release the claim to serving with the target as execution holder (§19 K8; record first, §7.5).

7.10 Stuck and declare-lost (M16)

The termination fence is M16's evidence, automatically (region HA L14, ruled H10; rev 7.19). Region HA §5.9 defines the termination fence: a regional worker observes state exactly terminated for the box's instance id, account and region as the roster records them, and writes the create-only fence record control/box-fences/<enrollment>.json; the claim puts the box on lost citing it (claim L2 to L4). For a move whose target is fenced that way, the move takes the fence as the evidence --declare-lost would have supplied, with no operator: the same legality table below applies (the target owes stop evidence, or released dirty and has not returned), under the same before-commit rule: before the record's commit CAS the move rolls back clean through the declared-loss path, with fenced_at as every scope's evidence time and the fence record as rollback.evidence; after the record's commit the target is authoritative and the move is not what recovers the instance: the move finishes its own close (its remaining steps are parks run by regional workers), and the instance's recovery is region HA's relocation, outside this spec. A source terminated before the flip (rev 7.20; claim rev 6.28 §4; R18-2; claim rev 6.30). "Before its flip" means before the authoritative record enters landing through the flip CAS (archived → flipped, which sets state = landing, §7.4). That is distinct from, and earlier than, the final commit CAS (probed → committed, §7.9): a record at landing whose claim half is still moving/sealed is already past the flip, and the conversion is refused there as everywhere after it. The fence converts the pre-flip moving operation to relocating in one CAS: it records the fence reference (below), sets op.exec = "none", preserves holder.stamp and holder.generation, starts relocating at pinning in the source's region, and leaves every obligation untouched; the move's staging lane, park-replica scoped moves/<host>/<op id> and owned by the target region, keeps its op id and stays executable (the conversion queues it when the move had not yet, as an abort would), and it blocks neither the conversion nor the relocation's release. Readiness, evidence and recovery bind to the replacement box choose() names when the relocation leaves pinning. After the flip (the record's landing state) the conversion is refused and this section's rules for a lost target apply. In a one-box region the converted operation has no eligible target: it sits at pinning with exec "none" and the lane's park still owed until region HA enrolls a replacement box (automatic ASG enrollment, H16 and H17). That state is safe, since no writer exists and the data is pinned in the source region's bucket, but the host is not recovered until a box exists. The operator sees it as relocating / pinning: waiting for a box in <region> in carlos move status and the fleet view, and one incident alert is raised when the conversion finds no live box in the region (§13); the alert is not repeated. The operator's --declare-lost stays for the stopped, unclear and vanished boxes the fence does not cover (claim D2).

The fence reference (rev 7.20; moves C7, claim rev 6.28 §7.3). Every transition that relies on a termination fence writes op.journal["fence.<box>"] = {"enrollment", "key", "sha256"}: the box's enrollment, the key control/box-fences/<enrollment>.json, and the SHA-256 of the exact bytes the transition verified. A loss.<id> intent written by the same transition cites the same reference. ReturnToSource and every other consumer accept a fence only through that reference, re-reading the record at key, requiring its digest to equal sha256 and its enrollment and cloud identity to match the roster's; the key is never reused for another box or enrollment within the operation. An automatic declaration from a fence needs no quarantine revision and no operator (L4); the terminated enrollment is permanently ineligible.

What a declared-lost box leaves behind (rev 7.11). Its acknowledged writes beyond its uploads are declared by the next admission's writes_lost (the record's remote_max_txid names where an operator finds them in the seal or the box's generation); its registered timers are declared by the console's declare-lost record itself and alerted, since no return lane will carry them; neither is ever exempted silently (R10-6). When the target of a rollback is the lost box and the seal was the one holder of the source's writes beyond its own replica (src_covered false, §7.4, §7.8), the return is clean for want of a target and the source's re-admission from its own generation declares its cut session as well, a second writes_lost record ({box: source, generation: source's, session: the cut's, remote_max_txid}) with its alert: the seal in the lost target's region is unreadable from the source and no lane brings it.

• stuck: the source's recovery probe failed. Held. carlos move resolve --host <h> --retry reruns the recovery's probing phase.
• --declare-lost <box> (M16), operator-only. carlos move resolve --host <h> --declare-lost <box> is the move-facing form of the claim spec's carlos ops host resolve <host> --declare-lost <box> (§7.2 there). The joint review's D6 text governs it (joint D6, N3):

> A claim CAS is bookkeeping, not fencing. The resolve command must > establish verified compute fencing, or an independently enforced > execution-lease expiry, before reopening the source. Recover validated > durable target data where available, not only an already-published > return. Retain M16's precommit restriction, exact-participant check, > source refusal and explicit loss confirmation.

This spec takes the first branch only: compute fencing (model 5). The verb requires the operator's cloud credentials to show the box stopped or terminated, verified through the cloud API by the CLI. An expired execution lease is not enough, even with the self-fencing watchdog: a whole-VM pause stops the watchdog with everything else, and on resume the application can write before the watchdog fires. The model allows the lease-expiry branch and finds two writers when a frozen target resumes beside the recovered source (1 seed in 30,000; 2 when the watchdog also runs inside the agent, so an agent pause defeats it too). The lease stays useful for liveness: a partitioned or hung participant fences itself.

It is legal in exactly these states, and refused otherwise: - the target owes stop evidence (landing, or a rollback before the target released): it proceeds as a clean rollback, after a confirmation naming the box, the flip time, and that the target's writes since then are lost (M-C18); - the target released dirty but had not returned its writes (model 6): the same, and the confirmation says so. Rev 3 missed this state; the model finds a move waiting forever on a return that a destroyed box can never send. The same CAS adds a park-staging obligation for the return lane, moves/<host>/<rollback id>/ in the source's region, owned by the source region's box, not before the lane's staging horizon (model 27): the lost target may have published part of its return, and the rollback now finishes as a clean one, which parks nothing else there; - a destroyed box owes only local chores (park-local): the obligation is removed and nothing else changes. This one is legal after commit, because no data authority is involved (model 6); - refused after committed in the first two states, refused for the source, refused for any box that is not that exact participant. "After committed" means after the record's commit CAS, whether or not the claim has followed it yet (§7.5). Before the commit the verb's rollback is the same record CAS as any other rollback, so it cannot race a commit.

The box goes on lost. A returning box is quarantined (claim §7.2): before anything else it retires every local artifact for the host under the host guard, and only then can an operator --readmit it. The model starts stopped boxes again after they were declared lost; without the quarantine they would keep stale local state for the host.

7.11 Abort

Legal in preparing, ready, and cutting with cut_phase = requested (CAS). A move whose readiness never comes aborts itself after a bound, so an unreachable target never needs a human.

Who retires what (joint N13). The source cannot read the target's moves/* and cannot write the target's superseded/ (M17 grants it Put, Delete and prefix-scoped List on moves/* only), so it cannot park target staging. Abort therefore adds a park-staging obligation owned by the target region's box, not before the staging horizon of §7.3. The source parks its own snapshots. (Plan 5 note, ruling K19: "parks" here means the source retires them from its own bucket, every version of move-snapshots/<host>/<op>/ through DeleteVersion; that prefix is outside the park scope grammar, and F3's retention of snapshots covers completed moves only.) The claim stays moving until every obligation has acknowledged; then the record clears (last_move = aborted) and the claim releases to serving (record first, §7.5). The model gives the source the target's park and records an IAM violation on every abort.

7.12 Deletes and parks under the claim

• Delete during a move is refused (409): the delete doors and PurgeApp CAS the claim from serving to deleting (claim spec §5), so they cannot start while a move op holds it (§19 K7). A purge of an app with a moving instance waits. An operator who must delete aborts first, or waits for the commit or rollback to finish.
• App purge (joint N9, model 7, 8). Claim §5.3 reserves the app first, then claims every host, then tears down stores. The model found two more rules it needs. Purge adopts first: a legacy host of the app with a record but no claim yet is invisible to a purge that looks only at claims, so the purge tore down a store under a serving instance; purge must run the one adoption routine (claim §9) for every unclaimed record of the app before deciding. The reservation is the purge's journal: the console's recovery pass finished a stalled purge's delete and freed the host, free dropped the reservation, a create for the same app went through, and the stalled purge then tore down the new incarnation's store. The reservation records the purge's phase; recovery drives those phases in order; only the purge's own completion removes it, never free. The purge fence (claim rev 5.1, CC21): a creating console can renew its registration, pause, and resume after purge's drain has removed that registration as expired. S3 cannot make the creator's claim write conditional on the registration object, so before purge removes a registration whose host claim does not name the create, it CASes that host's claim from free or absent to {op: {kind: purging, id}} with no holder, and releases it at done by writing a free claim. The creator's CAS from free or absent then fails. The model found the fence needs one more condition, and claim rev 5.2 adopted it (CC22, §19.4): the creator's CAS is If-Match the claim ETag it read when it registered, or If-None-Match: if the claim was absent then; a 412 restarts the create from step 0, with a new registration; and a claim object is never deleted (C5a there), because deleting a released fence would let the paused creator's If-None-Match: succeed. The creator's re-read of its registration just before the CAS stays, as a cheap extra; the model shows it is not sufficient alone (§14.2.5).
• Recreate during a move cannot happen: create requires the claim free or absent (claim spec C2).
• A delete after a move parks every region in touched.regions (claim spec §5). The move added each region and box to touched before writing there, so nothing it left is missed, and what it superseded is already out of the live namespace (§7.8, §7.9, INV-10). The claim's delete park copies moves/<host>/ and instances/<host>/ as separate subtrees, which is compatible with per-op staging (§7.3).

7.13 Crash at every step

The crashed actor restarts with no activator memory; everything it needs is in the record, the claim, its journals (F12) and the box's actual process state (§5.3).

| state / phase | source crash | target crash | console crash | |---|---|---|---| | preparing, ready | next round | next report | stateless | | cutting: requested, admitted | resumes the phase | n/a | | | cutting: stopping | ReconstructStopEvidence from cgroup and unit state | n/a | | | cutting: stopped to archived | resumes; the sealed archive is reused from its create-only key | n/a | | | flipped, record CAS done, claim CAS not | completes the claim CAS | waits for the claim | | | reverting | resumes the recovery, held | n/a | | | landing: checking to restored | holds moving | replays the phase per §7.6 | | | landing: probing, probed (the settle window) | | kills the tree, restarts the probe, which is an AdmitWriter within the landing (§7.14): cold, into a fresh generation restored from the dead probe's, since the dead probe's session has no certificate; the same for a push's, a revert's and a rollback's probe | | | any: the agent restarts under a running app | stops the app: the session's replicator died with the old agent and a new agent process is a new session (claim rev 6.10); the next wake is an AdmitWriter, cold, which declares what the app acknowledged meanwhile (§7.14) | the same | | | any: the admitted writer dies between its CAS and its marker | the generation is unfinished; its predecessor stays live; the next wake is a cold admission whose baseline is the predecessor, or the generation itself when it holds the first upload (§7.14) | the same | | | committed, the claim still landing | resumes the park | the target's next wake is an AdmitWriter within the landing (§7.14) | | | committed | resumes the park | opens | | | rollingback: target phases | | resumes its phase; evidence from actual state | the deadline sweep is a CAS | | rollingback: source phases | resumes its phase from its journal; never reinstalls after probing; a source whose database went with the crash verifies nothing and is admitted at its probe like any writer (§7.14) | | | | stuck | held; operator | | |

7.14 Writer admission (claim rev 6.10 §6.4a; R7-1, R8-1, R8-2, R9-1 to R9-4, R10-1 to R10-5)

Every path that opens replication is an AdmitWriter (§5.1 step 9), one claim CAS made before the app process starts (claim rev 6.10, R10-1), by the box the claim names as op.exec, and never by another. Two modes exist, warm and cold; nothing else (R9-3). Which box may be admitted in which phase, in which mode, into which generation, and the CAS that handed it op.exec first:

| op kind, phase | the box admitted | mode and generation | op.exec handed to it by | |---|---|---|---| | serving | the serving box, at every wake | warm into holder.generation on a certificate for holder.session; else cold into a fresh generation restored from holder.generation | the create's claim CAS, a push's release, a move's finalization or rollback release (§7.9, §7.8) | | pushing: probing | the pushing box, as its probe starts | cold into the push's prepared generation g-<push id>/ (its snapshot and anchor), opened once; a restarted probe is cold into a fresh generation restored from it | the push's claim CAS (op.exec = the serving box) | | moving (before the flip) | the source, at every wake; the target writes nothing | warm or cold as for serving; the source's clean closes certify | the move's claim CAS (op.exec = source) | | reverting: probing, probed | the source, as its probe starts and at every wake after | warm or cold as for serving (holder.generation is still the source's) | the revert CAS, which cites the stop evidence of the cut (§7.5) | | landing: probing, probed | the target, as its probe starts and at every restart of it | cold into the landing's prepared generation g-<move id>/, opened once; a restarted probe is cold into a fresh generation restored from it | the flip CAS, which cites the source's stop evidence (§7.5) | | landing, committed, not yet finalized | the target, at every wake | warm or cold as for serving | the same flip CAS | | restoring: probing, probed, opened (the source's rollback) | the source, as its probe starts and at every wake after | dirty: cold into the return generation prepared from the target's sealed copy, opened once; clean: the return CAS named the source's generation again, and the probe is warm or cold into it as for serving | the return CAS (op.exec = op.src, claim rev 6.5), after the target's release wrote op.exec = -1 with stop evidence | | restoring, the target's phases | nobody: the target is stopping and never opens replication again | | | | creating, deleting, parking, purging, placing | nobody: the admission CAS refuses these kinds (R9-4, R10-4, INV-13); a create's first writer is admitted after CompleteCreate, under serving | | |

Two writers never overlap because op.exec moves only through a CAS that cites stop evidence or a lost-box fence (§5.3, §7.10), and the admission CAS requires op.exec == this box (rule exec-writer) and is bound to the observed op.id, op.phase and kind (rule admit-bind-op; the model's general CAS condition on op.id, C2, already refuses a closure whose operation changed, so the binding adds the phase and the kinds). holder.generation is the only authoritative generation in every kind and phase: an operation's prepared generation (g-<op id>/, a rollback's return generation) is built by the operation's install phases and becomes holder.generation at its probe's cold admission, never before; the flip and the commit move no generation (rev 7.9's commit did). A clean rollback's return CAS names the source's generation again (op.journal.src_gen, recorded at the flip; only with src_covered, §7.8), since the target's probe had moved holder.generation to the target's and the target wrote nothing; the source's probe then restores from its own region's remote of it, is covered clean-return, and journals the target's writer as its predecessor, the last record of holder.admissions, never the holder's reset fields (claim rev 6.12, R11-4, INV-16).

The admitted writer's start, on its box, in this order; it is the agent's own loop around one claim CAS, not a set of claim transitions, and a new agent process never resumes it (a new agent is a new session):

| step | action | if it fails | |---|---|---| | decide | read the claim; op.exec must be this box and the kind one that admits; the certificate for holder.session decides warm or cold; a cold admission's generation is the operation's prepared one if holder.generation is not it or a descendant of it, else a fresh id; KeepStamp when holder.stamp > holder.session; Coverage sealed for a prepared generation from a from_db seal, clean-return for a clean rollback's return with src_covered, else ""; a lagging generation.json is read through holder.admissions (below) | nothing happened | | AdmitWriter | the CAS of §5.1 step 9, first: session, writerbox, the holder.admissions record with the last record as its predecessor, its own region and the predecessor's region; cold: generation, stamp unless kept, `writeslost only for coverage "" with no certificate; **no chore**: the predecessor is the unfinished generation's baseline until the marker names the new one (R10-2); born covered when the claim already holds a whole-location park for the predecessor's region (a rollback's return); the carried files are retagged with the new stamp here | a conflict: re-establish the evidence and decide again | | purge | delete the local database, with an error-returning purge | the start waits and purges again; the session stands | | restore | warm: holder.generation from this region's remote, to at least the certificate's maxtxid; cold, prepared: the prepared generation from its pinned snapshot and anchor (the operation's build journal); cold, fresh: the baseline from this region's remote, the predecessor or, behind a lagging marker, the nearest generation of the chain that holds an object | the start waits; a warm restore short of maxtxid is an alert, the remote is incomplete | | start, readiness | the app starts on the restored database and answers its readiness path; nothing it acknowledges is outside the session. A probe checks its attempt's deadline before the start and before accepting readiness (§7.7, R12-2) | the retry policy (§5.1 step 9): a doubling backoff from one step, five attempts. **A serving wake**: at the fifth failure the host is marked failed, the start abandoned, and no session is created until an operator clears it. **A probe**: the fifth failure, the window's end or a late readiness ends the attempt, the operation counts one budgeted try, and the host is never marked failed (claim rev 6.14; rev 7.12's row applied the marking to probes too, R12-4) | | first upload (cold, fresh, a non-empty baseline) | the full file [1, 1] of the restored database, captured once and acknowledged to the client; the generation has a root; it is in the session's ledger (R10-7) | retried with the same bytes after the client's wait, whether the original timed out or completed unseen; the session is uncertain for good | | marker (cold) | generation.json names the new generation: the pinned snapshot identity for a prepared one, snapshot_txid = 0 for a fresh one (its root is [1, 1]); never before the root exists (INV-11). **Then PublishGeneration** (§5.1 step 9), for every cold admission, a prepared generation's included, bound to the operation and phase it observed, legal in serving and in every operation a writer runs in: the walk over the uncovered records queues one park-generation per dead generation whose objects are in this region, the predecessor's, the chain's and any uncovered record's, and covers them; a predecessor in another region stays uncovered for that region's whole-location park or publication | retried after the timeout; the writer waits | | anchor (warm, when the restored position is above the level-0 maximum) | [N, N]`, acknowledged to the client; in the ledger (R10-7) | retried with the same bytes; the session is uncertain for good | | open | replication opens; the replica reads its remote position at its first sync; every later upload is the session's. An app stopped idle before this point is not closed: the replicator opens, ships what the app wrote, then closes cleanly | |

Admissions, coverage and retirement (operative, rev 7.14)

This list, with §5.1 step 9 and the two tables above, is the operative rule set for writer admission (R12-4), mirroring claim rev 6.22 §6.4a's operative subsection item for item. Where any other passage of this spec reads differently (the restore contract's older wording in §5.1, the §7.8 rows as rev 7.11 had them, the authoritative-region table, the per-revision blocks of §14.2.2, which are history by construction), this text wins.

1. The record. Each admission appends {session, box, generation, region, predecessor: {session, box, generation, stamp}, predecessor_region, mode, coverage, covered, writes_lost?} to holder.admissions. The predecessor is the last record, never the holder's fields (INV-16); region is the admitted box's region, where its generation's objects are; predecessor_region is the last record's region, before any record the writer box's region, "" when the generation holds nothing anywhere; a warm admission continues the same generation in the same region, so its region equals its predecessor record's (a clean return's first admission is cold: an old source certificate does not certify the target's session). Born covered: item 5.
2. Coverage "" | sealed | clean-return, as §5.1 step 9 states it: sealed for a from_db seal of the stopped predecessor, clean-return for a clean rollback with src_covered, a target that gave its evidence and no declared-lost box, speaking for the target's probe session and the source's cut session only; "" otherwise, and without a certificate it records writes_lost (behind a lost target, one record for every session the target was admitted into since the cut, and a second for the source's cut session when src_covered is false, under its persisted cut.session): writes_lost (one) plus additional_writes_lost (a list), each {box, generation, session, remote_max_txid}, unique by (box, session) across both, one alert per declaration (R13-3, R14-2; INV-21). The legacy identity {session 0, generation "" (@root), holder.writer_box} is valid in both; every other declaration has a session above 0, and every declaration names a box, so a predecessor with no writer is not declared (INV-24, claim rev 6.24, R16-3). A writes_lost record declares the writes of the session it names and no other (INV-18, R12-1).
3. The baseline. A prepared generation from its pinned snapshot in the admitting box's region, opened once; otherwise the predecessor generation's remote in this region; in an unfinished run the newest generation of the run that holds an object in this region, else the marker's, walked as §5.1 step 9 says (R13-1): a covered foreign link is passed over, a covered local baseline refuses and alerts; the start restores the selected run generation rooted at [1, 1], the marker's through generation.json (R14-1); an empty generation outside an unfinished run is refused and alerted.
4. Stamps. A cold admission takes a new stamp except under KeepStamp (holder.stamp > holder.session); a clean return's CAS may name the source's generation and stamp again, leaving holder.session alone.
5. Coverage, completely. An entry becomes covered in exactly four ways (R13-2): at birth (a warm entry; an entry admitted while the claim holds an unscoped park-replica, or a park scoped exactly to holder.location, in its predecessor's region, claim rev 6.24); by publication; by CoverRegionPredecessors (item 6); by CoverParkedPredecessors (item 6). Publication: after the marker names the generation, one PublishGeneration(observedOpID, observedPhase, observedSession, publishedGeneration, region, newID) requires holder.generation to be the published generation and an entry to name it, then walks every entry in order, skipping covered ones, as §5.1 step 9 states: no objects anywhere, covered, no chore; live again, left uncovered, no chore; in region, one deduplicated chore, covered; another region, uncovered, no chore, the walk continues. Every cold admission publishes. Retirement happens only through it or through item 6.
6. Parks cover what they retire. CoverRegionPredecessors(op, phase, region) runs inside the CAS that queues a region's park of the whole location: the commit's park of the source region, the target's release and the console's lost-target release for the target region. It covers every record whose predecessor's objects are that region's and queues nothing. CoverParkedPredecessors(op, phase, region, generations) runs in the CAS that queues an at-rest park-sweep and in the CAS that acknowledges it, and covers only the records whose predecessor is among the generations that sweep parks. INV-17 checks the composition as each whole-location park completes. A foreign-region predecessor is never queued into its region from another one.
7. Starts. The admitting CAS first; a new agent process stops a running app, admits a new session and restarts it; failed starts are the retry policy's, five under one session with a doubling backoff; the failed-host marking is a serving wake's at the fifth failure; a probe attempt ends at the fifth failure, at its 30 s window, checked before each start and before readiness is accepted, or at a late readiness, counts one budgeted try (three for a landing, nine for a recovery) and never marks the host failed.
8. Retention and lost boxes. holder.admissions is trimmed conservatively: covered records from the front only, to eight, never past an uncovered one; no compaction. A declared-lost box's timers are declared on the console's record and alerted; adoption sets holder.writer_box to the pre-release writer's box.
9. Park state (claim rev 6.23 §2; R13-4, R14-3 to R14-5, R15-1; §6.4). Every remote chore carries a persisted park scope from its queuing CAS (a delete's or adoption's park binds one before its first step), {location, incarnation, evidence_at, request_limit} in the claim's grammar; evidence_at is the original evidence or fencing bound (a staging lane's is its seal bound, the seal plus the lease), never the cleanup's start; every retry uses it; every acknowledgement, a staging lane's included, waits a listing later than evidence_at + H, H the signature-age limit plus request_limit. A park executes strictly within its scope's namespace (claim rev 6.24 §2, R16-1, R16-2): the sweep's chores are grouped by location, each with its archive incarnation; an instances/… scope never touches moves/ and the legacy instances/<host> scope excludes child incarnations; INV-23 checks membership for every reference a chore archives or deletes, fresh or replayed from a persisted manifest (R17-1). A free host's at-rest sweep is a holderless parking op with intent.park_sweep, no exec and no holder, which blocks the successor create until FreeAfterPark frees the claim in its last acknowledgement's CAS; on a serving host sweep chores carry session:<holder.session>.

History. The paragraphs that follow and §14.2.2's per-revision blocks record how these rules were reached; where they differ from the list, the list governs.

An admitted writer that dies between its CAS and its marker leaves holder.generation naming an unfinished generation generation.json does not (R10-2): its journalled predecessor is the live baseline, no chore retires it and the sweep protects it. The next admission, by this box or another op.exec box, reads the lag through holder.admissions (§5.1 step 9): the marker names the latest admission's predecessor, or the predecessor of a chain of unfinished admissions, so this is the normal state and no alert; a holder.generation that holds objects (the first upload landed) has its marker published again, from the operation's build journal for a prepared generation, and the retire chores queued; an empty one is skipped and the baseline is the nearest generation of the chain that holds an object, else the marker's; the new marker retires them all. An empty holder.generation the journal does not explain is unexplained missing data: the start is refused and the box alerts. A clean rollback's return leaves the marker naming a descendant of holder.generation; the source publishes the source generation's marker again from its last version before anything else. holder.admissions lives in the holder, so an admission unfinished at a release (an abort released over a source admitted a tick earlier) stays explained through the next operation. A marker that lands after its writer died, before the writer's PublishGeneration, leaves the predecessor unretired: the next admission's PublishGeneration retires the predecessor of every record not yet covered. A pre-flip round never forces a sync on a session whose start is unfinished: there is no open replicator, and a forced upload would write the first upload's key with other bytes.

Behaviour change against today's activator. Today Restore materializes the local database from S3 only when it is absent, "a no-op when the warm-cache copy is still on disk", and doWake relies on that: "when it's still on disk it is the warm cache: on one box, with the lease held, the local copy can only be what we ourselves checkpointed at the last sleep" (internal/activator/activator.go). Rev 7.10 changes this: every wake restores, warm or cold. It costs a restore per wake, one pass over the database from regional S3 at the local rate (§7.3 prices it, and prices the probe's restore per attempt), and it loses the acknowledged writes a crash left unuploaded, which the warm cache preserved on a same-box restart; those are declared through writes_lost and an alert. The loss is normally within the replication interval (§7.3, the sync class), the window between syncs; a failed or stalled upload extends it back to the last upload that landed, so the bound is the interval in operation and the age of the last durable upload in a fault (R10-8). Two more changes against today's activator (rev 7.11): the admitting CAS precedes the app start, so a start that fails leaves a session and a retry policy behind it rather than nothing; and an agent that restarts under a running app stops it and re-admits, where today's activator reattaches to the running unit. What it buys is one rule with no provenance machinery: a box's database is always the certified remote's, so a cached, truncated or foreign copy can never be served (R9-1), and the claim alone decides who writes what.

A cold admission costs the three local passes of an install (§7.3) for an operation's prepared generation, one full upload for a fresh one, none for an empty one, and a dead generation to park. It runs after every crash, OOM kill, lease takeover or lost disk, after a close that could not certify (a retry, a timeout, a lost response, R9-5), and at the first wake of a created incarnation or an adopted legacy host, whose origin generation has no writer yet. It does not run after a certified close.

The source that lost its disk during a revert or a rollback has nothing to verify against the digest it recorded at the stop: its recovery skips the digest check and its probe is admitted like any other writer (rev 7.9, R8-2); a target that never restored a database returns nothing dirty (rev 7.10: the probe's admission restores it, so a target whose probe never started has none).

8. The archive (codex 19)

8.1 Content

A tar of the files directory (F4, without .files-gen) and <host>.env (F6), in sorted path order, with owners and times zeroed and modes kept, so equal content gives equal plaintext. Regular files and directories only; a symlink, device, FIFO or socket refuses with its name. The 256 MiB cap is enforced while streaming (M5). Then zstd.

8.2 Sealing

For the deployment's config keypair (P-256 ECDH, internal/appconfig/crypto.go:44-59): a fresh 256-bit data key; AES-256-GCM over 1 MiB chunks, each nonce the chunk index, the last chunk flagged; the data key sealed with appconfig.Seal (crypto.go:86, fresh ephemeral key and nonce); a manifest with the sealed data key, the sealed object's sha256, the plaintext sha256, the per-file list (path, size, sha256), the op id and the incarnation. Encryption is randomized and never made deterministic.

8.3 Identity, publication, retention

• plain (plaintext digest) identifies content; sealed (ciphertext digest) identifies one immutable object. Content checks use plain; fetches use sealed.
• The plain digest of the files directory as stopped is computed at stopped without sealing, so recoveries have a baseline before any archive exists (§7.4).
• One sealed object per cut: written create-only to move-snapshots/<host>/<move id>/files-<sealed>.{sealed,json}, then its digests recorded in the record, then copied to staging files/. A crash before the record write leaves an unreferenced object; after it, replay reuses the recorded object (codex 19).
• Retention: the source's snapshots stay until F3; staging is parked at finalization (§7.9, §7.8).
• The files manifest (region HA L17; rev 7.19). The archive is the transfer; durability between moves is region HA §5.6's files publisher: immutable objects <location>files/<generation>/objects/<seq>-<sha256> and one manifest per generation, replaced with If-Match. Every installation, a landing's and a dirty return's included, publishes its installed files directory and <host>.env as that generation's first manifest in local, before .files-gen; the serving writer then keeps it current per the app's files_durability. The classifier treats files/<generation>/ as that generation's (claim L13), so a park-generation chore retires it with the generation, except objects the files live set names.

9. Changes to existing code (codex 13, 15)

9.1 Config render for a held row

SyncExec skips non-ready rows (internal/appconfig/syncexec.go:643-647) and writes an ack only when a file changes (:1159). New: appconfig.RenderHeld(ctx, rt, op) renders the same file, writes it, and writes a move-bound ack with the op, the file's sha256 and the bundle etags, changed or not. SyncExec keeps skipping held rows, so the two never race on one file.

9.2 Release materialization for a held row

release.Adoptable excludes non-ready rows (internal/release/adopt.go:816-819). New: release.MaterializeHeld(rt, op, version) stages exactly the pinned release (move.inputs.release).

Amendment, 2026-10-12 (Paul's ruling on T7, Q2.1). With host claims on, the stage and the publication are split. T7 (§7.3) stages the pinned release and verifies it without touching live/<host> (release.StageHeldVerified). The landing's configured step, and a dirty return's, publishes it under the claim's held-release selection, whose identity names exactly that version (release.MaterializeHeldUnder), and then reads it back as T7 does with claims off (release.VerifyHeldLive). The held render in the same step runs under a held-config selection (appconfig.RenderHeldUnderBefore, which keeps carry (c)'s journal before the write), and a merge that is not the pinned inputs is the "configuration changed" rollback before anything is selected or written. With host claims off, MaterializeHeld and RenderHeld run as before. The landing still refuses at checking under the claim (RollbackClaimWired, ruling G16) until this box's moves source is registered with the claim.

9.3 The activator

• ProbeWake (§7.7); RetireExcept keeps held entries.
• ReconstructStopEvidence (§5.3); strict spawns under a move.
• The start check (§5.1) in Start, Seed and ProbeWake, reading the claim.
• Restore writes <dbPath>.gen and parks a warm file of another generation. promoteStagedReplica and its call (backend_exec.go:290) are deleted.

9.4 Timers frozen, drained and restored (codex 15, R1-15 partial)

• Drained: entering stopping, the source waits until the runner has no delivery in flight for the host (the runner's per-host claim, internal/schedule/runner.go:154) before taking evidence, so a delivery that started before the hold cannot advance a row after the snapshot.
• Frozen: the runner skips, with no bookkeeping, any held row (today a blocked delivery still advances attempts, runner.go:345-351), and the converger neither upserts nor prunes timers for a host whose claim op is moving (internal/schedule/converge.go:114, :223-241).
• Replaced exactly: Registry.ReplaceTimers(host, rows) deletes and inserts in one transaction, preserving next_at, due_at, attempts and registration. UpsertTimer resets them on rearm (internal/registry/timers.go:46-55), so it is not used here.
• The runner's own prune (joint N14). A second actor deletes timer rows: the runner's daily sweep (internal/schedule/runner.go:260), whose PruneTimers removes aged completed once-timers even for a live host (internal/registry/timers.go:183). It cannot be frozen without stalling every other host, so the snapshot is canonical instead: the timers digest covers active rows and their bookkeeping, and excludes disposable history (completed once-timers). Pruning history therefore never changes the digest a clean recovery compares. The model includes history in the digest and finds clean rollbacks stuck on a "mismatch" the runner caused; it lets a held row's refused deliveries advance bookkeeping and finds the same.
• Carried timers are acknowledged state. A once-timer the app registered is a write the app was told succeeded. The model counts it as one for INV-2, and finds timers lost when the files marker is written before the timers are imported (R2-6).
• Declared schedules converge again once the claim returns to serving.
• relocating holds (region HA L17; rev 7.19). The same freezing and draining apply to a row held by region HA's relocating op: the runner skips the held row with no bookkeeping, the converger neither upserts nor prunes the host's timers while the claim op is relocating, and the relocation's release flush carries the timers snapshot as §7.4 stopped does.

9.5 Edge

None in Phase 1. Platform-domain hosts get the 503 pending page during the window (#174, internal/edge/pending.go); custom domains get 404 until F1.

9.6 Reconcile (codex R2-4)

• Mint: while the claim holds a move operation, a participant box mints the host's row held (landing on the target after the flip, restoring on the source during recovery), never ready.
• Removal: never removes a row of a host whose claim names this box as a participant, whatever the record's region (reconcile.go:1114-1159; claim spec §8, "rows that a running operation lists as participants are retained"). The move worker deletes it at its own finalization step.
• Orphan retirement (claim spec §8, a row whose incarnation is not the claim's holder) does not act on a participant row of a move op; a move never changes the holder, so the case cannot arise for a live move, and the guard makes that explicit (§19 K9).

10. The secrets key and the shared fingerprint

The platform reads no SSM parameter at runtime. An exec instance's secrets reach it through its config bundle, opened with the box's CARLOS_SECRETS_KEY, so a target needs only the deployment's key.

Shared with nearest-region R9. One edges-file field for both specs:

• name: secrets_key_fp, in edgesFile (internal/host/edgesfile.go:155-176, written at :603-605);
• format: "sha256:" and 64 lowercase hex digits of SHA-256 over (*ecdh.PublicKey).Bytes() (the uncompressed P-256 point) of the box's CARLOS_SECRETS_KEY;
• not omitempty, like hibernation_configured: absent means unknown, "" means no key;
• the console computes the same over CARLOS_SECRETS_PUBKEY. A box is key-ready when its value equals the console's.

11. Versions and the protocol floor (codex 7)

• Every box publishes moves_protocol: 1; the console reports its own. The request door and T1 refuse unless every box in both regions and the console are at or above it, and every box is claim-aware (§19 K10).
• Before the first production move the deployment writes control/moves-protocol.json {"min": 1, "min_release": "vX.Y.Z"}, create-only. Every path that activates an executable refuses a release below it: carlos system apply, explicit rollback, and automatic boot recovery of carlos.prev (internal/host/systemapply.go:901, restoring through :817), which validates .prev and any outstanding 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,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).

12. The operator surface (M16, M18)

API. The existing doors (internal/console/authcli.go:625-628). Every move mutation requires an operator (Store.IsOperator, internal/console/store.go:1858); others get the family's 404. Instance-role tokens keep the status GET only (M18), which closes the member-minted token path (apiinstances.go:1554) for moves (codex 11). New: POST …/move/resolve (§7.10). GET …/move?detail=1 adds phases, reports, evidence and reasons.

CLI. docs/site/cli.md gets the heading in the same change (internal/docsite fails the gate otherwise).

carlos move --host <h> --to <region> [--manual-cut] [--no-wait]
carlos move status  --host <h>
carlos move cut     --host <h>
carlos move abort   --host <h>
carlos move resolve --host <h> --retry | --declare-lost <box>

--wait is the default; exit 0 done, 3 rolled back, 4 stuck or waiting, 5 refused.

13. Observability

• Move log: one object per event under moves/<acct>/<app>/<host>/<op id>/ in the deployment bucket, beside the reports and evidence.
• Timings: prepare, cut, land, and offline (cut_at to the open, or to the source's reopen after a rollback), each against its budget.
• Paging: rolled_back (warning); stuck, rolling_back past release_deadline, a refused start check, and a refused stop evidence (stray process) (incident); preparing with no promotable round for 60 minutes (warning); a move converted to relocating by a termination fence with no live box in its region (incident, once; M-C22 is the operator's line, rev 7.20).
• Member stream: each transition is an event on the app's platform log (emitEvent, internal/activator/logsink.go:31-36).

14. Tests

14.1 Unit and integration

Every transition and guard; each readiness check failing alone (T4 against MinIO); every journaled phase crashing between its individual side effects and replaying; ReconstructStopEvidence against a real cgroup v2 hierarchy with a forked descendant that closes its descriptors and outlives its parent; the start check; RenderHeld, MaterializeHeld, ReplaceTimers; reconcile keeping participant rows.

14.2 The executable joint model

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

Rev 6: strict classification (J2-R2-10). mutate.sh reports CAUGHT only when the run completed and reported a seed that violated an invariant, with the seed number parsed from its output. A build failure, a panic, a timeout or unparsable output is ERROR, never a detection; every run's log is kept. expected-outcomes.txt beside the script declares the rules not expected to be caught alone (liveness-only, unreachable, combination-only, unexercised), each with its reason. The sweep exits nonzero on any ERROR, any unexpected MISSED, and any expected miss that is now caught (STALE).

The evidence policy (Paul, 2026-10-06). The deep sweeps were using half the shared box's cores and starving other agents. From rev 7.14 on: each revision runs the gate (300 seeds plus the witnesses) and one mutation sweep at 3,000 seeds, serially, with HOSTLIFE_PAR=2 under nice -n 19, never alongside another sweep or a baseline; baselines run at 30,000 seeds only; the 100,000-seed baseline and the 30,000- and 100,000-seed mutation sweeps run once, at a final pre-implementation checkpoint, and only when Paul says so. A table cell or column those sweeps would have filled says "not run" for the revision, never a placeholder and never a number carried over from an earlier revision. Rev 7.14's 100,000-seed baseline had already run, clean, before the policy was set and is reported in §14.2.3; its 30,000- and 100,000-seed mutation sweeps were stopped mid-run and are not evidence.

Rev 7.14: TestInterruptedCleanReturn, INV-20. go test runs the positive case of the run walk across regions beside the witnesses: a clean rollback's fresh source admission dies before its first upload and the recovery walks R → T → S, then one more interrupted admission walks R2 → R → T → S; both restore the source's data. INV-20 is checked in the create's claim CAS: no obligation may be outstanding when a create claims a host.

Rev 7.13: INV-17 at the park, TestProbeWindow. The oracle for regional coverage runs when a whole-location park of holder.location completes in a region, not at the end: a record whose predecessor's objects were there and that is still uncovered is INV-17 at that CAS (a record born after the park is not in question). go test runs TestProbeWindow beside the witnesses: the landing probe's environment ready k steps after the attempt's first start, for k = 29, 30, 31.

Rev 7.12: the final oracle runs the recovery. When the run is quiescent with the serving host at rest after a session that did not certify, the final oracle no longer exempts the acknowledged, unuploaded writes as a prospective declaration (R10-6: that recorded and alerted nothing, with writes-lost off too). It wakes the host, runs the cold admission for real, drives its chores to quiescence, and judges the database by what the admission declared; a recovery that cannot run within the bound is