diff --git a/deps/k_release b/deps/k_release index b98d1d3f..c73b21b8 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.3.5 +6.3.25 diff --git a/deps/kwasm_release b/deps/kwasm_release index 20f49513..7ac4e5e3 100644 --- a/deps/kwasm_release +++ b/deps/kwasm_release @@ -1 +1 @@ -0.1.11 +0.1.13 diff --git a/deps/pyk_release b/deps/pyk_release index 105f5e4d..c25df638 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.662 +v0.1.685 diff --git a/deps/wasm-semantics b/deps/wasm-semantics index c29dcba3..200feff9 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit c29dcba3730a3d35b6027de9a61948380910f84a +Subproject commit 200feff9dfe2d58d1f19f22eafb39e6ec9d6f2f0 diff --git a/elrond-node.md b/elrond-node.md index e08be6f6..ea861a0d 100644 --- a/elrond-node.md +++ b/elrond-node.md @@ -131,7 +131,7 @@ Storage maps byte arrays to byte arrays. ### Bytes Stack ```k - syntax BytesStack ::= List{Bytes, ":"} [klabel(bytesStackList), symbol] + syntax BytesStack ::= List{Bytes, ":"} [symbol(bytesStackList)] // -------------------------------------- syntax BytesOp ::= #pushBytes ( Bytes ) diff --git a/kmultiversx/poetry.lock b/kmultiversx/poetry.lock index 2bc0de09..661ac005 100644 --- a/kmultiversx/poetry.lock +++ b/kmultiversx/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.8.1 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. [[package]] name = "attrs" @@ -494,13 +494,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.98.13" +version = "6.98.17" description = "A library for property-based testing" optional = false python-versions = ">=3.8" files = [ - {file = "hypothesis-6.98.13-py3-none-any.whl", hash = "sha256:42ba2cc2d1fe04a65124fadfc6a305dbf62607aa9f8f94a10efadee9cfa1c4dd"}, - {file = "hypothesis-6.98.13.tar.gz", hash = "sha256:746b5316da2c7af4c3816c34af675909fcb1a6a0e5c7af5cfc36c450be2dca34"}, + {file = "hypothesis-6.98.17-py3-none-any.whl", hash = "sha256:313f64b9f9f95e12c8b5342466bef7f352d2608afeeb434817c039602b45f0c4"}, + {file = "hypothesis-6.98.17.tar.gz", hash = "sha256:bbd227000cc21a9686a00867f031479c3812d8ab076e4af1c813f6b3a50c98f5"}, ] [package.dependencies] @@ -970,7 +970,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.662" +version = "0.1.685" description = "" optional = false python-versions = "^3.10" @@ -991,12 +991,12 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.662" -resolved_reference = "975f9d0e8d5ebe28fbda58b56325ef5aee9a075b" +reference = "v0.1.685" +resolved_reference = "03a8ca03c8f93dcc78aecc335a262c4f1524edb2" [[package]] name = "pykwasm" -version = "0.1.11" +version = "0.1.13" description = "" optional = false python-versions = "^3.10" @@ -1007,13 +1007,13 @@ develop = false cytoolz = "^0.12.1" numpy = "^1.24.2" py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.2.0.tar.gz"} -pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.662"} +pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.685"} [package.source] type = "git" url = "https://github.com/runtimeverification/wasm-semantics.git" -reference = "v0.1.11" -resolved_reference = "c29dcba3730a3d35b6027de9a61948380910f84a" +reference = "v0.1.13" +resolved_reference = "200feff9dfe2d58d1f19f22eafb39e6ec9d6f2f0" subdirectory = "pykwasm" [[package]] @@ -1291,4 +1291,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "caa0733bd2288f44a6c247c602d4d20a99204c2b6e8c5cbd13e456bf28ad9095" +content-hash = "0a0cd97e2f2fa04acf62b5711b6c546cc5689e589d1f21b8773ac97f73a84b11" diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index bd0335e8..e1c27c23 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.10" +version = "0.1.11" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.11", subdirectory = "pykwasm" } +pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.13", subdirectory = "pykwasm" } pycryptodomex = "^3.18.0" hypothesis = "^6.82.6" diff --git a/kmultiversx/src/kmultiversx/kasmer.py b/kmultiversx/src/kmultiversx/kasmer.py index d261d8f6..34c0ff4b 100644 --- a/kmultiversx/src/kmultiversx/kasmer.py +++ b/kmultiversx/src/kmultiversx/kasmer.py @@ -13,7 +13,7 @@ from hypothesis.errors import HypothesisWarning from hypothesis.strategies import integers, tuples from pyk.cli.utils import dir_path -from pyk.cterm import CTerm, build_claim +from pyk.cterm import CTerm, cterm_build_claim from pyk.kast.inner import KApply, KSequence, KSort, KVariable, Subst from pyk.kast.manip import split_config_from from pyk.ktool.krun import KRun @@ -343,7 +343,7 @@ def generate_claim( conf_rhs = Subst(rhs_subst)(sym_conf) rhs = CTerm(conf_rhs) - claim, _ = build_claim(f'{func}', lhs, rhs) + claim, _ = cterm_build_claim(f'{func}', lhs, rhs) return claim, lhs, rhs diff --git a/mandos.md b/mandos.md index 639b3040..5db1d66b 100644 --- a/mandos.md +++ b/mandos.md @@ -43,7 +43,7 @@ Only take the next step once both the Elrond node and Wasm are done executing. .K .K - syntax Steps ::= List{Step, ""} [klabel(mandosSteps), symbol] + syntax Steps ::= List{Step, ""} [symbol(mandosSteps)] // ------------------------------------------------------------- rule [steps-empty]: .Steps => .K diff --git a/package/version b/package/version index 9767cc98..20f49513 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.10 +0.1.11