Implement komet-node: local Soroban testnet backed by K semantics

.cruft.json

@@ -0,0 +1,19 @@
+{
+  "template": "https://github.com/runtimeverification/python-project-template",
+  "commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68",
+  "checkout": null,
+  "context": {
+    "cookiecutter": {
+      "project_name": "komet-node",
+      "project_slug": "komet-node",
+      "package_name": "komet_node",
+      "version": "0.1.0",
+      "description": "Local development testnet for Stellar based on K semantics",
+      "author_name": "Runtime Verification, Inc.",
+      "author_email": "contact@runtimeverification.com",
+      "_template": "https://github.com/runtimeverification/python-project-template",
+      "_commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68"
+    }
+  },
+  "directory": null
+}

.flake8

@@ -0,0 +1,7 @@
+[flake8]
+max-line-length = 120
+extend-select = B9, TC1
+extend-ignore = B950,E,W1,W2,W3,W4,W5
+per-file-ignores =
+    */__init__.py: F401
+type-checking-strict = true

.gitignore

@@ -0,0 +1,3 @@
+/dist/
+__pycache__/
+.coverage

Makefile

@@ -15,6 +15,14 @@ clean:
 build:
 	$(UV) build
 
+# Semantics
+
+kdist-build:
+	$(UV_RUN) kdist -v build -j2 komet-node.*
+	$(UV_RUN) kdist -v build -j2 soroban-semantics.*
+
+kdist-clean:
+	$(UV_RUN) kdist clean
 
 # Tests
 

docs/architecture.md

