// Package hostlife is a deterministic, randomized model of the host
// lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md,
// rev 6.5, d36adcfa) and Phase 1 of move-any-app
// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.7).
//
// Since joint round 2 the model encodes what the specs say and nothing
// stronger: restore reads the holder's location and the generation the
// claim names, the start check compares markers, every multi-object step
// is split at its real write boundaries, and the final oracle only reads.
//
// It is test-only. Nothing here is product code: every file is a _test.go
// file, so `go build ./...` never sees it. It exists to find interleavings
// that prose review rounds kept missing, and to prove each protocol rule is
// load-bearing by mutation (see rules_test.go and README in the spec §14.2).
//
// The model is an abstraction. What it keeps, and what it drops, is listed
// in the spec's §14.2; the short version:
//
//   - one host, three regions, one box per region (plus replacement boxes);
//   - every bucket is versioned, with the real IAM split: a box has full
//     rights on its own data bucket, and only Put/Delete/CopyInto on another
//     region's moves/* (no Get, no ListVersions, no DeleteVersion);
//   - every S3 request may complete late, after the client gave up;
//   - boxes crash (agent restart: flat children die, memory lost), reboot,
//     freeze (whole-VM pause), pause (agent only), partition from the
//     control bucket, are destroyed, or boot-recover an old executable;
//   - the application writes and registers timers on its own, through
//     descendants that may outlive the main process.
package hostlife

import (
	"fmt"
	"sort"
	"strings"
)

const (
	nRegions = 3
	app0     = "A"
	app1     = "B"

	// Time is in model steps.
	// H, the late-completion horizon (claim §6.2a): a request may complete
	// up to H steps after issue. It is the signature-age limit plus the
	// request bound, request_limit_ns (claim rev 6.15 §2); the park scope
	// persists the request bound and the horizon is computed from it (R14-3)
	horizonH      = sigAgeH + requestLimitH
	sigAgeH       = 45  // the signature-age allowance (the 15 minutes)
	requestLimitH = 15  // request_limit_ns: the longest request, added to the signature age
	execTTL       = 40  // exec lease TTL
	execRenew     = 15  // renew when this close to expiry
	lostMargin    = 10  // declare-lost margin past expiry
	cutBudget     = 320 // absolute cut deadline after admission
	stagingTTL    = 400 // staging-work lease TTL: longer than the cut budget, as in production
	probeTries    = 3
	// probeStartWindow is a probe attempt's readiness window in steps (the
	// budget's 30 s, §7.3): the retry policy's app restarts within one
	// admitted session share it, and when it passes the attempt fails and
	// the operation counts one of its budgeted tries (rev 7.12 §7.7)
	probeStartWindow = 30
	readyWait        = 800 // abort a move whose readiness never comes
	maxSkew          = 1   // a box clock is within this of true time
	maxPause         = 3   // a typical pause between a check and the act (a VM freeze is longer)
	sigAge           = 30  // S3's signature-age limit; H covers it plus the longest request
	beyondH          = 20  // one long-tail request in this many completes after H (R2-1)
	retiredCap       = 32  // retired_incarnations keeps this many (claim rev 6 §2)
)

// retire adds inc to retired_incarnations, dropping the oldest past the cap.
func retire(xs []int, inc int) []int {
	xs = addUniq(xs, inc)
	if len(xs) > retiredCap {
		xs = append([]int(nil), xs[len(xs)-retiredCap:]...)
	}
	return xs
}

// ---------- storage ----------

type blob struct {
	Kind    string // "ltx", "base", "files", "snap", "lock", "manifest", "lease", "report", "gen"
	Inc     int    // incarnation tag; 0 = untagged legacy
	Gen     string // lineage that wrote it
	Seq     int
	SealKey int // the instance.key the data is sealed with
	// an LTX file (ltx_test.go, R4-1, R5-2): its level (0 and 1, 9 for a
	// snapshot), its range in replication numbering, the final image of
	// every key it touches (0 is a delete), and, for the oracle only, the
	// writes it covers. No database checksum: the pinned writers put none
	// in a file (litestreamfacts, R5-2)
	Level int
	Min   int
	Max   int
	Pages map[string]int
	TXs   []int
	// Full: the file carries every page (a snapshot, an anchor, litestream's
	// first sync after a cold initialization, a compaction of one of those),
	// so applying it replaces the state; a key absent from it is gone
	Full bool
	// a "gen" marker (R3-1, R4-1): the generation's snapshot by key, version
	// id and TXID
	Base    int
	SnapKey string
	TX      int
	// a "closed" certificate (claim rev 6.8 §6.4a): the writer's stamp and
	// session; Seq is its box and TX its max_txid
	Stamp   int
	Session int
	Files   *filesDir
	Timers  []int
	Refs    []ref // a park manifest's archive set
	Dels    []ref // a park manifest's deletion set, delete markers included
	Text    string
}

type ref struct {
	Region int // -1 = control bucket
	Key    string
	Ver    int
}

type version struct {
	ID        int
	B         *blob
	Marker    bool
	Straggler bool // created by a request that completed after H
	SweepOwed bool // a dead generation's files key its park kept while live: the at-rest sweep's once obsolete (claim §6.2a)
}

type bucket struct {
	objs map[string][]*version
}

func newBucket() *bucket { return &bucket{objs: map[string][]*version{}} }

func (b *bucket) keys(prefix string) []string {
	var out []string
	for k := range b.objs {
		if strings.HasPrefix(k, prefix) {
			out = append(out, k)
		}
	}
	sort.Strings(out)
	return out
}

func (b *bucket) current(key string) *version {
	vs := b.objs[key]
	if len(vs) == 0 {
		return nil
	}
	v := vs[len(vs)-1]
	if v.Marker {
		return nil
	}
	return v
}

func (b *bucket) byID(key string, id int) *version {
	for _, v := range b.objs[key] {
		if v.ID == id {
			return v
		}
	}
	return nil
}

// dataVersions are every non-marker version under prefix.
func (b *bucket) dataVersions(prefix string) []ref {
	var out []ref
	for _, k := range b.keys(prefix) {
		for _, v := range b.objs[k] {
			if !v.Marker {
				out = append(out, ref{Key: k, Ver: v.ID})
			}
		}
	}
	return out
}

func (b *bucket) hasData(prefix string, skipLock bool) bool {
	for _, k := range b.keys(prefix) {
		if skipLock && strings.HasSuffix(k, "lock.json") {
			continue
		}
		for _, v := range b.objs[k] {
			if !v.Marker {
				return true
			}
		}
	}
	return false
}

// ---------- locations and generations (claim C3a, moves rev 6 §5.1) ----------

// locationFor is holder.location for an incarnation.
func locationFor(inc int, legacy bool) string {
	if legacy || !on("location-per-incarnation") {
		return "instances/" + host + "/"
	}
	return fmt.Sprintf("instances/%s/%d/", host, inc)
}

// dataKey is a replica object of generation gen within location loc. The
// origin generation keeps the bare layout; every later generation has its
// own operation-scoped prefix, so a request from one generation that lands
// late can only ever add an object to that generation.
func dataKey(loc, gen, kind string) string {
	if gen == "" {
		return loc + kind
	}
	return loc + "g-" + gen + "/" + kind
}

func genMarkerKey(loc string) string { return loc + "generation.json" }

func isDataKey(k string) bool {
	return strings.HasPrefix(k, "instances/") && ltxKeyRe.MatchString(k)
}

