mirror of
https://github.com/vercel-labs/fx.git
synced 2026-10-28 18:25:19 +08:00
Pranit
73b9704036
- Add models, checkers, and Bun drivers for ACP permission modes and speed, launch flags, durable libfx, the MCP-v2 engine and the MCP host, /usage, the shell tool and git admission, the shell snapshot and terminal lifecycle, the libfx provider credential edge, the indexer's grep, file picker, and snapshot reuse, and the session rollout. - Add tests/tla/lib/ and tests/tla/drivers/lib/ so every checker and driver finds TLC and Java the same way, gives each TLC run its own temp folder, runs the binary from this checkout, and keeps sound off. - Add tests/tla/mcp/rules.md, the MCP specification rules the MCP-v2 models cite by ID. - Mark the models that describe the next MCP-v2 version, and run their drivers only with --next or FX_TLA_NEXT_MCP=1. - Point the /usage and MCP trace comments in src/ at their models, and update tests/tla/README.md, tests/AGENTS.md, and CONTRIBUTING.md.
20 lines
978 B
Plaintext
20 lines
978 B
Plaintext
---------------------------- MODULE ShellOracle ----------------------------
|
|
(***************************************************************************)
|
|
(* Prints the model's emission set and Record(e) for every emission. *)
|
|
(* bun/bridge.ts uses it to require that the runtime observed every *)
|
|
(* modeled call, and to explain a mismatch. It never decides acceptance; *)
|
|
(* ShellTrace does. *)
|
|
(***************************************************************************)
|
|
EXTENDS ShellContract, FiniteSets
|
|
|
|
Line(e) ==
|
|
LET r == Record(e) IN
|
|
<<"FXT_PREDICT", e.intent, e.shape, r.accepted, r.decoded, r.history, r.outcome>>
|
|
|
|
(* The count lets the bridge refuse a partial parse of the lines below. *)
|
|
ASSUME PrintT(<<"FXT_EMITS", Cardinality(Emits)>>)
|
|
ASSUME \A e \in Emits : PrintT(Line(e))
|
|
|
|
OracleNext == UNCHANGED vars
|
|
=============================================================================
|