diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index d3635634f..022bc2309 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -81,7 +81,7 @@ jobs: - name: 'Build KEVM' run: | docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install' - docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` evm-semantics.plugin kontrol.foundry' + docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.foundry' - name: 'Run profiling' run: | PROF_ARGS=--numprocesses=8 @@ -113,7 +113,7 @@ jobs: - name: 'Build KEVM' run: | docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install' - docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kevm-dist --verbose build -j`nproc` evm-semantics.plugin evm-semantics.haskell kontrol.foundry' + docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry' - name: 'Run integration tests' run: | TEST_ARGS=--numprocesses=8 diff --git a/Dockerfile b/Dockerfile index efec215ba..c25372796 100644 --- a/Dockerfile +++ b/Dockerfile @@ -44,4 +44,4 @@ USER user ENV PATH=/home/user/.local/bin:${PATH} RUN pip install ./kontrol \ && rm -rf kontrol \ - && CXX=clang++-14 kevm-dist --verbose build -j4 + && CXX=clang++-14 kdist --verbose build -j4 diff --git a/README.md b/README.md index e801b6cf6..6119c1017 100644 --- a/README.md +++ b/README.md @@ -30,25 +30,25 @@ poetry install In order to build `kontrol`, you need to build these specific targets: ```sh -poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry +poetry run kdist --verbose build -j3 evm-semantics.haskell kontrol.foundry ``` To change the default compiler: ```sh -CXX=clang++-14 poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry +CXX=clang++-14 poetry run kdist --verbose build -j3 evm-semantics.haskell kontrol.foundry ``` On Apple Silicon: ```sh -APPLE_SILICON=true poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry +APPLE_SILICON=true poetry run kdist --verbose build -j3 evm-semantics.haskell kontrol.foundry ``` Targets can be cleaned with: ```sh -poetry run kevm-dist clean +poetry run kdist clean ``` -For more information, refer to `kevm-dist --help`. +For more information, refer to `kdist --help`. ## For developers diff --git a/deps/k_release b/deps/k_release index a17ac40fb..c7d7bcb6e 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.1.25 +6.1.35 diff --git a/deps/kevm_release b/deps/kevm_release index 0f55df9cf..b94725e12 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.372 +1.0.381 diff --git a/flake.lock b/flake.lock index 74debadb8..7df2a92ec 100644 --- a/flake.lock +++ b/flake.lock @@ -72,17 +72,17 @@ ] }, "locked": { - "lastModified": 1700130818, - "narHash": "sha256-i4hqzOfI5qpqU4sL0Vk/tJK8VSQEXIuSC42jnNp/0Z0=", + "lastModified": 1701231950, + "narHash": "sha256-tDMOnzs4qv7EYygfhYuEvuTK96GJBS5IAC2c8KesB/U=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "ac35589bb31831b346e143bfa98c51e670237b8e", + "rev": "f2ae5990cc61618e97c0350ffea7485574b246d1", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "ac35589bb31831b346e143bfa98c51e670237b8e", + "rev": "f2ae5990cc61618e97c0350ffea7485574b246d1", "type": "github" } }, @@ -217,11 +217,11 @@ ] }, "locked": { - "lastModified": 1699089190, - "narHash": "sha256-t9W8eIeJBUVt6n8sfDrG9J/t0B4KZ73M3ARis+DwQhM=", + "lastModified": 1701270599, + "narHash": "sha256-6JNWZuON189C2pJci7jBBXtJqGPO9UKEKGzHY9dTGKs=", "owner": "shazow", "repo": "foundry.nix", - "rev": "fc064153ac002e825724ff2091cd91e7d501ffef", + "rev": "1d4d9d015a64e9921f8837a83941d93182d92a71", "type": "github" }, "original": { @@ -238,17 +238,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1698918605, - "narHash": "sha256-p3n0+My1U+rfHjaFPClK92HxAjAWIxSmCYyORCWJfxo=", + "lastModified": 1701192512, + "narHash": "sha256-VWytUWtgTCaEYuRlFdRMQxt+La/xaPbC8KlxemyMBf0=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "eebe4e9fd9dd6c606b37a384dbbfecca85943a38", + "rev": "827252a324f651f361ac62de40dbf8888a089503", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "eebe4e9fd9dd6c606b37a384dbbfecca85943a38", + "rev": "827252a324f651f361ac62de40dbf8888a089503", "type": "github" } }, @@ -284,16 +284,16 @@ "rv-utils": "rv-utils" }, "locked": { - "lastModified": 1700563497, - "narHash": "sha256-DUqHy8PAyfHktEzELfyVEW5BJXIPS41yzC6cVqemYUg=", + "lastModified": 1701439419, + "narHash": "sha256-yGFiJyxgmHaeDB1or9aNn9xqcHpkD1Jwd60TVi2gq2E=", "owner": "runtimeverification", "repo": "k", - "rev": "41dfa2474fea88b1313e8ac2b12c25dd3e722f9e", + "rev": "549dc1e2e6a5fa1dc6ea40c35c42ebce47bf4587", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.1.25", + "ref": "v6.1.35", "repo": "k", "type": "github" } @@ -337,16 +337,16 @@ ] }, "locked": { - "lastModified": 1700882614, - "narHash": "sha256-aiC19H5n3d95CGsh0uEz4ei3sRSMgw1qrSlBPJQ26ro=", + "lastModified": 1701675705, + "narHash": "sha256-QosFguHrGRySYCJclMT68XoLviPloK5KxxN0Zz52fDY=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "ff93f5e41f4836c916b0103f05e24bcf7744572c", + "rev": "8c169c89ebf4e3541d93bad16e835aed85cc0e79", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.372", + "ref": "v1.0.381", "repo": "evm-semantics", "type": "github" } @@ -388,11 +388,11 @@ ] }, "locked": { - "lastModified": 1700523811, - "narHash": "sha256-WgzIxCEAyB2X1n1AoBds9hXIdWPyRhUJ0MRu2ZWWuQk=", + "lastModified": 1701348593, + "narHash": "sha256-kBtj9cf2VF4vid7w8C95OPjC7wWlN8lFFVsFL2J7f3w=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "5ca593b04cd15a3173cf09835eb2656f1264db64", + "rev": "4cbbb3a13dfb92903d9a955b1d7da4f38c6ef5fd", "type": "github" }, "original": { @@ -543,16 +543,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1700835993, - "narHash": "sha256-tnjEEO3L7xs6UrXLrMkt5IUeFfPF96UNQ3Lmov7axj0=", + "lastModified": 1701458619, + "narHash": "sha256-8A31wHmB31rzBulxAGhEJvNWep9QY7tN9D3CMYXSsC0=", "owner": "runtimeverification", "repo": "pyk", - "rev": "3c948debc4d6219315e94b60508cddc8e5bbe9b9", + "rev": "4a1a2c990078361259bbdaaaac41dd85c0cf1802", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.513", + "ref": "v0.1.525", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index 91194259d..527b1bdb5 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.372"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.381"; nixpkgs.follows = "kevm/nixpkgs"; nixpkgs-pyk.follows = "kevm/nixpkgs-pyk"; k-framework.follows = "kevm/k-framework"; @@ -76,7 +76,7 @@ cmake # This is somewhat hacky but it's only a build time dependency. # We basically override kevm-pyk to add kontrol as a runtime dependency - # so that kevm-dist finds the foundry target. + # so that kdist finds the foundry target. (prev.kevm-pyk.overridePythonAttrs (old: { propagatedBuildInputs = (old.propagatedBuildInputs or [ ]) ++ [ @@ -104,7 +104,7 @@ prev.lib.optionalString (prev.stdenv.isAarch64 && prev.stdenv.isDarwin) "APPLE_SILICON=true" - } kevm-dist build kontrol.foundry + } kdist build kontrol.foundry ''; installPhase = '' @@ -122,7 +122,7 @@ final.foundry-bin (solc.mkDefault final solc_version) ]) - } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR $out + } --set NIX_LIBS "${nixLibs prev}" --set KDIST_DIR $out ''; passthru = if solc_version == null then { diff --git a/package/version b/package/version index 1f7a170d7..59057fc2c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.77 +0.1.78 diff --git a/poetry.lock b/poetry.lock index c5149ab8f..363ac624e 100644 --- a/poetry.lock +++ b/poetry.lock @@ -293,13 +293,13 @@ pyflakes = ">=3.1.0,<3.2.0" [[package]] name = "flake8-bugbear" -version = "23.9.16" +version = "23.12.2" 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-23.9.16.tar.gz", hash = "sha256:90cf04b19ca02a682feb5aac67cae8de742af70538590509941ab10ae8351f71"}, - {file = "flake8_bugbear-23.9.16-py3-none-any.whl", hash = "sha256:b182cf96ea8f7a8595b2f87321d7d9b28728f4d9c3318012d896543d19742cb5"}, + {file = "flake8-bugbear-23.12.2.tar.gz", hash = "sha256:32b2903e22331ae04885dae25756a32a8c666c85142e933f43512a70f342052a"}, + {file = "flake8_bugbear-23.12.2-py3-none-any.whl", hash = "sha256:83324bad4d90fee4bf64dd69c61aff94debf8073fbd807c8b6a36eec7a2f0719"}, ] [package.dependencies] @@ -338,13 +338,13 @@ flake8 = "*" [[package]] name = "flake8-type-checking" -version = "2.5.1" +version = "2.7.0" description = "A flake8 plugin for managing type-checking imports & forward references" optional = false python-versions = ">=3.8" files = [ - {file = "flake8_type_checking-2.5.1-py3-none-any.whl", hash = "sha256:1cd5cd9731f34921b33640751455643ca1cf7ee4a347a45cd94d3af328a3dd64"}, - {file = "flake8_type_checking-2.5.1.tar.gz", hash = "sha256:bfc51dd6e09a26662ab19191f44102f0606377ec0271a0e764ae993346a206d6"}, + {file = "flake8_type_checking-2.7.0-py3-none-any.whl", hash = "sha256:bcb0f8bd88d2921482dcdc8349017f1c55d024c207e02c4f13cdd47c2d898a56"}, + {file = "flake8_type_checking-2.7.0.tar.gz", hash = "sha256:a738157af62e2040b0cd501a548d57dba49480dbb2227809aba2c0140c7856d2"}, ] [package.dependencies] @@ -383,20 +383,20 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "importlib-metadata" -version = "6.8.0" +version = "7.0.0" description = "Read metadata from Python packages" optional = false python-versions = ">=3.8" files = [ - {file = "importlib_metadata-6.8.0-py3-none-any.whl", hash = "sha256:3ebb78df84a805d7698245025b975d9d67053cd94c79245ba4b3eb694abe68bb"}, - {file = "importlib_metadata-6.8.0.tar.gz", hash = "sha256:dbace7892d8c0c4ac1ad096662232f831d4e64f4c4545bd53016a3e9d4654743"}, + {file = "importlib_metadata-7.0.0-py3-none-any.whl", hash = "sha256:d97503976bb81f40a193d41ee6570868479c69d5068651eb039c40d850c59d67"}, + {file = "importlib_metadata-7.0.0.tar.gz", hash = "sha256:7fc841f8b8332803464e5dc1c63a2e59121f46ca186c0e2e182e80bf8c1319f7"}, ] [package.dependencies] zipp = ">=0.5" [package.extras] -docs = ["furo", "jaraco.packaging (>=9)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"] +docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (<7.2.5)", "sphinx (>=3.5)", "sphinx-lint"] perf = ["ipython"] testing = ["flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs", "pytest (>=6)", "pytest-black (>=0.3.7)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-mypy (>=0.9.1)", "pytest-perf (>=0.9.2)", "pytest-ruff"] @@ -430,7 +430,7 @@ requirements-deprecated-finder = ["pip-api", "pipreqs"] [[package]] name = "kevm-pyk" -version = "1.0.372" +version = "1.0.381" description = "" optional = false python-versions = "^3.10" @@ -439,15 +439,14 @@ develop = false [package.dependencies] pathos = "*" -pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.513"} +pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.525"} tomlkit = "^0.11.6" -xdg-base-dirs = "^6.0.0" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.372" -resolved_reference = "ff93f5e41f4836c916b0103f05e24bcf7744572c" +reference = "v1.0.381" +resolved_reference = "8c169c89ebf4e3541d93bad16e835aed85cc0e79" subdirectory = "kevm-pyk" [[package]] @@ -810,7 +809,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.513" +version = "0.1.525" description = "" optional = false python-versions = "^3.10" @@ -826,12 +825,13 @@ psutil = "5.9.5" pybind11 = "^2.10.3" textual = "^0.27.0" tomli = "^2.0.1" +xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.513" -resolved_reference = "3c948debc4d6219315e94b60508cddc8e5bbe9b9" +reference = "v0.1.525" +resolved_reference = "4a1a2c990078361259bbdaaaac41dd85c0cf1802" [[package]] name = "pyperclip" @@ -1081,4 +1081,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "d740e84b8fe1991c704412120464680dff1d89785c1dfb08ccd23303bdce15f5" +content-hash = "d7448ed223671ed6df1f7bd37a4b0ca9360f97cb88fab5a6437cb2338dbddf44" diff --git a/pyproject.toml b/pyproject.toml index 57d2436ad..6fb4bb9fe 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.77" +version = "0.1.78" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.372", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.381", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 4ffb262b2..f48ec5221 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.77' +VERSION: Final = '0.1.78' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 0b00ac9ee..59079a69f 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -153,7 +153,7 @@ def exec_build( _ignore_arg(kwargs, 'o2', '-O2') _ignore_arg(kwargs, 'o3', '-O3') if target is None: - target = KompileTarget.HASKELL_BOOSTER + target = KompileTarget.HASKELL foundry_kompile( foundry_root=foundry_root, includes=includes, diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 626421e69..be1ea75fd 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -60,8 +60,8 @@ def kompile_target_args(self) -> ArgumentParser: args.add_argument( '--target', type=KompileTarget, - choices=[KompileTarget.HASKELL_BOOSTER, KompileTarget.MAUDE], - help='[haskell-booster|maude]', + choices=[KompileTarget.HASKELL, KompileTarget.MAUDE], + help='[haskell|maude]', ) return args diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index 49c5248c2..c6b05b904 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -6,10 +6,10 @@ from pathlib import Path from typing import TYPE_CHECKING -from kevm_pyk import kdist from kevm_pyk.kevm import KEVM from kevm_pyk.kompile import KompileTarget, kevm_kompile from pyk.kast.outer import KDefinition, KFlatModule, KImport, KRequire +from pyk.kdist import kdist from pyk.utils import ensure_dir_path, hash_str from .foundry import Foundry @@ -36,7 +36,7 @@ def foundry_kompile( llvm_kompile: bool = True, debug: bool = False, verbose: bool = False, - target: KompileTarget = KompileTarget.HASKELL_BOOSTER, + target: KompileTarget = KompileTarget.HASKELL, no_forge_build: bool = False, ) -> None: syntax_module = 'FOUNDRY-CONTRACTS' diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 70ea6c355..d7302023c 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -8,12 +8,12 @@ from subprocess import CalledProcessError from typing import TYPE_CHECKING -from kevm_pyk import kdist from kevm_pyk.kevm import KEVM from pyk.kast.inner import KApply, KLabel, KRewrite, KSort, KVariable from pyk.kast.kast import KAtt from pyk.kast.manip import abstract_term_safely from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal +from pyk.kdist import kdist from pyk.prelude.kbool import TRUE, andBool from pyk.prelude.kint import intToken from pyk.prelude.string import stringToken diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index c1f5fb844..786e4e74a 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -61,7 +61,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (502 steps) +│ (505 steps) ├─ 12 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> #return 128 0 ~> #pc [ STATICC ... │ pc: 2984