sim

type AbuseFamily int

type AbuseOutcome struct {
	FailureMsg string // populated when GotFailure
	Family     AbuseFamily
	GotFailure bool // server replied with a typed FAILURE
	GotClose   bool // server closed the connection cleanly (or it became unreadable)
}

type Actor interface {
	// Name returns a stable identifier for the actor (used in reports).
	Name() string
	// NextOp returns the next operation to execute, drawing all randomness from
	// seed and reading current contents from oracle.
	NextOp(seed *Seed, oracle *GraphOracle) Op
}

type BoltAbuser struct{}

type BoltAuthArm struct {
	// Name identifies the arm in a violation message.
	Name string
	// WantCode is the failure code a REFUSE arm must be told. It is empty for an
	// ADMIT arm.
	WantCode string
	// GotCode is the failure code actually received ("" when none was).
	GotCode string
	// Detail carries any harness-level note (e.g. the connection closed before a
	// reply, which is an acceptable refusal shape for a terminated session).
	Detail string
	// GotMessage is the FAILURE's message text, and WantStateInMessage the session
	// state the refusal must name.
	//
	// They exist because the authentication gate and the state-machine gate return
	// the SAME code — failTransition's Neo.ClientError.Request.Invalid — so a code
	// match cannot tell which one refused. That matters: if LOGOFF's target state
	// regressed (state.go's TX_READY/READY cases), commit-after-logoff would be
	// refused by the STATE check one line above the auth check, the arm would still
	// see Request.Invalid, and the CWE-306 gate would be untested while the
	// scenario stayed green. failTransition reports the ORIGIN state in its
	// message, which is exactly the discriminator: a refusal by the auth gate names
	// the LEGAL state the session was in (READY / TX_READY), a refusal by the state
	// gate names FAILED or the wrong state. An empty WantStateInMessage waives the
	// check for arms whose refusal is not a failTransition (a credential rejection).
	GotMessage         string
	WantStateInMessage string
	// FramesBefore/FramesAfter bracket the arm with [wal.Stats.Frames].
	FramesBefore, FramesAfter uint64
	// BytesBefore/BytesAfter bracket the arm with [wal.Stats.Bytes].
	BytesBefore, BytesAfter uint64
	// Admit records the arm's INTENT: true when the server is expected to accept
	// the operation and append to the WAL, false when it must refuse it and
	// append nothing.
	Admit bool
	// Accepted records what actually happened: the server answered SUCCESS to the
	// arm's decisive message.
	Accepted bool
}

type BoltAuthEvidence struct {
	// Arms are the probes in the order they ran.
	Arms []BoltAuthArm
	// GhostNodes is how many nodes carrying [abuseGhostLabel] exist at the end:
	// the count of writes that a de-authorised or unauthenticated session managed
	// to apply. It must be zero.
	GhostNodes int
	// HonestNodes is how many nodes carrying [authHonestLabel] exist at the end:
	// the writes the properly authenticated arms committed. It must equal the
	// number of ADMIT arms, which is what proves the harness could write at all.
	HonestNodes int
	// RecoveredGhosts / RecoveredHonest are the same two censuses taken after a
	// crash and a real WAL replay, so a frame that was appended but not yet
	// visible in the live engine cannot hide from the oracle.
	RecoveredGhosts int
	RecoveredHonest int
	// Seed is the seed the run was built from.
	Seed uint64
}

type BoltBeginExtrasEvidence struct {
	// Bookmarks are the causal-read arms, in the order they ran (a seed-drawn
	// permutation).
	Bookmarks []BoltBookmarkArm
	// Timeouts, Modes and DBs are the other arm families, likewise in run order.
	Timeouts []BoltTimeoutArm
	Modes    []BoltModeArm
	DBs      []BoltDBArm
	// Route and Metadata are single observations rather than families.
	Route    BoltRouteObs
	Metadata BoltMetadataObs
	// CommittedNodes is how many nodes the writer committed under
	// [beginCausalLabel]: the seed-drawn figure every causal read must observe. It is
	// the harness's own count, never read back from the engine, so it is the
	// independent side of the causality comparison.
	CommittedNodes int
	// IssuedBookmarks are the bookmarks the writer's successive COMMITs returned, in
	// order. Their literal text is NOT reachable from the seed (see the file header),
	// so clauses are written over relations between them, and the rendering shows
	// them positionally.
	IssuedBookmarks []string
	// AutocommitBookmarkFresh is the `bookmark` in the terminal PULL SUCCESS of an
	// autocommit WRITE on a connection that has never committed an explicit
	// transaction. Measured EMPTY.
	AutocommitBookmarkFresh string
	// AutocommitBookmarkAfterCommit is the same field on a connection that HAS, and
	// AutocommitAfterCommitExpected is the bookmark that connection's COMMIT had
	// returned. The clause is that the two are EQUAL: the autocommit statement was
	// handed the earlier transaction's token rather than one minted for itself.
	AutocommitBookmarkAfterCommit string
	AutocommitAfterCommitExpected string
	// AutocommitStatsSeen records that the autocommit write's own terminal SUCCESS
	// reported it as an update, so the empty bookmark above cannot be explained by
	// the statement having written nothing.
	AutocommitStatsSeen bool
	// Seed is the seed the run was built from.
	Seed uint64
}

type BoltBookmarkArm struct {
	// Name identifies the arm in a violation message and in the rendering.
	Name string
	// SentToken renders the single element the arm put in the `bookmarks` list, as
	// the arm built it. It is "<issued>" for the writer's own bookmark — never the
	// literal text, which is not reachable from the seed — and the verbatim constant
	// for a fabricated one. Empty means the key was omitted entirely.
	SentToken string
	// SentKey records whether the `bookmarks` key was present at all, so an arm that
	// omitted it is distinguishable from one that sent an empty list.
	SentKey bool
	// ServerSawTokens is how many tokens [server.ExtractBookmarks] would keep from
	// what the arm sent, computed by the HARNESS from its own list rather than read
	// back from the server (the server reports nothing). It is 0 for the wrong-type
	// arm, which is the point of that arm.
	ServerSawTokens int
	// Accepted is true when BEGIN was answered SUCCESS.
	Accepted bool
	// GotCode / GotMessage are the FAILURE's code and message, empty when none came.
	GotCode, GotMessage string
	// Observed is how many nodes carrying [beginCausalLabel] the arm's causal read
	// returned. It is compared ACROSS arms rather than against a literal, because
	// what the pin is about is that the token changed nothing.
	Observed int
	// ReadFailed carries a harness-level note when the causal read could not be
	// completed, so a broken read is never silently indistinguishable from a read
	// that returned zero.
	ReadFailed string
	// BeginElapsed is how long the BEGIN took in REAL time. It is the instrument for
	// "an unknown bookmark is not WAITED on", and it is deliberately absent from the
	// rendering: it is scheduling-dependent (rmp #2483's lesson) and belongs in a
	// clause, not in a byte-identity comparison.
	BeginElapsed time.Duration
}

type BoltCertRotationEvidence struct {
	// Steps are the rotation attempts in the order they ran.
	Steps []CertRotationStep
	// InitialLoadTornErr is the error [server.NewCertReloader] returned when
	// constructed over a TORN key, rendered. The initial load is documented as
	// mandatory, so this must be non-empty: a reloader that starts on unparseable
	// material would put a server into service with no certificate at all.
	InitialLoadTornErr string
	// WatchErrors are the errors the reloader's onError callback delivered while a
	// [server.Watch] goroutine polled a BROKEN pair.
	//
	// onError is the only operator-visible signal that a BACKGROUND rotation
	// failed, and before this scenario nothing in the module asserted it: deleting
	// the callback from Watch would have broken no test. It is the same defect
	// class as the Options.Logger bypass this sprint fixed — a security-relevant
	// event with no reachable destination — so the signal is now evidence.
	WatchErrors []string
	// UnloadedGetErr is the error a zero-value CertReloader's GetCertificate
	// returned, rendered. It must be non-empty rather than a nil certificate,
	// which the TLS stack would dereference.
	UnloadedGetErr string
	// Seed is the seed the run was built from.
	Seed uint64
}

type BoltDBArm struct {
	// Name identifies the arm; SentDB is the name sent, SentKey whether it was
	// present.
	Name    string
	SentDB  string
	SentKey bool
	// ReportedDB is the `db` field of the terminal PULL SUCCESS — the one a driver
	// turns into ResultSummary.Database().Name() (rmp #2172).
	ReportedDB string
	// ReportedOnRun is the `db` field of the RUN SUCCESS, which carries it too
	// (bolt/server/session.go handleRun). Recorded so the two are compared rather
	// than one assumed to follow the other.
	ReportedOnRun string
	// CommitMetaKeys is every key the COMMIT SUCCESS carried, sorted. It is here to
	// pin what COMMIT does NOT carry: `db` is absent from it, so a driver reading the
	// database name off a commit reply gets nothing.
	CommitMetaKeys []string
}

type BoltDecodeEvidence struct {
	// Census counts are read over the wire (live) and straight off a store reopened
	// through real recovery. Keyed by label; ids are never recorded, because a
	// created node's hidden key is minted from a process-global counter.
	LiveCensus      map[string]int
	RecoveredCensus map[string]int
	// ControlCensus is the same census on the CONTROL server's own engine, where
	// the bytes the pressured pool refused were served. Two engines, one payload:
	// the count differing between them IS the arm's claim.
	ControlCensus map[string]int
	// AbuserReplies is the swarm's reply census: code (or "SUCCESS") to count. It
	// is an invariant SUMMARY — which code, how many — and never says which
	// connection drew what, because that is the scheduler's business.
	AbuserReplies map[string]int
	// TransportErrors names every abuser exchange that failed at the transport
	// rather than drawing a Bolt reply. A reassembly-layer budget breach tears the
	// connection down (see the floor arithmetic on [boltDecodeSwarmAbusers]), so a
	// non-empty list here is the honest report of the swarm having been sized wrong
	// — not a silent pass.
	TransportErrors []string
	// Window is the boundary scan, in ascending element count.
	Window []BoltDecodeProbe
	// Arms are the named deterministic arms, in the order they were driven.
	Arms []BoltDecodeExchange
	// Honest are the swarm's honest exchanges, in order.
	Honest []BoltDecodeHonest
	// Seed is the run's seed.
	Seed uint64
	// Budget is the pressured (or swarm) server's ceiling in bytes.
	Budget int64
	// ControlBudget is the control server's ceiling, 0 on the swarm arm.
	ControlBudget int64
	// ModelBoundary is the largest element count the harness's model says the pool
	// admits. MeasuredBoundary is the largest the SERVER actually admitted inside
	// the scanned window, or -1 when the window did not span a transition.
	ModelBoundary    int
	MeasuredBoundary int
	// LeakProbeInitial and LeakProbeFinal are the same boundary-sized message sent
	// before any pressure and after all of it. The first CALIBRATES (a pristine
	// pool must admit it); the second is the no-leak oracle, since a pool that
	// failed to return any of what it lent would no longer admit it.
	LeakProbeInitial BoltDecodeProbe
	LeakProbeFinal   BoltDecodeProbe
	// AbuserAccepted / AbuserRejected are the swarm's totals.
	AbuserAccepted int
	AbuserRejected int
	// AbuserAliveAfter is how many abuser connections still served an honest
	// exchange once the swarm quiesced.
	AbuserAliveAfter int
	// Abusers is how many pushed.
	Abusers int
	// RefusalsConcurrentWithHonest is how many abusive messages were refused on a
	// round trip that OVERLAPPED a honest exchange's own flight.
	//
	// It is the overlap instrument, and it is an interval intersection rather than
	// an event-in-window test: the abuser samples the honest client's in-flight
	// state immediately before it writes and again at the moment it counts the
	// refusal, and both endpoints are published by the goroutine that owns them.
	// See [boltDecodeSwarm.abuser] for the sampling and
	// [checkBoltDecodeSwarmNonVacuity] for what the clause may and may not read
	// into it.
	RefusalsConcurrentWithHonest int64
	// RejectionsSpanningHonestWindow is how many abusive messages were refused on a
	// round trip that INTERSECTED the honest window — the interval from the first
	// honest exchange starting to the last one finishing.
	//
	// It is the quantity nv-swarm-pressure-density adjudicates, and it is an
	// interval intersection rather than a counter differenced across the window: the
	// abuser samples the honest window's published phase immediately before it
	// writes and again at the moment it counts the refusal. See
	// [boltDecodeSwarm.honestPhase] for the three phases and
	// [checkBoltDecodeSwarmNonVacuity] for why the counter difference it replaced
	// could not carry the claim.
	//
	// No FLOOR is ever put on it beyond nonzero. It is a count of events over an
	// interval whose length the machine controls, so any floor above that passes on
	// an idle host and fails on a busy one — which is exactly what two earlier
	// versions of nv-swarm-pressure-density did (rmp #2587).
	//
	// It cannot carry the overlap claim on its own: a fleet that took turns with the
	// honest client, never once refusing on a round trip that overlapped honest
	// work, would produce a large count here and witness nothing about concurrency.
	// Overlap is adjudicated on RefusalsConcurrentWithHonest above, and this total is
	// what gates it — a window that held no refusals at all is this clause's own
	// subject, not that one's.
	RefusalsSpanningHonestWindow int64
	// RejectionsDuringHonest is how many abusive messages the fleet-wide counter
	// ADVANCED BY between the honest client's own sample after the start barrier and
	// its deferred sample once the last exchange had finished.
	//
	// DIAGNOSTIC ONLY — no clause reads it any more, and rmp #2611 is why. It was
	// the density clause's instrument through two earlier versions, and a nonzero
	// floor on it was described here as the one floor that was safe. It is not: the
	// quantity is not a count of refusals drawn inside the window, it is a
	// difference between two reads of a counter an abuser increments only after
	// decoding its refusal reply. A refusal drawn on a round trip that straddles the
	// window's close is therefore counted AFTER the window and missed entirely, and
	// under load — where an abusive round trip outlasts the whole honest window —
	// that case stops being rare. Measured on a coverage-instrumented sweep of 100
	// seeds, 2 seeds per sweep read zero here while the fleet had drawn 3 refusals
	// and the overlap instrument had attributed 2 of them to honest FLIGHT: the
	// pressure was demonstrably live and this instrument could not see it.
	//
	// So this is the THIRD iteration of one defect. #2587 removed a numeric floor
	// (eight refusals) and then a positional one (one per segment) after both failed
	// on clean engines; what it left was a nonzero floor on this counter, which is
	// scheduler-dependent for a different reason — not the RATE of refusals but
	// WHERE the counter records them. The floor is gone with the instrument: the
	// claim now rests on RefusalsSpanningHonestWindow above.
	//
	// It is still rendered, and [boltDecodeSwarmInFlightRefusals] plus
	// [boltDecodeSwarmGapRefusals] is still exactly this number minus its tail, so
	// the three together keep showing where the counter recorded the pressure
	// relative to the honest client's own samples.
	RejectionsDuringHonest int64
	// WideHoldExpiries is how many WIDE honest exchanges reached
	// [boltDecodeSwarmWideHoldMax] before the fleet had completed the round trips
	// their hold was waiting for (see [boltDecodeSwarm.wideHold]).
	//
	// RENDERED and adjudicated nowhere, for the same reason as GateTimeouts below: a
	// threshold on it would be another floor that machine load moves. Zero is the
	// ordinary reading; a nonzero one says the fleet stalled, and the refusals that
	// run drew inside honest flight were coincidences again.
	WideHoldExpiries int64
	// GateTimeouts is how many times an abuser gave up waiting for a partner at the
	// fleet's rendezvous (see [boltDecodeSwarmGate]).
	//
	// It is RENDERED and adjudicated nowhere. Zero is the ordinary reading and every
	// regime measured for rmp #2611 returned zero; a nonzero one says the fleet
	// stopped pairing, so the refusals that run drew were coincidences again rather
	// than consequences of the construction. Thresholding it would put back exactly
	// the kind of load-moved floor this surface has now removed three times, so it
	// is reported as data and read by a human.
	GateTimeouts int64
	// PressureStarted records whether the honest client saw a refusal counted
	// before it began, i.e. whether the start barrier was satisfied rather than
	// expiring. It is what tells a failing run apart: honest exchanges that did not
	// straddle because there was no pressure, versus ones that did not straddle
	// while there was.
	PressureStarted bool
	// Swarm marks the concurrent arm, whose adjudication differs.
	Swarm bool
}