// ---------- requests (late completion) ----------

type reqKind int

const (
	rPut reqKind = iota
	rDelVer
	rDelKey // bare-key delete: forbidden on host prefixes (mutation only)
	rCopy   // copy srcRegion/srcKey?versionId=srcVer -> region/key
)

type request struct {
	kind      reqKind
	region    int
	key       string
	b         *blob
	ver       int
	srcRegion int
	srcKey    string
	srcVer    int
	doneAt    int
	beyond    bool // completes after H
	ifSet     bool // a conditional PUT: If-Match ifVer, or If-None-Match when ifVer is 0
	ifVer     int
	hold      bool // the biased schedule holds it until its worst moment (rev 7.5: a generation marker)
	by        string
	done      bool // completed (or refused) on the server; the client may have given up long before
	at        int  // when the client issued it
	// result, for an immediate completion
	resultVer int
}

// ---------- local box state ----------

type filesDir struct {
	Inc   int
	Key   int    // the app's instance.key identity
	Gen   string // .files-gen marker
	Env   int    // admin token identity in <host>.env
	Done  bool   // markers written last
	Stamp int    // the installation stamp that produced it (claim rev 6.5 §6.3)
	// Obj is the files object that holds this content (region HA §5.6,
	// rev 4): written by the generation that first held it, in ObjRegion's
	// bucket; an unchanged file keeps naming it generations later
	Obj       string
	ObjRegion int
}

func (f *filesDir) clone() *filesDir {
	if f == nil {
		return nil
	}
	c := *f
	return &c
}

type localDB struct {
	Inc     int
	Loc     string // the holder location it was restored from (claim C3a)
	Gen     string // <dbPath>.gen
	Key     int    // the key it was sealed with
	State   map[string]int
	TX      int   // the lineage's transaction id: the oracle's order of acknowledged writes
	Pos     int   // the replication position: litestream's TXID, the count of files shipped, which every LTX range is numbered in (R5-1)
	Pending []int // writes since Pos (what the next LTX file ships)
	// Epoch is the agent process that was admitted for this database: a
	// session belongs to the agent's replicator, and a new agent process
	// is a new session (claim rev 6.10), so a restarted agent neither
	// replicates nor certifies for it (seed 8528 / 30,000: the restarted
	// agent's first sync was skipped at the dead session's remote position)
	Epoch int
	// the local level-0 files not yet confirmed uploaded, oldest first:
	// litestream writes each sync's file locally and the replica uploads
	// them in TXID order, never past one that has not completed (rev 7.6)
	Queue      []*blob
	InFlight   *request // the head's upload, as the client sees it
	InFlightAt int
	// FirstFull: the next level-0 file carries every page (litestream's
	// first sync after a cold initialization, fact R5-1c)
	FirstFull bool
	// Closing: the writer stopped cleanly and is draining its uploads
	// before writing its certificate (claim rev 6.8 §6.4a); CloseReq is the
	// marker PUT once issued
	Closing  bool
	CloseReq *request
	// Session is the writer session this database was admitted under; Issued
	// is every request the writer issued that did not return at once (level
	// 0, compaction, snapshot, retention), and Uncertain is sticky once any
	// of them timed out and was retried (R8-5): no certificate then.
	Session   int
	Issued    []*request
	Uncertain bool
	// RemotePos is the remote position the pinned replica caches until an
	// initialization or an error: the newest remote level-0 TXID it has
	// seen or uploaded (R8-5)
	RemotePos int
	Log       []int // every write applied here, for the oracle
	Stamp     int   // the installation stamp that produced this artifact (claim rev 6.5 §6.3)
	Seq       int
}

func (d *localDB) clone() *localDB {
	if d == nil {
		return nil
	}
	c := *d
	c.State = cloneState(d.State)
	c.Pending = append([]int(nil), d.Pending...)
	c.Queue = append([]*blob(nil), d.Queue...)
	c.Log = append([]int(nil), d.Log...)
	return &c
}

type proc struct {
	Main    bool
	Strict  bool // spawned into the host cgroup by strict placement
	Inc     int
	Gen     string
	Session int // the writer session the process was started under: what its acknowledgements carry (rev 7.13, R12-1)
	Box     int
}

type row struct {
	Inc    int
	App    string
	Status string // ready, moving, landing, restoring, releasing
	HoldOp string
	Repl   string // carried column
	Next   int    // carried column
}

type box struct {
	ID          int
	Region      int
	Destroyed   bool
	Frozen      bool // whole-VM pause: nothing on the box runs
	AgentPaused bool // the agent alone is paused
	AgentDown   bool // the agent crashed and has not restarted
	Partitioned bool // cannot reach the control bucket
	Old         bool // running a pre-floor executable
	HasKey      bool
	Skew        int
	FailApp     bool // the app fails its readiness check on this box
	FailArchive bool // the final archive fails (too large) on this box
	FailSettle  bool // the app passes one readiness check, works, then fails
	Nested      bool // nested layout: children survive an agent crash
	// region HA (two boxes per region, L18)
	Terminated   bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk
	TerminatedAt int
	// a relocation controller's durable record (hostexec, 1b-next Task 7):
	// the operation it belongs to, whether its scoped cleanup is still owed
	// (ground truth for INV-29), and the fault that makes the cleanup fail
	execRecord          string
	cleanupPending      bool
	cleanupFails        bool
	relRecord           *releaseRecord // (rev 9) ReleasePositions: the flushed positions of one release, recorded on disk against its stop; an agent restart keeps it
	fencePending        bool           // (rev 8) this worker step found a relocation participant's fence it could not consume
	FenceObservedAt     int            // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4)
	Enrolled            bool           // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17)
	EnrollAt            int
	DeleteOnTermination bool // every volume the box had attached carried the flag while it ran (§5.9): decides only the automatic discharge of its park-local chores (H19), never a fence
	installEpoch        int  // the agent process that made this box's local install for a relocation (B2-5): a later process never remakes it once an admission named P
	// receipt is the box's install journal for a relocation (1b-next Task 8c,
	// VerifyReceipt): durable, it survives an agent restart; a park of the
	// installation removes it, and so does a lost volume (a witness)
	receipt *receiptEntry
	// the files publisher (§5.6, Task 4): the generation it publishes in,
	// its sequence there, the state its last manifest carried (in memory),
	// and the release's final manifest while its PUT is outstanding
	pubGen     string
	pubSeq     int
	published  string
	releaseSeq int
	// attemptTag is the probe attempt this agent process has counted and
	// not yet ended (memory: a restart forgets it, and the next attempt is
	// counted again, ruling 19)
	attemptTag string
	// L18 joint round findings 2 and 3 (regionha_completion_test.go):
	// actFence is the activator's fence on the host (its owner; "" none),
	// in the agent's memory, so a restart empties it; probeFence is the
	// persisted owner a probe stop installs under (probe-fence.json),
	// kept until the completion is marked; relFence is root's admission
	// fence of a release (the op it closed admission for), written with
	// Collect after the flush and the positions (ruling 28), never a row
	// hold; owedDischarge
	// is ground truth, the completed relocation whose participation this
	// box has not yet discharged (C10). foreignFence is a witness's
	// stand-in for another operation's fence that its owner never lifted
	// (INV-32's ground truth). dischargeFails, markFails and crashAfter
	// are witness knobs on the completion pass
	actFence   string
	probeFence string
	relFence   string
	// launchClosedOp and launchClosedSession: the session whose launch
	// journal a release's StopWriters closed (durable; L18 joint round 2
	// finding 3): it is never relaunched, an admitted start included
	launchClosedOp      string
	launchClosedSession int
	// probeRecord is the probe stop's recorded positions (ruling 87),
	// durable: a restart after it stops the session without a new flush
	probeRecord    *probeRecordEntry
	owedDischarge  string
	foreignFence   string
	dischargeFails bool
	markFails      bool
	crashAfter     string

	Row     *row
	DB      *localDB
	Files   *filesDir
	Config  int    // incarnation the config.env was rendered for; 0 none
	CfgVer  int    // the bundle version it was rendered from
	Live    string // app the live symlink points at
	LiveInc int
	Timers  []int // active once-timers (registration ids)
	History []int // delivered history (disposable)
	Attempt int   // runner bookkeeping
	Procs   []*proc
	// Stamps is the local record per host incarnation (claim rev 6.5 §6.4,
	// R4-2): {active_stamp | none, retired_stamps}. A stamp is the claim
	// gen captured at the CAS that made an installation current here. A
	// writer is admitted only if its stamp equals the active one.
	Stamps map[int]*stamps
	Parked int // count of locally parked artifacts
	// open is an admitted session's start in progress (rev 7.11 §7.14):
	// the claim CAS is done; the purge, the restore, the app start and
	// readiness, the first upload, the marker and the anchor follow, each
	// retried by the same agent process; the session is the agent's, and a
	// new agent process is a new session (claim rev 6.10)
	open *openState
	// lastProbe is the last probe attempt's timing on this box (INV-19);
	// envUnreadyFor is a witness knob holding the launch environment
	// unready for that many steps after an attempt's app stage first runs
	lastProbe     probeTiming
	envUnreadyFor int
	// the retry policy for failed app starts within a session (rev 7.11
	// §7.14): consecutive failures, the earliest next attempt, and the
	// host marked failed once the limit is reached (no new sessions until
	// an operator clears it)
	startFails  int
	nextStart   int
	hostFailed  bool
	failCounted bool // the operation's probe counted this host failure as one failed try
	failedAt    int  // when the host was marked failed; the operator looks after a while
	// PurgeFails is the fault: the purge of the local database an admitted
	// writer must make before it starts returns an error (claim rev 6.9)
	PurgeFails bool
	// anchors are the PUTs this box's activator must see acknowledged before
	// it goes on (an anchor, a recovery's snapshot, a closed.json), by key
	// (rev 7.7, R6-1): a request the client has waited uploadTimeout steps
	// for is retried with the same bytes.
	anchors map[string][]*request

	ExecUntil int // local exec-lease file (watchdog input); 0 none
	// in-memory, lost on crash
	snap          *claim
	stale         *claim // a stalled worker's old read
	deferred      []*localWrite
	Epoch         int
	plans         []*plan
	stopped       map[string]bool
	StopEvidence  map[string]bool // published stop evidence, by operation (survives a restart)
	mem           map[string]bool
	evidAt        map[string]int
	pendingTimers []int
}

