package engines

import (
	"fmt"
	"strings"
)

// Calls, identity, grants and arming (spec §5.2 the signed record; §5.3 the
// grant mirror; §5.4 the call path; §6.1 identity; §6.2 armed boxes; §6.4
// freshness).
//
// The console publishes the grant set as one signed record with a strictly
// increasing revision, its signing time and a 72-hour expiry, and re-signs it
// every two minutes and on every change; every edge mirrors it, keeps a
// durable revision floor, and treats a stale, expired or never-read table as
// empty. Stale is either no good read for ten minutes or a record signed more
// than ten minutes ago (ruling R5). A nested instance calls an engine through its engine socket, which
// is open only on an armed box; a host-app process calls through the door.
// The calling box proves the caller (the peer's cgroup, or a door key from a
// uid other than carlos), checks its own table and hops to the engine's home
// box with the caller signed into the hop's MAC. The engine box checks its
// own table again and dispatches to the engine hostname's own route only.
//
// The model leaves out the per-app cap, the transport limits and the deploy
// watch ticket (Plan 2 tests those directly).

// Time: one tick is 10 s.
const (
	pollTicks     = 3     // the mirror polls every 30 s
	staleTicks    = 60    // no good read, or a record signed, ten minutes ago: stale (R5)
	resignTicks   = 12    // the console re-signs every two minutes while it is up (R5)
	lifetimeTicks = 25920 // a record expires 72 hours after it is signed
)

// now is the model's clock: one tick per step, plus any fast-forward.
func (w *world) now() int { return w.step + w.skew }

// advance is time passing with no step: n ticks in which nothing polls (an
// outage, a console down for days).
func (w *world) advance(n int) {
	w.skew += n
	w.logf("%d ticks pass (now %d)", n, w.now())
}

// ---------- the console's record (spec §5.2) ----------

// record is one signed control/engines.json: its revision, its signed_at and
// expiry (in ticks), and its grants by account/app/engine.
type record struct {
	Rev, SignedAt, Expires int
	Grants                 map[string]bool
}

// mirror is an edge's grant mirror (§5.3): the record it holds, its revision
// floor and the tick of its last good read, and what it has persisted to its
// data directory (the record and the floor, written before either is used).
type mirror struct {
	Rec            *record
	Floor, ReadAt  int
	Persisted      *record
	PersistedFloor int
}

// engConsole is the console's side: its database (Grants, the authority),
// every record it has signed, the newest revision, and the object in the
// bucket. RevokedAt and RevokedRev are the oracle's: the tick and revision of
// the publish that stopped granting a key. BucketDown: the edges cannot read
// the bucket. Down: the console is down, so it neither re-signs nor takes a
// grant or revoke.
//
// Pinned is a bucket writer's replay: an older signed record it keeps in the
// bucket, overwriting each record the console publishes, until tick
// PinnedUntil.
type engConsole struct {
	Rev         int
	Records     map[int]*record
	Grants      map[string]bool
	RevokedAt   map[string]int
	RevokedRev  map[string]int
	Bucket      *record
	BucketDown  bool
	Down        bool
	Pinned      *record
	PinnedUntil int
}

// The engines the operator has named (carlos engines add): name to its
// hostname. eng's hostname is the engine group's minted row; site's is box
// 0's static row, whose path map sends /convert to eng's route (R4-2: the
// console cannot check a hostname, and path targets may cross apps).
const site = "site"

var engineHosts = map[string]string{eng: engHost, site: engSite}

// callerOf is the caller account/app calling engine.
func callerOf(app, engine string) caller {
	acct, a, _ := strings.Cut(app, "/")
	return caller{Account: acct, App: a, Engine: engine}
}

func (c caller) app() string { return c.Account + "/" + c.App }
func (c caller) key() string { return c.app() + "/" + c.Engine }

// initEngines is the starting world: the console's first record grants shop
// the engine eng, and every edge has read it.
func (w *world) initEngines() {
	w.console = engConsole{Records: map[int]*record{}, Grants: map[string]bool{"acct/shop/eng": true}, RevokedAt: map[string]int{}, RevokedRev: map[string]int{}}
	w.publish(1)
	for _, b := range w.boxes {
		w.mirrorTick(b)
	}
}

