docs: overhaul documentation and ignore runtime artifacts

Refine README, docs/, and in-code comments for clarity and accuracy:
remove a self-referential link, correct the "empty state.kore"
description, drop a filler preamble, and clarify that json.md is K's
built-in module. Ignore the server/interpreter runtime artifacts
(state.kore, metadata.json, transactions.json, response.json,
trace.jsonl) so they no longer show up as untracked.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: RaoulSchaffranek

.gitignore

@@ -2,3 +2,10 @@
 __pycache__/
 .coverage
 .direnv/
+
+# Runtime artifacts written by the server / interpreter in the io dir
+metadata.json
+response.json
+state.kore
+trace.jsonl
+transactions.json

README.md

@@ -16,7 +16,7 @@
 
 ## 🌟 Overview
 
-`komet-node` extends the standard Stellar RPC with a `traceTransaction` method that provides instruction-level execution traces. The node's state is persisted to disk, allowing the same ledger state to be reproduced and transactions to be replayed. The RPC logic itself runs inside the K formal semantics — Python is only a thin shim that decodes Stellar XDR.
+`komet-node` extends the standard Stellar RPC with a `traceTransaction` method that provides instruction-level execution traces. The node's state is persisted to disk, allowing the same ledger state to be reproduced and transactions to be replayed. The RPC logic itself runs inside the K formal semantics. The compiled semantics are a one-shot interpreter — given a state, it runs a single request to completion and exits — so a small Python program wraps it into a long-running server: it holds the HTTP connection, keeps the ledger state on disk between runs, and decodes Stellar's binary XDR transaction format, which K cannot read.
 
 ## 🚀 Quick Start
 
@@ -75,7 +75,7 @@ komet-node --trace               # enable instruction-level execution tracing
 | `--state-file` | `state.kore` | Path to the persistent state file |
 | `--trace` | off | Enable instruction-level execution tracing |
 
-On first start the server creates an empty `state.kore`, alongside `metadata.json` (the ledger counter) and `transactions.json` (the transaction store). Delete `state.kore` to reset the chain (the sidecar files are re-seeded), or point `--state-file` at a pre-built configuration to resume from a snapshot.
+On first start the server creates a fresh `state.kore` (the idle configuration — an empty chain), alongside `metadata.json` (the ledger counter) and `transactions.json` (the transaction store). Delete `state.kore` to reset the chain (the sidecar files are re-seeded), or point `--state-file` at a pre-built configuration to resume from a snapshot.
 
 #### Verify the server with `curl`
 
@@ -174,7 +174,7 @@ This produces `state.kore` plus `state_<n>_<step>.pretty` files under `./out`, l
 
 ## For Developers
 
