Skip to content

Commit fa5499c

Browse files
Merge pull request #36 from runtimeverification/feat/simulate-transaction
feat: implement simulateTransaction
2 parents 0615d0b + 7a25c98 commit fa5499c

9 files changed

Lines changed: 483 additions & 9 deletions

File tree

docs/architecture.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ sequenceDiagram
178178
## What's not yet implemented
179179

180180
- `resultXdr` / `resultMetaXdr` in `getTransaction` responses (contract return values)
181-
- `simulateTransaction` (dry-run without state mutation)
181+
- `simulateTransaction` of upload/deploy host functions, auth recording, resource metering, `events`/`restorePreamble`/`stateChanges` (only invoke-contract dry runs with the return value are supported)
182182
- `getEvents` and other read-only RPC methods (`getLedgerEntries` is implemented for the entry types the K state tracks: `ACCOUNT`, `CONTRACT_DATA`, `CONTRACT_CODE`)
183183
- `ExtendFootprintTTL` and `RestoreFootprint` operations
184184
- `SCVec` / `SCMap` contract-argument types in the request encoder (`scval_to_json`)

docs/notes.md

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,8 @@ The tests do not yet cover `bytes` / `address` SCVal arguments or `SCVec` / `SCM
3838
- `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.
3939
- `SCVec` / `SCMap` contract arguments are not yet encoded.
4040
- The `xdrFormat` parameter is accepted on `getTransaction`, `sendTransaction`, `getTransactions`, `getLedgers`, and `getLedgerEntries`, but only the default `'base64'` is supported; `'json'` is rejected with `-32602`.
41-
- `simulateTransaction`, `getEvents`, and TTL/footprint operations are not implemented.
41+
- `simulateTransaction` only simulates invoke-contract host functions (not uploads/deploys); `auth` is always empty, `minResourceFee`/`transactionData` are synthetic constants, and `events`/`restorePreamble`/`stateChanges` and the `resourceConfig`/`authMode`/`xdrFormat` parameters are not supported. `ScMap` return values are not yet encoded.
42+
- `getEvents` and TTL/footprint operations are not implemented.
4243
- `getFeeStats` reports constant distributions (there is no fee market); only its `latestLedger` is live.
4344
- `getTransactions` / `getLedgers` serve only ledgers with an index file under `ledgers/`; io-dirs created before the ledger index existed resume fine, but their earlier ledgers do not appear in the history.
4445
- `getLedgerEntries` covers the entry types the K state tracks (`ACCOUNT`, `CONTRACT_DATA`, `CONTRACT_CODE`); other key types are reported as not found. `lastModifiedLedgerSeq` is approximated by the current ledger (per-entry modification ledgers are not tracked), and only the balance is real in `ACCOUNT` entries (sequence number, thresholds, etc. are synthesised constants).

docs/server.md

Lines changed: 25 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ server = StellarRpcServer(io_dir=Path('out'))
4343
server.handle_rpc('sendTransaction', {'transaction': xdr})
4444
```
4545

46-
For `sendTransaction` it builds the request envelope with `encoder.build_tx_request` and runs it with `interpreter.run` (skipping the `<program>` wasm injection when the hash already has a receipt, so a duplicate is not re-executed — the semantics answer `DUPLICATE`); for the read-only methods (`getHealth`, `getNetwork`, `getLatestLedger`, `getTransaction`, `getTransactions`, `getLedgers`, `traceTransaction`) it builds a small envelope and runs it. For the history methods (`getTransactions`, `getLedgers`) the server also validates the pagination parameters — limit range, `startLedger` bounds, `cursor`/`startLedger` exclusivity — and resolves the cursor to the first ledger sequence to serve, because the JSON-RPC parameter-error path lives here. In every case the *content* of the response is produced by the semantics (`node.md`), not by Python — the exceptions are the failure fallback (below) and the per-ledger XDR artifacts (`_record_closed_ledger`), which K cannot construct. Each call is logged to stderr.
46+
For `sendTransaction` it builds the request envelope with `encoder.build_tx_request` and runs it with `interpreter.run` (skipping the `<program>` wasm injection when the hash already has a receipt, so a duplicate is not re-executed — the semantics answer `DUPLICATE`); for `simulateTransaction` it builds the envelope with `encoder.build_simulate_request` and runs it without committing; for the read-only methods (`getHealth`, `getNetwork`, `getLatestLedger`, `getTransaction`, `getTransactions`, `getLedgers`, `getLedgerEntries`, `traceTransaction`) it builds a small envelope and runs it. For the history methods (`getTransactions`, `getLedgers`) the server also validates the pagination parameters — limit range, `startLedger` bounds, `cursor`/`startLedger` exclusivity — and resolves the cursor to the first ledger sequence to serve, because the JSON-RPC parameter-error path lives here. In every case the *content* of the response is produced by the semantics (`node.md`), not by Python — the exceptions are the failure fallback (below), the per-ledger XDR artifacts (`_record_closed_ledger`), and the XDR fields of the `simulateTransaction` response, which K cannot construct or serialize. Each call is logged to stderr.
4747

4848
---
4949

@@ -157,6 +157,29 @@ Resubmitting a transaction whose hash already has a receipt returns status `DUPL
157157