// publish is the console signing its grant set as revision rev, signed now
// and expiring 72 hours out, and writing it to the bucket (where a pinned
// replay overwrites it at once). A revision is strictly increasing; a re-sign
// with the same grants is a new revision.
func (w *world) publish(rev int) {
	c := &w.console
	if rev <= c.Rev {
		panic(fmt.Sprintf("publish: revision %d after %d", rev, c.Rev))
	}
	rec := &record{Rev: rev, SignedAt: w.now(), Expires: w.now() + lifetimeTicks, Grants: map[string]bool{}}
	for k, v := range c.Grants {
		if v {
			rec.Grants[k] = true
		}
	}
	if prev := c.Records[c.Rev]; prev != nil {
		for _, k := range sortedKeys(prev.Grants) {
			if !rec.Grants[k] {
				c.RevokedAt[k], c.RevokedRev[k] = w.now(), rev
			}
		}
	}
	for k := range rec.Grants {
		delete(c.RevokedAt, k)
		delete(c.RevokedRev, k)
	}
	c.Records[rev], c.Rev, c.Bucket = rec, rev, rec
	w.logf("console: publishes revision %d, signed at %d, expiring at %d, grants %v", rev, rec.SignedAt, rec.Expires, sortedKeys(rec.Grants))
	if c.Pinned != nil {
		c.Bucket = c.Pinned
		w.logf("bucket writer: overwrites it with revision %d", c.Pinned.Rev)
	}
}

// consoleGrant and consoleRevoke are carlos engines grant/revoke: the
// database changes and the console publishes the next revision. A console
// that is down takes neither (false).
func (w *world) consoleGrant(key string) bool {
	if w.console.Down {
		w.logf("console: down; carlos engines grant %s fails", key)
		return false
	}
	w.console.Grants[key] = true
	w.publish(w.console.Rev + 1)
	return true
}

func (w *world) consoleRevoke(key string) bool {
	if w.console.Down {
		w.logf("console: down; carlos engines revoke %s fails", key)
		return false
	}
	delete(w.console.Grants, key)
	w.publish(w.console.Rev + 1)
	return true
}

// replay is a bucket writer restoring an older signed record (validly signed,
// and unexpired unless 72 hours have passed) and keeping it in the bucket
// over everything the console publishes, until it stops (unpin).
func (w *world) replay(rev int) { w.replayUntil(rev, 1<<62) }

// replayUntil is replay for a writer who stops at tick until.
func (w *world) replayUntil(rev, until int) {
	rec := w.console.Records[rev]
	if rec == nil {
		panic(fmt.Sprintf("replay: no revision %d", rev))
	}
	w.console.Bucket, w.console.Pinned, w.console.PinnedUntil = rec, rec, until
	w.logf("bucket writer: replays revision %d (signed at %d; newest %d) into the bucket, until tick %d", rev, rec.SignedAt, w.console.Rev, until)
}

// unpin is the bucket writer stopping: the newest record is in the bucket
// again.
func (w *world) unpin() {
	c := &w.console
	c.Pinned, c.Bucket = nil, c.Records[c.Rev]
	w.logf("bucket writer: stops; the bucket holds revision %d again", c.Rev)
}

func (w *world) setBucketDown(down bool) {
	w.console.BucketDown = down
	w.logf("the bucket is unreachable = %v", down)
}

// ---------- the grant mirror (spec §5.3) ----------

