Knowledge-Compiler / Model-Counter Server Protocol

This page specifies KCMCP (Knowledge Compiler / Model Counter Protocol), a small, backend-agnostic wire protocol for talking to a warm, long-lived knowledge compiler or model counter over a stream socket. It is the protocol ProvSQL aims to use to call out to an external knowledge compiler or model counter: the same external tool it would otherwise invoke on the command line, reached through a more convenient, efficient, and expressive interface than spawning a fresh process and exchanging temporary files. The protocol is written so that one client and one server code path work regardless of which engine sits behind them (see Probability Evaluation for where such an external tool sits in the probability pipeline).

It is an alternative to the way ProvSQL invokes these tools today, in command-line mode: forking a fresh process, writing the problem to a temporary file, exec-ing the tool, and reading its output back from another temporary file on every call. KCMCP replaces that per-call process spawn and the temporary files with a single warm process and a socket round-trip, while keeping the command-line path as a fallback so the two modes coexist.

The protocol is designed from first principles around explicit framing and capability negotiation. It is the protocol ProvSQL aims to converge on; it does not depend on, and is not derived from, the wire format of any server that exists today.

Note

The standalone tdkc tool is a reference implementation of the server side. Run it with tdkc --kcmcp unix:/path/to.sock or tdkc --kcmcp host:port; it advertises compile (to ddnnf-nnf) and wmc (to decimal) over dimacs-cnf input, serving each request through ProvSQL’s in-process tree decomposition, and implements the cancel and progress features. It exists to exercise and pin the protocol; ProvSQL itself keeps tree decomposition in process rather than talking to it over a socket. test/kcmcp/conformance.py drives it through a handshake, compile/wmc requests, PING/PONG, and error cases (make kcmcp-tdkc-test).

Design goals

KCMCP is built to the following principles. Each is a positive requirement on any conformant implementation, stated without reference to any particular engine’s current behaviour:

Explicit, byte-order-defined framing. Every integer is unsigned big-endian; every variable-length payload is length-prefixed. A message boundary is never found by scanning for a sentinel character, so a partial recv is always unambiguous and content can never truncate a frame.
Location-independent transport. The protocol runs over any reliable, ordered byte stream, so the server may be co-located with the client (a Unix socket or a loopback connection) or reached across a network (a TCP connection to a configured host and port). Where the channel is not inherently trusted, securing it – a private network, an SSH tunnel, or a TLS proxy in front of the server – is a deployment concern, not part of this version of the protocol.
A warm, supervised, queueing server. One long-lived process accepts many connections in a loop and serves requests over a persistent connection, so a client pays no per-request process-spawn cost and a future cross-query cache has somewhere to live. Concurrent clients queue rather than being refused.
Robust to bad input. A malformed or unsupported request is answered with an ERROR frame; the server never terminates on it.
Capability negotiation. A client discovers what the connected backend supports through a handshake, rather than assuming a fixed feature set, so one client speaks to counters and compilers alike.
Operation- and format-neutral. Counting, weighted counting and knowledge compilation are selected by fields in the request, and the input and output encodings are negotiated numbers, so the same wire carries every engine’s job.

KCMCP mandates no particular operation or format. What a backend can do is exactly what it advertises at the handshake; a client and a backend interoperate when their advertised capabilities share at least one (operation, input_format, output_format) combination. The names of operations and formats are drawn from a shared registry (below), so that a given name means the same thing to both sides – but which of them any one tool implements is its own choice. A pure knowledge compiler that only reads a particular circuit format and only emits a compiled form is as conformant as a counter that reads DIMACS-CNF and returns a number. DIMACS-CNF is merely the most widely understood input and therefore a convenient common denominator, not a requirement. When two peers share no usable combination, the handshake makes that explicit and the client falls back (for ProvSQL: to another tool).

Transport

KCMCP runs over a reliable, ordered, byte-stream socket. Where the server runs is a deployment choice, not part of the protocol; an implementation MUST support at least one of the following:

