package release

import (
	"fmt"
	"math/rand"
	"os"
	"sort"
	"strconv"
	"strings"
	"sync"
	"testing"

	"github.com/carlosframework/platform/internal/registry"
)

// TestUpdateRequestLifecycleSimulation runs random schedules of one
// instance's update life across three boxes (settings plan 4 Task 11): the
// channel head moves and bakes, the member presses "Update now", pins,
// unpins and holds, root and agent passes decide and repoint, wakes run
// builds against the database, boxes are lost and the instance moves.
//
// The decisions are production's: rootPass calls Target and NextConsumed;
// wake calls DecideHeldWake (the held wake check, ruling R-HELD-PURE) and
// enforces it as the activator's wakeCheck does (refuse, run the target, or
// wait for root), then HeldExecStale and NextBuildState (beforeExec, ruling
// R-MERGE); a graceful move calls CarryRequest (ruling R-SPEC-43A-2), and
// root's write of its record passes publishGate, the re-check root makes
// under the carry fence (ruling R-CARRY-FENCE). What
// surrounds them is not pure (settingsTarget's file and registry reads,
// adoptHost's bake, evidence and repoint, beforeExec's bucket write, the
// wake's wait) and is mirrored here in the smallest form that keeps its
// decisions.
//
// The invariants are checked against the model's own records, never against
// production helpers (a mutant of Watermark must not also move the oracle):
//
//  1. A completed request never runs again: once the watermark is >= R, no
//     box resolves R again, rule 2 never selects R again, and no wake
//     records R as newly completed. A wake that completes R does so because
//     R's T ran, and a wake that runs the build state's T for a pending R
//     completes it. The watermark is spec §4.3 rule 2's (ruling R-INV1): the
//     highest completed id in the bucket's build state (the true object,
//     whatever the box's copy says) or in the consumed file of the box doing
//     the pass, and also every failed completion a box had recorded when the
//     instance left it by a graceful move (ruling R-INV1-2: the move carries
//     it; only a lost box's records are exempt). UPDATESIM_STRICT=1 reads
//     every box's consumed file at once instead; that is documentation of a
//     known gap, not the gate (below).
//  2. The build state names the build that last touched the database.
//  3. No install lacks evidence. At the decision: Target names pointer
//     evidence only for the head, and asks for bake only on the head. At
//     the repoint: the build is the head, has a promotion record, or is the
//     box's own staged copy; that half holds by construction of the
//     adoptHost mirror (its evidence switch), and is kept as a tripwire.
//  4. Failure records outrank: no repoint a Target decision makes for a
//     route with settings lands on a build the box holds as failed (the
//     model never sets GoodVersion, so no instance has served a failed
//     build). A route with default settings keeps today's adoption, which
//     never reads the book, consumed file or not (rulings R-T6-BOOK,
//     R-T6-BOOK-2; adopt.go settingsTarget's !plain), so it is out of scope.
//  5. Unresolved requests block nothing: a held instance with an unresolved
//     request whose head is baking recovers onto last_executed; and a held
//     instance (no pin) never repoints anywhere but last_executed, a T its
//     pending request was resolved to, or, never having run, the head.
//  6. A request resolves at its first eligible pass, pin or not: the world
//     records firstEligible[R], the head at the first root pass where R is
//     pending, the build state is read (R-TARGET-UNKNOWN) and the head is
//     eligible on that box (or the request asked for fast track). That pass
//     must resolve R to it; every resolution of R a box records, and every
//     rule 2 install of R, names exactly that build. A resolution the
//     instance can no longer see was never run (a run completes R in the
//     build state), so it is spec §4.2's "Lost requests": firstEligible[R]
//     is cleared and the next eligible pass resolves R again. A record the
//     instance sees again (it returned to the box holding it) is R's
//     resolution once more; when the build state and the box's file both
//     hold one, the build state's is (ruling R-RESOLUTION-STATE-WINS), and
//     root's next pass with the state read rewrites the file to agree.
//  7. A wake runs only what the rules allow (§4.3 rule 3, "The wake checks
//     too"; ruling R-HELD-PURE), from the model's own records: a pinned
//     instance runs its pin; one with a pending request resolved to T runs
//     T; a held one runs the bucket's last_executed. Held is manual, or a
//     major setting whose head, as of root's last decision on this box, has
//     no tag or another major, or a major setting root has not decided for
//     yet (a missing or stale decision never makes a wake unheld).
//
// Copies (the agent's registry copy root and the wake read) go stale the ways
// production keeps them stale: a refresh that fails keeps the last known
// state and records ReadErr; a box the instance returns to may still hold its
// row from the earlier stay, copy and all, its refreshes failed while the
// instance was away. Root reads such a copy as unread (BuildStateCopy.Read).
// The wake refreshes first and is refused when that fails (Astra round 1
// finding 1).
//
// Strict mode (UPDATESIM_STRICT=1) checks invariants 1 and 6 across every
// box's consumed file, not only the one the instance is on. It is not the
// gate (ruling R-INV1): a LOST box's records are the spec's lost request
// (§4.2), and strict mode counts them.
//
// Seeds: UPDATESIM_SEEDS (default 200), spread over UPDATESIM_PAR goroutines
// (default 1); each seed has its own rand source and world. UPDATESIM_SEED=n
// replays seed n alone. A failure prints the seed, the step and the trace,
// and a line "INVARIANT <n> ..." per invariant any seed violated.
func TestUpdateRequestLifecycleSimulation(t *testing.T) {
	t.Run("seed 531 shape, unpinned", testUpdateSimSeed531Unpinned)
	t.Run("carry fence, a failed completion racing a cut", testUpdateSimCarryFence)
	t.Run("a file and the build state disagree on R1", testUpdateSimDisagreement)
	seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200)
	par := updateSimEnv(t, "UPDATESIM_PAR", 1)
	first := 0
	if v := os.Getenv("UPDATESIM_SEED"); v != "" {
		n, err := strconv.Atoi(v)
		if err != nil {
			t.Fatal(err)
		}
		first, seeds = n, 1
	}
	if par < 1 {
		par = 1
	}
	strict := os.Getenv("UPDATESIM_STRICT") == "1"
	results := make([]updateSimResult, seeds)
	jobs := make(chan int)
	var wg sync.WaitGroup
	for i := 0; i < par; i++ {
		wg.Add(1)
		go func() {
			defer wg.Done()
			for i := range jobs {
				results[i] = runUpdateSim(int64(first+i), updateSimSteps, strict)
			}
		}()
	}
	for i := 0; i < seeds; i++ {
		jobs <- i
	}
	close(jobs)
	wg.Wait()

	var total updateSimStats
	byInv := map[int][]*updateSimFailure{}
	for i := range results {
		total.add(results[i].stats)
		if f := results[i].fail; f != nil {
			seen := map[int]bool{}
			for _, v := range f.viols {
				if !seen[v.inv] {
					seen[v.inv] = true
					byInv[v.inv] = append(byInv[v.inv], f)
				}
			}
		}
	}
	t.Logf("%d seeds x %d steps (par %d, strict %v): %s", seeds, updateSimSteps, par, strict, total)
	invs := make([]int, 0, len(byInv))
	for inv := range byInv {
		invs = append(invs, inv)
	}
	sort.Ints(invs)
	for _, inv := range invs {
		fs := byInv[inv]
		f := fs[0]
		var msg string
		for _, v := range f.viols {
			if v.inv == inv {
				msg = v.msg
				break
			}
		}
		t.Errorf("INVARIANT %d (%s) violated in %d of %d seeds; first: seed %d step %d (%s): %s\ntrace (replay with UPDATESIM_SEED=%d):\n%s",
			inv, updateSimInvariants[inv], len(fs), seeds, f.seed, f.step, f.action, msg, f.seed, strings.Join(f.trace, "\n"))
	}
}

