feat: real resultXdr/resultMetaXdr and FAILED transaction reporting

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. |
 | `requests/request_<n>.json` | persistent | the server | an archive of each incoming JSON-RPC request, numbered by a monotonic counter, kept for debugging. |
 | `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. |
@@ -175,7 +175,6 @@ sequenceDiagram
 
 ## What's not yet implemented
 
-- `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
 - `simulateTransaction` (dry-run without state mutation)
 - `getEvents`, `getLedgerEntries`, `getFeeStats` and other read-only RPC methods
 - `ExtendFootprintTTL` and `RestoreFootprint` operations

docs/node-semantics.md

@@ -83,9 +83,13 @@ 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", ledger, createdAt, envelopeXdr, resultXdr: "", resultMetaXdr: "" }`,
+   `{ status: "SUCCESS", ledger, createdAt, envelopeXdr, 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}`.
 
+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.
+
 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.
 
 ### traceTransaction

docs/notes.md

@@ -33,6 +33,8 @@ 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).
 - `SCVec` / `SCMap` contract arguments are not yet encoded.
 - `simulateTransaction`, `getEvents`, `getLedgerEntries`, `getFeeStats`, and TTL/footprint operations are not implemented.

docs/server.md

@@ -136,18 +136,20 @@ All methods are answered by the K semantics and follow the [Stellar RPC specific
 ```json
 {
   "status": "SUCCESS", "ledger": "5", "createdAt": "1716000000",
-  "envelopeXdr": "<base64 XDR>", "resultXdr": "", "resultMetaXdr": "",
+  "envelopeXdr": "<base64 XDR>", "resultXdr": "<base64 XDR>", "resultMetaXdr": "<base64 XDR>",
   "latestLedger": "5", "latestLedgerCloseTime": "1716000000"
 }
 ```
 
-`resultXdr` and `resultMetaXdr` are currently empty stubs. The receipt carries no trace — use `traceTransaction` with the same hash to fetch it.
+`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.
 
 ---
 
 ## Failure fallback
 
-A failed transaction leaves the semantics stuck without writing `response.json`, so `interpreter.run` returns `None`. Only `sendTransaction` executes a transaction, so it is the only method that reaches this path. 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`. This is the only response content the server builds itself.
+A failed transaction leaves the semantics stuck without writing `response.json`, so `interpreter.run` returns `None`. Only `sendTransaction` executes a transaction, so it is the only method that reaches this path. 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.
+
+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. These are the only response contents the server builds itself.
 
 ---
 

src/komet_node/kdist/node.md

@@ -291,6 +291,13 @@ After the steps run, record the receipt, write the new ledger counter, and respo
 was already written to its own file during execution, so we only reset `<ioDir>`. Reaching
 this point means the steps completed without getting stuck, so the status is `SUCCESS`.
 
+The receipt 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(
@@ -304,22 +311,30 @@ this point means the steps completed without getting stuck, so the status is `SU
     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, 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",
             "ledger"        : Int2String( NEWL ),
             "createdAt"     : #getString( "now", REQ ),
             "envelopeXdr"   : #getString( "envelopeXdr", REQ ),
-            "resultXdr"     : "",
-            "resultMetaXdr" : ""
+            "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, NEWL )
           => #respond( #getJSON( "id", REQ ), {
                  "hash"                  : #getString( "txHash", REQ ),
@@ -419,6 +434,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)]
@@ -427,11 +446,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
 ```