// mirrorTick is one poll of b's mirror. It verifies the record's expiry and
// its signed_at (a record signed more than ten minutes ago is stale, like an
// expired one, grant-freshness-bound) and refuses a revision below its floor
// (an equal revision is the same signed bytes: the model's records are
// immutable per revision). A good read replaces the record, raises the floor,
// and persists both before either is used (floor-persisted).
func (w *world) mirrorTick(b *box) {
	m := &b.Mirror
	c := &w.console
	if c.BucketDown || c.Bucket == nil {
		return
	}
	rec, now := c.Bucket, w.now()
	if now >= rec.Expires {
		if m.Rec != rec {
			w.logf("box%d: mirror refuses revision %d: expired at %d", b.ID, rec.Rev, rec.Expires)
		}
		return
	}
	if now-rec.SignedAt >= staleTicks && on("grant-freshness-bound") {
		if m.Rec != rec {
			w.logf("box%d: mirror refuses revision %d: signed at %d, ten minutes ago or more", b.ID, rec.Rev, rec.SignedAt)
		}
		return
	}
	if rec.Rev < m.Floor {
		w.logf("box%d: mirror refuses revision %d: below the floor %d", b.ID, rec.Rev, m.Floor)
		return
	}
	if rec.Rev > m.Floor || m.Rec == nil {
		w.logf("box%d: mirror reads revision %d (floor %d -> %d)", b.ID, rec.Rev, m.Floor, rec.Rev)
	}
	m.Rec, m.ReadAt = rec, now
	if rec.Rev > m.Floor {
		m.Floor = rec.Rev
	}
	if rec.Rev > b.ReadRev {
		b.ReadRev = rec.Rev
	}
	if on("floor-persisted") {
		m.Persisted, m.PersistedFloor = m.Rec, m.Floor
	}
}

// restartEdge is b's edge restarting: it loads the persisted record and
// floor before any engine socket opens. The time of the last good read is
// persisted with the record, so a restart is not a good read.
func (w *world) restartEdge(b *box) {
	m := &b.Mirror
	m.Rec, m.Floor = m.Persisted, m.PersistedFloor
	rev := 0
	if m.Rec != nil {
		rev = m.Rec.Rev
	}
	w.logf("box%d: edge restarts: mirror loads revision %d, floor %d", b.ID, rev, m.Floor)
}

// rebuild is a new or rebuilt box: its edge's data directory is gone, so it
// has no floor and no record until its first read, and may admit any validly
// signed record a bucket writer replays, until ten minutes after its signing
// (§5.3). The oracle forgets what the box had read (ReadRev).
func (w *world) rebuild(b *box) {
	b.Mirror = mirror{}
	b.ReadRev = 0
	w.logf("box%d: rebuilt: the edge has no persisted floor", b.ID)
}

// tableGrants is b's grant table on key. Never read: empty. No good read for
// ten minutes, or expired: empty (stale-clears-grants). A record signed more
// than ten minutes ago: empty (grant-freshness-bound, R5).
func (w *world) tableGrants(b *box, key string) bool {
	m := b.Mirror
	if m.Rec == nil {
		return false
	}
	if on("stale-clears-grants") && (w.now()-m.ReadAt >= staleTicks || w.now() >= m.Rec.Expires) {
		return false
	}
	if on("grant-freshness-bound") && w.now()-m.Rec.SignedAt >= staleTicks {
		return false
	}
	return m.Rec.Grants[key]
}

// ---------- the call path (spec §5.4) ----------

// call is one engine call as its sender makes it. host is the instance
// whose engine socket the process connects to, or whose door key it
// presents; engine is the Host: header; forged an X-Carlos-Hop-Caller header
// the sender wrote, or nil.
type call struct {
	from    *box
	p       *proc
	viaDoor bool
	uid     string
	host    string
	engine  string
	path    string
	forged  *caller
}

// engineCall is process p on box from calling engine (its Host:) at path,
// through the engine socket of instance host, or through the door with
// host's door key under uid. It reports whether the call reached an engine
// process.
func (w *world) engineCall(from *box, p *proc, viaDoor bool, uid string, host, engine, path string) bool {
	return w.placeCall(call{from: from, p: p, viaDoor: viaDoor, uid: uid, host: host, engine: engine, path: path})
}

// unitBacked: the route runs as a unit-backed DynamicUser service. The
// model's engine route is (§8: arm succeeds with nested callers and a
// unit-backed engine); every other instance route is nested. Unit-backed
// routes are not callers (ruling R2): they have no engine socket.
func unitBacked(g string) bool { return g == eng }

