Merge pull request #30 from runtimeverification/feat/tx-return-values

Run transactions with non-Void return values

Author: RaoulSchaffranek

src/komet_node/kdist/node.md

@@ -393,10 +393,10 @@ SCVal arg encoding (key order also significant):
         => deployContract(Account(HexBytes(FROM)), Contract(HexBytes(ADDR)), HexBytes(HASH))
 
     rule #decodeStep({ "op" : "callTx" , "from" : FROM:String , "fromIsContract" : false , "func" : FUNC:String , "to" : TO:String , "args" : [ARGS:JSONs] })
-        => callTx(Account(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""), #decodeArgList(ARGS), Void)
+        => uncheckedCallTx(Account(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""), #decodeArgList(ARGS))
 
     rule #decodeStep({ "op" : "callTx" , "from" : FROM:String , "fromIsContract" : true , "func" : FUNC:String , "to" : TO:String , "args" : [ARGS:JSONs] })
-        => callTx(Contract(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""), #decodeArgList(ARGS), Void)
+        => uncheckedCallTx(Contract(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""), #decodeArgList(ARGS))
 
     syntax List  ::= #decodeArgList(JSONs) [function]
     syntax ScVal ::= #decodeArg(JSON)      [function]
@@ -415,6 +415,23 @@ SCVal arg encoding (key order also significant):
     rule #decodeArg({ "type" : "bytes"   , "value" : V:String }) => ScBytes(HexBytes(V))
     rule #decodeArg({ "type" : "address" , "addrType" : "account"  , "value" : V:String }) => ScAddress(Account(HexBytes(V)))
     rule #decodeArg({ "type" : "address" , "addrType" : "contract" , "value" : V:String }) => ScAddress(Contract(HexBytes(V)))
+```
+
+`uncheckedCallTx` is like komet's `callTx` but it does not entail a return value check.
+
+
+```k
+    syntax Step ::= uncheckedCallTx( from: Address, to: Address, func: WasmString, args: List)     [symbol(uncheckedCallTx)]
+
+    rule [uncheckedCallTx]:
+        <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>)
 
 endmodule
 ```

src/tests/integration/data/wasm/adder.wat

@@ -0,0 +1,33 @@
+(module
+  (type (;0;) (func))
+  (type (;1;) (func (param i64 i64) (result i64)))
+
+  ;; add: accept two u32 args, return their sum as u32 (a non-Void value)
+  ;; u32 HostVals carry the payload in the high 32 bits and tag 4 in the low bits
+  (func (;0;) (type 1) (param i64 i64) (result i64)
+    local.get 0
+    i64.const 32
+    i64.shr_u
+    local.get 1
+    i64.const 32
+    i64.shr_u
+    i64.add
+    i64.const 32
+    i64.shl
+    i64.const 4
+    i64.or)
+
+  ;; _ (Soroban ABI stub)
+  (func (;1;) (type 0))
+
+  (memory (;0;) 16)
+  (global (;0;) (mut i32) (i32.const 1048576))
+  (global (;1;) i32 (i32.const 1048576))
+  (global (;2;) i32 (i32.const 1048576))
+
+  (export "memory" (memory 0))
+  (export "add" (func 0))
+  (export "_" (func 1))
+  (export "__data_end" (global 1))
+  (export "__heap_base" (global 2))
+)

src/tests/integration/test_server.py

@@ -18,6 +18,7 @@
 
 EMPTY_CONTRACT_WAT = (Path(__file__).parent / 'data' / 'wasm' / 'empty.wat').resolve(strict=True)
 ARGS_CONTRACT_WAT = (Path(__file__).parent / 'data' / 'wasm' / 'args.wat').resolve(strict=True)
+ADDER_CONTRACT_WAT = (Path(__file__).parent / 'data' / 'wasm' / 'adder.wat').resolve(strict=True)
 
 
 def wat_to_wasm(wat_path: Path) -> bytes:
@@ -445,3 +446,55 @@ def invoke(func: str, args: list[xdr.SCVal]) -> None:
         ],
     )
     invoke('test_symbol', [xdr.SCVal(type=SCValType.SCV_SYMBOL, sym=xdr.SCSymbol(sc_symbol=b'hello'))])
+
+
+def test_call_tx_with_return_value(server: StellarRpcServer) -> None:
+    """A contract invocation that returns a non-Void value succeeds.
+
+    Regression test: transactions used to be decoded into ``callTx(..., Void)``, which
+    asserts the call returns Void. Invoking ``add(2, 3)`` (returning U32(5)) therefore got
+    stuck in the semantics and was recorded as FAILED. ``uncheckedCallTx`` drops the return
+    value check.
+    """
+    keypair = Keypair.random()
+    account = Account(keypair.public_key, sequence=0)
+
+    def send(tb: TransactionBuilder) -> None:
+        env = tb.set_timeout(30).build()
+        env.sign(keypair)
+        res = _rpc(server.port(), 'sendTransaction', {'transaction': env.to_xdr()})
+        assert res['result']['status'] == 'PENDING'
+        tx_hash = res['result']['hash']
+        get_res = _rpc(server.port(), 'getTransaction', {'hash': tx_hash})['result']
+        assert get_res['status'] == 'SUCCESS', f'Transaction failed: {get_res}'
+
+    def builder() -> TransactionBuilder:
+        return TransactionBuilder(account, Network.TESTNET_NETWORK_PASSPHRASE)
+
+    # Set up: create account, upload adder.wat, deploy contract
+    send(builder().append_create_account_op(keypair.public_key, '1000'))
+
+    wasm_bytecode = wat_to_wasm(ADDER_CONTRACT_WAT)
+    send(builder().append_upload_contract_wasm_op(wasm_bytecode))
+
+    from stellar_sdk.utils import sha256
+
+    wasm_hash = sha256(wasm_bytecode)
+    salt = b'\x00' * 32
+    send(builder().append_create_contract_op(wasm_hash, keypair.public_key, None, salt))
+
+    # add(2, 3) returns U32(5), not Void — the send() helper asserts SUCCESS.
+    contract_address = server.encoder.contract_address_from_deployer_address(keypair.public_key, salt)
+    send(
+        builder().append_invoke_contract_function_op(
+            contract_address,
+            'add',
+            [
+                xdr.SCVal(type=SCValType.SCV_U32, u32=xdr.Uint32(2)),
+                xdr.SCVal(type=SCValType.SCV_U32, u32=xdr.Uint32(3)),
+            ],
+        )
+    )
+
+    # All four transactions, including the non-Void invocation, advanced the ledger.
+    assert _rpc(server.port(), 'getLatestLedger', {})['result']['sequence'] == 4