type BoltDecodeExchange struct {
	// Name is the arm's stable name; it is what a violation cites.
	Name string
	// Vehicle is the message kind the abuse rode in on: "run" or "hello". The
	// HELLO arms matter on their own because the wire nesting cap is reachable
	// during the FIRST HELLO decode, before any authentication.
	Vehicle string
	// Composite is the nesting arm's chain kind — "list" or "map" — or "" for the
	// pool arms. Both kinds must hit the same cap: readValue's bound is on
	// composite depth, not on lists.
	Composite string
	// Reply is the terminal reply kind: "SUCCESS", "FAILURE", "IGNORED", or
	// "RECORD+SUCCESS" when records preceded it.
	Reply string
	// Code and Message are the FAILURE's, with the per-session id redacted
	// ([boltDecodeRedactSession]) so the rendering stays a function of the seed.
	Code    string
	Message string
	// Depth is the nesting chain's length for a nesting arm, 0 otherwise.
	Depth int
	// Elements is the parameter list's element count for a pool arm, -1 otherwise.
	Elements int
	// WireBytes is the message's size on the wire. For the nesting family it is the
	// evidence that SIZE cannot be what refused it.
	WireBytes int
	// ModelHeld is the harness's model of the pool hold, for pool arms only.
	ModelHeld int64
	// SessionUsable is whether the SAME connection served a follow-up exchange
	// with NO RESET in between. It is the third discriminator between the caps:
	// the two decode-layer refusals happen above the session state machine and
	// leave it READY; the engine's parameter cap travels through it and FAILS it.
	SessionUsable bool
	// FollowUpValue is what the follow-up RUN returned, or -1 when it was not
	// served. The harness picks the expected value, so a connection that answered
	// with someone else's row is a failure and not a pass.
	FollowUpValue int64
}

type BoltDecodeHonest struct {
	// Index identifies the exchange and IS the value its query must return, so the
	// oracle is arithmetic rather than the server's own claim.
	Index int
	// RejectionsBefore/RejectionsAfter sample the fleet-wide rejection counter
	// immediately before the request is written and immediately after the reply is
	// read. After > Before means abusive traffic was REFUSED, AND COUNTED, while
	// this exchange was in flight.
	//
	// That is weaker than it looks and it is REPORTED, never adjudicated: an abuser
	// increments the counter only after decoding its reply, so a refusal issued
	// before this exchange opened can be counted inside it. See
	// [boltDecodeSwarmInFlightRefusals] for the measurement that establishes how
	// badly, and [BoltDecodeEvidence.RefusalsConcurrentWithHonest] for the
	// instrument nv-swarm-overlap uses instead.
	RejectionsBefore int64
	RejectionsAfter  int64
	// Value is what the exchange returned, or -1 when it returned nothing.
	Value int64
	// Elapsed bounds liveness. It is deliberately NOT rendered: it is a property of
	// the machine, not of the seed.
	Elapsed time.Duration
	// OK is whether the exchange completed and returned exactly one record.
	OK bool
	// Wide marks an exchange that deliberately held its stream open for
	// [boltDecodeSwarmWideHold] between RUN and PULL. Its in-flight window is wide
	// enough to hold several refusals when they are arriving quickly, and the run
	// reports how many the narrowest one held; nothing thresholds it (rmp #2596).
	Wide bool
}

type BoltDecodeProbe struct {
	// Code is the failure code when the pool refused, else "".
	Code string
	// Elements is the parameter list's element count, the only thing that varies
	// across a scan.
	Elements int
	// ModelHeld is what [boltDecodeModelHeld] says this message's decode holds from
	// the shared pool at its peak. It is computed by the harness, never read from
	// the server.
	ModelHeld int64
	// Slack is Budget - ModelHeld: positive when the model says the message fits.
	// It is what makes the leak probe's SENSITIVITY explicit.
	Slack int64
	// Accepted is whether the server decoded and ran the message.
	Accepted bool
}

type BoltDrainCommit struct {
	// Name is the node name the statement would create.
	Name string
	// Phase is "pre" (issued and answered before the teardown began), "inflight"
	// (parked inside its WAL fsync when the teardown began) or "post" (issued after
	// the teardown).
	Phase string
	// RunCode is the failure code the RUN was answered with, "" for a SUCCESS.
	// RunAcked records an EXPLICIT [proto.Success], classified with [isSuccess]. For
	// an auto-commit write the RUN reply is the durability acknowledgement (see
	// [boltDrainAckIsRunSuccess]).
	RunCode  string
	RunAcked bool
	// RunIgnored records a [proto.Ignored] reply ([isIgnored]): the session was
	// already FAILED, so the statement was never dispatched and nothing was written.
	//
	// It has its own field because reading the acknowledgement as "not a FAILURE"
	// counts an IGNORED as a durable commit. That is not hypothetical: it is the
	// defect this file's FIRST oracle had, and it manufactured an ACID_DURABILITY
	// violation in 8 of 30 concurrent runs. The mechanism, measured: the shutdown
	// answered a committer's RUN with Neo.ClientError.Transaction.Terminated, which
	// puts the session in FAILED; the committer's NEXT RUN was answered IGNORED; the
	// harness recorded an acknowledgement; and the name it then demanded from
	// recovery had never been written at all — confirmed by finding it neither in the
	// live engine nor anywhere in the raw WAL image. bolt_auth_surface.go (rmp #2481)
	// added [isIgnored] against exactly this class of false positive and noted that
	// its own arms did not reach the branch; these arms do.
	RunIgnored bool
	// PullAcked records whether the client also drained the result stream. It is a
	// WITNESS, not a clause: a graceful Shutdown closes the connection as soon as
	// the in-flight statement's reply is flushed, so an acknowledged in-flight
	// commit routinely never gets its PULL through (measured; see the file
	// comment).
	PullAcked bool
	// PullCode is the failure code the PULL terminal carried, "" when there was
	// none, and PullIgnored records an IGNORED terminal.
	PullCode    string
	PullIgnored bool
	// Transport records that the round trip failed below the protocol (the
	// connection was closed under the client). Rendered as a boolean in the
	// evidence's String because the underlying text names a connection object.
	Transport bool
}

type BoltDrainConfig struct {
	// Seed is the master seed. Every node name and the SimDisk sub-stream derive
	// from it.
	Seed uint64
	// Arm names the variant (see the ArmBoltDrain* constants).
	Arm string
	// ParkCommit arms a [SyncGate] on the next fsync and holds one commit inside
	// it, so the teardown genuinely races an in-flight writer.
	ParkCommit bool
	// ShutdownBudget bounds the first Shutdown call. Zero passes
	// [context.Background], so Shutdown drains to completion.
	ShutdownBudget time.Duration
	// ExpiryByCancel bounds Shutdown with an explicit cancel on a context that has
	// NO deadline, instead of with a deadline. It is the only way to reach
	// Shutdown's `<-ctx.Done()` branch: with a deadline, Shutdown's own clamped
	// time.After wins (measured 12/12; see the file comment).
	ExpiryByCancel bool
	// ShutdownCalls is how many times Shutdown is called (minimum 1). Two is what
	// makes the published-identity clause a statement about the server's sync.Once.
	ShutdownCalls int
	// FailClose arms a one-shot fsync fault on the WAL close, so the store's
	// teardown FAILS and the value the server caches is non-nil.
	FailClose bool
	// CloseOutOfOrder closes the store DIRECTLY, with a live client mid-session and
	// no drain at all. It is the sensitivity seam: it reproduces what the ordering
	// exists to prevent, so the ordering and wire clauses are proved to fire.
	CloseOutOfOrder bool
	// Fleet drives several concurrent committers instead of the deterministic
	// single-commit geometry. NOT bit-reproducible.
	Fleet bool
	// SkipCheckpointer stands the store up with NO checkpointer at all: no loop, no
	// published snapshot, and recovery through WAL replay alone. It is the A/B seam
	// for attributing a lost commit to the checkpoint interaction rather than to the
	// drain, and it is deliberately a configuration rather than a separate code path
	// so the two sides differ in exactly one thing.
	//
	// It is not a shipped arm: with no snapshot and no loop to join, the coverage gate
	// fires on nonvacuity-snapshot and nonvacuity-loop by design.
	SkipCheckpointer bool
}

type BoltDrainEvidence struct {
	// Arm is the variant that produced this evidence; Seed is the seed it was
	// built from.
	Arm  string
	Seed uint64

	// CloserWired records that the server was actually given an
	// [server.Options.Closer]. Without it every ordering clause below is inert.
	CloserWired bool
	// ConnDecorated records that the connection tracker was installed, which is
	// what the ordering clause reads.
	ConnDecorated bool

	// CloseBodies is every invocation of the store's teardown, in call order. The
	// contract is exactly one.
	CloseBodies []boltDrainCloseBody
	// CloseBodiesWhileParked is how many teardown bodies had been entered while a
	// commit was still parked inside its WAL fsync AND Shutdown had demonstrably
	// closed the listener. It must be zero.
	CloseBodiesWhileParked int64
	// CloseBodiesAtShutdownReturn is how many teardown bodies had been entered at
	// the instant the FIRST Shutdown call returned. On an expiry arm it must be
	// zero: neither of Shutdown's failure branches closes the owned store
	// (bolt/server/serve.go:874-879), so the store is closed later, by Serve's exit
	// path — which is what makes the attribution clause below adjudicable there and
	// only a witness on the success path.
	CloseBodiesAtShutdownReturn int64
	// CloseFaultArmed records that a one-shot fsync fault was armed on the WAL
	// close, so the value the server caches is non-nil and its identity across
	// callers is a discriminating assertion.
	CloseFaultArmed bool

	// The four declarative echoes of the arm's configuration. They are in the
	// evidence so the adjudicators are pure functions of it and never re-derive an
	// expectation from the arm's NAME — which is what lets a falsifiability table
	// build a healthy value for any arm and perturb one field of it.
	//
	// ParkExpected: the arm intended to park a commit inside its fsync.
	// ExpiryExpected: the arm bounded Shutdown so it could not drain in time.
	// OutOfOrderArm: the arm closed the store directly, with no drain at all.
	// FleetArm: the arm drove concurrent committers and is not bit-reproducible.
	ParkExpected   bool
	ExpiryExpected bool
	OutOfOrderArm  bool
	FleetArm       bool

	// AckedAfterCheckpoint is how many acknowledged commits landed after the arm's
	// one checkpoint and therefore live ONLY in the WAL suffix. Without at least
	// one, every acked name could come back from the published snapshot and a WAL
	// close that flushed nothing would satisfy the durability clause — the same
	// measurement db_teardown.go records for its own arms.
	AckedAfterCheckpoint int

	// ConnsAccepted / ConnsClosed / ConnsPeak / ConnsLiveAtEnd are the connection
	// tracker's totals for the whole arm.
	ConnsAccepted   int64
	ConnsClosed     int64
	ConnsPeak       int64
	ConnsLiveAtEnd  int64
	IdleConnsOpened int

	// GateArmed records that a fsync rendezvous was armed, GateFired that it was
	// actually entered — the reachability observable rmp #2465 established, since
	// an ordinal that never matched is a silent no-op.
	GateArmed bool
	GateFired bool
	// ParkedLiveConns is how many server-side connections were live while the
	// commit was parked. It is SAMPLED at the instant the fsync gate fires, so it is
	// a coverage witness and not a function of the seed: like ConnsPeak it is read
	// by the non-vacuity gate but deliberately absent from
	// [BoltDrainEvidence.String], for the reason set out there.
	// ListenerClosedWhileParked records that the listener was
	// already closed in that window, which is what proves Shutdown had passed
	// ln.Close() and was inside its drain wait rather than not yet started.
	// DialRefusedAfterTeardown is the same observable from a client's point of view,
	// taken once the teardown is over (where a probe Dial can create nothing).
	ParkedLiveConns           int64
	ListenerClosedWhileParked bool
	DialRefusedAfterTeardown  bool

	// ShutdownErrs renders what each Shutdown call returned, in call order.
	ShutdownErrs []string
	// ShutdownFirstNil records whether the FIRST Shutdown drained cleanly, and
	// LastShutdownNil whether the LAST one did. They differ on the expiry arms: the
	// first reports the expiry, and the last — made after the drain finally
	// completed — observes the cached, successful close result.
	ShutdownFirstNil bool
	LastShutdownNil  bool
	// ShutdownCalls is how many Shutdown calls the arm made, and
	// DistinctShutdownErrs how many distinct error VALUES they returned — compared
	// by identity, never by class, because the class cannot tell one published
	// value from N re-derived ones.
	ShutdownCalls        int
	DistinctShutdownErrs int
	// ShutdownErrIsDrainTimeout / ShutdownErrIsCtx classify the FIRST call's error:
	// which of Shutdown's two failure branches was taken.
	ShutdownErrIsDrainTimeout bool
	ShutdownErrIsCtx          bool
	// ShutdownErrIsCloseFault records that the first call returned the store's own
	// close failure, which is what the publication arm asserts identity over.
	ShutdownErrIsCloseFault bool
	// ShutdownExpiryBudget is the bound the arm gave Shutdown (zero when it gave
	// none), and ShutdownExpiryByCancel records that the bound was an explicit
	// cancel on a deadline-free context rather than a deadline.
	ShutdownExpiryBudget   time.Duration
	ShutdownExpiryByCancel bool
	// ServeExitErr renders what [server.Server.Serve] returned, and
	// ServeExitErrIsCloseFault whether it carried the store's close failure —
	// which is how Serve's exit path is shown to observe the SAME cached result
	// without comparing a joined error by pointer.
	ServeExitErr             string
	ServeExitErrIsCloseFault bool

	// Commits is every write attempt over the wire, in the order it was made.
	Commits []BoltDrainCommit
	// InterruptedRuns and TerminatedRuns count the writes answered with each of the
	// two codes a shutdown-interrupted statement can receive. They are MEASUREMENTS,
	// carried so the difference between them is visible in a report: one is transient
	// and a driver retries it, the other is demoted to a client error and is never
	// retried (see [boltDrainTerminatedCode]).
	InterruptedRuns int
	TerminatedRuns  int
	// IgnoredReplies counts the RUN and PULL replies that were IGNORED because the
	// session was already FAILED. Such a reply is never an acknowledgement and never
	// enters the acked set; it is counted so a run in which the arms measured nothing
	// but ignored traffic is visible rather than silently green.
	IgnoredReplies int

	// PostCloseCommitErr renders what a commit attempted through the transaction
	// layer AFTER the teardown returned, and PostCloseCommitRefused whether it was
	// refused with [wal.ErrWriterClosed]. This is the one place the writer-closed
	// error is identifiable at all (over the wire it is sanitised), so it is both
	// the proof the WAL closed and the proof the detector is not blind.
	PostCloseCommitErr     string
	PostCloseCommitRefused bool

	// LoopAliveBeforeTeardown is the liveness probe taken BEFORE the teardown (a
	// checkpoint request succeeded, so there was a goroutine to join), and
	// LoopStoppedAfterTeardown the join verdict (a request afterwards returned
	// [checkpoint.ErrCheckpointerStopped]). A WAL-closed error instead would mean
	// the loop outlived the WAL — the failure the composed teardown exists to
	// prevent.
	LoopAliveBeforeTeardown  bool
	LoopStoppedAfterTeardown bool

	// AckedNames are the names whose RUN was acknowledged, IssuedNames every name
	// the arm sent, RecoveredNames what a reopen through real recovery found.
	// MissingAcked is acked minus recovered (a durability defect) and
	// PhantomNames recovered minus issued (a consistency defect).
	AckedNames     []string
	IssuedNames    []string
	RecoveredNames []string
	MissingAcked   []string
	PhantomNames   []string
	// PartialNames are recovered nodes missing their age property: a torn
	// transaction resurrected by recovery.
	PartialNames []string
	// RecoveredWALOps is how many WAL ops the reopen's recovery replayed. It is
	// what stops the durability clause being answered by a snapshot underneath it,
	// and it is a pure function of the seed: an op count does not depend on how wide
	// any encoded value happened to be.
	RecoveredWALOps int
	// WALBytes is the size of the durable WAL image the reopen read. It is a
	// DIAGNOSTIC ONLY and deliberately absent from [BoltDrainEvidence.String] and
	// from every violation message: a created node's hidden internal key is minted
	// as "__cx_"+hex(n) from a PROCESS-GLOBAL counter (cypher/exec/create_node.go)
	// and travels inside the WAL frame, so the same seed produces frames of
	// different widths depending on how many nodes every other test in the process
	// created first. The same limitation, from the same counter, is documented in
	// bolt_auth_surface.go and schema_mutation.go.
	WALBytes int
	// SnapshotPublished records whether a snapshot manifest sits beside the WAL,
	// and ReopenClean whether recovery reported a clean image.
	SnapshotPublished bool
	ReopenClean       bool
}