// socketOpen: instance g on b has an engine socket: the box is armed and
// its listener manager has the sockets open, and g is a nested instance.
func (w *world) socketOpen(b *box, g string) bool {
	if !b.Armed || !b.Sockets || unitBacked(g) {
		return false
	}
	for _, x := range w.groups(b) {
		if x == g {
			return true
		}
	}
	return false
}

// realApp is the account/app whose code process p runs: planted code's app,
// else its group's route's, else (a tenant with no row in the model: a flat,
// foreign or worker tenant) acct/<group). nil is a public client: no app.
func (w *world) realApp(b *box, p *proc) string {
	switch {
	case p == nil:
		return ""
	case p.Code != "":
		return p.Code
	}
	if r := b.Rows[p.Group]; r != nil && r.App != "" {
		return r.App
	}
	return "acct/" + p.Group
}

func (w *world) placeCall(c call) bool {
	b := c.from
	how := "socket of " + c.host
	if c.viaDoor {
		how = "door (uid " + c.uid + ", key of " + c.host + ")"
	}
	who := "a public client"
	if c.p != nil {
		who = fmt.Sprintf("process %d (%s)", c.p.ID, c.p.Slice)
	}
	w.logf("box%d: %s calls Host: %s%s through the %s", b.ID, who, c.engine, c.path, how)
	if strings.Contains(c.engine, ".") {
		w.logf("box%d: Host: %s is no engine name (it has a dot): not an engine call", b.ID, c.engine)
		return false
	}
	r := b.Rows[c.host]
	if r == nil || r.Kind != "instance" || r.Platform {
		w.logf("box%d: no instance route %s", b.ID, c.host)
		return false
	}
	// who is calling
	if !c.viaDoor {
		if !w.socketOpen(b, c.host) {
			w.logf("box%d: %s has no engine socket (armed %v)", b.ID, c.host, b.Armed)
			return false
		}
		if on("cgroup-identity") && c.p.Slice != "inst:"+c.host {
			w.logf("box%d: engine socket of %s: peer cgroup %s is not the instance's slice; closed unread", b.ID, c.host, c.p.Slice)
			return false
		}
	} else if on("door-uid") && c.uid == "carlos" {
		w.logf("box%d: door: an engine call from uid carlos: 404 engine not granted", b.ID)
		return false
	}
	mark := callerOf(r.App, c.engine)
	// the listener strips every X-Carlos-* header the sender wrote
	if c.forged != nil && on("hop-caller-signed") {
		w.logf("box%d: X-Carlos-Hop-Caller %s from the sender deleted", b.ID, c.forged.key())
		c.forged = nil
	}
	if !w.tableGrants(b, mark.key()) {
		w.logf("box%d: %s not in the grant table: 404 engine not granted", b.ID, mark.key())
		return false
	}
	hostname := engineHosts[c.engine]
	home := w.homeOf(hostname)
	if home == nil {
		w.logf("box%d: %s homed nowhere: 502 engine unreachable", b.ID, hostname)
		return false
	}
	seen := mark
	if home != b {
		w.logf("box%d: hop to box%d, caller %s signed into the MAC", b.ID, home.ID, mark.key())
		if c.forged != nil {
			w.logf("box%d: the hop also carries the sender's X-Carlos-Hop-Caller %s; the engine box takes it", home.ID, c.forged.key())
			seen = *c.forged
		}
	}
	return w.engineAdmit(home, b, seen, hostname, c.path, c.host, w.realApp(b, c.p), c.p)
}

// clientHop is a public client sending b's edge a request for hostname that
// carries X-Carlos-Hop-Caller with no hop MAC. Only a verified hop's caller
// is a caller (hop-caller-signed): the header is deleted and the request is
// a public request like any other.
func (w *world) clientHop(b *box, hostname, path string, forged caller) bool {
	w.logf("box%d: a public client sends %s%s with X-Carlos-Hop-Caller %s", b.ID, hostname, path, forged.key())
	if on("hop-caller-signed") {
		w.logf("box%d: unverified X-Carlos-Hop-Caller deleted; a public request", b.ID)
		if r := w.admitPublic(b, hostname, path); r != nil {
			w.deliver(r)
		}
		return false
	}
	return w.engineAdmit(b, b, forged, hostname, path, "", "", nil)
}

