perf(traceTransaction): embed trace via string concatenation

The trace file is JSONL already produced by the semantics, so decoding
each record with String2JSON and re-encoding the whole array via
JSON2String was a redundant round-trip whose cost scales with the trace
(which can be very large). Trust the file and build the result array by
concatenating the lines with commas inside brackets, running only the
small id through the JSON encoder.

Author: RaoulSchaffranek

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` parsed into a JSON array (one record per executed instruction), 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
 

src/komet_node/kdist/node.md

@@ -527,47 +527,74 @@ 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`. The file is JSONL (one JSON record per executed instruction); we parse
-it into a JSON array so the result is structured data rather than an opaque string. Responds
-with that array — empty when the transaction ran no instructions — 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, [ #parseTraceLines( {#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 ) )
 ```
 
-`#parseTraceLines` turns the JSONL trace text into a `JSONs` list, parsing each newline-
-delimited record with `String2JSON`. Empty segments (a leading/blank line, or the empty
-tail after the final record's trailing newline) are skipped, so an empty file yields `.JSONs`
-(an empty array).
+`#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 JSONs ::= #parseTraceLines( String ) [function, symbol(parseTraceLines)]
- // -------------------------------------------------------------------------------
-    rule #parseTraceLines( "" ) => .JSONs
+    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 #parseTraceLines( S ) => String2JSON( S ) , .JSONs
+    rule #traceElems( S ) => S
       requires S =/=String "" andBool findString( S, "\n", 0 ) <Int 0
 
-    // Split off the first line and recurse on the rest.
-    rule #parseTraceLines( S )
-      => String2JSON( substrString( S, 0, findString( S, "\n", 0 ) ) )
-       , #parseTraceLines( substrString( S, findString( S, "\n", 0 ) +Int 1, lengthString( S ) ) )
+    // 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 #parseTraceLines( S )
-      => #parseTraceLines( substrString( S, 1, lengthString( S ) ) )
+    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