@@ -0,0 +1,139 @@
+# komet-node: Architecture
+
+## 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 translates incoming Stellar transactions into K steps and executes them through the compiled K semantics according to the formal Soroban specification.
+
+The server receives and decodes a transaction and manages the current blockchain state (state.kore).
+The interpreter translates the transaction into K steps and runs them through krun producing an updated state.
+
+```
+Stellar client
+     │  JSON-RPC request (XDR transaction)
+     ▼
+StellarRpcServer                    ← server.py
+     │  decoded Transaction + state.kore
+     ▼
+NodeInterpreter                     ← interpreter.py
+     │  request.json (encoded steps) + state.kore
+     ▼
+K semantics (LLVM backend)          ← kdist/node.md + soroban-semantics
+     │  updated state.kore
+     ▼
+state.kore  (written back for the next transaction)
+```
+
+---
+
+## Components
+
+### `server.py` — `StellarRpcServer`
+
+The HTTP/JSON-RPC layer. Exposes the Stellar RPC API to clients, manages the `state.kore` file on disk, and dispatches transactions to `NodeInterpreter`.
+
+→ **[Detailed documentation](server.md)**
+
+Implemented RPC methods: `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`.
+
+`sendTransaction` always returns `PENDING` and clients poll `getTransaction` for the result — matching the Stellar RPC async pattern even though krun executes the transaction immediately. See [server.md](server.md) for details.
+
+---
+
+### `interpreter.py` — `NodeInterpreter`
+
+The core execution engine. Translates a decoded Transaction into K steps and runs them through krun, returning the updated state as a KORE string.
+
+→ **[Detailed documentation](interpreter.md)**
+
+---
+
+### `kdist/node.md` — K Semantics
+
+The K module compiled into the LLVM binary. Implements the `request.json` lifecycle on the K side: detects the file, parses and decodes the JSON steps, executes them via KASMER, removes the file, and halts with the updated state as output.
+
+→ **[Detailed documentation](node-semantics.md)**
+
+---
+
+## State management
+
+The entire blockchain state is a single KORE file (`state.kore`). It contains the full K configuration: accounts, contract code, contract storage, and ledger metadata, serialized in KORE (K's internal term format).
+
+```
+startup:  state.kore does not exist
+          → StellarRpcServer calls interpreter.empty_config()
+          → empty_config() runs krun with setExitCode(0) as the only step,
+            producing the initial empty idle K configuration
+            (no accounts, no contracts, no storage)
+          → server writes the result to state.kore
+
+per successful transaction:
+          → NodeInterpreter reads state.kore as krun input
+          → krun executes the transaction steps
+          → krun outputs the updated configuration to stdout
+          → server.py overwrites state.kore with the new state
+          → ledger_seq incremented
+
+per failed transaction:
+          → state.kore is NOT updated (implicit rollback)
+          → ledger_seq is NOT incremented
+```
+
+Because `state.kore` lives on disk, the server can be stopped and restarted between transactions without losing state. To resume from a previous session, point `--state-file` at a saved `state.kore`. To start fresh, delete or omit the file.
+
+---
+
+## Request flow (end to end)
+
+```
+1. Client: POST {"method": "sendTransaction", "params": {"transaction": "<base64 XDR>"}}
+
+2. StellarRpcServer.exec_send_transaction:
+   - TransactionEnvelope.from_xdr(xdr, network_passphrase)
+   - tx_hash = envelope.hash_hex()
+   - NodeInterpreter.run_transaction(state_file, envelope.transaction)
+
+3. NodeInterpreter.run_transaction:
+   - encode_transaction_to_json(tx) → JSON string (or None for wasm upload)
+   - run_request_file(state_file, json_str)  ← JSON path
+     OR
+     run_steps(state_file, kast_steps)       ← KORE path
+
+4. run_request_file:
+   - writes request.json to temp dir
+   - krun state.kore --definition simbolik --output kore --parser cat --term
+   - K semantics: insert-handleRequestFile → handleRequest → decode JSON
+     → execute steps → removeRequestFile → setExitCode(0)
+   - returns InterpreterResponse(final_kore=stdout, trace=...)
+
+5. StellarRpcServer:
+   - state_file.write_text(result.final_kore)
+   - ledger_seq += 1
+   - _transactions[tx_hash] = {status: SUCCESS, trace: result.trace, ...}
+   - returns {hash, status: PENDING, latestLedger, latestLedgerCloseTime}
+
+6. Client: POST {"method": "getTransaction", "params": {"hash": "<hash>"}}
+   → returns {status: SUCCESS, ledger, createdAt, envelopeXdr, trace, ...}
+```
+
+---
+
+## Dependencies
+
+| Dependency | Role |
+|---|---|
+| `komet` | Soroban K semantics, `SorobanDefinition`, `SCValue` dataclasses, `kasmer` step types |
+| `pyk` | K toolchain Python bindings: `krun`, `kdist`, KORE/KAst parsing, `JsonRpcServer` |
+| `pykwasm` | Wasm → K AST conversion (`wasm2kast`), used in the KORE path for wasm upload |
+| `stellar_sdk` | Stellar transaction types, XDR encoding/decoding, `TransactionEnvelope` |
+
+---
+
+## What's not yet implemented
+
+- `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
+- `simulateTransaction` (dry-run without state mutation)
+- `getEvents`, `getLedgerEntries`, `getFeeStats` and other read-only RPC methods
+- Persistent transaction store (results lost on server restart)
+- Persistent ledger counter (resets to 0 on server restart)
+- `ExtendFootprintTTL` and `RestoreFootprint` operations

docs/interpreter.md

@@ -0,0 +1,177 @@
+# `interpreter.py` — `NodeInterpreter`
+
+`NodeInterpreter` is the core of komet-node. It translates a `stellar_sdk.Transaction` into K execution steps, runs them through the compiled K semantics via `krun`, and returns the updated blockchain state.
+
+---
+
+## Class structure
+
+```python
+class NodeInterpreter:
+    definition: SimbolikDefinition   # compiled K definition (komet-node.simbolik)
+    network_passphrase: str
+    trace: bool                      # whether to enable instruction tracing
+```
+
+`SimbolikDefinition` is a thin subclass of `komet.SorobanDefinition`, pointing to the `komet-node.simbolik` compiled K definition (cached under `~/.cache/kdist-*/komet-node/simbolik/`).
+
+---
+
+## Execution paths
+
+`run_transaction(state_file, transaction)` is the main entry point. It chooses between two execution strategies depending on the transaction content:
+
+```
+Transaction
+    │
+    ├─ can encode to JSON? ──yes──► JSON fast path (run_request_file)
+    │                                   writes request.json, krun reads it
+    │
+    └─ no (wasm upload) ────────► KORE round-trip (run_steps)
+                                    Python parses state.kore, mutates AST,
+                                    re-serializes, krun on full KORE term
+```
+
+### JSON fast path (`run_request_file`)
+
+Used for all operations except wasm upload. The goal is to avoid Python-side KORE parsing and AST manipulation entirely.
+
+1. `encode_transaction_to_json(transaction)` serializes the transaction as a JSON string. Returns `None` if any operation cannot be expressed as JSON (currently only wasm upload).
+2. A temporary working directory is created. `request.json` is written there.
+3. `krun` is invoked with the current `state.kore` as input (`--term`). The K semantics detect `request.json`, read and decode it, execute the steps, remove the file, and halt. The updated state is captured from stdout.
+4. If tracing is enabled, `trace.jsonl` is read from the temp dir and included in the response.
+
+```python
+with temp_working_directory() as root:
+    (root / 'request.json').write_text(request_str)
+    res = _krun(input_file=state_file, definition_dir=..., term=True, output=KORE)
+    trace = (root / 'trace.jsonl').read_text() if tracing else None
+    return InterpreterResponse(final_kore=res.stdout, trace=trace)
+```
+
+Each request runs in its own temp dir so that concurrent requests (if added) and trace files are isolated.
+
+### KORE round-trip (`run_steps`)
+
+Used only for wasm upload. Wasm upload requires embedding a parsed `ModuleDecl` (the Wasm AST) directly into the K configuration — something that cannot be expressed as a flat JSON string.
+
+1. Parse `state.kore` into a Python KORE AST.
+2. Convert the AST to KAst (`kore_to_kast`).
+3. Inject K steps (including the `ModuleDecl`) into the `<program>` cell.
+4. Re-serialize to KORE (`kast_to_kore`) and run krun on the full term.
+
+This path is slower because it involves full KORE parsing and re-serialization on every wasm upload, but it is only triggered once per contract deployment.
+
+---
+
+## Supported operations
+
+| Stellar operation | K step | Execution path |
+|---|---|---|
+| `CreateAccount` | `setAccount(Account(bytes), stroops)` | JSON |
+| `InvokeHostFunction` / upload wasm | `uploadWasm(hash, ModuleDecl)` | KORE round-trip |
+| `InvokeHostFunction` / create contract (V1, V2) | `deployContract(from, address, wasmHash)` | JSON |
+| `InvokeHostFunction` / invoke contract | `callTx(from, to, func, args, Void)` | JSON |
+
+---
+
+## JSON request format
+
+The JSON fast path writes `request.json` with the following structure. **Key ordering is significant**: the K JSON sort is ordered, so Python dicts must produce keys in the same order as the K pattern-match rules in `node.md`.
+
+```json
+{
+  "steps": [
+    { "op": "setAccount",     "account": "<hex32>", "balance": <int> },
+    { "op": "deployContract", "from": "<hex32>", "address": "<hex32>", "wasmHash": "<hex32>" },
+    { "op": "callTx",         "from": "<hex32>", "fromIsContract": <bool>,
+                               "func": "<name>", "to": "<hex32>", "args": [ ... ] }
+  ]
+}
+```
+
+### SCVal argument encoding
+
+Contract function arguments (`callTx` args) are encoded as JSON dicts:
+
+| SCVal type | JSON encoding |
+|---|---|
+| `SCV_BOOL` | `{"type": "bool", "value": true\|false}` |
+| `SCV_I32` / `SCV_U32` | `{"type": "i32"\|"u32", "value": <int>}` |
+| `SCV_I64` / `SCV_U64` | `{"type": "i64"\|"u64", "value": <int>}` |
+| `SCV_I128` / `SCV_U128` | `{"type": "i128"\|"u128", "value": <int>}` (combined hi/lo) |
+| `SCV_SYMBOL` | `{"type": "symbol", "value": "<str>"}` |
+| `SCV_BYTES` | `{"type": "bytes", "value": "<lowercase hex>"}` |
+| `SCV_ADDRESS` (account) | `{"type": "address", "addrType": "account", "value": "<hex32>"}` |
+| `SCV_ADDRESS` (contract) | `{"type": "address", "addrType": "contract", "value": "<hex32>"}` |
+
+---
+
+## Initial configuration (`empty_config`)
+
+`empty_config()` produces the initial blank-slate `state.kore` by running krun with a single `setExitCode(0)` step. The output is the empty idle K configuration — no accounts, no contracts, no storage — which the server writes to `state.kore` on first startup.
+
+When `trace=True`, `empty_config` passes two extra arguments to krun:
+
+```python
+cmap = {'TRACE': str_dv('trace.jsonl').text}   # K string token
+pmap = {'TRACE': 'cat'}                         # parser: pass through as-is
+```
+
+These initialize the `<ioDir>` configuration cell (part of the `<trace>` cell, compiled in from the `k-tracing` selector) to `"trace.jsonl"`. Because this value is baked into `state.kore`, every subsequent krun invocation reads it and writes traces to `trace.jsonl` in the current working directory — which is the per-request temp dir.
+
+---
+
+## Tracing
+
+When the server is started with `--trace`, every `callTx` (contract invocation) produces an instruction-level execution trace. The trace records the VM state at each WebAssembly instruction.
+
+**How it works**:
+
+1. `empty_config()` bakes `<ioDir>trace.jsonl</ioDir>` into `state.kore`.
+2. For each transaction, `run_request_file` creates a temp dir, runs krun from it.
+3. The tracing K rules (from `soroban-semantics.tracing`) detect the non-empty `<ioDir>` and append one JSON record per instruction to `trace.jsonl` in the temp dir.
+4. After krun finishes, the trace file is read and returned in `InterpreterResponse.trace`.
+5. The server stores the trace string in `_transactions[hash]['trace']`, retrievable via `getTransaction`.
+
+**Trace format** (one JSON record per line):
+
+```json
+{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}}
+```
+
+| Field | Description |
+|---|---|
+| `pos` | Byte offset of the instruction in the binary, or `null` for synthetic instructions |
+| `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 |
+
+Tracing is only active for the LLVM backend. The `komet-node.simbolik` definition is compiled with `md_selector: 'k | k-tracing'`, so the tracing rules are always present; they are activated solely by `<ioDir>` being non-empty.
+
+---
+
+## `InterpreterResponse`
+
+```python
+class InterpreterResponse(NamedTuple):
+    final_kore: str        # updated K configuration (to write back to state.kore)
+    trace: str | None      # JSONL trace string, or None if tracing is disabled
+```
+
+---
+
+## Error handling
+
+`NodeInterpreterError` is raised when krun exits with a non-zero return code. The server catches this, stores a `FAILED` result for the transaction, and leaves `state.kore` unchanged (the state effectively rolls back).
+
+---
+
+## Address utilities
+
+`NodeInterpreter` also provides helpers for Stellar address encoding/decoding:
+
+- `decode_account_id(addr)` — G-strkey → 32-byte public key
+- `decode_contract_id(addr)` — C-strkey → 32-byte contract ID
+- `contract_address_from_deployer_address(deployer, salt)` — computes the C-strkey that `CREATE_CONTRACT` will assign
+- `contract_id_from_preimage(preimage)` — SHA-256 of the `HashIDPreimage` as used by Stellar