Local, same host. A Unix domain socket (filesystem permissions are the access-control boundary, with no port to allocate or leak), or a loopback TCP endpoint. When a supervisor launches the server it MAY let the OS assign an ephemeral port (bind to port 0) and learn the chosen port from the child (for ProvSQL: a supervisor background worker writes it into shared memory, mirroring how provsql_mmap.c registers its worker and how provsql_shmem.h carries shared state).
Remote host. A TCP connection to a host and port the client is configured with. A single warm server can then serve several client machines.

KCMCP v1 defines no authentication or transport encryption, and places no requirement on the bind address. On a single trusted host the local boundary is the security model; for a remote server the channel must be secured out of band (a private network, an SSH tunnel, or a TLS proxy in front of the server).

The server runs an accept loop. How it schedules work across connections is left to the implementation: it MAY serve them sequentially in a single process – the intended posture for a warm cross-query cache, in which case concurrent clients queue on the socket – or handle several concurrently. The protocol does not constrain this.

Endpoint identification

The protocol defines no discovery mechanism: the endpoint – a Unix-socket path or a host:port – is communicated to the client out of band. For ProvSQL the supervisor background worker publishes the live loopback port in shared memory, and republishes it after a respawn, so a backend always reaches the current server; a remote deployment is configured with a fixed host:port; a Unix socket lives at a known path.

Because KCMCP v1 has no authentication, a client trusts whatever answers at the endpoint. The HELLO handshake is the sanity check: before sending a problem the client confirms it received a well-formed HELLO carrying a kcmcp version it can speak and the capabilities it needs. That establishes “this is a KCMCP server I can use”, but not which server – identity rests on the transport. A Unix socket guarded by filesystem permissions scopes who can reach it; a loopback TCP ephemeral port has a squatting / race window (another local process may connect, or bind the port before the server does). Prefer the Unix socket where the trust boundary matters.

Connection lifecycle

A KCMCP session uses one connection for its entire life: the client opens the socket once – a single TCP or Unix-socket connect – and that same connection carries the whole exchange. It is not a fresh connection, nor a fresh handshake, per request. Reconnecting per job would re-pay the connect and the HELLO round-trip and, worse, discard the warm cross-query cache that motivates having a server at all.

A session proceeds as:

Connect. The client opens the socket to the server’s endpoint.
Handshake. Each side sends exactly one HELLO (request_id = 0) and reads the other’s, fixing the protocol version and the capabilities for the rest of the connection. It is never repeated.
Work. The client issues any number of request/response cycles on the same connection – a REQUEST answered by a RESULT or an ERROR, optionally preceded by PROGRESS frames – correlating each by request_id. A job in progress can be aborted with a CANCEL carrying its request_id.
Idle. Between jobs, and throughout a long-running compile, the connection simply stays open with no data flowing. PING / PONG keep it alive on a link (for example a remote TCP path through a NAT or stateful firewall) that would otherwise drop an idle connection; a local Unix-socket or loopback connection needs no such keepalive.
Close. Either side ends the session with a BYE and closes the socket.

While the server is computing a REQUEST it keeps reading the connection, so it can act on control frames mid-job – aborting on CANCEL, answering a PING with PONG, and emitting PROGRESS – rather than going deaf until the RESULT is ready. A server that cannot interleave computation with this socket servicing says so by omitting cancel (and progress) from its advertised features; for such a server a running job is uninterruptible, and the client falls back to transport-level keepalive and its own timeout. How the server schedules work across connections – serialising it or running several jobs at once – is, by contrast, left to the implementation (see Transport).

If the connection drops unexpectedly – reset, idle timeout, or a server crash – any in-flight job is abandoned: the client reconnects, re-handshakes, and resubmits. For ProvSQL the supervisor background worker respawns a crashed server, so the next connect lands on a fresh process (with an empty cache).

Frame format

Every message in either direction is a frame: a fixed 10-byte header followed by an opaque, length-delimited payload. All multi-byte integers are unsigned big-endian (network byte order).

