Proposal: JSON-RPC over stdin/stdout for subprocess integration

[frankhsueh]

Proposal: JSON-RPC over stdin/stdout for subprocess integration

I'd like to propose adding a stdio transport for Apalache's JSON-RPC API.

The intended use case is applications that embed Apalache as a local child process rather than operate it as an independently managed network service.

Today, such an application needs to:

1. spawn the Apalache server,
2. allocate/configure a TCP port,
3. wait for server readiness,
4. establish a network connection,
5. manage the server's lifecycle, and
6. ensure the server is terminated when the parent exits.

For a child-process integration, this adds complexity without providing much benefit from the network transport.

Proposed interface

For example:

apalache-mc server --stdio

or:

apalache-mc json-rpc --stdio

The process would use:

stdin   JSON-RPC requests
stdout  JSON-RPC responses
stderr  diagnostics/logging

The RPC methods and semantics would remain the same as the existing JSON-RPC server; only the transport would change.

Conceptually:

parent application
       │
       │ stdin/stdout
       ▼
    Apalache
       │
       ▼
 solver/session

Motivation

This would make Apalache substantially easier to embed in tools that want a private verifier process.

Advantages include:

• no port allocation or discovery;
• no readiness/connect race;
• no port collisions;
• no networking, firewall, or container concerns;
• simple parent/child process ownership;
• straightforward lifecycle management;
• usable from essentially any programming language;
• easy manual testing and debugging.

The existing network transports would remain useful for independently managed, shared, or remote Apalache servers. Stdio would be complementary, optimized for the local subprocess case.

Framing

The simplest framing would be newline-delimited JSON (NDJSON):

{"jsonrpc":"2.0","id":1,"method":"...","params":{...}}\n
{"jsonrpc":"2.0","id":1,"result":{...}}\n

Alternatively, a length-prefixed framing such as LSP's Content-Length scheme could avoid relying on newline-delimited messages.

This proposal does not require introducing a new RPC API. It reuses the existing JSON-RPC API and adds stdio as another transport.

[konnov]

Hi @frankhsueh!

This is an interesting proposal. Do you have a concrete use case that needs this?