4416b34ce · carlos/platform

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 c8a59c34d..bde830bee 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,22 @@

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

**Date:** 2026-10-06

-**Revision:** 7.22.

-

+**Revision:** 7.23.

+

+- **Rev 7.23** records Paul's ruling M4 (2026-10-10, moves Plan 5 delta

+ pre-flight after claim Plan 10): **every close is record first, then

+ the claim's release.** Rev 7.22 released the claim to `serving` first

+ and cleared `move` second (§7.5, §19 K8). Claim Plan 10's move-recovery

+ grant closes the record first, and a serving claim with a live move

+ record can never acquire that grant, so the two orders could not both

+ stand. Each close (the commit's, a rollback's, a revert's, an abort's)

+ now checks that no obligation of the op remains, CAS-clears `move` into

+ `last_move`, and then releases. A crash between the halves leaves the

+ record at rest and the claim still under the op with nothing owed; the

+ box passes are driven by records with a live move and do not come

+ back, so the console's recovery pass releases from `last_move`.

+ Amended: §7.5, §7.8 finalization, §7.9 step 5, §7.11, the `reverting`

+ table's `opened` row, §14.2.2's model row and §19 K8.

- **Rev 7.22** answers **joint round 19** (`CODEX-FINDINGS-JOINT-R19.md`,

"R19-1", the round's one finding, P2) and fixes the install

manifest's keys. **R19-1:** rev 7.21 bound the prepared files manifest

@@ -2607,7 +2621,7 @@ itself as execution holder, holds the row as `restoring` with

| `verify` | entered from `stopped`, `staged` or `archived`: check files and timers against the digests recorded at `stopped` | replayable **until `probing` is journaled** |

| `probing` | render held config and materialize the release (§7.7), then probe | restarts only the probe. **Never re-runs `verify`**: the probe's process may have written, and those writes are now the authoritative state (INV-2) |

| `probed` | conditional open on `hold_op = move id` | replayable |

-| `opened` | the claim waits for the staging obligation (§7.11), then releases to `serving` | |

+| `opened` | the claim waits for the staging obligation (§7.11); then the record clears (`last_move` = `rolled_back`) and the claim releases to `serving` (record first, §7.5) | |

Rev 3 compared digests again on re-entry, so a crash after the recovery

probe had written left the move stuck on a "mismatch" that was really the

@@ -2657,11 +2671,19 @@ with crashes, console loss and the recovery pass between them (§14.2.2).

The source row stays held (`moving`); reconcile keeps it because the claim

names this box as a participant (§9.6).

-**The close is the other way round.** Releasing to `serving` is a claim

-CAS first (§19 K8), then the record CAS that clears `move` and names the

-executor's region; the recovery pass finishes the second half after a

-crash. Until it lands, the record still carries a finished `move`, which

-admits nothing.

+**The close is record first too (rev 7.23, Paul's ruling M4).** The

+actor that closes first checks that no obligation this op created

+remains, then CASes the record: `move` is cleared and `last_move` names

+the move and its outcome (`done`, `rolled_back` or `aborted`). The claim's

+release to `serving` (§19 K8) is the second CAS, determined by

+`last_move`: the op id, its kind and phase, and the executor the outcome

+names. Until it lands, the claim still holds the op, so nothing else

+starts on the host. After a crash between the two, no box revisits the

+host (the box passes are driven by records with a live move), and the

+console's recovery pass writes the release from `last_move`. Rev 7.22

+had this the other way round, claim first; claim Plan 10's recovery

+grant can act only while the claim holds the move op, so a claim

+released over a live `move` could never be finished by it.

**Late record writes.** Every move write to the record is a conditional

CAS. One that completes after its client gave up either still matches,

@@ -2873,9 +2895,9 @@ install supersedes. These are the claim spec's durable chores (§2 there);

**Finalization:** when `recovered_at`, `opened_at` and `target_parked_at`

are all stamped, and no obligation this op created remains, whichever

actor stamps last writes the terminal log event (`rolled_back`, with every

-timing, digest and reason), releases the claim to `serving` (§19 K8), and

-CAS-clears `move`. Until then `move` and the claim stay, so nothing else

-can start on the host (codex 6). The source serves from `opened` on; the

+timing, digest and reason), CAS-clears `move`, and then releases the

+claim to `serving` (§19 K8; record first, §7.5). Until then `move` and

+the claim stay, so nothing else can start on the host (codex 6). The source serves from `opened` on; the

held claim blocks only other operations.

Nine failed recovery probe attempts (three times the landing's budget of

@@ -2917,8 +2939,9 @@ runs anywhere. It converges when the target returns (INV-3).

`moves/<host>/`): `moves/<host>/<move id>/` into

`superseded/<move id>/<host>/`; remove its obligation.

5. **Close** (when both obligations are gone): terminal log event `done`;

- release the claim to `serving` with the target as execution holder

- (§19 K8); CAS-clear `move`.

+ CAS-clear `move` (`last_move` = `done`); then release the claim to

+ `serving` with the target as execution holder (§19 K8; record first,

+ §7.5).

### 7.10 Stuck and declare-lost (M16)

@@ -3068,7 +3091,8 @@ source retires them from its own bucket, every version of

`move-snapshots/<host>/<op>/` through `DeleteVersion`; that prefix is outside

the park scope grammar, and F3's retention of snapshots covers completed

moves only.) The claim stays `moving` until every obligation

-has acknowledged, then releases to `serving`. The model gives the source

+has acknowledged; then the record clears (`last_move` = `aborted`) and

+the claim releases to `serving` (record first, §7.5). The model gives the source

the target's park and records an IAM violation on every abort.

### 7.12 Deletes and parks under the claim

@@ -3824,7 +3848,7 @@ the text. What changed, and what did not:

|---|---|

| restore stronger than the spec (an exact base pointer, historical lineage selection) | restore reads `holder.location` and `holder.generation` and replays every object of that generation (§5.1). The mutation restores the newest object under the location |

| the start check stronger than the spec (compared with the committed lineage) | the start check compares the box's own three markers with each other and, as a separate rule, with the claim's generation (§5.1); rev 5's check is the mutation |

-| claim transitions followed by an atomic record write | record-first flip, commit and rollback, then the claim half as a separate step, written by the actor, the other participant or the recovery pass; the close the other way round (§7.5) |