offset  size   field
------  -----  -----------------------------------------------------
  0     u8     type          message kind (see table below)
  1     u8     flags         bit0 MORE       payload continues in the
                                             next frame (same type and
                                             request_id)
                             bit1 COMPRESSED payload is zstd-compressed
                             bits2-7         reserved, MUST be 0
  2     u32    request_id    client-chosen correlation id;
                             0 = connection-scoped (no correlation)
  6     u32    payload_len   number of payload bytes that follow,
                             bounded by the advertised max_payload
 10     ...    payload[payload_len]

Carrying request_id in the header (rather than the payload) lets CANCEL, PROGRESS and RESULT frames reference an outstanding job without parsing its body, and leaves room to add request pipelining later without a format change. The MORE flag lets a large payload (a multi-megabyte d-DNNF RESULT, or an equally large REQUEST problem) stream as several frames sharing one request_id; the receiver concatenates their payloads in order until it sees a frame with MORE clear. MORE works in either direction and is the mechanism for sending a payload larger than the receiver’s per-frame limit: the sender splits it into frames each within that limit.

A receiver MUST reject (with an ERROR frame, code 7) any frame whose payload_len exceeds the max_payload it advertised at handshake, rather than attempting to allocate it. To guarantee a usable baseline, every implementation MUST accept a single frame whose payload is up to 1 MiB (1048576 bytes); accordingly a server’s advertised max_payload MUST be at least 1 MiB. A sender MUST NOT exceed the receiver’s limit – the advertised max_payload, or the 1 MiB floor for a peer that advertises none (i.e. the client) – and splits anything larger across MORE-flagged frames within that limit.

KCMCP v1 negotiates no payload compression, so a receiver need not support the COMPRESSED flag (bit 1). A sender MAY nonetheless set it optimistically: a receiver that cannot decode the payload drains it – its length is bounded by max_payload, so the stream stays synchronised – and replies with an ERROR of code 9 on the same connection, rather than mis-reading the bytes as plain. The sender then retries the frame uncompressed; the ERROR is the fallback signal, so the exchange doubles as a (coarse) compression negotiation. A future revision may instead advertise compression support as a feature, letting a client skip the trial.

Message types

Value	Name	Meaning
`0x00`	`HELLO`	Handshake; sent once by each side (`request_id = 0`).
`0x01`	`REQUEST`	A counting or compilation job.
`0x02`	`RESULT`	A successful answer to a `REQUEST`.
`0x03`	`ERROR`	A job-level or protocol-level failure.
`0x04`	`PROGRESS`	Optional liveness / log update for a long-running job.
`0x05`	`CANCEL`	Abort the job named by `request_id`.
`0x06` / `0x07`	`PING` / `PONG`	Connection keepalive.
`0x08`	`BYE`	Graceful connection close.

A server MUST reply to an unknown type with an ERROR frame (code 1) and keep the connection open; it MUST NOT terminate.

Handshake: `HELLO`

Immediately after the connection is established each side sends exactly one HELLO frame with request_id = 0. The payload is UTF-8 JSON: control metadata stays human-readable and freely extensible, while only the heavy problem and result payloads are binary.

The client announces the protocol version it understands:

{ "kcmcp": [1, 0], "client": "ProvSQL/1.8.0" }

Client HELLO fields:

Field	Type	Meaning
`kcmcp`	two-element array `[major, minor]` of integers	Required. The protocol version the client implements: `major` is bumped only for breaking changes, `minor` for backward-compatible revisions. The server selects a version no newer than this (see the server `kcmcp` field below).
`client`	string, `name/version` or bare `name`	Optional. Client identifier, surfaced in the server’s logs and diagnostics only. Either a `name/version` string (e.g. `ProvSQL/1.8.0`) or a bare `name` with no `/` when no version is reported. Never used for negotiation, so the server treats any value (or its absence) identically.

The server replies with the negotiated version and a capability descriptor – the object that makes the protocol generic:

{ "kcmcp": 1,
  "engine": "example-kc/1.0",
  "max_payload": 268435456,
  "operations":     ["count", "wmc", "compile"],
  "input_formats":  ["dimacs-cnf", "circuit-bcs12"],
  "output_formats": { "count":   ["decimal", "rational"],
                      "compile": ["ddnnf-nnf"] },
  "features":       ["cancel", "progress", "persistent-cache"] }

