feat: decode composite (vec/map) call arguments; raise recursion limit

README.md

@@ -123,71 +123,83 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \
   -d '{"jsonrpc":"2.0","id":1,"method":"traceTransaction","params":{"hash":"c7099cbe10a9bfa1cdf9c9d368e1e1c932f535a70e4403b7aa409ce19fc36805"}}'
 ```
 
-`traceTransaction` returns the stored trace as its result: a JSON array with one record per executed WebAssembly instruction.
+`traceTransaction` returns the stored trace as its result: a JSON array of records, one per executed WebAssembly instruction plus the higher-level records described below. Every record carries a `kind` field naming what it is, so a consumer dispatches on that one field without inspecting the rest of the record's shape.
 
 ```jsonc
 {
   "jsonrpc": "2.0",
   "id": 1,
   "result": [
     {
-      "pos": null, "instr": ["callContract"],
+      "kind": "ledger", "sequence": 4, "timestamp": 0,
+      "accounts": [{"account": {"type": "address", "addrType": "account", "value": "03a107bf…"}, "balance": 10000000000}],
+      "contracts": [], "codes": []
+    },
+    {
+      "kind": "callContract",
       "from": {"type": "address", "addrType": "account",  "value": "03a107bff3ce10be1d70dd18e74bc09967e4d6309ba50d5f1ddc8664125531b8"},
       "to":   {"type": "address", "addrType": "contract", "value": "6a20fec1a9081773a5f23ce370f925f236346e510438ddd6d40f6b2711c134e0"},
       "function": "foo", "args":[], "depth":1, "storage":[]
     },
-    {"pos": 3,    "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null},
-    {"pos": 11,   "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null},
-    {"pos": 19,   "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null},
-    {"pos": null, "instr": ["block"],                 "stack": [], "locals": {}, "mem": null},
-    {"pos": 3,    "instr": ["const", "i64", 2],       "stack": [], "locals": {}, "mem": null},
-    {"pos": null, "instr": ["endWasm"], "success":true, "depth":1, "result": {"type": "void"}}
+    {"kind": "instr", "pos": 3,    "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {}},
+    {"kind": "instr", "pos": 11,   "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576]}},
+    {"kind": "instr", "pos": 19,   "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576]}},
+    {"kind": "instr", "pos": null, "instr": ["block"],                 "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576], "2": ["i32", 1048576]}},
+    {"kind": "instr", "pos": 3,    "instr": ["const", "i64", 2],       "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576], "2": ["i32", 1048576]}},
+    {"kind": "endWasm", "success": true, "depth": 1, "result": {"type": "void"}}
   ]
 }
 ```
 
-A trace can contain five kinds of records:
-
+A trace can contain six kinds of records:
+
+- `ledger`
 - `callContract`
-- Wasm instruction records
+- Wasm instruction records (`kind: "instr"`)
 - `hostCall`
 - `contractData`
 - `endWasm`
 
-The example above only has three of these: `callContract`, instruction records, and `endWasm`. `foo()` doesn't touch storage or call any host functions, so no `contractData` or `hostCall` records show up.
- 
+The example above only has four of these: `ledger`, `callContract`, instruction records, and `endWasm`. `foo()` doesn't touch storage or call any host functions, so no `contractData` or `hostCall` records show up.
+
 Here's what each record type carries:
-
+
+- `ledger`: written once, as the trace's first record, before any step runs. Gives the ledger sequence and timestamp and every account's balance, so a consumer can seed its view of chain state and replay what follows on top of it rather than seeing only the parts a contract happened to touch. `contracts` and `codes` are reserved for contract-instance and uploaded-code metadata and are currently always empty — read an empty list as "not reported" rather than "none exist". This is the one record komet-node emits itself; the rest come from komet.
 - `callContract`: logged for each contract call in the transaction, including contract-to-contract calls. Records the caller, the callee, the function name, the arguments, the call depth, and the callee's storage before the call runs.
-- Instruction records: logged at each WebAssembly instruction's 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. `mem` is a snapshot of linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot).
-- `hostCall`: logged when the contract calls a host function. `instr` gives `["hostCall", moduleId, functionId]`, identifying which host function ran. `locals` holds the function's arguments, indexed by position. Host calls don't use the stack, so `stack` is absent.
+- Instruction records: logged at each WebAssembly instruction's 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. `mem` is a snapshot of linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot). `globals` is the executing module's WebAssembly globals keyed by module-relative index; unlike `mem` it is repeated in full on every record and is never `null`.
+- `hostCall`: logged when the contract calls a host function. `module` and `function` identify which host function ran. `locals` holds the function's arguments, indexed by position. Host calls don't use the stack, so `stack` is absent.
   Here's a `hostCall` record for a call to `put_contract_data`, module id `l`, function id `_`:
 ```jsonc
   {
-    "pos": null,
-    "instr": ["hostCall", "l", "_"],
+    "kind": "hostCall",
+    "module": "l",
+    "function": "_",
     "locals": {"2": ["i64",0], "1": ["i64",530242871224172548], "0": ["i64",45954062]}
   }
 ```
- 
-- `contractData`: logged for storage updates. Gives the contract and the storage type (`instance`, `persistent`, or `temporary`). A `put` carries the key and value as its two args; a `del` carries only the key.
+
+- `contractData`: logged for storage updates. Gives the contract, the `operation` (`put` or `del`) and the `durability` (`instance`, `persistent`, or `temporary`). A `put` carries the key and value as its two args; a `del` carries only the key.
   Here's a `contractData` record for a `put`, followed by a `del` on the same key:
 ```jsonc
   {
-    "pos": null,
-    "instr": ["contractData", "put", "temporary"],
+    "kind": "contractData",
+    "operation": "put",
+    "durability": "temporary",
     "contract": {"type": "address", "addrType": "contract", "value": "746573742d7363"},
     "args": [{"type": "symbol", "value": "foo"}, {"type": "u32", "value": 123456789}]
   }
   {
-    "pos": null,
-    "instr": ["contractData", "del", "temporary"],
+    "kind": "contractData",
+    "operation": "del",
+    "durability": "temporary",
     "contract": {"type": "address", "addrType": "contract", "value": "746573742d7363"},
     "args": [{"type": "symbol", "value": "foo"}]
   }
 ```
-
-- `endWasm`: logged once at the end of a call. Records whether the call succeeded, its depth, and its result.
+
+- `endWasm`: logged once at the end of a call, for a normal return and a trap alike. Records whether the call succeeded, its depth, and its result.
+
+The array is exactly the stored trace file — komet-node adds nothing to it. Anything derivable from the records is left to the consumer: which contract is executing at a given record, for instance, follows from the `callContract` and `endWasm` boundaries around it.
 
 
 

docs/node-semantics.md

@@ -84,6 +84,7 @@ If `request.json` is absent, `insert-handleRequestFile` does not fire and K halt
 #runTx(request)
    => #enableTrace(traces/trace_<hash>.jsonl)     ← clear the trace file and point <ioDir> at it
    ~> setLedgerSequence(<latest_ledger from metadata.json>)
+   ~> #traceLedger                                ← write the ledger baseline as the trace's first record
    ~> #decodeSteps(<the "steps" array>)           ← KASMER runs each decoded step
    ~> #finalizeTx(request)
 ```
@@ -188,18 +189,32 @@ Tracing is always on. Before running the steps, `#enableTrace` clears the transa
 **Trace format** (one JSON record per line):
 
 ```json
-{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}, "mem": null}
+{"kind": "instr", "pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}, "mem": null}
 ```
 
 | Field | Description |
 |---|---|
+| `kind` | Names the record; always `"instr"` for an instruction record. Every trace record carries one, so a consumer dispatches on this field alone |
 | `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 |
 | `mem` | Linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot) |
+| `globals` | The executing module's WebAssembly globals, keyed by module-relative index, as `[type, value]` pairs. Repeated in full on every record (never `null`, unlike `mem`) |
 
-Instruction records are one of several trace record kinds (`callContract`, `hostCall`, `contractData`, and `endWasm` are the others); see the [Trace a transaction](../README.md#trace-a-transaction) section of the README for all five.
+Instruction records are one of several trace record kinds (`ledger`, `callContract`, `hostCall`, `contractData`, and `endWasm` are the others); see the [Trace a transaction](../README.md#trace-a-transaction) section of the README, and komet's [`docs/tracing.md`](https://github.com/runtimeverification/komet/blob/master/docs/tracing.md) for the full format of each. The `ledger` record is the exception: komet never emits one, so it is built and documented here — see below.
+
+**The ledger baseline record.** `#traceLedger` writes one `ledger` record as the trace's first line, before any step runs:
+
+```json
+{"kind": "ledger", "sequence": 3, "timestamp": 0,
+ "accounts": [{"account": {"type": "address", "addrType": "account", "value": "6964b7…"}, "balance": 10000000000}],
+ "contracts": [], "codes": []}
+```
+
+It describes the ledger as the transaction's steps *found* it, which is what lets a debugger show chain state at any point of a recorded execution rather than only the parts a contract touched: the debugger seeds its view from this record and replays the storage writes and contract calls that follow on top of it.
+
+Because the baseline precedes the steps, a transaction that creates its own account reports no accounts — its `setAccount` step runs afterwards. A later transaction sees what earlier ones left behind, which is the case that matters (the debugger traces the last transaction of a sequence). Balances are read straight from the `<accounts>` cells by `#collectAccounts`, which gathers them one per rewrite step because a K cell collection cannot be passed to a function, and are serialized by `generateLedgerTrace`/`AccountBalances2JSONs` in `node.md` — the cells belong to komet, but the record is komet-node's, so the builders sit beside their only caller. `contracts` and `codes` are reserved for contract-instance and uploaded-code metadata and are currently always empty, so a consumer must read an empty list as "not reported" rather than "none exist".
 
 ---
 

docs/server.md

@@ -185,14 +185,16 @@ Failures are reported in the result body, matching real stellar-rpc; only an und
 
 `traceTransaction` is **not part of the Stellar RPC specification** — it exists only on komet-node, and clients must not expect it from real Stellar RPC endpoints. It keeps its plain name rather than a vendor-prefixed one (`komet_traceTransaction`): the official spec has no method of that name and none is announced, so there is no collision to avoid, and renaming would break every existing client for no gain. If stellar-rpc ever claims the name, the method will be renamed with a prefix.
 
-`traceTransaction` retrieves the instruction trace of a previously submitted transaction. It takes a `hash` parameter (the same one `getTransaction` takes) and returns the trace that `sendTransaction` stored for that transaction. The result is a JSON array with one record per executed WebAssembly instruction (empty when the transaction ran no instructions), or `null` when no transaction with that hash exists.
+`traceTransaction` retrieves the execution trace of a previously submitted transaction. It takes a `hash` parameter (the same one `getTransaction` takes) and returns the trace that `sendTransaction` stored for that transaction. The result is a JSON array of records — one per executed WebAssembly instruction, plus the `ledger` baseline and the Soroban VM records described in the [README](../README.md#trace-a-transaction) — or `null` when no transaction with that hash exists. Each record names itself with a `kind` field.
 
 ```json
 [
-  {"pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null}
+  {"kind": "instr", "pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {}}
 ]
 ```
 
+The server reads the stored file and streams it back in one linear pass, passing each record through verbatim: the served array is exactly the trace file. It derives nothing, by design — a trace runs to hundreds of megabytes, so anything a consumer can compute for itself should not be duplicated per record here. Which contract is executing at a given record is the standing example: a `callContract` names its callee and an `endWasm` closes it, so the debug adapter folds it out of boundaries it already walks.
+
 ### `getTransaction`
 
 `getTransaction` reads the hash's `receipts/receipt_<hash>.json` file. The `hash` parameter must be a 64-character hex string; anything else is rejected with `-32602 Invalid params` (this and `traceTransaction` share the validation).

pyproject.toml

@@ -10,7 +10,7 @@ readme = "README.md"
 requires-python = "~=3.10"
 dependencies = [
     "stellar-sdk>=13.2.1",
-    "komet@git+https://github.com/runtimeverification/komet.git@v0.1.86",
+    "komet@git+https://github.com/runtimeverification/komet.git@v0.1.88",
     "kframework>=7.1.323,<7.1.324",
 ]
 

src/komet_node/__init__.py

@@ -0,0 +1,13 @@
+from __future__ import annotations
+
+import sys
+
+# Parsing and traversing the KORE world-state configuration (via pyk's recursive-descent
+# KORE parser and the recursive cell rewrites in ``interpreter.py``) recurses with the depth
+# and size of the term. Large real contracts produce configurations far deeper than CPython's
+# default recursion limit (1000), which otherwise surfaces as a ``RecursionError`` mid-request.
+# Raise the ceiling to match the rest of the K tooling (pyk sets 10**7; komet sets its own
+# limit at import). This is the sole cross-cutting entry point, so setting it here covers the
+# server process, direct interpreter use, and the encoders. server.py backs this with a large
+# serve-thread stack so a deep term raises a catchable error rather than a SIGSEGV.
+sys.setrecursionlimit(10**7)