// testUpdateSimSeed531Unpinned replays the shape seed 531 found, through
// the model's own actions (so every invariant is checked at every step) and
// so through the production Target, NextConsumed, DecideHeldWake,
// CarryRequest, publishGate and NextBuildState. Box 0 runs a root pass that
// was already running when the cut began; before the carry fence its write
// landed after the cut carried box 0's record and stayed in box 0's file
// only. Under the fence (ruling R-CARRY-FENCE) it comes after the carry, so
// it meets the cut's hold and writes nothing. Box 1 resolves R1, to b3,
// under a pin set after the request, and its wake (running the pin) carries
// {R1, b3} into the build state; the instance returns to box 0, which holds
// no record of R1, and the pin is cleared. Rule 2 must then install the
// build state's b3, and the wake that runs it must complete R1.
func testUpdateSimSeed531Unpinned(t *testing.T) {
	w := newUpdateSimWorld(0, false)
	w.scripted = true
	for i := range w.boxes {
		w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
	}
	w.builds = []string{"b1", "b2", "b3"}
	for i, b := range w.builds {
		w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
	}
	w.head = "b2"
	for _, b := range w.boxes[:2] {
		b.eligible["b1"], b.eligible["b2"] = true, true
	}
	w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"}
	w.lastRan, w.replica = "b1", true
	w.at = 0
	w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true
	w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
	w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}

	steps := []func() string{
		func() string { w.settings.Pin = "b1"; return "pin b1 (after the request)" },
		func() string {
			return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, true)
		},
		func() string { w.head = "b3"; w.boxes[1].eligible["b3"] = true; return "promote b3, baked on box1" },
		func() string { return w.rootPass(w.boxes[1], true) },
		func() string { return w.wake(w.boxes[1]) },
		func() string { return w.moveTo(0, true) },
		func() string { w.settings.Pin = ""; return "unpin" },
		func() string { return w.rootPass(w.boxes[0], true) },
		func() string { return w.wake(w.boxes[0]) },
	}
	if !runScriptedSim(t, "the scripted seed-531 shape", w, steps) {
		return
	}
	if c := w.boxes[0].consumed; c != nil && c.Resolved != nil && c.Resolved.Target == "b2" {
		t.Errorf("scripted seed-531 shape: box0's racing pass published {R1, b2} under the cut's hold\ntrace:\n%s", strings.Join(w.trace, "\n"))
	}
	if st := w.state; st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[0].live != "b3" {
		t.Errorf("scripted seed-531 shape: after the unpinned pass and wake on box0, live %q, build state %+v; want b3 live and R1 completed by it\ntrace:\n%s",
			w.boxes[0].live, w.state, strings.Join(w.trace, "\n"))
	}
	t.Logf("trace:\n%s", strings.Join(w.trace, "\n"))
}

// runScriptedSim runs a scripted shape's steps, checking every invariant
// after each; false when one failed (reported).
func runScriptedSim(t *testing.T, name string, w *simWorld, steps []func() string) bool {
	t.Helper()
	for i, step := range steps {
		w.viols = nil
		action := step()
		w.trace = append(w.trace, fmt.Sprintf("%3d %s  %s", i+1, action, w.summary()))
		w.check()
		for _, v := range w.viols {
			t.Errorf("INVARIANT %d (%s) violated in %s at step %d (%s): %s\ntrace:\n%s",
				v.inv, updateSimInvariants[v.inv], name, i+1, action, v.msg, strings.Join(w.trace, "\n"))
		}
		if len(w.viols) > 0 {
			return false
		}
	}
	return true
}

// testUpdateSimDisagreement gates resolvedFor's order (ruling
// R-RESOLUTION-STATE-WINS; ruling R-M9-SCRIPTED) on a state built directly:
// box 0's consumed file resolves the pending R1 to b1 while the build state
// resolves the same R1 to b3, unpinned and manual. Under the carry fence no
// graceful path in this model leaves that state behind any more. It is still
// reachable in production from a box running a pre-fence binary (a racing
// root pass wrote its record after the cut's carry), or from a registry copy
// that stays stale for one reconcile without a read error (root resolves R1
// again from a copy that lacks the state's resolution). Root's rule 2 must
// install the build state's b3 (through the production Target and
// NextConsumed), and the wake that runs it must complete R1 (DecideHeldWake,
// HeldExecStale and NextBuildState). Following the file would run b1, which
// never completes R1.
func testUpdateSimDisagreement(t *testing.T) {
	w := newUpdateSimWorld(0, false)
	w.scripted = true
	for i := range w.boxes {
		w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
	}
	w.builds = []string{"b1", "b2", "b3"}
	for i, b := range w.builds {
		w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
	}
	w.head = "b3"
	for _, b := range w.boxes {
		b.eligible["b1"], b.eligible["b2"], b.eligible["b3"] = true, true, true
	}
	w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b2", Resolved: &ResolvedRequest{ID: 1, Target: "b3"}}
	w.lastRan, w.replica = "b2", true
	w.at = 0
	b0 := w.boxes[0]
	b0.live, b0.staged["b2"] = "b2", true
	b0.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
	b0.consumed = &Consumed{Schema: 1, Host: updateSimHost, Resolved: &ResolvedRequest{ID: 1, Target: "b1"}}
	w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}
	// R1's resolution as the world records it: the build state's
	// (R-RESOLUTION-STATE-WINS), so invariant 6 judges installs against b3.
	w.syncResolutions()
	steps := []func() string{
		func() string { return w.rootPass(b0, true) },
		func() string { return w.wake(b0) },
	}
	const name = "the scripted disagreement (file {R1, b1}, build state {R1, b3})"
	// The outcome is asserted even when an invariant stopped the steps early.
	runScriptedSim(t, name, w, steps)
	if st := w.state; b0.live != "b3" || st == nil || st.LastExecuted != "b3" || st.Completed != 1 || st.CompletedFailed {
		t.Errorf("%s: live %q, build state %+v; want rule 2 to install the build state's b3 and its wake to complete R1\ntrace:\n%s",
			name, b0.live, st, strings.Join(w.trace, "\n"))
	}
	t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n"))
}