Server HELLO fields (the capability descriptor):

Field	Type	Meaning
`kcmcp`	integer	Required. The major protocol version the server selected for this connection; never greater than the client’s `major`. A client that cannot speak it closes the connection and falls back. Because a `major` bump is a breaking change, there is no shared version when the client’s `major` exceeds every `major` the server implements: the server does not silently downgrade but replies with an `ERROR` of code `8` and closes, and the client falls back.
`engine`	string, `name/version` or bare `name`	Optional. Identifies the backend knowledge compiler / model counter the server drives – not the KCMCP server process itself (the two coincide only when the server is the engine). For the client’s logs and diagnostics only; not used for negotiation. Either a `name/version` string (e.g. `example-kc/1.0`) or a bare `name` with no `/`.
`max_payload`	integer (bytes)	Optional; an implementation-defined default (at least the 1 MiB floor) applies when absent. The largest `payload_len` the server will accept in a single frame; it MUST be at least 1 MiB (1048576). A client MUST NOT send a frame exceeding it (splitting larger problems with `MORE`), and the server rejects an oversize frame with an `ERROR` of code `7`.
`operations`	array of strings	Required. The operation names the server can perform, drawn from the operation registry (`count`, `wmc`, `compile`, …). Any subset is valid, including a single entry.
`input_formats`	array of strings	Required. The problem input-format names the server accepts, drawn from the input-format registry (`dimacs-cnf`, `circuit-bcs12`, …).
`output_formats`	object mapping each operation name to an array of strings	Required. For every operation the server offers, the output-format names valid for it. Its keys are a subset of `operations`; its values are drawn from the output-format registry (`decimal`, `rational`, `ddnnf-nnf`, …).
`features`	array of strings	Optional. Protocol capabilities the server implements beyond the mandatory core: currently `cancel` (reads and honours a `CANCEL` while a job is running, which requires servicing the connection mid-job), `progress` (may emit `PROGRESS` frames during a job), and `persistent-cache` (retains its solver cache across requests). A client uses only the features listed here; an absent feature is treated as unsupported – in particular, without `cancel` a running job cannot be aborted.

A client and a server interoperate when, for some operation the client needs, that operation is in operations, the input encoding the client will send is in input_formats, and the output encoding it wants is in output_formats for that operation. Both directions are extensible: a receiver MUST ignore any field it does not recognise, so later versions can add fields without a version bump (see Forward compatibility under Design notes and non-goals).

No entry is required: the operations, input_formats and output_formats sets are each free. A counter that lists just "count" over "dimacs-cnf" and a knowledge compiler that lists just "compile" over some circuit format are each fully conformant – a client simply uses whichever advertises a combination it can work with, and otherwise falls back.

`REQUEST` payload

offset  size   field
------  -----  -----------------------------------------------------
  0     u8     operation      0 count  1 wmc  2 compile
                              3 enumerate  4 sample  ...
  1     u8     input_format   0 dimacs-cnf  1 circuit-bcs12  2 aig ...
  2     u8     output_format  0 decimal 1 rational 2 double 3 bigint
                              4 ddnnf-nnf 5 sdd 6 obdd ...
                              (one shared code space; an operation
                               accepts only the subset listed for it)
  3     u8     reserved (0)
  4     u16    options_len
  6     ...    options[options_len]   UTF-8 JSON object (see Options)
 ...    ...    problem[ rest ]        the formula bytes;
                                      length = payload_len - 6 - options_len

The problem block is exactly the bytes a backend already parses with no \0 or z sentinel needed. (A backend MAY still tolerate a trailing sentinel for source-compatibility with existing DIMACS parsers; it just is not the framing mechanism.)

Format-orthogonal knobs – weights, the projection set, a time budget, an RNG seed – live in the options block rather than being smuggled into problem, so the problem stays a clean formula.

Options

The options block is a UTF-8 JSON object – the same encoding as the HELLO descriptor and the RESULT meta – and an empty block (options_len = 0) is equivalent to {}. A receiver MUST ignore any member it does not recognise: this is how method-specific extensions ride along safely – the server applies the members it knows and silently drops the rest, so a client may always send an option a given backend may or may not act on.

