carlos / platform Public

spec rev 7.20 (claim rev 6.28: the fence reference, the pre-flip source conversion to relocating, L13 files manifest, one-box scope); model: fence-converts-moving and wFenceConvertsMoving; plans: contract owners, D15, D16

Spec: §7.10 the fence reference op.journal["fence.<box>"] and the one-CAS
conversion of a pre-flip moving op to relocating at pinning, holding
with one alert in a one-box region until a replacement box enrolls; §7.1
the one-box refusal (M-C21); §7.6 and §8.3 L13 as claim C3, §6.2a and
P6-D3 state it; §13 the page; §14.2.5 and §14.2.6 the model's new rule
and its stated limit; §20 M-C21, M-C22.

Model: rule fence-converts-moving (recoveryPass converts, relocate takes
the host on the region's box, admits/release know relocating); witness
wFenceConvertsMoving. Gate green; mutate.sh 3000 fence-converts-moving
CAUGHT by the witness; HOSTLIFE_SEEDS=3000 unmutated run passed, both
niced at HOSTLIFE_PAR=2.

Plans: C1 to C4 are claim Plan 6 rev 2, C5 Plan 5, C6 and C7 Plans 8/8b
(C7 settled by 6.28 and narrowed to the helpers still owed), C8 region
HA; D15 one-box regions only; D16 the pre-flip source conversion on the
record side; Plan 1 Task 4 refuses multi-box regions and names chooseBox;
Plan 4 Task 2 ReturnToSource's fence form; Plan 5 Task 7 the conversion;
Plan 6 Task 2 the waiting-for-a-box state.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

claude 2 weeks ago cc30c2bf5f6ce591ed36ca42ae8725460929a509 parent d5716bf

13 files changed, +406 −42

docs/superpowers/plans/2026-10-06-moves-phase1-0-index.md +24 −4
docs/superpowers/plans/2026-10-06-moves-phase1-1-copy-and-staging.md +19 −8
docs/superpowers/plans/2026-10-06-moves-phase1-4-rollback-return-declare-lost.md +2 −2
docs/superpowers/plans/2026-10-06-moves-phase1-5-cleanup-and-parks.md +1 −0
docs/superpowers/plans/2026-10-06-moves-phase1-6-cli-status-observability.md +2 −2
docs/superpowers/plans/2026-10-06-moves-phase1-copy.md +2 −0
docs/superpowers/specs/2026-10-02-move-any-app-design.md +125 −26
internal/sim/hostlife/console_test.go +23 −0
internal/sim/hostlife/moves_test.go +132 −0
internal/sim/hostlife/protocol_test.go +5 −0
internal/sim/hostlife/rules_test.go +1 −0
internal/sim/hostlife/witness_test.go +63 −0
internal/sim/hostlife/world_test.go +7 −0

CI passed — run details

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-0-index.md b/docs/superpowers/plans/2026-10-06-moves-phase1-0-index.md

index 0df5cc745..fcd29fcc4 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-0-index.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-0-index.md

@@ -11,8 +11,9 @@ on `main` at 67547f5 or later, as an ordered series of plans that each

produce working, tested, mergeable software.

**Spec:** `docs/superpowers/specs/2026-10-02-move-any-app-design.md` (rev

-7.19: P7 cold-only and region HA L14 to L17 folded in; L18 stated as a

-limit). The executable model is `internal/sim/hostlife/` at 9c417aaa on

+7.20: P7 cold-only, region HA L13 to L17 folded in with claim rev 6.28's

+fence reference and pre-flip conversion; L18 stated as a limit; one-box

+regions only). The executable model is `internal/sim/hostlife/` at 9c417aaa on

the same branch; its witness names are cited in the tests the plans port.

**Claim library on `main` (built on, never re-implemented):**

@@ -120,6 +121,12 @@ Every task marked **BLOCKED-ON-CLAIM** names one of these contracts and

is not built until the contract is merged on `main`; the moves plans do

not guess the API beyond what is written here.

+Owners (the coordinator, 2026-10-06): **C1 to C4 are claim Plan 6 rev 2**,

+**C5 is claim Plan 5**, **C6 and C7 are claim Plans 8 and 8b**, **C8 is

+region HA's** (plan 1a). Claim rev 6.28 (4ffe8a0d) adopts region HA's L1

+to L20; spec rev 7.20 aligns with it (the fence reference, the pre-flip

+source conversion, L13, the one-box scope).

|---|---|---|---|

| C1 | `(a *Service) startAdmitted(ctx, e *actEntry, admitted hostclaim.Observed, policy startPolicy) error` with `startPolicy{MaxStarts int; Window time.Duration; Deadline time.Time; Probe bool; Prepared *moves.InstallManifest; Inputs *provision.MoveInputs}`: the admitted writer's start of claim rev 6.10 §6.4a (purge, restore of the admitted baseline or the prepared generation's pinned snapshot, start, readiness, first upload, `generation.json` by If-Match or If-None-Match, `PublishGeneration`, open), callable for a **held** row, returning `ErrAttemptOver` when the policy's window or deadline passes before readiness and never marking the host failed when `Probe` is true. Cold only (P7): the sequence never consults a certificate while P7 stands. | claim Plan 6 Tasks 7, 9 (work order 1) | Plan 3 Tasks 5, 6, 7; Plan 4 Task 9 |

@@ -128,8 +135,8 @@ not guess the API beyond what is written here.

| C4 | `hostbox.Regional.Run` runs `park-replica` chores scoped to `moves/<host>/<op id>` and to `instances/<host>/<inc>`, and `park-generation` chores, under move and rollback op ids; its `Leases.Acquire(bucket, location)` **shares the activator's held lease for a location this box itself serves** (an aggregate lease adapter, claim Plan 5 D3's wording), else a landing's residue chores and the at-rest sweep on a serving host can never acknowledge (`park/remote.go:404` acquires the location's lease). | claim Plan 6 Task 10, Plan 5 Task 3 | Plan 5 Tasks 1, 3, 5 acknowledgement after the horizon (the immediate half runs without it) |

| C5 | Production callers for `hostops.Controller.Adopt` (`adoptHostRecord`) on the reconcile pass and for `(s *Server) StartClaimRecoveryPass`: a legacy host gets its claim on the next reconcile pass. | claim Plan 5 integration (work order 3) | the rehearsal (Plan 7 P-5); the request door's "no host claim yet" refusal is correct meanwhile |

| C6 | The loss sequence, end to end: `CreateLossRecord` of a `prepared` record with `WriteSources` composed as **the latest target session as reason `target` and every earlier target session since the cut and, when `src_covered` is false, the source's cut session as further sources** (`lost.go:149-191` requires the frozen set to equal the admission's primary `WritesLost` plus `AdditionalWritesLost`, unique by `(box, generation, session)`, each with a validated baseline); the transition `prepared → committed` with `ResultClaimGen` after `DeclareLost` (`lost.go:119` admits only a `committed` record); `DestroyedStorage` attestations for `DischargeLocal`; `Enrollment` and `QuarantineRevision` as the roster supplies them (Plan 8b), and a fence form of the declaration with neither (region HA L2 to L4). Moves supplies `moves.LossOwner` (`ValidateDeclareLost`, `ValidateLossRecovery`) and the record-side `lost` phase; the claim owns the record's lifecycle and the exact `LossRecord` composition. | claim Plan 8 + 8b (work order 2) | Plan 4 Task 10; the lost-target branch of Plan 4 Task 5; Plan 6 Task 1 `--declare-lost`; Plan 7 Run 4 |

