package hostlife

import "testing"

// The cases region HA spec 1 §9 L18 and claim rev 6.30 §11 require of the
// joint model, each in a one-box and in a two-box region (bothShapes):
// region 0 holds box 0 alone, kept at one box by its group, or boxes 0
// and 3. Each is a direct test: it drives the case through the model's
// own actors and asserts the outcome the spec names; the final oracle
// (finish) checks every invariant. The witnesses (regionha_witness_test.go)
// are the mutation evidence; these are the coverage.

// serveAndPublish serves inc 1 of app A on box 0, runs it, and lets its
// first files manifest land, so a later failover has the host's files
// in S3 (finding F2 is the case where none landed).
func (w *world) serveAndPublish(t *testing.T) *box {
	from := w.boxes[0]
	w.serve(from, 1, app0)
	w.running(t, from)
	w.published(t, from)
	return from
}

// failedOver drives the failover of the terminated executor dead until
// the host serves again elsewhere, and returns the box it serves on: the
// peer in a two-box region, the box the group launched in a one-box
// region.
func (w *world) failedOver(t *testing.T, dead *box) *box {
	if !w.reach(t, 3000, "serving after the failover", func() bool {
		c := w.claim
		return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != dead.ID
	}, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) {
		return nil
	}
	return w.execBox(w.claim)
}

// relocTarget drives until the relocation names a target with its pin,
// and returns it (a one-box region's failover names the replacement the
// group launched once it enrolls).
func (w *world) relocTarget(t *testing.T) *box {
	if !w.reach(t, 400, "a target named and pinned", func() bool {
		c := w.claim
		return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 && c.Op.Pin != nil
	}, w.actAll(), w.recoveryPass) {
		return nil
	}
	return w.boxByID(w.claim.Op.Tgt)
}

func TestL18CreateSpread(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		w.serve(w.boxes[0], 1, app0)
		w.h2 = liteHost{}
		w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app0, OpID: w.newID("cr"), Inc: 9})
		w.reach(t, 50, "the second host of app A placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole)
		want := 0
		if boxes == 2 {
			want = 3 // the box running no instance of A (H12)
		}
		if w.h2.Box != want {
			t.Fatalf("the second instance of app A landed on box %d, want %d", w.h2.Box, want)
		}
		if boxes == 1 {
			return
		}
		w.h2 = liteHost{}
		w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app1, OpID: w.newID("cr"), Inc: 10})
		w.reach(t, 50, "the second host of app B placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole)
		tie := 0
		if tieHash(3) > tieHash(0) {
			tie = 3
		}
		if w.h2.Box != tie {
			t.Fatalf("tie-break: app B landed on box %d, want the greater tieHash (%d)", w.h2.Box, tie)
		}
	})
}

func TestL18RelocationByDrain(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		wr := w.appWrite(from)
		id := w.timerOn(from)
		w.userRelocate()
		if boxes == 1 {
			// no eligible target: the drain never starts and the host keeps
			// serving where it is (spec §4)
			if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID {
				t.Fatalf("a drain started in a one-box region: %s", w.state())
			}
			w.finish(t)
			return
		}
		to := w.peer()
		if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != to.ID {
			t.Fatalf("the drain did not start: %s", w.state())
		}
		w.servingOn(t, to)
		if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] > 1 || w.stats["writes declared lost"] != 0 {
			t.Errorf("released coverage: %d released, %d writes_lost covering %d writes (want 1, at most the first serving wake's, and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"], w.stats["writes declared lost"])
		}
		w.finish(t)
		if !contains(to.DB.Log, wr) || !contains(to.Timers, id) && !w.delivered[id] {
			t.Errorf("the drain lost write %d or timer %d", wr, id)
		}
	})
}

func TestL18TerminationDuringServing(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		wr := w.appWrite(from)
		w.replicate(from)
		w.completeDue(true)
		w.terminate(from)
		to := w.failedOver(t, from)
		if to == nil {
			return
		}
		if boxes == 2 && to != w.peer() || boxes == 1 && to.ID < 100 {
			t.Errorf("served on box %d after the failover (one-box regions wait for the group's replacement)", to.ID)
		}
		w.finish(t)
		if to.DB == nil || !contains(to.DB.Log, wr) {
			t.Errorf("the failover lost the replicated write %d", wr)
		}
	})
}