type BoltMetadataObs struct {
	// SentKeys are the keys the arm put in the `tx_metadata` map, sorted.
	SentKeys []string
	// Accepted is true when the BEGIN carrying them was answered SUCCESS.
	Accepted bool
	// GotCode carries a refusal, empty when none came.
	GotCode string
	// BeginMetaKeys, TerminalMetaKeys and CommitMetaKeys are every key the BEGIN
	// SUCCESS, the terminal PULL SUCCESS and the COMMIT SUCCESS carried, each sorted.
	// The clause is that no SentKey appears in any of them: `tx_metadata` is read
	// nowhere in the module, so there is nothing to echo, and pinning the absence is
	// the honest assertion.
	BeginMetaKeys, TerminalMetaKeys, CommitMetaKeys []string
}

type BoltModeArm struct {
	// Name identifies the arm; SentMode is the value sent, and SentKey whether the
	// key was present at all.
	Name     string
	SentMode string
	SentKey  bool
	// RegistryMode is [server.TransactionInfo.Mode] read off the server's own
	// open-transaction registry while the transaction was open. It is the INDEPENDENT
	// observable: BEGIN's SUCCESS carries no mode, so without the registry the only
	// evidence of the server's decision would be the write attempt itself, and a
	// clause resting on one observable could not tell a mis-recorded mode from a
	// mis-enforced one.
	RegistryMode string
	// WriteAccepted is true when a write statement inside the transaction was
	// answered SUCCESS; WriteCode and WriteMessage carry the refusal when it was not.
	WriteAccepted           bool
	WriteCode, WriteMessage string
	// BeginRefused records that the BEGIN ITSELF was refused, with its code and
	// message. It is separate from WriteCode because the two are different events
	// and were previously conflated: before rmp #2564 no arm could be refused at
	// BEGIN, so the driver reused the write fields, and a clause reading them
	// could not tell "the transaction never opened" from "the write inside it was
	// refused".
	BeginRefused            bool
	BeginCode, BeginMessage string
}

type BoltOffer struct {
	// Version is the top of the offered range.
	Version proto.Version
	// MinorRange is how far below Version.Minor the client will accept. Zero
	// offers that exact version and no fallback.
	MinorRange uint8
}

type BoltRouteObs struct {
	// ListenerAddr is [SimServer.ListenerAddr] — the independent reference the
	// advertised addresses are compared against.
	ListenerAddr string
	// SentDB and SentBookmark are what the populated ROUTE asked for, so the clause
	// that the reply ignores them names what was ignored.
	SentDB, SentBookmark string
	// Roles are the roles the table advertised, in the order the server listed them.
	Roles []string
	// AddressesByRole maps each advertised role to its address list. A role listed
	// twice would collide here, so RoleCount records the raw entry count separately.
	AddressesByRole map[string][]string
	RoleCount       int
	// TTL is the table's `ttl`, and TTLPresent whether the key was there and of the
	// expected type at all.
	TTL        int64
	TTLPresent bool
	// TableDB is the table's own `db` field. RoutingTable hardcodes it to the empty
	// string (bolt/server/route.go:30), so it does NOT echo SentDB — which is what
	// the arm pins.
	TableDB string
	// ZeroMessageRender is the rendering of the table returned for the ZERO ROUTE
	// message, and PopulatedRender the one for the populated message. They are
	// compared for equality, which is how "the routing context and the bookmarks are
	// ignored" is asserted rather than described.
	PopulatedRender, ZeroMessageRender string
	// Accepted records that both ROUTE messages were answered SUCCESS.
	Accepted bool
	// GotCode carries a refusal, empty when none came.
	GotCode string
}

type BoltStreamEvidence struct {
	// Seed is the seed the run was built from.
	Seed uint64

	// Reference is the record set the reference drain produced, decoded.
	Reference [][]packstream.Value
	// ReferenceTerminal / ReferenceHasMore are its terminal reply's kind and
	// has_more. A single PULL -1 always exhausts the stream, so has_more must be
	// false here; recording it makes the paged arm's true readings comparable
	// against a measured false rather than against an assumption.
	ReferenceTerminal string
	ReferenceHasMore  bool

	// PageSizes are the seed-drawn n values, in the order they were sent.
	PageSizes []int64
	// Pages is one entry per PULL {n} of the paged drain.
	Pages []BoltStreamPage
	// Paged is the concatenation of every RECORD the paged drain delivered.
	Paged [][]packstream.Value
	// PagingReusable records that a fresh RUN+PULL on the SAME connection was
	// acknowledged after the paged drain completed, i.e. the session returned to
	// READY.
	PagingReusable bool

	// WindowPageSizes are the drawn n values of the prefix pages, in order.
	WindowPageSizes []int64
	// WindowPrefixPages is how many drawn pages were pulled before the DISCARD.
	WindowPrefixPages int
	// WindowPrefixPagesSeen is one entry per prefix page.
	WindowPrefixPagesSeen []BoltStreamPage
	// WindowPrefix is what those pages delivered, concatenated.
	WindowPrefix [][]packstream.Value
	// WindowDiscardN is the seed-drawn n the DISCARD asked to drop.
	WindowDiscardN int64
	// WindowDiscard is the DISCARD exchange itself.
	WindowDiscard BoltStreamPage
	// WindowSuffix is what the closing PULL -1 delivered.
	WindowSuffix [][]packstream.Value
	// WindowSuffixPage is that closing exchange.
	WindowSuffixPage BoltStreamPage
	// WindowReusable records that a fresh RUN+PULL on the same connection was
	// acknowledged afterwards.
	WindowReusable bool

	// EffectDiscard is the DISCARD exchange that abandoned the write's delivery.
	EffectDiscard BoltStreamPage
	// EffectStats is the "stats" map the DISCARD's terminal SUCCESS reported,
	// flattened to int64 counters (a bool counter is recorded as 1).
	EffectStats map[string]int64
	// EffectLive / EffectRecovered are how many nodes carrying
	// boltStreamDiscardLabel exist in the live engine and in a graph reopened
	// through real recovery after a crash.
	EffectLive, EffectRecovered int
	// EffectReusable records that a fresh RUN+PULL on the same connection was
	// acknowledged after the mid-stream DISCARD, which is the AC's "a post-DISCARD
	// RUN succeeds" stated on the connection that did the discarding.
	EffectReusable bool

	// Refusals are the refusal probes in the order they ran.
	Refusals []BoltStreamRefusal
	// ProbedQIDs are the qid values the qid probes actually sent. Recorded so the
	// non-vacuity gate can require them to be POSITIVE: a probe that sent -1 would
	// be asserting the refusal of the current-stream qid.
	ProbedQIDs []int64
	// RunQIDs are the qid values every RUN SUCCESS in the run reported. Every one
	// must be -1, which is what makes "no positive qid is ever minted" an assertion
	// rather than an argument.
	RunQIDs []int64
	// QIDControlRows is how many RECORDs the qid=-1 control drain delivered on a
	// stream identical to the refused probes'. Zero would mean "every PULL is
	// refused", under which the refusal clauses say nothing about the qid.
	QIDControlRows int

	// TxArms are the committed and the doomed transaction, in that order.
	TxArms []BoltStreamTxArm
	// DoomedLive / DoomedRecovered are how many nodes carrying
	// boltStreamDoomedLabel exist live and after recovery. Both must be 0.
	DoomedLive, DoomedRecovered int
	// CommittedLive / CommittedRecovered are the same census for
	// boltStreamCommitLabel. Both must equal boltStreamInFlightCap: the cap allows
	// exactly that many cursors, and the arm writes one node per cursor.
	CommittedLive, CommittedRecovered int

	// StallArm marks this evidence as the concurrent slow-consumer arm rather than
	// the deterministic battery, so the checkers adjudicate the stall clauses and
	// skip the deterministic ones.
	StallArm bool
	// StallRecordsPulled is how many RECORDs the slow consumer drained before it
	// stopped, StallParked whether the stream was still open when the consumer
	// stalled, and StallClosedCleanly whether the connection tore down without an
	// unexpected transport fault.
	StallRecordsPulled int
	StallParked        bool
	StallClosedCleanly bool
	// StallBufferedPeak is the MAXIMUM number of bytes observed queued toward the
	// stalled consumer, sampled by [boltStreamPollParked].
	//
	// What it can and cannot show was verified in the harness's own code rather
	// than assumed. [halfPipe.write] fills to exactly [simConnBufferSize] and then
	// parks (internal/sim/simconn.go:96-124: it chunks each write to the space
	// remaining, so the buffer NEVER exceeds the bound). So "the server did not
	// buffer past the bound" is an invariant of the pipe, not a property of the
	// server, and a clause asserting it cannot fail against a real server. It is
	// kept as a guard on the harness itself and is labelled as such.
	//
	// What the peak DOES establish is that the writer really was blocked when the
	// consumer tore the connection down: a peak at the bound means the server had
	// rows it could not hand over. The server-side HEAP bound — that the page was
	// not materialised into a second in-memory copy ahead of the wire — is measured
	// where it can be measured, by the live-heap gate in
	// bolt/server/streaming_backpressure_test.go, and is not restated here.
	StallBufferedPeak int
	// StallSurfaceValues are the integers a FRESH connection's paged drain
	// delivered after the stalled connection was torn down mid-stream, and
	// StallSurfacePages the pages that drain took.
	//
	// The values are stored rather than a comparison verdict, because the
	// reference here is ARITHMETIC — the drain runs UNWIND range(1, N), so the
	// expected sequence is 1..N and the checker derives it without asking the
	// server anything. That keeps the stall arm's oracle independent without
	// paying for a second full reference drain.
	StallSurfaceValues []int64
	StallSurfacePages  []BoltStreamPage
}

type BoltStreamPage struct {
	// Terminal is the terminal reply's kind: "SUCCESS", "FAILURE", "IGNORED", or
	// "" when the exchange produced no terminal at all. It is recorded as a kind
	// rather than as a bool because a RUN SUCCESS is not an acknowledgement and an
	// IGNORED is not one either; only the terminal reply of the drain is.
	Terminal string
	// Code is the failure code when Terminal is "FAILURE", else "".
	Code string
	// Requested is the n the client asked for.
	Requested int64
	// Delivered is how many RECORDs actually arrived before the terminal reply.
	Delivered int
	// HasMore is the has_more the terminal SUCCESS reported.
	HasMore bool
	// Bookmarked reports whether the terminal SUCCESS carried a "bookmark" key.
	// The bookmark rides on the TERMINAL reply only, so it doubles as an
	// independent witness of which page the server considered final.
	Bookmarked bool
	// Discard records that this exchange was a DISCARD rather than a PULL.
	Discard bool
}

type BoltStreamRefusal struct {
	// Name identifies the probe in a violation message.
	Name string
	// WantCode / GotCode are the failure code the probe must be told and the one it
	// received ("" when the probe was not refused at all).
	WantCode, GotCode string
	// WantMessage is the exact FAILURE text the probe must be told, or "" to waive
	// the exact-text check in favour of WantStateInMessage.
	WantMessage string
	// GotMessage is the FAILURE text actually received.
	GotMessage string
	// WantStateInMessage is the session state failTransition must name, or "" when
	// the refusal is not a failTransition.
	//
	// It exists because handleRun's authentication gate (session.go:1072) and its
	// state gate (:1075) both return failTransition's
	// Neo.ClientError.Request.Invalid, so a code match cannot say which refused.
	// failTransition reports the ORIGIN state (:1885), which is the discriminator:
	// a refusal by the state gate on a live stream names STREAMING or TX_STREAMING,
	// whereas the auth gate would name whatever state the de-authorised session sat
	// in.
	WantStateInMessage string
	// NextTerminal is the terminal kind the NEXT request on the same connection
	// drew. Measured "IGNORED": the refusal routes through enterFailed, and a
	// FAILED session soft-ignores request-phase messages until RESET.
	NextTerminal string
	// Delivered is how many RECORDs the refused message delivered. It must be 0.
	Delivered int
	// Accepted records what actually happened: the decisive message drew a SUCCESS.
	Accepted bool
	// PriorAck records that an earlier statement on the SAME connection was
	// acknowledged through its terminal reply. Without it, "the message was
	// refused" is equally explained by a connection that never worked.
	PriorAck bool
	// RecoveredAfterReset records that a RUN+PULL after RESET was acknowledged on
	// the same connection, which is what makes the refusal SCOPED rather than
	// terminal.
	RecoveredAfterReset bool
}