+| claim transitions followed by an atomic record write | record-first flip, commit and rollback, then the claim half as a separate step, written by the actor, the other participant or the recovery pass; the close record first too, then the claim's release, which the recovery pass finishes from `last_move` after a crash (§7.5, rev 7.23) |

| every request completes by `issue + H` | one long-tail request in 20 completes up to 11 `H` late, after publication and after retirement; the restore contract keeps them out of data, the sweep retires them (§5.1, §6.4) |

| check and sign, check and local write, atomic | staging writers sign at the check and may then pause, a frozen box without bound (§7.3); host-guard writers are independent processes (`carlos-config-sync`, `carlos-adopt`) that survive an agent crash, pause before the guard and re-validate under it (claim §6.4); door listings read O1, pause, select, read O2 (claim §6.5) |

| atomic `localPark` | one artifact per step, the retired marker first |

@@ -6350,7 +6374,7 @@ The db door refuses on every move kind (claim spec §8).

| **K5 Revalidation** | Before each destructive step the actor re-reads the claim and requires op id, kind, phase and `exec` to be what the step expects (claim spec C3); it holds the lease of every location it writes, acting before `SafeUntil`, with the exception in §19.3 D4. A staging writer checks `SafeUntil` immediately before it signs each request, after any pause (§7.3, model 14). |

| **K6 Wake admission** | `doWake` reads the claim fresh (claim spec §8) and applies K1. A box that reads a claim whose `exec` does not name it kills that host's process tree (§5.3 step 1) before anything else. |

| **K7 Other operations** | Delete, purge, park and push start only from `serving` (claim spec §4); while a move op holds the claim they are refused. Create requires free or absent. |

-| **K8 Release** | Only the move releases to `serving`, naming `exec` (target after `done`; source after `rolled_back` or `aborted`), and only when every obligation this op created is gone (§7.8, §7.9). |