// plan is a host-specific write by a separate OS process
// (carlos-config-sync, carlos-adopt), decided now and acted on later: the
// shape of every stale-writer race (J-N8, J2-R2-3). It survives an agent
// crash, because it is not the agent; a reboot ends it. It may pause
// before it takes the host guard.
type plan struct {
	Kind string // "config", "adopt"
	Inc  int
	App  string
	Ver  int // the config bundle version it selected
	At   int // it takes the guard no earlier than this
	// Stamp is the installation stamp the pass read when it selected the
	// row (claim rev 6.5 §6.4, R2-3): the host guard admits the write only
	// if it is still the active stamp.
	Stamp int
}

// stamps is a box's local record for one incarnation of the host (claim
// rev 6.3 §6.4): the active installation's stamp (0 is none) and the
// stamps of the installations retired here.
type stamps struct {
	Active  int
	Retired []int
}

func (b *box) stampOf(inc int) int {
	if s := b.Stamps[inc]; s != nil {
		return s.Active
	}
	return 0
}

// stampRetired: st is in the record's retired_stamps for inc.
func (b *box) stampRetired(inc, st int) bool {
	s := b.Stamps[inc]
	return s != nil && contains(s.Retired, st)
}

// install is activation (claim rev 6.5 §6.4): the box's record for inc
// takes holder.stamp as the installing CAS wrote it (a create's serving
// CAS, a landing's flip, an adoption, a reinstall, a dirty rollback's
// probe CAS, a push's commit), or as initRecord read it fresh under the
// guard. Activation is one of the two moves of a stamp: the old active
// stamp, if any, goes into retired_stamps first, then the new one is set.
// Under the guard.
func (b *box) install(inc, gen int) {
	if b.Stamps == nil {
		b.Stamps = map[int]*stamps{}
	}
	if b.Stamps[inc] == nil {
		b.Stamps[inc] = &stamps{}
	}
	s := b.Stamps[inc]
	if s.Active != 0 && s.Active != gen && !contains(s.Retired, s.Active) {
		s.Retired = append(s.Retired, s.Active)
	}
	s.Active = gen
}

// retireArtifacts is claim rev 6.5's retire-artifacts(S): the local
// artifacts tagged S (the database, the files directory) are parked, and
// the record is untouched: neither active_stamp nor retired_stamps moves.
// Only activation and retire-installation move stamps. A landing uses it
// on its predecessor's leftovers; a dirty rollback parks its pre-move
// database with S still active, and S retires when the probe CAS's new
// stamp activates. It parks by tag, as the real inventory does (R6-4): an
// artifact of incarnation inc that carries another stamp stays, and the
// callers assert what they expect the tags to be (INV-6).
func (w *world) retireArtifacts(b *box, inc, stamp int) {
	w.retireDatabase(b, inc, stamp)
	if b.Files != nil && b.Files.Inc == inc && b.Files.Stamp == stamp {
		b.Files = nil
		b.Parked++
	}
}

// retireDatabase is retire-artifacts(S) for the database alone: the files
// directory is carried into the new generation (a push, F7 on §5.1; a
// landing's restore phase after its files were installed; the activator's
// park of a warm database from an earlier stay before a cold restore).
func (w *world) retireDatabase(b *box, inc, stamp int) {
	if b.DB != nil && b.DB.Inc == inc && b.DB.Stamp == stamp {
		b.DB = nil
		b.Parked++
	}
}

// retireStamp is claim rev 6.5's retire-installation: the active stamp
// moves into retired_stamps and becomes none; the caller parks every
// artifact. Used at a delete, a move away, and the quarantine.
func (b *box) retireStamp(inc int) {
	if b.Stamps == nil {
		b.Stamps = map[int]*stamps{}
	}
	if b.Stamps[inc] == nil {
		b.Stamps[inc] = &stamps{}
	}
	if a := b.Stamps[inc].Active; a != 0 {
		b.Stamps[inc].Retired = append(b.Stamps[inc].Retired, a)
	}
	b.Stamps[inc].Active = 0
}

// admitsStamp is the local record's admission (claim rev 6.5 §6.4): the
// writer's stamp must equal the active stamp; none active refuses all,
// and so does no record at all (R5-4: a writer is never admitted before
// initialization). The mutation of fence-stamp admits any writer for the
// incarnation while an installation is active (rev 7.4's behaviour); the
// mutation of fence-by-installation is rev 5.2's marker: once retired,
// never active again.
func (b *box) admitsStamp(inc, stamp int) bool {
	s := b.Stamps[inc]
	if s == nil {
		return false
	}
	if !on("fence-by-installation") && len(s.Retired) > 0 {
		return false
	}
	if s.Active == 0 {
		return false
	}
	if !on("fence-stamp") {
		return true
	}
	return stamp == s.Active
}