type BoltStreamTxArm struct {
	// Name identifies the arm.
	Name string
	// RefusalCode / RefusalMessage are the typed FAILURE the over-cap RUN drew.
	RefusalCode, RefusalMessage string
	// FramesBefore / FramesAfter bracket the arm with wal.Stats.Frames.
	FramesBefore, FramesAfter uint64
	// BytesBefore / BytesAfter bracket it with wal.Stats.Bytes. Only a ZERO delta
	// is adjudicated or rendered; see the file comment on seed-purity.
	BytesBefore, BytesAfter uint64
	// Cycles is how many RUN+PULL cycles the server accepted inside the
	// transaction. Each accepted RUN appends one cursor to tx.results.
	Cycles int
	// CursorsAtRefusal is the "open=N" figure the cap's own diagnostic reported,
	// parsed back out of the message. It is the server's own count of accumulated
	// cursors, so agreeing with Cycles is a cross-check between two independent
	// accountings.
	CursorsAtRefusal int
	// RefusalObserved records that a typed FAILURE arrived within
	// boltStreamReplyBound rather than the round trip stalling.
	RefusalObserved bool
	// Committed records that the arm's COMMIT was acknowledged.
	Committed bool
}

type BoltTimeoutArm struct {
	// Name identifies the arm.
	Name string
	// SentTimeoutMS is the `tx_timeout` value the arm put on BEGIN, in
	// milliseconds. SentKey distinguishes "sent zero" from "omitted".
	SentTimeoutMS int64
	SentKey       bool
	// IdleBound / DefaultTotalBound are the two server-side bounds installed, in
	// VIRTUAL time. They are recorded because the reaper fires at the earlier of the
	// two and the whole attribution of the arm rests on which one that is.
	IdleBound, DefaultTotalBound time.Duration
	// Advanced is how much VIRTUAL time the arm delivered, in the order it delivered
	// it. An arm may advance twice: once to show a bound is NOT yet reached, once to
	// reach it.
	Advanced []time.Duration
	// ReapedAfter is the index into Advanced of the advance that reaped the
	// transaction, or -1 when no advance did.
	ReapedAfter int
	// TimersArmed is how many timers the server registered on the injected clock
	// across the arm. It is what makes a NOT-reaped reading evidence: a reaper that
	// declined is a different thing from a reaper that was never armed, and only
	// this counter separates them. syncTxTimer's NewTimer is the only clock timer
	// registration in bolt/server (verified exhaustively for rmp #2482), so the count
	// is attributable.
	TimersArmed int64
	// GotCode / GotMessage are what the client was told on its next request-phase
	// message after the reap. SecondReplyKind is what the message AFTER that drew,
	// which must be IGNORED.
	GotCode, GotMessage string
	SecondReplyKind     string
	// Committed is true when the arm's COMMIT succeeded, which is what a NOT-reaped
	// control must report.
	Committed bool
	// ReplyElapsed is the REAL time from delivering the reaping advance to holding
	// the abort in hand. It is the "aborted rather than stalled" instrument and, being
	// scheduling-dependent, is kept out of the rendering.
	ReplyElapsed time.Duration
}

type BoltTxListingRow struct {
	// IDSuffix, Principal, Mode, Remote, State and Query are the listing's fields
	// verbatim, except that the id is reduced to its sequence suffix.
	IDSuffix  string
	Principal string
	Mode      string
	Remote    string
	State     string
	Query     string
	// StartedAt is TransactionInfo.StartedAt as an offset from the probe's base
	// instant. Because no advance is ever in flight while a transaction registers
	// — the arm advances only from its single controlling goroutine, and only
	// after the arming barrier — this must equal the plan's OpenedAt EXACTLY, not
	// approximately.
	StartedAt time.Duration
	// Elapsed is TransactionInfo.Elapsed verbatim. txRegistry.list computes it as
	// clk.Now() minus its own StartedAt (bolt/server/txregistry.go:174,185), so on
	// a still fake clock it must equal the listing instant minus StartedAt exactly.
	Elapsed time.Duration
}

type BoltTxPlanRow struct {
	// Principal is the identity the connection authenticated as. It is unique per
	// connection and is the only field that can attribute a listing entry to a
	// connection, because Remote is a constant.
	Principal string
	// Mode is the BEGIN access mode, "r" or "w", exactly as sent on the wire.
	Mode string
	// IDSuffix is the registry's per-server sequence suffix ("-1", "-2", …) taken
	// from the observed id. The id's prefix is crypto/rand and is never recorded,
	// so a report is reproducible; the suffix IS seed-reproducible, because it is
	// the ordinal of the BEGIN on this server.
	IDSuffix string
	// Query is the single statement run inside the transaction before it went
	// silent, which is what the listing must report back.
	Query string
	// OpenedAt is the fake instant the transaction was opened at, as a duration
	// since the probe's base instant.
	OpenedAt time.Duration
	// Conn is the connection's index in the plan, 0-based.
	Conn int
}

type BoltTxQuotaBegin struct {
	// Phase names the BEGIN's place in the roster.
	Phase string
	// Principal is the identity the connection authenticated as, which under
	// server.NoAuthHandler is exactly the quota key.
	Principal string
	// Mode is the access mode sent, "r" or "w".
	Mode string
	// Accepted records that the server answered SUCCESS. Code and Message are the
	// FAILURE's, verbatim, when it did not.
	Accepted bool
	Code     string
	Message  string
	// IDSuffix is the per-server sequence suffix of the id the registry minted,
	// empty for a refused BEGIN; WantSuffix is what the harness predicted from the
	// BEGIN's ordinal among the ACCEPTED ones, because only an accepted BEGIN
	// reaches txRegistry.nextID.
	IDSuffix   string
	WantSuffix string
	// RegistryBefore/RegistryAfter bracket the exchange with the WHOLE server's
	// listing size, and TimersBefore/TimersAfter with the counted timer
	// registrations. A refused BEGIN must move neither: it must leave the registry
	// exactly as it found it and arm nothing.
	//
	// The whole-server size is deliberately not the same quantity as the cap —
	// the control principal holds transactions of its own — so PrincipalOpenAfter
	// carries how many entries the BEGIN's OWN principal held once the answer was
	// in hand, which is the number the cap is actually about. The harness counts
	// it from the listing rather than from txQuota, which is unexported: they are
	// the same set, because Session.txClosed releases the slot and unregisters the
	// entry together (bolt/server/session.go:813-814).
	RegistryBefore     int
	RegistryAfter      int
	TimersBefore       int64
	TimersAfter        int64
	PrincipalOpenAfter int
	// WithinCeiling records that the exchange completed inside
	// [txQuotaRefusalCeiling] of REAL time — the clause that separates a typed
	// refusal from a stall. It is a boolean rather than the duration because the
	// duration is wall time and not seed-pure.
	WithinCeiling bool
}

type BoltTxQuotaEvidence struct {
	// Arm names the arm; Seed is the seed it was built from.
	Arm  string
	Seed uint64

	// Limit is server.Options.MaxOpenTxPerPrincipal as installed; PrincipalA is
	// the identity driven to it and PrincipalB the control.
	Limit      int
	PrincipalA string
	PrincipalB string

	// IdleBound, TotalBound and Step are the virtual geometry; Advances is how
	// many advances the reap composition made.
	IdleBound  time.Duration
	TotalBound time.Duration
	Step       time.Duration
	Advances   int

	// TimersTotal, Untils and Tickers are the counted registrations on the
	// injected clock, WantTimers the harness's own prediction of the total, and
	// Nows the read counter (not seed-pure; see the type comment). Touches is how
	// many open transactions the arm deliberately re-armed by sending them a
	// message after the clock had moved.
	TimersTotal int64
	WantTimers  int64
	Untils      int64
	Tickers     int64
	Nows        int64
	Touches     int

	// Begins is the BEGIN ledger, in the order the arm sent them.
	Begins []BoltTxQuotaBegin

	// CapModes are the access modes the cap-filling transactions used. Both kinds
	// must appear: the cap counts a read transaction exactly as it counts a write.
	CapModes []string
	// RegistryAtCap is the listing size once the principal held its cap.
	RegistryAtCap int

	// WantRefusalMessage is [txQuotaRefusalMessage] recomputed from PrincipalA and
	// Limit; the refusal's own text is on its ledger row.
	WantRefusalMessage string

	// PostRefusalAccepted records that an autocommit statement sent down the
	// REFUSED connection was served. It pins rmp #2561: the quota branch returns
	// before Transition and never enters FAILED, so the session is still READY.
	// PostRefusalCode and PostRefusalMessage carry what it was answered instead.
	PostRefusalAccepted bool
	PostRefusalCode     string
	PostRefusalMessage  string

	// PredictedReapOrdinals is [idleReapModel.reapOrdinalsWithin] computed BEFORE
	// the advances ran, over the three transactions open at that point;
	// ObservedReapOrdinals is the ordinal at which each was first absent, in the
	// same order. ReapProbeFires are the ordinals at which the arm's own uncounted
	// timer received the advance.
	PredictedReapOrdinals []int
	ObservedReapOrdinals  []int
	ReapProbeFires        []int
	// ReapCode and ReapMessage are what the reaped connection was told on its next
	// message — the attribution that turns "it is no longer listed" into "the idle
	// reaper ended it".
	ReapCode    string
	ReapMessage string

	// TerminateOutcome is what server.Server.TerminateTransaction returned for the
	// slot the operator reclaimed, and TerminatedGone that the entry left the
	// registry.
	TerminateOutcome txTerminateOutcome
	TerminatedGone   bool

	// The de-authorised-refusal composition (the rmp #2482 carry-over clause).
	// LogoffCommitCode and LogoffCommitMessage are what the refused COMMIT was
	// answered with, and LogoffEntryGone that the registry entry was reclaimed
	// rather than merely left behind by a refusal that wrote nothing.
	LogoffCommitCode    string
	LogoffCommitMessage string
	LogoffEntryGone     bool

	// Windows are the honest autocommit writes bracketing the run.
	Windows []BoltTxWriteWindow

	// GhostsLive/GhostsRecovered count [txQuotaGhostLabel] in the live engine and
	// after a crash and a real WAL replay; Honest* do the same for the witness.
	GhostsLive      int
	GhostsRecovered int
	HonestLive      int
	HonestRecovered int
}

type BoltTxRegistryEvidence struct {
	// Arm names the arm; Seed is the seed it was built from.
	Arm  string
	Seed uint64

	// TimersAtRendezvous is the counted timer registrations observed once every
	// transaction was open and its arming barrier had been reached. TimersTotal is
	// the count at the end of the run. Untils and Tickers are the other two
	// registration counters, and Nows is the read counter (not seed-pure; see the
	// type comment).
	TimersAtRendezvous int64
	TimersTotal        int64
	Untils             int64
	Tickers            int64
	Nows               int64

	// IdleBound and TotalBound are the two bounds installed on the SERVER.
	// ModelIdleBound is the bound the harness's own [idleReapModel] was built
	// from; a control desynchronises the two deliberately, and in the arm proper
	// they are equal.
	IdleBound      time.Duration
	TotalBound     time.Duration
	ModelIdleBound time.Duration
	// Step is one advance. SetupElapsed is the virtual time the staggered opens
	// consumed before the measured sequence began, and SimElapsed the total the
	// arm advanced. RendezvousAt is the virtual instant the listing was taken at.
	Step         time.Duration
	SetupElapsed time.Duration
	SimElapsed   time.Duration
	RendezvousAt time.Duration
	// Advances is how many advances the measured sequence made.
	Advances int

	// Plan is what the harness opened, in the order it opened it.
	Plan []BoltTxPlanRow
	// Listing is [server.Server.Transactions] at the rendezvous, in the order it
	// was returned. ListingOrder repeats that order as id suffixes alone, so a
	// re-ordering is legible in a report without reading the rows.
	Listing      []BoltTxListingRow
	ListingOrder []string

	// RegistryPeak is the largest listing the run ever observed. Accepted and
	// Refused count BEGINs by the server's answer — Refused is the per-principal
	// quota's refusal, which this arm installs no cap for and must therefore be
	// zero. Reaped counts the transactions observed to leave the registry across
	// the measured advances.
	RegistryPeak int
	Accepted     int
	Refused      int
	Reaped       int

	// PredictedReapOrdinals is [idleReapModel.reapOrdinals] computed BEFORE the
	// measured sequence ran; ObservedReapOrdinals is the ordinal at which each
	// transaction was first absent from the listing, in the same order as Plan,
	// or [reapNever] for one that never left.
	PredictedReapOrdinals []int
	ObservedReapOrdinals  []int
	// ProbeFireOrdinals are the ordinals at which the arm's own UNCOUNTED timer
	// received the advance. An ordinal missing here is an advance that never
	// reached a waiter, which would make "no reap at that ordinal" a statement
	// about the harness rather than about the reaper.
	ProbeFireOrdinals []int
	// SettleTimeoutOrdinals are the ordinals at which the registry never shrank to
	// the size the model predicts within [txRegistryObserveTimeout].
	SettleTimeoutOrdinals []int

	// ReapCodes and ReapMessages are what each abandoned connection was told on the
	// one message it was sent AFTER the measured sequence, in plan order: the typed
	// FAILURE the reaper arms, or "" when the server answered something else. They
	// are what attributes a transaction's ABSENCE from the registry to the reaper
	// rather than to a rollback, a dropped connection, or a harness mistake.
	ReapCodes    []string
	ReapMessages []string

	// Windows are the four honest autocommit writes, in the order they ran.
	Windows []BoltTxWriteWindow

	// ReapFrames and ReapBytes are the SUM of the per-advance WAL brackets. Each
	// bracket opens before an advance and closes when that advance has settled,
	// and the honest windows run BETWEEN advances, outside every bracket — which
	// is why this sum can be zero in a run that appended plenty of frames.
	//
	// The bracket is a LIVE instrument, measured rather than assumed: moving the
	// during-reap window inside an advance bracket made this read 4 frames and 195
	// bytes and fired the reap-wal clause, so a clean zero here is a statement
	// about the reap and not about a bracket that cannot see anything.
	ReapFrames uint64
	ReapBytes  uint64

	// SnapshotsBaseline, SnapshotsPeak and SnapshotsFinal are
	// [lpg.MVCCStats.ActiveSnapshots] before the first BEGIN, at its highest
	// reading, and once every transaction has been reaped. The final reading is
	// race-free: Session.abortTx rolls the engine transaction back — releasing the
	// horizon slot — BEFORE txClosed unregisters it (bolt/server/session.go:830),
	// so a registry the arm has watched empty cannot still be holding a slot.
	SnapshotsBaseline int
	SnapshotsPeak     int
	SnapshotsFinal    int

	// GhostsLive and GhostsRecovered count [txAbandonLabel] in the live engine and
	// after a crash and a real WAL replay. HonestLive and HonestRecovered do the
	// same for [txAbandonHonestLabel].
	GhostsLive      int
	GhostsRecovered int
	HonestLive      int
	HonestRecovered int
}