-Prerequisites: `python >= 3.10`, [`uv`](https://docs.astral.sh/uv/), [`wabt`](https://github.com/WebAssembly/wabt) (for `wat2wasm`), and the K Framework. The [Dev Container](#for-developers) provisions all of these for you.
+Prerequisites: `python >= 3.10`, [`uv`](https://docs.astral.sh/uv/), [`wabt`](https://github.com/WebAssembly/wabt) (for `wat2wasm`), and the K Framework. The Dev Container provisions all of these for you.
 
 1. Install [VS Code](https://code.visualstudio.com/) and the [Dev Containers extension](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers).
 2. Open this repository in VS Code and choose **Reopen in Container** when prompted.
@@ -201,14 +201,15 @@ 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 build
 pip install dist/*.whl
 ```
 
 ### Documentation
 
 - [Architecture overview](docs/architecture.md) — how the pieces fit together
-- [Server](docs/server.md) — the HTTP/RPC shim, state lifecycle, and full method reference
+- [Server](docs/server.md) — the long-running HTTP server that wraps the K interpreter, state lifecycle, and full method reference
 - [Transaction encoding](docs/transaction.md) — Stellar XDR → K request envelope
 - [Interpreter](docs/interpreter.md) — running request envelopes through the K semantics
 - [K semantics](docs/node-semantics.md) — the on-chain RPC dispatch and execution model

docs/architecture.md

@@ -2,15 +2,15 @@
 
 ## Overview
 
-komet-node is a local Stellar testnet whose execution engine is the [K formal semantics](https://github.com/runtimeverification/komet) of Soroban. Rather than running a real Stellar validator, it decodes incoming Stellar transactions into K steps and executes them through the compiled K semantics according to the formal Soroban specification.
+komet-node is a local Stellar testnet whose execution engine is the [K formal semantics](https://github.com/runtimeverification/komet) of Soroban. It decodes incoming Stellar transactions into K steps and executes them through the compiled semantics.
 
-The design keeps Python as a thin shim and pushes everything that is *grounded in the formal semantics* into K. Python only does what K cannot: decode the Stellar XDR envelope (and parse uploaded wasm). Everything else — RPC method dispatch, the transaction store, ledger-sequence accounting, status determination, and JSON-RPC response formatting — lives in the K semantics (`node.md`).
+The split between Python and K follows one rule: K does everything that is part of the Soroban/Stellar protocol, and Python does only what K structurally cannot. The compiled K semantics are a *one-shot interpreter* — one invocation runs one request to completion and exits, with no network, no memory between invocations, and no decoder for Stellar's binary XDR format. Python supplies exactly those three missing pieces: it is the long-running process that holds the HTTP socket, it keeps the world state on disk between invocations, and it decodes the XDR envelope (and parses uploaded wasm). Everything else — RPC method dispatch, the transaction store, ledger-sequence accounting, status determination, and JSON-RPC response formatting — runs inside the K semantics (`node.md`).
 
 ```
 Stellar client
      │  JSON-RPC request (base64 XDR transaction)
      ▼
-StellarRpcServer                    ← server.py   (raw http.server, no business logic)
+StellarRpcServer                    ← server.py   (long-running http.server; holds the socket + state files)
      │
      ├─ TransactionEncoder          ← transaction.py
      │     XDR → request envelope (+ kasmer steps for wasm uploads)
@@ -31,37 +31,37 @@ StellarRpcServer                    ← server.py   (raw http.server, no busines
 
 ### `server.py` — `StellarRpcServer`
 
-A raw `http.server.HTTPServer` shim. 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, transaction store, or response-formatting logic — those now live in K.
+`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, transaction store, or response-formatting logic — those live in K.
 
 `handle_rpc(method, params, id)` is the dispatch entry point and is usable without the HTTP layer (scripts, tests).
 
 → **[Detailed documentation](server.md)**
 
-Implemented RPC methods: `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`, `traceTransaction`. All are answered by the K semantics.
+The server implements six RPC methods — `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`, and `traceTransaction` — and the K semantics answer all of them.
 
 `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.
 
 ---
 
 ### `transaction.py` — `TransactionEncoder`
 
-The XDR boundary. Decodes a `stellar_sdk` transaction envelope into a JSON request envelope: the RPC method, the transaction hash, the envelope XDR, and the decoded operations as JSON "steps". For the one case K cannot consume as JSON — a wasm upload, whose `ModuleDecl` has no JSON form — it produces the kasmer steps in K-AST form for direct injection into the `<program>` cell.
+`TransactionEncoder` is the XDR boundary. It decodes a `stellar_sdk` transaction envelope into a JSON request envelope containing the RPC method, the transaction hash, the envelope XDR, and the decoded operations as JSON "steps". For the one case K cannot consume as JSON — a wasm upload, whose `ModuleDecl` has no JSON form — it produces the kasmer steps in K-AST form for direct injection into the `<program>` cell.
 
 → **[Detailed documentation](transaction.md)**
 
 ---
 
 ### `interpreter.py` — `NodeInterpreter`
 
-The K-execution boundary. Builds the initial configuration, runs a request envelope through the LLVM interpreter against `state.kore`, and persists the resulting state. It knows nothing about Stellar. It performs **no** whole-configuration `kast`↔`kore` conversions — the initial config is built directly in KORE and request steps are spliced into the `<program>` cell at the KORE level.
+`NodeInterpreter` is the K-execution boundary. It builds the initial configuration, runs a request envelope through the LLVM interpreter against `state.kore`, and persists the resulting state. It knows nothing about Stellar. It performs **no** whole-configuration `kast`↔`kore` conversions — the initial config is built directly in KORE and request steps are spliced into the `<program>` cell at the KORE level.
 
 → **[Detailed documentation](interpreter.md)**
 
 ---
 
 ### `kdist/node.md` — K Semantics
 
-The K module compiled into the LLVM binary. Implements the whole RPC layer on the K side: reads `request.json`, dispatches on the `method` field, reads/updates the bookkeeping files (`metadata.json`, `transactions.json`), executes transaction steps via KASMER, and writes the JSON-RPC `response.json`.
+`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 the bookkeeping files (`metadata.json`, `transactions.json`), executes transaction steps via KASMER, and writes the JSON-RPC `response.json`.
 
 → **[Detailed documentation](node-semantics.md)**
 
@@ -96,7 +96,7 @@ per failed (stuck) transaction:
             ledger is not bumped. The server synthesises a FAILED receipt.
 ```
 
-Because all three files live on disk, the server can be stopped and restarted without losing state — the ledger counter and transaction store now survive restarts. To resume from a session, point `--state-file` at a saved `state.kore` (its sidecar files are read if present). To start fresh, delete the files.
+Because all three files live on disk, the server can be stopped and restarted without losing the world state, the ledger counter, or the transaction store. To resume a session, point `--state-file` at a saved `state.kore` (its sidecar files are read if present). To start fresh, delete the files.
 
 ---
 

docs/interpreter.md

@@ -11,36 +11,39 @@ class NodeInterpreter:
     definition: SimbolikDefinition   # compiled K definition (komet-node.simbolik)
 ```
 
-`SimbolikDefinition` is a thin subclass of `komet.SorobanDefinition`, pointing to the `komet-node.simbolik` compiled K definition (cached under `~/.cache/kdist-*/komet-node/simbolik/`). Note there is no `network_passphrase` or `trace` here — those belong to the request side (`TransactionEncoder`); the interpreter is purely about running K.
+`SimbolikDefinition` is a thin subclass of `komet.SorobanDefinition`, pointing to the `komet-node.simbolik` compiled K definition (cached under `~/.cache/kdist-*/komet-node/simbolik/`). There is no `network_passphrase` or `trace` here — those belong to the request side (`TransactionEncoder`); the interpreter only runs K.
 
 ---
 
 ## No `kast`↔`kore` conversions
 
-A guiding constraint: whole-configuration `kore_to_kast` / `kast_to_kore` conversions take seconds and get slower as the configuration grows, so the interpreter avoids them entirely. `state.kore` is only ever parsed with `KoreParser` (KORE text → KORE AST, which is cheap) and handed straight to `llvm_interpret`. Terms that must be constructed are built directly in KORE.
+Whole-configuration `kore_to_kast` / `kast_to_kore` conversions take seconds and get slower as the configuration grows, so the interpreter avoids them entirely. `state.kore` is only ever parsed with `KoreParser` (KORE text → KORE AST, which is cheap) and handed straight to `llvm_interpret`. Terms that must be constructed are built directly in KORE.
 
 ### `empty_config()`
 
-Produces the initial blank-slate `state.kore`. It builds the top-cell initializer **in KORE** — seeding `$PGM` with a single `setExitCode(0)` step and `$TRACE` with an empty string — and runs it through `llvm_interpret`. No `krun` subprocess and no kast conversion are involved.
+`empty_config()` produces the initial blank-slate `state.kore`. It builds the top-cell initializer **in KORE** — seeding `$PGM` with a single `setExitCode(0)` step and `$TRACE` with an empty string — and runs it through the interpreter. No `krun` subprocess and no kast conversion are involved.
 
 ```python
 config = top_cell_initializer({
     '$PGM':   inj(SortSteps, K_ITEM, kasmerSteps(setExitCode(0), .Steps)),  # built in KORE
     '$TRACE': inj(SortString, K_ITEM, str_dv('')),
 })
-return llvm_interpret(self.definition.path, config, check=False).text
+with tempfile.TemporaryDirectory() as isolated_dir:        # see note below
+    return _llvm_interpret(self.definition.path, config, cwd=isolated_dir).text
 ```
 
 The result is the empty idle K configuration — no accounts, no contracts, no storage.
 
+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)`
 
-The main entry point. Runs a single RPC request envelope:
+`run` is the main entry point. It runs a single RPC request envelope through the following steps:
 
 1. Write the request envelope to `request.json` in `io_dir`, and delete any stale `response.json`.
 2. Parse `state.kore` with `KoreParser` (no kast conversion).
 3. For a wasm upload only, splice the upload steps into the `<program>` cell (see below).
-4. `chdir` into `io_dir` (so the K file-system hooks resolve the relative paths `request.json`, `response.json`, `metadata.json`, `transactions.json`, `trace.jsonl`) and call `llvm_interpret`.
+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`, `transactions.json`, `trace.jsonl`). 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.
 
 ### `_inject_program(pattern, steps)` — the wasm-upload path
@@ -58,7 +61,7 @@ Because Soroban allows only a single host-function operation per transaction, a
 
 ### `pretty_print(kore_str)`
 
-A debugging helper that pretty-prints a KORE configuration string using `krun --output pretty --depth 0`. Used by `demo.py` to render each step of a contract lifecycle.
+`pretty_print` is a debugging helper that pretty-prints a KORE configuration string using `krun --output pretty --depth 0`. `demo.py` uses it to render each step of a contract lifecycle.
 
 ---
 
@@ -77,4 +80,4 @@ The mapping from Stellar operations to kasmer steps is performed by [`Transactio
 
 ## Error handling
 
-`NodeInterpreterError` is raised for interpreter-level failures (e.g. `pretty_print`). A *transaction* failure is not an exception: the semantics simply get stuck without writing `response.json`, so `run` returns `None` and the server records a `FAILED` receipt while leaving `state.kore` unchanged (the state effectively rolls back).
+`NodeInterpreterError` is raised for interpreter-level failures (e.g. `pretty_print`). A *transaction* failure is not an exception: the semantics get stuck without writing `response.json`, so `run` returns `None` and the server records a `FAILED` receipt while leaving `state.kore` unchanged (the state effectively rolls back).