[llm] mcp -sessions: one engine per agent behind one MCP server

`easycrypt mcp' is one engine with one proof state. An MCP client such
as Claude Code opens one stdio connection per configured server and
lets every agent it runs share it, and the transport carries no caller
identity, so two agents driving the server clobber each other's goals.
The only fix is at the protocol level: a `session' argument on every
tool, and one engine per session.

Not several EcLlmCore states in one process. The engine is
single-threaded, so one agent loading a large development would block
every other session; the loader cache, the prover configuration and
the Why3 processes are global; and a loaded engine holds memory that
only a process exit gives back. `mcp -sessions' therefore runs a
multiplexer instead of an engine: the first call naming a session
starts a child `easycrypt mcp' -- the single-engine server, unchanged,
launched from our own executable with our own arguments minus the
multiplexer's -- and every later call naming it is forwarded there.
The child's result or error comes back under the client's id.
`initialize', `ping' and `tools/list' are answered locally, under the
same server name, so a client's approval of the server carries over.

Requests run concurrently, one thread each; the threads do I/O and
JSON and nothing else. Three mutexes: one per child (a child is
synchronous, so calls to one session serialise), one for the client's
stdout, one for the session table. A new session's handshake runs
under its own lock, not the table's, so a second caller on that name
queues behind it rather than stalling everyone. A child that dies
under a call is dropped and the caller told so in a tool-level error
that says to `ec_load' again; a name closed and re-created while a
call on the old child was in flight is not taken down by that call.

Children must not outlive the multiplexer: `at_exit' and handlers for
SIGTERM, SIGINT and SIGHUP kill them, and under SIGKILL they read EOF
on their stdin and stop once their current command completes. SIGPIPE
is ignored, so a write to a dead child is an EPIPE we can report on
that session rather than a signal that takes the server down. Exited
children are reaped. Session names double as log-file names, hence a
restricted alphabet. An idle reaper kills sessions unused for `-idle'
minutes (default 180) that are not mid-call.

Two tools of the multiplexer's own, `ec_sessions' and `ec_close'. The
tool table with `session' added is a pure function of the existing
one and lives next to it, so the two cannot drift apart. `Wire', the
initialize reply and the stdout dup trick move to module level in
EcMcp so both servers share them; `wire_stdout' now dups close-on-exec,
so no process we start holds the client's pipe. The single-engine
server is otherwise untouched: the 18 MCP goldens, the parity check
and the 38 REPL goldens pass unchanged.

`scripts/testing/mcp-sessions' checks the contract, and `make test-mcp'
runs it. It is not a golden: the multiplexer answers in whatever order
the children finish, and pids and idle times are not reproducible. It
drives the server as a client would and asserts the tool table, two
sessions loading different files at once without seeing each other,
tool-level errors for a missing or invalid name against pass-through
protocol errors from the engine, ec_sessions/ec_close, an engine that
exited being reported dead and restarted by the next call, and no
child surviving end of input or SIGTERM.

doc/llm/CLAUDE.md gains "Multi-agent sessions" -- what `mcp -help'
prints -- with the rule for agents: one session name per agent, never
another's.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RkdycFar1eka8ReJ9HeqZf

Author: bgregoir

Makefile

@@ -18,6 +18,7 @@ LLMWARM   += --bin=./ec.native
 MCPCHECK  := scripts/testing/mcp-golden
 MCPCHECK  += --bin=./ec.native
 MCPPARITY := scripts/testing/mcp-parity
+MCPSESSIONS := scripts/testing/mcp-sessions
 MCPPARITY += --bin=./ec.native
 NIX       ?= nix --extra-experimental-features "nix-command flakes"
 PROFILE   ?= dev
@@ -65,6 +66,7 @@ test-llm: build
 test-mcp: build
 	$(MCPCHECK)
 	$(MCPPARITY)
+	$(MCPSESSIONS)
 
 check: unit stdlib examples test-llm test-mcp
 	@true

README.md

@@ -170,7 +170,9 @@ 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
+stdio (`easycrypt mcp -sessions` serves one engine per named session,
+for clients that run several agents at once). Both drive the same
+proof engine, and both are documented in
 [doc/llm/CLAUDE.md](doc/llm/CLAUDE.md).
 
 ### Proof-General (Emacs)

doc/llm/CLAUDE.md

@@ -457,11 +457,14 @@ protocol, as a debug console, or for `-eval` scripting.
 
 ```
 easycrypt mcp [OPTIONS]