func TestL18NestedFailover(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		w.extraBox(0, spareID())
		var to *box
		if boxes == 2 {
			w.drainTo(t, nil)
			to = w.boxByID(w.claim.Op.Tgt)
		} else {
			w.terminate(from)
			to = w.relocTarget(t)
		}
		if to == nil || !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.actAll(), w.recoveryPass, func() { w.wake(to) }) {
			return
		}
		wr := w.appWrite(to)
		w.replicate(to)
		w.completeDue(true) // the target's write is in P's remote before it dies
		w.terminate(to)
		next := w.failedOver(t, to)
		w.finish(t)
		if next == nil || next.DB == nil || !contains(next.DB.Log, wr) {
			t.Fatalf("the nested failover lost the target's replicated write %d", wr)
		}
		if w.stats["nested failover after P was admitted"] != 1 {
			t.Fatalf("no nested failover: %v", w.stats)
		}
	})
}

func TestL18StaleEdgesFile(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		if boxes == 1 {
			// a one-box region's former executor is gone: a request through
			// its stale edges file reaches nothing
			w.terminate(from)
			w.failedOver(t, from)
			w.drive(30, never, func() { w.reconcile(from); w.wake(from) })
			if hasMain(from) {
				t.Fatalf("the terminated box ran the host")
			}
			w.finish(t)
			return
		}
		to := w.peer()
		w.drainTo(t, to)
		w.servingOn(t, to)
		if from.Row == nil || from.Row.Status == "ready" {
			t.Fatalf("the former executor's row is not held: %+v", from.Row)
		}
		w.drive(30, never, func() { w.reconcile(from); w.wake(from) })
		if hasMain(from) {
			t.Fatalf("a request through the stale edges file started the host on the former executor")
		}
		w.finish(t)
	})
}

func TestL18UnenrolledReference(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		if p := w.peer(); p != nil {
			p.HasKey = false // the region's other box may work, never take the host (R9)
		}
		w.terminate(from)
		w.now += replaceDelay
		w.launchReplacements()
		nb := w.boxes[len(w.boxes)-1]
		if nb.Region != 0 || nb.Enrolled {
			t.Fatalf("no unenrolled replacement in region 0: %+v", nb)
		}
		nb.EnrollAt = w.now + 10*enrollDelay // its confirmation is slow
		w.drive(3*enrollDelay, never, w.actAll(), w.recoveryPass)
		c := w.claim
		if c.Op.Exec == nb.ID || c.Op.Tgt == nb.ID {
			t.Fatalf("an unenrolled box was named: %s", w.state())
		}
		if boxes == 2 && (c.Op.Kind != "serving" || contains(c.Lost, from.ID)) {
			// Worker.Start needs an eligible target (rev 7, Astra round 4
			// finding 3): the failover does not start, and the claim still
			// names the dead box, until the replacement enrolls
			t.Fatalf("the failover started with no eligible target: %s", w.state())
		}
		if boxes == 1 && c.Op.Kind != "serving" {
			// no enrolled worker of the region exists to write the fence: the
			// claim still names the dead box until the replacement enrolls
			t.Fatalf("a one-box region was fenced with no enrolled worker in it: %s", w.state())
		}
		nb.EnrollAt = w.now - enrollDelay
		if to := w.failedOver(t, from); to != nb {
			t.Fatalf("served on %v, want the replacement %d once enrolled", to, nb.ID)
		}
		w.finish(t)
	})
}