// testUpdateSimCarryFence is Astra round 2 finding 2's shape (ruling
// R-CARRY-FENCE), scripted both ways. Box 0 resolves R1 to b2 and installs
// it; b2 then fails on box 0, so root's next pass there records R1
// completed, failed. That pass races a graceful cut to box 1. Early (its
// fence first) it publishes, and the cut carries the failed completion: box
// 1 never selects R1. Late (the cut's fence first) it meets the cut's hold
// and publishes nothing: R1 is still pending with T b2, which box 1 does not
// hold as failed, so box 1 installs b2 and its wake completes R1. A late
// record published past the hold (the fence's re-check removed) is left
// behind on box 0, and box 1 selects R1 after it completed (invariant 1).
func testUpdateSimCarryFence(t *testing.T) {
	for _, late := range []bool{false, true} {
		name := "the carry fence, root's pass before the hold"
		if late {
			name = "the carry fence, root's pass after the carry"
		}
		w := newUpdateSimWorld(0, false)
		w.scripted = true
		for i := range w.boxes {
			w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
		}
		w.builds = []string{"b1", "b2"}
		for i, b := range w.builds {
			w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
		}
		w.head = "b2"
		for _, b := range w.boxes {
			b.eligible["b1"], b.eligible["b2"] = true, true
		}
		w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"}
		w.lastRan, w.replica = "b1", true
		w.at = 0
		w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true
		w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
		w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}
		steps := []func() string{
			func() string { return w.rootPass(w.boxes[0], true) },
			func() string { w.boxes[0].failed["b2"] = true; return "mark-failed b2 on box0" },
			func() string {
				return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, late)
			},
			func() string { return w.rootPass(w.boxes[1], true) },
			func() string { return w.wake(w.boxes[1]) },
		}
		if !runScriptedSim(t, name, w, steps) {
			continue
		}
		st, c := w.state, w.boxes[0].consumed
		switch {
		case !late && (st == nil || st.Completed != 1 || !st.CompletedFailed || w.boxes[1].live == "b2"):
			t.Errorf("%s: build state %+v, box1 live %q; want R1 carried completed, failed, and b2 never installed on box1\ntrace:\n%s",
				name, st, w.boxes[1].live, strings.Join(w.trace, "\n"))
		case late && (c == nil || c.Completed != 0 || st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[1].live != "b2"):
			t.Errorf("%s: box0's file %+v, build state %+v, box1 live %q; want nothing published on box0, b2 installed on box1 and R1 completed by its run\ntrace:\n%s",
				name, c, st, w.boxes[1].live, strings.Join(w.trace, "\n"))
		}
		t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n"))
	}
}

const (
	updateSimHost  = "blog.example.com"
	updateSimSteps = 80
	updateSimBoxes = 3
)

var updateSimInvariants = map[int]string{
	0: "model consistency",
	1: "a completed request never runs again",
	2: "the build state names the build that last touched the database",
	3: "no install lacks evidence",
	4: "failure records outrank",
	5: "unresolved requests block nothing",
	6: "a request resolves at its first eligible pass, pin or not",
	7: "a wake runs only what the rules allow",
}

func updateSimEnv(t *testing.T, name string, def int) int {
	v := os.Getenv(name)
	if v == "" {
		return def
	}
	n, err := strconv.Atoi(v)
	if err != nil || n < 0 {
		t.Fatalf("%s=%q: want a count", name, v)
	}
	return n
}

// simBox is one box's view of the instance: root's consumed file, the live
// link, the failure book, the version store's staged copies, the bake clock
// (versions whose window has run here) and the agent's registry copy of the
// build state, which is what root reads.
type simBox struct {
	name string
	// status is the row's status on this box: "" (ready), or "moving" from
	// the moment a cut holds it until the hand-over.
	status   string
	consumed *Consumed
	live     string
	failed   map[string]bool
	staged   map[string]bool
	eligible map[string]bool
	copy     BuildStateCopy
	// The model's own record of root's last decision on this box (for
	// invariant 7, never Consumed.Settings): the settings column it decided
	// for and the head it saw. decided is false until root's first pass.
	decided         bool
	decidedSettings string
	decidedHead     string
}

// simWorld is the instance and everything around it. state is the bucket
// object (nil until the first pre-exec write). replica is whether the
// instance has a database (a legacy instance has one with no build state).
type simWorld struct {
	boxes    []*simBox
	at       int
	state    *BuildState
	replica  bool
	settings UpdateSettings
	head     string
	builds   []string
	tags     map[string]string
	major    map[string]int // 0: the build has no semver tag
	promoted map[string]bool
	lastRan  string
	rng      *rand.Rand
	strict   bool

	firstEligible  map[uint64]string
	completedByRun map[uint64]bool
	// carried is the highest failed completion any box had recorded when
	// the instance left it by a graceful move (ruling R-INV1-2): invariant
	// 1's watermark includes it. Only a lost box's records are exempt.
	carried uint64
	// scripted turns off the random faults (a failed refresh, a wait root
	// does not answer), for the scripted shapes.
	scripted bool

	trace []string
	viols []updateSimViolation
	stats updateSimStats
}

type updateSimViolation struct {
	inv int
	msg string
}

type updateSimFailure struct {
	seed   int64
	step   int
	action string
	viols  []updateSimViolation
	trace  []string
}

type updateSimResult struct {
	fail  *updateSimFailure
	stats updateSimStats
}

// updateSimStats counts the scenarios the invariants need, so a clean run
// shows they were reached.
type updateSimStats struct {
	resolutions, runCompletions, failedCompletions int
	failedHeadResolutions                          int // R-TARGET-FAILEDHEAD
	heldRecoveries                                 int // invariant 5's scenario, repointing onto last_executed
	heldBakingPasses                               int // invariant 5's scenario, any
	unknownWithCompleted                           int // Known false, the current request already completed (R-TARGET-UNKNOWN)
	unknownReturning                               int // Known false on a box whose consumed file names the current request
	pinnedEligible                                 int // invariant 6 under a pin
	lostResolutions                                int
	pickedUp                                       int // a move or return made another record of R the one in force
	leftBehind                                     int // a resolution or rule 2 pick strict mode would refuse
	moves, returns                                 int
	carriedRequests                                int // graceful moves whose cut carried a request record
	carriedFailed                                  int // ... a failed completion among them
	unreadRefusals                                 int // wakes refused: their refresh failed
	askRoot                                        int // wakes with no decision from root for the settings
	askRootRuns                                    int // ... that ran the installed build at once
	rootWaits                                      int // wakes that asked root and waited
	heldRuns                                       int // wakes that ran a held target
	retainedRuns                                   int // ... from a retained copy
	keptCopies                                     int // returns onto a kept, possibly stale, copy
	racingEarly                                    int // root passes racing a cut that published before its carry
	racingFenced                                   int // ... that met the move hold under the fence: nothing published
}

func (s *updateSimStats) add(o updateSimStats) {
	s.resolutions += o.resolutions
	s.runCompletions += o.runCompletions
	s.failedCompletions += o.failedCompletions
	s.failedHeadResolutions += o.failedHeadResolutions
	s.heldRecoveries += o.heldRecoveries
	s.heldBakingPasses += o.heldBakingPasses
	s.unknownWithCompleted += o.unknownWithCompleted
	s.unknownReturning += o.unknownReturning
	s.pinnedEligible += o.pinnedEligible
	s.lostResolutions += o.lostResolutions
	s.pickedUp += o.pickedUp
	s.leftBehind += o.leftBehind
	s.moves += o.moves
	s.returns += o.returns
	s.carriedRequests += o.carriedRequests
	s.carriedFailed += o.carriedFailed
	s.unreadRefusals += o.unreadRefusals
	s.askRoot += o.askRoot
	s.askRootRuns += o.askRootRuns
	s.rootWaits += o.rootWaits
	s.heldRuns += o.heldRuns
	s.retainedRuns += o.retainedRuns
	s.keptCopies += o.keptCopies
	s.racingEarly += o.racingEarly
	s.racingFenced += o.racingFenced
}

