carlos / platform Public

sim: witnesses and direct tests for the completion protocol, the catch-up hold and the C1/C11 fallbacks, and the residual and purge-deadlock scenarios

Ten witnesses: probe stop before serving (INV-31), another owner's fence
at the stop and at the lift after a restart (INV-32), a failed discharge
with a crash after the release (INV-31), mark last after a failed
discharge (INV-31), a failed mark and a crash after the lift retried from
the claim (INV-3), a drain, move and push held by the barrier (INV-31),
completion with region HA off after a restart (INV-3), the N6 handover
(INV-3), and the delayed source's catch-up hold (INV-33).

Direct tests: the C1 and C11 fallbacks (each fails under its mutation),
the refused probe stop changes nothing, the barrier's fenced-source
exemption, the delayed-source schedule with its assertions, the residual
ruling 85 leaves open (a successor relocation or move replaces the
serving op before the delayed source reconciles: its row stays ready
until its park-local), and the purge/failover deadlock behind the
operator's declare-lost.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude agent, operated by paul@keymail.dev 363055fee817ab0372b990dd6b3a5e6ed3c73698 parent 52ab850
2 files changed, +498 −0
  • internal/sim/hostlife/regionha_completion_witness_test.go +477 −0
  • internal/sim/hostlife/witness_test.go +21 −0