The basic members, which every implementation interprets identically:

Member	JSON type	Applies to	Meaning
`timeout_ms`	integer	all operations	Wall-clock budget in milliseconds for the job. `0` or absent means no limit. On exceeding it the server stops and returns an `ERROR` of code `4`.
`progress_every_ms`	integer	servers advertising `progress`	Minimum interval in milliseconds between `PROGRESS` frames for the job. `0` emits one on every internal progress check; absent leaves the cadence to the server. Ignored by a server that does not advertise the `progress` feature.
`seed`	integer	randomised operations	Seed for the engine’s RNG (e.g. `sample` or approximate counting). Absent leaves the choice to the engine, which may then be non-deterministic.
`projset`	array of integers	`count`, `wmc`	The projection (relevant) variable set, as positive variable indices: the count ranges over assignments to these variables only. Absent means no projection, i.e. the ordinary count over all variables.
`weights`	object: literal name to number	`wmc`	Per-literal weights, keyed by the DIMACS literal as a string (a signed, non-zero integer: `"5"` and `"-5"` are variable 5 set true and false). A literal with no entry defaults to weight `1`. For many weights a weighted input format carries them more compactly.

An example block:

{ "timeout_ms": 30000,
  "projset": [3, 7, 9],
  "weights": { "5": 0.3, "-5": 0.7 },
  "seed": 42 }

Engine-specific tuning – a backend’s solver, preprocessing, branching / scoring / phase heuristics, cache strategy, and the like – is carried as namespaced members, so it never collides with the basic keys and is dropped by other engines under the ignore-unknown rule. By convention such options live in an object keyed by the engine name (the name part of the server’s HELLO engine field): a server applies the sub-object matching its own engine and ignores the rest. This lets a client drive every knob the backend exposes. For a d4-family backend, for instance, the important d4v2 command-line options map directly onto members of a d4 object (its --input-type and --dump-file are already covered by input_format and the compile operation, and its preprocessing timeout by timeout_ms):

{ "timeout_ms": 30000,
  "d4": { "preproc": "vivification",
          "solver": "glucose",
          "scoring-method": "vsads",
          "branching-heuristic": "hybrid-partial-classic",
          "phase-heuristic": "polarity",
          "cache-method": "list",
          "float": false } }

`RESULT` payload

A RESULT carries the same request_id as its REQUEST.

offset  size   field
------  -----  -----------------------------------------------------
  0     u8     result_format  echoes the requested output_format
  1     u8     reserved (0)
  2     u16    meta_len
  4     ...    meta[meta_len]   UTF-8 JSON statistics
 ...    ...    result[ rest ]   encoded per result_format
                                (see Output formats)

The meta channel is where the protocol earns its generality. An exact counter or compiler returns timing and structural statistics; an approximate counter returns the same frame shape with a confidence interval instead:

{ "time_ms": 41, "nodes": 1278, "cache_hits": 904, "exact": true }

{ "time_ms": 5200, "exact": false, "ci": [1.01e6, 1.07e6], "delta": 0.05 }

Clients that do not care about meta ignore it and read only result. Because result is length-framed (and MORE-chunked when large), a fixed-size read buffer can never truncate it.

Operation and format registries

The operation, input_format and output_format bytes of a REQUEST, and the matching operations / input_formats / output_formats names in the HELLO descriptor, are drawn from these shared registries – the numeric codes are the on-wire REQUEST values, the names are the HELLO strings. KCMCP v1 specifies the entries below; any other value is reserved for future use, and a peer that does not recognise one rejects the request with an ERROR (code 1 for an operation, 2 for a format).

Operations

Code	Name	Meaning
`0`	`count`	Unweighted model count: the number of satisfying assignments of the input problem, a non-negative integer. A projection set, if any, is given in `options`.
`1`	`wmc`	Weighted model count: the sum, over satisfying assignments, of the product of per-literal weights. Weights come from `options` (or from the problem itself for a weighted input format).
`2`	`compile`	Knowledge compilation: transform the input into a tractable target representation, selected by `output_format`, and return that representation rather than a number.