func (b *box) forget() {
	b.Epoch++ // every goroutine of the old agent is gone
	// a new agent process is a new session (claim rev 6.10): an admitted
	// start in progress is gone with its restored database and its
	// outstanding requests (R10-2), and the start retry count with it
	b.open = nil
	b.startFails, b.nextStart = 0, 0
	b.deferred = nil
	b.snap, b.stopped, b.stale = nil, nil, nil
	b.mem = map[string]bool{}
	b.evidAt = map[string]int{}
	b.pendingTimers = nil
	b.attemptTag = ""
	b.actFence = "" // the activator's fences die with the agent; probe-fence.json survives (ruling 75)
	if b.DB != nil {
		b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again
		// a writer that was draining before its clean close is gone with
		// its uploads unaccounted for: no closed.json (claim rev 6.6 §6.4a)
		b.DB.Closing, b.DB.CloseReq = false, nil
	}
	b.anchors = nil // the activator issues the anchor again, the same bytes
}

// ackedPut is a PUT the activator must see acknowledged before it goes on
// (R6-1): it issues the request once, retries the same bytes after
// uploadTimeout steps while none has returned, and reports whether one has.
func (w *world) ackedPut(b *box, key string, bl *blob, ifNone bool) bool {
	acked, inflight := false, false
	for _, r := range b.anchors[key] {
		if r.done {
			acked = true
		} else if w.now-r.at < uploadTimeout {
			inflight = true
		}
	}
	if acked || inflight {
		return acked
	}
	r := &request{kind: rPut, region: b.Region, key: key, b: bl, ifSet: ifNone}
	if v := w.issue(b.ID, r); v > 0 {
		return true
	}
	if r.done {
		return true // refused (412): the object is already there, written once
	}
	if b.anchors == nil {
		b.anchors = map[string][]*request{}
	}
	b.anchors[key] = append(b.anchors[key], r)
	return false
}

// ---------- control plane ----------

type holder struct {
	Inc    int
	App    string
	Serial int // ground-truth creation event (model only)
	Legacy bool
	// Location is holder.location (claim C3a): instances/<host>/<inc>/ for a
	// new incarnation, instances/<host>/ for an adopted legacy host. It never
	// changes while this holder holds the host.
	Location string
	// Gen is the generation within the location that the claim names as
	// current (moves rev 6 §5.1): "" is origin; a move, a push and a dirty
	// rollback each install a generation named by their op id.
	Gen string
	// WriterBox is holder.writer_box (claim rev 6.9): the box every
	// admission names as the current writer; it survives operation
	// replacement, so a later cold admission's writes_lost names it (R9-2).
	WriterBox int
	// Admissions is holder.admissions (claim rev 6.12): the record of writer
	// admissions whose chain is not yet finished or whose predecessors are
	// not yet queued for retirement, plus the last few covered ones; it
	// lives in the holder, so it survives every operation transition,
	// release and new operation. An admission's predecessor is always the
	// last entry here (session, box, generation), never the generation an
	// operation chose for a restore (R11-4)
	Admissions []admissionRecord
	// Session is holder.session (claim rev 6.8 §6.4a, R8-1): the gen of the
	// AdmitWriter CAS that admitted the current writer session. Every path
	// that opens replication goes through that CAS, which moves the
	// session forward, so a clean-close certificate (written per session)
	// is one-use by construction.
	Session int
	// Stamp is holder.stamp (claim rev 6.5 §2, R5-4): the gen produced by
	// the CAS that made the current installation current, written by that
	// same CAS: a create's serving CAS, adoption, a flip, a reinstall, a
	// dirty rollback's install, a push's commit. The claim is where a box
	// recovers its local record from.
	Stamp int
}

type obligation struct {
	ID     string
	Op     string
	Kind   string // park-replica, park-local, park-superseded, park-staging
	Region int
	Box    int
	Prefix string
	Ret    string
	Quiet  int        // not before
	Scope  *parkScope // the persisted park scope of a remote chore (claim rev 6.15 §2), bound before its first step runs
	Owner  string     // a regional chore's owner: "" is region:<r> (any worker of the region, P6-D5); box:<b> is the legacy form a fence passes to the region (1b-next rev 6 finding 2)
}

// parkScope is claim rev 6.23's park scope {location, incarnation,
// evidence_at, request_limit_ns} (§2), persisted in the chore when it is
// queued or bound before its first step, so every retry, an agent
// restart's included, uses the same location, archive incarnation and
// original evidence time: a retry's own clock is never evidence (R13-4,
// R15-1). Location is exactly one of instances/<host>,
// instances/<host>/<incarnation>, moves/<host>/<op id> (a move's staging
// or a rollback's return lane) or moves/<host> (the staging sweep), with
// no trailing "/". EvidenceAt is always the original evidence or fencing
// bound: the stop evidence a whole-location park cites, the seal bound of
// a staging lane (the time after which no staging writer, its lease
// holder included, can still write), the sweeping box's listing, the
// publication that supersedes a generation; never cleanup's start time.
// Every scope has the one deadline: acknowledge only after a listing
// later than EvidenceAt + H, H = sigAgeH + RequestLimit.
type parkScope struct {
	Location     string
	Inc          int
	EvidenceAt   int
	RequestLimit int // request_limit_ns: the longest request, which H adds to the signature age
}

// deadline is the scope's acknowledgement bound: a listing later than
// evidence_at + H (claim rev 6.23 §2, §6.2a).
func (s *parkScope) deadline() int { return s.EvidenceAt + sigAgeH + s.RequestLimit }

// admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it
// produced, the box and generation it admitted, the stamp, the mode (warm
// or cold), whether the writer has opened, and the predecessor it observed.
type admissionRecord struct {
	Session, Box int
	Gen          string
	Stamp        int
	Mode         string // warm or cold (claim rev 6.9)
	Predecessor  pred
	Lost         *writesLost // a cold admission whose observed session had no certificate (claim rev 6.9, R9-2)
	// Coverage is the admission's coverage of its predecessor's writes
	// (claim rev 6.12): "" (uncovered: writes_lost unless certified),
	// "sealed" (a from_db seal), "clean-return" (a clean rollback with
	// src_covered). The entry always names it
	Coverage string
	Covered  bool // this cold admission's predecessor has had its park-generation chore queued by a PublishGeneration (claim rev 6.12)
	// Region is where this writer's generation keeps its objects;
	// PredRegion where the predecessor's are, -1 when it holds none
	// anywhere (claim rev 6.14 §6.4a item 1: region, predecessor_region)
	Region     int
	PredRegion int
	// AdditionalWritesLost (claim rev 6.22 item 2, additional_writes_lost):
	// behind a declared-lost target, every other session the target was
	// admitted into since the cut, certified or not (no return lane carries
	// any of their writes, seed 33373 / 100,000), and the source's cut
	// session when src_covered is false (the seal in the lost region was
	// the one holder of its writes beyond the replica, seeds 16395 and
	// 27191 / 30,000; rev 7.11's LostSrc). With Lost, unique by (box,
	// session) (R14-2)
	AdditionalWritesLost []*writesLost
}

