Skip to content

Commit d6fd0d7

Browse files
Merge pull request #1 from runtimeverification/burak/dev
Implement komet-node: local Soroban testnet backed by K semantics
2 parents 55d0403 + d77b000 commit d6fd0d7

25 files changed

Lines changed: 4350 additions & 3 deletions

.cruft.json

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
{
2+
"template": "https://github.com/runtimeverification/python-project-template",
3+
"commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68",
4+
"checkout": null,
5+
"context": {
6+
"cookiecutter": {
7+
"project_name": "komet-node",
8+
"project_slug": "komet-node",
9+
"package_name": "komet_node",
10+
"version": "0.1.0",
11+
"description": "Local development testnet for Stellar based on K semantics",
12+
"author_name": "Runtime Verification, Inc.",
13+
"author_email": "contact@runtimeverification.com",
14+
"_template": "https://github.com/runtimeverification/python-project-template",
15+
"_commit": "7a095b4dd0a51916da0a728b8fdd9adf7e469a68"
16+
}
17+
},
18+
"directory": null
19+
}

.flake8

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
[flake8]
2+
max-line-length = 120
3+
extend-select = B9, TC1
4+
extend-ignore = B950,E,W1,W2,W3,W4,W5
5+
per-file-ignores =
6+
*/__init__.py: F401
7+
type-checking-strict = true

.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
/dist/
2+
__pycache__/
3+
.coverage

Makefile

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,14 @@ clean:
1515
build:
1616
$(UV) build
1717

18+
# Semantics
19+
20+
kdist-build:
21+
$(UV_RUN) kdist -v build -j2 komet-node.*
22+
$(UV_RUN) kdist -v build -j2 soroban-semantics.*
23+
24+
kdist-clean:
25+
$(UV_RUN) kdist clean
1826

1927
# Tests
2028

docs/architecture.md

Lines changed: 139 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
# komet-node: Architecture
2+
3+
## Overview
4+
5+
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.
6+
7+
The server receives and decodes a transaction and manages the current blockchain state (state.kore).
8+
The interpreter translates the transaction into K steps and runs them through krun producing an updated state.
9+
10+
```
11+
Stellar client
12+
│ JSON-RPC request (XDR transaction)
13+
14+
StellarRpcServer ← server.py
15+
│ decoded Transaction + state.kore
16+
17+
NodeInterpreter ← interpreter.py
18+
│ request.json (encoded steps) + state.kore
19+
20+
K semantics (LLVM backend) ← kdist/node.md + soroban-semantics
21+
│ updated state.kore
22+
23+
state.kore (written back for the next transaction)
24+
```
25+
26+
---
27+
28+
## Components
29+
30+
### `server.py``StellarRpcServer`
31+
32+
The HTTP/JSON-RPC layer. Exposes the Stellar RPC API to clients, manages the `state.kore` file on disk, and dispatches transactions to `NodeInterpreter`.
33+
34+
**[Detailed documentation](server.md)**
35+
36+
Implemented RPC methods: `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`.
37+
38+
`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.
39+
40+
---
41+
42+
### `interpreter.py``NodeInterpreter`
43+
44+
The core execution engine. Translates a decoded Transaction into K steps and runs them through krun, returning the updated state as a KORE string.
45+
46+
**[Detailed documentation](interpreter.md)**
47+
48+
---
49+
50+
### `kdist/node.md` — K Semantics
51+
52+
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.
53+
54+
**[Detailed documentation](node-semantics.md)**
55+
56+
---
57+
58+
## State management
59+
60+
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).
61+
62+
```
63+
startup: state.kore does not exist
64+
→ StellarRpcServer calls interpreter.empty_config()
65+
→ empty_config() runs krun with setExitCode(0) as the only step,
66+
producing the initial empty idle K configuration
67+
(no accounts, no contracts, no storage)
68+
→ server writes the result to state.kore
69+
70+
per successful transaction:
71+
→ NodeInterpreter reads state.kore as krun input
72+
→ krun executes the transaction steps
73+
→ krun outputs the updated configuration to stdout
74+
→ server.py overwrites state.kore with the new state
75+
→ ledger_seq incremented
76+
77+
per failed transaction:
78+
→ state.kore is NOT updated (implicit rollback)
79+
→ ledger_seq is NOT incremented
80+
```
81+
82+
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.
83+
84+
---
85+
86+
## Request flow (end to end)
87+
88+
```
89+
1. Client: POST {"method": "sendTransaction", "params": {"transaction": "<base64 XDR>"}}
90+
91+
2. StellarRpcServer.exec_send_transaction:
92+
- TransactionEnvelope.from_xdr(xdr, network_passphrase)
93+
- tx_hash = envelope.hash_hex()
94+
- NodeInterpreter.run_transaction(state_file, envelope.transaction)
95+
96+
3. NodeInterpreter.run_transaction:
97+
- encode_transaction_to_json(tx) → JSON string (or None for wasm upload)
98+
- run_request_file(state_file, json_str) ← JSON path
99+
OR
100+
run_steps(state_file, kast_steps) ← KORE path
101+
102+
4. run_request_file:
103+
- writes request.json to temp dir
104+
- krun state.kore --definition simbolik --output kore --parser cat --term
105+
- K semantics: insert-handleRequestFile → handleRequest → decode JSON
106+
→ execute steps → removeRequestFile → setExitCode(0)
107+
- returns InterpreterResponse(final_kore=stdout, trace=...)
108+
109+
5. StellarRpcServer:
110+
- state_file.write_text(result.final_kore)
111+
- ledger_seq += 1
112+
- _transactions[tx_hash] = {status: SUCCESS, trace: result.trace, ...}
113+
- returns {hash, status: PENDING, latestLedger, latestLedgerCloseTime}
114+
115+
6. Client: POST {"method": "getTransaction", "params": {"hash": "<hash>"}}
116+
→ returns {status: SUCCESS, ledger, createdAt, envelopeXdr, trace, ...}
117+
```
118+
119+
---
120+
121+
## Dependencies
122+
123+
| Dependency | Role |
124+
|---|---|
125+
| `komet` | Soroban K semantics, `SorobanDefinition`, `SCValue` dataclasses, `kasmer` step types |
126+
| `pyk` | K toolchain Python bindings: `krun`, `kdist`, KORE/KAst parsing, `JsonRpcServer` |
127+
| `pykwasm` | Wasm → K AST conversion (`wasm2kast`), used in the KORE path for wasm upload |
128+
| `stellar_sdk` | Stellar transaction types, XDR encoding/decoding, `TransactionEnvelope` |
129+
130+
---
131+
132+
## What's not yet implemented
133+
134+
- `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
135+
- `simulateTransaction` (dry-run without state mutation)
136+
- `getEvents`, `getLedgerEntries`, `getFeeStats` and other read-only RPC methods
137+
- Persistent transaction store (results lost on server restart)
138+
- Persistent ledger counter (resets to 0 on server restart)
139+
- `ExtendFootprintTTL` and `RestoreFootprint` operations