func (s updateSimStats) String() string {
	return fmt.Sprintf("resolutions %d (failed head %d, under a pin %d), run completions %d, failed completions %d, "+
		"held+baking passes %d (recoveries onto last_executed %d), unread state with the request completed %d, "+
		"unread state on a returning box %d, lost resolutions %d, records picked up by a move %d, "+
		"left-behind records acted past %d, moves %d (returns %d, onto a kept copy %d), "+
		"cuts that carried a request record %d (a failed completion %d), wakes refused unread %d, "+
		"wakes with no decision for the settings %d (ran the installed build %d), wakes that waited on root %d, "+
		"held runs %d (from a retained copy %d), root passes racing a cut %d (published before the carry %d, fenced %d)",
		s.resolutions, s.failedHeadResolutions, s.pinnedEligible, s.runCompletions, s.failedCompletions,
		s.heldBakingPasses, s.heldRecoveries, s.unknownWithCompleted, s.unknownReturning, s.lostResolutions,
		s.pickedUp, s.leftBehind, s.moves, s.returns, s.keptCopies, s.carriedRequests, s.carriedFailed,
		s.unreadRefusals, s.askRoot, s.askRootRuns, s.rootWaits, s.heldRuns, s.retainedRuns,
		s.racingEarly+s.racingFenced, s.racingEarly, s.racingFenced)
}

func newUpdateSimWorld(seed int64, strict bool) *simWorld {
	w := &simWorld{
		rng:            rand.New(rand.NewSource(seed)),
		strict:         strict,
		settings:       UpdateSettings{Updates: UpdatesAuto},
		tags:           map[string]string{},
		major:          map[string]int{},
		promoted:       map[string]bool{},
		firstEligible:  map[uint64]string{},
		completedByRun: map[uint64]bool{},
	}
	for i := 0; i < updateSimBoxes; i++ {
		w.boxes = append(w.boxes, newSimBox(fmt.Sprintf("box%d", i)))
	}
	w.head = "b1"
	w.builds = []string{"b1"}
	w.tags["b1"], w.major["b1"], w.promoted["b1"] = "1.1.0", 1, true
	w.boxes[0].eligible["b1"] = true
	if w.rng.Intn(100) < 30 {
		// An instance from before this feature: a database, a live link, no
		// build state.
		w.replica = true
		w.boxes[0].live = "b1"
		w.boxes[0].staged["b1"] = true
	}
	if w.rng.Intn(100) < 25 {
		w.settings.Updates = UpdatesManual
	}
	return w
}

func newSimBox(name string) *simBox {
	return &simBox{name: name, failed: map[string]bool{}, staged: map[string]bool{}, eligible: map[string]bool{}}
}

func runUpdateSim(seed int64, steps int, strict bool) updateSimResult {
	w := newUpdateSimWorld(seed, strict)
	for step := 1; step <= steps; step++ {
		w.viols = nil
		action := w.act()
		w.trace = append(w.trace, fmt.Sprintf("%3d %s  %s", step, action, w.summary()))
		w.check()
		if len(w.viols) > 0 {
			return updateSimResult{stats: w.stats, fail: &updateSimFailure{seed: seed, step: step, action: action, viols: w.viols, trace: w.trace}}
		}
	}
	return updateSimResult{stats: w.stats}
}

func (w *simWorld) fail(inv int, format string, args ...any) {
	w.viols = append(w.viols, updateSimViolation{inv: inv, msg: fmt.Sprintf(format, args...)})
}

func (w *simWorld) cur() *simBox { return w.boxes[w.at] }

// act picks one action at random and applies it.
func (w *simWorld) act() string {
	weights := []int{8, 7, 9, 22, 5, 9, 14, 4, 2, 5, 5, 5, 3}
	sum := 0
	for _, x := range weights {
		sum += x
	}
	n := w.rng.Intn(sum)
	i := 0
	for ; n >= weights[i]; i++ {
		n -= weights[i]
	}
	switch i {
	case 0:
		return w.updateNow()
	case 1:
		return w.promote()
	case 2:
		return w.expireBake()
	case 3:
		return w.rootPass(w.cur(), true)
	case 4:
		return w.rootPass(w.cur(), false)
	case 5:
		return w.refresh()
	case 6:
		return w.wake(w.cur())
	case 7:
		return w.move()
	case 8:
		return w.loseBox()
	case 9:
		return w.markFailed()
	case 10:
		return w.toggleManual()
	case 11:
		return w.pin()
	default:
		return w.setMajor()
	}
}

// updateNow is the console's "Update now": a new request id. The console
// refuses it on a pinned instance (console apiupdates.go); a pin set while a
// request is pending is allowed, so the model sets pins either way.
func (w *simWorld) updateNow() string {
	if w.settings.Pin != "" {
		return "update-now refused: pinned"
	}
	w.settings.InstallRequest++
	w.settings.InstallFastTrack = w.rng.Intn(100) < 20
	return fmt.Sprintf("update-now R%d fast=%v", w.settings.InstallRequest, w.settings.InstallFastTrack)
}

// promote moves the channel head: a new build (no box has baked it yet), or
// a pull-back to an earlier one, which stays eligible wherever it baked.
func (w *simWorld) promote() string {
	if len(w.builds) > 1 && w.rng.Intn(100) < 15 {
		var older []string
		for _, b := range w.builds {
			if b != w.head {
				older = append(older, b)
			}
		}
		w.head = older[w.rng.Intn(len(older))]
		return "promote pull-back " + w.head
	}
	n := len(w.builds) + 1
	b := fmt.Sprintf("b%d", n)
	w.builds = append(w.builds, b)
	w.head = b
	w.promoted[b] = w.rng.Intn(100) < 85
	switch r := w.rng.Intn(100); {
	case r < 10:
		w.major[b], w.tags[b] = 0, ""
	default:
		m := 1
		if r >= 75 {
			m = 2
		}
		w.major[b], w.tags[b] = m, fmt.Sprintf("%d.%d.0", m, n)
	}
	return fmt.Sprintf("promote %s record=%v tag=%q", b, w.promoted[b], w.tags[b])
}

func (w *simWorld) expireBake() string {
	b := w.cur()
	if w.rng.Intn(100) >= 60 {
		b = w.boxes[w.rng.Intn(len(w.boxes))]
	}
	b.eligible[w.head] = true
	return fmt.Sprintf("bake-expired %s on %s", w.head, b.name)
}

// refresh is the agent reading the bucket object into its registry copy.
// One that fails keeps the last known copy and records ReadErr, as
// buildStates.refresh does.
func (w *simWorld) refresh() string {
	b := w.cur()
	if w.refreshCopy(b) {
		return "refresh " + b.name
	}
	return "refresh " + b.name + " FAILED (copy kept, read error)"
}

// refreshCopy is buildStates.refresh on b: true when the read succeeded.
func (w *simWorld) refreshCopy(b *simBox) bool {
	if !w.scripted && w.rng.Intn(100) < 15 {
		b.copy.ReadErr = "s3: timeout"
		return false
	}
	b.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(w.state)}
	return true
}

