diff --git a/README.md b/README.md index 1e64d82..2da8355 100644 --- a/README.md +++ b/README.md @@ -123,7 +123,7 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \ -d '{"jsonrpc":"2.0","id":1,"method":"traceTransaction","params":{"hash":"c7099cbe10a9bfa1cdf9c9d368e1e1c932f535a70e4403b7aa409ce19fc36805"}}' ``` -`traceTransaction` returns the stored trace as its result: a JSON array with one record per executed WebAssembly instruction. +`traceTransaction` returns the stored trace as its result: a JSON array of records, one per executed WebAssembly instruction plus the higher-level records described below. Every record carries a `kind` field naming what it is, so a consumer dispatches on that one field without inspecting the rest of the record's shape. ```jsonc { @@ -131,63 +131,75 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \ "id": 1, "result": [ { - "pos": null, "instr": ["callContract"], + "kind": "ledger", "sequence": 4, "timestamp": 0, + "accounts": [{"account": {"type": "address", "addrType": "account", "value": "03a107bf…"}, "balance": 10000000000}], + "contracts": [], "codes": [] + }, + { + "kind": "callContract", "from": {"type": "address", "addrType": "account", "value": "03a107bff3ce10be1d70dd18e74bc09967e4d6309ba50d5f1ddc8664125531b8"}, "to": {"type": "address", "addrType": "contract", "value": "6a20fec1a9081773a5f23ce370f925f236346e510438ddd6d40f6b2711c134e0"}, "function": "foo", "args":[], "depth":1, "storage":[] }, - {"pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null}, - {"pos": 11, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null}, - {"pos": 19, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null}, - {"pos": null, "instr": ["block"], "stack": [], "locals": {}, "mem": null}, - {"pos": 3, "instr": ["const", "i64", 2], "stack": [], "locals": {}, "mem": null}, - {"pos": null, "instr": ["endWasm"], "success":true, "depth":1, "result": {"type": "void"}} + {"kind": "instr", "pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {}}, + {"kind": "instr", "pos": 11, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576]}}, + {"kind": "instr", "pos": 19, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576]}}, + {"kind": "instr", "pos": null, "instr": ["block"], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576], "2": ["i32", 1048576]}}, + {"kind": "instr", "pos": 3, "instr": ["const", "i64", 2], "stack": [], "locals": {}, "mem": null, "globals": {"0": ["i32", 1048576], "1": ["i32", 1048576], "2": ["i32", 1048576]}}, + {"kind": "endWasm", "success": true, "depth": 1, "result": {"type": "void"}} ] } ``` -A trace can contain five kinds of records: - +A trace can contain six kinds of records: + +- `ledger` - `callContract` -- Wasm instruction records +- Wasm instruction records (`kind: "instr"`) - `hostCall` - `contractData` - `endWasm` -The example above only has three of these: `callContract`, instruction records, and `endWasm`. `foo()` doesn't touch storage or call any host functions, so no `contractData` or `hostCall` records show up. - +The example above only has four of these: `ledger`, `callContract`, instruction records, and `endWasm`. `foo()` doesn't touch storage or call any host functions, so no `contractData` or `hostCall` records show up. + Here's what each record type carries: - + +- `ledger`: written once, as the trace's first record, before any step runs. Gives the ledger sequence and timestamp and every account's balance, so a consumer can seed its view of chain state and replay what follows on top of it rather than seeing only the parts a contract happened to touch. `contracts` and `codes` are reserved for contract-instance and uploaded-code metadata and are currently always empty — read an empty list as "not reported" rather than "none exist". This is the one record komet-node emits itself; the rest come from komet. - `callContract`: logged for each contract call in the transaction, including contract-to-contract calls. Records the caller, the callee, the function name, the arguments, the call depth, and the callee's storage before the call runs. -- Instruction records: logged at each WebAssembly instruction's entry. `pos` is the instruction's byte offset in the binary (`null` for synthetic instructions), `instr` is the instruction and its operands, and `stack`/`locals` are the value stack and locals as `[type, value]` pairs. `mem` is a snapshot of linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot). -- `hostCall`: logged when the contract calls a host function. `instr` gives `["hostCall", moduleId, functionId]`, identifying which host function ran. `locals` holds the function's arguments, indexed by position. Host calls don't use the stack, so `stack` is absent. +- Instruction records: logged at each WebAssembly instruction's entry. `pos` is the instruction's byte offset in the binary (`null` for synthetic instructions), `instr` is the instruction and its operands, and `stack`/`locals` are the value stack and locals as `[type, value]` pairs. `mem` is a snapshot of linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot). `globals` is the executing module's WebAssembly globals keyed by module-relative index; unlike `mem` it is repeated in full on every record and is never `null`. +- `hostCall`: logged when the contract calls a host function. `module` and `function` identify which host function ran. `locals` holds the function's arguments, indexed by position. Host calls don't use the stack, so `stack` is absent. Here's a `hostCall` record for a call to `put_contract_data`, module id `l`, function id `_`: ```jsonc { - "pos": null, - "instr": ["hostCall", "l", "_"], + "kind": "hostCall", + "module": "l", + "function": "_", "locals": {"2": ["i64",0], "1": ["i64",530242871224172548], "0": ["i64",45954062]} } ``` - -- `contractData`: logged for storage updates. Gives the contract and the storage type (`instance`, `persistent`, or `temporary`). A `put` carries the key and value as its two args; a `del` carries only the key. + +- `contractData`: logged for storage updates. Gives the contract, the `operation` (`put` or `del`) and the `durability` (`instance`, `persistent`, or `temporary`). A `put` carries the key and value as its two args; a `del` carries only the key. Here's a `contractData` record for a `put`, followed by a `del` on the same key: ```jsonc { - "pos": null, - "instr": ["contractData", "put", "temporary"], + "kind": "contractData", + "operation": "put", + "durability": "temporary", "contract": {"type": "address", "addrType": "contract", "value": "746573742d7363"}, "args": [{"type": "symbol", "value": "foo"}, {"type": "u32", "value": 123456789}] } { - "pos": null, - "instr": ["contractData", "del", "temporary"], + "kind": "contractData", + "operation": "del", + "durability": "temporary", "contract": {"type": "address", "addrType": "contract", "value": "746573742d7363"}, "args": [{"type": "symbol", "value": "foo"}] } ``` - -- `endWasm`: logged once at the end of a call. Records whether the call succeeded, its depth, and its result. + +- `endWasm`: logged once at the end of a call, for a normal return and a trap alike. Records whether the call succeeded, its depth, and its result. + +The array is exactly the stored trace file — komet-node adds nothing to it. Anything derivable from the records is left to the consumer: which contract is executing at a given record, for instance, follows from the `callContract` and `endWasm` boundaries around it. diff --git a/docs/node-semantics.md b/docs/node-semantics.md index 6a154cc..e55c9d5 100644 --- a/docs/node-semantics.md +++ b/docs/node-semantics.md @@ -84,6 +84,7 @@ If `request.json` is absent, `insert-handleRequestFile` does not fire and K halt #runTx(request) => #enableTrace(traces/trace_.jsonl) ← clear the trace file and point at it ~> setLedgerSequence() + ~> #traceLedger ← write the ledger baseline as the trace's first record ~> #decodeSteps() ← KASMER runs each decoded step ~> #finalizeTx(request) ``` @@ -188,18 +189,32 @@ Tracing is always on. Before running the steps, `#enableTrace` clears the transa **Trace format** (one JSON record per line): ```json -{"pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}, "mem": null} +{"kind": "instr", "pos": 597, "instr": ["local.get", 0], "stack": [["i64", 4]], "locals": {"0": ["i64", 4]}, "mem": null} ``` | Field | Description | |---|---| +| `kind` | Names the record; always `"instr"` for an instruction record. Every trace record carries one, so a consumer dispatches on this field alone | | `pos` | Byte offset of the instruction in the binary, or `null` for synthetic instructions | | `instr` | Instruction name and operands as a JSON array | | `stack` | Value stack at instruction entry, as `[type, value]` pairs | | `locals` | Local variable bindings, keyed by index, as `[type, value]` pairs | | `mem` | Linear memory as a list of `{addr, bytes}` runs, emitted only when memory changed since the previous record and `null` otherwise (reuse the most recent snapshot) | +| `globals` | The executing module's WebAssembly globals, keyed by module-relative index, as `[type, value]` pairs. Repeated in full on every record (never `null`, unlike `mem`) | -Instruction records are one of several trace record kinds (`callContract`, `hostCall`, `contractData`, and `endWasm` are the others); see the [Trace a transaction](../README.md#trace-a-transaction) section of the README for all five. +Instruction records are one of several trace record kinds (`ledger`, `callContract`, `hostCall`, `contractData`, and `endWasm` are the others); see the [Trace a transaction](../README.md#trace-a-transaction) section of the README, and komet's [`docs/tracing.md`](https://github.com/runtimeverification/komet/blob/master/docs/tracing.md) for the full format of each. The `ledger` record is the exception: komet never emits one, so it is built and documented here — see below. + +**The ledger baseline record.** `#traceLedger` writes one `ledger` record as the trace's first line, before any step runs: + +```json +{"kind": "ledger", "sequence": 3, "timestamp": 0, + "accounts": [{"account": {"type": "address", "addrType": "account", "value": "6964b7…"}, "balance": 10000000000}], + "contracts": [], "codes": []} +``` + +It describes the ledger as the transaction's steps *found* it, which is what lets a debugger show chain state at any point of a recorded execution rather than only the parts a contract touched: the debugger seeds its view from this record and replays the storage writes and contract calls that follow on top of it. + +Because the baseline precedes the steps, a transaction that creates its own account reports no accounts — its `setAccount` step runs afterwards. A later transaction sees what earlier ones left behind, which is the case that matters (the debugger traces the last transaction of a sequence). Balances are read straight from the `` cells by `#collectAccounts`, which gathers them one per rewrite step because a K cell collection cannot be passed to a function, and are serialized by `generateLedgerTrace`/`AccountBalances2JSONs` in `node.md` — the cells belong to komet, but the record is komet-node's, so the builders sit beside their only caller. `contracts` and `codes` are reserved for contract-instance and uploaded-code metadata and are currently always empty, so a consumer must read an empty list as "not reported" rather than "none exist". --- diff --git a/docs/server.md b/docs/server.md index f325b1d..2328bdf 100644 --- a/docs/server.md +++ b/docs/server.md @@ -185,14 +185,16 @@ Failures are reported in the result body, matching real stellar-rpc; only an und `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. -`traceTransaction` retrieves the instruction trace of a previously submitted transaction. It takes a `hash` parameter (the same one `getTransaction` takes) and returns the trace that `sendTransaction` stored for that transaction. The result is a JSON array with one record per executed WebAssembly instruction (empty when the transaction ran no instructions), or `null` when no transaction with that hash exists. +`traceTransaction` retrieves the execution trace of a previously submitted transaction. It takes a `hash` parameter (the same one `getTransaction` takes) and returns the trace that `sendTransaction` stored for that transaction. The result is a JSON array of records — one per executed WebAssembly instruction, plus the `ledger` baseline and the Soroban VM records described in the [README](../README.md#trace-a-transaction) — or `null` when no transaction with that hash exists. Each record names itself with a `kind` field. ```json [ - {"pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null} + {"kind": "instr", "pos": 3, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}, "mem": null, "globals": {}} ] ``` +The server reads the stored file and streams it back in one linear pass, passing each record through verbatim: the served array is exactly the trace file. It derives nothing, by design — a trace runs to hundreds of megabytes, so anything a consumer can compute for itself should not be duplicated per record here. Which contract is executing at a given record is the standing example: a `callContract` names its callee and an `endWasm` closes it, so the debug adapter folds it out of boundaries it already walks. + ### `getTransaction` `getTransaction` reads the hash's `receipts/receipt_.json` file. The `hash` parameter must be a 64-character hex string; anything else is rejected with `-32602 Invalid params` (this and `traceTransaction` share the validation). diff --git a/pyproject.toml b/pyproject.toml index c93e34d..7a2b03f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,7 +10,7 @@ readme = "README.md" requires-python = "~=3.10" dependencies = [ "stellar-sdk>=13.2.1", - "komet@git+https://github.com/runtimeverification/komet.git@v0.1.86", + "komet@git+https://github.com/runtimeverification/komet.git@v0.1.88", "kframework>=7.1.323,<7.1.324", ] diff --git a/src/komet_node/__init__.py b/src/komet_node/__init__.py index e69de29..ae4f646 100644 --- a/src/komet_node/__init__.py +++ b/src/komet_node/__init__.py @@ -0,0 +1,13 @@ +from __future__ import annotations + +import sys + +# Parsing and traversing the KORE world-state configuration (via pyk's recursive-descent +# KORE parser and the recursive cell rewrites in ``interpreter.py``) recurses with the depth +# and size of the term. Large real contracts produce configurations far deeper than CPython's +# default recursion limit (1000), which otherwise surfaces as a ``RecursionError`` mid-request. +# Raise the ceiling to match the rest of the K tooling (pyk sets 10**7; komet sets its own +# limit at import). This is the sole cross-cutting entry point, so setting it here covers the +# server process, direct interpreter use, and the encoders. server.py backs this with a large +# serve-thread stack so a deep term raises a catchable error rather than a SIGSEGV. +sys.setrecursionlimit(10**7) diff --git a/src/komet_node/interpreter.py b/src/komet_node/interpreter.py index 05c9767..284585d 100644 --- a/src/komet_node/interpreter.py +++ b/src/komet_node/interpreter.py @@ -1,25 +1,26 @@ from __future__ import annotations import json +import os import tempfile +from hashlib import sha256 +from pathlib import Path from subprocess import CalledProcessError from typing import TYPE_CHECKING, Final from komet.kast.syntax import steps_of -from pyk.kast.inner import KSort -from pyk.konvert import kast_to_kore -from pyk.kore.parser import KoreParser +from pyk.kast.inner import KApply, KSort, KToken from pyk.kore.prelude import SORT_K_ITEM, inj, int_dv, str_dv, top_cell_initializer from pyk.kore.syntax import App, SortApp from pyk.utils import check_file_path, run_process_2 from .errors import NodeInterpreterError from .interfaces import Interpreter +from .kore_emit import kast_to_kore_text from .utils import simbolik_definition if TYPE_CHECKING: from collections.abc import Mapping - from pathlib import Path from typing import Any from pyk.kast.inner import KInner @@ -28,40 +29,54 @@ from .utils import SimbolikDefinition -def _llvm_interpret(definition_dir: Path, pattern: Pattern, *, cwd: str | Path | None = None) -> Pattern: - """Run the LLVM interpreter binary on a KORE pattern, optionally in ``cwd``. +def _run_interpreter(definition_dir: Path, config: Path | str, *, cwd: str | Path | None = None) -> str: + """Run the LLVM interpreter binary and return its output configuration as KORE text. - This mirrors pyk's ``llvm_interpret`` but runs the interpreter *subprocess* with its - working directory set to ``cwd`` (rather than ``os.chdir``-ing this process). The K - file-system hooks resolve their relative paths against the subprocess cwd, so the io-dir - files are found without mutating the parent process's global cwd — which would otherwise - race other threads (e.g. the server runs in a background thread in the tests). + This mirrors pyk's ``llvm_interpret`` but differs from it in two ways. + + It runs the interpreter *subprocess* with its working directory set to ``cwd`` (rather + than ``os.chdir``-ing this process). The K file-system hooks resolve their relative paths + against the subprocess cwd, so the io-dir files are found without mutating the parent + process's global cwd — which would otherwise race other threads (e.g. the server runs in + a background thread in the tests). + + And it exchanges KORE as *text*, never as a parsed ``Pattern``. A ``Path`` config is + handed to the interpreter to read itself; only a ``str`` config is fed on stdin. Parsing + the world state into Python objects and immediately re-serializing it dominated every + request — pyk's KORE parser needed ~1.8s for a 3MB state where the interpreter needs + ~0.5s, and it was paid twice per call (once in, once out) no matter how trivial the + request. Nothing here inspects the configuration, so nothing here parses it. The interpreter is run with ``check=True``: both a successful request and a failed (stuck) transaction exit 0 — failure is signalled by the absence of ``response.json``, not by the exit code — so a non-zero exit can only mean a genuine interpreter error, - which we surface rather than silently parsing whatever it emitted. + which we surface rather than silently returning whatever it emitted. """ interpreter_file = definition_dir / 'interpreter' check_file_path(interpreter_file) - args = [str(interpreter_file), '/dev/stdin', '-1', '/dev/stdout'] + config_arg = str(config) if isinstance(config, Path) else '/dev/stdin' + args = [str(interpreter_file), config_arg, '-1', '/dev/stdout'] try: - res = run_process_2(args, input=pattern.text, cwd=cwd, check=True) + res = run_process_2(args, input=None if isinstance(config, Path) else config, cwd=cwd, check=True) except CalledProcessError as err: raise NodeInterpreterError(f'Interpreter failed with status {err.returncode}: {err.stderr}', err) from err if not res.stdout: raise NodeInterpreterError(f'Interpreter produced no output: {res.stderr}', res) - return KoreParser(res.stdout).pattern() + return res.stdout -# KORE building blocks, used to construct the initial configuration and the -# cell directly in KORE — this avoids the multi-second, configuration-size-scaling -# kast<->kore round-trips that whole-config conversions incur. +# KORE building blocks, used to construct the initial configuration directly in KORE — this +# avoids the multi-second, configuration-size-scaling kast<->kore round-trips that +# whole-config conversions incur. _SORT_STEPS: Final = SortApp('SortSteps') _SORT_STRING: Final = SortApp('SortString') -_PROGRAM_CELL: Final = "Lbl'-LT-'program'-GT-'" _DOT_STEPS: Final = App("Lbl'Stop'List'LBraQuot'kasmerSteps'QuotRBra'") +# The serialized form of an idle ```` cell: the cell wrapping the empty +# ``kasmerSteps`` list. ``state.kore`` is only ever saved in the idle state, so this appears +# in it exactly once, which is what makes the textual splice below unambiguous. +EMPTY_PROGRAM_KORE: Final = "Lbl'-LT-'program'-GT-'{}(Lbl'Stop'List'LBraQuot'kasmerSteps'QuotRBra'{}())" + def _steps_kore(steps: tuple[Pattern, ...]) -> Pattern: """Build a KORE ``Steps`` term (a ``kasmerSteps`` cons list) from step patterns.""" @@ -71,13 +86,45 @@ def _steps_kore(steps: tuple[Pattern, ...]) -> Pattern: return result -def _set_cell(pattern: Pattern, cell_symbol: str, value: Pattern) -> Pattern: - """Replace the (single) child of the named cell in a KORE configuration pattern.""" - if isinstance(pattern, App): - if pattern.symbol == cell_symbol: - return App(pattern.symbol, pattern.sorts, (value,)) - return App(pattern.symbol, pattern.sorts, tuple(_set_cell(arg, cell_symbol, value) for arg in pattern.args)) - return pattern +def splice_program(config_text: str, steps_kore: str) -> str: + """Put ``steps_kore`` into the ```` cell of a serialized configuration. + + A textual substitution rather than a parse-edit-serialize round trip: the cost of the + latter scales with the whole accumulated world state, while this scales with a single + scan. It is unambiguous because a saved configuration is always idle, and an idle + ```` cell is exactly :data:`EMPTY_PROGRAM_KORE`. + + Anything else is an error rather than a no-op — returning the configuration unspliced + would silently drop the uploaded module and leave the transaction to fail obscurely. + """ + occurrences = config_text.count(EMPTY_PROGRAM_KORE) + if occurrences != 1: + raise NodeInterpreterError( + f'Expected exactly one idle cell in the configuration, found {occurrences}. ' + 'The configuration is not in the idle state, or the serializer changed.' + ) + return config_text.replace(EMPTY_PROGRAM_KORE, f"Lbl'-LT-'program'-GT-'{{}}({steps_kore})") + + +def upload_steps_cache_key(steps: list[KInner]) -> str | None: + """A content-address for an all-``uploadWasm`` step list, or ``None`` if it is not one. + + ``TransactionEncoder._upload_steps`` builds each step as + ``upload_wasm(sha256(wasm), wasm2kast(wasm))``, so both arguments derive from the same + bytes and the declared hash alone determines the whole step — and therefore the KORE it + converts to. Any other kind of step has no such key, so it is never cached. + """ + if not steps: + return None + hashes = [] + for step in steps: + if not isinstance(step, KApply) or step.label.name != 'uploadWasm' or len(step.args) != 2: + return None + wasm_hash = step.args[0] + if not isinstance(wasm_hash, KToken): + return None + hashes.append(wasm_hash.token) + return sha256('\x00'.join(hashes).encode()).hexdigest() class NodeInterpreter(Interpreter): @@ -92,6 +139,11 @@ class NodeInterpreter(Interpreter): The world state (accounts, contracts, uploaded wasm) round-trips through the KORE configuration (``state.kore``); the RPC bookkeeping (per-transaction receipts, ledger counter) is persisted as files in the working directory, read and written by the semantics. + + That round trip happens entirely as *text*: ``state.kore`` is handed to the interpreter + as a file path and its output is written straight back. The world state is never parsed + into Python, so the per-request cost no longer scales with how much contract code the + chain has accumulated. """ definition: SimbolikDefinition @@ -99,6 +151,65 @@ class NodeInterpreter(Interpreter): def __init__(self) -> None: self.definition = simbolik_definition() + # ------------------------------------------------------------------ + # Module KORE cache + # + # Converting an uploaded module to KORE is the one remaining Python cost that scales + # with the size of a contract, and it is a pure function of the wasm bytes. Caching it + # on disk makes re-uploading an unchanged contract — what every debug-session relaunch + # does — a file read instead of a fresh sort-inference pass over the whole module. + # ------------------------------------------------------------------ + + @property + def _definition_stamp(self) -> str: + """Identity of the compiled semantics, so a rebuild cannot be served stale KORE.""" + compiled = self.definition.path / 'compiled.json' + stat = compiled.stat() + return sha256(f'{compiled}:{stat.st_mtime_ns}:{stat.st_size}'.encode()).hexdigest()[:16] + + @property + def _cache_dir(self) -> Path: + """Where cached module KORE lives. + + Deliberately outside the io-dir: that is a fresh temporary directory per debug + session, so a cache inside it would never see a second hit. + """ + override = os.environ.get('KOMET_NODE_CACHE_DIR') + if override: + return Path(override) + xdg = os.environ.get('XDG_CACHE_HOME') + return (Path(xdg) if xdg else Path.home() / '.cache') / 'komet-node' / 'steps' + + def steps_kore_text(self, steps: list[KInner]) -> str: + """The KORE text for kasmer ``steps``, converted only if not already cached.""" + key = upload_steps_cache_key(steps) + if key is None: + return self._convert_steps(steps) + entry = self._cache_dir / f'{self._definition_stamp}-{key}.kore' + try: + cached = entry.read_text() + except OSError: + cached = '' + if cached: + return cached + text = self._convert_steps(steps) + self._write_cache_entry(entry, text) + return text + + def _convert_steps(self, steps: list[KInner]) -> str: + return kast_to_kore_text(self.definition.kdefinition, steps_of(steps), KSort('Steps')) + + @staticmethod + def _write_cache_entry(entry: Path, text: str) -> None: + """Populate a cache entry atomically. Failing to cache must never fail the run.""" + try: + entry.parent.mkdir(parents=True, exist_ok=True) + tmp = entry.with_name(f'{entry.name}.{os.getpid()}.tmp') + tmp.write_text(text) + tmp.replace(entry) + except OSError: + pass + def empty_config(self) -> str: """Return the initial idle K configuration as KORE. @@ -119,7 +230,7 @@ def empty_config(self) -> str: } ) with tempfile.TemporaryDirectory() as isolated_dir: - return _llvm_interpret(self.definition.path, config, cwd=isolated_dir).text + return _run_interpreter(self.definition.path, config.text, cwd=isolated_dir) def run( self, @@ -146,6 +257,9 @@ def run( With ``commit=False`` the resulting configuration is discarded even on success: the run executes against the current state but never writes ``state.kore`` back. This is what makes ``simulateTransaction`` a dry run. + + The state file itself is handed to the interpreter, and its output written straight + back, so a request that needs no configuration edit costs no configuration parse. """ state_file = state_file.resolve() io_dir = io_dir.resolve() @@ -155,31 +269,36 @@ def run( if response_file.exists(): response_file.unlink() - pattern = KoreParser(state_file.read_text()).pattern() if program_steps: - pattern = self._inject_program(pattern, program_steps) - - result = _llvm_interpret(self.definition.path, pattern, cwd=io_dir) + result = self._run_with_program(state_file, io_dir, program_steps) + else: + result = _run_interpreter(self.definition.path, state_file, cwd=io_dir) if response_file.exists(): if commit: - state_file.write_text(result.text) + state_file.write_text(result) return response_file.read_text() return None - def _inject_program(self, pattern: Pattern, steps: list[KInner]) -> Pattern: - """Embed kasmer steps into the ```` cell of a KORE configuration. + def _run_with_program(self, state_file: Path, io_dir: Path, steps: list[KInner]) -> str: + """Run with kasmer ``steps`` embedded in the ```` cell. Used for transactions that upload wasm: the resulting ``ModuleDecl`` cannot be - JSON-encoded, so the steps are injected directly into the configuration. - - We convert only the (small) steps term to KORE and splice it into the ```` - cell of the already-parsed configuration. We deliberately avoid a whole-config - ``kore_to_kast``/``kast_to_kore`` round-trip, whose cost scales with the (ever - growing) configuration size. The remaining ``kast_to_kore`` here is bounded by the - size of the uploaded wasm module — the one thing that can only originate as KAST - (``wasm2kast``), since the semantics have no wasm binary decoder — and is - independent of the accumulated world state. + JSON-encoded, so it cannot ride in ``request.json`` like every other request's + operations and has to go into the configuration instead. + + Only the steps are converted to KORE (cached by wasm hash, since that conversion is + the expensive part); splicing them into the configuration is textual, so the cost + stays bounded by the uploaded module rather than by the accumulated world state. The + spliced configuration goes to a temporary file — not into the io-dir, which may sit + on a slow shared mount. """ - steps_kore = kast_to_kore(self.definition.kdefinition, steps_of(steps), KSort('Steps')) - return _set_cell(pattern, _PROGRAM_CELL, steps_kore) + spliced = splice_program(state_file.read_text(), self.steps_kore_text(steps)) + handle, name = tempfile.mkstemp(suffix='.kore') + config_file = Path(name) + try: + with os.fdopen(handle, 'w') as f: + f.write(spliced) + return _run_interpreter(self.definition.path, config_file, cwd=io_dir) + finally: + config_file.unlink(missing_ok=True) diff --git a/src/komet_node/kdist/node.md b/src/komet_node/kdist/node.md index f4a5b78..6c794f2 100644 --- a/src/komet_node/kdist/node.md +++ b/src/komet_node/kdist/node.md @@ -23,6 +23,7 @@ state that is saved and reused for the next request. ```k requires "soroban-semantics/kasmer.md" +requires "soroban-semantics/json-utils.md" requires "fs.md" requires "json.md" @@ -34,6 +35,9 @@ module NODE imports KASMER imports FILE-OPERATIONS imports JSON + // For `Address2JSON`, used by the ledger baseline record below. Imported + // explicitly rather than relied on through KASMER's tracing-only import chain. + imports JSON-UTILS imports BYTES imports K-EQUAL imports STRING @@ -436,6 +440,7 @@ already run by the time we get here, leaving `steps` empty). rule #runTx( REQ ) => #enableTrace( #traceFile( #getString( "txHash", REQ ) ) ) ~> setLedgerSequence( #getInt( "latest_ledger", String2JSON( {#readFile("metadata.json")}:>String ) ) ) + ~> #traceLedger ~> #decodeSteps( #stepsJSONs( #getJSON( "steps", REQ, [ .JSONs ] ) ) ) ~> #finalizeTx( REQ ) ... @@ -455,6 +460,110 @@ at it so the executing steps append their records to it. _ => PATH ``` +`#traceLedger` writes the trace's first record: the **ledger baseline**, carrying the ledger +scalars and every account's balance. A debugger seeds its view of chain state from this record +and then replays the per-operation events (storage writes, contract calls) that follow, so it +can show the ledger at any point of a recorded execution rather than only the parts a contract +happened to touch. + +It runs after `setLedgerSequence` so the sequence it reports is this transaction's, not the +previous one's, and before `#decodeSteps` so it describes the ledger as the steps *found* it — +any `setAccount`, upload or deploy among those steps is a change on top of this baseline. + +The state reported here — ``, ``, `` — is all +declared in komet's `configuration.md`; this module only reads it. What belongs to komet-node +is the record itself: opening every trace with a baseline is a decision about how a +transaction's trace file is laid out, and komet emits no such record. So `generateLedgerTrace` +and its `AccountBalances2JSONs` helper live here, next to their only caller, rather than in +komet's `tracing.md` beside the record builders komet does use. + +The balances cannot be read in one match: `` is a K *cell collection*, so no +function can take it as an argument (its generated sort is not usable in a hand-written +`syntax` declaration), and a rule cannot match a variable number of `` cells at +once. So `#collectAccounts` gathers them one per rewrite step into a plain `Map`, which +`generateLedgerTrace` then serializes. The accumulator itself is the record of what has been +visited — an account is collected only if its address is not already a key. + +komet's `moduleGlobals` faces the same restriction and sidesteps it by reading the cells as +[function context](https://github.com/runtimeverification/k/blob/master/docs/user_manual.md#matching-global-context-in-function-rules) +(see its *Reading Globals*); the same would work here and would remove these rewrite steps. + +```k + syntax KItem ::= "#traceLedger" [symbol(traceLedger)] + | #collectAccounts(acc: Map) [symbol(collectAccounts)] + // --------------------------------------------------------- + rule #traceLedger => #collectAccounts(.Map) ... + PATH + requires PATH =/=String "" + + rule [collectAccounts-step]: + #collectAccounts(ACCTS => ACCTS [ ADDR <- BAL ]) ... + + ADDR + BAL + ... + + requires notBool ADDR in_keys(ACCTS) + [preserves-definedness] + + // Every account visited: emit the record. + rule [collectAccounts-done]: + #collectAccounts(ACCTS) + => #appendFileJSONLn( PATH, generateLedgerTrace( SEQ, TS, ACCTS ) ) + ... + + PATH + SEQ + TS + [owise] + + // Tracing disabled (a simulate/dry run leaves `` empty): a no-op, so the + // step never wedges. + rule #traceLedger => .K ... + "" +``` + +`generateLedgerTrace` builds the record: the ledger scalars plus every account's balance. It +follows the same convention as komet's record builders — a `kind` field naming the record, +then fields shaped for that record alone — so a consumer dispatches on the same field as for +every other line in the file. It carries no `pos`, like komet's other non-instruction records: +the baseline does not come from any position in a binary. + +`contracts` and `codes` are reserved for the contract-instance and uploaded-code metadata +(wasm hash, instance/code TTLs); they are emitted empty for now, and a consumer must treat an +empty list as "not reported" rather than "none exist". + +```k + syntax JSON ::= generateLedgerTrace(sequence: Int, timestamp: Int, accounts: Map) [function] + // --------------------------------------------------------------------------------------------- + rule generateLedgerTrace(SEQ, TS, ACCTS) + => { + "kind" : "ledger" , + "sequence" : SEQ , + "timestamp" : TS , + "accounts" : [ AccountBalances2JSONs(ACCTS) ] , + "contracts" : [ .JSONs ] , + "codes" : [ .JSONs ] + } +``` + +`AccountBalances2JSONs` serializes the `Map` of account `Address` |-> balance that +`#collectAccounts` built, using komet's `Address2JSON` so addresses match how every other +record spells them. The `owise` rule skips an entry that is not `Address |-> Int`, which +`#collectAccounts` cannot produce; it keeps a malformed accumulator from wedging the tracer. + +```k + syntax JSONs ::= AccountBalances2JSONs(Map) [function] + // ---------------------------------------------------------- + rule AccountBalances2JSONs(.Map) => .JSONs + + rule AccountBalances2JSONs((ADDR:Address |-> BAL:Int) REST:Map) + => { "account" : Address2JSON(ADDR) , "balance" : BAL } , AccountBalances2JSONs(REST) + + rule AccountBalances2JSONs((_K |-> _V) REST:Map) => AccountBalances2JSONs(REST) + [owise] +``` + After the steps run, record the receipt, write the new ledger counter, and respond. The trace was already written to its own file during execution, so we only reset ``. Reaching this point means the steps completed without getting stuck, so the status is `SUCCESS`. @@ -1164,6 +1273,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))) + + // Composite arguments. A vec reuses #decodeArgList (which already yields a List of + // ScVal); a map decodes its entries into a Map from ScVal keys to ScVal values. + // Enums, structs, and tuples all bottom out in vecs and maps, so these two rules + // cover every composite call argument. Encoded by scval_to_json as + // { "type": "vec", "value": [ , ... ] } + // { "type": "map", "value": [ { "key": , "val": }, ... ] } + rule #decodeArg({ "type" : "vec" , "value" : [ ELEMS:JSONs ] }) => ScVec(#decodeArgList(ELEMS)) + rule #decodeArg({ "type" : "map" , "value" : [ ENTRIES:JSONs ] }) => ScMap(#decodeMapEntries(ENTRIES)) + + syntax Map ::= #decodeMapEntries(JSONs) [function] + rule #decodeMapEntries(.JSONs) => .Map + rule #decodeMapEntries(E:JSON, ES:JSONs) + => #decodeMapEntry(E) #decodeMapEntries(ES) + + syntax Map ::= #decodeMapEntry(JSON) [function] + rule #decodeMapEntry({ "key" : K:JSON , "val" : V:JSON }) => #decodeArg(K) |-> #decodeArg(V) ``` `uncheckedCallTx` is like komet's `callTx` but it does not entail a return value check. diff --git a/src/komet_node/kore_emit.py b/src/komet_node/kore_emit.py new file mode 100644 index 0000000..3a13fe1 --- /dev/null +++ b/src/komet_node/kore_emit.py @@ -0,0 +1,177 @@ +"""A fast KAST-to-KORE-text conversion for plain terms. + +``pyk.konvert.kast_to_kore`` is general: it normalizes the term (six whole-term passes), +builds a KORE term, and the caller then serializes that. Every stage rebuilds every node, so +converting an uploaded wasm module — half a million subterms for an unoptimized build with +debug info — took ~40s, of which ~20s was passes that provably could not change it, plus a +million uncached ``resolve_sorts`` calls over a few hundred distinct labels. + +:func:`kast_to_kore_text` does the same job for *plain* terms in one pass, writing KORE text +straight into a buffer with every definition lookup memoized by label, sort, or token. It is +~17x faster on a contract module and produces byte-identical output; anything not plain falls +back to ``kast_to_kore``. + +A *plain* term is a tree of ``KApply`` and ``KToken`` with no K sequences, variables, +rewrites, ML connectives or quantifiers, or cells, and with every parametric label's sort +parameters already resolved. Those exclusions are exactly the features the normalization +passes exist to rewrite, which is what makes skipping them sound rather than merely faster. +Terms built by ``pykwasm``'s ``wasm2kast`` are plain. + +Nothing here is Soroban- or wasm-specific: this is generic ``pyk.konvert`` material and +belongs upstream in pyk, where it would speed up every K tool. It lives here until it does. +""" + +from __future__ import annotations + +from typing import TYPE_CHECKING, Final + +from pyk.kast.inner import KApply, KToken +from pyk.konvert import kast_to_kore +from pyk.konvert._kast_to_kore import ML_PATTERN_LABELS, _ktoken_to_kore, _label_to_kore + +if TYPE_CHECKING: + from pyk.kast.inner import KInner, KSort + from pyk.kast.outer import KDefinition + +# Cell labels (``, ``, ...) are excluded because `add_cell_map_items` rewrites +# collection items inside them. +_CELL_PREFIX: Final = '<' + + +def has_only_plain_nodes(term: KInner) -> bool: + """True when every node of ``term`` is a non-cell, non-ML ``KApply`` or a ``KToken``. + + The definition-free half of the plainness check: it rules out the node kinds and labels + the emitter cannot render (sequences, variables, rewrites, ML patterns) and the ones + whose presence would make a skipped normalization pass meaningful (cells). + """ + stack = [term] + while stack: + node = stack.pop() + if isinstance(node, KToken): + continue + if not isinstance(node, KApply): + return False + name = node.label.name + if name.startswith(_CELL_PREFIX) or name in ML_PATTERN_LABELS: + return False + stack.extend(node.args) + return True + + +def _sort_params_resolved(definition: KDefinition, term: KInner) -> bool: + """True when every label in ``term`` already carries its production's sort parameters. + + This is what makes ``add_sort_params`` a no-op for the term. A label whose parameters are + missing (or that the definition does not know at all) sends the term down the generic + path rather than into a ``resolve_sorts`` failure. + """ + arity: dict[str, int] = {} + stack = [term] + while stack: + node = stack.pop() + if not isinstance(node, KApply): + continue + name = node.label.name + expected = arity.get(name) + if expected is None: + production = definition.symbols.get(name) + if production is None: + return False + expected = arity[name] = len(production.params) + if len(node.label.params) != expected: + return False + stack.extend(node.args) + return True + + +def is_plain_kast(definition: KDefinition, term: KInner) -> bool: + """True when ``term`` can be converted by :func:`emit_kore_text`.""" + return has_only_plain_nodes(term) and _sort_params_resolved(definition, term) + + +def kast_to_kore_text(definition: KDefinition, term: KInner, sort: KSort) -> str: + """``kast_to_kore(definition, term, sort).text``, taking the fast path when it applies.""" + if is_plain_kast(definition, term): + return emit_kore_text(definition, term, sort) + return kast_to_kore(definition, term, sort).text + + +def emit_kore_text(definition: KDefinition, term: KInner, sort: KSort) -> str: + """Serialize a plain ``term`` to KORE text in a single pass. + + Caller must have established :func:`is_plain_kast`. The walk keeps its own stack (a + module nests far deeper than Python's recursion limit allows) of pending items: either a + subterm paired with the sort it must be injected to, or a literal chunk to append. The + stack is untyped for the same reason pyk's own conversion loops are — the two entry + shapes are discriminated by ``isinstance`` at the top of the loop. + + Every lookup is memoized: by ``KLabel`` for sorts and the opening text, by + (sort, literal) for tokens, and by sort pair for injections. Half a million subterms use + only a few hundred distinct labels, so the definition is consulted a few hundred times + rather than a million. + """ + chunks: list[str] = [] + resolved: dict[object, tuple[KSort, tuple[KSort, ...]]] = {} + openers: dict[object, str] = {} + tokens: dict[tuple[str, str], str] = {} + injections: dict[tuple[str, str], str] = {} + subsorts: dict[str, frozenset] = {} + + stack: list = [(term, sort)] + while stack: + node, target = stack.pop() + if isinstance(node, str): + chunks.append(node) + continue + + if isinstance(node, KToken): + actual = node.sort + else: + label = node.label + sorts = resolved.get(label) + if sorts is None: + sorts = resolved[label] = definition.resolve_sorts(label) + actual, argument_sorts = sorts + + inject = actual != target + if inject: + key = (actual.name, target.name) + wrapper = injections.get(key) + if wrapper is None: + allowed = subsorts.get(target.name) + if allowed is None: + allowed = subsorts[target.name] = definition.subsorts(target) + if actual not in allowed: + raise ValueError(f'Sort {actual.name} is not a subsort of {target.name}: {node}') + wrapper = injections[key] = f'inj{{Sort{actual.name}{{}}, Sort{target.name}{{}}}}(' + chunks.append(wrapper) + + if isinstance(node, KToken): + token_key = (actual.name, node.token) + text = tokens.get(token_key) + if text is None: + text = tokens[token_key] = _ktoken_to_kore(node).text + chunks.append(text) + if inject: + chunks.append(')') + continue + + opener = openers.get(label) + if opener is None: + params = ', '.join(f'Sort{p.name}{{}}' for p in label.params) + opener = openers[label] = f'{_label_to_kore(label.name)}{{{params}}}(' + chunks.append(opener) + + # Pushed in reverse so arguments come off the stack left to right, followed by the + # closing paren of this application and of its injection wrapper, if any. + if inject: + stack.append((')', None)) + stack.append((')', None)) + arguments = node.args + for index in range(len(arguments) - 1, -1, -1): + stack.append((arguments[index], argument_sorts[index])) + if index: + stack.append((', ', None)) + + return ''.join(chunks) diff --git a/src/komet_node/scval.py b/src/komet_node/scval.py index 36d21ed..29b9683 100644 --- a/src/komet_node/scval.py +++ b/src/komet_node/scval.py @@ -58,6 +58,20 @@ def scval_to_json(scval: SCVal) -> dict: return {'type': 'address', 'addrType': 'account', 'value': raw.hex()} assert addr.contract_id is not None return {'type': 'address', 'addrType': 'contract', 'value': addr.contract_id.contract_id.hash.hex()} + case SCValType.SCV_VEC: + # A vec recurses element-wise. User enums and tuples reduce to vecs at + # the XDR level, so this also covers those composite arguments. + assert scval.vec is not None + return {'type': 'vec', 'value': [scval_to_json(v) for v in scval.vec.sc_vec]} + case SCValType.SCV_MAP: + # A map recurses over its entries. Structs reduce to symbol-keyed maps at + # the XDR level. Key order follows the XDR entry order, which the SDK keeps + # sorted; the K side rebuilds a Map so ordering there is immaterial. + assert scval.map is not None + return { + 'type': 'map', + 'value': [{'key': scval_to_json(e.key), 'val': scval_to_json(e.val)} for e in scval.map.sc_map], + } case _: raise NotImplementedError(f'Unsupported SCVal type for JSON encoding: {scval.type}') diff --git a/src/komet_node/server.py b/src/komet_node/server.py index d5f27b4..3d24630 100644 --- a/src/komet_node/server.py +++ b/src/komet_node/server.py @@ -5,6 +5,7 @@ import logging import re import sys +import threading import time import traceback from datetime import datetime, timezone @@ -100,6 +101,13 @@ def _empty_transaction_data() -> str: # the default 'base64' format; see _require_supported_xdr_format. _XDR_FORMAT_METHODS: Final = ('getTransaction', 'sendTransaction') +# The request path drives deep Python recursion (pyk's recursive-descent KORE parser and the +# recursive cell rewrites in interpreter.py) proportional to the world-state term. komet_node +# raises the recursion *limit* (see __init__.py) so large real contracts do not hit CPython's +# default 1000; this backs that limit with a matching C stack, run on a dedicated serve thread, +# so a deep term raises a catchable error rather than overflowing an 8 MB stack into a SIGSEGV. +_SERVE_STACK_SIZE: Final = 512 * 1024 * 1024 + _log = logging.getLogger('komet_node') @@ -177,7 +185,18 @@ def log_message(self, *args: Any) -> None: # switch to ThreadingHTTPServer without reworking that file protocol. self._httpd = HTTPServer((self.host, int(self._port)), Handler) self._log_ready() - self._httpd.serve_forever() + + # Run the (blocking) serve loop on a worker thread with a large stack so the raised + # recursion limit is usable: the request handler recurses on this thread, and a big + # C stack is what keeps a deep world-state term from segfaulting. stack_size is a + # no-op fallback (default stack) on the rare platform that does not support it. + try: + threading.stack_size(_SERVE_STACK_SIZE) + except (ValueError, RuntimeError): + pass + worker = threading.Thread(target=self._httpd.serve_forever, name='komet-node-serve') + worker.start() + worker.join() def _log_ready(self) -> None: """Announce, once the socket is bound, where the server listens and how it started.""" @@ -296,6 +315,8 @@ def _dispatch(self, method: str | None, params: dict[str, Any], request_id: Any, return self._handle_simulate(params, request_id, now) if method == 'getLedgerEntries': return self._get_ledger_entries(params, request_id, now) + if method == 'traceTransaction': + return self._trace_transaction(params, request_id) envelope = self._read_only_envelope(method, params, request_id, now) response = self.interpreter.run(self.state_file, self.io_dir, envelope, None) @@ -378,6 +399,35 @@ def _get_ledger_entries(self, params: dict[str, Any], request_id: Any, now: str) raise RpcError.internal() return format_ledger_entries_response(response, self.store.wasms_dir) + def _trace_transaction(self, params: dict[str, Any], request_id: Any) -> str: + """Serve a transaction's execution trace directly from its JSONL file. + + The trace was streamed to ``traces/trace_.jsonl`` during ``sendTransaction`` — one + already-valid JSON record per line — so the result array is assembled here in a single + linear pass (join the lines with commas, wrap in brackets). This deliberately bypasses + the interpreter: the semantics reassembled the array by recursively copying the whole + remaining tail once per line, which is O(n^2) in time and memory and OOM-killed the + interpreter on multi-hundred-MB traces. Hash validation mirrors the read-only path. + + The records are passed through verbatim, so the served array is exactly the stored file. + Anything a consumer can derive from the trace is left to the consumer: the debug adapter + needs to know which contract is executing at each record, for instance, but a + ``callContract`` names its callee and an ``endWasm`` closes it, so that is a fold over + records it already walks — tagging every record here would only duplicate derivable data + on the one path whose whole purpose is to keep memory proportional to the trace. + """ + tx_hash = params.get('hash') + if not isinstance(tx_hash, str): + raise RpcError.invalid_params("'hash' (string) is required") + if _TX_HASH_RE.fullmatch(tx_hash) is None: + raise RpcError.invalid_params("'hash' must be a 64-character hex string") + trace_file = self.io_dir / 'traces' / f'trace_{tx_hash}.jsonl' + if not trace_file.is_file(): + return '{"jsonrpc":"2.0","id":' + json.dumps(request_id) + ',"result":null}' + text = trace_file.read_text() + body = ','.join(line for line in (raw.strip() for raw in text.split('\n')) if line) + return '{"jsonrpc":"2.0","id":' + json.dumps(request_id) + ',"result":[' + body + ']}' + def _read_only_envelope( self, method: str | None, params: dict[str, Any], request_id: Any, now: str ) -> dict[str, Any]: diff --git a/src/tests/integration/data/wasm/args.wat b/src/tests/integration/data/wasm/args.wat index 03f0937..e14d8d4 100644 --- a/src/tests/integration/data/wasm/args.wat +++ b/src/tests/integration/data/wasm/args.wat @@ -23,6 +23,15 @@ ;; _ (Soroban ABI stub) (func (;4;) (type 0)) + ;; test_vec / test_map: accept 1 composite arg (a HostVal object handle), + ;; return Void. Declared last and referenced by symbolic id so their function + ;; indices (and the exports below) do not depend on declaration order — + ;; wat2wasm numbers functions by position, ignoring the ;;(;N;) comments. + (func $test_vec (type 1) (param i64) (result i64) + i64.const 2) + (func $test_map (type 1) (param i64) (result i64) + i64.const 2) + (memory (;0;) 16) (global (;0;) (mut i32) (i32.const 1048576)) (global (;1;) i32 (i32.const 1048576)) @@ -34,6 +43,8 @@ (export "test_wide_integers" (func 2)) (export "test_symbol" (func 3)) (export "_" (func 4)) + (export "test_vec" (func $test_vec)) + (export "test_map" (func $test_map)) (export "__data_end" (global 1)) (export "__heap_base" (global 2)) ) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 4de0d68..20fc6c5 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -8,14 +8,45 @@ from __future__ import annotations import json +from io import BytesIO +from pathlib import Path from typing import TYPE_CHECKING -from komet_node.interpreter import NodeInterpreter +from komet.kast.syntax import steps_of, upload_wasm +from pyk.kast.inner import KApply, KSequence, KSort, KVariable +from pyk.kast.prelude.utils import token +from pyk.konvert import kast_to_kore +from pyk.kore.parser import KoreParser +from pyk.kore.syntax import App +from pykwasm.wasm2kast import wasm2kast +from stellar_sdk import Account, TransactionBuilder +from stellar_sdk.utils import sha256 -if TYPE_CHECKING: - from pathlib import Path +from komet_node.interpreter import EMPTY_PROGRAM_KORE, NodeInterpreter, splice_program +from komet_node.kore_emit import kast_to_kore_text + +from .conftest import PASSPHRASE, wat_to_wasm +if TYPE_CHECKING: import pytest + from pyk.kast.inner import KInner + from pyk.kore.syntax import Pattern + +EMPTY_CONTRACT_WAT = (Path(__file__).parent / 'data' / 'wasm' / 'empty.wat').resolve(strict=True) +ADDER_CONTRACT_WAT = (Path(__file__).parent / 'data' / 'wasm' / 'adder.wat').resolve(strict=True) + +# The reference implementation of the edit: parse the whole configuration and +# replace the cell's child. This is what `splice_program` has to agree with, and what it +# replaced in production — correct, but its cost scales with the whole world state. +_PROGRAM_CELL = "Lbl'-LT-'program'-GT-'" + + +def _set_cell(pattern: Pattern, cell_symbol: str, value: Pattern) -> Pattern: + if isinstance(pattern, App): + if pattern.symbol == cell_symbol: + return App(pattern.symbol, pattern.sorts, (value,)) + return App(pattern.symbol, pattern.sorts, tuple(_set_cell(arg, cell_symbol, value) for arg in pattern.args)) + return pattern def test_empty_config_ignores_stray_request_file(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: @@ -34,3 +65,229 @@ def test_empty_config_ignores_stray_request_file(tmp_path: Path, monkeypatch: py assert (tmp_path / 'request.json').exists() assert not (tmp_path / 'response.json').exists() assert 'healthy' not in config + + +# --------------------------------------------------------------------------- +# The splice +# +# ``run`` never parses the world state: for a wasm upload it puts the module into the +# cell by substituting text, and for everything else it hands ``state.kore`` to +# the interpreter untouched. These tests check the splice against the real idle +# configuration, and against what a whole-configuration KORE edit would have produced. +# --------------------------------------------------------------------------- + + +def _upload_steps_kore(interpreter: NodeInterpreter, wasm: bytes) -> str: + steps = [upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))] + return kast_to_kore(interpreter.definition.kdefinition, steps_of(steps), KSort('Steps')).text + + +def test_idle_config_has_exactly_one_empty_program_cell() -> None: + """The premise of the textual splice, checked against the real idle configuration. + + ``state.kore`` is always saved in the idle state, whose cell holds ``.Steps``. + If the serializer ever renders that cell differently, the splice must fail loudly rather + than silently drop an uploaded module — so pin the exact marker here. + """ + config = NodeInterpreter().empty_config() + + assert config.count(EMPTY_PROGRAM_KORE) == 1 + + +def test_splice_program_matches_a_whole_configuration_kore_edit(tmp_path: Path) -> None: + """Splicing text must produce the same KORE term as editing the parsed configuration. + + This is the correctness claim the fast path rests on: the cheap substitution and the + expensive parse-edit-serialize round trip are the same edit. + """ + interpreter = NodeInterpreter() + config = interpreter.empty_config() + steps_kore = _upload_steps_kore(interpreter, wat_to_wasm(EMPTY_CONTRACT_WAT)) + + spliced = KoreParser(splice_program(config, steps_kore)).pattern() + reference = _set_cell(KoreParser(config).pattern(), _PROGRAM_CELL, KoreParser(steps_kore).pattern()) + + assert spliced == reference + + +def test_upload_step_hash_is_the_wasm_content_hash() -> None: + """The invariant the module cache is keyed on, checked against the encoder. + + ``upload_steps_cache_key`` keys on the step's declared hash alone, which is only sound + because the encoder derives both the hash and the module from the same bytes. Checked + here against the encoder's own output rather than a hand-built step. + """ + from komet_node.transaction import TransactionEncoder + + wasm = wat_to_wasm(EMPTY_CONTRACT_WAT) + account = Account('GDIIXPI2CDPBXRI3WEF7UPVZEOBZRMI2ZQASKYDLN5ENWYS73OSG6FKO', sequence=0) + builder = TransactionBuilder(account, PASSPHRASE).append_upload_contract_wasm_op(wasm) + transaction = builder.set_timeout(30).build().transaction + + steps, uploaded = TransactionEncoder(PASSPHRASE)._upload_steps(transaction) + + (step,) = steps + assert isinstance(step, KApply) + assert step.label.name == 'uploadWasm' + assert step.args[0] == token(sha256(wasm)) + assert uploaded == {sha256(wasm).hex(): wasm} + + +# --------------------------------------------------------------------------- +# The module-KORE cache +# --------------------------------------------------------------------------- + + +def test_upload_steps_kore_is_cached_across_interpreters(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + """Converting a module to KORE is the one remaining term-scale Python cost. + + It is a pure function of the wasm bytes, so a second upload of the same contract — the + common case when a debug session is relaunched — must read the cache instead of + converting again. + """ + monkeypatch.setenv('KOMET_NODE_CACHE_DIR', str(tmp_path / 'cache')) + wasm = wat_to_wasm(ADDER_CONTRACT_WAT) + steps = [upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))] + + first = NodeInterpreter().steps_kore_text(steps) + + conversions = 0 + real = NodeInterpreter._convert_steps + + def counting(self: NodeInterpreter, steps: list[KInner]) -> str: + nonlocal conversions + conversions += 1 + return real(self, steps) + + monkeypatch.setattr(NodeInterpreter, '_convert_steps', counting) + second = NodeInterpreter().steps_kore_text(steps) + + assert second == first + assert conversions == 0, 'the second conversion should have come from the cache' + + +def test_upload_steps_cache_is_keyed_to_the_definition(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + """A rebuilt semantics must not be served stale KORE from a previous build.""" + monkeypatch.setenv('KOMET_NODE_CACHE_DIR', str(tmp_path / 'cache')) + wasm = wat_to_wasm(ADDER_CONTRACT_WAT) + steps = [upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))] + + interpreter = NodeInterpreter() + interpreter.steps_kore_text(steps) + cached = list((tmp_path / 'cache').iterdir()) + assert len(cached) == 1 + + monkeypatch.setattr(NodeInterpreter, '_definition_stamp', property(lambda self: 'a-different-build')) + NodeInterpreter().steps_kore_text(steps) + + assert len(list((tmp_path / 'cache').iterdir())) == 2 + + +def test_upload_steps_cache_survives_a_corrupt_entry(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None: + """A truncated or empty cache file must be recomputed, not served.""" + monkeypatch.setenv('KOMET_NODE_CACHE_DIR', str(tmp_path / 'cache')) + wasm = wat_to_wasm(ADDER_CONTRACT_WAT) + steps = [upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))] + + expected = NodeInterpreter().steps_kore_text(steps) + (entry,) = (tmp_path / 'cache').iterdir() + entry.write_text('') + + assert NodeInterpreter().steps_kore_text(steps) == expected + + +# --------------------------------------------------------------------------- +# The fast KAST -> KORE emitter +# +# `kast_to_kore` runs six normalization passes and then builds a KORE term, each stage +# rebuilding every node; converting a 389 KB module took 40s of which half was passes that +# provably could not change it. `kast_to_kore_text` walks a plain term once and writes KORE +# text directly. These tests pin the only property that matters: it produces exactly what +# the generic pipeline produces. +# --------------------------------------------------------------------------- + + +def test_emitted_kore_matches_kast_to_kore_for_a_real_module() -> None: + """The correctness claim the fast path rests on, on a real contract module.""" + interpreter = NodeInterpreter() + definition = interpreter.definition.kdefinition + wasm = wat_to_wasm(ADDER_CONTRACT_WAT) + term = steps_of([upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))]) + + emitted = kast_to_kore_text(definition, term, KSort('Steps')) + + assert emitted == kast_to_kore(definition, term, KSort('Steps')).text + + +def test_emitted_kore_matches_kast_to_kore_for_several_modules() -> None: + """Two structurally different contracts, so the check is not fitted to one module.""" + interpreter = NodeInterpreter() + definition = interpreter.definition.kdefinition + + for wat in (EMPTY_CONTRACT_WAT, ADDER_CONTRACT_WAT): + wasm = wat_to_wasm(wat) + term = steps_of([upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))]) + + assert ( + kast_to_kore_text(definition, term, KSort('Steps')) == kast_to_kore(definition, term, KSort('Steps')).text + ), f'diverged on {wat.name}' + + +def test_emitted_kore_matches_kast_to_kore_for_a_multi_module_upload() -> None: + """A transaction can upload more than one module; the cons list must convert too.""" + interpreter = NodeInterpreter() + definition = interpreter.definition.kdefinition + first, second = wat_to_wasm(EMPTY_CONTRACT_WAT), wat_to_wasm(ADDER_CONTRACT_WAT) + term = steps_of( + [ + upload_wasm(sha256(first), wasm2kast(BytesIO(first))), + upload_wasm(sha256(second), wasm2kast(BytesIO(second))), + ] + ) + + assert kast_to_kore_text(definition, term, KSort('Steps')) == kast_to_kore(definition, term, KSort('Steps')).text + + +def test_non_plain_terms_fall_back_to_the_generic_pipeline() -> None: + """A term the emitter does not handle must still convert, via `kast_to_kore`. + + Variables, sequences, rewrites, ML connectives and cells are all excluded from the fast + path because the normalization passes it skips exist to rewrite exactly those. + """ + definition = NodeInterpreter().definition.kdefinition + # A K sequence is sorted K, not KItem — hence the differing target sorts. + non_plain = [ + (KApply('setExitCode', [KVariable('N', KSort('Int'))]), KSort('KItem')), + (KSequence([KApply('setExitCode', [token(0)])]), KSort('K')), + ] + + for term, sort in non_plain: + assert ( + kast_to_kore_text(definition, term, sort) == kast_to_kore(definition, term, sort).text + ), f'diverged on {term}' + + +def test_plain_scalar_terms_convert_identically() -> None: + """Small plain terms take the fast path too; injections and tokens must still match.""" + definition = NodeInterpreter().definition.kdefinition + + for term, sort in [ + (KApply('setExitCode', [token(0)]), KSort('Step')), + (token(7), KSort('KItem')), + (token('hello "quoted" \\ text'), KSort('KItem')), + (token(b'\x00\xff\n'), KSort('KItem')), + ]: + assert ( + kast_to_kore_text(definition, term, sort) == kast_to_kore(definition, term, sort).text + ), f'diverged on {term}' + + +def test_the_interpreter_converts_steps_through_the_fast_path() -> None: + """The production call site must use the emitter, not the generic pipeline.""" + interpreter = NodeInterpreter() + wasm = wat_to_wasm(ADDER_CONTRACT_WAT) + steps = [upload_wasm(sha256(wasm), wasm2kast(BytesIO(wasm)))] + + converted = interpreter._convert_steps(steps) + + assert converted == kast_to_kore(interpreter.definition.kdefinition, steps_of(steps), KSort('Steps')).text diff --git a/src/tests/integration/test_server.py b/src/tests/integration/test_server.py index 783c7ac..0a0cee4 100644 --- a/src/tests/integration/test_server.py +++ b/src/tests/integration/test_server.py @@ -2,6 +2,7 @@ import importlib.metadata import json +import re import shutil import time from pathlib import Path @@ -455,9 +456,64 @@ def test_trace_transaction_retrieves_trace_by_hash(server: StellarRpcServer) -> assert send_result['status'] == 'PENDING' # The trace is keyed by the same hash getTransaction uses. A create-account op runs no - # wasm instructions, so the stored trace is an empty array (resolved, not null/NOT_FOUND). + # wasm instructions, so the trace holds only the leading `ledger` baseline record every + # traced transaction opens with (resolved, not null/NOT_FOUND). trace = _rpc(server.port(), 'traceTransaction', {'hash': send_result['hash']})['result'] - assert trace == [] + assert [record['kind'] for record in trace] == ['ledger'] + + +def test_trace_opens_with_a_ledger_baseline_record(server: StellarRpcServer) -> None: + """Every traced transaction opens with a `ledger` baseline record: the ledger scalars plus + every account's balance, as the transaction's steps FOUND them. + + A debugger seeds its view of chain state from this and replays the per-operation events that + follow on top, so it can show the ledger at any point of a recorded execution rather than + only the parts a contract happened to touch. + + The balances are those that existed when the transaction started, so a transaction that + creates its own account reports none — the `setAccount` step runs after the baseline. The + second transaction below therefore sees the account the first one created, which is what + makes the field useful for the debugger (it traces the last of a sequence). + """ + keypair = Keypair.random() + + def submit(sequence: int) -> str: + envelope = ( + TransactionBuilder(Account(keypair.public_key, sequence=sequence), PASSPHRASE) + .append_create_account_op(destination=keypair.public_key, starting_balance='1000') + .set_timeout(30) + .build() + ) + envelope.sign(keypair) + return _rpc(server.port(), 'sendTransaction', {'transaction': envelope.to_xdr()})['result']['hash'] + + first_hash = submit(0) + first = _rpc(server.port(), 'traceTransaction', {'hash': first_hash})['result'][0] + + assert first['kind'] == 'ledger' + # The ledger scalars are always reported. + assert isinstance(first['sequence'], int) + assert isinstance(first['timestamp'], int) + # Nothing existed before the first transaction ran its own steps. + assert first['accounts'] == [] + # Reserved for contract-instance / uploaded-code metadata; empty means "not reported". + assert first['contracts'] == [] + assert first['codes'] == [] + + # A second transaction starts from the ledger the first one left behind, so its baseline + # carries the account, with the balance and the address shape the debugger expects. + second_hash = submit(1) + second = _rpc(server.port(), 'traceTransaction', {'hash': second_hash})['result'][0] + + assert second['kind'] == 'ledger' + assert second['accounts'], "the second transaction should see the first transaction's account" + entry = second['accounts'][0] + assert entry['account']['type'] == 'address' + assert entry['account']['addrType'] == 'account' + assert re.fullmatch(r'[0-9a-f]*', entry['account']['value']) + assert isinstance(entry['balance'], int) + # The ledger advances between transactions. + assert second['sequence'] > first['sequence'] def test_trace_transaction_unknown_hash_returns_null(server: StellarRpcServer) -> None: @@ -485,16 +541,23 @@ def test_trace_transaction_returns_full_instruction_trace_for_foo(server: Stella shown in the README) so any drift in format, ordering, or the array-vs-string shape of the result is caught. The entry/exit frames carry per-run contract and account ids, so they are checked structurally rather than by value. + + CI-only: deploys a real WAT, so it needs ``wat2wasm`` on PATH and cannot run where it is absent. """ invoke = deploy_and_get_invoker(server, EMPTY_CONTRACT_WAT) tx_hash = invoke('foo') trace = _rpc(server.port(), 'traceTransaction', {'hash': tx_hash})['result'] - # A callContract entry frame opens the trace: the account calls foo() on the contract with - # no arguments at call depth 1. + # A `ledger` baseline record opens every traced transaction (see + # test_trace_opens_with_a_ledger_baseline_record); the callContract entry frame follows it. + assert trace[0]['kind'] == 'ledger' + trace = trace[1:] + + # A callContract entry frame opens the execution: the account calls foo() on the contract + # with no arguments at call depth 1. entry = trace[0] - assert entry['instr'] == ['callContract'] + assert entry['kind'] == 'callContract' assert entry['function'] == 'foo' assert entry['args'] == [] assert entry['depth'] == 1 @@ -502,17 +565,63 @@ def test_trace_transaction_returns_full_instruction_trace_for_foo(server: Stella assert entry['to']['addrType'] == 'contract' # The executed WebAssembly instructions, exactly as shown in the README. + # The first three records EVALUATE the module's global initialisers. A global is allocated + # only once its own initialiser has run, so each of these sees exactly the globals declared + # before it: none, then one, then two. By the time the function frame runs all three are + # allocated and reported by module-relative index (0..2, never store-level addresses). + initialised = {'0': ['i32', 1048576], '1': ['i32', 1048576], '2': ['i32', 1048576]} assert trace[1:-1] == [ - {'pos': 3, 'instr': ['const', 'i32', 1048576], 'stack': [], 'locals': {}, 'mem': None}, - {'pos': 11, 'instr': ['const', 'i32', 1048576], 'stack': [], 'locals': {}, 'mem': None}, - {'pos': 19, 'instr': ['const', 'i32', 1048576], 'stack': [], 'locals': {}, 'mem': None}, - {'pos': None, 'instr': ['block'], 'stack': [], 'locals': {}, 'mem': None}, - {'pos': 3, 'instr': ['const', 'i64', 2], 'stack': [], 'locals': {}, 'mem': None}, + { + 'kind': 'instr', + 'pos': 3, + 'instr': ['const', 'i32', 1048576], + 'stack': [], + 'locals': {}, + 'mem': None, + 'globals': {}, + }, + { + 'kind': 'instr', + 'pos': 11, + 'instr': ['const', 'i32', 1048576], + 'stack': [], + 'locals': {}, + 'mem': None, + 'globals': {'0': ['i32', 1048576]}, + }, + { + 'kind': 'instr', + 'pos': 19, + 'instr': ['const', 'i32', 1048576], + 'stack': [], + 'locals': {}, + 'mem': None, + 'globals': {'0': ['i32', 1048576], '1': ['i32', 1048576]}, + }, + { + 'kind': 'instr', + 'pos': None, + 'instr': ['block'], + 'stack': [], + 'locals': {}, + 'mem': None, + 'globals': initialised, + }, + { + 'kind': 'instr', + 'pos': 3, + 'instr': ['const', 'i64', 2], + 'stack': [], + 'locals': {}, + 'mem': None, + 'globals': initialised, + }, ] - # An endWasm exit frame closes the trace: the call succeeded and returned Void. + # An endWasm exit frame closes the trace: the call succeeded and returned Void. The exit frame + # is tagged with the finishing contract (the current top of stack) before its pop. exit_frame = trace[-1] - assert exit_frame['instr'] == ['endWasm'] + assert exit_frame['kind'] == 'endWasm' assert exit_frame['success'] is True assert exit_frame['result'] == {'type': 'void'} assert exit_frame['depth'] == 1 @@ -520,9 +629,11 @@ def test_trace_transaction_returns_full_instruction_trace_for_foo(server: Stella def test_trace_records_have_expected_structure_and_reflect_arguments(server: StellarRpcServer) -> None: """The trace opens with a ``callContract`` frame that echoes the decoded arguments, and each - WebAssembly instruction record is a ``{pos, instr, stack, locals}`` object. For a call that + WebAssembly instruction record is a ``{kind, pos, instr, stack, locals, ...}`` object. For a call that takes arguments the arguments are bound as locals while intermediate values build up on the stack — exercising a richer trace than the argument-less ``foo()`` case. + + CI-only: deploys a real WAT, so it needs ``wat2wasm`` on PATH and cannot run where it is absent. """ invoke = deploy_and_get_invoker(server, ARGS_CONTRACT_WAT) tx_hash = invoke( @@ -540,9 +651,13 @@ def test_trace_records_have_expected_structure_and_reflect_arguments(server: Ste assert isinstance(trace, list) assert len(trace) > 0 + # Skip the leading `ledger` baseline record every traced transaction opens with. + assert trace[0]['kind'] == 'ledger' + trace = trace[1:] + # The callContract entry frame echoes the call target and its decoded arguments. entry = trace[0] - assert entry['instr'] == ['callContract'] + assert entry['kind'] == 'callContract' assert entry['function'] == 'test_integers' assert entry['args'] == [ {'type': 'u32', 'value': 42}, @@ -552,13 +667,18 @@ def test_trace_records_have_expected_structure_and_reflect_arguments(server: Ste ] # The instruction records (everything between the call-boundary frames) share one shape. - instr_records = [record for record in trace if 'locals' in record] + instr_records = [record for record in trace if record['kind'] == 'instr'] assert instr_records for record in instr_records: - assert set(record) == {'pos', 'instr', 'stack', 'locals', 'mem'} + assert set(record) == {'kind', 'pos', 'instr', 'stack', 'locals', 'mem', 'globals'} assert record['pos'] is None or isinstance(record['pos'], int) # mem is null when linear memory is unchanged since the previous record, else a list of runs. assert record['mem'] is None or isinstance(record['mem'], list) + # globals is the executing module's globals keyed by module-relative index, repeated in + # full on every record (never null, unlike mem). + assert isinstance(record['globals'], dict) + assert all(key.isdigit() for key in record['globals']) + assert all(isinstance(e, list) and len(e) == 2 and isinstance(e[0], str) for e in record['globals'].values()) assert isinstance(record['instr'], list) and record['instr'] assert isinstance(record['instr'][0], str) # opcode mnemonic # stack and locals hold [type, value] pairs. @@ -588,7 +708,10 @@ def test_call_tx_with_args(server: StellarRpcServer) -> None: def assert_args_round_trip(func: str, args: list[xdr.SCVal]) -> None: tx_hash = invoke(func, args) - entry = _rpc(server.port(), 'traceTransaction', {'hash': tx_hash})['result'][0] + trace = _rpc(server.port(), 'traceTransaction', {'hash': tx_hash})['result'] + # The trace opens with the `ledger` baseline record, so find the call frame rather + # than assuming it is first. + entry = next(record for record in trace if record.get('kind') == 'callContract') assert entry['function'] == func assert [scval_from_json(arg) for arg in entry['args']] == args @@ -612,6 +735,82 @@ def assert_args_round_trip(func: str, args: list[xdr.SCVal]) -> None: assert_args_round_trip('test_symbol', [xdr.SCVal(type=SCValType.SCV_SYMBOL, sym=xdr.SCSymbol(sc_symbol=b'hello'))]) +def test_call_tx_with_composite_args(server: StellarRpcServer) -> None: + """The scval_to_json / #decodeArg pipeline decodes composite (vec / map) call args. + + Regression test for the composite-argument blocker: komet-node used to decode only + scalar SCVals in call arguments (``scval_to_json`` raised on SCV_VEC/SCV_MAP, and the + ``#decodeArg`` rules had no vec/map cases), so a Vec/Map argument was rejected at + admission and never ran. Both sides now recurse, so a contract call carrying vec and + map arguments reaches SUCCESS (asserted by ``invoke``) and — like ``test_call_tx_with_args`` + — the arguments echoed in the trace's ``callContract`` frame round-trip back to the exact + SCVals sent, so a decoding bug is caught even when the transaction still succeeds. + + User enums, structs, and tuples all reduce to vec/map at the XDR level, so the nested + ``Vec<(enum, i128)>`` case below (with an Address-carrying variant and a negative i128) + stands in for the real ``Vec<(AssetKey, i128)>`` motivating argument. + """ + invoke = deploy_and_get_invoker(server, ARGS_CONTRACT_WAT) + + def assert_args_round_trip(func: str, args: list[xdr.SCVal]) -> None: + tx_hash = invoke(func, args) + trace = _rpc(server.port(), 'traceTransaction', {'hash': tx_hash})['result'] + # A composite argument is allocated as a host object first, so the callContract + # frame is not necessarily trace[0] (unlike the scalar-only case): find it. + entry = next(record for record in trace if record.get('kind') == 'callContract') + assert entry['function'] == func + assert [scval_from_json(arg) for arg in entry['args']] == args + + def sym(name: str) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_SYMBOL, sym=xdr.SCSymbol(sc_symbol=name.encode())) + + def i128(value: int) -> xdr.SCVal: + # Two's-complement split into (hi: signed int64, lo: unsigned int64) so negative + # and high-bit values round-trip, not just small positive ones. + unsigned = value & ((1 << 128) - 1) + hi = unsigned >> 64 + lo = unsigned & ((1 << 64) - 1) + if hi >= (1 << 63): + hi -= 1 << 64 + return xdr.SCVal(type=SCValType.SCV_I128, i128=xdr.Int128Parts(hi=xdr.Int64(hi), lo=xdr.Uint64(lo))) + + def u32(value: int) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_U32, u32=xdr.Uint32(value)) + + def vec(elems: list[xdr.SCVal]) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_VEC, vec=xdr.SCVec(elems)) + + def mp(entries: list[tuple[xdr.SCVal, xdr.SCVal]]) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_MAP, map=xdr.SCMap([xdr.SCMapEntry(key=k, val=v) for k, v in entries])) + + address = Address(Keypair.random().public_key).to_xdr_sc_val() + + # A flat vec of scalars. + assert_args_round_trip('test_vec', [vec([u32(1), u32(2), u32(3)])]) + + # The nested motivating case: Vec<(enum, i128)> mirroring Vec<(AssetKey, i128)> — a unit + # variant (Native), an Address-carrying variant (Stellar(addr)), and a positive and a + # negative i128, exercising SCV_ADDRESS nested in a composite and the full signed i128 range. + assert_args_round_trip( + 'test_vec', + [ + vec( + [ + vec([vec([sym('Native')]), i128(1000)]), + vec([vec([sym('Stellar'), address]), i128(-5)]), + ] + ) + ], + ) + + # A map from symbol keys to scalar values (a struct at the XDR level). Keys are sent in + # sorted order ('amount' < 'nonce') to match the canonical SCMap ordering the trace echoes. + assert_args_round_trip('test_map', [mp([(sym('amount'), i128(500)), (sym('nonce'), u32(7))])]) + + # A map nested inside a vec — composites compose in both directions. + assert_args_round_trip('test_vec', [vec([mp([(sym('k'), u32(1))])])]) + + def test_call_tx_with_return_value(server: StellarRpcServer) -> None: """A contract invocation that returns a non-Void value succeeds. @@ -1680,3 +1879,66 @@ def test_get_transaction_not_found_omits_transaction_fields(server: StellarRpcSe assert get_result['status'] == 'NOT_FOUND' for field in ('ledger', 'createdAt', 'envelopeXdr', 'resultXdr', 'resultMetaXdr', 'returnValue'): assert field not in get_result, f'NOT_FOUND response must omit {field}' + + +def test_trace_transaction_served_from_file_without_interpreter(server: StellarRpcServer) -> None: + """traceTransaction is a pure read of ``traces/trace_.jsonl`` and must NOT invoke the + interpreter. + + The trace is already valid JSONL on disk (one record per line); reassembling it into a JSON + array is a linear string operation the Python layer can do directly. Routing it through the + semantics instead made the interpreter join the lines with a recursive per-line tail-copy — + O(n^2) in time and memory — which OOM-killed the interpreter on multi-hundred-MB traces. This + test pins the record content AND that no interpreter subprocess is spawned to serve the trace. + + The records are served VERBATIM — the array is exactly the stored file, field for field. The + server derives nothing and adds nothing; a consumer that wants, say, the contract executing at + each record folds it out of the `callContract`/`endWasm` boundaries itself. + """ + tx_hash = 'a' * 64 + contract_id = 'ab' * 32 + records: list[dict[str, Any]] = [ + { + 'kind': 'callContract', + 'function': 'f', + 'to': {'type': 'address', 'addrType': 'contract', 'value': contract_id}, + }, + {'kind': 'instr', 'pos': 1, 'instr': ['const', 'i32', 1]}, + {'kind': 'endWasm', 'success': True}, + ] + (server.io_dir / 'traces' / f'trace_{tx_hash}.jsonl').write_text('\n'.join(json.dumps(r) for r in records) + '\n') + + calls: list[Any] = [] + original_run = server.interpreter.run + + def _spy(*args: Any, **kwargs: Any) -> Any: + calls.append(args) + return original_run(*args, **kwargs) + + server.interpreter.run = _spy # type: ignore[method-assign] + try: + response = json.loads(server.handle_rpc('traceTransaction', {'hash': tx_hash})) + finally: + server.interpreter.run = original_run # type: ignore[method-assign] + + assert response['result'] == records + assert calls == [], 'traceTransaction must not invoke the interpreter' + + +def test_trace_transaction_missing_file_returns_null_without_interpreter(server: StellarRpcServer) -> None: + """A hash with no trace file yields ``result: null`` — again without touching the interpreter.""" + calls: list[Any] = [] + original_run = server.interpreter.run + + def _spy(*args: Any, **kwargs: Any) -> Any: + calls.append(args) + return original_run(*args, **kwargs) + + server.interpreter.run = _spy # type: ignore[method-assign] + try: + response = json.loads(server.handle_rpc('traceTransaction', {'hash': '0' * 64})) + finally: + server.interpreter.run = original_run # type: ignore[method-assign] + + assert response['result'] is None + assert calls == [], 'traceTransaction must not invoke the interpreter' diff --git a/src/tests/unit/test_interpreter.py b/src/tests/unit/test_interpreter.py new file mode 100644 index 0000000..d17e5ac --- /dev/null +++ b/src/tests/unit/test_interpreter.py @@ -0,0 +1,138 @@ +"""Unit tests for the interpreter's pure helpers. + +``NodeInterpreter.run`` hands ``state.kore`` to the LLVM interpreter as a file path and +writes its stdout straight back, so the world state never becomes a Python ``Pattern``. +The two things that still need Python are covered here: splicing the ```` cell +textually (for wasm uploads), and deriving the cache key that lets a module's KORE be +reused instead of re-converted. +""" + +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest +from komet.kast.syntax import set_exit_code, upload_wasm +from pyk.kast.inner import KApply +from pyk.kast.prelude.utils import token + +from komet_node.errors import NodeInterpreterError +from komet_node.interpreter import EMPTY_PROGRAM_KORE, splice_program, upload_steps_cache_key + +if TYPE_CHECKING: + from pyk.kast.inner import KInner + +# A stand-in for a serialized configuration: the empty cell surrounded by +# unrelated cells. The real thing is megabytes of the same shape. +_CONFIG = f"Lbl'-LT-'generatedTop'-GT-'{{}}({EMPTY_PROGRAM_KORE}, Lbl'-LT-'k'-GT-'{{}}(dotk{{}}()))" + + +# --------------------------------------------------------------------------- +# splice_program +# --------------------------------------------------------------------------- + + +def test_splice_program_replaces_the_empty_program_cell() -> None: + spliced = splice_program(_CONFIG, 'STEPS') + + assert "Lbl'-LT-'program'-GT-'{}(STEPS)" in spliced + # The idle .Steps token is gone; nothing else about the configuration moved. + assert EMPTY_PROGRAM_KORE not in spliced + assert "Lbl'-LT-'k'-GT-'{}(dotk{}())" in spliced + + +def test_splice_program_leaves_the_rest_of_the_configuration_byte_identical() -> None: + spliced = splice_program(_CONFIG, 'STEPS') + + # Splicing is a single substitution: undoing it must recover the original exactly. + assert spliced.replace("Lbl'-LT-'program'-GT-'{}(STEPS)", EMPTY_PROGRAM_KORE) == _CONFIG + + +def test_splice_program_rejects_a_configuration_with_no_empty_program_cell() -> None: + # A configuration whose cell is not the idle .Steps cannot be spliced into + # blindly — silently returning it unchanged would drop the uploaded module. + with pytest.raises(NodeInterpreterError): + splice_program("Lbl'-LT-'k'-GT-'{}(dotk{}())", 'STEPS') + + +def test_splice_program_rejects_an_ambiguous_configuration() -> None: + # Two candidate sites means we cannot tell which one is the real cell. + with pytest.raises(NodeInterpreterError): + splice_program(_CONFIG + _CONFIG, 'STEPS') + + +# --------------------------------------------------------------------------- +# upload_steps_cache_key +# --------------------------------------------------------------------------- + + +def _upload(wasm_hash: bytes, module: str = 'module') -> KInner: + return upload_wasm(wasm_hash, KApply(module)) + + +def test_upload_steps_cache_key_is_stable_for_the_same_wasm() -> None: + assert upload_steps_cache_key([_upload(b'\x01\x02')]) == upload_steps_cache_key([_upload(b'\x01\x02')]) + + +def test_upload_steps_cache_key_distinguishes_different_wasm() -> None: + assert upload_steps_cache_key([_upload(b'\x01\x02')]) != upload_steps_cache_key([_upload(b'\x03\x04')]) + + +def test_upload_steps_cache_key_distinguishes_order() -> None: + a, b = _upload(b'\x01'), _upload(b'\x02') + + assert upload_steps_cache_key([a, b]) != upload_steps_cache_key([b, a]) + + +def test_upload_steps_cache_key_distinguishes_count() -> None: + a = _upload(b'\x01') + + assert upload_steps_cache_key([a]) != upload_steps_cache_key([a, a]) + + +def test_upload_steps_cache_key_declines_non_upload_steps() -> None: + # Only uploadWasm steps are content-addressed by their first argument; anything else + # must not be cached, since we have no key that determines its KORE. + assert upload_steps_cache_key([set_exit_code(0)]) is None + + +def test_upload_steps_cache_key_declines_a_mixed_step_list() -> None: + assert upload_steps_cache_key([_upload(b'\x01'), set_exit_code(0)]) is None + + +def test_upload_steps_cache_key_declines_a_malformed_upload() -> None: + # A hash argument that is not a literal token gives us nothing to key on. + assert upload_steps_cache_key([KApply('uploadWasm', [KApply('notAToken'), KApply('module')])]) is None + + +def test_upload_steps_cache_key_declines_an_empty_step_list() -> None: + assert upload_steps_cache_key([]) is None + + +def test_upload_steps_cache_key_ignores_the_module_argument() -> None: + """The key is the declared wasm hash, because the module is a function of it. + + ``TransactionEncoder._upload_steps`` builds every step as + ``upload_wasm(sha256(wasm), wasm2kast(wasm))`` — both arguments derive from the same + bytes, so the hash alone determines the whole step. This test pins the assumption; the + integration test ``test_upload_step_hash_is_the_wasm_content_hash`` checks that the + encoder really does construct steps that way. + """ + assert upload_steps_cache_key([_upload(b'\x01', 'moduleA')]) == upload_steps_cache_key( + [_upload(b'\x01', 'moduleB')] + ) + + +def test_upload_steps_cache_key_is_filename_safe() -> None: + key = upload_steps_cache_key([_upload(b'\x00\xff/\\')]) + + assert key is not None + assert key.isalnum() + + +def test_token_shape_assumption() -> None: + """`upload_wasm` puts the hash in a KToken, which is what the key reads.""" + step = upload_wasm(b'\x01\x02', KApply('module')) + + assert isinstance(step, KApply) + assert step.args[0] == token(b'\x01\x02') diff --git a/src/tests/unit/test_kore_emit.py b/src/tests/unit/test_kore_emit.py new file mode 100644 index 0000000..d3d17e0 --- /dev/null +++ b/src/tests/unit/test_kore_emit.py @@ -0,0 +1,79 @@ +"""Unit tests for the structural half of the fast KAST-to-KORE emitter's guard. + +The emitter only handles *plain* terms — trees of ``KApply`` and ``KToken`` with no +sequences, variables, rewrites, ML connectives, or cells. Those exclusions are what make +the generic pipeline's normalization passes provably inapplicable, so the emitter can skip +straight to text. This module covers the definition-free part of that check; the part that +needs a ``KDefinition`` (sort parameters already resolved) is covered in the integration +tests, along with byte-equality against ``kast_to_kore``. +""" + +from __future__ import annotations + +from pyk.kast.inner import KApply, KRewrite, KSequence, KSort, KToken, KVariable +from pyk.kast.prelude.utils import token + +from komet_node.kore_emit import has_only_plain_nodes + + +def test_plain_tree_of_applies_and_tokens_is_plain() -> None: + term = KApply('uploadWasm', [token(b'\x01'), KApply('moduleDecl', [token(7)])]) + + assert has_only_plain_nodes(term) + + +def test_a_bare_token_is_plain() -> None: + assert has_only_plain_nodes(token(3)) + + +def test_a_childless_apply_is_plain() -> None: + assert has_only_plain_nodes(KApply('emptyModule')) + + +def test_a_variable_is_not_plain() -> None: + # `sort_vars` exists to rewrite variables, so a term containing one is not a term the + # normalization passes can be skipped for. + assert not has_only_plain_nodes(KApply('f', [KVariable('X', KSort('Int'))])) + + +def test_a_ksequence_is_not_plain() -> None: + # Two of the skipped passes exist purely to rewrite K sequences. + assert not has_only_plain_nodes(KApply('f', [KSequence([KApply('a'), KApply('b')])])) + + +def test_a_rewrite_is_not_plain() -> None: + assert not has_only_plain_nodes(KRewrite(KApply('a'), KApply('b'))) + + +def test_an_ml_connective_is_not_plain() -> None: + # ML patterns become \and, \equals, ... in KORE, with their own arity and sort rules. + assert not has_only_plain_nodes(KApply('#And', [KApply('a'), KApply('b')])) + + +def test_an_ml_quantifier_is_not_plain() -> None: + assert not has_only_plain_nodes(KApply('#Exists', [KVariable('X'), KApply('a')])) + + +def test_a_cell_is_not_plain() -> None: + # `add_cell_map_items` rewrites collection items inside cells. + assert not has_only_plain_nodes(KApply('', [KApply('a')])) + + +def test_nesting_is_checked_all_the_way_down() -> None: + deep = KApply('f', [KApply('g', [KApply('h', [KSequence([KApply('a')])])])]) + + assert not has_only_plain_nodes(deep) + + +def test_a_token_of_every_sort_is_plain() -> None: + for value in (1, 'text', b'\x00\xff', True): + assert has_only_plain_nodes(KApply('f', [token(value)])) + + +def test_plainness_does_not_depend_on_label_spelling() -> None: + # Only the specific exclusions matter; an ordinary label with punctuation is fine. + assert has_only_plain_nodes(KApply('_+Int_', [token(1), token(2)])) + + +def test_a_lone_angle_bracket_label_is_still_treated_as_a_cell() -> None: + assert not has_only_plain_nodes(KApply('', [KToken('.K', KSort('K'))])) diff --git a/src/tests/unit/test_scval.py b/src/tests/unit/test_scval.py new file mode 100644 index 0000000..162c88c --- /dev/null +++ b/src/tests/unit/test_scval.py @@ -0,0 +1,134 @@ +"""Unit tests for ``scval_to_json`` — the SCVal -> request-envelope JSON encoder. + +These are pure-Python tests (no K, no kdist build). They pin two things: + +* the JSON *shape* the K ``#decodeArg`` rules pattern-match on for composite + (vec / map) call arguments — key order is significant, so the expected dicts + are compared verbatim; and +* that encoding a deeply nested composite value does not blow Python's default + recursion limit (blocker #2). ``scval_to_json`` recurses with the value's + structure, so a deep value is a deterministic proxy for the large-real-contract + recursion that komet-node previously died on. +""" + +from __future__ import annotations + +import json + +from stellar_sdk import xdr +from stellar_sdk.xdr.sc_val_type import SCValType + +from komet_node.scval import scval_to_json + + +def _sym(name: str) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_SYMBOL, sym=xdr.SCSymbol(sc_symbol=name.encode())) + + +def _i128(value: int) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_I128, i128=xdr.Int128Parts(hi=xdr.Int64(0), lo=xdr.Uint64(value))) + + +def _u32(value: int) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_U32, u32=xdr.Uint32(value)) + + +def _vec(elems: list[xdr.SCVal]) -> xdr.SCVal: + return xdr.SCVal(type=SCValType.SCV_VEC, vec=xdr.SCVec(elems)) + + +def _map(entries: list[tuple[xdr.SCVal, xdr.SCVal]]) -> xdr.SCVal: + return xdr.SCVal( + type=SCValType.SCV_MAP, + map=xdr.SCMap([xdr.SCMapEntry(key=k, val=v) for k, v in entries]), + ) + + +def test_scval_to_json_vec_of_scalars() -> None: + """A vec encodes as ``{'type': 'vec', 'value': [, ...]}``. + + Key *order* is significant: the K ``#decodeArg`` rules pattern-match on JSON + member order, so this pins the exact serialization (a dict ``==`` compare is + order-insensitive and would not catch a reordering), not just the key/values. + """ + encoded = scval_to_json(_vec([_sym('Native'), _i128(1000)])) + assert encoded == { + 'type': 'vec', + 'value': [ + {'type': 'symbol', 'value': 'Native'}, + {'type': 'i128', 'value': 1000}, + ], + } + assert json.dumps(encoded) == ( + '{"type": "vec", "value": [{"type": "symbol", "value": "Native"}, ' '{"type": "i128", "value": 1000}]}' + ) + + +def test_scval_to_json_empty_vec() -> None: + assert scval_to_json(_vec([])) == {'type': 'vec', 'value': []} + + +def test_scval_to_json_map() -> None: + """A map encodes as ``{'type': 'map', 'value': [{'key': .., 'val': ..}, ..]}``.""" + encoded = scval_to_json(_map([(_sym('amount'), _u32(7))])) + assert encoded == { + 'type': 'map', + 'value': [ + {'key': {'type': 'symbol', 'value': 'amount'}, 'val': {'type': 'u32', 'value': 7}}, + ], + } + # Order-sensitive check: 'type' before 'value', and 'key' before 'val'. + assert json.dumps(encoded) == ( + '{"type": "map", "value": [{"key": {"type": "symbol", "value": "amount"}, ' + '"val": {"type": "u32", "value": 7}}]}' + ) + + +def test_scval_to_json_empty_map() -> None: + assert scval_to_json(_map([])) == {'type': 'map', 'value': []} + + +def test_scval_to_json_nested_composite_supply_shape() -> None: + """The real motivating case: ``Vec<(AssetKey, i128)>`` with a unit-enum variant. + + A unit enum variant (``AssetKey::Native``) is itself a single-element vec of a + symbol at the XDR level, and a tuple is a vec — so the whole argument is nested + vecs bottoming out in scalars. Encoding must recurse through every level. + """ + request = _vec([_vec([_vec([_sym('Native')]), _i128(1000)])]) + assert scval_to_json(request) == { + 'type': 'vec', + 'value': [ + { + 'type': 'vec', + 'value': [ + {'type': 'vec', 'value': [{'type': 'symbol', 'value': 'Native'}]}, + {'type': 'i128', 'value': 1000}, + ], + }, + ], + } + + +def test_scval_to_json_deeply_nested_vec_survives_recursion_limit() -> None: + """Encoding a deeply nested value must not raise ``RecursionError`` (blocker #2). + + ``scval_to_json`` recurses with the value's depth. Python's default recursion + limit (1000) is well below what a large real contract's values reach, so + komet-node raises the limit at import time. A 2000-deep vec is a deterministic + proxy: it exceeds the default limit but stays within the process stack. Without + the raised limit this raises ``RecursionError``; with it, it encodes cleanly. + """ + depth = 2000 + value = _sym('leaf') + for _ in range(depth): + value = _vec([value]) + + encoded = scval_to_json(value) + + # Peel the encoded structure back down and confirm it is intact to the leaf. + for _ in range(depth): + assert encoded['type'] == 'vec' + assert len(encoded['value']) == 1 + encoded = encoded['value'][0] + assert encoded == {'type': 'symbol', 'value': 'leaf'} diff --git a/uv.lock b/uv.lock index 8b41a20..0cf951d 100644 --- a/uv.lock +++ b/uv.lock @@ -729,8 +729,8 @@ wheels = [ [[package]] name = "komet" -version = "0.1.84" -source = { git = "https://github.com/runtimeverification/komet.git?rev=v0.1.86#e898e5b252abce6f02e3cb0341525fd09d95737b" } +version = "0.1.88" +source = { git = "https://github.com/runtimeverification/komet.git?rev=v0.1.88#673087c27e2024e45b03542ffd3f050ea3b6e69c" } dependencies = [ { name = "pykwasm" }, { name = "tomli" }, @@ -770,7 +770,7 @@ dev = [ [package.metadata] requires-dist = [ { name = "kframework", specifier = ">=7.1.323,<7.1.324" }, - { name = "komet", git = "https://github.com/runtimeverification/komet.git?rev=v0.1.86" }, + { name = "komet", git = "https://github.com/runtimeverification/komet.git?rev=v0.1.88" }, { name = "stellar-sdk", specifier = ">=13.2.1" }, ]