158158
A transaction that decodes as XDR but cannot be processed (e.g. it contains an operation the semantics do not support) is rejected at admission time with status `ERROR` and an `errorResultXdr` carrying a `txMALFORMED` `TransactionResult` — mirroring how real stellar-rpc reports core's admission rejections. Such a transaction never reaches the ledger: no receipt is stored (`getTransaction` stays `NOT_FOUND`) and the ledger does not advance. Undecodable XDR remains a plain `-32602 Invalid params` error, as in real stellar-rpc. `TRY_AGAIN_LATER` is never returned: it signals mempool backpressure, and komet-node executes synchronously without a mempool, so the condition it reports cannot arise.
159159

160+
### `simulateTransaction`
161+
162+
`simulateTransaction` takes a base64-encoded XDR transaction envelope (which may be unsigned) containing exactly one `InvokeHostFunction` operation and executes it as a dry run: the invocation runs against the current world state, but nothing is committed — no receipt, no trace, no ledger bump, and the resulting configuration is discarded (`interpreter.run(..., commit=False)`).
163+
164+
**Response** (success):
165+
```json
166+
{
167+
"latestLedger": 4,
168+
"minResourceFee": "100000",
169+
"results": [ { "xdr": "<base64 SCVal XDR>", "auth": [] } ],
170+
"transactionData": "<base64 SorobanTransactionData XDR>"
171+
}
172+
```
173+
174+
`results[0].xdr` is the host function's return value. The K semantics report it as a JSON-encoded ScVal (see the simulateTransaction section of `node.md`), and the server serializes it to SCVal XDR (`scval_from_json` in `scval.py`) — K has no XDR encoder and no base64 hook, so this is the one read path where Python builds part of the response content. `minResourceFee` is a synthetic constant and `transactionData` an empty-footprint, all-zero-resources placeholder, because the semantics do not meter resources. `auth` is always empty (authorization recording is not implemented).
175+
176+
**Response** (failure — the invocation trapped, the target contract does not exist, the transaction is not a single `InvokeHostFunction`, or the host function is an upload/deploy, which cannot be simulated yet):
177+
```json
178+
{ "error": "<reason>", "latestLedger": 4 }
179+
```
180+
181+
Failures are reported in the result body, matching real stellar-rpc; only an undecodable `transaction` parameter is a JSON-RPC error (`-32602`). A failed simulation likewise commits nothing. The optional `events`, `restorePreamble`, and `stateChanges` response fields and the `resourceConfig`/`authMode`/`xdrFormat` parameters are not supported.
182+
160183
### `traceTransaction` (komet-specific extension)
161184

162185
`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.
@@ -249,7 +272,7 @@ This is the one method whose response the server post-processes: the semantics l
249272

250273
## Failure fallback
251274

252-
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.
275+
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.
253276

254277
---
255278

src/komet_node/interpreter.py

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,8 @@ def run(
124124
io_dir: Path,
125125
request: dict[str, Any],
126126
program_steps: list[KInner] | None = None,
127+
*,
128+
commit: bool = True,
127129
) -> str | None:
128130
"""
129131
Run a single RPC request envelope against the saved KORE configuration.
@@ -137,6 +139,10 @@ def run(
137139
persist the new configuration to ``state.kore``. If ``response.json`` was not
138140
produced the request got stuck (a failed transaction) — we keep the previous
139141
``state.kore`` and return ``None`` so the caller can synthesise a failure response.
142+
143+
With ``commit=False`` the resulting configuration is discarded even on success:
144+
the run executes against the current state but never writes ``state.kore`` back.
145+
This is what makes ``simulateTransaction`` a dry run.
140146
"""
141147
state_file = state_file.resolve()
142148
io_dir = io_dir.resolve()
@@ -153,7 +159,8 @@ def run(
153159
result = _llvm_interpret(self.definition.path, pattern, cwd=io_dir)
154160

155161
if response_file.exists():
156-
state_file.write_text(result.text)
162+
if commit:
163+
state_file.write_text(result.text)
157164
return response_file.read_text()
158165
return None
159166

src/komet_node/kdist/node.md

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,8 @@ module NODE
5555
| #getTxResult( String, String, JSON, Int )
5656
| #respondTrace( JSON, String )
5757
| #respond( JSON, JSON )
58+
| #simulateStep( JSON )
59+
| #simulateRespond( JSON )
5860
| #respondError( JSON, Int, String )
5961
| #respondHealth( JSON, String, Int )
6062
| #respondLatestLedger( JSON, Int, Int )
@@ -523,6 +525,119 @@ exists for that hash.
523525
requires notBool #fileExists( #traceFile( HASH ) )
524526
```
525527

