Skip to content

Commit 95cc69c

Browse files
RaoulSchaffranekRaoulSchaffranek
authored
Merge pull request #24 from runtimeverification/docs/readme-rewrite
docs: rewrite README with quick start, usage, and dev guide
2 parents 2a25a2c + 2aa7f34 commit 95cc69c

2 files changed

Lines changed: 210 additions & 10 deletions

File tree

‎README.md‎

Lines changed: 206 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,219 @@
1-
# komet-node
21

2+
<div align="center">
33

4-
## Installation
4+
# 🌠 Komet Node
55

6-
Prerequsites: `python >= 3.10`, [`uv`](https://docs.astral.sh/uv/).
6+
**A local Stellar testnet node based on [K formal semantics](https://github.com/runtimeverification/komet) of Soroban.**
7+
8+
[![Install](https://img.shields.io/badge/install-kup-blue)](https://kframework.org/install)
9+
[![Discord](https://img.shields.io/badge/discord-join-7289da)](https://discord.gg/CurfmXNtbN)
10+
11+
[Installation](#installation) • [Usage](#usage) • [Contribute](#for-developers)
12+
13+
</div>
14+
15+
---
16+
17+
## 🌟 Overview
18+
19+
`komet-node` extends the standard Stellar RPC with a `traceTransaction` method that provides instruction-level execution traces. The node's ledger state can be saved to and restored from a single file, allowing the same ledger state to be reproduced and transactions to be replayed.
20+
21+
## 🚀 Quick Start
22+
23+
### Installation
24+
25+
#### Install with kup
26+
27+
`komet-node` is distributed through [`kup`](https://github.com/runtimeverification/kup), Runtime Verification's Nix-based package manager. It pulls prebuilt binaries (including the matching K Framework and kompiled semantics) from RV's binary cache, so there is nothing to compile.
28+
29+
```bash
30+
# 1. Install the kup package manager (one time)
31+
bash <(curl https://kframework.org/install)
32+
33+
# 2. Install komet-node
34+
kup install komet-node
35+
36+
# 3. Verify the installation
37+
komet-node --help
38+
```
39+
40+
To upgrade later, run `kup update komet-node`.
41+
42+
#### Run with Docker
43+
44+
Alternatively, a prebuilt image is published to Docker Hub for each release. It bundles K, the kompiled semantics, and `komet-node` ready to serve.
45+
46+
```bash
47+
# Pull the image (replace the tag with the release you want)
48+
docker pull runtimeverificationinc/komet-node:ubuntu-jammy-0.1.0
49+
50+
# Start the server, exposing the RPC port on the host
51+
docker run --rm -p 8000:8000 \
52+
runtimeverificationinc/komet-node:ubuntu-jammy-0.1.0 \
53+
komet-node --host 0.0.0.0 --port 8000
54+
```
55+
56+
> The server binds to `localhost` by default; pass `--host 0.0.0.0` inside the container so the port is reachable from the host.
57+
58+
---
59+
60+
### Usage
61+
62+
#### Start the server
63+
64+
```bash
65+
komet-node # serve on localhost:8000, state in ./state.kore
66+
komet-node --help # print general usage information
67+
komet-node --port 9000 # custom port
68+
komet-node --trace # enable instruction-level execution tracing
69+
```
70+
71+
| Flag | Default | Description |
72+
|---|---|---|
73+
| `--host` | `localhost` | Bind address |
74+
| `--port` | `8000` | Port to listen on |
75+
| `--state-file` | `state.kore` | Path to the persistent state file |
76+
| `--trace` | off | Enable instruction-level execution tracing |
77+
78+
On first start the server creates an empty `state.kore`. Delete that file to reset the chain, or point `--state-file` at a pre-built configuration to resume from a snapshot.
79+
80+
#### Verify the server with `curl`
81+
82+
The server is operated via the Stellar RPC protocol. The read-only methods below take no transaction payload and can be used as a quick health check:
83+
84+
```bash
85+
# Is the server alive?
86+
curl -s http://localhost:8000 \
87+
-H 'Content-Type: application/json' \
88+
-d '{"jsonrpc":"2.0","id":1,"method":"getHealth","params":{}}'
89+
# => {"jsonrpc":"2.0","id":1,"result":{"status":"healthy"}}
90+
```
91+
92+
```bash
93+
# Which network am I connected to?
94+
curl -s http://localhost:8000 \
95+
-H 'Content-Type: application/json' \
96+
-d '{"jsonrpc":"2.0","id":1,"method":"getNetwork","params":{}}'
97+
# => {"jsonrpc":"2.0","id":1,"result":{"passphrase":"Test SDF Network ; September 2015","protocolVersion":"22","friendbotUrl":null}}
98+
```
99+
100+
```bash
101+
# What is the current ledger sequence? (increments per committed transaction)
102+
curl -s http://localhost:8000 \
103+
-H 'Content-Type: application/json' \
104+
-d '{"jsonrpc":"2.0","id":1,"method":"getLatestLedger","params":{}}'
105+
# => {"jsonrpc":"2.0","id":1,"result":{"id":"00...00","protocolVersion":"22","sequence":0}}
106+
```
107+
108+
Submitting transactions uses the standard two-step Stellar pattern — `sendTransaction` with a base64 XDR envelope, then poll `getTransaction` by hash. Because there is no mempool, `komet-node` executes the transaction synchronously inside `sendTransaction`, so the result is already available by the time you poll. The trace example below shows this flow end-to-end with ready-to-run envelopes; see [docs/server.md](docs/server.md) for the full RPC reference.
109+
110+
#### Trace a transaction
111+
112+
`traceTransaction` executes a transaction and returns an instruction-level execution trace inline, in a single call. Tracing only applies to contract invocations, so the server must be started with `--trace`:
113+
114+
```bash
115+
komet-node --trace
116+
```
117+
118+
A trace requires a deployed contract. The four envelopes below are pre-built and signed (a tiny contract whose `foo()` returns void, deployed from a fixed key) so you can paste them straight in — the local node does not check signatures, sequence numbers, or timebounds, so they work as-is on a fresh chain. Run them in order against the server above.
119+
120+
```bash
121+
# 1. Create the deployer account
122+
curl -s http://localhost:8000 -H 'Content-Type: application/json' \
123+
-d '{"jsonrpc":"2.0","id":1,"method":"sendTransaction","params":{"transaction":"AAAAAgAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAGQAAAAAAAAAAQAAAAEAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEAAAAAAAAAAAAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAAJUC+QAAAAAAAAAAAESVTG4AAAAQMOMXdUuK9E9tF0pgpqX+z+nXFlE6Mn5e7rqOFL8jIolInsXc7XHPgvYs4VWDqlCGI/fom9SpYiHOQYUqKTvDAc="}}'
124+
125+
# 2. Upload the contract wasm
126+
curl -s http://localhost:8000 -H 'Content-Type: application/json' \
127+
-d '{"jsonrpc":"2.0","id":1,"method":"sendTransaction","params":{"transaction":"AAAAAgAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAGQAAAAAAAAAAgAAAAEAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEAAAAAAAAAGAAAAAIAAABzAGFzbQEAAAABCAJgAAF+YAAAAwMCAAEFAwEAEAYZA38BQYCAwAALfwBBgIDAAAt/AEGAgMAACwcvBQZtZW1vcnkCAANmb28AAAFfAAEKX19kYXRhX2VuZAMBC19faGVhcF9iYXNlAwIKCQIEAEICCwIACwAAAAAAAAAAAAAAAAESVTG4AAAAQOk89R0Qlko4dCBI3XziT3XTjdm4kyKtpy9ky3uVksIYsSFWXKHTHOiCDaxNKdecQKbhQnD/9ELWxxr98D5ecQ4="}}'
128+
129+
# 3. Deploy a contract instance
130+
curl -s http://localhost:8000 -H 'Content-Type: application/json' \
131+
-d '{"jsonrpc":"2.0","id":1,"method":"sendTransaction","params":{"transaction":"AAAAAgAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAGQAAAAAAAAAAwAAAAEAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEAAAAAAAAAGAAAAAMAAAAAAAAAAAAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAFdPOLtg6vmmrgodRyN6P3wk1UfHrQxVekpbnsYYOcpvAAAAAAAAAAAAAAAAAAAAARJVMbgAAABAnLtNirBI7XdD2xwH3ws3rTDEhCxJ8mCRNU66d7b4MR2Ih9WtZzqb6akBqK6yA1GIavzVa7ahq2FNBflk+JpOBg=="}}'
132+
133+
# 4. Invoke foo() via traceTransaction — the trace comes back inline
134+
curl -s http://localhost:8000 -H 'Content-Type: application/json' \
135+
-d '{"jsonrpc":"2.0","id":1,"method":"traceTransaction","params":{"transaction":"AAAAAgAAAAADoQe/884Qvh1w3RjnS8CZZ+TWMJulDV8d3IZkElUxuAAAAGQAAAAAAAAABAAAAAEAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAEAAAAAAAAAGAAAAAAAAAABaiD+wakIF3Ol8jzjcPkl8jY0blEEON3W1A9rJxHBNOAAAAADZm9vAAAAAAAAAAAAAAAAAAAAAAESVTG4AAAAQKB9w/QmdK59UzXVbxXJp+5qfNpFSa495yajOyPM5KmYblE3/AbWqnnZMxTiBea0ShGZehgvo12AIyw48Lb1Xw0="}}'
136+
```
137+
138+
The final call returns the result inline. The `trace` field is itself a JSONL string (one JSON record per executed WebAssembly instruction); it is shown decoded here for readability:
139+
140+
```jsonc
141+
{
142+
"jsonrpc": "2.0",
143+
"id": 1,
144+
"result": {
145+
"hash": "c7099cbe10a9bfa1cdf9c9d368e1e1c932f535a70e4403b7aa409ce19fc36805",
146+
"status": "SUCCESS",
147+
"ledger": "4",
148+
"latestLedger": "4",
149+
"latestLedgerCloseTime": "1716000000",
150+
"trace": [
151+
{"pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}},
152+
{"pos": 11, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}},
153+
{"pos": 19, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}},
154+
{"pos": null, "instr": ["block"], "stack": [], "locals": {}},
155+
{"pos": 3, "instr": ["const", "i64", 2], "stack": [], "locals": {}}
156+
]
157+
}
158+
}
159+
```
160+
161+
Each trace record captures the VM state at instruction entry: `pos` is the instruction's byte offset in the binary (`null` for synthetic instructions), `instr` is the instruction and its operands, and `stack`/`locals` are the value stack and locals as `[type, value]` pairs. See [docs/interpreter.md](docs/interpreter.md) for the full trace format.
162+
163+
#### Walk through a contract lifecycle
164+
165+
The bundled demo deploys and invokes a Soroban contract end-to-end (create account → upload wasm → deploy → invoke):
166+
167+
```bash
168+
uv run python -m komet_node.demo src/tests/integration/data/wasm/empty.wat
169+
```
170+
171+
This produces `state.kore` plus `state_<n>_<step>.pretty` files under `./out`, letting you inspect exactly how the formal state evolves. (Requires `wat2wasm` from [`wabt`](https://github.com/WebAssembly/wabt) on your `PATH`.)
172+
173+
---
174+
175+
## For Developers
176+
177+
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.
178+
179+
1. Install [VS Code](https://code.visualstudio.com/) and the [Dev Containers extension](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers).
180+
2. Open this repository in VS Code and choose **Reopen in Container** when prompted.
181+
3. Once the container finishes building, build the semantics and run the test suite:
182+
183+
```bash
184+
make kdist-build # compile the K semantics (first run only; takes a while)
185+
make test-unit # quick sanity check
186+
```
187+
188+
Common tasks are driven by `make` (see the [Makefile](Makefile) for the complete list):
189+
190+
| Target | Description |
191+
|---|---|
192+
| `make kdist-build` | Compile the K semantics (required before running integration tests) |
193+
| `make build` | Build the wheel |
194+
| `make test-unit` | Run unit tests |
195+
| `make test-integration` | Run integration tests |
196+
| `make test` | Run the full test suite |
197+
| `make cov` | Run tests with a coverage report |
198+
| `make check` | Run all style/type checks (flake8, mypy, autoflake, isort, black) |
199+
| `make format` | Auto-format the codebase |
200+
201+
To build the node from source use:
7202

8203
```bash
9204
make build
10205
pip install dist/*.whl
11206
```
12207

208+
### Documentation
13209

14-
## For Developers
210+
- [Architecture overview](docs/architecture.md) — how the pieces fit together
211+
- [Server](docs/server.md) — the RPC layer, state lifecycle, and full method reference
212+
- [Interpreter](docs/interpreter.md) — transaction → K step translation
213+
- [K semantics](docs/node-semantics.md) — the on-chain execution model
15214

16-
Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
215+
---
17216

18-
* `make build`: Build wheel
19-
* `make check`: Check code style
20-
* `make format`: Format code
21-
* `make test-unit`: Run unit tests
22-
* `make test-integration`: Run integration tests
217+
## About
23218

219+
`komet-node` is developed by [Runtime Verification](https://runtimeverification.com/). It builds on [Komet](https://github.com/runtimeverification/komet), the K semantics of Soroban smart contracts, and the [K Framework](https://github.com/runtimeverification/k).

‎src/komet_node/interpreter.py‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,10 @@ def run_request_file(self, input_file: Path, request_str: str) -> InterpreterRes
337337
empty and request.json exists, reads the file, dispatches #handleRequest, then
338338
removes the file and halts — leaving the updated idle state as output.
339339
"""
340+
# Resolve to an absolute path before temp_working_directory() chdir's away,
341+
# otherwise a relative state file (e.g. the default `state.kore`) would be
342+
# looked up inside the temp dir and krun would fail with "File does not exist".
343+
input_file = input_file.resolve()
340344
with temp_working_directory() as root:
341345
(root / REQUEST_FILE).write_text(request_str)
342346

0 commit comments

Comments
 (0)