// move hands the instance to another box with its replica and build state:
// a graceful move (a legacy cut, a Phase 1 cut, a rollback's return). The
// destination's registry row is new (copy unread) or carries the source's
// column (registry coldhandover copies build_state); a box the instance
// returns to may still hold its row from the earlier stay, old copy and all
// (a rolled-back move's source keeps its row). It still has its old consumed
// file and live link either way.
//
// A third of moves race a root pass on the source that was already running
// when the cut began (Astra round 2 finding 2). Under the carry fence it
// either published before the cut's carry, which takes its record, or meets
// the cut's hold and publishes nothing (moveToRacing).
func (w *simWorld) move() string {
	j := w.rng.Intn(len(w.boxes) - 1)
	if j >= w.at {
		j++
	}
	carried := w.rng.Intn(100) < 50
	if w.rng.Intn(100) < 33 {
		src := w.cur()
		return w.moveToRacing(j, carried, func() string { return w.rootPass(src, true) }, w.rng.Intn(100) < 50)
	}
	return w.moveTo(j, carried)
}

// moveTo moves the instance to box j; carried is whether the destination's
// registry row carries the source's build-state copy.
func (w *simWorld) moveTo(j int, carried bool) string {
	return w.moveToRacing(j, carried, nil, false)
}

// moveToRacing is moveTo with race, when set, a root pass on the source that
// was already running when the cut began, modelled through the carry fence
// (ruling R-CARRY-FENCE). Root's publication and the cut's carry serialize
// on one lock, the cut takes it only once its hold is effective, and root
// re-checks the hold under it (publishGate, in rootPass). So the race runs
// either before the hold (early: its fence came first; it publishes, and
// the carry below takes the record) or after the carry (late: its fence
// came second; it meets the hold and publishes nothing). The cut holds the
// row ("moving"), then carries the source's request record into the build
// state under the lease (release.CarryRequest; ruling R-SPEC-43A-2), and the
// source's registry copy follows the write, as buildStates.write sets it.
// Invariant 1's carried watermark is the source's file at the hand-over,
// after both (Astra round 2's simulation note: never sampled before a
// racing callback).
func (w *simWorld) moveToRacing(j int, carried bool, race func() string, late bool) string {
	src := w.cur()
	dst := w.boxes[j]
	note := ""
	if race != nil && !late {
		note += " | racing (before the hold) " + race()
		w.stats.racingEarly++
	}
	src.status = "moving"
	next := CarryRequest(cloneSimState(w.state), cloneSimConsumed(src.consumed))
	if !SameRequestState(w.state, &next) {
		next.Schema, next.Host = 1, updateSimHost
		w.state = &next
		src.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(&next)}
		w.stats.carriedRequests++
		note += " carried " + simRes(next.Resolved) + fmt.Sprintf(" done %d%s", next.Completed, simFailedMark(next.CompletedFailed))
	}
	if race != nil && late {
		note += " | racing (after the carry) " + race()
		w.stats.racingFenced++
	}
	if c := src.consumed; c != nil && c.CompletedFailed && c.Completed > w.carried {
		w.carried = c.Completed
		w.stats.carriedFailed++
	}
	src.status = ""
	kept := false
	switch {
	case carried:
		dst.copy = cloneSimCopy(src.copy)
	case dst.copy.Known && !w.scripted && w.rng.Intn(100) < 50:
		kept = true // its row from the earlier stay
		w.stats.keptCopies++
	default:
		dst.copy = BuildStateCopy{}
	}
	if w.scripted || w.rng.Intn(100) < 60 {
		src.copy = BuildStateCopy{} // the route retires here
	} else if src.copy.Known {
		// The source keeps its row for a return. Its refreshes while the
		// instance is away read a location that is not this box's (another
		// bucket: refused) and fail, so the copy keeps its last state with a
		// read error; a refresh that succeeds would leave it fresh, which no
		// rule can mistake.
		src.copy.ReadErr = "s3: the instance is on another box"
	}
	w.at = j
	w.stats.moves++
	if dst.consumed != nil || dst.live != "" {
		w.stats.returns++
	}
	w.syncResolutions()
	return fmt.Sprintf("move %s->%s copy-carried=%v kept=%v%s", src.name, dst.name, carried, kept, note)
}

// loseBox replaces a box with an empty one: its consumed file, live link,
// version store, failure book and bake clock are gone. If the instance was
// on it, its registry row is new too.
func (w *simWorld) loseBox() string {
	k := w.rng.Intn(len(w.boxes))
	name := w.boxes[k].name
	w.boxes[k] = newSimBox(name)
	w.syncResolutions()
	return "lose " + name
}

// syncResolutions runs after a move or a lost box, for every request with a
// first eligible build. A resolution the instance can no longer see (no
// record in the build state or, strict mode aside, its box's consumed file)
// never ran, since a run completes the request in the build state: spec
// §4.2 "Lost requests", so the next eligible pass resolves it again. A
// record it can see is R's resolution from now on (the instance returned to
// a box holding one); of two, the build state's (R-RESOLUTION-STATE-WINS).
func (w *simWorld) syncResolutions() {
	b := w.cur()
	records := map[uint64]map[string]bool{}
	note := func(r *ResolvedRequest) {
		if r == nil {
			return
		}
		if records[r.ID] == nil {
			records[r.ID] = map[string]bool{}
		}
		records[r.ID][r.Target] = true
	}
	if w.state != nil {
		note(w.state.Resolved)
	}
	for _, x := range w.boxes {
		if (x == b || w.strict) && x.consumed != nil {
			note(x.consumed.Resolved)
		}
	}
	ids := map[uint64]bool{}
	for r := range w.firstEligible {
		ids[r] = true
	}
	for r := range records {
		ids[r] = true
	}
	for r := range ids {
		if r <= w.wm(b) {
			continue
		}
		seen := records[r]
		fe, had := w.firstEligible[r]
		switch {
		case len(seen) == 0:
			delete(w.firstEligible, r)
			w.stats.lostResolutions++
		case !w.strict:
			// One record, or the build state's when both hold one
			// (R-RESOLUTION-STATE-WINS).
			t := ""
			for x := range seen {
				t = x
			}
			if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r {
				t = w.state.Resolved.Target
			}
			if !had || t != fe {
				w.firstEligible[r] = t
				w.stats.pickedUp++
			}
		}
	}
}

func (w *simWorld) markFailed() string {
	b := w.cur()
	var cands []string
	add := func(v string) {
		if v != "" {
			cands = append(cands, v)
		}
	}
	add(b.live)
	add(w.head)
	add(w.settings.Pin)
	if w.state != nil {
		add(w.state.LastExecuted)
		if w.state.Resolved != nil {
			add(w.state.Resolved.Target)
		}
	}
	if b.consumed != nil && b.consumed.Resolved != nil {
		add(b.consumed.Resolved.Target)
	}
	v := cands[w.rng.Intn(len(cands))]
	b.failed[v] = true
	return fmt.Sprintf("mark-failed %s on %s", v, b.name)
}

func (w *simWorld) toggleManual() string {
	if w.settings.Updates == UpdatesManual {
		w.settings.Updates = UpdatesAuto
	} else {
		w.settings.Updates = UpdatesManual
	}
	return "updates=" + w.settings.Updates
}

func (w *simWorld) pin() string {
	if w.settings.Pin != "" && w.rng.Intn(100) < 50 {
		w.settings.Pin = ""
		return "unpin"
	}
	w.settings.Pin = w.builds[w.rng.Intn(len(w.builds))]
	return "pin " + w.settings.Pin
}