// pred is the predecessor an admission journals: the session, writer box,
// generation and stamp it observed.
type pred struct {
	Session, Box int
	Gen          string
	Stamp        int
}

// openState is an admitted writer between its AdmitWriter CAS and its
// process start (rev 7.10 §7.14): the generation and session it was
// admitted to, the database it restored, and the stage whose PUT it waits
// for: "first" (a fresh generation's full first upload), "marker"
// (generation.json), "anchor" (a warm restore above the level-0 maximum).
type openState struct {
	Gen, Want string
	Session   int
	Mode      string
	Prepared  bool
	Probe     bool
	Source    string // the generation the restore reads
	SourcePin int    // how: -1 the marker's generation (restoreCalc); 0 a generation the run walk selected, rooted at [1, 1] (R14-1)
	RemoteMax int    // the certificate's max_txid a warm restore must reach
	DB        *localDB
	stage     string // restore, app, first, marker, anchor, open
	req       *request
	blob      *blob // the first upload's or the anchor's bytes, captured once: a retry carries the same bytes (R10-7; seed 7574 / 30,000)
	pendAt    int   // the pending writes the captured blob covers; later acknowledgements stay pending
	startedAt int   // when the app stage first ran: a probe attempt's readiness window runs from here (rev 7.12 §7.7)
}

// probeTiming is what INV-19 reads: when a probe attempt's app stage first
// ran and when its app answered readiness (rev 7.13, R12-2)
type probeTiming struct {
	startedAt, readyAt int
}

// writesLost is claim rev 6.9's writes_lost record: the writer whose
// acknowledged, unuploaded writes a cold admission leaves behind, named by
// holder.writer_box, never inferred from op.exec (R9-2). The box alerts.
type writesLost struct {
	Box           int
	Gen           string
	Session       int
	RemoteMaxTXID int
}

type opState struct {
	Kind  string // serving, creating, deleting, parking, purging, moving, landing, reverting, restoring, pushing
	ID    string
	Phase string
	Exec  int // -1 none
	Parts []int
	// ParkSweep is intent.park_sweep (claim rev 6.15 §6.2a): a free host's
	// at-rest sweep runs as a holderless parking op, {kind: parking,
	// intent: {park_sweep: "v1"}}, with no exec and no holder, carrying
	// only scoped remote chores; its last acknowledgement frees the claim
	// again in the same CAS (FreeAfterPark)
	ParkSweep string

	// FenceBox is the journal's fence.<box> reference (claim rev 6.28,
	// moves rev 7.20 §7.10): the terminated source whose termination fence
	// converted a pre-flip move to relocating. Alerted: the operator was
	// told once that the relocation waits for a box in the region.
	FenceBox int
	Alerted  bool

	// intent
	Src, Tgt             int
	SrcRegion, TgtRegion int
	NewInc               int
	NewApp               string
	NewRegion            int
	NewSerial            int
	NewBox               int // the executor a create named once (region HA §5.2, H12): never substituted
	// region HA relocation (spec 1 §5.8; claim rev 6.30 §4 L1). The
	// journal entries below are what the claim's op.journal carries
	RelocReason  string        // drain or failover
	FenceAt      int           // fence.<box>.observed_at of the latest fence the operation cites; 0 none
	FailedAt     int           // when the target entered probe-failed
	Release      *releaseEntry // the release sequence's journal entry (§5.8): the source's in releasing, a failed target's in probe-failed
	Pin          *pinEntry     // the pinned recovery set
	Prepared     string        // P, the prepared generation this installation builds; "" before installing
	InstallStamp int           // the stamp of the CAS that handed op.exec to the current target (op.journal.install_stamp)
	Receipt      *receiptEntry // the executor's local install receipt (local_install)
	ProbingSince int
	Replacements int   // targets replaced in this operation; two, then stuck
	Excluded     []int // replaced targets, never named again for this host
	InstalledOn  []int // every box this operation handed op.exec for an installation: each owes a park-local at serving unless discharged
	Discharged   []int // fenced boxes whose park-local chores the fence CAS discharged (L3, H19)
	Stuck        string
	// 1b-next rev 16's journal additions
	ReleasingSince int      // releasing_since: the release deadline's start (ruling 14)
	Attempts       int      // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
	PreparedOpened string   // prepared_opened: journaled by the admission that opened P (rev 12 S1)
	PinFailover    bool     // (rev 6) the initial failover's starting, 1b-next's StartRelocation with a fence: set by startFailover and by a drain's source lost in starting, cleared by the PinFailover CAS once the target is named and every participant has acknowledged
	Resolved       bool     // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
	Observed       []int    // every fence.<box>.observed_at the operation consumed, kept through replacements (rev 4)
	Acks           []int    // exec_ack.<box>: the participants that acknowledged, durable (rev 4)
	Abandoned      []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27)
	// L18 joint round finding 2: the built completion protocol
	// (regionha_completion_test.go). ProbePassedAt is the probe's
	// journaled time (Probe.At, ruling 67's bound); ProbeStop the target's
	// journaled stop of the passed probe's session (ruling 49); Completed
	// the serving op's completed_relocation record (ruling 56), which the
	// completion pass marks discharged last (ruling 80)
	ProbePassedAt int
	ProbeStop     *probeStopEntry
	Completed     *completedEntry

	// journal
	ReportAt     int
	ReportOK     bool
	CutAt        int
	CutDeadline  int
	StopAt       int
	StopDigest   digest
	StopFiles    *filesDir
	SealDB       ref
	SealFiles    ref
	SealQuiet    int
	LandPhase    string
	Installed    digest
	ProbeTries   int
	ProbedAt     int
	RevPhase     string
	SrcPhase     string
	Dirty        bool
	DirtyKnown   bool
	ReturnDB     ref
	ReturnFiles  ref
	ReturnQuiet  int
	ReturnParked bool // the return lane's park-staging chore is owed (rev 7.10)
	// SrcCovered (rev 7.11): at the seal, the source's own replica of its
	// generation reached the stopped database's position, so a clean
	// rollback may restore the source from it; otherwise the seal holds
	// writes the replica does not, and the return carries the seal
	SrcCovered bool
	// CutSession (rev 7.12) is holder.session at the cut's stop: the
	// source's session whose writes src_covered speaks for; a clean return's
	// coverage applies to it and to the target's probe session only
	CutSession int
	// SealFromDB (rev 7.11): the seal was built from the stopped database
	// itself, every page of it, so it covers every write the predecessor
	// acknowledged; false when the disk was gone and the seal is the
	// remote as it stood, which stops at the remote's position. The
	// prepared generation's admission declares writes_lost in that case
	// (seed 34260 / 100,000). ReturnFromDB is the same for a dirty
	// return's seal of the target
	SealFromDB   bool
	ReturnFromDB bool
	LostBox      int
	LostAt       int
	RollbackID   string
	PushSnap     *blob // a push's installed snapshot (the final checkpoint plus the push's mark)
	BaseKey      string
	BaseTX       int
	RecVer       int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4)
	FlipGen      int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4)
	SrcStamp     int // the source installation's stamp before the flip, for the return to source (claim rev 6.5)
	// SrcGen is the source's generation at the cut (rev 7.10): a clean
	// rollback's return CAS names it again for the restore. Rev 7.11's
	// op.journal.writers moved to holder.admissions (claim rev 6.12)
	SrcGen       string
	Committed    bool
	Opened       bool
	ParkLocalNow bool
	PinVer       int // move.inputs: the bundle version pinned at admission
	Auto         bool
	ReqAt        int
	Repl         string
	Next         int
	FlipAt       int
	TgtStopAt    int
	Reason       string
	App          string
	// FencedAbsent: a purge fence placed where no claim existed (claim rev
	// 5.2 §5.3). Its release writes a free claim; the mutation of
	// claim-never-deleted deletes the object instead
	FencedAbsent bool
	// BaseVer is the version id of the generation's installed snapshot,
	// recorded by the install manifest and named by generation.json: the
	// immutable snapshot identity the restore starts from (rev 7.4 §5.1,
	// R3-1)
	BaseVer int
}