enumerate and sample appear in the byte-layout example as reserved codes; v1 does not specify them.

Input formats

Code	Name	Meaning	Reference
`0`	`dimacs-cnf`	A CNF in DIMACS form, optionally carrying the weight (`c p weight`) and projection (`c p show`) lines used for `wmc` and projected counting. The interoperability baseline.	Model Counting Competition format
`1`	`circuit-bcs12`	A Boolean circuit in d4’s BC-S1.2 form (AND / OR / identity gates over input literals); ProvSQL emits this to preserve circuit structure instead of flattening to CNF.	jm62300/d4

aig appears in the byte-layout example as a reserved code; v1 does not specify it.

Output formats

output_format is a single code space shared by every operation: each code below is globally unique and is not reused across operations, so a result_format byte names exactly one encoding regardless of the operation that produced it. An operation accepts only the subset that makes sense for it – the number encodings 0–3 for count and wmc, the compiled representations 4–… for compile. The result bytes of a RESULT are encoded exactly as the code prescribes, and result_format echoes the code so the client knows how to decode them.

For count and wmc the result is a number; its wire encoding is specified precisely (text is US-ASCII, binary is big-endian / network byte order, consistent with the frame header):

Code	Name	Wire encoding
`0`	`decimal`	Text. A base-10 real, matching `[-]?digit+ ( '.' digit+ )? ( [eE] [-+]? digit+ )?` in US-ASCII. Precision is engine-dependent, so not necessarily exact for `wmc` (use `rational` or `bigint` when exactness matters). The interoperability baseline.
`1`	`rational`	Text. The exact value as `numerator/denominator`: two base-10 integers separated by a single `/`, the denominator strictly positive, no spaces (an integer count uses denominator `1`). Lossless.
`2`	`double`	Binary. The value as one IEEE-754 `binary64`, exactly 8 bytes, big-endian. Compact and fixed-width but lossy.
`3`	`bigint`	Binary. An exact non-negative integer (e.g. an unweighted `count` exceeding 64 bits) as its raw magnitude bytes, big-endian (most-significant byte first), no leading `0x00` except the single byte `0x00` for the value zero. Length is the frame’s.

For compile the result is a compiled representation:

Code	Name	Wire encoding	Reference
`4`	`ddnnf-nnf`	Text. A d-DNNF in the c2d / d4 NNF format (one node or arc per line); the form ProvSQL parses back for linear-time probability evaluation.	c2d, jm62300/d4

sdd (5) and obdd (6) appear in the byte-layout example as reserved codes; v1 does not specify them.

Errors, cancellation, and liveness

`ERROR`

Payload: u16 code followed by a UTF-8 message. Defined codes:

Code	Meaning
`1`	unsupported operation or unknown frame `type`
`2`	unsupported input / output format
`3`	parse error in the `problem` block
`4`	time budget exceeded
`5`	cancelled at client request
`6`	internal engine error
`7`	payload over `max_payload` / out of memory
`8`	unsupported protocol version (client requires a `major` the server does not implement; see Handshake)
`9`	`COMPRESSED` payload the server cannot decode (compression is not negotiated in v1)

Crucially, sending an ERROR never terminates the process: the accept loop keeps running for new connections. Whether the same connection survives depends on the error’s level:

Recoverable errors leave the byte stream synchronised, so the server returns the ERROR and keeps serving the connection. These are a malformed or unsupported REQUEST (codes 1–6, the offending frame having been read in full) and a COMPRESSED payload the server cannot decode (code 9): its length is bounded by max_payload, so the server drains it and the peer retries uncompressed in-band.
Fatal (framing- or handshake-level) errors leave the stream unresynchronisable, so the server MAY return the ERROR and then close that connection: a frame larger than max_payload (code 7, undrainable by definition), an unsupported protocol version (code 8, at the handshake), or any otherwise unreadable / desynchronised frame. The client then reconnects and re-handshakes.

`CANCEL`

