amadan

carlos / platform Public

sim: hostlife, an executable joint model of the host lifecycle claim and Phase 1 moves (#175)

A deterministic randomized simulation, test-only (every file is _test.go,
standard library only), of claim spec rev 2 (cf3a7861) and move-any-app
rev 4: the claim and records, versioned buckets with the real IAM split,
S3 requests that complete late after the client gave up, agent crashes,
reboots, whole-VM freezes, agent pauses, partitions, clock skew, destroyed
and restarted boxes, boot recovery to an old executable, and an
application whose descendants write on their own. Actors cover create,
delete, purge, push, the db door, wake, reconcile, config sync, release
adoption, the timer runner, the watchdog, every move phase, clean and
dirty rollback, abort, a stalled second worker, the recovery pass and an
operator.

Invariants are checked after every step and at the end of every run. The
gate runs 300 seeds (about a second); HOSTLIFE_SEEDS=30000 is clean. Every
protocol rule is a named guard; mutate.sh drops each in a scratch copy:
30 of 48 rules are caught alone, 8 more only in pairs, 2 are liveness
rules, and 8 are not exercised yet (spec §14.2.5).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 1486345c85073474a6bd28966ffd2082cabcc707 parent 4316db7
8 files changed, +3599 −0
  • internal/sim/hostlife/background_test.go +347 −0
  • internal/sim/hostlife/console_test.go +651 −0
  • internal/sim/hostlife/moves_test.go +864 −0
  • internal/sim/hostlife/mutate.sh +52 −0
  • internal/sim/hostlife/protocol_test.go +553 −0
  • internal/sim/hostlife/rules_test.go +76 −0
  • internal/sim/hostlife/sim_test.go +433 −0
  • internal/sim/hostlife/world_test.go +623 −0
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
new file mode 100644
index 000000000..5e4cd24f2
--- /dev/null
+++ b/internal/sim/hostlife/background_test.go
@@ -0,0 +1,347 @@
+package hostlife
+
+// ---------- the application ----------
+
+// traffic: every running process of the host does its own work, whether or
+// not a request arrived: background workers and descendants included.
+func (w *world) traffic(b *box) {
+ if b.Destroyed || b.Frozen {
+ return
+ }
+ for _, p := range b.Procs {
+ if w.rng.Intn(3) != 0 {
+ continue
+ }
+ w.nextW++
+ wr := w.nextW
+ if b.DB != nil && b.DB.Inc == p.Inc {
+ b.DB.Writes = append(b.DB.Writes, wr)
+ }
+ // acknowledged to the client or the outside world either way: a
+ // write into a purged or foreign database is a lost write
+ w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"})
+ if p.Main && w.rng.Intn(4) == 0 && b.Row != nil && b.Row.Inc == p.Inc {
+ w.nextW++
+ b.Timers = append(b.Timers, w.nextW)
+ w.acks = append(w.acks, ack{W: w.nextW, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "timer"})
+ }
+ }
+}
+
+// replicate: the serving process's ordinary litestream replication. The
+// claim's C3 exception: these are plain PUTs to reused keys.
+func (w *world) replicate(b *box) {
+ if !w.agentUp(b) || !hasMain(b) || b.DB == nil {
+ return
+ }
+ bl := &blob{Kind: "ltx", Inc: b.DB.Inc, Gen: b.DB.Gen, Writes: append([]int(nil), b.DB.Writes...), SealKey: b.DB.Key}
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: "instances/" + host + "/ltx", b: bl})
+}
+
+// idleStop: the activator's ordinary idle stop (main only; a descendant
+// keeps running, as today).
+func (w *world) idleStop(b *box) {
+ if !w.agentUp(b) || !hasMain(b) {
+ return
+ }
+ w.replicate(b)
+ var keep []*proc
+ for _, p := range b.Procs {
+ if !p.Main {
+ keep = append(keep, p)
+ }
+ }
+ b.Procs = keep
+}
+
+// wake: a request reaches this box's edge for the host.
+func (w *world) wake(b *box) {
+ if !w.agentUp(b) || b.Row == nil || b.Row.Status != "ready" || hasMain(b) {
+ return
+ }
+ if b.Old {
+ if w.rec == nil {
+ return
+ }
+ c := &claim{Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true}}
+ w.spawn(b, c, lin{}, false)
+ return
+ }
+ c, ok := w.admissionClaim(b)
+ if !ok || !w.admits(b, c, "") {
+ return
+ }
+ w.spawn(b, c, holderLin(c.Holder), false)
+}
+
+// ---------- reconcile ----------
+
+func (w *world) retireRow(b *box) {
+ if b.Row == nil {
+ return
+ }
+ if !b.Old && !w.evidence(b, "retire") {
+ return
+ }
+ if b.Old {
+ var keep []*proc
+ for _, p := range b.Procs {
+ if !p.Main {
+ keep = append(keep, p)
+ }
+ }
+ b.Procs = keep
+ }
+ b.Row = nil
+ b.Config = 0 // reapConfigEnv
+ // the schedule converger prunes timers of a host with no row
+ b.Timers, b.History, b.Attempt = nil, nil, 0
+}
+
+func (w *world) ownsLocalObligation(c *claim, b *box) bool {
+ for _, o := range c.Obl {
+ if o.Kind == "park-local" && o.Box == b.ID {
+ return true
+ }
+ }
+ return false
+}
+
+func (w *world) reconcile(b *box) {
+ if !w.agentUp(b) {
+ return
+ }
+ if b.Old {
+ if w.rec != nil && w.rec.Region == b.Region {
+ if b.Row == nil || b.Row.Inc != w.rec.Inc {
+ b.Row = &row{Inc: w.rec.Inc, App: w.rec.App, Status: "ready"}
+ }
+ } else if b.Row != nil {
+ w.retireRow(b)
+ }
+ return
+ }
+ c, ok := w.readClaim(b)
+ if !ok {
+ return
+ }
+ if c == nil {
+ w.adopt()
+ return
+ }
+ w.reconcileClaimed(b, c)
+}
+
+// adopt is the one adoption routine every actor uses (claim §9): a
+// create-only claim for an unclaimed legacy record, with discovery.
+func (w *world) adopt() bool {
+ if w.claim != nil || w.rec == nil {
+ return false
+ }
+ eb := w.regionBox(w.rec.Region)
+ if eb == nil {
+ return false
+ }
+ n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true},
+ Op: opState{Kind: "serving", Exec: eb.ID, Parts: []int{eb.ID}}, Regions: []int{w.rec.Region}, Boxes: []int{eb.ID}, Complete: false}
+ if on("legacy-discovery") {
+ // every other region parks whatever it holds: it cannot be the
+ // live lineage, because the record names another region
+ for r := 0; r < nRegions; r++ {
+ if r == w.rec.Region {
+ continue
+ }
+ for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} {
+ n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "adopt", Kind: "park-replica", Region: r, Box: -1, Prefix: p, Ret: "legacy"})
+ }
+ }
+ }
+ w.claim = n
+ w.logf("adopted legacy host inc %d on box %d", w.rec.Inc, eb.ID)
+ return true
+}
+
+func (w *world) reconcileClaimed(b *box, c *claim) {
+ h := c.Holder
+ if h == nil || w.rec == nil || w.rec.Inc != h.Inc {
+ if b.Row != nil && !w.ownsLocalObligation(c, b) {
+ w.retireRow(b)
+ }
+ return
+ }
+ if b.Row != nil && b.Row.Inc != h.Inc {
+ w.retireRow(b) // an orphan row (claim C1)
+ return
+ }
+ switch c.Op.Kind {
+ case "serving", "creating", "pushing":
+ if c.Op.Exec == b.ID {
+ if b.Row != nil && b.Row.Status != "ready" && c.Op.Kind == "serving" && on("stale-hold-release") {
+ // a hold whose operation has ended (the claim is serving here)
+ b.Row.Status, b.Row.HoldOp = "ready", ""
+ }
+ if b.Row == nil && c.Op.Kind == "serving" {
+ b.Row = &row{Inc: h.Inc, App: h.App, Status: "ready"}
+ if b.Retired != nil {
+ delete(b.Retired, h.Inc)
+ }
+ }
+ } else if b.Row != nil && !(on("participant-rows") && w.ownsLocalObligation(c, b)) {
+ w.retireRow(b)
+ }
+ default:
+ if w.isParticipant(c, b) {
+ if !on("participant-rows") && w.rec.Region != b.Region && b.Row != nil {
+ w.retireRow(b) // region mismatch retires a participant's row
+ }
+ return
+ }
+ if b.Row != nil && !w.ownsLocalObligation(c, b) {
+ w.retireRow(b)
+ }
+ }
+}
+
+// ---------- background passes with work in flight (J-N8) ----------
+
+func (w *world) passPlan(b *box, kind string) {
+ if !w.agentUp(b) || b.Row == nil || b.Row.Status != "ready" {
+ return
+ }
+ if kind == "config" && !b.HasKey {
+ return
+ }
+ b.plans = append(b.plans, &plan{Kind: kind, Inc: b.Row.Inc, App: b.Row.App})
+}
+
+func (w *world) passExec(b *box) {
+ if !w.agentUp(b) || len(b.plans) == 0 {
+ return
+ }
+ i := w.rng.Intn(len(b.plans))
+ p := b.plans[i]
+ b.plans = append(b.plans[:i:i], b.plans[i+1:]...)
+ if on("hostguard") {
+ c, ok := w.readClaim(b)
+ if !ok || c == nil || c.Holder == nil || c.Holder.Inc != p.Inc || b.Row == nil || b.Row.Inc != p.Inc || b.Retired[p.Inc] {
+ return
+ }
+ }
+ switch p.Kind {
+ case "config":
+ b.Config = p.Inc
+ case "adopt":
+ b.Live, b.LiveInc = p.App, p.Inc
+ }
+}
+
+// ---------- timers ----------
+
+func (w *world) runner(b *box) {
+ if !w.agentUp(b) || b.Row == nil {
+ return
+ }
+ if len(b.Timers) > 0 {
+ if b.Row.Status == "ready" && hasMain(b) {
+ id := b.Timers[0]
+ b.Timers = b.Timers[1:]
+ b.History = append(b.History, id)
+ w.delivered[id] = true
+ } else if b.Row.Status != "ready" && !on("timer-freeze") {
+ b.Attempt++ // a refused delivery still advances bookkeeping
+ }
+ }
+ if w.rng.Intn(4) == 0 {
+ b.History = nil // the runner's own daily prune (runner.go:260)
+ }
+}
+
+// ---------- self-fencing (claim §7.1) ----------
+
+func (w *world) watchdog(b *box) {
+ if b.Destroyed || b.Frozen {
+ return
+ }
+ if !on("watchdog-independent") && !w.agentUp(b) {
+ return
+ }
+ if b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil && len(b.Procs) > 0 {
+ b.Procs = nil
+ w.logf("box %d self-fenced (exec lease expired)", b.ID)
+ }
+}
+
+// ---------- faults ----------
+
+func (w *world) fault() {
+ if len(w.pending) > 0 && w.rng.Intn(3) == 0 {
+ i := w.rng.Intn(len(w.pending))
+ r := w.pending[i]
+ w.pending = append(w.pending[:i:i], w.pending[i+1:]...)
+ w.complete(r)
+ return
+ }
+ bs := w.liveBoxes()
+ b := bs[w.rng.Intn(len(bs))]
+ switch w.rng.Intn(9) {
+ case 0:
+ if !b.AgentDown {
+ b.AgentDown = true
+ var keep []*proc
+ for _, p := range b.Procs {
+ if b.Nested {
+ keep = append(keep, p)
+ }
+ }
+ b.Procs = keep
+ b.forget()
+ w.logf("box %d agent crashed", b.ID)
+ } else {
+ b.AgentDown = false
+ }
+ case 1:
+ b.Procs = nil
+ b.AgentDown, b.Frozen, b.AgentPaused = false, false, false
+ b.forget()
+ if !on("floor-boot-recovery") && w.rng.Intn(3) == 0 {
+ b.Old = true
+ w.logf("box %d boot-recovered an old executable", b.ID)
+ }
+ w.logf("box %d rebooted", b.ID)
+ case 2:
+ if w.fail["partition"] {
+ b.Partitioned = !b.Partitioned
+ }
+ case 3:
+ if w.fail["freeze"] {
+ b.Frozen = !b.Frozen
+ }
+ case 4:
+ if w.fail["pause"] {
+ b.AgentPaused = !b.AgentPaused
+ }
+ case 5:
+ c := w.claim
+ if w.fail["destroy"] && c != nil && (c.Op.Kind == "landing" || c.Op.Kind == "restoring") && !c.Op.Committed && b.ID == c.Op.Tgt {
+ b.Destroyed = true
+ b.Procs = nil
+ w.logf("box %d destroyed", b.ID)
+ }
+ case 6:
+ w.console = nil // console crash: plans dropped
+ default:
+ w.completeDue(false)
+ }
+}
+
+func (w *world) replaceDestroyed() {
+ for r := 0; r < nRegions; r++ {
+ if w.regionBox(r) == nil {
+ w.nextID++
+ nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true}
+ nb.forget()
+ w.boxes = append(w.boxes, nb)
+ w.logf("box %d replaces the destroyed box in region %d", nb.ID, r)
+ }
+ }
+}
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
new file mode 100644
index 000000000..3ac2eac67
--- /dev/null
+++ b/internal/sim/hostlife/console_test.go
@@ -0,0 +1,651 @@
+package hostlife
+
+import "fmt"
+
+// consolePlan is a multi-step console operation. A console crash drops
+// every plan; the claim-recovery pass must then finish or undo the work
+// from the claim alone (claim C2).
+type consolePlan struct {
+ Kind string // create, delete, purge
+ Step int
+ App string
+ OpID string
+}
+
+type doorPlan struct {
+ Region int
+ Key string
+ Ver int
+ Inc int
+}
+
+func (w *world) execBox(c *claim) *box {
+ if c == nil {
+ return nil
+ }
+ return w.boxByID(c.Op.Exec)
+}
+
+// fixRecord converges the record's region and move id to the claim. It is
+// the record half of every flip, release and recovery (claim C2).
+func (w *world) fixRecord() {
+ c := w.claim
+ if c == nil || c.Holder == nil || w.rec == nil || w.rec.Inc != c.Holder.Inc {
+ return
+ }
+ switch c.Op.Kind {
+ case "serving":
+ if b := w.execBox(c); b != nil {
+ w.rec.Region = b.Region
+ }
+ w.rec.MoveID = ""
+ case "moving", "reverting":
+ w.rec.Region, w.rec.MoveID = c.Op.SrcRegion, c.Op.ID
+ case "landing":
+ w.rec.Region, w.rec.MoveID = c.Op.TgtRegion, c.Op.ID
+ case "restoring":
+ w.rec.Region, w.rec.MoveID = c.Op.SrcRegion, c.Op.ID
+ }
+}
+
+func (w *world) liveBoxes() []*box {
+ var out []*box
+ for _, b := range w.boxes {
+ if !b.Destroyed {
+ out = append(out, b)
+ }
+ }
+ return out
+}
+
+// ---------- user operations ----------
+
+func (w *world) userCreate() {
+ c := w.claim
+ if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) {
+ return
+ }
+ if w.rec != nil {
+ return
+ }
+ app := app0
+ if w.rng.Intn(2) == 0 {
+ app = app1
+ }
+ if w.purgeRes[app] {
+ return
+ }
+ r := w.rng.Intn(nRegions)
+ b := w.regionBox(r)
+ if b == nil || (c != nil && contains(c.Lost, b.ID)) {
+ return
+ }
+ var inc int
+ if on("fresh-incarnation") || c == nil || len(c.Retired) == 0 {
+ w.nextInc++
+ inc = w.nextInc
+ } else {
+ inc = c.Retired[len(c.Retired)-1] // a caller-supplied CreatedAt repeats an identity
+ }
+ if on("fresh-incarnation") && c != nil && contains(c.Retired, inc) {
+ return
+ }
+ w.serial++
+ id := w.newID("cr")
+ if w.cas(c, func(n *claim) bool {
+ n.Holder = &holder{Inc: inc, App: app, Serial: w.serial}
+ n.Op = opState{Kind: "creating", ID: id, Exec: -1, NewInc: inc, NewApp: app, NewRegion: r, ReqAt: w.now}
+ n.Regions, n.Boxes, n.Complete, n.Obl = []int{r}, []int{b.ID}, true, nil
+ return true
+ }) {
+ w.stores[app] = true
+ w.console = append(w.console, &consolePlan{Kind: "create", OpID: id})
+ w.logf("create %s inc %d app %s in region %d", id, inc, app, r)
+ }
+}
+
+func (w *world) userDelete() {
+ c := w.claim
+ if c == nil || c.Holder == nil {
+ return
+ }
+ if on("claim-op-exclusive") && c.Op.Kind != "serving" {
+ return
+ }
+ id := w.newID("del")
+ if w.cas(c, func(n *claim) bool {
+ n.Op = opState{Kind: "deleting", ID: id, Exec: -1, ReqAt: w.now}
+ return true
+ }) {
+ w.console = append(w.console, &consolePlan{Kind: "delete", OpID: id})
+ w.logf("delete %s inc %d", id, c.Holder.Inc)
+ }
+}
+
+func (w *world) userMove() {
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
+ return
+ }
+ src := w.execBox(c)
+ if src == nil || src.Destroyed {
+ return
+ }
+ r := w.rng.Intn(nRegions)
+ if r == src.Region {
+ return
+ }
+ tgt := w.regionBox(r)
+ if tgt == nil || contains(c.Lost, tgt.ID) || tgt.Old {
+ return
+ }
+ if on("obligations-block-ops") {
+ for _, o := range c.Obl {
+ if o.Region == r || o.Box == tgt.ID || o.Box == src.ID || o.Region == src.Region {
+ return // an operation never starts over a pending chore in its regions
+ }
+ }
+ }
+ id := w.newID("mv")
+ if w.cas(c, func(n *claim) bool {
+ if n.Op.Kind != "serving" {
+ return false
+ }
+ n.Op = opState{Kind: "moving", ID: id, Phase: "leases", Exec: src.ID, Parts: []int{src.ID, tgt.ID},
+ Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App}
+ return true
+ }) {
+ w.fixRecord()
+ w.logf("move %s inc %d from box %d to box %d", id, c.Holder.Inc, src.ID, tgt.ID)
+ }
+}
+
+func (w *world) userPush() {
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
+ return
+ }
+ b := w.execBox(c)
+ if b == nil || b.FailApp {
+ return
+ }
+ if on("obligations-block-ops") {
+ for _, o := range c.Obl {
+ if o.Region == b.Region || o.Box == b.ID {
+ return
+ }
+ }
+ }
+ id := w.newID("push")
+ if w.cas(c, func(n *claim) bool {
+ if n.Op.Kind != "serving" {
+ return false
+ }
+ n.Op = opState{Kind: "pushing", ID: id, Phase: "stopping", Exec: b.ID, Parts: []int{b.ID}, Src: b.ID, Tgt: b.ID, SrcRegion: b.Region, TgtRegion: b.Region, ReqAt: w.now}
+ return true
+ }) {
+ w.logf("push %s on box %d", id, b.ID)
+ }
+}
+
+func (w *world) userPurge() {
+ c := w.claim
+ app := app0
+ if c != nil && c.Holder != nil {
+ app = c.Holder.App
+ }
+ for _, p := range w.console {
+ if p.Kind == "purge" {
+ return
+ }
+ }
+ w.console = append(w.console, &consolePlan{Kind: "purge", App: app})
+ w.logf("purge app %s", app)
+}
+
+func (w *world) parkingObligations(n *claim, inc int) {
+ regions := append([]int(nil), n.Regions...)
+ var boxes []int
+ boxes = append(boxes, n.Boxes...)
+ if !n.Complete && on("touched-incomplete") {
+ regions = nil
+ for r := 0; r < nRegions; r++ {
+ regions = append(regions, r)
+ }
+ for _, b := range w.liveBoxes() {
+ boxes = addUniq(boxes, b.ID)
+ }
+ }
+ for _, r := range regions {
+ for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} {
+ n.Obl = append(n.Obl, w.newObl(n, "park-replica", r, -1, p, fmt.Sprint(inc), 0))
+ }
+ }
+ for _, id := range boxes {
+ if b := w.boxByID(id); b != nil && !b.Destroyed {
+ n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, id, "", fmt.Sprint(inc), 0))
+ }
+ }
+ n.Retired = addUniq(n.Retired, inc)
+}
+
+// consoleStep runs the next step of the oldest console plan.
+func (w *world) consoleStep() {
+ if len(w.console) == 0 {
+ return
+ }
+ p := w.console[0]
+ done := w.runPlan(p)
+ if done {
+ w.console = w.console[1:]
+ }
+}
+
+func (w *world) runPlan(p *consolePlan) bool {
+ c := w.claim
+ switch p.Kind {
+ case "create":
+ if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" {
+ return true
+ }
+ if p.Step == 0 {
+ if w.rec == nil {
+ w.rec = &record{Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion}
+ }
+ p.Step = 1
+ return false
+ }
+ b := w.regionBox(c.Op.NewRegion)
+ if b == nil {
+ return false
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, p.OpID) {
+ return false
+ }
+ n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
+ return true
+ })
+ return true
+ case "delete":
+ if c == nil || c.Op.ID != p.OpID {
+ return true
+ }
+ return w.deleteSteps(c)
+ case "purge":
+ return w.purgeSteps(p)
+ }
+ return true
+}
+
+// deleteSteps: record DeleteIfMatch, then parking with obligations, then
+// free once every obligation is acknowledged (claim §5.2).
+func (w *world) deleteSteps(c *claim) bool {
+ switch c.Op.Kind {
+ case "deleting", "purging":
+ if w.rec != nil && w.rec.Inc == c.Holder.Inc {
+ w.rec = nil
+ return false
+ }
+ if w.rec != nil {
+ return false // C6: a mismatched record means wait
+ }
+ inc := c.Holder.Inc
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, c.Op.ID) {
+ return false
+ }
+ n.Op.Kind = "parking"
+ w.parkingObligations(n, inc)
+ return true
+ })
+ return false
+ case "parking":
+ if len(c.Obl) > 0 {
+ return false
+ }
+ w.free(c)
+ return true
+ }
+ return true
+}
+
+func (w *world) free(c *claim) {
+ app := ""
+ if c.Holder != nil {
+ app = c.Holder.App
+ }
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, c.Op.ID) || len(n.Obl) > 0 {
+ return false
+ }
+ n.Holder, n.Op, n.Regions, n.Boxes, n.Complete = nil, opState{}, nil, nil, true
+ return true
+ }) {
+ w.logf("host freed")
+ w.opsDone++
+ w.stats["freed"]++
+ if w.purgeRes[app] && !on("purge-journal") {
+ w.purgeRes[app] = false // freeing the host drops the reservation
+ }
+ }
+}
+
+func (w *world) purgeSteps(p *consolePlan) bool {
+ c := w.claim
+ reserve := func() {
+ w.purgeRes[p.App] = true
+ }
+ claimIt := func() bool {
+ if c == nil && w.rec != nil && w.rec.App == p.App && on("purge-adopts") {
+ // an unclaimed legacy record of this app: adopt it first (§9),
+ // so the purge decides over claims, not over their absence
+ w.adopt()
+ return false
+ }
+ if c == nil || c.Holder == nil || c.Holder.App != p.App {
+ return true // nothing of this app holds the host
+ }
+ if c.Op.Kind == "purging" || c.Op.Kind == "parking" || c.Op.Kind == "deleting" {
+ return true
+ }
+ if c.Op.Kind != "serving" {
+ return false // retry later; the reservation stays
+ }
+ id := w.newID("pg")
+ return w.cas(c, func(n *claim) bool {
+ if n.Op.Kind != "serving" {
+ return false
+ }
+ n.Op = opState{Kind: "purging", ID: id, Exec: -1, ReqAt: w.now}
+ return true
+ })
+ }
+ if on("purge-journal") {
+ if st, ok := w.purgeStep[p.App]; ok && st > p.Step {
+ p.Step = st // resume from the reservation's journal
+ }
+ defer func() {
+ if w.purgeRes[p.App] {
+ w.purgeStep[p.App] = p.Step
+ }
+ }()
+ }
+ switch p.Step {
+ case 0:
+ if on("purge-reserve-first") {
+ reserve()
+ p.Step = 1
+ } else {
+ w.stores[p.App] = false // tear down first
+ p.Step = 1
+ }
+ return false
+ case 1:
+ if !claimIt() {
+ return false
+ }
+ p.Step = 2
+ return false
+ case 2:
+ if on("purge-reserve-first") {
+ w.stores[p.App] = false
+ } else {
+ reserve()
+ }
+ p.Step = 3
+ return false
+ default:
+ if c == nil || c.Holder == nil || c.Holder.App != p.App {
+ if c == nil || c.Holder == nil {
+ w.purgeRes[p.App] = false
+ delete(w.purgeStep, p.App)
+ }
+ return true
+ }
+ w.deleteSteps(c)
+ return false
+ }
+}
+
+// resumePurges: the recovery pass restarts a purge whose plan was lost,
+// from its reservation's journal.
+func (w *world) resumePurges() {
+ if !on("purge-journal") {
+ return
+ }
+ for _, app := range []string{app0, app1} {
+ if !w.purgeRes[app] {
+ continue
+ }
+ running := false
+ for _, p := range w.console {
+ if p.Kind == "purge" && p.App == app {
+ running = true
+ }
+ }
+ if !running {
+ w.console = append(w.console, &consolePlan{Kind: "purge", App: app, Step: w.purgeStep[app]})
+ }
+ }
+}
+
+// ---------- the door (claim §6.5) ----------
+
+func (w *world) doorAuthorize() {
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
+ return
+ }
+ b := w.execBox(c)
+ if b == nil {
+ return
+ }
+ bk := w.buckets[b.Region]
+ key := "instances/" + host + "/ltx"
+ d := &doorPlan{Region: b.Region, Key: key, Inc: c.Holder.Inc}
+ if on("door-by-version") {
+ for _, v := range bk.objs[key] {
+ if !v.Marker && v.B.Inc == c.Holder.Inc {
+ d.Ver = v.ID
+ }
+ }
+ if d.Ver == 0 {
+ return
+ }
+ }
+ w.doorReads = append(w.doorReads, d)
+}
+
+func (w *world) doorOpen() {
+ if len(w.doorReads) == 0 {
+ return
+ }
+ i := w.rng.Intn(len(w.doorReads))
+ d := w.doorReads[i]
+ w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...)
+ bk := w.buckets[d.Region]
+ var v *version
+ if d.Ver != 0 {
+ v = bk.byID(d.Key, d.Ver)
+ } else {
+ v = bk.current(d.Key)
+ }
+ if v != nil && v.B.Inc != 0 && v.B.Inc != d.Inc {
+ w.violate("door: a read authorized for inc %d returned data of inc %d", d.Inc, v.B.Inc)
+ }
+}
+
+// ---------- the console's claim-recovery pass (claim §8) ----------
+
+func (w *world) recoveryPass() {
+ if !on("recovery-pass") {
+ return
+ }
+ w.resumePurges()
+ c := w.claim
+ if c == nil {
+ return
+ }
+ // an orphan record: the claim is free or names someone else
+ if w.rec != nil && (c.Holder == nil || c.Holder.Inc != w.rec.Inc) && c.Op.Kind != "creating" {
+ w.logf("recovery: removing orphan record inc %d", w.rec.Inc)
+ w.rec = nil
+ return
+ }
+ switch c.Op.Kind {
+ case "creating":
+ if w.now-c.Op.ReqAt < 15 {
+ return
+ }
+ if w.rec != nil && w.rec.Inc == c.Holder.Inc {
+ b := w.regionBox(c.Op.NewRegion)
+ if b == nil {
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, c.Op.ID) {
+ return false
+ }
+ n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
+ return true
+ })
+ } else if w.rec == nil {
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, c.Op.ID) {
+ return false
+ }
+ n.Holder, n.Op = nil, opState{}
+ n.Regions, n.Boxes = nil, nil
+ return true
+ })
+ }
+ case "deleting", "parking":
+ if w.now-c.Op.ReqAt < 15 {
+ return
+ }
+ w.deleteSteps(c)
+ case "purging":
+ if w.now-c.Op.ReqAt < 15 {
+ return
+ }
+ if on("purge-journal") {
+ w.resumePurges() // the purge's own phases, in order
+ return
+ }
+ w.deleteSteps(c)
+ case "landing":
+ w.fixRecord()
+ if !c.Op.Committed && w.now > c.Op.CutDeadline+10 && w.now > c.Op.FlipAt+10 {
+ w.rollback(c, "landing deadline")
+ }
+ case "moving", "reverting", "restoring", "serving":
+ w.fixRecord()
+ }
+}
+
+// ---------- the operator (calm phase only) ----------
+
+func (w *world) operator() {
+ c := w.claim
+ if c == nil {
+ return
+ }
+ // readmit a quarantined box once it has retired its old state (--readmit)
+ for _, id := range c.Lost {
+ if b := w.boxByID(id); b != nil && !b.Destroyed && b.Row == nil && b.DB == nil && b.Files == nil && len(b.Procs) == 0 {
+ w.cas(c, func(n *claim) bool {
+ var keep []int
+ for _, x := range n.Lost {
+ if x != id {
+ keep = append(keep, x)
+ }
+ }
+ n.Lost = keep
+ return true
+ })
+ w.logf("operator readmitted box %d", id)
+ return
+ }
+ }
+ // a destroyed box that owes only local chores: declare it lost (claim
+ // §7.2 removes its obligations); compute fencing is the box being gone
+ for _, o := range c.Obl {
+ if o.Kind != "park-local" {
+ continue
+ }
+ if b := w.boxByID(o.Box); b != nil && b.Destroyed {
+ w.cas(c, func(n *claim) bool {
+ var keep []obligation
+ for _, x := range n.Obl {
+ if !(x.Kind == "park-local" && x.Box == o.Box) {
+ keep = append(keep, x)
+ }
+ }
+ n.Obl = keep
+ n.Lost = addUniq(n.Lost, o.Box)
+ return true
+ })
+ w.logf("operator declared box %d lost (local chores only)", o.Box)
+ return
+ }
+ }
+ if c.Holder == nil {
+ return
+ }
+ op := c.Op
+ if (op.Kind != "landing" && op.Kind != "restoring") || op.Committed {
+ return
+ }
+ t := w.boxByID(op.Tgt)
+ if t == nil {
+ return
+ }
+ owesEvidence := op.Exec == op.Tgt
+ owesReturn := op.Kind == "restoring" && op.Exec == -1 && op.DirtyKnown && op.Dirty && op.Phase != "returned"
+ if !owesEvidence && !owesReturn {
+ return
+ }
+ ok := false
+ if on("declare-lost-compute") {
+ ok = t.Destroyed // cloud API: stopped or terminated
+ } else {
+ l := w.execLease[t.ID]
+ ok = t.Destroyed || (l.Op == op.ID && w.now > l.Expires+lostMargin)
+ }
+ if !ok {
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Committed {
+ return false
+ }
+ n.Lost = addUniq(n.Lost, t.ID)
+ if n.Op.Kind == "landing" {
+ n.Op.Kind, n.Op.RollbackID, n.Op.SrcPhase = "restoring", w.newID("rb"), "waiting"
+ }
+ n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.LostBox, n.Op.LostAt = -1, true, false, "released", t.ID, w.now
+ var keep []obligation
+ for _, o := range n.Obl {
+ if o.Kind == "park-local" && o.Box == t.ID {
+ continue
+ }
+ keep = append(keep, o)
+ }
+ n.Obl = keep
+ if owesEvidence { // a box that released already queued these
+ n.Obl = append(n.Obl,
+ w.newObl(n, "park-superseded", op.TgtRegion, -1, "instances/"+host+"/", "", w.now+horizonH),
+ w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
+ }
+ return true
+ }) {
+ for i := range w.acks {
+ if w.acks[i].Box == t.ID && w.acks[i].At >= op.FlipAt {
+ w.acks[i].Exempt = true
+ }
+ }
+ w.logf("operator declared box %d lost for %s", t.ID, op.ID)
+ w.fixRecord()
+ }
+}
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
new file mode 100644
index 000000000..b6c937262
--- /dev/null
+++ b/internal/sim/hostlife/moves_test.go
@@ -0,0 +1,864 @@
+package hostlife
+
+import "fmt"
+
+// worker is one box agent's lifecycle worker: exec-lease renewal, the
+// obligations it owns, then its role in the current operation. One call
+// performs at most one protocol step.
+func (w *world) worker(b *box) {
+ if b.Old {
+ return // a pre-floor executable knows nothing of claims
+ }
+ c, ok := w.readClaim(b)
+ if !ok {
+ return
+ }
+ if b.stale != nil && w.rng.Intn(6) == 0 {
+ // a stalled worker of this box resumes with the claim it read long ago
+ old := b.stale.clone()
+ b.stale = nil
+ if on("revalidate-before-effect") && !sameStep(old, c) {
+ return // it re-reads under its lease, sees the world moved, and stops
+ }
+ c = old
+ } else if w.rng.Intn(10) == 0 {
+ b.stale = c.clone()
+ }
+ // exec lease (claim §7.1)
+ if w.isParticipant(c, b) && !contains(c.Lost, b.ID) {
+ if b.ExecUntil == 0 || b.ExecUntil-w.localNow(b) < execRenew {
+ b.ExecUntil = w.localNow(b) + execTTL
+ w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL}
+ }
+ } else if c == nil || !w.isParticipant(c, b) {
+ b.ExecUntil = 0
+ }
+ if c == nil {
+ return
+ }
+ if contains(c.Lost, b.ID) && on("lost-quarantine") {
+ // a quarantined box retires whatever it kept before anything else
+ if b.Row != nil || b.DB != nil || b.Files != nil || len(b.Procs) > 0 {
+ if w.evidence(b, "quarantine") {
+ inc := 0
+ if b.DB != nil {
+ inc = b.DB.Inc
+ }
+ w.localPark(b, inc)
+ b.Row = nil
+ }
+ }
+ return
+ }
+ for _, o := range c.Obl {
+ if w.ownerOf(o) == b {
+ w.doObligation(b, c, o)
+ return
+ }
+ }
+ if c.Holder == nil {
+ return
+ }
+ switch c.Op.Kind {
+ case "moving":
+ if b.ID == c.Op.Src {
+ w.moveSource(b, c)
+ } else if b.ID == c.Op.Tgt {
+ w.moveReport(b, c)
+ }
+ case "reverting":
+ if b.ID == c.Op.Src {
+ w.revertSource(b, c)
+ }
+ case "landing":
+ if b.ID == c.Op.Tgt {
+ w.landTarget(b, c)
+ } else if b.ID == c.Op.Src {
+ w.holdSourceRow(b, c)
+ }
+ case "restoring":
+ if b.ID == c.Op.Tgt {
+ w.releaseTarget(b, c)
+ } else if b.ID == c.Op.Src {
+ w.recoverSource(b, c)
+ }
+ case "pushing":
+ if b.ID == c.Op.Src {
+ w.pushStep(b, c)
+ }
+ }
+}
+
+type execLease struct {
+ Op string
+ Expires int
+}
+
+func (w *world) leasesSeen(c *claim) bool {
+ for _, id := range c.Op.Parts {
+ l, ok := w.execLease[id]
+ if !ok || l.Op != c.Op.ID || l.Expires < w.now {
+ return false
+ }
+ }
+ return true
+}
+
+// stagingLease: the shared staging-work lease (claim C3), per target region.
+func (w *world) takeStaging(c *claim, b *box) bool {
+ l := w.staging[c.Op.TgtRegion]
+ if l.Op != "" && l.Op != c.Op.ID && l.Until >= w.now {
+ return false
+ }
+ w.staging[c.Op.TgtRegion] = stagingLease{Op: c.Op.ID, Box: b.ID, Until: w.now + stagingTTL}
+ return true
+}
+
+type stagingLease struct {
+ Op string
+ Box int
+ Until int
+}
+
+func (w *world) snapshotBlob(b *box, c *claim) (*blob, *blob) {
+ db := &blob{Kind: "snap", Inc: c.Holder.Inc}
+ if b.DB != nil {
+ db.Writes = append([]int(nil), b.DB.Writes...)
+ db.SealKey = b.DB.Key
+ db.Inc = b.DB.Inc
+ }
+ files := &blob{Kind: "files", Inc: c.Holder.Inc, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...)}
+ return db, files
+}
+
+func (w *world) moveSource(b *box, c *claim) {
+ op := c.Op
+ switch op.Phase {
+ case "leases":
+ if w.leasesSeen(c) {
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "preparing"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "preparing", "ready":
+ if !contains(c.Regions, op.TgtRegion) {
+ w.cas(c, func(n *claim) bool { n.Regions = addUniq(n.Regions, op.TgtRegion); return true })
+ return
+ }
+ srcReady := !on("source-readiness") || (b.Config == c.Holder.Inc && b.Live == c.Holder.App && b.LiveInc == c.Holder.Inc && b.HasKey)
+ if op.Phase == "ready" && op.ReportOK && w.now-op.ReportAt < 60 && op.Auto && srcReady {
+ // auto-cut: admission is atomic with abort eligibility
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.CutAt != 0 || n.Op.Kind != "moving" {
+ return false
+ }
+ n.Op.CutAt = w.now
+ n.Op.CutDeadline = w.now + cutBudget
+ if !on("cut-deadline") {
+ n.Op.CutDeadline = 1 << 30
+ }
+ n.Op.Phase = "stopping"
+ return true
+ })
+ return
+ }
+ if w.now-op.ReqAt > readyWait {
+ // readiness never came: abort on its own (no human)
+ w.logf("abort %s: phase=%s report=%v@%d srcReady=%v auto=%v", op.ID, op.Phase, op.ReportOK, op.ReportAt, srcReady, op.Auto)
+ w.abortMove(c, b)
+ return
+ }
+ if !w.takeStaging(c, b) {
+ return
+ }
+ db, files := w.snapshotBlob(b, c)
+ v1 := w.issue(b.ID, &request{kind: rPut, region: op.TgtRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.ID), b: db})
+ v2 := w.issue(b.ID, &request{kind: rPut, region: op.TgtRegion, key: fmt.Sprintf("moves/%s/%s/files", host, op.ID), b: files})
+ if v1 > 0 && v2 > 0 && op.Phase == "preparing" {
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "ready"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "aborting":
+ if c.oblFor(op.ID) == 0 {
+ w.release(c, op.Src)
+ }
+ case "stopping":
+ if b.Row != nil {
+ b.Row.Status, b.Row.HoldOp = "moving", op.ID
+ }
+ if w.now > op.CutDeadline {
+ w.startRevert(c)
+ return
+ }
+ if !w.evidence(b, op.ID) {
+ return
+ }
+ d := w.digestOf(b)
+ files := b.Files.clone()
+ repl, next := "", 0
+ if b.Row != nil {
+ repl, next = b.Row.Repl, b.Row.Next
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Phase != "stopping" {
+ return false
+ }
+ n.Op.Phase, n.Op.StopAt, n.Op.StopDigest, n.Op.StopFiles = "stopped", w.now, d, files
+ n.Op.Repl, n.Op.Next = repl, next
+ return true
+ })
+ case "stopped":
+ if w.now > op.CutDeadline || b.FailArchive {
+ w.startRevert(c)
+ return
+ }
+ if !w.takeStaging(c, b) {
+ return
+ }
+ db, files := w.snapshotBlob(b, c)
+ if op.SealDB.Ver == 0 {
+ v := w.issue(b.ID, &request{kind: rPut, region: op.TgtRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.ID), b: db})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool {
+ n.Op.SealDB = ref{Region: op.TgtRegion, Key: fmt.Sprintf("moves/%s/%s/db", host, op.ID), Ver: v}
+ return sameOp(n.Op.ID, op.ID)
+ })
+ }
+ return
+ }
+ v := w.issue(b.ID, &request{kind: rPut, region: op.TgtRegion, key: fmt.Sprintf("moves/%s/%s/files", host, op.ID), b: files})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) {
+ return false
+ }
+ n.Op.SealFiles = ref{Region: op.TgtRegion, Key: fmt.Sprintf("moves/%s/%s/files", host, op.ID), Ver: v}
+ n.Op.SealQuiet = w.now + stagingTTL + horizonH
+ if !on("staging-quiet") {
+ n.Op.SealQuiet = w.now
+ }
+ n.Op.Phase = "sealed"
+ return true
+ })
+ }
+ case "sealed":
+ // the flip: kind and exec move together, citing the source's evidence
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Phase != "sealed" || n.Op.StopAt == 0 {
+ return false
+ }
+ n.Op.Kind, n.Op.Exec, n.Op.LandPhase, n.Op.FlipAt = "landing", op.Tgt, "checking", w.now
+ return true
+ }) {
+ w.fixRecord()
+ }
+ }
+}
+
+func (w *world) moveReport(b *box, c *claim) {
+ op := c.Op
+ if op.Phase != "preparing" && op.Phase != "ready" {
+ return
+ }
+ if w.now-op.ReportAt < 20 {
+ return
+ }
+ ok := b.HasKey || !on("readiness-key")
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) {
+ return false
+ }
+ n.Op.ReportAt, n.Op.ReportOK = w.now, ok
+ return true
+ })
+}
+
+func (w *world) abortMove(c *claim, by *box) {
+ op := c.Op
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "moving" || n.Op.CutAt != 0 {
+ return false
+ }
+ n.Op.Phase = "aborting"
+ if on("abort-target-owner") {
+ n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH))
+ }
+ return true
+ })
+ if !on("abort-target-owner") && by != nil {
+ // the source tries to retire remote staging itself
+ w.issue(by.ID, &request{kind: rDelVer, region: op.TgtRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.ID), ver: 1})
+ }
+}
+
+func (w *world) startRevert(c *claim) {
+ op := c.Op
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "moving" {
+ return false
+ }
+ n.Op.Kind, n.Op.Exec = "reverting", op.Src
+ if op.StopAt == 0 {
+ n.Op.RevPhase = "evidence"
+ } else {
+ n.Op.RevPhase = "verify"
+ }
+ n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", w.now+stagingTTL+horizonH))
+ return true
+ })
+}
+
+func (w *world) holdRow(b *box, status, holdOp string, c *claim) {
+ if b.Row == nil {
+ b.Row = &row{Inc: c.Holder.Inc, App: c.Holder.App}
+ }
+ b.Row.Status, b.Row.HoldOp = status, holdOp
+}
+
+// openRow is the conditional open (moves §5.2).
+func (w *world) openRow(b *box, holdOp string) bool {
+ if b.Row == nil {
+ return false
+ }
+ if on("hold-op-open") && b.Row.HoldOp != holdOp {
+ return false
+ }
+ b.Row.Status, b.Row.HoldOp = "ready", ""
+ return true
+}
+
+func (w *world) revertSource(b *box, c *claim) {
+ op := c.Op
+ if !on("revert-journal") && !b.mem[op.ID+"rev"] && (op.RevPhase == "probing" || op.RevPhase == "probed") {
+ // the journal is not trusted after a restart: verify again
+ w.cas(c, func(n *claim) bool { n.Op.RevPhase = "verify"; return sameOp(n.Op.ID, op.ID) })
+ return
+ }
+ if op.RevPhase != "probed" && op.RevPhase != "opened" {
+ w.holdRow(b, "restoring", op.ID, c)
+ }
+ switch op.RevPhase {
+ case "evidence":
+ if w.evidence(b, op.ID) {
+ w.cas(c, func(n *claim) bool { n.Op.RevPhase = "probing"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "verify":
+ if !w.evidence(b, op.ID) {
+ return
+ }
+ ph := "probing"
+ if w.digestOf(b) != op.StopDigest {
+ ph = "stuck"
+ w.logf("revert: digest mismatch %+v vs %+v", w.digestOf(b), op.StopDigest)
+ }
+ w.cas(c, func(n *claim) bool { n.Op.RevPhase = ph; return sameOp(n.Op.ID, op.ID) })
+ case "probing":
+ b.mem[op.ID+"rev"] = true
+ if !w.admits(b, c, op.ID) {
+ return
+ }
+ if b.HasKey { // RenderHeld + MaterializeHeld before every probe
+ b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ }
+ if hasMain(b) || w.spawn(b, c, holderLin(c.Holder), true) {
+ w.cas(c, func(n *claim) bool { n.Op.RevPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ n.Op.ProbeTries++
+ if n.Op.ProbeTries >= probeTries*3 {
+ n.Op.RevPhase = "stuck"
+ }
+ return sameOp(n.Op.ID, op.ID)
+ })
+ case "probed":
+ if w.openRow(b, op.ID) {
+ w.cas(c, func(n *claim) bool { n.Op.RevPhase = "opened"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "opened":
+ if c.oblFor(op.ID) == 0 {
+ w.release(c, op.Src)
+ }
+ }
+}
+
+func (w *world) holdSourceRow(b *box, c *claim) {
+ if b.Row != nil && !c.Op.Committed {
+ b.Row.Status, b.Row.HoldOp = "moving", c.Op.ID
+ }
+}
+
+func (w *world) rollback(c *claim, why string) {
+ op := c.Op
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || n.Op.Committed {
+ return false
+ }
+ n.Op.Kind, n.Op.RollbackID, n.Op.SrcPhase, n.Op.Phase = "restoring", w.newID("rb"), "waiting", "releasing"
+ n.Op.Reason = why
+ return true
+ }) {
+ w.logf("rollback %s: %s", op.ID, why)
+ w.fixRecord()
+ }
+}
+
+func (w *world) landTarget(b *box, c *claim) {
+ op := c.Op
+ if c.Op.Exec != b.ID {
+ return
+ }
+ if !op.Committed {
+ w.holdRow(b, "landing", op.ID, c)
+ if w.now > op.CutDeadline {
+ w.rollback(c, "cut deadline") // N15: every phase before the commit
+ return
+ }
+ }
+ switch op.LandPhase {
+ case "checking":
+ w.cas(c, func(n *claim) bool {
+ n.Boxes = addUniq(n.Boxes, b.ID)
+ n.Op.LandPhase = "install-park"
+ return sameOp(n.Op.ID, op.ID)
+ })
+ case "install-park":
+ if !w.evidence(b, op.ID) {
+ return
+ }
+ if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], "") {
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "install-copy":
+ src := op.SealDB
+ if !on("seal-by-version") {
+ cur := w.buckets[b.Region].current(src.Key)
+ if cur == nil {
+ w.rollback(c, "staging missing")
+ return
+ }
+ src.Ver = cur.ID
+ }
+ v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: "instances/" + host + "/base", srcRegion: b.Region, srcKey: src.Key, srcVer: src.Ver})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.LandPhase = v, "local"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "local":
+ w.installLocal(b, c, op.ID, op.SealFiles, op.LandPhase, func(n *claim) { n.Op.LandPhase = "config" })
+ case "config":
+ if !b.HasKey && on("config-before-probe") {
+ w.rollback(c, "configuration did not render")
+ return
+ }
+ if b.HasKey {
+ b.Config = c.Holder.Inc
+ }
+ b.Live, b.LiveInc = c.Holder.App, c.Holder.Inc
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "restore"; return sameOp(n.Op.ID, op.ID) })
+ case "restore":
+ if b.DB == nil {
+ b.DB = w.restore(b, c.Holder.Inc, c.Holder.Legacy, lin{Op: op.ID, FilesGen: op.ID, Region: b.Region, Ver: op.BaseVer})
+ }
+ if b.DB == nil {
+ w.rollback(c, "restore failed")
+ return
+ }
+ d := w.digestOf(b)
+ w.cas(c, func(n *claim) bool { n.Op.Installed, n.Op.LandPhase = d, "probing"; return sameOp(n.Op.ID, op.ID) })
+ case "probing":
+ if w.now > op.CutDeadline {
+ w.rollback(c, "cut deadline")
+ return
+ }
+ if !w.admits(b, c, op.ID) {
+ return
+ }
+ if hasMain(b) || w.spawn(b, c, lin{Op: op.ID, FilesGen: op.ID, Region: b.Region, Ver: op.BaseVer}, true) {
+ if !on("commit-before-open") {
+ w.openRow(b, op.ID)
+ }
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase, n.Op.ProbedAt = "probed", w.now; return sameOp(n.Op.ID, op.ID) })
+ return
+ }
+ tries := op.ProbeTries + 1
+ w.cas(c, func(n *claim) bool { n.Op.ProbeTries = tries; return sameOp(n.Op.ID, op.ID) })
+ if tries >= probeTries {
+ w.rollback(c, "target would not start")
+ }
+ case "probed":
+ if !op.Committed {
+ if w.now > op.CutDeadline {
+ w.rollback(c, "cut deadline")
+ return
+ }
+ if w.now < op.ProbedAt+15 {
+ return // the settle window between the two readiness checks
+ }
+ // the settle window (§7.7): an app that answered once, did real
+ // work, and then fails its second readiness check
+ if b.FailSettle && hasMain(b) && w.digestOf(b) != op.Installed && w.rng.Intn(2) == 0 {
+ w.logf("box %d failed the settle check for %s", b.ID, op.ID)
+ w.rollback(c, "settle check failed")
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || w.now > n.Op.CutDeadline {
+ return false
+ }
+ n.Op.Committed = true
+ n.Holder.Lineage = lineage{Op: op.ID, Region: b.Region, Ver: op.BaseVer}
+ n.Holder.FilesGen = op.ID
+ q := op.StopAt + horizonH
+ if !on("quiet-before-ack") {
+ q = 0
+ }
+ n.Obl = append(n.Obl,
+ w.newObl(n, "park-superseded", op.SrcRegion, -1, "instances/"+host+"/", "", q),
+ w.newObl(n, "park-local", -1, op.Src, "", "", 0),
+ w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
+ if q > n.Quiet[op.SrcRegion] {
+ n.Quiet[op.SrcRegion] = q
+ }
+ return true
+ }) && w.now > op.CutAt+cutBudget {
+ w.violate("INV-9: %s committed at %d, cut at %d (budget %d)", op.ID, w.now, op.CutAt, cutBudget)
+ }
+ return
+ }
+ if !op.Opened {
+ if w.openRow(b, op.ID) || b.Row != nil && b.Row.Status == "ready" {
+ w.cas(c, func(n *claim) bool { n.Op.Opened = true; return sameOp(n.Op.ID, op.ID) })
+ }
+ return
+ }
+ if c.oblFor(op.ID) == 0 {
+ w.release(c, op.Tgt)
+ }
+ }
+}
+
+// installLocal is the local install, journaled so the files marker is
+// written last (R2-6). seal names the files archive version.
+func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, next func(n *claim)) {
+ if b.Files != nil && b.Files.Gen == gen && b.Files.Done && b.Files.Inc == c.Holder.Inc {
+ // the marker vouches for everything before it
+ w.cas(c, func(n *claim) bool { next(n); return true })
+ return
+ }
+ if b.Files == nil || b.Files.Gen != gen {
+ // fresh extraction: park whatever is there first
+ if b.DB != nil || b.Files != nil {
+ b.Parked++
+ }
+ b.DB = nil
+ b.Files = nil
+ src := w.buckets[b.Region].byID(seal.Key, seal.Ver)
+ if !on("seal-by-version") {
+ src = w.buckets[b.Region].current(seal.Key)
+ }
+ if src == nil || src.B.Files == nil {
+ return
+ }
+ if !on("files-carried") {
+ // the kpmg outage: nothing carries the files directory, and the
+ // landing carries on regardless
+ b.pendingTimers = append([]int(nil), src.B.Timers...)
+ b.Timers = append([]int(nil), b.pendingTimers...)
+ w.cas(c, func(n *claim) bool { next(n); return true })
+ return
+ }
+ f := src.B.Files.clone()
+ f.Gen, f.Done = gen, false
+ if !on("markers-last") {
+ f.Done = true
+ }
+ b.Files = f
+ b.pendingTimers = append([]int(nil), src.B.Timers...)
+ return
+ }
+ // files extracted, marker not yet written: env, timers, columns, marker
+ b.Timers = append([]int(nil), b.pendingTimers...)
+ if src := w.buckets[b.Region].byID(seal.Key, seal.Ver); src != nil {
+ b.Timers = append([]int(nil), src.B.Timers...)
+ }
+ b.Attempt = 0
+ b.History = nil
+ if b.Row != nil {
+ b.Row.Repl, b.Row.Next = c.Op.Repl, c.Op.Next
+ }
+ b.Files.Done = true
+ w.cas(c, func(n *claim) bool { next(n); return true })
+}
+
+func (w *world) release(c *claim, execBox int) {
+ op := c.Op
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) {
+ return false
+ }
+ n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}}
+ return true
+ }) {
+ w.logf("released %s to serving on box %d", op.ID, execBox)
+ w.fixRecord()
+ w.opsDone++
+ switch {
+ case op.Kind == "landing":
+ w.stats["move-done"]++
+ case op.Kind == "restoring" && op.LostBox != 0:
+ w.stats["declared-lost"]++
+ case op.Kind == "restoring" && op.Dirty:
+ w.stats["rollback-dirty"]++
+ case op.Kind == "restoring":
+ w.stats["rollback-clean"]++
+ case op.Kind == "reverting":
+ w.stats["revert"]++
+ case op.Kind == "moving":
+ w.stats["abort"]++
+ case op.Kind == "pushing":
+ w.stats["push"]++
+ }
+ }
+}
+
+func (w *world) releaseTarget(b *box, c *claim) {
+ op := c.Op
+ if op.Exec == b.ID {
+ w.holdRow(b, "releasing", op.RollbackID, c)
+ if !w.evidence(b, op.RollbackID) {
+ return
+ }
+ dirty := false
+ if op.LandPhase == "probing" || op.LandPhase == "probed" {
+ dirty = w.digestOf(b) != op.Installed
+ }
+ if !on("dirty-return") {
+ dirty = false
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Exec != b.ID {
+ return false
+ }
+ n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.TgtStopAt = -1, true, dirty, "released", w.now
+ q := w.now + horizonH
+ if on("target-park") {
+ n.Obl = append(n.Obl, w.newObl(n, "park-superseded", op.TgtRegion, -1, "instances/"+host+"/", "", q))
+ }
+ n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
+ if !dirty {
+ n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, b.ID, "", "", 0))
+ }
+ if q > n.Quiet[op.TgtRegion] {
+ n.Quiet[op.TgtRegion] = q
+ }
+ return true
+ })
+ return
+ }
+ if op.Dirty && op.Phase == "released" && op.Exec == -1 {
+ // return the target's writes over the approved lane (M17)
+ db, files := w.snapshotBlob(b, c)
+ if op.ReturnDB.Ver == 0 {
+ v := w.issue(b.ID, &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.RollbackID), b: db})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool {
+ n.Op.ReturnDB = ref{Region: op.SrcRegion, Key: fmt.Sprintf("moves/%s/%s/db", host, op.RollbackID), Ver: v}
+ return sameOp(n.Op.ID, op.ID)
+ })
+ }
+ return
+ }
+ v := w.issue(b.ID, &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/files", host, op.RollbackID), b: files})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) {
+ return false
+ }
+ n.Op.ReturnFiles = ref{Region: op.SrcRegion, Key: fmt.Sprintf("moves/%s/%s/files", host, op.RollbackID), Ver: v}
+ n.Op.ReturnQuiet = w.now + horizonH
+ n.Op.Phase = "returned"
+ n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, b.ID, "", "", 0))
+ return true
+ })
+ }
+ }
+}
+
+func (w *world) recoverSource(b *box, c *claim) {
+ op := c.Op
+ if !on("rollback-journal") && !b.mem[op.RollbackID] && op.SrcPhase != "waiting" && op.SrcPhase != "opened" && op.SrcPhase != "stuck" {
+ // without a durable journal a restarted source starts over
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "claimed"; return sameOp(n.Op.ID, op.ID) })
+ b.mem[op.RollbackID] = true
+ return
+ }
+ b.mem[op.RollbackID] = true
+ switch op.SrcPhase {
+ case "waiting":
+ if b.Row != nil && !op.Committed {
+ b.Row.Status, b.Row.HoldOp = "restoring", op.RollbackID
+ }
+ if op.Exec == -1 && op.DirtyKnown && (!op.Dirty || op.Phase == "returned") {
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Exec != -1 {
+ return false
+ }
+ n.Op.Exec, n.Op.SrcPhase = op.Src, "claimed"
+ return true
+ })
+ }
+ case "claimed":
+ w.holdRow(b, "restoring", op.RollbackID, c)
+ next := "verify"
+ if op.Dirty {
+ next = "install-park"
+ }
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = next; return sameOp(n.Op.ID, op.ID) })
+ case "verify":
+ if !w.evidence(b, op.RollbackID) {
+ return
+ }
+ ph := "config"
+ if w.digestOf(b) != op.StopDigest {
+ ph = "stuck"
+ w.logf("recover: digest mismatch %+v vs %+v", w.digestOf(b), op.StopDigest)
+ }
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = ph; return sameOp(n.Op.ID, op.ID) })
+ case "install-park":
+ if !w.evidence(b, op.RollbackID) {
+ return
+ }
+ if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, "") {
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "install-copy":
+ v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: "instances/" + host + "/base", srcRegion: b.Region, srcKey: op.ReturnDB.Key, srcVer: op.ReturnDB.Ver})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.SrcPhase = v, "local"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "local":
+ w.installLocal(b, c, op.RollbackID, op.ReturnFiles, "", func(n *claim) { n.Op.SrcPhase = "config" })
+ case "config":
+ b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probing"; return sameOp(n.Op.ID, op.ID) })
+ case "probing":
+ if !w.admits(b, c, op.RollbackID) {
+ return
+ }
+ L := holderLin(c.Holder)
+ if op.Dirty {
+ L = lin{Op: op.RollbackID, FilesGen: op.RollbackID, Region: b.Region, Ver: op.BaseVer}
+ }
+ if hasMain(b) || w.spawn(b, c, L, true) {
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ n.Op.ProbeTries++
+ if n.Op.ProbeTries >= probeTries*3 {
+ n.Op.SrcPhase = "stuck"
+ }
+ return sameOp(n.Op.ID, op.ID)
+ })
+ case "probed":
+ if op.Dirty && c.Holder.Lineage.Op != op.RollbackID {
+ w.cas(c, func(n *claim) bool {
+ n.Holder.Lineage = lineage{Op: op.RollbackID, Region: b.Region, Ver: op.BaseVer}
+ n.Holder.FilesGen = op.RollbackID
+ n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", op.ReturnQuiet))
+ return sameOp(n.Op.ID, op.ID)
+ })
+ return
+ }
+ if w.openRow(b, op.RollbackID) {
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "opened"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "opened":
+ if c.oblFor(op.ID) == 0 {
+ w.release(c, op.Src)
+ }
+ }
+}
+
+func (w *world) pushStep(b *box, c *claim) {
+ op := c.Op
+ switch op.Phase {
+ case "stopping":
+ w.holdRow(b, "moving", op.ID, c)
+ if !w.evidence(b, op.ID) {
+ return
+ }
+ var writes []int
+ if b.DB != nil {
+ writes = append(writes, b.DB.Writes...)
+ }
+ w.nextW++
+ mark := w.nextW
+ w.acks = append(w.acks, ack{W: mark, Inc: c.Holder.Inc, Box: b.ID, At: w.now, Kind: "write"})
+ writes = append(writes, mark)
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Phase != "stopping" {
+ return false
+ }
+ n.Op.Phase, n.Op.StopAt, n.Op.PushWrites = "park", w.now, writes
+ return true
+ })
+ case "park":
+ if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, "") {
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "install":
+ key := 0
+ if b.Files != nil {
+ key = b.Files.Key
+ }
+ v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: "instances/" + host + "/base", b: &blob{Kind: "base", Inc: c.Holder.Inc, Gen: op.ID, Writes: op.PushWrites, SealKey: key}})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.Phase = v, "restore"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "restore":
+ if b.DB != nil {
+ b.Parked++
+ b.DB = nil
+ }
+ b.DB = w.restore(b, c.Holder.Inc, c.Holder.Legacy, lin{Op: op.ID, FilesGen: c.Holder.FilesGen, Region: b.Region, Ver: op.BaseVer})
+ if b.DB == nil {
+ return
+ }
+ // every probe renders config and materializes the release for the
+ // held row first (the passes skip held rows): RenderHeld, MaterializeHeld
+ if !b.HasKey {
+ return
+ }
+ b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "probing"; return sameOp(n.Op.ID, op.ID) })
+ case "probing":
+ if !w.admits(b, c, op.ID) {
+ return
+ }
+ if hasMain(b) || w.spawn(b, c, lin{Op: op.ID, FilesGen: c.Holder.FilesGen, Region: b.Region, Ver: op.BaseVer}, true) {
+ w.cas(c, func(n *claim) bool {
+ n.Op.Phase = "probed"
+ n.Holder.Lineage = lineage{Op: op.ID, Region: b.Region, Ver: op.BaseVer}
+ q := op.StopAt + horizonH
+ if q > n.Quiet[b.Region] {
+ n.Quiet[b.Region] = q
+ }
+ return sameOp(n.Op.ID, op.ID)
+ })
+ }
+ case "probed":
+ if w.openRow(b, op.ID) {
+ w.release(c, b.ID)
+ }
+ }
+}
+
+// sameStep: the operation and every phase the worker branches on are what
+// the stale read said (claim C3's revalidation under the lease).
+func sameStep(a, b *claim) bool {
+ if a == nil || b == nil {
+ return a == b
+ }
+ x, y := a.Op, b.Op
+ return x.ID == y.ID && x.Kind == y.Kind && x.Phase == y.Phase && x.LandPhase == y.LandPhase &&
+ x.SrcPhase == y.SrcPhase && x.RevPhase == y.RevPhase && x.Exec == y.Exec && x.Committed == y.Committed &&
+ x.Opened == y.Opened && len(a.Obl) == len(b.Obl) && (a.Holder == nil) == (b.Holder == nil)
+}
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh
new file mode 100755
index 000000000..69331449a
--- /dev/null
+++ b/internal/sim/hostlife/mutate.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+# Mutation checks for the hostlife model (move-any-app spec §14.2.5).
+#
+# Each rule is dropped in its own scratch copy of the module, never in
+# place: an interrupted in-place mutation once left a disabled guard in a
+# source file. Rules run in parallel.
+#
+# internal/sim/hostlife/mutate.sh 3000 # every rule
+# internal/sim/hostlife/mutate.sh 30000 rule-a rule-b # named rules
+# internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a pair, dropped together
+#
+# A rule is CAUGHT when at least one seed fails. Scratch copies live under
+# ${HOSTLIFE_SCRATCH:-$HOME/.cache/hostlife-sim} and are removed after use.
+set -u
+SEEDS=${1:?seeds}
+shift
+ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel)
+SCRATCH=${HOSTLIFE_SCRATCH:-$HOME/.cache/hostlife-sim}
+mkdir -p "$SCRATCH/gotmp"
+RULES="$*"
+if [ -z "$RULES" ]; then
+ RULES=$(sed -n '/^var allRules/,/^}/p' "$ROOT/internal/sim/hostlife/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')
+fi
+
+one() {
+ r=$1
+ d="$SCRATCH/mut-$(echo "$r" | tr ',' '+')"
+ rm -rf "$d"
+ mkdir -p "$d/internal/sim"
+ cp "$ROOT/go.mod" "$ROOT/go.sum" "$d/"
+ cp -a "$ROOT/internal/sim/hostlife" "$d/internal/sim/"
+ sed -i "s/^var mutated = \"\"/var mutated = \"$r\"/" "$d/internal/sim/hostlife/rules_test.go"
+ if ! grep -q "^var mutated = \"$r\"" "$d/internal/sim/hostlife/rules_test.go"; then
+ echo "SEDFAIL $r"
+ return
+ fi
+ out=$(cd "$d" && GOTMPDIR="$SCRATCH/gotmp" TMPDIR="$SCRATCH/gotmp" HOSTLIFE_SEEDS=$SEEDS \
+ go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1 -timeout 120m -v 2>&1)
+ rc=$?
+ if echo "$out" | grep -q "violated an invariant"; then
+ n=$(echo "$out" | grep -o "[0-9]* of $SEEDS seeds violated" | head -1)
+ echo "CAUGHT $r: $n"
+ elif [ $rc -ne 0 ]; then
+ echo "CAUGHT $r: test failed rc=$rc"
+ else
+ echo "MISSED $r ($SEEDS seeds)"
+ fi
+ rm -rf "$d"
+}
+export -f one
+export SEEDS ROOT SCRATCH
+printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {}
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
new file mode 100644
index 000000000..241142c2c
--- /dev/null
+++ b/internal/sim/hostlife/protocol_test.go
@@ -0,0 +1,553 @@
+package hostlife
+
+import (
+ "fmt"
+ "strings"
+)
+
+const host = "h"
+
+// ---------- small helpers ----------
+
+func (w *world) agentUp(b *box) bool {
+ return b != nil && !b.Destroyed && !b.Frozen && !b.AgentDown && !b.AgentPaused
+}
+
+func (w *world) localNow(b *box) int { return w.now + b.Skew }
+
+// readClaim is a fresh read by a box agent (C4). It fails when the box
+// cannot reach the control bucket (C6: a failed read never acts).
+func (w *world) readClaim(b *box) (*claim, bool) {
+ if !w.agentUp(b) || b.Partitioned {
+ return nil, false
+ }
+ c := w.claim.clone()
+ b.snap = c.clone()
+ return c, true
+}
+
+// admissionClaim is what admission sees: fresh, unless the rule is mutated,
+// in which case the box's last cached snapshot.
+func (w *world) admissionClaim(b *box) (*claim, bool) {
+ if on("fresh-admission") {
+ return w.readClaim(b)
+ }
+ if b.snap != nil {
+ return b.snap.clone(), true
+ }
+ return w.readClaim(b)
+}
+
+// cas writes the claim if nobody wrote since `old` was read. On an ETag
+// conflict it re-reads once and re-applies, but only if the op id is
+// unchanged (C2); the mutation drops that condition.
+func (w *world) cas(old *claim, mut func(c *claim) bool) bool {
+ cur := w.claim
+ curVer := 0
+ if cur != nil {
+ curVer = cur.Ver
+ }
+ oldVer := 0
+ if old != nil {
+ oldVer = old.Ver
+ }
+ base := old
+ if curVer != oldVer {
+ if old == nil || cur == nil {
+ return false
+ }
+ if on("claim-cas-opid") && cur.Op.ID != old.Op.ID {
+ return false
+ }
+ base = cur
+ }
+ n := base.clone()
+ if n == nil {
+ n = &claim{}
+ }
+ if !mut(n) {
+ return false
+ }
+ n.Ver = curVer + 1
+ w.claim = n
+ return true
+}
+
+func (w *world) isParticipant(c *claim, b *box) bool {
+ return c != nil && c.Op.Kind != "serving" && c.Op.Kind != "" && contains(c.Op.Parts, b.ID)
+}
+
+func liveProcs(b *box) []*proc {
+ if b.Destroyed {
+ return nil
+ }
+ return b.Procs
+}
+
+func hasMain(b *box) bool {
+ for _, p := range b.Procs {
+ if p.Main {
+ return true
+ }
+ }
+ return false
+}
+
+func setKey(xs []int) string { return intsKey(xs) }
+
+func (w *world) timerDigest(b *box) string {
+ if on("timer-canonical") {
+ return fmt.Sprintf("%s/%d", setKey(b.Timers), b.Attempt)
+ }
+ return fmt.Sprintf("%s/%s/%d", setKey(b.Timers), setKey(b.History), b.Attempt)
+}
+
+func (w *world) digestOf(b *box) digest {
+ d := digest{Valid: true}
+ if b.DB != nil {
+ d.Writes = setKey(b.DB.Writes)
+ }
+ if b.Files != nil {
+ d.Files = fmt.Sprintf("%d/%d/%d", b.Files.Inc, b.Files.Key, b.Files.Env)
+ }
+ d.Timers = w.timerDigest(b)
+ return d
+}
+
+// ---------- stop evidence (claim §6.1) ----------
+
+// evidence kills the host's process tree on b and reports whether stop
+// evidence holds. It reads only current system state unless mutated.
+func (w *world) evidence(b *box, opID string) bool {
+ if b.Destroyed {
+ return false
+ }
+ var keep []*proc
+ killed := len(b.Procs)
+ for _, p := range b.Procs {
+ if on("evidence-whole-tree") {
+ continue // cleanup-only reopen kills the cgroup and every identified stray
+ }
+ if p.Strict || p.Main {
+ continue // cgroup kill, and SIGTERM to the main
+ }
+ keep = append(keep, p) // an escaped descendant survives both
+ }
+ b.Procs = keep
+ if !on("evidence-from-state") {
+ // evidence only from this agent's memory: a stop it watched, or a
+ // remembered history. After a restart neither exists, and an empty
+ // box answers ErrStopUnproven forever (R2-2).
+ if b.stopped == nil {
+ b.stopped = map[string]bool{}
+ }
+ if killed > 0 {
+ b.stopped[opID] = true
+ }
+ if !b.stopped[opID] {
+ return false
+ }
+ }
+ if on("evidence-whole-tree") {
+ return len(b.Procs) == 0
+ }
+ return true // the mutation certifies an empty cgroup, blind to escapees
+}
+
+// ---------- restore and spawn ----------
+
+type lin struct {
+ Op string
+ FilesGen string
+ Region int
+ Ver int
+}
+
+func (w *world) restore(b *box, inc int, legacy bool, L lin) *localDB {
+ bk := w.buckets[b.Region]
+ db := &localDB{Inc: inc, Gen: L.Op}
+ if L.Op != "" {
+ if L.Region != b.Region {
+ return nil
+ }
+ v := bk.byID("instances/"+host+"/base", L.Ver)
+ if v == nil {
+ return nil
+ }
+ db.Writes = append(db.Writes, v.B.Writes...)
+ db.Key = v.B.SealKey
+ db.Inc = v.B.Inc
+ }
+ var best *version
+ if on("restore-lineage-filter") {
+ for _, v := range bk.objs["instances/"+host+"/ltx"] {
+ if v.Marker {
+ continue
+ }
+ okInc := v.B.Inc == inc || (legacy && v.B.Inc == 0)
+ if okInc && v.B.Gen == L.Op && (best == nil || len(v.B.Writes) >= len(best.B.Writes)) {
+ best = v
+ }
+ }
+ } else {
+ best = bk.current("instances/" + host + "/ltx")
+ }
+ if best != nil {
+ if best.B.Inc != 0 {
+ db.Inc = best.B.Inc
+ }
+ db.Writes = unionInts(db.Writes, best.B.Writes)
+ if db.Key == 0 {
+ db.Key = best.B.SealKey
+ }
+ }
+ return db
+}
+
+func unionInts(a, b []int) []int {
+ seen := map[int]bool{}
+ var out []int
+ for _, x := range append(append([]int(nil), a...), b...) {
+ if !seen[x] {
+ seen[x] = true
+ out = append(out, x)
+ }
+ }
+ return out
+}
+
+// spawn starts the app on b for the holder incarnation, with the given
+// expected lineage. It returns true if the app answered its readiness path.
+func (w *world) spawn(b *box, c *claim, L lin, probe bool) bool {
+ h := c.Holder
+ if b.Old {
+ // an old executable: no claim, no markers, best-effort placement
+ if b.DB == nil {
+ b.DB = w.restore(b, h.Inc, true, lin{})
+ }
+ } else {
+ if b.DB == nil {
+ b.DB = w.restore(b, h.Inc, h.Legacy, L)
+ if b.DB == nil {
+ return false
+ }
+ }
+ if on("start-check") {
+ if b.DB.Gen != L.Op || b.DB.Inc != h.Inc && !(h.Legacy && b.DB.Inc == 0) {
+ w.logf("box %d start check refused: db gen %q inc %d want %q %d", b.ID, b.DB.Gen, b.DB.Inc, L.Op, h.Inc)
+ return false
+ }
+ if b.Files != nil && (b.Files.Gen != L.FilesGen || b.Files.Inc != h.Inc) {
+ w.logf("box %d start check refused: files gen %q inc %d", b.ID, b.Files.Gen, b.Files.Inc)
+ return false
+ }
+ if b.Files == nil && L.FilesGen != "" {
+ w.logf("box %d start check refused: files missing for gen %q", b.ID, L.FilesGen)
+ return false
+ }
+ }
+ }
+ // what the app sees
+ if b.DB.Inc != 0 && b.DB.Inc != h.Inc {
+ w.violate("box %d started inc %d over a database of inc %d", b.ID, h.Inc, b.DB.Inc)
+ }
+ if b.Files != nil && b.Files.Inc != h.Inc {
+ w.violate("box %d started inc %d with files (instance.key) of inc %d", b.ID, h.Inc, b.Files.Inc)
+ }
+ if b.Config != 0 && b.Config != h.Inc {
+ w.violate("box %d started inc %d with config.env rendered for inc %d", b.ID, h.Inc, b.Config)
+ }
+ if b.Files == nil {
+ w.nextID++
+ b.Files = &filesDir{Inc: h.Inc, Key: w.nextID, Gen: L.FilesGen, Env: w.nextID, Done: true}
+ }
+ if b.DB.Key == 0 {
+ b.DB.Key = b.Files.Key // unsealed data (never booted) adopts the key
+ }
+ if b.DB.Key != b.Files.Key {
+ w.violate("INV-4: box %d started inc %d with instance.key %d over data sealed with %d", b.ID, h.Inc, b.Files.Key, b.DB.Key)
+ return false
+ }
+ // FailApp is the injected "the target cannot run it" fault: landing probes only
+ healthy := b.Config == h.Inc && b.Live == h.App && b.LiveInc == h.Inc && !(probe && b.FailApp && c.Op.Kind == "landing")
+ if !healthy {
+ w.logf("box %d unhealthy start inc %d: cfg=%d live=%s/%d fail=%v kind=%s", b.ID, h.Inc, b.Config, b.Live, b.LiveInc, b.FailApp, c.Op.Kind)
+ return false
+ }
+ strict := !b.Old && (on("strict-spawn") || w.rng.Intn(2) == 0)
+ b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: L.Op, Box: b.ID})
+ if w.rng.Intn(2) == 0 {
+ b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: L.Op, Box: b.ID})
+ }
+ w.logf("box %d spawned inc %d gen %q (probe=%v strict=%v)", b.ID, h.Inc, L.Op, probe, strict)
+ return true
+}
+
+func holderLin(h *holder) lin {
+ return lin{Op: h.Lineage.Op, FilesGen: h.LinFiles(), Region: h.Lineage.Region, Ver: h.Lineage.Ver}
+}
+
+// LinFiles: the files generation compatible with the lineage. Moves set it
+// to the move id; a push (not modelled as a separate generation of files)
+// keeps it.
+func (h *holder) LinFiles() string { return h.FilesGen }
+
+// ---------- admission (C4, §19.1 of the moves spec) ----------
+
+func (w *world) admits(b *box, c *claim, probe string) bool {
+ if c == nil || c.Holder == nil || b.Row == nil || b.Row.Inc != c.Holder.Inc {
+ return false
+ }
+ if on("lost-quarantine") && contains(c.Lost, b.ID) {
+ return false
+ }
+ if on("exec-admission") && c.Op.Exec != b.ID {
+ return false
+ }
+ if b.Retired[c.Holder.Inc] {
+ return false
+ }
+ if w.isParticipant(c, b) && b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil {
+ return false // self-fenced until the lease is renewed
+ }
+ if !w.isParticipant(c, b) {
+ b.ExecUntil = 0 // a fresh read with no operation ends the fence (§7.1)
+ }
+ op := c.Op
+ switch op.Kind {
+ case "serving":
+ return probe == "" && b.Row.Status == "ready"
+ case "moving":
+ return probe == "" && b.ID == op.Src && op.CutAt == 0 && b.Row.Status == "ready"
+ case "reverting":
+ if probe != "" {
+ return probe == op.ID && b.ID == op.Src && op.RevPhase == "probing"
+ }
+ return b.ID == op.Src && op.RevPhase == "opened" && b.Row.Status == "ready"
+ case "landing":
+ if probe != "" {
+ return probe == op.ID && b.ID == op.Tgt && op.LandPhase == "probing"
+ }
+ return b.ID == op.Tgt && op.Committed && b.Row.Status == "ready"
+ case "restoring":
+ if probe != "" {
+ return probe == op.RollbackID && b.ID == op.Src && op.SrcPhase == "probing"
+ }
+ return b.ID == op.Src && op.SrcPhase == "opened" && b.Row.Status == "ready"
+ case "pushing":
+ return probe == op.ID && op.Phase == "probing"
+ }
+ return false
+}
+
+// ---------- parking (claim §6.2) ----------
+
+// parkStep advances one park of `prefix` in b's own bucket into dest. It
+// returns true when the location is verified empty after the quiet time.
+// excludeGen keeps the current lineage's objects (push).
+func (w *world) parkStep(b *box, prefix, dest string, quiet int, excludeGen string) bool {
+ return w.parkDepth(b, prefix, dest, quiet, excludeGen, 0)
+}
+
+func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen string, depth int) bool {
+ if depth > 8 {
+ return false // a park that cannot finish: reported as non-convergence
+ }
+ bk := w.buckets[b.Region]
+ // the parker takes the location's replica lease first (claim §6.2 step 1):
+ // its own lock.json, renewed on every visit
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: prefix + "lock.json", b: &blob{Kind: "lock", Text: fmt.Sprintf("box%d@%d", b.ID, w.now)}})
+ manKey := dest + "manifest"
+ if !on("retirement-ids") {
+ // one destination per operation, shared by every retirement event
+ if i := strings.Index(dest, "/"+host+"/"); i >= 0 {
+ manKey = dest[:i+len(host)+2] + "manifest"
+ dest = dest[:i+len(host)+2]
+ }
+ }
+ man := bk.current(manKey)
+ if man == nil {
+ // snapshot every data version except the live lock
+ var snap []ref
+ for _, k := range bk.keys(prefix) {
+ if strings.HasSuffix(k, "lock.json") && on("park-skip-lock") {
+ continue
+ }
+ vs := bk.objs[k]
+ for i, v := range vs {
+ if v.Marker {
+ continue
+ }
+ if excludeGen != "" && v.B != nil && v.B.Gen == excludeGen {
+ continue
+ }
+ if !on("park-all-versions") && i != len(vs)-1 {
+ continue
+ }
+ snap = append(snap, ref{Region: b.Region, Key: k, Ver: v.ID})
+ }
+ }
+ // copy each version by id; a destination keyed by the source
+ // version is idempotent, so progress accumulates across attempts
+ all := true
+ for _, r := range snap {
+ dk := dest + strings.TrimPrefix(r.Key, "instances/"+host+"/") + fmt.Sprintf(".v%d", r.Ver)
+ if bk.current(dk) != nil {
+ continue
+ }
+ all = false
+ w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: dk, srcRegion: b.Region, srcKey: r.Key, srcVer: r.Ver})
+ }
+ if !all {
+ return false
+ }
+ // the manifest last, once every copy exists
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manKey, b: &blob{Kind: "manifest", Refs: snap}})
+ return false
+ }
+ // delete the manifest's versions
+ for _, r := range man.B.Refs {
+ if bk.byID(r.Key, r.Ver) == nil {
+ continue
+ }
+ if on("park-by-version") {
+ w.issue(b.ID, &request{kind: rDelVer, region: b.Region, key: r.Key, ver: r.Ver})
+ } else {
+ w.issue(b.ID, &request{kind: rDelKey, region: b.Region, key: r.Key})
+ }
+ return false
+ }
+ if on("quiet-before-ack") {
+ if w.now < quiet {
+ return false
+ }
+ // a straggler written after the snapshot: park it as a new event
+ for _, k := range bk.keys(prefix) {
+ if strings.HasSuffix(k, "lock.json") && on("park-skip-lock") {
+ continue
+ }
+ for _, v := range bk.objs[k] {
+ if !v.Marker && !(excludeGen != "" && v.B.Gen == excludeGen) {
+ // start a further retirement event under a fresh id
+ return w.parkDepth(b, prefix, dest+"s/", quiet, excludeGen, depth+1)
+ }
+ }
+ }
+ }
+ return true
+}
+
+// localPark retires b's local state for incarnation inc under the host
+// guard: a retired marker first, then rename everything aside.
+func (w *world) localPark(b *box, inc int) {
+ if on("hostguard") {
+ if b.Retired == nil {
+ b.Retired = map[int]bool{}
+ }
+ b.Retired[inc] = true
+ }
+ if b.DB != nil || b.Files != nil || b.Config != 0 || b.Live != "" {
+ b.Parked++
+ }
+ b.DB, b.Files, b.Config, b.Live, b.LiveInc = nil, nil, 0, "", 0
+ b.Timers, b.History, b.Attempt = nil, nil, 0
+}
+
+// ---------- obligations ----------
+
+func (w *world) ownerOf(o obligation) *box {
+ if o.Kind == "park-local" {
+ b := w.boxByID(o.Box)
+ if b == nil || b.Destroyed {
+ return nil
+ }
+ return b
+ }
+ return w.regionBox(o.Region)
+}
+
+// doObligation runs one step of an obligation owned by b.
+func (w *world) doObligation(b *box, c *claim, o obligation) {
+ switch o.Kind {
+ case "park-local":
+ if !w.evidence(b, o.Op) {
+ return
+ }
+ inc := 0
+ if c.Holder != nil {
+ inc = c.Holder.Inc
+ }
+ if b.DB != nil && b.DB.Inc != 0 {
+ inc = b.DB.Inc
+ }
+ w.localPark(b, inc)
+ if b.Row != nil && b.Row.HoldOp == o.Op || b.Row != nil && (c.Holder == nil || b.ID != c.Op.Exec) {
+ b.Row = nil
+ }
+ default:
+ quiet := o.Quiet
+ if o.Kind == "park-replica" || o.Kind == "park-superseded" {
+ // the owner first proves the region's box runs nothing for the
+ // host, when it is not the current executor
+ if c.Op.Exec != b.ID || c.Holder == nil {
+ if !w.evidence(b, o.Op) {
+ return
+ }
+ }
+ // a replicator's PUT signed before that evidence can land up to
+ // the horizon later: verify only after it (this model's finding)
+ if b.evidAt == nil {
+ b.evidAt = map[string]int{}
+ }
+ if _, ok := b.evidAt[o.ID]; !ok {
+ b.evidAt[o.ID] = w.now
+ }
+ if on("quiet-before-ack") && b.evidAt[o.ID]+horizonH > quiet {
+ quiet = b.evidAt[o.ID] + horizonH
+ }
+ }
+ if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.excludeGen(c)) {
+ return
+ }
+ }
+ w.cas(c, func(n *claim) bool {
+ for i, x := range n.Obl {
+ if x.ID == o.ID {
+ n.Obl = append(n.Obl[:i:i], n.Obl[i+1:]...)
+ if o.Ret == "legacy" && n.oblFor("adopt") == 0 {
+ n.Complete = true // every region has acknowledged
+ }
+ return true
+ }
+ }
+ return false
+ })
+ w.logf("box %d finished obligation %s %s %s", b.ID, o.ID, o.Kind, o.Prefix)
+}
+
+func (o obligation) Dest() string {
+ if o.Kind == "park-replica" {
+ return fmt.Sprintf("parked/%s/%s/%s/", o.Ret, host, o.ID)
+ }
+ return fmt.Sprintf("superseded/%s/%s/%s/", o.Op, host, o.ID)
+}
+
+func (o obligation) excludeGen(c *claim) string { return o.Exclude }
+
+func (w *world) newObl(c *claim, kind string, region, boxID int, prefix, ret string, quiet int) obligation {
+ return obligation{ID: w.newID("ob"), Op: c.Op.ID, Kind: kind, Region: region, Box: boxID, Prefix: prefix, Ret: ret, Quiet: quiet}
+}
+
+func (c *claim) oblFor(op string) int {
+ n := 0
+ for _, o := range c.Obl {
+ if o.Op == op {
+ n++
+ }
+ }
+ return n
+}
+
+// sameOp is the op.id condition every transition carries (claim C2). The
+// mutation drops it everywhere at once, CAS retry and closures alike.
+func sameOp(a, b string) bool { return !on("claim-cas-opid") || a == b }
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
new file mode 100644
index 000000000..340df4aa6
--- /dev/null
+++ b/internal/sim/hostlife/rules_test.go
@@ -0,0 +1,76 @@
+package hostlife
+
+import "strings"
+
+// Every protocol rule the model enforces has a name here. The mutation
+// harness (spec §14.2) copies the tree to a scratch directory, sets
+// `mutated` below to one rule name, runs the simulation, and requires at
+// least one seed to fail. A rule whose mutation no seed catches is either
+// redundant or untested, and the run says which.
+//
+// Never edit `mutated` in place; the harness does it in a copy.
+var mutated = ""
+
+func on(rule string) bool {
+ for _, m := range strings.Split(mutated, ",") {
+ if m == rule {
+ return false
+ }
+ }
+ return true
+}
+
+// allRules is the mutation list, in spec order. The comment names the
+// finding or spec section each rule answers.
+var allRules = []string{
+ // claim spec
+ "claim-op-exclusive", // C2/§4: one operation at a time
+ "claim-cas-opid", // C2: every CAS conditional on op.id
+ "revalidate-before-effect", // C3: a worker re-reads under its lease before acting
+ "fresh-admission", // C4: admission reads the claim fresh
+ "exec-admission", // C4/K1: op.exec names this box
+ "recovery-pass", // C2/§8: console claim-recovery pass
+ "fresh-incarnation", // §5.1/R3-12
+ "touched-incomplete", // §9/J-N5: adopted legacy parks every region
+ "legacy-discovery", // this model's finding: park legacy residue at adoption
+ "obligations-block-ops", // this model's finding: no op over a pending chore
+ "park-by-version", // C3/J-N1: destructive calls name versions
+ "park-all-versions", // §6.2 step 5: noncurrent versions too
+ "park-skip-lock", // §6.2 step 2/J-N6
+ "retirement-ids", // §6.2/J-D5/J-N7
+ "hostguard", // §6.4/J-N8
+ "purge-reserve-first", // §5.3/J-N9
+ "purge-adopts", // this model's finding: purge claims unclaimed legacy records first
+ "purge-journal", // this model's finding: the reservation is the purge's journal
+ "door-by-version", // §6.5/J-N10
+ "strict-spawn", // §6.1/J-D3
+ "evidence-whole-tree", // §6.1: stray and non-strict processes
+ "evidence-from-state", // §6.1/R2-2
+ "watchdog-independent", // §7.1 self-fencing outside the agent
+ "declare-lost-compute", // §7.2 compute fencing (this model's finding)
+ "lost-quarantine", // §7.2
+ "floor-boot-recovery", // §10/J-N12
+ "participant-rows", // claim §2/R2-4
+ "stale-hold-release", // this model's finding: release a hold whose op ended
+ "restore-lineage-filter", // this model's finding (replication exception)
+ "quiet-before-ack", // this model's finding (late writes after a park)
+ // moves spec
+ "seal-by-version", // J-N2: landing copies sealed versions
+ "staging-quiet", // J-N2: staging retired after its writers' horizon
+ "commit-before-open", // INV-5
+ "hold-op-open", // §5.2 conditional open
+ "start-check", // INV-4
+ "markers-last", // R2-6
+ "revert-journal", // J-N11
+ "rollback-journal", // R2-3
+ "dirty-return", // INV-2
+ "target-park", // R2-5/INV-10
+ "abort-target-owner", // J-N13
+ "timer-freeze", // J-N14 runner bookkeeping
+ "timer-canonical", // J-N14 prune path
+ "cut-deadline", // J-N15
+ "readiness-key", // T2
+ "source-readiness", // S1: the source can run the instance before the cut
+ "files-carried", // §8 (the kpmg outage)
+ "config-before-probe", // L3 (the kpmg outage)
+}
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
new file mode 100644
index 000000000..ac1850524
--- /dev/null
+++ b/internal/sim/hostlife/sim_test.go
@@ -0,0 +1,433 @@
+package hostlife
+
+import (
+ "fmt"
+ "math/rand"
+ "os"
+ "strconv"
+ "strings"
+ "testing"
+)
+
+const (
+ chaosSteps = 2000
+ calmSteps = 6000
+)
+
+func newWorld(seed int64, verbose bool) *world {
+ w := &world{seed: seed, rng: rand.New(rand.NewSource(seed)), verbose: verbose,
+ stores: map[string]bool{app0: true, app1: true}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},
+ control: newBucket(), delivered: map[int]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
+ for r := 0; r < nRegions; r++ {
+ w.buckets[r] = newBucket()
+ }
+ for _, f := range []string{"partition", "freeze", "pause", "destroy"} {
+ w.fail[f] = w.rng.Intn(2) == 0
+ }
+ for r := 0; r < nRegions; r++ {
+ b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
+ if r != 0 && w.rng.Intn(4) == 0 {
+ b.FailApp = true
+ }
+ if w.rng.Intn(10) == 0 {
+ b.FailArchive = true
+ }
+ if r != 0 && w.rng.Intn(2) == 0 {
+ b.FailSettle = true
+ }
+ b.forget()
+ w.boxes = append(w.boxes, b)
+ }
+ if w.rng.Intn(3) == 0 {
+ w.legacyStart()
+ }
+ return w
+}
+
+// legacyStart: a host that exists before the release. Its data is untagged,
+// a best-effort-placed descendant may be running, and an earlier
+// (pre-release) move left a replica in another region.
+func (w *world) legacyStart() {
+ r := w.rng.Intn(nRegions)
+ b := w.regionBox(r)
+ w.nextInc++
+ inc := w.nextInc
+ w.rec = &record{Inc: inc, App: app0, Region: r}
+ key := 7
+ var writes []int
+ for i := 0; i < 3; i++ {
+ w.nextW++
+ writes = append(writes, w.nextW)
+ w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: 0, Kind: "write"})
+ }
+ b.Row = &row{Inc: inc, App: app0, Status: "ready"}
+ b.DB = &localDB{Inc: inc, Key: key, Writes: writes}
+ b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true}
+ b.Config, b.Live, b.LiveInc = inc, app0, inc
+ w.buckets[r].objs["instances/"+host+"/ltx"] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes, SealKey: key}}}
+ other := (r + 1 + w.rng.Intn(nRegions-1)) % nRegions
+ w.buckets[other].objs["instances/"+host+"/ltx"] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes[:1], SealKey: key}}}
+ if w.rng.Intn(2) == 0 {
+ b.Procs = []*proc{{Main: true, Strict: false, Inc: inc, Box: b.ID}, {Main: false, Strict: false, Inc: inc, Box: b.ID}}
+ }
+}
+
+// ---------- the scheduler ----------
+
+func (w *world) step() {
+ w.now++
+ w.completeDue(false)
+ bs := w.liveBoxes()
+ b := bs[w.rng.Intn(len(bs))]
+ n := w.rng.Intn(100)
+ switch {
+ case !w.calm && n < 6:
+ switch w.rng.Intn(7) {
+ case 0, 1:
+ w.userCreate()
+ case 2:
+ w.userMove()
+ case 3:
+ w.userDelete()
+ case 4:
+ w.userPush()
+ case 5:
+ if w.rng.Intn(3) == 0 {
+ w.userPurge()
+ }
+ default:
+ w.doorAuthorize()
+ }
+ case !w.calm && n < 12:
+ w.fault()
+ case n < 20:
+ w.consoleStep()
+ case n < 24:
+ w.recoveryPass()
+ case n < 25:
+ w.doorOpen()
+ case n < 26:
+ if !w.calm {
+ w.doorAuthorize()
+ }
+ case n < 28:
+ if w.calm || w.rng.Intn(4) == 0 {
+ w.operator() // operators act during the incident too, not only after
+ }
+ case n < 58:
+ w.worker(b)
+ case n < 64:
+ w.reconcile(b)
+ case n < 72:
+ w.traffic(b)
+ w.wake(b)
+ case n < 77:
+ w.replicate(b)
+ case n < 78:
+ w.idleStop(b)
+ case n < 81:
+ w.passPlan(b, "config")
+ case n < 84:
+ w.passPlan(b, "adopt")
+ case n < 89:
+ w.passExec(b)
+ case n < 94:
+ w.runner(b)
+ default:
+ w.watchdog(b)
+ }
+ w.checkStep()
+}
+
+// heal ends the chaos. On the first call some faults linger, so the
+// operator meets a frozen, paused or partitioned participant, and destroyed
+// boxes stay down; on the final call everything heals, and each stopped box
+// either comes back (an instance stopped, then started) or is replaced.
+func (w *world) heal(final bool) {
+ w.calm = true
+ c := w.claim
+ for _, b := range w.boxes {
+ linger := !final && c != nil && (c.Op.Kind == "landing" || c.Op.Kind == "restoring") && b.ID == c.Op.Tgt && w.rng.Intn(2) == 0
+ if linger {
+ continue
+ }
+ b.Partitioned, b.Frozen, b.AgentPaused, b.AgentDown = false, false, false, false
+ }
+ if final {
+ for _, b := range w.boxes {
+ if b.Destroyed && w.regionBox(b.Region) == nil && w.rng.Intn(2) == 0 {
+ b.Destroyed = false // started again, with its old disk
+ b.forget()
+ w.logf("stopped box %d started again", b.ID)
+ }
+ }
+ w.replaceDestroyed()
+ }
+ // a box with no key gets one: ops distributes it (the approved fix)
+ for _, b := range w.boxes {
+ b.HasKey = true
+ b.FailArchive = false
+ }
+}
+
+func (w *world) quiescent() bool {
+ if len(w.pending) > 0 || len(w.console) > 0 {
+ return false
+ }
+ c := w.claim
+ if c == nil {
+ return w.rec == nil
+ }
+ if c.Holder == nil {
+ return c.Op.Kind == "" && w.rec == nil && len(c.Obl) == 0
+ }
+ if c.Op.Kind != "serving" || len(c.Obl) > 0 || w.rec == nil || w.rec.Inc != c.Holder.Inc || w.rec.MoveID != "" {
+ return false
+ }
+ e := w.execBox(c)
+ if e == nil || e.Row == nil || e.Row.Status != "ready" {
+ return false
+ }
+ if e.Config != c.Holder.Inc || e.Live != c.Holder.App || e.LiveInc != c.Holder.Inc {
+ return false // config sync and adoption still owe this incarnation
+ }
+ for _, b := range w.liveBoxes() {
+ if b != e && (b.Row != nil || len(b.Procs) > 0) {
+ return false
+ }
+ }
+ return true
+}
+
+// ---------- invariants ----------
+
+// checkStep runs after every step.
+func (w *world) checkStep() {
+ // one writer per host, across every region
+ var writers []int
+ for _, b := range w.boxes {
+ if !b.Destroyed && !b.Frozen && len(b.Procs) > 0 {
+ writers = append(writers, b.ID)
+ }
+ }
+ if len(writers) > 1 {
+ w.violate("INV-1: boxes %v run the host at once", writers)
+ }
+ // an app store exists while any instance of the app is held for serving
+ if c := w.claim; c != nil && c.Holder != nil && !w.stores[c.Holder.App] {
+ switch c.Op.Kind {
+ case "purging", "deleting", "parking":
+ default:
+ w.violate("purge: store of app %s destroyed while its host is %s", c.Holder.App, c.Op.Kind)
+ }
+ }
+ if c := w.claim; c != nil && c.Op.Kind == "restoring" && c.Op.SrcPhase == "stuck" {
+ w.violate("stuck: source could not recover %s", c.Op.ID)
+ }
+ if c := w.claim; c != nil && c.Op.Kind == "reverting" && c.Op.RevPhase == "stuck" {
+ w.violate("stuck: source could not revert %s", c.Op.ID)
+ }
+}
+
+func (w *world) boxesState() string {
+ s := ""
+ for _, b := range w.liveBoxes() {
+ s += fmt.Sprintf(" [box %d r%d row=%+v procs=%d db=%v files=%v cfg=%d live=%s/%d old=%v]", b.ID, b.Region, b.Row, len(b.Procs), b.DB != nil, b.Files != nil, b.Config, b.Live, b.LiveInc, b.Old)
+ }
+ return s
+}
+
+func (w *world) final() {
+ if !w.quiescent() {
+ w.violate("INV-3: no convergence after %d calm steps: %s%s", calmSteps, w.state(), w.boxesState())
+ return
+ }
+ 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 r := 0; r < nRegions; r++ {
+ if w.buckets[r].hasData("instances/"+host+"/", true) || w.buckets[r].hasData("moves/"+host+"/", true) {
+ w.violate("INV-10: region %d still holds data for a freed host", r)
+ }
+ }
+ 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)
+ }
+ }
+ return
+ }
+ e := w.execBox(c)
+ 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)
+ }
+ for r := 0; r < nRegions; r++ {
+ if r != e.Region && (w.buckets[r].hasData("instances/"+host+"/", true) || w.buckets[r].hasData("moves/"+host+"/", true)) {
+ w.violate("INV-10: region %d holds live-namespace data; the host serves from region %d", r, e.Region)
+ }
+ }
+ if w.buckets[e.Region].hasData("moves/"+host+"/", true) {
+ w.violate("INV-10: staging left in the serving region %d", e.Region)
+ }
+ for _, b := range w.liveBoxes() {
+ if b != e && (b.DB != nil || b.Files != nil) {
+ w.violate("INV-10: box %d holds local state; the host serves from box %d", b.ID, e.ID)
+ }
+ }
+ // make the serving box start, then check every acknowledged write
+ if !hasMain(e) {
+ if !w.admits(e, c, "") || !w.spawn(e, c, holderLin(c.Holder), false) {
+ w.violate("final: the serving box %d cannot start the host (%s) box: row=%+v db=%+v files=%+v cfg=%d live=%s/%d retired=%v fail=%v until=%d",
+ e.ID, w.state(), e.Row, e.DB, e.Files, e.Config, e.Live, e.LiveInc, e.Retired, e.FailApp, e.ExecUntil)
+ return
+ }
+ }
+ w.checkAcks(c, e, e.DB.Writes, "local")
+ // and the replica path: replicate now, cold-restore, check again
+ bl := &blob{Kind: "ltx", Inc: e.DB.Inc, Gen: e.DB.Gen, Writes: append([]int(nil), e.DB.Writes...), SealKey: e.DB.Key}
+ w.complete(&request{kind: rPut, region: e.Region, key: "instances/" + host + "/ltx", b: bl})
+ db := w.restore(e, c.Holder.Inc, c.Holder.Legacy, holderLin(c.Holder))
+ if db == nil {
+ w.violate("final: cold restore failed on box %d", e.ID)
+ return
+ }
+ w.checkAcks(c, e, db.Writes, "cold restore")
+}
+
+func (w *world) checkAcks(c *claim, e *box, writes []int, how string) {
+ have := map[int]bool{}
+ for _, x := range writes {
+ have[x] = true
+ }
+ timers := map[int]bool{}
+ for _, x := range e.Timers {
+ timers[x] = true
+ }
+ for _, a := range w.acks {
+ if a.Inc != c.Holder.Inc || a.Exempt {
+ continue
+ }
+ if a.Kind == "write" && !have[a.W] {
+ w.violate("INV-2 (%s): acknowledged write %d (box %d, t=%d) lost", how, a.W, a.Box, a.At)
+ return
+ }
+ if a.Kind == "timer" && how == "local" && !w.delivered[a.W] && !timers[a.W] {
+ w.violate("INV-2: acknowledged timer %d (box %d, t=%d) lost", a.W, a.Box, a.At)
+ return
+ }
+ }
+}
+
+func (w *world) state() string {
+ c := w.claim
+ if c == nil {
+ return fmt.Sprintf("claim absent, record %+v", w.rec)
+ }
+ return fmt.Sprintf("op=%s/%s phase=%s land=%s src=%s rev=%s exec=%d obl=%d holder=%+v rec=%+v pending=%d console=%d",
+ c.Op.Kind, c.Op.ID, c.Op.Phase, c.Op.LandPhase, c.Op.SrcPhase, c.Op.RevPhase, c.Op.Exec, len(c.Obl), c.Holder, w.rec, len(w.pending), len(w.console))
+}
+
+// ---------- running ----------
+
+func runSeed(seed int64, verbose bool) *world {
+ w := newWorld(seed, verbose)
+ for i := 0; i < chaosSteps; i++ {
+ w.step()
+ }
+ w.heal(false)
+ for i := 0; i < calmSteps && !w.quiescent(); i++ {
+ w.step()
+ if i == 400 || i%400 == 399 {
+ w.heal(true)
+ }
+ }
+ w.completeDue(true)
+ w.final()
+ return w
+}
+
+func seedsFromEnv(def int) int {
+ if s := os.Getenv("HOSTLIFE_SEEDS"); s != "" {
+ if n, err := strconv.Atoi(s); err == nil {
+ return n
+ }
+ }
+ return def
+}
+
+// TestHostLifecycle runs the joint model. HOSTLIFE_SEEDS sets the seed
+// count (the gate's default is short); HOSTLIFE_SEED=n runs one seed and
+// prints its trace.
+func TestHostLifecycle(t *testing.T) {
+ if s := os.Getenv("HOSTLIFE_SEED"); s != "" {
+ seed, _ := strconv.ParseInt(s, 10, 64)
+ w := runSeed(seed, true)
+ for _, line := range w.trace {
+ t.Log(line)
+ }
+ for _, v := range w.violations {
+ t.Errorf("seed %d: %s", seed, v)
+ }
+ return
+ }
+ n := seedsFromEnv(300)
+ failed := 0
+ kinds := map[string]int{}
+ firstSeed := map[string]int64{}
+ ops := 0
+ stats := map[string]int{}
+ for seed := int64(1); seed <= int64(n); seed++ {
+ w := runSeed(seed, false)
+ ops += w.opsDone
+ for k, v := range w.stats {
+ stats[k] += v
+ }
+ if len(w.violations) > 0 {
+ failed++
+ k := kind(w.violations[0])
+ kinds[k]++
+ if _, ok := firstSeed[k]; !ok {
+ firstSeed[k] = seed
+ t.Logf("seed %d: %s", seed, w.violations[0])
+ }
+ }
+ }
+ t.Logf("%d seeds, %d failed, %d completed operations; mutated=%q", n, failed, ops, mutated)
+ t.Logf("outcomes: %v", stats)
+ for k, c := range kinds {
+ t.Logf(" %4d × %s (first seed %d)", c, k, firstSeed[k])
+ }
+ if failed > 0 {
+ t.Fatalf("%d of %d seeds violated an invariant", failed, n)
+ }
+}
+
+func kind(v string) string {
+ if i := strings.Index(v, ": "); i >= 0 {
+ v = v[i+2:]
+ }
+ // strip ids and numbers so a family groups together
+ var b strings.Builder
+ skip := false
+ for _, r := range v {
+ if r >= '0' && r <= '9' {
+ if !skip {
+ b.WriteByte('#')
+ }
+ skip = true
+ continue
+ }
+ skip = false
+ b.WriteRune(r)
+ }
+ v = b.String()
+ if i := strings.Index(v, " holder="); i >= 0 {
+ v = v[:i]
+ }
+ if len(v) > 110 {
+ v = v[:110]
+ }
+ return v
+}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
new file mode 100644
index 000000000..a7add043f
--- /dev/null
+++ b/internal/sim/hostlife/world_test.go
@@ -0,0 +1,623 @@
+// Package hostlife is a deterministic, randomized model of the host
+// lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md,
+// rev 2) and Phase 1 of move-any-app
+// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 4).
+//
+// It is test-only. Nothing here is product code: every file is a _test.go
+// file, so `go build ./...` never sees it. It exists to find interleavings
+// that prose review rounds kept missing, and to prove each protocol rule is
+// load-bearing by mutation (see rules_test.go and README in the spec §14.2).
+//
+// The model is an abstraction. What it keeps, and what it drops, is listed
+// in the spec's §14.2; the short version:
+//
+// - one host, three regions, one box per region (plus replacement boxes);
+// - every bucket is versioned, with the real IAM split: a box has full
+// rights on its own data bucket, and only Put/Delete/CopyInto on another
+// region's moves/* (no Get, no ListVersions, no DeleteVersion);
+// - every S3 request may complete late, after the client gave up;
+// - boxes crash (agent restart: flat children die, memory lost), reboot,
+// freeze (whole-VM pause), pause (agent only), partition from the
+// control bucket, are destroyed, or boot-recover an old executable;
+// - the application writes and registers timers on its own, through
+// descendants that may outlive the main process.
+package hostlife
+
+import (
+ "fmt"
+ "math/rand"
+ "sort"
+ "strings"
+)
+
+const (
+ nRegions = 3
+ app0 = "A"
+ app1 = "B"
+
+ // Time is in model steps.
+ horizonH = 60 // a request may complete up to H steps after issue
+ execTTL = 40 // exec lease TTL
+ execRenew = 15 // renew when this close to expiry
+ lostMargin = 10 // declare-lost margin past expiry
+ cutBudget = 220 // absolute cut deadline after admission
+ stagingTTL = 30 // staging-work lease TTL
+ probeTries = 3
+ readyWait = 400 // abort a move whose readiness never comes
+)
+
+// ---------- storage ----------
+
+type blob struct {
+ Kind string // "ltx", "base", "files", "snap", "lock", "manifest", "lease", "report"
+ Inc int // incarnation tag; 0 = untagged legacy
+ Gen string // lineage that wrote it
+ Seq int
+ SealKey int // the instance.key the data is sealed with
+ Writes []int
+ Files *filesDir
+ Timers []int
+ Refs []ref
+ Text string
+}
+
+type ref struct {
+ Region int // -1 = control bucket
+ Key string
+ Ver int
+}
+
+type version struct {
+ ID int
+ B *blob
+ Marker bool
+}
+
+type bucket struct {
+ objs map[string][]*version
+}
+
+func newBucket() *bucket { return &bucket{objs: map[string][]*version{}} }
+
+func (b *bucket) keys(prefix string) []string {
+ var out []string
+ for k := range b.objs {
+ if strings.HasPrefix(k, prefix) {
+ out = append(out, k)
+ }
+ }
+ sort.Strings(out)
+ return out
+}
+
+func (b *bucket) current(key string) *version {
+ vs := b.objs[key]
+ if len(vs) == 0 {
+ return nil
+ }
+ v := vs[len(vs)-1]
+ if v.Marker {
+ return nil
+ }
+ return v
+}
+
+func (b *bucket) byID(key string, id int) *version {
+ for _, v := range b.objs[key] {
+ if v.ID == id {
+ return v
+ }
+ }
+ return nil
+}
+
+// dataVersions are every non-marker version under prefix.
+func (b *bucket) dataVersions(prefix string) []ref {
+ var out []ref
+ for _, k := range b.keys(prefix) {
+ for _, v := range b.objs[k] {
+ if !v.Marker {
+ out = append(out, ref{Key: k, Ver: v.ID})
+ }
+ }
+ }
+ return out
+}
+
+func (b *bucket) hasData(prefix string, skipLock bool) bool {
+ for _, k := range b.keys(prefix) {
+ if skipLock && strings.HasSuffix(k, "lock.json") {
+ continue
+ }
+ for _, v := range b.objs[k] {
+ if !v.Marker {
+ return true
+ }
+ }
+ }
+ return false
+}
+
+// ---------- requests (late completion) ----------
+
+type reqKind int
+
+const (
+ rPut reqKind = iota
+ rDelVer
+ rDelKey // bare-key delete: forbidden on host prefixes (mutation only)
+ rCopy // copy srcRegion/srcKey?versionId=srcVer -> region/key
+)
+
+type request struct {
+ kind reqKind
+ region int
+ key string
+ b *blob
+ ver int
+ srcRegion int
+ srcKey string
+ srcVer int
+ doneAt int
+ by string
+ // result, for an immediate completion
+ resultVer int
+}
+
+// ---------- local box state ----------
+
+type filesDir struct {
+ Inc int
+ Key int // the app's instance.key identity
+ Gen string // .files-gen marker
+ Env int // admin token identity in <host>.env
+ Done bool // markers written last
+}
+
+func (f *filesDir) clone() *filesDir {
+ if f == nil {
+ return nil
+ }
+ c := *f
+ return &c
+}
+
+type localDB struct {
+ Inc int
+ Gen string // <dbPath>.gen
+ Key int // the key it was sealed with
+ Writes []int
+ Seq int
+}
+
+func (d *localDB) clone() *localDB {
+ if d == nil {
+ return nil
+ }
+ c := *d
+ c.Writes = append([]int(nil), d.Writes...)
+ return &c
+}
+
+type proc struct {
+ Main bool
+ Strict bool // spawned into the host cgroup by strict placement
+ Inc int
+ Gen string
+ Box int
+}
+
+type row struct {
+ Inc int
+ App string
+ Status string // ready, moving, landing, restoring, releasing
+ HoldOp string
+ Repl string // carried column
+ Next int // carried column
+}
+
+type box struct {
+ ID int
+ Region int
+ Destroyed bool
+ Frozen bool // whole-VM pause: nothing on the box runs
+ AgentPaused bool // the agent alone is paused
+ AgentDown bool // the agent crashed and has not restarted
+ Partitioned bool // cannot reach the control bucket
+ Old bool // running a pre-floor executable
+ HasKey bool
+ Skew int
+ FailApp bool // the app fails its readiness check on this box
+ FailArchive bool // the final archive fails (too large) on this box
+ FailSettle bool // the app passes one readiness check, works, then fails
+ Nested bool // nested layout: children survive an agent crash
+
+ Row *row
+ DB *localDB
+ Files *filesDir
+ Config int // incarnation the config.env was rendered for; 0 none
+ Live string // app the live symlink points at
+ LiveInc int
+ Timers []int // active once-timers (registration ids)
+ History []int // delivered history (disposable)
+ Attempt int // runner bookkeeping
+ Procs []*proc
+ Retired map[int]bool // retired-incarnation markers (hostguard)
+ Parked int // count of locally parked artifacts
+
+ ExecUntil int // local exec-lease file (watchdog input); 0 none
+ // in-memory, lost on crash
+ snap *claim
+ stale *claim // a stalled worker's old read
+ plans []*plan
+ stopped map[string]bool
+ mem map[string]bool
+ evidAt map[string]int
+ pendingTimers []int
+}
+
+// plan is a background pass's decision, taken now and acted on later: the
+// shape of every stale-writer race (J-N8).
+type plan struct {
+ Kind string // "config", "adopt"
+ Inc int
+ App string
+}
+
+func (b *box) forget() {
+ b.snap, b.plans, b.stopped, b.stale = nil, nil, nil, nil
+ b.mem = map[string]bool{}
+ b.evidAt = map[string]int{}
+ b.pendingTimers = nil
+}
+
+// ---------- control plane ----------
+
+type holder struct {
+ Inc int
+ App string
+ Serial int // ground-truth creation event (model only)
+ Legacy bool
+ Lineage lineage
+ FilesGen string // the files generation compatible with the lineage
+}
+
+type lineage struct {
+ Op string // "" = origin
+ Region int
+ Ver int // version of instances/<host>/base in Region
+}
+
+type obligation struct {
+ ID string
+ Op string
+ Kind string // park-replica, park-local, park-superseded, park-staging
+ Region int
+ Box int
+ Prefix string
+ Ret string
+ Quiet int // not before
+ Exclude string // lineage to leave in place (a push parks only the old one)
+}
+
+type opState struct {
+ Kind string // serving, creating, deleting, parking, purging, moving, landing, reverting, restoring, pushing
+ ID string
+ Phase string
+ Exec int // -1 none
+ Parts []int
+
+ // intent
+ Src, Tgt int
+ SrcRegion, TgtRegion int
+ NewInc int
+ NewApp string
+ NewRegion int
+ NewSerial int
+
+ // journal
+ ReportAt int
+ ReportOK bool
+ CutAt int
+ CutDeadline int
+ StopAt int
+ StopDigest digest
+ StopFiles *filesDir
+ SealDB ref
+ SealFiles ref
+ SealQuiet int
+ LandPhase string
+ Installed digest
+ BaseVer int
+ ProbeTries int
+ ProbedAt int
+ RevPhase string
+ SrcPhase string
+ Dirty bool
+ DirtyKnown bool
+ ReturnDB ref
+ ReturnFiles ref
+ ReturnQuiet int
+ LostBox int
+ LostAt int
+ RollbackID string
+ PushWrites []int
+ Committed bool
+ Opened bool
+ ParkLocalNow bool
+ Auto bool
+ ReqAt int
+ Repl string
+ Next int
+ FlipAt int
+ TgtStopAt int
+ Reason string
+ App string
+}
+
+type digest struct {
+ Writes string
+ Files string
+ Timers string
+ Valid bool
+}
+
+type claim struct {
+ Ver int
+ Holder *holder
+ Op opState
+ Regions []int
+ Boxes []int
+ Complete bool
+ Obl []obligation
+ Lost []int
+ Retired []int
+ Quiet [nRegions]int
+ PurgeRes bool
+}
+
+type record struct {
+ Ver int
+ Inc int
+ App string
+ Region int
+ MoveID string
+}
+
+// ---------- the world ----------
+
+type ack struct {
+ W int
+ Inc int
+ Box int
+ At int
+ Kind string // "write" or "timer"
+ Exempt bool // lost under a declared loss (M16)
+}
+
+type world struct {
+ t testingT
+ seed int64
+ rng *rand.Rand
+ now int
+ ver int
+ verbose bool
+
+ claim *claim // nil = absent
+ rec *record
+ stores map[string]bool
+ purgeRes map[string]bool
+ purgeStep map[string]int // the reservation's durable phase (purge journal)
+ floor bool
+ buckets [nRegions]*bucket
+ control *bucket
+ boxes []*box
+ pending []*request
+ acks []ack
+ nextW int
+ nextInc int
+ serial int
+ nextID int
+ delivered map[int]bool
+ doorReads []*doorPlan
+ execLease map[int]execLease
+ staging [nRegions]stagingLease
+ console []*consolePlan
+ fail map[string]bool // which faults this seed exercises
+ stats map[string]int
+
+ violations []string
+ opsDone int
+ calm bool
+ trace []string
+}
+
+type testingT interface {
+ Fatalf(format string, args ...any)
+ Logf(format string, args ...any)
+}
+
+func (w *world) logf(format string, args ...any) {
+ if w.verbose {
+ w.trace = append(w.trace, fmt.Sprintf("%5d ", w.now)+fmt.Sprintf(format, args...))
+ }
+}
+
+func (w *world) violate(format string, args ...any) {
+ msg := fmt.Sprintf("t=%d: ", w.now) + fmt.Sprintf(format, args...)
+ if len(w.violations) >= 3 {
+ return
+ }
+ w.violations = append(w.violations, msg)
+ w.logf("VIOLATION %s", msg)
+}
+
+func (w *world) newID(prefix string) string {
+ w.nextID++
+ return fmt.Sprintf("%s%d", prefix, w.nextID)
+}
+
+func (w *world) newVer() int {
+ w.ver++
+ return w.ver
+}
+
+func (w *world) boxByID(id int) *box {
+ for _, b := range w.boxes {
+ if b.ID == id {
+ return b
+ }
+ }
+ return nil
+}
+
+// regionBox is the live (not destroyed) box in a region.
+func (w *world) regionBox(r int) *box {
+ for _, b := range w.boxes {
+ if b.Region == r && !b.Destroyed {
+ return b
+ }
+ }
+ return nil
+}
+
+func contains(xs []int, x int) bool {
+ for _, y := range xs {
+ if y == x {
+ return true
+ }
+ }
+ return false
+}
+
+func addUniq(xs []int, x int) []int {
+ if contains(xs, x) {
+ return xs
+ }
+ return append(xs, x)
+}
+
+func intsKey(xs []int) string {
+ c := append([]int(nil), xs...)
+ sort.Ints(c)
+ return fmt.Sprint(c)
+}
+
+func (c *claim) clone() *claim {
+ if c == nil {
+ return nil
+ }
+ n := *c
+ if c.Holder != nil {
+ h := *c.Holder
+ n.Holder = &h
+ }
+ n.Op.Parts = append([]int(nil), c.Op.Parts...)
+ n.Op.PushWrites = append([]int(nil), c.Op.PushWrites...)
+ n.Op.StopFiles = c.Op.StopFiles.clone()
+ n.Regions = append([]int(nil), c.Regions...)
+ n.Boxes = append([]int(nil), c.Boxes...)
+ n.Obl = append([]obligation(nil), c.Obl...)
+ n.Lost = append([]int(nil), c.Lost...)
+ n.Retired = append([]int(nil), c.Retired...)
+ return &n
+}
+
+// ---------- bucket access with IAM ----------
+
+// actor names: "box:N" or "console" or "operator".
+
+func (w *world) iamCheck(actorBox int, r *request) bool {
+ if actorBox < 0 { // console: control bucket only, plus GetObjectVersion on data (door)
+ return false
+ }
+ b := w.boxByID(actorBox)
+ if r.region == b.Region {
+ if r.kind == rCopy && r.srcRegion != b.Region {
+ return false // no Get on a sibling
+ }
+ return true
+ }
+ // sibling bucket: Put/Delete on moves/* only, and CopyObject INTO moves/*
+ // from the box's own bucket.
+ if !strings.HasPrefix(r.key, "moves/") {
+ return false
+ }
+ switch r.kind {
+ case rPut, rDelKey:
+ return true
+ case rCopy:
+ return r.srcRegion == b.Region
+ }
+ return false // DeleteObjectVersion is not granted on a sibling
+}
+
+// issue sends a request. It returns the new version id when it completed
+// immediately and the client saw the answer; 0 when the client timed out
+// (the request may still complete later).
+func (w *world) issue(actorBox int, r *request) int {
+ if !w.iamCheck(actorBox, r) {
+ w.violate("IAM: box %d may not %v %s in region %d", actorBox, r.kind, r.key, r.region)
+ return 0
+ }
+ if w.rng.Intn(10) < 7 {
+ return w.complete(r)
+ }
+ r.doneAt = w.now + 1 + w.rng.Intn(6)
+ tail := 8
+ if strings.HasPrefix(r.key, "moves/") {
+ tail = 3 // staging rounds stall more often: the cross-region path is the slow one
+ }
+ if w.rng.Intn(tail) == 0 {
+ r.doneAt = w.now + 1 + w.rng.Intn(horizonH) // the long tail: signed, cancelled, completed late
+ }
+ r.by = fmt.Sprintf("box:%d", actorBox)
+ w.pending = append(w.pending, r)
+ w.logf("box %d issued %v %s r%d (late until %d)", actorBox, r.kind, r.key, r.region, r.doneAt)
+ return 0
+}
+
+func (w *world) complete(r *request) int {
+ bk := w.buckets[r.region]
+ switch r.kind {
+ case rPut:
+ v := &version{ID: w.newVer(), B: r.b}
+ bk.objs[r.key] = append(bk.objs[r.key], v)
+ return v.ID
+ case rDelVer:
+ vs := bk.objs[r.key]
+ for i, v := range vs {
+ if v.ID == r.ver {
+ bk.objs[r.key] = append(vs[:i:i], vs[i+1:]...)
+ break
+ }
+ }
+ return -1
+ case rDelKey:
+ v := &version{ID: w.newVer(), Marker: true}
+ bk.objs[r.key] = append(bk.objs[r.key], v)
+ return v.ID
+ case rCopy:
+ src := w.buckets[r.srcRegion].byID(r.srcKey, r.srcVer)
+ if src == nil || src.Marker {
+ return 0
+ }
+ v := &version{ID: w.newVer(), B: src.B}
+ bk.objs[r.key] = append(bk.objs[r.key], v)
+ return v.ID
+ }
+ return 0
+}
+
+func (w *world) completeDue(force bool) {
+ var keep []*request
+ for _, r := range w.pending {
+ if force || r.doneAt <= w.now {
+ w.complete(r)
+ w.logf("late completion %v %s r%d (%s)", r.kind, r.key, r.region, r.by)
+ } else {
+ keep = append(keep, r)
+ }
+ }
+ w.pending = keep
+}