[Docs] Add exhaustive task lifecycle verification GAP report

docs/architecture/native-tool-call-parser-scoping-model.md

@@ -12,7 +12,7 @@ For focused debugging, run this submodel directly with:
 pnpm parser-scope:model-check
 ```
 
-The command is composed into the same verification suite, but this remains a separate protocol and state space from the persisted task lifecycle model and shared-store concurrency model. It owns its parser-scoping invariants and adds no parser state to `HistoryItem` or `taskLifecycle.ts`; instead, it replays the public production `NativeToolCallParser` APIs using two independent scope objects.
+The command runs this check sequentially with the other lifecycle checks, but this remains a separate protocol and state space from the persisted task lifecycle model and shared-store concurrency model. It owns its parser-scoping invariants and adds no parser state to `HistoryItem` or `taskLifecycle.ts`; instead, it replays the public production `NativeToolCallParser` APIs using two independent scope objects. The authoritative [lifecycle coverage audit and issue tracker](./task-lifecycle-model.md#coverage-audit) records its evidence class and cross-model limits.
 
 ## Bounds and replay
 

docs/architecture/task-cleanup-protocol-model.md

@@ -14,6 +14,8 @@ pnpm cleanup-protocol:model-check
 
 This is a separate child model from the persisted task lifecycle and shared-store concurrency models. It follows the native tool-call parser model pattern: keep an independent bounded state space for an independent protocol, require every action and semantic landmark to remain reachable, and connect the abstract claims to focused production tests.
 
+The authoritative [lifecycle coverage audit and issue tracker](./task-lifecycle-model.md#coverage-audit) classifies how this abstract model relates to production and other submodels.
+
 ## Bounds and environment actions
 
 The model uses two tasks and explores every reachable interleaving through depth 20, with an explicit 100,000-state budget. Abort, disposal, final-save, provider abort/drain phases, and shutdown-cursor state are modeled directly. Independent abort and disposal calls may interleave freely, while provider-initiated calls are gated to the current shutdown task. Cleanup and editor-reversion settlement or rejection are environment actions, so the explorer does not assume they eventually occur.

package.json

@@ -13,7 +13,7 @@
 		"check-types": "turbo check-types --log-order grouped --output-logs new-only",
 		"test": "turbo test --log-order grouped --output-logs new-only",
 		"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",
+		"lifecycle:model-check": "tsx scripts/check-task-lifecycle.ts && tsx scripts/check-task-store-concurrency.ts && tsx scripts/check-provider-handoff-scheduler.ts && tsx scripts/check-task-fanout-protocol.ts && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts",
 		"cleanup-protocol:model-check": "tsx scripts/check-task-cleanup-protocol.ts",
 		"parser-scope:model-check": "node scripts/run-native-tool-call-parser-scoping.mjs",
 		"mcp:integration-check": "tsx scripts/check-mcp-oauth-integration.ts",

scripts/check-provider-handoff-scheduler.ts

@@ -147,6 +147,18 @@ for (const scenario of PROFILE_SCENARIOS) {
 	assert.equal(parentContext.apiConfiguration.consecutiveMistakeLimit, 3, `${scenario.name}: parent context mutated`)
 }
 
+const downstreamConsumerWitness = selectHandoffExecutionContext(
+	{ ...parentContext, mode: "orchestrator" },
+	"code",
+	"orchestrator",
+	false,
+)
+assert.notEqual(
+	downstreamConsumerWitness.mode,
+	"orchestrator",
+	"#921/#1623 witness requires task-local and shared provider modes to diverge",
+)
+
 const fixed = explore(FIXED_POLICY, false)
 const counterexamples = LEGACY_POLICIES.map((policy) => {
 	const result = explore(policy, true)
@@ -156,7 +168,7 @@ const counterexamples = LEGACY_POLICIES.map((policy) => {
 })
 
 console.log(
-	`Provider handoff/scheduler model check passed: ${fixed.states} distinct reachable states, ${PROFILE_SCENARIOS.length}/${PROFILE_SCENARIOS.length} profile scenarios, ${fixed.actions.size}/${EXPECTED_ACTIONS.length} actions, ${fixed.landmarks.size}/${Object.keys(LANDMARKS).length} landmarks, depth <= ${MAX_DEPTH}, states <= ${MAX_STATES}, ${counterexamples.length}/${LEGACY_POLICIES.length} legacy counterexamples`,
+	`Provider handoff/scheduler model check passed: ${fixed.states} distinct reachable states, ${PROFILE_SCENARIOS.length}/${PROFILE_SCENARIOS.length} profile scenarios, 1/1 downstream shared-mode witness, ${fixed.actions.size}/${EXPECTED_ACTIONS.length} actions, ${fixed.landmarks.size}/${Object.keys(LANDMARKS).length} landmarks, depth <= ${MAX_DEPTH}, states <= ${MAX_STATES}, ${counterexamples.length}/${LEGACY_POLICIES.length} legacy counterexamples`,
 )
 for (const counterexample of counterexamples) {
 	console.log(

scripts/check-task-fanout-protocol.ts

@@ -0,0 +1,224 @@
+import assert from "node:assert/strict"
+
+const CHILDREN = ["a", "b"] as const
+type Child = (typeof CHILDREN)[number]
+type ChildState = "idle" | "running" | "ready" | "delivered" | "cancelled"
+
+type ModelState = {
+	parentLive: boolean
+	children: Record<Child, ChildState>
+	permitOwners: Child[]
+	resultWriters: Partial<Record<Child, Child>>
+	deliveries: Child[]
+	deliveryAfterParentLoss: boolean
+}
+
+type Transition = { name: string; kind: string; next: ModelState }
+type TraceStep = { action: string; state: ModelState }
+
+const MAX_DEPTH = 10
+const MAX_STATES = 500
+const EXPECTED_ACTIONS = ["launch", "finish", "deliver", "lose-parent", "cancel-orphan", "release"] as const
+const LANDMARKS = {
+	"live-parent-with-two-children": (state: ModelState) =>
+		state.parentLive && CHILDREN.every((child) => state.children[child] === "running"),
+	"out-of-order-results": (state: ModelState) => state.deliveries.join(",") === "b,a",
+	"single-writer-results": (state: ModelState) =>
+		CHILDREN.every((child) => state.resultWriters[child] === undefined || state.resultWriters[child] === child),
+	"parent-loss-with-running-child": (state: ModelState) =>
+		!state.parentLive && CHILDREN.some((child) => state.children[child] === "running"),
+	"orphan-cleanup": (state: ModelState) =>
+		!state.parentLive && CHILDREN.every((child) => !["running", "ready"].includes(state.children[child])),
+} satisfies Record<string, (state: ModelState) => boolean>
+
+const start = initialState()
+const queue: Array<{ state: ModelState; trace: TraceStep[] }> = [
+	{ state: start, trace: [{ action: "initial", state: start }] },
+]
+const visited = new Set([canonical(start)])
+const actions = new Set<string>()
+const landmarks = new Set<string>()
+const frontier: ModelState[] = []
+
+const KNOWN_BAD_STATES: Array<{ name: string; state: ModelState; expected: string }> = [
+	{
+		name: "wrong-result-writer",
+		state: {
+			...initialState(),
+			children: { a: "ready", b: "idle" },
+			permitOwners: ["a"],
+			resultWriters: { a: "b" },
+		},
+		expected: "a: result has the wrong writer",
+	},
+	{
+		name: "early-delivery",
+		state: { ...initialState(), children: { a: "delivered", b: "idle" }, deliveries: ["a"] },
+		expected: "a: result delivered before readiness",
+	},
+	{
+		name: "duplicate-delivery",
+		state: {
+			...initialState(),
+			children: { a: "delivered", b: "idle" },
+			resultWriters: { a: "a" },
+			deliveries: ["a", "a"],
+		},
+		expected: "a: result delivered more than once",
+	},
+	{
+		name: "post-parent-loss-delivery",
+		state: { ...initialState(), parentLive: false, deliveryAfterParentLoss: true },
+		expected: "result routed after parent loss",
+	},
+	{
+		name: "scheduler-over-allocation",
+		state: { ...initialState(), permitOwners: ["a", "b", "a"] },
+		expected: "scheduler capacity exceeded",
+	},
+]
+
+for (const unsafe of KNOWN_BAD_STATES) {
+	assert.ok(invariantViolations(unsafe.state).includes(unsafe.expected), `${unsafe.name}: invariant did not fire`)
+}
+
+for (let index = 0; index < queue.length; index++) {
+	const node = queue[index]!
+	for (const [name, predicate] of Object.entries(LANDMARKS)) {
+		if (predicate(node.state)) landmarks.add(name)
+	}
+	const violations = invariantViolations(node.state)
+	assert.deepEqual(violations, [], formatViolation(violations, node.trace))
+	if (node.trace.length - 1 === MAX_DEPTH) {
+		frontier.push(node.state)
+		continue
+	}
+
+	for (const transition of transitions(node.state)) {
+		actions.add(transition.kind)
+		const trace = [...node.trace, { action: transition.name, state: transition.next }]
+		const nextViolations = invariantViolations(transition.next)
+		assert.deepEqual(nextViolations, [], formatViolation(nextViolations, trace))
+		const key = canonical(transition.next)
+		if (visited.has(key)) continue
+		visited.add(key)
+		queue.push({ state: transition.next, trace })
+		assert.ok(visited.size <= MAX_STATES, `exceeded ${MAX_STATES}-state budget`)
+	}
+}
+
+const missingActions = EXPECTED_ACTIONS.filter((action) => !actions.has(action))
+assert.deepEqual(missingActions, [], `unreachable actions: ${missingActions.join(", ")}`)
+const missingLandmarks = Object.keys(LANDMARKS).filter((name) => !landmarks.has(name))
+assert.deepEqual(missingLandmarks, [], `unreachable landmarks: ${missingLandmarks.join(", ")}`)
+const unseen = frontier.flatMap(transitions).find(({ next }) => !visited.has(canonical(next)))
+assert.equal(unseen, undefined, `depth ${MAX_DEPTH} has unseen successor ${unseen?.name}`)
+
+console.log(
+	`Task fan-out protocol model check passed: ${visited.size} distinct reachable states, ${actions.size}/${EXPECTED_ACTIONS.length} actions, ${landmarks.size}/${Object.keys(LANDMARKS).length} landmarks, ${KNOWN_BAD_STATES.length}/${KNOWN_BAD_STATES.length} unsafe counterexamples, depth <= ${MAX_DEPTH}, states <= ${MAX_STATES}`,
+)
+
+function transitions(state: ModelState): Transition[] {
+	const result: Transition[] = []
+	for (const child of CHILDREN) {
+		if (state.parentLive && state.children[child] === "idle" && state.permitOwners.length < 2) {
+			result.push(
+				action(`launch(${child})`, "launch", state, (next) => {
+					next.children[child] = "running"
+					next.permitOwners.push(child)
+				}),
+			)
+		}
+		if (state.children[child] === "running") {
+			result.push(
+				action(`finish(${child})`, "finish", state, (next) => {
+					next.children[child] = "ready"
+					next.resultWriters[child] = child
+				}),
+			)
+		}
+		if (state.parentLive && state.children[child] === "ready" && state.resultWriters[child] === child) {
+			result.push(
+				action(`deliver(${child}, parent)`, "deliver", state, (next) => {
+					next.children[child] = "delivered"
+					next.deliveries.push(child)
+				}),
+			)
+		}
+		if (!state.parentLive && ["running", "ready"].includes(state.children[child])) {
+			result.push(
+				action(`cancel-orphan(${child})`, "cancel-orphan", state, (next) => {
+					next.children[child] = "cancelled"
+				}),
+			)
+		}
+		if (state.permitOwners.includes(child) && ["delivered", "cancelled"].includes(state.children[child])) {
+			result.push(
+				action(`release(${child})`, "release", state, (next) => {
+					next.permitOwners = next.permitOwners.filter((owner) => owner !== child)
+				}),
+			)
+		}
+	}
+	if (state.parentLive && CHILDREN.some((child) => state.children[child] !== "idle")) {
+		result.push(
+			action("lose-parent", "lose-parent", state, (next) => {
+				next.parentLive = false
+			}),
+		)
+	}
+	return result
+}
+
+function invariantViolations(state: ModelState): string[] {
+	const violations: string[] = []
+	if (new Set(state.permitOwners).size !== state.permitOwners.length) violations.push("duplicate permit owner")
+	if (state.permitOwners.length > 2) violations.push("scheduler capacity exceeded")
+	if (state.deliveryAfterParentLoss) violations.push("result routed after parent loss")
+	for (const child of CHILDREN) {
+		const active = ["running", "ready"].includes(state.children[child])
+		if (active && !state.permitOwners.includes(child)) violations.push(`${child}: active without permit ownership`)
+		if (state.children[child] === "idle" && state.permitOwners.includes(child)) {
+			violations.push(`${child}: idle child owns a permit`)
+		}
+		if (state.resultWriters[child] !== undefined && state.resultWriters[child] !== child) {
+			violations.push(`${child}: result has the wrong writer`)
+		}
+		if (state.deliveries.filter((delivered) => delivered === child).length > 1) {
+			violations.push(`${child}: result delivered more than once`)
+		}
+		if (state.children[child] === "delivered" && state.resultWriters[child] !== child) {
+			violations.push(`${child}: result delivered before readiness`)
+		}
+	}
+	return violations
+}
+
+function initialState(): ModelState {
+	return {
+		parentLive: true,
+		children: { a: "idle", b: "idle" },
+		permitOwners: [],
+		resultWriters: {},
+		deliveries: [],
+		deliveryAfterParentLoss: false,
+	}
+}
+
+function action(name: string, kind: string, state: ModelState, update: (next: ModelState) => void): Transition {
+	const next = structuredClone(state)
+	update(next)
+	return { name, kind, next }
+}
+
+function canonical(state: ModelState): string {
+	return JSON.stringify({ ...state, permitOwners: [...state.permitOwners].sort() })
+}
+
+function formatViolation(violations: string[], trace: TraceStep[]): string {
+	return [
+		violations.join("; "),
+		`Bounds: depth=${MAX_DEPTH}, states=${MAX_STATES}`,
+		...trace.map((step, index) => `${index}. ${step.action}\n   ${canonical(step.state)}`),
+	].join("\n")
+}