// homeOf is the box whose registry has hostname (the edge's home map).
func (w *world) homeOf(hostname string) *box {
	for _, b := range w.boxes {
		if b.Rows[hostname] != nil {
			return b
		}
	}
	return nil
}

// exactRoute is the row an engine call to hostname resolves to on b: the
// hostname's own row, through an alias (the same route), never a path map
// (exact-route-engine). ok is false for an unknown host.
func (w *world) exactRoute(b *box, hostname string) (row, bool) {
	final, ok := b.EdgeRows[hostname]
	if ok && final.Alias != "" {
		final, ok = b.EdgeRows[final.Alias]
	}
	return final, ok
}

// engineAdmit is the engine box (home) deciding an engine-marked request for
// hostname: the route must be internal, the engine box's own table must name
// the hostname for the mark's engine and grant it to the mark's app
// (engine-box-recheck), and the route must be the hostname's own
// (exact-route-engine). Then the activator's dispatch, which may wake the
// engine. via is the instance whose engine socket or door key the call came
// through ("" for a client's hop); real is the calling process's real app;
// p the process.
func (w *world) engineAdmit(home, from *box, mark caller, hostname, path, via, real string, p *proc) bool {
	final, ok := w.exactRoute(home, hostname)
	if !ok {
		w.logf("box%d: engine call to %s: unknown host", home.ID, hostname)
		return false
	}
	if !on("exact-route-engine") {
		if to, ok := final.PathTo[path]; ok {
			if t, ok := home.EdgeRows[to]; ok {
				w.logf("box%d: engine call to %s%s follows the path map to %s", home.ID, hostname, path, to)
				final = t
			}
		}
	}
	if home.Serving[final.Host] != markInternal {
		w.logf("box%d: engine call to %s: %s is not internal (%v): the internal refusal", home.ID, hostname, final.Host, home.Serving[final.Host])
		return false
	}
	if on("engine-box-recheck") {
		if engineHosts[mark.Engine] != hostname || !w.tableGrants(home, mark.key()) {
			w.logf("box%d: engine box: %s not granted for %s: the internal refusal", home.ID, mark.key(), hostname)
			return false
		}
	}
	g := truthGroup(home, final.Host)
	q := w.newest(home, g)
	if q == nil {
		w.wake(home, g, "recovery", nil)
		q = w.newest(home, g)
	}
	if q == nil {
		w.logf("box%d: engine call: %s has no process; the wake failed", home.ID, g)
		return false
	}
	w.logf("box%d: engine call reaches process %d (%s v%d); the access log records caller %s", home.ID, q.ID, q.Group, q.Ver, mark.app())
	w.events["engine-call-reached"]++
	w.checkCall(home, from, mark, via, real, p, q)
	return true
}

// ---------- armed boxes (spec §6.2) ----------

// unisolatedKinds are the launch paths that run tenant code outside an
// instance slice: a flat instance, a foreign one, and an app's worker.
var unisolatedKinds = []string{"flat", "foreign", "worker"}

// arm is `carlos engines arm`: refused unless every exec-backed instance
// route is nested (unit-backed routes are judged by backing and admitted),
// no route spawns workers, and every carlos-exec@ cgroup is empty
// (arm-checks-box). Then the box records the armed state and the edge opens
// the engine sockets.
func (w *world) arm(b *box) bool {
	if b.Armed {
		return true
	}
	if on("arm-checks-box") {
		var why []string
		for _, k := range sortedKeys(b.Unisolated) {
			why = append(why, "a "+k+" route")
		}
		for _, p := range b.Procs {
			if p.Unisolated {
				why = append(why, fmt.Sprintf("process %d in %s", p.ID, p.Slice))
			}
		}
		if len(why) > 0 {
			w.logf("box%d: carlos engines arm: refused: %s", b.ID, strings.Join(why, ", "))
			return false
		}
	}
	b.Armed = true
	b.Sockets = true
	w.logf("box%d: armed; engine sockets open (arming vouches for the present, not the past)", b.ID)
	return true
}