528+
## simulateTransaction
529+
530+
Run a single contract invocation against the current world state *without committing
531+
anything*: no receipt, no trace, no ledger bump, and the Python server does not persist the
532+
resulting configuration (`interpreter.run(..., commit=False)`). Tracing stays disabled
533+
because `<ioDir>` is left empty.
534+
535+
The request envelope carries exactly one `callTx` step (the server rejects anything else
536+
before dispatching here). After the call, the invocation's return value sits on the
537+
`<hostStack>` as a fully resolved `ScVal` — the one thing `sendTransaction` discards and
538+
simulation exists to report.
539+
540+
The K side responds with an *internal* result, `{ "latestLedger": N, "returnValue": <scval
541+
json> }` on success or `{ "latestLedger": N, "error": <string> }` when the call trapped.
542+
The server maps it to the spec response shape: the return value must be serialized as
543+
base64 SCVal XDR and `transactionData` as base64 `SorobanTransactionData`, and K can build
544+
neither (no XDR encoder, no base64 hook), so that final serialization step lives in Python
545+
(`server.py`). A simulation that gets stuck (e.g. calling a contract that does not exist)
546+
produces no `response.json`, and the server synthesises the error result.
547+
548+
```k
549+
rule <k> #dispatchMethod( "simulateTransaction", REQ )
550+
=> setLedgerSequence( #getInt( "latest_ledger", String2JSON( {#readFile("metadata.json")}:>String ) ) )
551+
~> #simulateStep( #firstJSON( #getJSON( "steps", REQ, [ .JSONs ] ) ) )
552+
~> #simulateRespond( #getJSON( "id", REQ ) )
553+
...
554+
</k>
555+
556+
syntax JSON ::= #firstJSON( JSON ) [function, symbol(firstJSON)]
557+
// ----------------------------------------------------------------
558+
rule #firstJSON( [ J , _ ] ) => J
559+
```
560+
561+
Like komet's `callTx`, the invocation clears the `<host>` cell first, so afterwards the
562+
stack holds exactly the call's result. Unlike `callTx` (and `uncheckedCallTx`), there is no
563+
`#resetHost` after the call: `#simulateRespond` still needs the result, and the
564+
configuration is thrown away when the run ends, so nothing leaks into later requests. The
565+
step patterns must mirror the `callTx` case of `#decodeStep` (key order is significant).
566+
567+
```k
568+
rule [simulateStep-account]:
569+
<k> #simulateStep({ "op" : "callTx" , "from" : FROM:String , "fromIsContract" : false , "func" : FUNC:String , "to" : TO:String , "args" : [ ARGS:JSONs ] })
570+
=> allocObjects(#decodeArgList(ARGS))
571+
~> callContractFromStack(Account(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""))
572+
...
573+
</k>
574+
(_:HostCell => <host> <hostStack> .HostStack </hostStack> ... </host>)
575+
576+
rule [simulateStep-contract]:
577+
<k> #simulateStep({ "op" : "callTx" , "from" : FROM:String , "fromIsContract" : true , "func" : FUNC:String , "to" : TO:String , "args" : [ ARGS:JSONs ] })
578+
=> allocObjects(#decodeArgList(ARGS))
579+
~> callContractFromStack(Contract(HexBytes(FROM)), Contract(HexBytes(TO)), string2WasmToken("\"" +String FUNC +String "\""))
580+
...
581+
</k>
582+
(_:HostCell => <host> <hostStack> .HostStack </hostStack> ... </host>)
583+
584+
rule [simulateRespond]:
585+
<k> #simulateRespond( ID )
586+
=> #respond( ID, #simulateResult( SCVAL,
587+
#getInt( "latest_ledger", String2JSON( {#readFile("metadata.json")}:>String ) ) ) )
588+
...
589+
</k>
590+
<hostStack> SCVAL:ScVal : _ </hostStack>
591+
592+
// A trapped call self-heals (the world state is rolled back by `endWasm-error`) and
593+
// leaves an `Error` ScVal on the stack; report it as a result-level error.
594+
syntax JSON ::= #simulateResult( ScVal, Int ) [function, symbol(simulateResult)]
595+
// --------------------------------------------------------------------------------
596+
rule #simulateResult( Error(T, C), LL ) => {
597+
"latestLedger" : LL,
598+
"error" : "host function invocation failed (error type "
599+
+String Int2String(ErrorType2Int(T))
600+
+String ", code " +String Int2String(C) +String ")"
601+
}
602+
rule #simulateResult( SCVAL, LL ) => {
603+
"latestLedger" : LL,
604+
"returnValue" : #scValJSON( SCVAL )
605+
} [owise]
606+
```
607+
608+
`#scValJSON` encodes an `ScVal` return value as JSON for the Python side to XDR-serialize
609+
(`scval_from_json` in `scval.py` is its inverse — keep the two in sync). Python reads these
610+
objects with order-independent lookups, but the fields are emitted in the same order as the
611+
`#decodeArg` patterns for consistency. Unsupported return types (`ScMap`, unresolved host
612+
values, ...) have no rule: the run gets stuck and the server reports a simulation error.
613+
614+
```k
615+
syntax JSON ::= #scValJSON( ScVal ) [function, symbol(scValJSON)]
616+
// -----------------------------------------------------------------
617+
rule #scValJSON( SCBool(B) ) => { "type" : "bool" , "value" : B }
618+
rule #scValJSON( Void ) => { "type" : "void" }
619+
rule #scValJSON( U32(I) ) => { "type" : "u32" , "value" : I }
620+
rule #scValJSON( I32(I) ) => { "type" : "i32" , "value" : I }
621+
rule #scValJSON( U64(I) ) => { "type" : "u64" , "value" : I }
622+
rule #scValJSON( I64(I) ) => { "type" : "i64" , "value" : I }
623+
rule #scValJSON( U128(I) ) => { "type" : "u128" , "value" : I }
624+
rule #scValJSON( I128(I) ) => { "type" : "i128" , "value" : I }
625+
rule #scValJSON( Symbol(S) ) => { "type" : "symbol" , "value" : S }
626+
rule #scValJSON( ScString(S) ) => { "type" : "string" , "value" : S }
627+
rule #scValJSON( ScBytes(B) ) => { "type" : "bytes" , "value" : Bytes2Hex(B) }
628+
rule #scValJSON( ScAddress(Account(B)) ) => { "type" : "address" , "addrType" : "account" , "value" : Bytes2Hex(B) }
629+
rule #scValJSON( ScAddress(Contract(B)) ) => { "type" : "address" , "addrType" : "contract" , "value" : Bytes2Hex(B) }
630+
rule #scValJSON( ScVec(L) ) => { "type" : "vec" , "value" : [ #scValJSONs(L) ] }
631+
632+
syntax JSONs ::= #scValJSONs( List ) [function, symbol(scValJSONs)]
633+
// -------------------------------------------------------------------
634+
rule #scValJSONs( .List ) => .JSONs
635+
rule #scValJSONs( ListItem(V:ScVal) L ) => #scValJSON(V) , #scValJSONs(L)
636+
```
637+
638+
`Bytes2Hex` (the inverse of `HexBytes`, two hex digits per byte) is K's hooked builtin from
639+
the BYTES module; the Python decoder (`bytes.fromhex`) accepts either letter case.
640+
526641
## getLedgerEntries
527642

528643
The Python server decodes each base64 `LedgerKey` of the request (K cannot parse XDR)

src/komet_node/scval.py

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@
2424
from stellar_sdk.xdr.sc_address_type import SCAddressType
2525
from stellar_sdk.xdr.sc_val_type import SCValType
2626

27+
_UINT64_MASK = (1 << 64) - 1
28+
2729
if TYPE_CHECKING:
2830
from komet.scval import SCValue
2931
from stellar_sdk.xdr.sc_address import SCAddress as XDRSCAddress

0 commit comments

Comments
 (0)