+easycrypt mcp -sessions [-idle <minutes>] [-logdir <dir>] [OPTIONS]
 ```
 
-The same loader and prover options as `llm` are available (`-I`,
-`-timeout`, `-p`, `-stdlib`, etc.). Use `-help` to print this section
-and exit:
+The first form is one engine for one client; the second, one engine
+per named session behind one server, for clients that run several
+agents at once (see "Multi-agent sessions" below). The same loader
+and prover options as `llm` are available in both (`-I`, `-timeout`,
+`-p`, `-stdlib`, etc.). Use `-help` to print this section and exit:
 
 ```
 easycrypt mcp -help
@@ -477,7 +480,9 @@ resources, no prompts, no sampling.
 ### Tools
 
 Thirteen tools. Required arguments are marked; the others default as
-noted.
+noted. Under `-sessions`, every one of them takes a required `session`
+as well, and two more tools appear, `ec_sessions` and `ec_close`; see
+"Multi-agent sessions" below.
 
 | Tool | Arguments | Description |
 |------|-----------|-------------|
@@ -530,8 +535,9 @@ 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
+one engine state: tool calls run strictly in arrival order even when a
+client pipelines them. Several agents sharing one client need one
+engine each; that is what `-sessions` provides (see below). 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
@@ -601,6 +607,67 @@ Add loader options to `args` as needed, e.g. `["mcp", "-I",
 claude mcp add easycrypt -- easycrypt mcp
 ```
 
+### Multi-agent sessions
+
+An MCP client such as Claude Code opens one connection per configured
+server and lets every agent it runs share it, and the stdio transport
+carries no caller identity. Two agents driving one `easycrypt mcp`
+therefore clobber each other's goals. The fix is at the protocol
+level:
+
+```
+easycrypt mcp -sessions [-idle <minutes>] [-logdir <dir>]
+```
+
+runs a *multiplexer* instead of an engine: the same tools, each with
+one more required argument, `session`, naming the engine the call
+runs in. The first call naming a session starts a child
+`easycrypt mcp` — the single-engine server above, with the loader and
+prover options the multiplexer received — and every later call naming
+it is forwarded there. Sessions are independent processes: their own
+loaded file, uuids, checkpoints, strict mode and memory. Calls to
+different sessions run in parallel; calls to the same session run in
+arrival order, as before. `initialize`, `tools/list` and `ping` are
+answered by the multiplexer itself, under the same server name, so a
+client's approval of the server carries over.
+
+**The rule for agents: one session name per agent, and never another
+agent's.** Use your agent tag, or any name that is yours alone, in
+every call. A call without `session` is refused with a tool-level
+error, as is a name that is not made of letters, digits, `_`, `-` and
+`.` (at most 64 characters). Two agents that share a name share an
+engine and are back to clobbering each other.
+
+Two tools belong to the multiplexer:
+
+| Tool | Arguments | Description |
+|------|-----------|-------------|
+| `ec_sessions` | — | List the live sessions, one line each: `NAME  pid PID  idle Ns`, with `(dead)` appended when the engine has exited; or `no live session` |
+| `ec_close` | `session` (req) | Kill that session's engine and forget it; answers `closed NAME` or ``no session `NAME'`` |
+
+A session unused for `-idle` minutes (default 180) is killed, unless a
+call is running in it; a loaded large development is a lot of resident
+memory, and only a process exit gives it back. Close your own session
+with `ec_close` when you are done with it. A session whose engine died
+— killed, timed out, or stopped by an `exit.` phrase — is dropped, and
+the next call naming it starts a fresh engine, which needs an
+`ec_load` again; a call that finds the engine gone says so in a
+tool-level error rather than failing silently.
+
+Each child's stderr — the engine's own chatter, which the single
+server also writes to stderr — goes to `<dir>/ec-mcp-<session>.log`,
+with `-logdir` defaulting to `$TMPDIR`, else `/tmp`. The
+multiplexer's stdout carries the protocol and nothing else. When the
+client closes the connection, or the multiplexer is terminated, every
+child is killed with it.
+
+A ready-to-use client configuration:
+
+```json
+{"mcpServers": {"easycrypt": {"command": "easycrypt",
+                              "args": ["mcp", "-sessions"]}}}
+```
+
 ## EasyCrypt proof strategy
 
 ### General approach