carlos / platform Public

Download this file

File too large to show in full — download it above (showing a truncated preview below).

1	# Move any app or instance to another region: Phase 1, a safe single-instance move
2
3	**Date:** 2026-10-06
4	**Revision:** 7.24.
5
6	- **Rev 7.24** lets a move target the home region (moves into home,
7	part 2; plan `docs/superpowers/plans/2026-10-15-moves-home-region-part2.md`,
8	amadan #236). Phase 1 moves between two non-fleet placements, into home
9	only with host claims on (§2). §7.1 refuses a target of home on a
10	console without host claims, or a home whose box sets a region code of
11	its own. §16 F2 records home as a target as delivered by that plan.
12	Paul's rulings of 2026-10-15, decided: **R1**, home targets only under
13	host claims; **R3**, `--to` takes the home's configured name, with no
14	`home` keyword, and `carlos move back` stays a follow-on; **R5**, no
15	protocol version bump (a home box without the new T3 fails T3 and waits,
16	fail closed; boxes roll before consoles); **R7**, a home target may be
17	the console's own box (the records and the claim are durable, so a box
18	lost mid-landing delays recovery and loses nothing). R2(a) and R6 bind
19	the rehearsal runbook, not this spec.
20	- **Rev 7.23** records Paul's ruling M4 (2026-10-10, moves Plan 5 delta
21	pre-flight after claim Plan 10): **every close is record first, then
22	the claim's release.** Rev 7.22 released the claim to `serving` first
23	and cleared `move` second (§7.5, §19 K8). Claim Plan 10's move-recovery
24	grant closes the record first, and a serving claim with a live move
25	record can never acquire that grant, so the two orders could not both
26	stand. Each close (the commit's, a rollback's, a revert's, an abort's)
27	now checks that no obligation of the op remains, CAS-clears `move` into
28	`last_move`, and then releases. A crash between the halves leaves the
29	record at rest and the claim still under the op with nothing owed; the
30	box passes are driven by records with a live move and do not come
31	back, so the console's recovery pass releases from `last_move`.
32	Amended: §7.5, §7.8 finalization, §7.9 step 5, §7.11, the `reverting`
33	table's `opened` row, §14.2.2's model row and §19 K8. **The model**
34	(`internal/sim/hostlife`, moves Plan 5 Task 7 fix round 1) closes the
35	same way: a box's close CASes the record (`last_move`), and on every
36	third step stops before the release; the recovery pass releases from
37	`last_move` (`fixRecord`). A new invariant, K8, fails any move's release
38	whose record still carries the move, and a new rule,
39	`record-first-close`, whose mutation is rev 7.22's claim-first close, is
40	caught by it (1,060 / 3,000 seeds, first seed 1; no witness). The
41	3,000-seed sweep of every rule otherwise matches its expected outcomes. The `claim-cas-opid` witness is
42	restaged: its stalled goroutine is now the source between the record's
43	close and its release (§14.2.5).
44	- **Rev 7.22** answers **joint round 19** (`CODEX-FINDINGS-JOINT-R19.md`,
45	"R19-1", the round's one finding, P2) and fixes the install
46	manifest's keys. **R19-1:** rev 7.21 bound the prepared files manifest
47	to "the holder location and generation" during `local`, but
48	`holder.generation` still names the source's pre-move generation `S`
49	until the probe's admission (§7.14, §9.4), and claim rev 6.30 binds the
50	manifest to the **prepared** generation `P`; a manifest bound to `S`
51	could never be `P`'s baseline and an ordinary cold landing would block.
52	§7.6 now binds the manifest, and places it, under the installation's
53	**prepared destination generation**: `g-<move id>` for a forward
54	landing, the prepared return generation `g-<rollback id>` for a dirty
55	rollback; `holder.generation` is unchanged until admission. Plan 2
56	Task 10's `local` step matches. **`install.json` keys:** §7.6 names the
57	snake_case keys claim Plan 6's `install_contract.go` tags the shared
58	`moves.InstallManifest` with (`snapshot_txid` for the Go field `N`).
59	The model encodes no manifest binding (§14.2.6); no rule changed, gate
60	only.
61
62	- **Rev 7.21** answers **joint round 18** (`CODEX-FINDINGS-JOINT-R18.md`,
63	cited "R18-n"; not clean: one P2, three P3s, no P1). **R18-1 (P2):**
64	the first files manifest of an installation is not the session-bound
65	publisher's, since no target session exists until `probing`; §7.6 now
66	has the landing build the initial immutable files objects and a
67	create-only **prepared manifest**, mirroring claim rev 6.30
68	(73b1b9dc) exactly: published by `op.exec` before any session exists,
69	in a phase that permits installation; bound to `{location,
70	generation, op id, installation stamp}`, naming exact versions, at
71	sequence 0, never replaced, retired with its generation; the
72	session-bound publisher starts only after the first admission, takes
73	that manifest by exact version as its baseline and publishes from
74	sequence 1 (region HA spec 1 §5.8's prepared-manifest build, `:809`,
75	is the same rule). **R18-2 (P3):** §7.10's "before the flip" is stated
76	as "the record has not entered `landing`", the flip's record CAS,
77	distinct from the final commit. **R18-4 (P3):** M-C22 no longer
78	promises that nothing is lost; it describes the retained remote data,
79	the pending recovery and the declaration a restart may make (§20).
80	R18-3 is the claim's (§11 there). The model encodes no publication
81	timing beyond installing the files at the installation CAS, which is
82	the prepared manifest's moment (§14.2.6); no rule changed and no sweep
83	was run.
84	- **Rev 7.20** aligns with claim rev 6.28 (4ffe8a0d), which adopts region
85	HA's L1 to L20 at its sections (`CODEX-ANALYSIS-REGION-HA-L1-L20.md`
86	beside it). **The fence reference** (§7.10, moves C7): every transition
87	that relies on a termination fence writes `op.journal["fence.<box>"] =
88	{"enrollment","key","sha256"}`; a `loss.<id>` intent cites the same
89	reference; `ReturnToSource` accepts a fence only through it,
90	re-verifying the record; an automatic declaration needs no quarantine
91	revision and no operator (L4). **A source terminated before the flip**
92	(§7.10): the fence converts the `moving` op to `relocating` in one CAS
93	(exec `"none"`, stamp and generation preserved, `relocating` at
94	`pinning` in the source region, every obligation untouched, the lane's
95	`park-replica` queued when not yet owed); in a one-box region it holds
96	at `pinning`, safe but **not recovered**, until region HA enrolls a
97	replacement box; the operator sees `waiting for a box in <region>` and
98	one alert; after the flip the conversion is refused. This replaces rev
99	7.19's "the move aborts". **L13** (§7.6, §8.3): the files manifest is
100	claim C3's, §6.2a's and P6-D3's: the session-bound publisher,
101	origin-qualified manifest references, files reachability independent of
102	the database baseline. **Scope ruling:** Phase 1 is for one-box regions;
103	a move into or out of a region with more than one eligible box is
104	refused at the door with new copy (M-C21, pending Paul) until region
105	HA's own model and plan cover multi-box; the model stays one box per
106	region (§14.2.6). The model gains rule `fence-converts-moving` and
107	witness `wFenceConvertsMoving` (§14.2.5).
108	- **Rev 7.19** records Paul's rulings of 2026-10-06 on amadan #236 as
109	claim rev 6.27 (989ee349) §1.1 states them, and folds in region HA's
110	requests L14 to L17 (spec 1 rev 5.4, branch `design-region-ha-rev5`,
111	`2026-10-04-region-ha-box-placement-design.md` §9). New §0.5. **P7,
112	cold-only admissions:** until a reviewed Litestream fix (#234) makes a
113	clean-close certificate safe, every admission is cold, no certificate
114	is issued, and nothing in Phase 1 depends on warm; §5.1 step 9's warm
115	mode stays as specified future behaviour. **L14** (§7.10): a target
116	terminated mid-move is taken off the move by the termination fence,
117	as M16's evidence, automatically, under the before-commit rules.
118	**L15** (§7.1, §7.3, §19.1): a move names its target box in the start
119	CAS, chosen by region HA's `choose()`; readiness, evidence, install and
120	recovery bind to it. **L16** (§5.1, §7.6): the install is one shared
121	routine with relocation, fed by a sealed staged replica or a pinned set
122	of remote versions. **L17** (§6.1, §8, §9.4): every installation writes
123	a files manifest in its new generation; the archive at the cut stays;
124	timer freezing and draining apply to `relocating` holds. **L18**
125	(§14.2.6): the model stays at one box per region plus replacements;
126	the two-box extension is stated as a limit, not done here. Nothing in
127	the protocol of rev 7.18 changes otherwise. Conflicts and claim
128	changes these raise are listed in `region-ha-conflicts.md` (the
129	coordinator's record) for platform-1e.
130	- **Rev 7.18** folds in **joint round 17**'s two P3s
131	(`CODEX-FINDINGS-JOINT-R17.md`, cited "R17-n"); the round was **clean**,
132	A, B and C ready for moves Phase 1 implementation planning, after
133	seventeen rounds. Claim rev 6.26 (98b45332) fixes R17-2 on its side;
134	the code is main at 67547f5. **R17-1:** the model's INV-23 now checks
135	scope membership for every reference a scoped park archives or
136	deletes, in the manifest it builds and in a persisted manifest it
137	replays, whatever rules are on; an out-of-scope reference is a
138	violation and is never acted on (rev 7.17 checked candidate keys, and
139	only with the confinement rule off); the operations' own parks run
140	under a scope of `holder.location`; `TestForeignManifestReplayRefused`
141	replays a manifest naming another incarnation's key under a valid
142	scope. **R17-2:** the scope grammar's `moves/<host>` form is used by a
143	delete's park of the staging namespace (§5.2) and by an at-rest sweep,
144	each while no operation stages there, as claim rev 6.26 says. No rule
145	change (107 rules; 73 witnesses): the gate alone, per §14.2.1; the
146	mutation tables stand at rev 7.17's.
147
148	- **Rev 7.17** answers **joint round 16** (`CODEX-FINDINGS-JOINT-R16.md`,
149	cited "R16-n") and is written against **claim spec rev 6.24**
150	(0b821896: the legacy identity, scope namespaces, the narrowed
151	born-covered) **and rev 6.25** (413b12cb, which answers this
152	revision's four notes: §5.2 now has a delete park only
153	`holder.location` plus `moves/<host>`, never the whole host prefix,
154	as the model does); the code the model aligns with is **main at
155	67547f5**, which carries platform-1e's R16-1 and R16-3 fixes
156	(c7e595b, "park, hostclaim: scopes stay in their own namespace; the
157	legacy session-0 loss identity") and the first-admission fix (a
158	created incarnation's first admission declares nothing; note 2 was
159	an E bug); §22.23 has every disposition. **A park executes
160	strictly within its scope** (R16-2): the model's sweep groups residue
161	by the location it belongs to, an incarnation's own, the legacy
162	`instances/<host>` (never a child incarnation) or `moves/<host>`, and
163	queues one chore per location with that scope and its archive
164	incarnation; the archive names the incarnation; every scoped chore's
165	listing is confined to its scope and INV-23 checks every key a chore
166	would archive for membership, not only the location's syntax; the
167	delete parks the deleted incarnation's own location and the staging
168	namespace, never the whole host prefix. **The legacy identity is
169	session 0** (R16-3): an adopted host's pre-claim writer is `{session:
170	0, generation: "" (@root), box: holder.writer_box}`, valid in both
171	`writes_lost` and `additional_writes_lost`; every other declaration
172	has a session above 0, and a declaration always names a box, so a
173	created incarnation's first admission, whose predecessor has no
174	writer, declares nothing (INV-24); the model no longer gives adoption
175	session 1; `TestLegacyLostTargetReturn` walks adopt → a move with
176	`src_covered` false → a cold target admission → the target declared
177	lost → the return declaring the target's session and the source's cut
178	session 0. **An instance park never touches staging** (R16-1):
179	`TestStagingSurvivesLegacyPark`. **Born covered, narrowed** (6.24 item
180	5): only an unscoped `park-replica` or a park scoped exactly to
181	`holder.location`. Rule `scope-membership` (107 in all); witness
182	`wSweepScopeMembership` (73 in all). Evidence under the policy of
183	§14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.
184
185	- **Rev 7.16** answers **joint round 15** (`CODEX-FINDINGS-JOINT-R15.md`,
186	cited "R15-1") and is written against **claim spec rev 6.23**
187	(876d6908, §2's park scope: the location grammar, the archive
188	incarnation, `evidence_at` always the original evidence or fencing
189	bound, one deadline for every scope); E is merged to main as 99084d7,
190	F merges next; §22.22 has the disposition. **Every remote chore
191	carries the claim's scope from its queuing CAS** (R15-1): `location`
192	exactly one of `instances/<host>`, `instances/<host>/<incarnation>`,
193	`moves/<host>/<op id>` (a move's staging or a rollback's return lane)
194	or `moves/<host>` (the staging sweep), no trailing `/` (INV-23);
195	`incarnation` the location's own, the staging op's holder incarnation
196	or, for a free host's `moves/<host>` sweep, the newest retired one;
197	**`evidence_at` the original bound**, the cut's stop for the commit's
198	source park, the release or the declaration for the target region's,
199	**the seal bound for a staging lane** (the time after which no staging
200	writer, its lease holder included, can still write: the seal plus the
201	staging lease), the listing for a sweep, the publication for a
202	generation chore; **never the cleanup's start time**. **One deadline
203	for every scope, staging included:** acknowledge only after a listing
204	later than `evidence_at + H`; there is no separate staging contract
205	(rev 7.15 bound a staging park at cleanup and then kept the seal's
206	quiet time instead, which Astra's example exposed: sealed at 100,
207	deadline 560, a cleanup first running at 600 must acknowledge at
208	once, not at 660). Witness `wStagingScopeDeadline` (delayed cleanup
209	through an agent restart; INV-9 under the mutation);
210	`wParkScopeSurvivesRestart` takes its deadline from the persisted
211	scope. Rules unchanged (106); witnesses 72. Evidence under the policy
212	of §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.
213
214	- **Rev 7.15** answers **joint round 14** (`CODEX-FINDINGS-JOINT-R14.md`,
215	cited "R14-n"), against claim spec rev 6.22 (0bf2f49f) with
216	platform-1e's answers to the six rev 7.14 notes, E f0127321 and F
217	d7621a29, both MERGE-READY there; §22.21 has every disposition. **The
218	start restores what the run walk selected** (R14-1): the open state
219	carries the restore mode, the marker's generation through
220	`generation.json` or a run generation rooted at `[1, 1]`, so the start
221	and the recovery oracle use one selection; witness
222	`wIntermediateBaseline` (R's first upload pending at its crash, an
223	empty R2, R's upload landing). **One `writes_lost` plus
224	`additional_writes_lost`, unique by `(box, session)`** (R14-2): the
225	source's cut session joins the list under its persisted identity, the
226	separate representation is gone, one alert per declaration, INV-21;
227	witnesses before and after the target's first admission. **The
228	horizon keeps its signature-age allowance** (R14-3): the park scope
229	persists `request_limit`, and every acknowledgement waits
230	`evidence_at + H` with `H` the signature-age limit plus
231	`request_limit`; a park-sweep acknowledges only after a verification
232	listing later than that (platform-1e's answer to note 2). **A running
233	holderless sweep admits another region's chores** (R14-4;
234	`TestJoinHolderlessSweep`). **Every remote chore runs under a
235	persisted scope** (R14-5): generation chores take theirs from the
236	publication, staging parks bind one before their first step, INV-22.
237	Two fidelity limits stated in §14.2.6 (occupancy by current objects;
238	the publication's precondition and trimming aligned with E). Rules
239	`restore-selected-baseline`, `unique-declarations` (106 in all);
240	witnesses `wIntermediateBaseline`, `wNoDuplicateDeclarationEarly`,
241	`wNoDuplicateDeclarationLate` (71 in all). Evidence under the policy
242	of §14.2.1: the gate, the 30,000-seed baseline, one 3,000-seed sweep.
243
244	- **Rev 7.14** answers **joint round 13** (`CODEX-FINDINGS-JOINT-R13.md`,
245	cited "R13-n") and is written against **claim spec rev 6.22**
246	(0bf2f49f, which adopts rev 7.13's seven notes in rev 6.21 and
247	answers R13-1 to R13-3; rev 6.15 and 6.16 added the persisted park
248	scope and the holderless sweep), the library E on
249	`feat/hostclaim-r713` at f0127321 and the generation selector F on
250	`feat/hostclaim-genselect` at d7621a29; §22.20 has every disposition.
251	**The model's park state is the claim's** (R13-4): every remote chore
252	carries a persisted **park scope** `{location, incarnation,
253	evidence_at, request_limit}`, bound in a CAS before its first step or
254	at the sweep's queuing CAS, so a retry after an agent restart keeps the
255	original evidence time and never restarts the horizon; a free host's
256	at-rest sweep is a **holderless parking op** `{kind: parking, intent:
257	{park_sweep: "v1"}}` with no exec and no holder, carrying only scoped
258	remote chores, which blocks the successor create and frees the claim
259	again in its last acknowledgement's CAS (`FreeAfterPark`); on a
260	serving host the sweep's chores carry `session:<n>`; INV-20, a create
261	never claims a host over an outstanding park. **Coverage, completely**
262	(R13-2): an entry becomes covered in exactly four ways, at birth (a
263	warm entry; an entry admitted under a pending whole-location park of
264	its predecessor's region), by publication (which requires an entry to
265	name the published generation and walks every entry in order, skipping
266	covered ones), by `CoverRegionPredecessors` in the three
267	whole-location-park CASes, and by `CoverParkedPredecessors(region,
268	generations)` in the sweep's queuing and acknowledgement CASes, only
269	for the generations the sweep parks. **The run walk, precisely**
270	(R13-1): from `holder.generation` back to the marker's generation, a
271	link whose generation keeps its objects in another region is passed
272	over, covered or not; a link in this region must be uncovered, and a
273	covered local generation reached as a needed baseline refuses the
274	start and alerts; `restoreCalc` stays the reference and
275	`TestInterruptedCleanReturn` walks R → T → S and R2 → R → T → S.
276	**`additional_writes_lost`** (R13-3): the lost-target return's extra
277	declarations, one per target session since the cut, unique by `(box,
278	session)`, each alerted. Rules `persisted-park-scope`,
279	`holderless-park`, `covered-baseline-refused` (104 in all); witnesses
280	`wParkScopeSurvivesRestart`, `wFreeSweepVsCreate`,
281	`wCoveredLocalBaseline` (68 in all). Results in §14.2.3 and §14.2.5.
282	**The evidence policy** (Paul, 2026-10-06; §14.2.1): each revision
283	runs the gate and one mutation sweep at 3,000 seeds, serially and
284	niced; baselines at 30,000 only; the 100,000-seed baseline and the
285	30,000- and 100,000-seed mutation sweeps run once, at a final
286	pre-implementation checkpoint, when Paul says so. Rev 7.14's 100,000
287	baseline ran before the policy and is reported; its deeper sweeps were
288	stopped and are marked not run.
289
290	- **Rev 7.13** answers **joint round 12** (`CODEX-FINDINGS-JOINT-R12.md`,
291	cited "R12-n") and is written against **claim spec rev 6.14**
292	(dc146058, whose §6.4a has one operative subsection, "Admissions,
293	coverage and retirement (operative, rev 6.14)", and answers R12-4 and
294	R12-6; rev 6.13, b3825827, adopted rev 7.12's five notes) and the
295	library E at 47426cc1 (unchanged since round 12 judged it
296	merge-ready); §22.19 has every disposition. **Coverage is regional
297	and recorded** (R12-3): every admission record carries `region` and
298	`predecessor_region`; `PublishGeneration` walks the uncovered records
299	(a predecessor holding nothing anywhere is covered with no chore, one
300	in the publishing region gets its chore and is covered, one in another
301	region stays uncovered with no chore, and one that is the live
302	generation again is left uncovered too, a reading against item 5's
303	first bullet: covered, nothing would retire it later), every cold admission publishes, a prepared generation's
304	included, and **`CoverRegionPredecessors`** runs inside the CAS that
305	queues a region's whole-location park: the commit's park of the
306	source region, a rollback's park of the target region, the console's
307	lost-target release (note 5's discharge, adopted). Two readings for
308	the claim: a record admitted while such a park is already queued for
309	its predecessor's region is **born covered**, and the sweep's CASes
310	cover the records whose predecessors it parks. INV-17 checks, as a
311	whole-location park completes, that no record whose predecessor was
312	there is uncovered. **The loss oracle matches the declared identity**
313	(R12-1): acknowledgements carry the writer session and generation of
314	the process that gave them, a `writes_lost` record exempts the writes
315	of the session it names and no other, the source-cut declaration
316	stays separate, and a declared-lost target's **every** session since
317	the cut is declared, certified or not (a probe session that certified
318	and a warm continuation that did not are two, and no return lane
319	carries either's writes); a two-session witness (INV-18). **The probe deadline
320	is checked before each start and before readiness is accepted**
321	(R12-2): an expired attempt never starts, a late readiness is not
322	accepted, INV-19 at every probe acceptance, and `TestProbeWindow`
323	walks k = 29, 30, 31. **One operative rule set for admission** (R12-4):
324	§7.14 states it, mirroring claim rev 6.14's structure, and the
325	passages that disagreed are corrected or marked history: the restore
326	contract's "after installed and probed", the dirty-return region
327	rows, the start table's failed-host marking (a serving wake's only; a
328	probe never marks the host failed), the recovery limit (nine attempts,
329	R12-5), and `holder.admissions` retention (conservative, no
330	compaction). The absent-marker sweep fault has its own rule and
331	mutant, `absent-marker-origin`, so `wOriginSwept`'s evidence no longer
332	rides on `baseline-live`. Rules `foreign-region-uncovered`,
333	`cover-at-park`, `session-scoped-loss`, `probe-window`,
334	`absent-marker-origin` (101 in all); witnesses
335	`wTwoSessionDeclaration`, `wRollbackBaselinePreserved`,
336	`wCommitCoverage`, `wCommitInterrupted`, `wCommitReplayed`,
337	`wProbeWindowAt` (65 in all). Results in §14.2.3 and §14.2.5.
338
339	- **Rev 7.12** answers **joint round 11** (`CODEX-FINDINGS-JOINT-R11.md`,
340	cited "R11-n") and is written against **claim spec rev 6.12**
341	(b202ea4e, which answers rev 7.11's eight notes and R11-2 to R11-5)
342	and the library E at 34224a29; §22.18 has every disposition.
343	**`holder.admissions`** replaces `op.journal.writers`: the record of
344	admissions lives in the holder, so it survives every operation,
345	release and new operation, trimmed to eight covered records and never
346	an uncovered one or the current predecessor. **An admission's
347	predecessor is always the last record there** (session, box,
348	generation), never the generation an operation chose for a restore
349	(R11-4): a clean return resets `holder.generation` to the source's
350	for the restore, but the predecessor is still the target's writer
351	(INV-16). **`Coverage`** `""` | `sealed` | `clean-return` replaces
352	`BaselineCoversPredecessor`: only `""` with no certificate records
353	`writes_lost`, and the record always names its coverage; a clean
354	rollback with `src_covered` declares nothing. **`PublishGeneration`**
355	replaces `QueueGenerationRetire`: the one retirement path, bound to
356	the observed operation and phase, legal while serving and inside any
357	operation a writer runs in (R11-5), chores with `op = op.id` inside an
358	operation and `session:<n>` while serving, only of predecessors in
359	`holder.admissions`; `""` and `"@root"` are one origin, so nothing
360	retires an adopted host's replica before a cold admission has
361	published a successor (R11-2). **The sweep reads an absent
362	`generation.json` as the origin** (R11-1), as the residue oracle does,
363	so an unfinished admission's chain protects an adopted host's replica;
364	witness `wOriginSwept`. **The final oracle runs the recovery
365	admission for real** when the serving session is uncertified and
366	judges by what it declared; an admission that cannot run is counted as
367	an unverified prospective declaration, never exempted (R10-6). **A
368	probe attempt's five app restarts share its 30 s readiness window**
369	(§7.7): the fifth failure or the window ends the attempt and the
370	operation counts one of its three budgeted attempts; a probe never
371	marks the host failed. §5.1, §7.8 and the authoritative-region table
372	carry no instruction left that assigns `holder.generation` outside a
373	cold admission's CAS or the clean return (R10-3). Rule
374	`clean-return-identity` (96 in all); witnesses `wCleanReturnIdentity`
375	and `wOriginSwept` (59 in all). Results in §14.2.3 and §14.2.5.
376
377	- **Rev 7.11** answers **joint round 10** (`CODEX-FINDINGS-JOINT-R10.md`,
378	cited "R10-n") and is written against **claim spec rev 6.10**
379	(3f916b05, with rev 6.9.1's answers to rev 7.10's readings); §22.17
380	has every disposition. **The admitting CAS comes first** (R10-1): before
381	the purge, the restore, the app start and readiness, so nothing the app
382	acknowledges is ever outside a writer session; a session belongs to the
383	**agent's replicator**, app restarts under the same agent stay in it, a
384	new agent process is a new session and stops a running app it finds;
385	failed starts are governed by a **retry policy** (five attempts under
386	one session with a doubling backoff from one step, then the host is
387	marked failed and gets no new session until an operator clears it).
388	**A cold admission's generation is unfinished until `generation.json`
389	names it** (R10-2): its journalled predecessor stays live, no chore
390	retires it, and the sweep never parks it; the retire chores are queued
391	by the marker's publication; a marker lagging behind
392	`holder.generation` that names the predecessor of the latest admission,
393	or of a chain of unfinished ones, is the normal state and no alert, any
394	other disagreement leaves the location untouched and alerts.
395	**§7.5, §7.6, §7.8 and §7.9 are rewritten around §7.14's protocol**
396	(R10-3): the commit and the `probed` CASes move no generation;
397	`holder.generation` is always the latest admission's. The admission is
398	**API-shaped like the library's `Admission`** (R10-4): `KeepStamp` only
399	when `holder.stamp > holder.session`, warm with an empty
400	`NewGeneration`, refused in `creating`, `deleting`, `parking`,
401	`purging` and `placing`, `BaselineCoversPredecessor` for a seal that
402	covers the stopped predecessor (compared against the seal's own
403	position; the journal says `baseline: sealed`, no `writes_lost`), the
404	empty-generation ancestor restore only for the latest journalled
405	unfinished admission. Serving-time chores use `op = "session:<n>"` and
406	an adopted host's root generation is `"@root"` (R10-5). **Disk-loss
407	faults exempt nothing** (R10-6): every exemption comes from a durable
408	`writes_lost` declaration, alert delivery is checked separately
409	(INV-14), timers are never exempted by the database rule, and a write
410	the remote holds is never declared lost while its writer's box is with
411	us (INV-15). **Startup PUTs are session evidence** (R10-7): the first
412	upload and the anchor enter the ledger, a retry after the client's wait
413	makes the session uncertain for good, server completion and client
414	response are distinct, and the bytes of a retry are the original's.
415	**The budget prices the new protocol** (R10-8): a restore per probe
416	attempt, the admission's overhead, a fresh generation's full upload on a
417	retried probe; the 2 GiB example runs to 117.9 s and admits one attempt,
418	the review's 2.5 GiB is refused at 131.2 s; the replication interval is
419	the normal window a failed upload extends. **Counters are structured**
420	(R10-9): the baseline logs `COUNTERS {json}`, the generator fails on a
421	missing field, §14.2.3 and the change note are regenerated. Two gaps the
422	rerun found beyond the review: a rollback is **clean only when the
423	source's own replica covered its stopped database** at the seal, else
424	the return carries the seal, whether or not the target wrote (§7.8,
425	rule `seal-return`, INV-15); and a pre-flip round never forces a sync on
426	a session whose start is unfinished. Rules `admit-before-start`,
427	`baseline-live`, `seal-return` (95 in all); witnesses for the
428	acknowledgement before admission, the parked baseline, the first-upload
429	and anchor retries and the uncovered return (57 in all). Results in
430	§14.2.3 and §14.2.5.
431
432	- **Rev 7.10** answers **joint round 9** (`CODEX-FINDINGS-JOINT-R9.md`,
433	cited "R9-n") under Paul's ruling to **simplify**, and is written
434	against **claim spec rev 6.9** (f6180ae4); §22.16 has every disposition.
435	**A box never reuses its local database.** Every admitted writer, warm
436	or cold, in every phase, purges the local database (an error-returning
437	purge; if it fails the writer does not start) and restores from the
438	certified remote: warm, the same generation up to the certificate's
439	`max_txid`; cold, the predecessor generation's remote. Lineage,
440	provenance and the `warm-provenance` rule are gone (R9-1 closed by
441	construction; its clean-close stale-database scenario is the witness
442	`wStaleLocalAfterClose`). Warm continuation needs only the certificate
443	for the observed session with a matching `max_txid`, and **any
444	`op.exec` box** may continue (claim rev 6.8.2 reverses rev 7.9's
445	same-box reading). **`holder.writer_box`** is set by every admission and
446	survives operation replacement; a cold admission of an uncertified
447	session records **`writes_lost {box: observed writer_box, generation,
448	session, remote_max_txid}`** in its journal entry and the box alerts, so
449	a crash with acknowledged, unuploaded writes loses them declared, never
450	silently (R9-2). **Only warm and cold survive** (R9-3): a first install
451	is a cold admission into an empty generation; `holder.generation` is the
452	only authoritative generation in every kind and phase; a probe or
453	recovery that opens replication is a cold admission that moves it; an
454	operation's prepared generation is opened once, by its probe's cold
455	admission, and never re-entered; a fresh generation roots at the
456	writer's full first upload, made after the CAS and before its marker;
457	a failed cold start leaves an empty, unpublished generation for the
458	sweep and the next attempt is cold again. Admission happens after
459	readiness and before any upload, and is **bound to the observed `op.id`
460	and `op.phase`**, serving's `""` compared literally, refused in
461	deleting, parking, purging and creating (R9-4; INV-13). Close evidence
462	is **client-observed success** for every request class, level-0,
463	compaction, snapshot and retention, with a sticky uncertainty for a
464	timeout or a lost response (R9-5). §14.2.5's tables are regenerated from
465	the retained verdicts (R9-6). The spec states plainly how today's
466	activator differs (§7.14: production keeps the warm cache and restores
467	only when the local copy is absent; this is a behaviour change, costing
468	a restore per wake and the unuploaded writes on a crash). Rules
469	`remote-baseline`, `writes-lost`, `admit-bind-op` (92 in all);
470	witnesses for the stale local database after a clean close, the silent
471	loss, the stale closure during a delete, a maintenance retry and a lost
472	response (52 in all); the whole-start-check witness is retired, subsumed
473	by regional restores. Results in §14.2.3 and §14.2.5.
474
475	- **Rev 7.9** answers **joint round 8** (`CODEX-FINDINGS-JOINT-R8.md`,
476	cited "R8-n") and is written against **claim spec rev 6.8** (5462d293),
477	whose rewritten §6.4a, writer sessions and epochs, answers R8-1 to
478	R8-4, and **rev 6.8.1** (a963d98d): only `op.exec` may open
479	replication, in every op kind; §22.15 has every disposition. **R8-1
480	(P1):** rev 7.8's `closed.json` was consumed by deleting the version
481	the writer read, which is not one-use under S3's semantics (an exact
482	version delete removes it and exposes an older version; a delayed or
483	replayed PUT recreates it); the certificate is now **per writer
484	session**, `closed/<session>.json`, never deleted, and what makes it
485	one-use is the **admitting CAS** that moves `holder.session` forward:
486	a certificate names a dead session from then on, whatever its stamp
487	and `max_txid` say. **R8-2 (P1):** rev 7.8 checked replication state
488	only at an ordinary wake; **every** path that opens replication is an
489	`AdmitWriter` now (a committed landing's serving, a restarted probe, a
490	reverted source, an opened rollback recovery, a push's writer), and a
491	cold admission runs **inside** the operation it interrupts, keeping its
492	kind, id, journal, participants and obligations (§7.14's phase table
493	says which box may be admitted in which phase; `op.exec` is handed
494	over before any probe or landing write). **R8-3 (P2):** a created
495	incarnation's first wake is a cold admission into an **empty**
496	generation: no snapshot `[1, 0]`, no anchor `[0, 0]` (the pinned
497	encoder refuses a zero TXID, `TestFact_R8_3_EmptyBootstrap`); the app
498	starts first and may create its database, and the first transaction's
499	file is the first upload. **R8-4 (P2):** the warm database is the cold
500	baseline only with **provenance**: a lineage file naming the
501	journalled predecessor's `{generation, session}`, the predecessor's box
502	being this box, and an integrity check; re-initializing a stamp record
503	never writes lineage. **R8-5 (P2):** the clean close's evidence is
504	every request of the writer's lifetime, level-0, compaction, snapshot
505	and retention, with a sticky uncertainty flag for a timed-out original
506	whose retry succeeded. **R8-6 (P3):** §14.2.5's retired-door rows
507	separate the historical results from the current ones. Rules
508	`writer-session`, `admit-everywhere`, `exec-writer`,
509	`warm-provenance`, `valid-ltx`, `close-evidence`; witnesses for a dead
510	session's certificate replayed, the collision during a committed
511	landing's serving and during a probe restart, a non-exec writer, a
512	warm database with a foreign lineage, an empty first wake, and a retry
513	that succeeds while its original stays unresolved. 90 rules, 49
514	witnesses. The model faults this round found before the final numbers
515	(a stalled worker replaying a finished build, the carried files
516	untagged, a source that lost its disk during a rollback, the biased
517	schedule's unbounded hold in the calm phase, a lost target's unfinished
518	admission blocking the rollback, every close outside `serving`
519	dropped) are in §14.2.2. Results in
520	§14.2.3 and §14.2.5.
521
522	- **Rev 7.8** answers **joint round 7** (`CODEX-FINDINGS-JOINT-R7.md`,
523	cited "R7-n") and is written against **claim spec rev 6.6** (b10547e1),
524	whose new §6.4a, writer epochs, answers R7-1; §22.14 has every
525	disposition. **R7-1 (P1):** the hazard rev 7.7's note raised is real
526	and now closed: litestream's level-0 PUT is unconditional and its key is
527	prefix, level and TXID range only (`TestFact_R7_1_UnconditionalPut`),
528	so a dead writer's in-flight upload for `[N + 1]` can replace the file
529	the next writer uploaded for the same TXID, or make its upload loop
530	skip it. **Two writers whose uploads could overlap never share a
531	generation** (§5.1 step 9, §7.14): a writer that stops cleanly drains
532	its uploads and writes `closed.json {stamp, max_txid}` once; a wake
533	continues the generation only if that marker exists, its `max_txid` is
534	the generation's remote maximum and its stamp is the box's own, and the
535	writer consumes it as it opens; anything else is lost replication state
536	and a **cold recovery**, an installing CAS into a fresh generation
537	(new `holder.generation`, new `holder.stamp`), built under stop
538	evidence from the warm database or the old generation restored,
539	published, then served, with the old generation parked as a chore.
540	Rules `recovery-generation`, `closed-marker`, `close-waits`; witnesses
541	for both completion orders, the initialization/remote-position race, a
542	stale marker, a crash before the marker, and a clean close that must
543	wait. **R7-2 (P2):** the cold-restore oracle checks required writes by
544	identity and compares the state with the replay of exactly the writes
545	the restored files carry; the per-key mask is gone, with the review's
546	counterexample as a witness. **R7-3 (P2):** every retention path keeps
547	the newest level-0 file (`newest-l0`, witness with the local position
548	ahead of the uploads). **R7-4 (P2):** a build is a durable intent, then
549	acknowledged artifacts, then a completed manifest, and `generation.json`
550	is published only from the completed state (§5.1 step 2, §7.6; INV-11,
551	`build-completion`, witness with crashes between the steps). **R7-5
552	(P3):** the Store gate awaits each maintenance event it claims, compares
553	row contents with updates and deletes, and forces a restore through
554	compacted continuation files (§14.2.1). The model's full files replace
555	the state they are applied to and carry every write they hold, which the
556	rebuilt oracle needed. 84 rules, 42 witnesses (two rules the sweep no
557	longer reaches at 3,000 seeds under writer epochs, `evidence-whole-tree`
558	and `timer-freeze`, gained witnesses; the two door witnesses are
559	retired). Results in §14.2.3 and §14.2.5.
560
561	- **Rev 7.7** answers **joint round 6** (`CODEX-FINDINGS-JOINT-R6.md`,
562	cited "R6-n") and is written against **claim spec rev 6.5** (d36adcfa),
563	whose new invariant answers R6-4: `holder.stamp` always names the
564	installation `op.exec` should run, so every CAS that changes `op.exec`
565	writes it, a new installation's new gen or an existing installation's
566	own stamp from the op journal; §22.13 has every disposition. Round 6
567	judged the claim ready for planning and found no P1. **R6-1 (P2):** the
568	model's restore oracle wrote anchors into the system it checked and
569	granted a position before the anchor PUT succeeded; the restore is now
570	a pure calculation (`restoreCalc`) that every oracle uses, and the
571	activator's initialization (`restoreInit`) opens replication only once
572	the anchor PUT is **acknowledged**, reading the position from the
573	listing, never from the restored TXID (§5.1 step 7; rule
574	`anchor-acked`, witness: the anchor PUT held across attempted opens);
575	every oracle asserts its purity (buckets, versions, queues, anchors,
576	console, random draws unchanged), and every number in §14.2 is rerun.
577	**R6-2 (P2):** `litestreamfacts` asserts exact facts and fails on any
578	alternative (the newest level-0 file retained by identity, the next
579	TXID exactly `N + 1`, every row, the original continuation gone, the
580	rooted restore's exact refusal), and gains the missing integration
581	gate: one anchored lineage through the production Store shape with
582	compaction, snapshot rotation, time-based level-0 expiry, disk loss and
583	repeated cold restores, exact positions and contents asserted
584	(§14.2.1). **R6-3 (P2):** the `restored` phase **verifies** the database
585	`building` produced instead of restoring it again, T11 prices regional
586	S3 and the disk separately and the verification pass too, and the
587	worked example is one set of numbers in the spec, the note and the test
588	(2 GiB at 10 / 250 / 500 MiB/s: 53.6 s fixed, one attempt; §7.3, §7.6).
589	**R6-4 (P3):** the return to source encoded as claim rev 6.5 states it
590	(the flip keeps the source's stamp in the journal, the return CAS
591	writes it back, a lost local record re-initializes from it, artifacts
592	are tagged when the new stamp activates, `retire-artifacts` parks by
593	tag; §6.4, §7.8; rule `return-stamp`, witness: a dirty return with a
594	lost local record). **R6-5 (P3):** the anchor's encoding inputs, the
595	header timestamp included, are persisted in the install manifest so a
596	replayed PUT repeats identical bytes (§5.1 step 2;
597	`TestFact_R6_5_AnchorReplayBytes`). Compaction in the model keeps the
598	newest level-0 file, as litestream's retention does. 79 rules, 34
599	witnesses. Results in §14.2.3 and §14.2.5.
600
601	- **Rev 7.6** answers the moves side of **joint round 5**
602	(`CODEX-FINDINGS-JOINT-R5.md`, cited "R5-n") and is written against
603	**claim spec rev 6.4** (697f0f9f), which answers the claim side of
604	R5-4 (rev 6.3: `holder.stamp`, the record's initialization, two named
605	retirements; rev 6.4: the stamp captured at work selection,
606	`retire-artifacts` never moves a stamp, the legacy location's children);
607	§22.12 has every disposition. Round 5 found that rev 7.5
608	described the pinned libraries from their documentation; rev 7.6
609	starts from **their observed behaviour**: `internal/sim/litestreamfacts/`
610	drives litestream v0.5.14 and `superfly/ltx` v0.5.1 as pinned and
611	asserts each fact this spec relies on (§14.2.6). **R5-1 (P1):** a
612	snapshot-only install restarts replication at TXID 1 (fact R5-1a) and a
613	later cold restore loses the new writes (R5-1b); the install now writes
614	a **level-0 anchor** `[N, N]` beside the snapshot, which the pinned
615	open takes as its position (R5-1c, d); `-txid` is follow-only (R5-1e).
616	**R5-2:** the pinned writers set `HeaderFlagNoChecksum`, so there is no
617	post-apply checksum to compare; verification is what the format
618	supplies, the per-file CRC-64 trailer, plus SQLite's integrity check and
619	the required TXID (§5.1 step 5); the whole-state checksum is gone from
620	the model. **R5-3:** snapshot rotation and retention are specified and
621	modelled; the restore roots at the **newest current successor
622	snapshot** of the named generation at or past the pinned one, and only
623	at the pinned version when no successor is current (R5-3d, e). **R5-4:**
624	claim rev 6.4's stamp lifecycle, encoded exactly (§6.4): `holder.stamp`
625	written by every installing CAS, the local record initialized only from
626	a fresh read under the guard, no record refuses, `retire-artifacts`
627	against `retire-installation`, and a dirty rollback's install carries
628	its own stamp. **R5-5:** the sealed snapshot is **built on the target**
629	from the staged replica; T11 prices the final delta within the bar and
630	the target's restore, snapshot and anchor at the local rate, and
631	`budget_test.go` shows a 2 GiB database over 10 MiB/s admitted that
632	way and refused as a cross-region transfer (§7.3, §7.6). **R5-6:** the
633	retention fixture populates 2 to 33 and asserts the injected
634	incarnation absent. LTX keys follow the pinned S3 client's layout,
635	`<prefix>/<level, 4 hex>/<min>-<max>.ltx`. Two new rules, each with a
636	witness (`restore-anchor`, `root-advance`). Results: 30,000 and 100,000
637	seeds clean; 77 rules, 63 caught alone, 11 in stated combinations, 2
638	liveness, 1 unreachable, none unexercised (§14.2.3, §14.2.5).
639
640	- **Rev 7.5** answers the moves side of **joint round 4**
641	(`CODEX-FINDINGS-JOINT-R4.md`, cited "R4-n") and is written against
642	**claim spec rev 6.2** (30d572c4), which answers the claim side (R4-2
643	installation stamps, R4-3 the region-qualified live set, R4-4
644	retirement under purge) and the moves session's three questions (rev
645	6.1, 79a5243c); §22.11 has every disposition. **R4-1 (P1):** the restore
646	contract is one implementable contract (§5.1): the sealed transfer is a
647	verified final snapshot, `generation.json` names it by key, version,
648	TXID and checksum, and the restore is litestream v0.5.14's planner from
649	that snapshot, overlap allowed, failing closed on a missing snapshot, a
650	gap or a checksum mismatch; §7.6 produces what the restore consumes.
651	The model's databases are key-value maps with inserts, updates and
652	deletes, its replica objects are LTX files with ranges, page images,
653	checksums and compaction, and its restore is the planner, so a
654	compacted continuation and a genuine gap each have a witness
655	(`restore-overlap`, `restore-gap-closed`). **R4-2:** installation stamps
656	as claim rev 6.2 states them, the op counter gone (§6.4); a stale writer
657	across a retire-and-reinstall is the new witness (`fence-stamp`).
658	**R4-3:** the live set is `{authoritative region, location,
659	generation}`, with a phase table naming the authoritative region
660	(§5.1), and a witness for an old regional PUT after adoption
661	(`live-set-region`). **R4-4:** retirement under the purge's own claim,
662	encoded. The random generator gains marker-hold and targeted-freeze
663	schedules, a retention fixture and two successful-move oracles, so
664	`generation-conditional`, `declare-lost-compute` and `sweep-namespace`
665	are now caught by the sweep as well. Results: 30,000 and 100,000 seeds
666	clean; 75 rules, 60 caught alone, 12 in stated combinations, 2
667	liveness, 1 unreachable, none unexercised (§14.2.5).
668
669	- **Rev 7.4** answers the moves side of **joint round 3**
670	(`CODEX-FINDINGS-JOINT-R3.md`, cited "R3-n") and is written against
671	**claim spec rev 6** (3ea3f90c), which answers the claim side (R3-2,
672	R3-3, R3-4); §22.10 has every disposition. On the spec: **R3-1**, the
673	restore contract is an algorithm now (§5.1): `generation.json` names
674	the installed snapshot by version id and TXID, and the restore replays
675	the LTX chain that continues it, skipping what it already covers and
676	refusing a conflict, never guessing; **R2-5**, a recovery install's
677	`configured` phase renders current inputs and is never gated on
678	`move.inputs` (§7.6, §7.8); **R3-7**, T11's permitted probe attempts
679	depend on the admitted budget, and a test shows rev 7.3's formula
680	refused every default move (§7.3, `budget_test.go`); claim rev 6's
681	installation-scoped retired marker, ordered orphan cleanup and
682	namespace sweep are taken into §6.4 and §19.4. On the model (§14.2):
683	restore is a chain, not a union; the local fence is per installation
684	and a deterministic UK→US→UK round trip serves on UK again; orphan
685	cleanup is a plan with pauses; the sweep discovers locations from the
686	namespace with the 32-entry cap modelled; a public request to a landing
687	target before the commit is INV-5 (**R3-5**), which gives
688	`commit-before-open` its own violation; `mutate.sh` fails on
689	orchestration errors and missing witness output (**R3-6**); every
690	witness names its failure and the gate proves it under every proper
691	subset of its mutation set. Three new rules (`fence-by-installation`,
692	`orphan-order`, `sweep-namespace`), each with a witness. Results:
693	30,000 and 100,000 seeds clean; 71 rules, 57 caught alone, 11 in
694	stated combinations, 2 liveness, 1 unreachable, none unexercised
695	(§14.2.5).
696
697	- **Rev 7.3** adds **deterministic witness scenarios** to the model
698	(§14.2.2, `witness_test.go`): one fixed, hand-scheduled scenario per
699	rule the random sweep catches rarely or only in combination, 22
700	scenarios for 20 rules. Each forces exactly the interleaving its rule
701	exists for, under a quiet RNG that injects nothing, holds with the
702	rules in place, and violates an invariant under the rule's mutation,
703	alone or in the stated combination. Witnesses never draw from a seed's
704	RNG, so adding one reshuffles nothing, and the whack-a-mole of rev 7.1
705	(`lost-return-park`) and rev 7.2 (`generation-conditional`) ends.
706	`mutate.sh` runs them beside the sweep and reports both; a rule counts
707	as caught if either catches it. Nine rules are caught alone by their
708	witness, `generation-conditional` and `declare-lost-compute` among
709	them, which the sweep misses at 100,000; eleven hold alone and violate
710	in their combination, which is the redundancy the combination table
711	states, shown rather than inferred (§14.2.5). Found on the way: the
712	purge drain iterated registrations in Go map order, the model's one
713	source of nondeterminism; it drains in create-id order now and two
714	runs agree exactly. Results: 30,000 and 100,000 seeds clean; 68 rules,
715	53 caught alone, 12 in stated combinations, 2 liveness, 1 unreachable,
716	**none unexercised**.
717
718	- **Rev 7.2** is written against **claim spec rev 5.2** (465fee96), which
719	adopted CC22: the creator's claim CAS is `If-Match` the ETag read at
720	registration (`If-None-Match: *` when the claim was absent), a 412
721	restarts the create from step 0 with a new registration, the purge
722	fence is released by writing a free claim, and a new **C5a** says a
723	claim object is never deleted. The model encodes that text: the 412
724	restarts the create instead of abandoning it, and a new rule,
725	`claim-never-deleted`, lets the mutation delete a fence that found no
726	claim; dropped, a paused creator's `If-None-Match: *` passes again
727	(§14.2.2, §14.2.5). Rev 7.2 also closes the gap rev 7.1 left: a
728	**biased schedule** in half the seeds makes the target's app write in
729	the settle window, fails the settle check, and stops the target the
730	moment its first return PUT is out, so declare-lost meets a partial
731	return lane. `lost-return-park` (model 27) is caught alone (3 / 3,000,
732	32 / 30,000), where rev 7.1 reached it in no seed of 300,000. Results:
733	30,000 and 100,000 seeds clean; 68 rules (§14.2.5). The reshuffle this
734	schedule causes moves two rare rules back: `declare-lost-compute` is
735	combination-only again (0 / 100,000 alone, 3 / 100,000 with
736	`watchdog-independent`), and `generation-conditional` (model 29) is
737	unexercised (0 / 300,000; 2 / 100,000 on rev 7.1), listed as such in
738	`expected-outcomes.txt` as rev 7.1 listed `lost-return-park` (§14.2.5).
739
740	- **Rev 7.1** is written against **claim spec rev 5.1** (64eec93b), which
741	adopted CC20 (the sweep lists `moves/<host>/`) and answered CC21 with a
742	**purge fence** on the host claim instead of the creator-side check
743	rev 7 proposed: S3 cannot condition one object's write on another's
744	version. The model encodes the fence, a biased schedule that pauses a
745	creator between its registration re-read and its claim CAS, and finds
746	one more condition the fence needs: the creator's claim CAS must be
747	conditional on the claim ETag it read **when it registered** (CC22),
748	or a fence placed and released while it slept lets it through
749	(§14.2.5, §19.4). It also fixes a moves-side fault the 100,000-seed run
750	surfaced: `generation.json` is a reused key, and an earlier push's PUT
751	completing late put an older generation back and left recovery stuck;
752	the marker is now written If-Match the one it supersedes (model 29,
753	§5.1). Results: 30,000 and 100,000 seeds clean; 67 rules, 51 caught
754	alone (the fence and the ETag condition among them), 12 in stated
755	combinations, the re-read alone shown insufficient (287 / 30,000), and
756	`declare-lost-compute` now caught alone (§14.2.5). The mutation harness
757	runs one prebuilt test binary under `$TMPDIR`, with no copies of the
758	source (§14.2.1).
759
760	- **Rev 7** was written against **claim spec rev 5** (4a458a9c on
761	`design-replica-ownership`), which adopted CC15 to CC19. It:
762	- closes the model's last gap: a **biased schedule** beside the uniform
763	one recreates a host where it last served while the previous
764	incarnation's requests are still in flight, and races door listings
765	against the delete and the recreate. `location-per-incarnation`
766	(claim C3a) is now caught alone, and both door rules with it
767	(§14.2.5);
768	- re-encodes claim rev 5: the at-rest sweep under an obligation the
769	sweeping box owns, registration leases, orphan records at any time,
770	`holder.generation`, signatures taken at the deadline check with an
771	SDK retry that must not re-sign;
772	- asks for two more claim changes, CC20 and CC21 (§19.4).
773
774	Earlier revisions:
775
776	- **Rev 6** (7ac666fe) answers joint Astra round 2 (`CODEX-FINDINGS-JOINT-R2.md`,
777	df41156c; cited "J2-…"), whose three verdicts were "not ready", and is
778	written against **claim spec rev 4** (a3c86fa5 on
779	`design-replica-ownership`), which answers the claim-side findings. Rev 6:
780	- **rebuilds the model to encode exactly what the specs say**
781	(§14.2): restore and the start check no stronger than §5.1;
782	record-first transitions split from their claim halves, with crash
783	points between; independent processes for the host guard; a door
784	listing with O1 and O2; creates and purges as concurrent console
785	plans over two hostnames; requests that complete after `H`; a final
786	oracle that only reads; and a mutation harness that counts only a
787	parsed invariant violation as a detection (J2-R2-9, J2-R2-10);
788	- specifies this spec's share of J2-R2-1: **operation-scoped
789	generations** within the claim's `holder.location`, a restore
790	contract that reads only the generation the claim names, and a
791	**straggler sweep** for what lands after `H` (§5.1, §6.4);
792	- fixes J2-R2-5: a recovery probe runs on the inputs it renders now,
793	not the move's pinned ones (§7.6, §7.7);
794	- fixes J2-R2-8: the start check also requires the generation the claim
795	expects, so the third admission fence the model relied on is now
796	specified (§5.1);
797	- makes the record and the claim consistent: every move transition is
798	one record CAS, and the claim follows it; any actor may write the
799	claim half, which the record fully determines (§7.5, §19 K4);
800	- makes the cut promise the enforced deadline (§7.4, T11);
801	- records that `CARLOS_SECRETS_KEY` is on every flagship box and config
802	sync is armed in every region (§1.2, §15);
803	- lists CC15 to CC19 for platform-1e (§19.4).
804
805	Rev 6's changes are marked "(J2-…)" for the review's findings and
806	"(model N)" for the stricter model's.
807
808	- **Rev 5** (4ec3282b) was written against **claim spec rev 3** (8b5bccb2 on
809	`design-replica-ownership`), which adopted CC1 to CC13. It answers the
810	coordinator's round on rev 4:
811	- the model (§14.2) is extended until it exercises every rule rev 4
812	listed as a gap: stalled staging signers, paused registry writes that
813	resume at the worst moment, an obligation runner beside the role
814	worker, and admission from cached reads. It is re-encoded against
815	claim rev 3, and reruns clean at 30,000 and 100,000 seeds, with the
816	full mutation sweep (§14.2.5);
817	- N2's second half is now proven: dropping the seal by version loses
818	acknowledged writes, and dropping the staging horizon leaves residue.
819	The model also found the rule both rest on: a staging writer signs
820	only before its lease's `SafeUntil` (model 14, §7.3);
821	- CC11 is now proven: an operation started over a pending park loses
822	acknowledged writes (model 15);
823	- T12 and the install wait on `quiet_after` cannot bite under claim
824	rev 3: they are kept as defence in depth (§14.2.5);
825	- §15 step 8 is done: every AWS behaviour the model assumes was checked
826	against the real service;
827	- one more claim change, CC14, goes to platform-1e (§19.4).
828
829	Rev 5's changes are marked "(model N)" like rev 4's.
830
831	Earlier revisions:
832
833	- **Rev 4** (a80ff90b) was the first revision checked against an **executable model**
834	instead of a prose round. The joint Astra review of the claim spec (rev 1)
835	and this spec (rev 3), `CODEX-FINDINGS-JOINT-R1.md` (4316db73), found 12
836	new P1s and 3 P2s, and recommended a joint simulation before planning.
837	Rev 4:
838	- builds the model: `internal/sim/hostlife/`, a test-only Go package
839	(§14.2). It encodes claim spec rev 2 (cf3a7861) and this spec, with the
840	real IAM split, late S3 completion, crashes, partitions, whole-VM
841	pauses, destroyed and restarted boxes, and old executables. It runs
842	30,000 seeds clean, and a mutation harness drops each rule in turn;
843	- adopts the joint review's adjudicated text for D1, D3 to D8 and I-7,
844	and answers the findings this spec owns: N2, N11, N13, N14, N15, and the
845	moves side of the others. Changes are marked "(joint N)";
846	- fixes what the model found beyond the review, marked "(model N)"
847	(§14.2.4);
848	- lists the claim changes the model requires (§19.4), for platform-1e.
849
850	- **Rev 1** (e41c4fef) went to Astra (GPT-6, via codex): 12 P1, 7 P2, 1 P3,
851	"not ready". The findings are in `CODEX-FINDINGS-MOVES-R1.md` (9fbf4afe).
852	- **Rev 2** (45b77691) answered them, cut the scope to Phase 1, took Paul's
853	rulings M4 to M15, and rebuilt on #199 rev 3. Round 2,
854	`CODEX-FINDINGS-MOVES-R2.md` (e5b67514), resolved or accepted the
855	deferral of most of round 1. It found 6 new P1s and 4 P2s: "not ready".
856	- **Rev 3** answers round 2. Changes are marked "(codex R2-N)"; rev 2's
857	marks "(codex N)" stay. §22 records every disposition from both rounds.
858	Rev 3 also:
859	- takes Paul's rulings M16 to M18 (§0.1);
860	- builds on **the host lifecycle claim** that Paul ruled on 2026-10-02:
861	one object per host, updated by CAS, that serializes delete, park,
862	move, push, the db door and wake. It is specified in
863	`docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`
864	(rev 1 at 653ad4b1 on `design-replica-ownership`; "the claim spec").
865	§19 says how moves use it and where this spec asks it to change.
866
867	**Status:** DRAFT for review. Nothing here is built.
868	**Discussion:** amadan `carlos/platform` #175.
869	**Goal (Paul, 2026-10-02):** "I want region-default AND the ability to
870	easily move any app or instance to a different region." The region default
871	is `docs/superpowers/specs/2026-10-01-nearest-region-default-design.md` on
872	branch `design-nearest-region`.
873	**Builds on:**
874
875	- #331, `docs/superpowers/specs/2026-08-28-instance-move-design.md`.
876	- The moves design record (the "09-24 record"),
877	`docs/superpowers/specs/2026-09-24-instance-moves-for-every-app-design.md`
878	on branch `docs-instance-moves-design`, with `CODEX-RULINGS-INSTANCE-MOVES.md`.
879	- On `main` (7edd4b33): P0 (the cut fence), P7 (the edge door), and the
880	move-ready fix (16 MiB readiness bar, copy receipts for multipart ETags).
881	- #199 rev 3, `docs/superpowers/specs/2026-10-02-replica-ownership-design.md`
882	at 66f1dad3 on `design-replica-ownership` (the "#199 spec"). It failed
883	review for the same reason as round 2's P1s; the claim spec supersedes it
884	from its §2 onward (tombstones become the claim's `deleting` and
885	`parking` operations).
886	- The claim spec, `docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`,
887	**rev 6.2 at 30d572c4** on `design-replica-ownership`. Rev 7.5 is
888	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
889	against rev 5 (4a458a9c); rev 6 against rev 4 (a3c86fa5); rev 5 against rev 3
890	(8b5bccb2); rev 4 against rev 2 (cf3a7861).
891
892	Citations are to this worktree at 7edd4b33 unless they name another branch
893	or repo.
894
895	## 0. Rulings and the shared primitive
896
897	### 0.1 Paul's rulings (2026-10-02). Not reopened here.
898
899	| id | ruling | where Phase 1 spends it |
900	|---|---|---|
901	| 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) |
902	| 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 |
903	| M3 | **Stores move with the app.** | F4; Phase 1 leaves the app store in place and refuses private stores (§7.1) |
904	| M4 | The files the move carries are a fixed set. | §6.1 |
905	| M5 | The files archive is capped at 256 MiB, enforced while streaming and again at the cut. | §8.1 |
906	| M6 | Person-started moves cut automatically once ready and validated; the API default stays manual; `--manual-cut` exists. | §12 |
907	| M7 | The source copy is held for 7 days after a move; owners may end the hold early. | F3 |
908	| M8 | An app move pauses when one of its instances rolls back, and keeps the target app region. | F5 |
909	| M9 | An app store's final copy holds every consumer at 503, behind a durable barrier covering concurrent creates. | F4, F5 |
910	| M10 | An app with sidecars is refused an app move until sidecar moves exist. | F5 |
911	| M11 | Target pre-warming is deferred; eligibility is gated on the measured duration of the whole cut. | §7.3 (T11) |
912	| M12 | Rehearsal order: a probe app, then a disposable ips instance, then kpmg, each with scoped approval. | §14.4 |
913	| M13 | Owners only, not members; the member-minted instance-token bypass is closed. | §12; F1 |
914	| M14 | One landing path in production. | §7.6 |
915	| M15 | A landed copy is installed into the target's `instances/`, never served from `moves/`. | §5.1, §7.6 |
916	| **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 |
917	| **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 |
918	| **M18** | **Tito waits.** Move mutations are operator-only; instance-role tokens keep only the status read. | §12 |
919
920	### 0.2 The 09-24 record's rulings
921
922	They bind unless M1 to M18 override them. **R4** ("rollback is a move
923	back") is narrowed by M2: a landing that fails before the target admits
924	traffic is undone automatically (§7.8); after the target opens, R4 stands.
925	**Q5** (other accounts operator-only until #171) is consistent with Phase 1.
926
927	### 0.3 What #199 contributes
928
929	- Replica data stays at `instances/<host>`
930	(`internal/activator/activator.go:138`). No record field carries storage
931	identity, so this spec names a generation by the operation id that
932	installed it, in object names and marker files (§5.1).
933	- The incarnation, `provision.Incarnation(rec)`, including the
934	zero-CreatedAt legacy identity, and the park helpers (copy with a manifest
935	then delete; local rename), now specified in the claim spec §2 and §5.
936
937	### 0.4 The host lifecycle claim
938
939	From claim spec rev 5.1 (§2 to §10 there), the parts this spec relies on:
940
941	- **The object** `control/hosts/<host>.json`, rewritten whole by CAS: a
942	per-write revision `gen` (not a data generation, J-D2); a `holder`;
943	`op` with `kind`, `id`, `phase`, `intent` (written in the start CAS),
944	`journal`, `exec` and `participants`; `touched` (with `complete`);
945	`inventory`; `obligations[]`; the `lost` quarantine; and
946	`retired_incarnations`.
947	- **Its invariants:** C1 one holder; C2 intent before effect, a recovery
948	owner for every state, every CAS conditional on `op.id` as well as the
949	ETag; C3 storage mutated only by the current operation and only on
950	**exact object versions**, with a shared staging-work lease for
951	cross-region staging; C4 fresh admission; C5 revocation needs stop
952	evidence or a lost-box fence; C6 a read error never acts; C7
953	already-admitted work is drained (`hostguard`). Rev 3 limits C3's
954	"late completion is harmless" to the operation's own version-bound
955	calls, and covers the replication exception with a late-completion
956	horizon (§6.2a there). Rev 4 adds **C3a: no storage location is shared
957	between incarnations.** `holder.location` is
958	`instances/<host>/<incarnation>/` for a new incarnation and
959	`instances/<host>/` for an adopted legacy host, set with the holder and
960	immutable while it holds; restore reads only that location, plus this
961	spec's generation within it, from the same fresh admission read.
962	- **Op kinds** (§4 there): `moving`, `landing` and `reverting`/`restoring`
963	belong to this spec. One operation runs at a time.
964	- **Mechanisms:** stop evidence from system state, with every probe
965	rendering held config (§6.1); parking by exact version into
966	per-retirement destinations keyed `<relative key>@<source versionId>`
967	(§6.2); the late-completion horizon `H` and the per-region `quiet_after`
968	that survives `free` (§6.2a); local retirement for both layouts (§6.3);
969	the host guard, an exclusive `flock` shared by every OS process that
970	writes host state, with a fresh claim read under it (§6.4); door
971	listings that read the claim twice, O1 and O2 (§6.5); execution
972	leases for liveness, and declare-lost by compute fencing only (§7); one
973	`claim.Adopt` routine whose discovery parks every other region and every
974	other box (§9); app admission registration, closed and drained by purge,
975	which fences a drained registration's host claim before removing it
976	(§5.1, §5.3, CC21); `cancelled_creates` (§5.1); the purge journal
977	`reserved → adopted → claimed → torn-down → retired → done` (§5.3); park
978	manifests with separate archive and deletion sets (§6.2); the floor on
979	every executable restore path (§10).
980
981	This spec's rules for using the claim are K1 to K13 in §19, named "K" so
982	they never read as the claim spec's C1 to C7. **Execution holder** below
983	means the claim's `op.exec` (rev 2 made it a first-class field, as rev 3
984	asked).
985
986	Rev 4's model required CC1 to CC13 of claim rev 2, and claim rev 3
987	adopted them; rev 5's CC14 is in claim rev 3.1 and rev 4; rev 6's CC15 to
988	CC19 are in claim rev 5, rev 7's CC20 and CC21 in claim rev 5.1 (CC21
989	as a purge fence), and rev 7.1's CC22 in claim rev 5.2, with C5a (§19.4).
990	Claim rev 6 (3ea3f90c) answers the claim side of joint round 3 (R3-2,
991	R3-3, R3-4) with no request from this spec; rev 7.4 encodes it. Claim rev
992	6.2 (30d572c4) answers joint round 4's claim side (R4-2 installation
993	stamps, R4-3 the region-qualified live set, R4-4 retirement under purge)
994	and the moves session's three questions; rev 7.5 encodes it (§5.1, §6.4,
995	§14.2.2, §19.4).
996	Until platform-1e adopts them, this spec states each as the behaviour it
997	relies on.
998
999	### 0.5 Paul's rulings of 2026-10-06 (#236; claim rev 6.27 §1.1) and region HA's requests
1000
1001	Claim rev 6.27 (989ee349) §1.1 records every ruling of amadan #236. The
1002	ones this spec acts on:
1003
1004	- **P1, the floor is the first fully integrated release.** §11's
1005	`control/moves-protocol.json` names a real release that carries the
1006	claim, the moves and the region HA code together; no placeholder tag.
1007	- **P5, record-backed placement only.** A move's target is a record's
1008	region and a box the roster knows; nothing places by hand.
1009	- **P6, rename and transfer stay refused.** Out of scope here as before.
1010	- **P7, cold-only admissions.** Until a reviewed Litestream fix (#234)
1011	makes a clean-close certificate safe, **every admission is cold**: no
1012	`closed/<session>.json` is written, no `PredecessorCertified` admission
1013	is made, and no plan task depends on warm. §5.1 step 9's warm mode,
1014	the certificate ledger and `KeepStamp`'s interaction with warm stay in
1015	this spec as the behaviour a later revision turns on; the model keeps
1016	both modes so the rule stays checked. The cost in Phase 1: every wake
1017	restores from the remote (one regional S3 read and one disk write of
1018	the database), writes a fresh generation's first upload (one disk read
1019	and one regional S3 write) and its `generation.json`, and
1020	`PublishGeneration` queues one `park-generation` chore for the dead
1021	predecessor per wake. T11 already prices every probe attempt as a
1022	cold admission (rev 7.11, R10-8), so the readiness budget is
1023	unchanged by P7; the per-wake chore is a claim CAS and a regional
1024	park after the horizon, outside the cut window.
1025
1026	Region HA (spec 1 rev 5.4, §9) asks four things of this spec, folded in
1027	as follows; the fifth, L18, is stated as a limit:
1028
1029	- **L14** (§7.10): the termination fence is M16's evidence, automatically.
1030	- **L15** (§7.1, §7.3, §19.1): the target box is chosen in the start CAS.
1031	- **L16** (§5.1 step 2, §7.6): one install routine, two sources.
1032	- **L17** (§6.1, §8.3, §9.4): a files manifest per installation.
1033	- **L18** (§14.2.6): two boxes per region in the model is not done here.
1034
1035	## 1. What happened in production
1036
1037	### 1.1 Finding 1: busy instances never reached `ready` (fixed on main)
1038
1039	Multipart ETags never matched after `CopyObject`. Fixed in 2cbf6196 and
1040	167d721b (merged as 7edd4b33): copy receipts
1041	(`internal/activator/backend_exec.go:1557`) and a 16 MiB readiness bar
1042	(`internal/host/movespass.go:215-235`, applied at `:387`).
1043
1044	### 1.2 Finding 2: a completed move could not start for 1h54m
1045
1046	`kpmg.bdn.oncarlos.com` (account bdn, app ips) moved IE (home) to uk, and
1047	every wake on the UK box then failed with `instance not healthy within 30s`
1048	(`backend_exec.go:1443`). Both causes are confirmed.
1049
1050	**(a) The per-host data directory does not move.** The cut mirrors the
1051	replica (`movespass.go:476-490`), purges database files only
1052	(`backend_exec.go:1566-1575`), and flips the record (`movespass.go:494`).
1053	The app keeps `instance.key` and `report.token` in `/data/<host>/`, which no
1054	platform code names. On the UK box the app minted a new key.
1055
1056	**(b) Only the Ireland box holds `CARLOS_SECRETS_KEY` (codex 20).** The UK,
1057	US and AU journals log "config sync loop disabled: CARLOS_SECRETS_KEY not
1058	set" (`internal/host/agent.go:884`). Both config loops return at once
1059	(`agent.go:881-886`, `:1279`), the fast converge skips its config leg
1060	(`agent.go:1812`), and the spawn treats a missing config file as empty
1061	(`backend_exec.go:1146-1149`). Paul approved distributing the key to every
1062	region box. **Done (2026-10-03): the key is on all four flagship boxes,
1063	and config sync is armed in every region.** The fingerprint every box
1064	publishes (§10) still verifies it per box, and T2 still refuses any
1065	target without it: a new or rebuilt box can lack it again. With config
1066	sync live everywhere, bundle updates now reach a box during a move, which
1067	is why J2-R2-5's case is real (§7.6).
1068
1069	### 1.3 Finding 3: the rehearsal proved nothing
1070
1071	`bdf/hello` has no key file, store, config or timers. §14.4 rehearses with
1072	an app shaped like ips.
1073
1074	### 1.4 Finding 4: SSM Parameter Store is regional
1075
1076	carloku-infrastructure `region-uk.tf:61-64`: nothing replicates `/carlos/*`
1077	between regions. §10 shows that an instance needs only the box's secrets
1078	key from it.
1079
1080	## 2. Phase 1: what it does and what it refuses
1081
1082	Phase 1 moves **one** exec-backed, hibernating `kind:"instance"` record
1083	between two non-fleet placements, into home only with host claims on
1084	(Ruling R1, rev 7.24), driven by an operator. It carries every piece of per-host state, proves the target can
1085	run it before the source stops, starts it on the target with no public
1086	traffic, and opens only after a commit. If the target cannot start it, the
1087	instance returns to the source automatically, carrying anything the target
1088	wrote. Phase 1 refuses everything §7.1 lists. It deletes nothing: what a
1089	move supersedes is parked under the operation's id, out of every live
1090	namespace, ready for F3's cleanup.
1091
1092	## 3. Words
1093
1094	- **Source / target:** the box serving before the move, and after. "Box"
1095	means the one box whose registry owns the route (`OwnsRoute`,
1096	`movespass.go:180-185`).
1097	- **Move id / rollback id:** console-minted, unique, `mv_` or `rb_` plus 26
1098	lowercase base32 characters. Each names one **operation**.
1099	- **Generation:** one installed copy of an instance's state (database,
1100	files, timers), identified by `(op id, incarnation)`. An instance that has
1101	never moved is in the **origin** generation (no markers anywhere).
1102	- **Handoff:** the transfer of the execution right from one box to another,
1103	with a new generation (§5). A move is a handoff; a dirty rollback is a
1104	handoff back; a future `carlos db push` is a handoff on one box.
1105	- **Hold:** a registry row status that admits no traffic, ticks or ordinary
1106	wakes (§5.2).
1107	- **Flip / commit / open:** the CAS that sets `region` to the target; the
1108	CAS after which the target is authoritative; the target row becoming
1109	`ready`.
1110
1111	## 4. Invariants
1112
1113	Stated first, designed to, and proved by the simulation in §14.2.
1114
1115	- **INV-1 One writer.** At any instant at most one process tree, on any box
1116	in any region, runs the instance with write access to its database, files
1117	or store. A box starts the instance only while the claim names it as the
1118	execution holder, and the right moves only on **stop evidence** proving
1119	the previous holder's whole process tree is gone (§5.3). A timeout never
1120	moves it (codex 1, R2-1).
1121	- **INV-2 No lost acknowledged write.** No write the instance acknowledged,
1122	to a client, a tick, its own background work or an external system, is
1123	lost by any outcome. A rollback carries back whatever the target wrote,
1124	and a source recovery never reinstalls over its own new writes (codex 2,
1125	R2-3). M16's `--declare-lost` is the one disclosed exception.
1126	- **INV-3 Convergence without a human.** A crash of any actor (a console or
1127	agent process restart, or a box reboot) at any step leaves a state from
1128	which the move reaches a terminal outcome with no human action. This
1129	holds even when the crashed activator has lost all memory (codex R2-2).
1130	The exception is a box that never returns, handled by M16 (§7.10).
1131	- **INV-4 Files match the database.** Every start, on any box, uses a files
1132	directory whose generation equals its database's generation, and the
1133	generation installed in the box's own bucket. Otherwise the start is
1134	refused (§5.1).
1135
1136	Supporting invariants:
1137
1138	- **INV-5 No admission before commit.** A row leaves a hold only by a
1139	conditional write naming the operation that holds it (codex 3, 6).
1140	- **INV-6 The environment that runs is the environment that was checked,**
1141	from inputs whose versions were pinned at readiness (codex 14, R2-8).
1142	- **INV-7 Install is never replayed over writes,** on the target or the
1143	source; and a completion marker is published only after everything it
1144	vouches for is durable (codex 5, R2-3, R2-6).
1145	- **INV-8 Phase 1 deletes nothing a recovery might need** (codex 8).
1146	- **INV-9 Bounded.** Every non-terminal state has a deadline after which it
1147	advances, recovers, or pages in a state that still satisfies INV-1 and
1148	INV-2. Recovery deadlines are separate from the promised cut window
1149	(codex R2-10).
1150	- **INV-10 Incarnation isolation.** When a move or rollback ends, no copy
1151	of the instance's data remains in a live host namespace
1152	(`instances/<host>/`, `moves/<host>/`, the flat DB path, the files
1153	directory) on any box or bucket except the one the claim names as
1154	current. Everything else is parked under the operation id (codex R2-5).
1155
1156	**What the model checks (§14.2).** The coordinator's list for the joint
1157	model, and where each lives:
1158
1159	| invariant | checked | here |
1160	|---|---|---|
1161	| at most one writer per host, across regions | after every step | INV-1 |
1162	| 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 |
1163	| no recreated host sees a previous incarnation's database, key or config | at every spawn | INV-4, C1 |
1164	| no live-namespace residue after an operation ends | at the end, every bucket and box | INV-10 |
1165	| claim and record agree after recovery | at the end | C2 |
1166	| every crash converges with no human, except declared loss (M16) | at the end: the run must reach a quiescent state | INV-3 |
1167	| an app store exists while its host is held for anything but delete | after every step | claim §5.3 |
1168	| a door read returns only the incarnation it authorized | at every open | claim §6.5 |
1169	| a commit happens within the cut budget | at the commit | INV-9 |
1170	| an admitted cut never waits out `quiet_after` (rev 5) | at the landing's park | INV-9, T12 |
1171	| no IAM violation | at every request | M17 |
1172	| no stuck recovery | after every step | INV-3 |
1173
1174	## 5. The handoff protocol
1175
1176	### 5.1 Generations, markers and the restore contract (codex R2-6, R2-9, J2-R2-1, J2-R2-8)
1177
1178	**Location and generation.** Claim C3a gives each incarnation its own
1179	replica location, `holder.location`: `instances/<host>/<incarnation>/`,
1180	or `instances/<host>/` for an adopted legacy host. Within it, every
1181	installed state of the database is a **generation**, named by the
1182	operation that installed it: the origin generation (`""`, written by the
1183	host's own replication from its first wake), then one per committed move,
1184	per push, and per dirty rollback. Each generation has its own key prefix:
1185
1186	| generation | replica objects |
1187	|---|---|
1188	| origin | `<location>` itself, the layout litestream writes today (`<location>ltx…`, a legacy host's existing objects) |
1189	| an operation `op` | `<location>g-<op id>/…`: the installed snapshot, its anchor and every LTX object replicated on top of them |
1190
1191	Within a generation prefix the objects are litestream's, in the layout
1192	the pinned S3 client writes (`s3/replica_client.go`, `ltx.FormatFilename`):
1193	`<prefix>/<level as four hex digits>/<MinTXID as sixteen hex digits>-<MaxTXID
1194	as sixteen hex digits>.ltx`, so a snapshot ending at TXID 7 is
1195	`0009/0000000000000001-0000000000000007.ltx` and a level-0 file for TXID 8
1196	is `0000/0000000000000008-0000000000000008.ltx`. Rev 7.5 wrote
1197	`ltx/<level>/`, which is not the layout (R5-6). Rev 7.6 writes the real
1198	one in this spec and in the model.
1199
1200	The claim names the current one, **`holder.generation`** (CC18): written
1201	only by a cold admission's `AdmitWriter` CAS (a landing's, a push's or a
1202	dirty rollback's probe into its prepared generation, every recovery into
1203	a fresh one, §7.14) and by a clean rollback's return CAS, which names the
1204	source's generation again for the restore (§7.8; R10-3: no commit,
1205	`probed` or install phase writes it). Restore reads it from the same fresh
1206	admission read as `holder.location` (claim C3a).
1207
1208	**The restore contract (J2-R2-1; R3-1; R4-1).** A restore reads
1209	`holder.location`, generation `holder.generation`, in the box's own
1210	bucket, and nothing else. It never picks "the newest object under the
1211	prefix". Rev 7.4's algorithm required each next LTX object to start at
1212	`current TXID + 1`, which is not how LTX works (R4-1): compaction merges
1213	files into one covering `[Min of first, Max of last]` whose page images
1214	are the state at `Max`, deletes the inputs, and so leaves overlapping
1215	ranges and no individual intermediate objects. A snapshot ending at 100
1216	with one current continuation `[91, 110]` is a healthy replica; rev 7.4
1217	would have refused it, or restored through 100 and let a move commit
1218	without transactions 101 to 110. Rev 7.5 took **one implementable
1219	contract: the sealed transfer is a verified final snapshot, and the
1220	restore is litestream's own planner over that snapshot and the
1221	generation's later files**. Joint round 5 showed that rev 7.5 described
1222	`litestream` v0.5.14 and `superfly/ltx` v0.5.1, the versions this
1223	repository pins, from their documentation and got three things wrong
1224	(R5-1, R5-2, R5-3). Rev 7.6 writes the contract against the libraries'
1225	**observed** behaviour: `internal/sim/litestreamfacts/facts_test.go`
1226	drives the pinned libraries with the file replica client and asserts
1227	every fact cited below as "fact R5-n"; a library upgrade that changes one
1228	fails there first (§14.2.6).
1229
1230	1. **The sealed transfer is the staged replica at the required final
1231	TXID (R5-5).** At the cut, after the final checkpoint and
1232	`SyncAndWait`, the source's replication position is `N`: the
1233	`MaxTXID` of its newest level-0 file. The final mirror round
1234	(`staged`, §7.4) copies the delta of the source's replica into
1235	staging's `replica/`, within the 16 MiB bar, and the **seal** records
1236	`N` and the exact `versionId` of every current LTX file under
1237	`replica/`. Nothing larger crosses the region boundary at the cut: rev
1238	7.5 shipped a whole snapshot of the stopped database after the stop,
1239	which a 2 GiB database over a 10 MiB/s path cannot do in a 120 s
1240	window, while T11 priced only the 16 MiB delta (R5-5). `N` is the
1241	**required final TXID** of the transfer.
1242	2. **The target builds the generation's snapshot from the staged
1243	replica** (§7.6 `building`). It restores the sealed versions with the
1244	planner of step 4, in its own region, verifying each file's trailer
1245	(`ltx.Decoder.Verify`: the CRC-64 `FileChecksum`), and requires the
1246	result to reach exactly `N` and to pass `PRAGMA integrity_check`.
1247	From that database it writes two files into the move's own
1248	generation: the **snapshot**, one level-9 LTX file `[1, N]`, every
1249	page, at `<location>g-<move id>/0009/<1>-<N>.ltx`; and the **anchor**
1250	(step 7), one level-0 LTX file `[N, N]`, every page, at
1251	`<location>g-<move id>/0000/<N>-<N>.ltx`. Both are written as the
1252	pinned writers write theirs: `HeaderFlagNoChecksum` set, pre- and
1253	post-apply checksums zero, the trailer's CRC-64 present (fact R5-2);
1254	the anchor's `WALOffset` is the WAL header size, which `Verify`
1255	requires (fact R5-1c). **A build is two durable states, never one
1256	object** (R7-4): first the **build intent**,
1257	`<location>g-<move id>/build-intent.json`, written before any PUT, with
1258	the encoding inputs the builder will use (the header timestamp, the
1259	page size, the commit, `N`) so that a replay (a restarted `building`)
1260	encodes **identical bytes** (R6-5: the bytes depend on the timestamp,
1261	`TestFact_R6_5_AnchorReplayBytes`); then, only once the snapshot PUT
1262	and the anchor PUT have both returned, the **completed install
1263	manifest**, `<location>g-<move id>/install.json`, with the artifacts'
1264	acknowledged identities (keys, the `versionId` each PUT returned, `N`,
1265	each file's CRC-64) and the verification results (`integrity_check`
1266	passed, the sha256 of the database file the build produced). Its
1267	keys are the shared `moves.InstallManifest`'s json tags (claim Plan 6's
1268	`internal/moves/install_contract.go`; rev 7.22): `v`, `op`, `host`,
1269	`snapshot_txid` (the Go field `N`), `snapshot_key`,
1270	`snapshot_version`, `snapshot_crc64`, `anchor_key`, `anchor_version`,
1271	`anchor_crc64`, `integrity_check`, `db_sha256`, `built_at`. The
1272	completion predicate is the manifest's existence, never the intent's:
1273	rev 7.7 said "the install manifest records the inputs before the PUTs"
1274	and "`building` is done when the install manifest exists", so a crash
1275	after the inputs and before the artifacts left a manifest that
1276	satisfied the completion predicate (R7-4). A replay reads the intent,
1277	encodes the same bytes, and reuses a snapshot or anchor it finds
1278	already current under its key rather than writing again (the model's
1279	cold admission does the same, §7.14). `generation.json` is published
1280	only from the completed state (step 3). The cost is three passes over
1281	the database, each across regional S3 and the disk, plus a
1282	verification read, which T11 prices (§7.3).
1283	3. **`generation.json` names the snapshot**: `snapshot_key`,
1284	`snapshot_version`, `snapshot_txid = N`, `snapshot_crc64`. These are
1285	the snapshot identity: the **pinned root**. A second version under the
1286	same key, from a PUT that completed late, is identical bytes and is
1287	never read.
1288	4. **The restore is litestream's planner** (`replica.go`
1289	`CalcRestorePlan`, v0.5.14), rooted in the named generation and
1290	nowhere else. Its **root** is the newest current level-9 file of the
1291	generation whose `MaxTXID ≥ snapshot_txid` (a **verified successor
1292	snapshot**, step 8), or, when no such file is current, the pinned
1293	snapshot opened by `snapshot_version`. From `current = root.MaxTXID` it
1294	takes, among the generation's current files at levels 0 to 8, the
1295	file with `MinTXID ≤ current + 1` and `MaxTXID > current` (overlap
1296	allowed: `ltx.IsContiguous`), preferring the highest `MaxTXID`, then
1297	the lowest `MinTXID`, then the higher level, applies it, sets `current
1298	= MaxTXID`, and repeats until nothing extends the range. A compacted
1299	`[91, 110]` over a snapshot at 100 is taken: its pages are the state
1300	at 110, so applying them over the state at 100 is exact. Files are
1301	taken from the current listing, as litestream lists them; nothing
1302	reads noncurrent LTX versions, because compaction's and retention's
1303	deletes make the superseded files noncurrent on purpose. Rev 7.5 said
1304	"every level" and rooted at the pinned snapshot for good; after
1305	retention that root has no continuation (fact R5-3d) and the restore
1306	would have refused a healthy replica (R5-3).
1307	5. **Fail closed, by what the format supplies (R5-2).** The pinned level-0
1308	writer, snapshot writer and compactor all set `HeaderFlagNoChecksum`;
1309	`PreApplyChecksum` and `PostApplyChecksum` are zero in every file, and
1310	`ltx.Trailer.Validate` requires them to be with that flag (fact R5-2,
1311	litestream `db.go:1948`, `db.go:2412`, ltx `compactor.go`). There is no
1312	database checksum to compare after applying a file; rev 7.5's step 5
1313	would have refused every healthy continuation, or been skipped. What
1314	the format supplies is **per-file integrity**: the trailer's CRC-64
1315	over the file, which `Decoder.Verify` checks, and which SQLite's own
1316	`PRAGMA integrity_check` (`CheckDB`, `backend_exec.go:313`) complements
1317	over the result. The restore refuses, with a member-safe reason and a
1318	page, and never produces a database, when: no root is current and the
1319	pinned version is missing or its `MaxTXID` is not `snapshot_txid`; a
1320	file fails `Verify`; a current file starts beyond `current + 1` once
1321	nothing extends the range (litestream's "non-contiguous ltx files": a
1322	gap); the result fails `integrity_check`; or, at an install, the
1323	result is not at the required final TXID. End-state checksums would
1324	need the three writers changed; Phase 1 does not change them, and the
1325	model carries none (§14.2.2).
1326	6. **What a gap means.** Litestream does not advance past a failed
1327	upload, and a timed-out upload is retried with the same bytes before
1328	the next range, so a gap in a generation's current listing is a lost
1329	or not-yet-landed object, never a healthy replica. The refusal holds
1330	until the object lands, or pages an operator.
1331	7. **The anchor: restore-to-replication initialization (R5-1).**
1332	Litestream's open (`db.go` `checkDatabaseBehindReplica`) takes a fresh
1333	box's replication position from the **newest remote level-0 file**; a
1334	`<db>-txid` sidecar is read in follow mode only (fact R5-1e). A
1335	generation holding a snapshot and nothing at level 0 therefore starts
1336	replication at TXID 1: the first upload is `[1, 1]` (fact R5-1a), later
1337	writes land below `N`, and a cold restore rooted at `N` skips them and
1338	loses every write since the install (fact R5-1b; the R5-1
1339	counterexample, confirmed). The remedy the pinned library supports
1340	unchanged is the **anchor** of step 2: a level-0 file `[N, N]` with
1341	every page, beside the snapshot. The open takes `N` as its position,
1342	the local WAL does not match it, and the next sync is a full upload at
1343	`N + 1` (fact R5-1c); a cold restore afterwards holds every row (fact
1344	R5-1d). Every install of a generation writes its anchor before any
1345	process may open the database: a landing (§7.6 `building`), a push's
1346	install, a dirty rollback's install on the source (§7.8). **The PUT
1347	must be acknowledged before replication opens, and the position is
1348	what the listing then shows** (R6-1): litestream derives its position
1349	from the remote level-0 files actually present, so an anchor still in
1350	flight is no anchor, and an activator that opened on the strength of
1351	having issued the PUT would replicate from TXID 1. The activator
1352	therefore waits for the PUT's response, retrying the same bytes after
1353	its client timeout (the original may still land, identical), and only
1354	then opens; it never sets the position itself. Rev 7.6's model did
1355	(`db.Pos = cur`, R6-1); rev 7.7's `restoreInit` returns nothing until
1356	the anchor is acknowledged and reads the position from the listing
1357	(rule `anchor-acked`; the witness holds the anchor PUT across forty
1358	attempted opens and requires the host not to open, §14.2.5). A **cold
1359	restore of a replica that has replicated since needs no anchor**: the
1360	newest level-0 file is never removed by TXID- or time-based retention
1361	(fact R5-1f, asserted by identity), so a fresh box continues at exactly
1362	`N + 1` (facts R5-1g, h; `TestGate_AnchoredLineageThroughStore` for
1363	three disk losses in a row). The wake writes one anyway whenever the
1364	restored TXID is above the newest current level-0 file, which costs
1365	nothing when it is not (the model's `restore-anchor`). Oracles never
1366	write one: a cold-restore check is the pure calculation of steps 4, 5
1367	and 8 (R6-1).
1368	8. **Rotation, retention and root advancement (R5-3).** Litestream writes
1369	a new snapshot `[1, P]` at its snapshot interval, and
1370	`EnforceSnapshotRetention` keeps the newest, returning
1371	`minSnapshotTXID` = the `MaxTXID` of the snapshot before the oldest
1372	kept one; the store then expires every level-1 and higher file whose
1373	`MaxTXID` is below it, and level 0 by time (fact R5-3a, b). After two
1374	rotations no current file continues from the pinned snapshot (fact
1375	R5-3f): a restore rooted there fails with "non-contiguous ltx files:
1376	have up to 1 but next file starts at 5" (fact R5-3d) while a restore
1377	from the newest snapshot holds every row (fact R5-3e). Protecting the
1378	pinned version alone does not protect its continuation; **the root
1379	advances**. A **verified successor snapshot** is a current level-9
1380	file of the named generation with `MaxTXID ≥ snapshot_txid` that
1381	passes `Verify`; only the generation's own replicator writes under its
1382	prefix (C3a, and the generation name is the operation's), and a
1383	stale re-upload of a rotated snapshot is identical bytes under the
1384	same key, so the newest current one is the one litestream itself
1385	restores from. `generation.json` is not rewritten at rotation: the
1386	pinned root is the install's identity and the floor the successor must
1387	clear, not the only root (step 4). The sweep protects every current
1388	version under `holder.generation` and the pinned version (§6.4). **The
1389	newest level-0 file survives every retention path** (facts R5-1f to h;
1390	R7-3): compaction deletes its inputs bar the newest, and the expiry
1391	below the previous snapshot never takes the newest level-0 file, which
1392	is where a fresh box reads its position. Rev 7.7's model kept it only
1393	through compaction and expired it when the local position had run
1394	ahead of the uploads (R7-3; the model's `newest-l0`).
1395	9. **Writer sessions and epochs: two writers whose uploads could overlap
1396	never share a generation, every path that opens replication is
1397	admitted before its app starts, and a box never reuses its local
1398	database (claim rev 6.10 §6.4a; R7-1, R8-1 to R8-5, R9-1 to R9-5,
1399	R10-1 to R10-7).** Litestream writes each
1400	file to a key built from the level and the TXID range only, and its
1401	PUT is unconditional (`TestFact_R7_1_UnconditionalPut`). So a writer A
1402	whose level-0 upload for `[N + 1]` is still in flight when A dies with
1403	its disk, and a writer B that restores the generation through `N` and
1404	uploads its own `[N + 1]`, collide: if A's PUT lands last it replaces
1405	B's file and the next cold restore loses B's acknowledged writes; if it
1406	lands after B initialized its position and before B's sync, B's upload
1407	loop takes the remote `[N + 1]` as already uploaded and skips B's
1408	(`replica.go` `Sync`), and B's write is never replicated at all.
1409	`lock.json` cannot revoke a PUT S3 has accepted, and waiting for the
1410	lease to expire proves nothing about requests already signed. Claim
1411	rev 6.9 states the rule and this spec owns the data path:
1412	- **`AdmitWriter`, one claim CAS before the app process starts**
1413	(claim rev 6.10, R10-1; this reverses rev 6.8.2's order, which let
1414	an app acknowledge work before it had a session: a background worker
1415	committed and acknowledged, the app crashed before readiness, the
1416	old certificate still stood and the next warm admission purged the
1417	acknowledgement silently). The order is: the CAS; the purge and the
1418	restore of the baseline; the app start; readiness; uploads. A
1419	**session belongs to the agent's replicator**, not to the app
1420	process: an app that crashes or restarts while the same agent keeps
1421	replicating stays within the admitted session and is not re-admitted;
1422	**a new agent process is always a new session**, so an agent that
1423	restarts under a running app stops it (the replicator that was
1424	admitted died with the old agent) and its next wake is a new
1425	admission, which declares what the app acknowledged meanwhile.
1426	`holder.session` is the claim `gen` of the CAS that admitted the
1427	current writer session; `holder.writer_box` is the box it admitted
1428	(R9-2). Every path that opens replication makes this CAS: an ordinary
1429	wake, a committed move's target serving while the claim is still
1430	`landing`, a probe and a restarted probe, a reverted source, an
1431	opened rollback recovery, a push's writer (R8-2). The library's call
1432	is `AdmitWriter(Admission{ObservedOpID, ObservedPhase,
1433	ObservedSession, ObservedGeneration, Box, Mode, NewGeneration,
1434	PredecessorCertified, RemoteMaxTXID, KeepStamp, Coverage, Region,
1435	PredecessorRegion})` (R10-4; `Coverage` since claim rev 6.12,
1436	`Region` and `PredecessorRegion` since rev 6.13, E 47426cc1), and
1437	this spec's model is shaped like it. It requires the observed `op.id` and `op.phase` (serving's
1438	`""` compared literally, so a closure computed under serving fails
1439	once any operation starts), the observed `holder.session` and
1440	`holder.generation`, and **`op.exec` to be this box**, in every op
1441	kind (claim rev 6.8.1); it is refused in **`creating`, `deleting`,
1442	`parking`, `purging` and `placing`** (R9-4, R10-4): a create's first
1443	writer is admitted after `CompleteCreate`, under `serving`, and
1444	nothing writes while a placement runs. After a conflict the box
1445	re-establishes its evidence, the certificate, the exec handover,
1446	rather than re-reading alone. It writes `holder.session = its
1447	resulting gen`, `holder.writer_box = this box`, and a record in
1448	**`holder.admissions`** `{session, box, generation, region,
1449	predecessor: {session, box, generation, stamp}, predecessor_region,
1450	mode, coverage, covered, writes_lost?}` (claim rev 6.14 §6.4a item
1451	1; the library's `AdmissionRecord`). `region` is where the new
1452	writer's generation keeps its objects, the admitted box's region;
1453	`predecessor_region` is the last record's `region` (before any
1454	record, the writer box's region, `""` when the generation holds
1455	nothing anywhere, as after a create).
1456	**The predecessor is the last record there**, with its own session,
1457	box and generation; it never comes from the holder's fields, which a
1458	clean return has reset to the source's generation for the restore
1459	while the predecessor is still the target's writer (R11-4; rev 7.11
1460	journalled the target's session and box with the source's
1461	generation, a writer that never was; INV-16). `holder.admissions`
1462	lives in the holder, so it survives every operation transition,
1463	release and new operation; its retention is **deliberately
1464	conservative** (claim rev 6.14 item 8, R12-6): covered records are
1465	trimmed from the front only, while more than eight remain, an
1466	uncovered record stops the trimming and everything behind it is
1467	kept, and there is no compaction. The
1468	admission **never replaces the operation**: kind, id, phase,
1469	participants, obligations and the rest of the journal are kept.
1470	- **Failed starts are governed by a retry policy, never by another
1471	admission** (R10-1). Within the admitted session the agent retries
1472	the app start with a doubling backoff from one step (1, 2, 4, 8, 16
1473	steps in the model; seconds in production) up to **five attempts**;
1474	a start the environment is not ready for (config not rendered, the
1475	release not live) waits and counts no attempt. For a **serving
1476	wake**, at the fifth failure the box marks the host **failed**,
1477	abandons the session's start, and creates no new session for the
1478	host until an operator clears it (or a health signal does; the
1479	model's operator clears it after half a horizon). For a **probe**,
1480	the restarts share the probe attempt's 30 s readiness window (§7.7):
1481	the fifth failure or the window's end, whichever comes first, ends
1482	the attempt, the operation counts one of its budgeted attempts, and
1483	the host is not marked failed. Five attempts because the start's own
1484	faults (a missing key, a bad bundle) do not heal within the window
1485	and a crash loop would otherwise churn generations. The waits
1486	between attempts total 15 s (1 + 2 + 4 + 8); each attempt's own
1487	start and readiness time is on top, so five attempts are not a
1488	bound on a serving wake's duration, only on its count. An app's
1489	writes are never left in an interval without an admitted session:
1490	there is no app before the CAS, and the session stands until the
1491	next CAS.
1492	- **A box never reuses its local database (R9-1).** Before it starts,
1493	every admitted writer purges the local database with an
1494	error-returning purge; if the purge fails the writer does not start
1495	(a transient error: the next attempt purges again). It then restores
1496	from the certified remote baseline, under the lease, and starts the
1497	app on that; the restore is version-pinned and the planner's (steps
1498	4 and 5). A warm database is never the baseline, whatever it holds:
1499	acknowledged writes it held that never uploaded are lost, and they
1500	are **declared** (below), never silently dropped. There is no
1501	lineage file and no provenance check.
1502	- **Warm continuation** is an admission in **warm** mode: legal only
1503	if `closed/<holder.session>.json` exists for the observed session and
1504	its `max_txid` equals the generation's remote maximum TXID over every
1505	level (`PredecessorCertified`). **Any `op.exec` box** may continue
1506	on it (claim rev 6.8.2): the certificate proves every upload of the
1507	session completed, whichever box made them. The admitting CAS moves
1508	`holder.session` forward, so that certificate names a dead session: a
1509	delayed, replayed or re-created certificate of any earlier session
1510	can never authorize anything again. The writer restores the same
1511	generation **up to the certificate's `max_txid`**, refusing to start
1512	on a restore that stops short of it, and reads its remote position
1513	at its first sync (litestream initializes it lazily).
1514	- **Everything else is cold**: no certificate for the observed
1515	session, a mismatched `max_txid`, any doubt. A cold admission is an
1516	installing CAS: in the same write a new `holder.generation`
1517	(`NewGeneration`) and `holder.stamp = the resulting gen`. The new
1518	generation is either the operation's **prepared** generation (a
1519	landing's or a push's `g-<op id>/`, built from the sealed archive
1520	with its snapshot `[1, N]` and anchor `[N, N]`; a dirty rollback's
1521	return generation), opened exactly once, by its probe, and never
1522	re-entered once it is `holder.generation` or an ancestor of it (a
1523	dead writer's uploads may still land in it); or a **fresh** id; warm
1524	passes an **empty** `NewGeneration` (R10-4). The writer restores the
1525	prepared generation from its pinned snapshot, or the predecessor
1526	generation's remote (`holder.generation` as observed) for a fresh
1527	one, in its own region; a fresh generation is **empty** until the
1528	writer's first upload, the full file `[1, 1]` of the restored
1529	baseline (fact R5-1c), made after the app started and before the
1530	marker; the bytes are captured once and a retry carries the same
1531	bytes (R10-7). When the observed session had no certificate and the
1532	baseline does not cover the predecessor's last acknowledged position,
1533	the CAS records **`writes_lost {box: holder.writer_box, generation,
1534	session, remote_max_txid}`** in its journal entry and the box raises
1535	an alert (R9-2): the predecessor's acknowledged writes beyond its
1536	uploads are gone with its database. When the baseline is a **seal
1537	that covers the stopped predecessor** (a landing's, a push's, a
1538	return's prepared generation, built from the stopped database's
1539	every page), there is nothing to declare: the admission's
1540	**`Coverage`** is `sealed` (claim rev 6.12, replacing rev 6.9.1's
1541	`BaselineCoversPredecessor`); the comparison is against the seal's
1542	own position, never a TXID from another region. A clean rollback's
1543	return with `src_covered` (§7.8) is covered too, `clean-return`: the
1544	unchanged target and the source's complete replica establish
1545	preservation, and the source's re-admission declares nothing. The
1546	coverage speaks for the **target's probe session** and for the
1547	**source's cut session** (`cut.session`, journalled at the stop)
1548	only: a later session of the recovered source that dies uncertified
1549	is declared like any other, and a return made clean only by a
1550	declared-lost target is not covered at all: it records `writes_lost`
1551	for **every session the target was admitted into since the cut**,
1552	certified or not (a probe session that closed cleanly and a warm
1553	continuation that died are two; the first's writes are durable only
1554	in the lost target's region, and no return lane carries either's;
1555	seed 33373 / 100,000, hidden until the session-scoped match of
1556	R12-1). **Representation** (claim rev 6.22 item 2, R13-3, R14-2): the
1557	admission entry carries `writes_lost` (one, the predecessor's
1558	session) and **`additional_writes_lost`** (a list, the other target
1559	sessions since the cut, and the source's cut session, under its
1560	persisted identity `cut.session`, when `src_covered` is false),
1561	each `{box, generation, session, remote_max_txid}`, **unique by
1562	`(box, session)` across both**: a target destroyed after the flip
1563	and before its first admission leaves the source's cut session as
1564	the predecessor itself, declared once (rev 7.14 declared it twice,
1565	through a separate field; INV-21); the caller supplies
1566	the list and the library records it in the admitting CAS; the
1567	admitting box raises **one alert per declaration** after the CAS
1568	and retries until delivered, and the console's durable loss record
1569	is the long-term copy, so trimming a covered entry never loses a
1570	declaration (the model: `admissionRecord.AdditionalWritesLost`, an
1571	alert each, INV-14 counts them). Only
1572	coverage `""` with no certificate records `writes_lost`, and the
1573	record always names its coverage, certified or not. A seal built
1574	from the **remote** because the disk was gone (`seal.from_db` false,
1575	§7.4) stops at the remote's position and covers nothing beyond it:
1576	the prepared generation's admission has coverage `""` and records
1577	`writes_lost` for the predecessor's acknowledged writes past it, as
1578	a cold admission from the remote would. The box is never inferred from `op.exec`. A write the
1579	host's remote holds, in any generation, is never declared lost while
1580	its writer's box is with us (INV-15): the lineage adopts the
1581	generation that holds it, a dirty return's lane, instead; a box
1582	declared lost may leave such writes behind, and so may a rollback
1583	whose target was declared lost (no return lane runs; the seal in the
1584	target's region is unreadable from the source); the record's
1585	`remote_max_txid` names where an operator finds them (§7.10).
1586	- **Only warm and cold exist (R9-3).** A first install, after a create
1587	or an adoption with nothing replicated, is a cold admission into an
1588	empty generation: no LTX file until the first committed transaction,
1589	never a zero-TXID file (`TestFact_R8_3_EmptyBootstrap`); the app
1590	starts first and may create its database, as the activator does
1591	today. There is no fresh, reserve, build or open transition.
1592	`holder.generation` is the only authoritative generation in every
1593	kind and phase: a probe or a recovery that opens replication is a
1594	cold admission that moves it, never an op-journal generation. A
1595	cold admission issues a new `holder.stamp` **except** when no writer
1596	was admitted since the current stamp was issued (`holder.stamp >
1597	holder.session`, the library's `KeepStamp`, claim rev 6.9.1): a
1598	landing's first probe after the flip keeps the stamp the flip issued
1599	and the target's record activated; a restarted probe, a push and a
1600	dirty return take a new one.
1601	- **A cold admission's generation is unfinished until `generation.json`
1602	names it** (claim rev 6.10, R10-2). Until then its baseline, the
1603	journalled predecessor, is part of the live set: no `park-generation`
1604	chore for it may be queued and the sweep never parks it (rev 7.10
1605	queued the chore at the CAS, so a writer that died before its first
1606	upload could have its only baseline archived under it). The chores
1607	that retire superseded generations are queued by the **marker's
1608	publication**, through one **`PublishGeneration(observedOpID,
1609	observedPhase, observedSession, publishedGeneration, region,
1610	newID)`** CAS (claim rev 6.12, replacing `QueueGenerationRetire`):
1611	bound to the observed operation and phase like the admission, legal
1612	while serving and inside any operation a writer runs in (a restarted
1613	landing probe, a rollback's or a revert's source; R11-5), it
1614	**requires `holder.generation` to be the published generation and
1615	an entry to name it, then walks every entry of `holder.admissions`
1616	in order, skipping covered ones** (claim rev 6.22 item 5, R13-2;
1617	bounded by the list's length; warm entries are born covered, so it
1618	visits every uncovered cold entry): a predecessor whose
1619	`predecessor_region` is `""` (it holds nothing anywhere) is covered
1620	with no chore; one that is the published, live generation again (a
1621	clean return's source generation, a republished lagging marker's)
1622	is **left uncovered** with no chore (covered, nothing would retire
1623	it once a later admission supersedes it, since that admission's
1624	predecessor is the last record and not the generation it restored
1625	from: seed 41914 / 100,000 left the source's generation as residue;
1626	rev 7.13 note 6, adopted); one whose objects are in the publishing
1627	`region` gets one deduplicated `park-generation` chore there and is
1628	covered; one whose objects are in **another region** stays
1629	uncovered, with no chore, and the walk goes on. The walk finds what
1630	rev 7.12 enumerated: the predecessor; behind a lagging marker,
1631	every generation of the chain of unfinished admissions between the
1632	marker's generation and the new one, and the marker's; and the
1633	predecessor of any earlier cold admission not yet covered (its
1634	writer died after its marker landed and before the CAS). **Every
1635	cold admission publishes**, a prepared generation's included (rev
1636	7.12's model left a prepared generation's predecessor to the
1637	operation, R12-3): a landing's publication in the target's region
1638	leaves the source's generation uncovered, and the commit covers it
1639	(below). Its chores carry `op = op.id` inside an operation and `op =
1640	"session:<holder.session>"` while serving. **Retirement happens only through it, and only of
1641	predecessors recorded in `holder.admissions`** (R11-2). An adopted
1642	legacy host's generation is the location root itself, named by the
1643	sentinel **`"@root"`** so a chore can name it; `""` and `"@root"`
1644	are one origin, so nothing retires the active legacy replica before
1645	a cold admission has created a successor and published it;
1646	`holder.generation` is `""` for such a host until its first cold
1647	admission, and the adoption writes `holder.writer_box` as the box
1648	running the pre-release process, so the first cold admission's
1649	`writes_lost` names the writer whose unuploaded writes it leaves
1650	behind (R10-5, R11-3). **That writer is the legacy identity**
1651	(claim rev 6.24, R16-3): `{session: 0, generation: "" (read as
1652	@root), box: holder.writer_box}`, adoption's `holder.session` being
1653	0; it is valid in both `writes_lost` and `additional_writes_lost`
1654	(a lost-target return after a move cut at session 0 declares it
1655	there), every other declaration has a session above 0, and a
1656	declaration always names a box: a created incarnation's first
1657	admission, whose predecessor has no writer (`holder.writer_box`
1658	empty), declares nothing (INV-24; rev 7.13 to 7.16 gave adoption
1659	session 1 and declared a boxless record for a created
1660	incarnation's first admission). **Coverage, completely** (claim rev 6.22 item 5,
1661	R13-2): a record is covered when its predecessor's retirement is in
1662	hand in the region that holds the predecessor's objects, and an
1663	entry becomes covered in **exactly four ways**, no other transition
1664	covers anything: **at birth**, a warm entry (its predecessor is its
1665	own generation, which nothing retires; the next cold admission's
1666	record names it and queues the chore), or an entry admitted while
1667	the claim already holds a park of the whole location in its
1668	`predecessor_region`: an unscoped `park-replica`, or a park scoped
1669	**exactly to `holder.location`**; a scoped park of an old
1670	incarnation or of a staging prefix does not count (claim rev 6.24
1671	item 5; that park retires the predecessor: a rollback's return
1672	admitted after the release queued the target region's park, which
1673	the CAS that queued it could not see; seed 1036 / 3,000); **by publication**, above; **by
1674	`CoverRegionPredecessors(op, phase, region)`** in one of the three
1675	CASes that queue a whole-location park of `region`, every uncovered
1676	entry whose `predecessor_region` is `region`: the commit's
1677	`park-superseded` of the source region (§7.9), a rollback's
1678	`park-superseded` of the target region at the target's release
1679	(§7.8), and the console's release of a declared-lost target (§7.10),
1680	which retire those generations wholesale and so queue nothing; and
1681	**by `CoverParkedPredecessors(op, phase, region, generations)`** in
1682	the CAS that queues an at-rest `park-sweep` and in the CAS that
1683	acknowledges it, only the uncovered entries whose predecessor is one
1684	of the listed generations, the ones that sweep actually retires (a
1685	predecessor with a sweepable object at the queuing; one whose
1686	objects it retired on the way, at the acknowledgement): a sweep
1687	never covers a predecessor it did not park. A predecessor whose
1688	objects live in another region (a move's source generation, seen by
1689	the target's publication) is **never queued into its region from
1690	here**, since the rollback may still need it (seeds 1036 and 1296 /
1691	rev 7.12; witness `wRollbackBaselinePreserved`). INV-17: when a
1692	whole-location park of `holder.location` completes in a region, no
1693	record whose predecessor's objects were there is uncovered. A dead
1694	generation holding nothing yet still gets its chore in the
1695	publishing region, as does one whose objects were parked already: a
1696	dead writer's late upload or certificate may land in it within the
1697	chore's horizon. A failed cold start leaves an empty, unpublished
1698	generation; the next attempt is cold again and the marker it
1699	publishes retires it.
1700	- **A marker that lags `holder.generation`** (an absent marker is the
1701	origin `""`, for the sweep as for the restore, R11-1) is read through
1702	`holder.admissions`: when it names the predecessor of the latest
1703	admission, or the predecessor of a chain of admissions each of which
1704	died before its marker (two in a row happen: the second's purge
1705	failed after its CAS), that is the normal unfinished state, every
1706	generation of the chain and the marker's is live, and there is no
1707	alert. **The run walk, in one region's bucket** (claim rev 6.22
1708	§6.2a, R13-1): the next admission follows each record's
1709	`predecessor` back from `holder.generation` to the marker's
1710	generation, newest first. A link whose generation keeps its objects
1711	in **another region** is passed over, covered or not: it holds
1712	nothing in this bucket, and its own region's park retires it (a
1713	clean rollback's fresh source admission R, admitted after the
1714	target region's park was queued and dead before its first upload,
1715	walks R, then the target's T in the other region, born covered under
1716	that park, then the source's S, and restores S;
1717	`TestInterruptedCleanReturn` walks that and R2 → R → T → S after
1718	it). A link **in this region** must be uncovered: a covered local
1719	generation is retired or being retired here, so reaching one as a
1720	needed baseline **refuses the start and alerts** (rev 7.13 read
1721	objects alone and would restore the marker's retired generation as
1722	an empty database; witness `wCoveredLocalBaseline`); an uncovered
1723	local link that holds an object is the baseline, the nearest such;
1724	one that holds none (a fresh generation that never uploaded) is
1725	passed over; else the marker's generation. **The start restores
1726	what the walk selected** (R14-1): the marker's generation through
1727	`generation.json`, as every ordinary restore; a run generation the
1728	walk selected **rooted at `[1, 1]`**, its first full upload, never
1729	through the marker, which still names the run's baseline (rev
1730	7.14's start selected R from R2 → R → S and then refused it because
1731	the marker named S, while the oracle restored it; the marker is
1732	never published backwards). The model's `restoreCalc` over the
1733	marker's generation and `restoreWith` rooted at `[1, 1]` over a
1734	selected one are the reference the selector F mirrors. An empty
1735	`holder.generation` for any other reason is unexplained missing data:
1736	refuse the start and alert. A `holder.generation` that holds objects
1737	has its marker published again (from the operation's build journal
1738	for a prepared generation, rooted at `[1, 1]` otherwise) and the
1739	chores queued, before anything else. Any other disagreement between
1740	the marker and the claim leaves the location untouched and alerts
1741	(§6.4).
1742	- **A clean close is a one-use certificate.** A writer session
1743	stopping cleanly first waits until **every request it issued over
1744	its lifetime** returned **success to the client, within the client's
1745	wait** (R8-5, R9-5, R10-7): every level-0 upload, every compaction
1746	and snapshot upload, every retention delete, **and the start's own
1747	PUTs**, the fresh generation's first upload and a warm restore's
1748	anchor, which enter the same ledger. A request the client timed out
1749	on, whether or not it later completed on the server (a lost
1750	response), one the server refused, and any retry after a timeout
1751	make the session **uncertain for good**; server completion and the
1752	client's response are distinct, and only the latter advances the
1753	start. A session whose start has not opened replication, or whose
1754	replicator died with its agent, certifies nothing. A session that can prove
1755	completion writes `<location>/<generation>/closed/<session>.json`
1756	`{session, box, max_txid, closed_at}` once (`If-None-Match`), then
1757	releases its lease; nothing of the host may run when it certifies
1758	(the unit stop kills the cgroup; a descendant that escaped it makes
1759	the close fail rather than wait, since its writes would be lost
1760	silently at the next purge, and the next wake is cold and declares).
1761	A certificate PUT not acknowledged within the client's wait ends the
1762	close uncertified: the PUT may still land, and a later wake that
1763	finds it may continue warm, since the drain was complete; the next
1764	wake is cold. **No certificate is ever deleted or reused**.
1765	Litestream's `Replicator.Close` drops the initial `SyncAndWait`
1766	error (`internal/lease/lease.go`), so certificate eligibility needs
1767	its own evidence, never `Close`'s return value. An operation that
1768	takes the writer over, a push, a move's cut, a delete or a purge,
1769	drops a pending close: the generation is being replaced or parked.
1770	- **Writers are bound to their generation.** The replica client is
1771	constructed for the `{holder.location, holder.generation, session}`
1772	the writer was admitted with and refuses any key outside
1773	`<location>/<generation>/`: level-0 files, compaction, snapshots,
1774	retention. It never re-reads the generation, so a new admission is a
1775	new writer. A dead writer's late uploads land in the old generation,
1776	or in the current one **before** the session that superseded it
1777	opened; a cold successor has a new generation, and a warm successor
1778	exists only after the old session certified that every one of its
1779	requests had completed.
1780	- **Conditional PUT alone would not do** (R7 review): if A's file won a
1781	create-only race, B would have to detect differing bytes and fail
1782	closed; the remote-position shortcut would have to check identity;
1783	multipart completion would need the same condition; and a delete
1784	marker makes a key creatable again. Disjoint generation prefixes
1785	need none of that.
1786
1787	The model encodes all of it (§14.2.2): both completion orders and the
1788	race are witnesses whose late upload lands harmlessly in the dead
1789	generation with the rule and loses B's write without it; a dead
1790	session's certificate with a matching stamp and `max_txid` authorizes
1791	nothing; the collision during a committed landing's serving and during
1792	a probe restart is caught by the admission inside the operation; a
1793	non-exec writer is refused; a valid certificate over a stale local
1794	database restores the remote; a crash with an unuploaded write is
1795	declared; a stale closure during a delete is refused; an empty first
1796	wake and an empty install write no file; a retry that succeeds while
1797	its original stays unresolved, a maintenance retry, a lost response, a
1798	first-upload retry and an anchor retry write no certificate; a
1799	background acknowledgement right after the start, then a crash, is
1800	declared by the next admission (under rev 6.8.2's order it is purged
1801	silently); a crash before the first upload leaves the predecessor live
1802	until the marker names the new generation (with the chore at the CAS
1803	the predecessor is parked and the recovery restores nothing); a
1804	rollback whose source replica stopped short of the stopped database
1805	returns the seal. The cost is a restore at every wake, warm or cold, a
1806	full first upload per fresh cold generation (none for an empty one),
1807	three local passes for an operation's prepared generation as §7.3
1808	prices an install, a restore per probe attempt, and a dead generation
1809	to park.
1810
1811	So:
1812
1813	- a request that completes late can only add an object to **its own**
1814	generation. A late snapshot or anchor PUT repeats identical bytes
1815	(another version, never opened); a late LTX PUT from an old executor,
1816	or from a dead writer of the same incarnation (step 9), lands in a
1817	generation the claim no longer names. Neither is ever restored into
1818	the current state;
1819	- the claim moves to a new generation at its writer's **cold admission**,
1820	before the restore, the app start and the probe (§7.14; rev 7.12's
1821	wording here, "only after that generation is fully installed and
1822	probed", described rev 7.9's protocol and is superseded, R12-4). A
1823	restore still never meets a half-written generation: a prepared
1824	generation is complete, snapshot and anchor, before any admission
1825	opens it, and a fresh one is empty until its own writer's first
1826	upload, which is the baseline's full file and lands before the marker
1827	names the generation; a restore reads the baseline the admission
1828	names, never a generation under construction;
1829	- what lands in a dead generation after its retirement is residue, not
1830	data: the straggler sweep (§6.4) retires it.
1831
1832	**Against litestream.** `lease.Restore` (`internal/lease/lease.go:404`)
1833	delegates to `Replica.Restore`, whose planner lists each level without
1834	versions and opens LTX files by key. Phase 1 needs three things beside
1835	it, none a change to the pinned library: the root rule of step 4 (the
1836	newest current successor snapshot of the named generation, else the
1837	pinned version opened by `versionId`, never another generation's or
1838	"the latest under the location"); the builder of step 2 (restore the
1839	staged versions, write the snapshot and the anchor with `ltx.NewEncoder`
1840	as `litestreamfacts` does); and the wake's anchor check of step 7. The
1841	rest of the planner, overlap rule, preference order and the
1842	non-contiguous error included, is used as it is. The repository's
1843	compaction ladder (`lease.go:55`: levels 0 to 3) is what produces the
1844	overlapping ranges step 4 handles. `internal/sim/litestreamfacts/`
1845	verifies the library behaviour this section relies on (facts R5-1 to
1846	R5-3, §14.2.6); §15 step 8 verified the S3 behaviour (claim §13 rows 2,
1847	3 and 10).
1848
1849	**In the model** (§14.2.2) a database is a map of keys to values with
1850	a lineage TXID and, separately, a **replication position**; transactions
1851	insert, update and delete; an LTX file carries its level, its range in
1852	replication numbering and the final image of every key it touches, and
1853	no checksum (R5-2); the serving process ships one level-0 file per sync
1854	at `position + 1`; compaction merges three level-0 files into a level-1
1855	file and deletes the inputs, then rotates a snapshot `[1, position]` and
1856	enforces retention as step 8 states (R5-3). The restore is steps 4, 5, 7
1857	and 8 as written: the root is the newest current successor snapshot at
1858	or past the pinned one, the position is read from the newest current
1859	level-0 file, and the anchor is written when the restored TXID is above
1860	it. The model drops the contract (`restore-by-generation`: the newest
1861	object under the location) and loses acknowledged writes; it drops the
1862	overlap rule (`restore-overlap`: rev 7.4's `min == current + 1`) and
1863	loses a compacted continuation; it drops the gap refusal
1864	(`restore-gap-closed`) and wakes a host without durable transactions; it
1865	drops the anchor (`restore-anchor`) and a snapshot-only install that
1866	wrote, replicated and lost its disk loses every write since the push;
1867	it drops root advancement (`root-advance`) and a host whose replica
1868	rotated four times refuses to wake (§14.2.5). Rev 7.4's model carried a
1869	full transaction history in every object, which no LTX file has; rev
1870	7.5's carried a whole-state checksum no pinned file has and a position
1871	that litestream never derives from a snapshot (R5-1, R5-2).
1872
1873	**Markers.** A generation is named in three markers. None is a record
1874	field.
1875
1876	| marker | where | written | content |
1877	|---|---|---|---|
1878	| `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) |
1879	| `<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) |
1880	| `.files-gen` | inside the files directory | **last**, after files, `<host>.env`, timers and the carried registry columns are all durable (§7.6) | `{"op","incarnation"}` |
1881
1882	`generation.json` is the one reused key a generation writes: everything
1883	else lives under the generation's own prefix. Without the condition, an
1884	earlier publication that completes late puts an older generation back:
1885	the claim names the new generation, the bucket names the old one, and
1886	every wake and recovery probe refuses: the start check compares the
1887	markers with the claim's generation and refuses forever (model 29; the
1888	model finds it after a push in 2 seeds of 100,000, §14.2.5). With the
1889	condition the late write fails with 412 (claim §13 rows 5 and 6), and
1890	the later generation stays.
1891
1892	All three are **protocol metadata**: excluded from the archive, from every
1893	content digest, and from F4's definition of the files directory (§6.1).
1894	Absent everywhere means origin. The claim's `gen` is a per-write version
1895	(claim spec §2), not a generation, so it never appears in a marker.
1896
1897	**The authoritative region (claim rev 6.5 §6.2a, R4-3).** The live set is
1898	`{authoritative region, holder.location, holder.generation}` plus the
1899	versions this spec names for the generation (the snapshot version in
1900	`generation.json`, noncurrent included; every current version under the
1901	generation, successor snapshots and anchors among them). Objects of the generation are
1902	live only in the authoritative region's bucket; a matching key in any
1903	other region is residue, and the sweep parks it. The authoritative region
1904	is the region of the holder's current installation:
1905
1906	| claim state | authoritative region for `holder.generation` |
1907	|---|---|
1908	| `serving`, `pushing` | `op.exec`'s region |
1909	| `moving` (before the flip), `reverting` | the source's region |
1910	| `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 |
1911	| `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) |
1912	| `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 |
1913	| `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) |
1914	| `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 |
1915	| `creating`, `deleting`, `parking`, `purging`, free | none: nothing is live |
1916
1917	**The start check (INV-4, J2-R2-8).** Before every spawn (`Start`, `Seed`,
1918	`ProbeWake`), the activator requires:
1919
1920	1. the box's own `<location>generation.json` (absent is origin) to name
1921	**the generation the claim expects**: `holder.generation`, as the
1922	admission's CAS left it, for every start; a probe's first admission
1923	publishes the operation's prepared generation (the move id, the
1924	rollback id, the push id) and a restarted probe's a fresh generation
1925	restored from it (§7.14; rev 7.11's clause named the prepared
1926	generation for every probe, R10-3); a lagging marker is read through
1927	`holder.admissions` (§5.1 step 9); and its incarnation to be the
1928	holder's;
1929	2. `.files-gen`, when the files directory exists, to name the holder's
1930	incarnation and either `holder.generation` or its cold predecessor
1931	(the newest cold admission into `holder.generation`, warm self-links
1932	skipped), which is the prepared generation a restarted probe was restored
1933	from; no older generation counts;
1934	3. `<dbPath>.gen` to name the same generation, exactly: the plain name
1935	carries no location, which the claim's `holder.location` vouches for.
1936	A warm database that does not is from an earlier stay on this box: the
1937	activator parks it (§6.3) and restores cold.
1938
1939	Rev 5's check compared the three markers with each other only. Astra
1940	showed (J2-R2-8) that after a commit, before the source is retired, the
1941	source's own three markers still agree with each other, so the "third
1942	fence" the model reported in rev 5 did not exist in the text: the model's
1943	check was stronger than the spec. Rule 1 makes it exist. A mismatch
1944	refuses the wake with a member-safe reason and pages. A marker that merely
1945	exists proves nothing (codex R2-6). The bucket read rides the wake's
1946	existing lease round trip to the same prefix. This replaces "staging wins"
1947	(`backend_exec.go:1581-1588`); `promoteStagedReplica` is deleted (M15).
1948
1949	### 5.2 Holds
1950
1951	A hold status is one the edge does not serve (`internal/edge/edge.go:595`),
1952	ticks refuse (`activator.go:2785-2789`), and no ordinary wake reaches:
1953	`moving` (source), `landing` (target), `restoring` (source, recovering),
1954	`releasing` (target, during a rollback). The `routes` table gains an
1955	additive column, `hold_op`, set whenever a hold is written. Leaving a hold
1956	is one conditional statement:
1957
1958	```sql
1959	UPDATE routes SET status='ready', hold_op='' WHERE host=? AND hold_op=?
1960	```
1961
1962	A late write from a finished operation matches nothing (codex 6). Reconcile
1963	mints held rows for every participant the claim names and never mints
1964	`ready` while the claim holds a move operation (`moving`, `reverting`,
1965	`landing` before the commit, or `restoring`) (§9.6, §19 K9).
1966
1967	### 5.3 Stop evidence (codex 1, R2-1, R2-2)
1968
1969	The execution right moves only on stop evidence. Rev 2 relied on the
1970	activator's in-memory `FenceAndStop` (`internal/activator/maintenance.go:50`).
1971	Round 2 showed two gaps: a flat child's descendant that outlives it
1972	(`childProc.Stop` waits for the main process only, `backend_exec.go:1502-1543`),
1973	and evidence that cannot be produced after an agent restart, because
1974	`FenceAndStop` returns `ErrStopUnproven` when it has neither an entry nor a
1975	remembered stop history (`maintenance.go:90-100`). Evidence comes from
1976	**durable, observable state**, never from memory. Claim spec §6.1 (rev 2
1977	and rev 3) adopts the joint review's D3 text, and this section follows it (joint D3):
1978
1979	> All lifecycle-controlled spawns require strict containment. Stop evidence
1980	> requires a closed admission fence, drained spawn attempts, an empty
1981	> complete process tree, closed replicators and no remaining database/WAL/SHM
1982	> holders. An absent host cgroup is insufficient where an earlier spawn
1983	> could escape containment.
1984
1985	and
1986
1987	> Reconstruction uses a cleanup-only operation that can reopen, identify,
1988	> kill and drain an existing populated cgroup without granting spawn
1989	> authority. `PrepareStrict` remains the empty-group spawn API. A pre-move
1990	> best-effort child is not certified stopped by ordinary parent exit.
1991
1992	`PrepareStrict` refuses a populated group (`internal/cgroup/strict_linux.go:206`),
1993	so the cleanup-only operation is a separate call, `cgroup.ReopenAndDrain`.
1994
1995	**Every spawn under a move is strict.** Flat children already run in a
1996	per-host cgroup, `carlos-exec@<host>` under the agent's delegated subtree
1997	(`internal/cgroup/cgroup.go:37`, `:243`; `Delegate=` in
1998	`internal/host/units/carlos-edge.service`), but placement is best-effort:
1999	a failed placement spawns "unaccounted" in the agent's own cgroup
2000	(`cgroup.go:248-252`). The strict path exists
2001	(`internal/cgroup/strict_linux.go`: `PrepareStrict`, `Populated`,
2002	`KillAndEmpty`). Under a move, every spawn of the host (the source's
2003	recovery, the target's probe, and the source's ordinary wakes while the
2004	claim says `moving`) uses `PrepareStrict` and refuses to spawn if it
2005	cannot. A nested child already runs in its own `carlos-instance@<iid>`
2006	unit.
2007
2008	**The source's pre-move child.** Its cgroup placement was best-effort. The
2009	source's readiness (§7.3, S2) therefore requires its current or next child
2010	to be strict: before `ready`, it stops an awake non-strict child (an
2011	ordinary idle stop) so the next wake is strict.
2012
2013	**Evidence** is `ReconstructStopEvidence(host)`, a new activator call that
2014	reads only the box's current state, so it gives the same answer after an
2015	agent restart as before:
2016
2017	1. **Kill and drain the tree.** Flat: write `cgroup.kill` on
2018	`carlos-exec@<host>` and wait until `cgroup.events` says
2019	`populated 0` (`KillAndEmpty`). Nested: stop `carlos-instance@<iid>`
2020	(and its seed and sidecar units) through the instance-control channel
2021	and require each unit inactive and its cgroup unpopulated.
2022	2. **No stray process.** The agent's own cgroup (`cgroup.procs` of the
2023	service's leaf) holds only the agent's own process. A strict spawn never
2024	leaves anything there; anything else is unattributable and refuses
2025	evidence with an alert.
2026	3. **No open database.** No process on the box holds the instance's
2027	database, WAL or SHM open (a scan of `/proc/*/fd` for the paths,
2028	restricted to the `carlos` uid).
2029	4. **Lease released.** The host's `lock.json` lease
2030	(`internal/lease/lease.go:86`) is absent, released, or expired by more
2031	than the lease's renewal margin.
2032	5. **Replica final.** After 1 to 4, a final checkpoint of the local
2033	database (if any) into the box's own `instances/<host>`, and its
2034	sha256.
2035
2036	**A durably never-spawned operation.** If the box's journal for the
2037	operation shows no spawn was ever attempted (the target's `landing_phase`
2038	before `probing`), steps 1 to 4 still run: an empty tree proves the same
2039	thing whether or not a spawn happened. "No entry in memory" is never
2040	evidence on its own (codex R2-2).
2041
2042	The box writes the result to the deployment bucket at
2043	`moves/<acct>/<app>/<host>/<op id>/stopped-<role>.json`: box label,
2044	incarnation, the claim `gen` it read, each step's observation, and the database, files
2045	and timers digests. It then CASes the claim's execution holder to `none`
2046	(§19 K3). The next holder reads the evidence and the claim before it starts
2047	anything.
2048
2049	**Evidence also starts a clock (model 1).** Ordinary replication is the one
2050	storage write claim C3 does not bind to a version: the serving process's
2051	litestream PUTs go to reused keys (litestream v0.5.14 `LTXFilePath`, names by TXID range,
2052	restarting at 1 for a new lineage). A PUT signed before the evidence can
2053	still complete afterwards. So every retirement of a location that a
2054	replicator wrote acknowledges only after a verification listing taken
2055	later than `evidence time + H`, where H is the late-completion horizon
2056	(S3 refuses a request whose signature is more than 15 minutes old, so H is
2057	15 minutes plus the longest request). The model drops this rule and finds
2058	residue in a freed host's namespace.
2059
2060	## 6. State inventory
2061
2062	### 6.1 Files on a box (codex R2-9)
2063
2064	| # | state | where | disposition |
2065	|---|---|---|---|
2066	| 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) |
2067	| F2 | litestream meta dirs | `<db>-litestream`, `.activator-<db>-litestream` (`backend_exec.go:1570-1571`) | rebuilt on restore |
2068	| F3 | `<dbPath>.gen` | beside the DB | protocol marker (§5.1); **local-parked with the database**, flat or nested |
2069	| 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` |
2070	| F5 | `.files-gen` | inside F4 | protocol marker (§5.1), never archived or digested |
2071	| F6 | `<host>.env` | `paths.go:50`; `CARLOS_ADMIN_TOKEN` (`admintoken.go:115`) and operator overrides | **carried** in the archive, as its own entry |
2072	| F7 | `<host>.config.env` | `syncexec.go:71-76` | **rendered** for the held row (§9.1), pinned by T3 |
2073	| F8 | `<host>-sidecar.env` | `paths.go:51` | **refused** (§7.1) |
2074	| F9 | launch files, sockets, log sockets, exit records | `provision.go:1282-1294` | rewritten per start |
2075	| F10 | quarantined restore `<db>.corrupt` | `backend_exec.go:313-324` | local-parked with the database |
2076	| F11 | layout journal | `<DataDir>/layout/<host>.json` (`provision.go:1303`) | the cut waits while present (`movespass.go:447`) |
2077	| F12 | operation journals | `<DataDir>/.moves/<host>/<op id>/` (new) | protocol state for this box's phases (§7.6, §7.8); parked at finalization |
2078
2079	### 6.2 Registry state (codex 16)
2080
2081	Every `routes` column (`internal/registry/registry.go:34`):
2082
2083	| column(s) | class | Phase 1 |
2084	|---|---|---|
2085	| 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`) |
2086	| Socket, DBPath | reproduced | derived for the target row's layout; **Phase 1 lands flat** (`routeFor` mints flat) |
2087	| Provisioned | reproduced | true |
2088	| Status, hold_op (new) | protocol | §5.2 |
2089	| **Replication** | **carried** | box-local (`registry.go:138-145`, `reconcile.go:1100-1113`) |
2090	| **NextDue** | **carried** | the app's own next wake, probed at stop (`activator.go:2019-2030`) |
2091	| Version, PrevVersion | reset | materialized for the held row (§9.2) |
2092	| LastError, DNSStatus, DNSCheckedAt, CertExpiresAt, CreatedAt | reset | recomputed by their passes |
2093	| Caps, Unit, Backing (unit), Platform, Tunnel, FleetBox, Pool, Canary, Addr, Addrs, Health | **refused** if set | not the platform's to move |
2094	| Replica, Replicas | **refused** | a replica, or a home with replicas (Q2) |
2095	| IdleSeconds, MaxRunSeconds, Args | n/a | sidecar columns |
2096
2097	The `timers` table (`registry.go:565-579`) is carried as a snapshot (§9.4).
2098
2099	### 6.3 Other host-keyed state (codex R2-9)
2100
2101	| state | where | disposition |
2102	|---|---|---|
2103	| 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 |
2104	| 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 |
2105	| copy receipts | `move-receipts/<host>/<op id>.json` (source bucket) | keyed by operation |
2106	| snapshots | `move-snapshots/<host>/<op id>/` (source bucket) | §8.3 |
2107
2108	### 6.4 Parking
2109
2110	Phase 1 uses the claim spec's park (§6.2 there) and local retirement
2111	(§6.3 there), with the move's own destinations:
2112
2113	- **One destination per retirement event (joint D5, N7).** Superseded data
2114	goes to `superseded/<op id>/<host>/<retirement id>/{instances,moves}/`,
2115	and local state to `.parked/superseded-<op id>/<host>/<retirement id>/`.
2116	The landing's park of an earlier stay, a failed target's cleanup, the
2117	source's retirement after commit and each staging retirement are
2118	separate events with separate manifests, even inside one operation. The
2119	model drops the retirement ids and the park never finishes: the second
2120	event finds the first event's immutable manifest and stops on unlisted
2121	keys.
2122	- **What a move parks is its location, not the host namespace.** The
2123	landing's park of an earlier stay, the source's park after commit, a
2124	rolled-back target's park and a push's park all name `holder.location`
2125	in their own region (C3a); staging parks name `moves/<host>/<op id>/`.
2126	- **Exact versions (joint N1, J2-R2-6).** The snapshot takes every version
2127	under the location, noncurrent included. The manifest records two sets
2128	(claim §6.2): the **archive set**, every non-marker version, copied by
2129	`versionId`; and the **deletion set**, every version, delete markers
2130	included, which is what a retry replays, by `VersionId`. The model replaces version deletes with bare-key deletes
2131	(delete markers on a versioned bucket) and finds parks that never
2132	finish, in 2,325 of 3,000 seeds (rev 5).
2133	- **The live lock is not data (joint N6).** The parker takes the location's
2134	replica lease first, and renews its own `lock.json` while it works. That
2135	key is excluded from the snapshot, the manifest and the emptiness check,
2136	and released by the parker's own version after the completion CAS. The
2137	model includes the lock and the park never finishes.
2138	- **Progress accumulates (model 2).** A copy's destination key carries the
2139	source version id (`<relative key>@<source versionId>`, claim §6.2), so a
2140	retry skips copies that landed and the manifest is written once every
2141	copy exists. Restarting the snapshot from scratch on
2142	every retry, with many versions and late completions, does not converge
2143	in the model.
2144	- **Verify after the horizon (model 1).** A park acknowledges only after a
2145	verification listing taken later than `evidence time + H` (§5.3, claim
2146	§6.2a) and, for a staging retirement, later than the staging horizon
2147	(§7.3). Anything found then is parked as a further retirement event of
2148	the same obligation, and the verification repeats.
2149	- **Local retirement** takes the host guard and writes a retired marker
2150	first (claim C7), so a stale background write for that incarnation is
2151	refused. **Installation stamps** (claim rev 6.5 §6.4, R3-3, R4-2,
2152	R5-4): an installation's stamp is the claim `gen` produced by the CAS
2153	that made it current, and **that CAS writes it into `holder.stamp`**
2154	(claim rev 6.5 §2), so the claim is the durable record of every
2155	installation's stamp and the recovery source for every box. The CASes
2156	that install, and so write `holder.stamp`, are: a create's serving CAS
2157	(claim §5.1 step 4); adoption (claim §9); a landing's flip (§7.5); a
2158	push's probe CAS (F7); a dirty rollback's source probe CAS (§7.8); a
2159	reinstall after quarantine. A dirty rollback installs a new generation
2160	and **never keeps its predecessor's stamp** (rev 7.5's model did,
2161	R5-4). The stamp is kept for as long as the installation exists,
2162	serving included. Each box keeps, under the guard, a record per host
2163	incarnation: `{active_stamp | none, retired_stamps}`. **Initialization
2164	(claim rev 6.5 §6.4):** a box creates or refreshes its record only from
2165	a fresh claim read under the guard, only when that read names it
2166	`op.exec` or the landing participant (the phase table, §5.1), setting
2167	`active_stamp = holder.stamp`: a create's first wake, adoption on the
2168	serving box after the adoption CAS, a landing in its `checking` phase,
2169	a box whose record was lost, on restart. Rev 7.5's model initialized
2170	the record from the claim revision at reconciliation, which
2171	intervening claim writes change (R5-4). **No local record: refuse.**
2172	Every host-state writer (config sync, release adoption, the
2173	activator's admission) carries `{incarnation, stamp}` **captured from
2174	the box's local record when it selected its work** (claim rev 6.5's
2175	answer 1: the fresh claim read under the guard is still required, for
2176	the incarnation, the operation and the config and release identity,
2177	but the stamp is the selection's), and is admitted only if its stamp
2178	**equals** the active stamp; a lower stamp, a retired
2179	stamp, any stamp while the active stamp is `none`, and any stamp while
2180	the box has no record, are refused (rev 7.5's model admitted a writer
2181	when no record existed, R5-4). **Two retirements, named at every
2182	call** (claim rev 6.5 §6.4): `retire-artifacts(S)` parks the local
2183	artifacts tagged with stamp `S` and **moves no stamp**: neither
2184	`active_stamp` nor `retired_stamps` changes (rev 6.3 had it add `S` to
2185	the retired set; rev 6.4's answer 2 withdraws that). It parks **by
2186	tag**: every local artifact carries the stamp of the installation that
2187	produced it (claim §6.3's inventory), `retire-artifacts(S)` parks the
2188	ones tagged `S` and leaves the rest, and a caller that expected another
2189	tag has made a mistake the model records (R6-4). Where the files
2190	directory is carried into the new generation (a push, F7; a landing's
2191	`restored` phase; the activator's park of a warm database before a cold
2192	restore) the retirement is of the database alone. It is what a
2193	landing that has activated its own stamp in `checking` uses in `local`
2194	to park its predecessor's database, files and `<host>.env`, what the
2195	activator uses on a warm database from an earlier stay, and what a
2196	dirty rollback's install uses on the source, whose pre-move stamp is
2197	still active at that point. Only two things move a stamp:
2198	**activation**, which puts the old `active_stamp`, if any, into
2199	`retired_stamps` and then sets the new one (so the dirty rollback's
2200	pre-move stamp retires when its probe CAS's new stamp activates), and
2201	`retire-installation`, which moves `active_stamp` into
2202	`retired_stamps`, sets `none` and parks every artifact; it is the local
2203	park at a delete, a move away (the source's finalization, §7.9), a
2204	rolled-back target's `cleaning` and quarantine (CC12). Nothing calls
2205	`retire-installation` to clean up a predecessor: rev 7.5's §7.6
2206	reused the general local park in `local`, which read literally retires
2207	the installation `checking` had just activated and refuses its own
2208	probe (R5-4). **A cold admission is an installing CAS too** (claim rev
2209	6.9 §6.4a; §5.1 step 9, §7.14): it writes a new `holder.generation`,
2210	a new `holder.stamp` and `holder.writer_box` in one write, with the
2211	predecessor's `{session, box, generation, stamp}` journalled in the
2212	same write; the box's record activates the new stamp from its next
2213	fresh read, and the carried files are retagged with it at the CAS,
2214	whether or not the start completes (the first rev 7.9 model left the
2215	files under the dead writer's stamp, and the next dirty install parked
2216	an artifact of a retired stamp, seed 453 / 30,000; rev 7.10's first
2217	model retagged them only at the start, seed 62 / 300); the restored
2218	database carries it; the dead writer's stamp retires with it. The
2219	purge of the local database that precedes every restore (§5.1 step 9)
2220	is not a retirement event: it deletes a file no installation will run
2221	again. There is no lineage file (rev 7.10). The admission's writer
2222	opens the new generation without a certificate of its own; its clean
2223	close writes the first one. **The return to source (claim rev 6.5,
2224	R6-4).**
2225	`holder.stamp` always names the installation `op.exec` should run, so
2226	**every CAS that changes `op.exec` writes `holder.stamp` in the same
2227	write**: a CAS that makes a new installation current writes the gen it
2228	produces; a CAS that makes an existing installation current again
2229	writes that installation's own stamp, taken from the op journal. The
2230	flip records the source's pre-move stamp `S` in the journal
2231	(`op.source_stamp`) as it writes the target's `F`; a rollback's return
2232	CAS (§7.8 `claimed`: `op.exec` back to the source) writes `holder.stamp
2233	= S`, never `F`. The source's initialization then finds `holder.stamp`
2234	equal to its `active_stamp` and changes nothing; a source whose local
2235	record was lost (a reboot) re-initializes to `S` from the same fresh
2236	read. A dirty rollback's install runs under `S`, its artifacts tagged
2237	`S`; the probe CAS issues `R` with `holder.generation`, and
2238	**activation of `R` tags the generation's artifacts `R`** and retires
2239	`S`. `F` was only ever active on the target and retires there
2240	(`retire-installation` at `cleaning`). Rev 7.6's model returned
2241	execution with `holder.stamp` still `F`, so the source activated the
2242	target's installation and tagged its artifacts `F` (R6-4); rev 7.7
2243	encodes rev 6.5 and records any activation of a stamp the claim issued
2244	for another box as INV-6 (`return-stamp`, with a witness whose source
2245	has lost its record, §14.2.5). Op ids are opaque and never compared
2246	(claim rev 6.1 Q1).
2247	Rev 7.4's marker compared operations by an order the production system
2248	does not have and admitted its own installation only by a `- 1` in the
2249	model (R4-2); rev 7.3's marker fenced the whole incarnation, and the
2250	move back never passed its probe. The model keeps the stamp record
2251	exactly as claim rev 6.5 states it (every installing CAS writes
2252	`holder.stamp`, `initRecord` under the guard, refusal without a record,
2253	activation the only move of the old stamp, `retire-artifacts` a named
2254	no-op on the record), requires the UK→US→UK round
2255	trip to serve on UK again unmutated, records a landing probe refused by
2256	its own installation record as a violation, and shows a stale config
2257	pass admitted across a retire-and-reinstall only when the stamp check
2258	and the host guard's fresh check are both gone (§14.2.5,
2259	`fence-by-installation`, `fence-stamp`).
2260
2261	No park destination is an ancestor of a live prefix (codex 8). **A park is
2262	its own journaled phase**, complete before any install into the vacated
2263	namespace begins (codex R2-6).
2264
2265	**The straggler sweep (J2-R2-1, CC15, model 17; claim rev 5 §6.2a).** S3's
2266	signature limit bounds when a request is accepted, not when it completes
2267	(claim C3a), so a request accepted before a retirement's horizon listing
2268	can still land after it. Within one incarnation the restore contract
2269	(§5.1) makes such a straggler harmless to data. It is still residue, and
2270	no later retirement of that location may ever run. Claim rev 5's at-rest
2271	sweep owns it: for a host with no operation running, each region's box
2272	lists the host's namespace and parks what is not live, as a further
2273	retirement event, under a `park-sweep` obligation the sweeping box owns.
2274	**The chore carries a persisted park scope** (claim rev 6.23 §2; R13-4,
2275	R14-5, R15-1): `{location, incarnation, evidence_at, request_limit}`,
2276	written at the queuing CAS, so every retry, an agent restart's included,
2277	uses the same location, archive incarnation and **original** evidence
2278	time; a retry's own clock is never evidence, and a restart never starts
2279	the horizon again (rev 7.13's model kept the evidence time in a
2280	box-local map that the restart cleared; witness
2281	`wParkScopeSurvivesRestart`). **`location`** is exactly one of
2282	`instances/<host>`, `instances/<host>/<incarnation>`, `moves/<host>/<op
2283	id>` (a move's staging or a rollback's return lane, the op id with no
2284	`/`) or `moves/<host>` (used by a delete's park of the staging namespace,
2285	§5.2, and by an at-rest sweep, each while no operation stages there;
2286	claim rev 6.26, R17-2), nothing else and no trailing `/` (the model's INV-23
2287	checks every scope against that grammar). **`incarnation`** names the
2288	archive: the location's own, the staging op's holder incarnation, or,
2289	for a free host's `moves/<host>` sweep, the newest retired incarnation.
2290	**`evidence_at` is always the original evidence or fencing bound**,
2291	never the cleanup's start time: the cut's stop evidence for the commit's
2292	park of the source region; the release's stop, or the declaration's
2293	`fenced_at`, for the target region's; **a staging lane's own seal
2294	bound**, the time after which no staging writer, its lease holder
2295	included, can still write (the seal plus the staging lease), persisted
2296	when the lane is sealed or fenced; the sweeping box's complete listing
2297	for a sweep; the publication that supersedes a generation for a
2298	generation chore. A chore queued without a scope (a delete's or an
2299	adoption's `park-replica`, whose CAS has no evidence time yet) binds one
2300	in a CAS before its first step runs, once its stop evidence is in hand,
2301	and never again; INV-22, no remote chore runs a step unscoped. **One
2302	deadline for every scope** (R15-1): acknowledge only after a
2303	verification listing later than **`evidence_at + H`**, with **`H` = the
2304	signature-age limit plus `request_limit`** (claim §6.2a, §2: 15 minutes
2305	plus 120 s in production; `sigAgeH + requestLimitH = horizonH` in the
2306	model, 45 + 15 = 60 steps). There is no separate staging contract: rev
2307	7.15 bound a staging park at cleanup and then kept the seal's quiet time
2308	instead of that bound, so a lane sealed at step 100, deadline 560, whose
2309	cleanup first ran at 600 would have waited until 660 (witness
2310	`wStagingScopeDeadline`: the cleanup acknowledges at once, through an
2311	agent restart, since the persisted deadline has passed). Rev 7.14 wrote
2312	`evidence_at + request_limit` here, dropping the signature-age
2313	allowance (R14-3). The sweep parks at once and acknowledges, with its
2314	straggler pass, only after a **verification listing later than
2315	`evidence_at + H`** (platform-1e's answer to rev 7.14 note 2: a
2316	park-sweep is a retirement event and is not exempt from the horizon). **On a serving host** the chore's op is
2317	`session:<holder.session>`, as for `PublishGeneration`. **On a free host**
2318	(no holder) the sweep is a **holderless sweep** (claim rev 6.15 §6.2a):
2319	one CAS sets `op = {kind: parking, id: <new op id>, intent: {park_sweep:
2320	"v1"}}` with no `exec` and no holder and queues only scoped remote chores
2321	owned by that op; it is the only holderless claim that may carry
2322	obligations, so it blocks `free`'s successor create while it runs (the
2323	create waits, it is not refused), and its last acknowledgement frees the
2324	claim again in the same CAS (`FreeAfterPark`), keeping `quiet_after`
2325	(witness `wFreeSweepVsCreate`; INV-20: a create never claims a host while
2326	a park of its namespace is outstanding). Another region's sweep while the
2327	op runs **joins** it with its own scoped chores under the same op id
2328	(R14-4, platform-1e's preferred reading of rev 7.14 note 1;
2329	`TestJoinHolderlessSweep` has two regions' residue parked under one op
2330	and one `FreeAfterPark`); any other operation running suppresses new
2331	sweeps; the console's recovery pass leaves the op to its
2332	runners and only replays `FreeAfterPark` for one whose chores are all
2333	acknowledged.
2334	**It discovers locations from the namespace itself** (claim rev 6 §6.2a,
2335	R3-4), not from `retired_incarnations`, which is capped at 32 entries and
2336	exists only to stop an incarnation being reused: it lists
2337	`instances/<host>/` with delimiter `/`, every page, refusing on a listing
2338	error; a child prefix of 64 hex characters is an incarnation location,
2339	residue unless it is `holder.location`; a level directory directly under
2340	the host prefix is the legacy location, residue unless `holder.location`
2341	is the host prefix itself; and within `holder.location`, every generation
2342	other than `holder.generation` is residue. **What it finds is grouped by
2343	the location it belongs to** (claim rev 6.24 §2, R16-2): each
2344	incarnation location its own, the legacy `instances/<host>` (a level
2345	directory or generation directly under the host prefix, never a child
2346	incarnation), `moves/<host>` for staging residue; **one chore per
2347	location**, scoped to that location with its archive incarnation (the
2348	location's own; the holder's for the legacy location or the staging
2349	sweep; the newest retired on a free host), and the archive is written
2350	under that incarnation. **A park executes strictly within its scope**:
2351	its listing is confined to the scope's namespace (an `instances/…`
2352	scope never lists or parks anything under `moves/`, the legacy
2353	`instances/<host>` scope excludes child incarnations, a staging lane's
2354	scope only its own lane), and every key a chore would archive must be a
2355	member of its scope (the model's INV-23 checks membership for every
2356	reference a park archives or deletes, in the manifest it builds and in a
2357	persisted manifest it replays, whatever rules are on, and an out-of-scope
2358	reference is never acted on, R17-1; rev 7.16 scoped the
2359	whole `instances/<host>/` listing as `instances/<host>` under the
2360	serving incarnation and archived a deleted incarnation's late object
2361	from there; witness `wSweepScopeMembership`). The same confinement
2362	governs a delete's parks, which cover the deleted incarnation's own
2363	location and the staging namespace, never the whole host prefix (claim
2364	rev 6.25 §5.2); an older incarnation's residue is this sweep's. **The live set is
2365	region-qualified** (claim rev 6.5 §6.2a, R4-3): `{authoritative region,
2366	holder.location, holder.generation}` plus the versions §5.1 names for the
2367	generation, the snapshot version `generation.json` names included, is
2368	protected in the authoritative region's bucket only (the table in §5.1);
2369	within `holder.generation` every current version is live, the successor
2370	snapshots and the anchor among them (§5.1 steps 7 and 8); and, in claim
2371	rev 6.4 §6.2a's words, **a child prefix that is not an incarnation id
2372	(64 hex) belongs to the host prefix's own location**: a level directory
2373	`0000` to `0009` or a generation prefix `g-<op id>/` directly under the
2374	host prefix is the legacy location's, never an incarnation location (the
2375	model's `locationOf`; rev 7.6's first baseline misread `g-<op>/` under a
2376	legacy host as an incarnation and swept the live generation, caught in 2
2377	seeds of 3,000);
2378	a matching key in any other region is residue and is parked, so a
2379	replica PUT for a legacy host serving in UK that lands in US after US's
2380	retirement is parked, not exempted. Claim §6.2a owns the sweep-side rule:
2381	the sweep never parks or deletes an object version in the live set, never
2382	touches the version `generation.json` names, never treats the marker as
2383	residue, reads the live set under the same fresh claim observation it
2384	uses for everything else, and touches nothing in a location whose marker
2385	disagrees with `holder.generation`, raising an alert instead, **except**
2386	for the one disagreement that is normal (claim rev 6.10, R10-2): a marker
2387	that names the journalled predecessor of the latest admission, or of a
2388	chain of admissions each of which died before its marker, while
2389	`holder.generation` is ahead of it; then every generation of the chain
2390	and the marker's are live, protected, and no alert is raised (§5.1 step
2391	9). The model
2392	keeps the real cap and shows a replication PUT of an incarnation 33
2393	recreates old landing after the list forgot it (`sweep-namespace`), and
2394	an old US PUT for a legacy host serving in UK parked only when the live
2395	set is region-qualified (`live-set-region`, §14.2.5). Being an obligation, it
2396	holds off any new operation over that region until it acknowledges (CC11),
2397	and every delete names a snapshot version, so nothing written later is
2398	touched.
2399
2400	**`moves/<host>/` too (CC20, in claim rev 5.1).** Claim rev 5's list left
2401	out staging. A staging request accepted before its lease ended can complete
2402	after the staging cleanup, and after the move's release nothing lists
2403	`moves/<host>/<move id>/` again. The sweep also parks everything under
2404	`moves/<host>/` while no operation runs, when no move is staging there.
2405	The model drops this and leaves staging residue for good (§14.2.5).
2406
2407	A periodic listing per host and region is the cost (rate: once a day, and
2408	after each operation's release). The horizon of §6.2a stays: it is what
2409	makes INV-10 hold **when an operation ends**, for every request that
2410	completes within `H`; the sweep covers only what completes after it. The
2411	model checks both: INV-10 at every release and free, excepting only
2412	versions created after `H`, and INV-10 everywhere at the end of the run.
2413
2414	## 7. The move
2415
2416	### 7.1 Request and refusals
2417
2418	`POST /api/cli/apps/{account}/{app}/instances/{host}/move`
2419	`{"region":"uk","cut":"auto"|"manual"}`, operator-only (§12). The door
2420	CASes the claim from `serving` (holder = this incarnation, execution
2421	holder = the source box) to `moving` with op id = the move id (§19 K2).
2422	**The target box is named in that CAS** (region HA L15, ruled H12): the
2423	door computes region HA's `choose(eligibleBoxes(region, pool), app)`
2424	(spec 1 §5.2: prefer a box running no instance of the app, then the most
2425	headroom, then the SHA-256 tie-break) over the roster and the edges
2426	snapshot. **Phase 1 scope (rev 7.20):** a move **into or out of a region
2427	with more than one eligible box is refused** at the door, with M-C21,
2428	until region HA's own model and plan cover multi-box regions; so in
2429	Phase 1 `choose()` always names the region's one box, and the source is
2430	the one box of its region. The refusal is a scope rule, not a safety
2431	rule: the protocol below is written for any target box the start CAS
2432	names. The choice is made once and recorded as `op.participants[1]`
2433	and `op.intent.target`; readiness (T8, T9), evidence, install and
2434	recovery bind to that box, and nothing substitutes another box: a target
2435	that cannot complete is replaced only by an explicit fenced transition
2436	(§7.10, L14), never by recovery picking a new one (P5-D2, A1-10). It
2437	is refused (400 or 409, with the sentence), and every box step re-checks:
2438
2439	- not exec-backed `kind:"instance"`, addr-backed, pooled, fleet-placed,
2440	non-hibernating (`internal/console/apiinstancemove.go:53-72`);
2441	- a replica (`:187-190`, `provision.go:978-980`), or a home with replicas
2442	(new);
2443	- a target of home on a console without host claims, or a home whose box
2444	sets a region code of its own (`apiinstancemove.go:203-209`; F2, rev
2445	7.24, Ruling R1), the current region, or one outside the manifest's
2446	`regions` (`apiinstances.go:1797`). A home target is named by the
2447	home's configured name; there is no `home` keyword (Ruling R3);
2448	- a source `<host>-sidecar.env`, or any refused registry column (§6.2);
2449	- a private store bound to the instance's environment (codex 12; F4);
2450	- the claim not `serving`, or any box in either region below the protocol
2451	floor (§11).
2452
2453	### 7.2 Record fields
2454
2455	Additive under `move` (`provision.go:907-917`). The claim carries the
2456	cross-operation serialization (§19); the record carries this move's phase
2457	journal, because only a move reads it.
2458
2459	```json
2460	"move": {
2461	"id": "mv_…", "incarnation": "…", "from": "", "to": "uk", "cut": "auto",
2462	"state": "landing", "requested_by": "…", "requested_at": "…", "updated_at": "…",
2463	"ready_at": "…",
2464	"inputs": {"bundle_etags": {"…": "…"}, "overlay_etag": "…", "release": "…",
2465	"files_plain": "sha256:…", "env_report": "sha256:…"},
2466	"cut_phase": "flipped", "cut_at": "…", "cut_budget_s": 95,
2467	"source": {"replication": "stream", "next_due": 0, "db_sha256": "…",
2468	"files": {"plain": "sha256:…", "sealed": "sha256:…", "bytes": 1824, "entries": 4},
2469	"timers_sha256": "…", "evidence": "…/stopped-source.json"},
2470	"flipped_at": "…", "landing_deadline": "…",
2471	"landing_phase": "probing", "landing": {"installed_db_sha256": "…"},
2472	"committed_at": "…", "opened_at": "…", "source_parked_at": "…",
2473	"rollback": {"id": "rb_…", "requested_at": "…", "reason": "…",
2474	"target_phase": "returned", "dirty": true, "evidence": "…",
2475	"source_phase": "probing", "recovered_at": "…", "opened_at": "…",
2476	"target_parked_at": "…", "release_deadline": "…"},
2477	"reason": "…"
2478	}
2479	```
2480
2481	Every box transition is a CAS on the record guarded by `move.id` and
2482	`move.incarnation`, **and** revalidates the claim's op id, kind and phase
2483	first (§19 K5).
2484
2485	### 7.3 Preparing and readiness
2486
2487	**Staging layout (codex R2-7).** Each artifact class has its own
2488	subprefix under `moves/<host>/<move id>/` in the target bucket:
2489
2490	| subprefix | content | writer |
2491	|---|---|---|
2492	| `replica/` | the mirrored litestream replica; the only subtree `MirrorPrefix` touches | source rounds |
2493	| `files/` | sealed archive and manifest | source |
2494	| `timers/` | the timers snapshot | source |
2495	| `move.json` (outside every subtree) | `{"move_id","incarnation","host","from","to"}`, create-only | source, before the first round |
2496
2497	`MirrorPrefix` runs on `replica/` only, so it can never delete an archive,
2498	a snapshot or `move.json`. Landing installs only `replica/` into
2499	`instances/<host>/` (§7.6). Receipts are `move-receipts/<host>/<move id>.json`
2500	in the source bucket.
2501
2502	**The staging-work lease, sealing and draining (joint D4, N2).** M17's
2503	push-only grant stays: the source can put and delete in the target's
2504	`moves/*` but cannot read it, so it cannot hold the target's `lock.json`.
2505	Exclusion between staging writers uses the claim's shared staging-work
2506	lease in the deployment bucket, keyed by target region and host (claim C3).
2507	Every round, the final round and every staging retirement take it first,
2508	then revalidate the claim's op id and phase. That is enough for two workers
2509	of one operation (a restarted agent beside a stalled one), but a lease
2510	cannot fence a request already signed, so staging safety rests on two
2511	further rules:
2512
2513	- **Seal by version.** Each PUT's response carries the new object's
2514	`VersionId`. The final round records the exact versions of
2515	`replica/…`, `files/…` and `timers/…` in the claim's op journal: the
2516	**seal**. Landing copies those versions by `versionId` and nothing else.
2517	A stale round that lands later creates a newer version, which the seal
2518	does not name, or a delete marker, which a copy by `versionId` ignores.
2519	So nothing has to be drained for correctness.
2520	- **Sign only before `SafeUntil`, and sign at the check (model 14,
2521	model 18).** A staging writer checks its lease's `SafeUntil` immediately
2522	before it signs each request, after any pause, and drops the request if
2523	the time has passed. Revalidating at the start of the round is not
2524	enough: a goroutine that revalidated and then paused can sign long after
2525	its lease ended. **The signature is computed at that check**, with the
2526	check's time as its `X-Amz-Date`, and never recomputed, including by the
2527	SDK's automatic retry, which must resend the original signature (claim
2528	rev 5, CC19): a pause between
2529	the check and the send, even a whole-VM freeze that no in-process bound
2530	can promise against, then ends in S3 refusing the request once its
2531	signature is older than the signature-age limit (403
2532	`RequestTimeTooSkewed`, verified, §15 step 8). `SafeUntil` therefore
2533	leaves room for the signature's whole valid life: `SafeUntil = Until −
2534	clock skew − 15 min`. Rev 5's rule signed at send time; the stricter
2535	model freezes a box between a passed check and the send, and the write
2536	lands after the staging cleanup (1 seed in 100,000; CC19, §19.4).
2537	- **Retire staging after its writers' horizon.** Staging is retired (by
2538	the target-region box, §7.11) only after `seal time + staging-lease TTL +
2539	H`, when no writer that held the lease can still have a request in
2540	flight. That bound holds only because of the rule above: a request is
2541	signed at a check made before `SafeUntil − 15 min`, and S3 accepts it
2542	only within 15 minutes of that, so it is accepted before `Until` and
2543	completes within `H` of acceptance, or it is a straggler that completes
2544	later, which only the straggler sweep can retire (§6.4).
2545
2546	All three are proven by the model (§14.2.5). A staging round's goroutine
2547	can pause between revalidation and signing (one round in three), past its
2548	lease; a cut round's lost-response retry can leave a paused duplicate
2549	(one in three). Dropping the seal by version loses acknowledged writes:
2550	the install copies a stale round's older snapshot. Dropping the staging
2551	horizon or the `SafeUntil` check leaves staging in the serving region or
2552	in a region the instance left.
2553
2554	**Where correctness rests on the pause assumption (model 14).** Claim rev
2555	3 keeps its clock and pause assumption "only for liveness", because every
2556	destructive request is version-bound. A staging PUT is not destructive,
2557	but its residency is: the staging horizon is a bound on signing time, and
2558	the only thing that enforces it is the `SafeUntil` check, whose margin
2559	must cover the clock skew and the longest pause between check and
2560	signature. The worst case is garbage under `moves/<host>/<move id>/`
2561	(never live data, because the seal names versions), but in a region the
2562	instance left that is a residency failure. CC14 asks the claim spec to
2563	say so (§19.4).
2564
2565	**Snapshot rounds (source).** Each round the source builds the files
2566	archive (§8) when the plaintext digest changes, and publishes its **launch
2567	report** `moves/<acct>/<app>/<host>/<move id>/source.json`: every variable
2568	of the **composed** launch environment its next spawn would get, which is
2569	`childEnv` (`backend_exec.go:1158-1196`) over `instanceEnv`
2570	(`:1135-1153`) plus the agent-owned variables (`:975-993`), including the
2571	non-`CARLOS_*` variables `childEnv` inherits from the agent (codex R2-8).
2572	Each value is reported as an HMAC-SHA256 under a key derived (HKDF) from
2573	`CARLOS_SECRETS_KEY`, so the report reveals names and equality only.
2574
2575	**Readiness report (target).** For every record whose `move.to` is its
2576	placement, the target writes `moves/<acct>/<app>/<host>/<move id>/target.json`:
2577
2578	| check | passes when |
2579	|---|---|
2580	| T1 protocol | this box is at or above the protocol floor (§11) (codex 7) |
2581	| T2 secrets key | this box publishes `secrets_key_fp` equal to the console's (§10) |
2582	| 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) |
2583	| 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>` |
2584	| T5 archive | the newest archive opens with this box's key, matches its manifest, has no special file, and is under the cap |
2585	| T6 disk | free space (`readDiskFrac`, `internal/host/probes.go:209`) covers twice the replica, plus the archive, plus 2 GiB, and stays under 85% |
2586	| 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 |
2587	| T8 one owner | exactly one hosting box publishes the target placement |
2588	| 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) |
2589	| T10 return lane | this box can put and delete `moves/_lane/<move id>` in the source's bucket (M17) |
2590	| 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 |
2591	| 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 |
2592	| 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) |
2593
2594	**Source readiness.** S1: a probe request (§7.7) to the readiness path on
2595	the instance as it runs today answers 200 to 399 from its own process
2596	(codex 14); an app that fails is refused with "declare `moves.ready_path`".
2597	S2: its next spawn is strict (§5.3). **S1 is load-bearing (model 3):** a
2598	source box that cannot run the instance now (in the model, one without
2599	`CARLOS_SECRETS_KEY`, finding 2b's state) can be cut, and its pre-flip
2600	recovery then never passes its probe. The model drops S1 and finds moves
2601	stuck in `reverting`.
2602
2603	`ready` requires a round at most the 16 MiB bar, a passing target report
2604	and source readiness, each under 10 minutes old.
2605
2606	### 7.4 The cut, journaled (codex 4, R2-8, R2-10)
2607
2608	Each phase is written to `cut_phase` before its side effects.
2609
2610	| phase | entered by | action | failure and recovery |
2611	|---|---|---|---|
2612	| `requested` | cut door or the source (auto-cut), CAS `ready` → `cutting` | none | |
2613	| `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 |
2614	| `stopping` | source | row `moving`, `hold_op = move id`; `ReconstructStopEvidence` (§5.3) | its budget, then `reverting` |
2615	| `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) | |
2616	| `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` |
2617	| `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` |
2618	| `flipped` | source, the flip CAS | `region = to`, `state = landing`, `landing_deadline`; and the claim: `op.kind = landing`, execution holder = target (§19 K4) | |
2619
2620	**One absolute deadline, equal to the promise (joint N15, J2-N15).** The
2621	M2 promise is the window from the source's stop to the target's open.
2622	Admission writes `cut_deadline = cut_at + cut_budget − open_budget` into
2623	the move journal. Every phase before the commit checks it, on the source
2624	and on the target alike, and **the commit is a record CAS conditional on
2625	`now ≤ cut_deadline`** (§7.9): that CAS is the decision, and the claim
2626	follows it unconditionally, so the deadline cannot be passed between the
2627	two writes. After the commit the target is authoritative and its open is a
2628	local conditional update on its own box, bounded by `open_budget`; an open
2629	that overruns it is reported against the promise, but nothing is rolled
2630	back after a commit. Exceeding the deadline before the commit starts
2631	recovery: `reverting` before the flip, a rollback after it. Rev 5 bounded
2632	the commit and called that the promise; the promise was stop to open
2633	(J2-N15). The recovery's own deadlines (`reverting` 15 min, the release
2634	deadline 15 min) are separate from the promised window (codex R2-10).
2635	Rev 3 checked the deadline only while probing; the model found commits far
2636	past the budget after slow installs, and finds them again when the deadline
2637	is dropped. The source does not purge its
2638	database or files at the cut; finalization parks them (§7.9).
2639
2640	**`reverting` (pre-flip recovery, codex 4, joint N11).** The record still
2641	names the source. The source CASes the claim to `op.kind = reverting` with
2642	itself as execution holder, holds the row as `restoring` with
2643	`hold_op = move id`, and runs a **journaled** recovery,
2644	`op.journal.rev_phase`:
2645
2646	| phase | action | replay |
2647	|---|---|---|
2648	| `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 |
2649	| `verify` | entered from `stopped`, `staged` or `archived`: check files and timers against the digests recorded at `stopped` | replayable **until `probing` is journaled** |
2650	| `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) |
2651	| `probed` | conditional open on `hold_op = move id` | replayable |
2652	| `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) | |
2653
2654	Rev 3 compared digests again on re-entry, so a crash after the recovery
2655	probe had written left the move stuck on a "mismatch" that was really the
2656	app's own work (joint N11). The model reproduces that when it drops the
2657	journal. Fifteen minutes of failed probes: `stuck`, held.
2658
2659	**Source digests at `stopped`.** The source records `files.plain` (§8.3) and
2660	`timers_sha256` at `stopped`, before any phase that can fail, so every
2661	recovery has a baseline.
2662
2663	### 7.5 The flip, and how the claim follows the record (J2: record/claim ordering)
2664
2665	**Every move transition is one record CAS, and the claim follows it.**
2666	The record carries the move's journal, so the record CAS is the decision:
2667	the flip (`archived` → `flipped`), the commit (`probed` → `committed`,
2668	§7.9) and a rollback (`landing` → `rolling_back`, §7.8) are each one CAS on
2669	the record, guarded by move id and incarnation. The commit and a rollback
2670	CAS the same field, so exactly one wins. The claim half is a second CAS
2671	that the record fully determines: the op id, the claim's prior kind and
2672	phase, and its new kind, phase and execution holder:
2673
2674	| record transition | claim CAS that follows | execution holder |
2675	|---|---|---|
2676	| `flipped` | `moving`/`sealed` → `landing`, `landing_phase = checking` | `none` → target, citing the source's evidence (`stopped-source.json`) |
2677	| `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) |
2678	| `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) |
2679
2680	**Any actor that reads both objects and sees the record ahead writes the
2681	claim half**: the actor that wrote the record, on its next step; the other
2682	participant; or the console's recovery pass (claim C2's recovery owner for
2683	this state). The CAS is conditional on the op id and the prior claim
2684	state, so two actors racing to write it cannot both succeed, and neither
2685	can write anything the record did not decide. Until it lands, the claim
2686	still names the previous state: after the flip nobody holds the execution
2687	right (the source gave it up at `stopped`, K3); after the commit the target
2688	is not yet admitted to serve; after a rollback decision the target is still
2689	the executor and must still give evidence. Each is safe.
2690
2691	This replaces rev 5's wording, in which §7.5 had the source complete the
2692	handoff while K4 reserved it to the receiving participant (J2-D7). K4 now
2693	says the execution holder changes only in the claim CAS that mirrors a
2694	record transition, citing the evidence that transition names (§19 K4).
2695
2696	The model writes the record half and the claim half as separate steps,
2697	with crashes, console loss and the recovery pass between them (§14.2.2).
2698
2699	The source row stays held (`moving`); reconcile keeps it because the claim
2700	names this box as a participant (§9.6).
2701
2702	**The close is record first too (rev 7.23, Paul's ruling M4).** The
2703	actor that closes first checks that no obligation this op created
2704	remains, then CASes the record: `move` is cleared and `last_move` names
2705	the move and its outcome (`done`, `rolled_back` or `aborted`). The claim's
2706	release to `serving` (§19 K8) is the second CAS, determined by
2707	`last_move`: the op id, its kind and phase, and the executor the outcome
2708	names. Until it lands, the claim still holds the op, so nothing else
2709	starts on the host. After a crash between the two, no box revisits the
2710	host (the box passes are driven by records with a live move), and the
2711	console's recovery pass writes the release from `last_move`. Rev 7.22
2712	had this the other way round, claim first; claim Plan 10's recovery
2713	grant can act only while the claim holds the move op, so a claim
2714	released over a live `move` could never be finished by it.
2715
2716	**Late record writes.** Every move write to the record is a conditional
2717	CAS. One that completes after its client gave up either still matches,
2718	and repeats a decision already taken, or fails on the ETag.
2719
2720	### 7.6 Landing and install (codex 5, 13, R2-6)
2721
2722	The target's reconcile mints the row held as `landing` with
2723	`hold_op = move id` (§9.6). The target's worker runs these phases. Each is
2724	written to `landing_phase` before its side effects, and its local work is
2725	journaled in `<DataDir>/.moves/<host>/<move id>/` (F12).
2726
2727	| phase | action | done when | replay |
2728	|---|---|---|---|
2729	| `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 |
2730	| `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) |
2731	| `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 |
2732	| `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 |
2733	| `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) |
2734	| `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) |
2735	| `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 |
2736	| `probing` | the probe (§7.7) | | **never replays an earlier phase** (INV-7); a crash restarts only the probe |
2737	| `probed` | probe passed | | |
2738
2739	Any failure from `checking` to `probing`, or `landing_deadline`, triggers a
2740	rollback (§7.8).
2741
2742	**One install routine, two sources (region HA L16; rev 7.19).**
2743	`building` and `published` are one routine shared with region HA's
2744	relocation (spec 1 §5.8): its input is a **pinned set of remote
2745	versions** (key, version id, level, TXID range) plus the required final
2746	TXID, and its output is the prepared generation's snapshot, anchor, build
2747	intent and completed install manifest exactly as above. A move feeds it
2748	the seal's `replica/` versions and `N`; a relocation feeds it the
2749	versions `genselect.SelectPrepared` or the generation's current listing
2750	pins and that listing's maximum TXID. The anchor rule, the two durable
2751	states, the replay rule and the marker rule are the routine's, so both
2752	callers get them once. **Every installation writes a files manifest in
2753	its new generation** (L17, §8.3; claim rev 6.28 C3, §6.2a, P6-D3; rev
2754	7.21 after R18-1): the first manifest is **not** the session-bound
2755	publisher's, because no target writer session exists until `probing`
2756	(claim C3 binds that publisher to an admitted `{location, generation,
2757	session}`). It is the **prepared manifest**, as claim rev 6.30 (73b1b9dc) states the
2758	rule and region HA spec 1 §5.8's remote build (`:809`) uses it:
2759	**before any session exists, `op.exec` may publish an installation's
2760	initial files state in a phase that permits installation**: a move's
2761	`local`, a relocation's `installing`, or region HA's prepared build. That
2762	state is **create-only content objects plus one create-only prepared
2763	manifest**: in `local`, after the archive is extracted and verified, the
2764	target writes the installed files, `<host>.env` and the wake state (the
2765	timers snapshot, `NextDue`, `Replication`) as region HA §5.6's immutable
2766	objects under `<location>files/<P>/objects/` and then the one
2767	manifest `<location>files/<P>/manifest.json`, **bound to
2768	`{location, P, op id, installation stamp}`** where **`P` is the
2769	installation's prepared destination generation, never
2770	`holder.generation`** (rev 7.22, R19-1): `g-<move id>` for a forward
2771	landing, the prepared return generation `g-<rollback id>` for a dirty
2772	rollback (§7.12), the same name the install manifest and the generation
2773	prefix of §5.1 use. `holder.generation` still names the source's
2774	pre-move generation `S` until the probe's cold admission moves it
2775	(§7.14, §9.4) and is **not** changed by `local`; a manifest bound to or
2776	filed under `S` could never be `P`'s baseline, so the first landing
2777	admission would block (claim rev 6.30 requires the prepared generation).
2778	The binding's other members are the move id (or rollback id), the holder
2779	location and the flip's stamp. The manifest is published **naming exact
2780	versions, with sequence 0, never replaced, and retired with its
2781	generation**; it is journalled in the op journal like the install
2782	manifest, before `.files-gen` is written, and a replay reuses the objects
2783	it finds by digest and the manifest by key (create-only, so a late second
2784	write fails). The **session-bound publisher starts only after the first
2785	admission** (the probe's, §7.14): it **takes that manifest by exact
2786	version as its baseline and publishes from sequence 1**; until then
2787	nothing but the install writes under `files/<generation>/`. Manifest entries carry **origin-qualified
2788	references** (claim P6-D3): an object is named by its own incarnation
2789	location and region, so copying a manifest into a new generation never
2790	reinterprets its references, and a cross-region landing's prepared
2791	manifest names destination-local objects it materialized and verified
2792	from the sealed archive. **Files reachability is
2793	independent of the database baseline:** a cold admission establishes its
2794	files manifest from the newest valid manifest in the admitted predecessor
2795	chain, read by exact version, before the app starts; missing or malformed
2796	manifest data is never an empty-files bootstrap. The archive at the cut
2797	stays as the sealed transfer and the rollback's evidence.
2798
2799	### 7.7 The probe (codex 14)
2800
2801	`ProbeWake(host, op)`, legal only on a row held with `hold_op = op` and
2802	only while the claim names this box as execution holder:
2803
2804	- **first, render held config and materialize the release** (`RenderHeld`,
2805	`MaterializeHeld`, §9.1, §9.2), for every kind of probe: the landing, the
2806	source's pre-flip and rollback recoveries, and a push (model 4). Config
2807	sync and adoption skip held rows, so an instance created shortly before
2808	the operation began may never have been rendered. In the model, pushes
2809	and reverts of such an instance never pass their probe until this rule is
2810	applied to every probe;
2811	- **check the actual launch environment at spawn** (joint N8): recompose it
2812	exactly as the spawn will, including inherited agent variables after any
2813	restart. **The landing probe** requires the input versions pinned at
2814	admission (`move.inputs`) and the executable. **A recovery probe** (the
2815	source's pre-flip revert and its rollback recovery, §7.4, §7.8) requires
2816	the inputs it rendered itself, now, and records them in the journal
2817	(`recovery.inputs`); it is not bound to `move.inputs` (J2-R2-5). Rev 5
2818	bound every probe to the pinned inputs: a bundle published after
2819	admission rolled the landing back and then failed every recovery probe
2820	forever, because recovery renders the current bundle. The pin exists so
2821	the target runs what the source ran (T3); on the source itself, the
2822	current bundle is what it would run had there been no move. A bundle
2823	that is itself broken fails the recovery probe as it would fail any
2824	wake: `stuck`, held, and paged;
2825	- a strict spawn (§5.3), with `CARLOS_MOVE_PROBE=1` (advisory);
2826	- the answer must come from the spawned tree: the socket peer's
2827	credentials (`SO_PEERCRED`) name a process in the host's cgroup;
2828	- the readiness path (`moves.ready_path` from the instances manifest, `/`
2829	otherwise) answers 200 to 399 within 30 s (`backend_exec.go:36`);
2830	- a 20 s settle, the process still running, and a second request;
2831	- up to three attempts for a landing, and never more than T11 admitted
2832	for this budget (§7.3, R3-7); a recovery probe (a revert's or a
2833	rollback's source) has **nine** before `stuck` (§7.8, §7.10; R12-5).
2834	**One attempt is one cold admission** (§7.14): its app may be
2835	restarted under the retry policy of §5.1 step 9 within the attempt's
2836	**30 s readiness window**, which runs from the first start (the waits
2837	total 15 s, each start's own time is on top), and the fifth failure or
2838	the window's end, whichever comes first, ends the attempt; the next
2839	attempt, if the budget allows one, is a new cold admission into a
2840	fresh generation restored from the dead attempt's. **The deadline is
2841	checked before each start and before readiness is accepted** (R12-2):
2842	an attempt whose window passed while the agent was paused, or between
2843	a failed start and its retry, does not start the app at all (rev 7.12
2844	checked only while the environment was unready or after a failed
2845	start, so a successful start after the window made an expired attempt
2846	the probed writer); an app that answers readiness at or after the
2847	deadline is stopped and the attempt fails; and the probe's acceptance
2848	checks the attempt it accepts answered within its window (INV-19). At
2849	the boundary, readiness k steps after the attempt's first start: k =
2850	29 is accepted, k = 30 fails before the start, k = 31 fails at the
2851	deadline with the environment still unready (`TestProbeWindow`). A
2852	probe never marks the host failed; the operation's rollback (or
2853	`stuck`) is its outcome. The budget's attempts and the policy's five
2854	restarts are different things: at most three (or nine) admissions,
2855	each with at most five starts inside 30 s. The absolute `cut_deadline`
2856	(§7.4) still bounds the whole.
2857
2858	The probe's activator entry is **held**: `RetireExcept`
2859	(`internal/edge/edge.go:924`, `activator.go:2624`) keeps it, and the edge
2860	never admits a request to it (codex 13).
2861
2862	### 7.8 Rollback (codex 1, 2, 3, R2-3, R2-4, R2-5)
2863
2864	**Triggers:** a landing failure (the target), or `landing_deadline` (the
2865	source or the console's sweep). Both are a record CAS `landing` →
2866	`rolling_back`, guarded by move id; the commit is a CAS from `probed` on
2867	the same record, so exactly one wins. The CAS sets `region = from`,
2868	`rollback.id`, `reason`, `release_deadline = now + 15 min`, and the claim
2869	moves to `op.kind = restoring` under the same op id, with the execution
2870	holder still the target until its evidence arrives. Both boxes stay
2871	participants, so **reconcile keeps both rows
2872	held** (§9.6, §19 K9): the target row is not retired by the region change
2873	(codex R2-4).
2874
2875	**Target release**, journaled as `rollback.target_phase`:
2876
2877	| phase | action |
2878	|---|---|
2879	| `releasing` | row `releasing` with `hold_op = rollback id`; `ReconstructStopEvidence` |
2880	| `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` |
2881	| `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 |
2882	| `returned` (dirty only) | every artifact published |
2883	| `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 |
2884	| `cleaned` | CAS `rollback.target_parked_at` |
2885
2886	The `cleaning` phase is what leaves no copy of the incarnation in the
2887	target's live namespace, so a later delete and recreate there cannot
2888	restore it (codex R2-5, INV-10). It waits for the source's recovery
2889	because, until then, a source failure might need the target's state again.
2890
2891	**Source recovery**, journaled as `rollback.source_phase` and in
2892	`<DataDir>/.moves/<host>/<rollback id>/` (codex R2-3):
2893
2894	| phase | action | replay |
2895	|---|---|---|
2896	| `waiting` | until `released` (clean) or `returned` (dirty) and the claim's execution holder is `none` | |
2897	| `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` | |
2898	| `restoring` | row `restoring`, `hold_op = rollback id` | replayable |
2899	| 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 |
2900	| 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 |
2901	| `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 |
2902	| `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 | |
2903	| `recovered` | CAS `rollback.recovered_at` | |
2904	| `opened` | the conditional open on `hold_op = rollback id`; CAS `rollback.opened_at` | |
2905
2906	**Obligations.** The target's `released` CAS also adds to the claim, in the
2907	same write, a `park-superseded` obligation for the target box and region
2908	(its replica, staging and local state; destination
2909	`superseded/<move id>/<host>/`), which its `cleaning` phase discharges,
2910	and in the same write runs `CoverRegionPredecessors` for the target
2911	region (claim rev 6.14 item 6, R12-3): every record whose predecessor's
2912	objects are the target's (a restarted probe's record names the dead
2913	probe's generation there) is covered, with no chore, since the park
2914	retires the whole location. The console's release of a declared-lost
2915	target (§7.10) queues the same park and covers the same way. The
2916	source's return admission comes after this CAS, so its record, whose
2917	predecessor is the target's writer, is **born covered** under the park
2918	the claim already holds (§5.1 step 9). A
2919	dirty source recovery adds one for its own region and box for what its
2920	install supersedes. These are the claim spec's durable chores (§2 there);
2921	§19.3 asks for the kind.
2922
2923	**Finalization:** when `recovered_at`, `opened_at` and `target_parked_at`
2924	are all stamped, and no obligation this op created remains, whichever
2925	actor stamps last writes the terminal log event (`rolled_back`, with every
2926	timing, digest and reason), CAS-clears `move`, and then releases the
2927	claim to `serving` (§19 K8; record first, §7.5). Until then `move` and
2928	the claim stay, so nothing else can start on the host (codex 6). The source serves from `opened` on; the
2929	held claim blocks only other operations.
2930
2931	Nine failed recovery probe attempts (three times the landing's budget of
2932	three; `probeTries*3` in the model): `stuck`, held (§7.10). Rev 7.12's
2933	sentence here said three, against its own model description (R12-5).
2934
2935	**Waiting.** If `release_deadline` passes with no target evidence, the move
2936	stays in `rolling_back` ("waiting for uk to release"), paged, safe: nothing
2937	runs anywhere. It converges when the target returns (INV-3).
2938
2939	### 7.9 Commit and finalization (codex 6)
2940
2941	1. **Commit** (target): record CAS `probed` → `committed`, conditional on
2942	`now ≤ cut_deadline` (§7.4). The commit is also refused once a rollback
2943	reason is recorded, and it is bounded by the earlier of `cut_deadline`
2944	and `landing_deadline` (§7.8 makes the second a rollback trigger; Plan 2
2945	ruling P2-deadline). Then the claim follows (§7.5): phase
2946	`committed`, plus the obligations in the same claim write,
2947	`park-superseded` for the source's location in its region and box,
2948	and `park-staging` for the target's staging (§19.3).
2949	**`holder.generation` is not written** (R10-3): it is whatever the
2950	latest admission chose, the prepared generation `g-<move id>/` when
2951	the first probe passed, a fresh generation restored from it when a
2952	probe was restarted (§7.14). Rev 7.9's commit wrote `move id` here;
2953	after a restarted probe that had acknowledged writes into its fresh
2954	generation, that put the obsolete prepared generation back into
2955	authority and the next restore lost them.
2956	2. **Open** (target): conditional open on `hold_op = move id`; CAS
2957	`opened_at`. From here the target serves on the session its probe was
2958	admitted with; the claim's `landing` op with phase `committed` admits
2959	its later wakes as `AdmitWriter`s like serving's (§19 K6, §7.14).
2960	3. **Source park** (source, holding the lease on its own
2961	`instances/<host>/`, claim spec C3): bucket-park its `instances/<host>/` into
2962	`superseded/<move id>/<host>/`; local-park its database (with
2963	`<dbPath>.gen`), files, `<host>.env`, quarantine and journals; delete its
2964	row (conditional on `hold_op = move id`) and its timers rows; CAS
2965	`source_parked_at` and remove its obligation.
2966	4. **Target staging park** (target, holding the lease on its own
2967	`moves/<host>/`): `moves/<host>/<move id>/` into
2968	`superseded/<move id>/<host>/`; remove its obligation.
2969	5. **Close** (when both obligations are gone): terminal log event `done`;
2970	CAS-clear `move` (`last_move` = `done`); then release the claim to
2971	`serving` with the target as execution holder (§19 K8; record first,
2972	§7.5).
2973
2974	### 7.10 Stuck and declare-lost (M16)
2975
2976	**The termination fence is M16's evidence, automatically (region HA
2977	L14, ruled H10; rev 7.19).** Region HA §5.9 defines the termination
2978	fence: a regional worker observes state exactly `terminated` for the
2979	box's instance id, account and region as the roster records them, and
2980	writes the create-only fence record `control/box-fences/<enrollment>.json`;
2981	the claim puts the box on `lost` citing it (claim L2 to L4). For a move
2982	whose **target** is fenced that way, the move takes the fence as the
2983	evidence `--declare-lost` would have supplied, with no operator: the
2984	same legality table below applies (the target owes stop evidence, or
2985	released dirty and has not returned), **under the same before-commit
2986	rule**: before the record's commit CAS the move rolls back clean through
2987	the declared-loss path, with `fenced_at` as every scope's evidence time
2988	and the fence record as `rollback.evidence`; after the record's commit
2989	the target is authoritative and the move is not what recovers the
2990	instance: the move finishes its own close (its remaining steps are parks
2991	run by regional workers), and the instance's recovery is region HA's
2992	relocation, outside this spec. **A source terminated before the flip (rev 7.20; claim rev 6.28 §4;
2993	R18-2; claim rev 6.30).** "Before its flip" means **before the
2994	authoritative record enters `landing` through the flip CAS** (`archived
2995	→ flipped`, which sets `state = landing`, §7.4). That is distinct from,
2996	and earlier than, the final commit CAS (`probed → committed`, §7.9): a
2997	record at `landing` whose claim half is still `moving/sealed` is already
2998	past the flip, and the conversion is refused there as everywhere after
2999	it. The fence converts
3000	the pre-flip `moving` operation to `relocating` in **one CAS**: it records the fence reference (below), sets `op.exec =
3001	"none"`, preserves `holder.stamp` and `holder.generation`, starts
3002	`relocating` at `pinning` in the source's region, and leaves every
3003	obligation untouched; the move's staging lane, `park-replica` scoped
3004	`moves/<host>/<op id>` and owned by the target region, keeps its op id
3005	and stays executable (the conversion queues it when the move had not
3006	yet, as an abort would), and it blocks neither the conversion nor the
3007	relocation's release. Readiness, evidence and recovery bind to the
3008	replacement box `choose()` names when the relocation leaves `pinning`.
3009	After the flip (the record's `landing` state) the conversion is
3010	**refused** and this section's rules for a lost target apply. **In a
3011	one-box region** the converted operation has no eligible target: it sits
3012	at `pinning` with exec `"none"` and the lane's park still owed until
3013	region HA enrolls a replacement box (automatic ASG enrollment, H16 and
3014	H17). That state is safe, since no writer exists and the data is pinned
3015	in the source region's bucket, but the host is **not recovered until a
3016	box exists**. The operator sees it as `relocating / pinning: waiting for
3017	a box in <region>` in `carlos move status` and the fleet view, and one
3018	incident alert is raised when the conversion finds no live box in the
3019	region (§13); the alert is not repeated. The operator's `--declare-lost`
3020	stays for the stopped, unclear and vanished boxes the fence does not
3021	cover (claim D2).
3022
3023	**The fence reference (rev 7.20; moves C7, claim rev 6.28 §7.3).** Every
3024	transition that relies on a termination fence writes
3025	`op.journal["fence.<box>"] = {"enrollment", "key", "sha256"}`: the box's
3026	enrollment, the key `control/box-fences/<enrollment>.json`, and the
3027	SHA-256 of the exact bytes the transition verified. A `loss.<id>` intent
3028	written by the same transition cites the same reference. `ReturnToSource`
3029	and every other consumer accept a fence only through that reference,
3030	re-reading the record at `key`, requiring its digest to equal `sha256`
3031	and its enrollment and cloud identity to match the roster's; the key is
3032	never reused for another box or enrollment within the operation. An
3033	automatic declaration from a fence needs no quarantine revision and no
3034	operator (L4); the terminated enrollment is permanently ineligible.
3035
3036	**What a declared-lost box leaves behind (rev 7.11).** Its acknowledged
3037	writes beyond its uploads are declared by the next admission's
3038	`writes_lost` (the record's `remote_max_txid` names where an operator
3039	finds them in the seal or the box's generation); its **registered
3040	timers** are declared by the console's declare-lost record itself and
3041	alerted, since no return lane will carry them; neither is ever exempted
3042	silently (R10-6). When the target of a rollback is the lost box and the
3043	seal was the one holder of the **source's** writes beyond its own
3044	replica (`src_covered` false, §7.4, §7.8), the return is clean for want
3045	of a target and the source's re-admission from its own generation
3046	declares its **cut session** as well, a second `writes_lost` record
3047	(`{box: source, generation: source's, session: the cut's,
3048	remote_max_txid}`) with its alert: the seal in the lost target's region
3049	is unreadable from the source and no lane brings it.
3050
3051	- **`stuck`:** the source's recovery probe failed. Held. `carlos move
3052	resolve --host <h> --retry` reruns the recovery's `probing` phase.
3053	- **`--declare-lost <box>` (M16)**, operator-only. `carlos move resolve
3054	--host <h> --declare-lost <box>` is the move-facing form of the claim
3055	spec's `carlos ops host resolve <host> --declare-lost <box>` (§7.2
3056	there). The joint review's D6 text governs it (joint D6, N3):
3057
3058	> A claim CAS is bookkeeping, not fencing. The resolve command must
3059	> establish verified compute fencing, or an independently enforced
3060	> execution-lease expiry, before reopening the source. Recover validated
3061	> durable target data where available, not only an already-published
3062	> return. Retain M16's precommit restriction, exact-participant check,
3063	> source refusal and explicit loss confirmation.
3064
3065	**This spec takes the first branch only: compute fencing (model 5).** The
3066	verb requires the operator's cloud credentials to show the box `stopped`
3067	or `terminated`, verified through the cloud API by the CLI. An expired
3068	execution lease is not enough, even with the self-fencing watchdog: a
3069	whole-VM pause stops the watchdog with everything else, and on resume the
3070	application can write before the watchdog fires. The model allows the
3071	lease-expiry branch and finds two writers when a frozen target resumes
3072	beside the recovered source (1 seed in 30,000; 2 when the watchdog also
3073	runs inside the agent, so an agent pause defeats it too). The lease stays useful for liveness: a
3074	partitioned or hung participant fences itself.
3075
3076	It is legal in exactly these states, and refused otherwise:
3077	- **the target owes stop evidence** (landing, or a rollback before the
3078	target released): it proceeds as a clean rollback, after a
3079	confirmation naming the box, the flip time, and that the target's
3080	writes since then are lost (M-C18);
3081	- **the target released dirty but had not returned its writes** (model
3082	6): the same, and the confirmation says so. Rev 3 missed this state;
3083	the model finds a move waiting forever on a return that a destroyed box
3084	can never send. **The same CAS adds a `park-staging` obligation for the
3085	return lane, `moves/<host>/<rollback id>/` in the source's region,
3086	owned by the source region's box, not before the lane's staging
3087	horizon** (model 27): the lost target may have published part of its
3088	return, and the rollback now finishes as a clean one, which parks
3089	nothing else there;
3090	- **a destroyed box owes only local chores** (`park-local`): the
3091	obligation is removed and nothing else changes. This one is legal
3092	after commit, because no data authority is involved (model 6);
3093	- refused after `committed` in the first two states, refused for the
3094	source, refused for any box that is not that exact participant.
3095	"After `committed`" means after the **record's** commit CAS, whether or
3096	not the claim has followed it yet (§7.5). Before the commit the verb's
3097	rollback is the same record CAS as any other rollback, so it cannot
3098	race a commit.
3099
3100	The box goes on `lost`. **A returning box is quarantined** (claim §7.2):
3101	before anything else it retires every local artifact for the host under
3102	the host guard, and only then can an operator `--readmit` it. The model
3103	starts stopped boxes again after they were declared lost; without the
3104	quarantine they would keep stale local state for the host.
3105
3106	### 7.11 Abort
3107
3108	Legal in `preparing`, `ready`, and `cutting` with `cut_phase = requested`
3109	(CAS). A move whose readiness never comes aborts itself after a bound, so
3110	an unreachable target never needs a human.
3111
3112	**Who retires what (joint N13).** The source cannot read the target's
3113	`moves/*` and cannot write the target's `superseded/` (M17 grants it Put,
3114	Delete and prefix-scoped List on `moves/*` only), so it cannot park target
3115	staging. Abort therefore adds a `park-staging` obligation **owned by the
3116	target region's box**, not before the staging horizon of §7.3. The source
3117	parks its own snapshots. (Plan 5 note, ruling K19: "parks" here means the
3118	source retires them from its own bucket, every version of
3119	`move-snapshots/<host>/<op>/` through `DeleteVersion`; that prefix is outside
3120	the park scope grammar, and F3's retention of snapshots covers completed
3121	moves only.) The claim stays `moving` until every obligation
3122	has acknowledged; then the record clears (`last_move` = `aborted`) and
3123	the claim releases to `serving` (record first, §7.5). The model gives the source
3124	the target's park and records an IAM violation on every abort.
3125
3126	### 7.12 Deletes and parks under the claim
3127
3128	- **Delete during a move is refused** (409): the delete doors and
3129	`PurgeApp` CAS the claim from `serving` to `deleting` (claim spec §5), so
3130	they cannot start while a move op holds it (§19 K7). A purge of an app
3131	with a moving instance waits. An operator who must delete aborts first,
3132	or waits for the commit or rollback to finish.
3133	- **App purge (joint N9, model 7, 8).** Claim §5.3 reserves the app first,
3134	then claims every host, then tears down stores. The model found two more
3135	rules it needs. **Purge adopts first:** a legacy host of the app with a
3136	record but no claim yet is invisible to a purge that looks only at
3137	claims, so the purge tore down a store under a serving instance; purge
3138	must run the one adoption routine (claim §9) for every unclaimed record of
3139	the app before deciding. **The reservation is the purge's journal:** the
3140	console's recovery pass finished a stalled purge's delete and freed the
3141	host, `free` dropped the reservation, a create for the same app went
3142	through, and the stalled purge then tore down the new incarnation's
3143	store. The reservation records the purge's phase; recovery drives those
3144	phases in order; only the purge's own completion removes it, never
3145	`free`. **The purge fence (claim rev 5.1, CC21):** a creating console
3146	can renew its registration, pause, and resume after purge's drain has
3147	removed that registration as expired. S3 cannot make the creator's claim
3148	write conditional on the registration object, so before purge removes
3149	a registration whose host claim does not name the create, it CASes that
3150	host's claim from free or absent to `{op: {kind: purging, id}}` with no
3151	holder, and releases it at `done` by writing a free claim. The
3152	creator's CAS from free or absent then fails. The model found the fence
3153	needs one more condition, and claim rev 5.2 adopted it (CC22, §19.4):
3154	the creator's CAS is If-Match the claim ETag it read when it
3155	registered, or If-None-Match: * if the claim was absent then; a 412
3156	restarts the create from step 0, with a new registration; and a claim
3157	object is never deleted (C5a there), because deleting a released fence
3158	would let the paused creator's If-None-Match: * succeed. The creator's
3159	re-read of its registration just before the CAS stays, as a cheap
3160	extra; the model shows it is not sufficient alone (§14.2.5).
3161	- **Recreate during a move** cannot happen: create requires the claim free
3162	or absent (claim spec C2).
3163	- **A delete after a move** parks every region in `touched.regions`
3164	(claim spec §5). The move added each region and box to `touched` before
3165	writing there, so nothing it left is missed, and what it superseded is
3166	already out of the live namespace (§7.8, §7.9, INV-10). The claim's
3167	delete park copies `moves/<host>/` and `instances/<host>/` as separate
3168	subtrees, which is compatible with per-op staging (§7.3).
3169
3170	### 7.13 Crash at every step
3171
3172	The crashed actor restarts with **no activator memory**; everything it
3173	needs is in the record, the claim, its journals (F12) and the box's actual
3174	process state (§5.3).
3175
3176	| state / phase | source crash | target crash | console crash |
3177	|---|---|---|---|
3178	| preparing, ready | next round | next report | stateless |
3179	| cutting: requested, admitted | resumes the phase | n/a | |
3180	| cutting: stopping | `ReconstructStopEvidence` from cgroup and unit state | n/a | |
3181	| cutting: stopped to archived | resumes; the sealed archive is reused from its create-only key | n/a | |
3182	| flipped, record CAS done, claim CAS not | completes the claim CAS | waits for the claim | |
3183	| reverting | resumes the recovery, held | n/a | |
3184	| landing: checking to restored | holds `moving` | replays the phase per §7.6 | |
3185	| 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 | |
3186	| 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 | |
3187	| 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 | |
3188	| committed, the claim still `landing` | resumes the park | the target's next wake is an `AdmitWriter` within the landing (§7.14) | |
3189	| committed | resumes the park | opens | |
3190	| rolling_back: target phases | | resumes its phase; evidence from actual state | the deadline sweep is a CAS |
3191	| rolling_back: 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) | | |
3192	| stuck | held; operator | | |
3193
3194	### 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)
3195
3196	Every path that opens replication is an `AdmitWriter` (§5.1 step 9), one
3197	claim CAS made **before the app process starts** (claim rev 6.10, R10-1),
3198	by the box the claim names as `op.exec`, and never by another. Two modes
3199	exist, **warm** and **cold**; nothing else (R9-3). **Which box may be admitted in which
3200	phase**, in which mode, into which generation, and the CAS that handed it
3201	`op.exec` first:
3202
3203	| op kind, phase | the box admitted | mode and generation | `op.exec` handed to it by |
3204	|---|---|---|---|
3205	| `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) |
3206	| `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) |
3207	| `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) |
3208	| `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) |
3209	| `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) |
3210	| `landing`, committed, not yet finalized | the target, at every wake | warm or cold as for `serving` | the same flip CAS |
3211	| `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 |
3212	| `restoring`, the target's phases | nobody: the target is stopping and never opens replication again | | |
3213	| `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` | | |
3214
3215	Two writers never overlap because `op.exec` moves only through a CAS that
3216	cites stop evidence or a lost-box fence (§5.3, §7.10), and the admission
3217	CAS requires `op.exec == this box` (rule `exec-writer`) and is bound to
3218	the observed `op.id`, `op.phase` and kind (rule `admit-bind-op`; the
3219	model's general CAS condition on `op.id`, C2, already refuses a closure
3220	whose operation changed, so the binding adds the phase and the kinds).
3221	**`holder.generation` is the only authoritative generation** in every
3222	kind and phase: an operation's prepared generation (`g-<op id>/`, a
3223	rollback's return generation) is built by the operation's install phases
3224	and becomes `holder.generation` at its probe's cold admission, never
3225	before; the flip and the commit move no generation (rev 7.9's commit did).
3226	A clean rollback's **return CAS names the source's generation again**
3227	(`op.journal.src_gen`, recorded at the flip; only with `src_covered`,
3228	§7.8), since the target's probe had moved `holder.generation` to the
3229	target's and the target wrote nothing; the source's probe then restores
3230	from its own region's remote of it, is covered `clean-return`, and
3231	journals the **target's writer** as its predecessor, the last record of
3232	`holder.admissions`, never the holder's reset fields (claim rev 6.12,
3233	R11-4, INV-16).
3234
3235	**The admitted writer's start**, on its box, in this order; it is the
3236	agent's own loop around one claim CAS, not a set of claim transitions,
3237	and a new agent process never resumes it (a new agent is a new session):
3238
3239	| step | action | if it fails |
3240	|---|---|---|
3241	| 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 |
3242	| **`AdmitWriter`** | the CAS of §5.1 step 9, **first**: session, writer_box, the `holder.admissions` record with the last record as its predecessor, its own region and the predecessor's region; cold: generation, stamp unless kept, `writes_lost` 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 |
3243	| purge | delete the local database, with an error-returning purge | the start waits and purges again; the session stands |
3244	| restore | warm: `holder.generation` from this region's remote, to at least the certificate's `max_txid`; 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 `max_txid` is an alert, the remote is incomplete |
3245	| 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) |
3246	| 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 |
3247	| 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 |
3248	| 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 |
3249	| 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 | |
3250
3251	#### Admissions, coverage and retirement (operative, rev 7.14)
3252
3253	This list, with §5.1 step 9 and the two tables above, is the operative
3254	rule set for writer admission (R12-4), mirroring claim rev 6.22 §6.4a's
3255	operative subsection item for item. Where any other passage of this
3256	spec reads differently (the restore contract's older wording in §5.1,
3257	the §7.8 rows as rev 7.11 had them, the authoritative-region table, the
3258	per-revision blocks of §14.2.2, which are history by construction),
3259	this text wins.
3260
3261	1. **The record.** Each admission appends `{session, box, generation,
3262	region, predecessor: {session, box, generation, stamp},
3263	predecessor_region, mode, coverage, covered, writes_lost?}` to
3264	`holder.admissions`. The predecessor is the last record, never the
3265	holder's fields (INV-16); `region` is the admitted box's region, where
3266	its generation's objects are; `predecessor_region` is the last
3267	record's `region`, before any record the writer box's region, `""`
3268	when the generation holds nothing anywhere; a warm admission
3269	continues the same generation in the same region, so its region
3270	equals its predecessor record's (a clean return's first admission is
3271	cold: an old source certificate does not certify the target's
3272	session). Born covered: item 5.
3273	2. **Coverage** `""` | `sealed` | `clean-return`, as §5.1 step 9 states
3274	it: `sealed` for a `from_db` seal of the stopped predecessor,
3275	`clean-return` for a clean rollback with `src_covered`, a target that
3276	gave its evidence and no declared-lost box, speaking for the target's
3277	probe session and the source's cut session only; `""` otherwise, and
3278	without a certificate it records `writes_lost` (behind a lost target, one
3279	record for every session the target was admitted into since the cut,
3280	and a second for the source's cut session when `src_covered` is
3281	false, under its persisted `cut.session`): `writes_lost` (one) plus
3282	`additional_writes_lost` (a list), each `{box, generation, session,
3283	remote_max_txid}`, unique by `(box, session)` across both, one alert
3284	per declaration (R13-3, R14-2; INV-21). The legacy identity `{session
3285	0, generation "" (@root), holder.writer_box}` is valid in both; every
3286	other declaration has a session above 0, and every declaration names
3287	a box, so a predecessor with no writer is not declared (INV-24, claim
3288	rev 6.24, R16-3). A `writes_lost` record
3289	declares the writes of the session it names and no other (INV-18,
3290	R12-1).
3291	3. **The baseline.** A prepared generation from its pinned snapshot in
3292	the admitting box's region, opened once; otherwise the predecessor
3293	generation's remote in this region; in an unfinished run the newest
3294	generation of the run that holds an object **in this region**, else
3295	the marker's, walked as §5.1 step 9 says (R13-1): a covered foreign
3296	link is passed over, a covered local baseline refuses and alerts; the
3297	start restores the selected run generation rooted at `[1, 1]`, the
3298	marker's through `generation.json` (R14-1); an empty generation
3299	outside an unfinished run is refused and alerted.
3300	4. **Stamps.** A cold admission takes a new stamp except under
3301	`KeepStamp` (`holder.stamp > holder.session`); a clean return's CAS may
3302	name the source's generation and stamp again, leaving
3303	`holder.session` alone.
3304	5. **Coverage, completely.** An entry becomes covered in exactly four
3305	ways (R13-2): at birth (a warm entry; an entry admitted while the
3306	claim holds an unscoped `park-replica`, or a park scoped exactly to
3307	`holder.location`, in its predecessor's region, claim rev 6.24); by
3308	publication; by `CoverRegionPredecessors` (item 6); by
3309	`CoverParkedPredecessors` (item 6). **Publication:** after the marker
3310	names the generation, one `PublishGeneration(observedOpID,
3311	observedPhase, observedSession, publishedGeneration, region, newID)`
3312	requires `holder.generation` to be the published generation and an
3313	entry to name it, then walks every entry in order, skipping covered
3314	ones, as §5.1 step 9 states: no objects anywhere, covered, no chore;
3315	live again, left uncovered, no chore; in `region`, one deduplicated
3316	chore, covered; another region, uncovered, no chore, the walk
3317	continues. Every cold admission publishes. Retirement happens only
3318	through it or through item 6.
3319	6. **Parks cover what they retire.** `CoverRegionPredecessors(op, phase,
3320	region)` runs inside the CAS that queues a region's park of the whole
3321	location: the commit's park of the source region, the target's
3322	release and the console's lost-target release for the target region.
3323	It covers every record whose predecessor's objects are that region's
3324	and queues nothing. `CoverParkedPredecessors(op, phase, region,
3325	generations)` runs in the CAS that queues an at-rest `park-sweep` and
3326	in the CAS that acknowledges it, and covers only the records whose
3327	predecessor is among the generations that sweep parks. INV-17 checks
3328	the composition as each whole-location park completes. A
3329	foreign-region predecessor is never queued into its region from
3330	another one.
3331	7. **Starts.** The admitting CAS first; a new agent process stops a
3332	running app, admits a new session and restarts it; failed starts are
3333	the retry policy's, five under one session with a doubling backoff;
3334	the failed-host marking is a **serving wake's** at the fifth failure;
3335	a probe attempt ends at the fifth failure, at its 30 s window, checked
3336	before each start and before readiness is accepted, or at a late
3337	readiness, counts one budgeted try (three for a landing, nine for a
3338	recovery) and never marks the host failed.
3339	8. **Retention and lost boxes.** `holder.admissions` is trimmed
3340	conservatively: covered records from the front only, to eight, never
3341	past an uncovered one; no compaction. A declared-lost box's timers are
3342	declared on the console's record and alerted; adoption sets
3343	`holder.writer_box` to the pre-release writer's box.
3344	9. **Park state** (claim rev 6.23 §2; R13-4, R14-3 to R14-5, R15-1;
3345	§6.4). Every remote chore carries a persisted park scope from its
3346	queuing CAS (a delete's or adoption's park binds one before its first
3347	step), `{location, incarnation, evidence_at, request_limit}` in the
3348	claim's grammar; `evidence_at` is the original evidence or fencing
3349	bound (a staging lane's is its seal bound, the seal plus the lease),
3350	never the cleanup's start; every retry uses it; every acknowledgement,
3351	a staging lane's included, waits a listing later than `evidence_at +
3352	H`, `H` the signature-age limit plus `request_limit`. A park executes
3353	strictly within its scope's namespace (claim rev 6.24 §2, R16-1,
3354	R16-2): the sweep's chores are grouped by location, each with its
3355	archive incarnation; an `instances/…` scope never touches `moves/`
3356	and the legacy `instances/<host>` scope excludes child incarnations;
3357	INV-23 checks membership for every reference a chore archives or
3358	deletes, fresh or replayed from a persisted manifest (R17-1).
3359	A free host's at-rest sweep is a holderless `parking` op with
3360	`intent.park_sweep`, no exec and no holder, which blocks the successor
3361	create until `FreeAfterPark` frees the claim in its last
3362	acknowledgement's CAS; on a serving host sweep chores carry
3363	`session:<holder.session>`.
3364
3365	**History.** The paragraphs that follow and §14.2.2's per-revision
3366	blocks record how these rules were reached; where they differ from the
3367	list, the list governs.
3368
3369	An admitted writer that dies between its CAS and its marker leaves
3370	`holder.generation` naming an **unfinished** generation `generation.json`
3371	does not (R10-2): its journalled predecessor is the live baseline, no
3372	chore retires it and the sweep protects it. The next admission, by this
3373	box or another `op.exec` box, reads the lag through `holder.admissions`
3374	(§5.1 step 9): the marker names the latest admission's predecessor, or
3375	the predecessor of a chain of unfinished admissions, so this is the
3376	normal state and no alert; a `holder.generation` that holds objects (the
3377	first upload landed) has its marker published again, from the
3378	operation's build journal for a prepared generation, and the retire
3379	chores queued; an empty one is skipped and the baseline is the nearest
3380	generation of the chain that holds an object, else the marker's; the new
3381	marker retires them all. An empty `holder.generation` the journal does
3382	not explain is unexplained missing data: the start is refused and the
3383	box alerts. A clean rollback's return leaves the marker naming a
3384	descendant of `holder.generation`; the source publishes the source
3385	generation's marker again from its last version before anything else.
3386	`holder.admissions` lives in the holder, so an admission unfinished at a
3387	release (an abort released over a source admitted a tick earlier) stays
3388	explained through the next operation. A marker that lands after its
3389	writer died, before the writer's `PublishGeneration`, leaves the
3390	predecessor unretired: the next admission's `PublishGeneration` retires
3391	the predecessor of every record not yet covered. A pre-flip round never forces a sync on a session whose start is
3392	unfinished: there is no open replicator, and a forced upload would write
3393	the first upload's key with other bytes.
3394
3395	**Behaviour change against today's activator.** Today `Restore`
3396	materializes the local database from S3 only when it is absent, "a
3397	no-op when the warm-cache copy is still on disk", and `doWake` relies on
3398	that: "when it's still on disk it is the warm cache: on one box, with the
3399	lease held, the local copy can only be what we ourselves checkpointed at
3400	the last sleep" (`internal/activator/activator.go`). Rev 7.10 changes
3401	this: every wake restores, warm or cold. It costs a restore per wake,
3402	one pass over the database from regional S3 at the local rate (§7.3
3403	prices it, and prices the probe's restore per attempt), and it loses the
3404	acknowledged writes a crash left unuploaded, which the warm cache
3405	preserved on a same-box restart; those are declared through
3406	`writes_lost` and an alert. **The loss is normally within the
3407	replication interval** (§7.3, the sync class), the window between syncs;
3408	a failed or stalled upload extends it back to the last upload that
3409	landed, so the bound is the interval in operation and the age of the
3410	last durable upload in a fault (R10-8). Two more changes against today's
3411	activator (rev 7.11): the admitting CAS precedes the app start, so a
3412	start that fails leaves a session and a retry policy behind it rather
3413	than nothing; and an agent that restarts under a running app stops it
3414	and re-admits, where today's activator reattaches to the running unit.
3415	What it buys is one rule with no provenance machinery: a box's database
3416	is always the certified remote's, so a cached, truncated or foreign copy
3417	can never be served (R9-1), and the claim alone decides who writes what.
3418
3419	A cold admission costs the three local passes of an install (§7.3) for
3420	an operation's prepared generation, one full upload for a fresh one,
3421	none for an empty one, and a dead generation to park. It runs after
3422	every crash, OOM kill, lease takeover or lost disk, after a close that
3423	could not certify (a retry, a timeout, a lost response, R9-5), and at the
3424	first wake of a created incarnation or an adopted legacy host, whose
3425	origin generation has no writer yet. It does not run after a certified
3426	close.
3427
3428	**The source that lost its disk** during a revert or a rollback has
3429	nothing to verify against the digest it recorded at the stop: its
3430	recovery skips the digest check and its probe is admitted like any other
3431	writer (rev 7.9, R8-2); a target that never restored a database returns
3432	nothing dirty (rev 7.10: the probe's admission restores it, so a target
3433	whose probe never started has none).
3434
3435	## 8. The archive (codex 19)
3436
3437	### 8.1 Content
3438
3439	A tar of the files directory (F4, without `.files-gen`) and `<host>.env`
3440	(F6), in sorted path order, with owners and times zeroed and modes kept, so
3441	equal content gives equal plaintext. Regular files and directories only; a
3442	symlink, device, FIFO or socket refuses with its name. The 256 MiB cap is
3443	enforced while streaming (M5). Then zstd.
3444
3445	### 8.2 Sealing
3446
3447	For the deployment's config keypair (P-256 ECDH,
3448	`internal/appconfig/crypto.go:44-59`): a fresh 256-bit data key; AES-256-GCM
3449	over 1 MiB chunks, each nonce the chunk index, the last chunk flagged; the
3450	data key sealed with `appconfig.Seal` (`crypto.go:86`, fresh ephemeral key
3451	and nonce); a manifest with the sealed data key, the sealed object's
3452	sha256, the plaintext sha256, the per-file list (path, size, sha256), the op
3453	id and the incarnation. Encryption is randomized and never made
3454	deterministic.
3455
3456	### 8.3 Identity, publication, retention
3457
3458	- **`plain`** (plaintext digest) identifies content; **`sealed`**
3459	(ciphertext digest) identifies one immutable object. Content checks use
3460	`plain`; fetches use `sealed`.
3461	- The `plain` digest of the files directory as stopped is computed at
3462	`stopped` without sealing, so recoveries have a baseline before any
3463	archive exists (§7.4).
3464	- **One sealed object per cut:** written create-only to
3465	`move-snapshots/<host>/<move id>/files-<sealed>.{sealed,json}`, then its
3466	digests recorded in the record, then copied to staging `files/`. A crash
3467	before the record write leaves an unreferenced object; after it, replay
3468	reuses the recorded object (codex 19).
3469	- **Retention:** the source's snapshots stay until F3; staging is parked at
3470	finalization (§7.9, §7.8).
3471	- **The files manifest (region HA L17; rev 7.19).** The archive is the
3472	transfer; durability between moves is region HA §5.6's files publisher:
3473	immutable objects `<location>files/<generation>/objects/<seq>-<sha256>`
3474	and one manifest per generation, replaced with `If-Match`. Every
3475	installation, a landing's and a dirty return's included, publishes its
3476	installed files directory and `<host>.env` as that generation's first
3477	manifest in `local`, before `.files-gen`; the serving writer then keeps
3478	it current per the app's `files_durability`. The classifier treats
3479	`files/<generation>/` as that generation's (claim L13), so a
3480	`park-generation` chore retires it with the generation, except objects
3481	the files live set names.
3482
3483	## 9. Changes to existing code (codex 13, 15)
3484
3485	### 9.1 Config render for a held row
3486
3487	`SyncExec` skips non-`ready` rows (`internal/appconfig/syncexec.go:643-647`)
3488	and writes an ack only when a file changes (`:1159`). New:
3489	`appconfig.RenderHeld(ctx, rt, op)` renders the same file, writes it, and
3490	writes a **move-bound ack** with the op, the file's sha256 and the bundle
3491	etags, changed or not. `SyncExec` keeps skipping held rows, so the two never
3492	race on one file.
3493
3494	### 9.2 Release materialization for a held row
3495
3496	`release.Adoptable` excludes non-`ready` rows
3497	(`internal/release/adopt.go:816-819`). New: `release.MaterializeHeld(rt, op,
3498	version)` stages exactly the pinned release (`move.inputs.release`).
3499
3500	**Amendment, 2026-10-12 (Paul's ruling on T7, Q2.1).** With host claims on,
3501	the stage and the publication are split. T7 (§7.3) stages the pinned
3502	release and verifies it without touching `live/<host>`
3503	(`release.StageHeldVerified`). The landing's `configured` step, and a dirty
3504	return's, publishes it under the claim's `held-release` selection, whose
3505	identity names exactly that version (`release.MaterializeHeldUnder`), and
3506	then reads it back as T7 does with claims off (`release.VerifyHeldLive`).
3507	The held render in the same step runs under a `held-config` selection
3508	(`appconfig.RenderHeldUnderBefore`, which keeps carry (c)'s journal before
3509	the write), and a merge that is not the pinned inputs is the "configuration
3510	changed" rollback before anything is selected or written. With host claims
3511	off, `MaterializeHeld` and `RenderHeld` run as before. The landing still
3512	refuses at `checking` under the claim (`RollbackClaimWired`, ruling G16)
3513	until this box's moves source is registered with the claim.
3514
3515	### 9.3 The activator
3516
3517	- `ProbeWake` (§7.7); `RetireExcept` keeps held entries.
3518	- `ReconstructStopEvidence` (§5.3); strict spawns under a move.
3519	- The start check (§5.1) in `Start`, `Seed` and `ProbeWake`, reading the
3520	claim.
3521	- Restore writes `<dbPath>.gen` and parks a warm file of another generation.
3522	`promoteStagedReplica` and its call (`backend_exec.go:290`) are deleted.
3523
3524	### 9.4 Timers frozen, drained and restored (codex 15, R1-15 partial)
3525
3526	- **Drained:** entering `stopping`, the source waits until the runner has
3527	no delivery in flight for the host (the runner's per-host claim,
3528	`internal/schedule/runner.go:154`) before taking evidence, so a delivery
3529	that started before the hold cannot advance a row after the snapshot.
3530	- **Frozen:** the runner skips, with no bookkeeping, any held row (today a
3531	blocked delivery still advances `attempts`, `runner.go:345-351`), and the
3532	converger neither upserts nor prunes timers for a host whose claim op is
3533	`moving` (`internal/schedule/converge.go:114`, `:223-241`).
3534	- **Replaced exactly:** `Registry.ReplaceTimers(host, rows)` deletes and
3535	inserts in one transaction, preserving `next_at`, `due_at`, `attempts`
3536	and `registration`. `UpsertTimer` resets them on rearm
3537	(`internal/registry/timers.go:46-55`), so it is not used here.
3538	- **The runner's own prune (joint N14).** A second actor deletes timer
3539	rows: the runner's daily sweep (`internal/schedule/runner.go:260`), whose
3540	`PruneTimers` removes aged completed once-timers even for a live host
3541	(`internal/registry/timers.go:183`). It cannot be frozen without stalling
3542	every other host, so the **snapshot is canonical instead**: the timers
3543	digest covers active rows and their bookkeeping, and excludes disposable
3544	history (completed once-timers). Pruning history therefore never changes
3545	the digest a clean recovery compares. The model includes history in the
3546	digest and finds clean rollbacks stuck on a "mismatch" the runner caused;
3547	it lets a held row's refused deliveries advance bookkeeping and finds the
3548	same.
3549	- **Carried timers are acknowledged state.** A once-timer the app
3550	registered is a write the app was told succeeded. The model counts it as
3551	one for INV-2, and finds timers lost when the files marker is written
3552	before the timers are imported (R2-6).
3553	- Declared schedules converge again once the claim returns to `serving`.
3554	- **`relocating` holds (region HA L17; rev 7.19).** The same freezing
3555	and draining apply to a row held by region HA's `relocating` op: the
3556	runner skips the held row with no bookkeeping, the converger neither
3557	upserts nor prunes the host's timers while the claim op is
3558	`relocating`, and the relocation's release flush carries the timers
3559	snapshot as §7.4 `stopped` does.
3560
3561	### 9.5 Edge
3562
3563	None in Phase 1. Platform-domain hosts get the 503 pending page during the
3564	window (#174, `internal/edge/pending.go`); custom domains get 404 until F1.
3565
3566	### 9.6 Reconcile (codex R2-4)
3567
3568	- **Mint:** while the claim holds a move operation, a participant box mints the
3569	host's row held (`landing` on the target after the flip, `restoring` on
3570	the source during recovery), never `ready`.
3571	- **Removal:** never removes a row of a host whose claim names this box as a
3572	participant, whatever the record's region (`reconcile.go:1114-1159`;
3573	claim spec §8, "rows that a running operation lists as participants are
3574	retained"). The move worker deletes it at its own finalization step.
3575	- **Orphan retirement** (claim spec §8, a row whose incarnation is not the
3576	claim's holder) does not act on a participant row of a move op; a move
3577	never changes the holder, so the case cannot arise for a live move, and
3578	the guard makes that explicit (§19 K9).
3579
3580	## 10. The secrets key and the shared fingerprint
3581
3582	The platform reads no SSM parameter at runtime. An exec instance's secrets
3583	reach it through its config bundle, opened with the box's
3584	`CARLOS_SECRETS_KEY`, so a target needs only the deployment's key.
3585
3586	**Shared with nearest-region R9.** One edges-file field for both specs:
3587
3588	- **name:** `secrets_key_fp`, in `edgesFile`
3589	(`internal/host/edgesfile.go:155-176`, written at `:603-605`);
3590	- **format:** `"sha256:"` and 64 lowercase hex digits of SHA-256 over
3591	`(*ecdh.PublicKey).Bytes()` (the uncompressed P-256 point) of the box's
3592	`CARLOS_SECRETS_KEY`;
3593	- **not omitempty**, like `hibernation_configured`: absent means unknown,
3594	`""` means no key;
3595	- the console computes the same over `CARLOS_SECRETS_PUBKEY`. A box is
3596	key-ready when its value equals the console's.
3597
3598	## 11. Versions and the protocol floor (codex 7)
3599
3600	- Every box publishes `moves_protocol: 1`; the console reports its own. The
3601	request door and T1 refuse unless every box in both regions and the
3602	console are at or above it, and every box is claim-aware (§19 K10).
3603	- Before the first production move the deployment writes
3604	`control/moves-protocol.json` `{"min": 1, "min_release": "vX.Y.Z"}`,
3605	create-only. **Every path that activates an executable** refuses a
3606	release below it: `carlos system apply`, explicit rollback, and
3607	**automatic boot recovery** of `carlos.prev` (`internal/host/systemapply.go:901`,
3608	restoring through `:817`), which validates `.prev` and any outstanding
3609	update journal before activating (joint N12; claim §10). Any downgrade of
3610	a box that is a participant in a held operation is refused. The console
3611	roll recipe states the same floor. The model lets a reboot restore an old
3612	executable and fails in 2,696 of 3,000 seeds (rev 5), mostly as parks an old
3613	executable can never let finish.
3614	- **The floor is published before any protected production rehearsal**
3615	(joint N12). Rev 3's rollout order had it the other way round (§15).
3616
3617	## 12. The operator surface (M16, M18)
3618
3619	**API.** The existing doors (`internal/console/authcli.go:625-628`). Every
3620	move mutation requires an operator (`Store.IsOperator`,
3621	`internal/console/store.go:1858`); others get the family's 404. Instance-role
3622	tokens keep the status GET only (M18), which closes the member-minted token
3623	path (`apiinstances.go:1554`) for moves (codex 11). New:
3624	`POST …/move/resolve` (§7.10). `GET …/move?detail=1` adds phases, reports,
3625	evidence and reasons.
3626
3627	**CLI.** `docs/site/cli.md` gets the heading in the same change
3628	(`internal/docsite` fails the gate otherwise).
3629
3630	```
3631	carlos move --host <h> --to <region> [--manual-cut] [--no-wait]
3632	carlos move status --host <h>
3633	carlos move cut --host <h>
3634	carlos move abort --host <h>
3635	carlos move resolve --host <h> --retry | --declare-lost <box>
3636	```
3637
3638	`--wait` is the default; exit 0 done, 3 rolled back, 4 stuck or waiting,
3639	5 refused.
3640
3641	## 13. Observability
3642
3643	- **Move log:** one object per event under
3644	`moves/<acct>/<app>/<host>/<op id>/` in the deployment bucket, beside the
3645	reports and evidence.
3646	- **Timings:** prepare, cut, land, and **offline** (`cut_at` to the open, or
3647	to the source's reopen after a rollback), each against its budget.
3648	- **Paging:** `rolled_back` (warning); `stuck`, `rolling_back` past
3649	`release_deadline`, a refused start check, and a refused stop evidence
3650	(stray process) (incident); `preparing` with no promotable round for 60
3651	minutes (warning); a move converted to `relocating` by a termination
3652	fence with no live box in its region (incident, once; M-C22 is the
3653	operator's line, rev 7.20).
3654	- **Member stream:** each transition is an event on the app's platform log
3655	(`emitEvent`, `internal/activator/logsink.go:31-36`).
3656
3657	## 14. Tests
3658
3659	### 14.1 Unit and integration
3660
3661	Every transition and guard; each readiness check failing alone (T4 against
3662	MinIO); every journaled phase crashing between its individual side effects
3663	and replaying; `ReconstructStopEvidence` against a real cgroup v2 hierarchy
3664	with a forked descendant that closes its descriptors and outlives its
3665	parent; the start check; `RenderHeld`, `MaterializeHeld`, `ReplaceTimers`;
3666	reconcile keeping participant rows.
3667
3668	### 14.2 The executable joint model
3669
3670	Built for rev 4, as the coordinator directed and the joint review
3671	recommended: `internal/sim/hostlife/`, a deterministic randomized Go
3672	simulation. **It is test-only**: every file is a `_test.go` file, so
3673	`go build ./...` never sees it, and it imports only the standard library.
3674	Rev 5 re-encodes it against claim spec rev 3 (8b5bccb2) and this spec as
3675	they would be implemented, and every rule is a named, mutable guard
3676	(`rules_test.go`).
3677
3678	#### 14.2.1 Running it
3679
3680	```
3681	go test ./internal/sim/hostlife/ # the gate: 300 seeds, about a second
3682	HOSTLIFE_SEEDS=30000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v -timeout 60m
3683	HOSTLIFE_SEEDS=100000 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v -timeout 300m
3684	HOSTLIFE_SEED=1796 go test ./internal/sim/hostlife/ -run TestHostLifecycle -v # one seed, full trace
3685	```
3686
3687	**Rev 6: strict classification (J2-R2-10).** `mutate.sh` reports CAUGHT
3688	only when the run completed and reported a seed that violated an
3689	invariant, with the seed number parsed from its output. A build failure, a
3690	panic, a timeout or unparsable output is ERROR, never a detection; every
3691	run's log is kept. `expected-outcomes.txt` beside the script declares the
3692	rules not expected to be caught alone (liveness-only, unreachable,
3693	combination-only, unexercised), each with its reason. The sweep exits
3694	nonzero on any ERROR, any unexpected MISSED, and any expected miss that is
3695	now caught (STALE).
3696
3697	**The evidence policy (Paul, 2026-10-06).** The deep sweeps were using
3698	half the shared box's cores and starving other agents. From rev 7.14 on:
3699	each revision runs **the gate** (300 seeds plus the witnesses) and **one
3700	mutation sweep at 3,000 seeds**, serially, with `HOSTLIFE_PAR=2` under
3701	`nice -n 19`, never alongside another sweep or a baseline; **baselines
3702	run at 30,000 seeds only**; the 100,000-seed baseline and the 30,000-
3703	and 100,000-seed mutation sweeps run **once**, at a final
3704	pre-implementation checkpoint, and only when Paul says so. A table cell
3705	or column those sweeps would have filled says "not run" for the
3706	revision, never a placeholder and never a number carried over from an
3707	earlier revision. Rev 7.14's 100,000-seed baseline had already run,
3708	clean, before the policy was set and is reported in §14.2.3; its 30,000-
3709	and 100,000-seed mutation sweeps were stopped mid-run and are not
3710	evidence.
3711
3712	**Rev 7.14: `TestInterruptedCleanReturn`, INV-20.** `go test` runs the
3713	positive case of the run walk across regions beside the witnesses: a
3714	clean rollback's fresh source admission dies before its first upload and
3715	the recovery walks R → T → S, then one more interrupted admission walks
3716	R2 → R → T → S; both restore the source's data. INV-20 is checked in the
3717	create's claim CAS: no obligation may be outstanding when a create claims
3718	a host.
3719
3720	**Rev 7.13: INV-17 at the park, `TestProbeWindow`.** The oracle for
3721	regional coverage runs when a whole-location park of `holder.location`
3722	completes in a region, not at the end: a record whose predecessor's
3723	objects were there and that is still uncovered is INV-17 at that CAS
3724	(a record born after the park is not in question). `go test` runs
3725	`TestProbeWindow` beside the witnesses: the landing probe's environment
3726	ready k steps after the attempt's first start, for k = 29, 30, 31.
3727
3728	**Rev 7.12: the final oracle runs the recovery.** When the run is
3729	quiescent with the serving host at rest after a session that did not
3730	certify, the final oracle no longer exempts the acknowledged, unuploaded
3731	writes as a prospective declaration (R10-6: that recorded and alerted
3732	nothing, with `writes-lost` off too). It wakes the host, runs the cold
3733	admission for real, drives its chores to quiescence, and judges the
3734	database by what the admission declared; a recovery that cannot run
3735	within the bound is