runtimeverification · RaoulSchaffranek · Jul 2, 2026 · Jul 3, 2026 · Jul 3, 2026 · Jul 3, 2026
diff --git a/docs/architecture.md b/docs/architecture.md
@@ -51,7 +51,7 @@ flowchart TB
 
 → **[Detailed documentation](server.md)**
 
-The server implements six RPC methods — `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`, and `traceTransaction` — and the K semantics answer all of them.
+The server implements seven RPC methods — `getHealth`, `getNetwork`, `getLatestLedger`, `sendTransaction`, `getTransaction`, `getLedgerEntries`, and `traceTransaction` — and the K semantics answer all of them. 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.
 
@@ -92,6 +92,7 @@ All of the server's input and output artifacts live in one directory, the *io di
 | `receipts/receipt_<hash>.json` | persistent | the semantics (on success) or the server (on failure) | one stored receipt per transaction, keyed by tx hash, answering `getTransaction`. Each is `{status, ledger, createdAt, envelopeXdr, resultXdr, 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 this file's contents. |
 | `requests/request_<n>.json` | persistent | the server | an archive of each incoming JSON-RPC request, numbered by a monotonic counter, kept for debugging. |
+| `wasms/<hash>.wasm` | persistent | the server | the raw bytes of each successfully uploaded wasm module, keyed by hex sha256. The K state stores modules parsed (`ModuleDecl`), so `getLedgerEntries` CONTRACT_CODE entries read the original bytes from here. |
 | `request.json` | transient | the server | the request envelope for the call in flight (`method`, `id`, `now`, and method-specific fields). The semantics remove it once they respond. |
 | `response.json` | transient | the semantics | the JSON-RPC response (`{jsonrpc, id, result}`) for the most recent call. The server reads it back; it is absent when a transaction gets stuck. |
 
@@ -102,7 +103,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/"]
+    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 -->|"yes"| reuse["use existing state.kore<br/>seed metadata.json if missing · ensure artifact dirs exist"]
     init --> ready(["ready for requests"])
     reuse --> ready
@@ -177,6 +178,6 @@ sequenceDiagram
 
 - `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
 - `simulateTransaction` (dry-run without state mutation)
-- `getEvents`, `getLedgerEntries`, `getFeeStats` and other read-only RPC methods
+- `getEvents`, `getFeeStats` and other read-only RPC methods (`getLedgerEntries` is implemented for the entry types the K state tracks: `ACCOUNT`, `CONTRACT_DATA`, `CONTRACT_CODE`)
 - `ExtendFootprintTTL` and `RestoreFootprint` operations
 - `SCVec` / `SCMap` contract-argument types in the request encoder (`scval_to_json`)
diff --git a/docs/node-semantics.md b/docs/node-semantics.md
@@ -39,7 +39,7 @@ insert-handleRequestFile → handleRequestFile
          ▼
 #dispatchMethod(method, request)        ← routes on the "method" field
          │
-         ├─ getHealth / getNetwork / getLatestLedger / getTransaction / traceTransaction → #respond(...)
+         ├─ getHealth / getNetwork / getLatestLedger / getTransaction / getLedgerEntries / traceTransaction → #respond(...)
          │
          └─ sendTransaction → #runTx → run steps
                 → #finalizeTx → record receipt + bump ledger → #respond(...)
@@ -62,6 +62,7 @@ If `request.json` is absent, `insert-handleRequestFile` does not fire and K halt
 - `getNetwork` → `{ "friendbotUrl": null, "passphrase": ..., "protocolVersion": ... }` (passphrase/version come from the request, keeping the semantics network-agnostic)
 - `getLatestLedger` → reads `metadata.json` and returns `{ "id": <64 zeros>, "protocolVersion": ..., "sequence": <latest_ledger> }`
 - `getTransaction` → reads the hash's `receipts/receipt_<hash>.json` file; returns the stored receipt merged with the current `latestLedger`/`latestLedgerCloseTime`, or `{ "status": "NOT_FOUND", ... }` when the file is absent