-| C7 | The journal key under which a termination fence is cited on the claim (`loss.<id>` with a fence intent, or a `fence` key) so `ReturnToSource` can accept it as evidence (region HA L14). | claim 8b / region HA L2 to L4 | Plan 4 Task 2's fence form |

-| C8 | Region HA's files publisher API, `files.Publish(ctx, store lease.VersionedStore, location, generation, dir, envPath string) (manifestVersion string, err error)` or its real name, for `local`'s files manifest (spec rev 7.19 §7.6, L17). | region HA plan 1a | Plan 2 Task 10 `local`'s manifest step (`.files-gen` alone until then) |

+| C7 | **Settled by claim rev 6.28 §7.3 (spec rev 7.20 §7.10):** `op.journal["fence.<box>"] = {"enrollment","key","sha256"}` names `control/box-fences/<enrollment>.json` and the digest of the bytes verified; a `loss.<id>` intent cites the same reference; consumers accept a fence only through it, re-verifying the record; an automatic declaration needs no quarantine revision and no operator. Still owed by Plans 8/8b: the fence record's writer and the verification helper (`hostclaim.VerifyFence(ctx, s, ref) error` or its real name) and the one-CAS conversion of a pre-flip `moving` op to `relocating` at `pinning` (`hostclaim.ConvertMovingToRelocating(opID, fence FenceRef) func(*Claim) error` or its real name: exec `"none"`, stamp and generation preserved, obligations untouched, `relocating`/`pinning` in the source region; refused once the record is `landing`). Moves' `ReturnToSource` (Plan 4 Task 2) and the console pass (Plan 5 Task 7) consume both. | claim Plans 8 and 8b | Plan 4 Task 2's fence form; Plan 5 Task 7's conversion call; Plan 6 Task 2's `waiting for a box in <region>` state |

+| C8 | Region HA's files publisher API, `files.Publish(ctx, store lease.VersionedStore, location, generation, dir, envPath string) (manifestVersion string, err error)` or its real name, for `local`'s files manifest (spec rev 7.20 §7.6, L17), bound to the session (claim C3), writing origin-qualified references (P6-D3), with the reader a cold admission uses to establish its files manifest from the admitted predecessor chain by exact version. | region HA plan 1a | Plan 2 Task 10 `local`'s manifest step (`.files-gen` alone until then); Plan 3 Task 5's admitted start (files from the manifest once C8 exists) |

## Decisions locked across the series

@@ -153,6 +160,8 @@ not guess the API beyond what is written here.

- **D11 The terminal outcome survives the close.** Every close CAS (`done`, `rolled_back`, `aborted`) writes `Record.LastMove = &MoveOutcome{ID, Outcome, At, OfflineS}` as it clears `Move`, so a CLI that missed the intermediate states reads the outcome of the move id it requested from `GET …/move` (`{"state":"none","last":{…}}`) and exits with the right code.

- **D12 Order within the series.** The copy gate (the record file and the ship check) is Plan 1 Task 15, so every later plan's strings are checked from the day they are written; the paging primitive `host.PageOperator` is Plan 5 Task 0, before the console pass that needs it; `carlos move`'s dispatch and its `docs/site/cli.md` heading land in one task (Plan 6 Task 1), so no commit fails the docsite gate. `registry.DeleteIfHold` is Plan 1 Task 13's, beside `ReleaseHold`; `hostclaim.ReleaseMove` is Plan 1 Task 3's (Plan 4 widens its legal states); Plan 1 Task 11's host-side report pass is built inside Task 14 (it needs that task's harness).

- **D13 The operator-off switch.** Every move entry point (the request door and its siblings, the box worker's handling of any record with `move`, the console's move pass, `carlos move`) is behind `CARLOS_MOVES_PHASE1=on`, read by the console and the agent, **off by default**. Off: the door answers 409 "moves are not enabled on this deployment", the worker skips every record with a move (one log line a minute), the pass does nothing. The switch is spec §15 step 4's dormancy made concrete: the series merges to `main` task by task without exposing a half-move, and the default stays off until every plan is merged and Paul's rehearsal order begins (Plan 7 P-1 turns it on per deployment). The copy gate ties to it: `TestPendingCopyIsNotWired` becomes `TestPendingCopyKeepsTheSwitchOff`: while any row of the copy record is `pending`, `moves.DefaultEnabled` must be `false`, and no task may flip it. Pending strings may therefore be wired as the tasks are built; nothing ships to an operator until Paul approves the record and the switch default changes in one commit.