// TestL18AdverseVolume (claim §11's adverse-volume case; H19; rev 5, Astra
// round 2 finding 2): the current executor is terminated with a
// volume that was not DeleteOnTermination. Execution recovery proceeds
// to serving on the region's other box (two-box) or on the group's
// replacement (one-box) with no operator, and the dead box's park-local
// stays open throughout; only the operator's cleanup (the declared
// destroyed-local loss) removes it.
func TestL18AdverseVolume(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		from.DeleteOnTermination = false
		w.terminate(from) // the current executor
		if !w.reach(t, 3000, "serving after the failover, with no operator", func() bool {
			c := w.claim
			return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != from.ID
		}, w.actAll(), w.recoveryPass, w.wakeExec) {
			return
		}
		to := w.execBox(w.claim)
		if boxes == 2 && to != w.peer() {
			t.Fatalf("served on %v, want the region's other box %d", to, w.peer().ID)
		}
		if !w.owesLocal(w.claim, from) {
			t.Fatalf("the dead box's park-local is not open after the failover: %s", w.state())
		}
		if w.stats["fence: park-local chores left open (volume evidence)"] == 0 || w.stats["fence: park-local chores discharged"] != 0 {
			t.Fatalf("the fence's discharge ignored the volume evidence: %v", w.stats)
		}
		w.drive(200, never, w.actAll(), w.recoveryPass, w.wakeExec)
		if !w.owesLocal(w.claim, from) {
			t.Fatalf("the dead box's park-local closed without the operator: %s", w.state())
		}
		w.finish(t) // the operator's destroyed-local declaration clears it
		if w.owesLocal(w.claim, from) {
			t.Fatalf("the park-local is still open after the operator's cleanup: %s", w.state())
		}
	})
}

func TestL18CrashDuringInstallation(t *testing.T) {
	for _, boxes := range []int{1, 2} {
		for _, at := range []string{"installing", "installed", "probing"} {
			t.Run(map[int]string{1: "one-box region", 2: "two-box region"}[boxes]+"/"+at, func(t *testing.T) {
				w := regionWorld(boxes)
				from := w.serveAndPublish(t)
				w.timerOn(from)
				if boxes == 2 {
					w.drainTo(t, nil)
				} else {
					w.terminate(from)
				}
				w.relocPhase(t, at, w.actAll(), w.recoveryPass)
				to := w.boxByID(w.claim.Op.Tgt)
				w.drive(2, never, w.act(to)) // a step into the phase: a PUT issued, a files directory extracted
				w.crash(to)
				if c := w.claim; c.Op.Kind == "relocating" && c.Op.Phase == "probed" && c.Op.ProbeStop == nil && to.probeRecord == nil {
					// the probe passed and the crash came before the probe
					// stop recorded its flush (ruling 87): no replicator, so
					// the stop refuses until the deadline, and the operator's
					// resolve serves the host elsewhere
					w.servingOn(t, nil)
				} else {
					w.servingOn(t, to)
				}
				w.finish(t)
				w.mustHold(t)
			})
		}
	}
}

func TestL18LateFileUploads(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		late := w.timerOn(from)
		loc := w.claim.Holder.Location
		w.holdKey(loc + "files/")
		w.publishFiles(from) // the manifest carrying the timer, held
		w.hold = nil
		w.terminate(from)
		to := w.failedOver(t, from)
		if to == nil {
			return
		}
		if contains(to.Timers, late) {
			t.Fatalf("the install applied a manifest that had not landed at the pin")
		}
		declared := false
		for _, a := range w.acks {
			if a.W == late && a.Exempt {
				declared = true
			}
		}
		if !declared {
			t.Fatalf("the timer the late manifest carried was not declared with the fence")
		}
		if n := w.completeHeld(loc + "files/"); n != 1 {
			t.Fatalf("held manifest PUTs completed: %d, want 1", n)
		}
		w.finish(t)
	})
}

func TestL18LatePutAfterTermination(t *testing.T) {
	bothShapes(t, func(t *testing.T, w *world, boxes int) {
		from := w.serveAndPublish(t)
		late := w.appWrite(from)
		loc := w.claim.Holder.Location
		w.holdKey(loc)
		w.replicate(from) // the upload of the late write is held
		w.hold = nil
		w.terminate(from)
		to := w.failedOver(t, from)
		if to == nil {
			return
		}
		if contains(to.DB.Log, late) {
			t.Fatalf("the install restored a write whose upload had not landed at the pin")
		}
		if n := w.completeHeld(loc); n == 0 {
			t.Fatalf("no held upload to complete")
		}
		w.finish(t) // the late object lands in generation_from, read by nothing, parked
	})
}

// ---------- claim §11's region HA witnesses beyond L18 (two-box) ----------

// TestRelocationStartRacesPurge: a worker read the serving claim, then
// paused; a purge started meanwhile. A fresh start reads the purging
// claim and refuses; no relocation runs over a purging host.
func TestRelocationStartRacesPurge(t *testing.T) {
	w := twoBoxWitness()
	w.serve(w.boxes[0], 1, app0)
	w.userPurge()
	w.reach(t, 100, "the purge started", func() bool { return w.claim.Op.Kind == "purging" || w.admit[app0].Closed }, w.runConsole)
	w.userRelocate()
	if w.claim.Op.Kind == "relocating" {
		t.Fatalf("a relocation started over a purging host: %s", w.state())
	}
	w.finish(t)
	w.mustHold(t)
}

