runtimeverification · RaoulSchaffranek · Jul 23, 2026 · Jul 23, 2026
diff --git a/README.md b/README.md
@@ -224,7 +224,7 @@ Common tasks are driven by `make` (see the [Makefile](Makefile) for the complete
 To build the node from source use:
 
 ```bash
-make build-kdist
+make kdist-build
 make build
 pip install dist/*.whl
 ```

diff --git a/docs/architecture.md b/docs/architecture.md
@@ -45,13 +45,13 @@ flowchart TB
 
 ### `server.py` — `StellarRpcServer`
 
-`StellarRpcServer` is the long-running process around the semantics: a plain `http.server.HTTPServer` that keeps the HTTP socket open and the state files on disk across requests — the networking and persistence the one-shot K interpreter has no notion of. It receives JSON-RPC requests, uses `TransactionEncoder` to turn a transaction into a request envelope, hands the envelope to `NodeInterpreter`, and returns the `response.json` the semantics produced. It holds **no** ledger counter, receipt store, or response-formatting logic — those live in K.
+`StellarRpcServer` is the long-running process around the semantics: a plain `http.server.HTTPServer` that keeps the HTTP socket open across requests — the networking the one-shot K interpreter has no notion of. It receives JSON-RPC requests, uses an `Encoder` to turn a transaction into a request envelope, hands the envelope to an `Interpreter`, and returns the `response.json` the semantics produced. It holds **no** ledger counter, receipt store, or response-formatting logic — those live in K — and it reaches the on-disk artifacts through a `Store` rather than touching paths itself.
 
-`handle_rpc(method, params, id)` is the dispatch entry point and is usable without the HTTP layer (scripts, tests).
+The three collaborators (`Encoder`, `Interpreter`, `Store`) are injected as the protocols declared in `interfaces.py`, not as their concrete classes, so a test can substitute fakes; `build_server` in `__main__.py` wires up the concretes. `handle_rpc(method, params, id)` is the dispatch entry point and is usable without the HTTP layer (scripts, tests).
 
 → **[Detailed documentation](server.md)**
 
-The server implements eleven RPC methods — `getHealth`, `getNetwork`, `getLatestLedger`, `getVersionInfo`, `getFeeStats`, `sendTransaction`, `getTransaction`, `getTransactions`, `getLedgers`, `getLedgerEntries`, and the komet-specific `traceTransaction` extension — and the K semantics answer all of them. JSON-RPC framing (single calls, batch arrays, notifications) is handled in Python; the semantics see one request envelope per invocation. For `getLedgerEntries` the semantics' answer is an intermediate shape: K performs the state lookups, and `ledger_entries.py` translates between the base64 XDR wire format (`LedgerKey` in, `LedgerEntryData` out) and the JSON the semantics exchange, since K cannot parse or produce XDR.
+The server implements thirteen RPC methods — `getHealth`, `getNetwork`, `getLatestLedger`, `getVersionInfo`, `getFeeStats`, `sendTransaction`, `simulateTransaction`, `getTransaction`, `getTransactions`, `getLedgers`, `getLedgerEntries`, `getEvents`, and the komet-specific `traceTransaction` extension — and the K semantics answer all of them. JSON-RPC framing (single calls, batch arrays, notifications) is handled in Python; the semantics see one request envelope per invocation. For `getLedgerEntries` the semantics' answer is an intermediate shape: K performs the state lookups, and `ledger_entries.py` translates between the base64 XDR wire format (`LedgerKey` in, `LedgerEntryData` out) and the JSON the semantics exchange, since K cannot parse or produce XDR.
 
 `sendTransaction` always returns `PENDING` and clients poll `getTransaction` for the result — matching the Stellar RPC async pattern even though the transaction executes synchronously. See [server.md](server.md) for details.
 
@@ -73,6 +73,12 @@ The server implements eleven RPC methods — `getHealth`, `getNetwork`, `getLate
 
 ---
 
+### `store.py` — `ChainStore`
+
+`ChainStore` owns the io-dir layout: it knows the paths, the file-naming conventions, and the JSON shapes, and it is the only component that reads or writes them. The server holds one and asks it for receipts, ledgers, events, and the ledger counter. It is the concrete `Store` the server depends on through the [io-dir table below](#the-io-dir).
+
+---
+
 ### `kdist/node.md` — K Semantics
 
 `node.md` is the K module compiled into the LLVM binary. It implements the whole RPC layer on the K side: it reads `request.json`, dispatches on the `method` field, reads and updates `metadata.json` and the per-transaction `receipts/` files, executes transaction steps via KASMER, and writes the JSON-RPC `response.json`. KASMER is the Komet execution harness whose `Step`s — `setAccount`, `deployContract`, `callTx`, `uploadWasm` — carry out the Soroban operations a transaction decodes into.
@@ -89,7 +95,7 @@ All of the server's input and output artifacts live in one directory, the *io di
 |---|---|---|---|
 | `state.kore` | persistent | `NodeInterpreter` | the full K world-state configuration — accounts, contract code (including uploaded wasm `ModuleDecl`s), contract storage, ledger metadata — serialized in KORE. Read before each run and rewritten after a successful one. |
 | `metadata.json` | persistent | the K semantics | `{"latest_ledger": N}` — the server ledger counter, bumped by 1 per committed transaction. |
-| `receipts/receipt_<hash>.json` | persistent | the semantics and the server (on success — the server rewrites the semantics' internal `returnValue` field into `resultXdr`/`resultMetaXdr`), or the server alone (on failure) | one stored receipt per transaction, keyed by tx hash, answering `getTransaction`. Each is `{status, ledger, createdAt, envelopeXdr, resultXdr, resultMetaXdr?}`. |
+| `receipts/receipt_<hash>.json` | persistent | the semantics and the server (on success — the server rewrites the semantics' internal `returnValue` field into `resultXdr`/`resultMetaXdr`), or the server alone (on failure) | one stored receipt per transaction, keyed by tx hash, answering `getTransaction`. Each is `{status, applicationOrder, feeBump, envelopeXdr, resultXdr, ledger, createdAt, resultMetaXdr?}`. |
 | `traces/trace_<hash>.jsonl` | persistent | the semantics | one execution trace per transaction, keyed by tx hash — the instruction-level records, one JSON object per line. `traceTransaction` returns these records as a JSON array. |
 | `ledgers/ledger_<seq>.json` | persistent | the server (on success) | one record per closed ledger — `{sequence, txHash, closedAt, hash, headerXdr, metadataXdr}` — the ledger→transaction index behind `getTransactions` and `getLedgers`. Written in Python because the header artifacts are XDR, which K cannot construct. |
 | `requests/request_<n>.json` | persistent | the server | an archive of each incoming JSON-RPC request, numbered by a monotonic counter, kept for debugging. |
@@ -106,7 +112,7 @@ The world state stays in KORE (rather than a JSON snapshot) because an uploaded
 ```mermaid
 flowchart TB
     boot(["server start"]) --> exists{"state.kore exists?"}
-    exists -->|"no"| init["empty_config() builds the idle K config in KORE<br/>write state.kore · seed metadata.json {latest_ledger: 0}<br/>create receipts/ traces/ requests/ wasms/"]
+    exists -->|"no"| init["empty_config() builds the idle K config in KORE<br/>write state.kore · seed metadata.json {latest_ledger: 0}<br/>create receipts/ traces/ ledgers/ requests/ wasms/ events/"]
     exists -->|"yes"| reuse["use existing state.kore<br/>seed metadata.json if missing · ensure artifact dirs exist"]
     init --> ready(["ready for requests"])
     reuse --> ready

diff --git a/docs/interpreter.md b/docs/interpreter.md
@@ -36,7 +36,7 @@ The result is the empty idle K configuration — no accounts, no contracts, no s
 
 The run happens in a throwaway empty directory on purpose. The idle configuration ends with empty `<k>`/`<program>` cells, which is exactly the precondition that makes the request-handling rule fire if a `request.json` is present. Running in an empty directory guarantees no stray `request.json` is picked up and dispatched into the configuration that is about to be saved as `state.kore`.
 
-### `run(state_file, io_dir, request, program_steps=None)`
+### `run(state_file, io_dir, request, program_steps=None, *, commit=True)`
 
 `run` is the main entry point. It runs a single RPC request envelope through the following steps:
 
@@ -46,6 +46,8 @@ The run happens in a throwaway empty directory on purpose. The idle configuratio
 4. Run the interpreter with its subprocess working directory set to `io_dir` (so the K file-system hooks resolve the relative paths `request.json`, `response.json`, `metadata.json`, and the `receipts/` and `traces/` files). The directory is set on the subprocess only — the server's own process never `chdir`s, so concurrent requests in other threads are unaffected.
 5. If the semantics wrote `response.json`, persist the new configuration to `state.kore` and return the response text. If not, the transaction got stuck (failed) — leave `state.kore` unchanged and return `None`, so the caller can synthesise a failure response.
 
+`commit` defaults to `True`. Pass `commit=False` to run a request without persisting its result: the response text is still returned, but the new configuration is discarded and `state.kore` is left unchanged even on success. `simulateTransaction` uses this to execute a dry run against the current world state without advancing the chain.
+
 ### `_inject_program(pattern, steps)` — the wasm-upload path
 
 A wasm upload cannot be expressed as a JSON step, because the resulting `ModuleDecl` (the parsed Wasm AST from `wasm2kast`) has no JSON form. Instead the steps are injected directly into the `<program>` cell of the already-parsed configuration, so KASMER runs them before the request is dispatched.

diff --git a/docs/node-semantics.md b/docs/node-semantics.md
@@ -188,7 +188,7 @@ Tracing is always on. Before running the steps, `#enableTrace` clears the transa
 **Trace format** (one JSON record per line):
 
 ```json
-{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}}
+{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}, "mem": null}
 ```
 
 | Field | Description |
@@ -197,6 +197,9 @@ Tracing is always on. Before running the steps, `#enableTrace` clears the transa
 | `instr` | Instruction name and operands as a JSON array |
 | `stack` | Value stack at instruction entry, as `[type, value]` pairs |
 | `locals` | Local variable bindings, keyed by index, as `[type, value]` pairs |
+| `mem` | Linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot) |
+
+Instruction records are one of several trace record kinds (`callContract`, `hostCall`, `contractData`, and `endWasm` are the others); see the [Trace a transaction](../README.md#trace-a-transaction) section of the README for all five.
 
 ---
 

diff --git a/docs/notes.md b/docs/notes.md
@@ -43,7 +43,7 @@ The tests do not yet cover `bytes` / `address` SCVal arguments or `SCVec` / `SCM
 - `sendTransaction`'s `errorResultXdr` is always a generic `txMALFORMED` result (no per-cause codes such as `txBAD_SEQ` — sequence numbers, fees, and signatures are not modelled), and `diagnosticEventsXdr` is never populated (both fields are optional in the spec). `TRY_AGAIN_LATER` is never returned by design: it signals mempool backpressure, which cannot arise in a synchronous node without a mempool.
 - `SCVec` / `SCMap` contract arguments are not yet encoded.
 - The `xdrFormat` parameter is accepted on `getTransaction`, `sendTransaction`, `getTransactions`, `getLedgers`, `getLedgerEntries`, and `getEvents`, but only the default `'base64'` is supported; `'json'` is rejected with `-32602`.
-- `simulateTransaction` only simulates invoke-contract host functions (not uploads/deploys); `auth` is always empty, `minResourceFee`/`transactionData` are synthetic constants, and `events`/`restorePreamble`/`stateChanges` and the `resourceConfig`/`authMode`/`xdrFormat` parameters are not supported. `ScMap` return values are not yet encoded.
+- `simulateTransaction` only simulates invoke-contract host functions (not uploads/deploys); `auth` is always empty, `minResourceFee`/`transactionData` are synthetic constants, and `events`/`restorePreamble`/`stateChanges` and the `resourceConfig`/`authMode`/`xdrFormat` parameters are not supported.
 - `getEvents` serves contract events only: `system` events are never emitted (the semantics have no source of them), and events whose topics/data have no staging representation (maps, errors, 256-bit ints) are dropped with a warning.
 - TTL/footprint operations are not implemented.
 - `getFeeStats` reports constant distributions (there is no fee market); only its `latestLedger` is live.