func (w *simWorld) setMajor() string {
	switch w.rng.Intn(3) {
	case 0:
		w.settings.Major = nil
		return "major=none"
	default:
		m := 1 + w.rng.Intn(2)
		w.settings.Major = &m
		return fmt.Sprintf("major=%d", m)
	}
}

// heldNow is rule 3's condition from the model's own records.
func (w *simWorld) heldNow() bool {
	u := w.settings
	if u.Updates == UpdatesManual {
		return true
	}
	return u.Major != nil && (w.major[w.head] == 0 || w.major[w.head] != *u.Major)
}

// wm is invariant 1's watermark for a pass or wake on box b: the highest
// completed id in the bucket's build state or b's consumed file (spec §4.3
// rule 2), or in every box's consumed file in strict mode.
func (w *simWorld) wm(b *simBox) uint64 {
	if w.strict {
		return w.watermarkAnywhere()
	}
	var m uint64
	if w.state != nil {
		m = w.state.Completed
	}
	if b.consumed != nil && b.consumed.Completed > m {
		m = b.consumed.Completed
	}
	if w.carried > m {
		m = w.carried
	}
	return m
}

// watermarkAnywhere is the highest completed id any record holds: the
// build state and every box's consumed file.
func (w *simWorld) watermarkAnywhere() uint64 {
	var m uint64
	if w.state != nil {
		m = w.state.Completed
	}
	for _, b := range w.boxes {
		if b.consumed != nil && b.consumed.Completed > m {
			m = b.consumed.Completed
		}
	}
	return m
}

// boxView is what a pass on b can see of request r: pending (above both
// sources' completed ids) and the T either source resolved it to, the build
// state's first (R-RESOLUTION-STATE-WINS).
func boxView(c *Consumed, st *BuildState, r uint64) (pending bool, t string) {
	var m uint64
	if c != nil {
		m = c.Completed
	}
	if st != nil && st.Completed > m {
		m = st.Completed
	}
	if r == 0 || r <= m {
		return false, ""
	}
	if st != nil && st.Resolved != nil && st.Resolved.ID == r {
		return true, st.Resolved.Target
	}
	if c != nil && c.Resolved != nil && c.Resolved.ID == r {
		return true, c.Resolved.Target
	}
	return true, ""
}

// rootPass is settingsTarget then adoptHost for the instance on box b.
// resolve is root's pass (it writes the consumed file); false is the agent's
// pass, which stops when the decision needs root's resolution.
func (w *simWorld) rootPass(b *simBox, resolve bool) string {
	who := "root"
	if !resolve {
		who = "agent"
	}
	u := w.settings
	head := w.head
	wmBefore := w.wm(b)
	held := w.heldNow()

	// settingsTarget: a route with default settings and no consumed file is
	// today's adoption (no Target, no book, no consumed write).
	viaTarget := !(u.Default() && b.consumed == nil)
	var dec TargetDecision
	var in TargetInput
	if !viaTarget {
		dec = TargetDecision{Version: head, Reason: ReasonAdopt, Evidence: EvidencePointer, Bake: true, Detail: head}
	} else {
		in = TargetInput{
			Route:     registry.Route{Host: updateSimHost, Kind: "instance", UpdateSettings: u.Column()},
			Pointer:   &ChannelPointer{Channel: "production", Version: head},
			HeadTag:   w.tags[head],
			Settings:  u,
			Build:     cloneSimCopy(b.copy),
			Consumed:  cloneSimConsumed(b.consumed),
			Installed: b.live,
		}
		if !b.eligible[head] {
			in.HeadHeld = "in its supply-chain bake window"
		}
		// settingsTarget gives Target the failure book only for a route
		// with settings (!plain); default settings keep today's adoption,
		// which never read it, even with a consumed file (R-T6-BOOK-2).
		if !u.Default() {
			failed := b.failed
			in.Failed = func(v string) bool { return failed[v] }
		}
		dec = Target(in)
		if resolve {
			// publishConsumed: root's record is written under the carry
			// fence, and only for a row no move holds (ruling
			// R-CARRY-FENCE). A refused pass publishes nothing and installs
			// nothing for the route: the decision never happened.
			if err := publishGate(&registry.Route{Host: updateSimHost, Kind: "instance", Status: b.status}); err != nil {
				return fmt.Sprintf("%s@%s %s: fenced: nothing published or installed", who, b.name, simDec(dec))
			}
		}
		w.checkEvidence(dec, head)
		w.checkDecision(b, in, dec, resolve, wmBefore, held)
		if resolve {
			next := NextConsumed(in, dec)
			b.consumed = &next
			b.decided, b.decidedSettings, b.decidedHead = true, u.Column(), head
			// Invariant 6: with the build state read, root's file agrees with
			// it on the pending request's T once the pass is written.
			if r := u.InstallRequest; in.Build.Read() && r > w.wm(b) && w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r &&
				next.Resolved != nil && next.Resolved.ID == r && next.Resolved.Target != w.state.Resolved.Target {
				w.fail(6, "after root's pass R%d has two resolutions: the build state says %s, %s's consumed file %s",
					r, w.state.Resolved.Target, b.name, next.Resolved.Target)
			}
		} else if dec.Resolve != nil && dec.Reason == ReasonRequest {
			return fmt.Sprintf("%s@%s %s: stops, relays to root", who, b.name, simDec(dec))
		}
	}
	desc := fmt.Sprintf("%s@%s %s", who, b.name, simDec(dec))

	// Invariant 5's scenario: a held instance, no pin, the build state read
	// with a last_executed, an unresolved request whose head bakes here.
	recovery := ""
	if viaTarget && held && u.Pin == "" && in.Build.Read() && in.Build.State != nil && in.Build.State.LastExecuted != "" {
		le := in.Build.State.LastExecuted
		pending, t := boxView(in.Consumed, in.Build.State, u.InstallRequest)
		if pending && t == "" && in.HeadHeld != "" && !u.InstallFastTrack && !b.failed[le] && (w.promoted[le] || b.staged[le]) {
			recovery = le
			w.stats.heldBakingPasses++
		}
	}
	defer func() {
		if recovery != "" && b.live != recovery {
			w.fail(5, "held, request R%d unresolved behind baking head %s, last_executed %s authorized: live is %q after the pass (%s)",
				u.InstallRequest, head, recovery, b.live, simDec(dec))
		}
	}()

	// adoptHost.
	ver := dec.Version
	if ver == "" {
		return desc + ": nothing installed"
	}
	if b.live == ver {
		return desc + ": up to date"
	}
	if (!viaTarget || dec.Bake) && !b.eligible[ver] {
		return desc + ": " + ver + " baking"
	}
	stagedBefore := b.staged[ver]
	switch {
	case !viaTarget || dec.Evidence == EvidencePointer:
		if ver != head {
			return desc + ": not the signed head, not staged"
		}
	case dec.Evidence == EvidenceRecord:
		if !w.promoted[ver] && !stagedBefore {
			return desc + ": no promotion record, no staged copy: refused"
		}
	default:
		return desc + ": no evidence"
	}

	// The repoint. Invariant 3's repoint half holds by construction of the
	// evidence switch above; it stays as a tripwire for the mirror.
	if !(ver == head || w.promoted[ver] || stagedBefore) {
		w.fail(3, "repointed onto %s: not the head %s, no promotion record, not staged on %s", ver, head, b.name)
	}
	if viaTarget && !u.Default() && b.failed[ver] {
		w.fail(4, "%s repointed onto %s, which it holds as failed (%s)", b.name, ver, simDec(dec))
	}
	if viaTarget && held && u.Pin == "" {
		ok := !w.replica && ver == head
		if w.state != nil && w.state.LastExecuted == ver {
			ok = true
		}
		if r := u.InstallRequest; r > w.wm(b) {
			if _, t := boxView(b.consumed, w.state, r); t == ver {
				ok = true
			}
		}
		if !ok {
			w.fail(5, "held instance repointed onto %s: not last_executed %q, not a T of pending R%d, not a new instance's head (%s)",
				ver, simLE(w.state), u.InstallRequest, simDec(dec))
		}
	}
	if recovery != "" && ver == recovery {
		w.stats.heldRecoveries++
	}
	prev := b.live
	b.staged[ver] = true
	b.live = ver
	return fmt.Sprintf("%s: repoint %q->%s", desc, prev, ver)
}