+- **D15 One-box regions only (spec rev 7.20 §7.1, the coordinator's scope ruling).** The request door refuses a move into or out of a region with more than one eligible box (M-C21, pending Paul), computed with the same `eligibleBoxes` the create door uses (`internal/console/boxchoice.go` on main); `choose()` therefore names the region's one box. The model stays at one box per region (spec §14.2.6); the two-box model is not built in this series. Plan 1 Task 4 carries the refusal; Plan 7's rehearsals run only in one-box regions.

+- **D16 A source terminated before the flip (spec rev 7.20 §7.10).** The fence converts the `moving` op to `relocating` at `pinning` in one claim CAS (C7's claim-side helper); the moves side writes the record's `move.state = "relocating"` with `reason` and, in a one-box region, shows `waiting for a box in <region>` (M-C22) and pages once (Plan 5 Task 7, Plan 6 Tasks 2 and 5); the lane's `park-replica` runs under the target region as for an abort; the move's record clears when the relocation releases to `serving` (the console pass, on `serving` with `rec.Move.ID == op id`). Nothing in Phase 1 builds the relocation itself: that is region HA's.

- **D14 Cold only (P7, claim rev 6.27 §1.1).** No task passes `Mode: "warm"` or `PredecessorCertified: true` to `AdmitWriter`; no task writes `closed/<session>.json`; `KeepStamp` follows the library's rule unchanged. The budget already prices every attempt as a cold admission (Plan 1 Task 10); the per-wake `park-generation` chore is outside the cut window.

## Global constraints (every plan repeats these)

@@ -246,6 +255,17 @@ contracts (the BLOCKED-ON-CLAIM table above).

| R1-11 | unknown-floor participation missed preparing participants | Plan 1 Task 12: a participant is a held row **or** a record whose move names this box |

| R1-27 | Task 7's retry contradicted Task 1 | Plan 4 Task 7 resumes at `StuckAt` |

+## The model's limit (rev 7.20)

+`internal/sim/hostlife` stays at one box per region plus replacement

+boxes. It gains rule `fence-converts-moving` and witness

+`wFenceConvertsMoving` (a source terminated before the flip in a one-box

+region: conversion to `relocating`/`pinning`, no churn and one alert

+while no box exists, completion on the replacement box). It does not

+model `choose()`, two target replacements, `stuck` after them, or the

+files publisher (it takes the fenced source's files directory as

+published). The two-box model is region HA's, on its own branch.

## What the model proved and the plans port

Witnesses that become real tests, by plan: Plan 2 ports `wSealByVersion`,

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-1-copy-and-staging.md b/docs/superpowers/plans/2026-10-06-moves-phase1-1-copy-and-staging.md

index 4fad3d74f..7f91d1587 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-1-copy-and-staging.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-1-copy-and-staging.md

@@ -1001,6 +1001,16 @@ func (s *Server) handleAPIInstanceMoveRequest(w http.ResponseWriter, r *http.Req

jsonError(w, http.StatusConflict, "the fleet's edges files could not all be read. try again")

return

}

+ // Phase 1 is for one-box regions (spec rev 7.20 §7.1, index D15): a

+ // region with more than one eligible box, on either side, is refused.

+ if n := len(eligibleBoxes(snapshotFor(ctx, s.cfg.Releases), to, rec.Pool)); n > 1 {

+ jsonError(w, http.StatusBadRequest, s.homeRegionOut(to)+" has more than one box. Moves between regions with several boxes are not supported yet.")

+ return

+ }

+ if n := len(eligibleBoxes(snapshotFor(ctx, s.cfg.Releases), rec.Region, rec.Pool)); n > 1 {

+ jsonError(w, http.StatusBadRequest, s.homeRegionOut(rec.Region)+" has more than one box. Moves between regions with several boxes are not supported yet.")

+ return

+ }

if targetBox == "" {

jsonError(w, http.StatusBadRequest, "no box in "+to+" publishes an edges file yet")

return

@@ -1066,14 +1076,15 @@ func moveTargetBox(ctx context.Context, s release.Store, to, from string) (box s

return "", false, false

}

floorOK, complete = true, true

- // The target box in a multi-box region is region HA's choose() (spec

- // rev 7.19 §7.1, L15): prefer a box running no instance of the app,

- // then the most headroom (fewest claimed hosts), then the SHA-256

- // tie-break. Until region HA's eligibleBoxes is exported, one box per

- // region is the deployment's shape and the rule degenerates to "the

- // only box"; the lexically-first fallback below is kept for a region

- // that already has two, and TestMoveTargetBoxPrefersChoose pins the

- // choose() order once the helper exists.

+ // The target box is region HA's choose() over the eligible boxes (spec

+ // rev 7.20 §7.1, L15): main's same-package eligibleBoxes and chooseBox

+ // (internal/console/boxchoice.go) are the one implementation; the

+ // create door uses them too. Phase 1 refuses a multi-box region at the

+ // door (D15), so choose() names the region's one box here, and this

+ // loop only finds it; TestMoveTargetBoxUsesChoose pins that the call

+ // is chooseBox's and that chooseBox's tie-break is the approved

+ // SHA-256 of host + "\x00" + box reference (region HA §5.2), fixing

+ // chooseBox where it still differs.

for _, f := range snap.Files {

if f.Placement != to && f.Placement != from {

continue

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-4-rollback-return-declare-lost.md b/docs/superpowers/plans/2026-10-06-moves-phase1-4-rollback-return-declare-lost.md

index b8d97e89e..f6912e0b3 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-4-rollback-return-declare-lost.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-4-rollback-return-declare-lost.md

@@ -72,7 +72,7 @@

**Interfaces:**

- `RollBack(opID, rbID string) func(*Claim) error`: `KindLanding` (any phase but `committed`) → `KindRestoring`, phase `"releasing"`, `Intent["rollback"] = rbID`; exec unchanged (the target still owes evidence).

- `TargetReleased(opID, targetBox, targetRegion, evidenceKey string, scope ParkScope, newID func() string) func(*Claim) error`: `KindRestoring`, `Exec == targetBox` → `ExecToNone(... JournalEvidenceTarget)`, phase `"released"`, `QueueLocationPark(opID, targetRegion, targetBox, scope, newID)` (a `park-replica` scoped to the whole location plus the box's `park-local`, D6), then `CoverRegionPredecessors(opID, "released", targetRegion)` (claim rev 6.14 item 6, R12-3).

-- `ReturnToSource(opID, sourceBox string, clean bool) func(*Claim) error` (§7.8 `claimed`, K4): `KindRestoring`; `Exec == ""` **or `"none"`** (claim Plan 8's `declareLostTransition` writes the literal `"none"`, line 1511); either `evidence_target` journalled **or** a `loss.<id>` journal entry present (a declared-lost target gives no evidence; the declaration is the cited fence, §7.10); `sourceBox == participants[0]` (the lost target has been removed from `participants` by the declaration, so the source may be the only participant left) → `Exec = sourceBox`, phase `"claimed"`, `holder.stamp = ParseUint(journal[source_stamp])`; when `clean`, `holder.generation = journal[src_gen]`; `holder.admissions` untouched (R11-4). `TargetReleased` is not called for a declared-lost target: the console's resolve door queues the target region's location `park-replica` and runs `CoverRegionPredecessors` itself (Task 10), since no box can give evidence for the lost one.

+- `ReturnToSource(opID, sourceBox string, clean bool, verifyFence func(ref string) error) func(*Claim) error` (§7.8 `claimed`, K4): `KindRestoring`; `Exec == ""` **or `"none"`** (claim Plan 8's `declareLostTransition` writes the literal `"none"`, line 1511); either `evidence_target` journalled, **or** a `loss.<id>` journal entry present (an operator's declaration), **or** `op.journal["fence.<target box>"]` present (spec rev 7.20 §7.10, claim rev 6.28 §7.3: `{"enrollment","key","sha256"}`), in which case `verifyFence(ref)` must re-read `control/box-fences/<enrollment>.json` and confirm the digest and the roster identity before the transition proceeds (the caller supplies the verifier, C7's `hostclaim.VerifyFence`; until it exists the fence form is BLOCKED-ON-CLAIM and the closure returns `ErrWrongState` for a fence-only claim); `sourceBox == participants[0]` (the lost target has been removed from `participants` by the declaration, so the source may be the only participant left) → `Exec = sourceBox`, phase `"claimed"`, `holder.stamp = ParseUint(journal[source_stamp])`; when `clean`, `holder.generation = journal[src_gen]`; `holder.admissions` untouched (R11-4). `TargetReleased` is not called for a declared-lost target: the console's resolve door queues the target region's location `park-replica` and runs `CoverRegionPredecessors` itself (Task 10), since no box can give evidence for the lost one.

- `ReleaseMove(opID, execBox string) func(*Claim) error` (K8): kind in `landing/committed`, `restoring/opened`, `reverting/opened` or `moving/aborting`; no obligation with `Op == opID` remains; sets `Op = Op{Kind: KindServing, Exec: execBox}` (participants cleared; journal dropped; the admissions stay in the holder).

- `SetRevPhase(opID, from, to string)` (`rev_phase` in the journal under `KindReverting`, order `evidence, verify, probing, probed, opened`).

- `QueueReturnLanePark(opID, sourceRegion string, scope ParkScope, newID)` (dirty: the lane `moves/<host>/<rb id>` in the source's region, queued at `probed`, §7.8).

@@ -196,7 +196,7 @@ Tests: `TestRevertFromStoppingComputesEvidenceFirst`; `TestRevertVerifyThenProbe

3. **The claim** (BLOCKED-ON-CLAIM C6: the exact lifecycle is the claim's; moves supplies the owner and the inputs listed here): `hostclaim.Read` fresh; if `Op.Kind == KindLanding` the claim half of the rollback is still owed → `hostclaim.Update(RollBack(id, rbID))` first. Then the loss sequence as `lost.go` on `feat/hostclaim-leases` requires it: `CreateLossRecord` of a `prepared` record whose `WriteSources` are composed per C6 (the latest target session as `target`, every earlier target session since `cut_session`, and the source's cut session when `src_covered` is false; moves computes the list from `holder.admissions` and the seal), with `CloudObservation{ObservedAt, Account, Region, InstanceID, State, RequestID}` from the body (every field required), `OperatorAttestation{MaintainComputeFence: true, ColdQuarantineStartOnly: true, DestroyedStorage: <the body's attested volume ids, required when any park-local is to be discharged>}`, `FencedAt: cloud.ObservedAt`, `ConfirmedConsequences` as the claim computes them from the observed claim, `Timers: TimerLoss{Knowledge: TimersPartial, Source: <the cut's timers/ object>}` when it exists else `TimersUnknown`, `Enrollment` and `QuarantineRevision` from Plan 8b's roster; `DeclareLost(ctx, s.cfg.Releases, pub, obs, lossID, moves.LossOwner{Record: *rec})`; then the record's `prepared → committed` with `ResultClaimGen` through `ReplaceLossRecord` (the claim's function; `AdmitWriterWithLoss` admits only a `committed` record, `lost.go:119`); then `MoveRollbackLossCommitted(g)` (Task 1) moves the record from `lost` to `released` clean with `Evidence = LossRef`. A crash between any two of these replays from the loss record's `State`.

4. In one more claim CAS, cases (a) and (b) only: `QueueLocationPark(id, targetRegion, "", scope{Location: TrimSuffix(holder.location, "/"), Incarnation, EvidenceAt: FencedAt, RequestLimit: 120 s}, newID)` and `CoverRegionPredecessors(id, obs.Claim.Op.Phase, targetRegion)` (what `TargetReleased` does for a live target), and for case (b) `QueueReturnLanePark(id, sourceRegion, scope{Location: ScopeLocation(host, rbID), Incarnation, EvidenceAt: FencedAt, RequestLimit: 120 s}, newID)` (model 27). The declaration itself discharged the box's `park-local` chores (or left them for the operator path) and reassigned its regional chores to `region:<target>`.

5. The declared timers are alerted through `host.PageOperator` (Plan 5 Task 0); the box is on `claim.Lost`. **`TargetParkedAt` for a lost target** (round-2 finding 18): the lost box's `cleaning` never runs; the console pass (Plan 5 Task 7) stamps `MoveRollbackTargetPhase(… → cleaned, TargetParkedAt)` when no obligation under the op is owned by `box:<lost box>` or by `region:<target region>` remains unacknowledged, which the surviving regional runner (C4) brings about; a region with no surviving box leaves the chores to the at-rest sweep and the close waits, paged once an hour (§7.8 "Waiting" applies to the park as it does to the evidence).

- Until claim Plan 8b lands (index), the door answers 409 "declare-lost is not enabled in this deployment yet" unless `CARLOS_MOVES_DECLARE_LOST=1` is set on the console, which only a test sets. **The termination fence (spec rev 7.19 §7.10, L14)** is the same path with the fence record as `LossRef`, driven by the console pass instead of an operator, once C7 names the journal key; BLOCKED-ON-CLAIM with the rest of this task.

+ Until claim Plan 8b lands (index), the door answers 409 "declare-lost is not enabled in this deployment yet" unless `CARLOS_MOVES_DECLARE_LOST=1` is set on the console, which only a test sets. **The termination fence (spec rev 7.20 §7.10, L14; claim rev 6.28 §7.3)** is the same record-side path with `LossRef` = the fence's journal reference (`fence.<box>`), driven by the console pass (Plan 5 Task 7) instead of an operator, with no quarantine revision and no operator attestation (L4); a target fenced after the flip takes this path; **a source fenced before the flip takes none of it**: the claim's one-CAS conversion to `relocating` at `pinning` (C7's helper) applies, and the moves side only records `move.state = "relocating"` with the reason and clears the record when the relocation releases (index D16). BLOCKED-ON-CLAIM with the rest of this task.

- The source's recovery with a lost target: `waiting` ends when the record's target phase is `released` with `Evidence == LossRef` (the door's `MoveRollbackLossCommitted`, after the loss record is `committed`) and the claim carries the `loss.<id>` entry with `Exec == "none"`; a record still at `lost` is **not** consumed (round-2 finding 15); `claimed` is `ReturnToSource(id, cfg.Box, clean = true)` (Task 2's loss form); the probe admits through `hostclaim.AdmitWriterWithLoss(ctx, s, pub, obs, admission, lossID, validated, moves.LossOwner{...})` instead of `Writer.Admit` (the moves pass passes `lossID` through `ProbeConfig.LossID`), with `validated` built from the admissions table as above (`ValidatedWriteSource{Reason: "target" | "source-cut", Box, Generation, Session, Region, Baseline, RemoteMaxTXID}`); `TestLostTargetRecoveryRunsAgainstARealDeclaration` drives the source pass from the claim Plan 8's `DeclareLost` actually produced in the previous test, not a hand-written claim.

- A returning box (`Lost` contains it) refuses every move step and runs `Local.RetireInstallation` for the host under the guard before anything else (claim §7.2 quarantine; Plan 8's `hostquarantine` when it lands, else the `park.Local` call directly).

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-5-cleanup-and-parks.md b/docs/superpowers/plans/2026-10-06-moves-phase1-5-cleanup-and-parks.md

index a32565108..4e0cc663c 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-5-cleanup-and-parks.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-5-cleanup-and-parks.md

@@ -146,6 +146,7 @@ Tests: `TestSweepSkipsWhileAMoveStages` (Review Focus 3); `TestFreeHostSweepIsHo

- deadline sweeps: `landing` past `landing_deadline` → `MoveRollBack(g, NewRollbackID, "landing deadline", now)` (the box writes the claim half or this pass does on its next tick); `rolling_back` past `release_deadline` with no target evidence → `alert("incident", ...)` once per hour (M-C10's sentence for the operator view); `preparing` with `UpdatedAt` older than 60 minutes → `alert("warning", ...)`; older than `moves.AbortAfter` (6 h) → `MoveAbort()`.

- the finalization halves: `committed` with both stamps and no obligations → `ReleaseMove` then `MoveClose`; `rolling_back` with the three stamps and no obligations → `ReleaseMove(source)` then `MoveRolledBackClose`; `aborting` with no obligations → `ReleaseMove(source)` then `MoveAbortComplete`; a `rolling_back` record whose target is on `claim.Lost` and whose target phase is `released` (the loss committed) gets `TargetParkedAt` stamped by this pass once no obligation under the op is owned by that box or by its region (Plan 4 Task 10 step 5).

- the landing phase catch-up (Plan 2 Task 10 `syncClaimPhase`) for any `landing` record whose claim phase is behind its `landing_phase`.

+ - **a source terminated before the flip** (spec rev 7.20 §7.10, index D16; BLOCKED-ON-CLAIM C7): a `moving` claim whose source box carries a verified termination fence and whose record is not `landing` → the claim's one-CAS conversion to `relocating`/`pinning` (C7's helper) and the record's `MoveRelocating(g, reason)` (a `provision` transition this task adds: `preparing|ready|cutting → relocating`, keeping `Move.ID`; the record clears when the relocation releases, through the `serving` finalization half above, which already clears a finished `move`); when the source region has no live enrolled box, one incident page with M-C22's sentence (`host.PageOperator`, rate-limited by the op journal), and `GET …/move` shows `state: relocating` with `detail.waiting_for_box = <region>` (Plan 6 Task 2). A `moving` claim whose record is already `landing` is not converted: the flip is the record's decision and §7.10's lost-target path applies.

- `Server.startMovesPass(ctx)`: the ticker, logging each pass's errors; `alert` is `host.PageOperator` (Task 0), which the console binary links already (`internal/host` is in the CLI).

- The closes write `MoveClose(g, now)`, `MoveRolledBackClose(g, now)` and `MoveAbortComplete` with `LastMove` (index D11).

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-6-cli-status-observability.md b/docs/superpowers/plans/2026-10-06-moves-phase1-6-cli-status-observability.md

index 58794b246..b1d5d3b7a 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-6-cli-status-observability.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-6-cli-status-observability.md

@@ -63,7 +63,7 @@ Tests: `TestMoveWaitExitCodes` (a fake console serving a scripted sequence of de

**Interfaces:**

- `moveView` gains `Last *provision.MoveOutcome \`json:"last,omitempty"\`` (index D11: `{"state":"none","last":{"id":"mv_…","outcome":"rolled_back","at":"…","offline_s":41.2}}` after a close; every caller of the flat view sees it, M18's Instance-role token included, since it reveals nothing the state did not); `moveDetail{moveView; Move *provision.MoveState; Claim struct{Kind, Phase, Exec string; Participants []string}; Target *moves.TargetReport; Source *moves.SourceReport (env HMACs only); Evidence struct{Source, Target string} (keys); Log []string (the last 20 log keys)}`; `GET …/move?detail=1` is operator-only beyond the flat view (an Instance-role token gets the flat view with no detail, M18).

-- `handleAPIInstanceMoveStatus` reads `detail`; reads `hostclaim.Read`, the two reports and `s.cfg.Releases.List(moves.ReportPrefix(...)+"log/")`.

+- `handleAPIInstanceMoveStatus` reads `detail`; reads `hostclaim.Read`, the two reports and `s.cfg.Releases.List(moves.ReportPrefix(...)+"log/")`. A record in `relocating` (spec rev 7.20 §7.10, index D16) answers `state: relocating` and, when the claim is `relocating/pinning` with exec `"none"` and no live enrolled box in the source region, `detail.waiting_for_box = <region>`; the CLI prints M-C22 for it and `--wait` exits 4 (waiting). Test `TestMoveDetailShowsWaitingForBox`.

Tests: `TestMoveDetailLeaksNothing` (Review Focus 2: the response body contains no value of the launch environment, no evidence body, no `CARLOS_` value; it contains the report's check ids and the evidence keys); `TestMoveDetailIsOperatorOnly`.

@@ -102,7 +102,7 @@ Tests: `TestLogKeysAreTransitionIdentities` (two writers of `landing-probing` pr

**Files:** create `internal/host/movespaging.go`, `internal/host/movespaging_test.go` (the primitive `host.PageOperator` is Plan 5 Task 0).

**Interfaces:**

-- Rules (§13): `rolled_back` → warning once; `stuck` → incident once per entry; `rolling_back` past `release_deadline` → incident once per hour; a refused start check or a refused stop evidence (stray process, M-C20) → incident once per op; `preparing` with no promotable round for 60 minutes → warning once. State for rate limits lives in the op journal (`Journal.Steps["paged:<rule>"]`), so a restart does not page again.

+- Rules (§13; a move converted to `relocating` by a termination fence with no live box in its region → incident, once, M-C22; spec rev 7.20): `rolled_back` → warning once; `stuck` → incident once per entry; `rolling_back` past `release_deadline` → incident once per hour; a refused start check or a refused stop evidence (stray process, M-C20) → incident once per op; `preparing` with no promotable round for 60 minutes → warning once. State for rate limits lives in the op journal (`Journal.Steps["paged:<rule>"]`), so a restart does not page again.

Test `TestPagingIsRateLimited` (Review Focus 4).

diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md b/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md

index 87fe3b263..cf8cf81c2 100644

--- a/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md

+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md

@@ -33,6 +33,8 @@ Columns: id, file, text, status.

## Plan 1

diff --git a/docs/superpowers/specs/2026-10-02-move-any-app-design.md b/docs/superpowers/specs/2026-10-02-move-any-app-design.md

index 0f8487eef..1950fbd41 100644

--- a/docs/superpowers/specs/2026-10-02-move-any-app-design.md

+++ b/docs/superpowers/specs/2026-10-02-move-any-app-design.md

@@ -1,8 +1,32 @@

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

**Date:** 2026-10-06

-**Revision:** 7.19.

+**Revision:** 7.20.

+- **Rev 7.20** aligns with claim rev 6.28 (4ffe8a0d), which adopts region

+ HA's L1 to L20 at its sections (`CODEX-ANALYSIS-REGION-HA-L1-L20.md`

+ beside it). **The fence reference** (§7.10, moves C7): every transition

+ that relies on a termination fence writes `op.journal["fence.<box>"] =

+ {"enrollment","key","sha256"}`; a `loss.<id>` intent cites the same

+ reference; `ReturnToSource` accepts a fence only through it,

+ re-verifying the record; an automatic declaration needs no quarantine

+ revision and no operator (L4). **A source terminated before the flip**

+ (§7.10): the fence converts the `moving` op to `relocating` in one CAS

+ (exec `"none"`, stamp and generation preserved, `relocating` at

+ `pinning` in the source region, every obligation untouched, the lane's

+ `park-replica` queued when not yet owed); in a one-box region it holds

+ at `pinning`, safe but **not recovered**, until region HA enrolls a

+ replacement box; the operator sees `waiting for a box in <region>` and

+ one alert; after the flip the conversion is refused. This replaces rev

+ 7.19's "the move aborts". **L13** (§7.6, §8.3): the files manifest is

+ claim C3's, §6.2a's and P6-D3's: the session-bound publisher,

+ origin-qualified manifest references, files reachability independent of

+ the database baseline. **Scope ruling:** Phase 1 is for one-box regions;

+ a move into or out of a region with more than one eligible box is

+ refused at the door with new copy (M-C21, pending Paul) until region

+ HA's own model and plan cover multi-box; the model stays one box per

+ region (§14.2.6). The model gains rule `fence-converts-moving` and

+ witness `wFenceConvertsMoving` (§14.2.5).

- **Rev 7.19** records Paul's rulings of 2026-10-06 on amadan #236 as

claim rev 6.27 (989ee349) §1.1 states them, and folds in region HA's

requests L14 to L17 (spec 1 rev 5.4, branch `design-region-ha-rev5`,

@@ -2308,12 +2332,17 @@ versions created after `H`, and INV-10 everywhere at the end of the run.

`{"region":"uk","cut":"auto"|"manual"}`, operator-only (§12). The door

CASes the claim from `serving` (holder = this incarnation, execution

holder = the source box) to `moving` with op id = the move id (§19 K2).

-**The target box is named in that CAS** (region HA L15, ruled H12): for

-a region with several boxes the door chooses it with region HA's

-`choose(eligibleBoxes(region, pool), app)` (spec 1 §5.2: prefer a box

-running no instance of the app, then the most headroom, then the SHA-256

-tie-break), over the roster and the edges snapshot; for a one-box region

-it is that box. The choice is made once and recorded as `op.participants[1]`

+**The target box is named in that CAS** (region HA L15, ruled H12): the

+door computes region HA's `choose(eligibleBoxes(region, pool), app)`

+(spec 1 §5.2: prefer a box running no instance of the app, then the most

+headroom, then the SHA-256 tie-break) over the roster and the edges

+snapshot. **Phase 1 scope (rev 7.20):** a move **into or out of a region

+with more than one eligible box is refused** at the door, with M-C21,

+until region HA's own model and plan cover multi-box regions; so in

+Phase 1 `choose()` always names the region's one box, and the source is

+the one box of its region. The refusal is a scope rule, not a safety

+rule: the protocol below is written for any target box the start CAS

+names. The choice is made once and recorded as `op.participants[1]`

and `op.intent.target`; readiness (T8, T9), evidence, install and

recovery bind to that box, and nothing substitutes another box: a target

that cannot complete is replaced only by an explicit fenced transition

@@ -2622,12 +2651,22 @@ versions `genselect.SelectPrepared` or the generation's current listing

pins and that listing's maximum TXID. The anchor rule, the two durable

states, the replay rule and the marker rule are the routine's, so both

callers get them once. **Every installation writes a files manifest in

-its new generation** (L17, §8.3): after `local` has extracted the

-archive, the installed files directory is published as region HA §5.6's

-objects and manifest under `<location>files/<generation>/`, before

-`.files-gen` is written, so a failure after this landing can restore the

-files without an archive; the archive at the cut stays as the sealed

-transfer.

+its new generation** (L17, §8.3; claim rev 6.28 C3, §6.2a, P6-D3): after

+`local` has extracted the archive, the installed files directory is

+published by the **session-bound files publisher** (claim C3's second

+ordinary-replication exception, bound to `{location, generation,

+session}`) as region HA §5.6's immutable objects and one manifest under

+`<location>files/<generation>/`, before `.files-gen` is written. Manifest

+entries carry **origin-qualified references** (claim P6-D3): an object is

+named by its own incarnation location and region, so copying a manifest

+into a new generation never reinterprets its references, and a cross-region

+landing publishes a manifest naming destination-local objects it

+materialized and verified from the sealed archive. **Files reachability is

+independent of the database baseline:** a cold admission establishes its

+files manifest from the newest valid manifest in the admitted predecessor

+chain, read by exact version, before the app starts; missing or malformed

+manifest data is never an empty-files bootstrap. The archive at the cut

+stays as the sealed transfer and the rollback's evidence.

### 7.7 The probe (codex 14)

@@ -2818,12 +2857,43 @@ and the fence record as `rollback.evidence`; after the record's commit

the target is authoritative and the move is not what recovers the

instance: the move finishes its own close (its remaining steps are parks

run by regional workers), and the instance's recovery is region HA's

-relocation, outside this spec. A terminated **source** is likewise not

-the move's to recover before the flip: the move aborts (its `moving`

-claim releases through the fence's lost-box path) and relocation takes

-the host. The fence supplies the evidence; this spec decides what the

-move does with it; the operator's `--declare-lost` stays for the

-stopped, unclear and vanished boxes the fence does not cover (claim D2).

+relocation, outside this spec. **A source terminated before the flip (rev 7.20; claim rev 6.28 §4).**

+The fence converts the pre-flip `moving` operation to `relocating` in

+**one CAS**: it records the fence reference (below), sets `op.exec =

+"none"`, preserves `holder.stamp` and `holder.generation`, starts

+`relocating` at `pinning` in the source's region, and leaves every

+obligation untouched; the move's staging lane, `park-replica` scoped

+`moves/<host>/<op id>` and owned by the target region, keeps its op id

+and stays executable (the conversion queues it when the move had not

+yet, as an abort would), and it blocks neither the conversion nor the

+relocation's release. Readiness, evidence and recovery bind to the

+replacement box `choose()` names when the relocation leaves `pinning`.

+After the flip (the record's `landing` state) the conversion is

+**refused** and this section's rules for a lost target apply. **In a

+one-box region** the converted operation has no eligible target: it sits

+at `pinning` with exec `"none"` and the lane's park still owed until

+region HA enrolls a replacement box (automatic ASG enrollment, H16 and

+H17). That state is safe, since no writer exists and the data is pinned

+in the source region's bucket, but the host is **not recovered until a

+box exists**. The operator sees it as `relocating / pinning: waiting for

+a box in <region>` in `carlos move status` and the fleet view, and one

+incident alert is raised when the conversion finds no live box in the

+region (§13); the alert is not repeated. The operator's `--declare-lost`

+stays for the stopped, unclear and vanished boxes the fence does not

+cover (claim D2).

+**The fence reference (rev 7.20; moves C7, claim rev 6.28 §7.3).** Every

+transition that relies on a termination fence writes

+`op.journal["fence.<box>"] = {"enrollment", "key", "sha256"}`: the box's

+enrollment, the key `control/box-fences/<enrollment>.json`, and the

+SHA-256 of the exact bytes the transition verified. A `loss.<id>` intent

+written by the same transition cites the same reference. `ReturnToSource`

+and every other consumer accept a fence only through that reference,

+re-reading the record at `key`, requiring its digest to equal `sha256`

+and its enrollment and cloud identity to match the roster's; the key is

+never reused for another box or enrollment within the operation. An

+automatic declaration from a fence needs no quarantine revision and no

+operator (L4); the terminated enrollment is permanently ineligible.

**What a declared-lost box leaves behind (rev 7.11).** Its acknowledged

writes beyond its uploads are declared by the next admission's

@@ -3420,7 +3490,9 @@ carlos move resolve --host <h> --retry | --declare-lost <box>

- **Paging:** `rolled_back` (warning); `stuck`, `rolling_back` past

`release_deadline`, a refused start check, and a refused stop evidence

(stray process) (incident); `preparing` with no promotable round for 60

- minutes (warning).

+ minutes (warning); a move converted to `relocating` by a termination

+ fence with no live box in its region (incident, once; M-C22 is the

+ operator's line, rev 7.20).

- **Member stream:** each transition is an event on the app's platform log

(`emitEvent`, `internal/activator/logsink.go:31-36`).

@@ -5457,6 +5529,20 @@ Each was a failing seed first, then a rule; each rule's mutation is in

#### 14.2.5 Mutation results

+**Rev 7.20** adds one rule, `fence-converts-moving` (108 in all), with

+one witness, `wFenceConvertsMoving` (74 in all): a source terminated

+before the flip in a one-box region; the fence converts the move to

+`relocating` at `pinning` (exec none, stamp and generation kept, the

+lane's park owed), the operator is alerted once, the claim does not churn

+while no box exists, and the relocation completes on the replacement box.

+Under the evidence policy of §14.2.1 the gate ran (every witness and the

+default seeds), `mutate.sh 3000 fence-converts-moving` at `HOSTLIFE_PAR=2`

+under `nice -n 10` reported `CAUGHT fence-converts-moving: sweep 0 of

+3000; witness violated` (the random sweep never terminates a source, so

+the witness alone catches it, as designed), and one unmutated

+`HOSTLIFE_SEEDS=3000` run at `HOSTLIFE_PAR=2` passed. No other rule

+changed and no other sweep was run.

Every rule was dropped in turn, with the one prebuilt binary of §14.2.1,

on the final rev 7.17 model (b9e97783; rev 7.18 changed no rule and ran no sweep, §14.2.1), with the strict classification,

**in two ways**: the **random sweep**, 3,000 seeds each (the 30,000- and

@@ -5920,11 +6006,22 @@ baselines, this sweep and the witnesses are the evidence for rev 7.10.

whose `box.Region` and per-region bookkeeping assume one box; it is

not a change this revision can make within the CPU policy (the gate

plus one niced 3000 sweep per revision) or its scope. **Stated as a

- limit:** nothing in §14.2.3's results speaks for two boxes in one

- region, for `choose()`'s spread, or for a termination fence taking a

- participant off an operation. The extension belongs to a joint round

- with the region HA session, on its own branch, with its own sweeps,

- after relocation's protocol is fixed in claim rev 6.27's successors.

+ limit (rev 7.20, the coordinator's scope ruling):** the model stays at

+ one box per region; Phase 1 refuses multi-box regions at the door

+ (§7.1), so the limit matches the scope. Nothing in §14.2.3's results

+ speaks for two boxes in one region or for `choose()`'s spread. Rev

+ 7.20 adds the one fence case Phase 1 meets: rule

+ `fence-converts-moving` and witness `wFenceConvertsMoving`, a source

+ terminated before the flip in a one-box region, converted to

+ `relocating` at `pinning`, holding without churn and with one alert

+ until a replacement box enrolls (the model's replacement mechanism),

+ then completing on it. The model collapses the relocation's install

+ into the cold admission's restore of the pinned generation from the

+ region's remote, and stands in for region HA's files publisher by

+ taking the fenced source's files directory as published (L17); it

+ does not model `choose()`, two replacements, or `stuck` after them.

+ The two-box extension belongs to a joint round with the region HA

+ session, on its own branch, with its own sweeps.

- **It is a model.** It checks the protocol, not the code that will

implement it. Its S3 is a versioned map with the documented semantics,

every one checked against the real service (§15 step 8). Its

@@ -6686,6 +6783,8 @@ copy-review gate. No em dashes.

| M-C18 | This declares <box> lost. Anything <host> wrote on <box> after <time> is lost. Type the host name to confirm. |

| M-C19 | <host> is being moved. Delete it after the move finishes, or abort the move first. |

| M-C20 | <box> is running a process for <host> that this move cannot account for. An operator has been paged. |

+| M-C21 | <region> has more than one box. Moves between regions with several boxes are not supported yet. |

+| M-C22 | <host> is waiting for a box in <region>. Its last box was terminated before the move finished. Nothing is lost, and it will start when a box joins the region. |

## 21. Out of scope for Phase 1, restated

diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go

index 89c0e50d7..c85851365 100644

--- a/internal/sim/hostlife/console_test.go

+++ b/internal/sim/hostlife/console_test.go

@@ -1019,6 +1019,29 @@ func (w *world) recoveryPass() {

if c == nil {

return

}

+ // a terminated source of a pre-flip move (moves rev 7.20 §7.10, claim

+ // rev 6.28 §4): the termination fence converts the operation to

+ // relocating at pinning. The flip is the record's decision, so a record

+ // at landing refuses the conversion and §7.10's own recovery applies.

+ if on("fence-converts-moving") && c.Holder != nil && c.Op.Kind == "moving" && !c.Op.Committed &&

+ !(w.rec != nil && w.rec.MoveID == c.Op.ID && w.rec.MoveState == "landing") {

+ if src := w.boxByID(c.Op.Src); src != nil && src.Destroyed {

+ w.convertToRelocating(c, src)

+ return

+ }

+ // a relocation with no box in its region (a one-box region whose only

+ // box was fenced): safe, nothing runs, the data is pinned; not

+ // recovered until region HA enrolls a replacement. The operator is

+ // told once (moves rev 7.20 §7.10, §13)

+ if c.Op.Kind == "relocating" && c.Op.Phase == "pinning" && c.Op.Exec == -1 && !c.Op.Alerted && w.regionBox(c.Op.SrcRegion) == nil {

+ if w.cas(c, func(n *claim) bool { n.Op.Alerted = true; return sameOp(n.Op.ID, c.Op.ID) && n.Op.Kind == "relocating" }) {

+ w.alerts++

+ w.stats["relocation: waiting for a box in the region"]++

+ w.logf("relocation %s waits at pinning: no box in region %d", c.Op.ID, c.Op.SrcRegion)

+ }

+ return

+ }

// a late record PUT from a cancelled create: an orphan, never admitted

// (C1); removed by the ordered cleanup of claim rev 6 §5.1 step 5, as

// a plan of this console (J2-R2-7, R3-2)

diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go

index e9531b677..6e5ae501f 100644

--- a/internal/sim/hostlife/moves_test.go

+++ b/internal/sim/hostlife/moves_test.go

@@ -223,6 +223,136 @@ func (w *world) role(b *box, c *claim) {

if b.ID == c.Op.Src {

w.pushStep(b, c)

}

+ case "relocating":

+ w.relocate(b, c)

+ }

+// convertToRelocating is the termination fence's conversion of a pre-flip

+// move (moves rev 7.20 §7.10; claim rev 6.28 §4): one CAS records the

+// fence (fence.<box>), sets exec none, keeps holder.stamp and

+// holder.generation, starts relocating at pinning in the source's region,

+// touches no existing obligation, and queues the staging lane's park for

+// the target region when the move had not queued it yet (as an abort

+// would). The fenced source is on lost and leaves the participants.

+func (w *world) convertToRelocating(c *claim, src *box) {

+ op := c.Op

+ if w.cas(c, func(n *claim) bool {

+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "moving" || n.Op.Committed {

+ return false

+ }

+ n.Op.Kind, n.Op.Phase, n.Op.Exec, n.Op.FenceBox = "relocating", "pinning", -1, src.ID

+ // the files the relocation installs: region HA §5.6's files

+ // publisher kept the source's files directory in S3 as it served

+ // (L17); this model has no publisher, so the fence takes the

+ // source's directory as published (a stand-in, moves §14.2.6)

+ if src.Files != nil {

+ n.Op.StopFiles = src.Files.clone()

+ }

+ var parts []int

+ for _, p := range n.Op.Parts {

+ if p != src.ID {

+ parts = append(parts, p)

+ }

+ n.Op.Parts = parts

+ n.Lost = addUniq(n.Lost, src.ID)

+ if c.oblFor(op.ID) == 0 {

+ n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH), w.now+stagingTTL, c.Holder.Inc))

+ }

+ return true

+ }) {

+ w.stats["relocation: source fenced before the flip"]++

+ w.logf("move %s: source box %d terminated before the flip; converted to relocating at pinning in region %d", op.ID, src.ID, op.SrcRegion)

+ }

+// relocate is the relocation's worker on a box of the source's region

+// (claim rev 6.28 §4's table, collapsed as this model collapses an install:

+// pinning hands execution to the region's one eligible box with a new

+// installation stamp, the install and the probe are the cold admission's

+// restore of the pinned generation from this region's remote, and the

+// release preserves the outstanding lane park, which is disjoint from the

+// serving location).

+func (w *world) relocate(b *box, c *claim) {

+ op := c.Op

+ if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) {

+ return

+ }

+ switch op.Phase {

+ case "pinning":

+ if op.Exec != -1 {

+ return

+ }

+ if w.cas(c, func(n *claim) bool {

+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "pinning" || n.Op.Exec != -1 {

+ return false

+ }

+ n.Op.Exec, n.Op.Tgt, n.Op.Phase = b.ID, b.ID, "probing"

+ n.Op.Parts = []int{b.ID}

+ n.Boxes = addUniq(n.Boxes, b.ID)

+ n.Holder.Stamp = w.issueStamp(n, b.ID) // a new installation's stamp (claim rev 6.28 §4)

+ return true

+ }) {

+ // the local install (collapsed): the published files directory

+ // (L17) materialized under the new stamp, before the probe

+ if op.StopFiles != nil && b.Files == nil {

+ f := op.StopFiles.clone()

+ f.Done = true

+ b.Files = f

+ }

+ w.logf("relocation %s: box %d takes the host in region %d", op.ID, b.ID, b.Region)

+ }

+ case "probing":

+ if op.Exec != b.ID {

+ return

+ }

+ if b.Row == nil {

+ w.holdRow(b, "landing", op.ID, c)

+ return

+ }

+ if !w.admits(b, c, op.ID) {

+ return

+ }

+ if b.HasKey { // RenderHeld + MaterializeHeld before every probe

+ b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc

+ }

+ if hasMain(b) || w.spawn(b, c, c.Holder.Gen, true) {

+ w.probeAccepted(b, c)

+ w.cas(c, func(n *claim) bool { n.Op.Phase = "probed"; return sameOp(n.Op.ID, op.ID) })

+ return

+ }

+ if b.hostFailed && !b.failCounted {

+ b.failCounted = true

+ } else if b.open != nil || b.hostFailed {

+ return

+ }

+ w.cas(c, func(n *claim) bool {

+ n.Op.ProbeTries++

+ if n.Op.ProbeTries >= probeTries*3 {

+ n.Op.Phase = "stuck"

+ }

+ return sameOp(n.Op.ID, op.ID)

+ })

+ case "probed":

+ if op.Exec != b.ID {

+ return

+ }

+ if b.open != nil {

+ return

+ }

+ if !hasMain(b) {

+ w.stats["probe restarted"]++

+ w.cas(c, func(n *claim) bool { n.Op.Phase = "probing"; return sameOp(n.Op.ID, op.ID) })

+ return

+ }

+ if w.openRow(b, op.ID) {

+ w.cas(c, func(n *claim) bool { n.Op.Phase = "opened"; return sameOp(n.Op.ID, op.ID) })

+ }

+ case "opened":

+ if op.Exec == b.ID {

+ w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4)

+ }

}

@@ -1238,6 +1368,8 @@ func (w *world) release(c *claim, execBox int) {

w.stats["abort"]++

case op.Kind == "pushing":

w.stats["push"]++

+ case op.Kind == "relocating":

+ w.stats["relocation"]++

}

diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go

index e0c6a387f..ec383bb1f 100644

--- a/internal/sim/hostlife/protocol_test.go

+++ b/internal/sim/hostlife/protocol_test.go

@@ -1431,6 +1431,11 @@ func (w *world) admits(b *box, c *claim, probe string) bool {

return role(op.Src) && op.SrcPhase == "opened" && b.Row.Status == "ready"

case "pushing":

return probe == op.ID && op.Phase == "probing"

+ case "relocating":

+ if probe != "" {

+ return probe == op.ID && role(op.Tgt) && op.Phase == "probing"

+ }

+ return role(op.Tgt) && op.Phase == "opened" && b.Row.Status == "ready"

}

return false

}

diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go

index 3efd01d9d..803320fad 100644

--- a/internal/sim/hostlife/rules_test.go

+++ b/internal/sim/hostlife/rules_test.go

@@ -116,6 +116,7 @@ var allRules = []string{

"generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes

"markers-last", // R2-6

"revert-journal", // J-N11

+ "fence-converts-moving", // moves rev 7.20 §7.10, claim rev 6.28 §4: a terminated source of a pre-flip move converts the op to relocating at pinning (exec none, stamp and generation kept, obligations untouched, the lane's park queued); a replacement box of the region takes it; without the rule the move never converges

"rollback-journal", // R2-3

"dirty-return", // INV-2

"seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal

diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go

index 7154794b8..9600d7fd0 100644

--- a/internal/sim/hostlife/witness_test.go

+++ b/internal/sim/hostlife/witness_test.go

@@ -47,6 +47,8 @@ type witness struct {

var witnesses = []witness{

{"generation-conditional", "generation-conditional", "cannot start the host",

"an earlier push's generation.json PUT completes after a later push's; unconditional, it puts the old generation back and the serving box cannot start", wGenerationConditional},

+ {"fence-converts-moving", "fence-converts-moving", "INV-3",

+ "the source of a pre-flip move is terminated in a one-box region; the fence converts the move to relocating at pinning with exec none and the lane's park owed, the operator is alerted once, nothing loops while no box exists, and the relocation completes on the replacement box region HA enrolls; without the rule the move never converges", wFenceConvertsMoving},

{"lost-return-park", "lost-return-park", "ended with residue",

"a target stopped after its first return PUT is declared lost; without the park the lane stays in the source region at the release (INV-10)", wLostReturnPark},

{"declare-lost-compute", "declare-lost-compute", "INV-1",

@@ -702,6 +704,67 @@ func wLostReturnPark(t *testing.T, w *world) {

w.finish(t)

}

+// wFenceConvertsMoving (moves rev 7.20 §7.10, claim rev 6.28 §4): the

+// source of a move that has not flipped is terminated, in a one-box

+// region. The termination fence converts the move to relocating at

+// pinning: exec none, the stamp and generation kept, the lane's park owed

+// to the target region. No box exists in the source region, so the

+// relocation holds there, safely (no writer, the data pinned), the

+// operator is told once, and the claim does not churn. Once region HA

+// enrolls a replacement box (the model's replacement mechanism), the

+// relocation completes on it and the host serves again in its region.

+func wFenceConvertsMoving(t *testing.T, w *world) {

+ src, tgt := w.boxes[0], w.boxes[1]

+ w.serve(src, 1, app0)

+ w.moveTo(tgt.Region)

+ w.reach(t, 100, "staging begins", func() bool {

+ c := w.claim

+ return c.Op.Kind == "moving" && c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region)

+ }, w.act(src, tgt))

+ w.stop(src) // the cloud terminates the source; the regional worker's read is the fence

+ if !w.reach(t, 50, "converted to relocating at pinning", func() bool {

+ c := w.claim

+ return c.Op.Kind == "relocating" && c.Op.Phase == "pinning" && c.Op.Exec == -1

+ }, w.act(tgt), w.recoveryPass) {

+ return // under the mutation the move never converges: reach recorded INV-3

+ }

+ c := w.claim

+ if !contains(c.Lost, src.ID) || c.Op.FenceBox != src.ID || c.oblFor(c.Op.ID) == 0 {

+ t.Fatalf("witness: the conversion did not record the fence and the lane's park: %s", w.state())

+ }

+ // it waits: no box in region 0. Nothing runs, nothing loops; the only

+ // claim writes are the lane park's own steps and the one alert

+ ver, alerts := c.Ver, w.alerts

+ w.drive(200, func() bool { return false }, w.act(tgt), w.recoveryPass, w.operator)

+ c = w.claim

+ if c.Op.Kind != "relocating" || c.Op.Phase != "pinning" || c.Op.Exec != -1 {

+ t.Fatalf("witness: the relocation did not hold at pinning: %s", w.state())

+ }

+ if w.alerts <= alerts {

+ t.Fatalf("witness: no alert for a relocation with no box in its region")

+ }

+ if c.Ver-ver > 8 {

+ t.Fatalf("witness: the claim churned %d times while waiting: %s", c.Ver-ver, w.state())

+ }

+ for _, b := range w.liveBoxes() {

+ if len(b.Procs) > 0 {

+ t.Fatalf("witness: box %d runs the host while the relocation waits", b.ID)

+ }

+ w.replaceDestroyed() // region HA enrolls a replacement box (H16, H17)

+ w.finish(t)

+ if len(w.violations) > 0 {

+ return

+ }

+ if w.stats["relocation"] != 1 {

+ t.Fatalf("witness: the relocation did not complete: %s", w.state())

+ }

+ nb := w.regionBox(src.Region)

+ if e := w.execBox(w.claim); e == nil || nb == nil || e.ID != nb.ID || w.claim.Op.Kind != "serving" {

+ t.Fatalf("witness: the host does not serve on the replacement box: %s", w.state())

+ }

// wDeclareLostCompute (model 5, §7.10): the target is frozen (a whole-VM

// pause) in its settle window; its execution lease expires.

func wDeclareLostCompute(t *testing.T, w *world) {

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index 574134d38..d0a6813e1 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -766,6 +766,13 @@ type opState struct {

// again in the same CAS (FreeAfterPark)

ParkSweep string

+ // FenceBox is the journal's fence.<box> reference (claim rev 6.28,

+ // moves rev 7.20 §7.10): the terminated source whose termination fence

+ // converted a pre-flip move to relocating. Alerted: the operator was

+ // told once that the relocation waits for a box in the region.

+ FenceBox int

+ Alerted bool

// intent

Src, Tgt int

SrcRegion, TgtRegion int