diff --git a/internal/sim/hostlife/regionha_completion_witness_test.go b/internal/sim/hostlife/regionha_completion_witness_test.go
new file mode 100644
index 000000000..1a5f25f8f
--- /dev/null
+++ b/internal/sim/hostlife/regionha_completion_witness_test.go
@@ -0,0 +1,477 @@
+package hostlife
+
+import "testing"
+
+// ---------- L18 joint round findings 2 to 4: witnesses and direct tests ----------
+
+// completedDrain drains the host from box 0 to box 3 with fault set on
+// the target first, and drives until the claim serves on box 3 with its
+// completion recorded (regionha_completion_test.go).
+func (w *world) completedDrain(t *testing.T, fault func(to *box)) (from, to *box, ok bool) {
+ w.twoBox()
+ from, to = w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ if fault != nil {
+ fault(to)
+ }
+ w.drainTo(t, to)
+ w.extraBox(0, 30) // a target for a successor drain from box 3 (box 0 owes its park-local)
+ ok = w.reach(t, 1500, "serving on box 3 with its completion recorded", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec == to.ID && c.Op.Completed != nil
+ }, w.act(from, to), w.recoveryPass)
+ return from, to, ok
+}
+
+// marked: the serving op's completion is marked discharged.
+func (w *world) marked() bool {
+ d := w.claim.Op.Completed
+ return w.claim.Op.Kind == "serving" && d != nil && d.Discharged
+}
+
+// wProbeStopBeforeServing (reloc-probe-stop): a drain completes; the
+// probe's session is stopped with root's receipt before the serving CAS,
+// and the host wakes on box 3 afterwards. Completed over the running
+// probe, its session outlives the kind change on a box whose
+// participation is not discharged (INV-31).
+func wProbeStopBeforeServing(t *testing.T, w *world) {
+ from, to, ok := w.completedDrain(t, nil)
+ if !ok {
+ return
+ }
+ _ = from
+ w.reach(t, 200, "the host runs on box 3 after the completion", func() bool { return hasMain(to) && w.marked() }, w.actAll(), w.recoveryPass, func() { w.wake(to) })
+ w.finish(t)
+}
+
+// wProbeStopMeetsAnotherFence (reloc-probe-fence-owner, the stop): the
+// probe has passed when another operation's fence closes the host on box
+// 3. The probe stop refuses with nothing stopped, and ruling 67 makes the
+// relocation stuck for an operator. Installed over that fence, the stop
+// later lifts it as its own, and the serving wake starts the host under a
+// fence its owner never lifted (INV-32).
+func wProbeStopMeetsAnotherFence(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ if !w.reach(t, 1500, "the probe passed", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && c.Op.Phase == "probed" && c.Op.ProbeStop == nil
+ }, w.act(from, to), w.recoveryPass) {
+ return
+ }
+ to.actFence, to.foreignFence = "op-elsewhere", "op-elsewhere"
+ w.reach(t, 3*releaseDeadline, "stuck with the probe unstopped", func() bool { return w.claim.Op.Stuck != "" }, w.act(from, to), w.recoveryPass, func() { w.wake(to) })
+}
+
+// wLiftAfterRestartMeetsAnotherFence (reloc-probe-fence-owner, the lift,
+// a crash): the completion's discharge fails for a while; the target's
+// agent restarts, which empties the activator's fences, and another
+// operation fences the host. The completion pass then discharges,
+// releases the hold and lifts only its own fence: the other one stays
+// and the serving wake waits. Lifting any fence opens the host under it
+// (INV-32).
+func wLiftAfterRestartMeetsAnotherFence(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ return
+ }
+ w.crash(to)
+ to.actFence, to.foreignFence = "op-elsewhere", "op-elsewhere"
+ to.dischargeFails = false
+ w.reach(t, 100, "the completion marked", w.marked, w.act(to), func() { w.wake(to) })
+ w.drive(20, never, w.act(to), func() { w.wake(to) })
+}
+
+// wDischargeFailsHoldsTheRow (reloc-completion-discharge-first, refusal
+// and crash): C10's discharge fails for thirty steps; the row stays held
+// and the fence installed, so no serving wake moves the holder off the
+// stopped probe session. Then the discharge succeeds, the agent crashes
+// after the hold's release, and the next pass resumes from the claim:
+// discharged again on positive evidence, marked, and the host serves.
+// With the hold released and the fence lifted first, a request admits a
+// writer before the discharge (INV-31).
+func wDischargeFailsHoldsTheRow(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ return
+ }
+ w.drive(30, never, w.act(to), w.recoveryPass, func() { w.wake(to) })
+ to.dischargeFails, to.crashAfter = false, "release"
+ w.reach(t, 200, "the completion marked after a crash", w.marked, w.act(to), w.recoveryPass, func() { w.wake(to) })
+ w.finish(t)
+}
+
+// wMarkLastAfterAFailedDischarge (reloc-completion-mark-last): the
+// discharge fails, and a drain from box 3 is asked for meanwhile; with
+// the mark last the record stays unmarked and the barrier refuses it
+// until the discharge succeeds. Marked first, the barrier lets the drain
+// name box 3 while its participation is still the completed op's
+// (INV-31), and the discharge is never retried.
+func wMarkLastAfterAFailedDischarge(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ return
+ }
+ w.drive(10, never, w.act(to), w.recoveryPass)
+ w.userRelocate()
+ w.drive(5, never, w.act(to), w.recoveryPass)
+ to.dischargeFails = false
+ if !w.reach(t, 200, "the completion marked", w.marked, w.act(to), w.recoveryPass, func() { w.wake(to) }) {
+ return
+ }
+ w.running(t, to)
+ w.userRelocate()
+ w.servingOn(t, nil)
+ w.finish(t)
+}
+
+// wFailedMarkRetriedFromTheClaim (reloc-completion-from-claim, a failed
+// mark and a crash): the mark fails once after the hold's release and
+// the lift; the next pass finds the unmarked completion from the claim
+// record and marks it. A second drain completes with a crash after the
+// lift, and is marked on the next pass too. Found from the row's hold,
+// which the release removed, the completion is never marked, and nothing
+// starts from the host again (INV-3).
+func wFailedMarkRetriedFromTheClaim(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.markFails = true })
+ if !ok {
+ return
+ }
+ if !w.reach(t, 200, "the completion marked after a failed mark", w.marked, w.act(to), w.recoveryPass, func() { w.wake(to) }) {
+ return
+ }
+ w.running(t, to)
+ w.userRelocate()
+ back := w.boxByID(w.claim.Op.Tgt)
+ if back == nil || w.claim.Op.Kind != "relocating" {
+ return
+ }
+ back.crashAfter = "lift"
+ w.servingOn(t, back)
+ w.reach(t, 200, "the second completion marked after a crash", w.marked, w.actAll(), w.recoveryPass, w.wakeExec)
+ w.finish(t)
+}
+
+// wSuccessorWaitsForTheDischarge (reloc-completion-barrier): while the
+// completion's discharge fails, a drain, a move and a push from box 3
+// are all refused; once it is discharged and marked the drain starts and
+// completes. Without the barrier the drain names box 3 while its
+// participation is still the completed op's (INV-31).
+func wSuccessorWaitsForTheDischarge(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ return
+ }
+ w.userRelocate()
+ w.moveTo(1)
+ w.userPush()
+ w.drive(5, never, w.act(to), w.recoveryPass)
+ if w.claim.Op.Kind != "serving" {
+ return // the mutation started one; INV-31 was recorded at the step
+ }
+ to.dischargeFails = false
+ if !w.reach(t, 200, "the completion marked", w.marked, w.act(to), w.recoveryPass, func() { w.wake(to) }) {
+ return
+ }
+ w.running(t, to)
+ w.userRelocate()
+ w.servingOn(t, nil)
+ w.finish(t)
+}
+
+// wCompletionWithRegionHAOff (reloc-completion-claim-mode, ruling 82,
+// a restart): the discharge fails, then region HA is turned off and the
+// target's agent restarts; the completion-only pass still discharges,
+// releases, lifts and marks, and the host serves on box 3. Run only with
+// region HA on, the completion is never finished (INV-3).
+func wCompletionWithRegionHAOff(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ return
+ }
+ w.haOff = true
+ w.crash(to)
+ to.dischargeFails = false
+ w.reach(t, 200, "the completion finished with region HA off", func() bool { return w.marked() && hasMain(to) }, w.act(to), w.recoveryPass, func() { w.wake(to) })
+ w.finish(t)
+}
+
+// wServingWakeHandsOver (reloc-completed-handover, N6): after the
+// completion the first serving wake on box 3 hands over from the probe's
+// receipt and the host runs. Routed to main's stop, its serving-shaped
+// fence replaces the probe's and the handover refuses for good (INV-3).
+func wServingWakeHandsOver(t *testing.T, w *world) {
+ _, to, ok := w.completedDrain(t, nil)
+ if !ok {
+ return
+ }
+ w.reach(t, 200, "the host runs on box 3", func() bool { return hasMain(to) }, w.actAll(), w.recoveryPass, func() { w.wake(to) })
+ w.finish(t)
+}
+
+// wDelayedSourceHoldsItsRow (reloc-completed-catchup-hold, finding 3):
+// the source releases and its admission fence closes, then its
+// reconcile is delayed until the target has completed. Its first
+// reconcile after that holds the row for the completed op, never
+// leaving it ready, until its park-local retires it. Without the
+// catch-up hold the row its release left ready stays ready (INV-33).
+func wDelayedSourceHoldsItsRow(t *testing.T, w *world) {
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ if !w.reach(t, 1500, "the source released", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && c.Op.Release != nil && c.Op.Release.Box == from.ID
+ }, func() { w.worker(from) }, w.act(to), w.recoveryPass) {
+ return
+ }
+ if !w.reach(t, 1500, "serving on box 3, the source not reconciled", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec == to.ID
+ }, func() { w.worker(from) }, w.act(to), w.recoveryPass) {
+ return
+ }
+ w.reconcile(from)
+ w.finish(t)
+}
+
+// TestDelayedSourceHoldsItsRow is the witness's schedule with its
+// assertions: the source's row is still ready when the target completes
+// (the release no longer holds it, ruling 28), held for the completed op
+// after the source's next reconcile, and gone once its park-local ran.
+func TestDelayedSourceHoldsItsRow(t *testing.T) {
+ w := newWitness()
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.reach(t, 1500, "the source released", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && c.Op.Release != nil && c.Op.Release.Box == from.ID
+ }, func() { w.worker(from) }, w.act(to), w.recoveryPass)
+ w.reach(t, 1500, "serving on box 3", func() bool { return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == to.ID }, func() { w.worker(from) }, w.act(to), w.recoveryPass)
+ w.mustHold(t)
+ if from.Row == nil || from.Row.Status != "ready" {
+ t.Fatalf("the delayed source's row is not the ready row its release left: %+v", from.Row)
+ }
+ op := w.claim.Op.Completed.Op
+ w.reconcile(from)
+ w.mustHold(t)
+ if from.Row == nil || from.Row.Status != "relocating" || from.Row.HoldOp != op {
+ t.Fatalf("the catch-up hold did not hold the source's row for %s: %+v", op, from.Row)
+ }
+ w.finish(t)
+ w.mustHold(t)
+ if from.Row != nil {
+ t.Fatalf("the source's row outlived its park-local: %+v", from.Row)
+ }
+}
+
+// TestCatchUpHoldResidualAfterASuccessor is the residual scenario ruling
+// 85 names and leaves open, modelled as the built code has it and not
+// hidden: the source's reconcile is delayed, the target completes and is
+// discharged and marked, a successor (a drain from the target, or a move
+// to region 1) replaces the serving op, which needs only the target's
+// discharge, and only then does the source reconcile. The successor took
+// the completion record with it, so the catch-up hold no longer applies,
+// and the source's row stays ready from then until its park-local
+// retires it. No invariant fails: the gap is availability, not a second
+// writer (the source's wake is refused by the exec check), so this is a
+// scenario test that asserts the gap is there, not a mutation witness.
+func TestCatchUpHoldResidualAfterASuccessor(t *testing.T) {
+ for _, successor := range []string{"relocation", "move"} {
+ t.Run(successor, func(t *testing.T) {
+ w := newWitness()
+ w.twoBox()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.reach(t, 1500, "the source released", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && c.Op.Release != nil && c.Op.Release.Box == from.ID
+ }, func() { w.worker(from) }, w.act(to), w.recoveryPass)
+ w.reach(t, 1500, "the completion marked, the source not reconciled", w.marked, func() { w.worker(from) }, w.act(to), w.recoveryPass, func() { w.wake(to) })
+ w.running(t, to)
+ // the region's chores the completion queued run on box 3; only
+ // box 0's park-local stays owed (box 0's agent is the slow one)
+ w.reach(t, 600, "only the source's park-local owed", func() bool {
+ for _, o := range w.claim.Obl {
+ if !(o.Kind == "park-local" && o.Box == from.ID) {
+ return false
+ }
+ }
+ return true
+ }, w.act(to), w.recoveryPass, func() { w.wake(to) })
+ w.mustHold(t)
+ if from.Row == nil || from.Row.Status != "ready" {
+ t.Fatalf("the delayed source's row is not the ready row its release left: %+v", from.Row)
+ }
+ want := "relocating"
+ if successor == "relocation" {
+ w.extraBox(0, 30)
+ w.userRelocate()
+ } else {
+ w.moveTo(1)
+ want = "moving"
+ }
+ if w.claim.Op.Kind != want {
+ t.Fatalf("the successor %s did not start: %s", successor, w.state())
+ }
+ w.reconcile(from)
+ w.wake(from)
+ w.mustHold(t)
+ if from.Row == nil || from.Row.Status != "ready" || hasMain(from) {
+ t.Fatalf("the residual is not as ruling 85 describes it (row %+v, running %v)", from.Row, hasMain(from))
+ }
+ t.Logf("residual: box %d's row is ready under %s %s, with its park-local still owed", from.ID, w.claim.Op.Kind, w.claim.Op.ID)
+ w.finish(t)
+ w.mustHold(t)
+ if from.Row != nil {
+ t.Fatalf("the source's row outlived its park-local: %+v", from.Row)
+ }
+ })
+ }
+}
+
+// TestFailedTargetCannotReleaseWithoutC1 (reloc-c1-failed-release-refused,
+// finding 4): with claim ask C1 open, a drain's target that fails its
+// probe cannot release in probe-failed: nothing is journaled, the
+// operation is stuck at the release deadline, and the operator's resolve
+// stops the target and replays, so the host serves again. The mutation
+// releases as if C1 had landed, and this test fails.
+func TestFailedTargetCannotReleaseWithoutC1(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ to.FailApp = true
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.extraBox(0, 30)
+ w.reach(t, 1500, "probe-failed", func() bool { return w.claim.Op.Phase == "probe-failed" }, w.act(from, to), w.recoveryPass)
+ w.reach(t, 3*releaseDeadline, "stuck in probe-failed", func() bool { return w.claim.Op.Stuck != "" }, w.act(from, to), w.recoveryPass)
+ w.mustHold(t)
+ if c := w.claim; c.Op.Phase != "probe-failed" || c.Op.Release != nil || c.Op.Exec != to.ID || w.stats["release journaled: failed target"] != 0 {
+ t.Fatalf("the failed target released without claim ask C1: %s", w.state())
+ }
+ if w.stats["release refused: no failed-target obligation (C1 open)"] == 0 {
+ t.Fatalf("the release was never refused: %v", w.stats)
+ }
+ w.servingOn(t, nil)
+ if w.stats["operator stopped a target that cannot release"] == 0 {
+ t.Fatalf("the operator did not stop the target: %v", w.stats)
+ }
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestLaterAttemptRefusedWithoutC11 (reloc-c11-later-attempt-refused,
+// finding 4): with claim ask C11 open, the target's first attempt opens P
+// and its agent crashes before the probe passes; the next attempt is
+// refused before it is counted, and the operation is probe-failed with
+// the count unchanged and no second admission. The mutation counts and
+// makes it, and this test fails.
+func TestLaterAttemptRefusedWithoutC11(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ if !w.probeOpened(t, from, to) {
+ w.mustHold(t)
+ }
+ attempts, gen := w.claim.Op.Attempts, w.claim.Holder.Gen
+ w.crash(to)
+ w.reach(t, 200, "probe-failed or a second attempt", func() bool {
+ c := w.claim
+ return c.Op.Phase == "probe-failed" || c.Op.Attempts != attempts || c.Holder.Gen != gen
+ }, w.act(from, to), w.recoveryPass)
+ w.mustHold(t)
+ if c := w.claim; c.Op.Phase != "probe-failed" || c.Op.Attempts != attempts || c.Holder.Gen != gen {
+ t.Fatalf("a later attempt was counted or made without claim ask C11 (attempts %d -> %d): %s", attempts, c.Op.Attempts, w.state())
+ }
+ if w.stats["probe-failed: a later attempt root cannot launch (C11 open)"] != 1 {
+ t.Fatalf("the refusal was not recorded once: %v", w.stats)
+ }
+ w.servingOn(t, nil)
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestCompletionBarrierExemptions (reloc-completion-barrier, ruling 77's
+// exemptions): while box 3's completion is unmarked, a drain is refused;
+// box 3 is then terminated, and the failover that cites its fence starts
+// over the unmarked record and serves elsewhere.
+func TestCompletionBarrierExemptions(t *testing.T) {
+ w := newWitness()
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ w.mustHold(t)
+ }
+ w.userRelocate()
+ if w.claim.Op.Kind != "serving" || w.stats["start refused: a completed relocation is not discharged"] == 0 {
+ t.Fatalf("the drain was not refused by the barrier: %s", w.state())
+ }
+ w.terminate(to)
+ w.reach(t, 200, "the failover started over the unmarked record", func() bool { return w.claim.Op.Kind == "relocating" }, w.actAll(), w.recoveryPass)
+ w.servingOn(t, nil)
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestProbeStopRefusesAnotherFence (reloc-probe-fence-owner, the
+// refusal's detail): the refused probe stop stops nothing, journals no
+// stop and leaves the other owner's fence in place.
+func TestProbeStopRefusesAnotherFence(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.drainTo(t, to)
+ w.reach(t, 1500, "the probe passed", func() bool { c := w.claim; return c.Op.Phase == "probed" && c.Op.ProbeStop == nil && hasMain(to) }, w.act(from, to), w.recoveryPass)
+ to.actFence = "op-elsewhere"
+ w.drive(20, never, w.act(from, to))
+ w.mustHold(t)
+ if c := w.claim; c.Op.ProbeStop != nil || !hasMain(to) || to.actFence != "op-elsewhere" || to.StopEvidence[probeKey(c.Op.ID)] {
+ t.Fatalf("the refused probe stop changed something (stop %+v, running %v, fence %q): %s", c.Op.ProbeStop, hasMain(to), to.actFence, w.state())
+ }
+}
+
+// TestTerminatedCompletionBoxBlocksAPurge records a gap in the built code
+// (seed 2224 / 3,000, two boxes): the completion box is terminated
+// before its discharge while a purge has closed the app's admission. The
+// purge's StartGuard is refused by the completion barrier (the box is not
+// on lost), and the failover that would cite the box's fence is refused
+// by the closed admission, so without an operator nothing moves. The
+// operator's declare-lost (declareDeadCompletionBox) puts the box on
+// lost, the barrier's exemption, and the purge proceeds.
+func TestTerminatedCompletionBoxBlocksAPurge(t *testing.T) {
+ w := newWitness()
+ _, to, ok := w.completedDrain(t, func(to *box) { to.dischargeFails = true })
+ if !ok {
+ w.mustHold(t)
+ }
+ w.userPurge()
+ w.reach(t, 100, "the purge closed the app's admission", func() bool { return w.admit[app0].Closed }, w.runConsole)
+ w.terminate(to)
+ w.drive(400, never, w.actAll(), w.runConsole, w.recoveryPass)
+ w.mustHold(t)
+ if c := w.claim; c == nil || c.Op.Kind != "serving" || contains(c.Lost, to.ID) {
+ t.Fatalf("something moved without the operator: %s", w.state())
+ }
+ if w.stats["start refused: a completed relocation is not discharged"] == 0 || w.stats["failover start: app admission closed"] == 0 {
+ t.Fatalf("not the deadlock: barrier %d, failover %d", w.stats["start refused: a completed relocation is not discharged"], w.stats["failover start: app admission closed"])
+ }
+ w.reach(t, 2000, "the purge freed the host after the operator's declare-lost", func() bool { c := w.claim; return c == nil || c.Holder == nil }, w.actAll(), w.runConsole, w.recoveryPass, w.operator)
+ w.mustHold(t)
+ if w.stats["operator declared a terminated completion box lost (purge and failover both refused)"] != 1 {
+ t.Fatalf("the operator's declare-lost did not run once: %v", w.stats)
+ }
+}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 597e6a357..303d359ab 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -268,6 +268,27 @@ var witnesses = []witness{
"joint round 1 review I1: a park-generation the source's restart queues during a move runs in the move's stopped phase, op.exec none; region 0 is still authoritative (moves §5.1), so the live manifest survives and the failover the source's termination converts the move into pins it and serves; with the files home read from op.exec alone it is archived and the failover is stuck for ever (INV-3)", wMoveStoppedKeepsLiveFiles},
{"files-home-move-phases", "files-home-move-phases", "INV-30",
"Astra joint round 2: the same park waits until the target's probe is admitted, runs before the commit, and the landing rolls back cleanly; the source region stays the files home until the commit, so the source's failover after the return pins the keyed manifest and serves; home only until the probe's admission, or never, it is archived and the failover is stuck for ever (INV-3)", wRollbackKeepsSourceFiles},
+ // L18 joint round findings 2 and 3 (regionha_completion_witness_test.go)
+ {"reloc-probe-stop", "reloc-probe-stop", "INV-31",
+ "a drain completes: the probe's session is stopped with root's receipt before the serving CAS, and the host wakes on the target afterwards; completed over the running probe, its session outlives the kind change on a box whose participation is not discharged", wProbeStopBeforeServing},
+ {"reloc-probe-fence-owner", "reloc-probe-fence-owner", "INV-32",
+ "another operation fences the host on the target after its probe passed: the probe stop refuses with nothing stopped and ruling 67 makes the relocation stuck; installed over that fence, the stop later lifts it as its own and the serving wake starts the host under it", wProbeStopMeetsAnotherFence},
+ {"reloc-probe-fence-owner", "reloc-probe-fence-owner", "INV-32",
+ "a crash: the target's agent restarts while the discharge fails, emptying the activator's fences, and another operation fences the host; the completion lifts only its own fence and the serving wake waits; lifting any fence opens the host under the other", wLiftAfterRestartMeetsAnotherFence},
+ {"reloc-completion-discharge-first", "reloc-completion-discharge-first", "INV-31",
+ "C10's discharge fails for thirty steps: the hold and the fence stay and no wake moves the holder; then it succeeds, the agent crashes after the hold's release, and the next pass resumes and marks; with the hold released and the fence lifted first, a request admits a writer before the discharge", wDischargeFailsHoldsTheRow},
+ {"reloc-completion-mark-last", "reloc-completion-mark-last", "INV-31",
+ "the discharge fails and a drain from the completion box is asked for: with the mark last the barrier refuses it until the discharge succeeds; marked first, the drain names the box while its participation is still the completed op's, and the discharge is never retried", wMarkLastAfterAFailedDischarge},
+ {"reloc-completion-from-claim", "reloc-completion-from-claim", "INV-3",
+ "the mark fails once after the hold's release and the lift, and a second completion crashes after the lift: each next pass finds the unmarked completion from the claim and marks it; found from the row's hold, which the release removed, it is never marked and nothing starts from the host again", wFailedMarkRetriedFromTheClaim},
+ {"reloc-completion-barrier", "reloc-completion-barrier", "INV-31",
+ "while the completion's discharge fails a drain, a move and a push from the completion box are refused; once marked the drain starts and completes; without the barrier the drain names the box while its participation is still the completed op's", wSuccessorWaitsForTheDischarge},
+ {"reloc-completion-claim-mode", "reloc-completion-claim-mode", "INV-3",
+ "ruling 82: the discharge fails, region HA is turned off and the target's agent restarts; the completion-only pass still discharges, releases, lifts and marks, and the host serves; run with region HA on only, the completion never finishes", wCompletionWithRegionHAOff},
+ {"reloc-completed-handover", "reloc-completed-handover", "INV-3",
+ "N6: the first serving wake after the completion hands over from the probe's receipt and the host runs; routed to main's stop, its serving-shaped fence replaces the probe's and the handover refuses for good", wServingWakeHandsOver},
+ {"reloc-completed-catchup-hold", "reloc-completed-catchup-hold", "INV-33",
+ "finding 3, ruling 85: the source releases, its reconcile is delayed until the target completed, and its next reconcile holds its row for the completed op until its park-local retires it; without the catch-up hold the row its release left ready stays ready", wDelayedSourceHoldsItsRow},
}
// TestWitnesses is the deterministic half of the mutation evidence.