Merge pull request #37 from runtimeverification/feat/tx-result-xdr

feat: real resultXdr/resultMetaXdr and FAILED transaction reporting

Author: RaoulSchaffranek

docs/architecture.md

@@ -89,7 +89,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 (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}`. |
+| `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. |
 | `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. |
@@ -177,7 +177,6 @@ sequenceDiagram
 
 ## What's not yet implemented
 
-- `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
 - `simulateTransaction` of upload/deploy host functions, auth recording, resource metering, `events`/`restorePreamble`/`stateChanges` (only invoke-contract dry runs with the return value are supported)
 - `getEvents` 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

docs/node-semantics.md

@@ -89,10 +89,14 @@ If `request.json` is absent, `insert-handleRequestFile` does not fire and K halt
 
 1. writes `metadata.json` with `latest_ledger + 1`,
 2. writes the receipt to `receipts/receipt_<hash>.json`:
-   `{ status: "SUCCESS", applicationOrder: 1, feeBump: false, envelopeXdr, resultXdr: "", resultMetaXdr: "", ledger, createdAt }`,
+   `{ status: "SUCCESS", applicationOrder: 1, feeBump: false, envelopeXdr, ledger, createdAt, returnValue }` — `returnValue` is
+   the contract call's return `ScVal`, JSON-encoded by `#scValToJSON` (or `null` when the
+   transaction made no contract call), read off the `<hostStack>` before the host is reset,
 3. responds with `{hash, status: "PENDING", latestLedger, latestLedgerCloseTime}`.
 