// checkEvidence is invariant 3 at the decision: only the head rests on the
// signed pointer, and only the head bakes (§4.1, §4.3: a pin, a resolved T
// and a recovery waive bake and need a record or a staged copy).
func (w *simWorld) checkEvidence(dec TargetDecision, head string) {
	if dec.Version == "" || dec.Version == head {
		return
	}
	if dec.Evidence == EvidencePointer {
		w.fail(3, "decision %s rests on the pointer for %s, not the head %s", simDec(dec), dec.Version, head)
	}
	if dec.Bake {
		w.fail(3, "decision %s bakes %s, not the head %s", simDec(dec), dec.Version, head)
	}
}

// checkDecision checks invariants 1 and 6 on one Target decision, before
// root writes it.
func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, resolve bool, wmBefore uint64, held bool) {
	u := in.Settings
	r := u.InstallRequest
	head := in.Pointer.Version

	if !in.Build.Read() && r != 0 {
		if w.state != nil && w.state.Completed >= r {
			w.stats.unknownWithCompleted++
		}
		if in.Consumed != nil && in.Consumed.Resolved != nil && in.Consumed.Resolved.ID == r {
			w.stats.unknownReturning++
		}
	}

	if all := w.watermarkAnywhere(); (dec.Reason == ReasonRequest && r <= all && r > wmBefore) ||
		(resolve && dec.Resolve != nil && dec.Resolve.ID <= all && dec.Resolve.ID > wmBefore) {
		w.stats.leftBehind++
	}

	// Invariant 1: rule 2 never selects a completed request.
	if dec.Reason == ReasonRequest && r <= wmBefore {
		w.fail(1, "rule 2 selected R%d (%s), already completed (watermark %d)", r, dec.Version, wmBefore)
	}
	if !resolve {
		return
	}
	if dec.Resolve != nil && dec.Resolve.ID <= wmBefore {
		w.fail(1, "%s resolved R%d again (to %s) after it completed (watermark %d)", b.name, dec.Resolve.ID, dec.Resolve.Target, wmBefore)
	}

	// Invariant 6: the first eligible pass resolves, pin or not (with the
	// build state read: never read, or a refresh that failed, is unread).
	if in.Build.Read() && r != 0 {
		pending, t := boxView(in.Consumed, in.Build.State, r)
		eligible := in.HeadHeld == "" || u.InstallFastTrack
		if pending && t == "" && eligible && r > wmBefore {
			if _, ok := w.firstEligible[r]; !ok {
				w.firstEligible[r] = head
			}
			if u.Pin != "" {
				w.stats.pinnedEligible++
			}
			want := w.firstEligible[r]
			if dec.Resolve == nil || dec.Resolve.ID != r || dec.Resolve.Target != want {
				w.fail(6, "R%d pending and %s eligible on %s (first eligible %s), pin %q: the pass resolved %s", r, head, b.name, want, u.Pin, simRes(dec.Resolve))
			}
		}
	}
	if dec.Resolve != nil {
		want, ok := w.firstEligible[dec.Resolve.ID]
		if !ok || want != dec.Resolve.Target {
			w.fail(6, "%s resolved R%d to %s; first eligible %q", b.name, dec.Resolve.ID, dec.Resolve.Target, want)
		}
		w.stats.resolutions++
		if b.failed[dec.Resolve.Target] {
			w.stats.failedHeadResolutions++
		}
	}
	if dec.Reason == ReasonRequest {
		if want := w.firstEligible[r]; dec.Version != want {
			w.fail(6, "rule 2 installs %s for R%d; first eligible %q", dec.Version, r, want)
		}
	}
	if dec.Fail != 0 {
		w.stats.failedCompletions++
	}
}

// wake is the agent's wake on box b, as production runs it with no planner
// and an identity it can exec by path:
//
//   - for a route whose settings could hold it, the copy is refreshed first
//     (buildStates.wakeTarget); a refresh that fails leaves ReadErr in it;
//   - the held wake check's decision is production's (DecideHeldWake, ruling
//     R-HELD-PURE), enforced as the activator's wakeCheck does: not held runs
//     the live link (today's wake); unread, unknown, or a target root reports
//     failed is refused; a held target runs when it is installed, or from
//     this box's retained copy; otherwise root is asked and the wake waits
//     for the install, and a changed answer ends the wait with nothing run.
//     With no decision from root for the current settings (AskRoot) the
//     build state's build runs only if it is installed; otherwise the wake
//     asks root for a pass and waits for its decision, then decides again.
//     The live link never runs blindly;
//   - a wait is root's pass, run inline (the stage relay), or, half the
//     time, no answer within the bound: the wake ends with nothing run;
//   - then beforeExec: HeldExecStale against the bucket object read under
//     the lease, and the merge, NextBuildState; then the run.
func (w *simWorld) wake(b *simBox) string {
	u := w.settings
	col := u.Column()
	desc := "wake@" + b.name
	if !u.Default() {
		if !w.refreshCopy(b) {
			desc += " (refresh failed)"
		}
	}
	decide := func() HeldWakeDecision {
		return DecideHeldWake(HeldWakeInput{Settings: col, Build: cloneSimCopy(b.copy), Consumed: cloneSimConsumed(b.consumed), Installed: b.live})
	}
	waitRoot := func() bool {
		w.stats.rootWaits++
		if !w.scripted && w.rng.Intn(100) < 50 {
			return false
		}
		desc += " [waits; " + w.rootPass(b, true) + "]"
		return true
	}
	d := decide()
	if d.Held && d.AskRoot && !d.Failed {
		w.stats.askRoot++
		if d.Target != "" && b.live == d.Target {
			w.stats.askRootRuns++
		} else {
			if !waitRoot() {
				return desc + ": no decision from root for its settings within the bound, nothing run"
			}
			if d = decide(); d.AskRoot && (d.Target == "" || b.live != d.Target) {
				return desc + ": root has not decided for its settings, nothing run"
			}
		}
	}
	run, retained := "", false
	switch {
	case !d.Held:
		run = b.live // today's wake
		if run == "" {
			return desc + ": nothing installed"
		}
	case d.Unread:
		w.stats.unreadRefusals++
		return desc + ": refused, its build state could not be read"
	case d.Unknown || d.Target == "":
		return desc + ": refused, build unknown"
	case d.Failed:
		return desc + ": refused, its target " + d.Target + " failed here"
	case b.live == d.Target:
		run = d.Target
	case !d.AskRoot && b.staged[d.Target]:
		run, retained = d.Target, true
	default:
		if !waitRoot() {
			return desc + ": waited for root to install " + d.Target + ", nothing run"
		}
		if b.live != d.Target {
			return desc + ": " + d.Target + " not installed when the wait ended, nothing run"
		}
		run = d.Target
	}
	if d.Held {
		w.stats.heldRuns++
		if retained {
			w.stats.retainedRuns++
			desc += " (retained copy)"
		}
	}
	// beforeExec: the held target revalidated against the object under the
	// lease, then the merge. A refused record runs nothing.
	fresh := DecideHeldWake(HeldWakeInput{Settings: col, Build: BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)},
		Consumed: cloneSimConsumed(b.consumed), Installed: b.live})
	if err := HeldExecStale(fresh, w.state, run, ""); err != nil { // the model's wake has no planner
		return desc + ": record refused: " + err.Error()
	}
	w.checkWakeRun(b, run)
	wmBefore := w.wm(b)
	cur := cloneSimState(w.state)
	next := NextBuildState(cur, cloneSimConsumed(b.consumed), run)
	next.Schema, next.Host = 1, updateSimHost

	if next.LastExecuted != run {
		w.fail(2, "wake ran %s; the build state says last_executed %q", run, next.LastExecuted)
	}
	var prev uint64
	if cur != nil {
		prev = cur.Completed
	}
	// Only the current request: a newer one supersedes an older resolution.
	if r := w.settings.InstallRequest; cur != nil && cur.Resolved != nil && cur.Resolved.ID == r && cur.Resolved.Target == run && r > w.wm(b) && next.Completed < r {
		w.fail(1, "wake ran %s, the build state's T for pending R%d, and R%d stays pending (completed %d)",
			run, cur.Resolved.ID, cur.Resolved.ID, next.Completed)
	}
	if next.Completed > prev && !next.CompletedFailed {
		r := next.Completed
		if r <= wmBefore || w.completedByRun[r] {
			w.fail(1, "wake running %s records R%d newly completed; already completed (watermark %d)", run, r, wmBefore)
		}
		if next.Resolved == nil || next.Resolved.ID != r || next.Resolved.Target != run {
			w.fail(1, "wake running %s records R%d completed, but R%d's T is %s", run, r, r, simRes(next.Resolved))
		}
		w.completedByRun[r] = true
		w.stats.runCompletions++
	}
	w.state = &next
	w.lastRan = run
	w.replica = true
	b.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(&next)}
	return fmt.Sprintf("%s runs %s", desc, run)
}

