From c0c96649a492cca26f68a77ecc62d9a8a53517a5 Mon Sep 17 00:00:00 2001 From: Hack Dance <344842+roodboi@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:05:25 -0400 Subject: [PATCH 1/4] docs(supervisor): review statechart before formal modeling --- docs/statechart.md | 140 +++++++++++++++++++++++++++++++++++++++ docs/supervisor-usage.md | 70 ++++++++++++++++++++ 2 files changed, 210 insertions(+) create mode 100644 docs/statechart.md create mode 100644 docs/supervisor-usage.md diff --git a/docs/statechart.md b/docs/statechart.md new file mode 100644 index 00000000..4a17f5b2 --- /dev/null +++ b/docs/statechart.md @@ -0,0 +1,140 @@ +# Supervisor job statechart and property derivation + +- Walkthrough: [supervisor-usage.md](supervisor-usage.md). +- Source revision: `08e0412a9fa063c33f4145b569c36afc5810e606`; no uncommitted product changes. +- Saved before modeling: 2026-10-23. The reviewed documentation is committed before any project TLA+ file. +- Boundary: the exported job runner, filesystem job store, service composition, and adjacent shell service. These are unsupported experimental surfaces, explicitly inspected for this verification task. + +## Code states + +```mermaid +stateDiagram-v2 + [*] --> Queued: T1 create + Queued --> Starting: T2 read / T3 persist starting + Starting --> Running: T4 spawn / T5 persist running and event + Starting --> Failed: T4 spawn fails + Running --> Claimed: T6 cancel or T7 exit and drain + Claimed --> TerminalMetadata: T8 write chosen status + TerminalMetadata --> TerminalEvent: T9 append event and update metadata + TerminalEvent --> CancelAcknowledged: T10 accepted cancellation + TerminalEvent --> Returned: T11 exit and drain finished + Claimed --> Rejected: T12 persistence failure + TerminalMetadata --> Rejected: T12 persistence failure + CancelAcknowledged --> Returned: T11 exit and drain finished + Returned --> Starting: T13 caller invokes runJob again +``` + +A terminal **outcome claim** is local to one invocation. There is no durable execution +claim, lease, queue consumer, attempt counter, or retry policy. `awaiting_input` is +accepted by the store parser but has no transition in these runner/service paths. +A cancelled job can still have a live process; metadata and process state are distinct. + +## User flow + +```mermaid +stateDiagram-v2 + [*] --> Submitted: U1 create job + Submitted --> Observing: U2 read metadata / events / logs + Observing --> CancelRequested: U3 cancel + CancelRequested --> CancelVisible: T10 successful response + CancelRequested --> Unavailable: T14 not_found / not_running + CancelRequested --> PersistenceError: T12 rejected promise + CancelVisible --> Observing: U2 process may still run + Observing --> Result: T11 run promise settles + Result --> Submitted: U4 submit again creates another job +``` + +Caller deadlines are external; this service supplies no job timeout or automatic retry. +A shell close response means a signal was sent, not that exit was observed. + +## Transition map + +Paths below are relative to `src/control-plane/extensions/supervisor/`. + +| ID | Trigger / guard / effect | Source :: function | Atomic boundary and observable result | Status | +| --- | --- | --- | --- | --- | +| T1 / U1 | Create UUID; write queued metadata and created event; start runner | `service.ts :: createJob`; `job-store.ts :: createJob` | Several awaited filesystem operations; returned metadata is the initial snapshot | Existing | +| T2 | Read existing metadata; require command, but do not check status or ownership | `runner.ts :: runJob` | Awaited read; another invocation may read the same job | Existing | +| T3 | Persist starting; append starting event | `runner.ts :: runJob`; `job-store.ts :: updateJobStatus, appendEvent` | Separate read/write, event append, and metadata rewrite awaits | Existing | +| T4 | Spawn process, or record failed status/event on spawn exception | `runner.ts :: runJob` | Synchronous spawn; error persistence awaits; no cancellation handle yet | Existing | +| T5 | Persist running and started event, then register cancellation callback | `runner.ts :: runJob`; `service.ts :: onSpawn` | Process is already live before persistence and registration finish | Existing | +| T6 | Cancel if no non-cancelled terminal outcome; signal once; choose cancelled | `runner.ts :: cancel, finish` | Signal and local terminal claim before first persistence await; repeated cancel shares `terminalWrite` | Existing | +| T7 | Observe process exit and drain both streams; choose completed/failed unless already claimed | `runner.ts :: runJob, finish, pipeStreamToFiles` | Exit and drain are independent waits; local outcome arbitration is synchronous | Existing | +| T8 | Persist chosen status | `runner.ts :: finish`; `job-store.ts :: updateJobStatus` | Read metadata, then write replacement; no compare-and-swap | Existing | +| T9 | Append terminal event, then rewrite metadata with sequence | `job-store.ts :: appendEventInternal` | Append and metadata write are separate; failure may occur between them | Existing | +| T10 / U3 | Resolve accepted cancellation only after T8/T9 complete | `runner.ts :: cancel`; `service.ts :: cancelJob` | Does not await process exit or pipe drain; repeated accepted requests reuse result | Existing | +| T11 | Resolve run after exit/drain and terminal persistence; remove service map entry | `runner.ts :: runJob`; `service.ts :: finally` | A process that never exits can keep the run pending after cancellation acknowledgement | Existing | +| T12 | Persistence rejects; preserve already claimed outcome; otherwise service attempts failed fallback | `service.ts :: catch`; `runner.ts :: finish` | No retry after a claimed terminal write fails; fallback can also reject | Existing | +| T13 | Invoke exported runner on same job again, including terminal jobs | `runner.ts :: runJob` | New independent local variables; no stored status guard | Existing low-level caller composition; not an advertised retry endpoint | +| T14 | Cancel missing job or missing local handle, or after another terminal outcome claims | `service.ts :: cancelJob` | Store read precedes local map lookup; return `not_found` or `not_running` | Existing | +| T15 / U4 | Resubmit create request | `service.ts :: createJob` | New UUID each call; no idempotency key | Existing; no transport retry deduplication | +| T16 | Create PTY and shell; publish running metadata; close sends signal; exit updates metadata/listeners; expire after ten minutes | `shell-service.ts :: createShell, closeShell, attachShell, handleShellExit` | In-memory session map; signal acknowledgement distinct from exit callback; no job-store writes | Existing separate lifecycle | +| T17 | Acquire durable execution ownership, bound retries, recover abandoned work | No implementation in these files | No claim/retry/recovery API to invoke | Absent requested guarantees, not a modeled existing transition | +| T18 / U2 | Read metadata/events/logs | `service.ts :: getJob, listJobs`; `job-store.ts :: readJobMeta, readEvents` | Reads can observe intermediate persistence; malformed metadata returns null | Existing | + +## Properties derived from transitions + +Hypotheses below are recorded before TLC. Names are stable check identifiers. + +| Check | Promise and harm | Transitions | Promise source / scope | Kind and model property | Bounds / fairness | Sensitivity and real-code replay | +| --- | --- | --- | --- | --- | --- | --- | +| P1 | At most one live runner per stored job; duplicate side effects otherwise | T2–T5, T13 | Requested job-wide guarantee; service normally creates fresh UUIDs | Safety `SingleRunner` | One job, two invocations; no fairness needed | Remove reference admission guard; two actual runner calls overlap on one stored job | +| P2 | After cancellation acknowledgement no process runs; post-cancel side effects otherwise | T6, T8–T11, T13 | Requested stronger guarantee; current documentation promises persisted outcome only | Safety `CancelQuiescent` | One job; signal may be ignored; separate exit transition | Reorder reference acknowledgement before exit; actual process dependency remains live after successful cancel | +| P3 | Retrying the same logical job does not execute it twice; repeated side effects otherwise | T2–T5, T11, T13, T15 | Requested idempotency; automatic retry and attempt budget are absent | Safety `RetryIdempotent` | One job, two sequential invocations; count executions rather than a set | Remove reference duplicate guard; actual runner executes a terminal job again | +| P4 | Every locally claimed outcome reaches durable terminal status and event | T6–T12 | Requested progress; current implementation exposes persistence errors without recovery | Liveness `ClaimedTerminal` | One invocation; weak fairness for enabled persistence, exit, and drain; one transient write rejection allowed | Disable reference recovery after rejected persistence; actual service rejects and retains running metadata despite subsequent store availability | +| P5 | Within one invocation, accepted cancellation preserves one cancelled terminal outcome/event | T6–T10 | Existing documented promise | Safety `CancelWins` | One invocation; successful persistence, no external store writers | Remove local finish memoization; actual cancellation/exit race attempts a second terminal write | + +The reference admission, exit-wait, deduplication, and persistence recovery controls are +hypothetical and must be labeled separately. Their passes are sensitivity controls, +not evidence that those fixes exist. Every property gets its own mutation config and +behavioral replay; no known failure may mask another. + +## Observations before TLC + +- P1/P3 likely fail at the exported runner boundary: T2 accepts any existing status. + No current service path is claimed to schedule the same UUID twice. +- P2 likely fails for a process that ignores termination. This is already documented + behavior, but does not meet the requested stronger guarantee. +- P4 likely fails after a finite terminal persistence error. Fair scheduling cannot + execute a recovery action that does not exist. Successful-I/O progress must also + be checked separately; do not call the absence of a queue claim API a hang. +- P5 appears protected by a synchronous local claim and shared promise. A global + job-level interpretation would be false because T13 creates a new local arbiter. + This assumes callbacks do not throw or synchronously re-enter `finish`. +- The daemon client can retry a failed POST transmission once after readiness + recovery (`src/daemon/client.ts :: resolveDaemonJsonResponse`). A lost create + response can therefore lead to T15 and a new UUID. This is an additional + idempotency concern, not an automatic job retry or a modeled same-ID submission. +- Job-store operations are not transactions: concurrent read-modify-write operations + may lose sequence/status updates. The minimal model can restrict stores to serialized + operations for P1–P4 counterexamples; it must not claim general store linearizability. +- Shell close has the same signal-versus-exit distinction but no job persistence or + retry machinery. Review it as an adjacent boundary, not as a fictitious job runner. + +## Deliberate exclusions + +- Transport authorization, gateway delivery, process groups/descendants, daemon crashes, + corrupt files, shell listener exceptions, and arbitrary concurrent store writers. +- UUID collisions, multiple jobs, unbounded caller submissions, and retry backoff (absent). +- Filesystem failure coverage is a finite rejected terminal status write. Partial event + appends are documented above and covered by existing service tests, not claimed exhaustive. + +## Review gate + +- Reviewer: implementation agent (source review; no human approval claimed). +- Reviewed revision: `08e0412a9fa063c33f4145b569c36afc5810e606`; product diff: none. +- Evidence: all four scoped source files, `docs/supervisor.md`, existing runner/service + tests, supervisor command callers, and daemon service construction inspected. +- Checks: caller responses, missing retry/claim APIs, independent process and persisted + states, pre-registration window, terminal errors, atomicity, and all five property + derivations checked against source. +- Findings/resolutions: execution ownership is absent, so label T2 a read rather than + a claim; P4 uses the actual terminal claim; stronger guarantees remain explicit + hypotheses; separate actual behavior from hypothetical controls. Keep serialized + store schedules as a stated coverage limit rather than inventing an atomic store. +- Gate: reviewed; blocking issues: none. Independent review may append corrections + before modeling. Commit this review and walkthrough first. + +Independent source audit confirmed the transition boundaries and missing ownership +and retry mechanisms. It also identified the lost-POST composition above and the +T5 startup failure window; these remain source-derived concerns until replayed. diff --git a/docs/supervisor-usage.md b/docs/supervisor-usage.md new file mode 100644 index 00000000..fb9ee5fd --- /dev/null +++ b/docs/supervisor-usage.md @@ -0,0 +1,70 @@ +# Supervisor verification walkthrough + +This walkthrough describes source revision +`08e0412a9fa063c33f4145b569c36afc5810e606`, before modeling. The supervisor is an +unsupported experimental surface; verification does not change that support status. +See [the reviewed statechart](statechart.md) for transition IDs and property hypotheses. + +A caller uses `createSupervisorService().createJob` with a project directory and a +command. The service generates a UUID, writes queued metadata and a creation event, +and starts `runJob` in the background. It returns the original metadata plus a run +promise. The daemon retains one service instance; local command handlers construct +fresh instances. Cancellation handles exist only in the instance that started a job. +Reading metadata is not proof that a local cancellation handle exists. + +The runner reads metadata and selects the command, then writes `starting`, appends +`job.starting`, and spawns. It subsequently writes `running` and `job.started` before +calling `onSpawn`. During those awaits the process exists but cancellation is not yet +registered. A spawn failure records `failed`. A storage failure after spawn can leave +a live child without a registered handle; that window is documented, not a recovery +mechanism in the model. + +For normal completion the runner waits for process exit and both output streams to +drain. It claims a terminal outcome synchronously, then writes status and event. +Cancellation signals the child and claims `cancelled` before those writes. Whichever +path first claims the outcome owns the shared `terminalWrite` promise. Later accepted +cancellations reuse it; a completed or failed claim makes cancellation return false. +The service reports `not_found` for absent metadata and `not_running` for an absent +local handle or a rejected late cancellation. + +A successful cancellation response establishes persisted cancellation metadata and an +event. It does not establish process exit. A child that ignores the signal can keep +executing and leave the run promise pending. Terminal persistence errors reject the +cancel/run promise; the service preserves the claimed outcome instead of replacing it +with `failed`. No automatic recovery retries the failed persistence operation. + +The store reads and rewrites whole metadata files. An event append and its subsequent +metadata update are separate operations. The model must preserve the status/event +boundary. It restricts store interleavings where necessary and does not prove file +atomicity, cross-process coordination, or event sequence uniqueness under concurrent +writers. Existing service tests exercise failures before and after event append. + +There is no durable execution claim or retry API. Calling exported `runJob` twice +with the same stored ID creates two independent executions; calling it after terminal +completion also runs again. Resubmitting `createJob` creates a fresh UUID. These are +explicit caller-composition tests for the requested job-wide guarantees, not claims +that the current service contains an automatic retry loop. Automatic attempt count is +one per invocation; no configured retry budget or idempotency key exists. +The daemon client separately retries a failed transmission once after readiness +recovery. A create response lost after acceptance can cause a second UUID to be +created; this transport composition is outside the bounded same-ID runner model. + +Shells use a separate in-memory map and PTY. `createShell` returns running metadata, +`closeShell` sends a signal and returns a boolean, and the exit handler changes status +to exited, notifies listeners, closes the terminal, and schedules metadata removal. +Neither close nor attachment close waits for exit. Shells never enter the job store; +the job model does not imply durable shell recovery or shell retry guarantees. + +## Verification procedure + +Use the Bun version pinned by `package.json` and the repository Java selection. +From the repository root, run `bun run check:tla`. The command will verify the pinned +TLC jar, run each actual-code property separately, check passing reference controls +and must-fail mutations, replay the schedules against imported implementation code, +exercise isolated real-code mutations, and rerun the baseline. Tool failures and +unexpected passes must fail the command. Expected reproduced bugs are reported by +name; a successful harness does not mean the stronger product guarantees hold. + +The implementation and exact outcomes will be recorded in +`specs/fv/COVERAGE.md`. This pre-model walkthrough intentionally records hypotheses, +not TLC results. Product fixes require a separate change and are outside this task. From 7903351ccfb18664ad894ae98ca6371779424935 Mon Sep 17 00:00:00 2001 From: Hack Dance <344842+roodboi@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:09:18 -0400 Subject: [PATCH 2/4] docs(supervisor): resolve pre-model review ambiguities --- docs/statechart.md | 22 +++++++++++++++++----- docs/supervisor-usage.md | 13 +++++++++++-- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/docs/statechart.md b/docs/statechart.md index 4a17f5b2..c97fe07b 100644 --- a/docs/statechart.md +++ b/docs/statechart.md @@ -24,6 +24,11 @@ stateDiagram-v2 Returned --> Starting: T13 caller invokes runJob again ``` +T13 can also start a **second invocation while the first is active**. The second +invocation enters T2/T3 against the same metadata; each invocation has its own +process, terminal claim, and persistence promise. The diagram's returned edge is +only the sequential case, not a guard on T13. + A terminal **outcome claim** is local to one invocation. There is no durable execution claim, lease, queue consumer, attempt counter, or retry policy. `awaiting_input` is accepted by the store parser but has no transition in these runner/service paths. @@ -64,7 +69,7 @@ Paths below are relative to `src/control-plane/extensions/supervisor/`. | T9 | Append terminal event, then rewrite metadata with sequence | `job-store.ts :: appendEventInternal` | Append and metadata write are separate; failure may occur between them | Existing | | T10 / U3 | Resolve accepted cancellation only after T8/T9 complete | `runner.ts :: cancel`; `service.ts :: cancelJob` | Does not await process exit or pipe drain; repeated accepted requests reuse result | Existing | | T11 | Resolve run after exit/drain and terminal persistence; remove service map entry | `runner.ts :: runJob`; `service.ts :: finally` | A process that never exits can keep the run pending after cancellation acknowledgement | Existing | -| T12 | Persistence rejects; preserve already claimed outcome; otherwise service attempts failed fallback | `service.ts :: catch`; `runner.ts :: finish` | No retry after a claimed terminal write fails; fallback can also reject | Existing | +| T12 | Persistence rejects; cancellation rejects immediately; run reaches the rejection after exit/drain, then service preserves a claimed outcome | `service.ts :: catch`; `runner.ts :: finish` | Until exit/drain, run and map entry may remain live. Pre-claim startup errors instead reach the service failed fallback directly, which can settle with a child still alive | Existing | | T13 | Invoke exported runner on same job again, including terminal jobs | `runner.ts :: runJob` | New independent local variables; no stored status guard | Existing low-level caller composition; not an advertised retry endpoint | | T14 | Cancel missing job or missing local handle, or after another terminal outcome claims | `service.ts :: cancelJob` | Store read precedes local map lookup; return `not_found` or `not_running` | Existing | | T15 / U4 | Resubmit create request | `service.ts :: createJob` | New UUID each call; no idempotency key | Existing; no transport retry deduplication | @@ -79,8 +84,8 @@ Hypotheses below are recorded before TLC. Names are stable check identifiers. | Check | Promise and harm | Transitions | Promise source / scope | Kind and model property | Bounds / fairness | Sensitivity and real-code replay | | --- | --- | --- | --- | --- | --- | --- | | P1 | At most one live runner per stored job; duplicate side effects otherwise | T2–T5, T13 | Requested job-wide guarantee; service normally creates fresh UUIDs | Safety `SingleRunner` | One job, two invocations; no fairness needed | Remove reference admission guard; two actual runner calls overlap on one stored job | -| P2 | After cancellation acknowledgement no process runs; post-cancel side effects otherwise | T6, T8–T11, T13 | Requested stronger guarantee; current documentation promises persisted outcome only | Safety `CancelQuiescent` | One job; signal may be ignored; separate exit transition | Reorder reference acknowledgement before exit; actual process dependency remains live after successful cancel | -| P3 | Retrying the same logical job does not execute it twice; repeated side effects otherwise | T2–T5, T11, T13, T15 | Requested idempotency; automatic retry and attempt budget are absent | Safety `RetryIdempotent` | One job, two sequential invocations; count executions rather than a set | Remove reference duplicate guard; actual runner executes a terminal job again | +| P2 | After cancellation acknowledgement no process for that stored job runs; post-cancel side effects otherwise | T6, T8–T11, T13 | Requested job-wide guarantee; current documentation promises persisted outcome only | Safety `CancelQuiescent` | One job, two invocations; signal may be ignored; acknowledgement is sticky | Reference waits for exit and prevents a second admission; mutation removes exit wait while retaining admission protection; actual process stays live after cancel and a later invocation can restart the job | +| P3 | Retrying the same stored job ID does not execute it twice; repeated side effects otherwise | T2–T5, T11, T13 | Requested same-ID idempotency; automatic retry and attempt budget are absent; T15 logical-request deduplication is separate and excluded | Safety `RetryIdempotent` | One job, two sequential invocations; count executions rather than a set | Remove reference duplicate guard; actual runner executes a terminal job again | | P4 | Every locally claimed outcome reaches durable terminal status and event | T6–T12 | Requested progress; current implementation exposes persistence errors without recovery | Liveness `ClaimedTerminal` | One invocation; weak fairness for enabled persistence, exit, and drain; one transient write rejection allowed | Disable reference recovery after rejected persistence; actual service rejects and retains running metadata despite subsequent store availability | | P5 | Within one invocation, accepted cancellation preserves one cancelled terminal outcome/event | T6–T10 | Existing documented promise | Safety `CancelWins` | One invocation; successful persistence, no external store writers | Remove local finish memoization; actual cancellation/exit race attempts a second terminal write | @@ -132,9 +137,16 @@ behavioral replay; no known failure may mask another. a claim; P4 uses the actual terminal claim; stronger guarantees remain explicit hypotheses; separate actual behavior from hypothetical controls. Keep serialized store schedules as a stated coverage limit rather than inventing an atomic store. -- Gate: reviewed; blocking issues: none. Independent review may append corrections - before modeling. Commit this review and walkthrough first. +- Gate: reviewed; blocking issues: none after the corrections below. Commit this + review and walkthrough first. Independent source audit confirmed the transition boundaries and missing ownership and retry mechanisms. It also identified the lost-POST composition above and the T5 startup failure window; these remain source-derived concerns until replayed. + +Independent pre-model documentation review identified four blocking ambiguities: +the diagram omitted overlapping T13 invocations; T12 conflated immediate cancel +rejection with eventual run rejection; P2 lacked job-wide reference admission +protection; P3 conflated same-ID execution with new-UUID resubmission. All four are +resolved above and in the walkthrough before any TLA+ file is created. Reviewer: +independent source-review agent; reviewed source revision remains the full SHA above. diff --git a/docs/supervisor-usage.md b/docs/supervisor-usage.md index fb9ee5fd..d2d3fb3d 100644 --- a/docs/supervisor-usage.md +++ b/docs/supervisor-usage.md @@ -30,8 +30,12 @@ local handle or a rejected late cancellation. A successful cancellation response establishes persisted cancellation metadata and an event. It does not establish process exit. A child that ignores the signal can keep executing and leave the run promise pending. Terminal persistence errors reject the -cancel/run promise; the service preserves the claimed outcome instead of replacing it -with `failed`. No automatic recovery retries the failed persistence operation. +cancel promise immediately; the run reaches that rejected persistence promise only +after process exit and stream drain. Until then its service handle may remain live. +When run rejects, the service preserves the claimed outcome instead of replacing it +with `failed`. Pre-claim startup errors instead reach the failed fallback directly, +which can settle without stopping a spawned child. No automatic recovery retries +the failed terminal persistence operation. The store reads and rewrites whole metadata files. An event append and its subsequent metadata update are separate operations. The model must preserve the status/event @@ -49,6 +53,11 @@ The daemon client separately retries a failed transmission once after readiness recovery. A create response lost after acceptance can cause a second UUID to be created; this transport composition is outside the bounded same-ID runner model. +P2 keeps cancellation acknowledgement sticky across both bounded invocations of the +same job. Its hypothetical reference both waits for exit and prevents re-admission; +the mutation removes only the exit wait. P3 covers same stored ID re-execution, +not T15's distinct UUIDs or logical-request deduplication. + Shells use a separate in-memory map and PTY. `createShell` returns running metadata, `closeShell` sends a signal and returns a boolean, and the exit handler changes status to exited, notifies listeners, closes the terminal, and schedules metadata removal. From e63c85dbb1c1c60b1d9aacd26a17140d422b5eb7 Mon Sep 17 00:00:00 2001 From: Hack Dance <344842+roodboi@users.noreply.github.com> Date: Fri, 23 Oct 2026 11:24:05 -0400 Subject: [PATCH 3/4] test(supervisor): restore pinned TLA checks and replay lifecycle gaps --- .factory/skills/control-plane-worker/SKILL.md | 3 + .gitignore | 15 + AGENTS.md | 4 + mise.toml | 3 + package.json | 1 + scripts/check-supervisor-replays.ts | 304 ++++++++++++++ scripts/check-tla-models.ts | 265 ++++++++++++ scripts/lib/tla-checks.ts | 63 +++ scripts/lib/tla-result.ts | 78 ++++ scripts/lib/tla-toolchain.ts | 154 +++++++ specs/fv/COVERAGE.md | 144 +++++++ specs/tla/P1.cfg | 9 + specs/tla/P2.cfg | 9 + specs/tla/P3.cfg | 9 + specs/tla/P4.cfg | 9 + specs/tla/P5.cfg | 9 + specs/tla/README.md | 46 +++ specs/tla/SupervisorJob.tla | 196 +++++++++ specs/tla/mutations/P1.cfg | 9 + specs/tla/mutations/P2.cfg | 9 + specs/tla/mutations/P3.cfg | 9 + specs/tla/mutations/P4.cfg | 9 + specs/tla/mutations/P5.cfg | 9 + specs/tla/reference/P1.cfg | 9 + specs/tla/reference/P2.cfg | 9 + specs/tla/reference/P3.cfg | 9 + specs/tla/reference/P4.cfg | 9 + specs/tla/reference/P4SuccessfulIO.cfg | 9 + tests/supervisor-formal-replay.test.ts | 382 ++++++++++++++++++ tests/supervisor-startup-replay.test.ts | 111 +++++ tests/tla-result.test.ts | 353 ++++++++++++++++ 31 files changed, 2257 insertions(+) create mode 100644 mise.toml create mode 100644 scripts/check-supervisor-replays.ts create mode 100644 scripts/check-tla-models.ts create mode 100644 scripts/lib/tla-checks.ts create mode 100644 scripts/lib/tla-result.ts create mode 100644 scripts/lib/tla-toolchain.ts create mode 100644 specs/fv/COVERAGE.md create mode 100644 specs/tla/P1.cfg create mode 100644 specs/tla/P2.cfg create mode 100644 specs/tla/P3.cfg create mode 100644 specs/tla/P4.cfg create mode 100644 specs/tla/P5.cfg create mode 100644 specs/tla/README.md create mode 100644 specs/tla/SupervisorJob.tla create mode 100644 specs/tla/mutations/P1.cfg create mode 100644 specs/tla/mutations/P2.cfg create mode 100644 specs/tla/mutations/P3.cfg create mode 100644 specs/tla/mutations/P4.cfg create mode 100644 specs/tla/mutations/P5.cfg create mode 100644 specs/tla/reference/P1.cfg create mode 100644 specs/tla/reference/P2.cfg create mode 100644 specs/tla/reference/P3.cfg create mode 100644 specs/tla/reference/P4.cfg create mode 100644 specs/tla/reference/P4SuccessfulIO.cfg create mode 100644 tests/supervisor-formal-replay.test.ts create mode 100644 tests/supervisor-startup-replay.test.ts create mode 100644 tests/tla-result.test.ts diff --git a/.factory/skills/control-plane-worker/SKILL.md b/.factory/skills/control-plane-worker/SKILL.md index d6bca134..36a80560 100644 --- a/.factory/skills/control-plane-worker/SKILL.md +++ b/.factory/skills/control-plane-worker/SKILL.md @@ -21,6 +21,9 @@ mission; do not assume those files or tools exist in ordinary tasks. 5. Complete required checks and report exact results and remaining uncertainty. Known warning-only diagnostics do not become a new blocker unless the change worsens them. Failed required checks still need repair. + For stateful control-plane changes, use `tlaplus-workbench`, review the saved + statechart and usage walkthrough before modeling, and run `bun run check:tla`. + Consult `specs/fv/COVERAGE.md` for scope, known bugs, and source sync revisions. 6. Stop only task-owned temporary processes. Record useful learning and actionable follow-up within authorization; skip empty handoff or ticket paperwork. diff --git a/.gitignore b/.gitignore index 01ee730c..aeb9fc00 100644 --- a/.gitignore +++ b/.gitignore @@ -80,6 +80,11 @@ zig-out/ SPECS/ +# Track the bounded verification suite even on case-insensitive filesystems. +!/specs/ +/specs/* +!/specs/tla/ +!/specs/fv/ _DOCS TODO.md REVIEW.md @@ -87,3 +92,13 @@ REVIEW.md dist .tmp + +# TLA+ tools and generated model-checking data +.tlc/ +states/ +*_TTrace_*.tla +*_TTrace_*.bin +*_TTrace_*.cfg +SpecTE.tla +SpecTE.cfg +*.jar diff --git a/AGENTS.md b/AGENTS.md index 50036763..8088b70f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -61,6 +61,10 @@ agent changes need source/render parity and actual client loading when relevant. Distinguish local tests, hosted CI, installed versions, and published artifacts. A required check failing is a blocker; unrelated optional integration warnings are not. +For stateful control-plane changes, use `tlaplus-workbench`: save and review the +statechart and usage walkthrough before modeling, then run `bun run check:tla`. +See `specs/fv/COVERAGE.md` for property scope, known bugs, and source sync revisions. + ## Runtime and secrets Use Hack for its managed runtime. Never hand-edit `.hack/.internal/` or `.hack/.branch/`. diff --git a/mise.toml b/mise.toml new file mode 100644 index 00000000..40711759 --- /dev/null +++ b/mise.toml @@ -0,0 +1,3 @@ +[tools] +bun = "1.3.9" +java = "temurin-17.0.20+101" diff --git a/package.json b/package.json index 0d0cf22a..ac5731df 100644 --- a/package.json +++ b/package.json @@ -52,6 +52,7 @@ "turbo:test": "bunx turbo run test", "turbo:check": "bunx turbo run check", "check": "bun run privacy:check && bun run turbo:check", + "check:tla": "bun run scripts/check-tla-models.ts", "prepare": "husky", "release:prepare": "bunx semantic-release --no-ci", "typecheck": "bun run turbo:typecheck", diff --git a/scripts/check-supervisor-replays.ts b/scripts/check-supervisor-replays.ts new file mode 100644 index 00000000..e8eaccde --- /dev/null +++ b/scripts/check-supervisor-replays.ts @@ -0,0 +1,304 @@ +import { cp, mkdir, mkdtemp, rm, symlink } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { join, resolve } from "node:path"; + +/** Expected findings, not a claim that the requested product guarantees pass. */ +export const replayManifest = [ + { id: "P1", property: "SingleRunner", actual: "VIOLATION" }, + { id: "P2", property: "CancelQuiescent", actual: "VIOLATION" }, + { id: "P3", property: "RetryIdempotent", actual: "VIOLATION" }, + { id: "P4", property: "ClaimedTerminal", actual: "VIOLATION" }, + { id: "P5", property: "CancelWins", actual: "PASS" }, +] as const; + +export type Replay = (typeof replayManifest)[number]; +const repoRoot = resolve(import.meta.dir, ".."); +const testFile = "tests/supervisor-formal-replay.test.ts"; +const runnerFile = "src/control-plane/extensions/supervisor/runner.ts"; +const modeVariable = "HACK_SUPERVISOR_STRICT_REPLAY"; + +export function replayMarker(opts: { + readonly replay: Replay; + readonly outcome: "PASS" | "VIOLATION"; +}): string { + return `SUPERVISOR_REPLAY:${opts.replay.id}:${opts.replay.property}:${opts.outcome}`; +} + +type StrictReplayOptions = { + readonly replay: Replay; + readonly expected: "PASS" | "VIOLATION"; + readonly root?: string; +}; + +/** Only an exact named oracle result and the corresponding single-test exit count. */ +export async function runStrictReplay( + opts: StrictReplayOptions +): Promise { + if (Bun.version !== "1.3.9") { + throw new Error("Supervisor replays require Bun 1.3.9"); + } + const dataRoot = await mkdtemp(join(tmpdir(), "hack-supervisor-data-")); + try { + await runReplayProcess({ ...opts, dataRoot }); + } finally { + await rm(dataRoot, { recursive: true, force: true }); + } +} + +async function runReplayProcess( + opts: StrictReplayOptions & { readonly dataRoot: string } +): Promise { + const proc = Bun.spawn( + [process.execPath, "test", `./${testFile}`, "--timeout", "10000"], + { + cwd: opts.root ?? repoRoot, + env: { + ...process.env, + [modeVariable]: opts.replay.id, + HACK_SUPERVISOR_REPLAY_DATA: opts.dataRoot, + NO_COLOR: "1", + FORCE_COLOR: "0", + }, + stdout: "pipe", + stderr: "pipe", + } + ); + let timedOut = false; + const timer = setTimeout(() => { + timedOut = true; + proc.kill("SIGKILL"); + }, 15_000); + try { + const [exitCode, stdout, stderr] = await Promise.all([ + proc.exited, + new Response(proc.stdout).text(), + new Response(proc.stderr).text(), + ]); + const violation = opts.expected === "VIOLATION"; + const [banner, marker, ...extra] = stdout.trim().split("\n"); + const expectedMarker = replayMarker({ + replay: opts.replay, + outcome: opts.expected, + }); + const summary = violation ? /\b0 pass\s+1 fail\b/ : /\b1 pass\s+0 fail\b/; + if ( + timedOut || + exitCode !== (violation ? 1 : 0) || + !/^bun test v1\.3\.9 \([a-z0-9]+\)$/.test(banner ?? "") || + marker !== expectedMarker || + extra.length !== 0 || + !summary.test(stderr) || + (violation && + !stderr.includes( + `PropertyViolation: Requested property violated: ${opts.replay.property}` + )) || + /unhandled|error between tests|timed out/i.test(stderr) + ) { + throw new Error( + `${opts.replay.id} ${opts.replay.property}: rejected replay evidence (exit=${exitCode}, timeout=${timedOut}); expected ${opts.expected}` + ); + } + } finally { + clearTimeout(timer); + if (proc.exitCode === null) { + proc.kill("SIGKILL"); + await proc.exited; + } + } +} + +type Replacement = { readonly before: string; readonly after: string }; +const admissionAnchor = " const command = opts.command ?? meta.command;"; +const terminalAdmissionCondition = + '["completed", "failed", "cancelled"].includes(meta.status)'; +const terminalWrite = ` await opts.jobStore.updateJobStatus({ + jobId: opts.jobId, + status: input.status, + });`; +const memoization = ` if (terminalWrite) { + return terminalWrite; + } +`; + +/** Bounded reference controls only; these are never applied to product files. */ +function referenceControl(replay: Replay): readonly Replacement[] { + switch (replay.id) { + case "P1": + return [ + admissionControl( + 'meta.status === "starting" || meta.status === "running"' + ), + ]; + case "P2": + return [ + admissionControl(terminalAdmissionCondition), + { + before: + ' await finish({ status: "cancelled" });\n return true;', + after: + ' await finish({ status: "cancelled" });\n await proc.exited;\n return true;', + }, + ]; + case "P3": + return [admissionControl(terminalAdmissionCondition)]; + case "P4": + return [ + { + before: terminalWrite, + after: ` try { +${terminalWrite} + } catch { +${terminalWrite} + }`, + }, + ]; + case "P5": + return []; + default: + throw new Error("Unknown replay"); + } +} + +function admissionControl(condition: string): Replacement { + return { + before: admissionAnchor, + after: ` if (${condition}) { + return { jobId: opts.jobId, status: meta.status, exitCode: 0 }; + } + +${admissionAnchor}`, + }; +} + +function replaceExactlyOnce(source: string, edit: Replacement): string { + if (source.split(edit.before).length !== 2) { + throw new Error("Replay control anchor drift: expected exactly one match"); + } + return source.replace(edit.before, edit.after); +} + +function applyEdits(source: string, edits: readonly Replacement[]): string { + let result = source; + for (const edit of edits) { + result = replaceExactlyOnce(result, edit); + } + return result; +} + +async function checkActual(label: string): Promise { + for (const replay of replayManifest) { + await runStrictReplay({ replay, expected: replay.actual }); + process.stdout.write( + `${label} ${replay.id} ${replay.property}: ${replay.actual}\n` + ); + } +} + +/** Extra implementation evidence; this is not a sixth formal property. */ +async function checkStartupPersistence(): Promise { + const dataRoot = await mkdtemp( + join(tmpdir(), "hack-supervisor-startup-data-") + ); + try { + const proc = Bun.spawn( + [ + process.execPath, + "test", + "./tests/supervisor-startup-replay.test.ts", + "--timeout", + "10000", + ], + { + cwd: repoRoot, + env: { + ...process.env, + HACK_SUPERVISOR_REPLAY_DATA: dataRoot, + NO_COLOR: "1", + FORCE_COLOR: "0", + }, + stdout: "pipe", + stderr: "pipe", + } + ); + const timer = setTimeout(() => proc.kill("SIGKILL"), 15_000); + try { + const [exitCode, stdout, stderr] = await Promise.all([ + proc.exited, + new Response(proc.stdout).text(), + new Response(proc.stderr).text(), + ]); + if ( + exitCode !== 0 || + !/^bun test v1\.3\.9 \([a-z0-9]+\)\n$/.test(stdout) || + !/\b2 pass\s+0 fail\b/.test(stderr) + ) { + throw new Error("Startup persistence characterization failed"); + } + process.stdout.write( + "characterization startup persistence (running status, job.started): BUG REPRODUCED\n" + ); + } finally { + clearTimeout(timer); + if (proc.exitCode === null) { + proc.kill("SIGKILL"); + await proc.exited; + } + } + } finally { + await rm(dataRoot, { recursive: true, force: true }); + } +} + +async function main(): Promise { + await checkActual("actual"); + await checkStartupPersistence(); + const scratch = await mkdtemp(join(tmpdir(), "hack-supervisor-controls-")); + try { + await cp(join(repoRoot, "src"), join(scratch, "src"), { recursive: true }); + await mkdir(join(scratch, "tests")); + await mkdir(join(scratch, "scripts")); + await cp(join(repoRoot, testFile), join(scratch, testFile)); + await cp( + import.meta.path, + join(scratch, "scripts/check-supervisor-replays.ts") + ); + await symlink( + join(repoRoot, "node_modules"), + join(scratch, "node_modules") + ); + const runnerPath = join(scratch, runnerFile); + const actual = await Bun.file(runnerPath).text(); + for (const replay of replayManifest) { + const edits = referenceControl(replay); + const reference = applyEdits(actual, edits); + if (edits.length > 0) { + await Bun.write(runnerPath, reference); + await runStrictReplay({ replay, expected: "PASS", root: scratch }); + process.stdout.write( + `scratch reference ${replay.id} ${replay.property}: PASS\n` + ); + } + // P2 keeps terminal admission protection; only early acknowledgement is mutated. + const removedControls = replay.id === "P2" ? edits.slice(1) : edits; + const mutation = + replay.id === "P5" + ? [{ before: memoization, after: "" }] + : removedControls + .toReversed() + .map((edit) => ({ before: edit.after, after: edit.before })); + await Bun.write(runnerPath, applyEdits(reference, mutation)); + await runStrictReplay({ replay, expected: "VIOLATION", root: scratch }); + process.stdout.write( + `scratch mutation ${replay.id} ${replay.property}: VIOLATION\n` + ); + await Bun.write(runnerPath, actual); + } + } finally { + await rm(scratch, { recursive: true, force: true }); + } + await checkActual("restored actual"); +} + +if (import.meta.main) { + await main(); +} diff --git a/scripts/check-tla-models.ts b/scripts/check-tla-models.ts new file mode 100644 index 00000000..556c07da --- /dev/null +++ b/scripts/check-tla-models.ts @@ -0,0 +1,265 @@ +#!/usr/bin/env bun +// Generic runner restored from c15fd8117547a11148f540ae9bbc0b4baf9c30b9; +// property catalogs and domain-specific result checks are intentionally external. +import { mkdir } from "node:fs/promises"; +import { dirname, isAbsolute, relative, resolve } from "node:path"; +import { CHECKS, type TlaCheck } from "./lib/tla-checks.ts"; +import { type TlaExpectation, verifyTlaResult } from "./lib/tla-result.ts"; +import { + resolveTlaJar, + runTlaProcess, + TLA_JAVA_FLAGS, + TLA_LAUNCHER, + TLA_TOOL, + withTlaScratch, +} from "./lib/tla-toolchain.ts"; + +type TlaRun = { + readonly check: TlaCheck; + readonly config: string; + readonly expected: TlaExpectation; + readonly phase: string; +}; + +export function validateTlaChecks(checks: readonly TlaCheck[]): void { + if (checks.length === 0) { + throw new Error("TLA+ manifest is empty; verification is blocked."); + } + const ids = new Set(); + for (const check of checks) { + if (!check.id || ids.has(check.id)) { + throw new Error(`Missing or duplicate TLA+ check id: ${check.id}.`); + } + ids.add(check.id); + if (!/^[A-Za-z_][A-Za-z0-9_]*$/.test(check.mutation.expected.property)) { + throw new Error(`Invalid property name for ${check.id}.`); + } + validateCheckPaths(check); + if ( + !check.mutation.config.includes("/mutations/") || + check.mutation.config === check.baseline.config + ) { + throw new Error(`Missing separate mutation config for ${check.id}.`); + } + if (check.baseline.expected.kind !== "pass") { + if (!check.reference) { + throw new Error( + `Known finding ${check.id} needs a passing reference control.` + ); + } + if ( + check.baseline.expected.kind !== check.mutation.expected.kind || + check.baseline.expected.property !== check.mutation.expected.property + ) { + throw new Error( + `Baseline and mutation must check the same property for ${check.id}.` + ); + } + } + } +} + +function validateCheckPaths(check: TlaCheck): void { + const configs = [check.baseline, check.mutation, ...passingControls(check)]; + for (const path of [ + check.module, + ...configs.map((config) => config.config), + ]) { + if (isAbsolute(path) || path.split(/[\\/]/).includes("..")) { + throw new Error(`TLA+ paths must be repository-relative: ${path}.`); + } + } + if ( + !check.module.endsWith(".tla") || + configs.some((config) => !config.config.endsWith(".cfg")) + ) { + throw new Error(`Expected .tla module and .cfg configs for ${check.id}.`); + } +} + +function passingControls(check: TlaCheck) { + return [ + ...(check.reference ? [check.reference] : []), + ...(check.controls ?? []), + ]; +} + +export async function runTlaSequence(opts: { + readonly checks: readonly TlaCheck[]; + readonly runCheck: (run: TlaRun) => Promise; + readonly runReplays: () => Promise; +}): Promise { + validateTlaChecks(opts.checks); + const baselines = async (phase: string) => { + for (const check of opts.checks) { + await opts.runCheck({ check, ...check.baseline, phase }); + for (const control of passingControls(check)) { + await opts.runCheck({ check, ...control, phase: `${phase} control` }); + } + } + }; + await baselines("baseline"); + for (const check of opts.checks) { + await opts.runCheck({ check, ...check.mutation, phase: "mutation" }); + } + await opts.runReplays(); + await baselines("restored baseline"); +} + +async function copyModelSources(opts: { + source: string; + target: string; +}): Promise { + for await (const file of new Bun.Glob("**/*.{tla,cfg}").scan({ + cwd: opts.source, + onlyFiles: true, + followSymlinks: false, + })) { + const target = resolve(opts.target, file); + await mkdir(dirname(target), { recursive: true }); + await Bun.write(target, Bun.file(resolve(opts.source, file))); + } +} + +export async function runTlaModel( + opts: TlaRun & { + readonly root: string; + readonly jar: string; + readonly java: string; + } +): Promise { + await withTlaScratch(async (scratch) => { + const source = dirname(resolve(opts.root, opts.check.module)); + const configPath = relative(source, resolve(opts.root, opts.config)); + if (configPath.startsWith("..") || isAbsolute(configPath)) { + throw new Error(`Config must be in the model directory: ${opts.config}.`); + } + const directory = resolve(scratch, "source"); + await copyModelSources({ source, target: directory }); + const module = resolve( + directory, + relative(source, resolve(opts.root, opts.check.module)) + ); + const config = resolve(directory, configPath); + if ( + !((await Bun.file(module).exists()) && (await Bun.file(config).exists())) + ) { + throw new Error( + `Missing module or config for ${opts.check.id}: ${opts.config}.` + ); + } + const launcher = resolve(scratch, "CheckedTlc.java"); + await Bun.write(launcher, TLA_LAUNCHER); + const javaTmp = resolve(scratch, "tmp"); + await mkdir(javaTmp); + const { kind, property } = opts.check.mutation.expected; + const result = await runTlaProcess({ + cwd: directory, + command: [ + opts.java, + ...TLA_JAVA_FLAGS, + `-Djava.io.tmpdir=${javaTmp}`, + "-cp", + opts.jar, + launcher, + kind, + property, + config, + "-tool", + "-workers", + "1", + "-fp", + "0", + "-seed", + "1", + "-metadir", + resolve(scratch, "states"), + "-config", + config, + module, + ], + }); + process.stdout.write(result.output); + if ( + !( + result.output.includes(TLA_TOOL.banner) && + verifyTlaResult({ ...result, expected: opts.expected }) + ) + ) { + throw new Error( + `${opts.check.id} ${opts.phase} rejected (exit=${result.exitCode}, interrupted=${result.failed}): ${opts.config}.` + ); + } + const outcome = + opts.expected.kind === "pass" + ? "pass" + : `expected ${opts.expected.kind} violation of ${opts.expected.property}`; + process.stdout.write( + `${opts.check.id} ${opts.phase}: ${outcome}; exit=${result.exitCode}\n` + ); + }); +} + +async function main(): Promise { + const args = process.argv.slice(2); + if (args.some((arg) => arg !== "--download")) { + throw new Error("Usage: bun scripts/check-tla-models.ts [--download]"); + } + if (Bun.version !== "1.3.9") { + throw new Error(`Use the pinned Bun 1.3.9; running ${Bun.version}.`); + } + validateTlaChecks(CHECKS); + const root = resolve(import.meta.dir, ".."); + const jar = await resolveTlaJar({ + root, + override: process.env.TLA2TOOLS_JAR, + download: args.includes("--download"), + }); + const java = process.env.JAVA_BIN ?? "java"; + const version = await runTlaProcess({ + command: [java, "-version"], + cwd: root, + }); + if ( + version.failed || + version.exitCode !== 0 || + !/version "17(?:\.|")/.test(version.output) + ) { + throw new Error( + `Java 17 is required; set JAVA_BIN or use mise exec.\n${version.output}` + ); + } + process.stdout.write( + `TLA+ jar=${jar}\nsha256=${TLA_TOOL.sha256}\n${version.output}\n` + ); + await runTlaSequence({ + checks: CHECKS, + runCheck: (run) => runTlaModel({ ...run, root, jar, java }), + runReplays: async () => { + const result = await runTlaProcess({ + command: [process.execPath, "scripts/check-supervisor-replays.ts"], + cwd: root, + }); + process.stdout.write(result.output); + if (result.failed || result.exitCode !== 0) { + throw new Error( + `Supervisor replay/sensitivity checks failed (exit=${result.exitCode}, interrupted=${result.failed}).` + ); + } + }, + }); + process.stdout.write( + "TLC expectations, mutation controls, replays, and restored baselines verified. Expected findings remain findings.\n" + ); +} + +if (import.meta.main) { + try { + await main(); + } catch (error) { + process.stderr.write( + `${error instanceof Error ? error.message : String(error)}\n` + ); + process.exitCode = 1; + } +} diff --git a/scripts/lib/tla-checks.ts b/scripts/lib/tla-checks.ts new file mode 100644 index 00000000..a17e0c1f --- /dev/null +++ b/scripts/lib/tla-checks.ts @@ -0,0 +1,63 @@ +import type { TlaExpectation, TlaViolation } from "./tla-result.ts"; + +export type TlaCheck = { + readonly id: string; + readonly module: string; + readonly baseline: { + readonly config: string; + readonly expected: TlaExpectation; + }; + readonly reference?: { + readonly config: string; + readonly expected: { readonly kind: "pass" }; + }; + readonly controls?: readonly { + readonly config: string; + readonly expected: { readonly kind: "pass" }; + }[]; + readonly mutation: { + readonly config: string; + readonly expected: TlaViolation; + }; +}; + +/** Paths are repository-relative. Each config enables exactly one named check. */ +export const CHECKS: readonly TlaCheck[] = [ + { id: "P1", property: "SingleRunner", kind: "invariant" }, + { id: "P2", property: "CancelQuiescent", kind: "invariant" }, + { id: "P3", property: "RetryIdempotent", kind: "invariant" }, + { id: "P4", property: "ClaimedTerminal", kind: "temporal" }, + { id: "P5", property: "CancelWins", kind: "invariant" }, +].map(({ id, property, kind }): TlaCheck => { + const violation: TlaViolation = { + kind: kind === "temporal" ? "temporal" : "invariant", + property, + }; + return { + id, + module: "specs/tla/SupervisorJob.tla", + baseline: { + config: `specs/tla/${id}.cfg`, + expected: id === "P5" ? { kind: "pass" } : violation, + }, + ...(id === "P5" + ? {} + : { + reference: { + config: `specs/tla/reference/${id}.cfg`, + expected: { kind: "pass" as const }, + }, + }), + ...(id === "P4" + ? { + controls: [ + { + config: "specs/tla/reference/P4SuccessfulIO.cfg", + expected: { kind: "pass" as const }, + }, + ], + } + : {}), + mutation: { config: `specs/tla/mutations/${id}.cfg`, expected: violation }, + }; +}); diff --git a/scripts/lib/tla-result.ts b/scripts/lib/tla-result.ts new file mode 100644 index 00000000..b0cc1990 --- /dev/null +++ b/scripts/lib/tla-result.ts @@ -0,0 +1,78 @@ +export type TlaViolation = { + readonly kind: "invariant" | "temporal"; + readonly property: string; +}; + +export type TlaExpectation = { readonly kind: "pass" } | TlaViolation; + +export type TlaResult = { + readonly exitCode: number | null; + readonly output: string; + readonly failed?: boolean; +}; + +const COMPLETED = /^Model checking completed\. No error has been found\.$/m; +const DISTINCT_STATES = + /\b([\d,]+) distinct states found, 0 states left on queue\b/; +const TOOL_MESSAGE = + /^@!@!@STARTMSG (\d+):(\d+) @!@!@\r?\n([\s\S]*?)^@!@!@ENDMSG \1 @!@!@$/gm; +const TOOL_FAILURE = + /(?:^|\n)(?:Parsing or semantic analysis failed\.|\*\*\* (?:Parse )?Errors?:|Exception in thread |Error:)/; + +/** Accept only completed TLC tool-mode output and the exact expected result. */ +export function verifyTlaResult( + opts: TlaResult & { + readonly expected: TlaExpectation; + } +): boolean { + if (opts.failed || opts.exitCode === null || TOOL_FAILURE.test(opts.output)) { + return false; + } + const messages = Array.from(opts.output.matchAll(TOOL_MESSAGE), (match) => ({ + code: Number(match[1]), + severity: Number(match[2]), + body: match[3]?.trim() ?? "", + })); + if ( + messages.filter((message) => message.code === 2186).length !== 1 || + opts.output.split("@!@!@STARTMSG ").length - 1 !== messages.length || + opts.output.split("@!@!@ENDMSG ").length - 1 !== messages.length + ) { + return false; + } + const errors = messages.filter( + (message) => message.severity === 1 || message.severity === 2 + ); + if (opts.expected.kind === "pass") { + const states = DISTINCT_STATES.exec(opts.output)?.[1]?.replaceAll(",", ""); + return ( + opts.exitCode === 0 && + errors.length === 0 && + messages.some( + (message) => message.code === 2193 && COMPLETED.test(message.body) + ) && + Number(states) > 0 + ); + } + const { kind, property } = opts.expected; + const code = kind === "invariant" ? 2110 : 2116; + const diagnostic = + kind === "invariant" + ? `Invariant ${property} is violated.` + : `Temporal property ${property} was violated.`; + const allowedCodes = new Set([code, 2121, 2264]); + const violations = errors.filter((message) => message.code === code); + const temporalNames = opts.output + .split(/\r?\n/) + .filter((line) => /^Temporal property .+ was violated\.$/.test(line)); + return ( + opts.exitCode === (kind === "invariant" ? 12 : 13) && + errors.every((message) => allowedCodes.has(message.code)) && + violations.length === 1 && + (kind === "invariant" + ? violations[0]?.body === diagnostic + : violations[0]?.body === "Temporal properties were violated." && + temporalNames.length === 1 && + temporalNames[0] === diagnostic) + ); +} diff --git a/scripts/lib/tla-toolchain.ts b/scripts/lib/tla-toolchain.ts new file mode 100644 index 00000000..754442b2 --- /dev/null +++ b/scripts/lib/tla-toolchain.ts @@ -0,0 +1,154 @@ +import { link, mkdir, mkdtemp, rm } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { dirname, resolve } from "node:path"; +import type { TlaResult } from "./tla-result.ts"; + +/** Official v1.7.4 asset 184694200, checked against the retained pin on 2026-10-23. */ +export const TLA_TOOL = { + version: "1.7.4", + url: "https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar", + sha256: "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88", + banner: "TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)", +} as const; + +export const TLA_TIMEOUT_MS = 120_000; +export const TLA_JAVA_FLAGS = [ + "-Xmx512m", + "-XX:ActiveProcessorCount=1", + "-XX:+UseParallelGC", + "-XX:-UsePerfData", +] as const; + +export function verifyTlaChecksum(bytes: ArrayBuffer): void { + const actual = new Bun.CryptoHasher("sha256").update(bytes).digest("hex"); + if (actual !== TLA_TOOL.sha256) { + throw new Error( + `TLA+ jar checksum mismatch: expected ${TLA_TOOL.sha256}, got ${actual}.` + ); + } +} + +export async function resolveTlaJar(opts: { + readonly root: string; + readonly override?: string; + readonly download: boolean; +}): Promise { + const jar = resolve( + opts.root, + opts.override ?? `.cache/tlaplus/tla2tools-${TLA_TOOL.version}.jar` + ); + if (!(await Bun.file(jar).exists())) { + if (opts.override || !opts.download) { + throw new Error( + `Missing pinned TLA+ jar: ${jar}. Set TLA2TOOLS_JAR or rerun with --download.` + ); + } + await downloadTlaJar(jar); + } + verifyTlaChecksum(await Bun.file(jar).arrayBuffer()); + return jar; +} + +async function downloadTlaJar(jar: string): Promise { + const response = await fetch(TLA_TOOL.url, { + signal: AbortSignal.timeout(TLA_TIMEOUT_MS), + }); + if (!response.ok) { + throw new Error(`TLA+ download failed: HTTP ${response.status}.`); + } + const bytes = await response.arrayBuffer(); + verifyTlaChecksum(bytes); + await mkdir(dirname(jar), { recursive: true }); + const staging = await mkdtemp(resolve(dirname(jar), ".download-")); + try { + const downloaded = resolve(staging, "tla2tools.jar"); + await Bun.write(downloaded, bytes); + try { + await link(downloaded, jar); + } catch (error) { + if ( + !(error instanceof Error && "code" in error && error.code === "EEXIST") + ) { + throw error; + } + } + } finally { + await rm(staging, { recursive: true, force: true }); + } +} + +export async function runTlaProcess(opts: { + readonly command: readonly string[]; + readonly cwd: string; + readonly timeoutMs?: number; +}): Promise { + const child = Bun.spawn([...opts.command], { + cwd: opts.cwd, + stdin: "ignore", + stdout: "pipe", + stderr: "pipe", + timeout: opts.timeoutMs ?? TLA_TIMEOUT_MS, + killSignal: "SIGKILL", + }); + const [stdout, stderr, exitCode] = await Promise.all([ + new Response(child.stdout).text(), + new Response(child.stderr).text(), + child.exited, + ]); + return { + exitCode, + output: `${stdout}\n${stderr}`, + failed: child.signalCode !== null, + }; +} + +export async function withTlaScratch( + run: (scratch: string) => Promise +): Promise { + const scratch = await mkdtemp(resolve(tmpdir(), "hack-tla-")); + try { + return await run(scratch); + } finally { + await rm(scratch, { recursive: true, force: true }); + } +} + +/** + * The pinned TLC reports unnamed temporal failures. Its own config parser verifies + * that exactly one requested check is enabled; its message recorder names that + * property only when TLC emits the actual temporal-violation event. Java source + * launching keeps this adapter disposable and requires no compiled artifact. + * v1.7.4 generates no TE files unless -generateSpecTE is explicitly supplied. + */ +export const TLA_LAUNCHER = ` +import java.util.Arrays; +import tlc2.TLC; +import tlc2.output.EC; +import tlc2.output.MP; +import tlc2.output.MPRecorder; +import tlc2.tool.impl.ModelConfig; +import tlc2.util.Vect; +import util.SimpleFilenameToStream; + +class CheckedTlc { + public static void main(String[] args) throws Exception { + String kind = args[0]; + String property = args[1]; + ModelConfig config = new ModelConfig(args[2], new SimpleFilenameToStream()); + config.parse(); + Vect selected = kind.equals("temporal") ? config.getProperties() : config.getInvariants(); + Vect others = kind.equals("temporal") ? config.getInvariants() : config.getProperties(); + if (selected.size() != 1 || others.size() != 0 || !property.equals(selected.elementAt(0))) { + throw new IllegalArgumentException("Config must enable only " + kind + " " + property); + } + MP.setRecorder(new MPRecorder() { + @Override public void record(int code, Object... objects) { + if (code == EC.TLC_TEMPORAL_PROPERTY_VIOLATED && kind.equals("temporal")) { + System.out.println("Temporal property " + property + " was violated."); + } + } + }); + TLC.main(Arrays.copyOfRange(args, 3, args.length)); + } +} +`; diff --git a/specs/fv/COVERAGE.md b/specs/fv/COVERAGE.md new file mode 100644 index 00000000..c9a717a2 --- /dev/null +++ b/specs/fv/COVERAGE.md @@ -0,0 +1,144 @@ +# Supervisor verification coverage + +- Usage: [supervisor-usage.md](../../docs/supervisor-usage.md). +- Reviewed derivation: [statechart.md](../../docs/statechart.md), committed in + `c0c96649a492cca26f68a77ecc62d9a8a53517a5`; review corrections committed in + `7903351ccfb18664ad894ae98ca6371779424935` before the first specification. +- One repository rerun command: **`bun run check:tla`**. See + [setup](../tla/README.md) for pinned tools and first-run download. +- Product source reviewed and verified: **`08e0412a9fa063c33f4145b569c36afc5810e606`**. + No uncommitted product differences; this change contains verification only. +- TLC URL: `https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar`. +- Expected and independently verified downloaded SHA-256: + `936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`. +- Actual banner: `TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)`. +- Java: Temurin `17.0.20.1+1`, selected by mise pin `temurin-17.0.20+101`. + Flags: `-Xmx512m -XX:ActiveProcessorCount=1 -XX:+UseParallelGC -XX:-UsePerfData`, + TLC `-tool -workers 1 -fp 0 -seed 1`, + private metadir, 120-second subprocess timeout. Deadlock checking enabled; + `Idle` deliberately permits terminal stutter. No generated trace specs requested. +- Outputs: jar in ignored `.cache/tlaplus/`; raw TLC output on stdout, disposable + sources/state directories under the system temporary directory and removed. + Raw execution logs are not committed. TLC requires a local RMI listener. + +## Checks and source coverage + +All paths in this table are under `src/control-plane/extensions/supervisor/` unless +qualified. The common dependencies are `job-store.ts :: readJobMeta, updateJobStatus, +appendEvent, appendEventInternal` and `src/lib/fs.ts :: readTextFile, writeTextFile`. +The service map is a cancellation-handle registry, not execution ownership. +`StoreFree` explicitly prevents another modeled store call between a terminal +event append and its captured-metadata rewrite. This selects serialized real-code +schedules; it does not add a lock to the product. Process exit and local claims can +still interleave. Independent review caught and resolved an initially missing +restriction before final validation. +`commands.ts` and `src/daemon/server.ts` were reviewed as callers; only direct +same-ID runner composition and service cancellation are replayed. + +| Check / property | Transitions and model actions | Source and deterministic replay | Bound / assumptions | Full confirmed source sync | +| --- | --- | --- | --- | --- | +| P1 `SingleRunner` | T2–T5,T13; `Begin`, `Starting`, `Spawn`, `Running`, `Register` | `runner.ts :: runJob`; `service.ts :: createJob, onSpawn`; `singleRunner` replay starts B after A is registered but alive | One stored job, two invocations; serialized store operations; no fairness needed for safety | `08e0412a9fa063c33f4145b569c36afc5810e606` | +| P2 `CancelQuiescent` | T6,T8–T11,T13; `Cancel`, persistence, `Acknowledge`, `Exit`, `Begin` | `runner.ts :: cancel, finish`; `service.ts :: cancelJob`; `cancelQuiescent` checks live child at ack and same-ID restart | One job, two invocations; sticky acknowledgement; signals may be ignored; process exit separate from status | `08e0412a9fa063c33f4145b569c36afc5810e606` | +| P3 `RetryIdempotent` | T2–T5,T11,T13; `Begin`, `Spawn`, `Return` | `runner.ts :: runJob`; `retryIdempotent` executes completed ID again | One job, two sequential invocations; execution counter retains duplicate history; no actual automatic retry loop | `08e0412a9fa063c33f4145b569c36afc5810e606` | +| P4 `ClaimedTerminal` | T6–T12; `Cancel`/`Finish`, persistence, `RejectStatus`, `Return`; reference-only `Recover` | `runner.ts :: finish`; `service.ts :: catch, finally, cancelJob`; `claimedTerminal` injects one status failure and proves later storage availability | One invocation, one finite status rejection; weak fairness described below | `08e0412a9fa063c33f4145b569c36afc5810e606` | +| P5 `CancelWins` | T6–T10; `Cancel`, `Finish`, persistence, `Acknowledge` | `runner.ts :: finish, cancel`; `cancelWins` repeats cancellation then releases process exit | One invocation, successful storage, nonthrowing/nonreentrant callbacks, no external writer | `08e0412a9fa063c33f4145b569c36afc5810e606` | + +All checks use [SupervisorJob.tla](../tla/SupervisorJob.tla); actual configs are +`specs/tla/P1.cfg` through `P5.cfg`. Replay functions are in +`tests/supervisor-formal-replay.test.ts`, importing actual runner/store/service code. +Process exit and signal delivery are controlled dependencies; filesystem operations +use the real store. No timer selects a schedule. Subprocess timeouts only detect hangs. + +P4 uses the actual **terminal outcome claim**, not a nonexistent queue ownership +claim. Weak fairness is explicit for runnable continuations, status/event persistence, +exit, stream drain, acknowledgement, and reference recovery when enabled. Thus the +environment must eventually let processes exit, streams reach EOF, and nonfailed I/O +complete; no fairness forces a cancellation or a fault. One transient rejection may +disable actual persistence forever because there is no recovery action. The additional +`reference/P4SuccessfulIO.cfg` uses actual code with failures disabled and passes. +Fairness cannot establish unconditional job termination for arbitrary commands. + +## Must-fail controls + +Every config keeps its property enabled and changes behavior. Each is run by +`bun run check:tla`; its expected kind and exact name are checked by the generic +manifest/harness. P1–P4 have separately passing hypothetical controls before mutation. + +| Check | Checked-in mutation | Deliberate model break | Required failure | Corresponding isolated real-code break | +| --- | --- | --- | --- | --- | +| P1 | `specs/tla/mutations/P1.cfg` | Remove reference exclusive admission | exit 12, `Invariant SingleRunner is violated.` | Remove scratch active-status admission guard; two live children | +| P2 | `specs/tla/mutations/P2.cfg` | Permit acknowledgement before exit, retain reference duplicate-admission protection | exit 12, `Invariant CancelQuiescent is violated.` | Remove scratch `await proc.exited` from cancellation, retain terminal-ID admission guard | +| P3 | `specs/tla/mutations/P3.cfg` | Remove reference one-admission guard | exit 12, `Invariant RetryIdempotent is violated.` | Remove scratch terminal-ID guard; second sequential spawn | +| P4 | `specs/tla/mutations/P4.cfg` | Remove reference recovery after the one rejected write | exit 13, `Temporal property ClaimedTerminal was violated.` | Remove scratch one-time retry of terminal status write | +| P5 | `specs/tla/mutations/P5.cfg` | Remove existing terminal outcome memoization | exit 12, `Invariant CancelWins is violated.` | Remove `if (terminalWrite) return terminalWrite`; completion overwrites cancellation | + +Scratch reference guards reproduce the particular replay schedules; they are not +concurrent lock implementations. In particular, a status read/check is not atomic +reservation and cannot prove general P1/P2 admission safety. The model's hypothetical +reference admission is atomic; neither reference is presented as a product fix. +Original product files remain unchanged. Text anchors must match exactly once, then +the same behavioral oracle must pass with the reference and fail with the mutation. +A hash mismatch, parse error, timeout, or unrelated test failure cannot count. + +## Evidence and outcomes + +Observed on 2026-10-23. Distinct-state counts describe this finite abstraction and +its fixed configuration, not explored product schedules. Baseline and restored runs +matched. Each TLC invocation completed in seconds, below its 120-second limit. + +| Check | Actual baseline TLC | Passing control(s) | Mutation TLC | Actual replay / source mutation | Restored baseline | Outcome | +| --- | --- | --- | --- | --- | --- | --- | +| P1 | exit 12; named violation; 71 states before counterexample | hypothetical reference: 268 states, exit 0 | exit 12; same named violation | named violation / reference pass then named violation | same expected violation | **bug**: requested low-level job-wide guarantee absent | +| P2 | exit 12; named violation; 192 states before counterexample | hypothetical reference: 67 states, exit 0 | exit 12; 50 states; same named violation | named violation / reference pass then named violation | same expected violation | **bug**: requested stronger guarantee; current metadata-only contract is explicit | +| P3 | exit 12; named violation; 45 states before counterexample | hypothetical reference: 35 states, exit 0 | exit 12; same named violation | named violation / reference pass then named violation | same expected violation | **bug**: same-ID idempotency absent; no job retry policy implemented | +| P4 | exit 13; named temporal violation; 41 states | hypothetical recovery: 61 states; actual successful-I/O: 35 states; both exit 0 | exit 13; same named violation | named violation / reference pass then named violation | same expected violation | **bug** under finite persistence failure; **in sync** conditional successful-I/O progress | +| P5 | exit 0; 35 states | actual code is the passing control | exit 12; 38 states; named violation | pass / named violation after removing memoization | pass | **in sync** within one invocation | + +For each strict replay, a passing property requires exit 0 and exactly one passing +test. A violation requires exit 1, exactly one failing test, the exact property marker, +and its `PropertyViolation` error. The outer test/harness explicitly expects the +known finding. Zero wrapper exit means reproducible evidence, **not product green**. +All five model and implementation mutations demonstrated their intended failures. + +## Findings and limits + +- **F1 / P1:** starting a second exported `runJob` for one stored ID while the first + child is alive launches another child. Harm: duplicate command side effects. + Ordinary `createJob` creates a new UUID and calls the runner once; this replay is + a low-level composition gap, not evidence of duplicate UUID scheduling by the service. +- **F2 / P2:** cancel can acknowledge while its child is alive, and a later runner + call can execute the cancelled ID. Harm: work continues or restarts after cancel. + Existing documentation promises terminal persistence rather than process exit. +- **F3 / P3:** rerunning a completed stored ID spawns again. No idempotency key, + attempt counter, retry limit, or backoff exists. One invocation spawns at most once; + this does not establish a job-wide retry budget. Duplicate create-request handling + after a lost POST response creates a different UUID and is outside this model. +- **F4 / P4:** a transient cancelled-status write failure rejects cancellation; + after exit/drain the run rejects and the service drops its handle. Metadata remains + running with no terminal event despite restored store availability. Harm: stale + observable state without automatic recovery. No successful cancel was acknowledged. +- **F5 / additional real-code characterization:** after spawn, a rejected `running` + status write or `job.started` write makes the service fallback resolve the run as + failed while the child remains alive and cancellation returns `not_running`. + `tests/supervisor-startup-replay.test.ts` deterministically reproduces both paths + through the actual service/store and a controlled process. The repository check + runs these two cases once. This is extra bug evidence, not a sixth model property + or a claim of formal coverage of startup errors. Harm: an unmanaged live child. +- Shell creation, close, exit, and expiry were source-reviewed as separate in-memory + transitions (T16). There is no shell job claim or retry protocol. No shell model, + PTY behavior proof, or general shell cleanup guarantee is claimed. +- Not covered: process groups/descendants, daemon crashes/restarts, arbitrary commands + that never exit, corruption, partial writes beyond the finite status fault, + arbitrary concurrent store writers, global event sequence uniqueness, and transport + authorization. Existing runner/service tests additionally exercise partial event + persistence; they do not make this small model exhaustive. +- Product fixes: none. No introducing commit is assigned to these longstanding gaps. + +## Maintenance + +Initial verification sync is `08e0412a9fa063c33f4145b569c36afc5810e606` for every row. +The artifact-only documentation/checker commits do not advance that source marker. +After source changes, use `tlaplus-workbench-maintain`: inspect the covered diff, +new callers/writers and renamed paths, update/review the saved chart, run the command +including mutations and replays, and advance only confirmed per-check sync markers. +Do not weaken a property or accept unexpected passes merely to make the wrapper green. diff --git a/specs/tla/P1.cfg b/specs/tla/P1.cfg new file mode 100644 index 00000000..04297658 --- /dev/null +++ b/specs/tla/P1.cfg @@ -0,0 +1,9 @@ +\* actual; P1 / SingleRunner. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P1" + Actual = TRUE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT SingleRunner diff --git a/specs/tla/P2.cfg b/specs/tla/P2.cfg new file mode 100644 index 00000000..31992bd6 --- /dev/null +++ b/specs/tla/P2.cfg @@ -0,0 +1,9 @@ +\* actual; P2 / CancelQuiescent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P2" + Actual = TRUE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT CancelQuiescent diff --git a/specs/tla/P3.cfg b/specs/tla/P3.cfg new file mode 100644 index 00000000..79f694e0 --- /dev/null +++ b/specs/tla/P3.cfg @@ -0,0 +1,9 @@ +\* actual; P3 / RetryIdempotent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P3" + Actual = TRUE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT RetryIdempotent diff --git a/specs/tla/P4.cfg b/specs/tla/P4.cfg new file mode 100644 index 00000000..d54eb7b6 --- /dev/null +++ b/specs/tla/P4.cfg @@ -0,0 +1,9 @@ +\* actual; P4 / ClaimedTerminal. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P4" + Actual = TRUE + Mutation = FALSE + AllowFailure = TRUE +SPECIFICATION Spec +PROPERTY ClaimedTerminal diff --git a/specs/tla/P5.cfg b/specs/tla/P5.cfg new file mode 100644 index 00000000..06b20dfe --- /dev/null +++ b/specs/tla/P5.cfg @@ -0,0 +1,9 @@ +\* actual; P5 / CancelWins. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P5" + Actual = TRUE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT CancelWins diff --git a/specs/tla/README.md b/specs/tla/README.md new file mode 100644 index 00000000..6f93d6f3 --- /dev/null +++ b/specs/tla/README.md @@ -0,0 +1,46 @@ +# Supervisor model checks + +From the repository root: + +```sh +mise install +mise exec -- bun install --frozen-lockfile +mise exec -- bun run check:tla --download +``` + +The repository check command is **`bun run check:tla`**. With Bun 1.3.9 and Java 17 +already selected, run it directly. `--download` only bootstraps a missing jar; +subsequent checks use the verified cache. Alternatively, `TLA2TOOLS_JAR` selects an +existing jar and `JAVA_BIN` selects Java 17. Every jar is checked against the same +committed SHA-256 before execution; a mismatch fails without replacing the file. + +The restored tooling comes from source commit +`c15fd8117547a11148f540ae9bbc0b4baf9c30b9`. Only the checker structure, generic +result validation, tool pin, and relevant tool selections were retained. No old +product models or product changes were imported. + +TLC is the official `v1.7.4/tla2tools.jar`, pinned to +`936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88`. +The observed banner is `TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)`. +The checker uses one worker, a 512 MiB heap, fixed seed/fingerprint, and a 120-second +limit per subprocess. Deadlock checking stays enabled; explicit terminal stuttering +is intentional. This TLC version generates trace specifications only when requested; +the checker does not request them. Temporary models, Java instrumentation, and state +directories are removed after each run. The jar cache and generated traces are ignored. + +TLC 1.7.4 does not name temporal violations. The disposable Java launcher checks that +the config enables exactly one property, then records its name only when TLC emits +its actual temporal-violation event. The jar is unmodified. Exit 12 plus the exact +invariant diagnostic or exit 13 plus the exact temporal diagnostic is required; +parse errors, timeouts, unrelated violations, and unexpected passes fail the check. + +The command runs actual-code baselines, separately labeled hypothetical references, +every checked-in mutation config, deterministic implementation replays and isolated +source mutations, then restored baselines. The replay harness also rejects unrelated +failures. Passing reference controls are not shipped repairs or product evidence. + +**P1–P4 deliberately reproduce current guarantee gaps.** A zero wrapper exit means +all expected evidence matched, including those violations. P5 checks the existing +invocation-local cancellation promise and passes. See [coverage](../fv/COVERAGE.md) +for individual findings, limits, fairness assumptions, and source sync revisions. +The model's serialized store schedules do not establish store linearizability. diff --git a/specs/tla/SupervisorJob.tla b/specs/tla/SupervisorJob.tla new file mode 100644 index 00000000..51ccf012 --- /dev/null +++ b/specs/tla/SupervisorJob.tla @@ -0,0 +1,196 @@ +--------------------------- MODULE SupervisorJob --------------------------- +EXTENDS Naturals, FiniteSets + +\* Reviewed statechart committed before this file: 7903351ccfb18664ad894ae98ca6371779424935. +\* Actual = TRUE follows the current implementation on serialized store schedules. +\* Actual = FALSE enables ONLY the named check's hypothetical reference protection. +\* Mutation removes that protection (or the existing P5 terminal memoization). +CONSTANTS Count, Check, Actual, Mutation, AllowFailure +Actors == 1..Count + +VARIABLES step, live, exited, drained, claim, write, events, meta, ack, + admitted, executions, faultUsed +vars == <> + +Reference == ~Actual +ExclusiveAdmission == Reference /\ Check = "P1" /\ ~Mutation +DeduplicateAdmission == Reference /\ + (Check = "P2" \/ (Check = "P3" /\ ~Mutation)) +WaitForExit == Reference /\ Check = "P2" /\ ~Mutation +RecoverPersistence == Reference /\ Check = "P4" /\ ~Mutation +MemoizeOutcome == ~(Check = "P5" /\ Mutation) +\* Environment scheduling restriction, not a product lock: no other store call +\* overlaps the terminal event append and its captured-metadata rewrite. +StoreFree == \A r \in Actors : write[r] # "eventMeta" + +Init == + /\ step = [r \in Actors |-> "idle"] + /\ live = {} + /\ exited = {} + /\ drained = {} + /\ claim = [r \in Actors |-> "none"] + /\ write = [r \in Actors |-> "none"] + /\ events = [r \in Actors |-> 0] + /\ meta = "queued" + /\ ack = {} + /\ admitted = {} + /\ executions = 0 + /\ faultUsed = FALSE + +\* T2/T13: metadata existence/command validation; no actual ownership/status guard. +\* P3 restricts the caller schedule to a sequential retry of the same stored ID. +Begin(r) == + /\ StoreFree + /\ step[r] = "idle" + /\ Check # "P3" \/ r = 1 \/ step[1] = "done" + /\ ~ExclusiveAdmission \/ \A a \in Actors : step[a] \in {"idle", "done"} + /\ ~DeduplicateAdmission \/ admitted = {} + /\ step' = [step EXCEPT ![r] = "starting"] + /\ admitted' = admitted \cup {r} + /\ UNCHANGED <> + +\* T3/T5: complete successful store operations, serialized with other store calls. +\* This restriction is a real schedule, NOT a claim of store linearizability. +Starting(r) == + /\ StoreFree + /\ step[r] = "starting" + /\ meta' = "starting" + /\ step' = [step EXCEPT ![r] = "startingEvent"] + /\ UNCHANGED <> +StartingEvent(r) == + /\ StoreFree + /\ step[r] = "startingEvent" + /\ step' = [step EXCEPT ![r] = "spawn"] + /\ UNCHANGED <> +Spawn(r) == + /\ step[r] = "spawn" + /\ step' = [step EXCEPT ![r] = "running"] + /\ live' = live \cup {r} + /\ executions' = executions + 1 + /\ UNCHANGED <> +Running(r) == + /\ StoreFree + /\ step[r] = "running" + /\ meta' = "running" + /\ step' = [step EXCEPT ![r] = "startedEvent"] + /\ UNCHANGED <> +Register(r) == + /\ StoreFree + /\ step[r] = "startedEvent" + /\ step' = [step EXCEPT ![r] = "ready"] + /\ UNCHANGED <> + +\* T6: signal does not imply exit. Synchronous claim precedes persistence awaits. +Cancel(r) == + /\ step[r] = "ready" + /\ claim[r] = "none" + /\ claim' = [claim EXCEPT ![r] = "cancelled"] + /\ write' = [write EXCEPT ![r] = "status"] + /\ UNCHANGED <> +\* T7 environment: exit is independent of signal, followed by stream EOF/drain. +Exit(r) == + /\ r \in live + /\ live' = live \ {r} + /\ exited' = exited \cup {r} + /\ UNCHANGED <> +Drain(r) == + /\ r \in exited \ drained + /\ drained' = drained \cup {r} + /\ UNCHANGED <> +\* T7 finish: failed/completed are equivalent for these checks; use completed. +Finish(r) == + /\ step[r] = "ready" + /\ r \in drained + /\ claim[r] = "none" \/ + (~MemoizeOutcome /\ claim[r] = "cancelled" /\ write[r] = "done") + /\ claim' = [claim EXCEPT ![r] = "completed"] + /\ write' = [write EXCEPT ![r] = "status"] + /\ UNCHANGED <> + +\* T8/T9: status write, event append, and event-sequence metadata write are distinct. +PersistStatus(r) == + /\ StoreFree + /\ write[r] = "status" + /\ meta' = claim[r] + /\ write' = [write EXCEPT ![r] = "event"] + /\ UNCHANGED <> +AppendEvent(r) == + /\ StoreFree + /\ write[r] = "event" + /\ events' = [events EXCEPT ![r] = @ + 1] + /\ write' = [write EXCEPT ![r] = "eventMeta"] + /\ UNCHANGED <> +PersistEventMeta(r) == + /\ write[r] = "eventMeta" + /\ write' = [write EXCEPT ![r] = "done"] + /\ UNCHANGED <> +\* T10: ack is history, never reset by another invocation or terminal transition. +Acknowledge(r) == + /\ claim[r] = "cancelled" + /\ write[r] = "done" + /\ r \notin ack + /\ ~WaitForExit \/ r \in exited + /\ ack' = ack \cup {r} + /\ UNCHANGED <> +\* T11/T12: run cannot settle before exit and drain, even when persistence rejected. +Return(r) == + /\ step[r] = "ready" + /\ r \in drained + /\ write[r] = "done" \/ (write[r] = "rejected" /\ ~RecoverPersistence) + /\ step' = [step EXCEPT ![r] = "done"] + /\ UNCHANGED <> +\* One finite terminal status failure. Later store operations can succeed. +RejectStatus(r) == + /\ StoreFree + /\ AllowFailure /\ ~faultUsed + /\ write[r] = "status" + /\ faultUsed' = TRUE + /\ write' = [write EXCEPT ![r] = "rejected"] + /\ UNCHANGED <> +\* Hypothetical reference only; the product has no recovery transition. +Recover(r) == + /\ RecoverPersistence + /\ write[r] = "rejected" + /\ write' = [write EXCEPT ![r] = "status"] + /\ UNCHANGED <> + +Advance(r) == Begin(r) \/ Starting(r) \/ StartingEvent(r) \/ Spawn(r) \/ + Running(r) \/ Register(r) \/ Finish(r) \/ Return(r) +Idle == UNCHANGED vars +Next == (\E r \in Actors : Advance(r) \/ Cancel(r) \/ Exit(r) \/ Drain(r) \/ + PersistStatus(r) \/ AppendEvent(r) \/ PersistEventMeta(r) \/ + Acknowledge(r) \/ RejectStatus(r) \/ Recover(r)) \/ Idle + +\* Weak fairness: runnable continuations and store operations complete; processes +\* eventually exit and streams drain. No fairness requires cancellation or failure. +\* RejectStatus can disable persistence once; fairness cannot invent actual recovery. +Fairness == \A r \in Actors : + WF_vars(Advance(r)) /\ WF_vars(Exit(r)) /\ WF_vars(Drain(r)) /\ + WF_vars(PersistStatus(r)) /\ WF_vars(AppendEvent(r)) /\ + WF_vars(PersistEventMeta(r)) /\ WF_vars(Acknowledge(r)) /\ WF_vars(Recover(r)) +Spec == Init /\ [][Next]_vars /\ Fairness + +SingleRunner == Cardinality(live) <= 1 +CancelQuiescent == ack # {} => live = {} +RetryIdempotent == executions <= 1 +ClaimedTerminal == \A r \in Actors : (claim[r] # "none") ~> (write[r] = "done") +CancelWins == \A r \in ack : claim[r] = "cancelled" /\ meta = "cancelled" /\ events[r] = 1 +============================================================================= diff --git a/specs/tla/mutations/P1.cfg b/specs/tla/mutations/P1.cfg new file mode 100644 index 00000000..b707d6f6 --- /dev/null +++ b/specs/tla/mutations/P1.cfg @@ -0,0 +1,9 @@ +\* mutation; P1 / SingleRunner. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P1" + Actual = FALSE + Mutation = TRUE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT SingleRunner diff --git a/specs/tla/mutations/P2.cfg b/specs/tla/mutations/P2.cfg new file mode 100644 index 00000000..63861554 --- /dev/null +++ b/specs/tla/mutations/P2.cfg @@ -0,0 +1,9 @@ +\* mutation; P2 / CancelQuiescent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P2" + Actual = FALSE + Mutation = TRUE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT CancelQuiescent diff --git a/specs/tla/mutations/P3.cfg b/specs/tla/mutations/P3.cfg new file mode 100644 index 00000000..f81ee39a --- /dev/null +++ b/specs/tla/mutations/P3.cfg @@ -0,0 +1,9 @@ +\* mutation; P3 / RetryIdempotent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P3" + Actual = FALSE + Mutation = TRUE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT RetryIdempotent diff --git a/specs/tla/mutations/P4.cfg b/specs/tla/mutations/P4.cfg new file mode 100644 index 00000000..b7b888a3 --- /dev/null +++ b/specs/tla/mutations/P4.cfg @@ -0,0 +1,9 @@ +\* mutation; P4 / ClaimedTerminal. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P4" + Actual = FALSE + Mutation = TRUE + AllowFailure = TRUE +SPECIFICATION Spec +PROPERTY ClaimedTerminal diff --git a/specs/tla/mutations/P5.cfg b/specs/tla/mutations/P5.cfg new file mode 100644 index 00000000..cab53581 --- /dev/null +++ b/specs/tla/mutations/P5.cfg @@ -0,0 +1,9 @@ +\* mutation; P5 / CancelWins. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P5" + Actual = FALSE + Mutation = TRUE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT CancelWins diff --git a/specs/tla/reference/P1.cfg b/specs/tla/reference/P1.cfg new file mode 100644 index 00000000..b19c2023 --- /dev/null +++ b/specs/tla/reference/P1.cfg @@ -0,0 +1,9 @@ +\* reference; P1 / SingleRunner. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P1" + Actual = FALSE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT SingleRunner diff --git a/specs/tla/reference/P2.cfg b/specs/tla/reference/P2.cfg new file mode 100644 index 00000000..58181870 --- /dev/null +++ b/specs/tla/reference/P2.cfg @@ -0,0 +1,9 @@ +\* reference; P2 / CancelQuiescent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P2" + Actual = FALSE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT CancelQuiescent diff --git a/specs/tla/reference/P3.cfg b/specs/tla/reference/P3.cfg new file mode 100644 index 00000000..48ca72f6 --- /dev/null +++ b/specs/tla/reference/P3.cfg @@ -0,0 +1,9 @@ +\* reference; P3 / RetryIdempotent. Reference protections are hypothetical. +CONSTANTS + Count = 2 + Check = "P3" + Actual = FALSE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +INVARIANT RetryIdempotent diff --git a/specs/tla/reference/P4.cfg b/specs/tla/reference/P4.cfg new file mode 100644 index 00000000..173878f3 --- /dev/null +++ b/specs/tla/reference/P4.cfg @@ -0,0 +1,9 @@ +\* reference; P4 / ClaimedTerminal. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P4" + Actual = FALSE + Mutation = FALSE + AllowFailure = TRUE +SPECIFICATION Spec +PROPERTY ClaimedTerminal diff --git a/specs/tla/reference/P4SuccessfulIO.cfg b/specs/tla/reference/P4SuccessfulIO.cfg new file mode 100644 index 00000000..617787e6 --- /dev/null +++ b/specs/tla/reference/P4SuccessfulIO.cfg @@ -0,0 +1,9 @@ +\* actual with successful I/O; P4 / ClaimedTerminal. Reference protections are hypothetical. +CONSTANTS + Count = 1 + Check = "P4" + Actual = TRUE + Mutation = FALSE + AllowFailure = FALSE +SPECIFICATION Spec +PROPERTY ClaimedTerminal diff --git a/tests/supervisor-formal-replay.test.ts b/tests/supervisor-formal-replay.test.ts new file mode 100644 index 00000000..41309d27 --- /dev/null +++ b/tests/supervisor-formal-replay.test.ts @@ -0,0 +1,382 @@ +import { expect, spyOn, test } from "bun:test"; +import { mkdtemp, rm } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import { + type Replay, + replayManifest, + replayMarker, + runStrictReplay, +} from "../scripts/check-supervisor-replays.ts"; +import { + createJobStore, + type JobStore, +} from "../src/control-plane/extensions/supervisor/job-store.ts"; +import { + type JobRunResult, + type JobSpawnListener, + runJob, +} from "../src/control-plane/extensions/supervisor/runner.ts"; +import { createSupervisorService } from "../src/control-plane/extensions/supervisor/service.ts"; +import { logger } from "../src/ui/logger.ts"; + +/** Only this error can become named property evidence; setup/IO errors cannot. */ +class PropertyViolation extends Error { + readonly property: string; + + constructor(property: string) { + super(`Requested property violated: ${property}`); + this.name = "PropertyViolation"; + this.property = property; + } +} + +function assertProperty(property: string, holds: boolean): void { + if (!holds) { + throw new PropertyViolation(property); + } +} + +/** Signal delivery and exit are distinct. No timer controls a replay schedule. */ +function controlledChild(pid: number) { + const exit = Promise.withResolvers(); + const awaitingExit = Promise.withResolvers(); + const secondExitRead = Promise.withResolvers(); + let exitReads = 0; + const child = { + alive: true, + signals: 0, + awaitingExit: awaitingExit.promise, + secondExitRead: secondExitRead.promise, + exit: () => { + child.alive = false; + exit.resolve(0); + }, + proc: { + pid, + stdout: new ReadableStream({ + start: (stream) => stream.close(), + }), + stderr: new ReadableStream({ + start: (stream) => stream.close(), + }), + get exited() { + exitReads += 1; + awaitingExit.resolve(); + if (exitReads === 2) { + secondExitRead.resolve(); + } + return exit.promise; + }, + kill: () => { + child.signals += 1; + }, + }, + }; + return child; +} + +type Child = ReturnType; +type Control = Parameters[0]; +type Fixture = { + readonly store: JobStore; + readonly projectDir: string; + readonly children: Child[]; + readonly spawned: Promise; + readonly runs: Promise[]; +}; + +async function withFixture( + replay: (fixture: Fixture) => Promise +): Promise { + const dir = await mkdtemp( + join( + process.env.HACK_SUPERVISOR_REPLAY_DATA ?? tmpdir(), + "hack-supervisor-replay-" + ) + ); + const projectDir = join(dir, ".hack"); + const children: Child[] = []; + const runs: Promise[] = []; + const spawned = Promise.withResolvers(); + const spawn = spyOn(Bun, "spawn").mockImplementation((() => { + const child = controlledChild(10_000 + children.length); + children.push(child); + spawned.resolve(child); + return child.proc; + }) as unknown as typeof Bun.spawn); + try { + await replay({ + store: await createJobStore({ projectDir }), + projectDir, + children, + spawned: spawned.promise, + runs, + }); + } finally { + for (const child of children) { + child.exit(); + } + await Promise.allSettled(runs); + spawn.mockRestore(); + await rm(dir, { recursive: true, force: true }); + } +} + +async function seed(store: JobStore): Promise { + await store.createJob({ + jobId: "replay", + runner: "generic", + command: ["controlled-child"], + }); +} + +function start(fixture: Fixture) { + const ready = Promise.withResolvers(); + const run = runJob({ + jobStore: fixture.store, + jobId: "replay", + onSpawn: ready.resolve, + }); + fixture.runs.push(run); + // Observe rejection immediately, including while the schedule awaits onSpawn. + void run.catch(() => {}); + return { run, ready: ready.promise }; +} + +async function requireSpawn( + started: ReturnType +): Promise { + return await Promise.race([ + started.ready, + started.run.then(() => { + throw new Error("Expected a process to start"); + }), + ]); +} + +function childAt(fixture: Fixture, index: number): Child { + const child = fixture.children[index]; + if (!child) { + throw new Error("Missing controlled child"); + } + return child; +} + +async function singleRunner(fixture: Fixture): Promise { + await seed(fixture.store); + const first = start(fixture); + await requireSpawn(first); + const second = start(fixture); + await Promise.race([second.ready, second.run]); + const liveChildren = fixture.children.filter((child) => child.alive).length; + expect(liveChildren).toBeGreaterThanOrEqual(1); + // Finish separately: this replay does not assume concurrent store writes are atomic. + childAt(fixture, 0).exit(); + await first.run; + fixture.children[1]?.exit(); + await second.run; + assertProperty("SingleRunner", liveChildren <= 1); +} + +async function cancelQuiescent(fixture: Fixture): Promise { + await seed(fixture.store); + const first = start(fixture); + const control = await requireSpawn(first); + const child = childAt(fixture, 0); + const cancellation = control + .cancel() + .then((accepted) => ({ accepted, alive: child.alive })); + fixture.runs.push(cancellation); + // The reference reads exited a second time inside cancel. Release only after + // that wait is reached, or after actual code has acknowledged a still-live child. + await Promise.race([cancellation, child.secondExitRead]); + child.exit(); + const acknowledgement = await cancellation; + expect(acknowledgement.accepted).toBe(true); + expect(child.signals).toBe(1); + expect((await first.run).status).toBe("cancelled"); + const retry = start(fixture); + await Promise.race([retry.ready, retry.run]); + const restarted = fixture.children.length > 1; + fixture.children[1]?.exit(); + await retry.run; + assertProperty("CancelQuiescent", !(acknowledgement.alive || restarted)); +} + +async function retryIdempotent(fixture: Fixture): Promise { + await seed(fixture.store); + const first = start(fixture); + await requireSpawn(first); + childAt(fixture, 0).exit(); + expect((await first.run).status).toBe("completed"); + expect((await fixture.store.readJobMeta({ jobId: "replay" }))?.status).toBe( + "completed" + ); + const retry = start(fixture); + await Promise.race([retry.ready, retry.run]); + fixture.children[1]?.exit(); + await retry.run; + assertProperty("RetryIdempotent", fixture.children.length === 1); +} + +async function claimedTerminal(fixture: Fixture): Promise { + const fault = new Error("Injected single terminal status write rejection"); + let failures = 0; + const errors: string[] = []; + const service = createSupervisorService({ + logger: { ...logger, error: ({ message }) => errors.push(message) }, + createStore: async () => ({ + ...fixture.store, + updateJobStatus: async (input) => { + if (input.status === "cancelled" && failures === 0) { + failures += 1; + throw fault; + } + return await fixture.store.updateJobStatus(input); + }, + }), + }); + const created = await service.createJob({ + projectDir: fixture.projectDir, + runner: "generic", + command: ["controlled-child"], + }); + fixture.runs.push(created.run); + let runSettled = false; + const outcome = created.run.then( + (result) => { + runSettled = true; + return { result, error: undefined }; + }, + (error: unknown) => { + runSettled = true; + return { result: undefined, error }; + } + ); + const child = await Promise.race([ + fixture.spawned, + outcome.then(() => { + throw new Error("Service settled before spawn"); + }), + ]); + // The runner reads exited after onSpawn has registered the service handle. + await child.awaitingExit; + const input = { projectDir: fixture.projectDir, jobId: created.jobId }; + let cancellationError: unknown; + let cancellationAccepted = false; + try { + cancellationAccepted = (await service.cancelJob(input)).ok; + } catch (error: unknown) { + expect(error).toBe(fault); + cancellationError = error; + } + expect(child.alive).toBe(true); + expect(child.signals).toBe(1); + expect(runSettled).toBe(false); + child.exit(); + const settled = await outcome; + expect(failures).toBe(1); + if (settled.error !== undefined) { + expect(cancellationError).toBe(fault); + expect(settled.error).toBe(fault); + expect(errors).toHaveLength(1); + } else { + expect(cancellationAccepted).toBe(true); + expect(settled.result?.status).toBe("cancelled"); + expect(errors).toHaveLength(0); + } + const stored = await service.getJob(input); + if (!stored) { + throw new Error("Missing service metadata"); + } + // Prove the filesystem is writable after the finite fault without repairing it. + await fixture.store.updateJobStatus({ + jobId: created.jobId, + status: stored.status, + }); + expect(await service.cancelJob(input)).toEqual({ + ok: false, + status: "not_running", + }); + const events = await fixture.store.readEvents(input); + const terminal = events.filter((event) => terminalEventTypes.has(event.type)); + if (settled.error !== undefined) { + expect(stored.status).toBe("running"); + expect(terminal).toHaveLength(0); + } + assertProperty( + "ClaimedTerminal", + stored.status === "cancelled" && + terminal.length === 1 && + terminal[0]?.type === "job.cancelled" + ); +} + +const terminalEventTypes = new Set([ + "job.cancelled", + "job.completed", + "job.failed", +]); + +async function cancelWins(fixture: Fixture): Promise { + await seed(fixture.store); + const first = start(fixture); + const control = await requireSpawn(first); + expect(await control.cancel()).toBe(true); + expect(await control.cancel()).toBe(true); + childAt(fixture, 0).exit(); + const result: JobRunResult = await first.run; + const repeated = await control.cancel(); + const stored = await fixture.store.readJobMeta({ jobId: "replay" }); + const terminal = (await fixture.store.readEvents({ jobId: "replay" })).filter( + (event) => terminalEventTypes.has(event.type) + ); + assertProperty( + "CancelWins", + result.status === "cancelled" && + stored?.status === "cancelled" && + repeated && + childAt(fixture, 0).signals === 1 && + terminal.length === 1 && + terminal[0]?.type === "job.cancelled" + ); +} + +const schedules = { + P1: singleRunner, + P2: cancelQuiescent, + P3: retryIdempotent, + P4: claimedTerminal, + P5: cancelWins, +} satisfies Record Promise>; + +const strictId = process.env.HACK_SUPERVISOR_STRICT_REPLAY; +if (strictId === undefined) { + for (const replay of replayManifest) { + test(`${replay.id} ${replay.property}: documented actual ${replay.actual}`, async () => { + await runStrictReplay({ replay, expected: replay.actual }); + }, 20_000); + } +} else { + const replay = replayManifest.find((entry) => entry.id === strictId); + if (!replay) { + throw new Error("Unknown strict supervisor replay"); + } + test(`${replay.id} requested property ${replay.property}`, async () => { + try { + await withFixture(schedules[replay.id]); + } catch (error: unknown) { + if ( + error instanceof PropertyViolation && + error.property === replay.property + ) { + process.stdout.write( + `${replayMarker({ replay, outcome: "VIOLATION" })}\n` + ); + } + throw error; + } + process.stdout.write(`${replayMarker({ replay, outcome: "PASS" })}\n`); + }); +} diff --git a/tests/supervisor-startup-replay.test.ts b/tests/supervisor-startup-replay.test.ts new file mode 100644 index 00000000..5dbf7df5 --- /dev/null +++ b/tests/supervisor-startup-replay.test.ts @@ -0,0 +1,111 @@ +import { expect, spyOn, test } from "bun:test"; +import { mkdtemp, rm } from "node:fs/promises"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import { createJobStore } from "../src/control-plane/extensions/supervisor/job-store.ts"; +import { createSupervisorService } from "../src/control-plane/extensions/supervisor/service.ts"; +import { logger } from "../src/ui/logger.ts"; + +/** Additional bug characterization, outside the five formal properties. */ +for (const failurePoint of ["running-status", "job.started"] as const) { + test(`startup persistence bug: ${failurePoint} failure leaves a live, uncancellable child`, async () => { + const dir = await mkdtemp( + join( + process.env.HACK_SUPERVISOR_REPLAY_DATA ?? tmpdir(), + "hack-supervisor-startup-" + ) + ); + const projectDir = join(dir, ".hack"); + const exited = Promise.withResolvers(); + let alive = false; + let signals = 0; + let failures = 0; + let run: Promise | undefined; + const proc = { + pid: 10_001, + stdout: null, + stderr: null, + exited: exited.promise, + kill: () => { + signals += 1; + alive = false; + exited.resolve(143); + }, + }; + const spawn = spyOn(Bun, "spawn").mockImplementation((() => { + alive = true; + return proc; + }) as unknown as typeof Bun.spawn); + try { + const store = await createJobStore({ projectDir }); + const fault = new Error( + `Injected startup ${failurePoint} write rejection` + ); + const errors: string[] = []; + const service = createSupervisorService({ + logger: { ...logger, error: ({ message }) => errors.push(message) }, + createStore: async () => ({ + ...store, + updateJobStatus: async (input) => { + if ( + failurePoint === "running-status" && + input.status === "running" && + failures === 0 + ) { + failures += 1; + throw fault; + } + return await store.updateJobStatus(input); + }, + appendEvent: async (input) => { + if ( + failurePoint === "job.started" && + input.type === "job.started" && + failures === 0 + ) { + failures += 1; + throw fault; + } + return await store.appendEvent(input); + }, + }), + }); + const created = await service.createJob({ + projectDir, + runner: "generic", + command: ["controlled-child"], + }); + run = created.run; + expect(await created.run).toEqual({ + jobId: created.jobId, + status: "failed", + exitCode: 1, + }); + expect(spawn).toHaveBeenCalledTimes(1); + expect(failures).toBe(1); + expect(errors).toEqual([`Job failed: ${fault.message}`]); + const input = { projectDir, jobId: created.jobId }; + expect((await service.getJob(input))?.status).toBe("failed"); + const events = await store.readEvents(input); + expect(events.map((event) => event.type)).toEqual([ + "job.created", + "job.starting", + "job.failed", + ]); + expect(events.at(-1)?.payload?.error).toBe(fault.message); + expect(alive).toBe(true); + expect(await service.cancelJob(input)).toEqual({ + ok: false, + status: "not_running", + }); + expect(alive).toBe(true); + expect(signals).toBe(0); + } finally { + alive = false; + exited.resolve(0); + await run?.catch(() => {}); + spawn.mockRestore(); + await rm(dir, { recursive: true, force: true }); + } + }); +} diff --git a/tests/tla-result.test.ts b/tests/tla-result.test.ts new file mode 100644 index 00000000..39c95382 --- /dev/null +++ b/tests/tla-result.test.ts @@ -0,0 +1,353 @@ +import { describe, expect, test } from "bun:test"; +import { existsSync } from "node:fs"; +import { resolve } from "node:path"; +import { + runTlaSequence, + validateTlaChecks, +} from "../scripts/check-tla-models.ts"; +import type { TlaCheck } from "../scripts/lib/tla-checks.ts"; +import { + type TlaExpectation, + verifyTlaResult, +} from "../scripts/lib/tla-result.ts"; +import { + resolveTlaJar, + runTlaProcess, + verifyTlaChecksum, + withTlaScratch, +} from "../scripts/lib/tla-toolchain.ts"; + +function message(code: number, severity: number, body: string): string { + return `@!@!@STARTMSG ${code}:${severity} @!@!@\n${body}\n@!@!@ENDMSG ${code} @!@!@\n`; +} + +const finished = message(2186, 0, "Finished in 00s"); +const completed = + message(2193, 0, "Model checking completed. No error has been found.") + + message( + 2199, + 0, + "7 states generated, 5 distinct states found, 0 states left on queue." + ) + + finished; +const invariant = + message(2110, 1, "Invariant Guarded is violated.") + + message(2121, 1, "The behavior up to this point is:") + + finished; +const temporal = + "Temporal property Progress was violated.\n" + + message(2116, 1, "Temporal properties were violated.") + + message(2264, 1, "The following behavior constitutes a counter-example:") + + finished; + +describe("strict TLC results", () => { + test("accepts a complete nonempty baseline with exit zero", () => { + expect( + verifyTlaResult({ + exitCode: 0, + output: completed, + expected: { kind: "pass" }, + }) + ).toBe(true); + expect( + verifyTlaResult({ + exitCode: 0, + output: completed.replaceAll("5 distinct", "0 distinct"), + expected: { kind: "pass" }, + }) + ).toBe(false); + }); + + test("requires completion, an empty queue, and a successful exit", () => { + for (const output of [ + "", + completed.replace(finished, ""), + completed.replace("0 states left", "1 states left"), + ]) { + expect( + verifyTlaResult({ exitCode: 0, output, expected: { kind: "pass" } }) + ).toBe(false); + } + expect( + verifyTlaResult({ + exitCode: 12, + output: completed, + expected: { kind: "pass" }, + }) + ).toBe(false); + }); + + test("accepts only exit 12 and the exact named invariant", () => { + const expected: TlaExpectation = { kind: "invariant", property: "Guarded" }; + expect(verifyTlaResult({ exitCode: 12, output: invariant, expected })).toBe( + true + ); + for (const exitCode of [0, 1, 11, 13, 124, null]) { + expect(verifyTlaResult({ exitCode, output: invariant, expected })).toBe( + false + ); + } + expect( + verifyTlaResult({ + exitCode: 12, + output: invariant.replace("Guarded", "GuardedExtra"), + expected, + }) + ).toBe(false); + }); + + test("accepts only exit 13 and an instrumented exact temporal violation", () => { + const expected: TlaExpectation = { kind: "temporal", property: "Progress" }; + expect(verifyTlaResult({ exitCode: 13, output: temporal, expected })).toBe( + true + ); + for (const output of [ + temporal.replace("Temporal property Progress was violated.\n", ""), + temporal.replace("Progress", "OtherProgress"), + `Temporal property Progress was violated.\n${finished}`, + `${temporal}Temporal property Other was violated.\n`, + ]) { + expect(verifyTlaResult({ exitCode: 13, output, expected })).toBe(false); + } + expect(verifyTlaResult({ exitCode: 12, output: temporal, expected })).toBe( + false + ); + }); + + test("rejects extra violations, parse failures, tool bugs, and interrupted processes", () => { + const expected: TlaExpectation = { kind: "invariant", property: "Guarded" }; + for (const extra of [ + message(2110, 1, "Invariant Other is violated."), + message(3000, 1, "Parse failure"), + message(3001, 2, "Internal TLC bug"), + "*** Errors: 1\n", + "Exception in thread main\n", + "Parsing or semantic analysis failed.\n", + "@!@!@STARTMSG 3000:1 @!@!@\nUnterminated error\n", + ]) { + expect( + verifyTlaResult({ exitCode: 12, output: invariant + extra, expected }) + ).toBe(false); + } + expect( + verifyTlaResult({ + exitCode: 12, + output: invariant, + failed: true, + expected, + }) + ).toBe(false); + expect( + verifyTlaResult({ + exitCode: 0, + output: completed + message(3000, 1, "Parse failure"), + expected: { kind: "pass" }, + }) + ).toBe(false); + }); + + test("rejects unexpected passes and diagnostic text embedded in a state", () => { + expect( + verifyTlaResult({ + exitCode: 0, + output: completed, + expected: { kind: "invariant", property: "Guarded" }, + }) + ).toBe(false); + expect( + verifyTlaResult({ + exitCode: 12, + output: + message(2217, 4, 'message = "Invariant Guarded is violated."') + + finished, + expected: { kind: "invariant", property: "Guarded" }, + }) + ).toBe(false); + }); + + test("accepts CRLF output", () => { + expect( + verifyTlaResult({ + exitCode: 12, + output: invariant.replaceAll("\n", "\r\n"), + expected: { kind: "invariant", property: "Guarded" }, + }) + ).toBe(true); + }); +}); + +const passingCheck: TlaCheck = { + id: "guarded", + module: "specs/tla/Example.tla", + baseline: { config: "specs/tla/Guarded.cfg", expected: { kind: "pass" } }, + mutation: { + config: "specs/tla/mutations/Guarded.cfg", + expected: { kind: "invariant", property: "Guarded" }, + }, +}; + +describe("TLC orchestration", () => { + test("rejects empty manifests, duplicate ids, and unsafe or missing mutation paths", () => { + expect(() => validateTlaChecks([])).toThrow("empty"); + expect(() => validateTlaChecks([passingCheck, passingCheck])).toThrow( + "duplicate" + ); + expect(() => + validateTlaChecks([{ ...passingCheck, module: "../Example.tla" }]) + ).toThrow("repository-relative"); + expect(() => + validateTlaChecks([ + { + ...passingCheck, + mutation: { + ...passingCheck.mutation, + config: passingCheck.baseline.config, + }, + }, + ]) + ).toThrow("mutation config"); + }); + + test("known findings require a passing reference for the same property", () => { + const finding = { + ...passingCheck, + baseline: { + ...passingCheck.baseline, + expected: passingCheck.mutation.expected, + }, + }; + expect(() => validateTlaChecks([finding])).toThrow("passing reference"); + expect(() => + validateTlaChecks([ + { + ...finding, + reference: { + config: "specs/tla/Reference.cfg", + expected: { kind: "pass" }, + }, + baseline: { + ...finding.baseline, + expected: { kind: "invariant", property: "Other" }, + }, + }, + ]) + ).toThrow("same property"); + }); + + test("runs actual, reference, extra control, mutation, replays, then restored controls", async () => { + const events: string[] = []; + const check: TlaCheck = { + ...passingCheck, + baseline: { + ...passingCheck.baseline, + expected: passingCheck.mutation.expected, + }, + reference: { + config: "specs/tla/Reference.cfg", + expected: { kind: "pass" }, + }, + controls: [ + { config: "specs/tla/Control.cfg", expected: { kind: "pass" } }, + ], + }; + await runTlaSequence({ + checks: [check], + runCheck: async (run) => { + events.push(`${run.phase}:${run.config}`); + }, + runReplays: async () => { + events.push("replays"); + }, + }); + expect(events).toEqual([ + "baseline:specs/tla/Guarded.cfg", + "baseline control:specs/tla/Reference.cfg", + "baseline control:specs/tla/Control.cfg", + "mutation:specs/tla/mutations/Guarded.cfg", + "replays", + "restored baseline:specs/tla/Guarded.cfg", + "restored baseline control:specs/tla/Reference.cfg", + "restored baseline control:specs/tla/Control.cfg", + ]); + }); + + test("a rejected mutation prevents a successful combined result", async () => { + let replayed = false; + await expect( + runTlaSequence({ + checks: [passingCheck], + runCheck: async (run) => { + if (run.phase === "mutation") { + throw new Error("wrong violation"); + } + }, + runReplays: async () => { + replayed = true; + }, + }) + ).rejects.toThrow("wrong violation"); + expect(replayed).toBe(false); + }); +}); + +describe("TLC toolchain", () => { + test("rejects unknown bytes and preserves a mismatched override", async () => { + expect(() => verifyTlaChecksum(new ArrayBuffer(0))).toThrow( + "checksum mismatch" + ); + await withTlaScratch(async (root) => { + const jar = resolve(root, "bad.jar"); + await Bun.write(jar, "not the pinned jar"); + await expect( + resolveTlaJar({ root, override: jar, download: true }) + ).rejects.toThrow("checksum mismatch"); + expect(await Bun.file(jar).text()).toBe("not the pinned jar"); + await expect(resolveTlaJar({ root, download: false })).rejects.toThrow( + "Missing pinned" + ); + }); + }); + + test("removes scratch directories on both success and rejection", async () => { + let directory = ""; + await withTlaScratch(async (scratch) => { + directory = scratch; + await Bun.write(resolve(scratch, "evidence"), "ok"); + }); + expect(existsSync(directory)).toBe(false); + await expect( + withTlaScratch(async (scratch) => { + directory = scratch; + throw new Error("rejected"); + }) + ).rejects.toThrow("rejected"); + expect(existsSync(directory)).toBe(false); + }); + + test("subprocess failures and timeouts cannot satisfy a TLC expectation", async () => { + const result = await runTlaProcess({ + command: [process.execPath, "-e", "process.exit(12)"], + cwd: import.meta.dir, + }); + expect(result.exitCode).toBe(12); + expect( + verifyTlaResult({ + ...result, + expected: { kind: "invariant", property: "Guarded" }, + }) + ).toBe(false); + const timeout = await runTlaProcess({ + command: [process.execPath, "-e", "setInterval(() => {}, 1000)"], + cwd: import.meta.dir, + timeoutMs: 100, + }); + expect(timeout.failed).toBe(true); + expect( + verifyTlaResult({ + ...timeout, + output: invariant, + expected: { kind: "invariant", property: "Guarded" }, + }) + ).toBe(false); + }); +}); From 9b9a86636c71a9f14d34766a5478ecda538f6846 Mon Sep 17 00:00:00 2001 From: Hack Dance <344842+roodboi@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:00:35 -0400 Subject: [PATCH 4/4] test(supervisor): restrict terminal stuttering to expose deadlocks --- specs/fv/COVERAGE.md | 12 +++++++++++- specs/tla/README.md | 7 ++++++- specs/tla/SupervisorJob.tla | 12 +++++++++++- 3 files changed, 28 insertions(+), 3 deletions(-) diff --git a/specs/fv/COVERAGE.md b/specs/fv/COVERAGE.md index c9a717a2..cc8ca233 100644 --- a/specs/fv/COVERAGE.md +++ b/specs/fv/COVERAGE.md @@ -16,7 +16,11 @@ Flags: `-Xmx512m -XX:ActiveProcessorCount=1 -XX:+UseParallelGC -XX:-UsePerfData`, TLC `-tool -workers 1 -fp 0 -seed 1`, private metadir, 120-second subprocess timeout. Deadlock checking enabled; - `Idle` deliberately permits terminal stutter. No generated trace specs requested. + `Idle` permits stutter only after every invocation returns (including rejected + persistence) and any successful cancellation is acknowledged, or remains unstarted + because reference deduplication blocks admission. Active states cannot use `Idle`. + P4 still checks durable progress after an error return. No generated trace specs + requested. - Outputs: jar in ignored `.cache/tlaplus/`; raw TLC output on stdout, disposable sources/state directories under the system temporary directory and removed. Raw execution logs are not committed. TLC requires a local RMI listener. @@ -100,6 +104,12 @@ and its `PropertyViolation` error. The outer test/harness explicitly expects the known finding. Zero wrapper exit means reproducible evidence, **not product green**. All five model and implementation mutations demonstrated their intended failures. +After restricting `Idle` to settled invocations and reference-blocked admissions, +`bun run check:tla` retained all named violations, passing controls, replays, and +restored baselines. A disposable model with `Starting` disabled under `P5.cfg` +reported `Deadlock reached.` with exit 11, confirming that active-state deadlocks +are detected. The disposable control was removed; product source is unchanged. + ## Findings and limits - **F1 / P1:** starting a second exported `runJob` for one stored ID while the first diff --git a/specs/tla/README.md b/specs/tla/README.md index 6f93d6f3..a2111d0d 100644 --- a/specs/tla/README.md +++ b/specs/tla/README.md @@ -24,7 +24,12 @@ TLC is the official `v1.7.4/tla2tools.jar`, pinned to The observed banner is `TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)`. The checker uses one worker, a 512 MiB heap, fixed seed/fingerprint, and a 120-second limit per subprocess. Deadlock checking stays enabled; explicit terminal stuttering -is intentional. This TLC version generates trace specifications only when requested; +is limited to returned invocations (including rejected persistence), completed +cancellation acknowledgements, and unstarted invocations blocked by reference +deduplication. Active states cannot use `Idle` to hide a deadlock. A returned run +with rejected persistence still violates P4 `ClaimedTerminal`; a terminal return +does not imply durable success. This TLC version generates trace specifications +only when requested; the checker does not request them. Temporary models, Java instrumentation, and state directories are removed after each run. The jar cache and generated traces are ignored. diff --git a/specs/tla/SupervisorJob.tla b/specs/tla/SupervisorJob.tla index 51ccf012..bb22d66a 100644 --- a/specs/tla/SupervisorJob.tla +++ b/specs/tla/SupervisorJob.tla @@ -174,7 +174,17 @@ Recover(r) == Advance(r) == Begin(r) \/ Starting(r) \/ StartingEvent(r) \/ Spawn(r) \/ Running(r) \/ Register(r) \/ Finish(r) \/ Return(r) -Idle == UNCHANGED vars +\* Stutter only after all invocations settle, including rejected persistence. +\* Reference deduplication can leave an invocation permanently unstarted. +\* A rejected terminal write still violates P4; returning is not durable success. +Idle == + /\ \A r \in Actors : + \/ /\ step[r] = "done" + /\ write[r] = "done" \/ (write[r] = "rejected" /\ ~RecoverPersistence) + /\ claim[r] # "cancelled" \/ write[r] = "rejected" \/ r \in ack + \/ /\ step[r] = "idle" + /\ DeduplicateAdmission /\ admitted # {} + /\ UNCHANGED vars Next == (\E r \in Actors : Advance(r) \/ Cancel(r) \/ Exit(r) \/ Drain(r) \/ PersistStatus(r) \/ AppendEvent(r) \/ PersistEventMeta(r) \/ Acknowledge(r) \/ RejectStatus(r) \/ Recover(r)) \/ Idle