// TestEmptyDatabaseDrain: a created host whose database never committed
// (nothing replicated) but has files and a timer is drained: the release
// flushes at 0, the pin is an evidenced empty one, and the files and the
// timer arrive through the manifests.
func TestEmptyDatabaseDrain(t *testing.T) {
	w := twoBoxWitness()
	w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})
	w.reach(t, 100, "created", func() bool { c := w.claim; return c != nil && c.Holder != nil && c.Op.Kind == "serving" }, w.runConsole, w.recoveryPass)
	from := w.execBox(w.claim)
	w.reach(t, 100, "the host runs", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) })
	id := w.timerOn(from)
	key := from.Files.Key
	w.published(t, from)
	w.drainTo(t, nil)
	to := w.boxByID(w.claim.Op.Tgt)
	w.servingOn(t, to)
	w.finish(t)
	w.mustHold(t)
	if !contains(to.Timers, id) && !w.delivered[id] {
		t.Fatalf("the timer did not survive the empty-database drain")
	}
	if to.Files == nil || to.Files.Key != key {
		t.Fatalf("the files did not survive the empty-database drain: %+v", to.Files)
	}
}

// TestReleasedThenFailedProbe: the drain's first probe admission is
// covered released; the target cannot run the app, fails its probe,
// releases, and the nested relocation's admission is covered by the
// failed target's own release: nothing is declared.
func TestReleasedThenFailedProbe(t *testing.T) {
	w := twoBoxWitness()
	w.claimC1 = true // the failed target's release (claim ask C1, finding 4)
	from, to := w.boxes[0], w.boxes[3]
	to.FailApp = true
	w.serve(from, 1, app0)
	w.running(t, from)
	w.drainTo(t, to)
	third := w.extraBox(0, 30)
	w.servingOn(t, third)
	w.finish(t)
	w.mustHold(t) // nothing acknowledged is lost: each later attempt declares its predecessor's session, which acknowledged nothing
	if w.stats["admissions covered: released"] < 1 {
		t.Fatalf("the drain's first probe admission was not covered released: %v", w.stats)
	}
}

// TestStuckAfterTwoReplacements (reloc-replacement-cap, an operator
// bound): three targets die at installing; the third death is the
// exhausted fence, the operation is stuck, and the operator's resolve
// replays it onto a spare.
func TestStuckAfterTwoReplacements(t *testing.T) {
	w := twoBoxWitness()
	from := w.boxes[0]
	w.serve(from, 1, app0)
	w.running(t, from)
	w.extraBox(0, 30)
	w.extraBox(0, 31)
	w.drainTo(t, nil)
	for i := 0; i < 3; i++ {
		if !w.reach(t, 1500, "a target installing", func() bool {
			c := w.claim
			return c.Op.Kind == "relocating" && c.Op.Phase == "installing" && c.Op.Stuck == ""
		}, w.act(w.liveBoxes()...), w.recoveryPass) {
			t.Fatalf("target %d never installed: %s", i, w.state())
		}
		x := w.boxByID(w.claim.Op.Exec)
		w.terminate(x)
		w.reach(t, 100, "fenced", func() bool { return contains(w.claim.Lost, x.ID) }, w.act(w.liveBoxes()...))
	}
	if w.claim.Op.Stuck == "" {
		t.Fatalf("a third loss did not make the operation stuck: %s", w.state())
	}
	w.extraBox(0, spareID())
	w.servingOn(t, nil) // the operator resolves it
	w.finish(t)
	w.mustHold(t)
	if w.stats["operator resolved a stuck relocation"] != 1 {
		t.Fatalf("the operator did not resolve it: %v", w.stats)
	}
}