-A `sendTransaction` whose hash already has a receipt never reaches `#runTx`: dispatch answers `{hash, status: "DUPLICATE", latestLedger, latestLedgerCloseTime}` directly, without executing anything or advancing the ledger. (For wasm uploads the Python server also suppresses the `<program>` injection on duplicates, since those steps would run before dispatch.)
+The internal `returnValue` field never reaches an RPC client: the Python server immediately rewrites it into the spec-mandated `resultXdr`/`resultMetaXdr` base64 XDR fields (`_attach_result_xdr` in `server.py`), because K cannot construct XDR. To keep the return value observable here, `uncheckedCallTx` (unlike komet's `callTx`) does not `#resetHost` after the call; `#recordAndRespond` serialises the stack top and resets the host instead.
+
+A `sendTransaction` whose hash already has a receipt never reaches `#runTx`: dispatch answers `{hash, status: "DUPLICATE", latestLedger, latestLedgerCloseTime}` directly, without executing anything or advancing the ledger. (For wasm uploads the Python server also suppresses the `<program>` injection on duplicates, since those steps would run before dispatch.) The Python `_attach_result_xdr` rewrite is skipped for duplicates, so a resubmission never disturbs the stored receipt.
 
 The trace is not part of the receipt — the executing steps already appended it to `traces/trace_<hash>.jsonl`. Reaching `#finalizeTx` means the steps completed without getting stuck, so the status is `SUCCESS`. A failed transaction gets stuck before this point, `response.json` is never written, and the Python server records the `FAILED` receipt instead.
 

docs/notes.md

@@ -34,7 +34,9 @@ The tests do not yet cover `bytes` / `address` SCVal arguments or `SCVec` / `SCM
 
 ## Known gaps
 
-- `resultXdr` / `resultMetaXdr` are empty stubs (contract return values not surfaced).
+- `resultXdr` / `resultMetaXdr` are synthesised: `feeCharged` is 0, ledger-entry change
+  sets are empty, and the InvokeHostFunction success hash covers only the return value
+  (komet-node does not track fees, entry changes, or events).
 - `sendTransaction`'s `errorResultXdr` is always a generic `txMALFORMED` result (no per-cause codes such as `txBAD_SEQ` — sequence numbers, fees, and signatures are not modelled), and `diagnosticEventsXdr` is never populated (both fields are optional in the spec). `TRY_AGAIN_LATER` is never returned by design: it signals mempool backpressure, which cannot arise in a synchronous node without a mempool.
 - `SCVec` / `SCMap` contract arguments are not yet encoded.
 - The `xdrFormat` parameter is accepted on `getTransaction`, `sendTransaction`, `getTransactions`, `getLedgers`, and `getLedgerEntries`, but only the default `'base64'` is supported; `'json'` is rejected with `-32602`.

docs/server.md

@@ -204,14 +204,14 @@ Failures are reported in the result body, matching real stellar-rpc; only an und
 ```json
 {
   "status": "SUCCESS", "applicationOrder": 1, "feeBump": false,
-  "envelopeXdr": "<base64 XDR>", "resultXdr": "", "resultMetaXdr": "",
+  "envelopeXdr": "<base64 XDR>", "resultXdr": "<base64 XDR>", "resultMetaXdr": "<base64 XDR>",
   "ledger": 5, "createdAt": "1716000000",
   "latestLedger": 5, "latestLedgerCloseTime": "1716000000",
   "oldestLedger": 0, "oldestLedgerCloseTime": "0"
 }
 ```
 
-The ledger-range fields (`latestLedger` through `oldestLedgerCloseTime`) are present on every response, `NOT_FOUND` included. Every ledger contains exactly one transaction, so `applicationOrder` is always 1; fee-bump envelopes are not supported, so `feeBump` is always false. `resultXdr` and `resultMetaXdr` are currently empty stubs. The receipt carries no trace — use `traceTransaction` with the same hash to fetch it.
+The ledger-range fields (`latestLedger` through `oldestLedgerCloseTime`) are present on every response, `NOT_FOUND` included. Every ledger contains exactly one transaction, so `applicationOrder` is always 1; fee-bump envelopes are not supported, so `feeBump` is always false. `resultXdr` is a base64 `TransactionResult` (code `txSUCCESS` or `txFAILED`) and `resultMetaXdr` a base64 `TransactionMeta` v3; when the transaction invoked a contract, its return value is reported as `sorobanMeta.returnValue` inside the meta. Both are synthesised by the server (`result_xdr.py`) from the envelope and the return value the semantics recorded in the receipt — see [node-semantics.md](node-semantics.md). Fees and ledger-entry change sets in these structs are zero/empty (komet-node does not track them). `resultMetaXdr` is omitted on `FAILED` receipts — a failed run rolls back and produces no meta. The receipt carries no trace — use `traceTransaction` with the same hash to fetch it.
 
 Receipts are an internal format, not a stable one: receipts written by older komet-node versions stored `ledger` as a string and lack `applicationOrder`/`feeBump`, and `getTransaction` returns stored receipts verbatim. Start from a fresh io-dir after upgrading rather than resuming one with old receipts.
 
@@ -231,7 +231,7 @@ Receipts are an internal format, not a stable one: receipts written by older kom
 }
 ```
 
-Serialization follows real stellar-rpc: ledger sequences and the top-level close times are JSON numbers, and per-transaction `createdAt` is a number too (unlike the singular `getTransaction`, where it is a string — an upstream quirk). `resultXdr`/`resultMetaXdr` are omitted while the receipts carry empty stubs. Each ledger holds exactly one transaction on this node, so `applicationOrder` is always `1`. The `cursor` is a TOID-style stringified integer (`ledger << 32 | applicationOrder << 12`) naming the page's last transaction when the page is full, and empty otherwise; resume by passing it as `pagination.cursor` (without `startLedger`).
+Serialization follows real stellar-rpc: ledger sequences and the top-level close times are JSON numbers, and per-transaction `createdAt` is a number too (unlike the singular `getTransaction`, where it is a string — an upstream quirk). `resultXdr`/`resultMetaXdr` are populated from the stored receipt (real base64 XDR for a contract invocation) and omitted only when a receipt carries none. Each ledger holds exactly one transaction on this node, so `applicationOrder` is always `1`. The `cursor` is a TOID-style stringified integer (`ledger << 32 | applicationOrder << 12`) naming the page's last transaction when the page is full, and empty otherwise; resume by passing it as `pagination.cursor` (without `startLedger`).
 
 ### `getLedgers`
 
@@ -272,7 +272,9 @@ This is the one method whose response the server post-processes: the semantics l
 
 ## Failure fallback
 
-A failed transaction leaves the semantics stuck without writing `response.json`, so `interpreter.run` returns `None`. For `sendTransaction` the server then synthesises the response in Python: it writes a `FAILED` `receipts/receipt_<hash>.json` (so a later `getTransaction` finds it), without bumping the ledger, and returns `PENDING`. A stuck `simulateTransaction` run is answered with a result-level `{error, latestLedger}` and leaves no artifacts behind.
+A failed transaction leaves the semantics stuck without writing `response.json`, so `interpreter.run` returns `None`. For `sendTransaction` the server then synthesises the response in Python: it writes a `FAILED` `receipts/receipt_<hash>.json` (so a later `getTransaction` finds it) with a `txFAILED` `resultXdr` and no `resultMetaXdr`, without bumping the ledger, and returns `PENDING`. `ledger` on a `FAILED` receipt pins the latest ledger at failure time (the chain does not advance) and `createdAt` the submission time, with the same encoding as on `SUCCESS` receipts. A stuck `simulateTransaction` run is answered with a result-level `{error, latestLedger}` and leaves no artifacts behind.
+
+On the success path the server also post-processes the receipt the semantics wrote: `_attach_result_xdr` replaces the receipt's internal `returnValue` field (a JSON-encoded SCVal, or `null`) with the spec-mandated `resultXdr`/`resultMetaXdr` base64 XDR, which K cannot construct (skipped for a duplicate resubmission, whose receipt is already final). These are the only response contents the server builds itself.
 
 ---
 

src/komet_node/kdist/node.md

@@ -464,6 +464,13 @@ int64-as-string. Every ledger on this node contains exactly one transaction, so
 always false. (The Python failure fallback in server.py writes a `FAILED` receipt with the
 same field set — keep the two in sync.)
 
+The receipt also carries the contract call's return value (if the transaction made one):
+after `uncheckedCallTx` runs, the call's result `ScVal` is still sitting on the
+`<hostStack>` (see below), so we serialise it into the receipt's internal `returnValue`
+field and only then reset the host. The Python server immediately rewrites that field into
+the spec-mandated `resultXdr`/`resultMetaXdr` base64 XDR fields (K cannot construct XDR), so
+`returnValue` never reaches an RPC client.
+
 ```k
     rule <k> #finalizeTx( REQ )
           => #recordAndRespond(
@@ -477,24 +484,32 @@ same field set — keep the two in sync.)
     rule <k> #recordAndRespond( REQ, L )
           => #writeFile( "metadata.json", JSON2String({ "latest_ledger" : L +Int 1 }) )
           ~> #writeFile( #receiptFile( #getString( "txHash", REQ ) ),
-                 JSON2String( #txReceipt( REQ, L +Int 1 ) ) )
+                 JSON2String( #txReceipt( REQ, L +Int 1, #returnValueJSON( STACK ) ) ) )
+          ~> #resetHost
           ~> #respondTx( REQ, "PENDING", L +Int 1 )
              ...
          </k>
+         <hostStack> STACK </hostStack>
 
-    syntax JSON ::= #txReceipt( JSON, Int ) [function, symbol(txReceipt)]
- // ---------------------------------------------------------------------
-    rule #txReceipt( REQ, NEWL ) => {
+    syntax JSON ::= #txReceipt( JSON, Int, JSON ) [function, symbol(txReceipt)]
+ // ---------------------------------------------------------------------------
+    rule #txReceipt( REQ, NEWL, RETVAL ) => {
             "status"           : "SUCCESS",
             "applicationOrder" : 1,
             "feeBump"          : false,
             "envelopeXdr"      : #getString( "envelopeXdr", REQ ),
-            "resultXdr"        : "",
-            "resultMetaXdr"    : "",
             "ledger"           : NEWL,
-            "createdAt"        : #getString( "now", REQ )
+            "createdAt"        : #getString( "now", REQ ),
+            "returnValue"      : RETVAL
         }
 
+    // The return value of the transaction's contract call: the ScVal left on top of the
+    // host stack, or null when the transaction made no contract call.
+    syntax JSON ::= #returnValueJSON( HostStack ) [function, total, symbol(returnValueJSON)]
+ // ----------------------------------------------------------------------------------------
+    rule #returnValueJSON( VAL:ScVal : _ ) => #scValToJSON( VAL )
+    rule #returnValueJSON( _ )             => null                 [owise]
+
     rule <k> #respondTx( REQ, STATUS, LL )
           => #respond( #getJSON( "id", REQ ), {
                  "hash"                  : #getString( "txHash", REQ ),
@@ -1096,6 +1111,10 @@ SCVal arg encoding (key order also significant):
 
 `uncheckedCallTx` is like komet's `callTx` but it does not entail a return value check.
 
+Unlike `callTx`, it does not `#resetHost` after the call either: the call's return value is
+left on the `<hostStack>` so `#recordAndRespond` can serialise it into the receipt. The host
+is reset there instead (and each `uncheckedCallTx` clears the host cell before it runs, so a
+leftover value never bleeds into a later call).
 
 ```k
     syntax Step ::= uncheckedCallTx( from: Address, to: Address, func: WasmString, args: List)     [symbol(uncheckedCallTx)]
@@ -1104,11 +1123,70 @@ SCVal arg encoding (key order also significant):
         <k> uncheckedCallTx(FROM, TO, FUNC, ARGS)
          => allocObjects(ARGS)
          ~> callContractFromStack(FROM, TO, FUNC)
-         ~> #resetHost
             ...
         </k>
         // clear the host cell before contract calls
         (_:HostCell => <host> <hostStack> .HostStack </hostStack> ... </host>)
+```
+
+###############################################################################
+# ScVal serialisation
+
+`#scValToJSON` renders an `ScVal` as JSON for the receipt's internal `returnValue` field.
+The encoding mirrors the SCVal *argument* encoding accepted by `#decodeArg` above (and
+produced by `scval_to_json` in `scval.py`), extended with the value-only cases that can come
+back from a contract but never go in as arguments: `void`, `string`, `u256`, `vec`, `map`.
+The Python server decodes it with `scval_from_json` (`scval.py`) — keep the three in sync.
+Values with no JSON encoding (e.g. `Error`) render as `null`, i.e. as "no return value".
+
+```k
+    syntax JSON ::= #scValToJSON( ScVal ) [function, total, symbol(scValToJSON)]
+ // ----------------------------------------------------------------------------
+    rule #scValToJSON( SCBool(B)  ) => { "type" : "bool"   , "value" : B }
+    rule #scValToJSON( Void       ) => { "type" : "void" }
+    rule #scValToJSON( I32(V)     ) => { "type" : "i32"    , "value" : V }
+    rule #scValToJSON( U32(V)     ) => { "type" : "u32"    , "value" : V }
+    rule #scValToJSON( I64(V)     ) => { "type" : "i64"    , "value" : V }
+    rule #scValToJSON( U64(V)     ) => { "type" : "u64"    , "value" : V }
+    rule #scValToJSON( I128(V)    ) => { "type" : "i128"   , "value" : V }
+    rule #scValToJSON( U128(V)    ) => { "type" : "u128"   , "value" : V }
+    rule #scValToJSON( U256(V)    ) => { "type" : "u256"   , "value" : V }
+    rule #scValToJSON( Symbol(S)  ) => { "type" : "symbol" , "value" : S }
+    rule #scValToJSON( ScString(S)) => { "type" : "string" , "value" : S }
+    rule #scValToJSON( ScBytes(B) ) => { "type" : "bytes"  , "value" : #bytesToHex(B) }
+    rule #scValToJSON( ScAddress(Account(B))  ) => { "type" : "address" , "addrType" : "account"  , "value" : #bytesToHex(B) }
+    rule #scValToJSON( ScAddress(Contract(B)) ) => { "type" : "address" , "addrType" : "contract" , "value" : #bytesToHex(B) }
+    rule #scValToJSON( ScVec(L)   ) => { "type" : "vec"    , "value" : [ #scValsToJSONs(L) ] }
+    rule #scValToJSON( ScMap(M)   ) => { "type" : "map"    , "value" : [ #mapToJSONs(keys_list(M), M) ] }
+    rule #scValToJSON( _          ) => null                                     [owise]
+
+    syntax JSONs ::= #scValsToJSONs( List ) [function, symbol(scValsToJSONs)]
+ // -------------------------------------------------------------------------
+    rule #scValsToJSONs( .List ) => .JSONs
+    rule #scValsToJSONs( ListItem(V) REST ) => #scValToJSON({V}:>ScVal) , #scValsToJSONs(REST)
+
+    // Each map entry becomes a two-element [key, value] array, in key order.
+    syntax JSONs ::= #mapToJSONs( List, Map ) [function, symbol(mapToJSONs)]
+ // ------------------------------------------------------------------------
+    rule #mapToJSONs( .List, _ ) => .JSONs
+    rule #mapToJSONs( ListItem(KEY) REST, M )
+      => [ #scValToJSON({KEY}:>ScVal) , #scValToJSON({M[KEY]}:>ScVal) , .JSONs ] , #mapToJSONs(REST, M)
+```
+
+`#bytesToHex` is the inverse of `HexBytes`: lowercase hex, two digits per byte (zero-padded,
+since Base2String drops leading zeroes). Empty bytes encode as the empty string — the
+general rule would yield `"0"` (Base2String of 0), which `#padZeros` cannot trim.
+
+```k
+    syntax String ::= #bytesToHex( Bytes )      [function, total, symbol(bytesToHex)]
+                    | #padZeros( String, Int )  [function, total, symbol(padZeros)]
+ // --------------------------------------------------------------------------------
+    rule #bytesToHex( B ) => "" requires lengthBytes(B) ==Int 0
+    rule #bytesToHex( B ) => #padZeros( Base2String( Bytes2Int(B, BE, Unsigned), 16 ), 2 *Int lengthBytes(B) )
+      requires lengthBytes(B) >Int 0
+
+    rule #padZeros( S, N ) => #padZeros( "0" +String S, N ) requires lengthString(S) <Int N
+    rule #padZeros( S, _ ) => S                              [owise]
 
 endmodule
 ```