// releaseEntry is §5.8's release journal entry: the box, generation and
// session that gave the host up, its stopped database's final TXID (the
// listing shows it before pinning may cite it), and, until Task 4's files
// manifest, the files directory and wake state the box published. Flushed
// is false when the session's replicator was gone (an agent restart) and
// the entry names what the remote held: released coverage never applies
// to it, and the next admission declares the rest.
// releaseRecord is 1b-next Task 7's ReleasePositions record: the
// release a box computed once its writers stopped and its database and
// files flushed, bound to the stop (the operation, the phase and the
// writer session), durable before the producers close (rev 9).
type releaseRecord struct {
	Op, Phase string
	E         releaseEntry
	// Ctl is the flushing controller's identity: the agent process
	// (box.Epoch) that flushed and recorded (rev 11). Receipt is root's
	// durable stop receipt for this stop, persisted after the producers
	// drained (step 4), tracked apart from the recorded positions: only
	// the same controller may finish from the positions alone, and after a
	// restart the release needs the receipt too (1b-next Task 7 Release,
	// RecoveryReleaseDrain; Astra round 8)
	Ctl     int
	Receipt bool
}

type releaseEntry struct {
	Box, Session int
	Gen          string
	FinalTX      int
	ManifestSeq  int
	Flushed      bool
	Files        *filesDir
	Timers       []int
	At           int
}

// pinEntry is §5.8's pinned recovery set: the database position N the
// build restores to (exact versions in the real pin; the model's build
// never restores past N), the files manifest version (Task 4), and when
// the pin was taken (after a release's final_txid is visible, or after a
// fence's observed_at plus failoverPinDelay).
type pinEntry struct {
	Gen            string // the generation the pin reads (genselect over the admitted chain)
	TX             int
	ManKey         string
	ManVer, ManSeq int
	At             int
	ClaimVer       int // the claim version it was selected against (1b-next ruling 16: pin-<gen>.json)
	// Files and Timers are the files set the pin was taken with, until
	// Task 4's manifest: the release's, or a failover's stand-in
	Files  *filesDir
	Timers []int
	ManGen string // the generation whose manifest the files pin names (Task 4)
}

// receiptEntry is the local install receipt (§5.8 local_install): the
// box and the install_stamp of the CAS that handed it op.exec. A
// replacement executor never inherits its predecessor's.
// probeStopEntry is hostclaim.ProbeStop: the target's stop of the passed
// probe's session, with root's receipt (ruling 49).
type probeStopEntry struct {
	Box, Session int
}

// completedEntry is hostclaim.CompletedRelocation on the serving op: the
// relocation, the box and stopped probe session it completed with, and
// Discharged, the mark (MarkCompletedDischarged).
type completedEntry struct {
	Op           string
	Box, Session int
	Discharged   bool
}

type receiptEntry struct {
	Op         string
	Box, Stamp int
}

type digest struct {
	Writes string
	Files  string
	Timers string
	Valid  bool
}

type claim struct {
	Ver      int
	Holder   *holder
	Op       opState
	Regions  []int
	Boxes    []int
	Complete bool
	Obl      []obligation
	Lost     []int
	// Retired is retired_incarnations: anti-reuse only, capped at
	// retiredCap entries (claim rev 6 §2, §6.2a). The sweep does not read
	// it; it discovers locations from the namespace (R3-4).
	Retired  []int
	Quiet    [nRegions]int
	PurgeRes bool
	// Cancelled is cancelled_creates (claim rev 4 §5.1, J2-R2-7): creates
	// recovery cancelled, so a late record PUT can be removed. It survives free.
	Cancelled []cancelledCreate
	// readStamp is model bookkeeping on a box's read of the claim: the
	// installation stamp active on that box at the read, which a worker
	// carries with the claim it validated under (claim rev 6.5 §6.4)
	readStamp int
}

type cancelledCreate struct {
	Inc   int
	Until int
}

// liteHost is a second hostname of the same apps, modelled for the
// control plane only: create, app admission and purge (J2-R2-2).
type liteHost struct {
	Inc  int
	App  string
	Box  int    // the box its create named (region HA §5.2); control-plane only
	Kind string // "", "creating", "serving", "purging", "fenced"
	OpID string
	Rec  bool // its record is published
	At   int
	// FencedAbsent: the fence found no claim (epoch 0). Its release writes
	// free; the mutation of claim-never-deleted deletes the object, so the
	// epoch returns to 0 and a creator's If-None-Match: * passes again
	FencedAbsent bool
}

// admission is apps/<acct>/<app>/admission.json (claim rev 4 §5.1 step 0).
type admission struct {
	Closed bool
	Reg    map[string]regEntry // create id -> registration
}

type regEntry struct {
	Host  string
	Until int // a registration is a lease: a create claims before it ends (CC16)
}

type pendingRec struct {
	rec *record
	at  int
}

type record struct {
	Ver    int
	Inc    int
	App    string
	Region int
	MoveID string
	// MoveState is the record's move journal state for the four transitions
	// the moves spec makes record-first (§7.5, §7.8, §7.9): "landing" after
	// the flip, "committed", "rolling_back". The claim follows each.
	MoveState  string
	RollbackID string
	Reason     string
	// LastMove names the move whose close cleared MoveID: the close is record
	// first (moves rev 7.23 §7.5, Paul's ruling M4), so a record can say a
	// move is over while the claim still holds its op, until the release.
	LastMove string
}

// ---------- the world ----------

type ack struct {
	W       int
	Inc     int
	Box     int
	Session int    // the writer session that acknowledged it (rev 7.13, R12-1): a writes_lost record exempts the writes of the session it names, no other
	Gen     string // the generation that session wrote
	At      int
	Kind    string // "write" or "timer"
	Exempt  bool   // lost under a declared loss (M16) or past the last checkpoint of a lost disk
}

// intner is what the model draws from: the seed's *rand.Rand in the random
// sweep, a quiet source in a witness scenario (witness_test.go), so the
// witnesses never touch the seeds' streams.
type intner interface{ Intn(n int) int }