A CANCEL frame whose request_id names the running job asks the server to abort it. The server invokes its engine’s interrupt hook and replies with ERROR code 5. Honouring it requires the server to keep reading the connection while the job computes; a server that cannot does not advertise the cancel feature, and its jobs run uninterruptibly to completion. This is the wire-level counterpart of the cancel-polling the ProvSQL client must already do: the socket client honours CHECK_FOR_INTERRUPTS() and statement_timeout while waiting, mirroring the cancel discipline in external_tool.cpp.

`PROGRESS`

A server that advertised progress MAY emit PROGRESS frames (carrying the running job’s request_id) while it works on a job. PROGRESS is first of all a liveness signal, not a quantified completion measure: for the search-based counting and knowledge compilation these backends do, there is no reliable “percent done”, so the protocol does not mandate one. Its payload is a free-form UTF-8 JSON object, engine-defined; the client treats it as opaque – surfacing it for display or logging, and using its arrival to confirm the job is alive and to re-arm its deadline – and MUST NOT require any particular member. An empty object {} is a valid bare heartbeat.

A server MAY include any of these optional, well-known members, which a client MAY surface if present but MUST NOT depend on:

Member	JSON type	Meaning
`phase`	string	A coarse, engine-defined stage label (e.g. `"preprocess"`, `"compile"`), shown to the user verbatim.
`elapsed_ms`	integer	Wall-clock milliseconds since the job started; monotonic.
`message`	string	A human-readable status line.
`fraction`	number in [0, 1]	A best-effort completion estimate. Advisory only: it is often unavailable or non-monotonic for these problems, so it may be absent and a client must never treat it as authoritative.

A server SHOULD rate-limit PROGRESS (for example at most one every few seconds) so it stays a heartbeat rather than a flood.

`PING` / `PONG` / `BYE`

PING / PONG keep an idle warm connection alive. BYE closes it gracefully.

A worked exchange

One connection that counts, then – after an idle keepalive – compiles, the CNF $x_1 \vee x_2$ over three variables (p cnf 3 1 / 1 2 0). Every frame is shown in full – the 10-byte header fields followed by the complete payload – with no elision. The model count and the d-DNNF are the actual output of a d4v2 backend on this input (s 6 and a three-node d-DNNF); integer header fields are big-endian, and payload_len is the exact byte count of the payload shown.

C -> S  HELLO     type=0x00 flags=0x00 request_id=0  payload_len=40
        payload (JSON, 40 bytes):
          {"kcmcp":[1,0],"client":"ProvSQL/1.8.0"}

S -> C  HELLO     type=0x00 flags=0x00 request_id=0  payload_len=219
        payload (JSON, 219 bytes, one line):
          {"kcmcp":1,"engine":"example-kc/1.0","max_payload":1048576,"operations":["count","compile"],"input_formats":["dimacs-cnf"],"output_formats":{"count":["decimal"],"compile":["ddnnf-nnf"]},"features":["cancel","progress"]}

C -> S  REQUEST   type=0x01 flags=0x00 request_id=1  payload_len=24
        payload (24 bytes):
          operation     = 0   (count)
          input_format  = 0   (dimacs-cnf)
          output_format = 0   (decimal)
          reserved      = 0
          options_len   = 2
          options       = {}                          (2 bytes)
          problem       = "p cnf 3 1\n1 2 0\n"         (16 bytes)

S -> C  RESULT    type=0x02 flags=0x00 request_id=1  payload_len=31
        payload (31 bytes):
          result_format = 0   (decimal)
          reserved      = 0
          meta_len      = 26
          meta          = {"time_ms":2,"exact":true}
          result        = "6"                          (1 byte, the count)

(the connection sits idle; the client sends a keepalive)

C -> S  PING      type=0x06 flags=0x00 request_id=0  payload_len=0
        (no payload)

S -> C  PONG      type=0x07 flags=0x00 request_id=0  payload_len=0
        (no payload)