type BoltTxTerminateCall struct {
	// Name is the call's place in the roster: one of [txTerminateCalls].
	Name string
	// Target is the id SUFFIX the call aimed at.
	Target string
	// Got is what TerminateTransaction returned; Want is what the contract
	// requires for this call.
	Got  txTerminateOutcome
	Want txTerminateOutcome
}

type BoltTxTerminateEvidence struct {
	// Arm names the arm; Seed is the seed it was built from.
	Arm  string
	Seed uint64

	// IdleBound and TotalBound are the two bounds installed on the SERVER, and
	// Advances is how many times the arm advanced the fake clock. The arm's whole
	// attribution rests on Advances being zero.
	IdleBound  time.Duration
	TotalBound time.Duration
	Advances   int

	// Begins counts the explicit BEGINs the arm made; TimersArmed, Untils and
	// Tickers are the counted registrations on the injected clock, and Nows the
	// read count (not seed-pure; see the type comment).
	Begins      int
	TimersArmed int64
	Untils      int64
	Tickers     int64
	Nows        int64

	// Plan is the harness's id ledger, in the order it opened the transactions.
	Plan []BoltTxTerminateRow

	// ListedAtCap is every id suffix the registry held with the whole ledger open;
	// ListedAfterTerminate is what it held once the victim had gone. Both are
	// SORTED, not in listing order — see the file comment on why the order is not
	// deterministic in an arm that never advances the clock.
	ListedAtCap          []string
	ListedAfterTerminate []string
	// RegistryPeak is the largest listing the run observed.
	RegistryPeak int

	// Calls are the terminate calls in the order they were made.
	Calls []BoltTxTerminateCall

	// SuccessorSuffix is the id suffix of the SECOND transaction the victim's
	// connection opened; WantSuccessorSuffix is what the harness predicted from
	// its BEGIN ordinal. SuccessorListed and BystanderListed record whether each
	// was still listed after the stale-vs-successor terminate had settled.
	SuccessorSuffix     string
	WantSuccessorSuffix string
	SuccessorListed     bool
	BystanderListed     bool

	// VictimCode and VictimMessage are what the terminated connection was told on
	// the one message sent to it after the termination. They are what attributes
	// its departure to the operator call rather than to a rollback or a dropped
	// connection — and they are adjudicated against [txTerminateFailureCode] and
	// [txTerminateFailureMessage], which since rmp #2560 name the OPERATOR event
	// specifically. They used to be adjudicated against the reap pair, both of
	// whose halves were false here: no timeout had elapsed, and the writer lock the
	// message named was retired by rmp #2305/#2306.
	VictimCode    string
	VictimMessage string

	// TermFrames and TermBytes bracket the termination itself with [wal.Stats].
	// A rollback must append neither.
	TermFrames uint64
	TermBytes  uint64

	// Windows are the honest autocommit writes that bracket the termination.
	Windows []BoltTxWriteWindow

	// GhostsLive/GhostsRecovered count [txTerminateGhostLabel] in the live engine
	// and after a crash and a real WAL replay; Honest* and Committed* do the same
	// for the two witness labels.
	GhostsLive         int
	GhostsRecovered    int
	HonestLive         int
	HonestRecovered    int
	CommittedLive      int
	CommittedRecovered int
}

type BoltTxTerminateRow struct {
	// Role is the row's part in the arm: one of [txTerminateRoles].
	Role string
	// Principal is the identity the connection authenticated as, and the only
	// field that can attribute a listing entry to a connection (Remote is the same
	// constant on every SimConn).
	Principal string
	// Mode is the BEGIN access mode, "r" or "w", exactly as sent.
	Mode string
	// Query is the single statement run inside the transaction.
	Query string
	// IDSuffix is the per-server sequence suffix taken from the OBSERVED id;
	// WantSuffix is the suffix the harness predicted from the BEGIN's ordinal on
	// this server. The id's prefix is crypto/rand and is never recorded.
	IDSuffix   string
	WantSuffix string
	// Conn is the connection's index in the ledger, 0-based.
	Conn int
}

type BoltTxWriteWindow struct {
	// Name is the window's position in the run: one of [txAbandonWindows].
	Name string
	// Node is the name property the window wrote, unique per window.
	Node string
	// FramesBefore/FramesAfter and BytesBefore/BytesAfter bracket the window with
	// [wal.Stats].
	FramesBefore, FramesAfter uint64
	BytesBefore, BytesAfter   uint64
	// OpenTx is how many abandoned transactions the registry listed when the
	// window ran. It is what proves the window sat where its name says.
	OpenTx int
	// Ordinal is the advance ordinal the window ran after; 0 before the measured
	// sequence began.
	Ordinal int
	// Committed records that the server answered SUCCESS to both the RUN and the
	// PULL.
	Committed bool
}

type BoltVersionAbuse struct {
	// Name identifies the probe.
	Name string
	// Kind classifies the reply (`FAILURE`, `SUCCESS`, `IGNORED`, `CLOSED`).
	Kind string
	// Code and Message are the FAILURE's fields, empty when there was none.
	Code    string
	Message string
}

type BoltVersionArm struct {
	// Name is the target's name (`4.4`).
	Name string
	// Asked is the version the arm set out to negotiate.
	Asked proto.Version
	// Canonical is what the CANONICAL spelling (exact version, slot 0, range 0)
	// negotiated, and Spelled what the SEED-CHOSEN spelling negotiated. Both must
	// equal Asked; recording them separately is what makes
	// `arm-spelling-invariant` a comparison rather than a restatement.
	Canonical proto.Version
	Spelled   proto.Version
	// Spelling renders the seed-chosen offer preamble, and SpellingDiffers
	// reports whether it differed from the canonical one at all — the non-vacuity
	// question for the invariance clause.
	Spelling        string
	SpellingDiffers bool
	// NegotiateErr classifies a handshake failure, empty on success.
	NegotiateErr string

	// Auth holds the authentication script's outcomes.
	Auth BoltVersionAuthProbes

	// Entity holds the entity-encoding capture.
	Entity BoltVersionEntity
	// Temporals holds one entry per temporal kind, in a fixed order.
	Temporals []BoltVersionTemporal

	// Params are the decoded round-trip values for each parameter kind, in the
	// fixed order of [boltVersionParamCases]. They are compared across versions
	// by value AND by concrete Go type, following rmp #2484: the dynamic type IS
	// the wire encoding, so an Integer silently replaced by the
	// identically-rendered Float must fail.
	Params []any
	// ParamErr classifies a round-trip failure, empty on success.
	ParamErr string

	// TxCommitted reports whether the arm's explicit BEGIN/RUN/COMMIT committed,
	// TxBookmark the bookmark its COMMIT returned (rendered positionally; see the
	// file comment), and TxCountAfter the number of marker nodes visible
	// immediately afterwards.
	TxCommitted  bool
	TxBookmark   string
	TxCountAfter int
	// TxErr classifies a transaction-script failure, empty on success.
	TxErr string

	// Abuse holds one entry per malformed/ill-timed probe, in the fixed order of
	// [boltVersionAbuseCases]: the code and message the server answered.
	Abuse []BoltVersionAbuse
}

type BoltVersionAuthProbes struct {
	// HelloGoodKind / HelloGoodCode: a HELLO carrying the CORRECT credentials.
	HelloGoodKind string
	HelloGoodCode string
	// RunAfterHello*: a RUN sent immediately after that HELLO, with no LOGON.
	RunAfterHelloKind    string
	RunAfterHelloCode    string
	RunAfterHelloMessage string
	// HelloWrong*: a HELLO carrying a WRONG password, on its own connection.
	HelloWrongKind string
	HelloWrongCode string
	// WrongHelloConnAlive reports whether the connection survived that HELLO. At
	// the inline-auth versions a failed HELLO makes the session DEFUNCT and the
	// serve loop closes the socket (bolt/server/session.go:911), so the next write
	// fails; at the deferred-auth versions HELLO never authenticated, so it
	// cannot have refused and the connection is intact.
	WrongHelloConnAlive bool
	// HelloBareKind / HelloBareCode: a credential-LESS HELLO, on its own
	// connection.
	HelloBareKind string
	HelloBareCode string
	// LogonKind / RunAfterLogonKind: the LOGON that follows that bare HELLO where
	// the version allows one, and a RUN after it.
	LogonKind         string
	RunAfterLogonKind string
	// ResetAfterHelloKind / RunAfterReset*: a RESET sent on a session that has
	// completed HELLO but not LOGON, and the RUN that follows it.
	ResetAfterHelloKind  string
	RunAfterResetKind    string
	RunAfterResetCode    string
	RunAfterResetMessage string
}

type BoltVersionEntity struct {
	// Census is every (tag, arity) in the record, in encounter order, as the
	// independent reader saw it.
	Census []boltWireWidth
	// CodecCensus is the same, as the module's own decoder saw it. The two must
	// agree; see `encoding-walker-agrees-with-codec`.
	CodecCensus []boltWireWidth
	// Bytes is the record's length on the wire. It is a coarse but completely
	// independent witness that the two versions did not emit the same message.
	Bytes int
	// NodeID / NodeLabels / NodeProps are the returned node's version-INVARIANT
	// core.
	NodeID     int64
	NodeLabels []string
	NodeProps  map[string]any
	// RelID / RelStart / RelEnd / RelType / RelProps are the returned
	// relationship's version-invariant core.
	RelID    int64
	RelStart int64
	RelEnd   int64
	RelType  string
	RelProps map[string]any
	// PathNodeIDs / PathRelIDs / PathIndices are the returned path's
	// version-invariant core.
	PathNodeIDs []int64
	PathRelIDs  []int64
	PathIndices []int64
	// ElementIDs are the trailing element_id strings, in encounter order: the
	// node's, then the relationship's three, then the path's. It is EMPTY at the
	// Bolt 4 layout, which is itself the assertion.
	ElementIDs []string
	// Err classifies a capture failure, empty on success.
	Err string
}

type BoltVersionMatrixEvidence struct {
	// Negotiations are the raw-preamble probes in the order they ran.
	Negotiations []BoltVersionNegotiation
	// Supported is what [proto.SupportedVersions] advertised at collection time,
	// compared against [boltVersionSupportedTripwire].
	Supported []proto.Version
	// Arms are the per-version arms in the order of [boltVersionTargets].
	Arms []BoltVersionArm
	// TemporalRef is the harness's OWN reference for every temporal value the
	// scenario asks for, computed with Go's time package from the same literals
	// the query carries. It is what makes the temporal clauses independent of the
	// encoder they adjudicate. NamedZoneResolved is false when the zone database
	// was unavailable, which the non-vacuity gate reports as a shortfall rather
	// than letting the named-zone clause pass unexercised.
	TemporalRef       BoltVersionTemporalRefs
	NamedZoneResolved bool
	// LiveMarkers and RecoveredMarkers are the marker nodes each version
	// committed, as counted in the live engine and in a graph reopened through
	// real WAL recovery after a crash. The maps are keyed by the version name the
	// client itself wrote into the node.
	LiveMarkers      map[string]int
	RecoveredMarkers map[string]int
	// Seed is the seed the run was built from.
	Seed uint64
}

type BoltVersionNegotiation struct {
	// Name identifies the case in a violation message.
	Name string
	// Slots renders the four offer slots as the client wrote them, so a failure
	// says what was actually sent rather than what the case was named.
	Slots string
	// Accepted is true when the server answered a non-zero version.
	Accepted bool
	// Got is the version the server answered (zero when it refused).
	Got proto.Version
	// ReadErr classifies a failure to read the 4-byte reply, empty when it
	// arrived. It is a CLASSIFICATION and not the raw error text, so the
	// rendering stays a function of the seed.
	ReadErr string
}

type BoltVersionTemporal struct {
	// Kind names the value (`date`, `datetime-offset`, …).
	Kind string
	// Tag is the PackStream structure signature.
	Tag byte
	// Ints are the structure's integer fields in order.
	Ints []int64
	// Zone is the trailing IANA zone name for a named-zone datetime, empty
	// otherwise.
	Zone string
	// Err classifies a capture failure, empty on success.
	Err string
}

type BoltVersionTemporalRefs struct {
	// EpochDay is date('2020-01-02') as whole days since the Unix epoch.
	EpochDay int64
	// NanosOfDay is '03:04:05.000000006' as nanoseconds since midnight, shared by
	// the localtime and time values.
	NanosOfDay int64
	// LocalAsUTCSec is the localdatetime's wall clock read as if it were UTC,
	// which is what a zone-less local datetime carries on the wire.
	LocalAsUTCSec int64
	// OffsetUTCSec / OffsetNanos / OffsetSeconds describe the offset-zone
	// datetime: the true UTC epoch second, the sub-second part, and the zone
	// offset.
	OffsetUTCSec  int64
	OffsetNanos   int64
	OffsetSeconds int64
	// Named describes the named-zone datetime the same way. It is meaningful only
	// when the zone database resolved; see
	// [BoltVersionMatrixEvidence.NamedZoneResolved].
	Named BoltVersionZoneRef
	// Duration is the duration's four fields in wire order.
	Duration []int64
}

type BoltVersionZoneRef struct {
	// UTCSeconds is the true UTC epoch second, Nanos the sub-second part, and
	// OffsetSeconds the zone's offset from UTC at that instant.
	UTCSeconds    int64
	Nanos         int64
	OffsetSeconds int64
}

type BoundedChurnWriter struct{}

type CSRHeaderFacts struct {
	// NVertices and NEdges are the two little-endian uint64 counts that open the
	// file. NVertices includes the trailing sentinel offset.
	NVertices uint64
	NEdges    uint64
	// Width is the weightSizeBytes header byte: 1, 2, 4 or 8 for the dense native
	// weights column, 0 when there are no weights, and 0xFF
	// (store/snapshot's weightSizeCodec) for the variable-width codec-encoded
	// section rmp #2526 added.
	Width uint8
	// HasWeights is the hasWeights header byte, decoded as a bool.
	HasWeights bool
}

type CertRotationStep struct {
	// Name identifies the step in a violation message.
	Name string
	// WantCN is the Common Name that MUST be in service after this step: the newly
	// installed pair for a step expected to succeed, the previous one for a step
	// expected to fail.
	WantCN string
	// ServedCN is the Common Name actually served by GetCertificate afterwards.
	ServedCN string
	// ReloadErr is the error Reload returned, rendered ("" when it succeeded).
	ReloadErr string
	// HandshakeErr is the error the verifying TLS handshake returned, rendered
	// ("" when the handshake completed).
	HandshakeErr string
	// KeyBytes is the size of the key file this step left on disk, and KeyWantBytes
	// the size of the key the step was WRITING. They exist so the fault a step
	// claims to inject is proven distinct from its neighbour's: a torn key is
	// SHORTER than the key it truncates, a garbled one is exactly as long. Without
	// them two steps could quietly inject the same fault — they already produce the
	// same parse error — and the roster would overstate what was covered.
	KeyBytes, KeyWantBytes int
	// WantReloadOK records the step's INTENT: true when the pair on disk is
	// complete and valid, false when the step deliberately broke it.
	WantReloadOK bool
	// ReloadOK records what actually happened.
	ReloadOK bool
	// CertMTimeUnixNano / KeyMTimeUnixNano are the mtimes the step's mutation left
	// on disk, or 0 when the file is absent. They exist for the preserved-mtime arm:
	// that arm's whole claim is that the rotation did NOT advance the mtime, and
	// without recording it the arm would silently degrade into an ordinary rotation
	// the moment the projection changed.
	CertMTimeUnixNano int64
	KeyMTimeUnixNano  int64
	// ValidityRefused records whether the reload was refused BECAUSE the leaf on
	// disk was outside its validity window — matched with [errors.Is] against
	// [server.ErrCertOutsideValidity], not by reading the message. Without it the
	// expired arms would be satisfied by ANY refusal, including a parse failure,
	// and a shared failure signal cannot attribute a refusal to its cause.
	ValidityRefused bool
	// WantValidityRefused is the step's INTENT for [CertRotationStep.ValidityRefused].
	WantValidityRefused bool
	// Handshook records whether a real TLS handshake completed against the served
	// certificate. It must be true after EVERY step, successful or not: a broken
	// rotation may not change the certificate, and may not break the one in
	// service either.
	Handshook bool
}

