diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index da89c534f..57aa51434 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -114,11 +114,12 @@ python3 benchmarks/first_frame.py --binary /tmp/fx-before --binary ./zig-out/bin ### Check a TLA+ model -`tests/tla/` holds TLA+ models of the session manager, the workspace indexer, and libfx durable sessions and steering. CI runs the libfx model; run the matching checker yourself when you change behavior that one of the others describes. You need Java and `tla2tools.jar`, and `tests/tla/README.md` covers setup. +`tests/tla/` holds TLA+ models of fx, such as the session manager, the MCP engine and host, ACP, `/usage`, the shell tool, the workspace indexer, and libfx. Most come with Bun drivers that run the real binary and have TLC check what it did. CI runs the libfx model; run the matching checker yourself when you change behavior that one of the others describes. You need Java and `tla2tools.jar`, and `tests/tla/README.md` lists every model and covers setup. ```bash tests/tla/session_manager/check.sh SessionLog -tests/tla/indexer/check.sh +tests/tla/mcp/check.sh --model Engine +bun test ./tests/tla/drivers/shell_command/ ``` ### Run the model evals diff --git a/src/mcp/io/trace.zig b/src/mcp/io/trace.zig index 784c47f25..e18ce1994 100644 --- a/src/mcp/io/trace.zig +++ b/src/mcp/io/trace.zig @@ -1,9 +1,10 @@ //! JSONL trace of core steps (format version 1). //! //! The I/O layer writes one line per `step` call when tracing is on. The Bun -//! bridge turns a trace into a TLA+ observation and asks TLC whether it is a -//! behavior of the machine's model. `data` carries only model projections -//! (ids, versions, flags, counters), never tokens or user content. +//! bridge in `tests/tla/drivers/mcp/bridge.ts` turns a trace into a TLA+ +//! observation and asks TLC whether it is a behavior of the machine's model +//! in `tests/tla/mcp/`. `data` carries only model projections (ids, versions, +//! flags, counters), never tokens or user content. const std = @import("std"); diff --git a/src/usage/policy.zig b/src/usage/policy.zig index aba5a9ad0..b607491d9 100644 --- a/src/usage/policy.zig +++ b/src/usage/policy.zig @@ -1,6 +1,6 @@ //! When `/usage` fetches, and what one fetch asks for. Pure; mirrors //! `FloorClear`, `Open`, `Manual`, `Timer` and `StartFetch` in the -//! LeanUsage TLA+ model. +//! LeanUsage TLA+ model (`tests/tla/usage/LeanUsage.tla`). const std = @import("std"); const report = @import("report.zig"); diff --git a/src/usage/view.zig b/src/usage/view.zig index 9af466d11..a51706f87 100644 --- a/src/usage/view.zig +++ b/src/usage/view.zig @@ -1,5 +1,5 @@ //! What `/usage` shows for one period, built from a cache entry. Pure; -//! mirrors `ViewOf` in the LeanUsage TLA+ model: today's numbers count only +//! mirrors `ViewOf` in `tests/tla/usage/LeanUsage.tla`: today's numbers count only //! when they belong to the current UTC day (`TodayIsToday`). const std = @import("std"); diff --git a/tests/AGENTS.md b/tests/AGENTS.md index 0c33ec4bd..49cacd774 100644 --- a/tests/AGENTS.md +++ b/tests/AGENTS.md @@ -32,10 +32,13 @@ tests/ │ └── render-lab/ rendering evidence tool ├── evals/ model-backed evals, run only on request └── tla/ TLA+ models, their checkers, and their Bun drivers - ├── session_manager/ one folder per model, named after the module it describes - ├── indexer/ - ├── sdk/ - └── drivers/ Bun drivers that walk real code along a model's state graph + ├── session_manager/ one folder per model area, named after the module it describes, + ├── mcp/ each with a check.sh; tla/README.md lists them all + ├── ... + ├── lib/ tlc.sh and run-tlc.sh: find TLC and run configs with their verdicts + └── drivers/ Bun drivers that run real code and have TLC check each run + ├── lib/ tlc.ts and context.ts, shared by every driver + └── / one folder per model area ``` Only files that end in `.test.ts` at the root of `tests/e2e/` are E2E tests. CI discovers them there and nowhere else, so a test in a subfolder never runs in CI. @@ -75,10 +78,10 @@ python3 -m scripts.pgso.corpus --manifest scripts/pgso/corpus.json --list # fr Every TLA+ spec, its TLC checker, the Bun drivers that walk code along a spec, and the design record a spec checks live in `tests/tla/`, and nowhere else. `tests/tla/README.md` lists the requirements and commands. -- Name a model's folder after the module it describes: `session_manager/` for `src/core/session_manager/`, `indexer/` for `src/core/indexer/`, and `sdk/` for libfx. -- Give each folder a `check.sh` that runs every config and exits non-zero when one misses its expected verdict. Configs that must fail, such as witnesses and planted mutations, are part of that contract, so encode their verdicts in `check.sh`. -- Put Bun drivers in `tests/tla/drivers/`. They import the code under test by relative path and read the state graphs a model's `check.sh` writes, such as `tests/tla/sdk/graphs/`. Generated graphs are ignored by git. -- Find TLC through `TLA2TOOLS_JAR` and Java through `JAVA_HOME`, then Homebrew's OpenJDK, then `PATH`, as the shell scripts do. +- Name a model's folder after the module it describes: `session_manager/` for `src/core/session_manager/`, `mcp_host/` for `src/core/mcp_host/`, and `sdk/` for libfx. +- Give each folder a `check.sh` that runs every config and exits non-zero when one misses its expected verdict. Configs that must fail, such as witnesses and planted mutations, are part of that contract, so encode their verdicts in `check.sh`. Source `../lib/tlc.sh` and list each config with its verdict for `tlc_verdicts`, rather than finding TLC yourself. +- Put Bun drivers in `tests/tla/drivers//`. They run the code under test, from `zig-out/bin/fx` or by relative import, and have TLC check each run. Use `drivers/lib/tlc.ts` to run TLC and `drivers/lib/context.ts` for the binary, the output folder, and the `tests/e2e/` helpers. Every fx process a driver starts sets `FX_SOUND=0`. Generated output, such as `tests/tla/sdk/graphs/`, goes to the temp folder or is ignored by git. +- A model of code that has not landed says so at the top, and the drivers that need that code run only behind an explicit flag, such as `--next` or `FX_TLA_NEXT_MCP=1`. `tests/tla/README.md` lists them. Remove the flag in the change that lands the code. - When a change alters behavior that a spec models, update the spec in the same change and run its checker. CI runs only the `sdk/` model and its drivers; run the others yourself. - A new model, checker, or driver gets a row in `tests/tla/README.md`. diff --git a/tests/tla/.gitignore b/tests/tla/.gitignore new file mode 100644 index 000000000..c18dd8d83 --- /dev/null +++ b/tests/tla/.gitignore @@ -0,0 +1 @@ +__pycache__/ diff --git a/tests/tla/README.md b/tests/tla/README.md index de3dfa4fd..0d4ad5463 100644 --- a/tests/tla/README.md +++ b/tests/tla/README.md @@ -4,10 +4,19 @@ TLA+ specifications for fx, checked with TLC, together with the scripts and Bun | Folder | What it models | Checker | |---|---|---| -| `session_manager/` | The session log, turn lifecycle, writer lock, snapshots, fork, subagents, catalog, host wiring, the side-file move, and v1 conversion. `system-design.md` is the design record the specs check and defines the `D1` to `D62` decision numbers that code comments cite. | `session_manager/check.sh` | -| `indexer/` | Refreshing a scanned root, and when a previous listing may be reused. | `indexer/check.sh` | -| `sdk/` | libfx durable sessions (`DurableSession.tla`), agent names and routing (`AgentRouting.tla`), and steering (`DurableSteer.tla`). `check.sh` also writes the TLC state graphs the drivers walk. | `sdk/check.sh`, then the drivers | -| `drivers/` | The Bun drivers. `drive.mjs`, `drive-agents.mjs`, and `drive-steer.mjs` walk the real SDK code along the `sdk/` state graphs and check every step against the model. | `bun drivers/drive.mjs`, `bun drivers/drive-agents.mjs` | +| `acp/` | The ACP permission modes, which match the CLI's `/permissions`, and the per-session Standard, Fast, and Ultrafast speed (`src/acp/`). | `acp/check.sh`, then the drivers in `drivers/acp/` | +| `cli/` | How `fx` and `fx ask` handle `--model`, `--fast`, `--ultrafast`, and `--effort` at launch, for the current design and a proposed one that validates them. | `cli/check.sh`, `bun test drivers/cli/` | +| `durable/` | Durable libfx sessions (`sdk/durable/`): the journal, tool replay, parallel batches, fencing, the inbox, resumption, and snapshots. | `durable/check.sh`, `durable/mutants.py` | +| `indexer/` | When a scanned root's listing may be reused, merging parallel grep results, the file picker's loading row, and listing snapshots (`src/core/indexer/`). | `indexer/check.sh` | +| `mcp/` | The MCP-v2 engine (`src/mcp/`): wire format, requests, stdio, version detection, the tool catalog, both HTTP transports, input-required rounds, authorization, subscriptions, elicitation, and the engine. `rules.md` lists the MCP specification rules the models cite by ID. | `mcp/check.sh`, then the drivers in `drivers/mcp/` | +| `mcp_host/` | fx's MCP host (`src/core/mcp_host/`): host lifecycle, saved credentials, logins shared between processes, sign-in, and elicitation routing. | `mcp_host/check.sh`, `bun test drivers/mcp_host/` | +| `sdk/` | libfx durable sessions (`DurableSession.tla`), agent names and routing (`AgentRouting.tla`), steering (`DurableSteer.tla`), and the provider credential edge (`ProviderAuth.tla`). `check.sh` also writes the TLC state graphs the drivers walk. | `sdk/check.sh`, then the drivers | +| `session_manager/` | The session log, turn lifecycle, writer lock, snapshots, fork, subagents, catalog, host wiring, the side-file move, and v1 conversion. `rollout/` holds the models of the changes that moved fx onto the session manager. `system-design.md` is the design record the specs check and defines the `D1` to `D62` decision numbers that code comments cite. | `session_manager/check.sh`, `session_manager/rollout/run.py`, `bun test drivers/session_manager/` | +| `shell_command/` | How an agent git command is admitted and run (`src/core/shell_command/safe_git.zig`), and one model turn through the shell tool, for the current design and a redesign. | `shell_command/check.sh`, `bun test drivers/shell_command/` | +| `terminal/` | The in-memory shell snapshot owner (`src/core/terminal/shell_snapshot.zig`) and the lifecycle of hosted terminals. | `terminal/check.sh` | +| `usage/` | `/usage` refreshes and the shared usage cache (`src/usage/`): `LeanUsage.tla` and `UsageModel.tla`. | `usage/check.sh`, then the drivers in `drivers/usage/` | +| `drivers/` | The Bun drivers. They run the real fx binary or SDK code, record what happens, and have TLC check each run against its model. `drive.mjs`, `drive-agents.mjs`, and `drive-steer.mjs` walk the SDK code along the `sdk/` state graphs. | See each folder's `check.sh` | +| `lib/` | `tlc.sh`, which finds TLC and Java and runs a table of configs with their expected verdicts, and `run-tlc.sh`, which runs TLC once for the drivers. | | ## Requirements @@ -20,15 +29,35 @@ curl -fL -o ~/.local/share/tla/tla2tools.jar \ https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar ``` -Set `TLA2TOOLS_JAR` to use a jar in another location. The shell scripts look for Java in `JAVA_HOME`, then in Homebrew's OpenJDK, then on `PATH`. +Set `TLA2TOOLS_JAR` to use a jar in another location. The scripts look for Java in `JAVA_HOME`, then in Homebrew's OpenJDK, then on `PATH`. The `mcp/`, `durable/`, and `session_manager/` runners also need Python 3. -The SDK drivers also need Bun, the native addon, and the durable World packages: +The drivers need Bun. Most of them also run the binary that `zig build` puts in `zig-out/bin/fx`, and the terminal ones need tmux. They take these settings from the environment: + +| Variable | Default | Effect | +|---|---|---| +| `FX_BIN` | `zig-out/bin/fx` | The binary under test | +| `FX_WORKTREE` | this checkout | The checkout whose binary and `tests/e2e/` helpers a driver uses | +| `FX_TLA_OUT` | a folder under the system temp folder | Where traces, TLC logs, and reports go | +| `FX_SOUND` | `0` in every driver | Keep it at `0`; sound playback can overload a machine during a run | + +The SDK drivers also need the native addon and the durable World packages: ```sh zig build libfx-napi -Dnapi-surface=core npm ci --prefix sdk/durable ``` +## Models of code that has not landed + +Some models describe the next MCP-v2 version, which `src/mcp/` and `src/core/mcp_host/` do not have yet. Their model checks pass, but the real code does not match them until that version lands: + +- In `mcp/`, `Engine`, `EngineTrace`, `HttpModern`, `HttpModernTrace`, `HttpLegacy`, and `StdioConn` say so at the top. `drivers/mcp/labs/engine_lab.zig` does not build against `src/mcp/` yet, so `drivers/mcp/driver.ts` runs its scenarios only with `--next`. +- In `drivers/mcp_host/`, the tests marked `NEXT_MCP` run only with `FX_TLA_NEXT_MCP=1`. + +The MCP-v2 models of the two HTTP transports, input-required rounds, authorization, subscriptions, and elicitation are model-checked only. Their traces came from a conformance adapter that is not part of fx. The `drivers/mcp_host/` sign-in tests drive real fx over HTTP against the fake server in `drivers/mcp/fakes/`. + +The `cli/` and `shell_command/` tests also check a proposed design. Those checks run only with `FX_TLA_PROPOSED=1`, and they fail until fx implements the design. + ## Run From the repository root: @@ -38,11 +67,16 @@ tests/tla/session_manager/check.sh # every session spec tests/tla/session_manager/check.sh SessionLog Fork # selected specs tests/tla/session_manager/mutants.py # every planted bug must be caught tests/tla/session_manager/trace/selftest.sh # the trace validator must accept and reject -tests/tla/indexer/check.sh # every refresh config and its expected verdict +tests/tla/session_manager/rollout/run.py check # the rollout models; mutate for their planted bugs +tests/tla/indexer/check.sh # every config and its expected verdict +tests/tla/acp/check.sh # likewise for acp/, cli/, durable/, shell_command/, terminal/, usage/ +tests/tla/mcp/check.sh # every MCP-v2 model and planted bug +tests/tla/mcp_host/check.sh # every MCP host model, planted bug, and finding tests/tla/sdk/check.sh # the SDK specs; writes the state graphs the drivers walk bun tests/tla/drivers/drive.mjs send --walks 40 # one durable-session graph; see .github/workflows/ci.yml for the rest bun tests/tla/drivers/drive-agents.mjs send --walks 60 # agent routing bun tests/tla/drivers/drive-steer.mjs ideal --walks 20 # steering +bun test ./tests/tla/drivers/shell_command/ # a driver written as bun tests; see each check.sh for its own ``` -`Fork` and `V1Conversion` can run for many minutes. `session_manager/README.md` describes each session spec, the planted bugs, and the trace checkers. +A `check.sh` that uses `lib/tlc.sh` takes config names to run only those, for example `tests/tla/usage/check.sh LeanUsage`. `Fork`, `V1Conversion`, and the full `LeanUsage` config can run for many minutes. `session_manager/README.md` describes each session spec, the planted bugs, and the trace checkers. diff --git a/tests/tla/acp/AcpPermissionModes.tla b/tests/tla/acp/AcpPermissionModes.tla new file mode 100644 index 000000000..8bd30044e --- /dev/null +++ b/tests/tla/acp/AcpPermissionModes.tla @@ -0,0 +1,210 @@ +------------------------- MODULE AcpPermissionModes ------------------------- +(***************************************************************************) +(* fx's ACP permission-mode contract, matching the CLI's /permissions. *) +(* *) +(* - ACP lists exactly the CLI's three modes, in this order: auto (the *) +(* default), ask, full-access, named Auto, Ask, Full access. Both the *) +(* `mode` config option and the older `modes` field list them and show *) +(* the same current mode. *) +(* - A session (new, resumed, or new in a fresh process) starts in the *) +(* profile's saved permission_mode as it is when the session starts; *) +(* an unset profile means auto. Another fx process saving a mode does *) +(* not change a session that is already open. *) +(* - An accepted change, through session/set_config_option or the older *) +(* session/set_mode, switches the session and saves the mode as the *) +(* profile's default, as /permissions does in the CLI. *) +(* - Any other value is rejected and changes nothing. *) +(* - A prompt is enforced by the mode the client was shown: ask asks the *) +(* client, auto sends the action to fx's automatic reviewer, and full *) +(* access runs it without asking. *) +(* - Mode option values carry only ACP's fields (value, name, *) +(* description, _meta). *) +(* *) +(* `last` is what the client observes for the latest step; `stored` is *) +(* the profile's saved mode read back from settings.json after the step. *) +(* *) +(* Assumptions: one fx acp process at a time drives one active session; *) +(* other fx processes may save a mode between steps (External); resume *) +(* follows a prompt (fx saves a chat at its first turn). *) +(***************************************************************************) +EXTENDS Naturals, Sequences + +CONSTANTS Profiles, \* saved modes a run may start from: Modes \cup {"unset"} + Values \* values a client may send: Modes plus unknown ones + +ModeSeq == <<"auto", "ask", "full-access">> +Modes == {ModeSeq[k] : k \in 1..Len(ModeSeq)} +ModesCsv == "auto,ask,full-access" +NamesCsv == "Auto,Ask,Full access" +DefaultMode == "auto" + +Eff(p) == IF p = "unset" THEN DefaultMode ELSE p + +\* How the prompt probe (a shell call that writes a file) is handled. The +\* client declines permission requests and the reviewer clears the action. +Enforce(m) == + CASE m = "ask" -> "asked/no-run" + [] m = "auto" -> "reviewed/ran" + [] m = "full-access" -> "direct/ran" + +VARIABLES profile, cur, saved, last +vars == <> + +NoView == [current |-> "", legacy |-> "", listed |-> "", legacyListed |-> "", + names |-> "", schemaOk |-> TRUE] + +\* session/new and session/resume responses carry configOptions and modes. +SessionView(m) == [current |-> m, legacy |-> m, listed |-> ModesCsv, + legacyListed |-> ModesCsv, names |-> NamesCsv, schemaOk |-> TRUE] + +\* set_config_option responses carry configOptions only. +ConfigView(m) == [SessionView(m) EXCEPT !.legacy = "n/a", !.legacyListed = "n/a"] + +\* `fx status --json` lists the modes and the one a new session starts in. +StatusView(m) == ConfigView(m) + +Obs(op, arg, ok, hasView, view, enforce, stored) == + [op |-> op, arg |-> arg, ok |-> ok, hasView |-> hasView, view |-> view, + enforce |-> enforce, stored |-> stored] + +Init == + /\ profile \in Profiles + /\ cur = Eff(profile) + /\ saved = FALSE + /\ last = Obs("new", "none", TRUE, TRUE, SessionView(Eff(profile)), "none", profile) + +SetConfig(v) == + IF v \in Modes + THEN /\ cur' = v + /\ profile' = v + /\ last' = Obs("set", v, TRUE, TRUE, ConfigView(v), "none", v) + /\ UNCHANGED saved + ELSE /\ last' = Obs("set", v, FALSE, FALSE, NoView, "none", profile) + /\ UNCHANGED <> + +\* session/set_mode answers null, so the client sees no view. +SetLegacy(v) == + IF v \in Modes + THEN /\ cur' = v + /\ profile' = v + /\ last' = Obs("legacy", v, TRUE, FALSE, NoView, "none", v) + /\ UNCHANGED saved + ELSE /\ last' = Obs("legacy", v, FALSE, FALSE, NoView, "none", profile) + /\ UNCHANGED <> + +Prompt == + /\ saved' = TRUE + /\ last' = Obs("prompt", "none", TRUE, FALSE, NoView, Enforce(cur), profile) + /\ UNCHANGED <> + +\* A new fx acp process resumes the session. +Resume == + /\ saved + /\ LET resumed == Eff(profile) IN + /\ cur' = resumed + /\ last' = Obs("resume", "none", TRUE, TRUE, SessionView(resumed), "none", profile) + /\ UNCHANGED <> + +\* A new fx acp process starts a new session. +Fresh == + /\ LET started == Eff(profile) IN + /\ cur' = started + /\ last' = Obs("fresh", "none", TRUE, TRUE, SessionView(started), "none", profile) + /\ saved' = FALSE + /\ UNCHANGED profile + +\* session/new in the running process. +NewSession == + /\ LET opened == Eff(profile) IN + /\ cur' = opened + /\ last' = Obs("new", "none", TRUE, TRUE, SessionView(opened), "none", profile) + /\ saved' = FALSE + /\ UNCHANGED profile + +\* Another fx process (the CLI's /permissions, or another ACP process) +\* saves a mode. The open session keeps its own, like a second CLI window. +External(v) == + /\ profile' = v + /\ last' = Obs("other", v, TRUE, FALSE, NoView, "none", v) + /\ UNCHANGED <> + +\* `fx status --json` in the workspace, run beside the ACP process. +Status == + /\ last' = Obs("status", "none", TRUE, TRUE, StatusView(Eff(profile)), "none", profile) + /\ UNCHANGED <> + +Next == + \/ \E v \in Values : SetConfig(v) \/ SetLegacy(v) + \/ \E v \in Modes : External(v) + \/ Prompt + \/ Resume + \/ Fresh + \/ NewSession + \/ Status + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Safety properties. EnforceTable restates the expected handling so a *) +(* change to Enforce is caught. *) + +EnforceTable == [m \in Modes |-> + IF m = "ask" THEN "asked/no-run" + ELSE IF m = "auto" THEN "reviewed/ran" + ELSE "direct/ran"] + +SessionOps == {"new", "resume", "fresh"} +ChangeOps == {"set", "legacy"} + +ListsExactlyCliModes == + last.hasView => + /\ last.view.listed = ModesCsv + /\ last.view.names = NamesCsv + /\ last.view.legacyListed \in {ModesCsv, "n/a"} + +SchemaClean == last.hasView => last.view.schemaOk + +ReportsEnforcedMode == + (last.hasView /\ last.op # "status") => /\ last.view.current = cur + /\ last.view.legacy \in {cur, "n/a"} + +\* Status describes the next session, which may differ from an open one. +StatusMatchesNextSession == last.op = "status" => last.view.current = Eff(profile) + +SessionsStartFromProfile == + last.op \in SessionOps => /\ cur = Eff(profile) + /\ last.view.legacy = cur + /\ last.view.legacyListed = ModesCsv + +DefaultIsAuto == + (last.op \in SessionOps /\ profile = "unset") => cur = "auto" + +UnknownRejected == last.op \in ChangeOps => (last.ok <=> last.arg \in Modes) + +ChangeIsSaved == + (last.op \in ChangeOps /\ last.ok) => /\ cur = last.arg + /\ profile = last.arg + +StoredIsProfile == last.stored = profile + +PromptEnforcesMode == last.op = "prompt" => last.enforce = EnforceTable[cur] + +TypeOK == + /\ profile \in Modes \cup {"unset"} + /\ cur \in Modes + /\ saved \in BOOLEAN + +\* A rejected change leaves the session and the profile as they were. +RejectedChangesNothing == + [][(last'.op \in ChangeOps /\ ~last'.ok) => UNCHANGED <>]_vars + +\* Another process's choice never changes the open session. +OpenSessionKeepsMode == [][last'.op = "other" => cur' = cur]_vars + +\* A session only enters full access when the user picks it, or when it +\* starts while full access is the saved mode. +FullAccessOnlyByChoice == + [][(cur' = "full-access" /\ cur # "full-access") => + \/ (last'.op \in ChangeOps /\ last'.arg = "full-access") + \/ (last'.op \in SessionOps /\ profile' = "full-access")]_vars +============================================================================= diff --git a/tests/tla/acp/AcpPermissionModesTrace.tla b/tests/tla/acp/AcpPermissionModesTrace.tla new file mode 100644 index 000000000..6d244bf49 --- /dev/null +++ b/tests/tla/acp/AcpPermissionModesTrace.tla @@ -0,0 +1,50 @@ +--------------------- MODULE AcpPermissionModesTrace --------------------- +(***************************************************************************) +(* Trace validation: replays one observed run of the real `fx acp` binary *) +(* against AcpPermissionModes. TraceLog comes from the generated *) +(* AcpPermissionModesObs module; each element has the fields of Obs. *) +(* *) +(* NotDone is a sentinel: TLC reporting it violated means every *) +(* observation matched a spec step. Exhausting the search without that *) +(* violation means the run is not a behavior of the spec. *) +(***************************************************************************) +EXTENDS AcpPermissionModes, AcpPermissionModesObs, Sequences + +VARIABLE i + +traceVars == <> + +Match(o) == + /\ last.op = o.op + /\ last.arg = o.arg + /\ last.ok = o.ok + /\ last.hasView = o.hasView + /\ o.hasView => (last.view = o.view) + /\ last.enforce = o.enforce + /\ last.stored = o.stored + +StepFor(o) == + CASE o.op = "set" -> SetConfig(o.arg) + [] o.op = "legacy" -> SetLegacy(o.arg) + [] o.op = "prompt" -> Prompt + [] o.op = "resume" -> Resume + [] o.op = "fresh" -> Fresh + [] o.op = "new" -> NewSession + [] o.op = "other" -> External(o.arg) + [] o.op = "status" -> Status + [] OTHER -> FALSE + +ASSUME Len(TraceLog) >= 1 /\ TraceLog[1].op = "new" + +TraceInit == /\ i = 1 + /\ Init + /\ Match(TraceLog[1]) + +TraceNext == /\ i < Len(TraceLog) + /\ \E o \in {TraceLog[i + 1]} : + /\ StepFor(o) + /\ Match(o)' + /\ i' = i + 1 + +NotDone == i < Len(TraceLog) +============================================================================= diff --git a/tests/tla/acp/AcpSpeed.tla b/tests/tla/acp/AcpSpeed.tla new file mode 100644 index 000000000..45d83edb4 --- /dev/null +++ b/tests/tla/acp/AcpSpeed.tla @@ -0,0 +1,138 @@ +------------------------------- MODULE AcpSpeed ------------------------------- +(***************************************************************************) +(* Per-session speed contract for fx's ACP server, mirroring the CLI: *) +(* one Standard / Fast / Ultrafast choice per chat. *) +(* *) +(* - A client sees the `fast` option only for models that offer Fast and *) +(* the `ultrafast` option only for models that offer Ultrafast. *) +(* - Turning one lane on turns the other off. *) +(* - Enabling a lane the model lacks is rejected; disabling always works. *) +(* - Switching models turns off a lane the new model lacks. *) +(* - The choice is saved with the chat and survives resume. *) +(* - Unknown config ids are rejected instead of silently succeeding. *) +(* - A prompt carries Ultrafast, else Fast when the model supports it. *) +(* *) +(* `fast` may start on for a model without Fast when the user's settings *) +(* default enables it (CLI parity); it is then hidden and has no effect. *) +(* Every value is a string or boolean so TLC never compares mixed types. *) +(***************************************************************************) +EXTENDS Naturals, TLC + +CONSTANTS Models, SupFast, SupUltra + +ASSUME SupFast \subseteq Models /\ SupUltra \subseteq Models + +VARIABLES model, fast, ultra, last + +vars == <> + +Ops == {"new", "fast", "ultrafast", "model", "unknown", "prompt", "resume"} +Speeds == {"none", "standard", "fast", "ultrafast"} + +Bool(b) == IF b THEN "true" ELSE "false" + +(* What a client reads from configOptions after a step. *) +View == [model |-> model, + fast |-> IF model \in SupFast THEN Bool(fast) ELSE "absent", + ultra |-> IF model \in SupUltra THEN Bool(ultra) ELSE "absent"] + +(* The lane a prompt sends to the Gateway. *) +RequestSpeed == IF ultra THEN "ultrafast" + ELSE IF fast /\ model \in SupFast THEN "fast" + ELSE "standard" + +Result(op, arg, ok, speed) == [op |-> op, arg |-> arg, ok |-> ok, speed |-> speed] + +Init == /\ model \in Models + /\ fast \in BOOLEAN + /\ ultra = FALSE + /\ last = Result("new", "none", TRUE, "none") + +SetFast(b) == + IF b /\ model \notin SupFast + THEN /\ last' = Result("fast", Bool(b), FALSE, "none") + /\ UNCHANGED <> + ELSE /\ fast' = b + /\ ultra' = (ultra /\ ~b) + /\ last' = Result("fast", Bool(b), TRUE, "none") + /\ UNCHANGED model + +SetUltra(b) == + IF b /\ model \notin SupUltra + THEN /\ last' = Result("ultrafast", Bool(b), FALSE, "none") + /\ UNCHANGED <> + ELSE /\ ultra' = b + /\ fast' = (fast /\ ~b) + /\ last' = Result("ultrafast", Bool(b), TRUE, "none") + /\ UNCHANGED model + +SetModel(m) == + /\ model' = m + /\ fast' = (fast /\ m \in SupFast) + /\ ultra' = (ultra /\ m \in SupUltra) + /\ last' = Result("model", m, TRUE, "none") + +SetUnknown == + /\ last' = Result("unknown", "none", FALSE, "none") + /\ UNCHANGED <> + +Prompt == + /\ last' = Result("prompt", "none", TRUE, RequestSpeed) + /\ UNCHANGED <> + +(* A new process resumes the saved chat. Assumption: the chat has had a *) +(* prompt; the v2 store saves a chat at its first turn, so resuming an *) +(* untouched chat fails on main independently of speed. *) +Resume == + /\ last' = Result("resume", "none", TRUE, "none") + /\ UNCHANGED <> + +Next == \/ \E b \in BOOLEAN : SetFast(b) \/ SetUltra(b) + \/ \E m \in Models : SetModel(m) + \/ SetUnknown + \/ Prompt + \/ Resume + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Safety properties checked by TLC; planted mutants must violate them. *) + +TypeOK == /\ model \in Models + /\ fast \in BOOLEAN + /\ ultra \in BOOLEAN + /\ last.op \in Ops + /\ last.ok \in BOOLEAN + /\ last.speed \in Speeds + +(* Fast and Ultrafast are never both on. *) +Exclusive == ~(fast /\ ultra) + +(* Ultrafast is never on while hidden: a hidden lane would fail prompts. *) +UltraValid == ultra => model \in SupUltra + +(* Fast is never left on after a switch to a model without it. *) +SwitchClearsFast == last.op = "model" => (fast => model \in SupFast) + +(* An accepted lane request takes effect. *) +RequestHonored == + (last.ok /\ last.op = "fast") => Bool(fast) = last.arg +RequestHonoredUltra == + (last.ok /\ last.op = "ultrafast") => Bool(ultra) = last.arg + +(* Only enabling an unsupported lane is rejected. *) +RejectOnlyUnsupported == + /\ (last.op = "fast" /\ ~last.ok) => (last.arg = "true" /\ model \notin SupFast) + /\ (last.op = "ultrafast" /\ ~last.ok) => (last.arg = "true" /\ model \notin SupUltra) +AcceptOnlySupported == + /\ (last.op = "fast" /\ last.ok /\ last.arg = "true") => model \in SupFast + /\ (last.op = "ultrafast" /\ last.ok /\ last.arg = "true") => model \in SupUltra + +(* Unknown config ids are errors. *) +UnknownRejected == last.op = "unknown" => ~last.ok + +(* A prompt never sends a lane the model lacks. *) +PromptLaneSupported == + /\ (last.op = "prompt" /\ last.speed = "fast") => model \in SupFast + /\ (last.op = "prompt" /\ last.speed = "ultrafast") => model \in SupUltra +============================================================================= diff --git a/tests/tla/acp/AcpSpeedTrace.tla b/tests/tla/acp/AcpSpeedTrace.tla new file mode 100644 index 000000000..f6461de50 --- /dev/null +++ b/tests/tla/acp/AcpSpeedTrace.tla @@ -0,0 +1,52 @@ +---------------------------- MODULE AcpSpeedTrace ---------------------------- +(***************************************************************************) +(* Trace validation: replays one observed run of the real `fx acp` binary *) +(* against AcpSpeed. TraceLog comes from the generated AcpSpeedObs module. *) +(* Each element is *) +(* [op, arg, ok, speed, hasView, view] *) +(* where view is the client-visible configOptions projection. Steps that *) +(* return no config (errors and prompts) set hasView to FALSE and carry a *) +(* placeholder record, so TLC never compares a record with a string. *) +(* *) +(* NotDone is a sentinel: TLC reporting it violated (exit 12) means every *) +(* observation matched a spec step. Exhausting the search without that *) +(* violation means the run is not a behavior of the spec. *) +(***************************************************************************) +EXTENDS AcpSpeed, AcpSpeedObs, Sequences + +VARIABLE i + +traceVars == <> + +Match(o) == + /\ last.op = o.op + /\ last.arg = o.arg + /\ last.ok = o.ok + /\ last.speed = o.speed + /\ o.hasView => (View = o.view) + +StepFor(o) == + CASE o.op = "fast" -> SetFast(o.arg = "true") + [] o.op = "ultrafast" -> SetUltra(o.arg = "true") + [] o.op = "model" -> SetModel(o.arg) + [] o.op = "unknown" -> SetUnknown + [] o.op = "prompt" -> Prompt + [] o.op = "resume" -> Resume + [] OTHER -> FALSE + +ASSUME Len(TraceLog) >= 1 /\ TraceLog[1].op = "new" + +TraceInit == /\ i = 1 + /\ Init + /\ Match(TraceLog[1]) + +TraceNext == /\ i < Len(TraceLog) + /\ \E o \in {TraceLog[i + 1]} : + /\ StepFor(o) + /\ Match(o)' + /\ i' = i + 1 + +TraceSpec == TraceInit /\ [][TraceNext]_traceVars + +NotDone == i < Len(TraceLog) +============================================================================= diff --git a/tests/tla/acp/MCAcpPermissionModes.cfg b/tests/tla/acp/MCAcpPermissionModes.cfg new file mode 100644 index 000000000..792cb3c4a --- /dev/null +++ b/tests/tla/acp/MCAcpPermissionModes.cfg @@ -0,0 +1,22 @@ +CONSTANTS + Profiles <- MCProfiles + Values <- MCValues +INIT Init +NEXT Next +INVARIANTS + ListsExactlyCliModes + SchemaClean + ReportsEnforcedMode + StatusMatchesNextSession + SessionsStartFromProfile + DefaultIsAuto + UnknownRejected + ChangeIsSaved + StoredIsProfile + PromptEnforcesMode + TypeOK +PROPERTIES + RejectedChangesNothing + OpenSessionKeepsMode + FullAccessOnlyByChoice +CHECK_DEADLOCK FALSE diff --git a/tests/tla/acp/MCAcpPermissionModes.tla b/tests/tla/acp/MCAcpPermissionModes.tla new file mode 100644 index 000000000..611c1f9a7 --- /dev/null +++ b/tests/tla/acp/MCAcpPermissionModes.tla @@ -0,0 +1,9 @@ +------------------------ MODULE MCAcpPermissionModes ------------------------ +(* Exhaustive model: every starting profile, the three modes plus unknown *) +(* values a client might still send (the old "code" mode and the CLI's *) +(* internal "yolo" name). *) +EXTENDS AcpPermissionModes + +MCProfiles == {"unset", "auto", "ask", "full-access"} +MCValues == {"auto", "ask", "full-access", "code", "yolo"} +============================================================================= diff --git a/tests/tla/acp/MCAcpSpeed.cfg b/tests/tla/acp/MCAcpSpeed.cfg new file mode 100644 index 000000000..8307ca155 --- /dev/null +++ b/tests/tla/acp/MCAcpSpeed.cfg @@ -0,0 +1,22 @@ +\* Exhaustive check of the speed contract over three catalog shapes: +\* a model with both lanes, one with Fast only, and one with neither. +CONSTANTS + Models <- MCModels + SupFast <- MCSupFast + SupUltra <- MCSupUltra + +SPECIFICATION Spec + +INVARIANTS + TypeOK + Exclusive + UltraValid + SwitchClearsFast + RequestHonored + RequestHonoredUltra + RejectOnlyUnsupported + AcceptOnlySupported + UnknownRejected + PromptLaneSupported + +CHECK_DEADLOCK FALSE diff --git a/tests/tla/acp/MCAcpSpeed.tla b/tests/tla/acp/MCAcpSpeed.tla new file mode 100644 index 000000000..d6067e33a --- /dev/null +++ b/tests/tla/acp/MCAcpSpeed.tla @@ -0,0 +1,9 @@ +----------------------------- MODULE MCAcpSpeed ----------------------------- +(* Model-checking constants: the same three catalog shapes the runtime *) +(* driver serves from its fake Gateway. *) +EXTENDS AcpSpeed + +MCModels == {"openai/gpt-6-astra", "openai/gpt-5.6-priority", "anthropic/claude-plain"} +MCSupFast == {"openai/gpt-6-astra", "openai/gpt-5.6-priority"} +MCSupUltra == {"openai/gpt-6-astra"} +============================================================================= diff --git a/tests/tla/acp/check.sh b/tests/tla/acp/check.sh new file mode 100755 index 000000000..2bfbb9198 --- /dev/null +++ b/tests/tla/acp/check.sh @@ -0,0 +1,26 @@ +#!/bin/sh +# Model-check the ACP models with TLC and require each config's expected +# verdict. +# +# AcpPermissionModes: the ACP permission-mode contract, which matches the CLI's +# /permissions. AcpSpeed: the per-session Standard, Fast, and Ultrafast speed +# contract. Both configs must pass. +# +# The planted bugs and the runs of the real `fx acp` binary are in +# ../drivers/acp/: +# bun ../drivers/acp/permission_modes/check-spec.ts +# bun ../drivers/acp/permission_modes/driver.ts +# bun ../drivers/acp/speed/check-spec.ts +# bun ../drivers/acp/speed/driver.ts +# +# Needs Java 11+ and tla2tools.jar, as ../README.md describes. +set -eu + +cd "$(dirname "$0")" +# shellcheck source=../lib/tlc.sh +. ../lib/tlc.sh + +tlc_verdicts "$@" <<'EOF' +MCAcpPermissionModes MCAcpPermissionModes - +MCAcpSpeed MCAcpSpeed - +EOF diff --git a/tests/tla/cli/LaunchSelection.tla b/tests/tla/cli/LaunchSelection.tla new file mode 100644 index 000000000..549ca5dc2 --- /dev/null +++ b/tests/tla/cli/LaunchSelection.tla @@ -0,0 +1,268 @@ +---------------------------- MODULE LaunchSelection ---------------------------- +(***************************************************************************) +(* Launch-time model, speed and effort flags for `fx` and `fx ask`. *) +(* *) +(* One scenario fixes what the user asked for, what the catalog load *) +(* returns, and what the chosen model supports. The machine then runs the *) +(* entry point: *) +(* *) +(* ask: AskValidate -> Send *) +(* interactive: FirstFrame, then CatalogReady and Submit in the order *) +(* the scenario fixes (early = submit before the catalog). *) +(* *) +(* Send applies the turn-time gates that exist in both designs: Fast is *) +(* masked unless the catalog confirms it, Ultra fails the turn unless the *) +(* catalog confirms it, and effort is dropped unless the catalog lists it. *) +(* *) +(* Design = "current" has no launch validation at all. Design = *) +(* "proposed" validates at launch. Mutant plants one bug in the proposed *) +(* design so each invariant is shown to fail when its rule is broken. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets, TLC + +CONSTANTS + Design, \* "current" | "proposed" + Mutant, \* "none" | "reject_weak" | "no_canonical" | "block_frame" | "persist" | "silent" + Class \* "all" | "ideal" | "nonideal": which scenarios Init may pick + +ASSUME Design \in {"current", "proposed"} +ASSUME Mutant \in {"none", "reject_weak", "no_canonical", "block_frame", "persist", "silent"} +ASSUME Class \in {"all", "ideal", "nonideal"} + +VARIABLE st +vars == <> + +(* ----------------------------- Scenarios -------------------------------- *) + +Paths == {"ask", "interactive"} +(* none: no --model flag, the configured model is used. *) +(* private_hidden: a real team model that only an authenticated catalog *) +(* lists; the anonymous public catalog does not. *) +ModelReqs == {"none", "exact", "partial_unique", "partial_ambiguous", "unknown", "private_hidden"} +SpeedReqs == {"none", "fast", "ultrafast", "off"} +EffortReqs == {"none", "supported", "unsupported"} +(* absent: a provider without a catalog, such as a configured provider. *) +Catalogs == {"authenticated", "anonymous", "failed", "absent"} + +ScenarioSpace == + [path: Paths, model: ModelReqs, speed: SpeedReqs, effort: EffortReqs, + catalog: Catalogs, fastCap: BOOLEAN, ultraCap: BOOLEAN, early: BOOLEAN] + +Ideal(s) == + /\ s.catalog = "authenticated" + /\ s.model \in {"none", "exact"} + /\ s.speed = "fast" => s.fastCap + /\ s.speed = "ultrafast" => s.ultraCap + /\ s.effort # "unsupported" + /\ ~s.early + +Scenarios == + { s \in ScenarioSpace : + /\ s.path = "ask" => ~s.early + /\ CASE Class = "all" -> TRUE + [] Class = "ideal" -> Ideal(s) + [] Class = "nonideal" -> ~Ideal(s) } + +(* ------------------------- Catalog and gateway --------------------------- *) + +Loaded(s) == s.catalog \in {"authenticated", "anonymous"} +Authoritative(s) == s.catalog = "authenticated" + +(* What matchCatalogModel returns for the --model text. *) +Match(s) == + IF ~Loaded(s) THEN "no_catalog" + ELSE CASE s.model = "none" -> "none" + [] s.model = "exact" -> "matched" + [] s.model = "partial_unique" -> "matched" + [] s.model = "partial_ambiguous" -> "ambiguous" + [] s.model = "unknown" -> "unknown" + [] s.model = "private_hidden" -> IF Authoritative(s) THEN "matched" ELSE "unknown" + +(* Model names: "raw" is the --model text, "canonical" the catalog ID, *) +(* "configured" the saved model. An exact ID is already canonical. *) +Name(s, m) == IF m = "raw" /\ s.model \in {"exact", "private_hidden"} THEN "canonical" ELSE m + +(* The real gateway accepts a name only when that model exists. *) +GatewayAccepts(s, m) == Name(s, m) \in {"canonical", "configured"} + +(* fx knows the capabilities of the model it will send only when the loaded *) +(* catalog lists that exact name. *) +CapKnownFor(s, m) == + /\ Loaded(s) + /\ \/ Name(s, m) = "configured" + \/ /\ Name(s, m) = "canonical" + /\ (s.model = "private_hidden" => Authoritative(s)) + +(* -------------------------------- State ---------------------------------- *) + +(* Placeholder before any request; after = FALSE keeps it out of every check. *) +NoReq == + [ model |-> "none", claimedFast |-> FALSE, wireFast |-> FALSE, claimedUltra |-> FALSE, + wireUltra |-> FALSE, claimedEffort |-> "none", wireEffort |-> "none", after |-> FALSE ] + +Fresh(s) == + [ sc |-> s, + phase |-> "start", \* start | running | done + catalogSeen |-> FALSE, \* interactive: the UI saw the load finish + sel |-> [ model |-> IF s.model = "none" THEN "configured" ELSE "raw", + fast |-> s.speed = "fast", + ultra |-> s.speed = "ultrafast", + effort |-> s.effort ], + outcome |-> "pending", + req |-> NoReq, + corrections |-> {}, + notices |-> {}, + persisted |-> FALSE ] + +Init == st \in { Fresh(s) : s \in Scenarios } + +S == st.sc + +(* The proposed decision, shared by both entry points. *) +ModelRejected(s) == + /\ Match(s) \in {"ambiguous", "unknown"} + /\ (Authoritative(s) \/ Mutant = "reject_weak") + +Resolved(s, cur) == + IF Match(s) = "matched" /\ Mutant # "no_canonical" THEN "canonical" ELSE cur + +(* -------------------------------- ask ------------------------------------ *) + +AskValidate == + /\ S.path = "ask" + /\ st.phase = "start" + /\ IF Design = "current" + THEN st' = [st EXCEPT !.phase = "running"] + ELSE LET m == Resolved(S, st.sel.model) + k == CapKnownFor(S, m) + reason == + CASE ModelRejected(S) -> "rejected_model" + [] st.sel.ultra /\ ~(k /\ S.ultraCap) -> "rejected_ultrafast" + [] st.sel.fast /\ k /\ ~S.fastCap -> "rejected_fast" + [] st.sel.effort = "unsupported" /\ k -> "rejected_effort" + [] OTHER -> "none" + IN st' = [st EXCEPT !.sel.model = m, + !.phase = IF reason = "none" THEN "running" ELSE "done", + !.outcome = IF reason = "none" THEN "pending" ELSE reason] + +(* ----------------------------- interactive ------------------------------- *) + +FirstFrame == + /\ S.path = "interactive" + /\ st.phase = "start" + /\ Mutant = "block_frame" => st.catalogSeen + /\ st' = [st EXCEPT !.phase = "running"] + +Corrected(s, sel) == + IF ModelRejected(s) + THEN [ sel |-> [model |-> "configured", fast |-> FALSE, ultra |-> FALSE, effort |-> "none"], + corrections |-> {"model"} ] + ELSE LET m == Resolved(s, sel.model) + k == CapKnownFor(s, m) + fast == sel.fast /\ ~(k /\ ~s.fastCap) + ultra == sel.ultra /\ k /\ s.ultraCap + effort == IF sel.effort = "unsupported" /\ k THEN "none" ELSE sel.effort + IN [ sel |-> [model |-> m, fast |-> fast, ultra |-> ultra, effort |-> effort], + corrections |-> { c \in {"fast", "ultrafast", "effort"} : + CASE c = "fast" -> fast # sel.fast + [] c = "ultrafast" -> ultra # sel.ultra + [] c = "effort" -> effort # sel.effort } ] + +CatalogReady == + /\ S.path = "interactive" + /\ ~st.catalogSeen + /\ S.early => st.phase = "done" + /\ IF Design = "current" + THEN st' = [st EXCEPT !.catalogSeen = TRUE] + ELSE LET c == Corrected(S, st.sel) IN + st' = [st EXCEPT !.catalogSeen = TRUE, + !.sel = c.sel, + !.corrections = c.corrections, + !.notices = IF Mutant = "silent" THEN {} ELSE c.corrections, + !.persisted = Mutant = "persist" /\ c.corrections # {}] + +(* ------------------------------- sending --------------------------------- *) + +Send == + /\ st.phase = "running" + /\ S.path = "interactive" => (S.early <=> ~st.catalogSeen) + /\ LET m == st.sel.model + k == CapKnownFor(S, m) + IN IF st.sel.ultra /\ ~(k /\ S.ultraCap) + THEN st' = [st EXCEPT !.phase = "done", !.outcome = "turn_error"] + ELSE st' = [st EXCEPT + !.phase = "done", + !.outcome = IF GatewayAccepts(S, m) THEN "sent" ELSE "gateway_error", + !.req = [ model |-> Name(S, m), + claimedFast |-> st.sel.fast, + wireFast |-> st.sel.fast /\ k /\ S.fastCap, + claimedUltra |-> st.sel.ultra, + wireUltra |-> st.sel.ultra, + claimedEffort |-> st.sel.effort, + wireEffort |-> IF st.sel.effort = "supported" /\ k THEN "supported" ELSE "none", + after |-> S.path = "ask" \/ st.catalogSeen ]] + +Finished == + /\ st.phase = "done" + /\ S.path = "interactive" => st.catalogSeen + +Next == + \/ AskValidate + \/ FirstFrame + \/ CatalogReady + \/ Send + \/ (Finished /\ UNCHANGED vars) + +Spec == Init /\ [][Next]_vars + +(* Weak fairness: an enabled step eventually happens, so every run ends. *) +FairSpec == Spec /\ WF_vars(Next) + +(* ------------------------------ Invariants ------------------------------- *) + +(* A request sent after the decision point (always for ask; after the UI *) +(* saw the catalog for interactive). *) +Decided == st.req.after + +(* With an authenticated catalog, fx never sends a model that does not exist. *) +ValidModel == Decided /\ Authoritative(S) => GatewayAccepts(S, st.req.model) + +(* When fx knows the capabilities, the speed it shows is the speed it sends. *) +HonestSpeed == + Decided /\ CapKnownFor(S, st.req.model) => + /\ st.req.claimedFast = st.req.wireFast + /\ st.req.claimedUltra = st.req.wireUltra + +(* When fx knows the capabilities, the effort it claims is the effort it sends. *) +HonestEffort == + Decided /\ CapKnownFor(S, st.req.model) => st.req.claimedEffort = st.req.wireEffort + +(* fx ask fails during validation, never with a late turn error. *) +AskFailsEarly == S.path = "ask" => st.outcome # "turn_error" + +(* Every rejection or correction is backed by catalog evidence. *) +NoFalseReject == + /\ (st.outcome = "rejected_model" \/ "model" \in st.corrections) => + Authoritative(S) /\ S.model \in {"partial_ambiguous", "unknown"} + /\ (st.outcome = "rejected_fast" \/ "fast" \in st.corrections) => + CapKnownFor(S, st.sel.model) /\ ~S.fastCap + /\ (st.outcome = "rejected_effort" \/ "effort" \in st.corrections) => + CapKnownFor(S, st.sel.model) /\ S.effort = "unsupported" + /\ (st.outcome = "rejected_ultrafast" \/ "ultrafast" \in st.corrections) => + ~(CapKnownFor(S, st.sel.model) /\ S.ultraCap) + +(* A unique partial name runs on its catalog ID. *) +Canonical == Decided /\ S.model = "partial_unique" /\ Loaded(S) => st.req.model = "canonical" + +(* Per-launch flags never rewrite saved settings. *) +SettingsUntouched == ~st.persisted + +(* The interactive first frame never waits for the catalog. *) +FirstFrameNotBlocked == (S.path = "interactive" /\ st.phase = "start") => ENABLED FirstFrame + +(* Every automatic correction is announced. *) +CorrectionsAnnounced == st.corrections \subseteq st.notices + +(* Every behavior ends. *) +Termination == <>Finished +============================================================================= diff --git a/tests/tla/cli/LaunchTrace.tla b/tests/tla/cli/LaunchTrace.tla new file mode 100644 index 000000000..049425c28 --- /dev/null +++ b/tests/tla/cli/LaunchTrace.tla @@ -0,0 +1,65 @@ +---------------------------- MODULE LaunchTrace ---------------------------- +(***************************************************************************) +(* Trace validation: replays behavior observed from the real fx binary *) +(* through LaunchSelection's own actions. *) +(* *) +(* LaunchObserved is generated by bun/bridge.ts. It defines Observed, a *) +(* sequence of records *) +(* [sc, orderFree, outcome, notices, req] *) +(* where sc is a LaunchSelection scenario, req is *) +(* [present, model, indicator, wireFast, wireUltra, wireEffort] *) +(* and indicator is "on", "off" or "unobserved" (the footer speed glyph at *) +(* submit time; fx ask has no footer). *) +(* *) +(* orderFree marks the early-submit race: the prompt and the catalog land *) +(* together, so either interleaving may explain the observation. *) +(* *) +(* Observations are replayed in order. The index k advances only when the *) +(* machine has finished a scenario in exactly the observed way. The run is *) +(* ACCEPTED when TLC violates NotAllMatched, which is reachable only after *) +(* every observation matched. A completed search means REJECTED. *) +(***************************************************************************) +EXTENDS LaunchSelection, LaunchObserved, Sequences + +VARIABLE k +traceVars == <> + +Starts(o) == + { Fresh([o.sc EXCEPT !.early = e]) : e \in (IF o.orderFree THEN BOOLEAN ELSE {o.sc.early}) } + +IndicatorMatches(r, i) == + i = "unobserved" \/ ((r.claimedFast \/ r.claimedUltra) <=> (i = "on")) + +ReqMatches(r, o) == + IF ~o.present + THEN r.model = "none" + ELSE /\ r.model = o.model + /\ IndicatorMatches(r, o.indicator) + /\ r.wireFast = o.wireFast + /\ r.wireUltra = o.wireUltra + /\ r.wireEffort = o.wireEffort + +Matches(o) == + /\ Finished + /\ st.outcome = o.outcome + /\ st.notices = o.notices + /\ ReqMatches(st.req, o.req) + +TraceInit == k = 1 /\ st \in Starts(Observed[1]) + +Step == + /\ k <= Len(Observed) + /\ (AskValidate \/ FirstFrame \/ CatalogReady \/ Send) + /\ UNCHANGED k + +Advance == + /\ k <= Len(Observed) + /\ Matches(Observed[k]) + /\ k' = k + 1 + /\ IF k + 1 <= Len(Observed) THEN st' \in Starts(Observed[k + 1]) ELSE UNCHANGED st + +TraceSpec == TraceInit /\ [][Step \/ Advance]_traceVars + +(* Sentinel: violated exactly when every observation matched. *) +NotAllMatched == k <= Len(Observed) +============================================================================= diff --git a/tests/tla/cli/check.sh b/tests/tla/cli/check.sh new file mode 100755 index 000000000..6df2bc8f5 --- /dev/null +++ b/tests/tla/cli/check.sh @@ -0,0 +1,38 @@ +#!/bin/sh +# Model-check LaunchSelection, the launch-time --model, --fast, --ultrafast, +# and --effort handling of `fx` and `fx ask`, and require each config's +# expected verdict. +# +# proposed.cfg and current-holds.cfg must pass. Each current-*.cfg shows a +# property the design without launch validation breaks, and each mutant-*.cfg +# plants a bug in the proposed design that its property must catch. The +# simulate-*.cfg configs run random behaviors in ideal and non-ideal +# conditions; SIM_RUNS sets how many (default 20000). +# +# Run the real binary through every modeled scenario and have TLC replay it: +# bun test ../drivers/cli/ +# +# Needs Java 11+ and tla2tools.jar, as ../README.md describes. +set -eu + +cd "$(dirname "$0")" +# shellcheck source=../lib/tlc.sh +. ../lib/tlc.sh + +sim="-simulate num=${SIM_RUNS:-20000} -depth 20 -seed 1" +tlc_verdicts "$@" < m, legacy |-> m, listed |-> ModesCsv,`, + to: `[current |-> m, legacy |-> m, listed |-> "code,ask",`, + expect: "ListsExactlyCliModes", + }, + { + id: "extra-option-field", + note: "option values carry a field outside ACP's schema", + from: `names |-> NamesCsv, schemaOk |-> TRUE]`, + to: `names |-> NamesCsv, schemaOk |-> FALSE]`, + expect: "SchemaClean", + }, + { + id: "legacy-modes-stale", + note: "the older modes field shows the default instead of the session's mode", + from: `[current |-> m, legacy |-> m,`, + to: `[current |-> m, legacy |-> DefaultMode,`, + expect: "ReportsEnforcedMode", + }, + { + id: "resume-ignores-profile", + note: "a resumed session starts in the default mode", + from: `LET resumed == Eff(profile) IN`, + to: `LET resumed == DefaultMode IN`, + expect: "SessionsStartFromProfile", + }, + { + id: "fresh-ignores-profile", + note: "a new process starts sessions in the default mode", + from: `LET started == Eff(profile) IN`, + to: `LET started == DefaultMode IN`, + expect: "SessionsStartFromProfile", + }, + { + id: "default-ask", + note: "an unset profile means Ask instead of Auto", + from: `Eff(p) == IF p = "unset" THEN DefaultMode ELSE p`, + to: `Eff(p) == IF p = "unset" THEN "ask" ELSE p`, + expect: "DefaultIsAuto", + }, + { + id: "unknown-accepted", + note: "set_config_option answers success for an unknown mode (an earlier fx)", + from: `ELSE /\\ last' = Obs("set", v, FALSE, FALSE, NoView, "none", profile)`, + to: `ELSE /\\ last' = Obs("set", v, TRUE, FALSE, NoView, "none", profile)`, + expect: "UnknownRejected", + }, + { + id: "config-change-not-saved", + note: "a set_config_option change is not saved to the profile (an earlier fx)", + from: `/\\ profile' = v\n /\\ last' = Obs("set"`, + to: `/\\ profile' = profile\n /\\ last' = Obs("set"`, + expect: "ChangeIsSaved", + }, + { + id: "legacy-change-not-saved", + note: "a session/set_mode change is not saved to the profile (an earlier fx)", + from: `/\\ profile' = v\n /\\ last' = Obs("legacy"`, + to: `/\\ profile' = profile\n /\\ last' = Obs("legacy"`, + expect: "ChangeIsSaved", + }, + { + id: "stored-misread", + note: "the profile's saved mode differs from what the session uses", + from: `Enforce(cur), profile)`, + to: `Enforce(cur), "unset")`, + expect: "StoredIsProfile", + }, + { + id: "implicit-full-access", + note: "a prompt leaves the session in full access without the user choosing it", + from: `/\\ UNCHANGED <>`, + to: `/\\ cur' = "full-access"\n /\\ UNCHANGED profile`, + expect: "FullAccessOnlyByChoice", + }, + { + id: "status-shows-open-session", + note: "fx status reports the open session's mode instead of the next session's", + from: `StatusView(Eff(profile))`, + to: `StatusView(cur)`, + expect: "StatusMatchesNextSession", + }, + { + id: "new-session-stale", + note: "session/new keeps the process's mode instead of reading the saved one (the spare-process bug)", + from: `LET opened == Eff(profile) IN`, + to: `LET opened == cur IN`, + expect: "SessionsStartFromProfile", + }, + { + id: "other-process-leaks", + note: "another process saving a mode switches the open session", + from: `/\\ UNCHANGED <>`, + to: `/\\ cur' = v\n /\\ UNCHANGED saved`, + expect: "OpenSessionKeepsMode", + }, + { + id: "full-access-reviewed", + note: "full access still sends actions to the automatic reviewer", + from: `[] m = "full-access" -> "direct/ran"`, + to: `[] m = "full-access" -> "reviewed/ran"`, + expect: "PromptEnforcesMode", + }, + { + id: "rejection-changes-mode", + note: "a rejected change still switches the session", + from: `ELSE /\\ last' = Obs("set", v, FALSE, FALSE, NoView, "none", profile)\n /\\ UNCHANGED <>`, + to: `ELSE /\\ last' = Obs("set", v, FALSE, FALSE, NoView, "none", profile)\n /\\ cur' = "ask"\n /\\ UNCHANGED <>`, + expect: "RejectedChangesNothing", + }, +]; + +const SPEC_FILES = ["AcpPermissionModes.tla", "MCAcpPermissionModes.tla", "MCAcpPermissionModes.cfg"]; +const ACTION_PROPERTIES = new Set(["RejectedChangesNothing", "OpenSessionKeepsMode", "FullAccessOnlyByChoice"]); + +/// Checks a mutant against its target property alone, so a kill shows that +/// property catches the mistake regardless of which one TLC checks first. +function targetCfg(target: string): string { + return [ + "CONSTANTS", + " Profiles <- MCProfiles", + " Values <- MCValues", + "INIT Init", + "NEXT Next", + `${ACTION_PROPERTIES.has(target) ? "PROPERTY" : "INVARIANT"} ${target}`, + "CHECK_DEADLOCK FALSE", + "", + ].join("\n"); +} + +async function main() { + const tool = tlcToolchain(); + const reportDir = outDir("acp-permission-modes-spec"); + mkdirSync(reportDir, { recursive: true }); + + const base = await runTlc(join(reportDir, "base"), "MCAcpPermissionModes.tla", "MCAcpPermissionModes.cfg", SPEC_FILES); + const basePassed = base.exitCode === 0 && /No error has been found/.test(base.output); + console.log(`base spec: ${basePassed ? "PASS" : "FAIL"} (exit ${base.exitCode}, ${base.distinctStates} distinct states, depth ${base.depth})`); + + const source = readFileSync(join(SPEC_DIR, "AcpPermissionModes.tla"), "utf8"); + const mutants = []; + for (const mutant of MUTANTS) { + const count = source.split(mutant.from).length - 1; + if (count !== 1) throw new Error(`mutant ${mutant.id}: pattern matched ${count} times`); + const dir = join(reportDir, "mutants", mutant.id); + mkdirSync(dir, { recursive: true }); + writeFileSync(join(dir, "AcpPermissionModes.tla"), source.replace(mutant.from, mutant.to)); + writeFileSync(join(dir, "Target.cfg"), targetCfg(mutant.expect)); + const run = await runTlc(dir, "MCAcpPermissionModes.tla", "Target.cfg", ["MCAcpPermissionModes.tla"]); + const killed = run.exitCode !== 0 && run.violated === mutant.expect; + console.log(`mutant ${mutant.id}: ${killed ? "KILLED" : "SURVIVED"} (exit ${run.exitCode}, violated ${run.violated ?? "none"}, expected ${mutant.expect})`); + mutants.push({ ...mutant, exitCode: run.exitCode, violated: run.violated, killed }); + } + + const summary = { + toolchain: tool, + spec_sha256: Object.fromEntries(SPEC_FILES.map((name) => [name, sha256File(join(SPEC_DIR, name))])), + base: { passed: basePassed, exitCode: base.exitCode, distinctStates: base.distinctStates, depth: base.depth, argv: base.argv }, + mutants, + allKilled: mutants.every((mutant) => mutant.killed), + }; + writeJson(join(reportDir, "summary.json"), summary); + console.log(`mutants killed: ${mutants.filter((mutant) => mutant.killed).length}/${mutants.length}`); + console.log(`report: ${reportDir}`); + if (!basePassed || !summary.allKilled) process.exit(1); +} + +await main(); diff --git a/tests/tla/drivers/acp/permission_modes/driver.ts b/tests/tla/drivers/acp/permission_modes/driver.ts new file mode 100644 index 000000000..aa8f585b2 --- /dev/null +++ b/tests/tla/drivers/acp/permission_modes/driver.ts @@ -0,0 +1,331 @@ +// Runtime driver: runs the real `fx acp` binary from a worktree through +// directed and seeded-random permission-mode plans, records what a client +// observes (mode option and older modes field, JSON-RPC errors, the +// profile's saved mode, and how each prompt's shell call was enforced), and +// asks TLC whether each observed run is a behavior of +// tests/tla/acp/AcpPermissionModes.tla. +// +// bun tests/tla/drivers/acp/permission_modes/driver.ts --label main # from the repository root, after zig build +// +// No model calls: completions and reviewer answers come from the fake +// Gateway in tests/e2e/tmux-helpers.ts. --worktree runs another checkout's build. +import { existsSync, mkdirSync, writeFileSync } from "node:fs"; +import { join, resolve } from "node:path"; +import { Fixture, NO_VIEW, type Observation, loadHelpers, viewOf } from "./harness"; +import { REPO_ROOT, outDir } from "../../lib/tlc"; +import { sha256File, sha256Text, tlcToolchain, utcStamp, writeJson } from "./tlc"; +import { validate } from "./trace"; + +// ------------------------------------------------------------------ plans -- + +const MODES = ["auto", "ask", "full-access"]; +const UNKNOWN = ["code", "yolo"]; +const PROFILES = ["unset", ...MODES]; + +type PlanOp = + | { op: "set" | "legacy" | "other"; value: string } + | { op: "prompt" } + | { op: "resume" } + | { op: "fresh" } + | { op: "new" } + | { op: "status" }; + +type Plan = { name: string; profile: string; ops: PlanOp[] }; + +const set = (value: string): PlanOp => ({ op: "set", value }); +const legacy = (value: string): PlanOp => ({ op: "legacy", value }); +const other = (value: string): PlanOp => ({ op: "other", value }); +const P: PlanOp = { op: "prompt" }; +const R: PlanOp = { op: "resume" }; +const F: PlanOp = { op: "fresh" }; +const N: PlanOp = { op: "new" }; +const S: PlanOp = { op: "status" }; + +const DIRECTED: Plan[] = [ + { name: "d1-unset-is-auto", profile: "unset", + ops: [P, set("ask"), P, set("full-access"), P, set("auto"), P, R, P] }, + { name: "d2-profile-ask", profile: "ask", + ops: [P, F, legacy("full-access"), P, F, P, R, set("auto"), F, P] }, + { name: "d3-unknown-rejected", profile: "auto", + ops: [set("code"), legacy("code"), set("yolo"), legacy("yolo"), P, set("ask"), set("code"), P] }, + { name: "d4-profile-full-access", profile: "full-access", + ops: [P, set("ask"), P, R, P, F, P] }, + { name: "d5-legacy-only", profile: "unset", + ops: [legacy("ask"), P, legacy("auto"), P, legacy("full-access"), P, R, P, F] }, + // A warm process (like fx-plus's spare) must not start new sessions in a + // mode another process has since replaced. + { name: "d6-other-process", profile: "full-access", + ops: [P, other("ask"), P, N, P, other("full-access"), P, R, P, set("auto"), N, P] }, + // fx status reports the next session's mode, which an open session may not share. + { name: "d7-status", profile: "unset", + ops: [S, set("full-access"), S, other("ask"), S, P, N, S, legacy("auto"), F, S] }, +]; + +function mulberry32(seed: number) { + let a = seed >>> 0; + return () => { + a = (a + 0x6d2b79f5) >>> 0; + let t = a; + t = Math.imul(t ^ (t >>> 15), t | 1); + t ^= t + Math.imul(t ^ (t >>> 7), t | 61); + return ((t ^ (t >>> 14)) >>> 0) / 4294967296; + }; +} + +function randomPlans(count: number, steps: number, seed: number): Plan[] { + const rand = mulberry32(seed); + const pick = (items: T[]): T => items[Math.floor(rand() * items.length)]!; + const weighted: Array<() => PlanOp> = [ + () => set(pick(MODES)), () => set(pick(MODES)), () => set(pick(MODES)), () => set(pick(UNKNOWN)), + () => legacy(pick(MODES)), () => legacy(pick(MODES)), () => legacy(pick(UNKNOWN)), + () => other(pick(MODES)), () => N, () => S, + () => P, () => P, () => P, () => R, () => F, + ]; + // fx saves a chat at its first turn, so resume only follows a prompt in + // the current session (an explicit assumption in the spec). + return Array.from({ length: count }, (_, index) => { + const name = `r${String(index + 1).padStart(2, "0")}-seed${seed}`; + const profile = pick(PROFILES); + let prompted = false; + const ops = Array.from({ length: steps }, () => { + const op = pick(weighted)(); + const chosen = op.op === "resume" && !prompted ? P : op; + if (chosen.op === "prompt") prompted = true; + if (chosen.op === "fresh" || chosen.op === "new") prompted = false; + return chosen; + }); + return { name, profile, ops }; + }); +} + +// ------------------------------------------------------------------ runner -- + +async function runPlan(plan: Plan, worktree: string, helpers: Awaited>, dir: string) { + mkdirSync(dir, { recursive: true }); + writeJson(join(dir, "plan.json"), plan); + const fixture = new Fixture(worktree, helpers, plan.profile, join(dir, "fx-trace.log")); + const observations: Observation[] = []; + let error: string | null = null; + const sessionStep = (op: string, response: any) => { + const view = response.error ? null : viewOf(response.result); + observations.push({ + op, arg: "none", ok: !response.error && view !== null, hasView: view !== null, view: view ?? NO_VIEW, + enforce: "none", stored: fixture.stored(), + detail: response.error ? { error: response.error } : view ? undefined : { result: response.result }, + }); + return response.result?.sessionId as string | undefined; + }; + try { + let acp = await fixture.start(); + let sessionId = sessionStep("new", await acp.call("session/new", { cwd: fixture.workspace, mcpServers: [] })); + if (!sessionId) throw new Error("session/new returned no session"); + + for (const step of plan.ops) { + switch (step.op) { + case "set": { + const response = await acp.call("session/set_config_option", { sessionId, configId: "mode", value: step.value }); + const view = response.error ? null : viewOf(response.result); + observations.push({ + op: "set", arg: step.value, ok: !response.error, hasView: view !== null, view: view ?? NO_VIEW, + enforce: "none", stored: fixture.stored(), detail: response.error ? { error: response.error } : undefined, + }); + break; + } + case "legacy": { + const response = await acp.call("session/set_mode", { sessionId, modeId: step.value }); + observations.push({ + op: "legacy", arg: step.value, ok: !response.error, hasView: false, view: NO_VIEW, + enforce: "none", stored: fixture.stored(), + detail: response.error ? { error: response.error } : { result: response.result ?? null }, + }); + break; + } + case "prompt": { + const probe = await fixture.probePrompt(sessionId); + observations.push({ + op: "prompt", arg: "none", ok: probe.ok, hasView: false, view: NO_VIEW, + enforce: probe.enforce, stored: fixture.stored(), detail: probe.detail, + }); + break; + } + case "resume": { + acp = await fixture.restart(); + sessionStep("resume", await acp.call("session/resume", { sessionId, cwd: fixture.workspace, mcpServers: [] })); + break; + } + case "fresh": { + acp = await fixture.restart(); + const next = sessionStep("fresh", await acp.call("session/new", { cwd: fixture.workspace, mcpServers: [] })); + if (!next) throw new Error("session/new in a fresh process returned no session"); + sessionId = next; + break; + } + case "new": { + const next = sessionStep("new", await acp.call("session/new", { cwd: fixture.workspace, mcpServers: [] })); + if (!next) throw new Error("session/new returned no session"); + sessionId = next; + break; + } + case "status": { + const status = fixture.status(); + observations.push({ + op: "status", arg: "none", ok: status.ok, hasView: status.view !== null, view: status.view ?? NO_VIEW, + enforce: "none", stored: fixture.stored(), detail: status.detail, + }); + break; + } + case "other": { + fixture.saveFromOtherProcess(step.value); + observations.push({ + op: "other", arg: step.value, ok: true, hasView: false, view: NO_VIEW, + enforce: "none", stored: fixture.stored(), + }); + break; + } + } + } + } catch (caught) { + error = caught instanceof Error ? caught.message : String(caught); + } finally { + await fixture.dispose(); + } + + writeJson(join(dir, "observations.json"), observations); + writeFileSync(join(dir, "acp.jsonl"), fixture.acpLog.map((entry) => JSON.stringify(entry)).join("\n") + "\n"); + writeFileSync(join(dir, "gateway.jsonl"), fixture.gatewayLog.map((entry) => JSON.stringify(entry)).join("\n") + "\n"); + writeJson(join(dir, "processes.json"), fixture.processes); + return { observations, processes: fixture.processes, error }; +} + +// ---------------------------------------------------------------- controls -- + +function syntheticTrace(): Observation[] { + const session = (current: string) => ({ + current, legacy: current, listed: "auto,ask,full-access", legacyListed: "auto,ask,full-access", + names: "Auto,Ask,Full access", schemaOk: true, + }); + const config = (current: string) => ({ ...session(current), legacy: "n/a", legacyListed: "n/a" }); + const quiet = { hasView: false, view: NO_VIEW }; + return [ + { op: "new", arg: "none", ok: true, hasView: true, view: session("auto"), enforce: "none", stored: "unset" }, + { op: "prompt", arg: "none", ok: true, ...quiet, enforce: "reviewed/ran", stored: "unset" }, + { op: "set", arg: "ask", ok: true, hasView: true, view: config("ask"), enforce: "none", stored: "ask" }, + { op: "prompt", arg: "none", ok: true, ...quiet, enforce: "asked/no-run", stored: "ask" }, + { op: "set", arg: "code", ok: false, ...quiet, enforce: "none", stored: "ask" }, + { op: "legacy", arg: "full-access", ok: true, ...quiet, enforce: "none", stored: "full-access" }, + { op: "prompt", arg: "none", ok: true, ...quiet, enforce: "direct/ran", stored: "full-access" }, + { op: "resume", arg: "none", ok: true, hasView: true, view: session("full-access"), enforce: "none", stored: "full-access" }, + { op: "other", arg: "ask", ok: true, ...quiet, enforce: "none", stored: "ask" }, + { op: "status", arg: "none", ok: true, hasView: true, view: config("ask"), enforce: "none", stored: "ask" }, + { op: "prompt", arg: "none", ok: true, ...quiet, enforce: "direct/ran", stored: "ask" }, + { op: "new", arg: "none", ok: true, hasView: true, view: session("ask"), enforce: "none", stored: "ask" }, + { op: "prompt", arg: "none", ok: true, ...quiet, enforce: "asked/no-run", stored: "ask" }, + ]; +} + +/// Flips the latest prompt's enforcement (or a shown mode), so a conforming +/// trace stops conforming. +function tamper(observations: Observation[]): Observation[] | null { + const copy: Observation[] = structuredClone(observations); + for (let index = copy.length - 1; index >= 0; index -= 1) { + const step = copy[index]!; + if (step.op === "prompt" && step.ok) { + step.enforce = step.enforce === "direct/ran" ? "asked/no-run" : "direct/ran"; + return copy; + } + if (step.hasView) { + step.view.current = step.view.current === "ask" ? "auto" : "ask"; + return copy; + } + } + return null; +} + +// -------------------------------------------------------------------- main -- + +function argValue(name: string): string | undefined { + const index = process.argv.indexOf(name); + return index === -1 ? undefined : process.argv[index + 1]; +} + +function git(worktree: string, ...args: string[]): string { + const result = Bun.spawnSync(["git", "-C", worktree, ...args], { stdout: "pipe", stderr: "pipe" }); + return new TextDecoder().decode(result.stdout).trim(); +} + +async function main() { + const worktree = resolve(argValue("--worktree") ?? REPO_ROOT); + const fxBin = join(worktree, "zig-out", "bin", "fx"); + if (!existsSync(fxBin)) throw new Error(`missing ${fxBin}; run zig build first`); + const label = argValue("--label") ?? "run"; + const seed = Number(argValue("--seed") ?? "20261007"); + const randomCount = Number(argValue("--random") ?? "20"); + const steps = Number(argValue("--steps") ?? "12"); + + const reportDir = outDir(`acp-permission-modes-${label}`); + mkdirSync(reportDir, { recursive: true }); + const status = git(worktree, "status", "--porcelain"); + const manifest = { + label, + worktree, + head: git(worktree, "rev-parse", "HEAD"), + dirty: status.length > 0, + status: status.split("\n").filter(Boolean), + diff_sha256: status ? sha256Text(git(worktree, "diff", "HEAD")) : null, + fx_binary_sha256: sha256File(fxBin), + toolchain: tlcToolchain(), + bun: Bun.version, + seed, + randomCount, + steps, + argv: process.argv.slice(1), + }; + writeJson(join(reportDir, "manifest.json"), manifest); + if (status) writeFileSync(join(reportDir, "worktree.diff"), git(worktree, "diff", "HEAD") + "\n"); + + const helpers = await loadHelpers(worktree); + const only = argValue("--only"); + const plans = [...DIRECTED, ...randomPlans(randomCount, steps, seed)] + .filter((plan) => !only || new RegExp(only).test(plan.name)); + const results = []; + for (const plan of plans) { + const dir = join(reportDir, "traces", plan.name); + const run = await runPlan(plan, worktree, helpers, dir); + const processFailed = run.processes.some((proc) => proc.exit !== 0); + const checked = run.error ? null : await validate(run.observations, dir, plan.profile); + const verdict = run.error ? "RUN_ERROR" : processFailed ? "PROCESS_ERROR" : checked!.verdict; + results.push({ name: plan.name, profile: plan.profile, verdict, steps: run.observations.length, error: run.error, firstDivergence: checked?.firstDivergence ?? null, processes: run.processes.map((proc) => proc.exit) }); + const divergence = checked?.firstDivergence; + const where = divergence + ? ` first divergence at step ${divergence.step}: ${JSON.stringify({ ...divergence.observation, detail: undefined })}` + : ""; + console.log(`${plan.name} [${plan.profile}]: ${verdict} (${run.observations.length} steps)${run.error ? ` ${run.error}` : where}`); + } + + // Controls show the bridge separates conforming from non-conforming runs. + const controls = []; + const synthetic = syntheticTrace(); + controls.push({ name: "synthetic-conforming", expect: "ACCEPTED", got: (await validate(synthetic, join(reportDir, "controls", "synthetic-conforming"), "unset")).verdict }); + controls.push({ name: "synthetic-tampered", expect: "REJECTED", got: (await validate(tamper(synthetic)!, join(reportDir, "controls", "synthetic-tampered"), "unset")).verdict }); + controls.push({ name: "empty-trace", expect: "TOOL_ERROR", got: (await validate([], join(reportDir, "controls", "empty-trace"), "unset")).verdict }); + const firstAccepted = results.find((result) => result.verdict === "ACCEPTED"); + if (firstAccepted) { + const observed = (await Bun.file(join(reportDir, "traces", firstAccepted.name, "observations.json")).json()) as Observation[]; + const tampered = tamper(observed); + if (tampered) { + controls.push({ name: `tampered-${firstAccepted.name}`, expect: "REJECTED", got: (await validate(tampered, join(reportDir, "controls", `tampered-${firstAccepted.name}`), firstAccepted.profile)).verdict }); + } + } + for (const control of controls) console.log(`control ${control.name}: ${control.got} (expected ${control.expect})`); + + const counts = results.reduce>((acc, result) => ({ ...acc, [result.verdict]: (acc[result.verdict] ?? 0) + 1 }), {}); + const controlsPassed = controls.every((control) => control.got === control.expect); + const summary = { manifest, counts, controlsPassed, controls, results }; + writeJson(join(reportDir, "summary.json"), summary); + console.log(`verdicts: ${JSON.stringify(counts)}; controls ${controlsPassed ? "passed" : "FAILED"}`); + console.log(`report: ${reportDir}`); + const allAccepted = results.every((result) => result.verdict === "ACCEPTED"); + process.exit(controlsPassed && allAccepted ? 0 : 1); +} + +await main(); diff --git a/tests/tla/drivers/acp/permission_modes/harness.ts b/tests/tla/drivers/acp/permission_modes/harness.ts new file mode 100644 index 000000000..7c44b4da9 --- /dev/null +++ b/tests/tla/drivers/acp/permission_modes/harness.ts @@ -0,0 +1,340 @@ +// Shared runtime bridge for the permission-mode bundle: an ACP stdio client +// that declines permission requests, an isolated fx home and fake Gateway, +// the client-visible projection of the mode option, the profile's saved +// mode, and a prompt probe that shows how fx enforced the current mode. +import { existsSync, mkdirSync, mkdtempSync, readFileSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; + +// ------------------------------------------------------------ observation -- + +/// What a client sees of the mode setting in one response. `legacy` and +/// `legacyListed` come from the older `modes` field; responses without it +/// (set_config_option) report "n/a". +export type View = { + current: string; + legacy: string; + listed: string; + legacyListed: string; + names: string; + schemaOk: boolean; +}; + +export type Observation = { + op: string; + arg: string; + ok: boolean; + hasView: boolean; + view: View; + enforce: string; + stored: string; + detail?: unknown; +}; + +export const NO_VIEW: View = { current: "", legacy: "", listed: "", legacyListed: "", names: "", schemaOk: true }; + +// The ACP schema's fields for a select value (session config options). +const VALUE_KEYS = new Set(["value", "name", "description", "_meta"]); + +function flatValues(options: unknown): any[] { + if (!Array.isArray(options)) return []; + return options.flatMap((entry: any) => (Array.isArray(entry?.options) ? entry.options : [entry])); +} + +export function viewOf(result: any): View | null { + const configOptions = result?.configOptions; + if (!Array.isArray(configOptions)) return null; + const mode = configOptions.find((option: any) => option?.id === "mode"); + if (!mode || typeof mode.currentValue !== "string") return null; + const values = flatValues(mode.options); + const modes = result?.modes; + return { + current: mode.currentValue, + legacy: modes === undefined ? "n/a" : String(modes?.currentModeId ?? "missing"), + listed: values.map((value) => String(value?.value)).join(","), + legacyListed: modes === undefined ? "n/a" : (modes?.availableModes ?? []).map((entry: any) => String(entry?.id)).join(","), + names: values.map((value) => String(value?.name)).join(","), + schemaOk: + mode.type === "select" && + mode.category === "mode" && + values.every((value) => value && Object.keys(value).every((key) => VALUE_KEYS.has(key))), + }; +} + +/// The profile's saved permission mode, in the CLI's names. +export function storedMode(home: string): string { + const path = join(home, ".fx", "settings.json"); + if (!existsSync(path)) return "unset"; + let raw: unknown; + try { + raw = JSON.parse(readFileSync(path, "utf8"))?.permission_mode; + } catch { + return "unreadable"; + } + if (raw === undefined || raw === null) return "unset"; + const value = String(raw).toLowerCase(); + if (value === "ask" || value === "auto") return value; + if (value === "yolo" || value === "full-access" || value === "full access") return "full-access"; + return `raw:${value}`; +} + +// -------------------------------------------------------------- ACP client -- + +export class Acp { + private buffer = ""; + private lines: string[] = []; + private waiters: Array<(line: string) => void> = []; + private closed = false; + private nextId = 1; + stderr = ""; + permissionRequests = 0; + readonly exited: Promise; + + constructor(readonly proc: ReturnType, private readonly log: (entry: object) => void) { + this.exited = (async () => { + const code = await proc.exited; + this.closed = true; + for (const waiter of this.waiters.splice(0)) waiter(""); + return code; + })(); + (async () => { + const decoder = new TextDecoder(); + for await (const chunk of proc.stdout as ReadableStream) { + this.buffer += decoder.decode(chunk); + const parts = this.buffer.split("\n"); + this.buffer = parts.pop() ?? ""; + for (const line of parts) { + if (!line.trim()) continue; + const waiter = this.waiters.shift(); + if (waiter) waiter(line); + else this.lines.push(line); + } + } + })(); + (async () => { + const decoder = new TextDecoder(); + for await (const chunk of proc.stderr as ReadableStream) this.stderr += decoder.decode(chunk); + })(); + } + + private async readLine(): Promise { + const buffered = this.lines.shift(); + if (buffered) return JSON.parse(buffered); + if (this.closed) throw new Error(`fx acp exited: ${this.stderr.slice(-400)}`); + const line = await new Promise((resolveLine, reject) => { + const timer = setTimeout(() => reject(new Error(`fx acp read timeout: ${this.stderr.slice(-400)}`)), 30_000); + this.waiters.push((value) => { + clearTimeout(timer); + resolveLine(value); + }); + }); + if (!line) throw new Error(`fx acp exited: ${this.stderr.slice(-400)}`); + return JSON.parse(line); + } + + private send(message: object) { + (this.proc.stdin as any).write(`${JSON.stringify(message)}\n`); + (this.proc.stdin as any).flush?.(); + } + + async call(method: string, params: Record): Promise { + const id = this.nextId++; + this.log({ dir: "out", id, method, params }); + this.send({ jsonrpc: "2.0", id, method, params }); + while (true) { + const message = await this.readLine(); + if ("method" in message && "id" in message) { + // Agent-to-client request. Permission requests are declined with the + // reject option fx offers, so an "ask" turn never runs the tool. + if (message.method === "session/request_permission") { + this.permissionRequests += 1; + const options: any[] = message.params?.options ?? []; + const reject = options.find((option) => String(option?.kind ?? "").startsWith("reject")); + this.log({ dir: "in-request", method: message.method, options: options.map((option) => option?.kind), chose: reject?.optionId ?? "cancelled" }); + this.send({ + jsonrpc: "2.0", + id: message.id, + result: { outcome: reject ? { outcome: "selected", optionId: reject.optionId } : { outcome: "cancelled" } }, + }); + } else { + this.log({ dir: "in-request", method: message.method, answered: "error" }); + this.send({ jsonrpc: "2.0", id: message.id, error: { code: -32601, message: "Method not found" } }); + } + continue; + } + if (message.id === id) { + this.log({ dir: "in", id, method, error: message.error ?? null, result: message.result ?? null }); + return message; + } + } + } + + async close(): Promise<{ exit: number; stderr: string }> { + if (!this.closed) (this.proc.stdin as any).end(); + const timer = setTimeout(() => this.proc.kill("SIGKILL"), 5_000); + const exit = await this.exited; + clearTimeout(timer); + return { exit, stderr: this.stderr }; + } +} + +// -------------------------------------------------------------- fx fixture -- + +type Helpers = { + startDynamicFakeGateway: (respond: (body: string) => Response, options: object) => any; + fakeGatewayFinalText: (text: string) => Response; + fakeShellRun: (id: string, command: string, options?: Record) => Response; +}; + +export async function loadHelpers(worktree: string): Promise { + return (await import(join(worktree, "tests", "e2e", "tmux-helpers.ts"))) as Helpers; +} + +// Process overrides that would mask what the profile and ACP decide. +const STRIPPED_ENV = [ + "VERCEL_OIDC_TOKEN", "FX_PROVIDER", "FX_MODEL", "FX_FAST", "FX_ULTRAFAST", + "FX_PERMISSION_MODE", "FX_DEBUG_RECORD", "FX_SESSIONS_V2", +]; + +/// An isolated fx home, workspace and fake Gateway for one run. `profile` is +/// the saved permission_mode the run starts from ("unset" leaves it out). +export class Fixture { + readonly root: string; + readonly home: string; + readonly workspace: string; + readonly acpLog: object[] = []; + readonly gatewayLog: object[] = []; + readonly processes: Array<{ exit: number; stderr: string }> = []; + private readonly gateway: any; + private probe: { id: string; marker: string } | null = null; + private probeCount = 0; + acp: Acp | null = null; + + constructor(private readonly worktree: string, private readonly helpers: Helpers, profile: string, traceLog?: string) { + this.root = realpathSync(mkdtempSync(join(tmpdir(), "fx-acp-modes-"))); + this.home = join(this.root, "home"); + this.workspace = join(this.root, "workspace"); + mkdirSync(join(this.home, ".fx"), { recursive: true, mode: 0o700 }); + mkdirSync(this.workspace, { recursive: true, mode: 0o700 }); + const settings: Record = { session_titles: false }; + if (profile !== "unset") settings.permission_mode = profile; + writeFileSync(join(this.home, ".fx", "settings.json"), `${JSON.stringify(settings)}\n`, { mode: 0o600 }); + + this.gateway = helpers.startDynamicFakeGateway((body: string) => { + const probe = this.probe; + const kind = !probe ? "no-probe" : body.includes(probe.id) ? "final" : "tool-call"; + this.gatewayLog.push({ n: this.gatewayLog.length + 1, probe: probe?.id ?? null, kind }); + if (probe && kind === "tool-call") return helpers.fakeShellRun(probe.id, `printf ran > ${JSON.stringify(probe.marker)}`); + return helpers.fakeGatewayFinalText("done"); + }, {}); + this.traceLog = traceLog; + } + + private traceLog?: string; + + env(): Record { + const env: Record = {}; + for (const [key, value] of Object.entries({ + ...process.env, + NO_COLOR: "1", + HOME: this.home, + AI_GATEWAY_API_KEY: "acp-modes-fake-key", + FX_DISABLE_KEYCHAIN: "1", + FX_SKIP_ONBOARDING: "1", + FX_AUTO_UPGRADE: "0", + FX_SOUND: "0", + FX_GATEWAY_BASE_URL: this.gateway.baseUrl, + FX_GATEWAY_CHAT_URL: this.gateway.chatUrl, + FX_E2E_GATEWAY_MODELS_URL: `${this.gateway.baseUrl}/coding-agent/v1/models`, + FX_E2E_GATEWAY_CHAT_URL: this.gateway.chatUrl, + ...(this.traceLog ? { FX_TRACE_LOG: this.traceLog, FX_TRACE_SCOPES: "acp,permission,host_config" } : {}), + })) { + if (value === undefined || STRIPPED_ENV.includes(key)) continue; + env[key] = value; + } + return env; + } + + async start(): Promise { + const fxBin = join(this.worktree, "zig-out", "bin", "fx"); + const processNumber = this.processes.length + 1; + this.acp = new Acp( + Bun.spawn([fxBin, "acp"], { cwd: this.workspace, env: this.env(), stdin: "pipe", stdout: "pipe", stderr: "pipe" }), + (entry) => this.acpLog.push({ process: processNumber, ...entry }), + ); + await this.acp.call("initialize", { protocolVersion: 1 }); + return this.acp; + } + + async restart(): Promise { + if (this.acp) this.processes.push(await this.acp.close()); + return this.start(); + } + + /// Runs one turn whose model asks to write a marker file with the shell + /// tool, and reports how fx handled it: "asked" (a permission request + /// reached the client), "reviewed" (fx's automatic reviewer was called), + /// or "direct", plus whether the command ran. + async probePrompt(sessionId: string): Promise<{ ok: boolean; enforce: string; detail: object }> { + const acp = this.acp!; + this.probeCount += 1; + const marker = join(this.workspace, `probe-${this.probeCount}.txt`); + this.probe = { id: `probe_call_${this.probeCount}`, marker }; + const asked0 = acp.permissionRequests; + const reviewed0 = this.gateway.classifierRequests.length + this.gateway.evaluationRequests.length; + const response = await acp.call("session/prompt", { sessionId, prompt: [{ type: "text", text: "write the probe marker" }] }); + this.probe = null; + const asked = acp.permissionRequests - asked0; + const reviewed = this.gateway.classifierRequests.length + this.gateway.evaluationRequests.length - reviewed0; + const ran = existsSync(marker); + const ok = !response.error && response.result?.stopReason === "end_turn"; + const how = asked > 0 && reviewed > 0 ? "asked+reviewed" : asked > 0 ? "asked" : reviewed > 0 ? "reviewed" : "direct"; + return { + ok, + enforce: ok ? `${how}/${ran ? "ran" : "no-run"}` : "none", + detail: { asked, reviewed, ran, stopReason: response.result?.stopReason ?? null, error: response.error ?? null }, + }; + } + + stored(): string { + return storedMode(this.home); + } + + /// Runs `fx status --json` in the workspace and projects its modes the way + /// a client would read them before a session exists. + status(): { ok: boolean; view: View | null; detail: object } { + const fxBin = join(this.worktree, "zig-out", "bin", "fx"); + const run = Bun.spawnSync([fxBin, "status", "--json"], { cwd: this.workspace, env: this.env(), stdout: "pipe", stderr: "pipe" }); + const text = new TextDecoder().decode(run.stdout).trim(); + let parsed: any = null; + try { parsed = JSON.parse(text); } catch {} + const modes: any[] | null = Array.isArray(parsed?.modes) ? parsed.modes : null; + const ok = run.exitCode === 0 && typeof parsed?.mode === "string" && modes !== null; + const statusKeys = new Set(["id", "name", "description"]); + const view: View | null = ok ? { + current: parsed.mode, + legacy: "n/a", + listed: modes!.map((mode) => String(mode?.id)).join(","), + legacyListed: "n/a", + names: modes!.map((mode) => String(mode?.name)).join(","), + schemaOk: modes!.every((mode) => typeof mode?.id === "string" && typeof mode?.name === "string" && Object.keys(mode).every((key) => statusKeys.has(key))), + } : null; + return { ok, view, detail: { exit: run.exitCode, stderr: new TextDecoder().decode(run.stderr).slice(0, 300), permission_mode: parsed?.permission_mode ?? null } }; + } + + /// Saves a mode the way another fx process would (the CLI's /permissions + /// or another ACP process): fx persists full access as "yolo". + saveFromOtherProcess(mode: string) { + const path = join(this.home, ".fx", "settings.json"); + const settings = JSON.parse(readFileSync(path, "utf8")); + settings.permission_mode = mode === "full-access" ? "yolo" : mode; + writeFileSync(path, `${JSON.stringify(settings)}\n`, { mode: 0o600 }); + } + + async dispose() { + if (this.acp) this.processes.push(await this.acp.close()); + this.acp = null; + this.gateway.stop(); + rmSync(this.root, { recursive: true, force: true }); + } +} diff --git a/tests/tla/drivers/acp/permission_modes/tlc.ts b/tests/tla/drivers/acp/permission_modes/tlc.ts new file mode 100644 index 000000000..9ccbc1c93 --- /dev/null +++ b/tests/tla/drivers/acp/permission_modes/tlc.ts @@ -0,0 +1,13 @@ +// TLC helpers for the ACP permission-mode driver: the shared runner in +// ../../lib/tlc.ts, pointed at the specs in tests/tla/acp/. +import { join } from "node:path"; +import { TLA_ROOT, runTlc as runShared } from "../../lib/tlc"; + +export { sha256File, sha256Text, tlcToolchain, utcStamp, writeJson } from "../../lib/tlc"; +export type { TlcRun } from "../../lib/tlc"; + +export const SPEC_DIR = join(TLA_ROOT, "acp"); + +export function runTlc(dir: string, module: string, cfg: string, specs: string[]) { + return runShared(dir, module, cfg, specs, SPEC_DIR); +} diff --git a/tests/tla/drivers/acp/permission_modes/trace.ts b/tests/tla/drivers/acp/permission_modes/trace.ts new file mode 100644 index 000000000..ec6e1d591 --- /dev/null +++ b/tests/tla/drivers/acp/permission_modes/trace.ts @@ -0,0 +1,76 @@ +// TLC trace validation: turns one observed run into the generated +// AcpPermissionModesObs module and asks TLC whether it is a behavior of +// tests/tla/acp/AcpPermissionModes.tla (through tests/tla/acp/AcpPermissionModesTrace.tla). +import { mkdirSync, writeFileSync } from "node:fs"; +import { join } from "node:path"; +import type { Observation } from "./harness"; +import { runTlc, sha256Text, writeJson } from "./tlc"; + +const tla = (value: string) => JSON.stringify(value); +const bool = (value: boolean) => (value ? "TRUE" : "FALSE"); + +export function obsModule(observations: Observation[], profile: string, values: string[]): string { + const record = (o: Observation) => { + const v = o.view; + const view = `[current |-> ${tla(v.current)}, legacy |-> ${tla(v.legacy)}, listed |-> ${tla(v.listed)}, legacyListed |-> ${tla(v.legacyListed)}, names |-> ${tla(v.names)}, schemaOk |-> ${bool(v.schemaOk)}]`; + return `[op |-> ${tla(o.op)}, arg |-> ${tla(o.arg)}, ok |-> ${bool(o.ok)}, hasView |-> ${bool(o.hasView)}, view |-> ${view}, enforce |-> ${tla(o.enforce)}, stored |-> ${tla(o.stored)}]`; + }; + return [ + "--------------------- MODULE AcpPermissionModesObs ---------------------", + "(* Generated from one observed fx acp run. *)", + `TProfiles == {${tla(profile)}}`, + `TValues == {${[...new Set(values)].map(tla).join(", ")}}`, + "TraceLog == <<", + observations.map((o) => ` ${record(o)}`).join(",\n"), + ">>", + "=============================================================================", + "", + ].join("\n"); +} + +const TRACE_CFG = [ + "CONSTANTS", + " Profiles <- TProfiles", + " Values <- TValues", + "INIT TraceInit", + "NEXT TraceNext", + "INVARIANT NotDone", + "CHECK_DEADLOCK FALSE", + "", +].join("\n"); + +export type Verdict = "ACCEPTED" | "REJECTED" | "TOOL_ERROR"; + +export async function validate(observations: Observation[], dir: string, profile: string) { + mkdirSync(dir, { recursive: true }); + if (observations.length === 0) return { verdict: "TOOL_ERROR" as Verdict, reason: "empty trace", matched: 0, firstDivergence: null }; + const values = ["auto", "ask", "full-access", ...observations.filter((o) => o.op === "set" || o.op === "legacy").map((o) => o.arg)]; + const obs = obsModule(observations, profile, values); + writeFileSync(join(dir, "AcpPermissionModesObs.tla"), obs); + writeFileSync(join(dir, "AcpPermissionModesTrace.cfg"), TRACE_CFG); + const run = await runTlc(dir, "AcpPermissionModesTrace.tla", "AcpPermissionModesTrace.cfg", ["AcpPermissionModes.tla", "AcpPermissionModesTrace.tla"]); + const finalIndex = [...run.output.matchAll(/\/\\ i = (\d+)/g)].map((match) => Number(match[1])).at(-1) ?? null; + let verdict: Verdict; + let matched: number; + if (run.exitCode === 12 && run.violated === "NotDone" && finalIndex === observations.length) { + verdict = "ACCEPTED"; + matched = observations.length; + } else if (run.exitCode === 0 && /No error has been found/.test(run.output)) { + verdict = "REJECTED"; + // The trace's states are i = 1..k, so the search depth is how many steps matched. + matched = run.distinctStates === 0 ? 0 : run.depth ?? 0; + } else { + verdict = "TOOL_ERROR"; + matched = 0; + } + const result = { + verdict, + matched, + length: observations.length, + firstDivergence: verdict === "REJECTED" ? { step: matched + 1, observation: observations[matched] ?? null } : null, + tlc: { exitCode: run.exitCode, violated: run.violated, finalIndex, depth: run.depth, durationMs: run.durationMs }, + obs_sha256: sha256Text(obs), + }; + writeJson(join(dir, "verdict.json"), result); + return result; +} diff --git a/tests/tla/drivers/acp/speed/check-spec.ts b/tests/tla/drivers/acp/speed/check-spec.ts new file mode 100644 index 000000000..13f3b286b --- /dev/null +++ b/tests/tla/drivers/acp/speed/check-spec.ts @@ -0,0 +1,115 @@ +// Exhaustive TLC check of the speed contract plus mutation qualification: +// each planted mutant must violate the named invariant, which shows the +// invariants are not vacuous. Several mutants match how an earlier fx behaved. +// +// bun tests/tla/drivers/acp/speed/check-spec.ts +import { mkdirSync, readFileSync, writeFileSync } from "node:fs"; +import { join } from "node:path"; +import { outDir } from "../../lib/tlc"; +import { SPEC_DIR, runTlc, sha256File, tlcToolchain, utcStamp, writeJson } from "./tlc"; + +type Mutant = { id: string; note: string; from: string; to: string; expect: string }; + +const MUTANTS: Mutant[] = [ + { + id: "fast-ignored", + note: "an earlier fx: set fast succeeds but changes nothing", + from: " ELSE /\\ fast' = b\n /\\ ultra' = (ultra /\\ ~b)", + to: " ELSE /\\ fast' = fast\n /\\ ultra' = ultra", + expect: "RequestHonored", + }, + { + id: "unknown-accepted", + note: "an earlier fx: unknown config ids succeed", + from: 'Result("unknown", "none", FALSE, "none")', + to: 'Result("unknown", "none", TRUE, "none")', + expect: "UnknownRejected", + }, + { + id: "switch-keeps-ultra", + note: "an earlier fx: Ultrafast stays on, hidden, after switching to a model without it", + from: " /\\ ultra' = (ultra /\\ m \\in SupUltra)", + to: " /\\ ultra' = ultra", + expect: "UltraValid", + }, + { + id: "switch-keeps-fast", + note: "an earlier fx: Fast stays on, hidden, after switching to a model without it", + from: " /\\ fast' = (fast /\\ m \\in SupFast)", + to: " /\\ fast' = fast", + expect: "SwitchClearsFast", + }, + { + id: "fast-not-exclusive", + note: "enabling Fast leaves Ultrafast on", + from: " /\\ ultra' = (ultra /\\ ~b)", + to: " /\\ ultra' = ultra", + expect: "Exclusive", + }, + { + id: "ultra-not-exclusive", + note: "enabling Ultrafast leaves Fast on", + from: " /\\ fast' = (fast /\\ ~b)", + to: " /\\ fast' = fast", + expect: "Exclusive", + }, + { + id: "fast-unsupported-accepted", + note: "Fast can be enabled on a model without it", + from: " IF b /\\ model \\notin SupFast", + to: " IF FALSE", + expect: "AcceptOnlySupported", + }, + { + id: "fast-disable-rejected", + note: "turning Fast off is rejected on a model without it", + from: " IF b /\\ model \\notin SupFast", + to: " IF model \\notin SupFast", + expect: "RejectOnlyUnsupported", + }, + { + id: "prompt-hidden-fast", + note: "a prompt sends Fast for a model without it", + from: "ELSE IF fast /\\ model \\in SupFast THEN \"fast\"", + to: "ELSE IF fast THEN \"fast\"", + expect: "PromptLaneSupported", + }, +]; + +async function main() { + const tool = tlcToolchain(); + const reportDir = outDir("acp-speed-spec"); + mkdirSync(reportDir, { recursive: true }); + const specFiles = ["AcpSpeed.tla", "MCAcpSpeed.tla", "MCAcpSpeed.cfg"]; + + const base = await runTlc(join(reportDir, "base"), "MCAcpSpeed.tla", "MCAcpSpeed.cfg", specFiles); + const basePassed = base.exitCode === 0 && /No error has been found/.test(base.output); + console.log(`base spec: ${basePassed ? "PASS" : "FAIL"} (exit ${base.exitCode}, ${base.distinctStates} distinct states, depth ${base.depth})`); + + const source = readFileSync(join(SPEC_DIR, "AcpSpeed.tla"), "utf8"); + const mutants = []; + for (const mutant of MUTANTS) { + const count = source.split(mutant.from).length - 1; + if (count !== 1) throw new Error(`mutant ${mutant.id}: pattern matched ${count} times`); + const dir = join(reportDir, "mutants", mutant.id); + mkdirSync(dir, { recursive: true }); + writeFileSync(join(dir, "AcpSpeed.tla"), source.replace(mutant.from, mutant.to)); + const mutated = await runTlc(dir, "MCAcpSpeed.tla", "MCAcpSpeed.cfg", ["MCAcpSpeed.tla", "MCAcpSpeed.cfg"]); + const killed = mutated.exitCode === 12 && mutated.violated === mutant.expect; + console.log(`mutant ${mutant.id}: ${killed ? "KILLED" : "SURVIVED"} (exit ${mutated.exitCode}, violated ${mutated.violated ?? "none"}, expected ${mutant.expect})`); + mutants.push({ ...mutant, exitCode: mutated.exitCode, violated: mutated.violated, killed }); + } + + const summary = { + toolchain: tool, + spec_sha256: Object.fromEntries(specFiles.map((name) => [name, sha256File(join(SPEC_DIR, name))])), + base: { passed: basePassed, exitCode: base.exitCode, distinctStates: base.distinctStates, depth: base.depth, argv: base.argv }, + mutants, + allKilled: mutants.every((mutant) => mutant.killed), + }; + writeJson(join(reportDir, "summary.json"), summary); + console.log(`report: ${reportDir}`); + if (!basePassed || !summary.allKilled) process.exit(1); +} + +await main(); diff --git a/tests/tla/drivers/acp/speed/driver.ts b/tests/tla/drivers/acp/speed/driver.ts new file mode 100644 index 000000000..68407cc3a --- /dev/null +++ b/tests/tla/drivers/acp/speed/driver.ts @@ -0,0 +1,370 @@ +// Runtime driver: drives the real `fx acp` binary from a worktree through +// directed and seeded-random speed scenarios, records what a client observes +// (configOptions projections, JSON-RPC errors, and the lane each prompt sends +// to a local fake Gateway), and asks TLC whether each observed run is a +// behavior of tests/tla/acp/AcpSpeed.tla (trace validation via tests/tla/acp/AcpSpeedTrace.tla). +// +// bun tests/tla/drivers/acp/speed/driver.ts --label main # from the repository root, after zig build +// +// No live model calls: completions come from the fake Gateway in the +// worktree's own tests/e2e/tmux-helpers.ts. +import { existsSync, mkdirSync, mkdtempSync, realpathSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join, resolve } from "node:path"; +import { REPO_ROOT, outDir } from "../../lib/tlc"; +import { sha256File, sha256Text, tlcToolchain, utcStamp, writeJson } from "./tlc"; +import { Acp, NO_VIEW, type Observation, type View, laneOf, validate, viewOf } from "./trace"; + +// ---------------------------------------------------------------- catalog -- + +const BOTH = "openai/gpt-6-astra"; // Fast (priority tier) and Ultrafast +const FAST_ONLY = "openai/gpt-5.6-priority"; // Fast only +const PLAIN = "anthropic/claude-plain"; // neither +const MODELS = [BOTH, FAST_ONLY, PLAIN]; +const SUP_FAST = [BOTH, FAST_ONLY]; +const SUP_ULTRA = [BOTH]; +const TRACE_CATALOG = { models: MODELS, supFast: SUP_FAST, supUltra: SUP_ULTRA }; + +const CATALOG = [ + { + id: BOTH, name: "GPT-6 Astra", type: "language", owned_by: "openai", tags: ["tool-use", "reasoning"], + reasoning_options: [{ type: "effort", values: ["high", "xhigh"] }], + pricing: { + input_cache_read: "0.000001", + service_tiers: { + priority: { input: "0.00003", output: "0.00015", input_cache_read: "0.000003" }, + ultrafast: { input: "0.00006", output: "0.0003", input_cache_read: "0.000006" }, + }, + }, + }, + { + id: FAST_ONLY, name: "GPT-5.6 Priority", type: "language", owned_by: "openai", tags: ["tool-use"], + pricing: { service_tiers: { priority: { input: "0.00003", output: "0.00015" } } }, + }, + { id: PLAIN, name: "Claude Plain", type: "language", owned_by: "anthropic", tags: ["tool-use"] }, +]; + +// ------------------------------------------------------------------ plans -- + +type PlanOp = + | { op: "fast" | "ultrafast"; value: boolean } + | { op: "model"; model: string } + | { op: "unknown" } + | { op: "prompt" } + | { op: "resume" }; + +type Plan = { name: string; initialModel: string; defaultFast: boolean; ops: PlanOp[] }; + +const on = (op: "fast" | "ultrafast"): PlanOp => ({ op, value: true }); +const off = (op: "fast" | "ultrafast"): PlanOp => ({ op, value: false }); +const to = (model: string): PlanOp => ({ op: "model", model }); +const P: PlanOp = { op: "prompt" }; +const R: PlanOp = { op: "resume" }; +const U: PlanOp = { op: "unknown" }; + +const DIRECTED: Plan[] = [ + { name: "d1-lanes-exclusive", initialModel: BOTH, defaultFast: false, + ops: [P, on("fast"), P, on("ultrafast"), P, on("fast"), P, off("fast"), P, U, R, P] }, + { name: "d2-switch-drops-ultrafast", initialModel: BOTH, defaultFast: false, + ops: [on("ultrafast"), to(PLAIN), P, to(BOTH), P, on("ultrafast"), R, P, to(FAST_ONLY), P] }, + { name: "d3-fast-only-model", initialModel: FAST_ONLY, defaultFast: true, + ops: [P, on("ultrafast"), off("fast"), P, on("fast"), to(PLAIN), P, to(FAST_ONLY), P, R, P] }, + { name: "d4-plain-model", initialModel: PLAIN, defaultFast: true, + ops: [P, on("fast"), on("ultrafast"), off("fast"), off("ultrafast"), to(FAST_ONLY), P, R, P] }, + { name: "d5-hidden-default-fast", initialModel: PLAIN, defaultFast: true, + ops: [P, to(BOTH), P, R, P, on("ultrafast"), to(FAST_ONLY), P] }, +]; + +function mulberry32(seed: number) { + let a = seed >>> 0; + return () => { + a = (a + 0x6d2b79f5) >>> 0; + let t = a; + t = Math.imul(t ^ (t >>> 15), t | 1); + t ^= t + Math.imul(t ^ (t >>> 7), t | 61); + return ((t ^ (t >>> 14)) >>> 0) / 4294967296; + }; +} + +function randomPlans(count: number, steps: number, seed: number): Plan[] { + const rand = mulberry32(seed); + const pick = (items: T[]): T => items[Math.floor(rand() * items.length)]!; + const weighted: Array<() => PlanOp> = [ + () => on("fast"), () => off("fast"), () => on("fast"), + () => on("ultrafast"), () => off("ultrafast"), () => on("ultrafast"), + () => to(pick(MODELS)), () => to(pick(MODELS)), () => to(pick(MODELS)), + () => P, () => P, () => U, () => R, + ]; + // The v2 session store saves a chat at its first turn, so resuming earlier + // fails with "Session not found" on main too. Resume therefore only follows + // a prompt (an explicit assumption in tests/tla/acp/AcpSpeed.tla). + return Array.from({ length: count }, (_, index) => { + const name = `r${String(index + 1).padStart(2, "0")}-seed${seed}`; + const initialModel = pick(MODELS); + const defaultFast = rand() < 0.5; + let prompted = false; + const ops = Array.from({ length: steps }, () => { + const op = pick(weighted)(); + const chosen = op.op === "resume" && !prompted ? P : op; + if (chosen.op === "prompt") prompted = true; + return chosen; + }); + return { name, initialModel, defaultFast, ops }; + }); +} + +// ------------------------------------------------------------------ runner -- + +type Helpers = { + startDynamicFakeGateway: (respond: (body: string) => Response, options: object) => any; + fakeGatewayFinalText: (text: string) => Response; +}; + +async function runPlan(plan: Plan, worktree: string, helpers: Helpers, dir: string) { + mkdirSync(dir, { recursive: true }); + writeJson(join(dir, "plan.json"), plan); + const fxBin = join(worktree, "zig-out", "bin", "fx"); + const root = realpathSync(mkdtempSync(join(tmpdir(), "fx-acp-speed-"))); + const home = join(root, "home"); + const workspace = join(root, "workspace"); + mkdirSync(join(home, ".fx"), { recursive: true, mode: 0o700 }); + mkdirSync(workspace, { recursive: true, mode: 0o700 }); + writeFileSync( + join(home, ".fx", "settings.json"), + `${JSON.stringify({ session_titles: false, fast_mode: plan.defaultFast, models: { gateway: plan.initialModel } })}\n`, + { mode: 0o600 }, + ); + + const acpLog: object[] = []; + const gatewayLog: object[] = []; + let completions: string[] = []; + const gateway = helpers.startDynamicFakeGateway((body: string) => { + completions.push(body); + gatewayLog.push({ n: gatewayLog.length + 1, lane: laneOf(body), model: (() => { try { return JSON.parse(body).model; } catch { return null; } })() }); + return helpers.fakeGatewayFinalText(`reply ${gatewayLog.length}`); + }, { models: () => CATALOG }); + + const env: Record = {}; + for (const [key, value] of Object.entries({ + ...process.env, + NO_COLOR: "1", + HOME: home, + AI_GATEWAY_API_KEY: "acp-speed-fake-key", + FX_DISABLE_KEYCHAIN: "1", + FX_SKIP_ONBOARDING: "1", + FX_AUTO_UPGRADE: "0", + FX_SOUND: "0", + FX_GATEWAY_BASE_URL: gateway.baseUrl, + FX_GATEWAY_CHAT_URL: gateway.chatUrl, + FX_E2E_GATEWAY_MODELS_URL: `${gateway.baseUrl}/coding-agent/v1/models`, + FX_E2E_GATEWAY_CHAT_URL: gateway.chatUrl, + FX_TRACE_LOG: join(dir, "fx-trace.log"), + FX_TRACE_SCOPES: "acp,catalog", + })) { + if (value === undefined) continue; + // FX_PROVIDER and FX_MODEL are process overrides: fx then resumes every + // chat on the process's model instead of the chat's saved one, which no + // real ACP host (fx-plus included) does. The Gateway is already the default. + if (["VERCEL_OIDC_TOKEN", "FX_PROVIDER", "FX_MODEL", "FX_FAST", "FX_ULTRAFAST", "FX_SESSIONS_V2", "FX_PERMISSION_MODE", "FX_DEBUG_RECORD"].includes(key)) continue; + env[key] = value; + } + if (SESSIONS_V2 !== undefined) env.FX_SESSIONS_V2 = SESSIONS_V2; + + const processes: Array<{ exit: number; stderr: string }> = []; + const spawn = () => new Acp( + Bun.spawn([fxBin, "acp"], { cwd: workspace, env, stdin: "pipe", stdout: "pipe", stderr: "pipe" }), + (entry) => acpLog.push({ process: processes.length + 1, ...entry }), + ); + const observations: Observation[] = []; + let acp = spawn(); + let error: string | null = null; + try { + await acp.call("initialize", { protocolVersion: 1 }); + const created = await acp.call("session/new", { cwd: workspace, mcpServers: [] }); + const sessionId = created.result?.sessionId as string | undefined; + const view = viewOf(created.result?.configOptions); + if (!sessionId || !view) throw new Error(`session/new failed: ${JSON.stringify(created.error ?? created.result)}`); + observations.push({ op: "new", arg: "none", ok: true, speed: "none", hasView: true, view }); + + const configStep = async (op: string, arg: string, configId: string, value: string) => { + const response = await acp.call("session/set_config_option", { sessionId, configId, value }); + const stepView = response.error ? null : viewOf(response.result?.configOptions); + observations.push({ + op, arg, ok: !response.error, speed: "none", + hasView: stepView !== null, view: stepView ?? NO_VIEW, + detail: response.error ? { error: response.error } : undefined, + }); + }; + + for (const step of plan.ops) { + switch (step.op) { + case "fast": + case "ultrafast": + await configStep(step.op, String(step.value), step.op, String(step.value)); + break; + case "model": + await configStep("model", step.model, "model", step.model); + break; + case "unknown": + await configStep("unknown", "none", "turbo", "on"); + break; + case "prompt": { + completions = []; + const response = await acp.call("session/prompt", { sessionId, prompt: [{ type: "text", text: "speed check" }] }); + const ok = !response.error && response.result?.stopReason === "end_turn"; + const lanes = completions.map(laneOf); + const speed = !ok ? "none" : lanes.length === 1 ? lanes[0]! : `requests:${lanes.join(",") || "0"}`; + observations.push({ + op: "prompt", arg: "none", ok, speed, hasView: false, view: NO_VIEW, + detail: { lanes, error: response.error ?? null, stopReason: response.result?.stopReason ?? null }, + }); + break; + } + case "resume": { + processes.push(await acp.close()); + acp = spawn(); + await acp.call("initialize", { protocolVersion: 1 }); + const resumed = await acp.call("session/resume", { sessionId, cwd: workspace, mcpServers: [] }); + const resumedView = resumed.error ? null : viewOf(resumed.result?.configOptions); + observations.push({ + op: "resume", arg: "none", ok: !resumed.error, speed: "none", + hasView: resumedView !== null, view: resumedView ?? NO_VIEW, + detail: resumed.error ? { error: resumed.error } : undefined, + }); + break; + } + } + } + } catch (caught) { + error = caught instanceof Error ? caught.message : String(caught); + } finally { + processes.push(await acp.close()); + gateway.stop(); + rmSync(root, { recursive: true, force: true }); + } + + writeJson(join(dir, "observations.json"), observations); + writeFileSync(join(dir, "acp.jsonl"), acpLog.map((entry) => JSON.stringify(entry)).join("\n") + "\n"); + writeFileSync(join(dir, "gateway.jsonl"), gatewayLog.map((entry) => JSON.stringify(entry)).join("\n") + "\n"); + writeJson(join(dir, "processes.json"), processes); + return { observations, processes, error }; +} + +// ---------------------------------------------------------------- controls -- + +function syntheticTrace(): Observation[] { + const v = (fast: string, ultra: string): View => ({ model: BOTH, fast, ultra }); + return [ + { op: "new", arg: "none", ok: true, speed: "none", hasView: true, view: v("false", "false") }, + { op: "fast", arg: "true", ok: true, speed: "none", hasView: true, view: v("true", "false") }, + { op: "prompt", arg: "none", ok: true, speed: "fast", hasView: false, view: NO_VIEW }, + { op: "ultrafast", arg: "true", ok: true, speed: "none", hasView: true, view: v("false", "true") }, + { op: "prompt", arg: "none", ok: true, speed: "ultrafast", hasView: false, view: NO_VIEW }, + ]; +} + +function tamper(observations: Observation[]): Observation[] | null { + const copy: Observation[] = structuredClone(observations); + for (let index = copy.length - 1; index >= 0; index -= 1) { + const step = copy[index]!; + if (step.op === "prompt" && step.ok) { + step.speed = step.speed === "fast" ? "standard" : "fast"; + return copy; + } + if (step.hasView && step.view.fast !== "absent") { + step.view.fast = step.view.fast === "true" ? "false" : "true"; + return copy; + } + } + return null; +} + +// -------------------------------------------------------------------- main -- + +function argValue(name: string): string | undefined { + const index = process.argv.indexOf(name); + return index === -1 ? undefined : process.argv[index + 1]; +} + +// Session store backend under test ("0" = v1 event log, "1" = v2); unset uses fx's default. +const SESSIONS_V2 = argValue("--sessions-v2"); + +function git(worktree: string, ...args: string[]): string { + const result = Bun.spawnSync(["git", "-C", worktree, ...args], { stdout: "pipe", stderr: "pipe" }); + return new TextDecoder().decode(result.stdout).trim(); +} + +async function main() { + const worktree = resolve(argValue("--worktree") ?? REPO_ROOT); + const fxBin = join(worktree, "zig-out", "bin", "fx"); + if (!existsSync(fxBin)) throw new Error(`missing ${fxBin}; run zig build first`); + const label = argValue("--label") ?? "run"; + const seed = Number(argValue("--seed") ?? "20261006"); + const randomCount = Number(argValue("--random") ?? "24"); + const steps = Number(argValue("--steps") ?? "12"); + + const reportDir = outDir(`acp-speed-${label}`); + mkdirSync(reportDir, { recursive: true }); + const status = git(worktree, "status", "--porcelain"); + const manifest = { + label, + worktree, + head: git(worktree, "rev-parse", "HEAD"), + dirty: status.length > 0, + status: status.split("\n").filter(Boolean), + diff_sha256: status ? sha256Text(git(worktree, "diff", "HEAD")) : null, + fx_binary_sha256: sha256File(fxBin), + toolchain: tlcToolchain(), + bun: Bun.version, + seed, + randomCount, + steps, + sessionsV2: SESSIONS_V2 ?? "default", + argv: process.argv.slice(1), + }; + writeJson(join(reportDir, "manifest.json"), manifest); + if (status) writeFileSync(join(reportDir, "worktree.diff"), git(worktree, "diff", "HEAD") + "\n"); + + const helpers = await import(join(worktree, "tests", "e2e", "tmux-helpers.ts")) as Helpers; + const only = argValue("--only"); + const plans = [...DIRECTED, ...randomPlans(randomCount, steps, seed)] + .filter((plan) => !only || new RegExp(only).test(plan.name)); + const results = []; + for (const plan of plans) { + const dir = join(reportDir, "traces", plan.name); + const run = await runPlan(plan, worktree, helpers, dir); + const processFailed = run.processes.some((proc) => proc.exit !== 0); + const checked = run.error ? null : await validate(run.observations, dir, TRACE_CATALOG); + const verdict = run.error ? "RUN_ERROR" : processFailed ? "PROCESS_ERROR" : checked!.verdict; + results.push({ name: plan.name, verdict, steps: run.observations.length, error: run.error, firstDivergence: checked?.firstDivergence ?? null, processes: run.processes.map((proc) => proc.exit) }); + const where = checked?.firstDivergence ? ` first divergence at step ${checked.firstDivergence.step}: ${JSON.stringify(checked.firstDivergence.observation)}` : ""; + console.log(`${plan.name}: ${verdict} (${run.observations.length} steps)${run.error ? ` ${run.error}` : where}`); + } + + // Controls show the bridge separates conforming from non-conforming runs. + const controls = []; + const synthetic = syntheticTrace(); + controls.push({ name: "synthetic-conforming", expect: "ACCEPTED", got: (await validate(synthetic, join(reportDir, "controls", "synthetic-conforming"), TRACE_CATALOG)).verdict }); + controls.push({ name: "synthetic-tampered", expect: "REJECTED", got: (await validate(tamper(synthetic)!, join(reportDir, "controls", "synthetic-tampered"), TRACE_CATALOG)).verdict }); + controls.push({ name: "empty-trace", expect: "TOOL_ERROR", got: (await validate([], join(reportDir, "controls", "empty-trace"), TRACE_CATALOG)).verdict }); + const firstAccepted = results.find((result) => result.verdict === "ACCEPTED"); + if (firstAccepted) { + const observed = (await Bun.file(join(reportDir, "traces", firstAccepted.name, "observations.json")).json()) as Observation[]; + const tampered = tamper(observed); + if (tampered) { + controls.push({ name: `tampered-${firstAccepted.name}`, expect: "REJECTED", got: (await validate(tampered, join(reportDir, "controls", `tampered-${firstAccepted.name}`), TRACE_CATALOG)).verdict }); + } + } + for (const control of controls) console.log(`control ${control.name}: ${control.got} (expected ${control.expect})`); + + const counts = results.reduce>((acc, result) => ({ ...acc, [result.verdict]: (acc[result.verdict] ?? 0) + 1 }), {}); + const controlsPassed = controls.every((control) => control.got === control.expect); + const summary = { manifest, counts, controlsPassed, controls, results }; + writeJson(join(reportDir, "summary.json"), summary); + console.log(`verdicts: ${JSON.stringify(counts)}; controls ${controlsPassed ? "passed" : "FAILED"}`); + console.log(`report: ${reportDir}`); + const allAccepted = results.every((result) => result.verdict === "ACCEPTED"); + process.exit(controlsPassed && allAccepted ? 0 : 1); +} + +await main(); diff --git a/tests/tla/drivers/acp/speed/explain.ts b/tests/tla/drivers/acp/speed/explain.ts new file mode 100644 index 000000000..049eab735 --- /dev/null +++ b/tests/tla/drivers/acp/speed/explain.ts @@ -0,0 +1,55 @@ +// Diagnostic only: prints each observed step beside the state the spec +// predicts, to explain a TLC rejection. TLC remains the oracle; this mirrors +// tests/tla/acp/AcpSpeed.tla for readability and assumes a deterministic start. +// +// bun tests/tla/drivers/acp/speed/explain.ts /traces/ +import { join } from "node:path"; + +const SUP_FAST = new Set(["openai/gpt-6-astra", "openai/gpt-5.6-priority"]); +const SUP_ULTRA = new Set(["openai/gpt-6-astra"]); + +const dir = process.argv[2]; +if (!dir) throw new Error("usage: bun tests/tla/drivers/acp/speed/explain.ts "); +const plan = await Bun.file(join(dir, "plan.json")).json(); +const observations = await Bun.file(join(dir, "observations.json")).json(); + +let model: string = plan.initialModel; +let fast: boolean = plan.defaultFast; +let ultra = false; +let prompted = false; +const short = (m: string) => m.split("/").pop(); +const view = () => `${short(model)} fast=${SUP_FAST.has(model) ? fast : "absent"} ultra=${SUP_ULTRA.has(model) ? ultra : "absent"}`; + +console.log(`init ${short(plan.initialModel)} defaultFast=${plan.defaultFast}`); +for (const [index, o] of observations.entries()) { + let expectOk = true; + let expectSpeed = "none"; + switch (o.op) { + case "fast": { + const b = o.arg === "true"; + if (b && !SUP_FAST.has(model)) expectOk = false; + else { fast = b; if (b) ultra = false; } + break; + } + case "ultrafast": { + const b = o.arg === "true"; + if (b && !SUP_ULTRA.has(model)) expectOk = false; + else { ultra = b; if (b) fast = false; } + break; + } + case "model": + model = o.arg; fast = fast && SUP_FAST.has(model); ultra = ultra && SUP_ULTRA.has(model); + break; + case "unknown": + expectOk = false; + break; + case "prompt": + prompted = true; + expectSpeed = ultra ? "ultrafast" : fast && SUP_FAST.has(model) ? "fast" : "standard"; + break; + } + const seen = o.hasView ? `${short(o.view.model)} fast=${o.view.fast} ultra=${o.view.ultra}` : ""; + const want = o.hasView ? view() : ""; + const mismatch = o.ok !== expectOk || (o.op === "prompt" && o.speed !== expectSpeed) || (o.hasView && seen.replace(/"/g, "") !== want); + console.log(`${mismatch ? "!!" : " "} ${String(index + 1).padStart(2)} ${o.op.padEnd(9)} ${String(o.arg).split("/").pop()!.padEnd(16)} ok=${o.ok} speed=${o.speed.padEnd(9)} seen[${seen}]${mismatch ? ` want[ok=${expectOk} speed=${expectSpeed} ${want}]` : ""}${prompted ? "" : " (before first prompt)"}`); +} diff --git a/tests/tla/drivers/acp/speed/tlc.ts b/tests/tla/drivers/acp/speed/tlc.ts new file mode 100644 index 000000000..9939bc00c --- /dev/null +++ b/tests/tla/drivers/acp/speed/tlc.ts @@ -0,0 +1,13 @@ +// TLC helpers for the ACP speed driver: the shared runner in +// ../../lib/tlc.ts, pointed at the specs in tests/tla/acp/. +import { join } from "node:path"; +import { TLA_ROOT, runTlc as runShared } from "../../lib/tlc"; + +export { sha256File, sha256Text, tlcToolchain, utcStamp, writeJson } from "../../lib/tlc"; +export type { TlcRun } from "../../lib/tlc"; + +export const SPEC_DIR = join(TLA_ROOT, "acp"); + +export function runTlc(dir: string, module: string, cfg: string, specs: string[]) { + return runShared(dir, module, cfg, specs, SPEC_DIR); +} diff --git a/tests/tla/drivers/acp/speed/trace.ts b/tests/tla/drivers/acp/speed/trace.ts new file mode 100644 index 000000000..9c1978554 --- /dev/null +++ b/tests/tla/drivers/acp/speed/trace.ts @@ -0,0 +1,186 @@ +// Shared pieces of the runtime bridge: the ACP stdio client, the +// client-visible projection of configOptions, the lane a Gateway request +// asks for, and TLC trace validation against tests/tla/acp/AcpSpeedTrace.tla. +import { mkdirSync, writeFileSync } from "node:fs"; +import { join } from "node:path"; +import { runTlc, sha256Text, writeJson } from "./tlc"; + +// ------------------------------------------------------------ observation -- + +export type View = { model: string; fast: string; ultra: string }; +export type Observation = { op: string; arg: string; ok: boolean; speed: string; hasView: boolean; view: View; detail?: unknown }; +export const NO_VIEW: View = { model: "", fast: "", ultra: "" }; + +export function viewOf(configOptions: unknown): View | null { + if (!Array.isArray(configOptions)) return null; + const byId = new Map(configOptions.map((option: any) => [option?.id, option])); + const model = byId.get("model")?.currentValue; + if (typeof model !== "string") return null; + const lane = (id: string) => { + const option = byId.get(id); + if (!option) return "absent"; + return typeof option.currentValue === "string" ? option.currentValue : "invalid"; + }; + return { model, fast: lane("fast"), ultra: lane("ultrafast") }; +} + +export function laneOf(body: string): string { + try { + const providerOptions = JSON.parse(body).providerOptions ?? {}; + if (providerOptions.openai?.serviceTier === "ultrafast") return "ultrafast"; + if (providerOptions.gateway?.speed === "fast") return "fast"; + return "standard"; + } catch { + return "unparseable"; + } +} + +// -------------------------------------------------------------- ACP client -- + +export class Acp { + private buffer = ""; + private lines: string[] = []; + private waiters: Array<(line: string) => void> = []; + private closed = false; + private nextId = 1; + stderr = ""; + readonly exited: Promise; + + constructor(readonly proc: ReturnType, private readonly log: (entry: object) => void) { + this.exited = (async () => { + const code = await proc.exited; + this.closed = true; + for (const waiter of this.waiters.splice(0)) waiter(""); + return code; + })(); + (async () => { + const decoder = new TextDecoder(); + for await (const chunk of proc.stdout as ReadableStream) { + this.buffer += decoder.decode(chunk); + const parts = this.buffer.split("\n"); + this.buffer = parts.pop() ?? ""; + for (const line of parts) { + if (!line.trim()) continue; + const waiter = this.waiters.shift(); + if (waiter) waiter(line); + else this.lines.push(line); + } + } + })(); + (async () => { + const decoder = new TextDecoder(); + for await (const chunk of proc.stderr as ReadableStream) this.stderr += decoder.decode(chunk); + })(); + } + + private async readLine(): Promise { + const buffered = this.lines.shift(); + if (buffered) return JSON.parse(buffered); + if (this.closed) throw new Error(`fx acp exited: ${this.stderr}`); + const line = await new Promise((resolveLine, reject) => { + const timer = setTimeout(() => reject(new Error(`fx acp read timeout: ${this.stderr}`)), 20_000); + this.waiters.push((value) => { clearTimeout(timer); resolveLine(value); }); + }); + if (!line) throw new Error(`fx acp exited: ${this.stderr}`); + return JSON.parse(line); + } + + async call(method: string, params: Record): Promise { + const id = this.nextId++; + this.log({ dir: "out", id, method, params }); + (this.proc.stdin as any).write(`${JSON.stringify({ jsonrpc: "2.0", id, method, params })}\n`); + (this.proc.stdin as any).flush?.(); + while (true) { + const message = await this.readLine(); + if ("method" in message && "id" in message) { + this.log({ dir: "in-request", method: message.method }); + (this.proc.stdin as any).write(`${JSON.stringify({ jsonrpc: "2.0", id: message.id, result: { outcome: { outcome: "cancelled" } } })}\n`); + continue; + } + if (message.id === id) { + this.log({ dir: "in", id, method, error: message.error ?? null, result: message.result ?? null }); + return message; + } + } + } + + async close(): Promise<{ exit: number; stderr: string }> { + if (!this.closed) (this.proc.stdin as any).end(); + const timer = setTimeout(() => this.proc.kill("SIGKILL"), 5_000); + const exit = await this.exited; + clearTimeout(timer); + return { exit, stderr: this.stderr }; + } +} + +// ---------------------------------------------------------------- TLC side -- + +const tla = (value: string) => JSON.stringify(value); +const tlaSet = (values: string[]) => `{${values.map(tla).join(", ")}}`; + +export type TraceCatalog = { models: string[]; supFast: string[]; supUltra: string[] }; + +export function obsModule(observations: Observation[], catalog: TraceCatalog): string { + const record = (o: Observation) => { + const view = `[model |-> ${tla(o.view.model)}, fast |-> ${tla(o.view.fast)}, ultra |-> ${tla(o.view.ultra)}]`; + return `[op |-> ${tla(o.op)}, arg |-> ${tla(o.arg)}, ok |-> ${o.ok ? "TRUE" : "FALSE"}, speed |-> ${tla(o.speed)}, hasView |-> ${o.hasView ? "TRUE" : "FALSE"}, view |-> ${view}]`; + }; + return [ + "---------------------------- MODULE AcpSpeedObs ----------------------------", + "(* Generated from one observed fx acp run. *)", + `TModels == ${tlaSet(catalog.models)}`, + `TSupFast == ${tlaSet(catalog.supFast)}`, + `TSupUltra == ${tlaSet(catalog.supUltra)}`, + "TraceLog == <<", + observations.map((o) => ` ${record(o)}`).join(",\n"), + ">>", + "=============================================================================", + "", + ].join("\n"); +} + +const TRACE_CFG = [ + "CONSTANTS", + " Models <- TModels", + " SupFast <- TSupFast", + " SupUltra <- TSupUltra", + "INIT TraceInit", + "NEXT TraceNext", + "INVARIANT NotDone", + "CHECK_DEADLOCK FALSE", + "", +].join("\n"); + +export type Verdict = "ACCEPTED" | "REJECTED" | "TOOL_ERROR"; + +export async function validate(observations: Observation[], dir: string, catalog: TraceCatalog) { + mkdirSync(dir, { recursive: true }); + if (observations.length === 0) return { verdict: "TOOL_ERROR" as Verdict, reason: "empty trace", matched: 0 }; + const obs = obsModule(observations, catalog); + writeFileSync(join(dir, "AcpSpeedObs.tla"), obs); + writeFileSync(join(dir, "AcpSpeedTrace.cfg"), TRACE_CFG); + const run = await runTlc(dir, "AcpSpeedTrace.tla", "AcpSpeedTrace.cfg", ["AcpSpeed.tla", "AcpSpeedTrace.tla"]); + const finalIndex = [...run.output.matchAll(/\/\\ i = (\d+)/g)].map((match) => Number(match[1])).at(-1) ?? null; + let verdict: Verdict; + let matched: number; + if (run.exitCode === 12 && run.violated === "NotDone" && finalIndex === observations.length) { + verdict = "ACCEPTED"; + matched = observations.length; + } else if (run.exitCode === 0 && /No error has been found/.test(run.output)) { + verdict = "REJECTED"; + matched = run.distinctStates === 0 ? 0 : run.depth ?? 0; + } else { + verdict = "TOOL_ERROR"; + matched = 0; + } + const result = { + verdict, + matched, + length: observations.length, + firstDivergence: verdict === "REJECTED" ? { step: matched + 1, observation: observations[matched] ?? null } : null, + tlc: { exitCode: run.exitCode, violated: run.violated, finalIndex, depth: run.depth, durationMs: run.durationMs }, + obs_sha256: sha256Text(obs), + }; + writeJson(join(dir, "verdict.json"), result); + return result; +} diff --git a/tests/tla/drivers/cli/bridge.ts b/tests/tla/drivers/cli/bridge.ts new file mode 100644 index 000000000..2bf8a0714 --- /dev/null +++ b/tests/tla/drivers/cli/bridge.ts @@ -0,0 +1,129 @@ +// Connects behavior observed from the real fx binary to TLC. +// +// The observations become LaunchObserved.tla. LaunchTrace replays them through +// LaunchSelection's own actions for one design. ACCEPTED requires TLC exit 12 +// on the NotAllMatched sentinel, reachable only after every observation +// matched. A completed search is REJECTED; then each observation is replayed +// alone to name the first one the design cannot produce. +// +// Strict verdicts: unreadable or missing evidence is never acceptance. +import { createHash } from "node:crypto"; +import { copyFileSync, mkdirSync, mkdtempSync, readFileSync, writeFileSync } from "node:fs"; +import { join, resolve } from "node:path"; +import { TLA_ROOT, tlcToolchain } from "../lib/tlc"; +import type { Notice, Outcome, Scenario } from "./scenarios"; + +export type Design = "current" | "proposed"; +export type Verdict = "ACCEPTED" | "REJECTED" | "TOOL_ERROR"; + +export interface ObservedRequest { + present: boolean; + model: string; + indicator: "on" | "off" | "unobserved"; + wireFast: boolean; + wireUltra: boolean; + wireEffort: "supported" | "none" | "other"; +} + +export interface Observation { + id: string; + scenario: Scenario; + /** The early-submit race: either interleaving may explain the result. */ + orderFree: boolean; + outcome: Outcome; + notices: Notice[]; + req: ObservedRequest; + evidence: Record; +} + +export interface TraceResult { + design: Design; + verdict: Verdict; + detail: string; + firstMismatch?: string; + hashes: Record; +} + +const tla = join(TLA_ROOT, "cli"); + +const str = (value: string) => JSON.stringify(value); +const bool = (value: boolean) => (value ? "TRUE" : "FALSE"); + +function scenarioValue(s: Scenario): string { + return `[path |-> ${str(s.path)}, model |-> ${str(s.model)}, speed |-> ${str(s.speed)}, ` + + `effort |-> ${str(s.effort)}, catalog |-> ${str(s.catalog)}, fastCap |-> ${bool(s.fastCap)}, ` + + `ultraCap |-> ${bool(s.ultraCap)}, early |-> ${bool(s.early)}]`; +} + +function observationValue(o: Observation): string { + const r = o.req; + return `[sc |-> ${scenarioValue(o.scenario)}, orderFree |-> ${bool(o.orderFree)}, ` + + `outcome |-> ${str(o.outcome)}, notices |-> {${o.notices.map(str).join(", ")}}, ` + + `req |-> [present |-> ${bool(r.present)}, model |-> ${str(r.model)}, indicator |-> ${str(r.indicator)}, ` + + `wireFast |-> ${bool(r.wireFast)}, wireUltra |-> ${bool(r.wireUltra)}, wireEffort |-> ${str(r.wireEffort)}]]`; +} + +export function observedModule(observations: Observation[]): string { + return [ + "---------------------------- MODULE LaunchObserved ----------------------------", + "(* Generated by bun/bridge.ts from runtime observations. Do not edit. *)", + `Observed == << ${observations.map(observationValue).join(",\n ")} >>`, + "=============================================================================", + "", + ].join("\n"); +} + +const sha = (path: string) => createHash("sha256").update(readFileSync(path)).digest("hex"); + +async function runTrace(observations: Observation[], design: Design, parent: string): Promise<{ verdict: Verdict; log: string; dir: string }> { + const dir = mkdtempSync(join(parent, `trace-${design}-`)); + for (const file of ["LaunchSelection.tla", "LaunchTrace.tla"]) copyFileSync(join(tla, file), join(dir, file)); + writeFileSync(join(dir, "LaunchObserved.tla"), observedModule(observations)); + writeFileSync(join(dir, "trace.cfg"), [ + "SPECIFICATION TraceSpec", + "CONSTANTS", + ` Design = ${str(design)}`, + ' Mutant = "none"', + ' Class = "all"', + "INVARIANT NotAllMatched", + "CHECK_DEADLOCK FALSE", + "", + ].join("\n")); + const { java, jar } = tlcToolchain(); + mkdirSync(join(dir, ".tlc-tmp"), { recursive: true }); + const child = Bun.spawn([java, "-XX:+UseParallelGC", `-Djava.io.tmpdir=${join(dir, ".tlc-tmp")}`, "-cp", jar, "tlc2.TLC", "-workers", "1", + "-metadir", join(dir, ".tlc-states"), "-config", "trace.cfg", "LaunchTrace.tla"], { + cwd: dir, stdin: "ignore", stdout: "pipe", stderr: "pipe", + }); + const [stdout, stderr, code] = await Promise.all([new Response(child.stdout).text(), new Response(child.stderr).text(), child.exited]); + const log = `${stdout}\n${stderr}`; + writeFileSync(join(dir, "tlc.log"), log); + if (code === 12 && log.includes("Invariant NotAllMatched is violated")) return { verdict: "ACCEPTED", log, dir }; + if (code === 0 && log.includes("Model checking completed. No error has been found.")) return { verdict: "REJECTED", log, dir }; + return { verdict: "TOOL_ERROR", log, dir }; +} + +/** Replays every observation through one design. `parent` receives the TLC work. */ +export async function checkTrace(observations: Observation[], design: Design, parent: string): Promise { + const hashes = { + "LaunchSelection.tla": sha(join(tla, "LaunchSelection.tla")), + "LaunchTrace.tla": sha(join(tla, "LaunchTrace.tla")), + observations: createHash("sha256").update(JSON.stringify(observations)).digest("hex"), + }; + if (observations.length === 0) return { design, verdict: "TOOL_ERROR", detail: "no observations", hashes }; + const whole = await runTrace(observations, design, parent); + if (whole.verdict !== "REJECTED") { + return { design, verdict: whole.verdict, detail: `${observations.length} observations; TLC work ${whole.dir}`, hashes }; + } + for (const observation of observations) { + const single = await runTrace([observation], design, parent); + if (single.verdict !== "ACCEPTED") { + return { + design, verdict: "REJECTED", hashes, firstMismatch: observation.id, + detail: `${design} design cannot produce observation ${observation.id} ` + + `(outcome=${observation.outcome}, notices=[${observation.notices}], req=${JSON.stringify(observation.req)})`, + }; + } + } + return { design, verdict: "REJECTED", hashes, detail: "each observation matches alone, but not in sequence" }; +} diff --git a/tests/tla/drivers/cli/launch.test.ts b/tests/tla/drivers/cli/launch.test.ts new file mode 100644 index 000000000..295d65962 --- /dev/null +++ b/tests/tla/drivers/cli/launch.test.ts @@ -0,0 +1,255 @@ +// Runs the real fx binary through every launch-flag scenario the +// LaunchSelection TLA+ model covers (tests/tla/cli/LaunchSelection.tla), then has TLC +// replay what fx did through the model. No model calls: a local fake Gateway +// serves the catalog and accepts only models that exist. +// +// 1. The binary must conform to exactly one modeled design, current or proposed. +// 2. Controls: tampered and empty evidence must not be accepted. +// 3. With FX_TLA_PROPOSED=1: the binary must conform to the proposed design. +// This fails until fx validates launch flags. +import { test } from "bun:test"; +import assert from "node:assert/strict"; +import { mkdirSync, writeFileSync } from "node:fs"; +import { join } from "node:path"; +import { artifacts, binary, shellQuote, targetHelpers } from "../lib/context"; +import { checkTrace, type Design, type Observation, type ObservedRequest, type TraceResult } from "./bridge"; +import { + AUTHENTICATED_CATALOG, CONFIGURED, PUBLIC_CATALOG, SCENARIOS, SUPPORTED_EFFORT, TRUTH, + askRejection, flagArgs, nameClass, noticesIn, type Outcome, type Scenario, +} from "./scenarios"; + +const { startDynamicFakeGateway, fakeGatewayFinalText, TmuxSession } = await targetHelpers(); +const reports = join(artifacts, "tlc"); +mkdirSync(reports, { recursive: true }); +const TIMEOUT = 900_000; +const DONE_WORD = "MFV_DONE_7"; +const PROMPT = "Reply with the done word."; +const SLOW_CATALOG_MS = 4_000; + +const sleep = (ms: number) => new Promise(resolve => setTimeout(resolve, ms)); + +async function waitUntil(condition: () => boolean, timeoutMs: number): Promise { + const deadline = Date.now() + timeoutMs; + while (Date.now() < deadline) { + if (condition()) return true; + await sleep(50); + } + return condition(); +} + +interface Fixture { + root: string; home: string; workspace: string; + gateway: any; + env: Record; + catalogRequests: Array<{ authorized: boolean; status: number }>; + catalogServed: () => boolean; + rejectedModels: string[]; +} + +function fixture(s: Scenario): Fixture { + const root = join(artifacts, s.id); + const home = join(root, "home"); + const workspace = join(root, "workspace"); + mkdirSync(join(home, ".fx"), { recursive: true, mode: 0o700 }); + mkdirSync(workspace, { recursive: true }); + writeFileSync(join(home, ".fx/settings.json"), JSON.stringify({ auto_upgrade: false, model: CONFIGURED })); + const catalogRequests: Fixture["catalogRequests"] = []; + const rejectedModels: string[] = []; + let served = false; + let gateway: any; + gateway = startDynamicFakeGateway(() => { + const model = gateway.requests.at(-1)?.headers.get("ai-language-model-id") ?? ""; + if (!TRUTH.has(model)) { + rejectedModels.push(model); + return Response.json({ error: { type: "model_not_found", message: `Model '${model}' not found` } }, { status: 404 }); + } + return fakeGatewayFinalText(DONE_WORD); + }, { + models: async (request: Request) => { + const authorized = Boolean(request.headers.get("authorization")); + let response: Response; + if (s.catalog === "failed") { + response = new Response("catalog unavailable", { status: 500 }); + } else if (s.catalog === "anonymous" && authorized) { + response = Response.json({ error: { message: "unauthorized" } }, { status: 401 }); + } else { + if (s.early) await sleep(SLOW_CATALOG_MS); + response = Response.json({ data: s.catalog === "anonymous" ? PUBLIC_CATALOG : AUTHENTICATED_CATALOG }); + } + catalogRequests.push({ authorized, status: response.status }); + if (response.status === 200 || s.catalog === "failed") served = true; + return response; + }, + }); + const env: Record = {}; + for (const [key, value] of Object.entries(process.env)) if (value !== undefined && key !== "FX_MODEL") env[key] = value; + Object.assign(env, { + HOME: home, TMPDIR: root, + AI_GATEWAY_API_KEY: "fake-mfv-key", FX_PROVIDER: "gateway", + FX_GATEWAY_BASE_URL: gateway.baseUrl, FX_GATEWAY_CHAT_URL: gateway.chatUrl, + FX_E2E_GATEWAY_CHAT_URL: gateway.chatUrl, + FX_E2E_GATEWAY_MODELS_URL: `${gateway.baseUrl}/coding-agent/v1/models`, + FX_SOUND: "0", FX_AUTO_UPGRADE: "0", FX_DISABLE_KEYCHAIN: "1", FX_E2E_DISABLE_DOTENV: "1", + // Kept with the scenario evidence so an unexpected outcome can be traced. + FX_TRACE_LOG: join(root, "trace.log"), FX_TRACE_SCOPES: "agent,core,gateway,auth,session", + }); + return { root, home, workspace, gateway, env, catalogRequests, catalogServed: () => served, rejectedModels }; +} + +function wireOf(s: Scenario, f: Fixture, indicator: ObservedRequest["indicator"]): ObservedRequest { + const first = f.gateway.requests[0]; + if (!first) return { present: false, model: "none", indicator: "unobserved", wireFast: false, wireUltra: false, wireEffort: "none" }; + const sent = first.headers.get("ai-language-model-id") ?? ""; + let body: any = {}; + try { body = JSON.parse(first.body); } catch {} + const reasoning = body.reasoning; + return { + present: true, + model: nameClass(s, sent), + indicator, + wireFast: body.providerOptions?.gateway?.speed === "fast", + wireUltra: body.providerOptions?.openai?.serviceTier === "ultrafast", + wireEffort: reasoning === undefined ? "none" : reasoning === SUPPORTED_EFFORT ? "supported" : "other", + }; +} + +function requestEvidence(f: Fixture) { + const first = f.gateway.requests[0]; + let body: any = {}; + try { body = JSON.parse(first?.body ?? "{}"); } catch {} + return { + mainRequests: f.gateway.requests.length, + sentModel: first?.headers.get("ai-language-model-id") ?? null, + reasoning: body.reasoning ?? null, + providerOptions: body.providerOptions ?? null, + rejectedModels: f.rejectedModels, + catalogRequests: f.catalogRequests, + }; +} + +async function observeAsk(s: Scenario): Promise { + const f = fixture(s); + try { + const argv = ["ask", "--no-save", "--auto", ...flagArgs(s), PROMPT]; + const child = Bun.spawn([binary, ...argv], { + cwd: f.workspace, env: f.env, stdin: "ignore", stdout: "pipe", stderr: "pipe", + }); + const timer = setTimeout(() => child.kill(), 60_000); + const [stdout, stderr, code] = await Promise.all([new Response(child.stdout).text(), new Response(child.stderr).text(), child.exited]); + clearTimeout(timer); + let outcome: Outcome = "unknown"; + const requests = f.gateway.requests.length; + if (requests > 0) { + if (f.rejectedModels.length > 0) outcome = "gateway_error"; + else if (code === 0 && stdout.includes(DONE_WORD)) outcome = "sent"; + } else { + outcome = askRejection(stderr) ?? (code !== 0 ? "turn_error" : "unknown"); + } + return { + id: s.id, scenario: s, orderFree: false, outcome, notices: [], req: wireOf(s, f, "unobserved"), + evidence: { argv, exitCode: code, stdout: stdout.slice(-2000), stderr: stderr.slice(-2000), ...requestEvidence(f) }, + }; + } finally { + f.gateway.stop(); + } +} + +function footerLine(pane: string): string { + return pane.split("\n").map(line => line.trimEnd()).filter(Boolean).at(-1) ?? ""; +} + +async function observeInteractive(s: Scenario): Promise { + const f = fixture(s); + const cmd = [binary, ...flagArgs(s)].map(shellQuote).join(" "); + const session = await TmuxSession.create({ cmd, cwd: f.workspace, env: f.env, width: 140, height: 40, isolated: true, startupWaitMs: 300 }); + try { + await session.waitForComposer(20_000); + if (!s.early) { + await waitUntil(f.catalogServed, 15_000); + await sleep(1_500); + } + const footer = footerLine(await session.capturePane()); + const indicator = footer.includes("⚡") ? "on" : "off"; + const catalogSeenAtSubmit = f.catalogServed(); + await session.sendText(PROMPT); + let outcome: Outcome = "unknown"; + const sentRequest = await waitUntil(() => f.gateway.requests.length > 0, s.early ? SLOW_CATALOG_MS + 10_000 : 10_000); + if (sentRequest) { + if (await waitUntil(() => f.rejectedModels.length > 0, 1_500)) { + outcome = "gateway_error"; + } else { + const done = await session.waitForText(DONE_WORD, 15_000).then(() => true, () => false); + if (done) outcome = "sent"; + } + } else { + outcome = "turn_error"; + } + if (s.early) { + await waitUntil(f.catalogServed, 15_000); + await sleep(2_000); + } else { + await sleep(500); + } + const scrollback = await session.captureFullScrollback(); + return { + id: s.id, scenario: s, orderFree: s.early, outcome, notices: noticesIn(scrollback), req: wireOf(s, f, indicator), + evidence: { cmd, footerAtSubmit: footer, catalogSeenAtSubmit, scrollbackTail: scrollback.split("\n").slice(-40).join("\n"), ...requestEvidence(f) }, + }; + } finally { + await session.kill(); + f.gateway.stop(); + } +} + +let observed: Promise | undefined; +function observations(): Promise { + observed ??= (async () => { + const out: Observation[] = []; + for (const s of SCENARIOS) { + const observation = s.path === "ask" ? await observeAsk(s) : await observeInteractive(s); + console.log(`${s.kind.padEnd(8)} ${s.id.padEnd(34)} outcome=${observation.outcome} notices=[${observation.notices}] req=${JSON.stringify(observation.req)}`); + out.push(observation); + } + writeFileSync(join(artifacts, "observations.json"), JSON.stringify(out, null, 2)); + return out; + })(); + return observed; +} + +const verdicts = new Map>(); +function verdict(design: Design): Promise { + if (!verdicts.has(design)) { + verdicts.set(design, observations().then(async list => { + const result = await checkTrace(list, design, reports); + writeFileSync(join(artifacts, `trace-${design}.json`), JSON.stringify(result, null, 2)); + console.log(`trace ${design}: ${result.verdict} ${result.firstMismatch ?? ""} ${result.detail}`); + return result; + })); + } + return verdicts.get(design)!; +} + +test("real fx conforms to exactly one modeled design", async () => { + const [current, proposed] = await Promise.all([verdict("current"), verdict("proposed")]); + const accepted = [current, proposed].filter(result => result.verdict === "ACCEPTED").map(result => result.design); + writeFileSync(join(artifacts, "summary.json"), JSON.stringify({ binary, conforms: accepted, current, proposed }, null, 2)); + assert.equal(accepted.length, 1, `expected exactly one conforming design, got [${accepted}]: current=${current.detail}; proposed=${proposed.detail}`); +}, TIMEOUT); + +test("bridge rejects tampered and empty evidence", async () => { + const list = await observations(); + const conforming = (await verdict("current")).verdict === "ACCEPTED" ? "current" : "proposed"; + const tampered = list.map(item => ({ ...item, req: { ...item.req } })); + const target = tampered.find(item => item.req.present)!; + target.req.wireFast = !target.req.wireFast; + const result = await checkTrace(tampered, conforming, reports); + assert.equal(result.verdict, "REJECTED", `tampered evidence for ${target.id} was ${result.verdict}`); + assert.equal(result.firstMismatch, target.id); + assert.equal((await checkTrace([], conforming, reports)).verdict, "TOOL_ERROR"); +}, TIMEOUT); + +test.skipIf(process.env.FX_TLA_PROPOSED !== "1")("real fx meets the proposed design", async () => { + const proposed = await verdict("proposed"); + assert.equal(proposed.verdict, "ACCEPTED", proposed.detail); + assert.equal((await verdict("current")).verdict, "REJECTED"); +}, TIMEOUT); diff --git a/tests/tla/drivers/cli/scenarios.ts b/tests/tla/drivers/cli/scenarios.ts new file mode 100644 index 000000000..42d4152ab --- /dev/null +++ b/tests/tla/drivers/cli/scenarios.ts @@ -0,0 +1,136 @@ +// Runtime scenarios for the launch-flag contract, and how each one maps onto +// a LaunchSelection scenario. The fake Gateway serves CATALOG; the chat route +// accepts exactly the models in TRUTH, like the real Gateway. + +export type Path = "ask" | "interactive"; +export type ModelReq = "none" | "exact" | "partial_unique" | "partial_ambiguous" | "unknown" | "private_hidden"; +export type SpeedReq = "none" | "fast" | "ultrafast" | "off"; +export type EffortReq = "none" | "supported" | "unsupported"; +export type CatalogMode = "authenticated" | "anonymous" | "failed"; +export type Outcome = + | "sent" | "gateway_error" | "turn_error" + | "rejected_model" | "rejected_fast" | "rejected_ultrafast" | "rejected_effort" + | "unknown"; +export type Notice = "model" | "fast" | "ultrafast" | "effort"; + +export const CONFIGURED = "openai/mfv-configured"; +export const SUPPORTED_EFFORT = "high"; +export const UNSUPPORTED_EFFORT = "minimal"; + +const efforts = (values: string[]) => [{ type: "effort", values }]; +const price = { input: "0.000001", output: "0.000002" }; + +/** Fast, Ultra and three efforts. */ +const FULL = { + id: "openai/mfv-full", type: "language", owned_by: "openai", tags: ["tool-use", "reasoning"], + fast_options: [{ type: "toggle" }], reasoning_options: efforts(["low", "medium", SUPPORTED_EFFORT]), + pricing: { ...price, service_tiers: { priority: { input: "0.000002", output: "0.000004" }, ultrafast: { input: "0.00001", output: "0.00002" } } }, +}; +/** No Fast, no Ultra, two efforts. */ +const plain = (id: string, owned_by: string) => ({ + id, type: "language", owned_by, tags: ["tool-use", "reasoning"], + reasoning_options: efforts(["low", SUPPORTED_EFFORT]), pricing: { ...price }, +}); +const PLAIN = plain("anthropic/mfv-plain", "anthropic"); +const TERRA_ONE = plain("openai/mfv-terra-one", "openai"); +const TERRA_TWO = plain("openai/mfv-terra-two", "openai"); +const CONFIGURED_ENTRY = plain(CONFIGURED, "openai"); +/** Listed only to an authenticated catalog request. */ +const PRIVATE = plain("team/mfv-private", "team"); + +export const PUBLIC_CATALOG = [FULL, PLAIN, TERRA_ONE, TERRA_TWO, CONFIGURED_ENTRY]; +export const AUTHENTICATED_CATALOG = [...PUBLIC_CATALOG, PRIVATE]; +export const TRUTH = new Set(AUTHENTICATED_CATALOG.map(entry => entry.id)); + +export interface Scenario { + id: string; + kind: "ideal" | "nonideal"; + path: Path; + model: ModelReq; + /** The --model text, when model is not "none". */ + raw?: string; + /** The catalog ID the raw text should resolve to. */ + canonical?: string; + speed: SpeedReq; + effort: EffortReq; + catalog: CatalogMode; + /** Capabilities of the model fx would send. */ + fastCap: boolean; + ultraCap: boolean; + /** Interactive only: submit before the catalog arrives (slow catalog). */ + early: boolean; +} + +const full = { fastCap: true, ultraCap: true }; +const none = { fastCap: false, ultraCap: false }; +const base = { speed: "none", effort: "none", catalog: "authenticated", early: false } as const; + +export const SCENARIOS: Scenario[] = [ + // fx ask, ideal + { id: "ask-exact", kind: "ideal", path: "ask", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, ...full }, + { id: "ask-exact-fast", kind: "ideal", path: "ask", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, speed: "fast", ...full }, + { id: "ask-exact-ultrafast", kind: "ideal", path: "ask", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, speed: "ultrafast", ...full }, + { id: "ask-exact-effort", kind: "ideal", path: "ask", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, effort: "supported", ...full }, + // fx ask, non-ideal + { id: "ask-unknown", kind: "nonideal", path: "ask", model: "unknown", raw: "totally/not-a-real-model", ...base, ...none }, + { id: "ask-partial-unique", kind: "nonideal", path: "ask", model: "partial_unique", raw: "mfv-plain", canonical: PLAIN.id, ...base, ...none }, + { id: "ask-partial-ambiguous", kind: "nonideal", path: "ask", model: "partial_ambiguous", raw: "mfv-terra", ...base, ...none }, + { id: "ask-fast-unsupported", kind: "nonideal", path: "ask", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, speed: "fast", ...none }, + { id: "ask-ultrafast-unsupported", kind: "nonideal", path: "ask", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, speed: "ultrafast", ...none }, + { id: "ask-effort-unsupported", kind: "nonideal", path: "ask", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, effort: "unsupported", ...none }, + { id: "ask-configured-fast-unsupported", kind: "nonideal", path: "ask", model: "none", ...base, speed: "fast", ...none }, + { id: "ask-private-anonymous", kind: "nonideal", path: "ask", model: "private_hidden", raw: PRIVATE.id, canonical: PRIVATE.id, ...base, catalog: "anonymous", ...none }, + { id: "ask-unknown-catalog-failed", kind: "nonideal", path: "ask", model: "unknown", raw: "totally/not-a-real-model", ...base, catalog: "failed", ...none }, + { id: "ask-fast-catalog-failed", kind: "nonideal", path: "ask", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, speed: "fast", catalog: "failed", ...full }, + // interactive, ideal + { id: "tui-exact-fast", kind: "ideal", path: "interactive", model: "exact", raw: FULL.id, canonical: FULL.id, ...base, speed: "fast", ...full }, + // interactive, non-ideal + { id: "tui-unknown-fast", kind: "nonideal", path: "interactive", model: "unknown", raw: "totally/not-a-real-model", ...base, speed: "fast", ...none }, + { id: "tui-partial-unique", kind: "nonideal", path: "interactive", model: "partial_unique", raw: "mfv-plain", canonical: PLAIN.id, ...base, ...none }, + { id: "tui-ultrafast-unsupported", kind: "nonideal", path: "interactive", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, speed: "ultrafast", ...none }, + { id: "tui-effort-unsupported", kind: "nonideal", path: "interactive", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, effort: "unsupported", ...none }, + { id: "tui-private-anonymous", kind: "nonideal", path: "interactive", model: "private_hidden", raw: PRIVATE.id, canonical: PRIVATE.id, ...base, catalog: "anonymous", ...none }, + { id: "tui-fast-unsupported-early", kind: "nonideal", path: "interactive", model: "exact", raw: PLAIN.id, canonical: PLAIN.id, ...base, speed: "fast", early: true, ...none }, +]; + +export function flagArgs(s: Scenario): string[] { + const args: string[] = []; + if (s.model !== "none") args.push("--model", s.raw!); + if (s.speed === "fast") args.push("--fast"); + if (s.speed === "ultrafast") args.push("--ultrafast"); + if (s.speed === "off") args.push("--no-fast"); + if (s.effort === "supported") args.push("--effort", SUPPORTED_EFFORT); + if (s.effort === "unsupported") args.push("--effort", UNSUPPORTED_EFFORT); + return args; +} + +/** LaunchSelection's model-name class for a model ID fx actually sent. */ +/** No scenario passes CONFIGURED as --model, so the order below is unambiguous. */ +export function nameClass(s: Scenario, sent: string): "configured" | "canonical" | "raw" | "other" { + if (sent === CONFIGURED) return "configured"; + if (s.canonical && sent === s.canonical) return "canonical"; + if (s.raw && sent === s.raw) return "raw"; + return "other"; +} + +/** + * Classifies an `fx ask` failure that sent no request from its stderr. Launch + * rejections name the model; the turn-time Ultrafast failure does not. + */ +export function askRejection(stderr: string): Outcome | null { + if (/^fx ask: (Unknown model "|Model "[^"]*" matches several catalog models)/m.test(stderr)) return "rejected_model"; + if (/^fx ask: Fast mode is not available for model "/m.test(stderr)) return "rejected_fast"; + if (/^fx ask: Ultrafast mode is not available for model "/m.test(stderr)) return "rejected_ultrafast"; + if (/^fx ask: Reasoning effort (is unavailable|"[^"]*" is not available)/m.test(stderr)) return "rejected_effort"; + return null; +} + +/** Notice markers printed by interactive launch validation. */ +export function noticesIn(text: string): Notice[] { + const found = new Set(); + if (/Unknown model "|matches several catalog models/.test(text)) found.add("model"); + if (/(^|[^a-z])Fast mode is not available for model/.test(text)) found.add("fast"); + if (/Ultrafast mode is not available for model/.test(text)) found.add("ultrafast"); + if (/Reasoning effort "[^"]*" is not available for model|Reasoning effort is unavailable for the active model/.test(text)) found.add("effort"); + return [...found].sort(); +} diff --git a/tests/tla/drivers/lib/context.ts b/tests/tla/drivers/lib/context.ts new file mode 100644 index 000000000..026443ffb --- /dev/null +++ b/tests/tla/drivers/lib/context.ts @@ -0,0 +1,50 @@ +// Run context for the Bun drivers written as `bun test` files: which fx +// checkout and binary they drive, where their output goes, and the E2E helpers +// they borrow from tests/e2e/. +// +// FX_WORKTREE checkout under test (default: this one) +// FX_BIN binary under test (default: /zig-out/bin/fx) +// FX_TLA_OUT output root (default: a folder under the system temp dir) +// FX_TLA_REPEAT how many times a repeatable check runs (default: 1) +import { createHash } from "node:crypto"; +import { existsSync, readFileSync } from "node:fs"; +import { join, resolve } from "node:path"; +import { pathToFileURL } from "node:url"; +import { REPO_ROOT, outDir } from "./tlc"; + +export const worktree = resolve(process.env.FX_WORKTREE ?? REPO_ROOT); +export const binary = process.env.FX_BIN ?? join(worktree, "zig-out", "bin", "fx"); +export const artifacts = outDir(process.env.FX_TLA_CASE ?? "driver"); +export const repetitions = Number(process.env.FX_TLA_REPEAT ?? "1"); + +/// The checkout's tests/e2e/tmux-helpers.ts: tmux sessions and fake gateways. +export async function targetHelpers() { + const path = join(worktree, "tests", "e2e", "tmux-helpers.ts"); + if (!existsSync(path)) throw new Error(`missing ${path}`); + return await import(pathToFileURL(path).href); +} + +export function shellQuote(value: string): string { + return `'${value.replaceAll("'", "'\\''")}'`; +} + +export function hashFile(path: string): string { + return createHash("sha256").update(readFileSync(path)).digest("hex"); +} + +/// A minimal environment for an fx process under test: no inherited +/// credentials, sound, keychain, upgrade check, or dotenv. +export function testEnvironment(values: Record, inherited = process.env): Record { + const result: Record = {}; + for (const key of ["PATH", "TERM", "COLORTERM", "LANG", "LC_ALL", "TMPDIR"]) { + if (inherited[key]) result[key] = inherited[key]!; + } + return { + ...result, + FX_SOUND: "0", + FX_DISABLE_KEYCHAIN: "1", + FX_AUTO_UPGRADE: "0", + FX_E2E_DISABLE_DOTENV: "1", + ...values, + }; +} diff --git a/tests/tla/drivers/lib/tlc.ts b/tests/tla/drivers/lib/tlc.ts new file mode 100644 index 000000000..d78a68efc --- /dev/null +++ b/tests/tla/drivers/lib/tlc.ts @@ -0,0 +1,130 @@ +// Shared helpers for the Bun drivers under tests/tla/drivers/: find TLC and +// Java the same way tests/tla/lib/tlc.sh does, run TLC on a model in a +// scratch folder, and locate the fx binary under test. +// +// TLC comes from TLA2TOOLS_JAR or ~/.local/share/tla/tla2tools.jar. Java comes +// from JAVA_HOME, Homebrew's OpenJDK, or PATH. The binary is FX_BIN, or +// zig-out/bin/fx in this checkout. Output goes to FX_TLA_OUT, or a fresh folder +// under the system temp directory. +import { createHash } from "node:crypto"; +import { copyFileSync, existsSync, mkdirSync, readFileSync, writeFileSync } from "node:fs"; +import { homedir, tmpdir } from "node:os"; +import { dirname, join, resolve } from "node:path"; + +export const REPO_ROOT = resolve(import.meta.dirname, "../../../.."); +export const TLA_ROOT = join(REPO_ROOT, "tests", "tla"); + +export function sha256File(path: string): string { + return createHash("sha256").update(readFileSync(path)).digest("hex"); +} + +export function sha256Text(text: string): string { + return createHash("sha256").update(text).digest("hex"); +} + +/// The fx binary under test. Throws when it has not been built. +export function fxBin(): string { + const bin = process.env.FX_BIN ?? join(REPO_ROOT, "zig-out", "bin", "fx"); + if (!existsSync(bin)) throw new Error(`missing ${bin}; run zig build first or set FX_BIN`); + return bin; +} + +/// A fresh output folder for one driver run. The caller owns its contents. +export function outDir(name: string): string { + const base = process.env.FX_TLA_OUT ?? join(tmpdir(), "fx-tla"); + const dir = join(base, name, utcStamp()); + mkdirSync(dir, { recursive: true }); + return dir; +} + +export type Toolchain = { java: string; javaVersion: string; jar: string; jarSha256: string }; + +let toolchain: Toolchain | null = null; + +export function tlcToolchain(): Toolchain { + if (toolchain) return toolchain; + const jar = process.env.TLA2TOOLS_JAR ?? join(homedir(), ".local", "share", "tla", "tla2tools.jar"); + if (!existsSync(jar)) throw new Error(`tla2tools.jar not found at ${jar} (set TLA2TOOLS_JAR)`); + const which = Bun.spawnSync(["sh", "-c", "command -v java"], { stdout: "pipe" }); + const candidates = [ + process.env.JAVA_HOME ? join(process.env.JAVA_HOME, "bin", "java") : "", + "/opt/homebrew/opt/openjdk/bin/java", + "/usr/local/opt/openjdk/bin/java", + new TextDecoder().decode(which.stdout).trim(), + ]; + for (const java of candidates) { + if (!java || !existsSync(java)) continue; + // /usr/bin/java on macOS is a stub that fails -version without a runtime. + const probe = Bun.spawnSync([java, "-version"], { stdout: "pipe", stderr: "pipe" }); + if (probe.exitCode !== 0) continue; + const javaVersion = new TextDecoder().decode(probe.stderr).split("\n")[0]?.trim() ?? ""; + toolchain = { java, javaVersion, jar, jarSha256: sha256File(jar) }; + return toolchain; + } + throw new Error("no working Java runtime (set JAVA_HOME or brew install openjdk)"); +} + +export type TlcRun = { + exitCode: number; + output: string; + violated: string | null; + distinctStates: number | null; + depth: number | null; + argv: string[]; + durationMs: number; +}; + +/// Runs TLC on `module` with `cfg` from `dir`, after copying `specs` from +/// `specDir` into it, so each run keeps the exact files it checked. TLC's +/// output is also written to `dir/tlc.log`. +export async function runTlc( + dir: string, + module: string, + cfg: string, + specs: string[], + specDir: string, + extraArgs: string[] = [], +): Promise { + const { java, jar } = tlcToolchain(); + mkdirSync(dir, { recursive: true }); + for (const name of specs) copyFileSync(join(specDir, name), join(dir, name)); + // A private java.io.tmpdir per run: TLC unpacks its standard modules there, + // and concurrent runs sharing one folder can lose them. + const javaTmp = join(dir, ".tlc-tmp"); + mkdirSync(javaTmp, { recursive: true }); + const argv = [ + java, "-XX:+UseParallelGC", "-Xss4m", `-Djava.io.tmpdir=${javaTmp}`, "-cp", jar, "tlc2.TLC", + "-config", cfg, "-workers", "1", "-metadir", join(dir, ".tlc-states"), "-cleanup", "-nowarning", + ...extraArgs, module, + ]; + const started = performance.now(); + const proc = Bun.spawn(argv, { cwd: dir, stdout: "pipe", stderr: "pipe" }); + const [stdout, stderr, exitCode] = await Promise.all([ + new Response(proc.stdout).text(), + new Response(proc.stderr).text(), + proc.exited, + ]); + const output = stdout + (stderr ? `\n[stderr]\n${stderr}` : ""); + writeFileSync(join(dir, "tlc.log"), output); + const violated = /Error: (?:Invariant|Action property) (\w+) is violated/.exec(output)?.[1] ?? null; + const distinct = /(\d+) distinct states found/.exec(output)?.[1]; + const depth = /The depth of the complete state graph search is (\d+)/.exec(output)?.[1]; + return { + exitCode, + output, + violated, + distinctStates: distinct ? Number(distinct) : null, + depth: depth ? Number(depth) : null, + argv, + durationMs: Math.round(performance.now() - started), + }; +} + +export function writeJson(path: string, value: unknown) { + mkdirSync(dirname(path), { recursive: true }); + writeFileSync(path, `${JSON.stringify(value, null, 2)}\n`); +} + +export function utcStamp(): string { + return new Date().toISOString().replace(/[-:]/g, "").replace(/\.\d+Z$/, "Z"); +} diff --git a/tests/tla/drivers/mcp/bridge.test.ts b/tests/tla/drivers/mcp/bridge.test.ts new file mode 100644 index 000000000..c758d5399 --- /dev/null +++ b/tests/tla/drivers/mcp/bridge.test.ts @@ -0,0 +1,108 @@ +// Bridge self-test. Real Zig traces from labs/trace_demo.zig plus hand-written +// controls, all checked by real TLC against tests/tla/mcp/selftest/Selftest.tla. +// +// bun test ./tests/tla/drivers/mcp/bridge.test.ts + +import { beforeAll, describe, expect, test } from "bun:test"; +import { mkdtempSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join, resolve } from "node:path"; +import { checkTrace, type TraceResult } from "./bridge"; + +const ROOT = resolve(import.meta.dir, "../../../.."); +const SPEC_DIR = join(ROOT, "tests/tla/mcp/selftest"); +const TIMEOUT = 60_000; + +let work: string; +let demo: string; +let counter = 0; + +beforeAll(() => { + work = mkdtempSync(join(tmpdir(), "mcpv2-bridge-test-")); + demo = join(work, "trace_demo"); + const build = Bun.spawnSync( + ["zig", "build-exe", "--dep", "mcp", "-Mroot=tests/tla/drivers/mcp/labs/trace_demo.zig", "-Mmcp=src/mcp/mcp.zig", "--name", "trace_demo", `-femit-bin=${demo}`], + { cwd: ROOT, stdout: "pipe", stderr: "pipe" }, + ); + if (build.exitCode !== 0) throw new Error(`zig build-exe failed: ${build.stderr.toString()}`); +}); + +function check(trace: string, machine = "selftest", wrapper = "SelftestTrace"): TraceResult { + counter += 1; + return checkTrace({ trace, machine, specDir: SPEC_DIR, wrapper, reportDir: join(work, `report-${counter}`) }); +} + +function zigTrace(...args: string[]): string { + counter += 1; + const path = join(work, `zig-${counter}.jsonl`); + const run = Bun.spawnSync([demo, path, ...args], { stdout: "pipe", stderr: "pipe" }); + if (run.exitCode !== 0) throw new Error(`trace_demo failed: ${run.stderr.toString()}`); + return path; +} + +function line(seq: number, event: string, from: string, to: string, outcomes: number): string { + return JSON.stringify({ v: 1, seq, machine: "selftest", inst: "demo", event, from, to, effects: [], data: { outcomes } }); +} + +function handTrace(contents: string): string { + counter += 1; + const path = join(work, `hand-${counter}.jsonl`); + writeFileSync(path, contents); + return path; +} + +describe("real Zig traces", () => { + test("a run that follows the model is ACCEPTED", () => { + const result = check(zigTrace("cancel_requested")); + expect(result.verdict).toBe("ACCEPTED"); + expect(result.matched).toBe(1); + }, TIMEOUT); + + test("events the machine refuses leave no step, and the rest is ACCEPTED", () => { + const result = check(zigTrace("response_received", "cancel_requested")); + expect(result.verdict).toBe("ACCEPTED"); + expect(result.steps).toBe(1); + }, TIMEOUT); + + test("the planted late-delivery bug is REJECTED at the bad step", () => { + const result = check(zigTrace("--allow-late-delivery", "cancel_requested", "response_received")); + expect(result.verdict).toBe("REJECTED"); + expect(result.steps).toBe(2); + expect(result.matched).toBe(1); + expect(result.reason).toContain("step 2 (response_received: cancelled -> done)"); + }, TIMEOUT); +}); + +describe("controls", () => { + test("an empty trace is INCONCLUSIVE", () => { + expect(check(handTrace("")).verdict).toBe("INCONCLUSIVE"); + }); + + test("a sequence gap is INCONCLUSIVE", () => { + const result = check(handTrace(`${line(1, "cancel_requested", "pending", "cancelled", 1)}\n${line(3, "response_received", "cancelled", "done", 2)}\n`)); + expect(result.verdict).toBe("INCONCLUSIVE"); + expect(result.reason).toContain("seq 3"); + }); + + test("a torn last line is INCONCLUSIVE", () => { + expect(check(handTrace(line(1, "cancel_requested", "pending", "cancelled", 1))).verdict).toBe("INCONCLUSIVE"); + }); + + test("a trace with no steps for the machine is INCONCLUSIVE", () => { + expect(check(handTrace(`${line(1, "cancel_requested", "pending", "cancelled", 1)}\n`), "other").verdict).toBe("INCONCLUSIVE"); + }); + + test("a wrong projected value is REJECTED", () => { + const result = check(handTrace(`${line(1, "cancel_requested", "pending", "cancelled", 5)}\n`)); + expect(result.verdict).toBe("REJECTED"); + expect(result.matched).toBe(0); + }, TIMEOUT); + + test("an unknown event is REJECTED", () => { + expect(check(handTrace(`${line(1, "teleported", "pending", "done", 1)}\n`)).verdict).toBe("REJECTED"); + }, TIMEOUT); + + test("a missing trace wrapper is TOOL_ERROR", () => { + expect(check(handTrace(`${line(1, "cancel_requested", "pending", "cancelled", 1)}\n`), "selftest", "NoSuchTrace").verdict).toBe("TOOL_ERROR"); + }); +}); diff --git a/tests/tla/drivers/mcp/bridge.ts b/tests/tla/drivers/mcp/bridge.ts new file mode 100644 index 000000000..c47b01431 --- /dev/null +++ b/tests/tla/drivers/mcp/bridge.ts @@ -0,0 +1,295 @@ +// Trace bridge for the MCP-v2 engine models in tests/tla/mcp/. +// +// Turns a JSONL step trace into a generated TLA+ module (TraceObs) and asks TLC +// whether it is a behavior of the machine's model, using a hand-written trace +// wrapper that EXTENDS the model and TraceObs. Acceptance uses the sentinel +// technique from sessions-v2: the wrapper's NotDone invariant is violated only +// once every observed step has been matched, and the matched count must equal +// the trace length. +// +// CLI: bun tests/tla/drivers/mcp/bridge.ts --trace --machine [--instance ] +// --spec-dir --wrapper --report-dir +// Exit: 0 ACCEPTED, 1 REJECTED, 2 INCONCLUSIVE, 3 TOOL_ERROR. + +import { createHash } from "node:crypto"; +import { copyFileSync, existsSync, mkdirSync, readFileSync, readdirSync, writeFileSync } from "node:fs"; +import { basename, join, resolve } from "node:path"; + +export type Verdict = "ACCEPTED" | "REJECTED" | "INCONCLUSIVE" | "TOOL_ERROR"; + +export const verdictExit: Record = { + ACCEPTED: 0, + REJECTED: 1, + INCONCLUSIVE: 2, + TOOL_ERROR: 3, +}; + +export interface TraceRequest { + trace: string; + machine: string; + instance?: string; + specDir: string; + wrapper: string; + reportDir: string; + /** Extra definitions for TraceObs, such as model constants the trace can't show. */ + constants?: { [name: string]: number }; +} + +export interface TraceResult { + verdict: Verdict; + reason: string; + steps: number; + matched: number | null; + reportDir: string; +} + +type DataValue = number | boolean | string; + +interface TraceLine { + v: number; + seq: number; + machine: string; + inst: string; + event: string; + from: string; + to: string; + effects: string[]; + data: { [name: string]: DataValue }; +} + +const TLC_SH = resolve(import.meta.dir, "../../lib/run-tlc.sh"); +const SENTINEL = "NotDone"; +const TLC_INT_MIN = -(2 ** 31); +const TLC_INT_MAX = 2 ** 31 - 1; +const TLA_IDENT = /^[A-Za-z_][A-Za-z0-9_]*$/; + +function sha256(bytes: string | Buffer): string { + return createHash("sha256").update(bytes).digest("hex"); +} + +class Inconclusive extends Error {} + +function parseTrace(text: string): TraceLine[] { + if (text.length === 0) throw new Inconclusive("trace is empty"); + if (!text.endsWith("\n")) throw new Inconclusive("last record is incomplete (no trailing newline)"); + const lines = text.slice(0, -1).split("\n"); + return lines.map((line, index) => { + const at = `line ${index + 1}`; + let value: unknown; + try { + value = JSON.parse(line); + } catch { + throw new Inconclusive(`${at} is not valid JSON`); + } + const r = value as TraceLine; + if (typeof r !== "object" || r === null) throw new Inconclusive(`${at} is not an object`); + if (r.v !== 1) throw new Inconclusive(`${at} has unsupported format version ${String(r.v)}`); + if (r.seq !== index + 1) throw new Inconclusive(`${at} has seq ${String(r.seq)}, expected ${index + 1}`); + for (const key of ["machine", "inst", "event", "from", "to"] as const) { + if (typeof r[key] !== "string") throw new Inconclusive(`${at} field ${key} is not a string`); + } + if (!Array.isArray(r.effects) || !r.effects.every((e) => typeof e === "string")) { + throw new Inconclusive(`${at} field effects is not a list of strings`); + } + if (typeof r.data !== "object" || r.data === null || Array.isArray(r.data)) { + throw new Inconclusive(`${at} field data is not an object`); + } + for (const [name, v] of Object.entries(r.data)) { + if (!TLA_IDENT.test(name)) throw new Inconclusive(`${at} data field ${JSON.stringify(name)} is not a TLA+ identifier`); + if (typeof v === "number" && (!Number.isInteger(v) || v < TLC_INT_MIN || v > TLC_INT_MAX)) { + throw new Inconclusive(`${at} data field ${name} is not a TLC integer`); + } + if (!["number", "boolean", "string"].includes(typeof v)) { + throw new Inconclusive(`${at} data field ${name} has unsupported type`); + } + } + return r; + }); +} + +function tlaString(s: string): string { + const escaped = s + .replace(/\\/g, "\\\\") + .replace(/"/g, '\\"') + .replace(/\n/g, "\\n") + .replace(/\r/g, "\\r") + .replace(/\t/g, "\\t"); + if (/[\x00-\x1f]/.test(escaped)) throw new Inconclusive("string contains an unsupported control character"); + return `"${escaped}"`; +} + +function tlaValue(v: DataValue): string { + if (typeof v === "boolean") return v ? "TRUE" : "FALSE"; + if (typeof v === "number") return String(v); + return tlaString(v); +} + +function observationModule(steps: TraceLine[], source: string, constants: { [name: string]: number }): string { + const definitions = Object.entries(constants).map(([name, value]) => { + if (!TLA_IDENT.test(name) || !Number.isInteger(value) || value < TLC_INT_MIN || value > TLC_INT_MAX) { + throw new Inconclusive(`constant ${name} = ${value} is not a TLA+ identifier and TLC integer`); + } + return `${name} == ${value}`; + }); + const rows = steps.map((r) => { + const fields = Object.entries(r.data); + const data = fields.length === 0 ? "<<>>" : `[${fields.map(([k, v]) => `${k} |-> ${tlaValue(v)}`).join(", ")}]`; + const effects = `<<${r.effects.map(tlaString).join(", ")}>>`; + return ` [event |-> ${tlaString(r.event)}, from |-> ${tlaString(r.from)}, to |-> ${tlaString(r.to)}, effects |-> ${effects}, data |-> ${data}]`; + }); + return [ + "---- MODULE TraceObs ----", + `\\* Generated by tests/tla/drivers/mcp/bridge.ts from ${basename(source)} (${steps.length} steps). Do not edit.`, + // Integers for negative values. + "EXTENDS Integers", + ...definitions, + "ObsTrace == <<", + rows.join(",\n"), + ">>", + "====", + "", + ].join("\n"); +} + +function finish(request: TraceRequest, result: Omit, extra: object = {}): TraceResult { + const full: TraceResult = { ...result, reportDir: request.reportDir }; + writeFileSync(join(request.reportDir, "verdict.json"), JSON.stringify({ ...full, ...extra }, null, 2) + "\n"); + return full; +} + +export function checkTrace(request: TraceRequest): TraceResult { + mkdirSync(request.reportDir, { recursive: true }); + writeFileSync(join(request.reportDir, "request.json"), JSON.stringify(request, null, 2) + "\n"); + + if (!existsSync(request.trace)) { + return finish(request, { verdict: "INCONCLUSIVE", reason: "trace file is missing", steps: 0, matched: null }); + } + const raw = readFileSync(request.trace); + writeFileSync(join(request.reportDir, "trace.jsonl"), raw); + + let steps: TraceLine[]; + try { + steps = parseTrace(raw.toString("utf8")).filter( + (r) => r.machine === request.machine && (request.instance === undefined || r.inst === request.instance), + ); + } catch (error) { + if (error instanceof Inconclusive) { + return finish(request, { verdict: "INCONCLUSIVE", reason: error.message, steps: 0, matched: null }); + } + throw error; + } + if (steps.length === 0) { + return finish(request, { + verdict: "INCONCLUSIVE", + reason: `no steps for machine ${request.machine}${request.instance ? ` instance ${request.instance}` : ""}`, + steps: 0, + matched: null, + }); + } + + const wrapperTla = join(request.specDir, `${request.wrapper}.tla`); + const wrapperCfg = join(request.specDir, `${request.wrapper}.cfg`); + if (!existsSync(wrapperTla) || !existsSync(wrapperCfg)) { + return finish(request, { + verdict: "TOOL_ERROR", + reason: `trace wrapper ${request.wrapper}.tla or .cfg not found in ${request.specDir}`, + steps: steps.length, + matched: null, + }); + } + + let observation: string; + try { + observation = observationModule(steps, request.trace, request.constants ?? {}); + } catch (error) { + if (error instanceof Inconclusive) { + return finish(request, { verdict: "INCONCLUSIVE", reason: error.message, steps: steps.length, matched: null }); + } + throw error; + } + + const modelDir = join(request.reportDir, "model"); + mkdirSync(modelDir, { recursive: true }); + const hashes: { [file: string]: string } = {}; + for (const name of readdirSync(request.specDir)) { + if (name.endsWith(".tla") || name.endsWith(".cfg")) { + copyFileSync(join(request.specDir, name), join(modelDir, name)); + hashes[name] = sha256(readFileSync(join(modelDir, name))); + } + } + writeFileSync(join(modelDir, "TraceObs.tla"), observation); + hashes["TraceObs.tla"] = sha256(observation); + hashes["trace.jsonl"] = sha256(raw); + + const tlc = Bun.spawnSync([TLC_SH, join(modelDir, `${request.wrapper}.tla`), join(modelDir, `${request.wrapper}.cfg`), "-deadlock"], { + stdout: "pipe", + stderr: "pipe", + }); + const output = tlc.stdout.toString() + tlc.stderr.toString(); + writeFileSync(join(request.reportDir, "tlc.log"), output); + const jar = /jar_sha256=([0-9a-f]{64})/.exec(output)?.[1] ?? null; + const extra = { tlcExit: tlc.exitCode, jarSha256: jar, hashes }; + + if (tlc.exitCode === 12 && output.includes(`Invariant ${SENTINEL} is violated`)) { + const values = [...output.matchAll(/\/\\ i = (\d+)/g)].map((m) => Number(m[1])); + const matched = values.length > 0 ? values[values.length - 1] : null; + if (matched === steps.length) { + return finish(request, { verdict: "ACCEPTED", reason: `all ${steps.length} steps are a behavior of the model`, steps: steps.length, matched }, extra); + } + return finish(request, { verdict: "TOOL_ERROR", reason: `sentinel reached at i=${matched}, expected ${steps.length}`, steps: steps.length, matched }, extra); + } + if (tlc.exitCode === 0 && output.includes("Model checking completed. No error has been found.")) { + // Search depth also counts a wrapper's hidden environment steps, so find + // the first step the model rejects by checking prefixes of the trace. + const accepts = (count: number): boolean => { + writeFileSync(join(modelDir, "TraceObs.tla"), observationModule(steps.slice(0, count), request.trace, request.constants ?? {})); + const run = Bun.spawnSync([TLC_SH, join(modelDir, `${request.wrapper}.tla`), join(modelDir, `${request.wrapper}.cfg`), "-deadlock"], { stdout: "pipe", stderr: "pipe" }); + return run.exitCode === 12 && (run.stdout.toString() + run.stderr.toString()).includes(`Invariant ${SENTINEL} is violated`); + }; + let matched = 0; + let rejected = steps.length; + while (rejected - matched > 1) { + const mid = Math.floor((matched + rejected) / 2); + if (accepts(mid)) matched = mid; + else rejected = mid; + } + writeFileSync(join(modelDir, "TraceObs.tla"), observation); + const next = steps[matched]; + const detail = `; step ${matched + 1} (${next.event}: ${next.from} -> ${next.to}) is not allowed`; + return finish(request, { verdict: "REJECTED", reason: `the model matches only ${matched} of ${steps.length} steps${detail}`, steps: steps.length, matched }, extra); + } + const firstError = output.split("\n").find((line) => /error/i.test(line)) ?? `TLC exit ${tlc.exitCode}`; + return finish(request, { verdict: "TOOL_ERROR", reason: firstError.trim(), steps: steps.length, matched: null }, extra); +} + +export function requireAccepted(result: TraceResult): void { + if (result.verdict !== "ACCEPTED") { + throw new Error(`trace ${result.verdict}: ${result.reason} (evidence: ${result.reportDir})`); + } +} + +if (import.meta.main) { + const args = process.argv.slice(2); + const get = (flag: string) => { + const index = args.indexOf(flag); + return index >= 0 ? args[index + 1] : undefined; + }; + const trace = get("--trace"); + const machine = get("--machine"); + const specDir = get("--spec-dir"); + const wrapper = get("--wrapper"); + const reportDir = get("--report-dir"); + if (!trace || !machine || !specDir || !wrapper || !reportDir) { + console.error("usage: bun tests/tla/drivers/mcp/bridge.ts --trace --machine [--instance ] --spec-dir --wrapper --report-dir [--constant Name=Value ...]"); + process.exit(verdictExit.TOOL_ERROR); + } + const constants: { [name: string]: number } = {}; + args.forEach((arg, index) => { + if (arg !== "--constant") return; + const [name, value] = (args[index + 1] ?? "").split("="); + constants[name] = Number(value); + }); + const result = checkTrace({ trace: resolve(trace), machine, instance: get("--instance"), specDir: resolve(specDir), wrapper, reportDir: resolve(reportDir), constants }); + console.log(JSON.stringify(result)); + process.exit(verdictExit[result.verdict]); +} diff --git a/tests/tla/drivers/mcp/driver.ts b/tests/tla/drivers/mcp/driver.ts new file mode 100644 index 000000000..559b53af3 --- /dev/null +++ b/tests/tla/drivers/mcp/driver.ts @@ -0,0 +1,230 @@ +// Bun driver for the MCP-v2 engine models in tests/tla/mcp/. +// +// Builds the binaries the selected scenarios need, runs each scenario with an +// isolated HOME and MCPV2_TRACE, checks every expected trace through the +// bridge, and keeps all evidence under ///, where is a +// fresh folder under FX_TLA_OUT or the system temp folder. +// +// Usage: bun tests/tla/drivers/mcp/driver.ts [--unit S05] [--case name] [--repeat N] [--next] [--list] +// +// The binaries are labs built from labs/ against this checkout's src/mcp/. +// Exit: 0 every case passed, 1 a case failed, 2 usage or tooling error. + +import { createHash } from "node:crypto"; +import { existsSync, mkdirSync, mkdtempSync, readFileSync, readdirSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join, resolve } from "node:path"; +import { checkTrace } from "./bridge"; +import type { Scenario, ScenarioContext } from "./scenario"; +import { REPO_ROOT, outDir } from "../lib/tlc"; + +const ROOT = REPO_ROOT; +const SCENARIO_DIR = join(import.meta.dir, "scenarios"); + +/** Binaries the driver knows how to build, by name. */ +const BUILDABLE: { [name: string]: string } = { + trace_demo: "tests/tla/drivers/mcp/labs/trace_demo.zig", + request_lab: "tests/tla/drivers/mcp/labs/request_lab.zig", + wire_lab: "tests/tla/drivers/mcp/labs/wire_lab.zig", + stdio_lab: "tests/tla/drivers/mcp/labs/stdio_lab.zig", + engine_lab: "tests/tla/drivers/mcp/labs/engine_lab.zig", +}; + +function sha256File(path: string): string { + return createHash("sha256").update(readFileSync(path)).digest("hex"); +} + +function runId(): string { + const stamp = new Date().toISOString().replace(/[-:]/g, "").replace(/\.\d+Z$/, "Z"); + return `${stamp}-${crypto.randomUUID().slice(0, 8)}`; +} + +async function loadScenarios(): Promise { + const all: Scenario[] = []; + for (const file of readdirSync(SCENARIO_DIR).filter((f) => f.endsWith(".ts")).sort()) { + const mod = await import(join(SCENARIO_DIR, file)); + all.push(...(mod.scenarios as Scenario[])); + } + const names = new Set(); + for (const s of all) { + if (names.has(s.name)) throw new Error(`duplicate scenario name ${s.name}`); + names.add(s.name); + } + return all; +} + +function build(names: string[], binDir: string): { [name: string]: { path: string; sha256: string } } { + mkdirSync(binDir, { recursive: true }); + const built: { [name: string]: { path: string; sha256: string } } = {}; + for (const name of names) { + const rootFile = BUILDABLE[name]; + if (!rootFile) throw new Error(`no build recipe for binary ${name}`); + if (!existsSync(join(ROOT, rootFile))) throw new Error(`binary ${name} needs ${rootFile}, which does not exist yet`); + const out = join(binDir, name); + const result = Bun.spawnSync( + ["zig", "build-exe", "-O", "ReleaseSafe", "-lc", "--dep", "mcp", `-Mroot=${rootFile}`, "-Mmcp=src/mcp/mcp.zig", "--name", name, `-femit-bin=${out}`], + { cwd: ROOT, stdout: "pipe", stderr: "pipe" }, + ); + if (result.exitCode !== 0) throw new Error(`building ${name} failed:\n${result.stderr.toString()}`); + built[name] = { path: out, sha256: sha256File(out) }; + } + return built; +} + +/** SHA-256 over the sorted ` ` lines of every Zig file in src/mcp/. */ +function treeHash(): string { + const files = (readdirSync(join(ROOT, "src", "mcp"), { recursive: true }) as string[]) + .filter((name) => name.endsWith(".zig")) + .map((name) => `src/mcp/${name}`) + .sort(); + const lines = files.map((file) => `${sha256File(join(ROOT, file))} ${file}\n`).join(""); + return createHash("sha256").update(lines).digest("hex"); +} + +interface CaseResult { + name: string; + unit: string; + attempt: number; + passed: boolean; + problems: string[]; + exit: number | null; + signal: string | null; + seconds: number; + traces: { machine: string; expected: string; verdict: string; reason: string; reportDir: string }[]; + evidence: string; +} + +function runCase(scenario: Scenario, attempt: number, bins: { [name: string]: string }, evidenceRun: string): CaseResult { + const caseDir = join(evidenceRun, attempt > 1 ? `${scenario.name}-${attempt}` : scenario.name); + mkdirSync(caseDir, { recursive: true }); + const scratch = mkdtempSync(join(tmpdir(), "mcpv2-case-")); + const ctx: ScenarioContext = { + root: ROOT, + bin: bins, + home: join(scratch, "home"), + workdir: join(scratch, "work"), + tracePath: join(caseDir, "trace.jsonl"), + caseDir, + }; + mkdirSync(ctx.home, { recursive: true }); + mkdirSync(ctx.workdir, { recursive: true }); + scenario.setup?.(ctx); + + const command = scenario.command(ctx); + const env = { + PATH: process.env.PATH ?? "/usr/bin:/bin", + HOME: ctx.home, + TMPDIR: scratch, + MCPV2_HOME: join(ctx.home, ".mcpv2"), + MCPV2_TRACE: ctx.tracePath, + }; + writeFileSync(join(caseDir, "scenario.json"), JSON.stringify({ ...scenario, command, env }, null, 2) + "\n"); + + const started = performance.now(); + const proc = Bun.spawnSync(command, { cwd: ctx.workdir, env, stdout: "pipe", stderr: "pipe", timeout: scenario.timeoutMs ?? 30_000 }); + const seconds = Math.round(performance.now() - started) / 1000; + writeFileSync(join(caseDir, "stdout.txt"), proc.stdout); + writeFileSync(join(caseDir, "stderr.txt"), proc.stderr); + const signal = proc.signalCode ?? null; + const exit = proc.exitCode ?? null; + writeFileSync(join(caseDir, "process.json"), JSON.stringify({ exit, signal, seconds }, null, 2) + "\n"); + + const problems: string[] = []; + if (signal !== null) problems.push(`process ended by signal ${signal}`); + if (exit !== scenario.expect.exit) problems.push(`exit ${exit}, expected ${scenario.expect.exit}`); + if (scenario.expect.stdout) { + const problem = scenario.expect.stdout(proc.stdout.toString()); + if (problem !== null) problems.push(`stdout: ${problem}`); + } + + const traces = scenario.expect.traces.map((t, index) => { + const result = checkTrace({ + trace: ctx.tracePath, + machine: t.machine, + instance: t.instance, + specDir: resolve(ROOT, t.specDir), + wrapper: t.wrapper, + reportDir: join(caseDir, `bridge-${index + 1}-${t.machine}`), + constants: t.constants, + }); + if (result.verdict !== t.verdict) problems.push(`trace ${t.machine}: ${result.verdict} (${result.reason}), expected ${t.verdict}`); + return { machine: t.machine, expected: t.verdict, verdict: result.verdict, reason: result.reason, reportDir: result.reportDir }; + }); + + rmSync(scratch, { recursive: true, force: true }); + const result: CaseResult = { name: scenario.name, unit: scenario.unit, attempt, passed: problems.length === 0, problems, exit, signal, seconds, traces, evidence: caseDir }; + writeFileSync(join(caseDir, "result.json"), JSON.stringify(result, null, 2) + "\n"); + return result; +} + +async function main(): Promise { + const args = process.argv.slice(2); + const values = (flag: string) => args.flatMap((a, i) => (a === flag && args[i + 1] ? [args[i + 1]] : [])); + const repeat = Number(values("--repeat")[0] ?? "1"); + if (!Number.isInteger(repeat) || repeat < 1) { + console.error("driver: --repeat must be a positive integer"); + return 2; + } + + let scenarios = await loadScenarios(); + const units = values("--unit"); + const cases = values("--case"); + if (units.length > 0) scenarios = scenarios.filter((s) => units.includes(s.unit)); + if (cases.length > 0) scenarios = scenarios.filter((s) => cases.includes(s.name)); + scenarios = scenarios.filter((s) => !s.real); + if (args.includes("--list")) { + for (const s of scenarios) console.log(`${s.unit} ${s.name.padEnd(36)} ${s.description}`); + return 0; + } + // engine_lab is written for the next MCP-v2 version and does not build + // against this checkout's src/mcp/ yet. Its scenarios run only with --next. + const nextOnly = (s: Scenario) => s.needs.includes("engine_lab"); + if (!args.includes("--next")) { + const later = scenarios.filter(nextOnly); + if (later.length > 0) console.log(`driver: skipping ${later.length} scenario(s) that need engine_lab (next MCP-v2 version); pass --next to run them`); + scenarios = scenarios.filter((s) => !nextOnly(s)); + } + if (scenarios.length === 0) { + console.error("driver: no scenarios selected"); + return 2; + } + + const id = runId(); + const out = outDir("mcp"); + const needs = [...new Set(scenarios.flatMap((s) => s.needs))].sort(); + const binDir = join(tmpdir(), `mcpv2-bin-${id}`); + const built = build(needs, binDir); + const environment = { runId: id, treeSha256: treeHash(), binaries: built, bun: Bun.version, args }; + const bins = Object.fromEntries(Object.entries(built).map(([name, b]) => [name, b.path])); + + const results: CaseResult[] = []; + for (const unit of [...new Set(scenarios.map((s) => s.unit))].sort()) { + const evidenceRun = join(out, unit); + mkdirSync(evidenceRun, { recursive: true }); + writeFileSync(join(evidenceRun, "environment.json"), JSON.stringify(environment, null, 2) + "\n"); + const mine: CaseResult[] = []; + for (const scenario of scenarios.filter((s) => s.unit === unit)) { + for (let attempt = 1; attempt <= repeat; attempt++) { + const r = runCase(scenario, attempt, bins, evidenceRun); + mine.push(r); + const label = repeat > 1 ? `${r.name} #${attempt}` : r.name; + console.log(`${r.passed ? "PASS" : "FAIL"} ${unit} ${label.padEnd(36)} exit=${r.exit} ${r.traces.map((t) => `${t.machine}=${t.verdict}`).join(" ")}`); + for (const p of r.problems) console.log(` ${p}`); + } + } + writeFileSync(join(evidenceRun, "summary.json"), JSON.stringify(mine, null, 2) + "\n"); + console.log(`Summary: ${join(evidenceRun, "summary.json")}`); + results.push(...mine); + } + rmSync(binDir, { recursive: true, force: true }); + return results.every((r) => r.passed) ? 0 : 1; +} + +if (import.meta.main) { + main() + .then((code) => process.exit(code)) + .catch((error) => { + console.error(`driver: tooling error: ${error instanceof Error ? error.message : String(error)}`); + process.exit(2); + }); +} diff --git a/tests/tla/drivers/mcp/fakes/browser.ts b/tests/tla/drivers/mcp/fakes/browser.ts new file mode 100644 index 000000000..cf29029d1 --- /dev/null +++ b/tests/tla/drivers/mcp/fakes/browser.ts @@ -0,0 +1,35 @@ +// A stand-in browser for `mcpv2 auth --json` (U12). Runs the command and +// passes its output through. When it prints {"authorize": url}, it requests +// url without following the redirect, then goes to the redirect's address +// itself, as a browser would: mcpv2's loopback listener. With --deny it goes +// back with access_denied instead of the code, as a user who refuses. +// Exits with the command's exit code. +// +// Usage: bun tests/tla/drivers/mcp/fakes/browser.ts [--deny] -- + +const args = process.argv.slice(2); +const deny = args[0] === "--deny"; +const child = Bun.spawn(args.slice(args.indexOf("--") + 1), { stdin: "ignore", stdout: "pipe", stderr: "inherit" }); +const decoder = new TextDecoder(); +let pending = ""; +for await (const chunk of child.stdout) { + const text = decoder.decode(chunk, { stream: true }); + process.stdout.write(text); + pending += text; + for (let nl = pending.indexOf("\n"); nl >= 0; nl = pending.indexOf("\n")) { + const line = pending.slice(0, nl); + pending = pending.slice(nl + 1); + let url: unknown; + try { + url = JSON.parse(line).authorize; + } catch {} + if (typeof url !== "string") continue; + const back = new URL((await fetch(url, { redirect: "manual" })).headers.get("location") ?? ""); + if (deny) { + back.searchParams.delete("code"); + back.searchParams.set("error", "access_denied"); + } + await fetch(back); + } +} +process.exit(await child.exited); diff --git a/tests/tla/drivers/mcp/fakes/http.ts b/tests/tla/drivers/mcp/fakes/http.ts new file mode 100644 index 000000000..5feae1864 --- /dev/null +++ b/tests/tla/drivers/mcp/fakes/http.ts @@ -0,0 +1,292 @@ +// Scripted fake Streamable HTTP MCP server (U06, U07), like fakes/stdio.ts. +// +// Listens on 127.0.0.1 at a free port and prints {"listening": } first. +// Every POST request is matched against the rules in order: the first rule +// whose method (and, if given, version, cursor, or tool name) matches and +// still has uses left answers it. An unmatched request gets 404 with -32601 +// (the 2026 answer for an unknown method); notifications and replies get 202. +// Every request is logged with its headers to --log as JSONL, and so is every +// stream the client closes early. +// +// 2025 sessions (U07), with --session: initialize's answer assigns +// `Mcp-Session-Id: s`. Later requests without it get 400, and with an +// ended or unknown one 404 with a JSON-RPC error and no id, as the TypeScript +// SDK answers. A rule's `endSession` ends the session after answering. SSE +// answers may carry event ids (`ids`), a `retry`, and `poll` closes the stream +// after its first events, keeping the answer: a GET with Last-Event-ID gets +// it. A GET without one is the listening stream (--listen 405|open|close). +// DELETE ends the session (--delete-status, 200 by default). +// +// OAuth (U09), with --auth : see fakes/oauth.ts. Its endpoints are +// answered first, and the MCP endpoint's gate runs before any rule. +// +// Usage: bun tests/tla/drivers/mcp/fakes/http.ts --script [--log ] +// [--session | --no-session-id] [--listen 405|open|close] [--delete-status ] +// [--initialized-delay ] [--auth ] + +import { appendFileSync, readFileSync } from "node:fs"; +import { createAuth, type AuthConfig } from "./oauth"; + +export interface HttpRule { + method: string; + times?: number; + /** Match the 2026 `_meta` protocol version; null matches none sent. */ + version?: string | null; + cursor?: string | null; + /** Match `params.name` (tools/call). */ + name?: string; + /** HTTP status, 200 by default. */ + status?: number; + /** Answer as an SSE stream instead of a JSON body. */ + sse?: boolean; + /** Messages sent before the answer (SSE only), such as progress notifications. */ + before?: unknown[]; + result?: unknown; + error?: { code: number; message: string; data?: unknown }; + /** A raw body instead of a JSON-RPC answer, with this content type. */ + raw?: string; + contentType?: string; + /** Wait before answering, in milliseconds. */ + delayMs?: number; + /** SSE: send the `before` messages, then break the stream without an answer. */ + drop?: boolean; + /** SSE: send the `before` messages, then keep the stream open without an answer. */ + hang?: boolean; + /** Extra response headers. */ + headers?: Record; + /** SSE: give every event an id (`-`), starting with a priming event. */ + ids?: boolean; + /** SSE: the `retry` field sent with the first event. */ + retry?: number; + /** SSE: close the stream after the first events without the answer; a GET with Last-Event-ID resumes it. */ + poll?: boolean; + /** 2025: end the session after answering. */ + endSession?: boolean; + /** SSE messages sent `laterMs` (default 300) after `before`, on a stream left open (U10). */ + later?: unknown[]; + laterMs?: number; + /** SSE (U11): after `before`, wait for the client's replies to the requests in it (at most `awaitMs`, default 5000). */ + awaitReply?: boolean; + awaitMs?: number; + /** Messages sent on the open listening GET stream `laterMs` after the rule fired (U11). */ + listenLater?: unknown[]; + /** SSE: send the answer, then leave the stream open, as some servers do. */ + keepOpen?: boolean; +} + +interface Message { + jsonrpc?: string; + id?: string | number | null; + method?: string; + params?: { _meta?: Record; cursor?: string; name?: string }; +} + +const args = process.argv.slice(2); +const get = (flag: string) => { + const index = args.indexOf(flag); + return index >= 0 ? args[index + 1] : undefined; +}; +const rules = JSON.parse(readFileSync(get("--script") ?? "/dev/null", "utf8") || "[]") as HttpRule[]; +const used = rules.map(() => 0); +const logPath = get("--log"); +const sessions = args.includes("--session"); +// Without --session, answers carry a fixed session id (2026 clients must ignore it) unless --no-session-id. +const noSessionId = args.includes("--no-session-id"); +const listenMode = get("--listen") ?? "405"; +const deleteStatus = Number(get("--delete-status") ?? "200"); +// Holds the 202 to notifications/initialized this long, logging when it was answered. +const initializedDelay = Number(get("--initialized-delay") ?? "0"); +// Holds the listening GET's head this long (U11). +const listenDelay = Number(get("--listen-delay") ?? "0"); +const log = (entry: object) => { + if (logPath) appendFileSync(logPath, JSON.stringify({ t: Date.now(), ...entry }) + "\n"); +}; + +const authPath = get("--auth"); +const auth = authPath ? createAuth(JSON.parse(readFileSync(authPath, "utf8")) as AuthConfig, () => `http://127.0.0.1:${server.port}`, log) : null; + +// A rule's result and SSE messages may say "$id" for the request's id, as a +// listen's subscriptionId must (U10). +const withId = (value: T, id: unknown): T => JSON.parse(JSON.stringify(value).replaceAll('"$id"', JSON.stringify(id ?? null))); + +const encoder = new TextEncoder(); +const sseEvent = (message: unknown, id?: string, retry?: number) => + encoder.encode(`${retry !== undefined ? `retry: ${retry}\n` : ""}${id !== undefined ? `id: ${id}\n` : ""}event: message\ndata: ${message === undefined ? "" : JSON.stringify(message)}\n\n`); + +// 2025 sessions. +let sessionCount = 0; +let currentSession: string | null = null; +const ended = new Set(); +// Streams kept for a GET with Last-Event-ID: stream name -> the answer still to send. +const kept = new Map(); +let streamCount = 0; +// The open listening GET stream, for `listenLater` (U11). +let listenController: ReadableStreamDefaultController | null = null; +// Replies to the server's requests that a rule waits for: JSON of the id -> resolve. +const replies = new Map void>(); + +function sessionProblem(req: Request, initialize: boolean): Response | null { + if (!sessions || initialize) return null; + const id = req.headers.get("mcp-session-id"); + if (!id) return new Response("Bad Request: No valid session ID provided", { status: 400 }); + if (id !== currentSession || ended.has(id)) + return Response.json({ jsonrpc: "2.0", error: { code: -32001, message: "Session not found" }, id: null }, { status: 404 }); + return null; +} + +const server = Bun.serve({ + hostname: "127.0.0.1", + port: 0, + idleTimeout: 0, + async fetch(req) { + const headers = Object.fromEntries(req.headers.entries()); + const routed = auth ? await auth.route(req) : null; + if (routed) return routed; + if (req.method === "DELETE") { + log({ dir: "in", httpMethod: "DELETE", headers }); + const denied = auth?.check(req, "DELETE"); + if (denied) return denied; + const problem = sessionProblem(req, false); + if (problem) return problem; + if (currentSession) ended.add(currentSession); + return new Response(null, { status: deleteStatus }); + } + if (req.method === "GET") { + log({ dir: "in", httpMethod: "GET", headers }); + const deniedGet = auth?.check(req, "GET"); + if (deniedGet) return deniedGet; + const problem = sessionProblem(req, false); + if (problem) return problem; + const last = req.headers.get("last-event-id"); + if (last) { + const name = last.slice(0, last.lastIndexOf("-")); + const stream = kept.get(name); + if (!stream) return new Response("Unknown stream", { status: 400 }); + kept.delete(name); + return new Response(sseEvent(stream.answer, `${name}-${stream.next}`), { headers: { "content-type": "text/event-stream" } }); + } + if (listenMode === "405") return new Response("Method Not Allowed", { status: 405 }); + const name = `listen${++streamCount}`; + const body = new ReadableStream({ + start(controller) { + listenController = controller; + controller.enqueue(sseEvent(undefined, `${name}-0`)); + if (listenMode === "close") controller.close(); + }, + cancel() { + listenController = null; + log({ dir: "closed", stream: name }); + }, + }); + if (listenDelay > 0) await Bun.sleep(listenDelay); + log({ dir: "listen_open", stream: name }); + return new Response(body, { headers: { "content-type": "text/event-stream" } }); + } + if (req.method !== "POST") { + log({ dir: "in", httpMethod: req.method, headers }); + return new Response("Method Not Allowed", { status: 405 }); + } + const text = await req.text(); + log({ dir: "in", httpMethod: "POST", headers, body: text }); + let message: Message; + try { + message = JSON.parse(text) as Message; + } catch { + return Response.json({ jsonrpc: "2.0", id: null, error: { code: -32700, message: "Parse error" } }, { status: 400 }); + } + const denied = auth?.check(req, message.method); + if (denied) return denied; + const problem = sessionProblem(req, message.method === "initialize"); + if (problem) return problem; + // Notifications and replies to server requests. + if (message.id === undefined || message.method === undefined) { + if (message.method === undefined && message.id !== undefined) replies.get(JSON.stringify(message.id))?.(); + if (message.method === "notifications/initialized" && initializedDelay > 0) { + await Bun.sleep(initializedDelay); + log({ dir: "answered", method: message.method }); + } + return new Response(null, { status: 202 }); + } + const version = message.params?._meta?.["io.modelcontextprotocol/protocolVersion"] ?? null; + const index = rules.findIndex( + (r, i) => + r.method === message.method && + (r.version === undefined || r.version === version) && + (r.cursor === undefined || r.cursor === (message.params?.cursor ?? null)) && + (r.name === undefined || r.name === message.params?.name) && + (r.times === undefined || used[i] < r.times), + ); + if (index < 0) return Response.json({ jsonrpc: "2.0", id: message.id ?? null, error: { code: -32601, message: "Method not found" } }, { status: 404 }); + used[index] += 1; + const rule = rules[index]; + if (rule.listenLater) { + const messages = rule.listenLater; + setTimeout(() => { + for (const m of messages) listenController?.enqueue(sseEvent(m)); + }, rule.laterMs ?? 300); + } + if (rule.delayMs) await Bun.sleep(rule.delayMs); + const status = rule.status ?? 200; + const extra: Record = { ...(rule.headers ?? {}) }; + if (sessions && message.method === "initialize" && status === 200 && !rule.error) { + currentSession = `s${++sessionCount}`; + extra["mcp-session-id"] = currentSession; + } else if (!sessions && !noSessionId && !("mcp-session-id" in extra)) extra["mcp-session-id"] = "fake-session"; + if (rule.endSession && currentSession) ended.add(currentSession); + if (rule.raw !== undefined) return new Response(rule.raw, { status, headers: { "content-type": rule.contentType ?? "text/plain", ...extra } }); + const answer = rule.error ? { jsonrpc: "2.0", id: message.id ?? null, error: rule.error } : { jsonrpc: "2.0", id: message.id ?? null, result: withId(rule.result ?? {}, message.id) }; + if (!rule.sse) return Response.json(answer, { status, headers: extra }); + const id = message.id; + const name = `stream${++streamCount}`; + let n = 0; + const nextId = () => (rule.ids ? `${name}-${n++}` : undefined); + const stream = new ReadableStream({ + async start(controller) { + controller.enqueue(encoder.encode(": keep-alive\n\n")); + if (rule.ids) controller.enqueue(sseEvent(undefined, nextId(), rule.retry)); + else if (rule.retry !== undefined) controller.enqueue(encoder.encode(`retry: ${rule.retry}\n\n`)); + const asked: Promise[] = []; + for (const m of rule.before ?? []) { + const msg = withId(m, id) as Message; + if (rule.awaitReply && msg.method !== undefined && msg.id !== undefined) { + asked.push(new Promise((resolve) => replies.set(JSON.stringify(msg.id), resolve))); + } + controller.enqueue(sseEvent(msg, nextId())); + } + if (asked.length > 0) { + await Promise.race([Promise.all(asked), Bun.sleep(rule.awaitMs ?? 5000)]); + log({ dir: "replied", id }); + } + if (rule.later) { + await Bun.sleep(rule.laterMs ?? 300); + for (const m of rule.later) controller.enqueue(sseEvent(withId(m, id), nextId())); + } + if (rule.drop) { + await Bun.sleep(20); + controller.error(new Error("dropped by the fake server")); + return; + } + if (rule.hang) return; + if (rule.poll) { + kept.set(name, { answer, next: n }); + await Bun.sleep(20); + controller.close(); + return; + } + controller.enqueue(sseEvent(answer, nextId())); + if (!rule.keepOpen) controller.close(); + }, + cancel() { + log({ dir: "closed", id }); + }, + }); + req.signal.addEventListener("abort", () => log({ dir: "aborted", id })); + return new Response(stream, { status, headers: { "content-type": "text/event-stream", "cache-control": "no-cache", ...extra } }); + }, +}); + +console.log(JSON.stringify({ listening: server.port })); +process.on("SIGTERM", () => { + server.stop(true); + process.exit(0); +}); diff --git a/tests/tla/drivers/mcp/fakes/oauth.ts b/tests/tla/drivers/mcp/fakes/oauth.ts new file mode 100644 index 000000000..f9179c9cb --- /dev/null +++ b/tests/tla/drivers/mcp/fakes/oauth.ts @@ -0,0 +1,236 @@ +// Scripted fake OAuth for tests/tla/drivers/mcp/fakes/http.ts (U09): protected resource +// metadata for the MCP endpoint, and authorization servers at /as1, /as2, ..., +// each with metadata, /authorize, /token, and /register. The MCP endpoint's +// gate answers 401 with a challenge without a valid token, and 403 +// insufficient_scope when the token lacks a method's scopes. +// +// /authorize approves at once and redirects to the client's redirect_uri with +// a code, the state, and iss as configured; nothing is ever sent to that URI. +// The token endpoint checks the code, the PKCE verifier, the redirect URI, and +// resource; refresh tokens rotate unless told not to. Tokens can be limited to +// a number of uses, and after a number of tokens the resource metadata can +// name the next server, whose server then rejects the old ones (migration). +// Every auth request is logged as {dir: "auth", path, query, form, json, +// authorization}. + +export interface AuthServer { + /** Where its metadata is: RFC 8414's well-known URI, or OpenID's appended to its path. */ + metadata?: "oauth" | "oidc"; + /** The metadata's issuer, if not its own URL. */ + issuer?: string; + /** List S256 (default true). */ + pkce?: boolean; + /** authorization_response_iss_parameter_supported (default true). */ + issSupported?: boolean; + /** What the redirect's iss is (default correct). */ + iss?: "correct" | "omit" | "wrong"; + /** A registration endpoint (default true). */ + dcr?: boolean; + scopesSupported?: string[]; + expiresIn?: number; + /** Issue refresh tokens (default true), rotated (default true). */ + refresh?: boolean; + rotate?: boolean; + /** Answer every refresh with 400 and this error. */ + refreshError?: string; + /** The token endpoint is plain HTTP to another host. */ + insecureEndpoint?: boolean; + /** The token endpoint is on an internal address: 0.0.0.0, which reaches this machine, on port 1. */ + internalEndpoint?: boolean; + /** The only scopes it grants, whatever is asked. */ + grantOnly?: string[]; + /** Deny every authorization request with error=access_denied and this description. */ + deny?: string; + /** A revocation endpoint (RFC 7009); a revoked token is forgotten. */ + revoke?: boolean; + /** Refuse every authorization code at the token endpoint with this error. */ + codeError?: { error: string; description?: string }; + /** The token_type its tokens carry, instead of Bearer. */ + tokenType?: string; + /** Appended to every access token it issues, such as "\r\n". */ + tokenSuffix?: string; +} + +export interface AuthConfig { + /** Where the resource metadata is: "path" (default), "root", or a path. */ + prm?: string; + /** resource_metadata in the challenge (default true), or this URL instead. */ + inChallenge?: boolean; + /** "foreign": the same metadata URL on another origin (localhost for 127.0.0.1). */ + challengeUrl?: string; + /** The resource metadata's resource, if not the endpoint's URL. */ + resource?: string; + /** The resource metadata names this authorization server instead of its own. */ + authorizationServer?: string; + scopesSupported?: string[]; + /** The 401 challenge's scope. */ + challengeScope?: string; + /** Scopes a token needs per method. */ + requiredScopes?: Record; + servers: AuthServer[]; + /** After this many tokens, the resource metadata names the next server. */ + migrateAfterTokens?: number; + /** Each access token is accepted this many times. */ + tokenUses?: number; +} + +type Log = (entry: object) => void; + +interface Token { + server: number; + scopes: string[]; + uses: number; +} + +export function createAuth(config: AuthConfig, base: () => string, log: Log) { + let active = 0; + let tokens = 0; + let clients = 0; + const access = new Map(); + const refresh = new Map(); + const codes = new Map(); + const prmPath = config.prm === undefined || config.prm === "path" ? "/.well-known/oauth-protected-resource/mcp" : config.prm === "root" ? "/.well-known/oauth-protected-resource" : config.prm; + const prmUrl = () => base() + prmPath; + const serverUrl = (i: number) => `${base()}/as${i + 1}`; + const issuerOf = (i: number) => config.servers[i].issuer ?? serverUrl(i); + + function challenge(error?: string, scope?: string): string { + const parts = ["Bearer"]; + const params: string[] = []; + if (error) params.push(`error="${error}"`); + if (scope) params.push(`scope="${scope}"`); + const url = config.challengeUrl === "foreign" ? prmUrl().replace("127.0.0.1", "localhost") : (config.challengeUrl ?? prmUrl()); + if (config.inChallenge !== false) params.push(`resource_metadata="${url}"`); + return parts.concat(params.join(", ")).join(" "); + } + + function metadata(i: number) { + const s = config.servers[i]; + const url = serverUrl(i); + return { + issuer: issuerOf(i), + authorization_endpoint: `${url}/authorize`, + token_endpoint: s.insecureEndpoint ? "http://auth.example.com/token" : s.internalEndpoint ? "https://0.0.0.0:1/token" : `${url}/token`, + ...(s.dcr === false ? {} : { registration_endpoint: `${url}/register` }), + ...(s.revoke ? { revocation_endpoint: `${url}/revoke` } : {}), + response_types_supported: ["code"], + grant_types_supported: ["authorization_code", "refresh_token"], + ...(s.pkce === false ? {} : { code_challenge_methods_supported: ["S256"] }), + ...(s.issSupported === false ? {} : { authorization_response_iss_parameter_supported: true }), + token_endpoint_auth_methods_supported: ["none"], + ...(s.scopesSupported ? { scopes_supported: s.scopesSupported } : {}), + }; + } + + function issue(server: number, scopes: string[]) { + const s = config.servers[server]; + tokens += 1; + const at = `at${tokens}${s.tokenSuffix ?? ""}`; + access.set(at, { server, scopes, uses: 0 }); + const body: Record = { access_token: at, token_type: s.tokenType ?? "Bearer", expires_in: s.expiresIn ?? 3600, scope: scopes.join(" ") }; + if (s.refresh !== false) { + const rt = `rt${tokens}`; + refresh.set(rt, { server, scopes }); + body.refresh_token = rt; + } + if (config.migrateAfterTokens !== undefined && tokens >= config.migrateAfterTokens && active + 1 < config.servers.length) active += 1; + return body; + } + + async function sha256url(text: string): Promise { + const digest = new Uint8Array(await crypto.subtle.digest("SHA-256", new TextEncoder().encode(text))); + return Buffer.from(digest).toString("base64url"); + } + + return { + /** An auth endpoint's answer, or null for the MCP endpoint. */ + async route(req: Request): Promise { + const url = new URL(req.url); + const path = url.pathname; + if (path === prmPath && req.method === "GET") { + log({ dir: "auth", path, host: req.headers.get("host"), encoding: req.headers.get("accept-encoding") }); + return Response.json({ resource: config.resource ?? `${base()}/mcp`, authorization_servers: [config.authorizationServer ?? issuerOf(active)], ...(config.scopesSupported ? { scopes_supported: config.scopesSupported } : {}) }); + } + const m = path.match(/^(?:\/\.well-known\/(oauth-authorization-server|openid-configuration))?\/as(\d+)(\/.*)?$/); + if (!m) return null; + const i = Number(m[2]) - 1; + const s = config.servers[i]; + if (!s) return null; + const rest = m[3] ?? ""; + const form = req.method === "POST" && (req.headers.get("content-type") ?? "").includes("form") ? Object.fromEntries(new URLSearchParams(await req.text())) : undefined; + const json = req.method === "POST" && (req.headers.get("content-type") ?? "").includes("json") ? await req.json() : undefined; + log({ dir: "auth", path, host: req.headers.get("host"), encoding: req.headers.get("accept-encoding"), query: Object.fromEntries(url.searchParams), form, json, authorization: req.headers.get("authorization") }); + const wellKnown = m[1] ?? (rest === "/.well-known/openid-configuration" ? "openid-configuration-appended" : undefined); + if (wellKnown) { + const want = s.metadata === "oidc" ? "openid-configuration-appended" : "oauth-authorization-server"; + return wellKnown === want ? Response.json(metadata(i)) : new Response("Not Found", { status: 404 }); + } + if (rest === "/authorize") { + const q = url.searchParams; + const code = `code${codes.size + 1}`; + codes.set(code, { server: i, challenge: q.get("code_challenge") ?? "", redirect: q.get("redirect_uri") ?? "", scopes: (q.get("scope") ?? "").split(" ").filter(Boolean), resource: q.get("resource") ?? "" }); + const back = new URL(q.get("redirect_uri") ?? "http://invalid/"); + if (s.deny) { + back.searchParams.set("error", "access_denied"); + back.searchParams.set("error_description", s.deny); + } else back.searchParams.set("code", code); + if (q.get("state")) back.searchParams.set("state", q.get("state")!); + const iss = s.iss ?? "correct"; + if (iss === "correct") back.searchParams.set("iss", issuerOf(i)); + if (iss === "wrong") back.searchParams.set("iss", "https://evil.example.com"); + return Response.redirect(back.toString(), 302); + } + if (rest === "/register" && req.method === "POST") { + clients += 1; + return Response.json({ client_id: `client${clients}-as${i + 1}`, token_endpoint_auth_method: "none", redirect_uris: json?.redirect_uris ?? [] }, { status: 201 }); + } + if (rest === "/revoke" && req.method === "POST" && form && s.revoke) { + refresh.delete(form.token); + access.delete(form.token); + return new Response(null, { status: 200 }); + } + if (rest === "/token" && req.method === "POST" && form) { + if (form.grant_type === "authorization_code") { + const c = codes.get(form.code); + codes.delete(form.code); + if (s.codeError) { + const { error, description } = s.codeError; + return Response.json(description === undefined ? { error } : { error, error_description: description }, { status: 400 }); + } + if (!c || c.server !== i || c.redirect !== form.redirect_uri || !form.resource || c.challenge !== (await sha256url(form.code_verifier ?? ""))) + return Response.json({ error: "invalid_grant" }, { status: 400 }); + return Response.json(issue(i, s.grantOnly ? c.scopes.filter((x) => s.grantOnly!.includes(x)) : c.scopes)); + } + if (form.grant_type === "refresh_token") { + if (s.refreshError) return Response.json({ error: s.refreshError }, { status: 400 }); + const r = refresh.get(form.refresh_token); + if (!r || r.server !== i || !form.resource) return Response.json({ error: "invalid_grant" }, { status: 400 }); + const body = issue(i, r.scopes); + if (s.rotate === false) { + refresh.delete(body.refresh_token as string); + delete body.refresh_token; + } else refresh.delete(form.refresh_token); + return Response.json(body); + } + return Response.json({ error: "unsupported_grant_type" }, { status: 400 }); + } + return new Response("Not Found", { status: 404 }); + }, + + /** The gate in front of the MCP endpoint: an answer for a request it refuses. */ + check(req: Request, method: string | undefined): Response | null { + const header = req.headers.get("authorization") ?? ""; + const t = header.startsWith("Bearer ") ? access.get(header.slice(7)) : undefined; + const limit = config.tokenUses ?? Infinity; + if (!t || t.server !== active || t.uses >= limit) { + return Response.json({ error: "invalid_token" }, { status: 401, headers: { "www-authenticate": challenge(undefined, config.challengeScope) } }); + } + const needed = (method && config.requiredScopes?.[method]) ?? []; + if (!needed.every((n) => t.scopes.includes(n))) { + return Response.json({ error: "insufficient_scope" }, { status: 403, headers: { "www-authenticate": challenge("insufficient_scope", needed.join(" ")) } }); + } + t.uses += 1; + return null; + }, + }; +} diff --git a/tests/tla/drivers/mcp/fakes/stdio.test.ts b/tests/tla/drivers/mcp/fakes/stdio.test.ts new file mode 100644 index 000000000..ccdd5198d --- /dev/null +++ b/tests/tla/drivers/mcp/fakes/stdio.test.ts @@ -0,0 +1,115 @@ +// Tests for the scripted fake stdio server. +// +// bun test ./tests/tla/drivers/mcp/fakes/stdio.test.ts + +import { afterEach, expect, test } from "bun:test"; +import { mkdtempSync, readFileSync, rmSync, writeFileSync } from "node:fs"; +import { tmpdir } from "node:os"; +import { join } from "node:path"; +import type { Rule } from "./stdio"; + +const SERVER = join(import.meta.dir, "stdio.ts"); +let dirs: string[] = []; + +afterEach(() => { + for (const d of dirs) rmSync(d, { recursive: true, force: true }); + dirs = []; +}); + +async function exchange(rules: Rule[], lines: string[], flags: string[] = []) { + const dir = mkdtempSync(join(tmpdir(), "mcpv2-fake-stdio-")); + dirs.push(dir); + const script = join(dir, "rules.json"); + const log = join(dir, "log.jsonl"); + writeFileSync(script, JSON.stringify(rules)); + const proc = Bun.spawn([process.execPath, SERVER, "--script", script, "--log", log, ...flags], { stdin: "pipe", stdout: "pipe", stderr: "pipe" }); + for (const line of lines) proc.stdin.write(line + "\n"); + proc.stdin.end(); + const exit = await proc.exited; + const parse = (l: string) => { + try { + return JSON.parse(l); + } catch { + return l; // deliberately malformed output from a `raw` rule + } + }; + const out = (await new Response(proc.stdout).text()).split("\n").filter(Boolean).map(parse); + const logged = readFileSync(log, "utf8").split("\n").filter(Boolean).map((l) => JSON.parse(l)); + return { exit, out, logged }; +} + +const request = (id: number, method: string) => JSON.stringify({ jsonrpc: "2.0", id, method, params: {} }); + +test("answers a matching request with the scripted result and copies the id", async () => { + const { exit, out } = await exchange([{ method: "server/discover", result: { supportedVersions: ["2026-07-28"] } }], [request(7, "server/discover")]); + expect(exit).toBe(0); + expect(out).toEqual([{ jsonrpc: "2.0", id: 7, result: { supportedVersions: ["2026-07-28"] } }]); +}); + +test("answers an unmatched request with -32601 and ignores notifications", async () => { + const { out } = await exchange([], [request(1, "tools/list"), JSON.stringify({ jsonrpc: "2.0", method: "notifications/initialized" })]); + expect(out).toEqual([{ jsonrpc: "2.0", id: 1, error: { code: -32601, message: "Method not found" } }]); +}); + +test("rules with a use limit fall through to the next matching rule", async () => { + const rules: Rule[] = [ + { method: "tools/list", times: 1, error: { code: -32022, message: "Unsupported protocol version", data: { supported: ["2025-11-25"] } } }, + { method: "tools/list", result: { tools: [] } }, + ]; + const { out } = await exchange(rules, [request(1, "tools/list"), request(2, "tools/list")]); + expect(out[0].error.code).toBe(-32022); + expect(out[1]).toEqual({ jsonrpc: "2.0", id: 2, result: { tools: [] } }); +}); + +test("can send notifications before the reply, raw malformed lines, and crash", async () => { + const rules: Rule[] = [ + { method: "tools/call", times: 1, before: [{ jsonrpc: "2.0", method: "notifications/progress", params: { progressToken: 1, progress: 1 } }], result: { content: [] } }, + { method: "tools/call", raw: "{not json", then: "crash" }, + ]; + const proc = await exchange(rules, [request(1, "tools/call"), request(2, "tools/call"), request(3, "tools/call")]); + expect(proc.exit).toBe(1); + expect(proc.out[proc.out.length - 1]).toBe("{not json"); + const lines = proc.logged.filter((l) => l.dir === "out").map((l) => l.line); + expect(lines).toEqual([ + JSON.stringify({ jsonrpc: "2.0", method: "notifications/progress", params: { progressToken: 1, progress: 1 } }), + JSON.stringify({ jsonrpc: "2.0", id: 1, result: { content: [] } }), + "{not json", + ]); + expect(proc.logged.filter((l) => l.dir === "in").length).toBeGreaterThanOrEqual(2); +}); + +test("rules can match the request's 2026 protocol version, or its absence", async () => { + const rules: Rule[] = [ + { method: "tools/list", version: "2026-07-28", result: { era: "modern" } }, + { method: "tools/list", version: null, result: { era: "legacy" } }, + ]; + const modern = JSON.stringify({ jsonrpc: "2.0", id: 1, method: "tools/list", params: { _meta: { "io.modelcontextprotocol/protocolVersion": "2026-07-28" } } }); + const other = JSON.stringify({ jsonrpc: "2.0", id: 2, method: "tools/list", params: { _meta: { "io.modelcontextprotocol/protocolVersion": "2027-01-01" } } }); + const { out } = await exchange(rules, [modern, request(3, "tools/list"), other]); + expect(out.map((m: { id: number; result?: { era: string }; error?: { code: number } }) => [m.id, m.result?.era ?? m.error?.code])).toEqual([ + [1, "modern"], + [3, "legacy"], + [2, -32601], + ]); +}); + +test("--start-delay holds input until the delay passes", async () => { + const started = Date.now(); + const { out } = await exchange([{ method: "ping", result: {} }], [request(1, "ping")], ["--start-delay", "300"]); + expect(out).toEqual([{ jsonrpc: "2.0", id: 1, result: {} }]); + expect(Date.now() - started).toBeGreaterThanOrEqual(300); +}); + +test("rules can match the request's cursor, or its absence", async () => { + const rules: Rule[] = [ + { method: "tools/list", cursor: null, result: { page: 1 } }, + { method: "tools/list", cursor: "", result: { page: 2 } }, + ]; + const list = (id: number, cursor?: string) => JSON.stringify({ jsonrpc: "2.0", id, method: "tools/list", params: cursor === undefined ? {} : { cursor } }); + const { out } = await exchange(rules, [list(1), list(2, ""), list(3, "x")]); + expect(out.map((m: { id: number; result?: { page: number }; error?: { code: number } }) => [m.id, m.result?.page ?? m.error?.code])).toEqual([ + [1, 1], + [2, 2], + [3, -32601], + ]); +}); diff --git a/tests/tla/drivers/mcp/fakes/stdio.ts b/tests/tla/drivers/mcp/fakes/stdio.ts new file mode 100644 index 000000000..4eb9ea755 --- /dev/null +++ b/tests/tla/drivers/mcp/fakes/stdio.ts @@ -0,0 +1,160 @@ +// Scripted fake MCP server over stdio. +// +// Reads newline-delimited JSON-RPC from stdin and answers from a script. The +// first rule whose method matches and still has uses left is applied. A +// request with no matching rule gets -32601. Notifications get no reply unless +// a rule says so. Every line in and out is appended to --log as JSONL. +// +// Usage: bun tests/tla/drivers/mcp/fakes/stdio.ts --script [--log ] +// [--banner ] [--exit-at-start ] [--start-delay ] [--linger] [--ignore-term] +// [--once ] [--exit-after ] +// +// --banner write to stdout first, as a server printing a non-MCP line would +// --exit-at-start exit with before reading anything (a crash loop) +// --once a rule's "exit" or "crash" happens in the first process only, which leaves +// --exit-after exit with code 1 this long after starting (a server that dies later) +// --start-delay hold every input line until after start (a slow server) +// --linger keep running after stdin closes (forces the client's SIGTERM) +// --ignore-term ignore SIGTERM (forces the client's SIGKILL) + +import { appendFileSync, existsSync, readFileSync, writeFileSync, writeSync } from "node:fs"; + +export interface Rule { + /** JSON-RPC method to match. "*" matches any method. */ + method: string; + /** Match only requests whose 2026 `_meta` protocol version is this; null matches none sent. */ + version?: string | null; + /** Match only requests with this `cursor` param; null matches none sent. */ + cursor?: string | null; + /** Match only tools/call requests for this tool (U12). */ + tool?: string; + /** How many times the rule applies. Defaults to unlimited. */ + times?: number; + /** Lines to write before the reply, for example notifications. */ + before?: unknown[]; + /** Reply: a result, an error, a raw line (for malformed output), or nothing. */ + result?: unknown; + error?: { code: number; message: string; data?: unknown }; + raw?: string; + noReply?: boolean; + /** Wait before replying, in milliseconds. */ + delayMs?: number; + /** Lines to write to stderr before the reply, `stderrRepeat` times (default 1). */ + stderr?: string[]; + stderrRepeat?: number; + /** Write one stdout line of this many "x" bytes before the reply (an oversized line). */ + rawBytes?: number; + /** After replying: "exit" closes cleanly with code 0, "crash" exits with code 1. */ + then?: "exit" | "crash"; +} + +// A rule's result and `before` lines may say "$id" for the request's id, as a +// listen's subscriptionId must (U10). +const withId = (value: T, id: unknown): T => JSON.parse(JSON.stringify(value).replaceAll('"$id"', JSON.stringify(id ?? null))); + +interface Message { + jsonrpc?: string; + id?: string | number | null; + method?: string; + params?: unknown; +} + +function main(): void { + const args = process.argv.slice(2); + const get = (flag: string) => { + const index = args.indexOf(flag); + return index >= 0 ? args[index + 1] : undefined; + }; + const scriptPath = get("--script"); + if (!scriptPath) { + process.stderr.write("usage: fakes/stdio.ts --script [--log ]\n"); + process.exit(2); + } + const exitAtStart = get("--exit-at-start"); + if (exitAtStart !== undefined) process.exit(Number(exitAtStart)); + const exitAfter = get("--exit-after"); + if (exitAfter !== undefined) setTimeout(() => process.exit(1), Number(exitAfter)); + const once = get("--once"); + // A later process finds the file and skips the rule's ending. + const ends = once === undefined || !existsSync(once); + const linger = args.includes("--linger"); + if (args.includes("--ignore-term")) process.on("SIGTERM", () => {}); + const rules = JSON.parse(readFileSync(scriptPath, "utf8")) as Rule[]; + const used = rules.map(() => 0); + const logPath = get("--log"); + const log = (dir: "in" | "out", line: string) => { + if (logPath) appendFileSync(logPath, JSON.stringify({ dir, t: Date.now(), line }) + "\n"); + }; + const send = (line: string) => { + log("out", line); + // Synchronous so nothing is lost when a rule exits or crashes right after. + writeSync(1, line + "\n"); + }; + + const banner = get("--banner"); + if (banner !== undefined) send(banner); + + let pending = ""; + const startDelay = Number(get("--start-delay") ?? 0); + let queue: Promise = startDelay > 0 ? Bun.sleep(startDelay) : Promise.resolve(); + + const handle = async (line: string) => { + log("in", line); + let message: Message; + try { + message = JSON.parse(line) as Message; + } catch { + send(JSON.stringify({ jsonrpc: "2.0", id: null, error: { code: -32700, message: "Parse error" } })); + return; + } + const isRequest = message.id !== undefined && message.id !== null && typeof message.method === "string"; + const params = message.params as { _meta?: Record; cursor?: string; name?: string } | undefined; + const version = params?._meta?.["io.modelcontextprotocol/protocolVersion"] ?? null; + const cursor = params?.cursor ?? null; + const index = rules.findIndex( + (r, i) => + (r.method === "*" || r.method === message.method) && + (r.version === undefined || r.version === version) && + (r.cursor === undefined || r.cursor === cursor) && + (r.tool === undefined || r.tool === params?.name) && + (r.times === undefined || used[i] < r.times), + ); + if (index < 0) { + if (isRequest) send(JSON.stringify({ jsonrpc: "2.0", id: message.id, error: { code: -32601, message: "Method not found" } })); + return; + } + used[index] += 1; + const rule = rules[index]; + if (rule.delayMs) await Bun.sleep(rule.delayMs); + for (let n = 0; n < (rule.stderrRepeat ?? 1); n++) { + for (const line of rule.stderr ?? []) writeSync(2, line + "\n"); + } + if (rule.rawBytes) send("x".repeat(rule.rawBytes)); + for (const extra of rule.before ?? []) send(JSON.stringify(withId(extra, message.id))); + if (rule.raw !== undefined) send(rule.raw); + else if (rule.error) send(JSON.stringify({ jsonrpc: "2.0", id: message.id ?? null, error: rule.error })); + else if (!rule.noReply && (isRequest || rule.result !== undefined)) { + send(JSON.stringify({ jsonrpc: "2.0", id: message.id ?? null, result: withId(rule.result ?? {}, message.id) })); + } + if (rule.then !== undefined && ends && once !== undefined) writeFileSync(once, ""); + if (rule.then === "exit" && ends) process.exit(0); + if (rule.then === "crash" && ends) process.exit(1); + }; + + process.stdin.setEncoding("utf8"); + process.stdin.on("data", (chunk: string) => { + pending += chunk; + let newline: number; + while ((newline = pending.indexOf("\n")) >= 0) { + const line = pending.slice(0, newline).replace(/\r$/, ""); + pending = pending.slice(newline + 1); + if (line.length > 0) queue = queue.then(() => handle(line)); + } + }); + process.stdin.on("end", () => { + if (linger) setInterval(() => {}, 1000); + else queue.then(() => process.exit(0)); + }); +} + +if (import.meta.main) main(); diff --git a/tests/tla/drivers/mcp/fixtures/spec-examples.json b/tests/tla/drivers/mcp/fixtures/spec-examples.json new file mode 100644 index 000000000..919637254 --- /dev/null +++ b/tests/tla/drivers/mcp/fixtures/spec-examples.json @@ -0,0 +1,146 @@ +[ + { + "source": "2025-11-25_basic_lifecycle block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"method\": \"initialize\", \"params\": { \"protocolVersion\": \"2025-11-25\", \"capabilities\": { \"roots\": { \"listChanged\": true }, \"sampling\": {}, \"elicitation\": { \"form\": {}, \"url\": {} }, \"tasks\": { \"requests\": { \"elicitation\": { \"create\": {} }, \"sampling\": { \"createMessage\": {} } } } }, \"clientInfo\": { \"name\": \"ExampleClient\", \"title\": \"Example Client Display Name\", \"version\": \"1.0.0\", \"description\": \"An example MCP client application\", \"icons\": [ { \"src\": \"https://example.com/icon.png\", \"mimeType\": \"image/png\", \"sizes\": [\"48x48\"] } ], \"websiteUrl\": \"https://example.com\" } } }" + }, + { + "source": "2025-11-25_basic_lifecycle block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"result\": { \"protocolVersion\": \"2025-11-25\", \"capabilities\": { \"logging\": {}, \"prompts\": { \"listChanged\": true }, \"resources\": { \"subscribe\": true, \"listChanged\": true }, \"tools\": { \"listChanged\": true }, \"tasks\": { \"list\": {}, \"cancel\": {}, \"requests\": { \"tools\": { \"call\": {} } } } }, \"serverInfo\": { \"name\": \"ExampleServer\", \"title\": \"Example Server Display Name\", \"version\": \"1.0.0\", \"description\": \"An example MCP server providing tools and resources\", \"icons\": [ { \"src\": \"https://example.com/server-icon.svg\", \"mimeType\": \"image/svg+xml\", \"sizes\": [\"any\"] } ], \"websiteUrl\": \"https://example.com/server\" }, \"instructions\": \"Optional instructions for the client\" } }" + }, + { + "source": "2025-11-25_basic_lifecycle block 3", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/initialized\" }" + }, + { + "source": "2025-11-25_basic_lifecycle block 4", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"error\": { \"code\": -32602, \"message\": \"Unsupported protocol version\", \"data\": { \"supported\": [\"2024-11-05\"], \"requested\": \"1.0.0\" } } }" + }, + { + "source": "2025-11-25_basic_utilities_cancellation block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/cancelled\", \"params\": { \"requestId\": \"123\", \"reason\": \"User requested cancellation\" } }" + }, + { + "source": "2025-11-25_client_elicitation block 9", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"method\": \"elicitation/create\", \"params\": { \"mode\": \"form\", \"message\": \"Please provide your GitHub username\", \"requestedSchema\": { \"type\": \"object\", \"properties\": { \"name\": { \"type\": \"string\" } }, \"required\": [\"name\"] } } }" + }, + { + "source": "2025-11-25_client_elicitation block 10", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"result\": { \"action\": \"accept\", \"content\": { \"name\": \"octocat\" } } }" + }, + { + "source": "2025-11-25_client_elicitation block 11", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"method\": \"elicitation/create\", \"params\": { \"mode\": \"form\", \"message\": \"Please provide your contact information\", \"requestedSchema\": { \"type\": \"object\", \"properties\": { \"name\": { \"type\": \"string\", \"description\": \"Your full name\" }, \"email\": { \"type\": \"string\", \"format\": \"email\", \"description\": \"Your email address\" }, \"age\": { \"type\": \"number\", \"minimum\": 18, \"description\": \"Your age\" } }, \"required\": [\"name\", \"email\"] } } }" + }, + { + "source": "2025-11-25_client_elicitation block 12", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"result\": { \"action\": \"accept\", \"content\": { \"name\": \"Monalisa Octocat\", \"email\": \"octocat@github.com\", \"age\": 30 } } }" + }, + { + "source": "2025-11-25_client_elicitation block 13", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 3, \"method\": \"elicitation/create\", \"params\": { \"mode\": \"url\", \"elicitationId\": \"550e8400-e29b-41d4-a716-446655440000\", \"url\": \"https://mcp.example.com/ui/set_api_key\", \"message\": \"Please provide your API key to continue.\" } }" + }, + { + "source": "2025-11-25_client_elicitation block 14", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 3, \"result\": { \"action\": \"accept\" } }" + }, + { + "source": "2025-11-25_client_elicitation block 15", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/elicitation/complete\", \"params\": { \"elicitationId\": \"550e8400-e29b-41d4-a716-446655440000\" } }" + }, + { + "source": "2026-07-28_basic_index block 3", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"method\": \"tools/call\", \"params\": { \"name\": \"get_weather\", \"arguments\": { \"location\": \"New York\" }, \"_meta\": { \"traceparent\": \"00-0af7651916cd43dd8448eb211c80319c-00f067aa0ba902b7-01\" } } }" + }, + { + "source": "2026-07-28_basic_patterns_cancellation block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/cancelled\", \"params\": { \"requestId\": \"123\", \"reason\": \"User requested cancellation\" } }" + }, + { + "source": "2026-07-28_basic_patterns_progress block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"method\": \"some_method\", \"params\": { \"_meta\": { \"progressToken\": \"abc123\" } } }" + }, + { + "source": "2026-07-28_basic_patterns_progress block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/progress\", \"params\": { \"progressToken\": \"abc123\", \"progress\": 50, \"total\": 100, \"message\": \"Reticulating splines...\" } }" + }, + { + "source": "2026-07-28_basic_patterns_subscriptions block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"method\": \"subscriptions/listen\", \"params\": { \"_meta\": { \"io.modelcontextprotocol/protocolVersion\": \"2026-07-28\", \"io.modelcontextprotocol/clientInfo\": { \"name\": \"ExampleClient\", \"version\": \"1.0.0\" }, \"io.modelcontextprotocol/clientCapabilities\": {} }, \"notifications\": { \"toolsListChanged\": true, \"resourceSubscriptions\": [\"file:///project/config.json\"] } } }" + }, + { + "source": "2026-07-28_basic_patterns_subscriptions block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/subscriptions/acknowledged\", \"params\": { \"_meta\": { \"io.modelcontextprotocol/subscriptionId\": 1 }, \"notifications\": { \"toolsListChanged\": true, \"resourceSubscriptions\": [\"file:///project/config.json\"] } } }" + }, + { + "source": "2026-07-28_basic_patterns_subscriptions block 3", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/resources/updated\", \"params\": { \"_meta\": { \"io.modelcontextprotocol/subscriptionId\": 1 }, \"uri\": \"file:///project/config.json\" } }" + }, + { + "source": "2026-07-28_basic_patterns_subscriptions block 4", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"result\": { \"resultType\": \"complete\", \"_meta\": { \"io.modelcontextprotocol/subscriptionId\": 1 } } }" + }, + { + "source": "2026-07-28_basic_transports_streamable-http block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"error\": { \"code\": -32020, \"message\": \"Header mismatch: Mcp-Name header value 'foo' does not match body value 'bar'\" } }" + }, + { + "source": "2026-07-28_basic_versioning block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"error\": { \"code\": -32022, \"message\": \"Unsupported protocol version\", \"data\": { \"supported\": [\"2026-07-28\", \"2025-11-25\"], \"requested\": \"1900-01-01\" } } }" + }, + { + "source": "2026-07-28_server_discover block 1", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": \"discover-1\", \"method\": \"server/discover\", \"params\": { \"_meta\": { \"io.modelcontextprotocol/protocolVersion\": \"2026-07-28\", \"io.modelcontextprotocol/clientInfo\": { \"name\": \"ExampleClient\", \"version\": \"1.0.0\" }, \"io.modelcontextprotocol/clientCapabilities\": {} } } }" + }, + { + "source": "2026-07-28_server_discover block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": \"discover-1\", \"result\": { \"resultType\": \"complete\", \"supportedVersions\": [\"2026-07-28\"], \"capabilities\": { \"tools\": {}, \"resources\": {} }, \"_meta\": { \"io.modelcontextprotocol/serverInfo\": { \"name\": \"ExampleServer\", \"version\": \"1.0.0\" } }, \"instructions\": \"This server provides weather and resource utilities.\", \"ttlMs\": 3600000, \"cacheScope\": \"public\" } }" + }, + { + "source": "2026-07-28_server_tools block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"method\": \"tools/list\", \"params\": { \"cursor\": \"optional-cursor-value\" } }" + }, + { + "source": "2026-07-28_server_tools block 3", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 1, \"result\": { \"resultType\": \"complete\", \"tools\": [ { \"name\": \"get_weather\", \"title\": \"Weather Information Provider\", \"description\": \"Get current weather information for a location\", \"inputSchema\": { \"type\": \"object\", \"properties\": { \"location\": { \"type\": \"string\", \"description\": \"City name or zip code\" } }, \"required\": [\"location\"] }, \"icons\": [ { \"src\": \"https://example.com/weather-icon.png\", \"mimeType\": \"image/png\", \"sizes\": [\"48x48\"] } ] } ], \"nextCursor\": \"next-page-cursor\", \"ttlMs\": 300000, \"cacheScope\": \"public\" } }" + }, + { + "source": "2026-07-28_server_tools block 4", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"method\": \"tools/call\", \"params\": { \"name\": \"get_weather\", \"arguments\": { \"location\": \"New York\" } } }" + }, + { + "source": "2026-07-28_server_tools block 5", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"result\": { \"resultType\": \"complete\", \"content\": [ { \"type\": \"text\", \"text\": \"Current weather in New York:\\nTemperature: 72°F\\nConditions: Partly cloudy\" } ], \"isError\": false } }" + }, + { + "source": "2026-07-28_server_tools block 6", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 2, \"result\": { \"resultType\": \"input_required\", \"inputRequests\": { \"github_login\": { \"method\": \"elicitation/create\", \"params\": { \"mode\": \"form\", \"message\": \"Please provide your GitHub username\", \"requestedSchema\": { \"type\": \"object\", \"properties\": { \"name\": { \"type\": \"string\" } }, \"required\": [\"name\"] } } } }, \"requestState\": \"eyJsb2NhdGlvbiI6Ik5ldyBZb3JrIn0...\" } }" + }, + { + "source": "2026-07-28_server_tools block 7", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 3, \"method\": \"tools/call\", \"params\": { \"name\": \"get_weather\", \"arguments\": { \"location\": \"New York\" }, \"inputResponses\": { \"github_login\": { \"action\": \"accept\", \"content\": { \"name\": \"octocat\" } } }, \"requestState\": \"eyJsb2NhdGlvbiI6Ik5ldyBZb3JrIn0...\" } }" + }, + { + "source": "2026-07-28_server_tools block 8", + "input": "{ \"jsonrpc\": \"2.0\", \"method\": \"notifications/tools/list_changed\" }" + }, + { + "source": "2026-07-28_server_tools block 16", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 5, \"result\": { \"resultType\": \"complete\", \"content\": [ { \"type\": \"text\", \"text\": \"{\\\"temperature\\\": 22.5, \\\"conditions\\\": \\\"Partly cloudy\\\", \\\"humidity\\\": 65}\" } ], \"structuredContent\": { \"temperature\": 22.5, \"conditions\": \"Partly cloudy\", \"humidity\": 65 } } }" + }, + { + "source": "2026-07-28_server_tools block 18", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 6, \"result\": { \"resultType\": \"complete\", \"content\": [ { \"type\": \"text\", \"text\": \"Found 2 users: Alice (alice@example.com) and Bob (bob@example.com).\" } ], \"structuredContent\": [ { \"id\": \"1\", \"name\": \"Alice\", \"email\": \"alice@example.com\" }, { \"id\": \"2\", \"name\": \"Bob\", \"email\": \"bob@example.com\" } ] } }" + }, + { + "source": "2026-07-28_server_tools block 22", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 3, \"error\": { \"code\": -32602, \"message\": \"Unknown tool: invalid_tool_name\" } }" + }, + { + "source": "2026-07-28_server_tools block 23", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": 4, \"result\": { \"resultType\": \"complete\", \"content\": [ { \"type\": \"text\", \"text\": \"Invalid departure date: must be in the future. Current date is 08/08/2025.\" } ], \"isError\": true } }" + }, + { + "source": "2026-07-28_server_utilities_pagination block 2", + "input": "{ \"jsonrpc\": \"2.0\", \"id\": \"124\", \"method\": \"resources/list\", \"params\": { \"cursor\": \"eyJwYWdlIjogMn0=\" } }" + } +] diff --git a/tests/tla/drivers/mcp/lab.ts b/tests/tla/drivers/mcp/lab.ts new file mode 100644 index 000000000..85752cc6b --- /dev/null +++ b/tests/tla/drivers/mcp/lab.ts @@ -0,0 +1,133 @@ +// Shared builder for scenarios that run tests/tla/drivers/mcp/labs/stdio_lab.zig against the +// scripted fake stdio server (U02 transport-level and U03 to U05 scenarios). + +import { readFileSync, writeFileSync } from "node:fs"; +import { join } from "node:path"; +import type { Rule } from "./fakes/stdio"; +import type { Scenario, ScenarioContext, TraceExpectation } from "./scenario"; + +const FAKE = join(import.meta.dir, "fakes/stdio.ts"); +export const PING = '{"jsonrpc":"2.0","id":1,"method":"ping"}'; +export const PING2 = '{"jsonrpc":"2.0","id":2,"method":"ping"}'; + +export interface Seen { + did?: { action?: string; state?: string; error?: string; expect?: string; met?: boolean; era_error?: string }; + era?: { ready?: string; failed?: string }; + tools?: { event: string; fresh?: boolean; count?: number; names?: string[]; invalid?: number; duplicate?: number }; + call?: { id: number; kind: string; is_error?: boolean; content?: string; structured?: string | null; code?: number }; + seen?: { message?: string; stderr?: string; dropped?: string; state?: string; lost?: boolean }; + sub?: { sub: number; deliver?: string; acknowledged?: number; ended?: string }; + outcome?: { id: number; outcome: string }; + final?: { + state: string; + generation: number; + attempts: number; + term_sent: boolean; + kill_sent: boolean; + errored: boolean; + stderr_dropped: number; + spawn_error: string | null; + in_flight?: number; + era?: string; + era_version?: string; + era_failure?: string | null; + catalog?: string; + tools?: number; + }; +} + +export interface LabCase { + name: string; + unit: string; + description: string; + rules?: Rule[]; + /** Extra fake-server flags, or a full replacement command when `server` is set. */ + fakeFlags?: string[]; + server?: string[]; + labFlags?: string[]; + script: string[]; + /** The model's failure limit; the lab's default is 8. */ + maxAttempts?: number; + verdict?: "ACCEPTED" | "REJECTED"; + /** Also check the request machine's trace (U02 over stdio). */ + requestTrace?: boolean; + /** Also check the era machine's trace (U04): how many preferred versions the lab has. */ + era?: { preferred: number; verdict?: "ACCEPTED" | "REJECTED" }; + /** Also check the catalog machine's trace (U05): the lab's page limit. */ + catalog?: { maxPages: number; verdict?: "ACCEPTED" | "REJECTED" }; + /** Also check the subscription machine's trace (U10). */ + subscription?: { maxTries?: number; verdict?: "ACCEPTED" | "REJECTED" }; + /** Checks the lab's output and the fake server's log of every line it saw. */ + check?: (lines: Seen[], final: NonNullable, serverLog: { dir: string; line: string }[]) => string | null; + timeoutMs?: number; + real?: boolean; +} + +export function labScenario(c: LabCase): Scenario { + let caseDir = ""; + const traces: TraceExpectation[] = [ + { machine: "stdio", instance: "lab", specDir: "tests/tla/mcp", wrapper: "StdioConnTrace", verdict: c.verdict ?? "ACCEPTED", constants: { ObsMaxAttempts: c.maxAttempts ?? 8 } }, + ]; + if (c.requestTrace) traces.push({ machine: "request", instance: "lab", specDir: "tests/tla/mcp", wrapper: "RequestTrace", verdict: "ACCEPTED" }); + if (c.era) { + traces.push({ machine: "era", instance: "lab", specDir: "tests/tla/mcp", wrapper: "EraTrace", verdict: c.era.verdict ?? "ACCEPTED", constants: { ObsPreferredCount: c.era.preferred } }); + } + if (c.catalog) { + traces.push({ machine: "catalog", instance: "lab", specDir: "tests/tla/mcp", wrapper: "CatalogTrace", verdict: c.catalog.verdict ?? "ACCEPTED", constants: { ObsMaxPages: c.catalog.maxPages } }); + } + if (c.subscription) { + traces.push({ machine: "subscription", instance: "lab", specDir: "tests/tla/mcp", wrapper: "SubscriptionTrace", verdict: c.subscription.verdict ?? "ACCEPTED", constants: { ObsMaxTries: c.subscription.maxTries ?? 8 } }); + } + return { + name: c.name, + unit: c.unit, + description: c.description, + needs: ["stdio_lab"], + setup: (ctx: ScenarioContext) => { + caseDir = ctx.caseDir; + writeFileSync(join(ctx.caseDir, "rules.json"), JSON.stringify(c.rules ?? [])); + writeFileSync(join(ctx.caseDir, "script.txt"), c.script.join("\n") + "\n"); + }, + command: (ctx: ScenarioContext) => [ + ctx.bin.stdio_lab, + ctx.tracePath, + join(ctx.caseDir, "script.txt"), + ...(c.labFlags ?? []), + "--", + ...(c.server ?? [process.execPath, FAKE, "--script", join(ctx.caseDir, "rules.json"), "--log", join(ctx.caseDir, "server.jsonl"), ...(c.fakeFlags ?? [])]), + ], + expect: { + exit: 0, + traces, + stdout: (text) => { + const lines = text.split("\n").filter(Boolean).map((l) => JSON.parse(l) as Seen); + const unmet = lines.find((l) => l.did?.met === false || l.did?.error !== undefined); + if (unmet) return `script step failed: ${JSON.stringify(unmet.did)}`; + const final = lines.at(-1)?.final; + if (!final) return "no final line"; + if (!c.check) return null; + let serverLog: { dir: string; line: string }[] = []; + try { + serverLog = readFileSync(join(caseDir, "server.jsonl"), "utf8").split("\n").filter(Boolean).map((l) => JSON.parse(l)); + } catch { + // No log: the server never started. + } + return c.check(lines, final, serverLog); + }, + }, + timeoutMs: c.timeoutMs, + real: c.real, + }; +} + +export const messages = (lines: Seen[]) => lines.filter((l) => l.seen?.message !== undefined).map((l) => l.seen!.message!); +export const expectFinal = (final: NonNullable, want: Partial>): string | null => { + for (const [key, value] of Object.entries(want)) { + const got = (final as unknown as Record)[key]; + if (got !== value) return `final ${key} is ${JSON.stringify(got)}, expected ${JSON.stringify(value)}`; + } + return null; +}; + +export const outcomes = (lines: Seen[]) => + Object.fromEntries(lines.filter((l) => l.outcome).map((l) => [l.outcome!.id, l.outcome!.outcome])); diff --git a/tests/tla/drivers/mcp/labs/engine_lab.zig b/tests/tla/drivers/mcp/labs/engine_lab.zig new file mode 100644 index 000000000..683d8c7fc --- /dev/null +++ b/tests/tla/drivers/mcp/labs/engine_lab.zig @@ -0,0 +1,379 @@ +//! Written for the next MCP-v2 version: it does not build against this +//! checkout's src/mcp/ until that version lands, so the driver runs its +//! scenarios only with --next. +//! +//! U12 lab: runs a script of host actions against `mcp.engine`, playing the +//! host: its permission answers, its stderr sink, and what it does with each +//! event. One run traces every server's machines into one file, the engine +//! gate's under the server's name and each server's under ".". Dev +//! only; never moves into fx. +//! +//! Usage: engine_lab