// checkWakeRun is invariant 7 on a wake about to run build run on box b, from
// the model's own records (never Consumed.Settings or Reason).
func (w *simWorld) checkWakeRun(b *simBox, run string) {
	u := w.settings
	if u.Default() {
		return
	}
	if u.Pin != "" {
		if run != u.Pin {
			w.fail(7, "pinned on %s, the wake on %s ran %s", u.Pin, b.name, run)
		}
		return
	}
	if r := u.InstallRequest; r != 0 && r > w.wm(b) {
		t := ""
		if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r {
			t = w.state.Resolved.Target
		} else if b.consumed != nil && b.consumed.Resolved != nil && b.consumed.Resolved.ID == r {
			t = b.consumed.Resolved.Target
		}
		if t != "" {
			if run != t {
				w.fail(7, "R%d pending with T %s, the wake on %s ran %s", r, t, b.name, run)
			}
			return
		}
	}
	held := u.Updates == UpdatesManual
	if !held && u.Major != nil {
		if !b.decided || b.decidedSettings != u.Column() {
			held = true // root has not decided for these settings: the wake holds
		} else {
			m := w.major[b.decidedHead]
			held = m == 0 || m != *u.Major
		}
	}
	if le := simLE(w.state); held && le != "" && run != le {
		w.fail(7, "held (updates %s, major %v; root decided for these settings: %v), the wake on %s ran %s, not last_executed %s",
			u.Updates, simMajor(u.Major), b.decided && b.decidedSettings == u.Column(), b.name, run, le)
	}
}

func simMajor(m *int) string {
	if m == nil {
		return "-"
	}
	return strconv.Itoa(*m)
}

// check is the per-step state check (invariant 2); event checks run inside
// the actions. A known copy that differs from the bucket is not a model
// error: production keeps one after a failed refresh, and on a box the
// instance returns to, until the next refresh (Astra round 1's note on this
// simulation). The wake refreshes before it decides and is refused when
// that fails; root's passes read the copy as it is.
func (w *simWorld) check() {
	if w.lastRan != "" && (w.state == nil || w.state.LastExecuted != w.lastRan) {
		w.fail(2, "the database last ran %s; the build state says %q", w.lastRan, simLE(w.state))
	}
}

func (w *simWorld) summary() string {
	b := w.cur()
	u := w.settings
	s := fmt.Sprintf("[at %s live %q head %s req %d pin %q upd %s", b.name, b.live, w.head, u.InstallRequest, u.Pin, u.Updates)
	if u.Major != nil {
		s += fmt.Sprintf(" major %d", *u.Major)
	}
	if w.state != nil {
		s += fmt.Sprintf(" | state le %s res %s done %d%s", w.state.LastExecuted, simRes(w.state.Resolved), w.state.Completed, simFailedMark(w.state.CompletedFailed))
	}
	if b.consumed != nil {
		s += fmt.Sprintf(" | consumed res %s done %d%s", simRes(b.consumed.Resolved), b.consumed.Completed, simFailedMark(b.consumed.CompletedFailed))
	}
	if !b.copy.Known {
		s += " | copy unread"
	}
	return s + "]"
}

func simFailedMark(f bool) string {
	if f {
		return " failed"
	}
	return ""
}

func simDec(d TargetDecision) string {
	s := fmt.Sprintf("{%s %q", d.Reason, d.Version)
	if d.Resolve != nil {
		s += " resolve " + simRes(d.Resolve)
	}
	if d.Fail != 0 {
		s += fmt.Sprintf(" fail R%d", d.Fail)
	}
	return s + "}"
}

func simRes(r *ResolvedRequest) string {
	if r == nil {
		return "-"
	}
	return fmt.Sprintf("R%d->%s", r.ID, r.Target)
}

func simLE(s *BuildState) string {
	if s == nil {
		return ""
	}
	return s.LastExecuted
}

func simStatesEqual(a, b *BuildState) bool {
	if a == nil || b == nil {
		return a == nil && b == nil
	}
	ra, rb := simRes(a.Resolved), simRes(b.Resolved)
	return a.LastExecuted == b.LastExecuted && ra == rb && a.Completed == b.Completed && a.CompletedFailed == b.CompletedFailed
}

func cloneSimState(s *BuildState) *BuildState {
	if s == nil {
		return nil
	}
	v := *s
	v.Resolved = cloneSimResolved(s.Resolved)
	return &v
}

func cloneSimConsumed(c *Consumed) *Consumed {
	if c == nil {
		return nil
	}
	v := *c
	v.Resolved = cloneSimResolved(c.Resolved)
	return &v
}

func cloneSimCopy(c BuildStateCopy) BuildStateCopy {
	c.State = cloneSimState(c.State)
	return c
}

func cloneSimResolved(r *ResolvedRequest) *ResolvedRequest {
	if r == nil {
		return nil
	}
	v := *r
	return &v
}