// TestReleaseStopsAnEscapedDescendant (L10): a process that escaped the
// cgroup is stopped with the whole tree before release step 1 passes
// (the model's evidence-whole-tree: the cleanup-only reopen kills the
// cgroup and every identified stray); the source's release is journaled
// only once nothing of the host runs on it.
func TestReleaseStopsAnEscapedDescendant(t *testing.T) {
	w := twoBoxWitness()
	from, to := w.boxes[0], w.boxes[3]
	w.serve(from, 1, app0)
	w.running(t, from)
	from.Procs = append(from.Procs, &proc{Main: false, Strict: false, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session})
	w.drainTo(t, to)
	if !w.reach(t, 300, "the source's release journaled", func() bool { return w.claim.Op.Release != nil }, w.act(from, to), w.recoveryPass) {
		w.mustHold(t)
	}
	if len(from.Procs) != 0 {
		t.Fatalf("the release was journaled with %d processes of the host alive on the source", len(from.Procs))
	}
	w.servingOn(t, to)
	w.finish(t)
	w.mustHold(t)
}

// ---------- the bounds: direct evidence for the rules no invariant catches alone ----------

// TestDrainRefusedForANeverWokenHost (reloc-drain-needs-writer, ruling
// 11): a host with no writer session is never drained; its failover
// relocates it.
func TestDrainRefusedForANeverWokenHost(t *testing.T) {
	w := twoBoxWitness()
	w.serve(w.boxes[0], 1, app0)
	w.cas(w.claim, func(n *claim) bool { n.Holder.Session = 0; return true })
	w.userRelocate()
	if w.claim.Op.Kind != "serving" || w.stats["drain refused: the host never had a writer"] != 1 {
		t.Fatalf("a never-woken host was drained: %s", w.state())
	}
}

// TestReplacedTargetAcknowledgesBeforePinning (reloc-ack-before-pinning):
// the target is replaced in releasing; the operation leaves releasing
// only once the replacement's execution lease is current.
func TestReplacedTargetAcknowledgesBeforePinning(t *testing.T) {
	w := twoBoxWitness()
	from, to := w.boxes[0], w.boxes[3]
	w.serve(from, 1, app0)
	w.running(t, from)
	w.published(t, from)
	w.drainTo(t, to)
	spare := w.extraBox(0, 30)
	w.relocPhase(t, "releasing", w.act(from, to), w.recoveryPass)
	w.terminate(to)
	w.reach(t, 100, "the target replaced in releasing", func() bool { return w.claim.Op.Tgt == spare.ID }, w.act(from))
	// the spare never acts: no lease, so the operation must stay in releasing
	w.drive(40, never, w.act(from))
	if c := w.claim; c.Op.Phase != "releasing" || w.stats["pin after release: waits for the acknowledgements"] == 0 {
		t.Fatalf("left releasing without the replacement's acknowledgement: %s", w.state())
	}
	w.servingOn(t, spare)
	w.finish(t)
	w.mustHold(t)
}

// TestProbeAttemptsCountedBeforeTheyAreMade (reloc-probe-attempts,
// ruling 19): an agent that crashes in every attempt never buys a
// fourth; the target goes to probe-failed after three.
func TestProbeAttemptsCountedBeforeTheyAreMade(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.relocPhase(t, "probing", w.act(from, to), w.recoveryPass)
	to.envUnreadyFor = 1000 // the launch environment never gets ready: each attempt is still starting when the agent dies
	before := w.stats["admissions: cold"]
	for i := 0; i < 8 && w.claim.Op.Phase == "probing"; i++ {
		w.drive(3, func() bool { return to.open != nil }, w.act(to))
		w.crash(to) // each attempt dies before its probe
	}
	if n := w.stats["admissions: cold"] - before; n > probeTries || w.claim.Op.Phase == "probing" {
		t.Fatalf("%d attempts admitted, phase %s; want at most %d, then probe-failed", n, w.claim.Op.Phase, probeTries)
	}
}

// TestCreateNamesItsExecutorOnce (create-choice-once, claim P5-D2,
// P5-D6): a create names its executor in the intent; when that box is
// gone before the create completes, recovery cancels the create and
// never substitutes the region's other box.
func TestCreateNamesItsExecutorOnce(t *testing.T) {
	w := twoBoxWitness()
	p := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0}
	w.admit[app0].Reg[p.OpID] = regEntry{Until: w.now + 1000}
	w.console = append(w.console, p)
	w.reach(t, 50, "the create claimed the host", func() bool { c := w.claim; return c != nil && c.Op.Kind == "creating" }, w.runConsole)
	chosen := w.boxByID(w.claim.Op.NewBox)
	w.terminate(chosen)
	w.drive(200, func() bool { c := w.claim; return c == nil || c.Holder == nil || c.Op.Kind == "serving" }, w.runConsole, w.recoveryPass)
	if c := w.claim; c != nil && c.Holder != nil && c.Op.Kind == "serving" {
		t.Fatalf("the create substituted box %d for its chosen box %d", c.Op.Exec, chosen.ID)
	}
	if w.stats["create cancelled: its box is gone"] != 1 {
		t.Fatalf("the create was not cancelled: %v", w.stats)
	}
}