// disarm is `carlos engines disarm`: it closes every engine socket first,
// then clears the state; launches follow.
func (w *world) disarm(b *box) {
	if !b.Armed {
		return
	}
	b.Sockets = false
	b.Armed = false
	w.logf("box%d: disarmed: engine sockets closed, then the state cleared", b.ID)
}

// launchUnisolated starts tenant code outside an instance slice: kind flat
// or foreign (an instance of that layout, through the exec-child path) or
// worker (an app's worker in carlos-exec@). While armed it is refused before
// any process starts (armed-refuses-unisolated). The model's unisolated
// tenants are one route per kind, acct/<kind>.
func (w *world) launchUnisolated(b *box, kind string) bool {
	if b.Armed && on("armed-refuses-unisolated") {
		w.logf("box%d: %s launch refused: the box is armed (carlos engines disarm to run it)", b.ID, kind)
		return false
	}
	b.Unisolated[kind] = true
	w.nextID++
	p := &proc{ID: w.nextID, Group: kind, Slice: "exec:" + kind, Unisolated: true}
	b.Procs = append(b.Procs, p)
	w.logf("box%d: %s tenant started as process %d in %s", b.ID, kind, p.ID, p.Slice)
	return true
}

// moveToNested is the operator moving the kind route off the box's
// unisolated layouts (or its workers into instance slices): its processes
// stop and the route no longer blocks arming.
func (w *world) moveToNested(b *box, kind string) {
	w.stopGroup(b, kind)
	delete(b.Unisolated, kind)
	w.logf("box%d: the %s route moved to nested; its processes stopped", b.ID, kind)
}

// tamper is unisolated process by writing nested group g's instance
// directory (an environment file and an LD_PRELOAD): g's next start runs by's
// code inside g's slice. Only an unisolated process can, which an armed box
// never runs; the walk generates it only under flatEraTamper.
func (w *world) tamper(b *box, by *proc, g string) {
	b.Tampered[g] = w.realApp(b, by)
	w.logf("box%d: process %d (%s) plants code in %s's instance directory", b.ID, by.ID, by.Slice, g)
}

// applyTamper is a nested start picking up planted code (launch calls it).
func (w *world) applyTamper(b *box, p *proc) {
	if app := b.Tampered[p.Group]; app != "" {
		p.Code = app
		w.logf("box%d: process %d of %s runs code %s planted", b.ID, p.ID, p.Group, app)
	}
}

// ---------- the random walk ----------

// walkApps are the apps the console may grant: the model's routes' apps and
// the unisolated tenants'.
var walkApps = []string{"acct/eng", "acct/flat", "acct/shop", "acct/tcp"}

func (w *world) pickEngine() string { return []string{eng, site}[w.rng.Intn(2)] }
func (w *world) pickPath() string   { return []string{"/", engSitePath}[w.rng.Intn(2)] }
func (w *world) pickKey() string {
	return walkApps[w.rng.Intn(len(walkApps))] + "/" + w.pickEngine()
}

// maybeForged is, one call in four, an X-Carlos-Hop-Caller the sender wrote.
func (w *world) maybeForged() *caller {
	if w.rng.Intn(4) != 0 {
		return nil
	}
	c := callerOf(walkApps[w.rng.Intn(len(walkApps))], w.pickEngine())
	return &c
}

// pickReplay is the revision a bucket writer replays: one that grants a key
// the console has since revoked, if any (the damaging choice: half the time
// the newest such, signed most recently, else any), else any older one.
func (w *world) pickReplay() int {
	newest := w.console.Records[w.console.Rev]
	var damaging []int
	for r := 1; r < w.console.Rev; r++ {
		for k := range w.console.Records[r].Grants {
			if !newest.Grants[k] {
				damaging = append(damaging, r)
				break
			}
		}
	}
	if len(damaging) > 0 {
		if w.rng.Intn(2) == 0 {
			return damaging[len(damaging)-1]
		}
		return damaging[w.rng.Intn(len(damaging))]
	}
	return 1 + w.rng.Intn(w.console.Rev-1)
}