type CheckSelection struct {
	// IndexSpecs are the (Label, Property) indexes the consistency check walks.
	// They are declared by the scenario because the engine's index manager
	// exposes only opaque names, not (label, property) pairs.
	IndexSpecs []IndexSpec
	// IndexConsistency runs the full index-vs-base-data consistency check
	// ([CheckIndexConsistency]) at the end of the run (and, for the schema-chaos
	// scenario, after DDL churn). It is meaningful only for modes that exercise
	// indexes. The set of indexes to cross-check is [CheckSelection.IndexSpecs].
	IndexConsistency bool
	// Search runs the search-algorithm battery ([CheckSearch]) — structural
	// parity between the engine graph and the oracle model, per-algorithm
	// correctness against independent naive references, and the
	// context-cancellation contract of every public context-accepting entry point
	// in the five search packages — once at the end of the run. The search scenario also sets [Scenario.SearchEvery] for periodic
	// in-loop checks. It is meaningful only for the deterministic mode (the
	// battery needs a consistent, quiescent view of the graph).
	Search bool
}

type CheckpointCadenceConfig struct {
	// Seed is the master seed for the SimDisk sub-stream.
	Seed uint64
	// Arm names the variant under test. Empty defaults to
	// [ArmCheckpointCadenceClean].
	Arm string
	// MaxAge and Interval are the cadence geometry handed to
	// [checkpoint.Config]. Zero values take [cadenceMaxAge] and
	// [cadenceInterval]; a NEGATIVE MaxAge is how the interval-only control asks
	// for MaxAge: 0 without colliding with the "unset" meaning of zero.
	MaxAge   time.Duration
	Interval time.Duration
	// FaultOnCadenceFire arms a one-shot fsync fault immediately before the
	// faulted window, so exactly one periodic fire fails inside its snapshot
	// publish — before the WAL is synced and long before the prefix truncate.
	FaultOnCadenceFire bool
	// SkipTriggerPhase omits the explicit-trigger phase (and therefore the
	// age-timer question). The interval-only control uses it: with no MaxAge there
	// is no age timer to reset.
	SkipTriggerPhase bool
}

type CheckpointCadenceEvidence struct {
	// Arm is the variant that produced this evidence.
	Arm string

	// MaxAgeNS and IntervalNS are the geometry read back off the CONSTRUCTED
	// checkpointer's behaviour plan, not off the request: [checkpoint.New]
	// derives Interval from MaxAge when it is left at zero.
	MaxAgeNS   int64
	IntervalNS int64

	// TickersRegistered is how many tickers the loop took from the injected
	// clock. It must be 1: the cadence is on the seam, not on wall time.
	TickersRegistered int64
	// ClockNowCalls and ClockSinceCalls are the loop's total use of the seam, and
	// GateReadsOnTicks the part of it made while a TICK was being serviced. The
	// split matters: with MaxAge unset the age gate short-circuits before reading
	// the clock, so GateReadsOnTicks is 0 on that arm while the run's own explicit
	// trigger still moves the totals.
	ClockNowCalls    int64
	ClockSinceCalls  int64
	GateReadsOnTicks int64
	// SimulatedElapsedNS is how much FAKE time the run advanced, and
	// RealElapsedNS how long it took on the wall clock. The pair is the witness
	// that the cadence is virtual: the simulated total is a large multiple of
	// MaxAge whatever the real one happens to be.
	SimulatedElapsedNS int64
	RealElapsedNS      int64

	// The frozen-clock control, taken with the loop running and the ticker
	// registered: FrozenWindowNS of REAL time in which the fake clock did not
	// move.
	FrozenWindowNS     int64
	FrozenWindowFires  uint64
	FrozenWindowSinces int64

	// Ticks is how many one-interval advances the run made and TicksDelivered how
	// many of them the fake clock actually delivered to a waiter, measured with the
	// harness's own probe ticker on the same clock at the same period. The pair is
	// what makes "nothing fired" a statement about the AGE GATE rather than about a
	// tick that never arrived.
	Ticks          int
	TicksDelivered int
	// TriggerCalls is how many explicit [checkpoint.Checkpointer.Trigger] calls the
	// run issued, and TriggeredFires how many of those returned nil (and so
	// incremented the checkpoint counter).
	TriggerCalls   int
	TriggeredFires int
	// Checkpoints is the checkpointer's own lifetime counter at the end, and
	// CadenceFires the arithmetic attribution: the checkpoints this run did not
	// ask for.
	Checkpoints  uint64
	CadenceFires int

	// FireTicks are the tick ordinals at which the loop RAN a checkpoint —
	// successful or failed — observed as a change in the checkpoint counter or in
	// LastError. PredictedFireTicks are the ordinals the independent model
	// predicts, and PredictedFireTicksNoReset the ordinals the rival hypothesis
	// (an explicit trigger does NOT reset the age timer) predicts.
	FireTicks                 []int
	PredictedFireTicks        []int
	PredictedFireTicksNoReset []int

	// TriggerTick is the tick ordinal after which the explicit trigger was
	// issued (0 when the arm skipped that phase), and UnresetFireTick the ordinal
	// at which the rival hypothesis would have fired. FiredAtUnresetTick records
	// whether it did.
	TriggerTick                   int
	UnresetFireTick               int
	FiredAtUnresetTick            bool
	TicksFromTriggerToCadenceFire int

	// The transient failure. FailedFireTick is the ordinal whose fire failed (0
	// if none did), FailedFireErr what [checkpoint.Stats.LastError] then held, and
	// RetryFireTick the ordinal at which the next cadence fire ran.
	FaultArmed              bool
	FailedFireTick          int
	FailedFireErr           string
	FailedFireIsSimFault    bool
	TicksFromFailureToRetry int
	RetryFireTick           int
	// LastErrorAfterRetry is what LastError held once the retry had succeeded:
	// the answer to "does a success clear it".
	LastErrorAfterRetry string

	// The counters bracketing the failure. A failed fire must advance neither.
	CheckpointsBeforeFailure uint64
	CheckpointsAfterFailure  uint64
	WALTruncBeforeFailure    uint64
	WALTruncAfterFailure     uint64
	WALTruncAfterRetry       uint64
	// WALBytesBeforeFailure and WALBytesAfterFailure are the DURABLE WAL image on
	// the SimDisk across the failed fire. It must not shrink: a checkpoint that
	// did not publish must not have reclaimed anything.
	//
	// On a fault-free arm these three pairs bracket the same window with no failure
	// in it — the fire inside it succeeds and legitimately reclaims the prefix — so
	// they are informational there and the clauses that read them are gated on
	// FailedFireTick.
	WALBytesBeforeFailure int
	WALBytesAfterFailure  int

	// CheckpointsNonMonotonic and WALTruncNonMonotonic record whether either
	// lifetime counter was ever observed to DECREASE across the run's samples.
	CheckpointsNonMonotonic bool
	WALTruncNonMonotonic    bool
	// WALTruncTotal is the reclaimed prefix at the end — the checkpoint redo
	// position the WAL control file records (see cpCadenceEnv.walTrunc) — and
	// WALTruncAdvances how many samples it strictly increased at. The
	// WALTrunc* fields above read the same measure.
	WALTruncTotal    uint64
	WALTruncAdvances int

	// AckedKeys are every key acknowledged during the run and MissingAckedKeys
	// those the reopen could not find. MissingAckedKeys non-empty is a durability
	// defect.
	AckedKeys        []string
	MissingAckedKeys []string
	// AckedDuringFailure is how many commits were acknowledged while the
	// checkpointer was in its failed state, and AckedAfterLastCheckpoint how many
	// landed after the final fire and so live only in the WAL suffix.
	AckedDuringFailure       int
	AckedAfterLastCheckpoint int
	// RecoveredWALOps is how many WAL ops the reopen's recovery replayed, WALBytes
	// the durable image it read, and SnapshotPublished whether a snapshot manifest
	// sits beside it.
	RecoveredWALOps   int
	WALBytes          int
	SnapshotPublished bool
	// ReopenClean is whether the reopen's recovery found no genuine corruption.
	ReopenClean bool
}

type CheckpointConfig struct {
	// Dir is the SimDisk directory the snapshot and WAL live under. A non-empty
	// dir places the WAL at dir/wal and the snapshot at dir/snapshot. When empty
	// it falls back to [defaultCheckpointDir].
	Dir string
	// Every is the tick cadence between checkpoints. A non-positive value falls
	// back to [defaultCheckpointEvery]. The first checkpoint fires at the first
	// tick that is a positive multiple of Every.
	Every int
	// Enabled turns in-loop checkpointing on. When true the durable store is
	// opened in full-stack mode and the loop checkpoints on the cadence below.
	Enabled bool
}

type ConcurrentConfig struct {
	// Mix selects the per-connection actor behaviour. When nil, an honest
	// read/write mix is used.
	Mix *ConcurrentMix
	// Seed controls WHAT each connection sends and WHEN its faults fire. Goroutine
	// interleaving is NOT seed-controlled (see the package note on the hybrid
	// determinism model): this mode is robustness/liveness/leak-checked, not
	// bit-reproducible.
	Seed uint64
	// Connections is the number of concurrent client connections (one goroutine
	// each). Values <= 0 are normalised to 1.
	Connections int
	// OpsPerConn is the number of operations each connection performs before it
	// closes. Values <= 0 are normalised to 1. For the transactional roles one
	// operation is one whole transaction.
	OpsPerConn int
	// ContendedCounters is the size of the shared counter key space the
	// contended transactional role collides on (rmp #2439). Values <= 0
	// normalise to 2. Fewer counters means more conflicts.
	ContendedCounters int
	// ContendedNamespace separates this run's shared counters from every other
	// run's (rmp #2729). The counters are shared by every CONNECTION of this
	// run — that sharing is what the contended role exists to create — and by no
	// other run, whose acknowledged tally would otherwise be adjudicated against
	// a value another run had also incremented.
	//
	// Name it when several sequential [RunConcurrent] calls form ONE logical run
	// that must keep the same counters — [runProductionProfileEvidence] does,
	// because it accumulates each counter's total across crash cycles over one
	// durable store. Leave it empty and the namespace is derived from Seed, which
	// is already distinct per call in every caller that drives one shared server
	// concurrently.
	//
	// A namespace is leased to one run at a time per server: an overlapping run
	// that asks for a namespace already held is refused with a typed error rather
	// than left to corrupt both oracles.
	ContendedNamespace string
}

type ConcurrentMix struct {
	// WriterWeight, ReaderWeight, OverloadWeight are the relative weights for the
	// three honest-ish roles. They need not sum to 1.
	WriterWeight   float64
	ReaderWeight   float64
	OverloadWeight float64
	// TxWriterWeight selects the DISJOINT transactional writer (rmp #2439):
	// explicit multi-statement transactions over the real Bolt wire (BEGIN, one
	// to three uniquely-named creates, COMMIT or a seed-chosen ROLLBACK), whose
	// keys never collide with another connection's.
	TxWriterWeight float64
	// TxContendedWeight selects the CONTENDED transactional writer: an explicit
	// read-modify-write on a small shared counter space (the lost-update shape)
	// plus a unique marker create, so serialization conflicts are an expected,
	// typed outcome the run accounts for separately from failures.
	TxContendedWeight float64
	// BatchWriterWeight selects the atomic-batch writer (rmp #2440): one
	// explicit transaction of exactly isoBatchSize tagged creates, always
	// committed, so readers can assert batch-multiple visibility.
	BatchWriterWeight float64
	// IsoReaderWeight selects the during-run oracle reader (rmp #2440):
	// per-connection monotonic reads over the shared counters and the
	// batch-multiple atomic-visibility check.
	IsoReaderWeight float64
	// RYOWWriterWeight selects the read-your-own-writes probe role
	// (rmp #2440): write then immediately read back on the same connection.
	RYOWWriterWeight float64
	// OverloadHeavyWrites lets the overload role draw the heavy-WRITE family
	// [OverloadLargeCreateTx] instead of mapping it to a read (rmp #2736). It
	// is the write half of the graceful-degradation mandate: a read-only
	// overload population cannot establish that a large legitimate WRITE is
	// either served in full or refused with a typed error.
	//
	// It is opt-in rather than the default for a measured reason, not a
	// cautious one. A heavy write is ~6-10 ms and ~1.2 MiB of engine heap
	// against ~5 us for a read family whose connection is already in the Bolt
	// FAILED state, so enabling it everywhere would multiply the cost of every
	// caller that leaves Mix nil — including bench/contention's
	// dst-concurrent-bolt, whose operation count is calibrated on a documented
	// ~2.6 ms per operation. Callers whose subject IS heavy-write saturation
	// ask for it by name; the catalogue's "overload" scenario does.
	//
	// The population stays neutral either way: an enabled run tags, adjudicates
	// and then removes each heavy write's nodes, so the node-count oracle of
	// [ConcurrentResult.Consistent] holds unchanged and nothing accumulates.
	OverloadHeavyWrites bool
}