// TestStoppedBoxNeverFenced (fence-terminated-only): a stopped executor
// is never fenced; when it starts again with its disk, it serves.
func TestStoppedBoxNeverFenced(t *testing.T) {
	w := twoBoxWitness()
	from, to := w.boxes[0], w.boxes[3]
	w.serve(from, 1, app0)
	w.running(t, from)
	from.Destroyed, from.Procs = true, nil // stopped, not terminated
	w.drive(100, never, w.act(to), w.recoveryPass)
	if contains(w.claim.Lost, from.ID) || w.claim.Op.Kind != "serving" {
		t.Fatalf("a stopped box was fenced: %s", w.state())
	}
	from.Destroyed = false
	w.running(t, from)
	w.finish(t)
	w.mustHold(t)
}

// TestRelocationStartGuardRefuses (reloc-start-guard): a whole-location
// chore in the region refuses the start; a park-generation does not.
func TestRelocationStartGuardRefuses(t *testing.T) {
	w := twoBoxWitness()
	w.serve(w.boxes[0], 1, app0)
	w.claim.Obl = append(w.claim.Obl, obligation{ID: "pg", Op: "old", Kind: "park-generation", Region: 0, Box: -1, Prefix: w.claim.Holder.Location, Ret: "old"})
	if !w.relocationStartAllowed(w.claim, w.boxes[0], w.boxes[3]) {
		t.Fatalf("a park-generation refused the start (L11)")
	}
	w.claim.Obl = append(w.claim.Obl, obligation{ID: "pr", Op: "old", Kind: "park-replica", Region: 0, Box: -1, Prefix: w.claim.Holder.Location})
	if w.relocationStartAllowed(w.claim, w.boxes[0], w.boxes[3]) {
		t.Fatalf("a park-replica in the region did not refuse the start (CC11)")
	}
}

// TestOnlyTheExecutorInstalls (reloc-exec-only-installs, HA2): through a
// drain, no box but op.exec writes P or makes a local install.
func TestOnlyTheExecutorInstalls(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.servingOn(t, to)
	if from.receipt != nil || from.Files != nil && from.Files.Gen != "" && from.Files.Gen == w.claim.Holder.Gen {
		t.Fatalf("the source made a local install of P")
	}
}

// ---------- findings F1 to F3, closed by 1b-next rev 17 to 19 ----------

// TestFailoverBeforeTheFirstManifest (finding F2, closed by 1b-next
// ruling 25 as rev 18 amended it): a host none of whose files manifests
// has landed is terminated. The pin refuses files that carry no
// instance.key for a nonempty database, the operation is stuck, and
// nothing is installed: no fresh key over sealed data. The database is
// unrecoverable by relocation (L21); the operator's replay never accepts
// the keyless pin. Under the mutation of files-pin-needs-key the install
// mints a fresh key (INV-4) and this test fails.
func TestFailoverBeforeTheFirstManifest(t *testing.T) {
	w := twoBoxWitness()
	from := w.boxes[0]
	w.serve(from, 1, app0)
	loc := w.claim.Holder.Location
	w.holdKey(loc + "files/") // the first manifest's PUT has not landed
	w.running(t, from)
	w.hold = nil
	w.terminate(from)
	w.drive(400, func() bool { return len(w.violations) > 0 }, w.actAll(), w.recoveryPass, w.wakeExec)
	w.mustHold(t)
	c := w.claim
	if c.Op.Kind != "relocating" || c.Op.Stuck == "" || c.Op.Pin != nil || c.Op.Prepared != "" {
		t.Fatalf("the failover did not stop at an unevidenced files pin: %s", w.state())
	}
	if w.stats["pin: files unevidenced, no instance.key"] == 0 {
		t.Fatalf("the pin never refused: %v", w.stats)
	}
}