C -> S  REQUEST   type=0x01 flags=0x00 request_id=2  payload_len=24
        payload (24 bytes):
          operation     = 2   (compile)
          input_format  = 0   (dimacs-cnf)
          output_format = 4   (ddnnf-nnf)
          reserved      = 0
          options_len   = 2
          options       = {}
          problem       = "p cnf 3 1\n1 2 0\n"         (16 bytes)

S -> C  RESULT    type=0x02 flags=0x00 request_id=2  payload_len=68
        payload (68 bytes):
          result_format = 4   (ddnnf-nnf)
          reserved      = 0
          meta_len      = 21
          meta          = {"nodes":3,"edges":3}
          result        = (43 bytes, the d-DNNF d4v2 dumped):
            o 1 0
            o 2 0
            t 3 0
            2 3 1 0
            2 3 -1 2 0
            1 2 0

C -> S  BYE       type=0x08 flags=0x00 request_id=0  payload_len=0
        (no payload)

The same two frame types serve “count to a decimal” and “compile to a d-DNNF”; only the operation and output_format bytes differ. That is the central property: transport, framing, handshake, error and cancellation are all independent of whether the backend counts or compiles, and of which engine implements it.

ProvSQL’s client and managed server

ProvSQL is a KCMCP client: when a knowledge-compilation request selects a tool registered with kind = 'kcmcp' (see the tool registry), BooleanCircuit::compilation() compiles over a socket through the in-extension client (kcmcp_client.cpp) instead of spawning a CLI process. It serialises the problem exactly as the CLI path does (a Tseytin CNF, or a BC-S1.2 circuit when the record advertises circuit-bcs12), sends one compile REQUEST, and parses the ddnnf-nnf RESULT back with the same parseDDNNF the temp-file path uses – so results are identical and any failure (connect, protocol, server ERROR) falls back to the CLI path.

The client honours the protocol’s connection-for-life rule: it keeps one connection per backend, keyed by endpoint, reusing it across compilations so a warm server’s cross-query cache is not discarded (today it also just saves the per-compile connect + handshake). A reused connection that has gone stale (the server respawned, or an idle link dropped) is transparently reconnected once; a query cancel or statement_timeout closes the socket so the server abandons the job, mirroring the cancel discipline of the CLI path; and an on_proc_exit hook sends BYE at backend exit.

A kcmcp record’s endpoint is either a fixed address (unix:/path or host:port – endpoint mode, a server operated out of band) or the literal managed, resolved at compile time to the address of a server ProvSQL itself runs.

Managed server. A dedicated supervisor background worker (kcmcp_supervisor.c, registered alongside the mmap worker) owns the managed server’s lifecycle. When provsql.kcmcp_server is non-empty it is a shell command with a {endpoint} placeholder; the worker substitutes a Unix-socket path it chooses, forks/execs the command in its own process group, publishes the endpoint in shared memory (read by the client for an endpoint = 'managed' record), and supervises it – relaunching on exit, restarting a changed command on SIGHUP, idling on its latch when the GUC is empty, and killing the process group on shutdown. The worker needs only BGWORKER_SHMEM_ACCESS (no database): the command is a process-global GUC and the endpoint lives in the shared segment, which is why a cluster-level GUC – not a per-database registry column – carries it.

Design notes and non-goals

No framing by sentinel. Length prefixes everywhere; the z sentinel of the DIMACS dialect is tolerated inside problem but is never how a message boundary is found.
Forward compatibility. New operations, formats and features are added by extending the registries and the HELLO JSON. Receivers reject unknown frame types and formats with an ERROR, never by crashing, so a newer client and an older server degrade predictably.
Concurrency. Per connection there is one in-flight REQUEST at a time (the request_id field is already present so that pipelining or multiplexing can be added later under a feature flag without a wire change), but the server still services control frames on that connection while the job computes (see Connection lifecycle). How it schedules work across connections – serialise or run concurrently – is left to the implementation; the protocol does not constrain it.
Out of scope for v1: authentication, transport encryption, and persistent cross-query caching. A remote server is supported at the transport level, but securing the channel to it is left to the deployment (see Transport). Persistent caching is contingent on upstream engine support; the warm, serialized, single-process server is the prerequisite that lets it be exploited for free if and when it lands.