type ConcurrentResult struct {
	// AckedNames is the UNION, across every writer connection, of the unique
	// node names whose create was acknowledged (a SUCCESS-terminated PULL). It is
	// the durability oracle at the NAME granularity the durable-commit crash
	// scenario needs: every name here MUST survive a crash+recovery (recovered ⊇
	// acked). Each writer op uses a globally-unique name and is never retried, so
	// the union is a set with no duplicates. Populated only for the writer role;
	// nil-safe for read/overload-only runs (stays empty).
	AckedNames []string
	// IssuedNames is the UNION of every create name a writer connection SENT
	// (called RUN for), regardless of outcome. It is the phantom oracle: a
	// recovered name absent from IssuedNames would be a phantom the durable layer
	// invented (recovered ⊆ issued).
	IssuedNames []string
	// FailedNames is the UNION of every create name whose client observed an
	// explicit typed FAILURE (a [proto.Failure] at RUN or as the PULL terminal).
	// It is the atomicity oracle: a commit the client saw fail must have applied
	// nothing durable, so every FailedNames entry MUST be absent after recovery.
	// A name that received an IGNORED terminal (the connection was already in the
	// Bolt FAILED state) is deliberately NOT recorded here — its outcome is
	// ambiguous, so it is left as merely issued, never asserted-absent.
	FailedNames []string

	// TxMarkersAcked / TxMarkersRefused are the transaction-granular ledgers
	// (rmp #2439): the unique marker names created inside transactions whose
	// COMMIT the server acknowledged, and inside transactions the server
	// REFUSED (a typed conflict, an explicit rollback, or a failed commit).
	// At quiescence every acked marker must be present and every refused
	// marker absent — the all-or-nothing assertion at transaction granularity.
	TxMarkersAcked   []string
	TxMarkersRefused []string
	// ContendedAcked is, per shared counter, the number of read-modify-write
	// increments acknowledged; ContendedFinal is each counter's value read at
	// quiescence. Equality is the zero-lost-updates oracle.
	//
	// The equality holds only because the counters are private to this run's
	// namespace (rmp #2729): a counter another concurrent run also incremented
	// answers for increments this run never acknowledged, and the oracle would
	// then report a lost update that never happened — or, with a run that
	// acknowledged nothing readable, report nothing at all.
	//
	// Both are ALWAYS ConcurrentCounters long, on every path, so a caller may
	// index them by the same k without checking (rmp #2552). A counter no
	// connection touched reads 0 rather than being absent.
	ContendedAcked []int64
	ContendedFinal []int64
	// ContendedConnections is how many connections the seeded role draw gave the
	// contended-writer role. It is POPULATION evidence, not a result: a run that
	// drew none never touches a shared counter, so any counter oracle over it is
	// vacuous — and the harness must still produce well-formed counter evidence
	// for it. It is what lets a test assert it really entered that case instead
	// of replicating the draw and hoping (rmp #2552).
	ContendedConnections int

	Seed             uint64
	Connections      int
	AckedCreates     int64 // nodes connections committed (eventual oracle)
	EngineNodeCount  int64 // engine's live node count at quiescence
	Panics           int64 // recovered panics across all connection goroutines (must be 0)
	TransportErrors  int64 // unexpected transport errors (must be 0 on a healthy run)
	BoundedRejects   int64 // typed bound errors (overload caps) — acceptable, not a fault
	BaselineRoutines int   // goroutine count captured before the run
	FinalRoutines    int   // goroutine count after teardown

	// Transaction outcome accounting (rmp #2439). TxIssued counts explicit
	// transactions BEGUN; every one ends in exactly one bucket: committed
	// (COMMIT acknowledged), conflicted (the typed retriable serialization
	// conflict, classified by its Bolt code), rolled back (a deliberate
	// client ROLLBACK), failed (any other explicit FAILURE), or ambiguous
	// (the connection stopped mid-transaction on a transport error or
	// cancellation — its outcome is unknowable client-side and is never
	// asserted). Conservation: TxIssued == the sum of the five.
	TxIssued     int64
	TxCommitted  int64
	TxConflicted int64
	TxRolledBack int64
	TxFailed     int64
	TxAmbiguous  int64
	// TxMissingAcked / TxPhantomRefused are the quiescence verification
	// outcomes: acknowledged markers absent from the engine, and refused
	// markers present in it. Both must be zero.
	TxMissingAcked   int64
	TxPhantomRefused int64

	// During-run isolation oracle tallies (rmp #2440), reconciled from the
	// per-connection state after the join and asserted zero on HEAD:
	// a monotonic-read regression (a shared counter or the batch population
	// observed going backwards on one connection), a same-connection
	// read-your-own-writes miss, and a torn atomic batch (a count that is not
	// a multiple of the batch size).
	IsoMonotonicViolations int64
	IsoRYOWViolations      int64
	IsoBatchViolations     int64
	// IsoReads counts the oracle observations actually made, so a green run
	// is provably non-vacuous.
	IsoReads int64

	// Heavy-write overload ledger (rmp #2736), populated only when the mix set
	// [ConcurrentMix.OverloadHeavyWrites]:
	//
	//   - OverloadHeavyIssued / OverloadHeavyAcked — heavy-write transactions
	//     SENT, and those whose commit the server acknowledged. Issued is the
	//     non-vacuity evidence: a run that reports zero drew the family never,
	//     so any heavy-write claim over it is empty.
	//   - OverloadHeavyIgnored — heavy writes the server DISCARDED because the
	//     connection was still in the Bolt FAILED state from an earlier bound.
	//     Nothing reached the engine, so such an attempt exercises nothing; it
	//     must be zero, and it is the tally that distinguishes a heavy write
	//     the engine refused from one that was never issued.
	//   - OverloadHeavyAdjudications — how many of them had their committed
	//     population actually counted. It is to the violations below what
	//     IsoReads is to the isolation violations: a green run with zero
	//     adjudications proved nothing.
	//   - OverloadHeavyViolations — heavy writes whose committed population did
	//     not match their acknowledgement (all of the batch on an acknowledged
	//     commit, none of it on a refusal). Must be zero, and breaks
	//     [ConcurrentResult.Consistent] when it is not.
	OverloadHeavyIssued        int64
	OverloadHeavyAcked         int64
	OverloadHeavyIgnored       int64
	OverloadHeavyAdjudications int64
	OverloadHeavyViolations    int64

	// WireParamFailures holds one description per divergence found by the Bolt
	// parameter type matrix ([probeWireParamTypes], rmp #2462): every PackStream
	// kind a driver can bind — String, Integer, Float, Boolean, Null, List, Map —
	// is sent over the real wire and verified by read-back before any connection
	// spawns. Empty on a clean run; a non-empty slice breaks [Consistent].
	WireParamFailures []string
}

type Config struct {

	// Workload is the actor mix. When nil, [DefaultWorkload] is used.
	Workload *Workload
	// OnOp, when non-nil, is called synchronously with each tick and the
	// operation about to run, before it is executed. It is an observation hook
	// (e.g. for verbose tracing); it must not mutate state or draw from any
	// randomness, or it would break reproducibility. It runs on the simulation
	// goroutine.
	OnOp func(tick int64, op Op)
	// OnCrash, when non-nil, is called synchronously after each crash+recovery
	// cycle with the crash tick and how many WAL ops recovery replayed. Like
	// OnOp it is an observation hook and must not mutate state or draw
	// randomness.
	OnCrash func(tick int64, replayedWALOps int)
	// Checkpoint configures deterministic, in-loop checkpointing of the
	// SimDisk-backed store. The zero value disables it (Enabled == false), so a
	// run that does not opt in is byte-identical to before. When enabled, the
	// durable store is opened in FULL-STACK mode (WAL + snapshot under a checkpoint
	// directory) and the loop publishes a real snapshot + truncates the WAL prefix
	// every [CheckpointConfig.Every] ticks, so a subsequent crash recovers through
	// the full snapshot+WAL path. It requires the durable store, so it implies the
	// SimDisk-backed stack even when [Config.Crash] is disabled. See
	// [CheckpointConfig].
	Checkpoint CheckpointConfig
	// EngineOpts configures the in-memory engine the deterministic loop drives
	// (the non-crash, non-disk path). The zero value is byte-identical to
	// [cypher.NewEngine], so a scenario that does not set it is unaffected. The
	// mem-pressure scenario clamps the logical-resource budgets here
	// (MaxResultRows / MaxResultBytes / MaxCollectItems) so over-budget ops are
	// refused with a typed error, exercising graceful degradation deterministically.
	// It is applied only on the in-memory path; the durable (crash/disk) path uses
	// the recovery-config engine.
	EngineOpts cypher.EngineOptions
	// Crash configures deterministic crash/recovery injection. The zero value
	// disables it (Enabled == false), which is the safe default: a run that does
	// not opt in drives a plain in-memory engine exactly as before, byte for
	// byte. When enabled, the simulator instead drives a real SimDisk-backed
	// persistence stack (WAL append+sync + recovery replay) so a scheduled crash
	// drops the live engine and the store is reopened from the durable image.
	Crash CrashConfig
	// Disk, when its CapacityBytes > 0, bounds the SimDisk-backed durable store
	// to a finite size so the run drives the engine through a disk-full (ENOSPC)
	// condition on the real WAL append+sync path. A non-zero capacity implies the
	// durable store even when Crash is disabled; the zero value leaves the disk
	// unbounded (the prior behaviour). See [DiskConfig].
	Disk DiskConfig
	// Multigraph, when true, opens the engine's graph (durable and in-memory
	// alike) as a directed MULTIGRAPH, so a repeated CREATE between the same
	// endpoints adds a parallel edge instance instead of being rejected. Only a
	// scenario whose oracle models edges per instance may set it (the
	// edge-properties scenario, rmp #2449, discriminates instances by a unique
	// eid property); the default (false) keeps the simple-graph shape every
	// other scenario's (src,dst,label)-keyed oracle model requires, byte for
	// byte.
	Multigraph bool
	// Seed is the master seed; the entire run is a pure function of it.
	Seed uint64
	// MaxTicks is the number of ticks (operations) the safety phase runs.
	MaxTicks int
	// CheckEvery is the invariant-check cadence in ticks. Values <= 0 are
	// normalised to 1 (check every tick).
	CheckEvery int
	// contains filtered or unexported fields
}

type CountStoreConfig struct {
	Crash      CrashConfig
	Checkpoint CheckpointConfig
	Seed       uint64
	MaxTicks   int
	// ParityEvery is the tick cadence of the full cell-by-cell parity walk.
	ParityEvery int
	// ShapesEvery is the tick cadence of the four count(*) shapes.
	ShapesEvery int
	// Persons is how many Persons the prologue creates before the loop.
	Persons int
	// Hubs is how many additional Persons carry the never-churned [csLabelHub]
	// label. They are the nodes whose IN-side count cells stay EXACT under churn,
	// so the live DIn and T clauses have something to compare.
	Hubs int
	// MinEdgesForBoundClaim, when > 0, requires the run to have modelled at least
	// this many edges at some point, so the boundedness clause's "never |E|" half
	// rests on an |E| that actually grew. The short arm leaves it 0 (its budget
	// cannot grow |E| far); the soak arm sets it.
	MinEdgesForBoundClaim int64
}

type CountStoreEvidence struct {
	// LiveChecks / RecoveredChecks count the parity observations in each phase.
	// They are separate because the two phases assert DIFFERENT things: a run
	// with no recovered check never evaluated the self-heal claim at all.
	LiveChecks      int
	RecoveredChecks int
	// DirtyLiveChecks is how many live observations found a non-empty dirty set.
	// Without one, "the reopen cleared the dirty sets" is satisfied by a run that
	// never dirtied anything.
	DirtyLiveChecks int
	// NegativeLiveChecks is how many live observations held a negative cell, and
	// NegativeCellsSeen the total number of such cells across the run.
	NegativeLiveChecks int
	NegativeCellsSeen  int
	// NegativeArms is how many negative-cell fixtures the run constructed: one in
	// the prologue and one after every recovery, so the heal is witnessed on every
	// reopen rather than only on the first.
	NegativeArms int
	// HealedFromDirty counts recoveries whose IMMEDIATELY PRECEDING live
	// observation was dirty and whose post-recovery observation was clean — the
	// clause that makes the heal a measured transition rather than a static
	// property. HealedNegative is the same for a negative cell.
	HealedFromDirty int
	HealedNegative  int
	// CellFamilies[i] counts the live observations in which family i held at least
	// one cell, indexed by [csFamily]. A run that never populated `T` proved
	// nothing about the pair fan-out.
	CellFamilies [csFamilyCount]int
	// ComparedLive[i] / ComparedRecovered[i] count the model cells of family i that
	// were actually COMPARED — not skipped as dirty-covered — in each phase.
	//
	// These are the counters that matter, and they are separate from CellFamilies
	// for a measured reason: after a single DETACH DELETE the DIn and T families
	// are dirty for the deleted node's labels for the rest of the session, so a
	// live check can hold plenty of cells and compare none of them. The Hub label
	// exists to keep some of them exact; these counters are what prove it worked.
	ComparedLive      csCompared
	ComparedRecovered csCompared
	// DistinctTLabelsMax is the largest number of distinct labels ever seen in the
	// a-position of a `T` cell. One means the multi-label fan-out never happened,
	// so the `T` clause only ever compared the trivial single-label case.
	DistinctTLabelsMax int
	// ShapeProbes[i] counts the adjudications of shape i, ShapeCellChecks[i] the
	// subset that also compared the serving count-store cell, and
	// ShapeCellSkipped[i] the subset where that cell was dirty-covered and so
	// could not be compared. The skip counter is recorded rather than dropped: a
	// skip is a coverage deletion, and the only way to see how much of the run it
	// removed is to count it.
	ShapeProbes      []int
	ShapeCellChecks  []int
	ShapeCellSkipped []int
	// MaxCells / MaxEdges / MaxBound are the footprint measurements the
	// boundedness clause rests on. MaxEdgesAtMaxCells records the modelled edge
	// count at the observation that held the most cells, so the report can state
	// the ratio the design claims.
	MaxCells           int
	MaxEdges           int64
	MaxBound           int
	MaxEdgesAtMaxCells int64
	// Relabels is how many `SET`/`REMOVE` label ops the churn actor emitted (the
	// only route to `countRelabel`, hence to any dirty marking).
	Relabels int
	// Crashes / ForcedCrashes / Checkpoints are the recovery coverage the
	// recovered-phase clauses depend on.
	Crashes       int
	ForcedCrashes int
	Checkpoints   int
	// Digest folds every clause's (tick, clause, measured pair). It is the
	// scenario's reproducibility claim: same seed, same digest. It folds no
	// NodeID and no mapper key, both of which come from a process-global counter
	// and are not a function of the seed.
	Digest uint64
}

type CountStoreProbes struct {
	// contains filtered or unexported fields
}

type CountStoreWriter struct {
	// contains filtered or unexported fields
}

type CounterUniqueness int

type CoverageBucket struct {
	Dimension string
	Key       string
	Count     int
}

type CoverageSummary struct {
	// Buckets lists every tracked bucket (dimension-then-key sorted).
	Buckets []CoverageBucket
	// Exercised is the number of buckets with a non-zero count.
	Exercised int
	// Unexplored is the number of tracked buckets still at zero.
	Unexplored int
}

type CoverageTracker struct {
	// contains filtered or unexported fields
}

type CrashConfig struct {
	// Enabled turns crash injection on. When false the schedule never fires and
	// never draws from the seed, so the workload stream is unperturbed.
	Enabled bool
	// CrashProb is the per-eligible-tick crash probability, clamped to [0,1].
	// A non-positive value falls back to [defaultCrashProb].
	CrashProb float64
	// StabilityWindow is the minimum tick gap enforced after a restart before
	// another crash may fire. A non-positive value falls back to
	// [defaultStabilityWindow].
	StabilityWindow int64
}

type CrashKind uint8

type CrashSchedule struct {
	// contains filtered or unexported fields
}

type CrossReleaseDiffResult struct {
	// Tag is the prior release compared against.
	Tag string
	// Divergences lists every op-level difference, each classified. A run can
	// agree overall while still carrying benign divergences here.
	Divergences []CrossReleaseDivergence
	// PriorNodes/PriorEdges/CurrentNodes/CurrentEdges are the end-state counts.
	PriorNodes   int64
	PriorEdges   int64
	CurrentNodes int64
	CurrentEdges int64
	// PriorCommits / CurrentCommits are how many ops each side reported as
	// committed. They are the commit axis's WITNESS: a run in which neither side
	// committed anything compares false against false for every op and would
	// agree vacuously — rmp #2729's failure mode, where 192 contended
	// transactions produced zero commits and the oracle compared 0 with 0 and
	// passed. A zero here is therefore itself a divergence.
	PriorCommits   int
	CurrentCommits int
	// Agreed reports whether no UNEXPECTED (non-benign) divergence occurred.
	Agreed bool
	// FinalCountsMatch reports whether the prior and current end-state counts
	// matched.
	FinalCountsMatch bool
}