+- `getLedgerEntries` → looks each *key descriptor* of the request up in the world-state cells (`<accounts>`, `<contracts>`, `<contractData>`, `<contractCodes>`) and responds with `{ "entries": [...], "latestLedger": <int> }`. The server decodes the base64 `LedgerKey` XDR into the descriptors beforehand and re-encodes the found entries as `LedgerEntryData` XDR afterwards (`ledger_entries.py`) — the entries in K's response are an intermediate JSON shape (per-kind payloads such as `balance`, `wasmHash`, or an ScVal value serialised by `#scVal2JSON`, the inverse of `#decodeArg`). Keys that match nothing are skipped via an `[owise]` rule — per the spec they are not an error
 
 `#respond(ID, RESULT)` is the shared terminal: it writes the JSON-RPC envelope to `response.json`, removes `request.json`, and sets the exit code to 0.
 
@@ -141,6 +142,10 @@ rule HexBytes(S)  => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE)
   requires lengthString(S) >Int 0
 ```
 
+### `Bytes2Hex(Bytes) → String`
+
+The inverse direction is K's built-in `Bytes2Hex` (hook `BYTES.bytes2hex`): it encodes `Bytes` as a lowercase, zero-padded hex string. The `getLedgerEntries` rules use it to report hashes, addresses, and `ScBytes` values to the server.
+
 ### `string2WasmToken(String) → WasmStringToken`
 
 `string2WasmToken` wraps a K `String` into a `WasmStringToken` (`hook(STRING.string2token)`). It is required because `callTx` expects a `WasmString` for the function name.

diff --git a/docs/notes.md b/docs/notes.md
@@ -13,7 +13,8 @@
 | [`server.py`](server.md) — `StellarRpcServer` | Long-running HTTP/JSON-RPC server wrapping the one-shot K interpreter; `handle_rpc` dispatch; owns the io-dir files. Holds no ledger or receipt state. |
 | [`transaction.py`](transaction.md) — `TransactionEncoder` | XDR → request envelope + (for wasm uploads) kasmer steps; address/contract-id helpers. |
 | [`interpreter.py`](interpreter.md) — `NodeInterpreter` | Runs request envelopes through `llvm_interpret`; persists `state.kore`. No `kast`↔`kore` whole-config conversions. |
-| `scval.py` | XDR `SCVal` ↔ Komet `SCValue` (`scvalue_from_xdr`) and XDR `SCVal` → request JSON (`scval_to_json`). |
+| `scval.py` | XDR `SCVal` ↔ Komet `SCValue` (`scvalue_from_xdr`), XDR `SCVal` ↔ request/response JSON (`scval_to_json`, `scval_from_json`). |
+| `ledger_entries.py` | `getLedgerEntries` XDR translation: base64 `LedgerKey` → key descriptors for the semantics, intermediate entries → base64 `LedgerEntryData`. |
 | [`kdist/node.md`](node-semantics.md) | The K RPC layer: reads `request.json`, dispatches, updates `metadata.json` and the per-transaction `receipts/` files, writes `response.json`. |
 
 State lives in the io dir as `state.kore` (KORE world state) and `metadata.json` (ledger counter), with per-transaction receipts and traces under `receipts/` and `traces/`. See [architecture.md](architecture.md).
@@ -22,7 +23,7 @@ State lives in the io dir as `state.kore` (KORE world state) and `metadata.json`
 
 ## Tests (`src/tests/integration/`)
 
-- `test_server.py` drives the running HTTP server end-to-end. It exercises the read-only methods, `sendTransaction` + `getTransaction`, ledger increments, the full lifecycle (create → upload wasm → deploy → invoke), and the `traceTransaction` flows. `test_call_tx_with_args` deploys `args.wat` and calls functions with `bool`, `u32`, `i32`, `u64`, `i64`, `u128`, `i128`, and `symbol` arguments, exercising the `scval_to_json` / `#decodeArg` pipeline.
+- `test_server.py` drives the running HTTP server end-to-end. It exercises the read-only methods, `sendTransaction` + `getTransaction`, ledger increments, the full lifecycle (create → upload wasm → deploy → invoke), the `traceTransaction` flows, and `getLedgerEntries` (account, contract code, contract instance, and persistent storage entries via `storage.wat`, plus its parameter validation). `test_call_tx_with_args` deploys `args.wat` and calls functions with `bool`, `u32`, `i32`, `u64`, `i64`, `u128`, `i128`, and `symbol` arguments, exercising the `scval_to_json` / `#decodeArg` pipeline.
 - `test_integration.py` and `test_unit.py` hold small sanity checks.
 
 Run with `make test` (requires `make kdist-build` first).
