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/7] 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 000000000..4a17f5b29 --- /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 000000000..fb9ee5fdb --- /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/7] 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 4a17f5b29..c97fe07b5 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 fb9ee5fdb..d2d3fb3d4 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/7] 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 d6bca134a..36a80560e 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 01ee730c9..aeb9fc006 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 50036763c..8088b70fe 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 000000000..407117591 --- /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 0d0cf22ac..ac5731df4 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 000000000..e8eaccde3 --- /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 000000000..556c07da4 --- /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 000000000..a17e0c1ff --- /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 000000000..b0cc19909 --- /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 000000000..754442b25 --- /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 000000000..c9a717a25 --- /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 000000000..04297658f --- /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 000000000..31992bd65 --- /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 000000000..79f694e04 --- /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 000000000..d54eb7b6f --- /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 000000000..06b20dfe0 --- /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 000000000..6f93d6f3b --- /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 000000000..51ccf012d --- /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 000000000..b707d6f6d --- /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 000000000..63861554e --- /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 000000000..f81ee39a4 --- /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 000000000..b7b888a3e --- /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 000000000..cab535813 --- /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 000000000..b19c20235 --- /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 000000000..581818708 --- /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 000000000..48ca72f6a --- /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 000000000..173878f3a --- /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 000000000..617787e6f --- /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 000000000..41309d270 --- /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 000000000..5dbf7df56 --- /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 000000000..39c953822 --- /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/7] 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 c9a717a25..cc8ca233b 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 6f93d6f3b..a2111d0d2 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 51ccf012d..bb22d66a6 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 From d903b14b5bed8481c3e2c96bb09371bca54cbad2 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Mon, 2 Nov 2026 15:52:23 -0500 Subject: [PATCH 5/7] fix(supervisor): follow the repository Bun pin in formal checks The replay and TLA+ checks hardcoded Bun 1.3.9, the packageManager value when they were written. main moved to Bun 1.4.4 for a security fix, so the checks refused to run and the hosted test job failed. Read the required version from package.json. The checks still refuse any other runtime and still require the exact bun test banner of that version. Set mise.toml to 1.4.4 and add a test that keeps it equal to package.json. Replay results did not depend on the Bun version: P1-P4 still report the same named PropertyViolation and P5 still passes on 1.3.9 and 1.4.4. No expected result changed. Co-Authored-By: Claude Opus 5.5 --- mise.toml | 2 +- scripts/check-supervisor-replays.ts | 25 ++++++++++++------ scripts/check-tla-models.ts | 5 ++-- scripts/lib/pinned-bun.ts | 38 +++++++++++++++++++++++++++ specs/fv/COVERAGE.md | 7 +++++ specs/tla/README.md | 4 +-- tests/tla-result.test.ts | 40 +++++++++++++++++++++++++++++ 7 files changed, 107 insertions(+), 14 deletions(-) create mode 100644 scripts/lib/pinned-bun.ts diff --git a/mise.toml b/mise.toml index 407117591..8186aee45 100644 --- a/mise.toml +++ b/mise.toml @@ -1,3 +1,3 @@ [tools] -bun = "1.3.9" +bun = "1.4.4" java = "temurin-17.0.20+101" diff --git a/scripts/check-supervisor-replays.ts b/scripts/check-supervisor-replays.ts index e8eaccde3..afa1d28d7 100644 --- a/scripts/check-supervisor-replays.ts +++ b/scripts/check-supervisor-replays.ts @@ -1,6 +1,7 @@ import { cp, mkdir, mkdtemp, rm, symlink } from "node:fs/promises"; import { tmpdir } from "node:os"; import { join, resolve } from "node:path"; +import { assertPinnedBun, bunTestBannerPattern } from "./lib/pinned-bun.ts"; /** Expected findings, not a claim that the requested product guarantees pass. */ export const replayManifest = [ @@ -34,19 +35,20 @@ type StrictReplayOptions = { export async function runStrictReplay( opts: StrictReplayOptions ): Promise { - if (Bun.version !== "1.3.9") { - throw new Error("Supervisor replays require Bun 1.3.9"); - } + const bunVersion = await assertPinnedBun(); const dataRoot = await mkdtemp(join(tmpdir(), "hack-supervisor-data-")); try { - await runReplayProcess({ ...opts, dataRoot }); + await runReplayProcess({ ...opts, bunVersion, dataRoot }); } finally { await rm(dataRoot, { recursive: true, force: true }); } } async function runReplayProcess( - opts: StrictReplayOptions & { readonly dataRoot: string } + opts: StrictReplayOptions & { + readonly bunVersion: string; + readonly dataRoot: string; + } ): Promise { const proc = Bun.spawn( [process.execPath, "test", `./${testFile}`, "--timeout", "10000"], @@ -84,7 +86,9 @@ async function runReplayProcess( if ( timedOut || exitCode !== (violation ? 1 : 0) || - !/^bun test v1\.3\.9 \([a-z0-9]+\)$/.test(banner ?? "") || + !new RegExp(`^${bunTestBannerPattern(opts.bunVersion)}$`).test( + banner ?? "" + ) || marker !== expectedMarker || extra.length !== 0 || !summary.test(stderr) || @@ -196,6 +200,7 @@ async function checkActual(label: string): Promise { /** Extra implementation evidence; this is not a sixth formal property. */ async function checkStartupPersistence(): Promise { + const bunVersion = await assertPinnedBun(); const dataRoot = await mkdtemp( join(tmpdir(), "hack-supervisor-startup-data-") ); @@ -229,7 +234,7 @@ async function checkStartupPersistence(): Promise { ]); if ( exitCode !== 0 || - !/^bun test v1\.3\.9 \([a-z0-9]+\)\n$/.test(stdout) || + !new RegExp(`^${bunTestBannerPattern(bunVersion)}\\n$`).test(stdout) || !/\b2 pass\s+0 fail\b/.test(stderr) ) { throw new Error("Startup persistence characterization failed"); @@ -256,12 +261,16 @@ async function main(): Promise { try { await cp(join(repoRoot, "src"), join(scratch, "src"), { recursive: true }); await mkdir(join(scratch, "tests")); - await mkdir(join(scratch, "scripts")); + await mkdir(join(scratch, "scripts/lib"), { recursive: true }); await cp(join(repoRoot, testFile), join(scratch, testFile)); await cp( import.meta.path, join(scratch, "scripts/check-supervisor-replays.ts") ); + await cp( + join(repoRoot, "scripts/lib/pinned-bun.ts"), + join(scratch, "scripts/lib/pinned-bun.ts") + ); await symlink( join(repoRoot, "node_modules"), join(scratch, "node_modules") diff --git a/scripts/check-tla-models.ts b/scripts/check-tla-models.ts index 556c07da4..18bd2d727 100644 --- a/scripts/check-tla-models.ts +++ b/scripts/check-tla-models.ts @@ -3,6 +3,7 @@ // 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 { assertPinnedBun } from "./lib/pinned-bun.ts"; import { CHECKS, type TlaCheck } from "./lib/tla-checks.ts"; import { type TlaExpectation, verifyTlaResult } from "./lib/tla-result.ts"; import { @@ -205,9 +206,7 @@ async function main(): Promise { 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}.`); - } + await assertPinnedBun(); validateTlaChecks(CHECKS); const root = resolve(import.meta.dir, ".."); const jar = await resolveTlaJar({ diff --git a/scripts/lib/pinned-bun.ts b/scripts/lib/pinned-bun.ts new file mode 100644 index 000000000..2284f04f2 --- /dev/null +++ b/scripts/lib/pinned-bun.ts @@ -0,0 +1,38 @@ +import { resolve } from "node:path"; + +const manifestPath = resolve(import.meta.dir, "../../package.json"); + +export function parsePinnedBun(packageManager: unknown): string { + const match = + typeof packageManager === "string" + ? /^bun@(\d+\.\d+\.\d+)$/.exec(packageManager) + : null; + if (!match?.[1]) { + throw new Error( + `package.json must pin packageManager to an exact bun@x.y.z; found ${String(packageManager)}.` + ); + } + return match[1]; +} + +/** + * Formal checks stay single-version: evidence is only accepted from the runtime the + * repository pins. Returns that version. package.json is the one source of truth, so + * a repository Bun upgrade moves these checks with it and they must pass again there. + */ +export async function assertPinnedBun( + running: string = Bun.version +): Promise { + const manifest: { readonly packageManager?: unknown } = + await Bun.file(manifestPath).json(); + const pinned = parsePinnedBun(manifest.packageManager); + if (running !== pinned) { + throw new Error(`Use the pinned Bun ${pinned}; running ${running}.`); + } + return pinned; +} + +/** Unanchored source for the exact `bun test` banner printed by that version. */ +export function bunTestBannerPattern(version: string): string { + return `bun test v${version.replaceAll(".", "\\.")} \\([a-z0-9]+\\)`; +} diff --git a/specs/fv/COVERAGE.md b/specs/fv/COVERAGE.md index cc8ca233b..5a7d301c8 100644 --- a/specs/fv/COVERAGE.md +++ b/specs/fv/COVERAGE.md @@ -110,6 +110,13 @@ 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. +The replay and checker runtime follows the `packageManager` pin in `package.json`. +Moving that pin from Bun 1.3.9 to 1.4.4 changed no result: direct replays on both +versions gave the same exit, marker, named `PropertyViolation` and pass/fail counts, +and `bun run check:tla` on 1.4.4 retained every baseline, control, mutation, replay +and restored baseline above. Replay schedules use controlled children and no timers, +and TLC runs under Java. Any later pin change must pass this command on the new Bun. + ## 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 a2111d0d2..89d580720 100644 --- a/specs/tla/README.md +++ b/specs/tla/README.md @@ -8,8 +8,8 @@ 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; +The repository check command is **`bun run check:tla`**. With the Bun version pinned by +`package.json` 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. diff --git a/tests/tla-result.test.ts b/tests/tla-result.test.ts index 39c953822..e0c5f6803 100644 --- a/tests/tla-result.test.ts +++ b/tests/tla-result.test.ts @@ -5,6 +5,11 @@ import { runTlaSequence, validateTlaChecks, } from "../scripts/check-tla-models.ts"; +import { + assertPinnedBun, + bunTestBannerPattern, + parsePinnedBun, +} from "../scripts/lib/pinned-bun.ts"; import type { TlaCheck } from "../scripts/lib/tla-checks.ts"; import { type TlaExpectation, @@ -351,3 +356,38 @@ describe("TLC toolchain", () => { ).toBe(false); }); }); + +describe("pinned Bun for formal checks", () => { + test("accepts only an exact bun@x.y.z packageManager", () => { + expect(parsePinnedBun("bun@1.4.4")).toBe("1.4.4"); + for (const value of ["bun@latest", "bun@1.4", "npm@1.4.4", undefined]) { + expect(() => parsePinnedBun(value)).toThrow("exact bun@x.y.z"); + } + }); + + test("refuses any runtime other than the package.json pin", async () => { + const { packageManager } = await Bun.file( + resolve(import.meta.dir, "../package.json") + ).json(); + const pinned = parsePinnedBun(packageManager); + expect(await assertPinnedBun(pinned)).toBe(pinned); + await expect(assertPinnedBun(`${pinned}-other`)).rejects.toThrow( + `Use the pinned Bun ${pinned}` + ); + }); + + test("mise selects the same Bun as package.json", async () => { + const mise = await Bun.file( + resolve(import.meta.dir, "../mise.toml") + ).text(); + const selected = /^bun = "([^"]+)"$/m.exec(mise)?.[1]; + expect(selected).toBe(await assertPinnedBun()); + }); + + test("the banner pattern matches only that exact version", () => { + const banner = new RegExp(`^${bunTestBannerPattern("1.4.4")}$`); + expect(banner.test("bun test v1.4.4 (38afee6c8)")).toBe(true); + expect(banner.test("bun test v1.3.9 (cf6cdbbb)")).toBe(false); + expect(banner.test("bun test v1x4x4 (38afee6c8)")).toBe(false); + }); +}); From 21b8c6d61ebbdbb7ec7374c75cdb7785d8a880e0 Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Mon, 2 Nov 2026 16:07:23 -0500 Subject: [PATCH 6/7] test(supervisor): explain changed findings and scope the TLA guidance Keep the actual-code replays in the default suite, because hosted CI runs no other check of them. When a replay gives a complete named result that differs from the manifest, say that the recorded finding or pass no longer holds and what to update. Setup errors and unrelated failures are still rejected as before, and scratch controls keep their rejection message. The startup characterization now reports a fixed bug the same way. Replace contributor references to skills outside this repository with steps that work from the repository. Limit the guidance to the supervisor job lifecycle, which is all the check covers. Rename the statechart and walkthrough to supervisor-specific names and put the walkthrough in the present tense. Co-Authored-By: Claude Opus 5.5 --- docs/{statechart.md => supervisor-job-statechart.md} | 0 docs/{supervisor-usage.md => supervisor-job-walkthrough.md} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename docs/{statechart.md => supervisor-job-statechart.md} (100%) rename docs/{supervisor-usage.md => supervisor-job-walkthrough.md} (100%) diff --git a/docs/statechart.md b/docs/supervisor-job-statechart.md similarity index 100% rename from docs/statechart.md rename to docs/supervisor-job-statechart.md diff --git a/docs/supervisor-usage.md b/docs/supervisor-job-walkthrough.md similarity index 100% rename from docs/supervisor-usage.md rename to docs/supervisor-job-walkthrough.md From 856c1013fe23554d58ab00b5ffc106336c1de68a Mon Sep 17 00:00:00 2001 From: Dimitri Kennedy <344842+roodboi@users.noreply.github.com> Date: Mon, 2 Nov 2026 16:07:37 -0500 Subject: [PATCH 7/7] test(supervisor): report changed findings plainly and scope guidance Contains the content described by 21b8c6d6, which holds only the two doc renames because staging failed before that commit ran. Its message covers this commit too. Unpushed history was not rewritten to fix that. Replays stay in the default suite. A complete named result that differs from the manifest now says the recorded finding or pass no longer holds and what to update. Other failures are still rejected as replay evidence. Guidance no longer names skills outside this repository and now applies only to the supervisor job lifecycle. Co-Authored-By: Claude Opus 5.5 --- .factory/skills/control-plane-worker/SKILL.md | 6 +- AGENTS.md | 8 +- docs/supervisor-job-statechart.md | 2 +- docs/supervisor-job-walkthrough.md | 35 +++--- scripts/check-supervisor-replays.ts | 102 ++++++++++++++---- specs/fv/COVERAGE.md | 21 +++- tests/supervisor-startup-replay.test.ts | 19 ++-- tests/tla-result.test.ts | 79 ++++++++++++++ 8 files changed, 214 insertions(+), 58 deletions(-) diff --git a/.factory/skills/control-plane-worker/SKILL.md b/.factory/skills/control-plane-worker/SKILL.md index 36a80560e..49dde588a 100644 --- a/.factory/skills/control-plane-worker/SKILL.md +++ b/.factory/skills/control-plane-worker/SKILL.md @@ -21,8 +21,10 @@ 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`. + For supervisor job lifecycle changes (`runner.ts`, `job-store.ts`, `service.ts` in + `src/control-plane/extensions/supervisor/`), update and review + `docs/supervisor-job-statechart.md` and `docs/supervisor-job-walkthrough.md`, then + run `bun run check:tla`. It does not cover other control-plane state. 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/AGENTS.md b/AGENTS.md index 8088b70fe..be9572708 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -61,9 +61,11 @@ 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. +For changes to the supervisor job lifecycle (`runner.ts`, `job-store.ts` and +`service.ts` in `src/control-plane/extensions/supervisor/`), update and review +`docs/supervisor-job-statechart.md` and `docs/supervisor-job-walkthrough.md`, then +run `bun run check:tla`. It does not cover other control-plane state. See +`specs/fv/COVERAGE.md` for property scope, known bugs, and source sync revisions. ## Runtime and secrets diff --git a/docs/supervisor-job-statechart.md b/docs/supervisor-job-statechart.md index c97fe07b5..b4c528019 100644 --- a/docs/supervisor-job-statechart.md +++ b/docs/supervisor-job-statechart.md @@ -1,6 +1,6 @@ # Supervisor job statechart and property derivation -- Walkthrough: [supervisor-usage.md](supervisor-usage.md). +- Walkthrough: [supervisor-job-walkthrough.md](supervisor-job-walkthrough.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. diff --git a/docs/supervisor-job-walkthrough.md b/docs/supervisor-job-walkthrough.md index d2d3fb3d4..2a8ba8707 100644 --- a/docs/supervisor-job-walkthrough.md +++ b/docs/supervisor-job-walkthrough.md @@ -1,9 +1,9 @@ -# Supervisor verification walkthrough +# Supervisor job 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. +This walkthrough describes supervisor job behavior at source revision +`08e0412a9fa063c33f4145b569c36afc5810e606`. The supervisor is an unsupported +experimental surface; verification does not change that support status. See +[the statechart](supervisor-job-statechart.md) for transition IDs and property derivations. A caller uses `createSupervisorService().createJob` with a project directory and a command. The service generates a UUID, writes queued metadata and a creation event, @@ -13,11 +13,11 @@ fresh instances. Cancellation handles exist only in the instance that started a 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 +`job.starting`, and spawns. It then 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. +a live child without a registered handle; the model documents that window and adds +no recovery for it. 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. @@ -38,7 +38,7 @@ 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 +metadata update are separate operations. The model preserves 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. @@ -67,13 +67,12 @@ 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. +From the repository root, run `bun run check:tla`. The command verifies the pinned +TLC jar, runs each actual-code property separately, checks passing reference controls +and must-fail mutations, replays the schedules against imported implementation code, +exercises isolated real-code mutations, and reruns the baseline. Tool failures and +unexpected passes 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. +`specs/fv/COVERAGE.md` records the exact outcomes. This walkthrough describes behavior +and does not record TLC results. Product fixes are separate changes. diff --git a/scripts/check-supervisor-replays.ts b/scripts/check-supervisor-replays.ts index afa1d28d7..f3c81a461 100644 --- a/scripts/check-supervisor-replays.ts +++ b/scripts/check-supervisor-replays.ts @@ -76,32 +76,26 @@ async function runReplayProcess( 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({ + const observed = observedReplayOutcome({ replay: opts.replay, - outcome: opts.expected, + bunVersion: opts.bunVersion, + exitCode, + timedOut, + stdout, + stderr, }); - const summary = violation ? /\b0 pass\s+1 fail\b/ : /\b1 pass\s+0 fail\b/; - if ( - timedOut || - exitCode !== (violation ? 1 : 0) || - !new RegExp(`^${bunTestBannerPattern(opts.bunVersion)}$`).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) - ) { + if (observed === opts.expected) { + return; + } + // Scratch runs test temporary controls, so only actual code can contradict a record. + if (observed !== undefined && opts.root === undefined) { throw new Error( - `${opts.replay.id} ${opts.replay.property}: rejected replay evidence (exit=${exitCode}, timeout=${timedOut}); expected ${opts.expected}` + recordedResultChangedMessage({ replay: opts.replay, observed }) ); } + 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) { @@ -111,6 +105,68 @@ async function runReplayProcess( } } +type ReplayOutcome = "PASS" | "VIOLATION"; + +/** + * One complete, named result of a strict replay, or undefined for anything else: + * setup errors, unrelated failures and timeouts are never evidence of an outcome. + */ +export function observedReplayOutcome(opts: { + readonly replay: Replay; + readonly bunVersion: string; + readonly exitCode: number; + readonly timedOut: boolean; + readonly stdout: string; + readonly stderr: string; +}): ReplayOutcome | undefined { + const [banner, marker, ...extra] = opts.stdout.trim().split("\n"); + if ( + opts.timedOut || + extra.length !== 0 || + !new RegExp(`^${bunTestBannerPattern(opts.bunVersion)}$`).test( + banner ?? "" + ) || + /unhandled|error between tests|timed out/i.test(opts.stderr) + ) { + return; + } + const passed = + opts.exitCode === 0 && + marker === replayMarker({ replay: opts.replay, outcome: "PASS" }) && + /\b1 pass\s+0 fail\b/.test(opts.stderr); + if (passed) { + return "PASS"; + } + const violated = + opts.exitCode === 1 && + marker === replayMarker({ replay: opts.replay, outcome: "VIOLATION" }) && + /\b0 pass\s+1 fail\b/.test(opts.stderr) && + opts.stderr.includes( + `PropertyViolation: Requested property violated: ${opts.replay.property}` + ); + return violated ? "VIOLATION" : undefined; +} + +/** What a contributor sees when product behavior no longer matches the manifest. */ +export function recordedResultChangedMessage(opts: { + readonly replay: Replay; + readonly observed: ReplayOutcome; +}): string { + const { id, property } = opts.replay; + const change = + opts.observed === "PASS" + ? `Recorded finding no longer holds: ${id} ${property} now passes against the actual code.` + : `Recorded pass no longer holds: ${id} ${property} is now violated by the actual code.`; + const intent = + opts.observed === "PASS" + ? "If your change fixed this on purpose, record the fix" + : "If this is a regression, fix the code. If the guarantee changed on purpose, record it"; + return [ + change, + `${intent}: set ${id} to actual "${opts.observed}" in replayManifest (scripts/check-supervisor-replays.ts), then update the ${id} TLA+ model, its expectation in scripts/lib/tla-checks.ts and its row in specs/fv/COVERAGE.md, and run bun run check:tla.`, + ].join("\n"); +} + type Replacement = { readonly before: string; readonly after: string }; const admissionAnchor = " const command = opts.command ?? meta.command;"; const terminalAdmissionCondition = @@ -237,7 +293,9 @@ async function checkStartupPersistence(): Promise { !new RegExp(`^${bunTestBannerPattern(bunVersion)}\\n$`).test(stdout) || !/\b2 pass\s+0 fail\b/.test(stderr) ) { - throw new Error("Startup persistence characterization failed"); + throw new Error( + "Startup persistence characterization failed; run bun test ./tests/supervisor-startup-replay.test.ts for the reason" + ); } process.stdout.write( "characterization startup persistence (running status, job.started): BUG REPRODUCED\n" diff --git a/specs/fv/COVERAGE.md b/specs/fv/COVERAGE.md index 5a7d301c8..6f0c55684 100644 --- a/specs/fv/COVERAGE.md +++ b/specs/fv/COVERAGE.md @@ -1,7 +1,8 @@ # Supervisor verification coverage -- Usage: [supervisor-usage.md](../../docs/supervisor-usage.md). -- Reviewed derivation: [statechart.md](../../docs/statechart.md), committed in +- Scope: the supervisor job lifecycle only. No other control-plane state is modeled. +- Usage: [supervisor-job-walkthrough.md](../../docs/supervisor-job-walkthrough.md). +- Reviewed derivation: [supervisor-job-statechart.md](../../docs/supervisor-job-statechart.md), committed in `c0c96649a492cca26f68a77ecc62d9a8a53517a5`; review corrections committed in `7903351ccfb18664ad894ae98ca6371779424935` before the first specification. - One repository rerun command: **`bun run check:tla`**. See @@ -155,7 +156,17 @@ and TLC runs under Java. Any later pin change must pass this command on the new 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. +After changes to the covered source: inspect the covered diff, new callers/writers +and renamed paths, update and review the statechart and walkthrough, run +`bun run check:tla` 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. + +The default test suite runs the actual-code replays, so a change to recorded behavior +fails there. A failure that starts with `Recorded finding no longer holds` or +`Recorded pass no longer holds` means the actual code no longer matches +`replayManifest` in `scripts/check-supervisor-replays.ts`. If the change is intended, +update that manifest, the model and its expectation in `scripts/lib/tla-checks.ts`, +and the affected rows here in the same change. If not, fix the code. A failure that +says `rejected replay evidence` is not a changed finding: the replay did not produce +a complete named result. diff --git a/tests/supervisor-startup-replay.test.ts b/tests/supervisor-startup-replay.test.ts index 5dbf7df56..0c347d98b 100644 --- a/tests/supervisor-startup-replay.test.ts +++ b/tests/supervisor-startup-replay.test.ts @@ -93,13 +93,18 @@ for (const failurePoint of ["running-status", "job.started"] as const) { "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); + const aliveAfterFailure = alive; + const cancellation = await service.cancelJob(input); + if ( + !(aliveAfterFailure && alive) || + signals !== 0 || + cancellation.ok || + cancellation.status !== "not_running" + ) { + throw new Error( + `Recorded finding no longer holds: a ${failurePoint} startup failure no longer leaves a live, uncancellable child. If your change fixed this on purpose, remove this characterization from tests/supervisor-startup-replay.test.ts, update checkStartupPersistence in scripts/check-supervisor-replays.ts and the startup finding in specs/fv/COVERAGE.md, and run bun run check:tla.` + ); + } } finally { alive = false; exited.resolve(0); diff --git a/tests/tla-result.test.ts b/tests/tla-result.test.ts index e0c5f6803..b8314f394 100644 --- a/tests/tla-result.test.ts +++ b/tests/tla-result.test.ts @@ -1,6 +1,14 @@ import { describe, expect, test } from "bun:test"; import { existsSync } from "node:fs"; import { resolve } from "node:path"; +import { + observedReplayOutcome, + type Replay, + recordedResultChangedMessage, + replayManifest, + replayMarker, + runStrictReplay, +} from "../scripts/check-supervisor-replays.ts"; import { runTlaSequence, validateTlaChecks, @@ -391,3 +399,74 @@ describe("pinned Bun for formal checks", () => { expect(banner.test("bun test v1x4x4 (38afee6c8)")).toBe(false); }); }); + +describe("supervisor replay evidence", () => { + const bunVersion = "1.4.4"; + const banner = "bun test v1.4.4 (38afee6c8)"; + const replay = replayManifest[0] as Replay; + const violationStderr = `PropertyViolation: Requested property violated: ${replay.property}\n 0 pass\n 1 fail\n`; + const violation = { + replay, + bunVersion, + exitCode: 1, + timedOut: false, + stdout: `${banner}\n${replayMarker({ replay, outcome: "VIOLATION" })}\n`, + stderr: violationStderr, + }; + const pass = { + ...violation, + exitCode: 0, + stdout: `${banner}\n${replayMarker({ replay, outcome: "PASS" })}\n`, + stderr: " 1 pass\n 0 fail\n", + }; + + test("recognizes only complete named outcomes", () => { + expect(observedReplayOutcome(violation)).toBe("VIOLATION"); + expect(observedReplayOutcome(pass)).toBe("PASS"); + }); + + test("never treats other failures as a changed outcome", () => { + for (const rejected of [ + { ...violation, timedOut: true }, + { ...violation, stderr: " 0 pass\n 1 fail\n" }, + { ...violation, stdout: `${banner}\n` }, + { + ...violation, + stdout: `bun test v1.3.9 (cf6cdbbb)\n${violation.stdout}`, + }, + { ...violation, stdout: `${violation.stdout}extra\n` }, + { ...violation, stderr: `${violationStderr}Unhandled error\n` }, + { ...pass, exitCode: 1 }, + { ...pass, stderr: " 0 pass\n 1 fail\n" }, + ]) { + expect(observedReplayOutcome(rejected)).toBeUndefined(); + } + }); + + test("a fixed finding says so and names the manifest", () => { + const message = recordedResultChangedMessage({ replay, observed: "PASS" }); + expect(message).toContain("Recorded finding no longer holds"); + expect(message).toContain(`${replay.id} ${replay.property}`); + expect(message).toContain(`actual "PASS" in replayManifest`); + expect(message).toContain("bun run check:tla"); + }); + + test("a lost pass is reported as a possible regression", () => { + const message = recordedResultChangedMessage({ + replay, + observed: "VIOLATION", + }); + expect(message).toContain("Recorded pass no longer holds"); + expect(message).toContain("If this is a regression, fix the code"); + }); + + test("actual code and scratch controls report differently", async () => { + const root = resolve(import.meta.dir, ".."); + await expect(runStrictReplay({ replay, expected: "PASS" })).rejects.toThrow( + "Recorded pass no longer holds" + ); + await expect( + runStrictReplay({ replay, expected: "PASS", root }) + ).rejects.toThrow("rejected replay evidence"); + }, 30_000); +});