Merge pull request #27 from runtimeverification/chore/remove-demo-leftover

Remove leftover contract-lifecycle walkthrough and demo module

Author: RaoulSchaffranek

README.md

@@ -141,16 +141,6 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \
 
 Each trace record captures the VM state at instruction 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. See [docs/interpreter.md](docs/interpreter.md) for the full trace format.
 
-#### Walk through a contract lifecycle
-
-The bundled demo deploys and invokes a Soroban contract end-to-end (create account → upload wasm → deploy → invoke):
-
-```bash
-uv run python -m komet_node.demo src/tests/integration/data/wasm/empty.wat
-```
-
-This produces `state.kore` plus `state_<n>_<step>.pretty` files under `./out`, letting you inspect exactly how the ledger state evolves at each step. (Requires `wat2wasm` from [`wabt`](https://github.com/WebAssembly/wabt) on your `PATH`.)
-
 ---
 
 ## For Developers

docs/interpreter.md

@@ -59,10 +59,6 @@ return _set_cell(pattern, "<program> cell symbol", steps_kore)   # KORE-level sp
 
 Because Soroban allows only a single host-function operation per transaction, a wasm-upload transaction is exactly one `uploadWasm` op — this path never carries anything else.
 
-### `pretty_print(kore_str)`
-
-`pretty_print` is a debugging helper that pretty-prints a KORE configuration string using `krun --output pretty --depth 0`. `demo.py` uses it to render each step of a contract lifecycle.
-
 ---
 
 ## Supported operations
@@ -80,4 +76,4 @@ The mapping from Stellar operations to kasmer steps is performed by [`Transactio
 
 ## Error handling
 
-`NodeInterpreterError` is raised for interpreter-level failures (e.g. `pretty_print`). A *transaction* failure is not an exception: the semantics get stuck without writing `response.json`, so `run` returns `None` and the server records a `FAILED` receipt while leaving `state.kore` unchanged (the state effectively rolls back).
+`NodeInterpreterError` is raised for interpreter-level failures (e.g. the interpreter crashing or producing no output). A *transaction* failure is not an exception: the semantics get stuck without writing `response.json`, so `run` returns `None` and the server records a `FAILED` receipt while leaving `state.kore` unchanged (the state effectively rolls back).

docs/notes.md

@@ -4,8 +4,6 @@
 
 `komet-node` is a local Stellar testnet backed by the K semantics of Soroban. The compiled semantics are a one-shot interpreter (one process per request, no networking, no state between runs), so Python wraps them into a long-running server: it holds the HTTP socket, keeps state on disk between runs, and decodes Stellar XDR, which K cannot. The RPC layer itself — method dispatch, receipt bookkeeping, ledger accounting, status, and response formatting — runs inside the K semantics ([`node.md`](node-semantics.md)).
 
-See `src/komet_node/demo.py` for an end-to-end example: empty state → create account → upload wasm → deploy contract → call `foo()`, with each step's K configuration pretty-printed.
-
 ---
 
 ## Module map

src/komet_node/demo.py

@@ -11,10 +11,9 @@
 from pyk.kore.parser import KoreParser
 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.ktool.krun import KRunOutput, _krun
 from pyk.utils import check_file_path, run_process_2
 
-from .utils import simbolik_definition, temp_working_directory
+from .utils import simbolik_definition
 
 if TYPE_CHECKING:
     from pathlib import Path
@@ -175,24 +174,6 @@ def _inject_program(self, pattern: Pattern, steps: list[KInner]) -> Pattern:
         steps_kore = kast_to_kore(self.definition.kdefinition, steps_of(steps), KSort('Steps'))
         return _set_cell(pattern, _PROGRAM_CELL, steps_kore)
 
-    def pretty_print(self, kore_str: str) -> str:
-        """Pretty-print a KORE configuration string using the K definition."""
-        with temp_working_directory() as root:
-            kore_file = root / 'input.kore'
-            kore_file.write_text(kore_str)
-            res = _krun(
-                input_file=kore_file,
-                definition_dir=self.definition.path,
-                parser='cat',
-                term=True,
-                output=KRunOutput.PRETTY,
-                check=False,
-                depth=0,
-            )
-            if res.returncode:
-                raise NodeInterpreterError('Failed to pretty-print kore', res)
-            return res.stdout
-
 
 class NodeInterpreterError(RuntimeError):
     pass

src/komet_node/interpreter.py

@@ -1,28 +1,8 @@
 from __future__ import annotations
 
-import os
-import tempfile
-from contextlib import contextmanager
-from pathlib import Path
-from typing import TYPE_CHECKING
-
 from komet.utils import SorobanDefinition
 from pyk.kdist import kdist
 
-if TYPE_CHECKING:
-    from collections.abc import Generator
-
-
-@contextmanager
-def temp_working_directory() -> Generator[Path, None, None]:
-    original = os.getcwd()
-    with tempfile.TemporaryDirectory() as tmp_dir:
-        try:
-            os.chdir(tmp_dir)
-            yield Path(tmp_dir)
-        finally:
-            os.chdir(original)
-
 
 class SimbolikDefinition(SorobanDefinition): ...