From 0aec17f96384f41afa276bdd57c8932fc14c9620 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Wed, 8 Jul 2026 22:04:38 +0300 Subject: [PATCH 1/3] Bump komet to v0.1.85 and kframework to 7.1.323 --- flake.lock | 8 ++++---- flake.nix | 2 +- pyproject.toml | 4 ++-- uv.lock | 24 ++++++++++++------------ 4 files changed, 19 insertions(+), 19 deletions(-) diff --git a/flake.lock b/flake.lock index 17ac1b7..7ed0082 100644 --- a/flake.lock +++ b/flake.lock @@ -140,16 +140,16 @@ "uv2nix": "uv2nix" }, "locked": { - "lastModified": 1777293866, - "narHash": "sha256-FjpyrMez/5uHThx48uHAnCOJj1flv8Ij2o44TvRp1no=", + "lastModified": 1778594571, + "narHash": "sha256-Y8Ape8of1FBkDAwIxk3vC0s0Yrkn/7Fa/u4MaKI8+Jo=", "owner": "runtimeverification", "repo": "k", - "rev": "1469129d4f6f203461ed1bfd626625d837e523d6", + "rev": "6ee29000016c6addb83b39ac865860f9542b3ebf", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.319", + "ref": "v7.1.323", "repo": "k", "type": "github" } diff --git a/flake.nix b/flake.nix index a0c7b0d..b21a379 100644 --- a/flake.nix +++ b/flake.nix @@ -9,7 +9,7 @@ # `k` package directly (replacing the imperative `kup install k`); its # nixpkgs is intentionally NOT followed, so the k-framework binary caches # are hit instead of rebuilding K against our nixpkgs. - k-framework.url = "github:runtimeverification/k/v7.1.319"; + k-framework.url = "github:runtimeverification/k/v7.1.323"; # Use the same uv2nix as k-framework so we inherit the pyproject-nix version # that fixes the missing 'riscv64' attribute in pep600.nix (pep599.manyLinuxTargetMachines # lookup now uses `or tagArch` as a safe default for unknown architectures). diff --git a/pyproject.toml b/pyproject.toml index e888143..89629f3 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -10,8 +10,8 @@ readme = "README.md" requires-python = "~=3.10" dependencies = [ "stellar-sdk>=13.2.1", - "komet@git+https://github.com/runtimeverification/komet.git@v0.1.79", - "kframework>=7.1.318,<7.1.321", + "komet@git+https://github.com/runtimeverification/komet.git@v0.1.85", + "kframework>=7.1.323,<7.1.324", ] [[project.authors]] diff --git a/uv.lock b/uv.lock index 419f7e0..d741d4e 100644 --- a/uv.lock +++ b/uv.lock @@ -1,5 +1,5 @@ version = 1 -revision = 3 +revision = 2 requires-python = ">=3.10, <4" resolution-markers = [ "python_full_version >= '3.11'", @@ -703,7 +703,7 @@ wheels = [ [[package]] name = "kframework" -version = "7.1.319" +version = "7.1.323" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "coloredlogs" }, @@ -722,15 +722,15 @@ dependencies = [ { name = "tomli-w" }, { name = "xdg-base-dirs" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/b6/9f/4f483cd6ac148795fdefc314f113740056c4fa272a7bf2c5470b4c5ac7ba/kframework-7.1.319.tar.gz", hash = "sha256:a5c3299661ae11d4463c1a8ba49e0f941428b30f0247c0f3005f36d3d7bbf271", size = 244504, upload-time = "2026-04-27T13:56:07.565Z" } +sdist = { url = "https://files.pythonhosted.org/packages/2a/d9/a88f051a023540ea9bbab889183bb87e01869c4ebf6565de32bd5b93b439/kframework-7.1.323.tar.gz", hash = "sha256:29f1ef525a29ba2a1410614ce05c4526e6e44b977232ca107f50ff2750d4e149", size = 245892, upload-time = "2026-05-12T14:44:19.937Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/a2/d9/49627f3a9eafc143087382a8e892d29bb81186ae1ebb8e667d15ac937537/kframework-7.1.319-py3-none-any.whl", hash = "sha256:5441f7a2ac6633afa1491f4817f6dc3631b9f74e2017632ca9586b7c544e1642", size = 296077, upload-time = "2026-04-27T13:56:05.99Z" }, + { url = "https://files.pythonhosted.org/packages/e7/db/d555255f53fdb36ffdcdfb303529f07e939018ddb58a4392eb13f19dbe4d/kframework-7.1.323-py3-none-any.whl", hash = "sha256:d0b23ccf44babb5e3ac735e00242d0a41435864ec66012d761cf6718aee53413", size = 297459, upload-time = "2026-05-12T14:44:18.443Z" }, ] [[package]] name = "komet" -version = "0.1.79" -source = { git = "https://github.com/runtimeverification/komet.git?rev=v0.1.79#cad37497d502a38f11a523f3edca0554b60c2268" } +version = "0.1.84" +source = { git = "https://github.com/runtimeverification/komet.git?rev=v0.1.85#089b3aa59bcb685764a4579f7077ca1c2add8168" } dependencies = [ { name = "pykwasm" }, { name = "tomli" }, @@ -769,8 +769,8 @@ dev = [ [package.metadata] requires-dist = [ - { name = "kframework", specifier = ">=7.1.318,<7.1.321" }, - { name = "komet", git = "https://github.com/runtimeverification/komet.git?rev=v0.1.79" }, + { name = "kframework", specifier = ">=7.1.323,<7.1.324" }, + { name = "komet", git = "https://github.com/runtimeverification/komet.git?rev=v0.1.85" }, { name = "stellar-sdk", specifier = ">=13.2.1" }, ] @@ -1218,8 +1218,8 @@ wheels = [ [[package]] name = "py-wasm" -version = "0.3.0" -source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.0#07677b120f40b86d5b7839e2dde42889967dcfce" } +version = "0.3.1" +source = { git = "https://github.com/runtimeverification/py-wasm.git?rev=0.3.1#19f5a32b227c3f05cb49a604af65dfb7cc1ff083" } dependencies = [ { name = "cytoolz", marker = "implementation_name == 'cpython'" }, { name = "mypy-extensions" }, @@ -1405,8 +1405,8 @@ wheels = [ [[package]] name = "pykwasm" -version = "0.1.150" -source = { git = "https://github.com/runtimeverification/wasm-semantics.git?subdirectory=pykwasm&rev=v0.1.150#5ce9140c07a468c5616f9501b9a8ef1a57896fcc" } +version = "0.1.155" +source = { git = "https://github.com/runtimeverification/wasm-semantics.git?subdirectory=pykwasm&rev=v0.1.155#bd5cbe7bfb3aafbeb4740884fed905394b542320" } dependencies = [ { name = "kframework" }, { name = "py-wasm" }, From 7eb5654f65d881d073cad0defe800128533aff16 Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 9 Jul 2026 11:52:39 +0300 Subject: [PATCH 2/3] README.md: document all trace record kinds --- README.md | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 0bf228f..8f09f07 100644 --- a/README.md +++ b/README.md @@ -130,16 +130,67 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \ "jsonrpc": "2.0", "id": 1, "result": [ + {"pos": null, "instr": ["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": {}}, {"pos": 11, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}}, {"pos": 19, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}}, {"pos": null, "instr": ["block"], "stack": [], "locals": {}}, - {"pos": 3, "instr": ["const", "i64", 2], "stack": [], "locals": {}} + {"pos": 3, "instr": ["const", "i64", 2], "stack": [], "locals": {}}, + {"pos": null, "instr": ["endWasm"], "success":true, "depth":1, "result": {"type": "void"}} ] } ``` -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. +A trace can contain five kinds of records: + +- `callContract` +- Wasm instruction records +- `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. + +Here's what each record type carries: + +- `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. +- `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. + Here's a `hostCall` record for a call to `put_contract_data`, module id `l`, function id `_`: +```jsonc + { + "pos": null, + "instr": ["hostCall", "l", "_"], + "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. + Here's a `contractData` record for a `put`, followed by a `del` on the same key: +```jsonc + { + "pos": null, + "instr": ["contractData", "put", "temporary"], + "contract": {"type": "address", "addrType": "contract", "value": "746573742d7363"}, + "args": [{"type": "symbol", "value": "foo"}, {"type": "u32", "value": 123456789}] + } + { + "pos": null, + "instr": ["contractData", "del", "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. + + + +See [docs/interpreter.md](docs/interpreter.md) for the full trace format. --- From 346dad0e819c512c996ee74e8bbc7caa0b1cf8dd Mon Sep 17 00:00:00 2001 From: Burak Bilge Yalcinkaya Date: Thu, 9 Jul 2026 12:07:01 +0300 Subject: [PATCH 3/3] README.md: reformat trace json --- README.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 8f09f07..54dbfd4 100644 --- a/README.md +++ b/README.md @@ -130,10 +130,11 @@ curl -s http://localhost:8000 -H 'Content-Type: application/json' \ "jsonrpc": "2.0", "id": 1, "result": [ - {"pos": null, "instr": ["callContract"], - "from": {"type": "address", "addrType": "account", "value": "03a107bff3ce10be1d70dd18e74bc09967e4d6309ba50d5f1ddc8664125531b8"}, - "to": {"type": "address", "addrType": "contract", "value": "6a20fec1a9081773a5f23ce370f925f236346e510438ddd6d40f6b2711c134e0"}, - "function": "foo", "args":[], "depth":1, "storage":[] + { + "pos": null, "instr": ["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": {}}, {"pos": 11, "instr": ["const", "i32", 1048576], "stack": [], "locals": {}},