From 5348db8b98371050837d0ec4447556d032c58b29 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 12 Nov 2024 02:26:02 -0700 Subject: [PATCH 1/2] Update dependency: deps/kwasm_release (#44) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * deps/kwasm_release: Set Version 0.1.113 * Set Version: 0.1.38 * Sync Poetry files 0.1.113 * deps/k_release: sync release file version 7.1.167 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.39 * Sync Poetry files 0.1.113 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops Co-authored-by: Burak Bilge Yalçınkaya --- deps/k_release | 2 +- deps/kwasm_release | 2 +- flake.lock | 30 ++++----- flake.nix | 2 +- package/version | 2 +- poetry.lock | 157 ++++++++++++++++++++++++++++----------------- pyproject.toml | 4 +- 7 files changed, 120 insertions(+), 79 deletions(-) diff --git a/deps/k_release b/deps/k_release index 01b99c5..e03266d 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.165 +7.1.167 diff --git a/deps/kwasm_release b/deps/kwasm_release index 4b9b35d..c21e67e 100644 --- a/deps/kwasm_release +++ b/deps/kwasm_release @@ -1 +1 @@ -0.1.112 +0.1.113 diff --git a/flake.lock b/flake.lock index 797bc07..7085282 100644 --- a/flake.lock +++ b/flake.lock @@ -125,16 +125,16 @@ ] }, "locked": { - "lastModified": 1729686641, - "narHash": "sha256-LuhI4IRoAMFGVeoPobegWRV7lRu/W2CLzTSB3jMnp0o=", + "lastModified": 1730233640, + "narHash": "sha256-e/iu6Pn/7wdtFrHKckgEbdNxfC9KsahB3l3OlVK1oo0=", "owner": "runtimeverification", "repo": "k", - "rev": "516dbf2c181e21534cf98c3c7c7be916ad5088ce", + "rev": "dd93b05043dc9107b004a71f812e4bbef39a0e7c", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.165", + "ref": "v7.1.167", "repo": "k", "type": "github" } @@ -157,16 +157,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1729195362, - "narHash": "sha256-/Fw5o0F3AJ+zk9nEOEsxLnSrWiKrDOe5RN6ChilbVfY=", + "lastModified": 1730229432, + "narHash": "sha256-2Y4U7TCmSf9NAZCBmvXiHLOXrHxpiRgIpw5ERYDdNSM=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "37b1dd959d47f7b072751b8a3aaef3837de49a79", + "rev": "d5eab4b0f0e610bc60843ebb482f79c043b92702", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.101", + "ref": "v0.1.103", "repo": "llvm-backend", "type": "github" } @@ -319,11 +319,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1729650555, - "narHash": "sha256-j8Sohst1TbQM6LqQKa/HRMfzsUwMhosuNMj2uOn9JOA=", + "lastModified": 1731378398, + "narHash": "sha256-a0QWaiX8+AJ9/XBLGMDy6c90GD7HzpxKVdlFwCke5Pw=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "10c5eb61aaa32caddb9ecf0362a6eb9daeb08eab", + "rev": "0ae9fc2f2fe5361837d59c0bdebbda176427111e", "type": "github" }, "original": { @@ -475,16 +475,16 @@ ] }, "locked": { - "lastModified": 1729693573, - "narHash": "sha256-iG6jJy738Q0J7qlp7nGBlEFZ6fNf9OcQatnp8CsKn2M=", + "lastModified": 1730274141, + "narHash": "sha256-mwz+8I+MVcbS0QM2fMTMtZg2+6efZYZiG/EfiYWBG6Y=", "owner": "runtimeverification", "repo": "wasm-semantics", - "rev": "345e90e2dca5a7c4628fcbb3a0292897d0cdbf62", + "rev": "357bc66b36e549ea4047c2ed3bb3d68373ba7308", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.112", + "ref": "v0.1.113", "repo": "wasm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index b9160a4..e5373a4 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "komet - K tooling for the Soroban platform"; inputs = { - wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.112"; + wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.113"; k-framework.follows = "wasm-semantics/k-framework"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; diff --git a/package/version b/package/version index 5786113..528bd04 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.38 +0.1.39 diff --git a/poetry.lock b/poetry.lock index da01535..a331836 100644 --- a/poetry.lock +++ b/poetry.lock @@ -107,25 +107,27 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""} [[package]] name = "cmd2" -version = "2.4.3" +version = "2.5.4" description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python" optional = false -python-versions = ">=3.6" +python-versions = ">=3.8" files = [ - {file = "cmd2-2.4.3-py3-none-any.whl", hash = "sha256:f1988ff2fff0ed812a2d25218a081b0fa0108d45b48ba2a9272bb98091b654e6"}, - {file = "cmd2-2.4.3.tar.gz", hash = "sha256:71873c11f72bd19e2b1db578214716f0d4f7c8fa250093c601265a9a717dee52"}, + {file = "cmd2-2.5.4-py3-none-any.whl", hash = "sha256:287793e494faaa66d0f9e2549e79c1b923209b5a2261013eb282eb3b35d31691"}, + {file = "cmd2-2.5.4.tar.gz", hash = "sha256:405016f6cee5d4155534a39c8089ebedcfffbb3e24c37150a2b61df32ec90122"}, ] [package.dependencies] -attrs = ">=16.3.0" -pyperclip = ">=1.6" -pyreadline3 = {version = "*", markers = "sys_platform == \"win32\""} -wcwidth = ">=0.1.7" +gnureadline = {version = "*", markers = "platform_system == \"Darwin\""} +pyperclip = "*" +pyreadline3 = {version = "*", markers = "platform_system == \"Windows\""} +wcwidth = "*" [package.extras] -dev = ["codecov", "doc8", "flake8", "invoke", "mypy", "nox", "pytest (>=4.6)", "pytest-cov", "pytest-mock", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme", "twine (>=1.11)"] -test = ["codecov", "coverage", "gnureadline", "pytest (>=4.6)", "pytest-cov", "pytest-mock"] -validate = ["flake8", "mypy", "types-pkg-resources"] +build = ["build", "setuptools", "setuptools-scm"] +dev = ["codecov", "doc8", "invoke", "mypy", "pytest", "pytest-cov", "pytest-mock", "ruff", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme", "twine"] +docs = ["setuptools", "setuptools-scm", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme"] +test = ["codecov", "coverage", "pytest", "pytest-cov", "pytest-mock"] +validate = ["mypy", "ruff", "types-setuptools"] [[package]] name = "colorama" @@ -413,17 +415,17 @@ pyflakes = ">=3.2.0,<3.3.0" [[package]] name = "flake8-bugbear" -version = "24.8.19" +version = "24.10.31" description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle." optional = false python-versions = ">=3.8.1" files = [ - {file = "flake8_bugbear-24.8.19-py3-none-any.whl", hash = "sha256:25bc3867f7338ee3b3e0916bf8b8a0b743f53a9a5175782ddc4325ed4f386b89"}, - {file = "flake8_bugbear-24.8.19.tar.gz", hash = "sha256:9b77627eceda28c51c27af94560a72b5b2c97c016651bdce45d8f56c180d2d32"}, + {file = "flake8_bugbear-24.10.31-py3-none-any.whl", hash = "sha256:cccf786ccf9b2e1052b1ecfa80fb8f80832d0880425bcbd4cd45d3c8128c2683"}, + {file = "flake8_bugbear-24.10.31.tar.gz", hash = "sha256:435b531c72b27f8eff8d990419697956b9fd25c6463c5ba98b3991591de439db"}, ] [package.dependencies] -attrs = ">=19.2.0" +attrs = ">=22.2.0" flake8 = ">=6.0.0" [package.extras] @@ -431,13 +433,13 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest", [[package]] name = "flake8-comprehensions" -version = "3.15.0" +version = "3.16.0" description = "A flake8 plugin to help you write better list/set/dict comprehensions." optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "flake8_comprehensions-3.15.0-py3-none-any.whl", hash = "sha256:b7e027bbb52be2ceb779ee12484cdeef52b0ad3c1fcb8846292bdb86d3034681"}, - {file = "flake8_comprehensions-3.15.0.tar.gz", hash = "sha256:923c22603e0310376a6b55b03efebdc09753c69f2d977755cba8bb73458a5d4d"}, + {file = "flake8_comprehensions-3.16.0-py3-none-any.whl", hash = "sha256:7c1eadc9d22e765f39857798febe7766b4d9c519793c6c149e3e13bf99693f70"}, + {file = "flake8_comprehensions-3.16.0.tar.gz", hash = "sha256:9cbf789905a8f03f9d350fb82b17b264d9a16c7ce3542b2a7b871ef568cafabe"}, ] [package.dependencies] @@ -472,6 +474,45 @@ files = [ classify-imports = "*" flake8 = "*" +[[package]] +name = "gnureadline" +version = "8.2.13" +description = "The standard Python readline extension statically linked against the GNU readline library." +optional = false +python-versions = "*" +files = [ + {file = "gnureadline-8.2.13-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:0ca03501ce0939d7ecf9d075860d6f6ceb2f49f30331b4e96e4678ce03687bab"}, + {file = "gnureadline-8.2.13-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:c28e33bfc56d4204693f213abeab927f65c505ce91f668a039720bc7c46b0353"}, + {file = "gnureadline-8.2.13-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6472e3a780087eecd67c03e5455aecb209de51bcae74583222976f6b816f6192"}, + {file = "gnureadline-8.2.13-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:94b143ea5d22b0c1ca4a591265afe135272c69b7757e968e34fbb47a7858d1ce"}, + {file = "gnureadline-8.2.13-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:561a60b12f74ea7234036cc4fe558f3b46023be0dac5ed73541ece58cba2f88a"}, + {file = "gnureadline-8.2.13-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:daa405028b9fe92bfbb93624e13e0674a242a1c5434b70ef61a04294502fdb65"}, + {file = "gnureadline-8.2.13-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:576dac060887adc6067ee9d23fb2f0031fb2b3e560e07a6c9e666e05f0473af7"}, + {file = "gnureadline-8.2.13-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:10fcaf561bc4ed6ab7075ab3ead188a18faaf4e6e92d916f81a09c0a670ce906"}, + {file = "gnureadline-8.2.13-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:9c152a82613fa012ab4331bb9a0ffddb415e37561d376b910bf9e7d535607faf"}, + {file = "gnureadline-8.2.13-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:85e362d2d0e85e45f0affae7bbfaf998b00167c55a78d31ee0f214de9ff429d2"}, + {file = "gnureadline-8.2.13-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:b69e6608cc94e110018b721a11718d480a6330e0b62cbab65a22880e84011205"}, + {file = "gnureadline-8.2.13-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0cc77fc9c8a8fcf10e0a554e49ee763219683386b8f906b7e6ef07c9e40e8420"}, + {file = "gnureadline-8.2.13-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:2d3e33d2e0dd694d623a2ca1fae6990b52f1d25955504b7293a9350fb9912940"}, + {file = "gnureadline-8.2.13-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:6c550d08c4d2882a83293a724b14a262ee5078fd4fa7acdc78aa59cab26ae343"}, + {file = "gnureadline-8.2.13-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a7d6e3f5d9fd0cf8a84fb382d4e3ad2914331be4d929f17d50da01f1571c4b03"}, + {file = "gnureadline-8.2.13-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f59275168cae1b02ca1ec7586a9804bb04ce427df92f8582a80d16e96c846b78"}, + {file = "gnureadline-8.2.13-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:59c5505026646da6d5ced6a5316d6d191d011e8be422cba4abce71730ef37dc6"}, + {file = "gnureadline-8.2.13-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3f1050ecf789f34d0ab0aacdb605f177725009a864e0038e70380614af92dc0d"}, + {file = "gnureadline-8.2.13-cp36-cp36m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:23b43c8e9e2e6566cb3094749826181a86dba1d94b1e023b5f9923dc26e37876"}, + {file = "gnureadline-8.2.13-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:4f5fc90af56a1ae6f88c9c7122fc76141c395b6c342a63800abed8c813f48b85"}, + {file = "gnureadline-8.2.13-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d708e8f655d3b556a138f13e9fcb2d8a10a6901e3125c04cad5ef7c883191fe8"}, + {file = "gnureadline-8.2.13-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:265bcf6ef7082e130160fb34b9664284affb216a22c5bffcd518b35d02bcc4e9"}, + {file = "gnureadline-8.2.13-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:07231f8191adb7f204010a86a91df9df9a80944981a16576a471f59304ad6a16"}, + {file = "gnureadline-8.2.13-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:30cc1b6cb11d94554815cb91eb1dfa6a11887185aae50f253adaa393e91c6a86"}, + {file = "gnureadline-8.2.13-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:50c40bfffffa82d4fcb0fde4940d4ff128ba2f876c1da09bae9d6d9ff770095e"}, + {file = "gnureadline-8.2.13-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:dcfa601d95c00aa670ec5e4bf791caf6ba0bcf266de940fb54d44c278bd302fe"}, + {file = "gnureadline-8.2.13-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:c7b8d3f2a2c9b7e6feaf1f20bdb6ebb8210e207b8c5360ffe407a47efeeb3fb8"}, + {file = "gnureadline-8.2.13-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:811d85a70ac97cddeb1755282915e8a93c279dcf89513426f28617b8feff5aec"}, + {file = "gnureadline-8.2.13-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4f57a3aa97c3379b2513c8bfbac0de2dfb41f695623c0b2ad337babb646b51a7"}, + {file = "gnureadline-8.2.13.tar.gz", hash = "sha256:c9b9e1e7ba99a80bb50c12027d6ce692574f77a65bf57bc97041cf81c0f49bd1"}, +] + [[package]] name = "graphviz" version = "0.20.3" @@ -504,13 +545,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.115.3" +version = "6.118.8" description = "A library for property-based testing" optional = false python-versions = ">=3.9" files = [ - {file = "hypothesis-6.115.3-py3-none-any.whl", hash = "sha256:d2770b0db08ad666fe6ff36027910039ab681084d13bcf9c057449c2e27099c4"}, - {file = "hypothesis-6.115.3.tar.gz", hash = "sha256:d4efc8c7371bd4ec906d2777f1f18fee5539e47b3d7c7cdc93d1026ad35d9b33"}, + {file = "hypothesis-6.118.8-py3-none-any.whl", hash = "sha256:9363bde019f9d11d584d3c96af8273ab8a6a43009a7c9b1c2fd503c646062304"}, + {file = "hypothesis-6.118.8.tar.gz", hash = "sha256:2a564996f60b8961b5112672564516a522fbd6ab4b536f8c6f3e4adb125b7dd2"}, ] [package.dependencies] @@ -519,10 +560,10 @@ exceptiongroup = {version = ">=1.0.0", markers = "python_version < \"3.11\""} sortedcontainers = ">=2.1.0,<3.0.0" [package.extras] -all = ["black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.74)", "django (>=4.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.16)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.19.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"] +all = ["black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.77)", "django (>=4.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.18)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.19.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"] cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"] codemods = ["libcst (>=0.3.16)"] -crosshair = ["crosshair-tool (>=0.0.74)", "hypothesis-crosshair (>=0.0.16)"] +crosshair = ["crosshair-tool (>=0.0.77)", "hypothesis-crosshair (>=0.0.18)"] dateutil = ["python-dateutil (>=1.4)"] django = ["django (>=4.2)"] dpcontracts = ["dpcontracts (>=0.4)"] @@ -585,13 +626,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.165" +version = "7.1.167" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.165-py3-none-any.whl", hash = "sha256:a22e3cd3a3abc29d379f2022cba2cdecc553986bb582777317aa9f41ce164c11"}, - {file = "kframework-7.1.165.tar.gz", hash = "sha256:145dd780ecb1bc38492ed6190a9a4caa13741e0a6d81e4ea6fcf4b8bfdbbbeb7"}, + {file = "kframework-7.1.167-py3-none-any.whl", hash = "sha256:c6229b45f6af74cb605dd46d9f9625c7b3696f445300393f594d5b76c2d33a31"}, + {file = "kframework-7.1.167.tar.gz", hash = "sha256:b79d11a0e71650a14e8ae08b8cc38f766a4aea536066d1ab019b043acf02a712"}, ] [package.dependencies] @@ -805,13 +846,13 @@ files = [ [[package]] name = "packaging" -version = "24.1" +version = "24.2" description = "Core utilities for Python packages" optional = false python-versions = ">=3.8" files = [ - {file = "packaging-24.1-py3-none-any.whl", hash = "sha256:5b8f2217dbdbd2f7f384c41c628544e6d52f2d0f53c6d0c3ea61aa5d1d7ff124"}, - {file = "packaging-24.1.tar.gz", hash = "sha256:026ed72c8ed3fcce5bf8950572258698927fd1dbda10a5e981cdf0ac37f4f002"}, + {file = "packaging-24.2-py3-none-any.whl", hash = "sha256:09abb1bccd265c01f4a3aa3f7a7db064b36514d2cba19a2f694fe6150451a759"}, + {file = "packaging-24.2.tar.gz", hash = "sha256:c228a6dc5e932d346bc5739379109d49e8853dd8223571c7c5b55260edc0b97f"}, ] [[package]] @@ -977,7 +1018,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pykwasm" -version = "0.1.112" +version = "0.1.113" description = "" optional = false python-versions = "^3.10" @@ -986,15 +1027,15 @@ develop = false [package.dependencies] cytoolz = "^0.12.1" -kframework = "7.1.165" +kframework = "7.1.167" numpy = "^1.24.2" py-wasm = {git = "https://github.com/runtimeverification/py-wasm.git", tag = "0.2.1"} [package.source] type = "git" url = "https://github.com/runtimeverification/wasm-semantics.git" -reference = "v0.1.112" -resolved_reference = "345e90e2dca5a7c4628fcbb3a0292897d0cdbf62" +reference = "v0.1.113" +resolved_reference = "357bc66b36e549ea4047c2ed3bb3d68373ba7308" subdirectory = "pykwasm" [[package]] @@ -1045,17 +1086,17 @@ dev = ["argcomplete", "attrs (>=19.2)", "hypothesis (>=3.56)", "mock", "pygments [[package]] name = "pytest-cov" -version = "5.0.0" +version = "6.0.0" description = "Pytest plugin for measuring coverage." optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "pytest-cov-5.0.0.tar.gz", hash = "sha256:5837b58e9f6ebd335b0f8060eecce69b662415b16dc503883a02f45dfeb14857"}, - {file = "pytest_cov-5.0.0-py3-none-any.whl", hash = "sha256:4f0764a1219df53214206bf1feea4633c3b558a2925c8b59f144f682861ce652"}, + {file = "pytest-cov-6.0.0.tar.gz", hash = "sha256:fde0b595ca248bb8e2d76f020b465f3b107c9632e6a1d1705f17834c89dcadc0"}, + {file = "pytest_cov-6.0.0-py3-none-any.whl", hash = "sha256:eee6f1b9e61008bd34975a4d5bab25801eb31898b032dd55addc93e96fcaaa35"}, ] [package.dependencies] -coverage = {version = ">=5.2.1", extras = ["toml"]} +coverage = {version = ">=7.5", extras = ["toml"]} pytest = ">=4.6" [package.extras] @@ -1114,13 +1155,13 @@ tokenize-rt = ">=6.1.0" [[package]] name = "rich" -version = "13.9.3" +version = "13.9.4" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" optional = false python-versions = ">=3.8.0" files = [ - {file = "rich-13.9.3-py3-none-any.whl", hash = "sha256:9836f5096eb2172c9e77df411c1b009bace4193d6a481d534fea75ebba758283"}, - {file = "rich-13.9.3.tar.gz", hash = "sha256:bc1e01b899537598cf02579d2b9f4a415104d3fc439313a7a2c165d76557a08e"}, + {file = "rich-13.9.4-py3-none-any.whl", hash = "sha256:6049d5e6ec054bf2779ab3358186963bac2ea89175919d699e378b99738c2a90"}, + {file = "rich-13.9.4.tar.gz", hash = "sha256:439594978a49a09530cff7ebc4b5c7103ef57baf48d5ea3184f21d9a2befa098"}, ] [package.dependencies] @@ -1133,23 +1174,23 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] [[package]] name = "setuptools" -version = "75.2.0" +version = "75.4.0" description = "Easily download, build, install, upgrade, and uninstall Python packages" optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "setuptools-75.2.0-py3-none-any.whl", hash = "sha256:a7fcb66f68b4d9e8e66b42f9876150a3371558f98fa32222ffaa5bced76406f8"}, - {file = "setuptools-75.2.0.tar.gz", hash = "sha256:753bb6ebf1f465a1912e19ed1d41f403a79173a9acf66a42e7e6aec45c3c16ec"}, + {file = "setuptools-75.4.0-py3-none-any.whl", hash = "sha256:b3c5d862f98500b06ffdf7cc4499b48c46c317d8d56cb30b5c8bce4d88f5c216"}, + {file = "setuptools-75.4.0.tar.gz", hash = "sha256:1dc484f5cf56fd3fe7216d7b8df820802e7246cfb534a1db2aa64f14fcb9cdcb"}, ] [package.extras] -check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)", "ruff (>=0.5.2)"] -core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.collections", "jaraco.functools", "jaraco.text (>=3.7)", "more-itertools", "more-itertools (>=8.8)", "packaging", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] +check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)", "ruff (>=0.7.0)"] +core = ["importlib-metadata (>=6)", "jaraco.collections", "jaraco.functools (>=4)", "jaraco.text (>=3.7)", "more-itertools", "more-itertools (>=8.8)", "packaging", "packaging (>=24.2)", "platformdirs (>=4.2.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] cover = ["pytest-cov"] doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier", "towncrier (<24.7)"] enabler = ["pytest-enabler (>=2.2)"] -test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-home (>=0.5)", "pytest-perf", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"] -type = ["importlib-metadata (>=7.0.2)", "jaraco.develop (>=7.21)", "mypy (==1.11.*)", "pytest-mypy"] +test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test (>=5.5)", "packaging (>=24.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-home (>=0.5)", "pytest-perf", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"] +type = ["importlib-metadata (>=7.0.2)", "jaraco.develop (>=7.21)", "mypy (>=1.12,<1.14)", "pytest-mypy"] [[package]] name = "sortedcontainers" @@ -1195,13 +1236,13 @@ files = [ [[package]] name = "tomli" -version = "2.0.2" +version = "2.1.0" description = "A lil' TOML parser" optional = false python-versions = ">=3.8" files = [ - {file = "tomli-2.0.2-py3-none-any.whl", hash = "sha256:2ebe24485c53d303f690b0ec092806a085f07af5a5aa1464f3931eec36caaa38"}, - {file = "tomli-2.0.2.tar.gz", hash = "sha256:d46d457a85337051c36524bc5349dd91b1877838e2979ac5ced3e710ed8a60ed"}, + {file = "tomli-2.1.0-py3-none-any.whl", hash = "sha256:a5c57c3d1c56f5ccdf89f6523458f60ef716e210fc47c4cfb188c5ba473e0391"}, + {file = "tomli-2.1.0.tar.gz", hash = "sha256:3f646cae2aec94e17d04973e4249548320197cfabdf130015d023de4b74d8ab8"}, ] [[package]] @@ -1264,13 +1305,13 @@ files = [ [[package]] name = "zipp" -version = "3.20.2" +version = "3.21.0" description = "Backport of pathlib-compatible object wrapper for zip files" optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "zipp-3.20.2-py3-none-any.whl", hash = "sha256:a817ac80d6cf4b23bf7f2828b7cabf326f15a001bea8b1f9b49631780ba28350"}, - {file = "zipp-3.20.2.tar.gz", hash = "sha256:bc9eb26f4506fda01b81bcde0ca78103b6e62f991b381fec825435c836edbc29"}, + {file = "zipp-3.21.0-py3-none-any.whl", hash = "sha256:ac1bbe05fd2991f160ebce24ffbac5f6d11d83dc90891255885223d42b3cd931"}, + {file = "zipp-3.21.0.tar.gz", hash = "sha256:2c9958f6430a2040341a52eb608ed6dd93ef4392e02ffe219417c1b28b5dd1f4"}, ] [package.extras] @@ -1284,4 +1325,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "1ff7b3fd3b802aa4e3a84c8f4a3c99bf96db664ad7314ca1201cd7d0d51ff0ad" +content-hash = "0081471bed965f5a2a20aef41e43b1c0f8ccc2188e3c36efc8aacaf5d06292d9" diff --git a/pyproject.toml b/pyproject.toml index e44b682..2ddbf91 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.38" +version = "0.1.39" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", @@ -18,7 +18,7 @@ soroban-semantics = "komet.kdist.plugin" [tool.poetry.dependencies] python = "^3.10" -pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.112", subdirectory = "pykwasm" } +pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.113", subdirectory = "pykwasm" } [tool.poetry.group.dev.dependencies] autoflake = "*" From 3b9a1d913f68ed1ace9414515852eac3276f798f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Burak=20Bilge=20Yal=C3=A7=C4=B1nkaya?= Date: Mon, 18 Nov 2024 11:28:21 +0300 Subject: [PATCH 2/2] Implement `symbol_index_in_linear_memory` (#46) * move `loadSlices` to `symbol.md` * implement `symbol_index_in_linear_memory` * add komet test * Set Version: 0.1.39 * Set Version: 0.1.40 --------- Co-authored-by: devops --- package/version | 2 +- pyproject.toml | 2 +- src/komet/kdist/soroban-semantics/host/map.md | 42 -------- .../kdist/soroban-semantics/host/symbol.md | 99 ++++++++++++++++++- .../contracts/test_custom_types/Cargo.toml | 15 +++ .../contracts/test_custom_types/src/lib.rs | 50 ++++++++++ 6 files changed, 165 insertions(+), 45 deletions(-) create mode 100644 src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml create mode 100644 src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs diff --git a/package/version b/package/version index 528bd04..7172442 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.39 +0.1.40 diff --git a/pyproject.toml b/pyproject.toml index 2ddbf91..a2eab2a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.39" +version = "0.1.40" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kdist/soroban-semantics/host/map.md b/src/komet/kdist/soroban-semantics/host/map.md index aef32ca..9e6adfd 100644 --- a/src/komet/kdist/soroban-semantics/host/map.md +++ b/src/komet/kdist/soroban-semantics/host/map.md @@ -102,47 +102,5 @@ The function returns a `HostVal` pointing to the new map object. RELS requires size(KEYS) ==Int lengthBytes(VALS_BS) /Int 8 -``` - -## Helpers - - -```k - - syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)] - // -------------------------------------------------------------------------------- - rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned)) - Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS))) - requires lengthBytes(BS) >=Int 4 - rule Bytes2U32List(BS) => .List - requires lengthBytes(BS) loadSlices - => loadSlicesAux(Bytes2U32List(KEY_SLICES)) - ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8) - ... - - KEY_SLICES : S => S - - rule [loadSlicesAux-empty]: - loadSlicesAux(.List) => .K ... - - rule [loadSlicesAux]: - loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN)) - => #memLoad(OFFSET, LEN) - ~> mkSymbolFromStack - ~> loadSlicesAux(REST) - ... - - endmodule ``` \ No newline at end of file diff --git a/src/komet/kdist/soroban-semantics/host/symbol.md b/src/komet/kdist/soroban-semantics/host/symbol.md index 61032ec..1ea94b9 100644 --- a/src/komet/kdist/soroban-semantics/host/symbol.md +++ b/src/komet/kdist/soroban-semantics/host/symbol.md @@ -11,8 +11,11 @@ module HOST-SYMBOL imports WASM-OPERATIONS imports HOST-INTEGER imports SWITCH-SYNTAX +``` - // symbol_new_from_linear_memory +## symbol_new_from_linear_memory + +```k rule [hostfun-symbol-new-from-linear-memory]: hostCall ( "b" , "j" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) => #memLoad(getMajor(HostVal(LM_POS)), getMajor(HostVal(LEN))) @@ -38,11 +41,105 @@ module HOST-SYMBOL BS:Bytes : S => S requires validSymbol(Bytes2String(BS)) + // TODO add validity check syntax InternalInstr ::= "mkSymbolFromStack" [symbol(mkSymbolFromStack)] // --------------------------------------------------------------------------------- rule [mkSymbolFromStack]: mkSymbolFromStack => .K ... (BS => Symbol(Bytes2String(BS))) : _ +``` + +## symbol_index_in_linear_memory + +Linear search a `Symbol` in an array of byte slices. Return the index of the element or trap if not found. + +```k + rule [hostfun-symbol-index-in-linear-memory]: + hostCall ( "b" , "m" , [ i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(SYMBOL)) + ~> #memLoad(getMajor(HostVal(POS)), 8 *Int getMajor(HostVal(LEN))) + ~> loadSlices + ~> symbolIndexInLinearMemory + ... + + + 0 |-> < i64 > SYMBOL // Symbol + 1 |-> < i64 > POS // U32VAL + 2 |-> < i64 > LEN // U32VAL + + requires fromSmallValid(HostVal(POS)) + andBool fromSmallValid(HostVal(LEN)) + + syntax InternalInstr ::= "symbolIndexInLinearMemory" [symbol(symbolIndexInLinearMemory)] + | symbolIndexInLinearMemoryAux(Int) [symbol(symbolIndexInLinearMemoryAux)] + // ------------------------------------------------------------------------------------------------------ + rule [symbolIndexInLinearMemory]: + symbolIndexInLinearMemory + => symbolIndexInLinearMemoryAux(indexOf(HAYSTACK, NEEDLE)) + ... + + NEEDLE:List : (Symbol(_) #as HAYSTACK) : S => S + + rule [symbolIndexInLinearMemoryAux-trap]: + symbolIndexInLinearMemoryAux(-1) => trap ... + + rule [symbolIndexInLinearMemoryAux]: + symbolIndexInLinearMemoryAux(N) => toSmall(U32(N)) ... + requires N =/=Int -1 + +``` + +## Helpers + + +```k + + syntax List ::= Bytes2U32List(Bytes) [function, total, symbol(Bytes2U32List)] + // -------------------------------------------------------------------------------- + rule Bytes2U32List(BS) => ListItem(Bytes2Int(substrBytes(BS, 0, 4), LE, Unsigned)) + Bytes2U32List(substrBytes(BS, 4, lengthBytes(BS))) + requires lengthBytes(BS) >=Int 4 + rule Bytes2U32List(BS) => .List + requires lengthBytes(BS) loadSlices + => loadSlicesAux(Bytes2U32List(KEY_SLICES)) + ~> collectStackObjects(lengthBytes(KEY_SLICES) /Int 8) + ... + + KEY_SLICES : S => S + + rule [loadSlicesAux-empty]: + loadSlicesAux(.List) => .K ... + + rule [loadSlicesAux]: + loadSlicesAux(REST ListItem(OFFSET) ListItem(LEN)) + => #memLoad(OFFSET, LEN) + ~> mkSymbolFromStack + ~> loadSlicesAux(REST) + ... + +``` + +- `indexOf(X, XS)`: returns the index of the first element in `XS` which is equal to `X`, or `-1` if there is no such element. + +```k + syntax Int ::= indexOf (KItem, List) [function, total, symbol(indexOf)] + | indexOfAux(KItem, List, Int) [function, total, symbol(indexOfAux)] + // -------------------------------------------------------------------------- + rule indexOf(X, XS) => indexOfAux(X, XS, 0) + rule indexOfAux(_, .List, _) => -1 + rule indexOfAux(X, ListItem(Y) _, N) => N requires X ==K Y + rule indexOfAux(X, ListItem(Y) XS, N) => indexOfAux(X, XS, N +Int 1) requires X =/=K Y endmodule ``` \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml new file mode 100644 index 0000000..1cc50cc --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_custom_types/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_custom_types" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs new file mode 100644 index 0000000..04be9a8 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_custom_types/src/lib.rs @@ -0,0 +1,50 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, contracttype, symbol_short, Address, Bytes, Env, FromVal, Symbol, TryFromVal, TryIntoVal, Val, Vec, EnvBase}; + +#[contract] +pub struct TestCustomTypesContract; + +#[contracttype] +#[derive(PartialEq)] +pub enum MyBool { + True, + False +} + +fn to_bool(p: &MyBool) -> bool { + match p { + MyBool::True => true, + MyBool::False => false + } +} + +fn from_bool(p: bool) -> MyBool { + if p { + MyBool::True + } else { + MyBool::False + } +} + + +#[contractimpl] +impl TestCustomTypesContract { + + pub fn test_my_bool_roundtrip(env: Env, p: bool) -> bool { + + // mp:MyBool lives in the Wasm memory + let mp = from_bool(p); + + // convert MyBool to a host object + let v: Val = mp.try_into_val(&env).unwrap(); + + // convert v:Val to MyBool, load it to the Wasm memory + // (using the 'symbol_index_in_linear_memory' host function under the hood) + let mp2: MyBool = MyBool::try_from_val(&env, &v).unwrap(); + + let p2 = to_bool(&mp2); + + mp == mp2 && p == p2 + } + +}