// walkReplay is the walk's bucket writer: it replays an older record and
// keeps it in place for up to twenty minutes.
func (w *world) walkReplay() bool {
	if w.console.Rev < 2 {
		return false
	}
	w.replayUntil(w.pickReplay(), w.now()+1+w.rng.Intn(2*staleTicks))
	return true
}

// callers are the nested instance groups on b with an engine socket open.
func (w *world) callers(b *box) []string {
	var out []string
	for _, g := range w.groups(b) {
		if w.socketOpen(b, g) {
			out = append(out, g)
		}
	}
	return out
}

func init() {
	stepHooks = append(stepHooks,
		// a bucket writer whose time is up stops; the console, while up,
		// re-signs every two minutes (R5)
		func(w *world) {
			c := &w.console
			if c.Pinned != nil && w.now() >= c.PinnedUntil {
				w.unpin()
			}
			if !c.Down && w.now()-c.Records[c.Rev].SignedAt >= resignTicks {
				w.publish(c.Rev + 1)
			}
		},
		// the mirror polls every 30 s, whatever the walk does
		func(w *world) {
			if w.now()%pollTicks == 0 {
				for _, b := range w.boxes {
					w.mirrorTick(b)
				}
			}
		})
	actions = append(actions,
		action{name: "engine-call", weight: 4, run: func(w *world) bool {
			b := w.pickBox()
			gs := w.callers(b)
			if len(gs) == 0 || len(b.Procs) == 0 {
				return false
			}
			host := gs[w.rng.Intn(len(gs))]
			// usually the instance's own process; one call in three, any
			// process on the box connects to the socket (mode 0666)
			p := w.newest(b, host)
			if p == nil || w.rng.Intn(3) == 0 {
				p = b.Procs[w.rng.Intn(len(b.Procs))]
			}
			c := call{from: b, p: p, uid: "carlos", host: host, engine: w.pickEngine(), path: w.pickPath()}
			c.forged = w.maybeForged()
			w.placeCall(c)
			return true
		}},
		action{name: "door-call", weight: 1, run: func(w *world) bool {
			b := w.pickBox()
			gs := w.groups(b)
			if len(gs) == 0 {
				return false
			}
			host := gs[w.rng.Intn(len(gs))]
			c := call{from: b, viaDoor: true, host: host, engine: w.pickEngine(), path: w.pickPath()}
			if len(b.Procs) > 0 && w.rng.Intn(2) == 0 {
				// any process running as carlos presents host's door key
				// (every flat tenant can read every other's config)
				c.p, c.uid = b.Procs[w.rng.Intn(len(b.Procs))], "carlos"
			} else {
				// an enrolled host-app user: its own app's key, its own uid
				c.p, c.uid = &proc{Group: host, Slice: "user:u-" + host}, "u-"+host
			}
			c.forged = w.maybeForged()
			w.placeCall(c)
			return true
		}},
		action{name: "client-hop", weight: 1, run: func(w *world) bool {
			hosts := []string{engHost, engSite}
			c := callerOf(walkApps[w.rng.Intn(len(walkApps))], w.pickEngine())
			w.clientHop(w.pickBox(), hosts[w.rng.Intn(2)], w.pickPath(), c)
			return true
		}},
		action{name: "console-grant", weight: 1, run: func(w *world) bool { return w.consoleGrant(w.pickKey()) }},
		action{name: "console-revoke", weight: 1, run: func(w *world) bool {
			keys := sortedKeys(w.console.Grants)
			return len(keys) > 0 && w.consoleRevoke(keys[w.rng.Intn(len(keys))])
		}},
		action{name: "console-resign", weight: 1, run: func(w *world) bool {
			if w.console.Down {
				return false
			}
			w.publish(w.console.Rev + 1)
			return true
		}},
		action{name: "console-down", weight: 1, run: func(w *world) bool {
			w.console.Down = !w.console.Down && !w.calm()
			w.logf("console: down = %v", w.console.Down)
			return true
		}},
		action{name: "bucket-down", weight: 1, run: func(w *world) bool {
			w.setBucketDown(!w.console.BucketDown && !w.calm())
			return true
		}},
		action{name: "fast-forward", weight: 1, run: func(w *world) bool {
			if w.calm() {
				return false
			}
			if w.rng.Intn(8) == 0 {
				w.console.Down = true
				w.logf("console: down = true")
				w.advance(lifetimeTicks + staleTicks) // the console is down for three days
				return true
			}
			w.advance(staleTicks) // ten minutes with no poll
			return true
		}},
		// any older signed record, at any time: the freshness bound, not the
		// walk, limits what a replay can do (R5)
		action{name: "replay", weight: 1, run: func(w *world) bool {
			return w.walkReplay()
		}},
		action{name: "restart-edge", weight: 2, run: func(w *world) bool {
			switch w.rng.Intn(3) {
			case 0: // a release roll restarts every edge
				for _, b := range w.boxes {
					w.restartEdge(b)
				}
			case 1:
				w.restartEdge(w.pickBox())
			default:
				// a rebuilt box, the engine's home included; a bucket writer
				// may replay at once
				w.rebuild(w.pickBox())
				if w.rng.Intn(2) == 0 {
					w.walkReplay()
				}
			}
			return true
		}},
		action{name: "arm", weight: 2, run: func(w *world) bool {
			b := w.pickBox()
			if b.Armed {
				return false
			}
			w.arm(b)
			return true
		}},
		action{name: "disarm", weight: 1, run: func(w *world) bool {
			b := w.pickBox()
			if !b.Armed {
				return false
			}
			w.disarm(b)
			return true
		}},
		action{name: "launch-unisolated", weight: 1, run: func(w *world) bool {
			b := w.pickBox()
			kind := unisolatedKinds[w.rng.Intn(len(unisolatedKinds))]
			if !w.launchUnisolated(b, kind) || !w.flatEraTamper || b.Armed {
				return true
			}
			var gs []string
			for _, g := range w.groups(b) {
				if !unitBacked(g) {
					gs = append(gs, g)
				}
			}
			if len(gs) > 0 {
				w.tamper(b, w.newest(b, kind), gs[w.rng.Intn(len(gs))])
			}
			return true
		}},
		action{name: "unisolated-exit", weight: 1, run: func(w *world) bool {
			b := w.pickBox()
			var ps []*proc
			for _, p := range b.Procs {
				if p.Unisolated {
					ps = append(ps, p)
				}
			}
			if len(ps) == 0 {
				return false
			}
			p := ps[w.rng.Intn(len(ps))]
			for i, x := range b.Procs {
				if x == p {
					b.Procs = append(b.Procs[:i], b.Procs[i+1:]...)
					break
				}
			}
			w.logf("box%d: process %d (%s) exited", b.ID, p.ID, p.Slice)
			return true
		}},
		action{name: "move-to-nested", weight: 1, run: func(w *world) bool {
			b := w.pickBox()
			ks := sortedKeys(b.Unisolated)
			if len(ks) == 0 {
				return false
			}
			w.moveToNested(b, ks[w.rng.Intn(len(ks))])
			return true
		}},
	)
}

// mirrorsState is a one-line summary of the console and every mirror, for a
// failing witness.
func (w *world) mirrorsState() string {
	out := []string{fmt.Sprintf("console{rev %d bucket %d bucketDown %v down %v pinned %v now %d}", w.console.Rev, w.console.Bucket.Rev, w.console.BucketDown, w.console.Down, w.console.Pinned != nil, w.now())}
	for _, b := range w.boxes {
		m := b.Mirror
		rev := 0
		if m.Rec != nil {
			rev = m.Rec.Rev
		}
		out = append(out, fmt.Sprintf("box%d{rec %d floor %d readAt %d persisted %d readRev %d armed %v sockets %v}", b.ID, rev, m.Floor, m.ReadAt, m.PersistedFloor, b.ReadRev, b.Armed, b.Sockets))
	}
	return strings.Join(out, " ")
}