+| **K8 Release** | Only the move releases to `serving`, naming `exec` (target after `done`; source after `rolled_back` or `aborted`), and only when every obligation this op created is gone (§7.8, §7.9). The release follows the record's close: the closing actor checks that nothing is owed under the op, CAS-clears `move` into `last_move`, then releases; the console's recovery pass finishes the release from `last_move` after a crash (§7.5; rev 7.23, Paul's ruling M4). |

| **K9 Other passes while a move op holds the claim** | Reconcile mints participant rows held and never `ready`, and never removes or orphan-retires a participant row; the schedule converger neither upserts nor prunes the host's timers; `SyncExec` and release adoption skip the held rows (they already skip non-`ready`). |

| **K10 Version floor** | The claim spec's floor (§9 there) and `moves_protocol` (§11) are one object and one check. |

| **K11 Declare-lost** | §7.10; §19.3 D6. |

diff --git a/internal/host/movesabort.go b/internal/host/movesabort.go

index 7f1ecd3e1..23a9a25f9 100644

--- a/internal/host/movesabort.go

+++ b/internal/host/movesabort.go

@@ -49,13 +49,16 @@ import (

// release, and is a no-op once everything is gone: nothing infers from

// a missing journal that it already ran, and any error (a listing, a

// delete, the journal directory) ends the pass unreleased;

-// 5. it waits until no obligation under the op remains, then releases with

-// hostclaim.ReleaseAbort (K7: from moving/aborting only, so never before

-// the lane park was queued), and last clears the record with

-// provision.MoveGuardedAbortComplete (§7.5: the claim releases first,

-// the record clears second). A round that finds the claim already

-// serving and recording this move's release completes the record; any

-// other serving claim is left alone.

+// 5. it waits until no obligation under the op remains, then clears the

+// record with provision.MoveGuardedAbortComplete, and last releases

+// with hostclaim.ReleaseAbort (K7: from moving/aborting only, so never

+// before the lane park was queued). Record first, then the claim's

+// release (§7.5 and §19 K8 as Paul's ruling M4 amends them): a crash

+// between leaves the record at rest and the claim moving/aborting with

+// nothing owed, and the console's recovery pass releases from LastMove

+// (Plan 5 Task 7). A round that finds the claim already serving and

+// recording this move's release (a binary that closed claim first)

+// completes the record; any other serving claim is left alone.

//

// The target region's box, for a record aborting whose To is its region:

// movesParticipantRecord answers it as the target on the state alone (the

@@ -105,6 +108,7 @@ func (w *movesWorker) abortSource(ctx context.Context, s release.Store, rec prov

}

op := obs.Claim.Op

mine := op.Kind == hostclaim.KindMoving && op.ID == id

+ releaseAfter := false

switch {

case mine && op.Exec != cfg.Box:

w.notice(rec.Host+"#abort", "moves: %s: aborting move %s: the claim's executor is %q, not this box; left for the console pass", rec.Host, id, op.Exec)

@@ -122,19 +126,23 @@ func (w *movesWorker) abortSource(ctx context.Context, s release.Store, rec prov

}

fallthrough

case mine && op.Phase == hostclaim.PhaseAborting:

- // Every pass, before the release: the retirement is idempotent, and

- // a release never follows from inferring that it already ran (fix

+ // Every pass, before the close: the retirement is idempotent, and

+ // a close never follows from inferring that it already ran (fix

// round 1). Any error, the journal directory's included, ends the

- // pass with the claim still aborting.

+ // pass with the record and the claim still aborting.

if err := w.retireOwnMoveState(ctx, rec); err != nil {

return err

}

- if released, err := w.releaseAbort(ctx, s, rec, obs); err != nil || !released {

- return err

+ // Nothing owed under the op, checked before the record's close

+ // (ruling M4), as the console's grant checks it.

+ if w.abortOwes(rec, obs) {

+ return nil

}

+ releaseAfter = true

case hostclaim.RequireReleasedMove(id)(obs.Claim) == nil:

- // This abort released the claim before a crash: finish. The own

- // state went before the release; retiring it again is a no-op.

+ // A binary that closed claim first released before a crash:

+ // finish the record. The own state went before the release;

+ // retiring it again is a no-op.

if err := w.retireOwnMoveState(ctx, rec); err != nil {

return err

}

@@ -152,7 +160,13 @@ func (w *movesWorker) abortSource(ctx context.Context, s release.Store, rec prov

}

nudgeSerial(ctx, s)

log.Printf("moves: %s: move %s aborted; the instance stays in %q", rec.Host, id, rec.Region)

- return nil

+ if !releaseAfter {

+ return nil

+ }

+ if err := w.abFault("after-abort-record"); err != nil {

+ return err

+ }

+ return w.releaseAbort(ctx, s, rec)

}

// abortClaim is steps 1 to 3: the staging lease, the journalled bound and

@@ -225,23 +239,27 @@ func (w *movesWorker) abortClaim(ctx context.Context, s release.Store, rec provi

return true, nil

}

-// releaseAbort is step 5: the release once no obligation of the op remains.

-// released is false while the lane park is still owed.

-func (w *movesWorker) releaseAbort(ctx context.Context, s release.Store, rec provision.Record, obs hostclaim.Observed) (bool, error) {

+// abortOwes is step 5's wait: true, with a notice, while an obligation of

+// the op remains (the lane park the target region has not acknowledged).

+func (w *movesWorker) abortOwes(rec provision.Record, obs hostclaim.Observed) bool {

id := rec.Move.ID

for _, o := range obs.Claim.Obligations {

if o.Op == id {

w.notice(rec.Host+"#abort-wait", "moves: %s: aborting move %s waits for %s to park the staging lane (%s %s)", rec.Host, id, rec.Move.To, o.Kind, o.Region+o.Box)

- return false, nil

+ return true

}

- if _, err := hostclaim.Update(ctx, s, obs, hostclaim.ReleaseAbort(id, w.cfg.Box)); err != nil {

- return false, fmt.Errorf("release the host claim: %w", err)

- }

- if err := w.abFault("after-release-abort"); err != nil {

- return false, err

+ return false

+}

+

+// releaseAbort is step 5's second half: the record already says aborted, so

+// hostclaim.ReleaseAbort from a fresh read. A failure is left to the

+// console's recovery pass, which releases from LastMove.

+func (w *movesWorker) releaseAbort(ctx context.Context, s release.Store, rec provision.Record) error {

+ if err := releaseAfterClose(ctx, s, rec.Host, rec.Move.ID, hostclaim.ReleaseAbort(rec.Move.ID, w.cfg.Box)); err != nil {

+ return err

}

- return true, nil

+ return w.abFault("after-release-abort")

}

// retireOwnMoveState is step 4: the move's snapshots in this box's own

diff --git a/internal/host/movesclose_order_test.go b/internal/host/movesclose_order_test.go

new file mode 100644

index 000000000..5182afef2

--- /dev/null

+++ b/internal/host/movesclose_order_test.go

@@ -0,0 +1,135 @@

+package host

+

+import (

+ "context"

+ "strings"

+ "testing"

+ "time"

+

+ "github.com/carlosframework/platform/internal/hostclaim"

+ "github.com/carlosframework/platform/internal/provision"

+)

+

+// Paul's ruling M4 (2026-10-10; spec §7.5, §19 K8): every move close is

+// record first, then the claim's release. Each box close checks that nothing

+// is owed under the op, clears the record's move into LastMove, and only then

+// releases the claim. A crash between the two halves leaves the record closed

+// and the claim still under the move; the box pass is driven by records with

+// a live move, so it never comes back, and the console's recovery pass

+// releases from LastMove (internal/console, TestRecordFirstCloseCrashIsFinishedByThePass).

+//

+// Each case crashes at "after-close-record", the seam between the halves,

+// and asserts the crash state: the record at rest with the outcome, the

+// claim still in the move's closing op with nothing owed, and a further

+// pass of every box writes nothing.

+

+// closedButHeld asserts the state between the halves of a record-first

+// close: the record closed with outcome, the claim still at kind/phase under

+// the move with nothing owed under it.

+func closedButHeld(t *testing.T, rec provision.Record, c *hostclaim.Claim, outcome, kind, phase string) {

+ t.Helper()

+ if rec.Move != nil || rec.LastMove == nil || rec.LastMove.ID != p1ID || rec.LastMove.Outcome != outcome {

+ t.Fatalf("the record between the halves: move %+v last %+v, want closed %s", rec.Move, rec.LastMove, outcome)

+ }

+ if c.Op.ID != p1ID || c.Op.Kind != kind || c.Op.Phase != phase {

+ t.Fatalf("the claim between the halves: %+v, want %s/%q under %s (the release is second)", c.Op, kind, phase, p1ID)

+ }

+ for _, o := range c.Obligations {

+ if o.Op == p1ID {

+ t.Fatalf("the record closed while %s %s%s was still owed under the op", o.Kind, o.Region, o.Box)

+ }

+}

+

+func TestBoxClosesAreRecordFirst(t *testing.T) {

+ t.Run("committed close (movesparks.go)", func(t *testing.T) {

+ h := newCloseHarness(t)

+ h.land(t)

+ h.sourcePass(t)

+ h.clock.Advance(24 * time.Hour)

+ if err := h.regionalAck(t, h.chore(t, "ie", false)); err != nil {

+ t.Fatal(err)

+ }

+ h.landAt = "after-close-record"

+ h.crashLand(t)

+ closedButHeld(t, h.read(t, p1Host), h.claim(t), "done", hostclaim.KindLanding, hostclaim.PhaseCommitted)

+ gen := h.claim(t).Gen

+ h.freshTarget()

+ h.land(t)

+ h.sourcePass(t)

+ if c := h.claim(t); c.Gen != gen {

+ t.Fatalf("a box pass after the record's close wrote the claim (%d to %d): %+v", gen, c.Gen, c.Op)

+ }

+ })

+ t.Run("abort (movesabort.go)", func(t *testing.T) {

+ h := newAbortHarness(t)

+ h.abort(t)

+ h.abAt = "after-abort-record"

+ for i := 0; i < 6 && !h.abDone; i++ {

+ movesPass(context.Background(), h.s, h.w())

+ h.tPass(t)

+ if o := h.laneChore(t); o != nil {

+ h.pastHorizon(t, o)

+ h.tPass(t)

+ }

+ if !h.abDone {

+ t.Fatalf("never reached after-abort-record (%v)", h.abHits)

+ }

+ closedButHeld(t, h.read(t, p1Host), h.claim(t), "aborted", hostclaim.KindMoving, hostclaim.PhaseAborting)

+ h.ownStateGone(t)

+ gen := h.claim(t).Gen

+ h.worker1 = nil

+ h.pass(t)

+ h.tPass(t)

+ if c := h.claim(t); c.Gen != gen {

+ t.Fatalf("a box pass after the record's close wrote the claim (%d to %d): %+v", gen, c.Gen, c.Op)

+ }

+ })

+ t.Run("recovery close (movesrecover.go)", func(t *testing.T) {

+ h := newRecoverHarness(t, false)

+ h.released(t)

+ h.srcPass(t)

+ h.opened(t)

+ h.rcAt = "after-close-record"

+ h.closeOut(t)

+ if !h.rcDone {

+ t.Fatalf("never reached after-close-record (%v)", h.rcHits)

+ }

+ closedButHeld(t, h.read(t, p1Host), h.claim(t), "rolled_back", hostclaim.KindRestoring, hostclaim.PhaseOpened)

+ if n := strings.Count(strings.Join(h.sEvents, " "), "rolled_back"); n != 1 {

+ t.Fatalf("the terminal event %d times: %v", n, h.sEvents)

+ }

+ gen := h.claim(t).Gen

+ h.sw = nil

+ h.srcPass(t)

+ h.rollbackPass(t)

+ if c := h.claim(t); c.Gen != gen {

+ t.Fatalf("a box pass after the record's close wrote the claim (%d to %d): %+v", gen, c.Gen, c.Op)

+ }

+ })

+ t.Run("revert close (movesrevert.go)", func(t *testing.T) {

+ h := newRevertHarness(t)

+ h.fromStopped(t)

+ h.arm(t)

+ h.pass(t)

+ h.reopened(t)

+ h.rvAt = "after-close-record"

+ o := h.laneChore(t)

+ h.tPass(t)

+ h.pastHorizon(t, o)

+ h.tPass(t)

+ h.pass(t)

+ if !h.rvDone {

+ t.Fatalf("never reached after-close-record (%v)", h.rvHits)

+ }

+ closedButHeld(t, h.read(t, p1Host), h.claim(t), "rolled_back", hostclaim.KindReverting, hostclaim.PhaseOpened)

+ gen := h.claim(t).Gen

+ h.freshWorker()

+ h.pass(t)

+ h.tPass(t)

+ if c := h.claim(t); c.Gen != gen {

+ t.Fatalf("a box pass after the record's close wrote the claim (%d to %d): %+v", gen, c.Gen, c.Op)

+ }

+ })

+}

diff --git a/internal/host/moveslandcommit.go b/internal/host/moveslandcommit.go

index 2a564e71b..721073acf 100644

--- a/internal/host/moveslandcommit.go

+++ b/internal/host/moveslandcommit.go

@@ -97,8 +97,8 @@ func (w *movesWorker) committedTarget(ctx context.Context, s release.Store, rec

return fmt.Errorf("read the host claim: %w", err)

}

if !obs.Absent && hostclaim.RequireReleasedMove(m.ID)(obs.Claim) == nil {

- // The close released the claim and stopped before the record's

- // half (§7.5): only that is left.

+ // A binary that closed claim first released the claim and stopped

+ // before the record's half: only that is left (closeMove).

return w.closeMove(ctx, s, rec, l.fault)

}

if err := l.commitClaim(ctx); err != nil {

diff --git a/internal/host/movesparks.go b/internal/host/movesparks.go

index 0e515bf47..9ec7aa2d6 100644

--- a/internal/host/movesparks.go

+++ b/internal/host/movesparks.go

@@ -31,15 +31,17 @@ import (

// Step 5, the close (closeMove). Any participant that sees opened_at and

// source_parked_at on the record and no obligation of the op in the claim

// closes: the terminal event `done` (moves.LogEvent when the hook is wired,

-// Plan 6; a log line until then), then hostclaim.ReleaseMove to serving under

-// the target (§19 K8: the claim first), then provision.MoveClose (the record

-// last: LastMove{Outcome: "done"}, index D11). A crash between the two

-// leaves a finished move on the record that admits nothing (MoveRequest

-// refuses while Move is set), and the next pass of the target finds the

-// claim recording this move's release and writes only the record's close.

-// The target calls it every committed pass; the source calls it in the pass

-// that stamps source_parked_at, which is the last pass that routes the

-// record to it. The console's recovery pass also tries (Task 7).

+// Plan 6; a log line until then), then provision.MoveClose (the record

+// first: LastMove{Outcome: "done"}, index D11), then hostclaim.ReleaseMove

+// to serving under the target (§7.5, §19 K8 as Paul's ruling M4 amends

+// them: record first, then the claim's release). A crash between the two

+// leaves the record at rest and the claim still landing/committed with

+// nothing owed; no box pass visits a record without a move again, and the

+// console's recovery pass releases from LastMove (Recovery.Moves, Plan 5

+// Task 7). A claim found already released by this move (a binary that

+// closed claim first) gets only the record's close. The target calls it

+// every committed pass; the source calls it in the pass that stamps

+// source_parked_at, which is the last pass that routes the record to it.

//

// Production (K4). The staging park and the close are production-live only

// after Plan 5 Task 9 (park arming) and claim Plans 10 and 11. The committed

@@ -51,9 +53,9 @@ import (

// then the tests arm everything with fakes.

// closeMove is the close (§7.9 step 5; see the file comment). fault is the

-// caller's test seam, passed "after-close-release" between the claim's

-// release and the record's close. It does nothing until the record carries

-// both stamps and the claim owes nothing under the op.

+// caller's test seam, passed "after-close-record" between the record's close

+// and the claim's release. It does nothing until the record carries both

+// stamps and the claim owes nothing under the op.

func (w *movesWorker) closeMove(ctx context.Context, s release.Store, rec provision.Record, fault func(string) error) error {

host, id, inc := rec.Host, rec.Move.ID, rec.Move.Incarnation

fresh, err := provision.GetRecord(ctx, s, rec.Account, rec.App, host)

@@ -79,7 +81,11 @@ func (w *movesWorker) closeMove(ctx context.Context, s release.Store, rec provis

return fmt.Errorf("move %s has no host claim", id)

}

c := obs.Claim

- if hostclaim.RequireReleasedMove(id)(c) != nil {

+ // A claim this move already released was released by a binary that

+ // closed claim first: only the record's half is left.

+ released := hostclaim.RequireReleasedMove(id)(c) == nil

+ target := ""

+ if !released {

if c.Op.ID != id || c.Op.Kind != hostclaim.KindLanding || c.Op.Phase != hostclaim.PhaseCommitted || len(c.Op.Participants) != 2 {

w.notice(host+"#close", "moves: %s: move %s waits to close: the claim is %s/%q (%s), not this move's commit", host, id, c.Op.Kind, c.Op.Phase, c.Op.ID)

return nil

@@ -87,27 +93,15 @@ func (w *movesWorker) closeMove(ctx context.Context, s release.Store, rec provis

if c.Holder == nil || c.Holder.Incarnation != inc {

return fmt.Errorf("move %s: the host claim names another incarnation", id)

}

- owed := 0

- for _, o := range c.Obligations {

- if o.Op == id {

- owed++

- }

- if owed > 0 {

+ // Nothing owed under the op, checked here before the record's

+ // close (M4), as the console's grant checks it: a record closed

+ // over an owed chore would leave a release ReleaseMove refuses.

+ if owed := owedUnder(c, id); owed > 0 {

w.notice(host+"#close", "moves: %s: move %s waits for %d park(s) of the move to be acknowledged before it closes", host, id, owed)

return nil

}

+ target = c.Op.Participants[1]

w.logEvent(ctx, *fresh, "done")

- target := c.Op.Participants[1]

- if _, err := hostclaim.Update(ctx, s, obs, hostclaim.ReleaseMove(id, target)); err != nil {

- return fmt.Errorf("release the claim: %w", err)

- }

- log.Printf("moves: %s: the claim is serving under %s after move %s", host, target, id)

- if fault != nil {

- if err := fault("after-close-release"); err != nil {

- return err

- }

}

g := provision.MoveGuard{ID: id, Incarnation: inc}

if _, err := provision.SetRecordMove(ctx, s, fresh.Account, fresh.App, host, provision.MoveClose(g, w.now())); err != nil {

@@ -119,5 +113,52 @@ func (w *movesWorker) closeMove(ctx context.Context, s release.Store, rec provis

}

log.Printf("moves: %s: move %s is done; the instance is in %s", host, id, m.To)

nudgeSerial(ctx, s)

+ if released {

+ return nil

+ }

+ if fault != nil {

+ if err := fault("after-close-record"); err != nil {

+ return err

+ }

+ if err := releaseAfterClose(ctx, s, host, id, hostclaim.ReleaseMove(id, target)); err != nil {

+ return err

+ }

+ log.Printf("moves: %s: the claim is serving under %s after move %s", host, target, id)

+ return nil

+}

+

+// owedUnder counts the obligations of the claim under op id.

+func owedUnder(c *hostclaim.Claim, id string) int {

+ owed := 0

+ for _, o := range c.Obligations {

+ if o.Op == id {

+ owed++

+ }

+ return owed

+}

+

+// releaseAfterClose is the second half of every box close (ruling M4): the

+// record already carries the outcome in LastMove, so the claim is released

+// from a fresh read with the op's own release transition. A claim this move

+// already released (the console's pass finished it first) is success. Any

+// other failure is returned and left to the console's recovery pass, which

+// releases from LastMove: the box pass never visits a record without a move

+// again.

+func releaseAfterClose(ctx context.Context, s release.Store, host, id string, release func(*hostclaim.Claim) error) error {

+ obs, err := hostclaim.Read(ctx, s, host)

+ if err != nil {

+ return fmt.Errorf("read the host claim to release move %s: %w", id, err)

+ }

+ if obs.Absent {

+ return fmt.Errorf("move %s has no host claim to release", id)

+ }

+ if hostclaim.RequireReleasedMove(id)(obs.Claim) == nil {

+ return nil

+ }

+ if _, err := hostclaim.Update(ctx, s, obs, release); err != nil {

+ return fmt.Errorf("release the claim after the close of move %s (the console's recovery pass finishes it): %w", id, err)

+ }

return nil

}

diff --git a/internal/host/movesparks_test.go b/internal/host/movesparks_test.go

index 53f8e434a..ec4613b75 100644

--- a/internal/host/movesparks_test.go

+++ b/internal/host/movesparks_test.go

@@ -222,11 +222,15 @@ func TestCloseWaitsForBothObligations(t *testing.T) {

}

-// TestCloseIsRecordLast (§7.5, §19 K8): the close releases the claim before

-// it clears the record. A crash between leaves a finished move on the

-// record, which admits nothing (no new move starts over it), and the next

-// pass clears it without writing the claim again.

-func TestCloseIsRecordLast(t *testing.T) {

+// TestCloseIsRecordFirst (§7.5, §19 K8 as Paul's ruling M4 amends them):

+// the close clears the record before it releases the claim. A crash between

+// leaves the record at rest with LastMove done and the claim

+// landing/committed with nothing owed; no new move can start (the claim is

+// not serving), and no box pass writes the claim again: the release is the

+// console's recovery pass (TestBoxClosesAreRecordFirst; the console's

+// TestRecordFirstCloseCrashIsFinishedByThePass). Without a crash the same

+// pass releases.

+func TestCloseIsRecordFirst(t *testing.T) {

h := newCloseHarness(t)

h.land(t)

h.sourcePass(t)

@@ -234,26 +238,36 @@ func TestCloseIsRecordLast(t *testing.T) {

if err := h.regionalAck(t, h.chore(t, "ie", false)); err != nil {

t.Fatal(err)

}

- h.landAt = "after-close-release"

+ h.landAt = "after-close-record"

h.crashLand(t)

rec := h.read(t, p1Host)

- if rec.Move == nil || rec.Move.State != provision.MoveCommitted || rec.LastMove != nil {

- t.Fatalf("the record cleared before the claim released: %+v %+v", rec.Move, rec.LastMove)

+ if rec.Move != nil || rec.LastMove == nil || rec.LastMove.Outcome != "done" {

+ t.Fatalf("the record did not close first: %+v %+v", rec.Move, rec.LastMove)

}

c := h.claim(t)

- if c.Op.Kind != hostclaim.KindServing || c.Op.Exec != "uk-box" || hostclaim.RequireReleasedMove(p1ID)(c) != nil {

+ if c.Op.Kind != hostclaim.KindLanding || c.Op.Phase != hostclaim.PhaseCommitted || c.Op.ID != p1ID {

t.Fatalf("the claim at the crash point: %+v", c.Op)

}

- if _, err := provision.SetRecordMove(context.Background(), h.s, "bab", "app", p1Host, provision.MoveRequest("ie", h.clock.Now())); !errors.Is(err, provision.ErrMoveConflict) {

- t.Fatalf("a new move started over the finished one: %v", err)

+ if err := hostclaim.StartGuard(c, []string{"uk"}, []string{"uk-box"}); err == nil {

+ t.Fatal("a new operation could start over the unreleased claim")

}

gen := c.Gen

h.freshTarget()

h.land(t)

- h.done(t)

if after := h.claim(t).Gen; after != gen {

- t.Fatalf("the record's close wrote the claim again (%d to %d)", gen, after)

+ t.Fatalf("a box pass after the record's close wrote the claim (%d to %d)", gen, after)

+ }

+

+ // Without the crash, the pass that closes the record releases.

+ h2 := newCloseHarness(t)

+ h2.land(t)

+ h2.sourcePass(t)

+ h2.clock.Advance(24 * time.Hour)

+ if err := h2.regionalAck(t, h2.chore(t, "ie", false)); err != nil {

+ t.Fatal(err)

}

+ h2.land(t)

+ h2.done(t)

}

// Any participant that sees both stamps and nothing owed closes (§7.9 step

@@ -262,8 +276,8 @@ func TestCloseIsRecordLast(t *testing.T) {

func TestTheSourceClosesWhenItFinishesLast(t *testing.T) {

h := newCloseHarness(t)

h.landFault = func(point string) error {

- if point == "after-close-release" {

- t.Fatal("the target released before the source parked")

+ if point == "after-close-record" {

+ t.Fatal("the target closed before the source parked")

}

return nil

}

diff --git a/internal/host/movesrecover.go b/internal/host/movesrecover.go

index db4e59706..a1fd78401 100644

--- a/internal/host/movesrecover.go

+++ b/internal/host/movesrecover.go

@@ -82,10 +82,11 @@ import (

// - opened: the finalization. Once recovered_at, opened_at and

// target_parked_at are stamped and no obligation of the op remains in

// the claim, the terminal event (LogEvent, Plan 6's moves.LogEvent),

-// the claim's release to serving (ReleaseMove) and the record's close

-// (MoveRolledBackClose). Whichever actor stamps last tries; the

-// source's next pass, and Plan 5's console pass, finish what a crash

-// leaves.

+// the record's close (MoveRolledBackClose) and then the claim's

+// release to serving (ReleaseMove): record first, ruling M4. Whichever

+// actor stamps last tries; a crash before the record's close is the

+// source's next pass, and one after it the console's recovery pass

+// (Plan 5 Task 7), which releases from LastMove.

//

// Every record write goes through a provision transition (the record_seq

// rule); every claim write through a hostclaim transition.

@@ -768,9 +769,12 @@ func (r *recoverRun) open(ctx context.Context) (bool, error) {

// finalize (§7.8 rolled_back): with the source opened and recovered and the

// target parked, and no obligation of the op left in the claim, the

-// terminal event, the claim's release to serving and the record's close. A

-// claim already released by this move (a crash before the close) only

-// closes.

+// terminal event, the record's close, then the claim's release to serving:

+// record first (§7.5 and §19 K8 as Paul's ruling M4 amends them). A crash

+// between the halves leaves the record at rest and the claim

+// restoring/opened with nothing owed; the console's recovery pass releases

+// from LastMove. A claim already released by this move (a binary that

+// closed claim first) only closes.

func (r *recoverRun) finalize(ctx context.Context) (bool, error) {

cfg := r.cfg()

host, id, rb := r.rec.Host, r.g.ID, r.rollback()

@@ -785,31 +789,21 @@ func (r *recoverRun) finalize(ctx context.Context) (bool, error) {

if obs.Absent {

return false, fmt.Errorf("move %s has no host claim", id)

}

- if hostclaim.RequireReleasedMove(id)(obs.Claim) != nil {

+ released := hostclaim.RequireReleasedMove(id)(obs.Claim) == nil

+ if !released {

if err := r.ours(obs.Claim); err != nil {

return false, fmt.Errorf("move %s: %w", id, err)

}

if err := r.executing(obs.Claim, hostclaim.PhaseOpened); err != nil {

return false, err

}

- owed := 0

- for _, o := range obs.Claim.Obligations {

- if o.Op == id {

- owed++

- }

- if owed > 0 {

+ // Nothing owed under the op, checked before the record's close

+ // (M4), as the console's grant checks it.

+ if owed := owedUnder(obs.Claim, id); owed > 0 {

r.w.notice(host+"#rc-final", "moves: %s: rollback %s waits for %d chore(s) of the move to be acknowledged before it closes", host, r.rb, owed)

return false, nil

}

r.w.logEvent(ctx, r.rec, "rolled_back")

- if _, err := hostclaim.Update(ctx, r.s, obs, hostclaim.ReleaseMove(id, cfg.Box)); err != nil {

- return false, fmt.Errorf("release the claim: %w", err)

- }

- log.Printf("moves: %s: the claim is serving again after rollback %s", host, r.rb)

- if err := r.fault("after-release-move"); err != nil {

- return false, err

- }

}

if _, err := provision.SetRecordMove(ctx, r.s, r.rec.Account, r.rec.App, host, provision.MoveRolledBackClose(r.g, r.now())); err != nil {

if errors.Is(err, provision.ErrMoveConflict) {

@@ -820,6 +814,18 @@ func (r *recoverRun) finalize(ctx context.Context) (bool, error) {

}

log.Printf("moves: %s: move %s is rolled back and closed", host, id)

nudgeSerial(ctx, r.s)

+ if !released {

+ if err := r.fault("after-close-record"); err != nil {

+ return true, err

+ }

+ if err := releaseAfterClose(ctx, r.s, host, id, hostclaim.ReleaseMove(id, cfg.Box)); err != nil {

+ return true, err

+ }

+ log.Printf("moves: %s: the claim is serving again after rollback %s", host, r.rb)

+ if err := r.fault("after-release-move"); err != nil {

+ return true, err

+ }

if err := r.fault("after-close"); err != nil {

return true, err

}

diff --git a/internal/host/movesrecover_test.go b/internal/host/movesrecover_test.go

index 928368cb6..f0174bb47 100644

--- a/internal/host/movesrecover_test.go

+++ b/internal/host/movesrecover_test.go

@@ -612,10 +612,11 @@ func TestSourceRecoveryNeverReverifiesAfterProbing(t *testing.T) {

// TestRolledBackFinalizationReleasesTheClaim (§7.8 rolled_back): once the

// source has opened and the target has parked, and no obligation of the op

-// remains, the source writes the terminal event, releases the claim to

-// serving and closes the record with the rolled_back outcome. Until every

-// chore is acknowledged it waits; a crash between the claim's release and

-// the record's close is finished by the next pass.

+// remains, the source writes the terminal event, closes the record with the

+// rolled_back outcome and releases the claim to serving, in that order

+// (ruling M4). Until every chore is acknowledged it waits; a crash between

+// the record's close and the release is the console's to finish

+// (TestBoxClosesAreRecordFirst).

func TestRolledBackFinalizationReleasesTheClaim(t *testing.T) {

ctx := context.Background()

h := newRecoverHarness(t, false)

@@ -655,11 +656,7 @@ func TestRolledBackFinalizationReleasesTheClaim(t *testing.T) {

t.Fatal(err)

}

- h.rcAt = "after-release-move"

h.srcPass(t)

- if !h.rcDone {

- t.Fatalf("never reached the claim's release (%v)", h.rcHits)

- }

c := h.claim(t)

if c.Op.Kind != hostclaim.KindServing || c.Op.Exec != "ie-box" {

t.Fatalf("the claim was not released: %+v", c.Op)

@@ -667,8 +664,6 @@ func TestRolledBackFinalizationReleasesTheClaim(t *testing.T) {

if err := hostclaim.RequireReleasedMove(p1ID)(c); err != nil {

t.Fatal(err)

}

- h.sourceAt(t, provision.RbSourceOpened)

- h.srcPass(t)

rec := h.read(t, p1Host)

if rec.Move != nil || rec.LastMove == nil || rec.LastMove.ID != p1ID || rec.LastMove.Outcome != "rolled_back" || rec.Region != "ie" {

t.Fatalf("not closed: region %s move %+v last %+v", rec.Region, rec.Move, rec.LastMove)

diff --git a/internal/host/movesrevert.go b/internal/host/movesrevert.go

index 406b0294e..dfa54e91d 100644

--- a/internal/host/movesrevert.go

+++ b/internal/host/movesrevert.go

@@ -69,13 +69,15 @@ import (

// - opened: the claim waits for the lane's park the revert queued in the

// target region (§7.11), which the target region's box runs

// (laneParkTarget) and the park engine acknowledges after its horizon.

-// Then ReleaseMove to serving under this box, and MoveRevertClose:

-// LastMove rolled_back, offline from cut_at to the reopen. The source's

-// journal of the op is parked in the same pass; a crash before that

-// leaves it to the local journal sweep (sweepRevertJournal).

+// Then MoveRevertClose (LastMove rolled_back, offline from cut_at to

+// the reopen), and then ReleaseMove to serving under this box: record

+// first, ruling M4; a crash between is finished by the console's

+// recovery pass from LastMove. The source's journal of the op is parked

+// in the same pass; a crash before that leaves it to the local journal

+// sweep (sweepRevertJournal).

//

-// A claim this move already released (RequireReleasedMove: a crash before the

-// record's close) only closes.

+// A claim this move already released (RequireReleasedMove: a binary that

+// closed claim first crashed before the record's close) only closes.

//

// The target region's half (laneParkTarget). A revert never flipped, so its

// target box has neither the row nor a journal of the move; the participant

@@ -310,8 +312,9 @@ func (r *revertRun) step(ctx context.Context) (bool, error) {

}

c := obs.Claim

if hostclaim.RequireReleasedMove(id)(c) == nil {

- // A crash between the claim's release and the record's close.

- return r.close(ctx)

+ // A binary that closed claim first crashed between the claim's

+ // release and the record's close: only the record's half is left.

+ return r.close(ctx, false)

}

if c.Op.ID != id {

return false, fmt.Errorf("move %s: the claim names op %q", id, c.Op.ID)

@@ -688,38 +691,30 @@ func (r *revertRun) probed(ctx context.Context, obs hostclaim.Observed) (bool, e

}

// opened (§7.4 opened, §7.11): once no chore of the op is left in the claim

-// (the lane's park acknowledged), the claim's release to serving under this

-// box, then the record's close.

+// (the lane's park acknowledged), the record's close, then the claim's

+// release to serving under this box (record first, ruling M4).

func (r *revertRun) opened(ctx context.Context, obs hostclaim.Observed) (bool, error) {

- cfg := r.cfg()

host, id := r.rec.Host, r.g.ID

if r.rec.Move.ReopenedAt == nil {

return false, fmt.Errorf("move %s: the claim is opened and the record has no reopen", id)

}

- owed := 0

- for _, o := range obs.Claim.Obligations {

- if o.Op == id {

- owed++

- }

- if owed > 0 {

+ // Nothing owed under the op, checked before the record's close (M4), as

+ // the console's grant checks it.

+ if owed := owedUnder(obs.Claim, id); owed > 0 {

r.w.notice(host+"#rv-opened", "moves: %s: the revert of %s waits for %d chore(s) of the move, its lane's park, to be acknowledged", host, id, owed)

return false, nil

}

r.w.logEvent(ctx, r.rec, "rolled_back")

- if err := r.update(ctx, obs, "release the claim", hostclaim.ReleaseMove(id, cfg.Box)); err != nil {

- return false, err

- }

- log.Printf("moves: %s: the claim is serving again after the revert of %s", host, id)

- if err := r.fault("after-release-move"); err != nil {

- return false, err

- }

- return r.close(ctx)

+ return r.close(ctx, true)

}

-// close is the record's close (MoveRevertClose), then the source's journal of

-// the op parked.

-func (r *revertRun) close(ctx context.Context) (bool, error) {

+// close is the record's close (MoveRevertClose), then, when releaseClaim is set,

+// the claim's release to serving under this box, then the source's journal

+// of the op parked. A crash between the record's close and the release

+// leaves the claim reverting/opened with nothing owed; the console's

+// recovery pass releases it from LastMove. releaseClaim is false only for a

+// claim a claim-first binary already released.

+func (r *revertRun) close(ctx context.Context, releaseClaim bool) (bool, error) {

cfg := r.cfg()

host, id := r.rec.Host, r.g.ID

ok, err := r.record(ctx, "the revert's close", provision.MoveRevertClose(r.g, r.now()))

@@ -728,6 +723,18 @@ func (r *revertRun) close(ctx context.Context) (bool, error) {

}

log.Printf("moves: %s: move %s is reverted and closed", host, id)

nudgeSerial(ctx, r.s)

+ if releaseClaim {

+ if err := r.fault("after-close-record"); err != nil {

+ return true, err

+ }

+ if err := releaseAfterClose(ctx, r.s, host, id, hostclaim.ReleaseMove(id, cfg.Box)); err != nil {

+ return true, err

+ }

+ log.Printf("moves: %s: the claim is serving again after the revert of %s", host, id)

+ if err := r.fault("after-release-move"); err != nil {

+ return true, err

+ }

if err := r.fault("after-close"); err != nil {

return true, err

}

diff --git a/internal/provision/plan9_b8_census_test.go b/internal/provision/plan9_b8_census_test.go

index ecd3621dd..e30367f1c 100644

--- a/internal/provision/plan9_b8_census_test.go

+++ b/internal/provision/plan9_b8_census_test.go

@@ -525,10 +525,10 @@ var plan9B8CensusInventory = []censusEntry{

{"internal/host/moveslandcommit.go", "landingRun.probed", "record-writer", "key:SetRecordMove", "6f961790d8fe169af68e2f70790c400d37c2388a4f62c26921f22b8b47c859de"},

// Stamps opened_at through SetRecordMove (MoveOpened) inside the hold lock, after the proved release.

{"internal/host/moveslandcommit.go", "landingRun.open", "record-writer", "key:SetRecordMove", "65e6908056c3055d5d0df2c27bb88943e31c08691a2173a090a9edb94c8c0b49"},

- // Closes a committed move through SetRecordMove (MoveClose, LastMove done) after the claim's ReleaseMove; never writes the claim after the record.

- {"internal/host/movesparks.go", "movesWorker.closeMove", "record-writer", "key:SetRecordMove", "849d114cf80a45004e9d01c66fcf11516381b046fe0f7c40294a628a3b922b90"},

- // Closes the rollback record through SetRecordMove; claim release and local journal parking use separate storage.

- {"internal/host/movesrecover.go", "recoverRun.finalize", "record-writer", "key:SetRecordMove", "fff2e28c78db68bccb16da6ab70ca877b51243b0aa56b9cb2c513c6f5660f7f7"},

+ // Closes a committed move through SetRecordMove (MoveClose, LastMove done) once nothing is owed under the op, then releases the claim (ReleaseMove via releaseAfterClose): record first, ruling M4. A claim already released by this move gets only the record's close.

+ {"internal/host/movesparks.go", "movesWorker.closeMove", "record-writer", "key:SetRecordMove", "efb6fa290d9eb2ee6b64a67f853d690ff1b259bd565b6191327822d99a9c0771"},

+ // Closes the rollback record through SetRecordMove once nothing is owed under the op, then releases the claim (record first, ruling M4); local journal parking uses separate storage.

+ {"internal/host/movesrecover.go", "recoverRun.finalize", "record-writer", "key:SetRecordMove", "2986525fbe297ed1f5cccc58957c10c63156301df6700ab2484b2d7837664de5"},

// Advances the source recovery phase through SetRecordMove and its sequenced writer.

{"internal/host/movesrecover.go", "recoverRun.phase", "record-writer", "key:SetRecordMove", "d67132b6e797a88a9677d962c5c7aa30fc7f85fdbdff06ce8318562397a9ee78"},

// Records probe inputs through SetRecordMove; phase and stuck helpers use the same writer.

@@ -654,7 +654,8 @@ var plan9B8CensusInventory = []censusEntry{

{"internal/host/fleetbind.go", "WriteFleetBinding", "nonrecord", "sel:Put", "44ab984c2c9b30abcc938132118f61a6922ccc0cd40ed2b6cb61c7654aa0a1c3"},

{"internal/host/logship.go", "logshipFlush", "nonrecord", "sel:Put", "a2fa594c1206028af170a2d0cbedef55ba00a2f1c698a6853e1214cc3b172dd9"},

{"internal/host/metrics_loop.go", "putAlertState", "nonrecord", "sel:Put", "d5b6e8b34dc5a731d6bbafeac0b7d0c5c20706d6f413dff38088b3321b35a26c"},

- {"internal/host/movesabort.go", "movesWorker.abortSource", "record-writer", "key:SetRecordMove", "70f2cd7ec7709045043081c078f1abe63ef822325eef7016ab9f595a16cabad5"},

+ // Clears an aborting record through SetRecordMove (MoveGuardedAbortComplete) once nothing is owed under the op, then ReleaseAbort: record first, ruling M4.

+ {"internal/host/movesabort.go", "movesWorker.abortSource", "record-writer", "key:SetRecordMove", "c846c24a039e490f430bd41bb9672d00220a1d50fe5b2721b77fdeeafe98029c"},

{"internal/host/movesarchive.go", "cutRun.publishCutArchive", "nonrecord", "sel:CopyVersioned,sel:PutIfAbsent", "6c7fcfd2d4b2a0319ac15ecbfe003ed0292fe160457fd5704be508c2ab302a1b"},

{"internal/host/movescut.go", "cutRun.cutTransition", "record-writer", "key:SetRecordMove", "d0d67399aa784036de43b3c143e88c3d85f8b3d9e6345f84908d3b58ff56191e"},

{"internal/host/movescut.go", "publishStoppedReport", "nonrecord", "sel:Put", "c710682f31d99127ad76524add246fda9f640c63934940e45c79ea25ba36eb3c"},

carlos / platform Public

moves: every box close is record first, then the claim's release (ruling M4)