docs/interpreter.md

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
1+
# `interpreter.py``NodeInterpreter`
2+
3+
`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.
4+
5+
---
6+
7+
## Class structure
8+
9+
```python
10+
class NodeInterpreter:
11+
definition: SimbolikDefinition # compiled K definition (komet-node.simbolik)
12+
network_passphrase: str
13+
trace: bool # whether to enable instruction tracing
14+
```
15+
16+
`SimbolikDefinition` is a thin subclass of `komet.SorobanDefinition`, pointing to the `komet-node.simbolik` compiled K definition (cached under `~/.cache/kdist-*/komet-node/simbolik/`).
17+
18+
---
19+
20+
## Execution paths
21+
22+
`run_transaction(state_file, transaction)` is the main entry point. It chooses between two execution strategies depending on the transaction content:
23+
24+
```
25+
Transaction
26+
27+
├─ can encode to JSON? ──yes──► JSON fast path (run_request_file)
28+
│ writes request.json, krun reads it
29+
30+
└─ no (wasm upload) ────────► KORE round-trip (run_steps)
31+
Python parses state.kore, mutates AST,
32+
re-serializes, krun on full KORE term
33+
```
34+
35+
### JSON fast path (`run_request_file`)
36+
37+
Used for all operations except wasm upload. The goal is to avoid Python-side KORE parsing and AST manipulation entirely.
38+
39+
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).
40+
2. A temporary working directory is created. `request.json` is written there.
41+
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.
42+
4. If tracing is enabled, `trace.jsonl` is read from the temp dir and included in the response.
43+
44+
```python
45+
with temp_working_directory() as root:
46+
(root / 'request.json').write_text(request_str)
47+
res = _krun(input_file=state_file, definition_dir=..., term=True, output=KORE)
48+
trace = (root / 'trace.jsonl').read_text() if tracing else None
49+
return InterpreterResponse(final_kore=res.stdout, trace=trace)
50+
```
51+
52+
Each request runs in its own temp dir so that concurrent requests (if added) and trace files are isolated.
53+
54+
### KORE round-trip (`run_steps`)
55+
56+
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.
57+
58+
1. Parse `state.kore` into a Python KORE AST.
59+
2. Convert the AST to KAst (`kore_to_kast`).
60+
3. Inject K steps (including the `ModuleDecl`) into the `<program>` cell.
61+
4. Re-serialize to KORE (`kast_to_kore`) and run krun on the full term.
62+
63+
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.
64+
65+
---
66+
67+
## Supported operations
68+
69+
| Stellar operation | K step | Execution path |
70+
|---|---|---|
71+
| `CreateAccount` | `setAccount(Account(bytes), stroops)` | JSON |
72+
| `InvokeHostFunction` / upload wasm | `uploadWasm(hash, ModuleDecl)` | KORE round-trip |
73+
| `InvokeHostFunction` / create contract (V1, V2) | `deployContract(from, address, wasmHash)` | JSON |
74+
| `InvokeHostFunction` / invoke contract | `callTx(from, to, func, args, Void)` | JSON |
75+
76+
---
77+
78+
## JSON request format
79+
80+
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`.
81+
82+
```json
83+
{
84+
"steps": [
85+
{ "op": "setAccount", "account": "<hex32>", "balance": <int> },
86+
{ "op": "deployContract", "from": "<hex32>", "address": "<hex32>", "wasmHash": "<hex32>" },
87+
{ "op": "callTx", "from": "<hex32>", "fromIsContract": <bool>,
88+
"func": "<name>", "to": "<hex32>", "args": [ ... ] }
89+
]
90+
}
91+
```
92+
93+
### SCVal argument encoding
94+
95+
Contract function arguments (`callTx` args) are encoded as JSON dicts:
96+
97+
| SCVal type | JSON encoding |
98+
|---|---|
99+
| `SCV_BOOL` | `{"type": "bool", "value": true\|false}` |
100+
| `SCV_I32` / `SCV_U32` | `{"type": "i32"\|"u32", "value": <int>}` |
101+
| `SCV_I64` / `SCV_U64` | `{"type": "i64"\|"u64", "value": <int>}` |
102+
| `SCV_I128` / `SCV_U128` | `{"type": "i128"\|"u128", "value": <int>}` (combined hi/lo) |
103+
| `SCV_SYMBOL` | `{"type": "symbol", "value": "<str>"}` |
104+
| `SCV_BYTES` | `{"type": "bytes", "value": "<lowercase hex>"}` |
105+
| `SCV_ADDRESS` (account) | `{"type": "address", "addrType": "account", "value": "<hex32>"}` |
106+
| `SCV_ADDRESS` (contract) | `{"type": "address", "addrType": "contract", "value": "<hex32>"}` |
107+
108+
---
109+
110+
## Initial configuration (`empty_config`)
111+
112+
`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.
113+
114+
When `trace=True`, `empty_config` passes two extra arguments to krun:
115+
116+
```python
117+
cmap = {'TRACE': str_dv('trace.jsonl').text} # K string token
118+
pmap = {'TRACE': 'cat'} # parser: pass through as-is
119+
```
120+
121+
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.
122+
123+
---
124+
125+
## Tracing
126+
127+
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.
128+
129+
**How it works**:
130+
131+
1. `empty_config()` bakes `<ioDir>trace.jsonl</ioDir>` into `state.kore`.
132+
2. For each transaction, `run_request_file` creates a temp dir, runs krun from it.
133+
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.
134+
4. After krun finishes, the trace file is read and returned in `InterpreterResponse.trace`.
135+
5. The server stores the trace string in `_transactions[hash]['trace']`, retrievable via `getTransaction`.
136+
137+
**Trace format** (one JSON record per line):
138+
139+
```json
140+
{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}}
141+
```
142+
143+
| Field | Description |
144+
|---|---|
145+
| `pos` | Byte offset of the instruction in the binary, or `null` for synthetic instructions |
146+
| `instr` | Instruction name and operands as a JSON array |
147+
| `stack` | Value stack at instruction entry, as `[type, value]` pairs |
148+
| `locals` | Local variable bindings, keyed by index, as `[type, value]` pairs |
149+
150+
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.
151+
152+
---
153+
154+
## `InterpreterResponse`
155+
156+
```python
157+
class InterpreterResponse(NamedTuple):
158+
final_kore: str # updated K configuration (to write back to state.kore)
159+
trace: str | None # JSONL trace string, or None if tracing is disabled
160+
```
161+
162+
---
163+
164+
## Error handling
165+
166+
`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).
167+
168+
---
169+
170+
## Address utilities
171+
172+
`NodeInterpreter` also provides helpers for Stellar address encoding/decoding:
173+
174+
- `decode_account_id(addr)` — G-strkey → 32-byte public key
175+
- `decode_contract_id(addr)` — C-strkey → 32-byte contract ID
176+
- `contract_address_from_deployer_address(deployer, salt)` — computes the C-strkey that `CREATE_CONTRACT` will assign
177+
- `contract_id_from_preimage(preimage)` — SHA-256 of the `HashIDPreimage` as used by Stellar

0 commit comments

Comments
 (0)