From 9cecf500542a40f0307f9ea85961edce4dcabd1c Mon Sep 17 00:00:00 2001 From: Elliott de Launay Date: Thu, 29 Oct 2026 23:14:58 -0400 Subject: [PATCH 1/5] test(run-state): add model checker for the run-state kernel --- docs/architecture/task-lifecycle-model.md | 35 +- .../task-lifecycle-target-architecture.md | 2 +- package.json | 2 +- scripts/check-run-state-kernel.ts | 835 ++++++++++++++++++ 4 files changed, 869 insertions(+), 5 deletions(-) create mode 100644 scripts/check-run-state-kernel.ts diff --git a/docs/architecture/task-lifecycle-model.md b/docs/architecture/task-lifecycle-model.md index 081cd96a0c..686aff2464 100644 --- a/docs/architecture/task-lifecycle-model.md +++ b/docs/architecture/task-lifecycle-model.md @@ -6,7 +6,7 @@ Zoo Code checks task lifecycle protocols through one umbrella command for indepe pnpm lifecycle:model-check ``` -The baseline command runs eight independent bounded checks in sequence: +The baseline command runs nine independent bounded checks in sequence: 1. the persisted task delegation lifecycle; 2. shared-store concurrency across task-history hosts; @@ -14,8 +14,9 @@ The baseline command runs eight independent bounded checks in sequence: 4. the task cleanup protocol; 5. request-stream parser scoping; 6. completion persistence; -7. delegated-mode reader refinement; and -8. tool-turn continuation. +7. delegated-mode reader refinement; +8. tool-turn continuation; and +9. the in-memory run-state kernel. The planned two-sibling fan-out protocol is intentionally outside the baseline and CI umbrella. Run it explicitly with `pnpm fanout-protocol:model-check`; it describes optional future functionality, not current production coverage. @@ -199,6 +200,7 @@ These are safety claims within the documented bounds. The checks do not claim li | Cleanup | Abstract bounded universal plus adapter tests | Abort, disposal, settlement, rejection, and provider shutdown are modeled as protocol/environment actions. | No direct execution of all production cleanup methods, filesystem/editor promises, timing liveness, fairness, or arbitrary task counts. | | Parser request scope | Production-backed bounded schedule replay | The checker executes production parser APIs across 924 order-preserving schedules for two scopes. | Assumes callers stop invoking a finalized scope; transport behavior, arbitrary request counts, indices, and malformed histories are outside the claim. | | Completion persistence | Abstract bounded universal plus production tests and one fresh-host E2E path | The model abstracts persistence as a durable phase with at most two write starts; production guards and retry paths are tested separately. | Production permits more retries; no power-loss/filesystem proof, fairness, arbitrary retry count, complete delegated fallback, provider status metadata, or downstream event-consumer model. | +| Run-state kernel | Production-backed bounded universal | The explorer calls the production `nextRunState` and compares each result with a transcription of the design-doc guard and effect table. | Models one task's run state only. Excludes persistence, the actor mailbox, and the wiring of `Task.ts` to the kernel. Witness and source-pair checks have no self-test. | The production mapping above names primary lifecycle transitions, not every mutation or consumer. Generic store upserts, reconciliation, repair replay, migrations, tool entry points, webview/public API abandonment, provider status updates, and public `TaskCompleted` re-emission remain outside the persisted reducer graph unless explicitly named by a submodel or focused test. For task-local mode, the consumers named under #921/#1623 are a confirmed set, not an exhaustive repository-wide inventory; other mode-sensitive tools must be audited before claiming universal reader isolation. @@ -265,8 +267,35 @@ Completion-readiness changes belong in `scripts/check-completion-persistence.ts` Parser request scoping is one such independent bounded submodel within the umbrella suite. Extend `scripts/check-native-tool-call-parser-scoping.ts` and its focused architecture document instead of adding parser state or transitions to `taskLifecycle.ts` or the persisted lifecycle state graph. +Run-state kernel changes belong in `scripts/check-run-state-kernel.ts`. Update the guard and effect table in the checker together with the Transitions table in the target-architecture document, and add a known-unsafe kernel for each new check. + ## Test layering Keep reducer permutations in this model and focused Vitest suites. The real VS Code extension-host suite using a mocked provider in `apps/vscode-e2e/src/suite/subtasks.test.ts` already covers the boundaries the pure explorer cannot: task creation and rehydration, persisted parent-child state, cancellation during a delayed provider stream, interrupted-child resume, abandonment followed by a real resume/save/completion cycle, pending approvals across leave/return, and scheduler-driven resume. `restart-persistence.test.ts` separately verifies completion history through a fresh extension host. Add E2E coverage only when a lifecycle change crosses one of those runtime boundaries or introduces a new one. For example, #1453 persistence-readiness semantics require a controlled fresh-host test, and #369/#372 fan-out requires scheduler permit, live-parent routing, orphan cleanup, and task-scoping E2E. Do not add E2E cases solely to replay reducer orderings already exhausted here; they increase fixture and timing cost without strengthening the proof claim. + +## Run-state kernel submodel + +`scripts/check-run-state-kernel.ts` explores the pure `nextRunState` in `src/core/task/run-state/runState.ts`. It is an independent submodel. It does not use `taskLifecycle.ts` and does not share state with the persisted graph. + +The checker applies every event in every reachable state, within the generation and ask-timestamp caps. The budget is 20,000 states and the depth bound is 20. The stream generation and the ask timestamp are each at most 3. At each step it checks: + +- the result of the kernel against a transcription of the guard and effect table ([Transitions](task-lifecycle-target-architecture.md#transitions)), including that a rejection leaves the state unchanged; +- the seven design-doc invariants (same document, Invariants); +- the kernel does not mutate its state or its event, and the transition checks that hold without the table (latches, generation, phase, stream, and ask rules). + +The checker also requires: + +- the event tags in `runState.ts` to equal the event tags in the table (once, at startup, as a text scan of `case` labels); +- every event to be reachable, with the `askSettledStale` no-op, a settle for an ask that a newer pending ask replaced, as its own action; +- every guard clause to be the only failing clause in some rejected event; +- named witnesses, each tied to an event and the states around it: abort during a pending approval in a live stream, an ask after the stream ends, abandon after the stream ends, dispose after completion, a new stream after a failure cleanup without abort, a stream that starts without user input, an approval before the first stream, and a rejected late completion accept after a newer ask; +- every ordered pair of the stream, ask, cancel, and dispose event sources to follow each other, where both events change the state; +- no unseen successor at the depth bound; +- thirty-one known-unsafe kernels, each of which the checker must reject. They include a throwing kernel, a kernel that returns nothing, and one kernel for each check that runs at every search step without the table; and +- self-tests that a small depth bound and a small state budget each fail the checker. + +The kernel has no resume event. A resumed task is `initialized` followed by `streamStarted` or `askStarted`. The witnesses `first-stream-without-ask` and `approval-before-first-stream` cover those paths. + +The mapping from kernel events and latches to the cleanup protocol model is in [The verification boundary](task-lifecycle-target-architecture.md#the-verification-boundary). diff --git a/docs/architecture/task-lifecycle-target-architecture.md b/docs/architecture/task-lifecycle-target-architecture.md index 571413f43a..285f0c08b3 100644 --- a/docs/architecture/task-lifecycle-target-architecture.md +++ b/docs/architecture/task-lifecycle-target-architecture.md @@ -423,7 +423,7 @@ Replace the process-global tool state with keyed state. Key partial-call state b Draw one line. The checked core is verified. The periphery is ordinary code. -1. Checked core: the seven baseline checkers in `pnpm lifecycle:model-check` (task lifecycle, task store concurrency, provider handoff and scheduler, cleanup protocol, parser scope, completion persistence, and delegated mode readers), plus the pure `nextRunState`. Bounded model-checkers explore these exhaustively within the state budget. This is the "conservative abstraction that keeps only state-relevant information" pattern that AWS uses with formal methods ([How Amazon Web Services uses formal methods](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)). +1. Checked core: the baseline checkers in `pnpm lifecycle:model-check` (task lifecycle, task store concurrency, provider handoff and scheduler, cleanup protocol, parser scope, completion persistence, delegated mode readers, tool-turn continuation, and the run-state kernel `nextRunState`). Bounded model-checkers explore these exhaustively within the state budget. This is the "conservative abstraction that keeps only state-relevant information" pattern that AWS uses with formal methods ([How Amazon Web Services uses formal methods](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)). 2. Periphery: streaming, filesystem, webview, and provider I/O. Focused tests and E2E cover these. No exhaustive proof is claimed. The run-state kernel is a new in-memory submodel. It is not a persisted lifecycle mutation, so it does not live in the shared reducers that `AGENTS.md` pins to `taskLifecycle.ts`. It uses the independent-submodel pattern (`task-lifecycle-model.md`, Extending the model). Add a boundary mapping before any claim spans two submodels (`task-lifecycle-model.md`, introduction). The abort and dispose ordering is already model-checked in `task-cleanup-protocol-model.md`. Map the kernel latches to that model rather than re-proving them: diff --git a/package.json b/package.json index a67f824dcc..73a81df1c8 100644 --- a/package.json +++ b/package.json @@ -20,7 +20,7 @@ "test:agent-evals:unit": "node --import tsx --test scripts/agent-evals/*.test.ts", "agent-evals:check-types": "tsc -p scripts/agent-evals/tsconfig.json", "test:mutation-ci": "node --test scripts/stryker-diff.test.mjs", - "lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && tsx scripts/check-provider-handoff-scheduler.ts && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts && tsx scripts/check-file-replacement-restart.ts && tsx scripts/check-delegated-mode-readers.ts && pnpm tool-turn:model-check", + "lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && tsx scripts/check-provider-handoff-scheduler.ts && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts && tsx scripts/check-file-replacement-restart.ts && tsx scripts/check-delegated-mode-readers.ts && pnpm tool-turn:model-check && tsx scripts/check-run-state-kernel.ts", "webview-recovery:model-check": "node --import tsx scripts/check-webview-recovery.ts", "webview-recovery:check-types": "tsc -p scripts/tsconfig.webview-recovery.json", "fanout-protocol:model-check": "tsx scripts/check-task-fanout-protocol.ts", diff --git a/scripts/check-run-state-kernel.ts b/scripts/check-run-state-kernel.ts new file mode 100644 index 0000000000..d4dd9b4ddd --- /dev/null +++ b/scripts/check-run-state-kernel.ts @@ -0,0 +1,835 @@ +import assert from "node:assert/strict" +import { readFileSync } from "node:fs" +import { fileURLToPath } from "node:url" + +import { nextRunState, initialRunState } from "../src/core/task/run-state/runState" +import type { AbortReason, Ask, RunEvent, RunState, Transition } from "../src/core/task/run-state/runState" + +type Source = "init" | "stream" | "ask" | "cancel" | "dispose" +type EventTag = RunEvent["tag"] +type StartedAsk = Exclude +type Step = (state: RunState, event: RunEvent) => Transition | undefined + +interface ModelState { + run: RunState + askCount: number + completionAsks: number[] + lastEndedStreamCleaned: boolean +} + +interface ModelEvent { + name: string + source: Source + event: RunEvent +} + +interface TraceStep { + action: string + source: Source | "initial" + state: ModelState +} + +interface Options { + step: Step + useTable: boolean + maxDepth: number + maxStates: number +} + +interface Applied { + next: ModelState + accepted: boolean + problems: string[] +} + +interface WitnessContext { + prev: ModelState + next: ModelState + event: RunEvent +} + +const MAX_DEPTH = 20 +const MAX_STATES = 20_000 +const MAX_GENERATION = 3 +const MAX_ASK_TS = 3 +const KERNEL_PATH = fileURLToPath(new URL("../src/core/task/run-state/runState.ts", import.meta.url)) + +const abortReasons: Record = { user_cancelled: true, streaming_failed: true } +const askBuilders: Record StartedAsk> = { + approval: (askTs) => ({ tag: "approval", askTs, toolCallId: `tool-${askTs}`, approvalId: `approval-${askTs}` }), + approvalWithoutIds: (askTs) => ({ tag: "approval", askTs }), + completion: (askTs) => ({ tag: "completion", askTs }), + other: (askTs) => ({ tag: "other", askTs }), +} +const eventSources = ["stream", "ask", "cancel", "dispose"] as const + +// One field per cell of the state described in the target-architecture doc, so rows read like the doc table. +interface Flat { + phase: RunState["phase"] + generation: number + streamLive: boolean + streamGeneration: number | null + cleanupFinished: boolean | null + askTag: Ask["tag"] + askTs: number | null + toolCallId: string | null + approvalId: string | null + abort: boolean + abandoned: boolean + disposed: boolean + reason: AbortReason | null + lastCompletionAskTs: number | null +} + +function flatten(run: RunState): Flat { + const ask = run.ask + return { + phase: run.phase, + generation: run.generation, + streamLive: run.stream.tag === "live", + streamGeneration: run.stream.tag === "live" ? run.stream.generation : null, + cleanupFinished: run.stream.tag === "live" ? run.stream.cleanupFinished : null, + askTag: ask.tag, + askTs: ask.tag === "none" ? null : ask.askTs, + toolCallId: ("toolCallId" in ask && ask.toolCallId) || null, + approvalId: ("approvalId" in ask && ask.approvalId) || null, + abort: run.latches.abort, + abandoned: run.latches.abandoned, + disposed: run.latches.disposed, + reason: run.latches.reason ?? null, + lastCompletionAskTs: run.lastCompletionAskTs ?? null, + } +} + +interface Row { + guard?: Record boolean> + effect: (f: Flat, e: E) => void +} + +type Rows = { [T in EventTag]: Row> } + +const clearAsk = (f: Flat) => { + f.askTag = "none" + f.askTs = f.toolCallId = f.approvalId = null +} + +// Transcribes the Guard and Effect columns of task-lifecycle-target-architecture.md (Transitions). +const rows: Rows = { + initialized: { + guard: { uninitialized: (f) => f.phase === "uninitialized" }, + effect: (f) => void (f.phase = "running"), + }, + streamStarted: { + guard: { running: (f) => f.phase === "running", "no live stream": (f) => !f.streamLive }, + effect: (f) => { + f.generation += 1 + f.streamLive = true + f.streamGeneration = f.generation + f.cleanupFinished = false + f.lastCompletionAskTs = null + }, + }, + streamCleanupFinished: { + guard: { "live stream": (f) => f.streamLive }, + effect: (f) => void (f.cleanupFinished = true), + }, + streamEnded: { + guard: { "live stream": (f) => f.streamLive }, + effect: (f) => { + f.streamLive = false + f.streamGeneration = f.cleanupFinished = null + }, + }, + askStarted: { + guard: { running: (f) => f.phase === "running", "not aborted": (f) => !f.abort }, + effect: (f, e) => { + f.askTag = e.ask.tag + f.askTs = e.ask.askTs + f.toolCallId = (e.ask.tag === "approval" && e.ask.toolCallId) || null + f.approvalId = (e.ask.tag === "approval" && e.ask.approvalId) || null + f.lastCompletionAskTs = e.ask.tag === "completion" ? e.ask.askTs : null + }, + }, + askSettled: { + effect: (f, e) => { + if (f.askTs === e.askTs) clearAsk(f) + }, + }, + completionAccepted: { + guard: { + running: (f) => f.phase === "running", + "not aborted": (f) => !f.abort, + "latest completion ask": (f, e) => e.askTs === f.lastCompletionAskTs, + }, + effect: (f) => { + f.phase = "completed" + clearAsk(f) + }, + }, + reasonSet: { + effect: (f, e) => void (f.reason ??= e.reason), + }, + abortRequested: { + effect: (f, e) => { + f.abort = true + if (e.abandoned) f.abandoned = true + }, + }, + abandonRequested: { + guard: { aborted: (f) => f.abort }, + effect: (f) => void (f.abandoned = true), + }, + disposeRequested: { + effect: (f) => { + f.abort = true + f.disposed = true + }, + }, +} + +const eventTags = Object.keys(rows) as EventTag[] +const guardClauses = eventTags.flatMap((tag) => + Object.keys((rows[tag] as Row).guard ?? {}).map((clause) => `${tag}: ${clause}`), +) +const expectedActions = [...eventTags, "askSettledStale"] + +function referenceResult(run: RunState, event: RunEvent): { accepted: boolean; flat: Flat; failedClauses: string[] } { + const flat = flatten(run) + const row = rows[event.tag] as Row + const failedClauses = Object.entries(row.guard ?? {}) + .filter(([, holds]) => !holds(flat, event)) + .map(([clause]) => `${event.tag}: ${clause}`) + const accepted = failedClauses.length === 0 + if (accepted) row.effect(flat, event) + return { accepted, flat, failedClauses } +} + +function kernelEventTags(): string[] { + const source = readFileSync(KERNEL_PATH, "utf8") + return [...source.matchAll(/case "(\w+)":/g)].map((match) => match[1]!) +} + +const rejectionWitnesses = new Set(["late-completion-accept-rejected-after-new-ask"]) +const semanticWitnesses = { + "abort-during-pending-approval-in-live-stream": ({ prev, next, event }: WitnessContext) => + event.tag === "abortRequested" && + prev.run.stream.tag === "live" && + prev.run.ask.tag === "approval" && + !prev.run.latches.abort && + next.run.latches.abort, + "ask-after-stream-ended": ({ prev, next, event }: WitnessContext) => + event.tag === "askStarted" && + prev.run.stream.tag === "none" && + prev.run.generation > 0 && + next.run.ask.tag !== "none", + "abandon-after-stream-ended": ({ prev, next, event }: WitnessContext) => + (event.tag === "abandonRequested" || (event.tag === "abortRequested" && event.abandoned)) && + prev.run.stream.tag === "none" && + prev.run.generation > 0 && + !prev.run.latches.abandoned && + next.run.latches.abandoned, + "dispose-after-completion": ({ prev, next, event }: WitnessContext) => + event.tag === "disposeRequested" && prev.run.phase === "completed" && next.run.latches.disposed, + "stream-after-failure-cleanup": ({ prev, next, event }: WitnessContext) => + event.tag === "streamStarted" && + prev.lastEndedStreamCleaned && + !prev.run.latches.abort && + next.run.stream.tag === "live" && + !next.run.stream.cleanupFinished && + next.run.generation >= 2, + "first-stream-without-ask": ({ prev, next, event }: WitnessContext) => + event.tag === "streamStarted" && + prev.run.phase === "running" && + prev.run.generation === 0 && + prev.run.ask.tag === "none" && + next.run.stream.tag === "live", + "approval-before-first-stream": ({ prev, next, event }: WitnessContext) => + event.tag === "askStarted" && + prev.run.phase === "running" && + prev.run.generation === 0 && + next.run.ask.tag === "approval", + "late-completion-accept-rejected-after-new-ask": ({ prev, event }: WitnessContext) => + event.tag === "completionAccepted" && + prev.completionAsks.includes(event.askTs) && + prev.askCount > event.askTs && + prev.run.lastCompletionAskTs !== event.askTs && + prev.run.phase === "running" && + !prev.run.latches.abort, +} satisfies Record boolean> + +function initialState(): ModelState { + return { run: structuredClone(initialRunState), askCount: 0, completionAsks: [], lastEndedStreamCleaned: false } +} + +function stable(value: unknown): unknown { + if (Array.isArray(value)) return value.map(stable) + if (typeof value !== "object" || value === null) return value + return Object.fromEntries( + Object.entries(value) + .filter(([, child]) => child !== undefined) + .sort(([a], [b]) => (a < b ? -1 : 1)) + .map(([key, child]) => [key, stable(child)]), + ) +} + +function canonical(value: unknown): string { + return JSON.stringify(stable(value)) +} + +function eventsFor({ run, askCount }: ModelState): ModelEvent[] { + const events: ModelEvent[] = [{ name: "initialized()", source: "init", event: { tag: "initialized" } }] + if (run.generation < MAX_GENERATION) { + events.push({ name: "streamStarted()", source: "stream", event: { tag: "streamStarted" } }) + } + events.push( + { name: "streamCleanupFinished()", source: "stream", event: { tag: "streamCleanupFinished" } }, + { name: "streamEnded()", source: "stream", event: { tag: "streamEnded" } }, + ) + if (askCount < MAX_ASK_TS) { + for (const [kind, build] of Object.entries(askBuilders)) { + const ask = build(askCount + 1) + events.push({ name: `askStarted(${kind}, ${ask.askTs})`, source: "ask", event: { tag: "askStarted", ask } }) + } + } + for (let askTs = 1; askTs <= MAX_ASK_TS; askTs++) { + const supersededByNewerAsk = run.ask.tag !== "none" && run.ask.askTs > askTs + events.push( + { + name: `${supersededByNewerAsk ? "askSettledStale" : "askSettled"}(${askTs})`, + source: "ask", + event: { tag: "askSettled", askTs }, + }, + { name: `completionAccepted(${askTs})`, source: "ask", event: { tag: "completionAccepted", askTs } }, + ) + } + for (const reason of Object.keys(abortReasons) as AbortReason[]) { + events.push({ name: `reasonSet(${reason})`, source: "cancel", event: { tag: "reasonSet", reason } }) + } + for (const abandoned of [false, true]) { + events.push({ + name: `abortRequested(${abandoned})`, + source: "cancel", + event: { tag: "abortRequested", abandoned }, + }) + } + events.push( + { name: "abandonRequested()", source: "cancel", event: { tag: "abandonRequested" } }, + { name: "disposeRequested()", source: "dispose", event: { tag: "disposeRequested" } }, + ) + return events +} + +const phaseOrder = { uninitialized: 0, running: 1, completed: 2 } as const + +function stateViolations({ run, askCount }: ModelState): string[] { + const violations: string[] = [] + if (run.latches.abandoned && !run.latches.abort) violations.push("abandoned without abort") + if (run.latches.disposed && !run.latches.abort) violations.push("disposed without abort") + if (run.phase === "completed" && run.ask.tag !== "none") violations.push("completed task has a pending ask") + if (run.ask.tag !== "none" && run.ask.askTs !== askCount) violations.push("pending ask is not the newest ask") + if (run.stream.tag === "live" && run.stream.generation !== run.generation) { + violations.push("live stream generation differs from run generation") + } + return violations +} + +function transitionViolations(before: RunState, after: RunState): string[] { + const violations: string[] = [] + for (const latch of ["abort", "abandoned", "disposed"] as const) { + if (before.latches[latch] && !after.latches[latch]) violations.push(`latch ${latch} returned to false`) + } + if (before.latches.reason !== undefined && after.latches.reason !== before.latches.reason) { + violations.push("abort reason changed after the first write") + } + if (after.generation < before.generation) violations.push("generation decreased") + if (phaseOrder[after.phase] < phaseOrder[before.phase]) violations.push("phase moved backwards") + const askChanged = canonical(after.ask) !== canonical(before.ask) + if (after.latches.abort && after.ask.tag !== "none" && askChanged) violations.push("an ask started after abort") + if (before.phase === "completed" && before.stream.tag === "none" && after.stream.tag === "live") { + violations.push("a stream started after completion") + } + if ( + after.phase === "completed" && + before.phase !== "completed" && + before.stream.tag === "none" && + after.stream.tag === "live" + ) { + violations.push("a task completed and started a stream at once") + } + if ( + before.stream.tag === "live" && + after.stream.tag === "live" && + after.stream.generation !== before.stream.generation + ) { + violations.push("a live stream was replaced") + } + if (before.stream.tag === "none" && after.stream.tag === "live" && after.stream.cleanupFinished) { + violations.push("a new stream started with cleanupFinished true") + } + return violations +} + +function apply(options: Options, state: ModelState, { event }: ModelEvent): Applied { + const input = structuredClone(state.run) + const eventInput = structuredClone(event) + let result: Transition | undefined + try { + result = options.step(input, eventInput) + } catch (error) { + return { next: state, accepted: false, problems: [`${event.tag} threw: ${String(error)}`] } + } + if (result === undefined || !("ok" in result || "rejected" in result)) { + return { next: state, accepted: false, problems: [`${event.tag} returned neither ok nor rejected`] } + } + + const problems: string[] = [] + if (canonical(input) !== canonical(state.run)) problems.push(`${event.tag} mutated its state`) + if (canonical(eventInput) !== canonical(event)) problems.push(`${event.tag} mutated its event`) + const accepted = "ok" in result + const actual = "ok" in result ? result.ok : result.rejected + if (options.useTable) { + const wanted = referenceResult(state.run, event) + if (accepted !== wanted.accepted) + problems.push(`${event.tag} ${accepted ? "accepted" : "rejected"} against the table`) + if (canonical(flatten(actual)) !== canonical(wanted.flat)) + problems.push(`${event.tag} result differs from the table`) + } + if (!accepted && canonical(actual) !== canonical(state.run)) problems.push(`${event.tag} rejection changed state`) + if (!accepted) return { next: state, accepted, problems } + + problems.push(...transitionViolations(state.run, actual)) + const next: ModelState = { ...state, run: actual } + if (event.tag === "askStarted") { + next.askCount = event.ask.askTs + if (event.ask.tag === "completion") next.completionAsks = [...state.completionAsks, event.ask.askTs] + } + if (event.tag === "streamEnded" && state.run.stream.tag === "live") { + next.lastEndedStreamCleaned = state.run.stream.cleanupFinished + } + return { next, accepted, problems } +} + +function formatCounterexample(message: string, trace: TraceStep[], options: Options): string { + const steps = trace.map( + (step, index) => + `${index}. ${step.action}\n${JSON.stringify(step.state, null, 2) + .split("\n") + .map((line) => ` ${line}`) + .join("\n")}`, + ) + return [ + `Run-state kernel invariant failed: ${message}`, + `Bounds: depth=${options.maxDepth}, states=${options.maxStates}, generations=${MAX_GENERATION}, asks=${MAX_ASK_TS}`, + ...steps, + ].join("\n") +} + +interface CheckResult { + states: number + deepest: number +} + +function runModelCheck(options: Options): CheckResult { + const start = initialState() + const startTrace: TraceStep[] = [{ action: "initial", source: "initial", state: start }] + const startProblems = stateViolations(start) + if (startProblems.length) throw new Error(formatCounterexample(startProblems.join("; "), startTrace, options)) + + const queue = [{ state: start, trace: startTrace }] + const visited = new Set([canonical(start)]) + const reachedActions = new Set() + const reachedRejections = new Set() + const reachedWitnesses = new Set() + const reachedInterleavings = new Set() + let deepest = 0 + + for (let index = 0; index < queue.length; index++) { + const node = queue[index]! + const depth = node.trace.length - 1 + deepest = Math.max(deepest, depth) + const previousStep = node.trace[depth]! + const previousChangedState = + depth > 0 && canonical(previousStep.state.run) !== canonical(node.trace[depth - 1]!.state.run) + + for (const modelEvent of eventsFor(node.state)) { + const applied = apply(options, node.state, modelEvent) + const trace = [...node.trace, { action: modelEvent.name, source: modelEvent.source, state: applied.next }] + const problems = [...applied.problems, ...(applied.accepted ? stateViolations(applied.next) : [])] + if (problems.length) throw new Error(formatCounterexample(problems.join("; "), trace, options)) + + for (const [name, matches] of Object.entries(semanticWitnesses)) { + if (applied.accepted === rejectionWitnesses.has(name)) continue + if (matches({ prev: node.state, next: applied.next, event: modelEvent.event })) + reachedWitnesses.add(name) + } + if (!applied.accepted) { + const { failedClauses } = referenceResult(node.state.run, modelEvent.event) + if (failedClauses.length === 1) reachedRejections.add(failedClauses[0]!) + continue + } + reachedActions.add(modelEvent.name.slice(0, modelEvent.name.indexOf("("))) + const changesState = canonical(applied.next.run) !== canonical(node.state.run) + if (previousChangedState && changesState && previousStep.source !== modelEvent.source) { + reachedInterleavings.add(`${previousStep.source}->${modelEvent.source}`) + } + + const key = canonical(applied.next) + if (visited.has(key)) continue + if (depth === options.maxDepth) { + throw new Error( + `Run-state kernel exploration reached depth ${options.maxDepth} with an unseen successor (${modelEvent.name}); increase the depth bound`, + ) + } + visited.add(key) + queue.push({ state: applied.next, trace }) + if (visited.size > options.maxStates) { + throw new Error( + `Run-state kernel exploration exceeded its ${options.maxStates}-state budget; increase or reduce bounds`, + ) + } + } + } + + const assertNoneMissing = (label: string, names: string[]) => { + if (names.length) throw new Error(`Run-state kernel model has ${label}: ${names.join(", ")}`) + } + assertNoneMissing( + "unreachable actions", + expectedActions.filter((action) => !reachedActions.has(action)), + ) + assertNoneMissing( + "guard clauses that are never the only reason for a rejection", + guardClauses.filter((clause) => !reachedRejections.has(clause)), + ) + assertNoneMissing( + "unreachable semantic witnesses", + Object.keys(semanticWitnesses).filter((name) => !reachedWitnesses.has(name)), + ) + assertNoneMissing( + "missing event-source interleavings between state changes", + eventSources + .flatMap((from) => eventSources.filter((to) => to !== from).map((to) => `${from}->${to}`)) + .filter((pair) => !reachedInterleavings.has(pair)), + ) + return { states: visited.size, deepest } +} + +function assertKernelHandlesTableEvents(): void { + const handled = new Set(kernelEventTags()) + const missingFromKernel = eventTags.filter((tag) => !handled.has(tag)) + const missingFromTable = [...handled].filter((tag) => !(tag in rows)) + assert.deepEqual( + { missingFromKernel, missingFromTable }, + { missingFromKernel: [], missingFromTable: [] }, + `the event tags in ${KERNEL_PATH} and in the checker table differ`, + ) +} + +const freshLive = (generation: number): RunState["stream"] => ({ tag: "live", generation, cleanupFinished: false }) + +interface UnsafeKernel { + step: Step + caughtBy: RegExp + useTable: boolean +} + +const differsFor = (tag: EventTag) => + new RegExp(`${tag} (result differs from the table|(accepted|rejected) against the table)`) +const unsafeKernels: Record = { + "second-stream-replaces-live-stream": { + step: (state, event) => + event.tag === "streamStarted" && state.phase === "running" && state.stream.tag === "live" + ? { ok: { ...state, generation: state.generation + 1, stream: freshLive(state.generation + 1) } } + : nextRunState(state, event), + caughtBy: /live stream was replaced/, + useTable: false, + }, + "stream-end-clears-ask": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "streamEnded" && "ok" in result + ? { ok: { ...result.ok, ask: { tag: "none" } } } + : result + }, + caughtBy: differsFor("streamEnded"), + useTable: true, + }, + "ask-starts-after-abort": { + step: (state, event) => + event.tag === "askStarted" && state.phase === "running" && state.latches.abort + ? { ok: { ...state, ask: event.ask } } + : nextRunState(state, event), + caughtBy: /ask started after abort/, + useTable: false, + }, + "stale-settle-clears-newer-ask": { + step: (state, event) => + event.tag === "askSettled" ? { ok: { ...state, ask: { tag: "none" } } } : nextRunState(state, event), + caughtBy: differsFor("askSettled"), + useTable: true, + }, + "abandon-without-abort": { + step: (state, event) => + event.tag === "abandonRequested" + ? { ok: { ...state, latches: { ...state.latches, abandoned: true } } } + : nextRunState(state, event), + caughtBy: /abandoned without abort/, + useTable: false, + }, + "later-reason-overwrites-first": { + step: (state, event) => + event.tag === "reasonSet" + ? { ok: { ...state, latches: { ...state.latches, reason: event.reason } } } + : nextRunState(state, event), + caughtBy: /abort reason changed/, + useTable: false, + }, + "dispose-without-abort": { + step: (state, event) => + event.tag === "disposeRequested" + ? { ok: { ...state, latches: { ...state.latches, disposed: true } } } + : nextRunState(state, event), + caughtBy: /disposed without abort/, + useTable: false, + }, + "stream-starts-after-completion": { + step: (state, event) => + event.tag === "streamStarted" && state.phase === "completed" + ? { ok: { ...state, stream: freshLive(state.generation) } } + : nextRunState(state, event), + caughtBy: /stream started after completion/, + useTable: false, + }, + "completion-starts-a-stream": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "completionAccepted" && "ok" in result && result.ok.stream.tag === "none" + ? { ok: { ...result.ok, stream: freshLive(result.ok.generation) } } + : result + }, + caughtBy: /completed and started a stream/, + useTable: false, + }, + "abort-drops-abandon": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "abortRequested" && "ok" in result + ? { ok: { ...result.ok, latches: { ...result.ok.latches, abandoned: state.latches.abandoned } } } + : result + }, + caughtBy: differsFor("abortRequested"), + useTable: true, + }, + "cleanup-flag-survives-new-stream": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "streamStarted" && "ok" in result && result.ok.stream.tag === "live" + ? { ok: { ...result.ok, stream: { ...result.ok.stream, cleanupFinished: true } } } + : result + }, + caughtBy: /cleanupFinished true/, + useTable: false, + }, + "approval-drops-opaque-ids": { + step: (state, event) => + event.tag === "askStarted" && event.ask.tag === "approval" + ? nextRunState(state, { ...event, ask: { tag: "approval", askTs: event.ask.askTs } }) + : nextRunState(state, event), + caughtBy: differsFor("askStarted"), + useTable: true, + }, + "ask-merges-previous-ask": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "askStarted" && "ok" in result + ? { ok: { ...result.ok, ask: { ...state.ask, ...event.ask } } } + : result + }, + caughtBy: differsFor("askStarted"), + useTable: true, + }, + "late-completion-accepted": { + step: (state, event) => + event.tag === "completionAccepted" && state.phase === "running" && !state.latches.abort + ? { ok: { ...state, phase: "completed", ask: { tag: "none" } } } + : nextRunState(state, event), + caughtBy: differsFor("completionAccepted"), + useTable: true, + }, + "reason-set-clears-abort": { + step: (state, event) => + event.tag === "reasonSet" && state.latches.abort + ? { ok: { ...state, latches: { ...state.latches, abort: false } } } + : nextRunState(state, event), + caughtBy: /latch abort returned to false/, + useTable: false, + }, + "reason-set-clears-abandoned": { + step: (state, event) => + event.tag === "reasonSet" && state.latches.abandoned + ? { ok: { ...state, latches: { ...state.latches, abandoned: false } } } + : nextRunState(state, event), + caughtBy: /latch abandoned returned to false/, + useTable: false, + }, + "reason-set-clears-disposed": { + step: (state, event) => + event.tag === "reasonSet" && state.latches.disposed + ? { ok: { ...state, latches: { ...state.latches, disposed: false } } } + : nextRunState(state, event), + caughtBy: /latch disposed returned to false/, + useTable: false, + }, + "repeated-reason-rejected": { + step: (state, event) => + event.tag === "reasonSet" && state.latches.reason !== undefined + ? { rejected: state } + : nextRunState(state, event), + caughtBy: /reasonSet rejected against the table/, + useTable: true, + }, + "stream-start-guard-dropped": { + step: (state, event) => + event.tag === "streamStarted" && state.phase !== "running" && state.stream.tag === "none" + ? { ok: state } + : nextRunState(state, event), + caughtBy: /never the only reason for a rejection: streamStarted: running$/, + useTable: false, + }, + "abandon-guard-dropped": { + step: (state, event) => + event.tag === "abandonRequested" && !state.latches.abort ? { ok: state } : nextRunState(state, event), + caughtBy: /never the only reason for a rejection: abandonRequested: aborted$/, + useTable: false, + }, + "dispose-always-rejected": { + step: (state, event) => (event.tag === "disposeRequested" ? { rejected: state } : nextRunState(state, event)), + caughtBy: /unreachable actions: disposeRequested$/, + useTable: false, + }, + "completion-keeps-ask": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "completionAccepted" && "ok" in result + ? { ok: { ...result.ok, ask: state.ask } } + : result + }, + caughtBy: /completed task has a pending ask/, + useTable: false, + }, + "stream-start-lowers-generation": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "streamStarted" && "ok" in result + ? { ok: { ...result.ok, generation: state.generation - 1 } } + : result + }, + caughtBy: /generation decreased/, + useTable: false, + }, + "ask-timestamp-skips-ahead": { + step: (state, event) => + event.tag === "askStarted" && state.phase === "running" && !state.latches.abort + ? { ok: { ...state, ask: { ...event.ask, askTs: event.ask.askTs + 1 } } } + : nextRunState(state, event), + caughtBy: /pending ask is not the newest ask/, + useTable: false, + }, + "abort-reopens-completed-task": { + step: (state, event) => + event.tag === "abortRequested" && state.phase === "completed" + ? { ok: { ...state, phase: "running", latches: { ...state.latches, abort: true } } } + : nextRunState(state, event), + caughtBy: /phase moved backwards/, + useTable: false, + }, + "stream-start-skews-live-generation": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "streamStarted" && "ok" in result + ? { ok: { ...result.ok, stream: freshLive(result.ok.generation + 1) } } + : result + }, + caughtBy: /live stream generation differs/, + useTable: false, + }, + "rejection-bumps-generation": { + step: (state, event) => { + const result = nextRunState(state, event) + return "rejected" in result + ? { rejected: { ...result.rejected, generation: state.generation + 1 } } + : result + }, + caughtBy: /rejection changed state/, + useTable: false, + }, + "mutates-its-state": { + step: (state, event) => { + if (event.tag === "abortRequested") state.latches.abort = true + return nextRunState(state, event) + }, + caughtBy: /abortRequested mutated its state/, + useTable: false, + }, + "mutates-its-event": { + step: (state, event) => { + if (event.tag === "askSettled" && state.ask.tag !== "none") event.askTs = state.ask.askTs + return nextRunState(state, event) + }, + caughtBy: /askSettled mutated its event/, + useTable: false, + }, + "returns-nothing": { + step: (state, event) => (event.tag === "streamEnded" ? undefined : nextRunState(state, event)), + caughtBy: /returned neither/, + useTable: false, + }, + "throws-on-stale-settle": { + step: (state, event) => { + if (event.tag === "askSettled" && state.ask.tag !== "none" && state.ask.askTs !== event.askTs) { + throw new Error("stale settle") + } + return nextRunState(state, event) + }, + caughtBy: /threw/, + useTable: false, + }, +} + +function runUnsafeKernels(): void { + for (const [name, { step, caughtBy, useTable }] of Object.entries(unsafeKernels)) { + const options = { step, useTable, maxDepth: MAX_DEPTH, maxStates: MAX_STATES } + assert.throws(() => runModelCheck(options), caughtBy, `unsafe kernel not caught as expected: ${name}`) + } +} + +function runBoundSelfTests(): void { + const base = { step: nextRunState, useTable: true, maxDepth: MAX_DEPTH, maxStates: MAX_STATES } + assert.throws(() => runModelCheck({ ...base, maxDepth: 3 }), /unseen successor/) + assert.throws(() => runModelCheck({ ...base, maxStates: 50 }), /state budget/) +} + +function runRepresentativeScenarios(): void { + const running = nextRunState(structuredClone(initialRunState), { tag: "initialized" }) + assert.ok("ok" in running) + const asked = nextRunState(running.ok, { tag: "askStarted", ask: { tag: "approval", askTs: 1 } }) + assert.ok("ok" in asked) + const aborted = nextRunState(asked.ok, { tag: "abortRequested", abandoned: false }) + assert.ok("ok" in aborted) + assert.ok("rejected" in nextRunState(aborted.ok, { tag: "askStarted", ask: { tag: "other", askTs: 2 } })) + assert.deepEqual(nextRunState(asked.ok, { tag: "askSettled", askTs: 2 }), { ok: asked.ok }) +} + +assertKernelHandlesTableEvents() +runRepresentativeScenarios() +const { states, deepest } = runModelCheck({ + step: nextRunState, + useTable: true, + maxDepth: MAX_DEPTH, + maxStates: MAX_STATES, +}) +runUnsafeKernels() +runBoundSelfTests() +console.log( + `Run-state kernel model check passed: ${states} reachable states, ${expectedActions.length}/${expectedActions.length} actions reachable, ${guardClauses.length}/${guardClauses.length} guard clauses isolated, ${Object.keys(semanticWitnesses).length}/${Object.keys(semanticWitnesses).length} witnesses reached, ${eventSources.length * (eventSources.length - 1)} source interleavings, ${Object.keys(unsafeKernels).length} unsafe kernels caught, fixed point at depth ${deepest} (bound ${MAX_DEPTH}), generations <= ${MAX_GENERATION}, asks <= ${MAX_ASK_TS}`, +) From 0250ab0f9ea0f4de4b634e04d1a205ea202812bf Mon Sep 17 00:00:00 2001 From: Elliott de Launay Date: Sat, 31 Oct 2026 15:35:29 -0400 Subject: [PATCH 2/5] test(run-state): cover the turn events in the kernel model checker --- docs/architecture/task-lifecycle-model.md | 5 +- scripts/check-run-state-kernel.ts | 115 +++++++++++++++++++++- 2 files changed, 117 insertions(+), 3 deletions(-) diff --git a/docs/architecture/task-lifecycle-model.md b/docs/architecture/task-lifecycle-model.md index 686aff2464..93d7ac639f 100644 --- a/docs/architecture/task-lifecycle-model.md +++ b/docs/architecture/task-lifecycle-model.md @@ -279,7 +279,7 @@ Add E2E coverage only when a lifecycle change crosses one of those runtime bound `scripts/check-run-state-kernel.ts` explores the pure `nextRunState` in `src/core/task/run-state/runState.ts`. It is an independent submodel. It does not use `taskLifecycle.ts` and does not share state with the persisted graph. -The checker applies every event in every reachable state, within the generation and ask-timestamp caps. The budget is 20,000 states and the depth bound is 20. The stream generation and the ask timestamp are each at most 3. At each step it checks: +The checker applies every event except the seven turn events in every reachable state, within the generation and ask-timestamp caps. The budget is 20,000 states and the depth bound is 20. The stream generation and the ask timestamp are each at most 3. At each step it checks: - the result of the kernel against a transcription of the guard and effect table ([Transitions](task-lifecycle-target-architecture.md#transitions)), including that a rejection leaves the state unchanged; - the seven design-doc invariants (same document, Invariants); @@ -287,13 +287,14 @@ The checker applies every event in every reachable state, within the generation The checker also requires: +- the seven turn events (`turnStarted`, `firstChunkAwaitStarted`, `firstChunkAwaitEnded`, `toolRejected`, `toolUsed`, `toolFailed`, `streamReadCompleted`) to be accepted and to match the table in each of the 32 turn states, and in one state of every distinct shape of the reachable states. Every other event is also applied to the same shape states with all five turn fields true, so no other event may change the turn. The search does not include turn events, because they would multiply the state count by 32; - the event tags in `runState.ts` to equal the event tags in the table (once, at startup, as a text scan of `case` labels); - every event to be reachable, with the `askSettledStale` no-op, a settle for an ask that a newer pending ask replaced, as its own action; - every guard clause to be the only failing clause in some rejected event; - named witnesses, each tied to an event and the states around it: abort during a pending approval in a live stream, an ask after the stream ends, abandon after the stream ends, dispose after completion, a new stream after a failure cleanup without abort, a stream that starts without user input, an approval before the first stream, and a rejected late completion accept after a newer ask; - every ordered pair of the stream, ask, cancel, and dispose event sources to follow each other, where both events change the state; - no unseen successor at the depth bound; -- thirty-one known-unsafe kernels, each of which the checker must reject. They include a throwing kernel, a kernel that returns nothing, and one kernel for each check that runs at every search step without the table; and +- thirty-three known-unsafe kernels, each of which the checker must reject. They include a throwing kernel, a kernel that returns nothing, and one kernel for each check that runs at every search step without the table; and - self-tests that a small depth bound and a small state budget each fail the checker. The kernel has no resume event. A resumed task is `initialized` followed by `streamStarted` or `askStarted`. The witnesses `first-stream-without-ask` and `approval-before-first-stream` cover those paths. diff --git a/scripts/check-run-state-kernel.ts b/scripts/check-run-state-kernel.ts index d4dd9b4ddd..30f609830b 100644 --- a/scripts/check-run-state-kernel.ts +++ b/scripts/check-run-state-kernel.ts @@ -5,7 +5,7 @@ import { fileURLToPath } from "node:url" import { nextRunState, initialRunState } from "../src/core/task/run-state/runState" import type { AbortReason, Ask, RunEvent, RunState, Transition } from "../src/core/task/run-state/runState" -type Source = "init" | "stream" | "ask" | "cancel" | "dispose" +type Source = "init" | "stream" | "ask" | "cancel" | "dispose" | "turn" type EventTag = RunEvent["tag"] type StartedAsk = Exclude type Step = (state: RunState, event: RunEvent) => Transition | undefined @@ -62,6 +62,20 @@ const askBuilders: Record StartedAsk> = { other: (askTs) => ({ tag: "other", askTs }), } const eventSources = ["stream", "ask", "cancel", "dispose"] as const +const turnTags = [ + "turnStarted", + "firstChunkAwaitStarted", + "firstChunkAwaitEnded", + "toolRejected", + "toolUsed", + "toolFailed", + "streamReadCompleted", +] as const +const turnEvent = (tag: (typeof turnTags)[number]): ModelEvent => ({ + name: `${tag}()`, + source: "turn", + event: { tag }, +}) // One field per cell of the state described in the target-architecture doc, so rows read like the doc table. interface Flat { @@ -70,6 +84,11 @@ interface Flat { streamLive: boolean streamGeneration: number | null cleanupFinished: boolean | null + waitingForFirstChunk: boolean + toolRejected: boolean + toolUsed: boolean + toolFailed: boolean + streamReadComplete: boolean askTag: Ask["tag"] askTs: number | null toolCallId: string | null @@ -89,6 +108,7 @@ function flatten(run: RunState): Flat { streamLive: run.stream.tag === "live", streamGeneration: run.stream.tag === "live" ? run.stream.generation : null, cleanupFinished: run.stream.tag === "live" ? run.stream.cleanupFinished : null, + ...run.turn, askTag: ask.tag, askTs: ask.tag === "none" ? null : ask.askTs, toolCallId: ("toolCallId" in ask && ask.toolCallId) || null, @@ -119,6 +139,17 @@ const rows: Rows = { guard: { uninitialized: (f) => f.phase === "uninitialized" }, effect: (f) => void (f.phase = "running"), }, + turnStarted: { + effect: (f) => { + f.toolRejected = f.toolUsed = f.toolFailed = f.streamReadComplete = false + }, + }, + firstChunkAwaitStarted: { effect: (f) => void (f.waitingForFirstChunk = true) }, + firstChunkAwaitEnded: { effect: (f) => void (f.waitingForFirstChunk = false) }, + toolRejected: { effect: (f) => void (f.toolRejected = true) }, + toolUsed: { effect: (f) => void (f.toolUsed = true) }, + toolFailed: { effect: (f) => void (f.toolFailed = true) }, + streamReadCompleted: { effect: (f) => void (f.streamReadComplete = true) }, streamStarted: { guard: { running: (f) => f.phase === "running", "no live stream": (f) => !f.streamLive }, effect: (f) => { @@ -424,6 +455,62 @@ function formatCounterexample(message: string, trace: TraceStep[], options: Opti ].join("\n") } +const dirtyTurn = { + waitingForFirstChunk: true, + toolRejected: true, + toolUsed: true, + toolFailed: true, + streamReadComplete: true, +} + +const shapeOf = ({ run }: ModelState) => + canonical({ + phase: run.phase, + generation: run.generation > 0, + stream: run.stream.tag === "live" ? run.stream.cleanupFinished : "none", + ask: run.ask.tag, + latches: run.latches, + lastCompletionAskTs: run.lastCompletionAskTs !== undefined, + }) + +function checkTurnRegion(options: Options, searched: ModelState[], reachedActions: Set): void { + const shapes = new Map(searched.map((state) => [shapeOf(state), state])) + const cases = [...shapes.values()].flatMap((state) => [ + { state, events: [...eventsFor(state), ...turnTags.map(turnEvent)] }, + { state: { ...state, run: { ...state.run, turn: dirtyTurn } }, events: eventsFor(state) }, + ]) + const everyTurn = Array.from({ length: 32 }, (_, bits) => ({ + waitingForFirstChunk: Boolean(bits & 1), + toolRejected: Boolean(bits & 2), + toolUsed: Boolean(bits & 4), + toolFailed: Boolean(bits & 8), + streamReadComplete: Boolean(bits & 16), + })) + for (const turn of everyTurn) { + const state = initialState() + cases.push({ state: { ...state, run: { ...state.run, turn } }, events: turnTags.map(turnEvent) }) + } + + for (const { state, events } of cases) { + for (const modelEvent of events) { + const applied = apply(options, state, modelEvent) + const turnEventRejected = modelEvent.source === "turn" && !applied.accepted + const problems = [ + ...applied.problems, + ...(turnEventRejected ? [`${modelEvent.event.tag} was rejected`] : []), + ] + if (problems.length) { + const trace = [ + { action: "initial", source: "initial" as const, state }, + { action: modelEvent.name, source: modelEvent.source, state: applied.next }, + ] + throw new Error(formatCounterexample(problems.join("; "), trace, options)) + } + if (modelEvent.source === "turn") reachedActions.add(modelEvent.event.tag) + } + } +} + interface CheckResult { states: number deepest: number @@ -490,6 +577,12 @@ function runModelCheck(options: Options): CheckResult { } } + checkTurnRegion( + options, + queue.map((node) => node.state), + reachedActions, + ) + const assertNoneMissing = (label: string, names: string[]) => { if (names.length) throw new Error(`Run-state kernel model has ${label}: ${names.join(", ")}`) } @@ -707,6 +800,26 @@ const unsafeKernels: Record = { caughtBy: /unreachable actions: disposeRequested$/, useTable: false, }, + "turn-start-clears-first-chunk-wait": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "turnStarted" && "ok" in result + ? { ok: { ...result.ok, turn: { ...result.ok.turn, waitingForFirstChunk: false } } } + : result + }, + caughtBy: differsFor("turnStarted"), + useTable: true, + }, + "stream-start-resets-turn": { + step: (state, event) => { + const result = nextRunState(state, event) + return event.tag === "streamStarted" && "ok" in result + ? { ok: { ...result.ok, turn: { ...result.ok.turn, toolUsed: false } } } + : result + }, + caughtBy: differsFor("streamStarted"), + useTable: true, + }, "completion-keeps-ask": { step: (state, event) => { const result = nextRunState(state, event) From 33514831178c17fd20a51aedaf8f32aa54ac71d7 Mon Sep 17 00:00:00 2001 From: Elliott de Launay Date: Sat, 31 Oct 2026 16:27:57 -0400 Subject: [PATCH 3/5] test(run-state): require a recorded stream failure in the failure-cleanup witness --- scripts/check-run-state-kernel.ts | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/scripts/check-run-state-kernel.ts b/scripts/check-run-state-kernel.ts index 30f609830b..ba4daf9433 100644 --- a/scripts/check-run-state-kernel.ts +++ b/scripts/check-run-state-kernel.ts @@ -14,7 +14,7 @@ interface ModelState { run: RunState askCount: number completionAsks: number[] - lastEndedStreamCleaned: boolean + lastEndedStreamFailedAndCleaned: boolean } interface ModelEvent { @@ -263,7 +263,7 @@ const semanticWitnesses = { event.tag === "disposeRequested" && prev.run.phase === "completed" && next.run.latches.disposed, "stream-after-failure-cleanup": ({ prev, next, event }: WitnessContext) => event.tag === "streamStarted" && - prev.lastEndedStreamCleaned && + prev.lastEndedStreamFailedAndCleaned && !prev.run.latches.abort && next.run.stream.tag === "live" && !next.run.stream.cleanupFinished && @@ -289,7 +289,12 @@ const semanticWitnesses = { } satisfies Record boolean> function initialState(): ModelState { - return { run: structuredClone(initialRunState), askCount: 0, completionAsks: [], lastEndedStreamCleaned: false } + return { + run: structuredClone(initialRunState), + askCount: 0, + completionAsks: [], + lastEndedStreamFailedAndCleaned: false, + } } function stable(value: unknown): unknown { @@ -435,7 +440,8 @@ function apply(options: Options, state: ModelState, { event }: ModelEvent): Appl if (event.ask.tag === "completion") next.completionAsks = [...state.completionAsks, event.ask.askTs] } if (event.tag === "streamEnded" && state.run.stream.tag === "live") { - next.lastEndedStreamCleaned = state.run.stream.cleanupFinished + next.lastEndedStreamFailedAndCleaned = + state.run.stream.cleanupFinished && state.run.latches.reason === "streaming_failed" } return { next, accepted, problems } } From d670011c227007cb5eaab2e1ba9de921d00575c7 Mon Sep 17 00:00:00 2001 From: Elliott de Launay Date: Mon, 2 Nov 2026 20:48:35 -0500 Subject: [PATCH 4/5] test(run-state): track the stream failure per stream in the checker --- scripts/check-run-state-kernel.ts | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/scripts/check-run-state-kernel.ts b/scripts/check-run-state-kernel.ts index ba4daf9433..bce13476dd 100644 --- a/scripts/check-run-state-kernel.ts +++ b/scripts/check-run-state-kernel.ts @@ -15,6 +15,7 @@ interface ModelState { askCount: number completionAsks: number[] lastEndedStreamFailedAndCleaned: boolean + currentStreamFailed: boolean } interface ModelEvent { @@ -294,6 +295,7 @@ function initialState(): ModelState { askCount: 0, completionAsks: [], lastEndedStreamFailedAndCleaned: false, + currentStreamFailed: false, } } @@ -439,9 +441,12 @@ function apply(options: Options, state: ModelState, { event }: ModelEvent): Appl next.askCount = event.ask.askTs if (event.ask.tag === "completion") next.completionAsks = [...state.completionAsks, event.ask.askTs] } + if (event.tag === "reasonSet" && event.reason === "streaming_failed" && state.run.stream.tag === "live") { + next.currentStreamFailed = state.currentStreamFailed || state.run.latches.reason === undefined + } if (event.tag === "streamEnded" && state.run.stream.tag === "live") { - next.lastEndedStreamFailedAndCleaned = - state.run.stream.cleanupFinished && state.run.latches.reason === "streaming_failed" + next.lastEndedStreamFailedAndCleaned = state.run.stream.cleanupFinished && state.currentStreamFailed + next.currentStreamFailed = false } return { next, accepted, problems } } From 6c66e34a4efa9bcc8ca985714b8f8041d460b928 Mon Sep 17 00:00:00 2001 From: Elliott de Launay Date: Wed, 4 Nov 2026 20:24:19 -0500 Subject: [PATCH 5/5] test(run-state): add an unsafe kernel for a rejected turn event --- docs/architecture/task-lifecycle-model.md | 2 +- scripts/check-run-state-kernel.ts | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/docs/architecture/task-lifecycle-model.md b/docs/architecture/task-lifecycle-model.md index 93d7ac639f..5352156402 100644 --- a/docs/architecture/task-lifecycle-model.md +++ b/docs/architecture/task-lifecycle-model.md @@ -294,7 +294,7 @@ The checker also requires: - named witnesses, each tied to an event and the states around it: abort during a pending approval in a live stream, an ask after the stream ends, abandon after the stream ends, dispose after completion, a new stream after a failure cleanup without abort, a stream that starts without user input, an approval before the first stream, and a rejected late completion accept after a newer ask; - every ordered pair of the stream, ask, cancel, and dispose event sources to follow each other, where both events change the state; - no unseen successor at the depth bound; -- thirty-three known-unsafe kernels, each of which the checker must reject. They include a throwing kernel, a kernel that returns nothing, and one kernel for each check that runs at every search step without the table; and +- thirty-four known-unsafe kernels, each of which the checker must reject. They include a throwing kernel, a kernel that returns nothing, and one kernel for each check that runs at every search step without the table; and - self-tests that a small depth bound and a small state budget each fail the checker. The kernel has no resume event. A resumed task is `initialized` followed by `streamStarted` or `askStarted`. The witnesses `first-stream-without-ask` and `approval-before-first-stream` cover those paths. diff --git a/scripts/check-run-state-kernel.ts b/scripts/check-run-state-kernel.ts index bce13476dd..23cc156ef0 100644 --- a/scripts/check-run-state-kernel.ts +++ b/scripts/check-run-state-kernel.ts @@ -821,6 +821,11 @@ const unsafeKernels: Record = { caughtBy: differsFor("turnStarted"), useTable: true, }, + "turn-event-rejected": { + step: (state, event) => (event.tag === "toolUsed" ? { rejected: state } : nextRunState(state, event)), + caughtBy: /toolUsed was rejected/, + useTable: false, + }, "stream-start-resets-turn": { step: (state, event) => { const result = nextRunState(state, event)