diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 3f55bc7ef..b04198003 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` plugin foundry' + 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' - 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` plugin haskell foundry' + 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' - name: 'Run integration tests' run: | TEST_ARGS=--numprocesses=8 diff --git a/README.md b/README.md index 36dd476be..e801b6cf6 100644 --- a/README.md +++ b/README.md @@ -30,17 +30,17 @@ poetry install In order to build `kontrol`, you need to build these specific targets: ```sh -poetry run kevm-dist --verbose build -j3 plugin haskell foundry +poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry ``` To change the default compiler: ```sh -CXX=clang++-14 poetry run kevm-dist --verbose build -j3 plugin haskell foundry +CXX=clang++-14 poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry ``` On Apple Silicon: ```sh -APPLE_SILICON=true poetry run kevm-dist --verbose build -j3 plugin haskell foundry +APPLE_SILICON=true poetry run kevm-dist --verbose build -j3 evm-semantics.plugin evm-semantics.haskell kontrol.foundry ``` Targets can be cleaned with: @@ -81,4 +81,4 @@ For more information about the [K Framework], refer to these sources: - [Logical Frameworks](https://dl.acm.org/doi/10.5555/208683.208700): Discussion of logical frameworks. [K Framework]: -[kup package manager]: \ No newline at end of file +[kup package manager]: diff --git a/deps/k_release b/deps/k_release index 31ef8ee69..f3b5af39e 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.174 +6.1.1 diff --git a/deps/kevm_release b/deps/kevm_release index 50b74d4d0..5e952e4f0 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.333 +1.0.347 diff --git a/flake.lock b/flake.lock index aa0f01cbf..fb8bd2ff8 100644 --- a/flake.lock +++ b/flake.lock @@ -72,17 +72,17 @@ ] }, "locked": { - "lastModified": 1698380696, - "narHash": "sha256-+2ll6O1nn53Fgm09R+Bz4otMs5jn3Xeo2nx0tfhmnH0=", + "lastModified": 1699449951, + "narHash": "sha256-XQ4xHUGvG77JTWPepKzeGnKyTMHm3T7YlzaCyRuRu0w=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "59bdfa3f5e3ee4d82351d8de44137029c47e23a8", + "rev": "15a9fc41edcf6b22730f37e77a3e29acb2ae3601", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "59bdfa3f5e3ee4d82351d8de44137029c47e23a8", + "rev": "15a9fc41edcf6b22730f37e77a3e29acb2ae3601", "type": "github" } }, @@ -226,22 +226,18 @@ "foundry": { "inputs": { "flake-utils": [ - "kevm", - "k-framework", "flake-utils" ], "nixpkgs": [ - "kevm", - "k-framework", "nixpkgs" ] }, "locked": { - "lastModified": 1696410815, - "narHash": "sha256-uku47D/L+VzO3sVoZbnexPQPGeQtMwMFBesyaA1vKtE=", + "lastModified": 1699089190, + "narHash": "sha256-t9W8eIeJBUVt6n8sfDrG9J/t0B4KZ73M3ARis+DwQhM=", "owner": "shazow", "repo": "foundry.nix", - "rev": "a56126a754d73f85d904768fed569a9e250388d9", + "rev": "fc064153ac002e825724ff2091cd91e7d501ffef", "type": "github" }, "original": { @@ -258,17 +254,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1697702407, - "narHash": "sha256-r9c5qpgoejKJePbxqq01QkHx/wZNypY/fUSugsapF8w=", + "lastModified": 1698918605, + "narHash": "sha256-p3n0+My1U+rfHjaFPClK92HxAjAWIxSmCYyORCWJfxo=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "03a6228f78d7f4805fee4b9d9c45208dcbe0c9fb", + "rev": "eebe4e9fd9dd6c606b37a384dbbfecca85943a38", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "03a6228f78d7f4805fee4b9d9c45208dcbe0c9fb", + "rev": "eebe4e9fd9dd6c606b37a384dbbfecca85943a38", "type": "github" } }, @@ -306,16 +302,16 @@ "rv-utils": "rv-utils" }, "locked": { - "lastModified": 1698399750, - "narHash": "sha256-5l1tHDW848AQAniqPsITLn51ywV+s+5YILjR0CYFmQ8=", + "lastModified": 1699459419, + "narHash": "sha256-HMGdPX8jWdN/hSW8TMogVS+gcLEOzy5Iw5Inb+cpqQA=", "owner": "runtimeverification", "repo": "k", - "rev": "5f141fe4cd5c945015c4ac45946d37c7afedb3df", + "rev": "1d8b5cad4dba8e660ff20121be28251c10349af4", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.0.174", + "ref": "v6.1.1", "repo": "k", "type": "github" } @@ -330,7 +326,6 @@ "k-framework", "flake-utils" ], - "foundry": "foundry", "haskell-backend": [ "kevm", "k-framework", @@ -357,20 +352,19 @@ "kevm", "k-framework", "rv-utils" - ], - "solc": "solc" + ] }, "locked": { - "lastModified": 1698865334, - "narHash": "sha256-x2N8nhH+G83apOdGvxcD7EKn3TSuaoXV1ryNtteNy0s=", + "lastModified": 1699521787, + "narHash": "sha256-tqUrZNT73ZU3mFP6snSr4K8/YtJ+INyMFn0DeD6UKmY=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "f14d29c829417a6be1a04789f6201af1981d7c20", + "rev": "2e56a6371066a87a684ec4bd0ef4f0387cbcb865", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.333", + "ref": "v1.0.347", "repo": "evm-semantics", "type": "github" } @@ -416,11 +410,11 @@ ] }, "locked": { - "lastModified": 1697808331, - "narHash": "sha256-3jDWLywHyoOT2VdyITBl9yzHMw9GX6fRUXqDofjbFKE=", + "lastModified": 1699324123, + "narHash": "sha256-1BPe87ABW1FSe/sBdN3vy2y4gWQM9GsPysBuMlElRnM=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "480b54218da5f82876f25c70cb96c441f1a8eecd", + "rev": "cb8fe609ba0a9894b207c14da9e88bf311978d4c", "type": "github" }, "original": { @@ -444,16 +438,17 @@ ] }, "locked": { - "lastModified": 1643802645, - "narHash": "sha256-BynM25iwp/l3FyrcHqiNJdDxvN6IxSM3/zkFR6PD3B0=", - "owner": "nix-community", + "lastModified": 1656435814, + "narHash": "sha256-Gx4QoWB9eI437/66iqTr6AUjxGgN6WslqrQ57s+sL6A=", + "owner": "goodlyrottenapple", "repo": "mavenix", - "rev": "ce9ddfd7f361190e8e8dcfaf6b8282eebbb3c7cb", + "rev": "0cbd57b2494d52909b27f57d03580acc66bf0298", "type": "github" }, "original": { - "owner": "nix-community", + "owner": "goodlyrottenapple", "repo": "mavenix", + "rev": "0cbd57b2494d52909b27f57d03580acc66bf0298", "type": "github" } }, @@ -566,16 +561,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1698684955, - "narHash": "sha256-IO1mqA/Z4Mv9FF91qw4TfSWnBA0mse5snx3owKunnQc=", + "lastModified": 1699473822, + "narHash": "sha256-CzdPTlqBew6Xth/eUvEpEXAvyEZr0IWxfamVkK0ADRU=", "owner": "runtimeverification", "repo": "pyk", - "rev": "23a97935da94cded4392bc028cdf16bd6f7edd5b", + "rev": "edc297774f4ce99d44788aee7a0f6cee044aaf73", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.486", + "ref": "v0.1.494", "repo": "pyk", "type": "github" } @@ -603,10 +598,7 @@ "kevm", "flake-utils" ], - "foundry": [ - "kevm", - "foundry" - ], + "foundry": "foundry", "k-framework": [ "kevm", "k-framework" @@ -632,10 +624,7 @@ "kevm", "rv-utils" ], - "solc": [ - "kevm", - "solc" - ] + "solc": "solc" } }, "rv-utils": { @@ -673,13 +662,9 @@ "solc": { "inputs": { "flake-utils": [ - "kevm", - "k-framework", "flake-utils" ], "nixpkgs": [ - "kevm", - "k-framework", "nixpkgs" ] }, diff --git a/flake.nix b/flake.nix index 0c23ca838..4babb0b17 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.333"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.347"; nixpkgs.follows = "kevm/nixpkgs"; nixpkgs-pyk.follows = "kevm/nixpkgs-pyk"; k-framework.follows = "kevm/k-framework"; @@ -10,8 +10,17 @@ rv-utils.follows = "kevm/rv-utils"; pyk.follows = "kevm/pyk"; poetry2nix.follows = "kevm/poetry2nix"; - foundry.follows = "kevm/foundry"; - solc.follows = "kevm/solc"; + foundry = { + url = + "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases + inputs.nixpkgs.follows = "nixpkgs"; + inputs.flake-utils.follows = "flake-utils"; + }; + solc = { + url = "github:hellwolf/solc.nix"; + inputs.nixpkgs.follows = "nixpkgs"; + inputs.flake-utils.follows = "flake-utils"; + }; }; outputs = { self, k-framework, nixpkgs, flake-utils, poetry2nix, kevm , rv-utils, pyk, foundry, solc, ... }@inputs: @@ -93,16 +102,13 @@ prev.lib.optionalString (prev.stdenv.isAarch64 && prev.stdenv.isDarwin) "APPLE_SILICON=true" - } kevm-dist build -j4 foundry + } kevm-dist build kontrol.foundry ''; installPhase = '' mkdir -p $out cp -r ./kdist-*/* $out/ - ln -s ${prev.kevm}/haskell $out/haskell - ln -s ${prev.kevm}/haskell-standalone $out/haskell-standalone - ln -s ${prev.kevm}/llvm $out/llvm - ln -s ${prev.kevm}/plugin $out/plugin + ln -s ${prev.kevm}/evm-semantics $out/evm-semantics mkdir -p $out/bin makeWrapper ${ (kontrol-pyk { inherit solc_version; }) diff --git a/package/version b/package/version index 0665a48ef..8893a8e14 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.50 +0.1.55 diff --git a/poetry.lock b/poetry.lock index ee2ae44b9..7a5e7859e 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.7.0 and should not be changed by hand. [[package]] name = "attrs" @@ -35,29 +35,29 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} [[package]] name = "black" -version = "23.10.1" +version = "23.11.0" description = "The uncompromising code formatter." optional = false python-versions = ">=3.8" files = [ - {file = "black-23.10.1-cp310-cp310-macosx_10_16_arm64.whl", hash = "sha256:ec3f8e6234c4e46ff9e16d9ae96f4ef69fa328bb4ad08198c8cee45bb1f08c69"}, - {file = "black-23.10.1-cp310-cp310-macosx_10_16_x86_64.whl", hash = "sha256:1b917a2aa020ca600483a7b340c165970b26e9029067f019e3755b56e8dd5916"}, - {file = "black-23.10.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9c74de4c77b849e6359c6f01987e94873c707098322b91490d24296f66d067dc"}, - {file = "black-23.10.1-cp310-cp310-win_amd64.whl", hash = "sha256:7b4d10b0f016616a0d93d24a448100adf1699712fb7a4efd0e2c32bbb219b173"}, - {file = "black-23.10.1-cp311-cp311-macosx_10_16_arm64.whl", hash = "sha256:b15b75fc53a2fbcac8a87d3e20f69874d161beef13954747e053bca7a1ce53a0"}, - {file = "black-23.10.1-cp311-cp311-macosx_10_16_x86_64.whl", hash = "sha256:e293e4c2f4a992b980032bbd62df07c1bcff82d6964d6c9496f2cd726e246ace"}, - {file = "black-23.10.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7d56124b7a61d092cb52cce34182a5280e160e6aff3137172a68c2c2c4b76bcb"}, - {file = "black-23.10.1-cp311-cp311-win_amd64.whl", hash = "sha256:3f157a8945a7b2d424da3335f7ace89c14a3b0625e6593d21139c2d8214d55ce"}, - {file = "black-23.10.1-cp38-cp38-macosx_10_16_arm64.whl", hash = "sha256:cfcce6f0a384d0da692119f2d72d79ed07c7159879d0bb1bb32d2e443382bf3a"}, - {file = "black-23.10.1-cp38-cp38-macosx_10_16_x86_64.whl", hash = "sha256:33d40f5b06be80c1bbce17b173cda17994fbad096ce60eb22054da021bf933d1"}, - {file = "black-23.10.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:840015166dbdfbc47992871325799fd2dc0dcf9395e401ada6d88fe11498abad"}, - {file = "black-23.10.1-cp38-cp38-win_amd64.whl", hash = "sha256:037e9b4664cafda5f025a1728c50a9e9aedb99a759c89f760bd83730e76ba884"}, - {file = "black-23.10.1-cp39-cp39-macosx_10_16_arm64.whl", hash = "sha256:7cb5936e686e782fddb1c73f8aa6f459e1ad38a6a7b0e54b403f1f05a1507ee9"}, - {file = "black-23.10.1-cp39-cp39-macosx_10_16_x86_64.whl", hash = "sha256:7670242e90dc129c539e9ca17665e39a146a761e681805c54fbd86015c7c84f7"}, - {file = "black-23.10.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5ed45ac9a613fb52dad3b61c8dea2ec9510bf3108d4db88422bacc7d1ba1243d"}, - {file = "black-23.10.1-cp39-cp39-win_amd64.whl", hash = "sha256:6d23d7822140e3fef190734216cefb262521789367fbdc0b3f22af6744058982"}, - {file = "black-23.10.1-py3-none-any.whl", hash = "sha256:d431e6739f727bb2e0495df64a6c7a5310758e87505f5f8cde9ff6c0f2d7e4fe"}, - {file = "black-23.10.1.tar.gz", hash = "sha256:1f8ce316753428ff68749c65a5f7844631aa18c8679dfd3ca9dc1a289979c258"}, + {file = "black-23.11.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:dbea0bb8575c6b6303cc65017b46351dc5953eea5c0a59d7b7e3a2d2f433a911"}, + {file = "black-23.11.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:412f56bab20ac85927f3a959230331de5614aecda1ede14b373083f62ec24e6f"}, + {file = "black-23.11.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d136ef5b418c81660ad847efe0e55c58c8208b77a57a28a503a5f345ccf01394"}, + {file = "black-23.11.0-cp310-cp310-win_amd64.whl", hash = "sha256:6c1cac07e64433f646a9a838cdc00c9768b3c362805afc3fce341af0e6a9ae9f"}, + {file = "black-23.11.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:cf57719e581cfd48c4efe28543fea3d139c6b6f1238b3f0102a9c73992cbb479"}, + {file = "black-23.11.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:698c1e0d5c43354ec5d6f4d914d0d553a9ada56c85415700b81dc90125aac244"}, + {file = "black-23.11.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:760415ccc20f9e8747084169110ef75d545f3b0932ee21368f63ac0fee86b221"}, + {file = "black-23.11.0-cp311-cp311-win_amd64.whl", hash = "sha256:58e5f4d08a205b11800332920e285bd25e1a75c54953e05502052738fe16b3b5"}, + {file = "black-23.11.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:45aa1d4675964946e53ab81aeec7a37613c1cb71647b5394779e6efb79d6d187"}, + {file = "black-23.11.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:4c44b7211a3a0570cc097e81135faa5f261264f4dfaa22bd5ee2875a4e773bd6"}, + {file = "black-23.11.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2a9acad1451632021ee0d146c8765782a0c3846e0e0ea46659d7c4f89d9b212b"}, + {file = "black-23.11.0-cp38-cp38-win_amd64.whl", hash = "sha256:fc7f6a44d52747e65a02558e1d807c82df1d66ffa80a601862040a43ec2e3142"}, + {file = "black-23.11.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:7f622b6822f02bfaf2a5cd31fdb7cd86fcf33dab6ced5185c35f5db98260b055"}, + {file = "black-23.11.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:250d7e60f323fcfc8ea6c800d5eba12f7967400eb6c2d21ae85ad31c204fb1f4"}, + {file = "black-23.11.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5133f5507007ba08d8b7b263c7aa0f931af5ba88a29beacc4b2dc23fcefe9c06"}, + {file = "black-23.11.0-cp39-cp39-win_amd64.whl", hash = "sha256:421f3e44aa67138ab1b9bfbc22ee3780b22fa5b291e4db8ab7eee95200726b07"}, + {file = "black-23.11.0-py3-none-any.whl", hash = "sha256:54caaa703227c6e0c87b76326d0862184729a69b73d3b7305b6288e1d830067e"}, + {file = "black-23.11.0.tar.gz", hash = "sha256:4c68855825ff432d197229846f971bc4d6666ce90492e5b02013bcaca4d9ab05"}, ] [package.dependencies] @@ -430,7 +430,7 @@ requirements-deprecated-finder = ["pip-api", "pipreqs"] [[package]] name = "kevm-pyk" -version = "1.0.333" +version = "1.0.347" description = "" optional = false python-versions = "^3.10" @@ -439,15 +439,15 @@ develop = false [package.dependencies] pathos = "*" -pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.486"} +pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.494"} 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.333" -resolved_reference = "f14d29c829417a6be1a04789f6201af1981d7c20" +reference = "v1.0.347" +resolved_reference = "2e56a6371066a87a684ec4bd0ef4f0387cbcb865" subdirectory = "kevm-pyk" [[package]] @@ -808,7 +808,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.486" +version = "0.1.494" description = "" optional = false python-versions = "^3.10" @@ -828,8 +828,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.486" -resolved_reference = "23a97935da94cded4392bc028cdf16bd6f7edd5b" +reference = "v0.1.494" +resolved_reference = "edc297774f4ce99d44788aee7a0f6cee044aaf73" [[package]] name = "pyperclip" @@ -1079,4 +1079,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "67f482ed52fd3d5b0a04024ccf82ebd54a0492b71553bb5e1e4525984fd7b40d" +content-hash = "d517b19ada459b47510ec4af44d5c1030f637ecb61deeaaa6dd96fda1ccbac10" diff --git a/pyproject.toml b/pyproject.toml index b09d33b57..6db02ce86 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.50" +version = "0.1.55" 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.333", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.347", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index b6c248de6..d9c80697c 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.50' +VERSION: Final = '0.1.55' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 318a32fed..4c83971b2 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -6,10 +6,11 @@ from argparse import ArgumentParser from typing import TYPE_CHECKING -from kevm_pyk import kdist +import pyk from kevm_pyk.cli import node_id_like from kevm_pyk.utils import arg_pair_of from pyk.cli.utils import file_path +from pyk.kbuild.utils import KVersion, k_version from pyk.proof.reachability import APRProof from pyk.proof.tui import APRProofViewer @@ -63,6 +64,8 @@ def main() -> None: args = parser.parse_args() logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) + _check_k_version() + executor_name = 'exec_' + args.command.lower().replace('-', '_') if executor_name not in globals(): raise AssertionError(f'Unimplemented command: {args.command}') @@ -71,6 +74,29 @@ def main() -> None: execute(**vars(args)) +def _check_k_version() -> None: + expected_k_version = KVersion.parse(f'v{pyk.K_VERSION}') + actual_k_version = k_version() + + if not _compare_versions(expected_k_version, actual_k_version): + _LOGGER.warning(f'K version {expected_k_version} was expected but K version {actual_k_version} is being used.') + + +def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool: + if ver1.major != ver2.major or ver1.minor != ver2.minor or ver1.patch != ver2.patch: + return False + + if ver1.git == ver2.git: + return True + + if ver1.git and ver2.git: + return False + + git = ver1.git or ver2.git + assert git # git is not None for exactly one of ver1 and ver2 + return not git.ahead and not git.dirty + + # Command implementation @@ -92,11 +118,7 @@ def exec_solc_to_k( target: str | None = None, **kwargs: Any, ) -> None: - if target is None: - target = 'haskell' - k_text = solc_to_k( - definition_dir=kdist.get(target), contract_file=contract_file, contract_name=contract_name, main_module=main_module, @@ -439,7 +461,6 @@ def parse(s: str) -> list[T]: help='Output helper K definition for given JSON output from solc compiler.', parents=[ kontrol_cli_args.logging_args, - kontrol_cli_args.target_args, kontrol_cli_args.k_args, kontrol_cli_args.k_gen_args, ], diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md index 8050720c3..421d06180 100644 --- a/src/kontrol/kdist/foundry.md +++ b/src/kontrol/kdist/foundry.md @@ -1,85 +1,12 @@ -Foundry Specifications -====================== +#[Kontrol documentation](https://docs.runtimeverification.com/kontrol). -**ACTIVE DEVELOPMENT** +The documentation below may become deprecated. The documentation at the link above will be continuously updated and improved. -The Foundry integration allows users to take Solidity property tests and generate K specifications which can be executed using the Haskell symbolic backend. - -Before executing any of the KEVM instructions, make sure that you have the following: - 1. Successfully built or installed KEVM, - 2. The`kevm` binary is on your PATH, - 3. Activated the virtual environment (*applicable only for builds from source*). - -Below we are providing an example usage and a description of all the commands you can use with KEVM to improve your experience. - -Available Commands ------------------- - -Basic commands are (and each can be passed `--help`): - -- `kevm foundry-kompile`: Kompile a definition, generating claims for each Foundry test. - The best options are: - - `--regen` - needed if Solidity sources change, - - `--rekompile` - needed if K lemmas change, or K definition changes, - - `--require` - for adding an extra K file with lemmas, - - `--module-import` - importing an extra K module in one of the added K files with lemmas. - -- `kevm foundry-prove`: Run a given proof using the KCFG-based prover (not supporting loops yet, need to fall back to typical K for that). - The best options are: - - `--reinit` - want to start over from scratch, - - `--no-simplify-init` - do not want to invoke simplification on all the original nodes, can be faster, - - `--max-depth` - increase the space between saved nodes; bigger is faster, - - `--max-iterations` - maximum number of nodes to store in KCFG before giving on attempting proof for that run, - - `--break-every-step` - save a state every opcode, slow, good for debugging, - - `--break-on-calls` - save a state every time a call is made, good to turn on. - - `--verbose` - output what the prover is doing to make sure it's making progress. - -- `kevm foundry-show`: Display the given KCFG so far as text. - Options are: - - `--no-minimize` - do not omit all the gory details, - - `--node` - can be a repeated option, display more information about a given node hash, - - `--node-delta` - displays the delta between two given nodes in the KCFG. - -- `kevm foundry-view-kcfg`: Launch the more interactive exploration of the KCFG (can be done while exploration is running, must Ctrl-C + relaunch to view updates to KCFG). - - The interactive KCFG puts your terminal in *application mode*. To select text in this mode, hold the modifier key provided by your terminal emulator (typically SHIFT or OPTION) while clicking and dragging. Refer to the [Textualize documentation](https://github.com/Textualize/textual/blob/main/FAQ.md#how-can-i-select-and-copy-text-in-a-textual-app) for more information. - -- `kevm foundry-section-edge`: Given an edge in the graph, cut it into sections to get intermediate nodes. - -- `kevm foundry-step-node`: Step from a given node, adding it to the CFG. - -- `kevm foundry-simplify-node`: Simplify a given node, and potentially replace it. - -Example Usage -------------- - -The first step is to ensure the Solidity codebase is compiled and the `out/` directory is generated. - -For example, in the root of this repository, you can run: - -*Build Foundry Project:* - -```sh -$ cd tests/foundry -$ forge build -``` - -*Kompile to generate K specifications:* - -```sh -$ kevm foundry-kompile -``` - -*And discharge some specific test as a proof obligation (inside virtual environment):* - -```sh -$ kevm foundry-prove --test AssertTest.test_assert_true -``` - -Foundry Module for KEVM ------------------------ +Foundry Module for Kontrol +-------------------------- Foundry's testing framework provides a series of cheatcodes so that developers can specify what situation they want to test. -This file describes the KEVM specification of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. +This file describes the K semantics of the Foundry testing framework, which includes the definition of said cheatcodes and what does it mean for a test to pass. ```k requires "evm.md" @@ -145,9 +72,9 @@ Hence, checking if a `DSTest.assert*` has failed amounts to reading as a boolean module FOUNDRY-SUCCESS imports EVM - syntax Bool ::= + syntax Bool ::= "foundry_success" "(" - statusCode: StatusCode "," + statusCode: StatusCode "," failed: Int "," revertExpected: Bool "," opcodeExpected: Bool "," @@ -568,6 +495,7 @@ This rule returns a symbolic integer of up to the bit width that was sent as an requires SELECTOR ==Int selector ( "freshUInt(uint8)" ) andBool 0 #call_foundry SELECTOR _ => . ... - _ => #bufStrict(32, ?WORD) + _ => #buf(32, ?WORD) requires SELECTOR ==Int selector ( "freshBool()" ) ensures #rangeBool(?WORD) + [preserves-definedness] ``` Expecting the next call to revert @@ -1019,8 +948,8 @@ With address: Asserts the topics match and that the emitting address matches. ``` -Restricting the accounts that can be called in KEVM ---------------------------------------------------- +Restricting the accounts that can be called in Kontrol +------------------------------------------------------ A `StorageSlot` pair is formed from an address and a storage index. diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index 6f8ba817b..5a597caab 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -84,7 +84,7 @@ def foundry_kompile( copied_requires = [] copied_requires += [f'requires/{name}' for name in list(requires_paths.keys())] imports = ['FOUNDRY'] - kevm = KEVM(kdist.get('foundry')) + kevm = KEVM(kdist.get('kontrol.foundry')) empty_config = kevm.definition.empty_config(Foundry.Sorts.FOUNDRY_CELL) bin_runtime_definition = _foundry_to_contract_def( empty_config=empty_config, @@ -101,7 +101,7 @@ def foundry_kompile( ) kevm = KEVM( - kdist.get('foundry'), + kdist.get('kontrol.foundry'), extra_unparsing_modules=(bin_runtime_definition.all_modules + contract_main_definition.all_modules), ) @@ -133,7 +133,7 @@ def update_kompilation_digest() -> None: _LOGGER.info('Updated Kompilation digest') if not kompilation_up_to_date() or rekompile or not kompiled_timestamp.exists(): - plugin_dir = kdist.get('plugin') + plugin_dir = kdist.get('evm-semantics.plugin') kevm_kompile( target=KompileTarget.HASKELL_BOOSTER, diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 0baa57035..0c5fa7d5a 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -5,7 +5,7 @@ from typing import TYPE_CHECKING, NamedTuple from kevm_pyk.kevm import KEVM, KEVMSemantics -from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, kevm_prove, legacy_explore +from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, legacy_explore, run_prover from pathos.pools import ProcessPool # type: ignore from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence, KVariable, Subst @@ -204,15 +204,14 @@ def init_and_run_proof(test: FoundryTest) -> Proof: run_constructor=options.run_constructor, ) - kevm_prove( + run_prover( foundry.kevm, proof, kcfg_explore, max_depth=options.max_depth, max_iterations=options.max_iterations, - break_every_step=options.break_every_step, - break_on_jumpi=options.break_on_jumpi, - break_on_calls=options.break_on_calls, + cut_point_rules=KEVMSemantics.cut_point_rules(options.break_on_jumpi, options.break_on_calls), + terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), ) return proof diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 11e4b4970..fd4ef354b 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -8,6 +8,7 @@ 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 @@ -30,13 +31,13 @@ def solc_to_k( - definition_dir: Path, contract_file: Path, contract_name: str, main_module: str | None, requires: Iterable[str] = (), imports: Iterable[str] = (), ) -> str: + definition_dir = kdist.get('evm-semantics.haskell') kevm = KEVM(definition_dir) empty_config = kevm.definition.empty_config(KEVM.Sorts.KEVM_CELL) diff --git a/src/tests/integration/utils.py b/src/tests/integration/utils.py index 2c59cf1cb..27573a0c4 100644 --- a/src/tests/integration/utils.py +++ b/src/tests/integration/utils.py @@ -3,7 +3,6 @@ from pathlib import Path from typing import TYPE_CHECKING -from kevm_pyk import kdist from pyk.utils import check_dir_path from kontrol.solc_to_k import solc_to_k @@ -23,7 +22,6 @@ def gen_bin_runtime(contract_file: Path, output_dir: Path) -> tuple[Path, str]: main_file = output_dir / f'{contract_name.lower()}-bin-runtime.k' k_text = solc_to_k( - definition_dir=kdist.get('haskell'), contract_file=contract_file, contract_name=contract_name, main_module=main_module_name,