type CrossReleaseDivergence struct {
	// Op is the diverging op.
	Op Op
	// PriorRows / CurrentRows are the two canonical row signatures.
	PriorRows   string
	CurrentRows string
	// Reason explains the classification.
	Reason string
	// Index is the op index that diverged. A negative index marks a divergence
	// about the run as a whole rather than about one op.
	Index int
	// Benign reports whether the divergence is an expected/benign class.
	Benign bool
	// PriorCommitted / CurrentCommitted are the two sides' COMMIT outcomes for
	// this op. They are meaningful on every divergence, and they are the whole
	// content of a divergence whose Reason names the commit axis.
	PriorCommitted   bool
	CurrentCommitted bool
}

type CrossReleaseUpgradeResult struct {
	// DataCompatError is set when the current code FAILED-STOP opening the prior
	// image (refused to recover it). This is the explicit, non-silent
	// data-compatibility signal: a clear error rather than a silent mis-recovery.
	DataCompatError error
	// Tag is the prior release that wrote the image.
	Tag string
	// CountMismatch is set when the current code OPENED the image but recovered
	// different node/edge counts than the prior release's own recovery — a genuine
	// current-code data-compatibility regression.
	CountMismatch string
	// PriorLiveNodes / PriorLiveEdges are the prior release's LIVE engine counts
	// after the write phase (before any reopen).
	PriorLiveNodes int64
	PriorLiveEdges int64
	// PriorSelfNodes / PriorSelfEdges are the counts the prior release's OWN
	// recovery rebuilds from the image — the durable truth the current code must
	// reproduce.
	PriorSelfNodes int64
	PriorSelfEdges int64
	// RecoveredNodes / RecoveredEdges are the CURRENT code's counts after reopen.
	RecoveredNodes int64
	RecoveredEdges int64
	// ReplayedWALOps is how many WAL ops the current recovery replayed.
	ReplayedWALOps int
	// PriorWALFidelityGap is true when the prior release's OWN recovery already
	// diverges from its live counts (its WAL does not round-trip in its own
	// release). This is a PRIOR-release defect, recorded but NOT charged to the
	// current code; the current/prior-self contract can still hold.
	PriorWALFidelityGap bool

	// HelperBuildFallbackErr is the error that forced the helper build to drop
	// its checkpoint half at this tag, or nil when the checkpoint-bearing build
	// succeeded. See [BuildPriorReleaseHelper].
	HelperBuildFallbackErr error
	// CheckpointErr is the prior release's own checkpoint failure, empty when the
	// checkpoint succeeded or was never attempted.
	CheckpointErr string
	// SnapshotProvenanceGap is set when the image carries a snapshot directory on
	// disk that the CURRENT recovery did not load, or loaded but could not parse.
	// It is the fault this task exists to be able to detect at all.
	SnapshotProvenanceGap string
	// PriorSnapshot is what the current manifest reader saw in the prior
	// release's snapshot directory, read straight off disk.
	PriorSnapshot PriorSnapshotFacts
	// SnapshotLabels / SnapshotProperties are how many label and property records
	// the prior release's snapshot components fed back into the recovered graph.
	SnapshotLabels     int
	SnapshotProperties int
	// HelperCheckpointBuilt reports that the helper for this tag was built WITH
	// its checkpoint half; false means the tag's checkpoint API did not match and
	// the image is WAL-only.
	HelperCheckpointBuilt bool
	// CheckpointPublished reports that the prior release actually published the
	// checkpoint (it built AND ran).
	CheckpointPublished bool
	// SnapshotOpened reports that the CURRENT recovery loaded a snapshot from the
	// image. Compared against [PriorSnapshotFacts.Present], which is read from
	// the filesystem, so "there was a snapshot and the reader ignored it" is a
	// distinguishable state rather than an unfalsifiable false.
	SnapshotOpened bool
	// SnapshotOnlyRecovery reports the strongest provenance outcome: a non-empty
	// graph recovered with a snapshot loaded and ZERO WAL ops replayed, so every
	// recovered node came through the prior release's snapshot bytes and the WAL
	// cannot account for any of it.
	SnapshotOnlyRecovery bool
}

type DBTeardownConfig struct {
	// Seed is the master seed for the SimDisk sub-stream.
	Seed uint64
	// Arm names the variant under test; it is carried into the evidence so the
	// non-vacuity gate can apply the concurrency floor to the arm that claims
	// concurrency. Empty defaults to [ArmDBTeardownConcurrentClosers].
	Arm string
	// Closers is how many goroutines call Close/CloseCtx simultaneously (< 1
	// normalises to [dbTeardownClosers]). Two further SERIAL calls always follow
	// them — a Close and then a CloseCtx — which is how the "Close after
	// CloseCtx" and "CloseCtx after Close" orderings are pinned by the same
	// identity clause.
	Closers int
	// CancelBeforeClose cancels the context handed to CloseCtx before any closer
	// runs. It also forces EVERY concurrent closer onto CloseCtx: with the
	// io.Closer Close() in the mix a background context could win the sync.Once
	// and the arm would silently stop testing cancellation.
	CancelBeforeClose bool
	// FinalCheckpoint wires [store.WithFinalCheckpoint], so step 1 of the
	// teardown exists at all and the context has something to bound.
	//
	// It belongs to the cancelled-context arm and to no other, which was MEASURED
	// rather than assumed: the final checkpoint folds the whole WAL suffix into a
	// fresh snapshot and truncates the WAL to nothing, so with it enabled the
	// reopen replayed 0 WAL ops and every acknowledged key came back from the
	// snapshot. An arm whose subject is the WAL CLOSE therefore leaves it off, so
	// its durability clause is answered by the WAL the close secured.
	FinalCheckpoint bool
	// FaultOnClose arms a one-shot fsync fault on the next Sync, which is the
	// WAL close's own fsync, so the teardown produces a NON-NIL error whose
	// identity is a discriminating observation. It is mutually exclusive with
	// InFlightCommit (both claim the next Sync ordinal) and is normally combined
	// with FinalCheckpoint disabled, so the fault cannot be eaten by a
	// checkpoint's fsync.
	FaultOnClose bool
	// InFlightCommit parks one commit inside its WAL fsync (a [SyncGate]) and
	// keeps it there while the closers run, so the teardown genuinely races an
	// in-flight writer rather than an idle store.
	InFlightCommit bool
	// SkipCheckpointerHandoff is the SENSITIVITY seam: the DB is built WITHOUT
	// [store.WithCheckpointer], so nothing joins the checkpoint goroutine. It
	// reproduces the leak the composed teardown exists to prevent, which is how
	// the join clause is proved to fire. The run stops the loop itself
	// afterwards, so the seam leaves no goroutine behind.
	SkipCheckpointerHandoff bool
	// Probe, when non-nil, is called after every closer has returned and BEFORE
	// the run stops anything the DB did not stop itself. It is the seam that
	// lets a test observe the goroutine population at the instant the teardown
	// claims the checkpoint loop is joined. It must not touch the store.
	Probe func()
}

type DBTeardownEvidence struct {
	// Arm is the variant that produced this evidence.
	Arm string
	// CloseErr renders the value every caller was expected to observe (the first
	// closer's), and CloseErrNil records whether it was nil.
	CloseErr string
	// PostCloseTriggerErr is what a checkpoint request returned after the
	// teardown, and PostCloseCommitErr what a commit attempt returned.
	PostCloseTriggerErr string
	PostCloseCommitErr  string
	// InFlightCommitErr is the error of the commit that was parked inside its
	// fsync while the closers ran (empty when it was acknowledged).
	InFlightCommitErr string
	// AckedKeys are the keys of the commits acknowledged BEFORE the teardown,
	// and MissingAckedKeys those the reopen could not find. MissingAckedKeys
	// non-empty is a durability defect.
	AckedKeys        []string
	MissingAckedKeys []string
	// Closers is the number of concurrent callers, SerialClosers the number of
	// serial calls made after them (always 2: a Close then a CloseCtx).
	Closers       int
	SerialClosers int
	// DistinctCloseErrs is how many distinct error VALUES the callers observed.
	// It must be 1: the teardown publishes one result.
	DistinctCloseErrs int
	// WriterClosedClosers counts callers whose error carried
	// [wal.ErrWriterClosed] — the signature of a second WAL close reaching a
	// caller.
	WriterClosedClosers int
	// TeardownBodyRuns is how many times the quiesce callback (and therefore the
	// WAL close inside it) was invoked. The sync.Once must make it exactly 1.
	TeardownBodyRuns int64
	// CloseCalls, CloseErrorMetric, FinalCheckpointErrorMetric and
	// TriggerCtxErrors are the DB's and the checkpointer's OWN instrumentation,
	// read independently of everything above: how many calls reached CloseCtx,
	// how often the teardown recorded an error (inside the Once), how often the
	// final checkpoint's error was classified as a genuine failure rather than a
	// benign cancellation, and how often TriggerCtx returned an error.
	CloseCalls                 uint64
	CloseErrorMetric           uint64
	FinalCheckpointErrorMetric uint64
	TriggerCtxErrors           uint64
	// Counters is every metric the recording sink saw across the teardown. It is
	// what the arm's [ScenarioCounterDecl] is adjudicated against, so the
	// coverage precondition reads the SAME observation the clauses above do.
	Counters MetricsObservation

	// CheckpointsBefore / CheckpointsAfter bracket the teardown, so the witness
	// can report whether step 1 actually folded under a cancelled context.
	CheckpointsBefore uint64
	CheckpointsAfter  uint64
	// WALBytes is the size of the durable WAL image at reopen and
	// SnapshotPublished whether a snapshot manifest sits beside it. Together they
	// are the shape floor: an assertion about recovery over an absent durable
	// image would be satisfied by definition.
	WALBytes int
	// AckedCommits is how many commits were acknowledged before the teardown, and
	// AckedAfterCheckpoint how many of those landed after the last checkpoint and
	// therefore live only in the WAL suffix.
	AckedCommits         int
	AckedAfterCheckpoint int
	// RecoveredWALOps is how many WAL ops the reopen's recovery actually
	// replayed. It is the independent proof that the durability clause was
	// answered by the WAL and not by the snapshot underneath it.
	RecoveredWALOps int
	// CtxCancelled records that the context handed to CloseCtx was already
	// cancelled, and CloseErrIsCtx that the close returned that cancellation.
	CtxCancelled  bool
	CloseErrIsCtx bool
	// CloseErrNil, CloseErrIsSimFault report the published value's shape.
	CloseErrNil        bool
	CloseErrIsSimFault bool
	// FaultArmed records that a one-shot fsync fault was armed on the WAL close.
	FaultArmed bool
	// FinalCheckpoint records that step 1 was wired at all.
	FinalCheckpoint bool
	// CheckpointerOwned records that the DB was given the checkpointer to stop
	// (false only on the sensitivity seam).
	CheckpointerOwned bool
	// LoopAliveBeforeClose is the liveness probe taken BEFORE the teardown: a
	// checkpoint request succeeded, so there was a goroutine to join.
	LoopAliveBeforeClose bool
	// LoopStoppedAfterClose is the join verdict: after the teardown a checkpoint
	// request returned [checkpoint.ErrCheckpointerStopped]. A WAL-closed error
	// instead means the loop was still alive and touched a closed WAL — the exact
	// failure store.DB exists to prevent.
	LoopStoppedAfterClose bool
	// PostCloseCommitRefused is whether a commit attempted after the teardown was
	// refused with [wal.ErrWriterClosed], which is how "the WAL is closed" is
	// observed from outside.
	PostCloseCommitRefused bool
	// PostCloseKeyRecovered is whether the key of that refused commit was found
	// in the reopened graph — an unacknowledged write that became durable.
	PostCloseKeyRecovered bool
	// InFlightGated / GateFired record that the boundary arm parked a commit
	// inside its fsync and that the rendezvous actually happened.
	InFlightGated bool
	GateFired     bool
	// CloseBlockedOnInFlight is the ordering observation: no closer had returned
	// while the commit was still parked.
	CloseBlockedOnInFlight bool
	// SnapshotPublished is whether a snapshot manifest exists on the disk.
	SnapshotPublished bool
	// ReopenClean is whether the reopen's recovery found no genuine corruption.
	ReopenClean bool
}

type DiffResult struct {
	// DivergedOp is the op at the first divergence (zero value when agreed).
	DivergedOp Op
	// SignatureA / SignatureB are the diverging observable signatures of variant
	// A and B at DivergedAt (empty when agreed).
	SignatureA string
	SignatureB string
	// VariantA / VariantB are the variant names, for the report.
	VariantA string
	VariantB string
	// Reason is a human-readable description of the divergence (empty when
	// agreed): an end-state mismatch or a per-op result mismatch.
	Reason string
	// DivergedAt is the 0-based op index of the first divergence (-1 when the
	// variants agreed).
	DivergedAt int
	// Agreed reports whether the two variants produced identical observable
	// output for every op and an identical end-state.
	Agreed bool
}

type DiskConfig struct {
	// CapacityBytes, when > 0, is the total byte budget across all files in the
	// SimDisk-backed store. A WAL append or checkpoint write that would breach it
	// returns an ENOSPC error on the real durability path.
	CapacityBytes int64
	// ENOSPCOnSync selects where the out-of-space condition surfaces: false
	// (eager, at the growing Write) or true (delayed, at Sync). See [SimDisk].
	ENOSPCOnSync bool
	// FaultRate is the probability (clamped to [0,1]) that any individual Sync on
	// the SimDisk-backed durable store fails with [ErrSimFault] and that a freshly
	// written sector is marked faulted (a torn write). It is threaded into the
	// disk the durable-mode [New] path drives; the zero value (the default every
	// scenario carries) disables it, keeping the disk fault-free and every
	// existing scenario byte-identical. It takes effect only on the durable path
	// — the one a non-zero [DiskConfig.CapacityBytes], [Config.Crash] or
	// [Config.Checkpoint] selects — because the plain in-memory engine path never
	// touches the disk.
	FaultRate float64
}

type EdgeByName struct {
	Props    map[string]any
	Src, Dst string
	EID      int64
}

type EdgePropsWriter struct {
	// contains filtered or unexported fields
}

type EdgeState struct {
	Properties   map[string]any
	Label        string
	SrcID, DstID uint64
	EID          int64
}

type Engine interface {
	// Run executes a Cypher query with string-keyed parameters and returns a
	// Result the caller must Close.
	Run(ctx context.Context, query string, params map[string]any) (Result, error)
	// NodeCount returns the number of live nodes in the engine.
	NodeCount() (int64, error)
	// EdgeCount returns the number of live edges in the engine.
	EdgeCount() (int64, error)
}

type EngineAdapter struct {
	// contains filtered or unexported fields
}