@@ -35,4 +36,5 @@ The tests do not yet cover `bytes` / `address` SCVal arguments or `SCVec` / `SCM
 
 - `resultXdr` / `resultMetaXdr` are empty stubs (contract return values not surfaced).
 - `SCVec` / `SCMap` contract arguments are not yet encoded.
-- `simulateTransaction`, `getEvents`, `getLedgerEntries`, `getFeeStats`, and TTL/footprint operations are not implemented.
+- `simulateTransaction`, `getEvents`, `getFeeStats`, and TTL/footprint operations are not implemented.
+- `getLedgerEntries` covers the entry types the K state tracks (`ACCOUNT`, `CONTRACT_DATA`, `CONTRACT_CODE`); other key types are reported as not found. `lastModifiedLedgerSeq` is approximated by the current ledger (per-entry modification ledgers are not tracked), and only the balance is real in `ACCOUNT` entries (sequence number, thresholds, etc. are synthesised constants).
diff --git a/docs/server.md b/docs/server.md
@@ -64,7 +64,7 @@ Once the socket is bound, `serve` logs three lines to stderr: whether it is star
 ```
 startup (state.kore absent):
           → empty_config() → state.kore ; metadata.json {latest_ledger:0}
-          → create receipts/ traces/ requests/
+          → create receipts/ traces/ requests/ wasms/
 
 per successful transaction:
           → the semantics run the steps (trace → traces/trace_<hash>.jsonl),
@@ -143,6 +143,23 @@ All methods are answered by the K semantics and follow the [Stellar RPC specific
 
 `resultXdr` and `resultMetaXdr` are currently empty stubs. The receipt carries no trace — use `traceTransaction` with the same hash to fetch it.
 
+### `getLedgerEntries`
+
+`getLedgerEntries` takes `keys` (an array of up to 200 base64-encoded `LedgerKey` XDR strings; required) and an optional `xdrFormat` (only `"base64"` is supported — `"json"` is rejected with `-32602`). It returns the entries found for the supported key types — `ACCOUNT`, `CONTRACT_DATA` (both the contract-instance entry and persistent/temporary storage), and `CONTRACT_CODE` — the ones the K world state tracks. Keys that do not resolve (unknown, or of an untracked type) are not an error; they are simply absent from `entries`.
+
+**Response** (`latestLedger` and `lastModifiedLedgerSeq` are JSON numbers; `liveUntilLedgerSeq` appears only on Soroban entries):
+```json
+{
+  "entries": [
+    { "key": "<base64 LedgerKey>", "xdr": "<base64 LedgerEntryData>",
+      "lastModifiedLedgerSeq": 4, "liveUntilLedgerSeq": 4095 }
+  ],
+  "latestLedger": 4
+}
+```
+
+This is the one method whose response the server post-processes: the semantics look the keys up in the K state and answer with intermediate JSON entries, and `ledger_entries.py` re-encodes them as `LedgerEntryData` XDR (K cannot produce XDR). Because the K state keeps uploaded wasm parsed, the server stores the raw bytes under `wasms/<hash>.wasm` at upload time and reattaches them to `CONTRACT_CODE` entries. The semantics do not track per-entry modification ledgers, so `lastModifiedLedgerSeq` reports the current ledger; `ACCOUNT` entries carry the real balance but synthesised constants for the remaining required fields (sequence number 0, master weight 1, no signers).
+
 ---
 
 ## Failure fallback
@@ -161,4 +178,4 @@ komet-node [--host HOST] [--port PORT] [--io-dir DIR]
 |---|---|---|
 | `--host` | `localhost` | Bind address |
 | `--port` | `8000` | Port |
-| `--io-dir` | a fresh temp dir | Directory holding every artifact (`state.kore`, `metadata.json`, `receipts/`, `traces/`, `requests/`) |
+| `--io-dir` | a fresh temp dir | Directory holding every artifact (`state.kore`, `metadata.json`, `receipts/`, `traces/`, `requests/`, `wasms/`) |