type world struct {
	perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2
	issued    int // files manifests issued, in order: INV-28's ground truth (blob.Base)
	// pinWatch is INV-30's memory: per region that could still serve, the
	// manifest its next install would pin, as the oracle saw it last step
	pinWatch map[int]pinWatch
	// noPinWatch turns INV-30 off: TestFilesWitnessesStuckWithoutINV30's
	// liveness runs only
	noPinWatch bool
	// oneBoxRegion: a witness's region kept at one box by its group in the
	// two-box shape (H5's minimum is per region)
	oneBoxRegion [nRegions]bool
	// L18 joint round findings 2 and 4 (regionha_completion_test.go):
	// haOff is CARLOS_REGION_HA off with claim mode on, where only the
	// completion pass runs (ruling 82); claimC1 and claimC11 are claim
	// asks C1 (a failed target's release obligation) and C11 (root
	// launches a later probe attempt after P's opening). Both are open
	// today, so the model runs the built fallbacks; a witness or test of
	// the post-C1 or post-C11 behaviour sets them
	haOff, claimC1, claimC11 bool
	t                        testingT
	seed                     int64
	rng                      intner
	// hold, when set, is a witness's hand on S3: a request it answers true
	// for is accepted and completes only when the witness says so
	// (witness_test.go). The random sweep never sets it.
	hold func(r *request) bool
	// alerts raised to the operator (writes_lost, a marker disagreement, a
	// failed host, an uncertified close): counted for the oracle that every
	// writes_lost record was alerted (R10-6)
	alerts        int
	lostAlert     int
	markerAlerted map[string]bool
	// startHook runs right after the app starts, before replication opens:
	// a witness's background worker acknowledging work (R10-1)
	startHook func(b *box) bool // true: the hook crashed the box
	// openYield (rev 5, Astra round 2 on claim §11's open boundaries): a
	// witness's yield after generation.json names the new generation and
	// before replication opens; true: the start returns there and resumes
	// at "open" on the next call. Nil outside the witnesses
	openYield func(b *box) bool
	// lastIssued is the request issue saw last, for a caller that needs
	// the request object behind a helper's return value (resumeOpen)
	lastIssued *request
	// stampBox records, for every installation stamp the claim issued, the
	// box whose installation it names (claim rev 6.5: holder.stamp always
	// names the installation op.exec should run). The oracle refuses an
	// activation of another box's stamp (INV-6, R6-4).
	stampBox map[int]int
	now      int
	ver      int
	verbose  bool

	claim      *claim // nil = absent
	rec        *record
	stores     map[string]bool
	cfgVer     map[string]int // each app's current config bundle version
	purgeRes   map[string]bool
	purgeStep  map[string]int // the reservation's durable phase (purge journal)
	admit      map[string]*admission
	h2         liteHost
	recPend    *pendingRec       // a record PUT whose response was lost
	lastRegion int               // where the host served when it was last deleted
	legacyIncs map[int]bool      // incarnations that were adopted legacy hosts
	purgeOp    map[string]string // the purge id, kept in the reservation (the purge journal)
	h2Epoch    int               // the second host claim's ETag, for its fence and release; 0 is absent
	floor      bool
	buckets    [nRegions]*bucket
	control    *bucket
	boxes      []*box
	pending    []*request
	acks       []ack
	writeInc   map[int]int             // which incarnation acknowledged each write
	txs        map[int]tx              // every write as a transaction (ltx_test.go)
	durable    map[string]map[int]bool // per generation prefix: writes a completed replica object holds
	genParent  map[string]string       // generation prefix -> the one it superseded
	nextW      int
	nextInc    int
	serial     int
	nextID     int
	delivered  map[int]bool
	doorReads  []*doorPlan
	execLease  map[int]execLease
	staging    [nRegions]stagingLease
	console    []*consolePlan
	fail       map[string]bool // which faults this seed exercises
	stats      map[string]int
	stalled    []*stalledSign
	ccache     *claim // the console's short-lived claim cache

	violations []string
	opsDone    int
	calm       bool
	trace      []string
}

type testingT interface {
	Fatalf(format string, args ...any)
	Logf(format string, args ...any)
}

func (w *world) logf(format string, args ...any) {
	if w.verbose {
		w.trace = append(w.trace, fmt.Sprintf("%5d ", w.now)+fmt.Sprintf(format, args...))
	}
}

func (w *world) violate(format string, args ...any) {
	msg := fmt.Sprintf("t=%d: ", w.now) + fmt.Sprintf(format, args...)
	if len(w.violations) >= 3 {
		return
	}
	w.violations = append(w.violations, msg)
	w.logf("VIOLATION %s", msg)
}

func (w *world) newID(prefix string) string {
	w.nextID++
	return fmt.Sprintf("%s%d", prefix, w.nextID)
}

func (w *world) newVer() int {
	w.ver++
	return w.ver
}

// nextGen is the gen the claim CAS in progress will carry: what a writer
// captures as its installation stamp (claim rev 6.5 §6.4).
func (w *world) nextGen() int {
	if w.claim == nil {
		return 1
	}
	return w.claim.Ver + 1
}

func (w *world) boxByID(id int) *box {
	for _, b := range w.boxes {
		if b.ID == id {
			return b
		}
	}
	return nil
}

// regionBox is the live (not destroyed) box in a region.
func (w *world) regionBox(r int) *box {
	for _, b := range w.boxes {
		if b.Region == r && !b.Destroyed {
			return b
		}
	}
	return nil
}

func contains(xs []int, x int) bool {
	for _, y := range xs {
		if y == x {
			return true
		}
	}
	return false
}

func addUniq(xs []int, x int) []int {
	if contains(xs, x) {
		return xs
	}
	return append(xs, x)
}

func intsKey(xs []int) string {
	c := append([]int(nil), xs...)
	sort.Ints(c)
	return fmt.Sprint(c)
}

func (c *claim) clone() *claim {
	if c == nil {
		return nil
	}
	n := *c
	if c.Holder != nil {
		h := *c.Holder
		n.Holder = &h
	}
	n.Op.Parts = append([]int(nil), c.Op.Parts...)
	n.Op.StopFiles = c.Op.StopFiles.clone()
	n.Op.Excluded = append([]int(nil), c.Op.Excluded...)
	n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)
	n.Op.Discharged = append([]int(nil), c.Op.Discharged...)
	n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...)
	n.Op.Acks = append([]int(nil), c.Op.Acks...)
	n.Op.Observed = append([]int(nil), c.Op.Observed...)
	if r := c.Op.Release; r != nil {
		cp := *r
		cp.Files = r.Files.clone()
		cp.Timers = append([]int(nil), r.Timers...)
		n.Op.Release = &cp
	}
	if p := c.Op.Pin; p != nil {
		cp := *p
		cp.Files = p.Files.clone()
		cp.Timers = append([]int(nil), p.Timers...)
		n.Op.Pin = &cp
	}
	if r := c.Op.Receipt; r != nil {
		cp := *r
		n.Op.Receipt = &cp
	}
	if c.Holder != nil {
		n.Holder.Admissions = append([]admissionRecord(nil), c.Holder.Admissions...)
		for i := range n.Holder.Admissions {
			if l := n.Holder.Admissions[i].Lost; l != nil {
				cp := *l
				n.Holder.Admissions[i].Lost = &cp
			}
		}
	}
	n.Regions = append([]int(nil), c.Regions...)
	n.Boxes = append([]int(nil), c.Boxes...)
	n.Obl = append([]obligation(nil), c.Obl...)
	n.Lost = append([]int(nil), c.Lost...)
	n.Retired = append([]int(nil), c.Retired...)
	n.Cancelled = append([]cancelledCreate(nil), c.Cancelled...)
	return &n
}

// ---------- bucket access with IAM ----------

// actor names: "box:N" or "console" or "operator".

func (w *world) iamCheck(actorBox int, r *request) bool {
	if actorBox < 0 { // console: control bucket only, plus GetObjectVersion on data (door)
		return false
	}
	b := w.boxByID(actorBox)
	if r.region == b.Region {
		if r.kind == rCopy && r.srcRegion != b.Region {
			return false // no Get on a sibling
		}
		return true
	}
	// sibling bucket: Put/Delete on moves/* only, and CopyObject INTO moves/*
	// from the box's own bucket.
	if !strings.HasPrefix(r.key, "moves/") {
		return false
	}
	switch r.kind {
	case rPut, rDelKey:
		return true
	case rCopy:
		return r.srcRegion == b.Region
	}
	return false // DeleteObjectVersion is not granted on a sibling
}

