mirrors/fx
0
0 Fork 0
mirror of https://github.com/vercel-labs/fx.git synced 2026-10-28 10:15:17 +08:00
Code Activity

Merge pull request #1258 from vercel-labs/fazxes/move-design-docs-next-to-code

Browse Source 
Remove the top-level docs folder and keep TLA+ models in tests/tla
This commit is contained in:
Pranit authored and GitHub committed 2026-10-14 20:23:42 -04:00
2 parents 344884cf76 61e633b55b
commit f23db23601
499 files changed
+34272 -107
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

.github/workflows/ci.yml
+14 -14
View File
@@ -373,20 +373,20 @@ jobs:
jar="$RUNNER_TEMP/tla2tools.jar"
curl -fsSL -o "$jar" https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
echo "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 $jar" | sha256sum -c -
TLA2TOOLS_JAR="$jar" sdk/tests/model/check.sh
bun sdk/tests/model/drive.mjs send --walks 40
bun sdk/tests/model/drive.mjs lookup --walks 40 --seed 7
bun sdk/tests/model/drive.mjs send --walks 20 --seed 3 --durability world
bun sdk/tests/model/drive.mjs lookup --walks 20 --seed 9 --durability world
bun sdk/tests/model/drive.mjs write --walks 20 --seed 4
bun sdk/tests/model/drive.mjs cutoff --walks 20 --seed 5
bun sdk/tests/model/drive.mjs leased --walks 40 --seed 12
bun sdk/tests/model/drive.mjs queue --walks 40 --seed 4
bun sdk/tests/model/drive-agents.mjs send --walks 60 --seed 11
bun sdk/tests/model/drive-agents.mjs consume --walks 60 --seed 13
bun sdk/tests/model/drive-steer.mjs ideal --walks 20 --seed 2
bun sdk/tests/model/drive-steer.mjs faults --walks 20 --seed 4
bun sdk/tests/model/drive-steer.mjs faults --walks 10 --seed 6 --backend wasm
TLA2TOOLS_JAR="$jar" tests/tla/sdk/check.sh
bun tests/tla/drivers/drive.mjs send --walks 40
bun tests/tla/drivers/drive.mjs lookup --walks 40 --seed 7
bun tests/tla/drivers/drive.mjs send --walks 20 --seed 3 --durability world
bun tests/tla/drivers/drive.mjs lookup --walks 20 --seed 9 --durability world
bun tests/tla/drivers/drive.mjs write --walks 20 --seed 4
bun tests/tla/drivers/drive.mjs cutoff --walks 20 --seed 5
bun tests/tla/drivers/drive.mjs leased --walks 40 --seed 12
bun tests/tla/drivers/drive.mjs queue --walks 40 --seed 4
bun tests/tla/drivers/drive-agents.mjs send --walks 60 --seed 11
bun tests/tla/drivers/drive-agents.mjs consume --walks 60 --seed 13
bun tests/tla/drivers/drive-steer.mjs ideal --walks 20 --seed 2
bun tests/tla/drivers/drive-steer.mjs faults --walks 20 --seed 4
bun tests/tla/drivers/drive-steer.mjs faults --walks 10 --seed 6 --backend wasm
- name: Test libfx on a World
run: |
AGENTS.md
+8 -2
View File
@@ -40,7 +40,7 @@ zig fmt src/ # format all source files
zig fmt --check src/ # the formatting check CI runs
```
The test suites under `tests/` use Bun but are separate from the Zig codebase. See **Testing** below.
The test suites under `tests/` use Bun but are separate from the Zig codebase. `tests/tla/` holds the TLA+ models. See **Testing** and **TLA+ Models** below.
## Code Style
@@ -250,7 +250,7 @@ fx does not use declarations that Zig 0.17 deprecates. They still compile, so ch
## Testing (TypeScript)
Two test suites live under `tests/`, both using Bun.
Two test suites live under `tests/`, both using Bun. `tests/AGENTS.md` says where each kind of test belongs, how to wire a new E2E file into CI, and how code comments cite tests and specs.
Set `FX_SOUND=0` when you run either suite locally, for example `cd tests/e2e && FX_SOUND=0 bun test cli.test.ts`. On macOS, sound playback during a test run can overload the machine and crash it. The variable doesn't cover `notifications.test.ts`, which clears it, or the "TUI user-profile output preserves compact scrollback across slash commands" test in `tui-command-permissions.test.ts`, which sends `/sound on`. Leave those to CI. On Linux, fx rings the terminal bell instead of playing a sound, so they run safely there. The full `bun test` run below includes both, and `bun test tui-*.test.ts` includes the `/sound on` test, so on macOS pass test files by name.
@@ -276,6 +276,12 @@ cd tests/e2e && bun test tui-*.test.ts # just TUI tests (requires
TUI tests use tmux to drive the interactive terminal. They require `tmux` to be installed.
## TLA+ Models
Every TLA+ spec, its TLC checker, the Bun drivers that walk real code along a spec, and the session manager's design record live in `tests/tla/`, and nowhere else. `tests/AGENTS.md` describes the layout and how to add a model, and `tests/tla/README.md` lists the commands. Session decision numbers such as `D44` are defined in `tests/tla/session_manager/system-design.md`.
Code comments cite a spec by its repository-relative path and the property it checks, such as `tests/tla/session_manager/Wiring.tla` `ParentOutlivesChildren`, and never cite a file outside the repository. When a change alters behavior that a spec models, update the spec in the same change and run its checker.
## Pull Request Classification
Every pull request must have exactly one `type:` label before it merges, chosen by its primary intent:
CONTRIBUTING.md
+10
View File
@@ -112,6 +112,16 @@ The script builds a ReleaseSafe binary and needs hyperfine. On macOS, process an
python3 benchmarks/first_frame.py --binary /tmp/fx-before --binary ./zig-out/bin/fx
```
### Check a TLA+ model
`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/mcp/check.sh --model Engine
bun test ./tests/tla/drivers/shell_command/
```
### Run the model evals
The evals in `tests/evals/` drive the agent through `fx ask --json` against real models and need `AI_GATEWAY_API_KEY`. They make billed model calls and their results vary between runs, so they aren't part of the pull request checks.
docs/long-turn-memory.md → benchmarks/long-turn-memory.md
View File
File renamed without changes.
sdk/AGENTS.md
+2 -2
View File
@@ -59,8 +59,8 @@ Do not treat the demos or this file as the implementation contract. When prose a
| `encodeXtermKeyEvent()` or `xtermAdapter()` only | `sdk/node/test-xterm-adapter.mjs` |
| Core debugger query behavior or automation state | `sdk/tests/test-core-browser.mjs` |
| Terminal demo asset references, integrity, or cache policy | Package into a fresh temporary directory and inspect the generated HTML, manifest, and headers |
| Durable sessions: leases, fencing, takeovers, tool reruns, the UI stream | `sdk/tests/test-durable-core.mjs` on memory, local, world, and queue (the core with a scripted harness; world is an app-built World passed to `world()`, queue one whose queue delivers as Vercel Queues does, with `queueLeases`), `sdk/tests/test-durable.mjs` on memory, local, and world, then `sdk/tests/model/check.sh` and `bun sdk/tests/model/drive.mjs send`, `lookup`, `write`, `cutoff` (deadline cut-offs up to their bound), `leased` (a World without liveness, where each worker renews a short lease), and `queue` (a World whose queue shows whether a worker lives, so leases are held without renewals), which walk the real code along the TLC state graphs of `DurableSession.tla`; change the spec with the code. For agent names and routing, also `bun sdk/tests/model/drive-agents.mjs send` and `consume`, which walk `AgentRouting.tla`'s graphs with each process in a worker thread of its own. With a Vercel access token, also run both against Vercel's World: `test-durable.mjs vercel native` and `drive.mjs --durability vercel`, configured as `sdk/tests/vercel-storage.mjs` describes |
| Steering: interrupts, waits during tools, joins, hand-backs on cancel, image handoffs, steer ids | The libfx steering tests in `src/acp/libfx_steering.zig`, `sdk/tests/test-agent-steering.mjs` and `sdk/tests/test-durable.mjs` on native and wasm, then `sdk/tests/model/check.sh` and `bun sdk/tests/model/drive-steer.mjs ideal` and `faults`, with `--backend wasm` too, which walk the real code along the TLC state graphs of `DurableSteer.tla`; change the spec with the code |
| Durable sessions: leases, fencing, takeovers, tool reruns, the UI stream | `sdk/tests/test-durable-core.mjs` on memory, local, world, and queue (the core with a scripted harness; world is an app-built World passed to `world()`, queue one whose queue delivers as Vercel Queues does, with `queueLeases`), `sdk/tests/test-durable.mjs` on memory, local, and world, then `tests/tla/sdk/check.sh` and `bun tests/tla/drivers/drive.mjs send`, `lookup`, `write`, `cutoff` (deadline cut-offs up to their bound), `leased` (a World without liveness, where each worker renews a short lease), and `queue` (a World whose queue shows whether a worker lives, so leases are held without renewals), which walk the real code along the TLC state graphs of `DurableSession.tla`; change the spec with the code. For agent names and routing, also `bun tests/tla/drivers/drive-agents.mjs send` and `consume`, which walk `AgentRouting.tla`'s graphs with each process in a worker thread of its own. With a Vercel access token, also run both against Vercel's World: `test-durable.mjs vercel native` and `drive.mjs --durability vercel`, configured as `sdk/tests/vercel-storage.mjs` describes |
| Steering: interrupts, waits during tools, joins, hand-backs on cancel, image handoffs, steer ids | The libfx steering tests in `src/acp/libfx_steering.zig`, `sdk/tests/test-agent-steering.mjs` and `sdk/tests/test-durable.mjs` on native and wasm, then `tests/tla/sdk/check.sh` and `bun tests/tla/drivers/drive-steer.mjs ideal` and `faults`, with `--backend wasm` too, which walk the real code along the TLC state graphs of `DurableSteer.tla`; change the spec with the code |
| Supported public behavior or setup | Update `sdk/README.md` in the same change |
Use Node.js 24 for SDK tests. CI relies on its JSPI implementation behind `--experimental-wasm-jspi`.
src/acp/server.zig
+6 -1
View File
@@ -877,7 +877,7 @@ fn resolveSubagentAuthority(
}
/// Joins the child threads before the session they append to can close
/// (`tla/Wiring.tla` ParentOutlivesChildren).
/// (`tests/tla/session_manager/Wiring.tla` ParentOutlivesChildren).
pub fn disableSubagentHost(state: *ServerState) void {
if (state.subagent_host) |host| {
host.deinit();
@@ -3185,6 +3185,9 @@ fn handleCloseSession(state: *ServerState, alloc: Allocator, msg: *jsonrpc.Messa
try state.writer.writeResponse(alloc, msg.id, "{}");
}
/// Handles `session/set_config_option`. The `mode` option is modeled in
/// `tests/tla/acp/AcpPermissionModes.tla`, and `fast` and `ultrafast` in
/// `tests/tla/acp/AcpSpeed.tla`.
fn handleSetConfigOption(state: *ServerState, alloc: Allocator, msg: *jsonrpc.Message) !void {
const params = msg.params_raw orelse return state.writer.writeError(alloc, msg.id, .{
.code = ErrorCode.invalid_params,
@@ -3927,6 +3930,8 @@ fn commitActiveSessionUltrafast(
session.ultrafast_mode = ultrafast;
}
/// Handles the older `session/set_mode`, modeled with the `mode` option in
/// `tests/tla/acp/AcpPermissionModes.tla`.
fn handleSetMode(state: *ServerState, alloc: Allocator, msg: *jsonrpc.Message) !void {
const params = msg.params_raw orelse return state.writer.writeError(alloc, msg.id, .{
.code = ErrorCode.invalid_params,
src/core/app/app_mcp_runtime.zig
+2 -1
View File
@@ -1717,7 +1717,8 @@ pub const State = struct {
self.cancelPendingMenuOperation("menu_back");
}
/// Loads the host at startup with `load`, which reloads use too.
/// Loads the host at startup with `load`, which reloads use too. The host's
/// lifecycle is modeled in `tests/tla/mcp_host/HostLifecycle.tla`.
pub fn loadHost(
self: *State,
load: mcp_host.LoadFn,
src/core/app/app_session_runtime.zig
+1 -1
View File
@@ -3824,7 +3824,7 @@ pub fn Runtime(comptime App: type) type {
}
/// Stops the subagent host, joining its child threads, before the
/// session they append to can close (`tla/Wiring.tla`
/// session they append to can close (`tests/tla/session_manager/Wiring.tla`
/// ParentOutlivesChildren).
pub fn disableSubagentHost(app: *App) void {
if (app.session_persistence.subagent_host) |host| {
src/core/cli/cli_surface.zig
+3
View File
@@ -400,6 +400,9 @@ const GlobalLaunchArgs = struct {
}
};
/// Parses the launch flags `fx` and `fx ask` share. How `--model`, `--fast`,
/// `--ultrafast`, and `--effort` reach the first turn is modeled in
/// `tests/tla/cli/LaunchSelection.tla`.
fn parseGlobalLaunchArgs(
alloc: Allocator,
args: []const [:0]const u8,
src/core/indexer/git_index.zig
+1 -1
View File
@@ -9,7 +9,7 @@ const io_mod = @import("../shared/io.zig");
const Allocator = std.mem.Allocator;
/// D7: the index is never read beyond this size.
/// The index is never read beyond this size.
const max_index_bytes: usize = 128 * 1024 * 1024;
const mode_type_mask: u32 = 0o170000;
src/core/indexer/ignore.zig
+1 -1
View File
@@ -8,7 +8,7 @@ const wildmatch = @import("wildmatch.zig");
const Allocator = std.mem.Allocator;
/// Largest pattern file read, per source (D7).
/// Largest pattern file read, per source.
pub const max_pattern_file_bytes: usize = 1024 * 1024;
const Pattern = struct {
src/core/indexer/scan.zig
+5 -5
View File
@@ -29,12 +29,12 @@ pub const Kind = tree_mod.Kind;
pub const Entry = tree_mod.Entry;
pub const Options = struct {
/// D7: at most this many files are returned. Folder rows do not count;
/// At most this many files are returned. Folder rows do not count;
/// the collection limit (`collect_factor`) bounds them.
candidate_cap: usize = 100_000,
max_path_bytes: usize = 2048,
/// Folder and file names skipped outside repositories and below an
/// ignored root (D4, U3). Never applied inside a repository.
/// ignored root. Never applied inside a repository.
skipped_names: []const []const u8 = &default_skipped_names,
max_workers: usize = 8,
};
@@ -369,7 +369,7 @@ fn repositoryRules(arena: Allocator, index_alloc: Allocator, root: []const u8, r
.unavailable => incomplete.* = true,
}
}
// U3: below an ignored root, plain rules apply.
// Below an ignored root, plain rules apply.
if (ignore.isPathExcluded(lists.items, found.prefix, true, settings.ignore_case)) {
debug_trace.logf("indexer", "scan uses plain rules reason=ignored_root root={s}", .{root});
return null;
@@ -634,7 +634,7 @@ fn entryLessThan(_: void, a: Entry, b: Entry) bool {
}
/// Length of the sorted prefix that holds the first `cap` files, or null when
/// `entries` has no more than `cap` files. Folder rows do not count (D7).
/// `entries` has no more than `cap` files. Folder rows do not count.
fn capCut(entries: []const Entry, cap: usize) ?usize {
var files: usize = 0;
for (entries, 0..) |entry, index| {
@@ -762,7 +762,7 @@ test "repository scan follows git: index, ignore rules, folder rules and boundar
try std.testing.expect(sub.tree.repository);
try expectEntries(sub, &.{.{ .path = "h.txt", .kind = .file }});
// U3: a root that is itself ignored is listed with plain rules.
// A root that is itself ignored is listed with plain rules.
var ignored_root = try scan(std.testing.allocator, try std.Io.Dir.path.join(arena, &.{ tree.root, "repo/dist" }), .{}, null);
defer ignored_root.deinit();
try std.testing.expect(!ignored_root.tree.repository);
src/core/indexer/sources.zig
+3
View File
@@ -3,6 +3,9 @@
//! down, which a walker loads as it enters each directory. Every source is a
//! bounded regular-file read; one that cannot be read is reported so the
//! caller can mark its result incomplete, never replaced by running git.
//!
//! Which of these sources can change a saved listing is modeled in
//! `tests/tla/indexer/SnapshotSources.tla`.
const std = @import("std");
const io_mod = @import("../shared/io.zig");
src/core/indexer/tree.zig
+1 -1
View File
@@ -4,7 +4,7 @@
//! its times are older than the scan's start by the granularity margin, so a
//! change in the same clock tick as the scan, which a later stamp comparison
//! could not see, always forces a new scan. This is the reuse certificate the
//! refresh model (Refresh.tla) requires.
//! refresh model (`tests/tla/indexer/Refresh.tla`) requires.
const std = @import("std");
const io_mod = @import("../shared/io.zig");
src/core/input/picker_state.zig
+2 -1
View File
@@ -91,7 +91,8 @@ pub const InlineSlashQuery = struct {
/// Paces the frame for a keystroke that started a folder listing. Most folders
/// list well within one event-loop tick, so that frame waits for the rows and
/// the keystroke paints together with them instead of over an empty
/// "indexing files..." list. Times are monotonic milliseconds.
/// "indexing files..." list. Times are monotonic milliseconds. Modeled in
/// `tests/tla/indexer/ListingWait.tla`.
const FileListingWait = struct {
const hold_ms: i64 = 8;
src/core/mcp_host/credentials.zig
+3
View File
@@ -3,6 +3,9 @@
//! the macOS Keychain, or in a private file under `~/.fx/mcp-credentials/`.
//! Either way the directory's advisory lock is held while the store is read
//! and rewritten, so two fx processes don't overwrite each other's entries.
//!
//! TLA+ models: `tests/tla/mcp_host/Credentials.tla` and, for logins shared between
//! processes, `tests/tla/mcp_host/SharedLogins.tla`.
const std = @import("std");
const builtin = @import("builtin");
src/core/mcp_host/login.zig
+2
View File
@@ -3,6 +3,8 @@
//! came to goes to MCP-v2's `finishSignIn`. Anything else, such as a request
//! for an icon, gets a 404 and the wait goes on. A bridged sign-in (Slack's,
//! through fx.sh) comes back instead as a form its page posts.
//!
//! TLA+ model: `tests/tla/mcp_host/SignIn.tla`.
const std = @import("std");
const browser_callback = @import("../auth/browser_callback.zig");
src/core/mcp_host/menu.zig
+2
View File
@@ -2,6 +2,8 @@
//! showing servers. A server's actions are choices that run the `/mcp`
//! verbs, so the menu adds nothing of its own. Pure: the shell's state owns
//! one, and the footer draws it.
//!
//! TLA+ model: `tests/tla/mcp_host/HostLifecycle.tla`.
const std = @import("std");
const text_utils = @import("../shared/text_utils.zig");
src/core/mcp_host/runtime.zig
+5 -1
View File
@@ -4,6 +4,10 @@
//! engine's servers (`config.zig`), keeps sign-in credentials
//! (`credentials.zig`), and runs logins on a loopback listener (`login.zig`).
//! Chosen with FX_MCP_ENGINE=v2 until v1 is removed.
//!
//! TLA+ models: `tests/tla/mcp_host/HostLifecycle.tla`,
//! `tests/tla/mcp_host/SignIn.tla`, `tests/tla/mcp_host/SharedLogins.tla`, and
//! `tests/tla/mcp_host/ElicitationRouting.tla`.
const std = @import("std");
const mcp = @import("../../mcp/mcp.zig");
@@ -1160,7 +1164,7 @@ pub const Runtime = struct {
}
/// Permission is fx's tool admission, before the call reaches the
/// runtime, and only the runtime calls the engine (D6).
/// runtime, and only the runtime calls the engine.
fn allow(_: *anyopaque, _: []const u8, _: []const u8, _: ?[]const u8) bool {
return true;
}
src/core/session/session_adapter.zig
+9 -8
View File
@@ -18,7 +18,7 @@
//! ACP client's prompt and tool identities are settings (D46); hosted
//! terminal state lives in `~/.fx/terminal/{id}/` (D45). An older session
//! with a `~/.fx/session-files/{id}/` side folder moves on its first
//! writable open (D47, `tla/MoveSideFiles.tla`).
//! writable open (D47, `tests/tla/session_manager/MoveSideFiles.tla`).
const std = @import("std");
const testing_allocator = @import("../shared/testing_allocator.zig");
@@ -1123,7 +1123,7 @@ pub const Session = struct {
}
/// Closes the session and frees the adapter. Every child thread of this
/// session must have joined (`tla/Wiring.tla` ParentOutlivesChildren).
/// session must have joined (`tests/tla/session_manager/Wiring.tla` ParentOutlivesChildren).
/// A copy of its capability that a background reader still holds keeps
/// reading, and stores nothing more (D44).
pub fn close(self: *Session) void {
@@ -1782,11 +1782,12 @@ pub const Session = struct {
// -- the move off the side folder (D47) -----------------------------------
/// Makes an older session one manager folder (D47, `tla/MoveSideFiles.tla`)
/// on its first writable open, then loads the map its old handles resolve
/// through. Every body in the side folder becomes a blob, the map from
/// each old name to its blob is one more blob, and one batch records the
/// map, every moved blob, and the client's settings from the old files.
/// Makes an older session one manager folder (D47,
/// `tests/tla/session_manager/MoveSideFiles.tla`) on its first writable
/// open, then loads the map its old handles resolve through. Every body
/// in the side folder becomes a blob, the map from each old name to its
/// blob is one more blob, and one batch records the map, every moved
/// blob, and the client's settings from the old files.
/// Then the terminal folder moves to `~/.fx/terminal/{id}` and the side
/// folder goes. Each step can be repeated, so a crash at any point
/// redoes the move on the next open.
@@ -1813,7 +1814,7 @@ pub const Session = struct {
}
/// Every step of the move but the side folder's removal, in the order
/// `tla/MoveSideFiles.tla` checks; returns how many bodies moved.
/// `tests/tla/session_manager/MoveSideFiles.tla` checks; returns how many bodies moved.
fn moveOut(self: *Session, side: *io_mod.VerifiedDir) !usize {
var scratch = std.heap.ArenaAllocator.init(self.alloc);
defer scratch.deinit();
src/core/session_manager/api.zig
+2 -2
View File
@@ -3,7 +3,7 @@
//!
//! This file (L4) is the only public root; fx imports it and nothing else.
//! A process creates one `Manager` with `init`, which does no disk I/O.
//! Thirteen operations cover every host (docs/session-manager/system-design.md
//! Thirteen operations cover every host (`tests/tla/session_manager/system-design.md`
//! "API"), plus `verify` and `rebuild` for doctor:
//!
//! openNew openResume openFork openImport -> Session
@@ -431,7 +431,7 @@ pub const Manager = struct {
}
/// Deletes a session and the children it owns. Busy if any is open.
/// Order per session (`tla/Catalog.tla`): children first, then the
/// Order per session (`tests/tla/session_manager/Catalog.tla`): children first, then the
/// rename to `.trash`, the index tombstone, and the purge. fx removes
/// the matching terminal folders (D13).
pub fn delete(m: *Manager, id: []const u8) DeleteError!void {
src/core/session_manager/catalog.zig
+3 -3
View File
@@ -4,7 +4,7 @@
//! change: `put` (a session's summary), `opened` (a host opened it) and
//! `del` (a tombstone), appended under `index.lock` and never fsynced.
//! Folding it keeps the newest record per id; a tombstone is final, so a
//! deleted id never comes back (`tla/Catalog.tla` `NoResurrection`).
//! deleted id never comes back (`tests/tla/session_manager/Catalog.tla` `NoResurrection`).
//! `list` reads only the index and self-heals entries whose folder is gone;
//! `rebuild` re-derives it from the folders and sweeps `.tmp` and `.trash`.
//!
@@ -540,7 +540,7 @@ pub const Catalog = struct {
}
/// Whether the session's folder still exists; if not, it is tombstoned
/// (`tla/Catalog.tla` `Heal`) and reported once.
/// (`tests/tla/session_manager/Catalog.tla` `Heal`) and reported once.
/// One `stat` of the folder, no open: a published folder always holds
/// its synced log (publish renames it in whole, delete renames it away),
/// so the folder alone decides. `rebuild` checks the logs themselves.
@@ -717,7 +717,7 @@ test "the fold keeps the newest put, merges open times, and a tombstone is final
}
const catalog_model_tests = struct {
//! L3 and L4 against `tla/Catalog.tla`: publish, delete, crashes between
//! L3 and L4 against `tests/tla/session_manager/Catalog.tla`: publish, delete, crashes between
//! the folder change and the index write, self-heal and rebuild, driven
//! through the public API. Every run writes a trace for TLC.
src/core/session_manager/fold.zig
+2 -2
View File
@@ -4,7 +4,7 @@
//! and returns or updates a value it owns. `plan` decides what a batch may
//! write; `apply` folds a written line into the state; `encodeState` and
//! `decodeState` turn the state into a snapshot and back. Resuming from the
//! newest snapshot must equal a full fold (`tla/ResumeSnapshot.tla`).
//! newest snapshot must equal a full fold (`tests/tla/session_manager/ResumeSnapshot.tla`).
const std = @import("std");
const schema = @import("schema.zig");
@@ -313,7 +313,7 @@ pub fn plan(state: *const State, events: []const Event, out: []schema.Body) Tran
break :blk .{ .turn_interrupted = .{ .turn = turn, .reason = reason } };
},
.set => |s| .{ .set = s },
// One unfinished work item per child (`tla/Subagents.tla`
// One unfinished work item per child (`tests/tla/session_manager/Subagents.tla`
// OneOpenWork); a finish names exactly that one.
.child_spawned => |c| blk: {
if (openWorkAt(state, events[0..i], c.child) != null) return error.InvalidTransition;
src/core/session_manager/log.zig
+1 -1
View File
@@ -941,7 +941,7 @@ test "crc32c equals std's byte-at-a-time CRC32C at every length and alignment" {
}
const log_model_tests = struct {
//! L1 against `tla/SessionLog.tla`: random schedules of appends, syncs,
//! L1 against `tests/tla/session_manager/SessionLog.tla`: random schedules of appends, syncs,
//! process crashes (including in the middle of a write), machine crashes and
//! recoveries. After every step the four spec invariants are checked on the
//! real file, and selected runs write a trace for TLC (`zig build traces`).
src/core/session_manager/session.zig
+11 -10
View File
@@ -52,7 +52,7 @@ pub const Env = struct {
catalog_observer: if (hooks) ?CatalogObserver else void = if (hooks) null else {},
planted: if (hooks) trace.Planted else void = if (hooks) .none else {},
/// Hooks only: reports a catalog-level step (`tla/Catalog.tla`).
/// Hooks only: reports a catalog-level step (`tests/tla/session_manager/Catalog.tla`).
pub fn observeCatalog(env: *const Env, id: []const u8, what: CatalogStep) void {
if (hooks) {
const observer = env.catalog_observer orelse return;
@@ -404,7 +404,7 @@ pub const Session = struct {
/// The first turn: stage the session in `.tmp/{id}`, make line 1
/// durable, then rename it into place and sync the root, so a visible
/// session always has a durable first line (`tla/Lifecycle.tla`).
/// session always has a durable first line (`tests/tla/session_manager/Lifecycle.tla`).
fn publish(session: *Session, bodies: []const schema.Body, ts: u64) AppendError!void {
session.writeFirstTurn(bodies, ts) catch |err| {
// Nothing is visible; later calls name the cause (D40).
@@ -456,7 +456,7 @@ pub const Session = struct {
/// the lines framed in `session.batch`, blobs linked from a fork's
/// source, a synced log, the lock, a synced folder, the rename into
/// place, and a synced root. Only then is the session visible, always
/// with a durable first line (`tla/Lifecycle.tla`).
/// with a durable first line (`tests/tla/session_manager/Lifecycle.tla`).
fn stage(session: *Session, source_blobs: ?storage.Dir) AppendError!Live {
const env = session.env;
const s = env.s;
@@ -595,7 +595,7 @@ pub const Session = struct {
}
/// Every blob an item or a setting refers to must already exist in this
/// session (`tla/Fork.tla` `RefsExist`).
/// session (`tests/tla/session_manager/Fork.tla` `RefsExist`).
fn checkBlobRefs(session: *Session, live: *Live, bodies: []const schema.Body) AppendError!void {
if (!hasBlobRefs(bodies)) return;
const s = session.env.s;
@@ -974,12 +974,12 @@ fn hasTurnStart(bodies: []const schema.Body) bool {
return false;
}
/// Durability points (system-design.md "Durable State And Schema").
/// Durability points (`tests/tla/session_manager/system-design.md` "Durable State And Schema").
fn needsSync(bodies: []const schema.Body) bool {
for (bodies) |body| switch (body) {
.turn_committed, .turn_interrupted, .child_spawned, .child_finished => return true,
// Usage is durable before fx clears its usage-recovery marker
// (`tla/Wiring.tla` UsageNeverSilent).
// (`tests/tla/session_manager/Wiring.tla` UsageNeverSilent).
// fx removes the side folder only once the move is durable (D47).
// Compactor records need no sync of their own: the compaction line
// that cites them comes later in the log, which keeps a prefix (D50).
@@ -1268,7 +1268,7 @@ fn mapRead(err: log_mod.ReadError) OpenError {
};
}
/// Crash repair at the end of `openResume` (D1, `tla/Subagents.tla`).
/// Crash repair at the end of `openResume` (D1, `tests/tla/session_manager/Subagents.tla`).
fn repair(session: *Session, workspace: []const u8) AppendError!void {
const gpa = session.env.gpa;
const live = &session.phase.live;
@@ -1278,7 +1278,7 @@ fn repair(session: *Session, workspace: []const u8) AppendError!void {
try session.writeBodies(live, &.{.{ .turn_interrupted = .{ .turn = turn, .reason = .crash } }}, ts, .interrupt_repair);
}
session.observe(.reopened);
// Every unfinished work item gets a known outcome (tla/Subagents.tla).
// Every unfinished work item gets a known outcome (tests/tla/session_manager/Subagents.tla).
var finished: std.ArrayList(schema.Body) = .empty;
defer finished.deinit(gpa);
for (session.state.children.items) |child| {
@@ -1765,7 +1765,7 @@ pub fn childrenOf(env: *const Env, id_: []const u8) DeleteError![][]u8 {
return children.toOwnedSlice(gpa);
}
/// Step 1 of a delete (`tla/Catalog.tla` `Trash`): Busy if the session is
/// Step 1 of a delete (`tests/tla/session_manager/Catalog.tla` `Trash`): Busy if the session is
/// open anywhere, else it is renamed to `.trash/{id}`, which makes it gone
/// for everyone at once. The caller then appends the index tombstone and
/// calls `purgeTrashed`; owned children are deleted first (`childrenOf`),
@@ -3753,7 +3753,8 @@ const session_model_tests = struct {
const parent = t.parent orelse return out.items;
const bytes = (try readLog(t.root, parent)) orelse return out.items;
defer gpa.free(bytes);
// A child's work number counts its spawn lines (`tla/Subagents.tla`).
// A child's work number counts its spawn lines
// (`tests/tla/session_manager/Subagents.tla`).
var works: [2]u64 = .{ 0, 0 };
for (try diskLines(arena, bytes)) |line| {
if (t.horizon) |h| if (line.seq > h) break;
src/core/session_manager/trace.zig
+1 -1
View File
@@ -2,7 +2,7 @@
//!
//! Each traced run writes `zig-out/traces/SPEC--CASE.ndjson`: one JSON line
//! per spec action, named like the action, with one field per spec variable
//! (`docs/session-manager/tla/trace/README.md`). Fields that model the disk
//! (`tests/tla/session_manager/trace/README.md`). Fields that model the disk
//! are read back from the real files after the step; fields that model
//! memory come from the code's own state.
//!
src/core/shell_command/safe_git.zig
+2
View File
@@ -4,6 +4,8 @@
//! drivers and a signature verifier. Every invocation turns those off, while
//! the user's global and system config stay trusted, so a global Git LFS still
//! works. When fx cannot establish that, `prepare` refuses and git does not run.
//!
//! TLA+ model: `tests/tla/shell_command/GitAdmission.tla`.
const std = @import("std");
const builtin = @import("builtin");
src/core/subagent/tool_host.zig
+1 -1
View File
@@ -153,7 +153,7 @@ pub const Runtime = struct {
/// A host over a v2 parent, whose children live in its log (D22).
/// Borrows `children` and the callback contexts until deinit; the
/// parent stays open until then (`tla/Wiring.tla`
/// parent stays open until then (`tests/tla/session_manager/Wiring.tla`
/// ParentOutlivesChildren).
pub fn createV2(
alloc: Allocator,
src/core/terminal/recovery.zig
+2
View File
@@ -56,6 +56,8 @@ pub const Decision = struct {
screen_unavailable: ?contracts.ScreenUnavailableReason,
};
/// Decides what happens to a terminal record a process finds. The terminal
/// lifecycle is modeled in `tests/tla/terminal/TerminalLifecycle.tla`.
pub fn reconcile(input: Input) Decision {
if (input.record != .valid) {
return .{
src/core/terminal/shell_snapshot.zig
+2
View File
@@ -10,6 +10,8 @@
//!
//! Snapshot contents stay in memory. They reach a command only through its
//! environment and the supervisor's stdin script, and are never logged.
//!
//! TLA+ model: `tests/tla/terminal/ShellSnapshot.tla`.
const std = @import("std");
const builtin = @import("builtin");
src/core/workspace/grep_search.zig
+1
View File
@@ -59,6 +59,7 @@ pub const CountResult = struct {
/// owned by `arena`, which only the calling thread uses. `scratch` must be
/// thread-safe; it backs the listing and the content scan and is released
/// before return, so retained memory grows with matches, not scanned bytes.
/// The parallel search and its merge are modeled in `tests/tla/indexer/GrepCut.tla`.
pub fn collectDirectoryMatches(
scratch: Allocator,
arena: Allocator,
src/core/workspace/tool_files.zig
+2 -2
View File
@@ -73,7 +73,7 @@ fn relativeInside(workspace_root: []const u8, absolute_root: []const u8) ?[]cons
/// Whether the workspace tree's entries below `subtree` are exactly what a
/// scan of that folder would list: the walk entered it as an ordinary folder
/// of the workspace, not as a nested repository's boundary and not below an
/// ignored folder, where a direct scan applies the plain rules instead (U3).
/// ignored folder, where a direct scan applies the plain rules instead.
fn subtreeFromSnapshot(tree: *const indexer.Tree, subtree: []const u8) bool {
if (subtree.len == 0) return true;
for (tree.folders) |folder| {
@@ -204,7 +204,7 @@ test "listing sees a file created a moment earlier and honors hidden and custom
const root = try @import("../shared/io.zig").dirRealpathAlloc(arena, tmp.dir, "root");
// The temporary folder sits below an ignored path, so the skipped names
// apply (U3); `build` is skipped by default.
// apply; `build` is skipped by default.
const first = try list(std.testing.allocator, arena, root, root, .{});
try std.testing.expectEqual(@as(usize, 3), first.files.len);
try std.testing.expectEqualStrings("a.txt", first.files[0]);
src/mcp/core/auth.zig
+2
View File
@@ -9,6 +9,8 @@
//!
//! Pure. Tokens, URLs, and strings are the host's: a token is named by its
//! generation, issuers are numbered from 1, and scopes are bits.
//!
//! TLA+ models: `tests/tla/mcp/AuthGate.tla` (`Gate`) and `tests/tla/mcp/AuthFlow.tla` (`Flow`).
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/catalog.zig
+2
View File
@@ -7,6 +7,8 @@
//! invalidated since its listing started and, on a modern server, if
//! every page had a positive TTL; the shortest one sets its expiry. A legacy
//! list stays fresh until an invalidation or a new process.
//!
//! TLA+ model: `tests/tla/mcp/Catalog.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/elicitation.zig
+2
View File
@@ -5,6 +5,8 @@
//! and elicitationId by slot, and maps the server's cancels and completion
//! notifications to slots. 2026 rounds are `core/mrtr.zig`'s chains; the host's answers
//! there go through the same reader. Pure.
//!
//! TLA+ model: `tests/tla/mcp/Elicitation.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/engine.zig
+2
View File
@@ -6,6 +6,8 @@
//! call waits for it (LazyConnect), at most `max_attempts` times in a row,
//! and after a failure only once its backoff is over. A step that
//! also starts the server is traced as a second record. Pure.
//!
//! TLA+ model: `tests/tla/mcp/Engine.tla`.
const std = @import("std");
const request = @import("request.zig");
src/mcp/core/era.zig
+2
View File
@@ -5,6 +5,8 @@
//! a `Listed` mask over them, so the core never stores the server's strings.
//! The `classify*` functions turn a server's answer into an event, and the
//! `write*` functions build the detection messages.
//!
//! TLA+ model: `tests/tla/mcp/Era.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/http_legacy.zig
+2
View File
@@ -5,6 +5,8 @@
//!
//! The host keeps the strings: the session id and each stream's last event
//! id. This core only decides what goes out.
//!
//! TLA+ model: `tests/tla/mcp/HttpLegacy.tla`.
const std = @import("std");
const request = @import("request.zig");
src/mcp/core/http_modern.zig
+2
View File
@@ -4,6 +4,8 @@
//!
//! Each `post` effect is a new attempt: a new request, so a new id.
//! The request table never reuses ids, so this core holds none.
//!
//! TLA+ model: `tests/tla/mcp/HttpModern.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/mrtr.zig
+2
View File
@@ -2,6 +2,8 @@
//! tools/call. The host keeps the strings, the requestState and the input
//! requests; this core only decides.
//! A requestState is named by the round whose answer brought it.
//!
//! TLA+ model: `tests/tla/mcp/Mrtr.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/request.zig
+2
View File
@@ -9,6 +9,8 @@
//! duplicate messages for it are recognized and ignored. Responses without an
//! id can't be correlated; the I/O layer logs them and the request still
//! ends through its timeout.
//!
//! TLA+ model: `tests/tla/mcp/Request.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/stdio_conn.zig
+2
View File
@@ -6,6 +6,8 @@
//! Every process gets a new generation. Lines, timers, and exits carry the
//! generation they belong to, so anything from an earlier process is dropped
//! (NoStaleDelivery, SignalsOnTime, NoEarlyRestart).
//!
//! TLA+ model: `tests/tla/mcp/StdioConn.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/core/subscription.zig
+2
View File
@@ -2,6 +2,8 @@
//! The caller owns the listen requests, whose ids come from the request table
//! as kind `listen` (no timeouts), and the transport: it opens with
//! `opened` after `canOpen`, and answers `relisten` with `resent`.
//!
//! TLA+ model: `tests/tla/mcp/Subscription.tla`.
const std = @import("std");
const trace = @import("../io/trace.zig");
src/mcp/io/trace.zig
+5 -4
View File
@@ -1,9 +1,10 @@
//! JSONL trace of core steps (docs/approach.md §6, format version 1).
//! 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");
src/mcp/mcp.zig
+1 -1
View File
@@ -1,7 +1,7 @@
//! MCPv2 module root and public API.
//!
//! Files under `src/mcp/` import only `std` and each other. The host passes in
//! `std.Io` and everything else through `host.zig`. See `docs/approach.md`.
//! `std.Io` and everything else through `host.zig`.
const std = @import("std");
src/tools/shell/shell.zig
+3
View File
@@ -101,6 +101,9 @@ const OwnedInput = struct {
}
};
/// Decodes one shell call's arguments. How each argument shape is decoded,
/// admitted, and shown in history is modeled in
/// `tests/tla/shell_command/ShellContract.tla`.
pub fn decode(
ctx: tool_dispatch.DispatchContext,
args_json: []const u8,
src/usage/cache.zig
+3
View File
@@ -2,6 +2,9 @@
//! Every fx process reads it without a lock (writes land by rename) and
//! writes it under an exclusive lock as read, merge, write, rename, so a
//! newer answer is never replaced by an older one (`CacheNeverRegresses`).
//!
//! TLA+ model of the cache shared by several processes:
//! `tests/tla/usage/UsageModel.tla`.
const std = @import("std");
const report = @import("report.zig");
src/usage/policy.zig
+1 -1
View File
@@ -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");
src/usage/view.zig
+1 -1
View File
@@ -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");
tests/AGENTS.md
+102
View File
@@ -0,0 +1,102 @@
# AGENTS.md
Instructions for work under `tests/`. They supplement the repository-level `AGENTS.md`, which still owns the readiness rules, CI gates, and Zig conventions.
`tests/` holds the checks that run against the built binary or against a model of its design. Unit tests do not live here: Zig tests stay inline in the `src/` file they cover.
## Where a test belongs
Pick the lowest layer that proves the behavior, and extend the closest existing file before creating a new one.
| What you are proving | Where it goes |
| --- | --- |
| A parser, policy, reducer, formatter, or state transition | An inline `test` block in the owning `src/` file |
| Terminal cells, wrapping, cursor, scroll, or resize | `src/ui/resize_tests.zig` or a VT test in the owning UI file |
| CLI, ACP, or TUI behavior of the built binary | A root `tests/e2e/*.test.ts` file; terminal flows use `tui-*.test.ts` |
| fx against the official MCP client conformance suite | `tests/e2e/conformance/`, an isolated npm project |
| Evidence tooling for terminal rendering bugs | `tests/e2e/render-lab/` |
| Task quality or tool choice with real models | `tests/evals/` |
| A protocol or crash-safety design, checked with TLC | A folder under `tests/tla/` named after the module it models |
| libfx SDK behavior | `sdk/tests/`, which `sdk/AGENTS.md` owns |
| Startup latency or memory | `benchmarks/` |
## Layout
```text
tests/
├── e2e/ deterministic runtime tests, run on every pull request
│ ├── *.test.ts one file per feature area, all at this level
│ ├── *.ts shared helpers, such as tmux-helpers.ts and tui-render-assertions.ts
│ ├── fixtures/ fake servers, MCP servers, and recorded captures
│ ├── conformance/ MCP conformance package, run with npm
│ └── 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 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
└── <area>/ 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.
## Write an E2E test
- Build first with `zig build`. Tests run `zig-out/bin/fx` through `FX_BIN` from `tests/evals/eval-helpers.ts`, never an installed `fx`.
- Give every test its own profile with `createIsolatedTestHome()` and remove it with `cleanupIsolatedTestHome()`. A test must never read or write the developer's `~/.fx`.
- Keep the network local. Point fx at a fake model server with `startFakeGateway()` or `startDynamicFakeGateway()` from `tmux-helpers.ts`, or the builders in `fixtures/chat-completions.ts`. `TmuxSession` clears credentials and the `FX_E2E_*` overrides from the inherited environment.
- Wait for state the user can see: `TmuxSession.waitForText()`, `waitForStableGrid()`, `waitForComposer()`, or `waitForSessionEnd()`. A fixed sleep can pace input, but it does not prove the state you assert next.
- Skip, do not fail, a terminal test when tmux is missing: `test.skipIf(!tmuxAvailable())`.
- A new test must not play sound. `TmuxSession` and the fixtures set `FX_SOUND=0`; set it yourself when you spawn fx another way. Sound playback is covered only by `notifications.test.ts` and the `/sound on` test in `tui-command-permissions.test.ts`, so keep sound coverage there. The repository `AGENTS.md` explains how to run them locally.
- Fixtures are public. Use `/Users/example/` for home paths and never commit credentials. `scripts/check-public-surface.sh` rejects personal paths, real team IDs, and internal or personal project slugs.
## Wire an E2E file into CI
Every root `tests/e2e/*.test.ts` file needs these entries in the same change, and removing a file means removing them:
1. A positive integer weight in `tests/e2e/ci-shard-weights.json`. CI splits the files into four shards by weight.
2. Exactly one classification in `scripts/pgso/corpus.json`: a training scenario, a verification scenario, or an intentional exclusion with its reason. The repository `AGENTS.md` explains how to choose.
3. An entry in `tests/e2e/macos-platform-tests.json` when the file branches on `process.platform` or `platform()` being `darwin` or `linux`.
CI runs each file in its own Bun process and tmux server through `tests/e2e/ci-run-files.sh` and retries a failure once. A file that passes only on retry is reported as a warning: treat it as a race to fix, not a pass.
Check the wiring locally:
```sh
cd tests/e2e && bun test ci-shards.test.ts
python3 -m scripts.pgso.corpus --manifest scripts/pgso/corpus.json --list # from the repository root
```
## Evals
`tests/evals/` drives the agent through `fx ask --json` against real models. It needs `AI_GATEWAY_API_KEY` or `VERCEL_OIDC_TOKEN`, makes billed calls, and varies between runs, so it is not a pull request check. Do not move a deterministic check here; put it in `tests/e2e/` with a fake gateway.
## TLA+ models
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/`, `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/<area>/`. 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`.
## Cite tests and specs from `src/`
Code comments point readers at the test or model that pins a behavior. Keep those references stable and public.
- Cite by repository-relative path, plus the property, action, or test name, so a reader can open it without searching: ``(`tests/tla/session_manager/Wiring.tla` ParentOutlivesChildren)``.
- Cite session-manager design decisions by number, such as `(D44)`. They are defined in `tests/tla/session_manager/system-design.md`.
- Name a test by its file and test name, not by line number. Line numbers move with every edit.
- Cite only files in this repository. A reference to a local note, private harness, or file outside the tree is a dead end for every other contributor; describe the behavior instead.
- When you move or rename a test or spec, update every citation in the same change. A `git grep` for the old path should return nothing.
## Before you finish
- Run the check for what you changed: the E2E file, such as `FX_SOUND=0 bun test cli.test.ts` from `tests/e2e/`; the folder's `check.sh` under `tests/tla/`; or `zig build test` for inline Zig tests.
- After adding, removing, or renaming an E2E file, run the wiring checks above.
- Do not run the full E2E suite locally as your development loop. CI runs it on the pull request, and a passing focused run does not replace that result.
tests/e2e/sessions-v2.test.ts
+3 -3
View File
@@ -2025,9 +2025,9 @@ test("a crash while a named subagent works records it interrupted, and its next
expect(JSON.parse(resumed.stdout).output).toBe("AFTER_LOST_DONE");
// The reopen recorded the started work as interrupted, as
// `tla/Subagents.tla` repairs a child with a log; the next message is new
// work for the same child. A child streams no pieces, so its log holds
// nothing of the lost work.
// `tests/tla/session_manager/Subagents.tla` repairs a child with a
// log; the next message is new work for the same child. A child streams
// no pieces, so its log holds nothing of the lost work.
const lines = childLines(fixture, id);
expect(lines.map((line) => [line.kind, line.outcome ?? null])).toEqual([
["child_spawned", null], ["child_finished", "interrupted"], ["child_spawned", null], ["child_finished", "ok"],
tests/tla/.gitignore
+1
View File
@@ -0,0 +1 @@
__pycache__/
tests/tla/README.md
+82
View File
@@ -0,0 +1,82 @@
# TLA+ models
TLA+ specifications for fx, checked with TLC, together with the scripts and Bun drivers that check them. CI runs the SDK model. Run the others when you change the behavior they describe.
| Folder | What it models | Checker |
|---|---|---|
| `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
Java 11 or later and `tla2tools.jar`:
```sh
brew install openjdk
mkdir -p ~/.local/share/tla
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 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 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:
```sh
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/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
```
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.
tests/tla/acp/AcpPermissionModes.tla
+210
View File
@@ -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 == <<profile, cur, saved, last>>
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 <<profile, cur, saved>>
\* 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 <<profile, cur, saved>>
Prompt ==
/\ saved' = TRUE
/\ last' = Obs("prompt", "none", TRUE, FALSE, NoView, Enforce(cur), profile)
/\ UNCHANGED <<profile, cur>>
\* 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 <<profile, saved>>
\* 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 <<cur, saved>>
\* `fx status --json` in the workspace, run beside the ACP process.
Status ==
/\ last' = Obs("status", "none", TRUE, TRUE, StatusView(Eff(profile)), "none", profile)
/\ UNCHANGED <<profile, cur, saved>>
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 <<profile, cur>>]_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
=============================================================================
tests/tla/acp/AcpPermissionModesTrace.tla
+50
View File
@@ -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 == <<vars, i>>
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)
=============================================================================
tests/tla/acp/AcpSpeed.tla
+138
View File
@@ -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 == <<model, fast, ultra, last>>
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 <<model, fast, ultra>>
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 <<model, fast, ultra>>
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 <<model, fast, ultra>>
Prompt ==
/\ last' = Result("prompt", "none", TRUE, RequestSpeed)
/\ UNCHANGED <<model, fast, ultra>>
(* 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 <<model, fast, ultra>>
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
=============================================================================
tests/tla/acp/AcpSpeedTrace.tla
+52
View File
@@ -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 == <<vars, i>>
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)
=============================================================================
tests/tla/acp/MCAcpPermissionModes.cfg
+22
View File
@@ -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
tests/tla/acp/MCAcpPermissionModes.tla
+9
View File
@@ -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"}
=============================================================================
tests/tla/acp/MCAcpSpeed.cfg
+22
View File
@@ -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
tests/tla/acp/MCAcpSpeed.tla
+9
View File
@@ -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"}
=============================================================================
tests/tla/acp/check.sh
Executable
+26
View File
@@ -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
tests/tla/cli/LaunchSelection.tla
+268
View File
@@ -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 == <<st>>
(* ----------------------------- 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
=============================================================================
tests/tla/cli/LaunchTrace.tla
+65
View File
@@ -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 == <<st, k>>
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)
=============================================================================
tests/tla/cli/check.sh
Executable
+38
View File
@@ -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 "$@" <<EOF
LaunchSelection proposed -
LaunchSelection current-holds -
LaunchSelection current-model ValidModel
LaunchSelection current-speed HonestSpeed
LaunchSelection current-effort HonestEffort
LaunchSelection current-late-error AskFailsEarly
LaunchSelection current-canonical Canonical
LaunchSelection mutant-reject-weak NoFalseReject
LaunchSelection mutant-no-canonical Canonical
LaunchSelection mutant-block-frame FirstFrameNotBlocked
LaunchSelection mutant-persist SettingsUntouched
LaunchSelection mutant-silent CorrectionsAnnounced
LaunchSelection simulate-ideal simulate $sim
LaunchSelection simulate-nonideal simulate $sim
EOF
tests/tla/cli/current-canonical.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
Canonical
tests/tla/cli/current-effort.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
HonestEffort
tests/tla/cli/current-holds.cfg
+11
View File
@@ -0,0 +1,11 @@
SPECIFICATION FairSpec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
NoFalseReject
SettingsUntouched
FirstFrameNotBlocked
CorrectionsAnnounced
PROPERTY Termination
tests/tla/cli/current-late-error.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
AskFailsEarly
tests/tla/cli/current-model.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
ValidModel
tests/tla/cli/current-speed.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "current"
Mutant = "none"
Class = "all"
INVARIANTS
HonestSpeed
tests/tla/cli/mutant-block-frame.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "block_frame"
Class = "all"
INVARIANTS
FirstFrameNotBlocked
tests/tla/cli/mutant-no-canonical.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "no_canonical"
Class = "all"
INVARIANTS
Canonical
tests/tla/cli/mutant-persist.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "persist"
Class = "all"
INVARIANTS
SettingsUntouched
tests/tla/cli/mutant-reject-weak.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "reject_weak"
Class = "all"
INVARIANTS
NoFalseReject
tests/tla/cli/mutant-silent.cfg
+7
View File
@@ -0,0 +1,7 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "silent"
Class = "all"
INVARIANTS
CorrectionsAnnounced
tests/tla/cli/proposed.cfg
+16
View File
@@ -0,0 +1,16 @@
SPECIFICATION FairSpec
CONSTANTS
Design = "proposed"
Mutant = "none"
Class = "all"
INVARIANTS
ValidModel
HonestSpeed
HonestEffort
AskFailsEarly
NoFalseReject
Canonical
SettingsUntouched
FirstFrameNotBlocked
CorrectionsAnnounced
PROPERTY Termination
tests/tla/cli/simulate-ideal.cfg
+15
View File
@@ -0,0 +1,15 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "none"
Class = "ideal"
INVARIANTS
ValidModel
HonestSpeed
HonestEffort
AskFailsEarly
NoFalseReject
Canonical
SettingsUntouched
FirstFrameNotBlocked
CorrectionsAnnounced
tests/tla/cli/simulate-nonideal.cfg
+15
View File
@@ -0,0 +1,15 @@
SPECIFICATION Spec
CONSTANTS
Design = "proposed"
Mutant = "none"
Class = "nonideal"
INVARIANTS
ValidModel
HonestSpeed
HonestEffort
AskFailsEarly
NoFalseReject
Canonical
SettingsUntouched
FirstFrameNotBlocked
CorrectionsAnnounced
tests/tla/drivers/acp/permission_modes/check-spec.ts
+190
View File
@@ -0,0 +1,190 @@
// Exhaustive TLC check of the permission-mode contract plus mutation
// qualification: each planted mutant must violate the named property, which
// shows the properties are strong enough to catch that mistake.
//
// bun tests/tla/drivers/acp/permission_modes/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: "new-reports-ask",
note: "a new session reports Ask whatever fx enforces (an earlier fx)",
from: `/\\ last = Obs("new", "none", TRUE, TRUE, SessionView(Eff(profile)), "none", profile)`,
to: `/\\ last = Obs("new", "none", TRUE, TRUE, SessionView("ask"), "none", profile)`,
expect: "ReportsEnforcedMode",
},
{
id: "lists-code",
note: "the options still list the old code mode",
from: `[current |-> 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 <<profile, cur>>`,
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 <<cur, saved>>`,
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 <<profile, cur, saved>>`,
to: `ELSE /\\ last' = Obs("set", v, FALSE, FALSE, NoView, "none", profile)\n /\\ cur' = "ask"\n /\\ UNCHANGED <<profile, saved>>`,
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();
tests/tla/drivers/acp/permission_modes/driver.ts
+331
View File
@@ -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 = <T>(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<ReturnType<typeof loadHelpers>>, 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<Record<string, number>>((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();
tests/tla/drivers/acp/permission_modes/harness.ts
+340
View File
@@ -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<number>;
constructor(readonly proc: ReturnType<typeof Bun.spawn>, 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<Uint8Array>) {
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<Uint8Array>) this.stderr += decoder.decode(chunk);
})();
}
private async readLine(): Promise<any> {
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<string>((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<string, unknown>): Promise<any> {
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<string, unknown>) => Response;
};
export async function loadHelpers(worktree: string): Promise<Helpers> {
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<string, unknown> = { 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<string, string> {
const env: Record<string, string> = {};
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<Acp> {
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<Acp> {
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 });
}
}
tests/tla/drivers/acp/permission_modes/tlc.ts
+13
View File
@@ -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);
}
tests/tla/drivers/acp/permission_modes/trace.ts
+76
View File
@@ -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;
}
tests/tla/drivers/acp/speed/check-spec.ts
+115
View File
@@ -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();
tests/tla/drivers/acp/speed/driver.ts
+370
View File
@@ -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 = <T>(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<string, string> = {};
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<Record<string, number>>((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();
tests/tla/drivers/acp/speed/explain.ts
+55
View File
@@ -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 <report>/traces/<name>
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 <trace dir>");
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)"}`);
}
tests/tla/drivers/acp/speed/tlc.ts
+13
View File
@@ -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);
}
tests/tla/drivers/acp/speed/trace.ts
+186
View File
@@ -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<number>;
constructor(readonly proc: ReturnType<typeof Bun.spawn>, 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<Uint8Array>) {
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<Uint8Array>) this.stderr += decoder.decode(chunk);
})();
}
private async readLine(): Promise<any> {
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<string>((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<string, unknown>): Promise<any> {
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;
}
sdk/tests/model/agent-process.mjs → tests/tla/drivers/agent-process.mjs
+3 -3
View File
@@ -6,11 +6,11 @@
// all until a step delivers one here, to the queue handler of the World the
// driver picks.
import { parentPort, workerData } from "node:worker_threads";
import { createDurableAgentFactory, foldSessionLog } from "../../durable.js";
import { world } from "../../durable/world.mjs";
import { createDurableAgentFactory, foldSessionLog } from "../../../sdk/durable.js";
import { world } from "../../../sdk/durable/world.mjs";
const { names, mode } = workerData;
const { createWorld } = await import(new URL("../../durable/node_modules/@workflow/world-local/dist/index.js", import.meta.url).href);
const { createWorld } = await import(new URL("../../../sdk/durable/node_modules/@workflow/world-local/dist/index.js", import.meta.url).href);
const encoder = new TextEncoder();
const inner = Symbol("handler");
tests/tla/drivers/cli/bridge.ts
+129
View File
@@ -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<string, unknown>;
}
export interface TraceResult {
design: Design;
verdict: Verdict;
detail: string;
firstMismatch?: string;
hashes: Record<string, string>;
}
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<TraceResult> {
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" };
}
tests/tla/drivers/cli/launch.test.ts
+255
View File
@@ -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<boolean> {
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<string, string>;
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<string, string> = {};
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<Observation> {
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<Observation> {
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<Observation[]> | undefined;
function observations(): Promise<Observation[]> {
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<Design, Promise<TraceResult>>();
function verdict(design: Design): Promise<TraceResult> {
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);
tests/tla/drivers/cli/scenarios.ts
+136
View File
@@ -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<Notice>();
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();
}
sdk/tests/model/drive-agents.mjs → tests/tla/drivers/drive-agents.mjs
+2 -2
View File
@@ -2,7 +2,7 @@
// AgentRouting.tla, and checks after every step that the code is where the
// model allows.
//
// bun sdk/tests/model/drive-agents.mjs [send|consume] [--walks N] [--depth N] [--seed S]
// bun tests/tla/drivers/drive-agents.mjs [send|consume] [--walks N] [--depth N] [--seed S]
//
// Two processes, p1 and p2, are two worker threads (agent-process.mjs), each
// with a module instance and a globalThis of its own: p1 has the agents S
@@ -45,7 +45,7 @@ const random = () => {
const pick = (items) => items[Math.floor(random() * items.length)];
const here = fileURLToPath(new URL(".", import.meta.url));
const graph = await loadGraph(resolve(here, "graphs", `agents-${mode}.dot`));
const graph = await loadGraph(resolve(here, "../sdk/graphs", `agents-${mode}.dot`));
const hosts = { p1: ["S", "C"], p2: ["S"] };
// The queue the processes share: every message, until a step delivers it.
sdk/tests/model/drive-steer.mjs → tests/tla/drivers/drive-steer.mjs
+7 -6
View File
@@ -3,10 +3,11 @@
// WebAssembly, along paths of the TLC state graph of DurableSteer.tla, and
// checks after every step that the code is in a state the model allows.
//
// bun sdk/tests/model/drive-steer.mjs [ideal|faults] [--walks N] [--seed S]
// bun tests/tla/drivers/drive-steer.mjs [ideal|faults] [--walks N] [--seed S]
// [--backend native|wasm] [--durability local|world] [--verbose]
//
// `./check.sh` model-checks the spec and writes graphs/steer-<graph>.dot. The
// `tests/tla/sdk/check.sh` model-checks the spec and writes its
// graphs/steer-<graph>.dot. The
// ideal graph has no faults; the faults graph adds cancels, deadline handoffs
// and client retries.
//
@@ -23,8 +24,8 @@ import { mkdtemp, readFile, rm } from "node:fs/promises";
import { tmpdir } from "node:os";
import { join, resolve } from "node:path";
import { fileURLToPath } from "node:url";
import { createFxAgent } from "../../node.js";
import { local } from "../../durable/local.mjs";
import { createFxAgent } from "../../../sdk/node.js";
import { local } from "../../../sdk/durable/local.mjs";
import { loadGraph } from "./graph.mjs";
const args = process.argv.slice(2);
@@ -42,7 +43,7 @@ let seed = Number(option("seed", 1));
const here = fileURLToPath(new URL(".", import.meta.url));
const addon = resolve(here, "../../../zig-out/lib/libfx.node");
const wasm = backend === "wasm" ? await readFile(resolve(here, "../../../zig-out/bin/fx-core.wasm")) : undefined;
const { appWorldAt, closeAppWorlds } = durabilityKind === "world" ? await import("../app-world.mjs") : {};
const { appWorldAt, closeAppWorlds } = durabilityKind === "world" ? await import("../../../sdk/tests/app-world.mjs") : {};
const durableInternals = Symbol.for("libfx.durableInternals");
const stepTimeoutMs = 8000;
// How long the code must show the same state before the driver reads it.
@@ -352,7 +353,7 @@ const random = () => {
return seed / 2147483648;
};
const graph = await loadGraph(resolve(here, "graphs", `steer-${graphName}.dot`));
const graph = await loadGraph(resolve(here, "../sdk/graphs", `steer-${graphName}.dot`));
const covered = new Set();
const totalEdges = [...graph.next.values()].reduce((sum, targets) => sum + targets.size, 0);
let steps = 0;
sdk/tests/model/drive.mjs → tests/tla/drivers/drive.mjs
+12 -11
View File
@@ -3,7 +3,7 @@
// WebAssembly, along paths of the TLC state graph of DurableSession.tla, and
// checks after every step that the code is in a state the model allows.
//
// bun sdk/tests/model/drive.mjs [send|lookup|write|cutoff|leased|queue] [--walks N] [--seed S] [--backend native|wasm]
// bun tests/tla/drivers/drive.mjs [send|lookup|write|cutoff|leased|queue] [--walks N] [--seed S] [--backend native|wasm]
// [--durability local|world|vercel]
//
// The lookup and cutoff graphs run a lookup, which starts before its intent
@@ -32,7 +32,8 @@
// session in Vercel's World (see sdk/tests/vercel-storage.mjs for what it
// needs) instead of files.
//
// `./check.sh` model-checks the spec and writes graphs/<graph>.dot; the cutoff
// `tests/tla/sdk/check.sh` model-checks the spec and writes its
// graphs/<graph>.dot; the cutoff
// graph runs lookup with more claims and no freezes, so a step can be cut off
// at the deadline until the bound stops running it. Each walk
// starts two agents, A and B, on one local() World directory. Every model
@@ -47,9 +48,9 @@ import { mkdtemp, readFile, rm } from "node:fs/promises";
import { tmpdir } from "node:os";
import { join, resolve } from "node:path";
import { fileURLToPath } from "node:url";
import { createFxAgent } from "../../node.js";
import { local } from "../../durable/local.mjs";
import { holdWrites } from "../hold-writes.mjs";
import { createFxAgent } from "../../../sdk/node.js";
import { local } from "../../../sdk/durable/local.mjs";
import { holdWrites } from "../../../sdk/tests/hold-writes.mjs";
import { loadGraph } from "./graph.mjs";
const args = process.argv.slice(2);
@@ -74,8 +75,8 @@ if ((graphName === "queue") !== (durabilityKind === "queue")) throw new Error("t
// How long a leased worker's lease lasts after its last renewal.
const leaseMs = 1000;
const leasedWorld = leased ? await (async () => {
const { createWorld } = await import(new URL("../../durable/node_modules/@workflow/world-local/dist/index.js", import.meta.url).href);
const { world } = await import("../../durable/world.mjs");
const { createWorld } = await import(new URL("../../../sdk/durable/node_modules/@workflow/world-local/dist/index.js", import.meta.url).href);
const { world } = await import("../../../sdk/durable/world.mjs");
return (dir) => world(() => createWorld({ dataDir: dir, recoverActiveRuns: false }), { name: "leased", pollMs: 250, leaseMs });
})() : null;
// Vercel's World is a round trip away: settle, wait for streams, and give up
@@ -84,10 +85,10 @@ const remote = durabilityKind === "vercel";
const settleMs = remote ? 1500 : 60;
const streamQuietMs = remote ? 2500 : 120;
const stepTimeoutMs = remote ? 30_000 : 5000;
const { vercelStorage } = remote ? await import("../vercel-storage.mjs") : {};
const { appWorldAt, closeAppWorlds } = durabilityKind === "world" ? await import("../app-world.mjs") : {};
const { vercelStorage } = remote ? await import("../../../sdk/tests/vercel-storage.mjs") : {};
const { appWorldAt, closeAppWorlds } = durabilityKind === "world" ? await import("../../../sdk/tests/app-world.mjs") : {};
const queued = durabilityKind === "queue";
const { queueWorldAt, closeQueueWorlds } = queued ? await import("../queue-world.mjs") : {};
const { queueWorldAt, closeQueueWorlds } = queued ? await import("../../../sdk/tests/queue-world.mjs") : {};
const verbose = args.includes("--verbose");
let seed = Number(option("seed", 1));
const here = fileURLToPath(new URL(".", import.meta.url));
@@ -493,7 +494,7 @@ const random = () => {
return seed / 2147483648;
};
const graph = await loadGraph(resolve(here, "graphs", `${graphName}.dot`));
const graph = await loadGraph(resolve(here, "../sdk/graphs", `${graphName}.dot`));
const covered = new Set();
const totalEdges = [...graph.next.values()].reduce((sum, targets) => sum + targets.size, 0);
let steps = 0;
sdk/tests/model/graph.mjs → tests/tla/drivers/graph.mjs
+2 -2
View File
@@ -1,4 +1,4 @@
// The state graphs check.sh has TLC write, as the model drivers read them.
// The state graphs tests/tla/sdk/check.sh has TLC write, as the drivers read them.
import { strict as assert } from "node:assert";
import { readFile } from "node:fs/promises";
@@ -67,7 +67,7 @@ export function parseValue(text) {
/** The graph check.sh wrote to `path`: each state by id, its successors, and the initial state. */
export async function loadGraph(path) {
const dot = await readFile(path, "utf8").catch(() => {
throw new Error(`${path} is missing; run sdk/tests/model/check.sh first`);
throw new Error(`${path} is missing; run tests/tla/sdk/check.sh first`);
});
const states = new Map();
const next = new Map();
tests/tla/drivers/lib/context.ts
+50
View File
@@ -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: <checkout>/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<string, string>, inherited = process.env): Record<string, string> {
const result: Record<string, string> = {};
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,
};
}
tests/tla/drivers/lib/tlc.ts
+131
View File
@@ -0,0 +1,131 @@
// 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, mkdtempSync, 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 new private output folder for one driver run, made by mkdtemp directly
/// in FX_TLA_OUT or the system temp folder, so another user cannot plant a
/// file or link where output will be written. The caller owns its contents.
export function outDir(name: string): string {
const base = process.env.FX_TLA_OUT;
if (base) mkdirSync(base, { recursive: true });
return mkdtempSync(join(base ?? tmpdir(), `fx-tla-${name}-${utcStamp()}-`));
}
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<TlcRun> {
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");
}
tests/tla/drivers/mcp/bridge.test.ts
+108
View File
@@ -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");
});
});
Loaded 100 of 499 files, more files were not shown because too many files have changed in this diff. Show more