Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions docs/architecture/task-lifecycle-model.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,15 @@ Zoo Code checks task lifecycle protocols through one compositional verification
pnpm lifecycle:model-check
```

The command runs six independent bounded submodels in sequence:
The command runs seven independent bounded submodels in sequence:

1. the persisted task delegation lifecycle;
2. shared-store concurrency across task-history hosts;
3. production-backed provider handoff and scheduler ordering;
4. the task cleanup protocol;
5. request-stream parser scoping; and
6. completion persistence.
5. request-stream parser scoping;
6. completion persistence; and
7. API retry and logical-user-turn persistence.

This umbrella command is the single model-check entry point in the `compile` CI job after type checking. Command-level composition does not merge the submodels' state spaces: each checker retains its own bounds, transitions, invariant ownership, reachability requirements, and counterexample format. In particular, parser state is not part of the persisted lifecycle graph. The focused parser checker remains directly runnable with `pnpm parser-scope:model-check` for debugging.

Expand Down Expand Up @@ -124,6 +125,8 @@ The completion persistence checker additionally enforces:
4. Delegated completion crosses the same durability boundary as standalone completion and requires successful parent reopen.
5. A failed delegated parent reopen cannot emit the delegated completion event.

The API retry/persistence checker additionally enforces that automatic retries are bounded and visible, terminal `max_tokens` empty responses cannot re-enter automatic retry, and the logical user turn keeps the same `messageId` and timestamp across retry/restoration.

These are safety claims within the documented bounds. The checks do not claim liveness, fairness, power-loss durability, filesystem-lock correctness, or exhaustive coverage of arbitrary task counts or retry counts. The completion explorer specifies the event contract rather than importing `Task` or `AttemptCompletionTool`; focused unit tests and the restart E2E verify that concrete production paths implement the modeled guards. Delegated reopen is abstracted as one success-or-failure event after durable child history; fallback from a failed reopen into the normal standalone completion flow remains production-test coverage rather than part of this model. The lifecycle checker also does not distinguish a delayed pre-interruption completion from a legitimate post-resume completion for the same child ID; that requires a persisted attempt/generation token before it can become a sound invariant.

## Open-issue traceability
Expand Down
2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
Expand Up @@ -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 && pnpm cleanup-protocol:model-check && pnpm parser-scope:model-check && tsx scripts/check-completion-persistence.ts && tsx scripts/check-api-retry-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",
Expand Down
93 changes: 93 additions & 0 deletions scripts/check-api-retry-persistence.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
type StopReason = "none" | "max_tokens"
type Phase = "requesting" | "waiting" | "confirming" | "terminal"

interface State {
attempt: number
phase: Phase
visibleRetries: number
messageId: string
timestamp: number
stopReason: StopReason
}

interface Transition {
name: string
next: State
}

const MAX_RETRIES = 3
const initial: State = {
attempt: 0,
phase: "requesting",
visibleRetries: 0,
messageId: "logical-user-turn",
timestamp: 1,
stopReason: "none",
}

function transitions(state: State): Transition[] {
if (state.phase === "terminal") return []
if (state.phase === "waiting") {
return [{ name: "finish-visible-delay", next: { ...state, phase: "requesting" } }]
}
if (state.phase === "confirming") {
return [
{ name: "decline-retry", next: { ...state, phase: "terminal" } },
{ name: "confirm-retry", next: { ...state, attempt: 0, phase: "requesting" } },
]
}
if (state.stopReason === "max_tokens") {
return [{ name: "surface-terminal-stop", next: { ...state, phase: "terminal" } }]
}
if (state.attempt >= MAX_RETRIES) {
return [{ name: "exhaust-automatic-retries", next: { ...state, phase: "confirming" } }]
}
return [
{
name: "retry-visible",
next: {
...state,
attempt: state.attempt + 1,
visibleRetries: state.visibleRetries + 1,
phase: "waiting",
},
},
{
name: "receive-max-tokens-empty",
next: { ...state, stopReason: "max_tokens" },
},
]
}

const queue: Array<{ state: State; depth: number }> = [{ state: initial, depth: 0 }]
const seen = new Set<string>()
const landmarks = new Set<string>()

while (queue.length > 0) {
const current = queue.shift()!
const key = JSON.stringify(current.state)
if (seen.has(key)) continue
seen.add(key)

const state = current.state
if (state.attempt > MAX_RETRIES) throw new Error("automatic retry bound exceeded")
if (state.visibleRetries < state.attempt) throw new Error("retry occurred without a visible announcement")
if (state.messageId !== initial.messageId || state.timestamp !== initial.timestamp) {
throw new Error("logical user-turn identity changed across retry/restoration")
}
if (state.stopReason === "max_tokens" && state.phase === "waiting") {
throw new Error("terminal max_tokens response silently re-entered retry")
}

if (state.phase === "confirming" && state.attempt === MAX_RETRIES) landmarks.add("bounded-exhaustion")
if (state.stopReason === "max_tokens" && state.phase === "terminal") landmarks.add("terminal-max-tokens")
if (state.visibleRetries === MAX_RETRIES) landmarks.add("all-retries-visible")
if (current.depth >= 10) continue
for (const transition of transitions(state)) queue.push({ state: transition.next, depth: current.depth + 1 })
}

for (const landmark of ["bounded-exhaustion", "terminal-max-tokens", "all-retries-visible"]) {
if (!landmarks.has(landmark)) throw new Error(`semantic landmark unreachable: ${landmark}`)
}

console.log(`API retry/persistence model check passed (${seen.size} states)`)
Loading
Loading