diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7688d008b..1a583304d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -113,7 +113,7 @@ jobs: strategy: fail-fast: false matrix: - target: [unit, stdlib, examples] + target: [unit, stdlib, examples, test-llm, test-mcp] steps: - uses: actions/checkout@v4 - uses: actions/download-artifact@v4 diff --git a/Makefile b/Makefile index 62ace7ba2..2fb3307a9 100644 --- a/Makefile +++ b/Makefile @@ -13,6 +13,12 @@ CHECK += --jobs="$(ECJOBS)" CHECK += --bin-args=-timeout --bin-args="$(ECTOUT)" CHECK += $(foreach arg,$(ECARGS),--bin-args="$(arg)") CHECK += $(ECEXTRA) config/tests.config +LLMCHECK := scripts/testing/llm-golden +LLMCHECK += --bin=./ec.native +MCPCHECK := scripts/testing/mcp-golden +MCPCHECK += --bin=./ec.native +MCPPARITY := scripts/testing/mcp-parity +MCPPARITY += --bin=./ec.native NIX ?= nix --extra-experimental-features "nix-command flakes" PROFILE ?= dev @@ -22,6 +28,7 @@ UNAME_S = $(shell uname -s) # -------------------------------------------------------------------- .PHONY: default build byte native tests check examples +.PHONY: test-llm test-mcp .PHONY: nix-build nix-build-with-provers nix-develop .PHONY: clean install uninstall @@ -51,7 +58,14 @@ stdlib: build examples: build $(CHECK) examples mee-cbc -check: unit stdlib examples +test-llm: build + $(LLMCHECK) + +test-mcp: build + $(MCPCHECK) + $(MCPPARITY) + +check: unit stdlib examples test-llm test-mcp @true nix-build: diff --git a/README.md b/README.md index 9ef3d2917..c493052ec 100644 --- a/README.md +++ b/README.md @@ -166,6 +166,13 @@ with proof scripts). At present, the only available front-end is based on Emacs' [Proof General](https://github.com/ProofGeneral/PG). However, a front-end for VSCode is currently in development. +Besides these, EasyCrypt ships an interface aimed at LLM agents rather +than at humans: `easycrypt llm`, an interactive REPL speaking a +machine-friendly protocol, and `easycrypt mcp`, a +[Model Context Protocol](https://modelcontextprotocol.io/) server over +stdio. Both drive the same proof engine, and both are documented in +[doc/llm/CLAUDE.md](doc/llm/CLAUDE.md). + ### Proof-General (Emacs) EasyCrypt mode has been integrated upstream. Please, go diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md index 0cc20c5a3..b1b2f720b 100644 --- a/doc/llm/CLAUDE.md +++ b/doc/llm/CLAUDE.md @@ -6,59 +6,534 @@ computations, program logics (Hoare logic, probabilistic Hoare logic, probabilistic relational Hoare logic), and ambient mathematical reasoning. -## Using the `llm` command +## Using the `llm` interactive mode -The `llm` subcommand is designed for non-interactive, LLM-friendly -batch compilation. It produces no progress bar and no `.eco` cache -files. +The `llm` subcommand provides an interactive REPL with a +machine-friendly protocol designed for LLM agents. The LLM sends +commands over stdin and receives structured responses on stdout. The +same engine is also served over the Model Context Protocol by the `mcp` +subcommand — see [the MCP section](#using-the-mcp-mode) below. The +two are front-ends over one core, so everything said here about state, +uuids and the proof workflow holds there as well. ``` -easycrypt llm [OPTIONS] FILE.ec +easycrypt llm [OPTIONS] ``` -### Options +Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are +available. Use `-help` to print this guide and exit: -- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not - including) the given location, then print the current goal state to - stdout and exit with code 0. Use this to inspect the proof state at - a specific point in a file. +``` +easycrypt llm -help +``` -- `-lastgoals` — On failure, print the goal state (as it was just - before the failing command) to stdout, then print the error to - stderr, and exit with code 1. Use this to understand what the - failing tactic was supposed to prove. +Use `-eval STR` to feed a newline-separated script instead of reading +stdin. Useful for scripted callers and CI: the REPL runs the given +commands and exits (implicit end-of-input, no `QUIT` required): -Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are -also available. +``` +easycrypt llm -eval 'LOAD "myfile.ec" 42 +GOALS +COMMIT' +``` + +### Protocol + +**Startup.** EasyCrypt prints a `READY` message and waits for input: + +``` +READY [uuid:0] + +``` + +**Responses.** Every response has a typed envelope and an `` +sentinel: + +``` +OK [uuid:N] + + +``` + +``` +ERROR [uuid:N] + + +``` + +The `uuid` is a monotonically increasing integer identifying the proof +engine state. It increments with each successful command that changes +that state. Queries do not change it: `SEARCH`, and the `search`, +`print` and `locate` statements, report the uuid they were called at. + +### Meta-commands + +These are protocol-level commands, not EasyCrypt syntax: + +| Command | Description | +|---------|-------------| +| `LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]` | Reset state, compile file (optionally skip SMT or trace last sentence) | +| `UNDO` | Undo the last proof step | +| `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | +| `GOALS` | Print the current goal (first subgoal only, with remaining count) | +| `GOALS ALL` | Print all subgoals | +| `TREE` | List open subgoals with dotted-path labels showing nesting, marking the focused one | +| `TREE ALL` | Same as `TREE`, but with full goal bodies | +| `FOCUS P` | Rotate focus to the leaf addressed by path `P` (`N` or `N1.N2.N3...`) | +| `NEXT` | Rotate focus to the next subgoal (equivalent to `FOCUS 2`) | +| `COMMIT` | Emit recorded REPL phrases as a bulleted proof body (works under `+strict_bullets`) | +| `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | +| `SEARCH ` | Search for lemmas matching a pattern (read-only: the uuid does not move) | +| `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | +| `` / `` | Delimit multi-line EasyCrypt input | +| `HELP` | Print this guide | +| `QUIT` | Exit | + +### EasyCrypt commands + +Any line that is not a meta-command is parsed as EasyCrypt input. +This covers tactics, declarations, `search`, `print`, `require`, +etc. Every statement on the line must be complete and end with `.` + +``` +smt(). +rewrite H1 H2. +search (%/). +print mulzK. +``` + +A line may hold several statements; all of them are executed, in +order, exactly as if the text had been appended to the source file, +and a single reply describes the state they leave behind: + +``` +split. trivial. trivial. +``` + +If one of them fails, the reply is that failure and the statements +before it stay applied — again as in a file. `exit.` ends the session +there, with the statements that preceded it applied. + +For multi-line statements, wrap with `` and ``: + +``` + +lemma test : + 0 <= n => + 0 < n + 1. + +``` + +### Workflow + +**1. Load a file up to the proof point:** + +``` +LOAD "myfile.ec" 42 +``` + +This compiles the file through line 42 (processing any command whose +end is on or before that line). The response includes where it +stopped: + +``` +OK [uuid:15] [loaded:myfile.ec:42] +Current goal +... + +``` + +For large files, use `-nosmt` to skip SMT calls during prefix +compilation (safe when the prefix was already verified): + +``` +LOAD "myfile.ec" 436 -nosmt +``` + +Add `-trace` to a LOAD to inspect the proof state around the last +loaded sentence. The reply body contains four delimited blocks: + +``` +LOAD "myfile.ec" 42 -trace + +=== BEFORE: line 42 (col 0) === + +=== TACTIC (lines 42:0 - 42:10) === + +=== AFTER: line 42 (col 0) === + +=== SUMMARY === +open goals: N1 -> N2 +``` + +The position comes from the existing `LINE[:COL]` argument; omit it to +trace the file's last sentence. On tactic failure the reply uses the +`ERROR` envelope and still includes the BEFORE/TACTIC blocks plus an +`` marker in the AFTER block. + +A `-trace` LOAD that cannot trace at all (the target sentence is not +inside a proof, or there is no sentence to trace) reports the error but +still leaves the session where the same LOAD without `-trace` would: +you can carry on from there instead of reloading. + +**2. Try tactics, using REVERT to restart:** + +The uuid returned by LOAD is a revertible state. Use `REVERT` to +return to it after failed experiments — this is instant, unlike +re-doing LOAD which recompiles the prefix. + +``` +LOAD "myfile.ec" 42 +→ OK [uuid:15] [loaded:myfile.ec:42] -### Output conventions +smt(). ← fails, state unchanged +rewrite H1. smt(). ← succeeds (uuid:17) +rewrite H2. ← wrong direction +REVERT 17 ← back to after the successful smt() +``` + +To restart the proof from scratch, revert to the LOAD uuid: + +``` +REVERT 15 ← back to the state right after LOAD +``` + +Always note the LOAD uuid so you can return to it. + +**3. Use checkpoints for branching exploration:** + +``` +CHECKPOINT before_split +split. +smt(). ← fails +REVERT before_split +apply H. ← try a different approach +``` + +**4. Inspect and navigate nested subgoals with `TREE` and `FOCUS`:** + +When a tactic opens multiple subgoals, the engine focuses the first +one. By default subsequent tactics act on it; siblings wait their +turn. Use `TREE` to see the structure, including nested splits: + +``` +TREE +→ OK [uuid:N] [focus: 1/4] + [1.1.1] x = 0 <- focused + [1.1.2] y = 1 + [1.2] z = 2 +[2] w = 3 + +``` + +The labels are dotted paths. `FOCUS P` rotates focus to the leaf at +path `P`: + +``` +FOCUS 1.2 ← work on `z = 2` +FOCUS 2 ← work on `w = 3` +FOCUS 1.1.1 ← back to `x = 0` +``` + +`FOCUS k` (a single integer) targets the k-th open goal in the flat +listing. `NEXT` is shorthand for `FOCUS 2`. Selecting an internal +frame errors (`FOCUS: path must select a leaf goal, not a frame`). + +Replies carry a `[focus: k/N]` tag when more than one goal is open +(e.g. `OK [uuid:42] [focus: 1/3]`) so you always know which goal the +next tactic will hit. **TREE labels are not stable across focus +changes** — `FOCUS 1.2` from one state may name a different goal in +another, because the tree always shows the focused goal first. + +**5. Build a `+strict_bullets`-friendly proof with `COMMIT`:** + +The REPL records every successful interactive phrase except queries +(`search`, `print`, `locate`, and the `SEARCH` command), so you can +look things up mid-proof without polluting the body. `COMMIT` walks +the proof DAG and emits the recorded tactics with bullets inserted +at every multi-child split. The output is a proof body that compiles +under `pragma +strict_bullets`: + +``` +LOAD "myfile.ec" 42 +split. +- rewrite H. trivial. ← REPL accepts the unbulleted form +- exact hq. +COMMIT +→ OK [uuid:N] +split. +- rewrite H. trivial. +- exact hq. + +``` + +Bullet characters cycle through `-`, `+`, `*`, `--`, `++`, `**`, ... +and are chosen to avoid colliding with any frames the LOAD prefix +already opened. Use `COMMIT` once the proof is complete (or at any +checkpoint) and paste the result back into the source file. Running +`COMMIT` after `qed.` still emits a bulleted body: the proof structure +is read from a snapshot taken while the proof was open. -- **Goals** are printed to **stdout**. -- **Errors** are printed to **stderr**. -- **Exit code 0** means success (or `-upto` reached its target). -- **Exit code 1** means a command failed. -- If there is no active proof at the point where goals are requested, - stdout will contain: `No active proof.` +`UNDO` / `REVERT` trim the COMMIT transcript automatically. -### Workflow for writing and debugging proofs +**6. Use QUIET mode to save tokens during bulk tactic application:** -1. Try to write a pen-and-paper proof first. +``` +QUIET ON +rewrite H1. +rewrite H2. +rewrite H3. +QUIET OFF +GOALS +``` + +**7. Search for lemmas using patterns:** + +EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as +wildcard: + +``` +search (fdom _). ← lemmas involving fdom +search (_ %/ _). ← integer division lemmas +search (card (_ `|` _)). ← card of union +search (mu _ _) (_ <= _). ← mu lemmas with inequalities +``` -2. Write the `.ec` file with your proof attempt. For a large proof, - write down skeleton and `admit` subgoals first, and then detail - the proof. +The SEARCH meta-command is a shorthand that adds `search`/`.`: -3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file. - - If it succeeds (exit 0), you are done. - - If it fails (exit 1), read the error from stderr and the goal - state from stdout to understand what went wrong. +``` +SEARCH (fdom _) +SEARCH (_ %/ _) +``` -4. Use `-upto LINE` to inspect the proof state at a specific point - without running the rest of the file. This is useful for - incremental proof development. +## Using the MCP mode -5. Fix the proof and repeat from step 2. The ultimate proof should - not contain `admit` or `admitted`. +The `mcp` subcommand serves the same proof engine over the [Model +Context Protocol](https://modelcontextprotocol.io/) instead of the +text protocol above: JSON-RPC 2.0 messages, one per line, over stdio. +Use it from a client that already speaks MCP; use `llm` for the raw +protocol, as a debug console, or for `-eval` scripting. + +``` +easycrypt mcp [OPTIONS] +``` + +The same loader and prover options as `llm` are available (`-I`, +`-timeout`, `-p`, `-stdlib`, etc.). Use `-help` to print this section +and exit: + +``` +easycrypt mcp -help +``` + +Only protocol messages appear on stdout; everything the engine has to +say goes to stderr. The server speaks the `initialize` / +`notifications/initialized` handshake, implements `initialize`, +`ping`, `tools/list` and `tools/call`, and tolerates notifications as +no-ops. It advertises the `tools` capability and nothing else: no +resources, no prompts, no sampling. + +### Tools + +Eleven tools. Required arguments are marked; the others default as +noted. + +| Tool | Arguments | Description | +|------|-----------|-------------| +| `ec_load` | `file` (req), `line`, `col`, `nosmt` (false), `trace` (false) | Reset the session and compile `file` from the top, stopping after the last sentence that ends on or before `line` | +| `ec_step` | `phrase` (req) | Run EasyCrypt sentences — tactics, declarations, `require`, `print`, ... — against the current session | +| `ec_try` | `phrase` (req) | Like `ec_step`, but roll the engine back to its pre-call state whenever a sentence fails | +| `ec_goals` | `all` (false) | Print the focused subgoal, or, with `all`, every open subgoal | +| `ec_tree` | `full` (false) | List the open subgoals as a tree of dotted-path labels, marking the focused one | +| `ec_focus` | `path` (req) | Rotate the focus onto the subgoal at dotted path `path`, or onto the next one with `"next"` | +| `ec_undo` | — | Undo the last engine step | +| `ec_revert` | `target` (req) | Return the session to an earlier state, named by a uuid or by a checkpoint name | +| `ec_checkpoint` | `name` (req) | Record the current uuid under `name`, for a later `ec_revert` | +| `ec_commit` | — | Emit the phrases recorded since the last `ec_load` as a bulleted proof body | +| `ec_search` | `pattern` (req) | Search the environment for lemmas matching an EasyCrypt search pattern | + +`tools/list` carries a fuller, agent-facing `description` and a JSON +Schema for every tool; those are the authoritative texts. The tools +mirror the REPL meta-commands — `-nosmt`, `-trace`, dotted paths, +checkpoints, bullets and search patterns all behave exactly as +described above, and `NEXT` folds into `ec_focus` with path `"next"` — +plus `ec_try`, which has no REPL equivalent. The meta-commands that are +pure console affordances have no tool: multi-line input needs no +``/`` (a `phrase` may simply contain newlines), `QUIET` +has no purpose when the client decides what to display, `HELP` is this +section, and the session ends when the client closes stdin — or when a +phrase is `exit.`, which answers `session terminated` and stops the +process. + +### Running sentences + +`ec_step` takes one or more complete EasyCrypt sentences in a single +`phrase`, exactly as a REPL line does: all of them are executed, in +order, as if the text had been appended to the source file, and one +reply describes the state they leave behind. If one of them fails, the +reply is that failure, the sentences before it stay applied, and the +engine is left wherever the failing sentence left it. + +`ec_try` runs the same input under a rollback contract: whenever a +sentence fails, the engine is returned to the state it had before the +call — including input that failed only after having already advanced +the proof. The failure result sets `structuredContent.reverted` to +`true`, and its `uuid` and text describe that restored state, not the +point of failure. Use `ec_try` to probe a tactic without having to +`ec_revert` afterwards, and `ec_step` when you mean to keep whatever +progress the phrase makes. A successful phrase behaves identically +under both, and is recorded for `ec_commit` in both. + +### State and uuids + +The state model is the REPL's, unchanged. One client is one process is +one engine state: there is no multiplexing, and tool calls run strictly +in arrival order even when a client pipelines them. Every result +reports in its `structuredContent` the `uuid` the call left behind — +the same monotonically increasing state identifier the REPL prints as +`[uuid:N]`, advancing only on calls that change engine state — and +`ec_revert` accepts either one of those uuids or a name given to +`ec_checkpoint`. Note the uuid returned by `ec_load`: reverting to it +is the instant way back to the start of the proof. + +### Errors + +Two kinds of failure, deliberately kept apart: + +* **Protocol faults** — malformed JSON, an unknown method, an unknown + tool, an argument that violates the declared schema — are JSON-RPC + errors (`-32700`, `-32600`, `-32601`, `-32602`). +* **EasyCrypt failures** — a tactic that does not apply, a file that + does not compile, an SMT timeout, a file that is not there — are + *successful* responses carrying `"isError": true` and the prover's + error text. + +The second kind is data: read those messages and act on them, the way +the REPL's `ERROR` replies are meant to be read. + +### Result shape + +Every `tools/call` result, error or not, has the same shape: + +```json +{"content": [{"type": "text", "text": "Current goal\n..."}], + "structuredContent": {"text": "Current goal\n...", "uuid": 3, + "changed": true}, + "isError": false} +``` + +`text` is the body the REPL would print between its envelope and +``, `uuid` is the resulting state, and `changed` says whether the +engine advanced; `ec_try` adds `reverted` on failure, and each tool +declares an `outputSchema` matching that structured half. The text +appears twice on purpose: some clients hand the model +`structuredContent` alone and drop `content` whenever both are present, +so a payload living only in `content` would never reach the agent (the +measurement is in `tests/mcp/README.md`). + +What has no counterpart here are the REPL's status-line annotations: +`[loaded:file:N]` and the `[focus: k/N]` tag do not ride along, so ask +`ec_tree` when you need to know which of several goals the next tactic +will hit. + +### Client configuration + +As a project-scoped `.mcp.json`, dropped next to a proof development: + +```json +{ + "mcpServers": { + "easycrypt": { + "command": "easycrypt", + "args": ["mcp"] + } + } +} +``` + +Add loader options to `args` as needed, e.g. `["mcp", "-I", +"theories"]`. The equivalent one-liner, for Claude Code: + +``` +claude mcp add easycrypt -- easycrypt mcp +``` + +## EasyCrypt proof strategy + +### General approach + +- Start with a pen-and-paper proof plan before writing tactics. +- Use `smt()` aggressively. Try it first — if it fails, add hints: + `smt(lemma1 lemma2)`. +- Build proofs with `have` assertions. Establish intermediate facts + as named hypotheses, then combine with `smt()`. Avoid long rewrite + chains. +- Case split early: `case (n = 0) => [->|hn0].` Base cases often + close by computation. +- Provide specific instances of lemmas to smt: + `have h := lemma arg1 arg2.` SMT works much better with ground + instances than with universally quantified axioms. + +### Integer division (`%/`) + +- `divzK`: `d %| m => m %/ d * d = m` — recovering from exact + division +- `mulzK`: `d <> 0 => m * d %/ d = m` — canceling a known factor +- `divzMpl`: `0 < p => p * m %/ (p * d) = m %/ d` — simplifying + common factors +- To prove `a %/ d = x`, establish `a = x * d` (with `d %| a`), + then use `mulzK`. +- Don't try to rewrite inside `%/` expressions directly. Instead, + prove the equality as a `have` and use it. + +### What works, what doesn't + +- `ring` solves polynomial equalities over integers but treats + abstract ops (like `fact`) as opaque. It **cannot** simplify + `fact(n-1+1)` to `fact(n)`. +- `smt()` can do linear arithmetic and combine hypotheses, but + struggles with nonlinear integer division. Pre-compute key facts + with `have` and `divzK`/`mulzK`, then let smt combine them. +- `rewrite {k}h` rewrites the k-th occurrence only. Essential when a + term appears on both sides of an equation. +- For induction on naturals: `elim/natind: n` gives base (`n ≤ 0`) + and step (`0 ≤ n → P n → P (n+1)`). + +### SMT usage + +`smt()` and `/#` are equivalent — both call external SMT solvers. + +- Use `smt()` **only** on goals that are pure arithmetic or pure + propositional logic. If the goal contains abstract operators, + FMap terms, or `if-then-else`, reduce it first with `rewrite`, + `case`, or `have` before calling `smt()`. +- If `smt()` takes more than 1 second, the goal is too complex. + Simplify with interactive tactics instead of increasing the + timeout. + +### Common pitfalls + +- `rewrite (factS n) //` generates a side goal `0 <= n`. Use + `first smt()` or provide the precondition explicitly. +- `by` closes **all** remaining subgoals. If it fails, the error + refers to the first unclosed goal, which may not be the intended + one. +- When a tactic generates multiple subgoals, the engine focuses the + first one. Address them in any order via `FOCUS path`, or in the + default order by closing each in turn. Use `TREE` or `GOALS ALL` + to see what's open. +- When more than one subgoal is open, every `OK` reply that reflects + proof state -- tactics, `GOALS`, `GOALS ALL`, `TREE`, `TREE ALL`, + `FOCUS`, `NEXT`, `COMMIT`, `LOAD` -- carries a `[focus: k/N]` tag + (e.g. `OK [uuid:42] [focus: 1/3]`) so you know which one the next + tactic will hit. `HELP`, `QUIET` and `CHECKPOINT` are untagged. +- `pragma +strict_bullets` does **not** apply to REPL input. Files + loaded via `LOAD` still respect their own pragmas, but tactics typed + at the REPL prompt are never rejected for missing bullets — the + REPL is the focus mechanism. +- `rewrite lemma in H` modifies hypothesis `H` in place (it does + not consume it). If you need to preserve the original, copy it + first: `have H' := H; rewrite lemma in H'`. ## EasyCrypt language overview @@ -91,8 +566,6 @@ proof. by ring. qed. ### Common tactics - - - `trivial` — solve trivial goals - `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints - `auto` — automatic reasoning @@ -141,9 +614,10 @@ proof. by ring. qed. ### Guidelines -* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals). +* Use SMT solver only in direct mode (smt() or /#) on simple goals + (arithmetic goals, pure logical goals). * Refrain from unfolding operator definitions unless necessary. - If you need more properties on an operator, state this property in a dedicated lemma, - but avoid unfolding definitions in higher level proofs. - + If you need more properties on an operator, state this property + in a dedicated lemma, but avoid unfolding definitions in higher + level proofs. diff --git a/scripts/testing/llm-golden b/scripts/testing/llm-golden new file mode 100755 index 000000000..98361f38a --- /dev/null +++ b/scripts/testing/llm-golden @@ -0,0 +1,132 @@ +#! /bin/sh + +# -------------------------------------------------------------------- +# Golden-output regression harness for the `easycrypt llm` REPL. +# +# llm-golden [--bin PATH] [--record] [NAME...] +# +# Each tests/llm/scripts/NAME.script holds the newline-separated +# commands fed to `ec.exe llm -eval`. Lines starting with `#` are +# stripped before the script is passed to -eval; the first such line +# must be `# exit: N`, the expected process exit status. Stdout is +# compared against tests/llm/expected/NAME.out. +# +# Scripts run with tests/llm as the working directory, so fixture paths +# stay relative and the [loaded:...] reply tags remain machine +# independent. +# -------------------------------------------------------------------- + +set -u + +root=$(CDPATH= cd -- "$(dirname -- "$0")/../.." && pwd) +bin="$root/_build/default/src/ec.exe" +record=0 +names="" + +while [ $# -gt 0 ]; do + case "$1" in + --bin) + [ $# -ge 2 ] || { echo "llm-golden: --bin needs an argument" >&2; exit 2; } + bin=$2; shift 2 ;; + --bin=*) + bin=${1#--bin=}; shift ;; + --record) + record=1; shift ;; + -h|--help) + echo "usage: llm-golden [--bin PATH] [--record] [NAME...]"; exit 0 ;; + -*) + echo "llm-golden: unknown option: $1" >&2; exit 2 ;; + *) + names="$names $1"; shift ;; + esac +done + +case "$bin" in + /*) ;; + *) bin=$(CDPATH= cd -- "$(dirname -- "$bin")" && pwd)/$(basename -- "$bin") ;; +esac + +if [ ! -x "$bin" ]; then + echo "llm-golden: no such executable: $bin" >&2 + exit 2 +fi + +tests="$root/tests/llm" +scripts="$tests/scripts" +expected="$tests/expected" + +if [ -z "$names" ]; then + names=$(cd "$scripts" && ls *.script 2>/dev/null | sed 's/\.script$//') +fi + +mkdir -p "$expected" + +tmp=$(mktemp -d "${TMPDIR:-/tmp}/llm-golden.XXXXXX") || exit 2 +trap 'rm -rf "$tmp"' EXIT INT TERM + +nfail=0 +npass=0 + +for name in $names; do + script="$scripts/$name.script" + gold="$expected/$name.out" + + if [ ! -f "$script" ]; then + echo "FAIL $name (no such script: $script)" + nfail=$((nfail + 1)) + continue + fi + + want_exit=$(sed -n 's/^# *exit: *\([0-9][0-9]*\).*$/\1/p' "$script" | head -n 1) + if [ -z "$want_exit" ]; then + echo "FAIL $name (script has no '# exit: N' line)" + nfail=$((nfail + 1)) + continue + fi + + grep -v '^#' "$script" > "$tmp/eval.in" + + (cd "$tests" && "$bin" llm -eval "$(cat "$tmp/eval.in")") \ + > "$tmp/out" 2> "$tmp/err" + got_exit=$? + + if [ "$record" = 1 ]; then + cp "$tmp/out" "$gold" + if [ "$got_exit" != "$want_exit" ]; then + echo "RECORD $name (exit $got_exit, script declares $want_exit)" + nfail=$((nfail + 1)) + else + echo "RECORD $name" + npass=$((npass + 1)) + fi + continue + fi + + ok=1 + + if [ ! -f "$gold" ]; then + echo "FAIL $name (no golden: $gold; re-run with --record)" + ok=0 + elif ! diff -u "$gold" "$tmp/out" > "$tmp/diff"; then + echo "FAIL $name (stdout differs)" + sed 's/^/ /' "$tmp/diff" + ok=0 + fi + + if [ "$got_exit" != "$want_exit" ]; then + echo "FAIL $name (exit $got_exit, expected $want_exit)" + ok=0 + fi + + if [ "$ok" = 1 ]; then + echo "PASS $name" + npass=$((npass + 1)) + else + nfail=$((nfail + 1)) + fi +done + +echo "----" +echo "$npass passed, $nfail failed" + +[ "$nfail" = 0 ] diff --git a/scripts/testing/mcp-golden b/scripts/testing/mcp-golden new file mode 100755 index 000000000..56ee903e8 --- /dev/null +++ b/scripts/testing/mcp-golden @@ -0,0 +1,140 @@ +#! /bin/sh + +# -------------------------------------------------------------------- +# Golden-output regression harness for the `easycrypt mcp' server. +# +# mcp-golden [--bin PATH] [--record] [NAME...] +# +# Each tests/mcp/scripts/NAME.script holds the newline-delimited +# JSON-RPC messages fed to `ec.exe mcp' on stdin. Lines starting with +# `#' are stripped before the script is handed to the server; the first +# such line must be `# exit: N', the expected process exit status. +# Stdout -- the protocol stream, one JSON message per line -- is +# compared against tests/mcp/expected/NAME.out. +# +# Scripts run with tests/mcp as the working directory, so fixture paths +# stay relative and no golden bakes in a developer's home directory. +# The fixtures are the ones the REPL harness uses, under +# ../llm/fixtures. +# +# One field of the stream is not reproducible: serverInfo.version is a +# git-describe string. It is rewritten to "VERSION" before diffing. +# -------------------------------------------------------------------- + +set -u + +root=$(CDPATH= cd -- "$(dirname -- "$0")/../.." && pwd) +bin="$root/_build/default/src/ec.exe" +record=0 +names="" + +while [ $# -gt 0 ]; do + case "$1" in + --bin) + [ $# -ge 2 ] || { echo "mcp-golden: --bin needs an argument" >&2; exit 2; } + bin=$2; shift 2 ;; + --bin=*) + bin=${1#--bin=}; shift ;; + --record) + record=1; shift ;; + -h|--help) + echo "usage: mcp-golden [--bin PATH] [--record] [NAME...]"; exit 0 ;; + -*) + echo "mcp-golden: unknown option: $1" >&2; exit 2 ;; + *) + names="$names $1"; shift ;; + esac +done + +case "$bin" in + /*) ;; + *) bin=$(CDPATH= cd -- "$(dirname -- "$bin")" && pwd)/$(basename -- "$bin") ;; +esac + +if [ ! -x "$bin" ]; then + echo "mcp-golden: no such executable: $bin" >&2 + exit 2 +fi + +tests="$root/tests/mcp" +scripts="$tests/scripts" +expected="$tests/expected" + +if [ -z "$names" ]; then + names=$(cd "$scripts" && ls *.script 2>/dev/null | sed 's/\.script$//') +fi + +mkdir -p "$expected" + +tmp=$(mktemp -d "${TMPDIR:-/tmp}/mcp-golden.XXXXXX") || exit 2 +trap 'rm -rf "$tmp"' EXIT INT TERM + +nfail=0 +npass=0 + +for name in $names; do + script="$scripts/$name.script" + gold="$expected/$name.out" + + if [ ! -f "$script" ]; then + echo "FAIL $name (no such script: $script)" + nfail=$((nfail + 1)) + continue + fi + + want_exit=$(sed -n 's/^# *exit: *\([0-9][0-9]*\).*$/\1/p' "$script" | head -n 1) + if [ -z "$want_exit" ]; then + echo "FAIL $name (script has no '# exit: N' line)" + nfail=$((nfail + 1)) + continue + fi + + grep -v '^#' "$script" > "$tmp/rpc.in" + + (cd "$tests" && "$bin" mcp < "$tmp/rpc.in") \ + > "$tmp/raw" 2> "$tmp/err" + got_exit=$? + + sed 's/\("serverInfo":{"name":"easycrypt","version":\)"[^"]*"/\1"VERSION"/' \ + "$tmp/raw" > "$tmp/out" + + if [ "$record" = 1 ]; then + cp "$tmp/out" "$gold" + if [ "$got_exit" != "$want_exit" ]; then + echo "RECORD $name (exit $got_exit, script declares $want_exit)" + nfail=$((nfail + 1)) + else + echo "RECORD $name" + npass=$((npass + 1)) + fi + continue + fi + + ok=1 + + if [ ! -f "$gold" ]; then + echo "FAIL $name (no golden: $gold; re-run with --record)" + ok=0 + elif ! diff -u "$gold" "$tmp/out" > "$tmp/diff"; then + echo "FAIL $name (stdout differs)" + sed 's/^/ /' "$tmp/diff" + ok=0 + fi + + if [ "$got_exit" != "$want_exit" ]; then + echo "FAIL $name (exit $got_exit, expected $want_exit)" + ok=0 + fi + + if [ "$ok" = 1 ]; then + echo "PASS $name" + npass=$((npass + 1)) + else + nfail=$((nfail + 1)) + fi +done + +echo "----" +echo "$npass passed, $nfail failed" + +[ "$nfail" = 0 ] diff --git a/scripts/testing/mcp-inspector-check b/scripts/testing/mcp-inspector-check new file mode 100755 index 000000000..9b869110a --- /dev/null +++ b/scripts/testing/mcp-inspector-check @@ -0,0 +1,72 @@ +#! /bin/sh + +# -------------------------------------------------------------------- +# Manual smoke test against a real MCP client. +# +# mcp-inspector-check [--bin PATH] +# +# Drives `easycrypt mcp' with the reference client, the MCP Inspector's +# CLI mode, rather than with our own golden harness: the goldens only +# prove the server is consistent with itself, this proves a client that +# knows nothing about EasyCrypt can complete the handshake, read the +# tool declarations and call a tool. +# +# NOT wired into CI, and deliberately so: it downloads +# @modelcontextprotocol/inspector through npx, so it needs node and +# network access, and it tracks a version we do not pin. Run it by hand +# after touching the protocol layer (src/ecMcp.ml). +# +# Two checks, both of which must print their result and exit 0: +# +# 1. tools/list -- the handshake and the tool table; +# 2. tools/call -- ec_load on a test fixture, whose result must +# carry the goal `1 = 1 /\ 2 = 2' and uuid 3. +# -------------------------------------------------------------------- + +set -eu + +root=$(CDPATH= cd -- "$(dirname -- "$0")/../.." && pwd) +bin="$root/_build/default/src/ec.exe" + +while [ $# -gt 0 ]; do + case "$1" in + --bin) + [ $# -ge 2 ] || { echo "mcp-inspector-check: --bin needs an argument" >&2; exit 2; } + bin=$2; shift 2 ;; + --bin=*) + bin=${1#--bin=}; shift ;; + -h|--help) + echo "usage: mcp-inspector-check [--bin PATH]"; exit 0 ;; + *) + echo "mcp-inspector-check: unknown option: $1" >&2; exit 2 ;; + esac +done + +case "$bin" in + /*) ;; + *) bin=$(CDPATH= cd -- "$(dirname -- "$bin")" && pwd)/$(basename -- "$bin") ;; +esac + +if [ ! -x "$bin" ]; then + echo "mcp-inspector-check: no such executable: $bin" >&2 + exit 2 +fi + +if ! command -v npx > /dev/null 2>&1; then + echo "mcp-inspector-check: npx not found; install node, or skip" >&2 + exit 2 +fi + +inspector="npx --yes @modelcontextprotocol/inspector --cli" +fixture="$root/tests/llm/fixtures/simple.ec" + +echo "== tools/list ==============================================" +$inspector "$bin" mcp --method tools/list + +echo +echo "== tools/call ec_load ======================================" +$inspector "$bin" mcp \ + --method tools/call \ + --tool-name ec_load \ + --tool-arg "file=$fixture" \ + --tool-arg line=6 diff --git a/scripts/testing/mcp-parity b/scripts/testing/mcp-parity new file mode 100755 index 000000000..3901f637b --- /dev/null +++ b/scripts/testing/mcp-parity @@ -0,0 +1,189 @@ +#! /usr/bin/env python3 + +# -------------------------------------------------------------------- +# Parity check: `easycrypt llm' and `easycrypt mcp' are two front-ends +# over one core, so the same operation must produce the same answer on +# both wires. +# +# mcp-parity [--bin PATH] [-v] +# +# One representative operation per tool family is played, in order, +# against two sessions -- a REPL one driven with `llm -eval', an MCP +# one driven with a JSON-RPC script -- started from the same working +# directory on the same fixture. For each step the checker asserts: +# +# * the engine uuid matches: the REPL's `[uuid:N]' envelope tag +# against the MCP result's structuredContent.uuid; +# * the payload matches: the REPL's reply body (what it prints +# between the OK/ERROR line and `') against the MCP result's +# content[0].text. +# +# The payload comparison is up to one trailing newline, which the REPL +# appends to a body that lacks one so that `' starts a line of its +# own. That is the only licensed difference; see tests/mcp/README.md +# for the two structural asymmetries this check deliberately does not +# span (envelope tags, and notices on failures). +# -------------------------------------------------------------------- + +import json +import os +import subprocess +import sys + +# -------------------------------------------------------------------- +# The operations, as (label, REPL line, MCP tool name, MCP arguments). +# One per tool family, plus a failing phrase, played in this order +# against both sessions. + +STEPS = [ + ("load", 'LOAD "fixtures/simple.ec" 6', + "ec_load", {"file": "fixtures/simple.ec", "line": 6}), + ("step", 'split.', + "ec_step", {"phrase": "split."}), + ("goals", 'GOALS ALL', + "ec_goals", {"all": True}), + ("tree", 'TREE', + "ec_tree", {}), + ("focus", 'FOCUS 2', + "ec_focus", {"path": "2"}), + ("undo", 'UNDO', + "ec_undo", {}), + ("checkpoint", 'CHECKPOINT c0', + "ec_checkpoint", {"name": "c0"}), + ("step/2", 'trivial.', + "ec_step", {"phrase": "trivial."}), + ("revert", 'REVERT c0', + "ec_revert", {"target": "c0"}), + ("search", 'SEARCH (b2i _)', + "ec_search", {"pattern": "(b2i _)"}), + ("commit", 'COMMIT', + "ec_commit", {}), + ("failure", 'apply nosuchlemma.', + "ec_step", {"phrase": "apply nosuchlemma."}), +] + + +# -------------------------------------------------------------------- +def repl_replies(binary, cwd): + """Run the REPL script and return one (uuid, body) per reply. + + The REPL wire is a sequence of blocks, each opened by an + `OK [uuid:N]' or `ERROR [uuid:N]' line and closed by a lone + `'. The opening READY block is dropped.""" + + script = "\n".join(line for (_, line, _, _) in STEPS) + out = subprocess.run( + [binary, "llm", "-eval", script], + cwd=cwd, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL, + ).stdout.decode() + + replies, head, body = [], None, [] + for line in out.split("\n")[:-1]: + if head is None: + head = line + elif line == "": + replies.append((head, "".join(l + "\n" for l in body))) + head, body = None, [] + else: + body.append(line) + + def uuid_of(head): + return int(head.split("[uuid:")[1].split("]")[0]) + + return [(uuid_of(h), b) for (h, b) in replies][1:] + + +# -------------------------------------------------------------------- +def mcp_results(binary, cwd): + """Run the MCP script and return one (uuid, text) per tools/call.""" + + script = "".join( + json.dumps({ + "jsonrpc": "2.0", "id": i + 1, "method": "tools/call", + "params": {"name": tool, "arguments": args}, + }) + "\n" + for (i, (_, _, tool, args)) in enumerate(STEPS) + ) + out = subprocess.run( + [binary, "mcp"], input=script.encode(), + cwd=cwd, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL, + ).stdout.decode() + + results = [] + for line in out.splitlines(): + result = json.loads(line)["result"] + results.append((result["structuredContent"]["uuid"], + result["content"][0]["text"])) + return results + + +# -------------------------------------------------------------------- +def main(): + root = os.path.dirname(os.path.dirname(os.path.dirname( + os.path.abspath(__file__)))) + binary = os.path.join(root, "_build", "default", "src", "ec.exe") + verbose = False + + args = sys.argv[1:] + while args: + if args[0] == "--bin": + binary, args = args[1], args[2:] + elif args[0].startswith("--bin="): + binary, args = args[0][len("--bin="):], args[1:] + elif args[0] in ("-v", "--verbose"): + verbose, args = True, args[1:] + elif args[0] in ("-h", "--help"): + print("usage: mcp-parity [--bin PATH] [-v]") + return 0 + else: + print(f"mcp-parity: unknown option: {args[0]}", file=sys.stderr) + return 2 + + binary = os.path.abspath(binary) + if not os.access(binary, os.X_OK): + print(f"mcp-parity: no such executable: {binary}", file=sys.stderr) + return 2 + + # Both sessions run from tests/llm, so they name the fixture the + # same way and no path difference can leak into a reply. + cwd = os.path.join(root, "tests", "llm") + + repl = repl_replies(binary, cwd) + mcp = mcp_results(binary, cwd) + + nfail = 0 + + if len(repl) != len(STEPS) or len(mcp) != len(STEPS): + print(f"FAIL (reply count: {len(STEPS)} steps, " + f"{len(repl)} REPL replies, {len(mcp)} MCP results)") + return 1 + + for ((label, line, tool, _), (ruuid, body), (muuid, text)) in \ + zip(STEPS, repl, mcp): + # The REPL ends a non-empty body with a newline so that `' + # starts a line; MCP has no sentinel and so does not. + normalized = text if text.endswith("\n") or text == "" else text + "\n" + + problems = [] + if ruuid != muuid: + problems.append(f"uuid: REPL {ruuid}, MCP {muuid}") + if normalized != body: + problems.append(f"body:\n REPL {body!r}\n MCP {normalized!r}") + + if problems: + print(f"FAIL {label} ({line!r} vs {tool})") + for problem in problems: + print(" " + problem) + nfail += 1 + else: + print(f"PASS {label} (uuid {ruuid})") + if verbose: + print("".join(" | " + l + "\n" for l in body.splitlines())) + + print("----") + print(f"{len(STEPS) - nfail} passed, {nfail} failed") + return 1 if nfail else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/ec.ml b/src/ec.ml index f3bc3467b..f798081e9 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -158,7 +158,7 @@ let main () = let (module Sites) = EcRelocate.sites in (* Parse command line arguments *) - let conffiles, options = + let conffiles, projini, options = let sysfile = let xdgini = XDG.Config.file @@ -220,6 +220,19 @@ let main () = exit 1 in + (* The [easycrypt.project] context of a file (walking up from the + file's directory; from the cwd when no file is given). Also used + by the LLM REPL to reconfigure per loaded file. *) + let projini (path : string option) = + Option.bind (projfile path) (fun conffile -> + Option.map + (fun ini -> { + inic_ini = ini; + inic_root = Some (Filename.dirname conffile); + }) + (read_ini_file conffile) + ) in + let getini (path : string option) = let inisys = List.filter_map @@ -230,20 +243,9 @@ let main () = conffiles in - let iniproj = - Option.bind (projfile path) (fun conffile -> - Option.map - (fun ini -> { - inic_ini = ini; - inic_root = Some (Filename.dirname conffile); - }) - (read_ini_file conffile) - ) - in - - List.ocons iniproj inisys in + List.ocons (projini path) inisys in - (conffiles, EcOptions.parse_cmdline ~ini:getini Sys.argv) in + (conffiles, projini, EcOptions.parse_cmdline ~ini:getini Sys.argv) in (* Execution of eager commands *) begin @@ -328,6 +330,11 @@ let main () = ["-boot"] else [] in + let stdlib = + options.o_options.o_loader.ldro_stdlib + |> List.map (fun d -> ["-stdlib"; d]) + |> List.flatten in + let idirs = options.o_options.o_loader.ldro_idirs |> List.map (fun (pfx, name, rec_) -> @@ -341,7 +348,7 @@ let main () = maxjobs; timeout; cpufactor; ppwidth; provers; quorum ; pragmas ; checkall; profile; why3srv ; why3 ; - reloc ; noevict; boot ; idirs ; + reloc ; noevict; boot ; stdlib ; idirs ; ] in @@ -420,11 +427,20 @@ let main () = let ldropts = options.o_options.o_loader in begin + (* [-stdlib DIR] (repeatable) fully replaces the built-in + [Sites.theories] roots. This is stronger than [-boot], which + only skips the recursive-System add but still injects + [/prelude]. *) + let theories = + match ldropts.ldro_stdlib with + | [] -> Sites.theories + | ds -> ds + in List.iter (fun theory -> EcCommands.addidir ~namespace:`System (Filename.concat theory "prelude"); if not ldropts.ldro_boot then EcCommands.addidir ~namespace:`System ~recursive:true theory - ) Sites.theories; + ) theories; List.iter (fun (onm, name, isrec) -> EcCommands.addidir ?namespace:(omap (fun nm -> `Named nm) onm) @@ -569,34 +585,11 @@ let main () = end - | `Llm llmopts -> begin - let name = llmopts.llmo_input in - - begin try - let ext = Filename.extension name in - ignore (EcLoader.getkind ext : EcLoader.kind) - with EcLoader.BadExtension ext -> - Format.eprintf "do not know what to do with %s@." ext; - exit 1 - end; + | `Llm llmopts -> + EcLlm.run ~relocdir ~boot:ldropts.ldro_boot ~projini llmopts - let lastgoals = llmopts.llmo_lastgoals in - let terminal = - lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name)) - in - - { prvopts = llmopts.llmo_provers - ; input = Some name - ; terminal = terminal - ; interactive = false - ; eco = true - ; gccompact = None - ; docgen = false - ; outdirp = None - ; upto = llmopts.llmo_upto - ; trace = None } - - end + | `Mcp mcpopts -> + EcMcp.run ~relocdir ~boot:ldropts.ldro_boot ~projini mcpopts | `Runtest _ -> (* Eagerly executed *) diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 3e08fb640..1c6a8bb7e 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -996,6 +996,69 @@ let push_context scope context = ct_stack = context.ct_stack |> omap (fun st -> context.ct_current :: st); } +(* -------------------------------------------------------------------- *) +(* Rotate the focus of the currently active proof so that the goal at + 1-based index [k] becomes the focused one. The change is persisted + in the context with a new uuid so UNDO/REVERT can roll it back. + Returns the new number of open goals on success, or an error + message on failure. *) +let focus_goal (k : int) : (int, string) result = + match !context with + | None -> Error "no active context" + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> Error "no active proof" + | Some puc -> + match puc.EcScope.puc_active with + | None -> Error "no active proof" + | Some (pac, pct) -> + match pac.EcScope.puc_jdg with + | EcScope.PSNoCheck -> Error "proof is in no-check mode" + | EcScope.PSCheck pf -> + let n = List.length (EcCoreGoal.all_hd_opened pf) in + if n = 0 then Error "no open goals" + else if k < 1 || k > n then + Error (Printf.sprintf + "focus: index %d out of range (1..%d)" k n) + else if k = 1 then Ok n + else begin + let pf = EcCoreGoal.rotate_focus k pf in + let pac = { pac with EcScope.puc_jdg = EcScope.PSCheck pf } in + let puc = + { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some (push_context scope ctxt); + Ok n + end + +(* Disable bullet enforcement for REPL-driven phrases. Drops the global + pragma so newly-opened proofs have no bullet stack, and clears the + stack on any currently active proof so REPL phrases are not checked + against it. Idempotent. Does not advance the undo level. Returns + the stack that was in place (if any) at the moment the active + proof's bullets were first cleared; returns [None] on idempotent + calls (where the stack is already gone). Callers use the returned + stack to drive bullet-character selection in [COMMIT]. *) +let disable_repl_bullets () : EcBullets.stack option = + pragma_strict_bullets false; + match !context with + | None -> None + | Some ctxt -> + match EcScope.xgoal ctxt.ct_current with + | None -> None + | Some puc -> + match puc.EcScope.puc_active with + | None -> None + | Some (pac, pct) -> + match pac.EcScope.puc_bullets with + | None -> None + | Some _ as prior -> + let pac = { pac with EcScope.puc_bullets = None } in + let puc = { puc with EcScope.puc_active = Some (pac, pct) } in + let scope = EcScope.set_xgoal ctxt.ct_current puc in + context := Some { ctxt with ct_current = scope }; + prior + (* -------------------------------------------------------------------- *) let initialize ~restart ~undo ~boot ~checkmode ~checkproof = assert (restart || EcUtils.is_none !context); @@ -1136,8 +1199,50 @@ let pp_current_goal ?(all = false) stream = end (* -------------------------------------------------------------------- *) +let in_proof () = + Option.is_some (S.xgoal (current ())) + +(* Return the list of open-goal handles at the top level of the active + proof, focused-first, or [] if no proof is active. *) +let open_handles () : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.all_hd_opened pf + | _ -> [] + +(* The proof environment of the active proof, or [None] if no proof is + active. A [proofenv] is immutable and cumulative, so a snapshot taken + while the proof was open keeps answering DAG queries after [qed] has + discarded the active proof. *) +let current_proofenv () : EcCoreGoal.proofenv option = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + Some (EcCoreGoal.proofenv_of_proof pf) + | _ -> None + +(* Direct DAG children of [h] in the active proof. [] if no proof. *) +let children_of (h : EcCoreGoal.handle) : EcCoreGoal.handle list = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.children_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> [] + +(* Parent of [h] in the active proof's DAG, or [None] if [h] is the + root or no proof is active. *) +let parent_of (h : EcCoreGoal.handle) : EcCoreGoal.handle option = + match S.xgoal (current ()) with + | Some { S.puc_active = + Some ({ S.puc_jdg = S.PSCheck pf }, _) } -> + EcCoreGoal.parent_of_handle + (EcCoreGoal.proofenv_of_proof pf) h + | _ -> None + let pp_current_goal_or_noproof ?(all = false) stream = - if Option.is_some (S.xgoal (current ())) then + if in_proof () then pp_current_goal ~all stream else Format.fprintf stream "No active proof.@\n%!" @@ -1175,3 +1280,34 @@ let pp_all_goals () = end | _ -> [] + +(* -------------------------------------------------------------------- *) +(* Render the open-subgoals tree. Each entry is (index, is_focused, + text). [index] is 1-based, [is_focused] marks the focused goal + (always at index 1 with EC's current focus model), and [text] is + either a one-line conclusion digest (when [~all = false]) or the + full goal body (when [~all = true]). *) +let pp_tree ?(all = false) () : (int * bool * string) list = + let scope = current () in + match S.xgoal scope with + | Some { S.puc_active = Some ({ puc_jdg = S.PSCheck pf }, _) } -> begin + match EcCoreGoal.opened pf with + | None -> [] + | Some _ -> + let ppe = EcPrinting.PPEnv.ofenv (S.env scope) in + let goals = EcCoreGoal.all_opened pf in + List.mapi (fun i { EcCoreGoal.g_hyps; EcCoreGoal.g_concl } -> + let text = + if all then + let buf = Buffer.create 256 in + let hc = (EcEnv.LDecl.tohyps g_hyps, g_concl) in + Format.fprintf + (Format.formatter_of_buffer buf) + "%a@?" (EcPrinting.pp_goal1 ppe) hc; + Buffer.contents buf + else + Format.asprintf "%a" (EcPrinting.pp_form ppe) g_concl + in + (i + 1, i = 0, text)) goals + end + | _ -> [] diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 8a1220ae0..b44d30a75 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -64,6 +64,14 @@ val pp_current_goal : ?all:bool -> Format.formatter -> unit val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list +val in_proof : unit -> bool +val disable_repl_bullets : unit -> EcBullets.stack option +val pp_tree : ?all:bool -> unit -> (int * bool * string) list +val focus_goal : int -> (int, string) result +val open_handles : unit -> EcCoreGoal.handle list +val current_proofenv : unit -> EcCoreGoal.proofenv option +val children_of : EcCoreGoal.handle -> EcCoreGoal.handle list +val parent_of : EcCoreGoal.handle -> EcCoreGoal.handle option (* -------------------------------------------------------------------- *) val pragma_verbose : bool -> unit diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 728824b4d..fc79359c9 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -132,9 +132,13 @@ type proof = { } and proofenv = { - pr_uid : ID.id; (* unique ID for this proof *) - pr_main : ID.id; (* top goal, contains the final result *) - pr_goals : goal ID.Map.t; (* set of all goals, closed and opened *) + pr_uid : ID.id; (* unique ID for this proof *) + pr_main : ID.id; (* top goal, contains the final result *) + pr_goals : goal ID.Map.t; (* set of all goals, closed and opened *) + pr_parent : handle ID.Map.t; + (* For each non-root handle, the parent in the proof DAG: i.e. + the handle that was being worked on when this one was created + via [FApi.newgoal]. The root [pr_main] is absent. *) } and pregoal = { @@ -463,17 +467,24 @@ module FApi = struct tcenv (* ------------------------------------------------------------------ *) - let pf_newgoal (pe : proofenv) ?vx hyps concl = + let pf_newgoal (pe : proofenv) ?parent ?vx hyps concl = let hid = ID.gen () in let pregoal = { g_uid = hid; g_hyps = hyps; g_concl = concl; g_simpl = EcEnv.SimplifyContext.empty; } in let goal = { g_goal = pregoal; g_validation = vx; } in - let pe = { pe with pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals; } in + let pr_goals = ID.Map.add pregoal.g_uid goal pe.pr_goals in + let pr_parent = + match parent with + | None -> pe.pr_parent + | Some p -> ID.Map.add pregoal.g_uid p pe.pr_parent + in + let pe = { pe with pr_goals; pr_parent } in (pe, pregoal) (* ------------------------------------------------------------------ *) let newgoal (tc : tcenv) ?(hyps : LDecl.hyps option) (concl : form) = let hyps = ofdfl (fun () -> tc_hyps tc) hyps in - let (pe, pg) = pf_newgoal (tc_penv tc) hyps concl in + let parent = tc.tce_tcenv.tce_goal |> Option.map (fun g -> g.g_uid) in + let (pe, pg) = pf_newgoal (tc_penv tc) ?parent hyps concl in let pg = { pg with g_simpl = tc1_simplify_context tc.tce_tcenv } in let pe = update_goal_map (fun g -> { g with g_goal = pg }) pg.g_uid pe in @@ -1006,9 +1017,10 @@ let start (hyps : LDecl.hyps) (goal : form) = let goal = { g_uid = hid; g_hyps = hyps; g_concl = goal; g_simpl = EcEnv.SimplifyContext.empty; } in let goal = { g_goal = goal; g_validation = None; } in - let env = { pr_uid = uid; - pr_main = hid; - pr_goals = ID.Map.singleton hid goal; } in + let env = { pr_uid = uid; + pr_main = hid; + pr_goals = ID.Map.singleton hid goal; + pr_parent = ID.Map.empty; } in { pr_env = env; pr_opened = [hid]; } @@ -1030,6 +1042,33 @@ let all_opened (pf : proof) = (* -------------------------------------------------------------------- *) let closed (pf : proof) = List.is_empty pf.pr_opened +(* -------------------------------------------------------------------- *) +(* Direct children of [h] in the proof DAG, in creation order. This is + driven by [pr_parent], the explicit parent edge recorded by + [FApi.newgoal] at the moment each child handle is allocated. The + iteration order matches creation order because handles are + generated by a monotonic counter and [ID.Map] iterates by key. *) +let children_of_handle (pe : proofenv) (h : handle) : handle list = + ID.Map.fold + (fun child parent acc -> + if eq_handle parent h then child :: acc else acc) + pe.pr_parent [] + |> List.rev + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +let parent_of_handle (pe : proofenv) (h : handle) : handle option = + ID.Map.find_opt h pe.pr_parent + +(* -------------------------------------------------------------------- *) +let rotate_focus (k : int) (pf : proof) = + let n = List.length pf.pr_opened in + if k < 1 || k > n then + invalid_arg "EcCoreGoal.rotate_focus"; + if k = 1 then pf + else + let pre, post = List.split_at (k - 1) pf.pr_opened in + { pf with pr_opened = post @ pre } + (* -------------------------------------------------------------------- *) module Exn = struct let recast pe _hyps f x = diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index 2f1b51740..19d0feb09 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -207,6 +207,18 @@ val all_opened : proof -> pregoal list (* Check if a proof is done *) val closed : proof -> bool +(* Direct children of [h] in the proof DAG, in creation order. *) +val children_of_handle : proofenv -> handle -> handle list + +(* Parent of [h] in the proof DAG, or [None] if [h] is the root. *) +val parent_of_handle : proofenv -> handle -> handle option + +(* Rotate the list of opened goals at the top level. [rotate_focus k pf] + makes the goal currently at 1-based index [k] the new focused goal, + preserving the cyclic order of the others. Raises [Invalid_argument] + if [k] is out of range. *) +val rotate_focus : int -> proof -> proof + (* -------------------------------------------------------------------- *) val tc_error : proofenv -> ?catchable:bool -> ?loc:EcLocation.t -> ?who:string diff --git a/src/ecLlm.ml b/src/ecLlm.ml new file mode 100644 index 000000000..8a2c1ead6 --- /dev/null +++ b/src/ecLlm.ml @@ -0,0 +1,391 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL. See [ecLlm.mli] for the entry point. + + This is the text front-end only: line parsing, the OK/ERROR/ + envelope, the multi-line block buffer, QUIET, HELP and the -eval + driver. Everything engine-facing lives in [EcLlmCore], which the + MCP front-end shares. *) + +open EcUtils + +(* -------------------------------------------------------------------- *) +(* Path to the bundled LLM-agent guide. *) +let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + +(* Print the bundled guide to stdout. Used by [-help]. *) +let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + +(* -------------------------------------------------------------------- *) +(* Surface command vocabulary. Parsing turns each stdin line into one + of these, and dispatch is a flat pattern-match. Argument + parsing/validation lives here; commands that interact with mutable + session state (checkpoints table) carry only the raw user-supplied + data and let [EcLlmCore] do the lookup. *) +module Parse = struct + type command = + | Quit + | Help + | Undo + | Goals of [`One | `All] + | Tree of [`One | `All] + | Commit + | Focus of int list (* dotted path; [k] = "FOCUS k" *) + | Next + | Checkpoint of string + | Revert of string (* uuid-or-name; the core resolves *) + | Quiet of bool + | Search of string (* trailing "." already stripped *) + | Load of load (* parsed LOAD arguments *) + | Ec of string (* fall-through: raw EasyCrypt input *) + | Begin_multi + | Done_multi + | Multi_line of string + | Blank + + and load = { + ld_file : string; + ld_upto : (int * int option) option; + ld_nosmt : bool; + ld_trace : bool; + } + + exception Parse_error of string + + (* Match [kw] as a prefix: succeeds on exactly [kw] (no argument) + or [kw ^ " " ^ ...] (with argument), returning the stripped + argument tail. Returns [None] otherwise. This recognises both + "CHECKPOINT" and "CHECKPOINT foo" the same way, so we can + diagnose the missing-name case ourselves instead of falling + through to EC's parser. *) + let keyword_arg kw line = + if line = kw then Some "" + else if String.starts_with line (kw ^ " ") then + let n = String.length kw + 1 in + Some (String.strip + (String.sub line n (String.length line - n))) + else None + + let parse_focus arg = + if arg = "" then + raise (Parse_error "FOCUS: missing argument"); + let parts = String.split_on_char '.' arg in + let path = + try List.map int_of_string parts + with Failure _ -> + raise (Parse_error + (Printf.sprintf "FOCUS: not a path of integers: %s" arg)) + in + if List.exists (fun k -> k < 1) path then + raise (Parse_error + (Printf.sprintf "FOCUS: path indices must be >= 1: %s" arg)); + Focus path + + let parse_checkpoint name = + if name = "" then + raise (Parse_error "CHECKPOINT: missing name"); + Checkpoint name + + let parse_revert spec = + if spec = "" then + raise (Parse_error + "REVERT: missing uuid or checkpoint name"); + Revert spec + + let parse_search query = + if query = "" then + raise (Parse_error "SEARCH: missing query"); + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + Search query + + (* LOAD "file.ec" [LINE[:COL]] [-nosmt] [-trace]. Argument errors are + signalled with [failwith] and turned into [Parse_error] below, so + they reach the wire exactly as any other line-parse error does + (including the bare "int_of_string" of a malformed LINE:COL). *) + let parse_load args = + try + let args = String.strip args in + if args = "" then failwith "LOAD: missing filename"; + (* Parse quoted or unquoted filename. *) + let filename, rest = + if args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + if filename = "" then failwith "LOAD: missing filename"; + (* Checked here, before anything else touches the session: the + reader would otherwise raise [Sys_error] far downstream, and + the REPL would report it as an anomaly after having already + reset the scope. *) + if not (Sys.file_exists filename) then + failwith + (Printf.sprintf "LOAD: no such file: %s" filename); + + (* Parse optional LINE[:COL] and flags (-nosmt, -trace). *) + let upto, nosmt, trace = + let words = + String.split_on_char ' ' rest + |> List.filter (fun s -> s <> "") + in + let nosmt = List.mem "-nosmt" words in + let trace = List.mem "-trace" words in + let words = + List.filter + (fun s -> s <> "-nosmt" && s <> "-trace") + words + in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt, trace) + in + Load { ld_file = filename; ld_upto = upto; + ld_nosmt = nosmt; ld_trace = trace; } + with Failure msg -> raise (Parse_error msg) + + let of_line ~multi_active (raw : string) : command = + let line = String.strip raw in + if multi_active then + if line = "" then Done_multi + else Multi_line line + else + match line with + | "" -> Begin_multi + | "" -> Blank + | "QUIT" -> Quit + | "HELP" -> Help + | "UNDO" -> Undo + | "GOALS" -> Goals `One + | "GOALS ALL" -> Goals `All + | "TREE" -> Tree `One + | "TREE ALL" -> Tree `All + | "COMMIT" -> Commit + | "NEXT" -> Next + | "QUIET ON" -> Quiet true + | "QUIET OFF" -> Quiet false + | _ -> + match keyword_arg "FOCUS" line with Some a -> parse_focus a | None -> + match keyword_arg "CHECKPOINT" line with Some a -> parse_checkpoint a | None -> + match keyword_arg "REVERT" line with Some a -> parse_revert a | None -> + match keyword_arg "SEARCH" line with Some a -> parse_search a | None -> + match keyword_arg "LOAD" line with Some a -> parse_load a | None -> + Ec line +end + +(* -------------------------------------------------------------------- *) +let run ~relocdir ~boot ~projini (llmopts : EcOptions.llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + + let st = + try EcLlmCore.create ~relocdir ~boot ~projini ~prvopts + with EcLlmCore.Init_error msg -> + Format.eprintf "%s" msg; + exit 1 + in + + (* True iff replies should suppress goal bodies. Toggled by QUIET. *) + let quiet = ref false in + + (* ------------------------------------------------------------------ *) + (* OK/ERROR/ wire envelope: the only printers. *) + let had_error = ref false in + + let module Wire = struct + let reply_ok (r : EcLlmCore.reply) = + let body = + match r.EcLlmCore.body with + | EcLlmCore.Text body -> body + | EcLlmCore.Goals -> + if !quiet then "" else EcLlmCore.current_goals st + in + Printf.printf "OK [uuid:%d]%s\n" r.EcLlmCore.uuid r.EcLlmCore.tag; + let n = r.EcLlmCore.notices in + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!" + + let reply_failure (f : EcLlmCore.failure) = + had_error := true; + let goals = f.EcLlmCore.goals in + Printf.printf "ERROR [uuid:%d]\n%s\n" + f.EcLlmCore.uuid f.EcLlmCore.message; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!" + + (* Render an operation's outcome. *) + let reply = function + | Ok reply -> reply_ok reply + | Error failed -> reply_failure failed + + (* Same, for operations that may end the session. *) + let answer = function + | EcLlmCore.Quit -> exit 0 + | EcLlmCore.Done outcome -> reply outcome + + let reply_error msg = + reply_failure (EcLlmCore.make_failure st msg) + end in + + (* ------------------------------------------------------------------ *) + (* Command handlers. Each takes (already-parsed) data and produces a + wire reply via [Wire] (or exits the process). Multi-line state is + held here so [Parse] can stay pure. *) + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + let module Dispatch = struct + let do_help () = + EcLlmCore.clear_notices st; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + Wire.reply_ok + (EcLlmCore.make_reply st (EcLlmCore.Text (Buffer.contents buf))) + with Sys_error e -> + Wire.reply_error (Printf.sprintf "cannot read guide: %s" e) + end + + let do_quiet on = + EcLlmCore.clear_notices st; + quiet := on; + Wire.reply_ok (EcLlmCore.make_reply st (EcLlmCore.Text "")) + + let do_begin_multi () = + Buffer.clear multi_buf; + in_multi := true + + let do_done_multi () = + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then Wire.answer (EcLlmCore.step st input) + + let do_multi_line s = + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf s + + let run (cmd : Parse.command) = + match cmd with + | Blank -> () + | Quit -> exit 0 + | Help -> do_help () + | Undo -> Wire.reply (EcLlmCore.undo st) + | Goals `One -> Wire.reply (EcLlmCore.goals st ~all:false) + | Goals `All -> Wire.reply (EcLlmCore.goals st ~all:true) + | Tree `One -> Wire.reply (EcLlmCore.tree st ~all:false) + | Tree `All -> Wire.reply (EcLlmCore.tree st ~all:true) + | Commit -> Wire.reply (EcLlmCore.commit st) + | Focus path -> Wire.reply (EcLlmCore.focus st (`Path path)) + | Next -> Wire.reply (EcLlmCore.focus st `Next) + | Checkpoint n -> Wire.reply (EcLlmCore.checkpoint st ~name:n) + | Revert s -> Wire.reply (EcLlmCore.revert st s) + | Quiet on -> do_quiet on + | Search q -> Wire.answer (EcLlmCore.search st ~pattern:q) + | Load args -> + Wire.reply (EcLlmCore.load st + ~file:args.Parse.ld_file + ~upto:args.Parse.ld_upto + ~nosmt:args.Parse.ld_nosmt + ~trace:args.Parse.ld_trace) + | Ec input -> Wire.answer (EcLlmCore.step st input) + | Begin_multi -> do_begin_multi () + | Done_multi -> do_done_multi () + | Multi_line s -> do_multi_line s + end in + + (* ------------------------------------------------------------------ *) + (* Main loop. *) + + Printf.printf "READY [uuid:%d]\n\n%!" (EcLlmCore.uuid st); + + (* Input source: stdin by default, or the -eval string when given. + For -eval, we split on newlines up front (no lazy channel), which + keeps the driver simple and avoids ever touching stdin. *) + let read_line : unit -> string = + match llmopts.llmo_eval with + | None -> + fun () -> input_line stdin + | Some script -> + let lines = ref (String.split_on_char '\n' script) in + fun () -> + match !lines with + | [] -> raise End_of_file + | l :: tl -> lines := tl; l + in + + begin try while true do + let line = read_line () in + (try + let cmd = Parse.of_line ~multi_active:!in_multi line in + Dispatch.run cmd + with Parse.Parse_error msg -> + Wire.reply_error msg) + done with + | End_of_file -> () + end; + + (* Scripted runs (-eval) report in-band errors through the exit + status, so that automation does not mistake an ERROR reply for + success. Interactive sessions keep exiting 0. *) + exit (if llmopts.llmo_eval <> None && !had_error then 1 else 0) diff --git a/src/ecLlm.mli b/src/ecLlm.mli new file mode 100644 index 000000000..28b9896d5 --- /dev/null +++ b/src/ecLlm.mli @@ -0,0 +1,20 @@ +(* -------------------------------------------------------------------- *) +(* The LLM coding-agent REPL: an interactive proof-development protocol + over stdin/stdout. Driven via the [easycrypt llm] command. *) + +(* Path to the bundled agent guide ([doc/llm/CLAUDE.md] in a source + tree, its installed copy otherwise). [llm -help] and the [HELP] + command print the whole of it; exposed because [mcp -help] prints one + section of the same file. *) +val llm_guide_path : unit -> string + +(* Run the REPL until [QUIT] or EOF, then exit the process. Never + returns. [projini] resolves the [easycrypt.project] context of a + file path, so [LOAD] can apply the project's load path and prover + options the way the batch compiler does. *) +val run : + relocdir:string option + -> boot:bool + -> projini:(string option -> EcOptions.ini_context option) + -> EcOptions.llm_option + -> 'a diff --git a/src/ecLlmCore.ml b/src/ecLlmCore.ml new file mode 100644 index 000000000..dbc5d7b45 --- /dev/null +++ b/src/ecLlmCore.ml @@ -0,0 +1,1058 @@ +(* -------------------------------------------------------------------- *) +(* Engine-facing core of the LLM interaction protocol. See + [ecLlmCore.mli]. This module owns the session state and implements + one function per meta-command; it never prints and never exits. The + text envelope ([OK]/[ERROR]/[]) is the front-end's business. *) + +open EcUtils + +module EP = EcParsetree + +(* -------------------------------------------------------------------- *) +type body = + | Goals + | Text of string + +type reply = { + uuid : int; + tag : string; + notices : string; + body : body; + changed : bool; +} + +type failure = { + uuid : int; + message : string; + goals : string; + notices : string; + reverted : bool; + changed : bool; +} + +type answer = + | Done of (reply, failure) result + | Quit + +exception Init_error of string + +(* -------------------------------------------------------------------- *) +(* Session state. The proof engine ([EcCommands]) is a global mutable + singleton, so at most one [state] may exist per process. *) +type state = { + (* Prover options as given on the command line: the base [LOAD] + overlays the loaded file's [easycrypt.project] settings onto. *) + base_prvopts : EcOptions.prv_options; + + (* Resolves the [easycrypt.project] context of a file path. *) + projini : string option -> EcOptions.ini_context option; + + boot : bool; + + (* Prover options in effect: refreshed by [LOAD] with the loaded + file's [easycrypt.project] settings overlaid on the command-line + options, as the batch compiler does at option-parsing time. *) + cur_prvopts : EcOptions.prv_options ref; + + (* Messages emitted by the engine during a phrase; flushed into the + next reply. *) + notices : Buffer.t; + + (* Has [EcCommands.initialize] been called? Subsequent calls pass + [~restart:true]. *) + initialized : bool ref; + + (* Project-file load-path entries already added to the (global) + loader, so repeated [LOAD]s do not pile up duplicates. *) + projdirs : (string option * string * bool) list ref; + + (* CHECKPOINT name -> uuid. *) + checkpoints : (string, int) Hashtbl.t; + + (* Transcript of REPL-typed phrases that succeeded. Each entry is + [(uuid_before, src, parent, opens_at_entry)]: + - [parent]: focused handle right before the phrase ([None] iff + outside a proof); + - [opens_at_entry]: full open-handle list (focused first), used + by [Commit] to seed the sibling map when the first recorded + phrase already sits inside a frame opened by the LOAD prefix. + Trimmed by UNDO/REVERT; cleared on LOAD/Restart. *) + transcript : + (int * string * EcCoreGoal.handle option + * EcCoreGoal.handle list) list ref; + + (* Proof environment snapshot, refreshed at every recorded phrase. + [COMMIT] queries the proof DAG through it rather than through the + active proof, which is gone once [qed] has run. A [proofenv] is + immutable and cumulative, so the last snapshot knows about every + handle any transcript entry can mention. *) + commit_env : EcCoreGoal.proofenv option ref; + + (* The bullet stack of the active proof at the moment REPL input + took over. Captured the first time [disable_repl_bullets] clears + a non-empty stack. Used by [Commit] to pick bullet characters + that don't collide with frames opened by the LOAD prefix. + Cleared with the transcript on LOAD/Restart. *) + prior_bullets : EcBullets.stack option ref; +} + +(* -------------------------------------------------------------------- *) +let checkmode_of (prvopts : EcOptions.prv_options) = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_quorum = prvopts.prvo_quorum; + EcCommands.cm_profile = prvopts.prvo_profile; +} + +let notifier (st : state) = + fun (_ : EcGState.loglevel) (lazy msg) -> + Buffer.add_string st.notices msg; + Buffer.add_char st.notices '\n' + +let do_initialize (st : state) = + let initialized = st.initialized in + let cur_prvopts = st.cur_prvopts in + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot:st.boot ~checkmode:(checkmode_of !cur_prvopts) ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma_option !cur_prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier (notifier st); + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + !cur_prvopts.prvo_ppwidth + +(* -------------------------------------------------------------------- *) +let create ~relocdir ~boot ~projini ~prvopts = + Random.self_init (); + + prvopts.EcOptions.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + raise (Init_error (Format.asprintf + "cannot connect to Why3 server `%s': %s" server e))); + + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + let st = { + base_prvopts = prvopts; + projini; + boot; + cur_prvopts = ref prvopts; + notices = Buffer.create 256; + initialized = ref false; + projdirs = ref []; + checkpoints = Hashtbl.create 16; + transcript = ref []; + commit_env = ref None; + prior_bullets = ref None; + } in + + do_initialize st; st + +(* -------------------------------------------------------------------- *) +(* Goal/error formatting: shared between the reply layer and the + -trace block. *) +module Goals = struct + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + + (* Inline focus annotation ([focus: 1/N]) appended to reply tags + whenever the active proof has >=2 open subgoals. *) + let focus_tag () = + match EcCommands.pp_tree () with + | _ :: _ :: _ as entries -> + Printf.sprintf " [focus: 1/%d]" (List.length entries) + | _ -> "" +end + +(* -------------------------------------------------------------------- *) +(* Frame tree: group currently-open goals by their shared multi-child + ancestors. Used by [Tree] (rendering) and [Focus] (path lookup). + The tree is a *derivation*: it depends only on [pr_opened] and + [parent_of], no recorded transcript. *) +module FrameTree = struct + (* Internal nodes are split-point frames; leaves carry a handle + (the open goal), its index in [pr_opened] (1-based, used by + [EcCoreGoal.rotate_focus]), and its rendered text. *) + type node = + | Frame of node list (* >=2 child branches *) + | Leaf of + { idx : int (* 1-based in pr_opened *) + ; focused : bool (* idx = 1 *) + ; text : string } (* one-line conclusion *) + + (* Multi-child ancestors of [h], outermost first (= root-most + split first, deepest split last). This ordering means leaves + sharing the same OUTER frame will agree on the chain's first + element, which is what [group] partitions on. *) + let split_chain h = + let rec walk h acc = + match EcCommands.parent_of h with + | None -> acc + | Some p -> + match EcCommands.children_of p with + | [_] -> walk p acc + | _ -> walk p (p :: acc) + in + (* [walk] prepends each ancestor as we go up; the result has + outermost at the FRONT (we add it last). No reverse needed. *) + walk h [] + + (* Build the tree by grouping leaves with a common ancestor prefix. + [leaves] is a list of (chain, leaf) in [pr_opened] order. The + grouping is done recursively on the head of each chain. *) + let rec group (leaves : (EcCoreGoal.handle list * node) list) : node list = + let rec runs acc = function + | [] -> List.rev acc + | (chain, leaf) :: rest -> + match chain with + | [] -> runs (`Bare leaf :: acc) rest + | hd :: tl -> + let same_head, others = + List.partition_map (fun (c, l) -> + match c with + | h :: tail when EcCoreGoal.eq_handle h hd -> + Left (tail, l) + | _ -> Right (c, l)) + rest + in + runs (`Group ((tl, leaf) :: same_head) :: acc) others + in + List.map + (function + | `Bare leaf -> leaf + | `Group children -> Frame (group children)) + (runs [] leaves) + + (* Strip leading singleton frames so the top-level forest's + indices match what the user thinks of as "top-level subgoals + of the current frame." When all open leaves descend from a + single outermost split, the top-level forest has one Frame + containing the actual user-visible siblings; unwrap it. *) + let rec unwrap forest = + match forest with + | [Frame children] -> unwrap children + | _ -> forest + + let build () = + let handles = EcCommands.open_handles () in + let texts = EcCommands.pp_tree () in + if handles = [] then [] + else + let leaves = + List.mapi (fun i (h, (_, focused, text)) -> + let leaf = Leaf { idx = i + 1; focused; text } in + (split_chain h, leaf)) + (List.combine handles texts) + in + unwrap (group leaves) + + (* Render the tree with dotted-path labels matching what FOCUS + accepts. [all] requests full goal bodies (we re-query via + [pp_tree ~all:true] keyed by leaf index). *) + let render ?(all=false) () = + let forest = build () in + if forest = [] then "No active proof.\n" + else + let texts_all = + if all then Some (EcCommands.pp_tree ~all:true ()) + else None + in + let one_line s = + let s = + match String.index_opt s '\n' with + | None -> s + | Some k -> String.sub s 0 k + in + let limit = 80 in + if String.length s > limit + then String.sub s 0 (limit - 1) ^ "…" + else s + in + let buf = Buffer.create 256 in + let rec emit ~depth ~path = function + | Leaf { idx; focused; text } -> + let label = String.concat "." (List.rev_map string_of_int path) in + let marker = if focused then " <- focused" else "" in + for _ = 1 to depth do Buffer.add_string buf " " done; + (match texts_all with + | None -> + Buffer.add_string buf + (Printf.sprintf "[%s] %s%s\n" + label (one_line text) marker) + | Some entries -> + let (_, _, full) = + List.nth entries (idx - 1) + in + Buffer.add_string buf + (Printf.sprintf "[%s]%s\n%s\n" label marker full)) + | Frame children -> + List.iteri (fun i child -> + emit ~depth:(depth + 1) ~path:((i + 1) :: path) child) + children + in + List.iteri (fun i node -> + emit ~depth:0 ~path:[i + 1] node) + forest; + Buffer.contents buf + + (* Resolve a dotted path against the tree. Returns [Ok idx] where + [idx] is the 1-based position in [pr_opened] of the selected + leaf, or [Error msg]. *) + let resolve_path (path : int list) : (int, string) result = + let forest = build () in + let rec walk ~components nodes = + match components with + | [] -> Error "FOCUS: path must select a leaf goal" + | k :: rest -> + if k < 1 || k > List.length nodes then + Error (Printf.sprintf + "FOCUS: index %d out of range (1..%d)" + k (List.length nodes)) + else + match List.nth nodes (k - 1), rest with + | Leaf { idx; _ }, [] -> Ok idx + | Leaf _, _ -> + Error "FOCUS: path overshoots a leaf goal" + | Frame _, [] -> + Error "FOCUS: path must select a leaf goal, \ + not a frame" + | Frame kids, _ -> walk ~components:rest kids + in + if forest = [] then Error "FOCUS: no active proof" + else walk ~components:path forest +end + +(* -------------------------------------------------------------------- *) +(* Reply construction. The notice buffer is captured and cleared at + exactly the points the text front-end used to print it, so that + engine messages keep interleaving with replies as before. *) +let mk_reply (st : state) ~(pre : int) ?(tag = "") (body : body) = + let notices = Buffer.contents st.notices in + Buffer.clear st.notices; + let uuid = EcCommands.uuid () in + { uuid; tag; notices; body; changed = uuid <> pre; } + +(* The body of a reply that ends on the current goals. The front-end + decides whether to render them (QUIET is a presentation setting). *) +let mk_reply_goals (st : state) ~(pre : int) = + let tag = Goals.focus_tag () in + mk_reply st ~pre ~tag Goals + +let mk_failure (st : state) ~(pre : int) (message : string) = + let notices = Buffer.contents st.notices in + Buffer.clear st.notices; + let uuid = EcCommands.uuid () in + { uuid; message; goals = Goals.goals_to_string (); notices; + reverted = false; changed = uuid <> pre; } + +(* -------------------------------------------------------------------- *) +(* Transcript manipulation. *) +module Transcript = struct + let trim (st : state) target = + let transcript = st.transcript in + transcript := + List.filter + (fun (uuid_before, _, _, _) -> uuid_before < target) + !transcript + + let clear (st : state) = + st.transcript := []; + st.prior_bullets := None; + st.commit_env := None +end + +(* -------------------------------------------------------------------- *) +(* Process a single EasyCrypt command, respecting [gl_fail]. When + [~record:true], append a transcript entry on success: the parent + handle (focused goal before the phrase) and the open-handle list, + which together let [Commit] reconstruct bullet structure. *) +let process_action (st : state) ?(record=false) ~src (p : EP.global) = + let transcript = st.transcript in + let commit_env = st.commit_env in + let loc = p.EP.gl_action.EcLocation.pl_loc in + let pre_uuid = EcCommands.uuid () in + let opens_pre = + if record then EcCommands.open_handles () else [] + in + let parent = + match opens_pre with h :: _ -> Some h | [] -> None + in + (* Queries only inspect the environment: they neither advance the + proof nor belong in the body COMMIT emits. *) + let is_query = + match EcLocation.unloc p.EP.gl_action with + | EP.Gprint _ | EP.Gsearch _ | EP.Glocate _ -> true + | _ -> false + in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + (* The engine pushes an undo context for every command it runs, a + query included -- with the *same* scope, since a query returns the + scope it was handed. Pop it back off: a read-only command must not + spend a uuid, or REVERT targets and the MCP [readOnlyHint] would + both be lying. A no-op when the query failed (nothing was pushed). *) + if is_query then EcCommands.undo pre_uuid; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))); + if record && !succeeded && not p.EP.gl_fail && not is_query then begin + transcript := (pre_uuid, src, parent, opens_pre) :: !transcript; + (* Keep the newest non-empty snapshot: a phrase that closes the + proof ([qed]) leaves no active proof, and precisely then we + still need the environment the previous phrases built. *) + match EcCommands.current_proofenv () with + | None -> () + | Some _ as penv -> commit_env := penv + end + +(* -------------------------------------------------------------------- *) +(* COMMIT: replay the transcript against the proof DAG (parent_of / + children_of, backed by [EcCoreGoal.pr_parent]), inserting bullets + at multi-child splits. Levels the LOAD prefix's [puc_bullets] stack + already opened are addressed with that frame's own token; deeper + levels get fresh tokens, chosen so they collide with neither the + stack nor each other. *) +module Commit = struct + (* Token order matches PR 1017's lexer: -, +, *, --, ++, **, + ---, +++, *** ... *) + let token_at_index i = + let chars = [| "-"; "+"; "*" |] in + let rep = i / 3 + 1 in + let chr = chars.(i mod 3) in + String.concat "" (List.init rep (fun _ -> chr)) + + (* DAG queries go through the snapshot recorded at the last phrase, + so COMMIT still sees the structure after [qed]. Fall back to the + live proof when no phrase was recorded under a proof. *) + let parent_of (st : state) h = + match !(st.commit_env) with + | Some penv -> EcCoreGoal.parent_of_handle penv h + | None -> EcCommands.parent_of h + + let children_of (st : state) h = + match !(st.commit_env) with + | Some penv -> EcCoreGoal.children_of_handle penv h + | None -> EcCommands.children_of h + + let proof_text (st : state) = + let parent_of = parent_of st in + let children_of = children_of st in + let transcript = st.transcript in + let prior_bullets = st.prior_bullets in + let entries = List.rev !transcript in + let buf = Buffer.create 1024 in + let emit_indent depth = + for _ = 1 to depth do Buffer.add_string buf " " done + in + let module Hmap = + Map.Make (struct + type t = EcCoreGoal.handle + let compare = compare + end) + in + let sibling_depth : int Hmap.t ref = ref Hmap.empty in + let current_depth = ref 0 in + let bullet_to_string (b : EcParsetree.bullet) = + let ch = + match b.b_kind with + | `Minus -> "-" + | `Plus -> "+" + | `Star -> "*" + in + String.concat "" (List.init b.b_count (fun _ -> ch)) + in + (* Bullet frames the LOAD prefix left open, OUTERMOST first (the + stack stores the innermost frame at its head). Frame [t_d] is + the one whose siblings live at emitted depth [d]. *) + let frames : EcBullets.frame list = + match !prior_bullets with + | None -> [] + | Some stack -> List.rev stack + in + let in_use_tokens = + List.map + (fun (f : EcBullets.frame) -> bullet_to_string f.bf_bullet) + frames + in + let depth_cache : (int, string) Hashtbl.t = Hashtbl.create 8 in + let next_tok_idx = ref 0 in + let assigned_tokens = ref [] in + (* Depths 1..k address the next sibling of a frame the prefix + already opened, and strict bullets accepts nothing but that + frame's own token there. Deeper levels get fresh tokens, so + pre-populate the cache before any fresh pick happens. *) + List.iteri (fun i (f : EcBullets.frame) -> + let t = bullet_to_string f.bf_bullet in + Hashtbl.replace depth_cache (i + 1) t; + assigned_tokens := t :: !assigned_tokens) + frames; + let bullet_for_depth d = + match Hashtbl.find_opt depth_cache d with + | Some t -> t + | None -> + let rec pick () = + let t = token_at_index !next_tok_idx in + incr next_tok_idx; + if List.mem t in_use_tokens || List.mem t !assigned_tokens + then pick () + else t + in + let t = pick () in + assigned_tokens := t :: !assigned_tokens; + Hashtbl.add depth_cache d t; + t + in + (* Seed: the goals already open when the first recorded phrase ran + were left there by the LOAD prefix, so COMMIT must place each of + them at the depth the prefix's own bullets put it at. A frame + with floor [f] is discharged once [f] goals remain, hence it + still owns the first [n - f] goals of the focused-first list; + a goal covered by [c] frames sits at depth [c + 1]. + Nothing to seed when the prefix left no frame and a single goal + (the REPL just continues on the prefix's own focus). *) + (match entries with + | (_, _, Some _, (_ :: _ as opens)) :: _ + when frames <> [] || List.length opens >= 2 -> + let n = List.length opens in + List.iteri (fun i h -> + let pos = i + 1 in + let covering = + List.length + (List.filter + (fun (f : EcBullets.frame) -> pos <= n - f.bf_floor) + frames) + in + sibling_depth := Hmap.add h (covering + 1) !sibling_depth) + opens + | _ -> ()); + List.iter (fun (_uuid, src, parent_opt, _opens) -> + match parent_opt with + | None -> + Buffer.add_string buf src; + Buffer.add_char buf '\n' + | Some parent -> + (* Walk upward via pr_parent until we hit a registered + sibling ancestor. If found, emit its bullet and consume + the registration. *) + let rec find_ancestor h = + match Hmap.find_opt h !sibling_depth with + | Some d -> Some (h, d) + | None -> + match parent_of h with + | Some p -> find_ancestor p + | None -> None + in + (match find_ancestor parent with + | Some (h, d) -> + emit_indent (d - 1); + Buffer.add_string buf (bullet_for_depth d); + Buffer.add_char buf ' '; + current_depth := d; + sibling_depth := Hmap.remove h !sibling_depth + | None -> + emit_indent !current_depth); + Buffer.add_string buf src; + Buffer.add_char buf '\n'; + (* Register fresh siblings: walk the subtree rooted at + [parent], finding every multi-child split, and register + each such child at the right depth. Single-child links + are continuations and don't bump depth; multi-child + links do. A compound phrase like [split; split.] can + produce nested splits within one phrase. *) + let rec walk h d = + match children_of h with + | [c] -> walk c d + | (_ :: _ :: _) as cs -> + List.iter + (fun c -> + sibling_depth := + Hmap.add c d !sibling_depth; + walk c (d + 1)) + cs + | [] -> () + in + walk parent (!current_depth + 1) + ) entries; + Buffer.contents buf +end + +(* -------------------------------------------------------------------- *) +(* Accessors used by front-ends to build their own replies (HELP, + QUIET, parse errors) and to render a [Goals] body. *) +let uuid (_ : state) = + EcCommands.uuid () + +let clear_notices (st : state) = + Buffer.clear st.notices + +let current_goals (_ : state) = + Goals.goals_to_string () + +let make_reply (st : state) ?tag (body : body) = + mk_reply st ~pre:(EcCommands.uuid ()) ?tag body + +let make_failure (st : state) (message : string) = + mk_failure st ~pre:(EcCommands.uuid ()) message + +(* -------------------------------------------------------------------- *) +(* Process EasyCrypt input typed at the prompt. The input is a file + fragment, not a single phrase: every sentence it holds runs, in + order, and one reply describes the state they leave behind. A + failure stops the run there; the sentences before it stay applied, + exactly as they would in a compiled file. *) +let step (st : state) input = + let notices = st.notices in + let prior_bullets = st.prior_bullets in + let pre = EcCommands.uuid () in + Buffer.clear notices; + (* On the first REPL phrase of each proof, capture the bullet stack + the LOAD prefix left so COMMIT can avoid token collisions with + it. Subsequent calls return [None] and don't clobber the snapshot. *) + (match EcCommands.disable_repl_bullets () with + | None -> () + | Some _ as snapshot -> prior_bullets := snapshot); + let reader = EcIo.from_string input in + let last_src = ref "" in + (* Reply body, decided by the last item that did something: a run of + sentences ends on the goals, a doc comment on an empty body. The + end-of-input marker is an empty [P_Prog], and must not count. *) + let body = ref Goals in + let quit = ref false in + let answer = + begin try + begin try while true do + last_src := ""; + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + if commands <> [] then begin + body := Goals; + List.iter (process_action st ~record:true ~src) commands + end; + if locterm then raise Exit + | EP.P_Undo i -> + body := Goals; + EcCommands.undo i; + Transcript.trim st i + | EP.P_Exit -> + (* Everything before [exit.] stays applied; the front-end + owns what happens next. *) + quit := true; raise Exit + | EP.P_DocComment doc -> + body := Text ""; + EcCommands.doc_comment doc + done with Exit | End_of_file -> () end; + if !quit then Quit else + match !body with + | Goals -> Done (Ok (mk_reply_goals st ~pre)) + | Text _ as b -> Done (Ok (mk_reply st ~pre b)) + with + | EcCommands.Restart -> + do_initialize st; + Transcript.clear st; + Done (Ok (mk_reply st ~pre (Text "Session restarted"))) + | e -> + Done (Error (mk_failure st ~pre (Goals.format_error ~src:!last_src e))) + end + in + EcIo.finalize reader; + answer + +(* -------------------------------------------------------------------- *) +(* [step] with an automatic rollback on failure. A phrase can fail + after having advanced the engine, so the pre-entry uuid is the only + faithful notion of "unchanged": restore it the way REVERT does. + The failure is then re-stamped, because its uuid, goal text and + [changed] flag described the state at the point of failure, which no + longer exists. [changed] is recomputed against the same pre-entry + uuid, so it reports the *net* effect of the call: normally [false], + the rollback having undone whatever the input managed to do. It + stays [true] in the one case where the rollback cannot reach [pre], + namely a phrase that reset the engine ([pragma Reset]) and landed + below it -- then the state really did change. *) +let try_step (st : state) input = + let pre = EcCommands.uuid () in + match step st input with + | Quit -> Quit + | Done (Ok _) as answer -> answer + | Done (Error failure) -> + EcCommands.undo pre; + Transcript.trim st pre; + let uuid = EcCommands.uuid () in + Done (Error { failure with + uuid; + goals = Goals.goals_to_string (); + reverted = true; + changed = uuid <> pre; }) + +(* -------------------------------------------------------------------- *) +(* LOAD: run [file] up to [upto], optionally with SMT calls weakened + ([nosmt]) or with the last sentence of the prefix traced. The + argument string is parsed by the front-end. *) +let load (st : state) ~file ~upto ~nosmt ~trace = + let notices = st.notices in + let cur_prvopts = st.cur_prvopts in + let projdirs = st.projdirs in + let checkpoints = st.checkpoints in + let pre = EcCommands.uuid () in + Buffer.clear notices; + let filename = file in + let last_src = ref "" in + let trace_prefix = ref "" in + let exception Trace_failed of exn in + + try + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + (* Apply the configuration attached to the loaded file's + [easycrypt.project], as the batch compiler does when the + file is given on the command line: refresh the prover + options (timeout, provers, pragmas, ...) and extend the + load path with the project's include dirs. *) + let ini = Option.to_list (st.projini (Some filename)) in + cur_prvopts := + EcOptions.prv_options_with_ini ini st.base_prvopts; + List.iter (fun ((nm, dir, isrec) as entry) -> + if not (List.mem entry !projdirs) then begin + projdirs := entry :: !projdirs; + EcCommands.addidir + ?namespace:(omap (fun nm -> `Named nm) nm) + ~recursive:isrec dir + end) + (EcOptions.ini_loadpath ini); + + do_initialize st; + Hashtbl.clear checkpoints; + Transcript.clear st; + EcCommands.addidir (Filename.dirname filename); + EcCommands.set_current_path (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* For -trace: lazy whole-file bytes, used to slice the exact + source text of a sentence by byte offsets. *) + let input_bytes = lazy ( + let ic = open_in_bin filename in + let n = in_channel_length ic in + let b = Bytes.create n in + really_input ic b 0 n; + close_in ic; + Bytes.unsafe_to_string b) + in + let sentence_source (loc : EcLocation.t) = + let s = Lazy.force input_bytes in + let lo = max 0 loc.EcLocation.loc_bchar in + let hi = min (String.length s) loc.EcLocation.loc_echar in + if hi <= lo then "" else String.sub s lo (hi - lo) + in + + (* For -trace: defer execution of the last sentence within the + prefix so we can capture goals before and after it. *) + let pending : (string * EP.global) option ref = ref None in + let flush_pending () = + match !pending with + | None -> () + | Some (src, p) -> + last_src := src; + process_action st ~src p; + last_loc := Some p.EP.gl_action.EcLocation.pl_loc; + pending := None + in + let step src p = + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + if trace then begin + flush_pending (); + pending := Some (src, p) + end else begin + last_src := src; + process_action st ~src p; + last_loc := Some loc + end + in + + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (step src) commands; + if locterm then raise Exit + | EP.P_Undo i -> + last_src := src; + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + last_src := src; + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + if nosmt then EcCommands.pragma_check `Check; + + (* If -trace is set, the last in-prefix sentence is still + pending. Run it under goal capture and build the + BEFORE/TACTIC/AFTER/SUMMARY response body. *) + let body = + if not trace then + Goals.goals_to_string () + else + let pre_state = + match !pending with + | None -> `Nothing + | Some _ when not (EcCommands.in_proof ()) -> `NotInProof + | Some (src, p) -> `Ready (src, p) + in + match pre_state with + (* Tracing is off the table, but the prefix is not: run the + sentence we deferred so that the session ends up exactly + where a plain LOAD of the same prefix would leave it. A + failure inside the flush is reported by the enclosing + handler, as any prefix failure is. *) + | `Nothing -> + flush_pending (); + failwith "trace: nothing to trace" + | `NotInProof -> + flush_pending (); + failwith + "trace: target sentence is not in a proof context" + | `Ready (src, p) -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + let (sl, sc) = loc.EcLocation.loc_start in + let (el, ec) = loc.EcLocation.loc_end in + let before_goals = EcCommands.pp_all_goals () in + let n1 = List.length before_goals in + let buf = Buffer.create 1024 in + let fmt = Format.formatter_of_buffer buf in + Format.fprintf fmt + "=== BEFORE: line %d (col %d) ===@\n" sl sc; + EcCommands.pp_current_goal_or_noproof ~all:false fmt; + Format.fprintf fmt + "@\n=== TACTIC (lines %d:%d - %d:%d) ===@\n%s@\n@\n" + sl sc el ec (sentence_source loc); + last_src := src; + begin + try + process_action st ~src p; + last_loc := Some loc; + pending := None; + let after_goals = EcCommands.pp_all_goals () in + let n2 = List.length after_goals in + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n" sl sc; + let before_set = + List.fold_left + (fun s g -> EcMaps.Sstr.add g s) + EcMaps.Sstr.empty before_goals + in + (* The new focused goal always counts as "modified" + (its focus status changed even if its text matches + an old sibling); the rest are printed only if they + didn't appear in BEFORE. *) + let to_print = + match after_goals with + | [] -> [] + | head :: tl -> + head :: + List.filter + (fun g -> not (EcMaps.Sstr.mem g before_set)) + tl + in + begin match to_print with + | [] -> Format.fprintf fmt "(no open goals)@\n" + | _ -> + List.iteri (fun i g -> + if i > 0 then Format.fprintf fmt "@\n"; + Format.fprintf fmt "%s@\n" g) + to_print + end; + Format.fprintf fmt + "@\n=== SUMMARY ===@\nopen goals: %d -> %d@\n" n1 n2; + Format.pp_print_flush fmt (); + Buffer.contents buf + with e -> + Format.fprintf fmt + "=== AFTER: line %d (col %d) ===@\n@\n" + sl sc; + Format.pp_print_flush fmt (); + trace_prefix := Buffer.contents buf; + raise (Trace_failed e) + end + in + + let tag = + let loaded = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + loaded ^ Goals.focus_tag () + in + Ok (mk_reply st ~pre ~tag (Text body)) + + with + | EcCommands.Restart -> + do_initialize st; + Hashtbl.clear checkpoints; + Transcript.clear st; + Ok (mk_reply st ~pre (Text "Session restarted")) + | Trace_failed e -> + let msg = Goals.format_error ~src:!last_src e in + Error (mk_failure st ~pre (!trace_prefix ^ msg)) + | Failure s -> + Error (mk_failure st ~pre s) + | e -> + Error (mk_failure st ~pre (Goals.format_error ~src:!last_src e)) + +(* -------------------------------------------------------------------- *) +(* The remaining meta-commands. *) + +let goals (st : state) ~all = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + Ok (mk_reply st ~pre ~tag:(Goals.focus_tag ()) + (Text (Goals.goals_to_string ~all ()))) + +let tree (st : state) ~all = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + Ok (mk_reply st ~pre ~tag:(Goals.focus_tag ()) + (Text (FrameTree.render ~all ()))) + +let commit (st : state) = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + Ok (mk_reply st ~pre ~tag:(Goals.focus_tag ()) + (Text (Commit.proof_text st))) + +let undo (st : state) = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + Transcript.trim st (uuid - 1); + Ok (mk_reply_goals st ~pre) + end else + Error (mk_failure st ~pre "nothing to undo") + +let focus (st : state) request = + (* [request] is the user's intent normalized: + - [`Next] = rotate to the second open goal (or stay if <=1) + - [`Path p] = resolve dotted path [p] against the frame tree + and focus the matching leaf. *) + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + let resolved = + match request with + | `Next -> + let n = List.length (EcCommands.open_handles ()) in + Ok (if n <= 1 then 1 else 2) + | `Path path -> FrameTree.resolve_path path + in + match resolved with + | Error msg -> Error (mk_failure st ~pre msg) + | Ok target -> + match EcCommands.focus_goal target with + | Ok _ -> Ok (mk_reply_goals st ~pre) + | Error msg -> Error (mk_failure st ~pre msg) + +let checkpoint (st : state) ~name = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + Hashtbl.replace st.checkpoints name (EcCommands.uuid ()); + Ok (mk_reply st ~pre (Text (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())))) + +let revert (st : state) spec = + let pre = EcCommands.uuid () in + Buffer.clear st.notices; + let target = + try Some (int_of_string spec) + with Failure _ -> Hashtbl.find_opt st.checkpoints spec + in + match target with + | None -> + Error (mk_failure st ~pre (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" spec)) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + Error (mk_failure st ~pre (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid)) + else begin + EcCommands.undo target; + Transcript.trim st target; + Ok (mk_reply_goals st ~pre) + end + +let search (st : state) ~pattern = + step st (Printf.sprintf "search %s." pattern) diff --git a/src/ecLlmCore.mli b/src/ecLlmCore.mli new file mode 100644 index 000000000..ba85d13b3 --- /dev/null +++ b/src/ecLlmCore.mli @@ -0,0 +1,122 @@ +(* -------------------------------------------------------------------- *) +(* Engine-facing core of the LLM interaction protocol: one operation per + meta-command of the [easycrypt llm] REPL, with the text protocol + factored out. Operations never print, never exit, and never format a + wire envelope; they return structured values a front-end renders + (the REPL in [ecLlm.ml], the MCP server next to it). + + One process = one session: the proof engine ([EcCommands]) is global + mutable state, so at most one [state] may exist per process. *) + +(* -------------------------------------------------------------------- *) +type state + +(* Reply body. [Goals] means "the current goals"; the front-end renders + them through [current_goals] and may suppress them (the REPL does, + under QUIET). [Text] is a literal body and is never suppressed. *) +type body = + | Goals + | Text of string + +(* [notices] are the engine messages emitted while the operation ran, + captured and cleared at the point the REPL used to print them. + [changed] tells whether the engine uuid advanced. *) +type reply = { + uuid : int; + tag : string; + notices : string; + body : body; + changed : bool; +} + +(* [goals] is the goal state at the point of failure. The REPL does not + render [notices] on failures (it never did); they are captured all + the same, so the buffer is left clean for the next operation. + [reverted] is set by [try_step] only: it says the engine was rolled + back to the state it had before the operation ran, so [uuid] and + [goals] describe that restored state, not the point of failure. + [changed] tells whether the engine uuid advanced -- a failing + operation may well have moved the engine before failing. It reports + the *net* effect of the call, so under [try_step] it is [false] for + a phrase that advanced, failed and was rolled back: after the + rollback there is nothing left to have changed. *) +type failure = { + uuid : int; + message : string; + goals : string; + notices : string; + reverted : bool; + changed : bool; +} + +(* Operations that can be asked to end the session ([exit.]) return an + [answer]: the front-end owns the process, hence the exit. *) +type answer = + | Done of (reply, failure) result + | Quit + +(* Raised by [create] when the session cannot be set up. *) +exception Init_error of string + +(* -------------------------------------------------------------------- *) +(* Open a session: connect to the Why3 server, seed the loader with + [relocdir], and initialize the engine. [projini] resolves the + [easycrypt.project] context of a file path, so [load] can apply the + project's load path and prover options the way the batch compiler + does. *) +val create : + relocdir:string option + -> boot:bool + -> projini:(string option -> EcOptions.ini_context option) + -> prvopts:EcOptions.prv_options + -> state + +(* -------------------------------------------------------------------- *) +(* Operations. *) + +(* LOAD, on already-parsed arguments. *) +val load : + state + -> file:string + -> upto:(int * int option) option + -> nosmt:bool + -> trace:bool + -> (reply, failure) result + +(* Raw EasyCrypt input: one line, or a multi-line block. Every + sentence the input holds is executed, in order, and a single reply + describes the state they leave behind. A sentence that fails stops + the run at that point and its failure is returned; the sentences + before it stay applied, as they would in a compiled file. An + [exit.] ends the session immediately, with the sentences that + preceded it applied. *) +val step : state -> string -> answer + +(* [step], but a failure leaves no trace: the engine is rolled back to + the uuid it had on entry (as REVERT does) and the failure comes back + with [reverted = true]. Successes and [Quit] behave exactly as in + [step]. Input that fails after having already advanced the engine + -- a phrase with a side effect, or an earlier sentence of a + multi-sentence input -- is rolled back whole. *) +val try_step : state -> string -> answer + +val goals : state -> all:bool -> (reply, failure) result +val tree : state -> all:bool -> (reply, failure) result +val focus : state -> [`Next | `Path of int list] -> (reply, failure) result +val undo : state -> (reply, failure) result +val revert : state -> string -> (reply, failure) result +val checkpoint : state -> name:string -> (reply, failure) result +val commit : state -> (reply, failure) result +val search : state -> pattern:string -> answer + +(* -------------------------------------------------------------------- *) +(* Front-end helpers: for replies a front-end produces on its own (the + REPL's HELP and QUIET) and for errors it detects itself (line-parse + errors). Both capture-and-clear the notice buffer, as the operations + above do. *) + +val uuid : state -> int +val current_goals : state -> string +val clear_notices : state -> unit +val make_reply : state -> ?tag:string -> body -> reply +val make_failure : state -> string -> failure diff --git a/src/ecMcp.ml b/src/ecMcp.ml new file mode 100644 index 000000000..e0eb15b59 --- /dev/null +++ b/src/ecMcp.ml @@ -0,0 +1,744 @@ +(* -------------------------------------------------------------------- *) +(* The Model Context Protocol front-end. See [ecMcp.mli]. + + This module is to MCP what [EcLlm] is to the text protocol: a wire + layer only. Every engine-facing operation goes through [EcLlmCore], + which the two front-ends share. + + The loop is synchronous and single-threaded, which is not an + implementation shortcut but the correctness anchor: the proof engine + is a global mutable singleton and uuid ordering is what makes + [ec_revert] meaningful, so tool calls must run strictly in arrival + order even when a client pipelines them. *) + +module J = Yojson.Safe + +(* -------------------------------------------------------------------- *) +(* Protocol revisions. + + We speak the handshake-based ("legacy", in the vocabulary of the + 2026-07-28 spec) era: [initialize] / [notifications/initialized], + with the negotiated version fixed for the life of the process. Every + deployed client speaks it. + + Revision 2026-07-28 replaced the handshake with per-request [_meta] + and a mandatory [server/discover]; supporting it is a separate piece + of work. A dual-era client probes with [server/discover], gets our + [-32601] -- not a recognized modern error -- and falls back to + [initialize], which is exactly the intended detection path. *) +let protocol_latest = "2025-11-25" + +let protocol_supported = [ + "2025-11-25"; + "2025-06-18"; + "2025-03-26"; +] + +let server_name = "easycrypt" + +let server_version = + match EcVersion.hash with "n/a" -> "dev" | v -> v + +(* -------------------------------------------------------------------- *) +(* JSON-RPC 2.0 error codes. *) +let e_parse_error = -32700 +let e_invalid_request = -32600 +let e_method_not_found = -32601 +let e_invalid_params = -32602 + +(* Raised by argument validation: a malformed [tools/call] is a + *protocol* failure, and must not be dressed up as a prover error. *) +exception Invalid_params of string + +(* Raised by the checks a tool performs on its own behalf before + reaching the engine (a missing file, say). Those are EasyCrypt-level + failures and travel as successful responses with [isError]. *) +exception Tool_error of string + +(* -------------------------------------------------------------------- *) +(* [-help]. Where [llm -help] prints the whole agent guide, we print the + one section of it that describes this server: from its heading down + to the next heading of the same level. A guide in which that heading + cannot be found is printed whole, rather than not at all. *) +let usage_section = "## Using the MCP mode" + +let extract_usage (guide : string) = + let is_heading line = + String.length line >= 3 && String.sub line 0 3 = "## " in + let rec seek = function + | [] -> None + | line :: rest when String.trim line = usage_section -> + Some (line :: keep rest) + | _ :: rest -> seek rest + and keep = function + | [] -> [] + | line :: _ when is_heading line -> [] + | line :: rest -> line :: keep rest + in + match seek (String.split_on_char '\n' guide) with + | None -> guide + | Some lines -> String.concat "\n" lines + +let print_usage () = + let path = EcLlm.llm_guide_path () in + try + let ic = open_in_bin path in + let guide = really_input_string ic (in_channel_length ic) in + close_in ic; + print_string (extract_usage guide) + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + +(* -------------------------------------------------------------------- *) +(* JSON schema fragments for the tool declarations. *) +module Schema = struct + let str ?description () = + `Assoc (("type", `String "string") + :: (match description with + | None -> [] + | Some d -> [("description", `String d)])) + + let int ~description () = + `Assoc [("type", `String "integer"); + ("description", `String description)] + + let bool ~description ~default () = + `Assoc [("type", `String "boolean"); + ("description", `String description); + ("default", `Bool default)] + + let obj ?(required = []) props = + `Assoc ([("type", `String "object"); + ("properties", `Assoc props)] + @ (match required with + | [] -> [] + | _ -> [("required", + `List (List.map (fun s -> `String s) required))]) + @ [("additionalProperties", `Bool false)]) + + (* Every tool answers with the same structured payload: the reply + text, the engine state the call left behind, and whether it moved. + + [text] repeats [content[0].text] verbatim. The duplication is + deliberate: Claude Code, our primary client, hands the model the + [structuredContent] object alone and drops [content] whenever both + are present, so a payload that lives only in [content] never + reaches the agent. See tests/mcp/README.md. *) + let output ?(reverted = false) () = + let base = [ + ("text", str ~description:"the reply body -- goal state, proof \ + body, search results, error text; the \ + same string as content[0].text" ()); + ("uuid", int ~description:"engine state identifier after the call; \ + pass it to ec_revert to come back here" ()); + ("changed", `Assoc [("type", `String "boolean"); + ("description", + `String "whether the engine state advanced")]); + ] in + let base = + if not reverted then base + else base @ [ + ("reverted", + `Assoc [("type", `String "boolean"); + ("description", + `String "set when the phrase failed and the engine was \ + rolled back to its pre-call state")]); + ] + in + `Assoc [("type", `String "object"); + ("properties", `Assoc base); + ("required", `List [`String "text"; `String "uuid"; + `String "changed"])] +end + +(* -------------------------------------------------------------------- *) +(* The static tool table, in [tools/list] order. Descriptions are + agent-facing and track the wording of doc/llm/CLAUDE.md. *) +let tools : J.t list = + let tool ~name ~description ~input ?(annotations = []) ~output () = + `Assoc ([ + ("name", `String name); + ("description", `String description); + ("inputSchema", input); + ("outputSchema", output); + ] @ (match annotations with + | [] -> [] + | _ -> [("annotations", `Assoc annotations)])) + in [ + tool + ~name:"ec_load" + ~description: + "Reset the session and compile FILE from the top, stopping after \ + the last sentence that ends on or before LINE (and column COL \ + when given). This is the entry point: every other tool needs a \ + loaded file, and tactics need the position to land inside a \ + proof. Set nosmt to weaken SMT calls while replaying a prefix \ + that was already verified, which is much faster on large files. \ + Set trace to have the reply describe the last loaded sentence as \ + BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports \ + where compilation stopped and the resulting goal state; note the \ + uuid it returns, reverting to it is the instant way back to the \ + start of the proof." + ~input:(Schema.obj ~required:["file"] [ + ("file", Schema.str ~description:"path to the .ec/.eca file" ()); + ("line", Schema.int + ~description:"stop after the last sentence ending on \ + or before this line; omit to compile the \ + whole file" ()); + ("col", Schema.int + ~description:"column bound within `line'; requires \ + `line'" ()); + ("nosmt", Schema.bool + ~description:"weaken SMT calls while compiling the \ + prefix" ~default:false ()); + ("trace", Schema.bool + ~description:"report the proof state around the last \ + loaded sentence" ~default:false ()); + ]) + ~annotations:[("destructiveHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_step" + ~description: + "Run EasyCrypt sentences -- tactics, declarations, require, \ + print, ... -- against the current session. Every complete \ + sentence in the argument is executed, in order, exactly as if \ + the text had been appended to the source file, and a single \ + reply describes the state they leave behind; sentences may \ + span several lines. Requires a file loaded with ec_load, and, \ + for tactics, an open proof. On success the reply carries the \ + new goal state; on failure the prover's error text comes back \ + with isError set, the sentences before the failing one stay \ + applied and the engine is left wherever that sentence left it \ + -- use ec_try when you want a guaranteed rollback. Successful \ + non-query phrases are recorded for ec_commit." + ~input:(Schema.obj ~required:["phrase"] [ + ("phrase", Schema.str + ~description:"one or more complete EasyCrypt \ + sentences, each ending with `.'" ()); + ]) + ~annotations:[("destructiveHint", `Bool false); + ("idempotentHint", `Bool false)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_try" + ~description: + "Like ec_step, but the engine is rolled back to the state it had \ + before the call whenever a sentence fails, including input that \ + failed only after having already advanced the proof. The \ + failure reply sets structuredContent.reverted to true, and its \ + uuid and goal text describe the restored state, not the point \ + of failure. Use this to probe a tactic without having to \ + ec_revert afterwards; use ec_step when you mean to keep \ + whatever progress the phrase makes. A successful phrase behaves \ + exactly as under ec_step and is recorded for ec_commit." + ~input:(Schema.obj ~required:["phrase"] [ + ("phrase", Schema.str + ~description:"one complete EasyCrypt sentence, \ + ending with `.'" ()); + ]) + ~annotations:[("destructiveHint", `Bool false)] + ~output:(Schema.output ~reverted:true ()) + (); + + tool + ~name:"ec_goals" + ~description: + "Print the current proof state: the focused subgoal alone, or, \ + with all set, every open subgoal. Requires an open proof, and \ + does not advance the engine." + ~input:(Schema.obj [ + ("all", Schema.bool + ~description:"print every open subgoal instead of the \ + focused one" ~default:false ()); + ]) + ~annotations:[("readOnlyHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_tree" + ~description: + "List the open subgoals as a tree of dotted-path labels -- [1], \ + [1.2], [2.1.1] -- showing how the splits nest, and marking the \ + focused one. Those labels are exactly what ec_focus accepts. \ + Set full for whole goal bodies rather than one-line \ + conclusions. The labels are not stable across focus changes: \ + the tree always shows the focused goal first, so re-read it \ + after every ec_focus. Does not advance the engine." + ~input:(Schema.obj [ + ("full", Schema.bool + ~description:"print full goal bodies instead of \ + one-line conclusions" ~default:false ()); + ]) + ~annotations:[("readOnlyHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_focus" + ~description: + "Rotate the focus onto the subgoal at dotted path PATH, as \ + printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"); a single \ + integer selects the k-th goal of the flat listing, and the \ + special value \"next\" moves to the next open subgoal. \ + Subsequent tactics act on the focused goal. Selecting an \ + internal frame instead of a leaf goal is an error." + ~input:(Schema.obj ~required:["path"] [ + ("path", Schema.str + ~description:"\"N\", a dotted path \"N1.N2...\", or \ + \"next\"" ()); + ]) + ~annotations:[("destructiveHint", `Bool false)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_undo" + ~description: + "Undo the last engine step, returning to the immediately \ + preceding state. The ec_commit transcript is trimmed to match. \ + Fails when there is nothing left to undo." + ~input:(Schema.obj []) + ~annotations:[("destructiveHint", `Bool false)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_revert" + ~description: + "Return the session to an earlier state, named either by a uuid \ + reported in some previous structuredContent or by a name given \ + to ec_checkpoint. Reverting is instant, unlike re-running \ + ec_load, so going back to the uuid ec_load returned is the cheap \ + way to restart a proof from scratch after a failed experiment. \ + The ec_commit transcript is trimmed to match." + ~input:(Schema.obj ~required:["target"] [ + ("target", Schema.str + ~description:"a uuid (as a decimal string) or a \ + checkpoint name" ()); + ]) + ~annotations:[("destructiveHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_checkpoint" + ~description: + "Record the current uuid under NAME, so that ec_revert can \ + address it by name later. Worth doing before a branching \ + experiment, when carrying the bare uuid around is awkward. Does \ + not change the proof state." + ~input:(Schema.obj ~required:["name"] [ + ("name", Schema.str ~description:"checkpoint name" ()); + ]) + ~annotations:[("readOnlyHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_commit" + ~description: + "Emit the phrases recorded since the last ec_load as a proof \ + body, with bullets inserted at every multi-child split: the \ + result compiles under `pragma +strict_bullets' and can be \ + pasted straight into the source file. Queries (search, print, \ + locate, ec_search) are never recorded, so looking things up \ + mid-proof does not pollute the body, and ec_undo / ec_revert \ + trim the transcript. Still works after `qed.'. Does not change \ + the proof state." + ~input:(Schema.obj []) + ~annotations:[("readOnlyHint", `Bool true)] + ~output:(Schema.output ()) + (); + + tool + ~name:"ec_search" + ~description: + "Search the environment for lemmas matching an EasyCrypt search \ + pattern. This is pattern syntax, not keyword search: use _ as \ + the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ \ + <= _)\". Requires a loaded file. The query neither advances the \ + proof nor enters the ec_commit transcript." + ~input:(Schema.obj ~required:["pattern"] [ + ("pattern", Schema.str + ~description:"an EasyCrypt search pattern" ()); + ]) + ~annotations:[("readOnlyHint", `Bool true)] + ~output:(Schema.output ()) + (); + ] + +(* -------------------------------------------------------------------- *) +(* Argument access. Everything here reports through [Invalid_params]: + these are failures to satisfy the declared input schema, which the + spec classifies as protocol errors, not tool-execution errors. *) +module Args = struct + let of_params (params : J.t option) = + match params with + | None | Some `Null -> [] + | Some (`Assoc fields) -> fields + | Some _ -> raise (Invalid_params "`params' must be an object") + + let arguments (params : J.t option) = + match List.assoc_opt "arguments" (of_params params) with + | None | Some `Null -> [] + | Some (`Assoc fields) -> fields + | Some _ -> raise (Invalid_params "`arguments' must be an object") + + let bad tool name expected = + raise (Invalid_params + (Printf.sprintf "%s: `%s' must be %s" tool name expected)) + + let string_req tool args name = + match List.assoc_opt name args with + | Some (`String s) -> s + | Some _ -> bad tool name "a string" + | None -> + raise (Invalid_params + (Printf.sprintf "%s: missing required argument `%s'" tool name)) + + let bool_opt tool args name ~default = + match List.assoc_opt name args with + | None | Some `Null -> default + | Some (`Bool b) -> b + | Some _ -> bad tool name "a boolean" + + let int_opt tool args name = + match List.assoc_opt name args with + | None | Some `Null -> None + | Some (`Int i) -> Some i + | Some _ -> bad tool name "an integer" +end + +(* The [ec_focus] path is a string in the schema, so its shape is ours + to check: "next", or a dotted sequence of positive integers. *) +let focus_target (arg : string) = + if String.lowercase_ascii arg = "next" then `Next + else begin + let path = + try List.map int_of_string (String.split_on_char '.' arg) + with Failure _ -> + raise (Invalid_params + (Printf.sprintf "ec_focus: not a path of integers: %s" arg)) + in + if List.exists (fun k -> k < 1) path then + raise (Invalid_params + (Printf.sprintf "ec_focus: path indices must be >= 1: %s" arg)); + `Path path + end + +(* -------------------------------------------------------------------- *) +let run ~relocdir ~boot ~projini (mcpopts : EcOptions.mcp_option) = + if mcpopts.mcpo_help then begin + print_usage (); + exit 0 + end; + + (* stdout carries the protocol and nothing else. Rather than trust + every code path under the engine to stay silent, keep a private + descriptor for the protocol and point the process's stdout at + stderr, so a stray [print_string] anywhere lands in the client's + log instead of corrupting the message stream. *) + let wire = + let fd = Unix.dup Unix.stdout in + Unix.dup2 Unix.stderr Unix.stdout; + Unix.out_channel_of_descr fd + in + + let prvopts = mcpopts.mcpo_provers in + + let st = + try EcLlmCore.create ~relocdir ~boot ~projini ~prvopts + with EcLlmCore.Init_error msg -> + Printf.eprintf "%s\n%!" msg; + exit 1 + in + + (* ------------------------------------------------------------------ *) + (* The wire: one JSON value per line, flushed at once. Yojson escapes + newlines inside strings, so a message never contains one, as the + stdio transport requires. *) + let module Wire = struct + let send (msg : J.t) = + output_string wire (J.to_string msg); + output_char wire '\n'; + flush wire + + let result id (result : J.t) = + send (`Assoc [ + ("jsonrpc", `String "2.0"); + ("id", id); + ("result", result); + ]) + + let error ?data id code message = + send (`Assoc [ + ("jsonrpc", `String "2.0"); + ("id", id); + ("error", `Assoc ([ + ("code", `Int code); + ("message", `String message); + ] @ (match data with None -> [] | Some d -> [("data", d)]))); + ]) + end in + + (* ------------------------------------------------------------------ *) + (* Rendering [EcLlmCore] outcomes as tool results. *) + let module Result_of = struct + let content text = + `List [`Assoc [("type", `String "text"); ("text", `String text)]] + + (* [text] appears twice, once in each half of the result, and the + two copies are the same string by construction. Clients that read + [content] are served by the first; Claude Code, which drops + [content] as soon as [structuredContent] is present, is served + only by the second. *) + let make ~text ~uuid ~changed ~is_error ~extra = + `Assoc [ + ("content", content text); + ("structuredContent", + `Assoc ([("text", `String text); + ("uuid", `Int uuid); + ("changed", `Bool changed)] @ extra)); + ("isError", `Bool is_error); + ] + + (* The notice buffer holds whatever the engine said while the + operation ran; it precedes the body, as it does in the REPL. *) + let join notices body = + if notices = "" then body + else if body = "" then notices + else if String.length notices > 0 + && notices.[String.length notices - 1] = '\n' + then notices ^ body + else notices ^ "\n" ^ body + + let reply (r : EcLlmCore.reply) = + let body = + match r.EcLlmCore.body with + | EcLlmCore.Text body -> body + | EcLlmCore.Goals -> EcLlmCore.current_goals st + in + make + ~text:(join r.EcLlmCore.notices body) + ~uuid:r.EcLlmCore.uuid + ~changed:r.EcLlmCore.changed + ~is_error:false ~extra:[] + + (* A prover error is data, not a protocol failure: it comes back as + a successful response the agent can read and act on. *) + let failure ~extra (f : EcLlmCore.failure) = + let body = + if f.EcLlmCore.goals = "" then f.EcLlmCore.message + else f.EcLlmCore.message ^ "\n" ^ f.EcLlmCore.goals + in + make + ~text:(join f.EcLlmCore.notices body) + ~uuid:f.EcLlmCore.uuid + ~changed:f.EcLlmCore.changed + ~is_error:true ~extra:(extra f) + + let outcome ?(extra = fun _ -> []) = function + | Ok r -> reply r + | Error f -> failure ~extra f + end in + + (* ------------------------------------------------------------------ *) + (* Tool dispatch. + + Argument checking happens here, before the engine is touched: the + core trusts what it is handed (it does not test that a LOAD path + exists, for one), and a raw [int_of_string] message has no business + reaching an agent. Schema violations raise [Invalid_params] and + become JSON-RPC errors; checks a tool makes on its own behalf raise + [Tool_error] and become [isError] results. *) + + (* Set by a phrase that ends the session ([exit.]): the response still + goes out, then the process stops. *) + let quitting = ref false in + + let answer ?(extra = fun _ -> []) = function + | EcLlmCore.Quit -> + quitting := true; + Result_of.make ~text:"session terminated" + ~uuid:(EcLlmCore.uuid st) ~changed:false ~is_error:false ~extra:[] + | EcLlmCore.Done outcome -> + Result_of.outcome ~extra outcome + in + + let call_tool (name : string) (params : J.t option) : J.t = + let args = Args.arguments params in + let outcome = Result_of.outcome in + + match name with + | "ec_load" -> + let file = Args.string_req name args "file" in + let line = Args.int_opt name args "line" in + let col = Args.int_opt name args "col" in + let nosmt = Args.bool_opt name args "nosmt" ~default:false in + let trace = Args.bool_opt name args "trace" ~default:false in + if line = None && col <> None then + raise (Invalid_params "ec_load: `col' requires `line'"); + if not (Sys.file_exists file) then + raise (Tool_error + (Printf.sprintf "LOAD: no such file: %s" file)); + let upto = Option.map (fun line -> (line, col)) line in + outcome (EcLlmCore.load st ~file ~upto ~nosmt ~trace) + + | "ec_step" -> + answer (EcLlmCore.step st (Args.string_req name args "phrase")) + + | "ec_try" -> + answer + ~extra:(fun (f : EcLlmCore.failure) -> + [("reverted", `Bool f.EcLlmCore.reverted)]) + (EcLlmCore.try_step st (Args.string_req name args "phrase")) + + | "ec_goals" -> + outcome (EcLlmCore.goals st + ~all:(Args.bool_opt name args "all" ~default:false)) + + | "ec_tree" -> + outcome (EcLlmCore.tree st + ~all:(Args.bool_opt name args "full" ~default:false)) + + | "ec_focus" -> + outcome (EcLlmCore.focus st + (focus_target (Args.string_req name args "path"))) + + | "ec_undo" -> + outcome (EcLlmCore.undo st) + + | "ec_revert" -> + outcome (EcLlmCore.revert st (Args.string_req name args "target")) + + | "ec_checkpoint" -> + outcome (EcLlmCore.checkpoint st + ~name:(Args.string_req name args "name")) + + | "ec_commit" -> + outcome (EcLlmCore.commit st) + + | "ec_search" -> + answer (EcLlmCore.search st + ~pattern:(Args.string_req name args "pattern")) + + | _ -> + raise (Invalid_params (Printf.sprintf "unknown tool: %s" name)) + in + + (* ------------------------------------------------------------------ *) + (* Requests. *) + let initialize (params : J.t option) = + let requested = + match List.assoc_opt "protocolVersion" (Args.of_params params) with + | Some (`String v) -> Some v + | _ -> None + in + (* Spec: answer with the requested version when we speak it, + otherwise with the latest one we do speak. *) + let negotiated = + match requested with + | Some v when List.mem v protocol_supported -> v + | _ -> protocol_latest + in + `Assoc [ + ("protocolVersion", `String negotiated); + ("capabilities", `Assoc [("tools", `Assoc [])]); + ("serverInfo", `Assoc [ + ("name", `String server_name); + ("version", `String server_version); + ]); + ] + in + + let request id (meth : string) (params : J.t option) = + try + match meth with + | "initialize" -> + Wire.result id (initialize params) + | "ping" -> + Wire.result id (`Assoc []) + | "tools/list" -> + (* The tool set is static and short: no pagination, and a + [cursor] argument is simply ignored. *) + Wire.result id (`Assoc [("tools", `List tools)]) + | "tools/call" -> + let name = + match List.assoc_opt "name" (Args.of_params params) with + | Some (`String s) -> s + | Some _ -> raise (Invalid_params "`name' must be a string") + | None -> raise (Invalid_params "missing tool `name'") + in + let result = + try call_tool name params with + | Tool_error msg -> + Result_of.make ~text:msg ~uuid:(EcLlmCore.uuid st) + ~changed:false ~is_error:true ~extra:[] + in + Wire.result id result; + if !quitting then exit 0 + | _ -> + Wire.error id e_method_not_found + (Printf.sprintf "method not found: %s" meth) + with + | Invalid_params msg -> Wire.error id e_invalid_params msg + in + + (* Notifications never get a reply, whatever they are. The ones the + spec has us tolerate ([initialized], [cancelled], + [roots/list_changed]) are no-ops here, and so is anything else: + cancellation cannot preempt a synchronous tool call. *) + let notification (_ : string) (_ : J.t option) = () in + + (* ------------------------------------------------------------------ *) + let dispatch (msg : J.t) = + match msg with + | `List _ -> + (* Batching was removed from the protocol in revision 2025-06-18 + and has not come back. *) + Wire.error `Null e_invalid_request + "JSON-RPC batches are not supported by this protocol revision" + | `Assoc fields -> + let params = List.assoc_opt "params" fields in + let id = + (* A message is a request exactly when it carries a usable id; + MCP forbids a null id, so we read one as "no id" and stay + silent rather than answer a malformed request. *) + match List.assoc_opt "id" fields with + | None | Some `Null -> None + | Some id -> Some id + in + begin match List.assoc_opt "method" fields, id with + | Some (`String meth), Some id -> request id meth params + | Some (`String meth), None -> notification meth params + | Some _, Some id -> + Wire.error id e_invalid_request "`method' must be a string" + | Some _, None -> () + | None, Some id -> + Wire.error id e_invalid_request "missing `method'" + | None, None -> () + end + | _ -> + Wire.error `Null e_invalid_request + "a JSON-RPC message must be an object" + in + + (* ------------------------------------------------------------------ *) + (* Main loop. A blank line is not a message; skipping it keeps a + client's trailing newline from drawing a parse error. *) + begin try while true do + let line = input_line stdin in + if String.trim line <> "" then + match J.from_string line with + | exception _ -> + Wire.error `Null e_parse_error "invalid JSON" + | msg -> dispatch msg + done with End_of_file -> () end; + + exit 0 diff --git a/src/ecMcp.mli b/src/ecMcp.mli new file mode 100644 index 000000000..b8eeb3ac0 --- /dev/null +++ b/src/ecMcp.mli @@ -0,0 +1,14 @@ +(* -------------------------------------------------------------------- *) +(* Model Context Protocol server over stdio: a second front-end, next to + the [easycrypt llm] REPL, over the shared engine core in + [EcLlmCore]. Driven via the [easycrypt mcp] command. *) + +(* Serve JSON-RPC 2.0 messages on stdin/stdout until end of input, then + exit the process. Never returns. [projini] resolves the + [easycrypt.project] context of a file path, as for the REPL. *) +val run : + relocdir:string option + -> boot:bool + -> projini:(string option -> EcOptions.ini_context option) + -> EcOptions.mcp_option + -> 'a diff --git a/src/ecOptions.ml b/src/ecOptions.ml index a78822aaf..82e4d2dd9 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -11,6 +11,7 @@ type command = [ | `Why3Config | `DocGen of doc_option | `Llm of llm_option + | `Mcp of mcp_option ] and options = { @@ -49,10 +50,14 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; + llmo_eval : string option; +} + +and mcp_option = { + mcpo_provers : prv_options; + mcpo_help : bool; } and prv_options = { @@ -69,8 +74,9 @@ and prv_options = { } and ldr_options = { - ldro_idirs : (string option * string * bool) list; - ldro_boot : bool; + ldro_idirs : (string option * string * bool) list; + ldro_boot : bool; + ldro_stdlib : string list; } and glb_options = { @@ -381,11 +387,16 @@ let specs = { `Spec ("trace" , `Flag , "Save all goals & messages in .eco"); `Spec ("compact", `Int , "")]); - ("llm", "LLM-friendly batch compilation", [ + ("llm", "LLM-friendly interactive mode", [ + `Group "loader"; + `Group "provers"; + `Spec ("help", `Flag , "Print the LLM agent guide and exit"); + `Spec ("eval", `String, "Run the given commands (newline-separated) and exit, in lieu of reading stdin")]); + + ("mcp", "Model Context Protocol server (stdio)", [ `Group "loader"; `Group "provers"; - `Spec ("lastgoals" , `Flag , "Print last unproved goals on failure"); - `Spec ("upto" , `String, "Compile up to LINE or LINE:COL and print goals")]); + `Spec ("help", `Flag , "Print the MCP server usage and exit")]); ("cli", "Run EasyCrypt top-level", [ `Group "loader"; @@ -424,9 +435,10 @@ let specs = { ]); ("loader", "Options related to loader", [ - `Spec ("I" , `String, "Add to the list of include directories"); - `Spec ("R" , `String, "Recursively add to the list of include directories"); - `Spec ("boot", `Flag , "Don't load prelude")]) + `Spec ("I" , `String, "Add to the list of include directories"); + `Spec ("R" , `String, "Recursively add to the list of include directories"); + `Spec ("stdlib", `String, "Use as a standard-library root (System namespace, prelude + recursive), replacing the built-in one; repeatable"); + `Spec ("boot" , `Flag , "Don't load prelude")]) ] } @@ -486,8 +498,9 @@ let dirs_of_env = (* -------------------------------------------------------------------- *) let ldr_options_of_values ~env ?(ini = []) values = + let stdlib = get_strings "stdlib" values in if get_flag "boot" values then - { ldro_idirs = []; ldro_boot = true; } + { ldro_idirs = []; ldro_boot = true; ldro_stdlib = stdlib; } else let add_rec (fl : bool) ((nm, x) : string option * string) = (nm, x, fl) in @@ -501,8 +514,9 @@ let ldr_options_of_values ~env ?(ini = []) values = let rdirs = List.map (add_rec true) rdirs in let idirs_R = List.map (add_rec true) (List.map parse_idir (get_strings "R" values)) in - { ldro_idirs = idirs @ idirs_I @ rdirs @ idirs_R; - ldro_boot = false; } + { ldro_idirs = idirs @ idirs_I @ rdirs @ idirs_R; + ldro_boot = false; + ldro_stdlib = stdlib; } let glb_options_of_values ~env ini values = let why3 = @@ -548,6 +562,47 @@ let prv_options_of_values ini values = prvo_why3server = get_string "why3server" values; } +(* -------------------------------------------------------------------- *) +(* Overlay project INI settings (an [easycrypt.project] discovered when + a file is loaded at run time, e.g. by the LLM REPL's [LOAD]) on top + of already-parsed prover options. Mirrors the precedence used by + [prv_options_of_values] when the project file is known at + option-parsing time: project provers/pragmas extend the parsed + lists, project scalars take over the parsed values. *) +let prv_options_with_ini (ini : ini_context list) (prv : prv_options) = + let provers = + match Ini.get_all_provers ini with + | [] -> prv.prvo_provers + | ps -> + let old = odfl [] prv.prvo_provers in + Some (ps @ List.filter (fun p -> not (List.mem p ps)) old) + in + { prv with + prvo_provers = provers; + prvo_timeout = begin + match Ini.get_all_timeout ini with + | None -> prv.prvo_timeout + | Some _ as i -> i + end; + prvo_quorum = begin + match Ini.get_all_quorum ini with + | None -> prv.prvo_quorum + | Some _ as i -> i + end; + prvo_ppwidth = begin + match Ini.get_all_ppwidth ini with + | None -> prv.prvo_ppwidth + | Some _ as i -> i + end; + prvo_pragmas = Ini.get_all_pragmas ini @ prv.prvo_pragmas; } + +(* The load path contributed by INI contexts, in the shape and order of + [ldro_idirs]: plain include dirs first, then recursive ones. *) +let ini_loadpath (ini : ini_context list) = + List.map (fun (nm, dir) -> (nm, dir, false)) (Ini.get_all_idirs ini) + @ List.map (fun (nm, dir) -> (nm, dir, true)) (Ini.get_all_rdirs ini) + +(* -------------------------------------------------------------------- *) let cli_options_of_values ini values = { clio_emacs = get_flag "emacs" values; clio_provers = prv_options_of_values ini values; } @@ -574,26 +629,14 @@ let doc_options_of_values values input = { doco_input = input; doco_outdirp = get_string "outdir" values; } -let parse_upto values = - get_string "upto" values |> Option.map (fun s -> - let invalid () = - raise (Arg.Bad (Printf.sprintf - "invalid -upto format: expected LINE or LINE:COL, got %S" s)) in - match String.split_on_char ':' s with - | [line] -> - let line = try int_of_string line with Failure _ -> invalid () in - (line, None) - | [line; col] -> - let line = try int_of_string line with Failure _ -> invalid () in - let col = try int_of_string col with Failure _ -> invalid () in - (line, Some col) - | _ -> invalid ()) - -let llm_options_of_values ini values input = - { llmo_input = input; - llmo_provers = prv_options_of_values ini values; - llmo_lastgoals = get_flag "lastgoals" values; - llmo_upto = parse_upto values; } +let llm_options_of_values ini values = + { llmo_provers = prv_options_of_values ini values; + llmo_help = get_flag "help" values; + llmo_eval = get_string "eval" values; } + +let mcp_options_of_values ini values = + { mcpo_provers = prv_options_of_values ini values; + mcpo_help = get_flag "help" values; } (* -------------------------------------------------------------------- *) let parse getini argv = @@ -666,16 +709,23 @@ let parse getini argv = raise (Arg.Bad "this command takes a single input file as argument") end - | "llm" -> begin - match anons with - | [input] -> - let ini = getini (Some input) in - let cmd = `Llm (llm_options_of_values ini values input) in - (cmd, ini, true) + | "llm" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); - | _ -> - raise (Arg.Bad "this command takes a single argument") - end + let ini = getini None in + let cmd = `Llm (llm_options_of_values ini values) in + + (cmd, ini, true) + + | "mcp" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); + + let ini = getini None in + let cmd = `Mcp (mcp_options_of_values ini values) in + + (cmd, ini, true) | _ -> assert false diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 0fb1fc3c2..2c10f3a1d 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -7,6 +7,7 @@ type command = [ | `Why3Config | `DocGen of doc_option | `Llm of llm_option + | `Mcp of mcp_option ] and options = { @@ -45,10 +46,14 @@ and doc_option = { } and llm_option = { - llmo_input : string; llmo_provers : prv_options; - llmo_lastgoals : bool; - llmo_upto : (int * int option) option; + llmo_help : bool; + llmo_eval : string option; +} + +and mcp_option = { + mcpo_provers : prv_options; + mcpo_help : bool; } and prv_options = { @@ -65,8 +70,12 @@ and prv_options = { } and ldr_options = { - ldro_idirs : (string option * string * bool) list; - ldro_boot : bool; + ldro_idirs : (string option * string * bool) list; + ldro_boot : bool; + ldro_stdlib : string list; + (* When non-empty, these directories replace the built-in + [Sites.theories] for prelude and recursive-System namespace + loading. Empty means "use the built-in stdlib". *) } and glb_options = { @@ -99,6 +108,16 @@ exception InvalidIniFile of (int * string) val read_ini_file : string -> ini_options +(* -------------------------------------------------------------------- *) +(* Overlay project INI settings discovered at run time (e.g. by the LLM + REPL's [LOAD]) on top of already-parsed prover options, mirroring + the precedence of option parsing with a known project file. *) +val prv_options_with_ini : ini_context list -> prv_options -> prv_options + +(* The load path contributed by INI contexts, in [ldro_idirs] shape: + (namespace, dir, recursive). *) +val ini_loadpath : ini_context list -> (string option * string * bool) list + val parse_cmdline : ?ini:(string option -> ini_context list) -> string array diff --git a/src/ecScope.ml b/src/ecScope.ml index 8f0e27f87..960d48fbd 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -489,6 +489,10 @@ let goal (scope : scope) = let xgoal (scope : scope) = scope.sc_pr_uc +(* -------------------------------------------------------------------- *) +let set_xgoal (scope : scope) (puc : proof_uc) = + { scope with sc_pr_uc = Some puc } + (* -------------------------------------------------------------------- *) let dump_why3 (scope : scope) (filename : string) = try EcSmt.dump_why3 (env scope) filename diff --git a/src/ecScope.mli b/src/ecScope.mli index d73ed66d7..5aeae3e3b 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -87,6 +87,7 @@ val env : scope -> EcEnv.env val attop : scope -> bool val goal : scope -> proof_auc option val xgoal : scope -> proof_uc option +val set_xgoal : scope -> proof_uc -> scope (* Creates a scope that is identical to the supplied one except * that the environment and required theories are reset to the ones diff --git a/tests/llm/README.md b/tests/llm/README.md new file mode 100644 index 000000000..a21a91641 --- /dev/null +++ b/tests/llm/README.md @@ -0,0 +1,88 @@ +# `easycrypt llm` golden-output tests + +Byte-identity regression harness for the LLM REPL (`src/ecLlm.ml`). +Each scenario is a small script of REPL commands fed to +`ec.exe llm -eval`; its raw stdout and its process exit status are +compared against recorded goldens. + +## Layout + +| Path | Contents | +|------|----------| +| `fixtures/*` | tiny EasyCrypt files the scripts `LOAD` (plus one non-`.ec` file, for the unknown-extension error) | +| `scripts/*.script` | the newline-separated commands passed to `-eval` | +| `expected/*.out` | recorded stdout, one file per script | +| `../../scripts/testing/llm-golden` | the runner | + +## Running + +From the repository root: + +``` +make test-llm # build + run every scenario +scripts/testing/llm-golden # run every scenario +scripts/testing/llm-golden tree-nested commit-nested +scripts/testing/llm-golden --bin /path/to/ec.exe +``` + +The runner defaults to `_build/default/src/ec.exe`, resolved relative +to the repository root. It prints `PASS`/`FAIL` per scenario, a unified +diff for each mismatch, and exits nonzero if anything failed. That is +the CI invocation. + +## Re-recording + +``` +scripts/testing/llm-golden --record # all scenarios +scripts/testing/llm-golden --record load-goals # one scenario +``` + +`--record` overwrites `expected/*.out` with the current binary's +output instead of diffing. It still checks the declared exit status +and reports a mismatch, so a stale `# exit:` line cannot go unnoticed. + +Re-record only deliberately: these goldens are the gate for refactors +of `src/ecLlm.ml`, and every diff must be reviewed by hand. + +## Expected exit status + +Each `.script` declares its expected process exit status on its first +line: + +``` +# exit: 1 +``` + +Lines starting with `#` are comment lines: the runner strips **all** of +them before handing the script to `-eval`, so they can also be used for +prose. The first `# exit: N` line wins; a script without one fails. + +`ec.exe llm -eval` exits 1 if any command produced an `ERROR` reply and +0 otherwise, so scenarios that deliberately exercise error paths +declare `# exit: 1`. + +## Determinism rules + +The goldens are compared byte for byte, so scenarios must not leak +anything machine- or environment-dependent: + +* **Relative paths only.** The runner `cd`s into `tests/llm` before + invoking the binary, and scripts must refer to fixtures as + `LOAD "fixtures/foo.ec"`. `LOAD` echoes the filename verbatim in its + `[loaded:...]` reply tag, so an absolute path would bake the + developer's home directory into the golden. +* **No SMT.** Fixtures and scripts must never use `smt()`, `smt(...)` + or `/#`. Proofs close with `trivial`, `done`, `reflexivity` or + `split`. SMT would make the goldens depend on which provers are + installed, and on their timing. +* **stdout only.** stderr is discarded; only stdout is compared. +* **No `HELP`.** `HELP` echoes `doc/llm/CLAUDE.md`, which would make + every documentation edit a test failure. +* Fixtures require `AllCore` only. + +## Adding a scenario + +1. Add `scripts/NAME.script` starting with `# exit: N`. +2. Add any new fixture under `fixtures/`. +3. `scripts/testing/llm-golden --record NAME`. +4. Read `expected/NAME.out` and check it is what you meant to freeze. diff --git a/tests/llm/expected/commit-after-qed.out b/tests/llm/expected/commit-after-qed.out new file mode 100644 index 000000000..c55cefa12 --- /dev/null +++ b/tests/llm/expected/commit-after-qed.out @@ -0,0 +1,29 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] + +OK [uuid:6] + +OK [uuid:7] +added lemma: `simple_and' + +OK [uuid:7] + +OK [uuid:7] +split. +- trivial. +- trivial. +qed. + diff --git a/tests/llm/expected/commit-load-continuation.out b/tests/llm/expected/commit-load-continuation.out new file mode 100644 index 000000000..d90f6bebd --- /dev/null +++ b/tests/llm/expected/commit-load-continuation.out @@ -0,0 +1,25 @@ +READY [uuid:0] + +OK [uuid:4] [loaded:fixtures/midproof.ec:8] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] + +OK [uuid:5] + +OK [uuid:6] + +OK [uuid:6] + +OK [uuid:6] +No more goals + +OK [uuid:6] +- trivial. +- trivial. + diff --git a/tests/llm/expected/commit-nested.out b/tests/llm/expected/commit-nested.out new file mode 100644 index 000000000..0b8a2fa93 --- /dev/null +++ b/tests/llm/expected/commit-nested.out @@ -0,0 +1,37 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/nested.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +((1 = 1 /\ 2 = 2) /\ 3 = 3) /\ 4 = 4 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] [focus: 1/3] + +OK [uuid:6] [focus: 1/4] + +OK [uuid:7] [focus: 1/3] + +OK [uuid:8] [focus: 1/2] + +OK [uuid:9] + +OK [uuid:10] + +OK [uuid:10] + +OK [uuid:10] +split. +- split. + + split. + * trivial. + * trivial. + + trivial. +- trivial. + diff --git a/tests/llm/expected/commit-simple.out b/tests/llm/expected/commit-simple.out new file mode 100644 index 000000000..3a1e13b34 --- /dev/null +++ b/tests/llm/expected/commit-simple.out @@ -0,0 +1,25 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] + +OK [uuid:6] + +OK [uuid:6] + +OK [uuid:6] +split. +- trivial. +- trivial. + diff --git a/tests/llm/expected/commit-strict-bullets.out b/tests/llm/expected/commit-strict-bullets.out new file mode 100644 index 000000000..f844bb224 --- /dev/null +++ b/tests/llm/expected/commit-strict-bullets.out @@ -0,0 +1,25 @@ +READY [uuid:0] + +OK [uuid:6] [loaded:fixtures/strict.ec:11] [focus: 1/3] +Current goal (remaining: 3) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:6] + +OK [uuid:7] [focus: 1/2] + +OK [uuid:8] + +OK [uuid:9] + +OK [uuid:9] + +OK [uuid:9] + + trivial. + + trivial. +- trivial. + diff --git a/tests/llm/expected/commit-strict-nested.out b/tests/llm/expected/commit-strict-nested.out new file mode 100644 index 000000000..2a5a8c31f --- /dev/null +++ b/tests/llm/expected/commit-strict-nested.out @@ -0,0 +1,28 @@ +READY [uuid:0] + +OK [uuid:7] [loaded:fixtures/strictnested.ec:13] [focus: 1/4] +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:7] + +OK [uuid:8] [focus: 1/3] + +OK [uuid:9] [focus: 1/2] + +OK [uuid:10] + +OK [uuid:11] + +OK [uuid:11] + +OK [uuid:11] + * trivial. + * trivial. + + trivial. +- trivial. + diff --git a/tests/llm/expected/error-exit.out b/tests/llm/expected/error-exit.out new file mode 100644 index 000000000..8346241ef --- /dev/null +++ b/tests/llm/expected/error-exit.out @@ -0,0 +1,6 @@ +READY [uuid:0] + +ERROR [uuid:0] +nothing to undo +No active proof. + diff --git a/tests/llm/expected/focus-nav.out b/tests/llm/expected/focus-nav.out new file mode 100644 index 000000000..c7829c4bd --- /dev/null +++ b/tests/llm/expected/focus-nav.out @@ -0,0 +1,84 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/nested.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +((1 = 1 /\ 2 = 2) /\ 3 = 3) /\ 4 = 4 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] [focus: 1/3] + +OK [uuid:6] [focus: 1/4] + +OK [uuid:6] + +OK [uuid:6] [focus: 1/4] + [1.1.1] 1 = 1 <- focused + [1.1.2] 2 = 2 + [1.2] 3 = 3 +[2] 4 = 4 + +OK [uuid:7] [focus: 1/4] +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +ERROR [uuid:7] +FOCUS: path must select a leaf goal, not a frame +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +ERROR [uuid:7] +FOCUS: index 9 out of range (1..2) +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +ERROR [uuid:7] +FOCUS: not a path of integers: foo +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +ERROR [uuid:7] +FOCUS: missing argument +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +OK [uuid:8] [focus: 1/4] +Current goal (remaining: 4) + +Type variables: + +------------------------------------------------------------------------ +4 = 4 + +OK [uuid:8] [focus: 1/4] +[1] 4 = 4 <- focused + [2.1.1] 1 = 1 + [2.1.2] 2 = 2 + [2.2] 3 = 3 + diff --git a/tests/llm/expected/load-errors.out b/tests/llm/expected/load-errors.out new file mode 100644 index 000000000..7628f4c9e --- /dev/null +++ b/tests/llm/expected/load-errors.out @@ -0,0 +1,18 @@ +READY [uuid:0] + +ERROR [uuid:0] +LOAD: missing filename +No active proof. + +ERROR [uuid:0] +LOAD: no such file: fixtures/nosuch.ec +No active proof. + +ERROR [uuid:0] +unknown file extension: .txt +No active proof. + +ERROR [uuid:0] +LOAD: unexpected arguments +No active proof. + diff --git a/tests/llm/expected/load-goals.out b/tests/llm/expected/load-goals.out new file mode 100644 index 000000000..b48f2bebd --- /dev/null +++ b/tests/llm/expected/load-goals.out @@ -0,0 +1,48 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + + + + Goal #2 + ------------------------------------------------------------------------ + 2 = 2 + diff --git a/tests/llm/expected/load-nosmt.out b/tests/llm/expected/load-nosmt.out new file mode 100644 index 000000000..e08378e82 --- /dev/null +++ b/tests/llm/expected/load-nosmt.out @@ -0,0 +1,18 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + diff --git a/tests/llm/expected/load-trace-notinproof.out b/tests/llm/expected/load-trace-notinproof.out new file mode 100644 index 000000000..345e3ab82 --- /dev/null +++ b/tests/llm/expected/load-trace-notinproof.out @@ -0,0 +1,25 @@ +READY [uuid:0] + +ERROR [uuid:1] +trace: target sentence is not in a proof context +No active proof. + +OK [uuid:1] +No active proof. + +OK [uuid:2] +Current goal + +Type variables: + +------------------------------------------------------------------------ +b2i true = 1 + +OK [uuid:2] +Current goal + +Type variables: + +------------------------------------------------------------------------ +b2i true = 1 + diff --git a/tests/llm/expected/load-trace.out b/tests/llm/expected/load-trace.out new file mode 100644 index 000000000..b424004d7 --- /dev/null +++ b/tests/llm/expected/load-trace.out @@ -0,0 +1,30 @@ +READY [uuid:0] + +OK [uuid:4] [loaded:fixtures/midproof.ec:8] [focus: 1/2] +=== BEFORE: line 8 (col 0) === +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +=== TACTIC (lines 8:0 - 8:6) === +split. + +=== AFTER: line 8 (col 0) === +Type variables: + +------------------------------------------------------------------------ +1 = 1 + + +Type variables: + +------------------------------------------------------------------------ +2 = 2 + + +=== SUMMARY === +open goals: 1 -> 2 + diff --git a/tests/llm/expected/multi-sentence-error.out b/tests/llm/expected/multi-sentence-error.out new file mode 100644 index 000000000..2bd1cf2bf --- /dev/null +++ b/tests/llm/expected/multi-sentence-error.out @@ -0,0 +1,27 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:4] +: line 1 (7-25): unknown lemma `nosuchlemma' +source: apply nosuchlemma. +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] [focus: 1/2] +[1] 1 = 1 <- focused +[2] 2 = 2 + +OK [uuid:4] [focus: 1/2] +split. + diff --git a/tests/llm/expected/multi-sentence.out b/tests/llm/expected/multi-sentence.out new file mode 100644 index 000000000..46f132906 --- /dev/null +++ b/tests/llm/expected/multi-sentence.out @@ -0,0 +1,21 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:6] +No more goals + +OK [uuid:6] +No more goals + +OK [uuid:6] +split. +- trivial. +- trivial. + diff --git a/tests/llm/expected/multiline.out b/tests/llm/expected/multiline.out new file mode 100644 index 000000000..73772ea35 --- /dev/null +++ b/tests/llm/expected/multiline.out @@ -0,0 +1,37 @@ +READY [uuid:0] + +OK [uuid:1] [loaded:fixtures/simple.ec:3] +No active proof. + +OK [uuid:2] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:2] + +OK [uuid:3] [focus: 1/2] + +OK [uuid:4] + +OK [uuid:5] + +OK [uuid:5] + +OK [uuid:5] +No more goals + +OK [uuid:6] +added lemma: `multi' +No active proof. + +OK [uuid:6] +lemma multi : 1 = 1 /\ 2 = 2. +split. +- trivial. +- trivial. +qed. + diff --git a/tests/llm/expected/quiet.out b/tests/llm/expected/quiet.out new file mode 100644 index 000000000..6d7186947 --- /dev/null +++ b/tests/llm/expected/quiet.out @@ -0,0 +1,26 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] + +OK [uuid:5] + +OK [uuid:5] +Current goal + +Type variables: + +------------------------------------------------------------------------ +2 = 2 + diff --git a/tests/llm/expected/search-in-proof.out b/tests/llm/expected/search-in-proof.out new file mode 100644 index 000000000..e2d3a9984 --- /dev/null +++ b/tests/llm/expected/search-in-proof.out @@ -0,0 +1,40 @@ +READY [uuid:0] + +OK [uuid:4] [loaded:fixtures/midproof.ec:8] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:4] + +OK [uuid:5] + +OK [uuid:5] +(* RField.signr_odd *) +lemma signr_odd: + forall (n : int), 0 <= n => (- 1%r) ^ b2i (odd n) = (- 1%r) ^ n. +lemma b2rE: forall (b : bool), b2r b = (b2i b)%r. +lemma le_b2i: forall (b1 b2 : bool), (b1 => b2) <=> b2i b1 <= b2i b2. +lemma b2i_or: + forall (b1 b2 : bool), b2i (b1 \/ b2) = b2i b1 + b2i b2 - b2i b1 * b2i b2. +lemma b2i_le1: forall (b : bool), b2i b <= 1. +lemma b2i_ge0: forall (b : bool), 0 <= b2i b. +lemma b2i_eq1: forall (b : bool), b2i b = 1 <=> b. +lemma b2i_eq0: forall (b : bool), b2i b = 0 <=> !b. +lemma b2i_and: forall (b1 b2 : bool), b2i (b1 /\ b2) = b2i b1 * b2i b2. +lemma b2i1: b2i true = 1. +lemma b2i0: b2i false = 0. +lemma signr_odd: forall (n : int), 0 <= n => (-1) ^ b2i (odd n) = (-1) ^ n. + + +OK [uuid:6] + +OK [uuid:6] + +OK [uuid:6] +- trivial. +- trivial. + diff --git a/tests/llm/expected/search.out b/tests/llm/expected/search.out new file mode 100644 index 000000000..055e55810 --- /dev/null +++ b/tests/llm/expected/search.out @@ -0,0 +1,43 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] +(* RField.signr_odd *) +lemma signr_odd: + forall (n : int), 0 <= n => (- 1%r) ^ b2i (odd n) = (- 1%r) ^ n. +lemma b2rE: forall (b : bool), b2r b = (b2i b)%r. +lemma le_b2i: forall (b1 b2 : bool), (b1 => b2) <=> b2i b1 <= b2i b2. +lemma b2i_or: + forall (b1 b2 : bool), b2i (b1 \/ b2) = b2i b1 + b2i b2 - b2i b1 * b2i b2. +lemma b2i_le1: forall (b : bool), b2i b <= 1. +lemma b2i_ge0: forall (b : bool), 0 <= b2i b. +lemma b2i_eq1: forall (b : bool), b2i b = 1 <=> b. +lemma b2i_eq0: forall (b : bool), b2i b = 0 <=> !b. +lemma b2i_and: forall (b1 b2 : bool), b2i (b1 /\ b2) = b2i b1 * b2i b2. +lemma b2i1: b2i true = 1. +lemma b2i0: b2i false = 0. +lemma signr_odd: forall (n : int), 0 <= n => (-1) ^ b2i (odd n) = (-1) ^ n. + +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:3] +SEARCH: missing query +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + diff --git a/tests/llm/expected/tree-nested.out b/tests/llm/expected/tree-nested.out new file mode 100644 index 000000000..d8936191a --- /dev/null +++ b/tests/llm/expected/tree-nested.out @@ -0,0 +1,52 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/nested.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +((1 = 1 /\ 2 = 2) /\ 3 = 3) /\ 4 = 4 + +OK [uuid:3] + +OK [uuid:4] [focus: 1/2] + +OK [uuid:5] [focus: 1/3] + +OK [uuid:6] [focus: 1/4] + +OK [uuid:6] + +OK [uuid:6] [focus: 1/4] + [1.1.1] 1 = 1 <- focused + [1.1.2] 2 = 2 + [1.2] 3 = 3 +[2] 4 = 4 + +OK [uuid:6] [focus: 1/4] + [1.1.1] <- focused +Type variables: + +------------------------------------------------------------------------ +1 = 1 + + [1.1.2] +Type variables: + +------------------------------------------------------------------------ +2 = 2 + + [1.2] +Type variables: + +------------------------------------------------------------------------ +3 = 3 + +[2] +Type variables: + +------------------------------------------------------------------------ +4 = 4 + + diff --git a/tests/llm/expected/undo-revert.out b/tests/llm/expected/undo-revert.out new file mode 100644 index 000000000..e00e426a8 --- /dev/null +++ b/tests/llm/expected/undo-revert.out @@ -0,0 +1,105 @@ +READY [uuid:0] + +OK [uuid:3] [loaded:fixtures/simple.ec:6] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] +checkpoint 'start' set at uuid 3 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:5] +Current goal + +Type variables: + +------------------------------------------------------------------------ +2 = 2 + +OK [uuid:4] [focus: 1/2] +Current goal (remaining: 2) + +Type variables: + +------------------------------------------------------------------------ +1 = 1 + +OK [uuid:3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:3] +CHECKPOINT: missing name +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:3] +REVERT: missing uuid or checkpoint name +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +OK [uuid:3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:3] +REVERT: 'nosuch' is not a valid uuid or checkpoint name +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + +ERROR [uuid:3] +REVERT: uuid 999 out of range [0, 3] +Current goal + +Type variables: + +------------------------------------------------------------------------ +1 = 1 /\ 2 = 2 + diff --git a/tests/llm/fixtures/midproof.ec b/tests/llm/fixtures/midproof.ec new file mode 100644 index 000000000..6b2bad195 --- /dev/null +++ b/tests/llm/fixtures/midproof.ec @@ -0,0 +1,8 @@ +(* Deliberately truncated: the file ends inside the proof, so a bare + `LOAD "fixtures/midproof.ec"` lands mid-proof with two open goals. + Used for the LOAD-continuation and -trace scenarios. *) +require import AllCore. + +lemma cont_and : 1 = 1 /\ 2 = 2. +proof. +split. diff --git a/tests/llm/fixtures/nested.ec b/tests/llm/fixtures/nested.ec new file mode 100644 index 000000000..b30ba0234 --- /dev/null +++ b/tests/llm/fixtures/nested.ec @@ -0,0 +1,14 @@ +(* Nested conjunction: `split. split. split.` from the state at line 6 + opens four goals nested as [1.1.1] [1.1.2] [1.2] [2]. *) +require import AllCore. + +lemma nested_and : ((1 = 1 /\ 2 = 2) /\ 3 = 3) /\ 4 = 4. +proof. +split. +split. +split. +trivial. +trivial. +trivial. +trivial. +qed. diff --git a/tests/llm/fixtures/notec.txt b/tests/llm/fixtures/notec.txt new file mode 100644 index 000000000..a3de7e3c6 --- /dev/null +++ b/tests/llm/fixtures/notec.txt @@ -0,0 +1,2 @@ +This file exists but is not an EasyCrypt source: LOAD must reject it +with the unknown-extension error, not with the missing-file error. diff --git a/tests/llm/fixtures/simple.ec b/tests/llm/fixtures/simple.ec new file mode 100644 index 000000000..ceb2d9c37 --- /dev/null +++ b/tests/llm/fixtures/simple.ec @@ -0,0 +1,10 @@ +(* Simple conjunction: LOAD stops on line 5 (the `proof.`), leaving one + open goal `1 = 1 /\ 2 = 2`. *) +require import AllCore. + +lemma simple_and : 1 = 1 /\ 2 = 2. +proof. +split. +trivial. +trivial. +qed. diff --git a/tests/llm/fixtures/strict.ec b/tests/llm/fixtures/strict.ec new file mode 100644 index 000000000..6d0948646 --- /dev/null +++ b/tests/llm/fixtures/strict.ec @@ -0,0 +1,11 @@ +(* Deliberately truncated, under +strict_bullets: the LOAD prefix leaves + the bullet stack holding `-`, so COMMIT must pick a different token + for the bullets it emits. *) +pragma +strict_bullets. + +require import AllCore. + +lemma strict_and : (1 = 1 /\ 2 = 2) /\ 3 = 3. +proof. +split. +- split. diff --git a/tests/llm/fixtures/strictnested.ec b/tests/llm/fixtures/strictnested.ec new file mode 100644 index 000000000..3dccf4d83 --- /dev/null +++ b/tests/llm/fixtures/strictnested.ec @@ -0,0 +1,13 @@ +(* Deliberately truncated, under +strict_bullets: the LOAD prefix leaves + two frames on the bullet stack (`-` outermost, `+` inside it) and + four open goals. COMMIT must address the goals still owned by those + frames with the frames' own tokens, and open one fresh level. *) +pragma +strict_bullets. + +require import AllCore. + +lemma strict_nested : ((1 = 1 /\ 2 = 2) /\ 3 = 3) /\ 4 = 4. +proof. +split. +- split. + + split. diff --git a/tests/llm/scripts/commit-after-qed.script b/tests/llm/scripts/commit-after-qed.script new file mode 100644 index 000000000..48e5c1493 --- /dev/null +++ b/tests/llm/scripts/commit-after-qed.script @@ -0,0 +1,13 @@ +# exit: 0 +# COMMIT run after `qed.`: the active proof is gone, but COMMIT queries +# the proofenv snapshot taken at the last recorded phrase, so the body +# still carries bullets. `qed.` itself stays flat (no goal was open +# right before it, hence no parent handle). +LOAD "fixtures/simple.ec" 6 +QUIET ON +split. +trivial. +trivial. +qed. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/commit-load-continuation.script b/tests/llm/scripts/commit-load-continuation.script new file mode 100644 index 000000000..fcd9a3c1b --- /dev/null +++ b/tests/llm/scripts/commit-load-continuation.script @@ -0,0 +1,9 @@ +# exit: 0 +# LOAD a file that ends mid-proof, continue it at the REPL, COMMIT. +LOAD "fixtures/midproof.ec" +QUIET ON +trivial. +trivial. +QUIET OFF +GOALS +COMMIT diff --git a/tests/llm/scripts/commit-nested.script b/tests/llm/scripts/commit-nested.script new file mode 100644 index 000000000..175da21f8 --- /dev/null +++ b/tests/llm/scripts/commit-nested.script @@ -0,0 +1,13 @@ +# exit: 0 +# COMMIT after nested splits: bullets nest as - / + / *. +LOAD "fixtures/nested.ec" 6 +QUIET ON +split. +split. +split. +trivial. +trivial. +trivial. +trivial. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/commit-simple.script b/tests/llm/scripts/commit-simple.script new file mode 100644 index 000000000..7dd1fead9 --- /dev/null +++ b/tests/llm/scripts/commit-simple.script @@ -0,0 +1,9 @@ +# exit: 0 +# COMMIT after a plain split + two trivials. +LOAD "fixtures/simple.ec" 6 +QUIET ON +split. +trivial. +trivial. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/commit-strict-bullets.script b/tests/llm/scripts/commit-strict-bullets.script new file mode 100644 index 000000000..8912983aa --- /dev/null +++ b/tests/llm/scripts/commit-strict-bullets.script @@ -0,0 +1,11 @@ +# exit: 0 +# The LOAD prefix of fixtures/strict.ec ends under `pragma +# +strict_bullets` with `-` on the bullet stack, so COMMIT must pick a +# token other than `-`. +LOAD "fixtures/strict.ec" +QUIET ON +trivial. +trivial. +trivial. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/commit-strict-nested.script b/tests/llm/scripts/commit-strict-nested.script new file mode 100644 index 000000000..c1fd92099 --- /dev/null +++ b/tests/llm/scripts/commit-strict-nested.script @@ -0,0 +1,13 @@ +# exit: 0 +# The LOAD prefix of fixtures/strictnested.ec stops under two open +# bullet frames (`-` then `+`) with four goals open. COMMIT must reuse +# `-` for the outer frame's next sibling, `+` for the inner frame's, +# and pick `*` fresh for the level the prefix never opened. +LOAD "fixtures/strictnested.ec" +QUIET ON +trivial. +trivial. +trivial. +trivial. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/error-exit.script b/tests/llm/scripts/error-exit.script new file mode 100644 index 000000000..01bb443d2 --- /dev/null +++ b/tests/llm/scripts/error-exit.script @@ -0,0 +1,3 @@ +# exit: 1 +# A script whose only command errors: the process must exit 1. +UNDO diff --git a/tests/llm/scripts/focus-nav.script b/tests/llm/scripts/focus-nav.script new file mode 100644 index 000000000..54963c73e --- /dev/null +++ b/tests/llm/scripts/focus-nav.script @@ -0,0 +1,17 @@ +# exit: 1 +# FOCUS with a dotted path, on a frame (error), out of range (error), +# with a non-integer path (parse error), then NEXT. +LOAD "fixtures/nested.ec" 6 +QUIET ON +split. +split. +split. +QUIET OFF +TREE +FOCUS 1.2 +FOCUS 1 +FOCUS 9 +FOCUS foo +FOCUS +NEXT +TREE diff --git a/tests/llm/scripts/load-errors.script b/tests/llm/scripts/load-errors.script new file mode 100644 index 000000000..66338b489 --- /dev/null +++ b/tests/llm/scripts/load-errors.script @@ -0,0 +1,7 @@ +# exit: 1 +# LOAD argument errors: missing filename, missing file, an existing +# file with an unknown extension, trailing junk. +LOAD +LOAD "fixtures/nosuch.ec" +LOAD "fixtures/notec.txt" +LOAD "fixtures/simple.ec" 6 7 diff --git a/tests/llm/scripts/load-goals.script b/tests/llm/scripts/load-goals.script new file mode 100644 index 000000000..83d64c2b8 --- /dev/null +++ b/tests/llm/scripts/load-goals.script @@ -0,0 +1,7 @@ +# exit: 0 +# LOAD a file up to a proof point, then inspect with GOALS / GOALS ALL. +LOAD "fixtures/simple.ec" 6 +GOALS +split. +GOALS +GOALS ALL diff --git a/tests/llm/scripts/load-nosmt.script b/tests/llm/scripts/load-nosmt.script new file mode 100644 index 000000000..deb495e0b --- /dev/null +++ b/tests/llm/scripts/load-nosmt.script @@ -0,0 +1,4 @@ +# exit: 0 +# LOAD -nosmt just has to load. +LOAD "fixtures/simple.ec" 6 -nosmt +GOALS diff --git a/tests/llm/scripts/load-trace-notinproof.script b/tests/llm/scripts/load-trace-notinproof.script new file mode 100644 index 000000000..4022dc223 --- /dev/null +++ b/tests/llm/scripts/load-trace-notinproof.script @@ -0,0 +1,9 @@ +# exit: 1 +# LOAD -trace whose target sentence is outside any proof. Tracing +# fails, but the prefix must be in effect exactly as after a plain +# LOAD: the deferred `require import AllCore.` has run, so `b2i' below +# resolves and GOALS shows its goal. +LOAD "fixtures/simple.ec" 3 -trace +GOALS +lemma preserved : b2i true = 1. +GOALS diff --git a/tests/llm/scripts/load-trace.script b/tests/llm/scripts/load-trace.script new file mode 100644 index 000000000..b02e820bc --- /dev/null +++ b/tests/llm/scripts/load-trace.script @@ -0,0 +1,3 @@ +# exit: 0 +# LOAD -trace on a file ending mid-proof: BEFORE/TACTIC/AFTER/SUMMARY. +LOAD "fixtures/midproof.ec" -trace diff --git a/tests/llm/scripts/multi-sentence-error.script b/tests/llm/scripts/multi-sentence-error.script new file mode 100644 index 000000000..3471c6909 --- /dev/null +++ b/tests/llm/scripts/multi-sentence-error.script @@ -0,0 +1,10 @@ +# exit: 1 +# File semantics for a multi-sentence line: the sentences before the +# failing one stay applied. `split.' succeeds, `apply nosuchlemma.' +# fails, and the trailing `trivial.' never runs -- so the session is +# left with the two goals `split.' opened, and COMMIT holds `split.' +# alone. +LOAD "fixtures/simple.ec" 6 +split. apply nosuchlemma. trivial. +TREE +COMMIT diff --git a/tests/llm/scripts/multi-sentence.script b/tests/llm/scripts/multi-sentence.script new file mode 100644 index 000000000..29efb00d1 --- /dev/null +++ b/tests/llm/scripts/multi-sentence.script @@ -0,0 +1,7 @@ +# exit: 0 +# Several sentences on one line: every one of them runs, and a single +# reply describes the state they leave behind. COMMIT records all three. +LOAD "fixtures/simple.ec" 6 +split. trivial. trivial. +GOALS +COMMIT diff --git a/tests/llm/scripts/multiline.script b/tests/llm/scripts/multiline.script new file mode 100644 index 000000000..32299a6b0 --- /dev/null +++ b/tests/llm/scripts/multiline.script @@ -0,0 +1,16 @@ +# exit: 0 +# / multi-line EasyCrypt input. +LOAD "fixtures/simple.ec" 3 + +lemma multi : + 1 = 1 /\ + 2 = 2. + +QUIET ON +split. +trivial. +trivial. +QUIET OFF +GOALS +qed. +COMMIT diff --git a/tests/llm/scripts/quiet.script b/tests/llm/scripts/quiet.script new file mode 100644 index 000000000..aa2917b6b --- /dev/null +++ b/tests/llm/scripts/quiet.script @@ -0,0 +1,8 @@ +# exit: 0 +# QUIET ON suppresses goal bodies; QUIET OFF restores them. +LOAD "fixtures/simple.ec" 6 +QUIET ON +split. +trivial. +QUIET OFF +GOALS diff --git a/tests/llm/scripts/search-in-proof.script b/tests/llm/scripts/search-in-proof.script new file mode 100644 index 000000000..f462e9cc3 --- /dev/null +++ b/tests/llm/scripts/search-in-proof.script @@ -0,0 +1,10 @@ +# exit: 0 +# A query issued in the middle of a proof must not end up in the body +# COMMIT emits: the two `trivial.` lines are the whole proof. +LOAD "fixtures/midproof.ec" +QUIET ON +trivial. +SEARCH (b2i _) +trivial. +QUIET OFF +COMMIT diff --git a/tests/llm/scripts/search.script b/tests/llm/scripts/search.script new file mode 100644 index 000000000..80a5404ac --- /dev/null +++ b/tests/llm/scripts/search.script @@ -0,0 +1,5 @@ +# exit: 1 +# SEARCH with a pattern, then SEARCH with no argument (error). +LOAD "fixtures/simple.ec" 6 +SEARCH (b2i _) +SEARCH diff --git a/tests/llm/scripts/tree-nested.script b/tests/llm/scripts/tree-nested.script new file mode 100644 index 000000000..ce9dd92a7 --- /dev/null +++ b/tests/llm/scripts/tree-nested.script @@ -0,0 +1,10 @@ +# exit: 0 +# Nested splits: TREE and TREE ALL show dotted labels [1.1.1] ... [2]. +LOAD "fixtures/nested.ec" 6 +QUIET ON +split. +split. +split. +QUIET OFF +TREE +TREE ALL diff --git a/tests/llm/scripts/undo-revert.script b/tests/llm/scripts/undo-revert.script new file mode 100644 index 000000000..34e6800f2 --- /dev/null +++ b/tests/llm/scripts/undo-revert.script @@ -0,0 +1,16 @@ +# exit: 1 +# UNDO, REVERT by numeric uuid, CHECKPOINT + REVERT by name, and the +# CHECKPOINT/REVERT argument errors. +LOAD "fixtures/simple.ec" 6 +CHECKPOINT start +split. +UNDO +split. +trivial. +REVERT 4 +REVERT 3 +CHECKPOINT +REVERT +REVERT start +REVERT nosuch +REVERT 999 diff --git a/tests/mcp/README.md b/tests/mcp/README.md new file mode 100644 index 000000000..fa161c019 --- /dev/null +++ b/tests/mcp/README.md @@ -0,0 +1,270 @@ +# `easycrypt mcp` golden-output tests + +Byte-identity regression harness for the MCP server (`src/ecMcp.ml`). +Each scenario is a newline-delimited script of JSON-RPC messages fed to +`ec.exe mcp` on stdin; the raw protocol stream it writes on stdout, and +its process exit status, are compared against recorded goldens. + +This is the sibling of `../llm`, which does the same for the REPL. The +two front-ends share `src/ecLlmCore.ml`, so most behaviour changes show +up in both sets of goldens — that is the point. + +## Layout + +| Path | Contents | +|------|----------| +| `scripts/*.script` | the JSON-RPC messages piped into the server | +| `expected/*.out` | recorded stdout, one file per script | +| `claude-code.mcp.json` | a ready-to-paste client configuration | +| `../llm/fixtures/*` | the EasyCrypt files the scripts load (shared with the REPL harness, never duplicated) | +| `../../scripts/testing/mcp-golden` | the runner | +| `../../scripts/testing/mcp-parity` | the REPL/MCP parity checker (see below) | +| `../../scripts/testing/mcp-inspector-check` | manual smoke test against a real client (see below) | + +## Running + +From the repository root: + +``` +make test-mcp # build + run every scenario +scripts/testing/mcp-golden # run every scenario +scripts/testing/mcp-golden happy-path protocol-errors +scripts/testing/mcp-golden --bin /path/to/ec.exe +scripts/testing/mcp-parity -v # the parity check, alone +``` + +The runner defaults to `_build/default/src/ec.exe`, resolved relative +to the repository root. It prints `PASS`/`FAIL` per scenario, a unified +diff for each mismatch, and exits nonzero if anything failed. That is +the CI invocation. + +## Re-recording + +``` +scripts/testing/mcp-golden --record # all scenarios +scripts/testing/mcp-golden --record tools-list # one scenario +``` + +`--record` overwrites `expected/*.out` with the current binary's +output instead of diffing. It still checks the declared exit status. + +Re-record only deliberately, and read the diff: these goldens are the +gate for changes to the protocol layer. + +## Scenarios + +| Scenario | What it pins | +|----------|--------------| +| `initialize` | the lifecycle handshake, the `initialized` notification, `ping` | +| `version-negotiation` | an unsupported revision falls back to the latest we speak; a supported one is echoed | +| `tools-list` | the whole tool table: names, descriptions, input/output schemas, annotations | +| `happy-path` | a session end to end: load, step, goals, tree, focus, commit | +| `prover-error` | EasyCrypt-level failures as `isError` results carrying the goal state | +| `try-revert` | `ec_try` rolling back a phrase that had already advanced the proof | +| `protocol-errors` | `-32700`, `-32600`, `-32601` and the `-32602` family | +| `revert` | `ec_revert` by uuid and by checkpoint name | +| `load-missing` | a missing file and an unknown extension: `isError`, *not* `-32602` | +| `notifications` | notifications, known and unknown, draw no reply | +| `exit` | `exit.` answers "session terminated", then the process stops | +| `eof` | end of input is a clean shutdown, exit 0 | + +## Result shape + +Every `tools/call` result carries the reply text **twice**: + +```json +{"content": [{"type": "text", "text": "Current goal\n..."}], + "structuredContent": {"text": "Current goal\n...", "uuid": 3, + "changed": true}, + "isError": false} +``` + +The two strings are the same by construction — `Result_of.make` takes +one `~text` and writes it into both halves — and `outputSchema` +declares `text` required alongside `uuid` and `changed` (and optional +`reverted`, on `ec_try`). + +The duplication is deliberate, and it is empirical rather than +aesthetic. Claude Code, the client this server is primarily for, hands +the model the `structuredContent` object **alone** and drops `content` +entirely whenever both are present. Isolated against a four-tool probe +server returning the same text under four result shapes (the run is +recorded in the message of commit `e3dce8552`): + +| result shape | payload reaches the model? | +|--------------|----------------------------| +| `content` + `structuredContent`, with `outputSchema` | no | +| `content` + `structuredContent`, without `outputSchema` | no | +| `content` only | yes | +| `content` + `structuredContent` *containing* the text | yes | + +So it is the presence of `structuredContent`, not of `outputSchema`, +that suppresses `content` — and before the text was duplicated, an +agent driving this server through Claude Code saw `{"uuid":3, +"changed":true}` and nothing else, while the Inspector, which displays +both halves, showed no problem at all. + +Row 4 is the shape we ship. Keeping `content` as well as filling +`structuredContent.text` costs one repeated string per reply and keeps +the server correct for spec-abiding clients that read `content`, for +clients that read only the structured half, and for the parity check, +which compares the REPL body against `content[0].text`. + +## Parity + +`make test-mcp` runs `scripts/testing/mcp-parity` after the goldens. +Where the goldens freeze *what* the MCP server answers, the parity +check pins *why the two front-ends can be trusted to agree*: they are +two wire layers over one core, so the same operation must produce the +same answer on both. + +It plays one representative operation per tool family — load, step, +goals, tree, focus, undo, checkpoint, step again, revert, search, +commit, and a failing phrase — in that order, against two sessions +started from the same directory (`tests/llm`, so both name the fixture +identically and no path difference can leak into a reply): a REPL +session driven with `llm -eval`, and an MCP session driven with a +JSON-RPC script. For each step it asserts two things. + +**The uuid matches.** The REPL's `[uuid:N]` envelope tag against the +MCP result's `structuredContent.uuid`. + +**The payload matches.** The REPL's reply body — everything it prints +between the `OK`/`ERROR` line and `` — against the MCP result's +`content[0].text`, *up to one trailing newline*. That slack is the +whole of the licensed difference: the REPL terminates a body that lacks +a newline so that `` starts a line of its own, and MCP, having no +sentinel, does not. The checker appends that newline and then demands +byte equality. + +The comparison is derived from the two envelopes rather than pattern +matched out of them: the REPL wire is a sequence of blocks opened by a +status line and closed by a lone ``, and the MCP wire is one JSON +object per line. Both are parsed structurally, so the checker cannot +be fooled by a body that happens to contain something envelope-shaped. + +Two asymmetries are structural, and the check deliberately does not +span them: + +* **Envelope tags.** The REPL's `[loaded:file:N]` and `[focus: 1/N]` + annotations ride on the status line, not in the body; MCP's envelope + is `structuredContent`, which carries `text`, `uuid` and `changed`, + none of which reproduces them. So an MCP client does not see them at + all. That is a gap worth closing one day — the natural home is a + further `structuredContent` field — but it is not a parity violation: + no body differs. +* **Notices on failures.** The REPL has never rendered the engine's + notice buffer on an `ERROR` reply; the MCP failure result does + include it. The two therefore agree only when the failing operation + emitted no notices, which is the case for the failing phrase the + check plays. Should a future step want a noisy failure, this is the + invariant to weaken — knowingly, and here. + +## Real clients + +Neither the goldens nor the parity check involve an MCP client: they +speak the wire themselves, so they prove the server is consistent with +itself and with the REPL, not that a client can use it. Two manual +checks close that gap. Neither is in CI — both need network access — +and both should be run after touching `src/ecMcp.ml`. + +**The reference client.** `scripts/testing/mcp-inspector-check` drives +the server with the MCP Inspector's CLI mode, `npx +@modelcontextprotocol/inspector --cli`, over `tools/list` and a +`tools/call` of `ec_load`: + +``` +scripts/testing/mcp-inspector-check --bin ./ec.native +``` + +**Claude Code.** `claude-code.mcp.json` is a project configuration to +drop next to a proof development. It names `easycrypt` on the `PATH`, +so it stays free of absolute paths: + +```json +{"mcpServers": {"easycrypt": {"command": "easycrypt", "args": ["mcp"]}}} +``` + +A project-scoped `.mcp.json` needs interactive approval, so for a +headless check register the server at local scope instead and ask for +its health: + +``` +claude mcp add-json easycrypt '{"command":"/abs/path/ec.exe","args":["mcp"]}' --scope local +claude mcp list # easycrypt: ... - ✔ Connected +claude mcp remove easycrypt -s local +``` + +Health is not the interesting question, though: it was this headless +check that found the payload never reaching the agent (see **Result +shape** above), which no wire-level test can see. So ask the session to +*use* the server and quote back what it got — that, and not the +connection, is what the client-side check is for: + +``` +claude -p 'Call ec_load with file=/tests/llm/fixtures/simple.ec + and line=6, then ec_goals. Quote the goal text verbatim.' \ + --allowedTools mcp__easycrypt__ec_load mcp__easycrypt__ec_goals +``` + +An agent that can quote `1 = 1 /\ 2 = 2` is reading the payload; one +that answers with a bare uuid is not. + +## Expected exit status + +Each `.script` declares its expected process exit status on its first +line: + +``` +# exit: 0 +``` + +Lines starting with `#` are comment lines: the runner strips **all** of +them before piping the script into the server, so they can also be used +for prose. The first `# exit: N` line wins; a script without one fails. + +`easycrypt mcp` exits 0 on end of input and 0 after an `exit.` phrase; +EasyCrypt-level failures are `isError` results, not exit statuses, so +every scenario here declares `# exit: 0`. The field is kept all the +same, so that a future exit path cannot change silently. + +## Determinism rules + +The goldens are compared byte for byte, so scenarios must not leak +anything machine- or environment-dependent: + +* **Relative paths only.** The runner `cd`s into `tests/mcp` before + invoking the binary, and scripts refer to fixtures as + `"../llm/fixtures/simple.ec"`. Error messages echo the path + verbatim, so an absolute one would bake the developer's home + directory into the golden. +* **One normalization, and only one.** `serverInfo.version` is a + git-describe string; the runner rewrites it to `VERSION` with `sed` + before diffing. Nothing else is touched — if a second unstable field + ever appears, that is a bug in the server, not a reason to normalize + more. +* **No SMT.** As in `../llm`: proofs close with `trivial`, `done` or + `split`, never with `smt`, whose availability and timing vary by + machine. +* **stdout only.** stderr carries the engine's diagnostics (the server + points the process's stdout at stderr and keeps a private descriptor + for the protocol); it is discarded. +* Fixtures require `AllCore` only. + +## Reading a golden + +The stream is the protocol: one JSON message per line, unindented, +exactly as a client sees it. `tools-list.out` is therefore a single +very long line, and `diff` will show it whole. To read one by hand: + +``` +python3 -m json.tool < <(head -n 1 tests/mcp/expected/tools-list.out) +``` + +## Adding a scenario + +1. Add `scripts/NAME.script` starting with `# exit: N`. +2. Reuse a fixture from `../llm/fixtures/`; add a new one there (not + here) if none fits. +3. `scripts/testing/mcp-golden --record NAME`. +4. Read `expected/NAME.out` and check it is what you meant to freeze. diff --git a/tests/mcp/claude-code.mcp.json b/tests/mcp/claude-code.mcp.json new file mode 100644 index 000000000..4ce195032 --- /dev/null +++ b/tests/mcp/claude-code.mcp.json @@ -0,0 +1,8 @@ +{ + "mcpServers": { + "easycrypt": { + "command": "easycrypt", + "args": ["mcp"] + } + } +} diff --git a/tests/mcp/expected/eof.out b/tests/mcp/expected/eof.out new file mode 100644 index 000000000..8ddc98e50 --- /dev/null +++ b/tests/mcp/expected/eof.out @@ -0,0 +1 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} diff --git a/tests/mcp/expected/exit.out b/tests/mcp/expected/exit.out new file mode 100644 index 000000000..366d40ffc --- /dev/null +++ b/tests/mcp/expected/exit.out @@ -0,0 +1,2 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"session terminated"}],"structuredContent":{"text":"session terminated","uuid":0,"changed":false},"isError":false}} diff --git a/tests/mcp/expected/happy-path.out b/tests/mcp/expected/happy-path.out new file mode 100644 index 000000000..23d4391d0 --- /dev/null +++ b/tests/mcp/expected/happy-path.out @@ -0,0 +1,8 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\n\n Goal #2\n ------------------------------------------------------------------------\n 2 = 2\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n\n\n\n Goal #2\n ------------------------------------------------------------------------\n 2 = 2\n","uuid":4,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":5,"result":{"content":[{"type":"text","text":"[1] 1 = 1 <- focused\n[2] 2 = 2\n"}],"structuredContent":{"text":"[1] 1 = 1 <- focused\n[2] 2 = 2\n","uuid":4,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":6,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n","uuid":5,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":7,"result":{"content":[{"type":"text","text":"No more goals\n"}],"structuredContent":{"text":"No more goals\n","uuid":7,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":8,"result":{"content":[{"type":"text","text":"split.\n- trivial.\n- trivial.\n"}],"structuredContent":{"text":"split.\n- trivial.\n- trivial.\n","uuid":7,"changed":false},"isError":false}} diff --git a/tests/mcp/expected/initialize.out b/tests/mcp/expected/initialize.out new file mode 100644 index 000000000..1f7c0553c --- /dev/null +++ b/tests/mcp/expected/initialize.out @@ -0,0 +1,2 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{}} diff --git a/tests/mcp/expected/load-missing.out b/tests/mcp/expected/load-missing.out new file mode 100644 index 000000000..d1fb8737e --- /dev/null +++ b/tests/mcp/expected/load-missing.out @@ -0,0 +1,3 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"LOAD: no such file: ../llm/fixtures/nosuchfile.ec"}],"structuredContent":{"text":"LOAD: no such file: ../llm/fixtures/nosuchfile.ec","uuid":0,"changed":false},"isError":true}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"unknown file extension: .txt\nNo active proof.\n"}],"structuredContent":{"text":"unknown file extension: .txt\nNo active proof.\n","uuid":0,"changed":false},"isError":true}} diff --git a/tests/mcp/expected/notifications.out b/tests/mcp/expected/notifications.out new file mode 100644 index 000000000..c71fd037e --- /dev/null +++ b/tests/mcp/expected/notifications.out @@ -0,0 +1,2 @@ +{"jsonrpc":"2.0","id":1,"result":{}} +{"jsonrpc":"2.0","id":2,"result":{}} diff --git a/tests/mcp/expected/protocol-errors.out b/tests/mcp/expected/protocol-errors.out new file mode 100644 index 000000000..d920f69df --- /dev/null +++ b/tests/mcp/expected/protocol-errors.out @@ -0,0 +1,16 @@ +{"jsonrpc":"2.0","id":null,"error":{"code":-32700,"message":"invalid JSON"}} +{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"JSON-RPC batches are not supported by this protocol revision"}} +{"jsonrpc":"2.0","id":2,"error":{"code":-32601,"message":"method not found: server/discover"}} +{"jsonrpc":"2.0","id":3,"error":{"code":-32600,"message":"missing `method'"}} +{"jsonrpc":"2.0","id":4,"error":{"code":-32600,"message":"`method' must be a string"}} +{"jsonrpc":"2.0","id":null,"error":{"code":-32600,"message":"a JSON-RPC message must be an object"}} +{"jsonrpc":"2.0","id":5,"error":{"code":-32602,"message":"unknown tool: ec_nosuchtool"}} +{"jsonrpc":"2.0","id":6,"error":{"code":-32602,"message":"missing tool `name'"}} +{"jsonrpc":"2.0","id":7,"error":{"code":-32602,"message":"`name' must be a string"}} +{"jsonrpc":"2.0","id":8,"error":{"code":-32602,"message":"ec_step: missing required argument `phrase'"}} +{"jsonrpc":"2.0","id":9,"error":{"code":-32602,"message":"ec_goals: `all' must be a boolean"}} +{"jsonrpc":"2.0","id":10,"error":{"code":-32602,"message":"ec_load: `col' requires `line'"}} +{"jsonrpc":"2.0","id":11,"error":{"code":-32602,"message":"ec_load: `line' must be an integer"}} +{"jsonrpc":"2.0","id":12,"error":{"code":-32602,"message":"ec_focus: not a path of integers: 1.oops"}} +{"jsonrpc":"2.0","id":13,"error":{"code":-32602,"message":"ec_focus: path indices must be >= 1: 0"}} +{"jsonrpc":"2.0","id":14,"error":{"code":-32602,"message":"`params' must be an object"}} diff --git a/tests/mcp/expected/prover-error.out b/tests/mcp/expected/prover-error.out new file mode 100644 index 000000000..2cc6d95de --- /dev/null +++ b/tests/mcp/expected/prover-error.out @@ -0,0 +1,6 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":": line 1 (0-18): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":": line 1 (0-18): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":true}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":"FOCUS: index 7 out of range (1..1)\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"FOCUS: index 7 out of range (1..1)\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":true}} +{"jsonrpc":"2.0","id":5,"result":{"content":[{"type":"text","text":"No active proof.\n"}],"structuredContent":{"text":"No active proof.\n","uuid":0,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":6,"result":{"content":[{"type":"text","text":"nothing to undo\nNo active proof.\n"}],"structuredContent":{"text":"nothing to undo\nNo active proof.\n","uuid":0,"changed":false},"isError":true}} diff --git a/tests/mcp/expected/revert.out b/tests/mcp/expected/revert.out new file mode 100644 index 000000000..60c85a271 --- /dev/null +++ b/tests/mcp/expected/revert.out @@ -0,0 +1,11 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":"checkpoint 'start' set at uuid 3"}],"structuredContent":{"text":"checkpoint 'start' set at uuid 3","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":5,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":6,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":7,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n2 = 2\n","uuid":5,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":8,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":9,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":10,"result":{"content":[{"type":"text","text":""}],"structuredContent":{"text":"","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":11,"result":{"content":[{"type":"text","text":"REVERT: 'nosuchname' is not a valid uuid or checkpoint name\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"REVERT: 'nosuchname' is not a valid uuid or checkpoint name\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":true}} diff --git a/tests/mcp/expected/tools-list.out b/tests/mcp/expected/tools-list.out new file mode 100644 index 000000000..ab9b959cb --- /dev/null +++ b/tests/mcp/expected/tools-list.out @@ -0,0 +1 @@ +{"jsonrpc":"2.0","id":1,"result":{"tools":[{"name":"ec_load","description":"Reset the session and compile FILE from the top, stopping after the last sentence that ends on or before LINE (and column COL when given). This is the entry point: every other tool needs a loaded file, and tactics need the position to land inside a proof. Set nosmt to weaken SMT calls while replaying a prefix that was already verified, which is much faster on large files. Set trace to have the reply describe the last loaded sentence as BEFORE / TACTIC / AFTER / SUMMARY blocks. The reply reports where compilation stopped and the resulting goal state; note the uuid it returns, reverting to it is the instant way back to the start of the proof.","inputSchema":{"type":"object","properties":{"file":{"type":"string","description":"path to the .ec/.eca file"},"line":{"type":"integer","description":"stop after the last sentence ending on or before this line; omit to compile the whole file"},"col":{"type":"integer","description":"column bound within `line'; requires `line'"},"nosmt":{"type":"boolean","description":"weaken SMT calls while compiling the prefix","default":false},"trace":{"type":"boolean","description":"report the proof state around the last loaded sentence","default":false}},"required":["file"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_step","description":"Run EasyCrypt sentences -- tactics, declarations, require, print, ... -- against the current session. Every complete sentence in the argument is executed, in order, exactly as if the text had been appended to the source file, and a single reply describes the state they leave behind; sentences may span several lines. Requires a file loaded with ec_load, and, for tactics, an open proof. On success the reply carries the new goal state; on failure the prover's error text comes back with isError set, the sentences before the failing one stay applied and the engine is left wherever that sentence left it -- use ec_try when you want a guaranteed rollback. Successful non-query phrases are recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one or more complete EasyCrypt sentences, each ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false,"idempotentHint":false}},{"name":"ec_try","description":"Like ec_step, but the engine is rolled back to the state it had before the call whenever a sentence fails, including input that failed only after having already advanced the proof. The failure reply sets structuredContent.reverted to true, and its uuid and goal text describe the restored state, not the point of failure. Use this to probe a tactic without having to ec_revert afterwards; use ec_step when you mean to keep whatever progress the phrase makes. A successful phrase behaves exactly as under ec_step and is recorded for ec_commit.","inputSchema":{"type":"object","properties":{"phrase":{"type":"string","description":"one complete EasyCrypt sentence, ending with `.'"}},"required":["phrase"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"},"reverted":{"type":"boolean","description":"set when the phrase failed and the engine was rolled back to its pre-call state"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_goals","description":"Print the current proof state: the focused subgoal alone, or, with all set, every open subgoal. Requires an open proof, and does not advance the engine.","inputSchema":{"type":"object","properties":{"all":{"type":"boolean","description":"print every open subgoal instead of the focused one","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_tree","description":"List the open subgoals as a tree of dotted-path labels -- [1], [1.2], [2.1.1] -- showing how the splits nest, and marking the focused one. Those labels are exactly what ec_focus accepts. Set full for whole goal bodies rather than one-line conclusions. The labels are not stable across focus changes: the tree always shows the focused goal first, so re-read it after every ec_focus. Does not advance the engine.","inputSchema":{"type":"object","properties":{"full":{"type":"boolean","description":"print full goal bodies instead of one-line conclusions","default":false}},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_focus","description":"Rotate the focus onto the subgoal at dotted path PATH, as printed by ec_tree (\"2\", \"1.2\", \"1.1.1\"); a single integer selects the k-th goal of the flat listing, and the special value \"next\" moves to the next open subgoal. Subsequent tactics act on the focused goal. Selecting an internal frame instead of a leaf goal is an error.","inputSchema":{"type":"object","properties":{"path":{"type":"string","description":"\"N\", a dotted path \"N1.N2...\", or \"next\""}},"required":["path"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_undo","description":"Undo the last engine step, returning to the immediately preceding state. The ec_commit transcript is trimmed to match. Fails when there is nothing left to undo.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":false}},{"name":"ec_revert","description":"Return the session to an earlier state, named either by a uuid reported in some previous structuredContent or by a name given to ec_checkpoint. Reverting is instant, unlike re-running ec_load, so going back to the uuid ec_load returned is the cheap way to restart a proof from scratch after a failed experiment. The ec_commit transcript is trimmed to match.","inputSchema":{"type":"object","properties":{"target":{"type":"string","description":"a uuid (as a decimal string) or a checkpoint name"}},"required":["target"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"destructiveHint":true}},{"name":"ec_checkpoint","description":"Record the current uuid under NAME, so that ec_revert can address it by name later. Worth doing before a branching experiment, when carrying the bare uuid around is awkward. Does not change the proof state.","inputSchema":{"type":"object","properties":{"name":{"type":"string","description":"checkpoint name"}},"required":["name"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_commit","description":"Emit the phrases recorded since the last ec_load as a proof body, with bullets inserted at every multi-child split: the result compiles under `pragma +strict_bullets' and can be pasted straight into the source file. Queries (search, print, locate, ec_search) are never recorded, so looking things up mid-proof does not pollute the body, and ec_undo / ec_revert trim the transcript. Still works after `qed.'. Does not change the proof state.","inputSchema":{"type":"object","properties":{},"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}},{"name":"ec_search","description":"Search the environment for lemmas matching an EasyCrypt search pattern. This is pattern syntax, not keyword search: use _ as the wildcard, as in \"(fdom _)\", \"(_ %/ _)\" or \"(mu _ _) (_ <= _)\". Requires a loaded file. The query neither advances the proof nor enters the ec_commit transcript.","inputSchema":{"type":"object","properties":{"pattern":{"type":"string","description":"an EasyCrypt search pattern"}},"required":["pattern"],"additionalProperties":false},"outputSchema":{"type":"object","properties":{"text":{"type":"string","description":"the reply body -- goal state, proof body, search results, error text; the same string as content[0].text"},"uuid":{"type":"integer","description":"engine state identifier after the call; pass it to ec_revert to come back here"},"changed":{"type":"boolean","description":"whether the engine state advanced"}},"required":["text","uuid","changed"]},"annotations":{"readOnlyHint":true}}]}} diff --git a/tests/mcp/expected/try-revert.out b/tests/mcp/expected/try-revert.out new file mode 100644 index 000000000..665049196 --- /dev/null +++ b/tests/mcp/expected/try-revert.out @@ -0,0 +1,7 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":3,"result":{"content":[{"type":"text","text":": line 1 (7-25): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":": line 1 (7-25): unknown lemma `nosuchlemma'\nsource: apply nosuchlemma.\nCurrent goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false,"reverted":true},"isError":true}} +{"jsonrpc":"2.0","id":4,"result":{"content":[{"type":"text","text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n"}],"structuredContent":{"text":"Current goal\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1 /\\ 2 = 2\n","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":5,"result":{"content":[{"type":"text","text":""}],"structuredContent":{"text":"","uuid":3,"changed":false},"isError":false}} +{"jsonrpc":"2.0","id":6,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":true},"isError":false}} +{"jsonrpc":"2.0","id":7,"result":{"content":[{"type":"text","text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n"}],"structuredContent":{"text":"Current goal (remaining: 2)\n\nType variables: \n\n------------------------------------------------------------------------\n1 = 1\n","uuid":4,"changed":false},"isError":false}} diff --git a/tests/mcp/expected/version-negotiation.out b/tests/mcp/expected/version-negotiation.out new file mode 100644 index 000000000..6e0aa6aa9 --- /dev/null +++ b/tests/mcp/expected/version-negotiation.out @@ -0,0 +1,3 @@ +{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":2,"result":{"protocolVersion":"2025-06-18","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} +{"jsonrpc":"2.0","id":3,"result":{"protocolVersion":"2025-11-25","capabilities":{"tools":{}},"serverInfo":{"name":"easycrypt","version":"VERSION"}}} diff --git a/tests/mcp/scripts/eof.script b/tests/mcp/scripts/eof.script new file mode 100644 index 000000000..b50d488d2 --- /dev/null +++ b/tests/mcp/scripts/eof.script @@ -0,0 +1,3 @@ +# exit: 0 +# End of input is a clean shutdown, exit 0, with no farewell message. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} diff --git a/tests/mcp/scripts/exit.script b/tests/mcp/scripts/exit.script new file mode 100644 index 000000000..cbec912ad --- /dev/null +++ b/tests/mcp/scripts/exit.script @@ -0,0 +1,7 @@ +# exit: 0 +# `exit.' ends the session: the response still goes out, then the +# process stops. The ping after it is never read, so it must not +# appear in the golden. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"exit."}}} +{"jsonrpc":"2.0","id":3,"method":"ping"} diff --git a/tests/mcp/scripts/happy-path.script b/tests/mcp/scripts/happy-path.script new file mode 100644 index 000000000..c5961b668 --- /dev/null +++ b/tests/mcp/scripts/happy-path.script @@ -0,0 +1,13 @@ +# exit: 0 +# A whole session over MCP: load a file up to its `proof.', split, +# inspect the goals and the tree, close both branches, and read the +# proof body back out of ec_commit. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","method":"notifications/initialized"} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"split."}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_goals","arguments":{"all":true}}} +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_tree","arguments":{}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"name":"ec_focus","arguments":{"path":"2"}}} +{"jsonrpc":"2.0","id":7,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"trivial. trivial."}}} +{"jsonrpc":"2.0","id":8,"method":"tools/call","params":{"name":"ec_commit","arguments":{}}} diff --git a/tests/mcp/scripts/initialize.script b/tests/mcp/scripts/initialize.script new file mode 100644 index 000000000..ea3ac3291 --- /dev/null +++ b/tests/mcp/scripts/initialize.script @@ -0,0 +1,6 @@ +# exit: 0 +# The lifecycle handshake: initialize, the client's initialized +# notification (no reply), then a ping. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{},"clientInfo":{"name":"golden","version":"0"}}} +{"jsonrpc":"2.0","method":"notifications/initialized"} +{"jsonrpc":"2.0","id":2,"method":"ping"} diff --git a/tests/mcp/scripts/load-missing.script b/tests/mcp/scripts/load-missing.script new file mode 100644 index 000000000..e7aa4ef5a --- /dev/null +++ b/tests/mcp/scripts/load-missing.script @@ -0,0 +1,8 @@ +# exit: 0 +# A file the tool cannot find is an EasyCrypt-level failure, so it +# comes back as an isError result and NOT as a -32602: the arguments +# satisfy the schema, it is the world that does not. Same for a file +# whose extension the loader does not know. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/nosuchfile.ec"}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/notec.txt"}}} diff --git a/tests/mcp/scripts/notifications.script b/tests/mcp/scripts/notifications.script new file mode 100644 index 000000000..9eaadab7e --- /dev/null +++ b/tests/mcp/scripts/notifications.script @@ -0,0 +1,13 @@ +# exit: 0 +# Notifications never draw a reply, whatever they are: the three the +# spec has us tolerate, an unknown one, and a message whose id is +# null (which MCP forbids, so we read it as "no id" and stay silent). +# The two pings bracket them, so the golden shows nothing in between. +{"jsonrpc":"2.0","id":1,"method":"ping"} +{"jsonrpc":"2.0","method":"notifications/initialized"} +{"jsonrpc":"2.0","method":"notifications/cancelled","params":{"requestId":1}} +{"jsonrpc":"2.0","method":"notifications/roots/list_changed"} +{"jsonrpc":"2.0","method":"notifications/nobody/knows"} +{"jsonrpc":"2.0","id":null,"method":"ping"} + +{"jsonrpc":"2.0","id":2,"method":"ping"} diff --git a/tests/mcp/scripts/protocol-errors.script b/tests/mcp/scripts/protocol-errors.script new file mode 100644 index 000000000..4d18d3ba6 --- /dev/null +++ b/tests/mcp/scripts/protocol-errors.script @@ -0,0 +1,22 @@ +# exit: 0 +# Protocol-level failures, which are JSON-RPC errors and never +# isError results: malformed JSON (-32700), a batch array and a +# malformed envelope (-32600), an unknown method (-32601), and the +# -32602 family -- unknown tool, missing and ill-typed arguments, +# `col' without `line', and an unparsable ec_focus path. +{not json at all +[{"jsonrpc":"2.0","id":1,"method":"ping"}] +{"jsonrpc":"2.0","id":2,"method":"server/discover"} +{"jsonrpc":"2.0","id":3} +{"jsonrpc":"2.0","id":4,"method":42} +"just a string" +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_nosuchtool","arguments":{}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"arguments":{}}} +{"jsonrpc":"2.0","id":7,"method":"tools/call","params":{"name":17,"arguments":{}}} +{"jsonrpc":"2.0","id":8,"method":"tools/call","params":{"name":"ec_step","arguments":{}}} +{"jsonrpc":"2.0","id":9,"method":"tools/call","params":{"name":"ec_goals","arguments":{"all":"yes"}}} +{"jsonrpc":"2.0","id":10,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","col":3}}} +{"jsonrpc":"2.0","id":11,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":"6"}}} +{"jsonrpc":"2.0","id":12,"method":"tools/call","params":{"name":"ec_focus","arguments":{"path":"1.oops"}}} +{"jsonrpc":"2.0","id":13,"method":"tools/call","params":{"name":"ec_focus","arguments":{"path":"0"}}} +{"jsonrpc":"2.0","id":14,"method":"tools/call","params":"not an object"} diff --git a/tests/mcp/scripts/prover-error.script b/tests/mcp/scripts/prover-error.script new file mode 100644 index 000000000..a599dfea9 --- /dev/null +++ b/tests/mcp/scripts/prover-error.script @@ -0,0 +1,11 @@ +# exit: 0 +# An EasyCrypt-level failure is data, not a protocol error: a +# successful response carrying isError, the prover's message and the +# goal state at the point of failure. ec_undo then reports there is +# nothing left to undo, which is the same kind of failure. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"apply nosuchlemma."}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_focus","arguments":{"path":"7"}}} +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_revert","arguments":{"target":"0"}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"name":"ec_undo","arguments":{}}} diff --git a/tests/mcp/scripts/revert.script b/tests/mcp/scripts/revert.script new file mode 100644 index 000000000..2f37151c0 --- /dev/null +++ b/tests/mcp/scripts/revert.script @@ -0,0 +1,15 @@ +# exit: 0 +# ec_revert addressed both ways: by the uuid ec_load reported, and by +# a name given to ec_checkpoint. Each revert is followed by ec_goals, +# so the golden records where the session actually landed. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_checkpoint","arguments":{"name":"start"}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"split."}}} +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_revert","arguments":{"target":"3"}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"name":"ec_goals","arguments":{}}} +{"jsonrpc":"2.0","id":7,"method":"tools/call","params":{"name":"ec_step","arguments":{"phrase":"split. trivial."}}} +{"jsonrpc":"2.0","id":8,"method":"tools/call","params":{"name":"ec_revert","arguments":{"target":"start"}}} +{"jsonrpc":"2.0","id":9,"method":"tools/call","params":{"name":"ec_goals","arguments":{}}} +{"jsonrpc":"2.0","id":10,"method":"tools/call","params":{"name":"ec_commit","arguments":{}}} +{"jsonrpc":"2.0","id":11,"method":"tools/call","params":{"name":"ec_revert","arguments":{"target":"nosuchname"}}} diff --git a/tests/mcp/scripts/tools-list.script b/tests/mcp/scripts/tools-list.script new file mode 100644 index 000000000..ea2b8ad25 --- /dev/null +++ b/tests/mcp/scripts/tools-list.script @@ -0,0 +1,5 @@ +# exit: 0 +# The tool declarations, verbatim. This golden pins the agent-facing +# contract: names, descriptions, input schemas, output schemas and +# annotations. Editing any tool description re-records this file. +{"jsonrpc":"2.0","id":1,"method":"tools/list"} diff --git a/tests/mcp/scripts/try-revert.script b/tests/mcp/scripts/try-revert.script new file mode 100644 index 000000000..2d4e7e3f4 --- /dev/null +++ b/tests/mcp/scripts/try-revert.script @@ -0,0 +1,12 @@ +# exit: 0 +# ec_try rolls back. The phrase advances the proof (`split.') before +# failing, so the rollback has real work to do: the failure reply +# reports reverted true and changed false, and the ec_goals that +# follows proves the pre-call goal is back. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2025-11-25","capabilities":{}}} +{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"ec_load","arguments":{"file":"../llm/fixtures/simple.ec","line":6}}} +{"jsonrpc":"2.0","id":3,"method":"tools/call","params":{"name":"ec_try","arguments":{"phrase":"split. apply nosuchlemma."}}} +{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"ec_goals","arguments":{}}} +{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"ec_commit","arguments":{}}} +{"jsonrpc":"2.0","id":6,"method":"tools/call","params":{"name":"ec_try","arguments":{"phrase":"split."}}} +{"jsonrpc":"2.0","id":7,"method":"tools/call","params":{"name":"ec_goals","arguments":{}}} diff --git a/tests/mcp/scripts/version-negotiation.script b/tests/mcp/scripts/version-negotiation.script new file mode 100644 index 000000000..f638af715 --- /dev/null +++ b/tests/mcp/scripts/version-negotiation.script @@ -0,0 +1,7 @@ +# exit: 0 +# Version negotiation. An unsupported revision gets the latest one we +# speak; a supported older revision is echoed back; a missing or +# non-string protocolVersion also falls back to the latest. +{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2099-01-01","capabilities":{},"clientInfo":{"name":"golden","version":"0"}}} +{"jsonrpc":"2.0","id":2,"method":"initialize","params":{"protocolVersion":"2025-06-18","capabilities":{}}} +{"jsonrpc":"2.0","id":3,"method":"initialize","params":{"capabilities":{}}}