// issue sends a request. It returns the new version id when it completed
// immediately and the client saw the answer; 0 when the client timed out
// (the request may still complete later).
func (w *world) issue(actorBox int, r *request) int {
	r.at = w.now
	w.lastIssued = r
	if r.kind == rPut && r.b != nil && isDataKey(r.key) && (r.b.Min == 0 || r.b.Max == 0) {
		// INV-12 (R8-3): the pinned LTX encoder refuses a zero TXID, so no
		// such file can exist; a position-0 snapshot [1,0] or anchor [0,0]
		// is a builder bug, never an object
		w.violate("INV-12: box %d wrote an LTX file with a zero TXID, %s, which the pinned encoder refuses (R8-3)", actorBox, r.key)
	}
	if !w.iamCheck(actorBox, r) {
		w.violate("IAM: box %d may not %v %s in region %d", actorBox, r.kind, r.key, r.region)
		return 0
	}
	if w.hold != nil && w.hold(r) {
		r.doneAt, r.by = 1<<30, fmt.Sprintf("box:%d", actorBox)
		w.pending = append(w.pending, r)
		w.logf("box %d issued %v %s r%d (held by the witness)", actorBox, r.kind, r.key, r.region)
		return 0
	}
	if r.hold {
		// the biased schedule: accepted, completing at its worst moment or
		// long after everything else
		r.doneAt, r.by, r.beyond = w.now+40*horizonH, fmt.Sprintf("box:%d", actorBox), true
		w.pending = append(w.pending, r)
		w.logf("box %d issued %v %s r%d (held for its worst moment)", actorBox, r.kind, r.key, r.region)
		return 0
	}
	if w.rng.Intn(10) < 7 {
		return w.complete(r)
	}
	r.doneAt = w.now + 1 + w.rng.Intn(6)
	tail := 8
	if strings.HasPrefix(r.key, "moves/") {
		tail = 3 // staging rounds stall more often: the cross-region path is the slow one
	}
	if w.rng.Intn(tail) == 0 {
		r.doneAt = w.now + 1 + w.rng.Intn(horizonH) // the long tail: signed, cancelled, completed late
		if w.rng.Intn(4) == 0 {
			r.doneAt = w.now + horizonH // as late as the signature-age limit allows
		}
		if w.rng.Intn(beyondH) == 0 {
			// accepted before the signature limit, completed after it: S3
			// bounds acceptance, not completion (claim C3a, J2-R2-1)
			r.doneAt = w.now + horizonH + 1 + w.rng.Intn(10*horizonH)
			r.beyond = true
			if w.fail["recreate"] && !w.calm && w.rng.Intn(2) == 0 {
				// the biased schedule: no bound at all, so it can outlive a
				// delete and a recreate; it lands at its worst moment. Chaos
				// only: in the calm phase a chain of such holds, one per park
				// of a dead generation, can outlast the whole convergence
				// window (seed 20077 / 30,000), which says nothing about the
				// protocol
				r.doneAt = w.now + 40*horizonH
			}
		}
	}
	r.by = fmt.Sprintf("box:%d", actorBox)
	w.pending = append(w.pending, r)
	w.logf("box %d issued %v %s r%d (late until %d)", actorBox, r.kind, r.key, r.region, r.doneAt)
	return 0
}

func (w *world) complete(r *request) int {
	r.done = true
	bk := w.buckets[r.region]
	switch r.kind {
	case rPut:
		if r.ifSet {
			cur := 0
			if v := bk.current(r.key); v != nil {
				cur = v.ID
			}
			if cur != r.ifVer {
				return 0 // 412 Precondition Failed
			}
		}
		v := &version{ID: w.newVer(), B: r.b, Straggler: r.beyond}
		bk.objs[r.key] = append(bk.objs[r.key], v)
		w.markDurable(r.key, r.b)
		return v.ID
	case rDelVer:
		vs := bk.objs[r.key]
		for i, v := range vs {
			if v.ID == r.ver {
				bk.objs[r.key] = append(vs[:i:i], vs[i+1:]...)
				break
			}
		}
		return -1
	case rDelKey:
		v := &version{ID: w.newVer(), Marker: true}
		bk.objs[r.key] = append(bk.objs[r.key], v)
		return v.ID
	case rCopy:
		src := w.buckets[r.srcRegion].byID(r.srcKey, r.srcVer)
		if src == nil || src.Marker {
			return 0
		}
		v := &version{ID: w.newVer(), B: src.B, Straggler: r.beyond}
		bk.objs[r.key] = append(bk.objs[r.key], v)
		w.markDurable(r.key, src.B)
		return v.ID
	}
	return 0
}

// markDurable: a write is durable in a generation once a completed replica
// object of that generation holds it. The cold-restore checks (§14.2.3)
// require every write durable in the claim's generation or in any
// generation it superseded.
func (w *world) markDurable(key string, b *blob) {
	if b == nil || !isDataKey(key) {
		return
	}
	p := genPrefixOf(key)
	if w.durable[p] == nil {
		w.durable[p] = map[int]bool{}
	}
	for _, x := range b.TXs {
		w.durable[p][x] = true
	}
}

// isDurable: W is durable anywhere (the disk-loss fault's RPO line).
func (w *world) isDurable(x int) bool {
	for _, m := range w.durable {
		if m[x] {
			return true
		}
	}
	return false
}

// newGen records that the claim's generation moved from old to gen within
// loc, so the durability promise carries over.
func (w *world) newGen(loc, old, gen string) {
	if old != gen {
		w.genParent[dataKey(loc, gen, "")] = dataKey(loc, old, "")
	}
}

// worstMoment: the biased schedule completes a pending write of an earlier
// incarnation's replica data the moment another incarnation holds the host
// with an executor in that region, inside its own window or past H, which
// is the interleaving C3a exists for (a recreate while the previous
// incarnation's requests are still in flight).
func (w *world) worstMoment(r *request) bool {
	if r.hold && r.b != nil && r.b.Kind == "gen" {
		// a held marker publication lands once a newer marker is current
		cur := w.buckets[r.region].current(r.key)
		return cur != nil && cur.B.Gen != r.b.Gen
	}
	if !w.fail["recreate"] || r.kind != rPut || r.b == nil || r.b.Inc == 0 || !isDataKey(r.key) {
		return false
	}
	c := w.claim
	if c == nil || c.Holder == nil || c.Holder.Inc == r.b.Inc {
		return false
	}
	if c.Op.Kind == "creating" && c.Op.NewRegion == r.region {
		return w.rng.Intn(2) == 0
	}
	e := w.execBox(c)
	return e != nil && e.Region == r.region && w.rng.Intn(2) == 0
}

func (w *world) completeDue(force bool) {
	var keep []*request
	for _, r := range w.pending {
		if force || r.doneAt <= w.now || w.worstMoment(r) {
			w.complete(r)
			if r.beyond {
				w.stats["completed beyond H"]++
			}
			w.logf("late completion %v %s r%d (%s)", r.kind, r.key, r.region, r.by)
		} else {
			keep = append(keep, r)
		}
	}
	w.pending = keep
}