Merge pull request #28 from runtimeverification/fix/trace-transaction-json-array

fix: return traceTransaction result as a JSON array

Author: RaoulSchaffranek

README.md

@@ -123,7 +123,7 @@ 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. The trace is a JSONL string (one JSON record per executed WebAssembly instruction); it is shown decoded here for readability:
+`traceTransaction` returns the stored trace as its result: a JSON array with one record per executed WebAssembly instruction.
 
 ```jsonc
 {

docs/architecture.md

@@ -90,7 +90,7 @@ All of the server's input and output artifacts live in one directory, the *io di
 | `state.kore` | persistent | `NodeInterpreter` | the full K world-state configuration — accounts, contract code (including uploaded wasm `ModuleDecl`s), contract storage, ledger metadata — serialized in KORE. Read before each run and rewritten after a successful one. |
 | `metadata.json` | persistent | the K semantics | `{"latest_ledger": N}` — the server ledger counter, bumped by 1 per committed transaction. |
 | `receipts/receipt_<hash>.json` | persistent | the semantics and the server (on success — the server rewrites the semantics' internal `returnValue` field into `resultXdr`/`resultMetaXdr`), or the server alone (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. |
+| `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 these records as a JSON array. |
 | `ledgers/ledger_<seq>.json` | persistent | the server (on success) | one record per closed ledger — `{sequence, txHash, closedAt, hash, headerXdr, metadataXdr}` — the ledger→transaction index behind `getTransactions` and `getLedgers`. Written in Python because the header artifacts are XDR, which K cannot construct. |
 | `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. |

docs/node-semantics.md

@@ -105,7 +105,7 @@ The trace is not part of the receipt — the executing steps already appended it
 
 ### traceTransaction
 
-`traceTransaction` is a komet-specific extension, not part of the Stellar RPC specification (see [server.md](server.md#tracetransaction-komet-specific-extension)). It is a read-only lookup: it takes a `hash` (the same parameter `getTransaction` takes) and responds with the contents of `traces/trace_<hash>.jsonl`, or `null` when no trace file exists for that hash. Because tracing is always on, every `sendTransaction` writes this file.
+`traceTransaction` is a komet-specific extension, not part of the Stellar RPC specification (see [server.md](server.md#tracetransaction-komet-specific-extension)). It is a read-only lookup: it takes a `hash` (the same parameter `getTransaction` takes) and responds with the contents of `traces/trace_<hash>.jsonl` as a JSON array (one record per executed instruction), or `null` when no trace file exists for that hash. Rather than decoding and re-encoding each record — a full round-trip whose cost scales with the (potentially very large) trace — the semantics trust that the file the tracer wrote is already valid JSON and build the array by string concatenation, joining the lines with commas inside `[` … `]`. Because tracing is always on, every `sendTransaction` writes this file.
 
 ### Two ways steps are delivered
 

docs/server.md

@@ -185,10 +185,12 @@ 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 on that transaction's receipt. The result is the trace itself: a JSONL string with one record per executed WebAssembly instruction, or `null` when no transaction with that hash exists.
+`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.
 
 ```json
-"<jsonl string>"
+[
+  {"pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}}
+]
 ```
 
 ### `getTransaction`

src/komet_node/kdist/node.md

@@ -527,21 +527,76 @@ the spec-mandated `resultXdr`/`resultMetaXdr` base64 XDR fields (K cannot constr
 
 Retrieve the execution trace of a previously submitted transaction, looked up by `hash` (the
 same parameter `getTransaction` takes). The trace was written to `traces/trace_<hash>.jsonl`
-by `sendTransaction`. Responds with the trace file's contents, or `null` when no trace file
-exists for that hash.
+by `sendTransaction`. The file is JSONL (one JSON record per executed instruction), and each
+line is already valid JSON produced by the semantics — so rather than decoding every record
+into a `JSON` term and re-encoding the whole array (a full round-trip whose cost scales with
+the trace, which can be very large), we build the result array by *string concatenation*:
+join the trusted lines with commas and wrap them in `[` … `]`. Responds with that array —
+empty when the transaction ran no instructions — or `null` when no trace file exists for that
+hash.
+
+Because the trace body is spliced in as raw text, `#respondTrace` writes the JSON-RPC
+envelope directly (mirroring `#respond`) instead of building a `JSON` term for `JSON2String`:
+only the small `id` value is serialized through the encoder.
 
 ```k
     rule <k> #dispatchMethod( "traceTransaction", REQ )
           => #respondTrace( #getJSON( "id", REQ ), #getString( "hash", REQ ) )
              ...
          </k>
 
-    rule <k> #respondTrace( ID, HASH ) => #respond( ID, {#readFile( #traceFile( HASH ) )}:>String ) ... </k>
+    rule <k> #respondTrace( ID, HASH )
+          => #writeFile( "response.json",
+                 "{\"jsonrpc\":\"2.0\",\"id\":"
+                   +String JSON2String( ID )
+                   +String ",\"result\":"
+                   +String #traceArray( {#readFile( #traceFile( HASH ) )}:>String )
+                   +String "}" )
+          ~> #remove( "request.json" )
+             ...
+         </k>
+         <exitCode> _ => 0 </exitCode>
       requires #fileExists( #traceFile( HASH ) )
+
     rule <k> #respondTrace( ID, HASH ) => #respond( ID, null ) ... </k>
       requires notBool #fileExists( #traceFile( HASH ) )
 ```
 
+`#traceArray` wraps the JSONL trace text in array brackets; `#traceElems` joins the
+newline-delimited records with commas without touching their contents. Empty segments (a
+leading/blank line, or the empty tail after the final record's trailing newline) are skipped
+via `#maybeComma`, which prefixes a separator only when a following record actually exists —
+so a trailing newline never yields a dangling comma, and an empty file yields `[]`.
+
+```k
+    syntax String ::= #traceArray( String )  [function, symbol(traceArray)]
+                    | #traceElems( String )  [function, symbol(traceElems)]
+                    | #maybeComma( String )  [function, symbol(maybeComma)]
+ // -----------------------------------------------------------------------
+    rule #traceArray( S ) => "[" +String #traceElems( S ) +String "]"
+
+    rule #traceElems( "" ) => ""
+
+    // No more newlines: the whole remaining string is the final record.
+    rule #traceElems( S ) => S
+      requires S =/=String "" andBool findString( S, "\n", 0 ) <Int 0
+
+    // Split off the first line and recurse; a comma is added only if the tail is non-empty.
+    rule #traceElems( S )
+      => substrString( S, 0, findString( S, "\n", 0 ) )
+         +String #maybeComma( #traceElems( substrString( S, findString( S, "\n", 0 ) +Int 1, lengthString( S ) ) ) )
+      requires findString( S, "\n", 0 ) >Int 0
+
+    // Empty leading line (the string starts with a newline): drop it and recurse.
+    rule #traceElems( S )
+      => #traceElems( substrString( S, 1, lengthString( S ) ) )
+      requires findString( S, "\n", 0 ) ==Int 0
+
+    rule #maybeComma( "" ) => ""
+    rule #maybeComma( S )  => "," +String S
+      requires S =/=String ""
+```
+
 ## simulateTransaction
 
 Run a single contract invocation against the current world state *without committing