amadan

carlos / platform Public

sim/hostlife: the move close is record first (Task 7 fix round 1, ruling 2)

The executable model now closes a move the way rev 7.23 and the boxes do.
closeMove (landing, rollback, revert and abort closes): with nothing owed
under the op, closeRecord clears the record's move into last_move and
names the executor's region, then the claim releases. On every third
step the box stops between the halves (a deterministic schedule, so no
seed's random stream changes), and never comes back; fixRecord, the
recovery pass, releases from last_move. Pushes and relocations release
as before.

A new invariant, K8, fails any move's release whose record still carries
the move. A new rule, record-first-close, mutates back to rev 7.22's
claim-first close; the sweep catches it on 1,060 of 3,000 seeds.

The claim-cas-opid witness is restaged: its stalled goroutine is the
source between the record's close and its release, resuming after the
recovery pass released and a purge claimed the host. With record first,
a goroutine stalled before the close is stopped by its record CAS alone.

final() judges a host freed during its last recovery drive as a freed
host, instead of dereferencing a nil record (seed 2547 / 3,000 under
admission-registration, a latent harness bug the new schedule reached).

Spec rev 7.23 entry and the §14.2.5 witness row describe the model.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude c7b04cc6c7f233805bd39c0800b97a6e8bcf8f33 parent cb6a242
7 files changed, +158 −24
  • docs/superpowers/specs/2026-10-02-move-any-app-design.md +12 −2
  • internal/sim/hostlife/console_test.go +13 −2
  • internal/sim/hostlife/moves_test.go +78 −5
  • internal/sim/hostlife/rules_test.go +1 −0
  • internal/sim/hostlife/sim_test.go +24 −8
  • internal/sim/hostlife/witness_test.go +26 −7
  • internal/sim/hostlife/world_test.go +4 −0
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 bde830bee..fc6d8c40e 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
@@ -16,7 +16,17 @@
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.
+ table's `opened` row, §14.2.2's model row and §19 K8. **The model**
+ (`internal/sim/hostlife`, moves Plan 5 Task 7 fix round 1) closes the
+ same way: a box's close CASes the record (`last_move`), and on every
+ third step stops before the release; the recovery pass releases from
+ `last_move` (`fixRecord`). A new invariant, K8, fails any move's release
+ whose record still carries the move, and a new rule,
+ `record-first-close`, whose mutation is rev 7.22's claim-first close, is
+ caught by it (1,060 / 3,000 seeds, first seed 1; no witness). The
+ 3,000-seed sweep of every rule otherwise matches its expected outcomes. The `claim-cas-opid` witness is
+ restaged: its stalled goroutine is now the source between the record's
+ close and its release (§14.2.5).
- **Rev 7.22** answers **joint round 19** (`CODEX-FINDINGS-JOINT-R19.md`,
"R19-1", the round's one finding, P2) and fixes the install
manifest's keys. **R19-1:** rev 7.21 bound the prepared files manifest
@@ -5938,7 +5948,7 @@ witness to hold there; each witness violates with the failure it names.
| `staging-quiet` (J-N2) | a staging round completes after the landing's staging park acknowledged, before the release | **violated**: INV-10 at the release | | 1 / 3,000 |
| `dirty-return` (INV-2) | the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write | **violated**: treated as clean with the source's replica covering the stop, the return is covered `clean-return`, nothing is declared and the serving database lacks the target's write (INV-2 local at the final recovery; rev 7.11 saw INV-15 at the declaration) | | 1 / 3,000 |
| `commit-before-open` (INV-5; R3-5) | a public request reaches the target's edge while its probe runs | **violated**: INV-5 | | 3 / 3,000 |
-| `claim-cas-opid` (C2) | a stalled source goroutine with the rollback's last read resumes after a purge claimed the host | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000 |
+| `claim-cas-opid` (C2) | the source closes a rollback's record and its goroutine stalls before the release, holding the rollback's last read (rev 7.23: before it, a goroutine stalled before a claim-first release); the recovery pass releases from `last_move`, a purge claims the host, and the goroutine resumes into its release | held | with `revalidate-before-effect`: **violated**, the store is torn down under a serving host | 0 / 3,000 |
| `exec-admission`, `hold-op-open`, `start-check-claim-gen`, `exec-writer` (J2-R2-8; claim rev 6.8.1) | a paused open from an earlier operation lands after the commit while the source's row is still held; a request wakes the source | held, each, and under every proper subset | all four: **violated**, INV-1 (the non-exec source is admitted cold into a fresh generation restored from its own region's old files and serves beside the target) | 0 / 3,000 |
| `start-check` (INV-4) | the same, dropping the whole start check | retired in rev 7.10: with every restore from the box's own region, the stale source finds nothing of the target's generation to restore and cannot start; subsumed (`expected-outcomes.txt`) | | 0 |
| `strict-spawn` (J-D3) | the source runs a main process and a descendant placed as its parent was; the move cuts | held | with `evidence-whole-tree`: **violated**, INV-1 | 13 / 3,000 |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index c85851365..e0cf5fea8 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -56,13 +56,24 @@ func (w *world) execBox(c *claim) *box {
// fixRecord is the recovery owner for the record halves of a move (claim
// C2): the request's `move` field after the claim's intent; the claim half
-// of a record-first transition (followRecord); and, after a release, the
-// CAS that clears `move` and names the executor's region (§7.9 step 5).
+// of a record-first transition (followRecord); the claim's release after a
+// move's record-first close, from last_move (rev 7.23 §7.5, ruling M4: the
+// closing box may stop between the halves and never comes back); and, after
+// any other release (a push, a relocation, or rev 7.22's claim-first close
+// under its mutation), the CAS that clears `move` and names the executor's
+// region.
func (w *world) fixRecord() {
c := w.claim
if c == nil || c.Holder == nil || w.rec == nil || w.rec.Inc != c.Holder.Inc {
return
}
+ if moveClose(c.Op) && w.rec.LastMove == c.Op.ID && w.rec.MoveID == "" {
+ if c.oblFor(c.Op.ID) == 0 {
+ w.stats["recovery: release from last_move"]++
+ w.release(c, closeExec(c.Op))
+ }
+ return
+ }
switch c.Op.Kind {
case "serving":
if b := w.execBox(c); b != nil && (w.rec.MoveID != "" || w.rec.Region != b.Region) {
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 6e5ae501f..d66c63aad 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -544,7 +544,7 @@ func (w *world) moveSource(b *box, c *claim) {
}
case "aborting":
if c.oblFor(op.ID) == 0 {
- w.release(c, op.Src)
+ w.closeMove(c, op.Src)
}
case "stopping":
if b.Row != nil {
@@ -938,7 +938,7 @@ func (w *world) revertSource(b *box, c *claim) {
}
case "opened":
if c.oblFor(op.ID) == 0 {
- w.release(c, op.Src)
+ w.closeMove(c, op.Src)
}
}
}
@@ -1258,7 +1258,7 @@ func (w *world) landTarget(b *box, c *claim) {
return
}
if c.oblFor(op.ID) == 0 {
- w.release(c, op.Tgt)
+ w.closeMove(c, op.Tgt)
}
}
}
@@ -1334,8 +1334,80 @@ func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, n
w.cas(c, func(n *claim) bool { next(n); return true })
}
+// moveClose reports whether op is a move's close: a committed landing, an
+// opened rollback or revert, or an abort. Pushes and relocations release on
+// their own terms.
+func moveClose(op opState) bool {
+ switch op.Kind {
+ case "landing", "restoring", "reverting":
+ return true
+ case "moving":
+ return op.Phase == "aborting"
+ }
+ return false
+}
+
+// closeExec is the box a move's close releases to: the target after a
+// landing, the source otherwise (§19 K8).
+func closeExec(op opState) int {
+ if op.Kind == "landing" {
+ return op.Tgt
+ }
+ return op.Src
+}
+
+// closeMove is a move's close by the box that runs it, record first (moves
+// rev 7.23 §7.5 and §19 K8, Paul's ruling M4). With nothing owed under the
+// op, the record's CAS clears move into last_move and names the executor's
+// region; only then does the claim release. The box may stop between the
+// halves (every third step here, a deterministic schedule that draws
+// nothing from the seed's stream). It never comes back to a record without a
+// move, so a closed record whose claim still holds the op is the recovery
+// pass's to release, from last_move (fixRecord).
+func (w *world) closeMove(c *claim, execBox int) {
+ op := c.Op
+ if c.oblFor(op.ID) != 0 {
+ return
+ }
+ if !on("record-first-close") {
+ // rev 7.22: the claim first; the recovery pass wrote the record
+ // half after the release
+ w.release(c, execBox)
+ return
+ }
+ if !w.closeRecord(c, execBox) {
+ return // closed already (last_move): not the box's any more
+ }
+ if w.now%3 == 0 {
+ w.stats["close: stopped between the record and the release"]++
+ return
+ }
+ w.release(c, execBox)
+}
+
+// closeRecord is the close's record half: the CAS that clears move into
+// last_move and names the executor's region, conditional on the record still
+// carrying this move for the claim's incarnation.
+func (w *world) closeRecord(c *claim, execBox int) bool {
+ r, op := w.rec, c.Op
+ if r == nil || c.Holder == nil || r.Inc != c.Holder.Inc || r.MoveID != op.ID {
+ return false
+ }
+ if b := w.boxByID(execBox); b != nil {
+ r.Region = b.Region
+ }
+ r.MoveID, r.MoveState, r.RollbackID, r.LastMove = "", "", "", op.ID
+ r.Ver = w.newVer()
+ w.logf("close %s: record closed (last_move)", op.ID)
+ return true
+}
+
func (w *world) release(c *claim, execBox int) {
op := c.Op
+ if moveClose(op) && (w.rec == nil || w.rec.LastMove != op.ID || w.rec.MoveID == op.ID) {
+ // K8 as rev 7.23 amends it: never a serving claim over a live move
+ w.violate("K8: %s releases the claim before its record closed (record first, rev 7.23)", op.ID)
+ }
if w.cas(c, func(n *claim) bool {
if !sameOp(n.Op.ID, op.ID) {
return false
@@ -1348,7 +1420,8 @@ func (w *world) release(c *claim, execBox int) {
}) {
w.logf("released %s to serving on box %d", op.ID, execBox)
w.opsDone++
- // the record half (CAS-clear move) follows on a later step (§7.9)
+ // a move's record closed before this (closeMove, rev 7.23); a
+ // push's or a relocation's record half follows on a later step
w.checkDurable(w.claim, "at the release of "+op.ID)
if r := w.residueAtEnd(); len(r) > 0 {
w.violate("INV-10: %s ended with residue %v", op.ID, r)
@@ -1639,7 +1712,7 @@ func (w *world) recoverSource(b *box, c *claim) {
}
case "opened":
if c.oblFor(op.ID) == 0 {
- w.release(c, op.Src)
+ w.closeMove(c, op.Src)
}
}
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 803320fad..1ba023d6c 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -107,6 +107,7 @@ var allRules = []string{
"sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations
"live-set-region", // claim rev 6.5 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region
// moves spec
+ "record-first-close", // rev 7.23 §7.5, §19 K8 (ruling M4): a move's close CASes the record (move into last_move) before the claim's release, and the recovery pass releases from last_move; the mutation is rev 7.22's claim-first close, whose record half the recovery pass wrote after the release
"seal-by-version", // J-N2: landing copies sealed versions
"staging-quiet", // J-N2: staging retired after its writers' horizon
"commit-before-open", // INV-5
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index 1cac18606..59ac976f6 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -508,6 +508,19 @@ func (w *world) canStart(e *box, c *claim) string {
return ""
}
+// finalFreed is the end state of a freed host: no record, and no box holds
+// local state for it.
+func (w *world) finalFreed() {
+ if w.rec != nil {
+ w.violate("claim/record: claim free but record inc %d exists", w.rec.Inc)
+ }
+ for _, b := range w.liveBoxes() {
+ if b.DB != nil || b.Files != nil {
+ w.violate("INV-10: box %d still holds local state for a freed host", b.ID)
+ }
+ }
+}
+
func (w *world) final() {
if !w.quiescent() {
if len(w.pending) == 0 && len(w.console) == 0 && w.atRest() {
@@ -519,14 +532,7 @@ func (w *world) final() {
}
c := w.claim
if c == nil || c.Holder == nil {
- if w.rec != nil {
- w.violate("claim/record: claim free but record inc %d exists", w.rec.Inc)
- }
- for _, b := range w.liveBoxes() {
- if b.DB != nil || b.Files != nil {
- w.violate("INV-10: box %d still holds local state for a freed host", b.ID)
- }
- }
+ w.finalFreed()
return
}
e := w.execBox(c)
@@ -556,8 +562,18 @@ func (w *world) final() {
}
}
c = w.claim
+ if c == nil || c.Holder == nil {
+ // the final drive ran the console too: a purge may have freed
+ // the host (seed 2547 / 3,000 under admission-registration)
+ w.finalFreed()
+ return
+ }
e = w.execBox(c)
}
+ if e == nil || w.rec == nil {
+ w.violate("claim/record: the claim's holder has no record or no executing box at the end: %s", w.state())
+ return
+ }
if w.rec.Region != e.Region {
w.violate("claim/record: record region %d, claim serves from box %d in region %d", w.rec.Region, e.ID, e.Region)
}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 9600d7fd0..b4f229f37 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -66,7 +66,7 @@ var witnesses = []witness{
{"staging-quiet", "staging-quiet", "ended with residue",
"a staging round completes after the landing's staging park acknowledged; retired at the seal rather than after the writers' horizon, the round is residue at the release (INV-10)", wStagingQuiet},
{"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", "store of app",
- "redundant alone: a stalled source goroutine with the rollback's last read resumes after a purge claimed the host; revalidation stops it, and so does the op-id condition on its release CAS; with both gone the release overwrites the purge and the store is torn down under a serving host", wClaimCasOpID},
+ "redundant alone: the source closes the rollback's record and stalls before its release (rev 7.23, record first); the recovery pass releases from last_move, a purge claims the host, and the stalled goroutine resumes into its release with the rollback's last read; revalidation stops it, and so does the op-id condition on its release CAS; with both gone the release overwrites the purge and the store is torn down under a serving host", wClaimCasOpID},
{"dirty-return", "dirty-return", "INV-2",
"the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write to the source; treated as clean with the source's replica covering the stop, the source's admission is covered clean-return, declares nothing, and the serving database lacks the target's write (INV-2 local at the final recovery, rev 7.12; rev 7.11 saw INV-15 at the declaration, rev 7.10 INV-2 on the serving database)", wDirtyReturn},
{"commit-before-open", "commit-before-open", "INV-5",
@@ -905,28 +905,47 @@ func wStagingQuiet(t *testing.T, w *world) {
w.finish(t)
}
-// wClaimCasOpID (claim C2): a clean rollback; a second goroutine of the
-// source read the claim just before the release and stalls; the host is
-// released, a purge claims it, and the goroutine resumes.
+// wClaimCasOpID (claim C2): a clean rollback; the source's close writes the
+// record (record first, rev 7.23) and its goroutine stalls before the
+// release, holding the claim it read; the recovery pass releases from
+// last_move, a purge claims the host, and the goroutine resumes into its
+// release.
func wClaimCasOpID(t *testing.T, w *world) {
src, tgt := w.boxes[0], w.boxes[1]
w.serve(src, 1, app0)
w.landProbed(t, src, tgt)
w.rollback(w.claim, "cut deadline")
- w.reach(t, 1500, "source about to release", func() bool {
+ w.reach(t, 1500, "source about to close", func() bool {
c := w.claim
return c.Op.Kind == "restoring" && c.Op.SrcPhase == "opened" && c.oblFor(c.Op.ID) == 0
}, w.act(src, tgt), w.recoveryPass)
old := w.claim.clone() // the stalled goroutine's read
- w.reach(t, 50, "released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(src, tgt), w.recoveryPass)
+ if !w.closeRecord(old, src.ID) {
+ t.Fatalf("witness: the record did not close: %s", w.state())
+ }
+ w.reach(t, 50, "released from last_move", func() bool { return w.claim.Op.Kind == "serving" }, w.recoveryPass)
pg := &consolePlan{Kind: "purge", App: app0}
w.reach(t, 20, "purge claimed the host", func() bool { return w.claim.Op.Kind == "purging" }, func() { w.runPlan(pg) })
- w.resumeStale(src, old) // the goroutine wakes with the rollback's last read
+ w.resumeStaleRelease(src, old) // the goroutine wakes into its release
w.tick()
w.tick(func() { w.runPlan(pg) }) // the purge tears the store down
w.tick(func() { w.runPlan(pg) })
}
+// resumeStaleRelease is a close's goroutine that stalled between the
+// record's close and the claim's release, resuming with the claim it read:
+// it revalidates (claim C3), then writes the release half.
+func (w *world) resumeStaleRelease(b *box, old *claim) {
+ c, ok := w.readClaim(b)
+ if !ok {
+ return
+ }
+ if on("revalidate-before-effect") && !sameStep(old, c) {
+ return
+ }
+ w.release(old, closeExec(old.Op))
+}
+
// wDirtyReturn (INV-2; also commit-before-open's witness): the target
// writes during its probe and is rolled back.
func wDirtyReturn(t *testing.T, w *world) {
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index d0a6813e1..16ba94654 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -937,6 +937,10 @@ type record struct {
MoveState string
RollbackID string
Reason string
+ // LastMove names the move whose close cleared MoveID: the close is record
+ // first (moves rev 7.23 §7.5, Paul's ruling M4), so a record can say a
+ // move is over while the claim still holds its op, until the release.
+ LastMove string
}
// ---------- the world ----------