// TestProbeFailedInATwoBoxRegion (finding F1, closed by 1b-next ruling
// 26): a drain's target cannot run the app; its probe fails and it
// releases. With no spare the worker waits, and ReleaseDeadline after
// probe_failed_since the operation is stuck; nothing names the source
// automatically. The operator's resolve returns the host to the source
// (plan ruling 13). Under the mutation of reloc-no-spare-bound the
// operation waits for ever (INV-3) and this test fails.
func TestProbeFailedInATwoBoxRegion(t *testing.T) {
	w := twoBoxWitness()
	w.claimC1 = true // the failed target's release (claim ask C1, finding 4)
	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.reach(t, 1500, "probe-failed with the target released", func() bool {
		c := w.claim
		return c.Op.Phase == "probe-failed" && c.Op.Release != nil && c.Op.Release.Box == to.ID
	}, w.actAll(), w.recoveryPass)
	w.drive(releaseDeadline/2, never, w.actAll(), w.recoveryPass)
	if c := w.claim; c.Op.Stuck != "" || c.Op.Tgt == from.ID {
		t.Fatalf("before the deadline the operation is stuck or names the source: %s", w.state())
	}
	w.reach(t, 1500, "stuck with no spare", func() bool { return w.claim.Op.Stuck == "no eligible box for the nested relocation" }, w.actAll(), w.recoveryPass)
	w.servingOn(t, from)
	w.finish(t)
	w.mustHold(t)
}

// TestAbandonedPreparedGenerationParked (finding F3, closed by 1b-next
// ruling 27 and rev 18 finding 3): an unopened P is recorded on every
// path that drops it and parked at completion. installing: the target
// is replaced at installing and the replacement builds P'. probe-failed:
// the probe deadline passes before any admission, the target is then
// terminated, and the replacement table's nested branch drops P. Under
// the mutation of reloc-abandoned-prepared INV-10 finds P's objects.
func TestAbandonedPreparedGenerationParked(t *testing.T) {
	for _, path := range []string{"installing", "probe-failed"} {
		t.Run(path, func(t *testing.T) {
			w := twoBoxWitness()
			from, to := w.boxes[0], w.boxes[3]
			w.serve(from, 1, app0)
			w.running(t, from)
			w.published(t, from)
			w.drainTo(t, to)
			third := w.extraBox(0, 30)
			w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass)
			p := w.claim.Op.Prepared
			if path == "probe-failed" {
				w.dropPBeforeAdmission(t, from, to)
			} else {
				w.terminate(to)
			}
			w.reach(t, 300, "P dropped", func() bool { return w.claim.Op.Prepared != p }, w.actAll(), w.recoveryPass)
			w.servingOn(t, third)
			if w.stats["relocation: abandoned prepared generation parked"] == 0 {
				t.Fatalf("the abandoned P %q was not parked at serving", p)
			}
			w.finish(t)
			w.mustHold(t)
		})
	}
}

// dropPBeforeAdmission is rev 18 finding 3's trace: the target freezes
// in probing until the probe deadline passes with P unopened, the worker
// moves it to probe-failed, and it is terminated there.
func (w *world) dropPBeforeAdmission(t *testing.T, from, to *box) {
	w.reach(t, 1500, "probing", func() bool { return w.claim.Op.Phase == "probing" }, w.act(from, to), w.recoveryPass)
	to.Frozen = true
	w.reach(t, 3*probeDeadline, "probe-failed before any admission", func() bool { return w.claim.Op.Phase == "probe-failed" }, w.act(from), w.recoveryPass)
	if preparedOpened(w.claim) {
		t.Fatalf("P was opened")
	}
	w.terminate(to)
}

// invNumber is the n of the first "INV-n" in a violation, 0 if none.
func invNumber(v string) int {
	for i := 0; i+4 < len(v); i++ {
		if v[i:i+4] == "INV-" {
			n := 0
			for j := i + 4; j < len(v) && v[j] >= '0' && v[j] <= '9'; j++ {
				n = n*10 + int(v[j]-'0')
			}
			return n
		}
	}
	return 0
}

// mustHold fails the test, with the trace, if any invariant was violated.
func (w *world) mustHold(t *testing.T) {
	t.Helper()
	if len(w.violations) > 0 {
		dump(t, w)
		t.Fatalf("%s", w.violations[0])
	}
}