From bb00217f028217d9fb26ec0427e83f10505e8958 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:12:05 +0000 Subject: [PATCH 01/43] deps/pyk_release: Set Version v0.1.426 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index 6187db8f0b..a028cac101 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.425 +v0.1.426 From f3e173d508be0061660e18148a6859ec248c72aa Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:12:25 +0000 Subject: [PATCH 02/43] Set Version: 1.0.279 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3efd2e7e4d..f83ad4789d 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.278" +version = "1.0.279" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index a2fb0482ec..900d25ea87 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.278) unstable; urgency=medium +kevm (1.0.279) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 432f3a15bb..e83845c706 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.278 +1.0.279 From 056211f4e6cf4907e11308fff155e54352c3b02d Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:14:51 +0000 Subject: [PATCH 03/43] kevm-pyk/: sync poetry files pyk version v0.1.426 --- kevm-pyk/poetry.lock | 8 ++++---- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index b0b1ca95fb..7a226cb99c 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -788,7 +788,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.425" +version = "0.1.426" description = "" optional = false python-versions = "^3.10" @@ -808,8 +808,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.425" -resolved_reference = "c292c4610183acec2ae44d8f68973ebf3cb4cd1e" +reference = "v0.1.426" +resolved_reference = "2262611c2759adcf7bd59a7f8d020facf48a099f" [[package]] name = "pyperclip" @@ -1048,4 +1048,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "7a6eba6fae9c636c5f96e42d56b7f5cf5033f59481f4dd9e0344e3efe231b03b" +content-hash = "33c9177b01c67423fbb6e15639d21acd489a14d51be188fed6cddae82d30c5c9" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index f83ad4789d..e3389309cc 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.425" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.426" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From 3a8f76e2732cb38e79ffd08e426a72b0cf1e9924 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:17:04 +0000 Subject: [PATCH 04/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 14 +++++++------- flake.nix | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/flake.lock b/flake.lock index 88a3a02a3c..5459a10a29 100644 --- a/flake.lock +++ b/flake.lock @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1692801807, - "narHash": "sha256-4UwTosCoYspT9Jww3L+gQW4GChv4spJSkGtP7BP2hp0=", + "lastModified": 1692914670, + "narHash": "sha256-FFLdeMwj/pSTuRK9Rve0Fw6hbIxqqRY0dulxO3FyZ0I=", "owner": "runtimeverification", "repo": "pyk", - "rev": "c292c4610183acec2ae44d8f68973ebf3cb4cd1e", + "rev": "2262611c2759adcf7bd59a7f8d020facf48a099f", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.425", + "ref": "v0.1.426", "repo": "pyk", "type": "github" } @@ -1863,11 +1863,11 @@ ] }, "locked": { - "lastModified": 1692863432, - "narHash": "sha256-IKDrCwbSY7+9wQkRlH31UygyXSpSeo44DqraBh2UeLo=", + "lastModified": 1692871473, + "narHash": "sha256-2eLQOPBzQomQfcC8wQdYekccvl1KtYCqkDdw7oPeOiU=", "owner": "hellwolf", "repo": "solc.nix", - "rev": "d87ead250023a730633f30620dec95d97b9b3e7f", + "rev": "fbbe5553a7fc52f2d423afac81316023a183e72c", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 42fbd9b6d0..76c8cf9abd 100644 --- a/flake.nix +++ b/flake.nix @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.425"; + pyk.url = "github:runtimeverification/pyk/v0.1.426"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From a6c01d8c3c43d9d39e69176e7ebc6086a6066358 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:52:51 +0000 Subject: [PATCH 05/43] deps/pyk_release: Set Version v0.1.427 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index a028cac101..3a0d0b0137 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.426 +v0.1.427 From c9bb34714dedf144142b4286ffe1373c6ed5fb4d Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:55:59 +0000 Subject: [PATCH 06/43] kevm-pyk/: sync poetry files pyk version v0.1.427 --- kevm-pyk/poetry.lock | 8 ++++---- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 7a226cb99c..2cbab89f43 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -788,7 +788,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.426" +version = "0.1.427" description = "" optional = false python-versions = "^3.10" @@ -808,8 +808,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.426" -resolved_reference = "2262611c2759adcf7bd59a7f8d020facf48a099f" +reference = "v0.1.427" +resolved_reference = "fe1047044be2e3e2a3ea5090d824ea3daa449d8c" [[package]] name = "pyperclip" @@ -1048,4 +1048,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "33c9177b01c67423fbb6e15639d21acd489a14d51be188fed6cddae82d30c5c9" +content-hash = "a5ea55d8524ac5d04e0af5e79c7b76b5dba6c412f9d2655ca94068d9e00a4f85" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e3389309cc..e16caf990e 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.426" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.427" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From 48dcdd43932012deab0a001b548d55005612beec Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 24 Aug 2023 22:58:20 +0000 Subject: [PATCH 07/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index 5459a10a29..6423a8bd54 100644 --- a/flake.lock +++ b/flake.lock @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1692914670, - "narHash": "sha256-FFLdeMwj/pSTuRK9Rve0Fw6hbIxqqRY0dulxO3FyZ0I=", + "lastModified": 1692917001, + "narHash": "sha256-90mfRUkiQ2aQMLDaurig/YjDurQEowam2PCCnGyIFoE=", "owner": "runtimeverification", "repo": "pyk", - "rev": "2262611c2759adcf7bd59a7f8d020facf48a099f", + "rev": "fe1047044be2e3e2a3ea5090d824ea3daa449d8c", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.426", + "ref": "v0.1.427", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index 76c8cf9abd..c7deed3e25 100644 --- a/flake.nix +++ b/flake.nix @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.426"; + pyk.url = "github:runtimeverification/pyk/v0.1.427"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From 9601a84bbbc1d4987298767d4c2cfd6063ca02d8 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 25 Aug 2023 07:31:50 +0000 Subject: [PATCH 08/43] deps/pyk_release: Set Version v0.1.428 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index 3a0d0b0137..7076077b25 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.427 +v0.1.428 From 1ef0bb47d7acf9b63a5dc4480112636e6071231b Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 25 Aug 2023 07:34:08 +0000 Subject: [PATCH 09/43] kevm-pyk/: sync poetry files pyk version v0.1.428 --- kevm-pyk/poetry.lock | 8 ++++---- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 2cbab89f43..9f47470ea2 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -788,7 +788,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.427" +version = "0.1.428" description = "" optional = false python-versions = "^3.10" @@ -808,8 +808,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.427" -resolved_reference = "fe1047044be2e3e2a3ea5090d824ea3daa449d8c" +reference = "v0.1.428" +resolved_reference = "525c629460c24579ebc4d78a1cecaef44a0d89cb" [[package]] name = "pyperclip" @@ -1048,4 +1048,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "a5ea55d8524ac5d04e0af5e79c7b76b5dba6c412f9d2655ca94068d9e00a4f85" +content-hash = "1df8ad3c1fe59049e6ace33ed853be90bce5afa6c71d0c479b1867150638e431" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e16caf990e..33281eff42 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.427" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.428" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From 4c9b4f65cb455db242e497200e604257a0e73da6 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 25 Aug 2023 07:34:09 +0000 Subject: [PATCH 10/43] deps/k_release: sync release file version 6.0.69 --- deps/k_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/k_release b/deps/k_release index f889afac18..c6a0785c7b 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.67 +6.0.69 From 1f9b015624cee213bb2478c7c2f65dcd6b60ff02 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 25 Aug 2023 07:36:22 +0000 Subject: [PATCH 11/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 28 ++++++++++++++-------------- flake.nix | 4 ++-- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/flake.lock b/flake.lock index 6423a8bd54..0b52496187 100644 --- a/flake.lock +++ b/flake.lock @@ -547,11 +547,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1689068808, - "narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=", + "lastModified": 1692799911, + "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", "owner": "numtide", "repo": "flake-utils", - "rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4", + "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", "type": "github" }, "original": { @@ -1076,16 +1076,16 @@ "rv-utils": "rv-utils" }, "locked": { - "lastModified": 1692732310, - "narHash": "sha256-gcBd/kMS8XDSB148ttYpUxvSk+361Fx4+knc3ZQU3wk=", + "lastModified": 1692817190, + "narHash": "sha256-rwMLR1F4U+m6XbxO3KQ2Y1EUqQC0EtOBCBnHmO7CvKE=", "owner": "runtimeverification", "repo": "k", - "rev": "9045d43f9a900e79eeb5303e88d009fc371db464", + "rev": "645ffc4d6e3c34de3d85574a93604c9507af222e", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.0.67", + "ref": "v6.0.69", "repo": "k", "type": "github" } @@ -1139,11 +1139,11 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1692267154, - "narHash": "sha256-8jeSucCQ/1XPlDBIEfXcy+OHNXn/bVeY0ux8uWTqe3M=", + "lastModified": 1692815027, + "narHash": "sha256-oydxYW0oLxlmEsohMWg0IEryob9R1VCLmpbMRwKhdIg=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "7a964b819d16e7b651f581271798b40d152cb2d6", + "rev": "2cd7199d67842439504e26776efab88f719e6e41", "type": "github" }, "original": { @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1692917001, - "narHash": "sha256-90mfRUkiQ2aQMLDaurig/YjDurQEowam2PCCnGyIFoE=", + "lastModified": 1692948181, + "narHash": "sha256-FzQ54MIexQcC+sNGxtm7t9MQbp5l7UWpUfdPfy/bYs0=", "owner": "runtimeverification", "repo": "pyk", - "rev": "fe1047044be2e3e2a3ea5090d824ea3daa449d8c", + "rev": "525c629460c24579ebc4d78a1cecaef44a0d89cb", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.427", + "ref": "v0.1.428", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index c7deed3e25..0e2d759eb2 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { nixpkgs.url = "github:NixOS/nixpkgs/b01f185e4866de7c5b5a82f833ca9ea3c3f72fc4"; - k-framework.url = "github:runtimeverification/k/v6.0.67"; + k-framework.url = "github:runtimeverification/k/v6.0.69"; k-framework.inputs.nixpkgs.follows = "nixpkgs"; #nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.427"; + pyk.url = "github:runtimeverification/pyk/v0.1.428"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From 2db3b6dd0096d5aef871131786c88b4b0b3ebd34 Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 27 Aug 2023 23:12:05 +0000 Subject: [PATCH 12/43] deps/pyk_release: Set Version v0.1.429 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index 7076077b25..7ef627e7b5 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.428 +v0.1.429 From a3d26cad38f2a6bbc5e80b0cac917a892fbac9c5 Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 27 Aug 2023 23:12:26 +0000 Subject: [PATCH 13/43] Set Version: 1.0.280 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 33281eff42..06eaf70069 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.279" +version = "1.0.280" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 900d25ea87..f416f538a6 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.279) unstable; urgency=medium +kevm (1.0.280) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e83845c706..4418310f44 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.279 +1.0.280 From 46e32877f47d8059c2c2792436ed4db6667065ae Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 27 Aug 2023 23:14:55 +0000 Subject: [PATCH 14/43] kevm-pyk/: sync poetry files pyk version v0.1.429 --- kevm-pyk/poetry.lock | 16 ++++++++-------- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 9f47470ea2..f920a189a3 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -672,13 +672,13 @@ test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4)", "pytest-co [[package]] name = "pluggy" -version = "1.2.0" +version = "1.3.0" description = "plugin and hook calling mechanisms for python" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "pluggy-1.2.0-py3-none-any.whl", hash = "sha256:c2fd55a7d7a3863cba1a013e4e2414658b1d07b6bc57b3919e0c63c9abb99849"}, - {file = "pluggy-1.2.0.tar.gz", hash = "sha256:d12f0c4b579b15f5e054301bb226ee85eeeba08ffec228092f8defbaa3a4c4b3"}, + {file = "pluggy-1.3.0-py3-none-any.whl", hash = "sha256:d89c696a773f8bd377d18e5ecda92b7a3793cbe66c87060a6fb58c7b6e1061f7"}, + {file = "pluggy-1.3.0.tar.gz", hash = "sha256:cf61ae8f126ac6f7c451172cf30e3e43d3ca77615509771b3a984a0730651e12"}, ] [package.extras] @@ -788,7 +788,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.428" +version = "0.1.429" description = "" optional = false python-versions = "^3.10" @@ -808,8 +808,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.428" -resolved_reference = "525c629460c24579ebc4d78a1cecaef44a0d89cb" +reference = "v0.1.429" +resolved_reference = "8a27ac0637840bbee4d81e5df37cec5a2d8248d0" [[package]] name = "pyperclip" @@ -1048,4 +1048,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "1df8ad3c1fe59049e6ace33ed853be90bce5afa6c71d0c479b1867150638e431" +content-hash = "5529c3175099002ee5b74e296fd5127f6012f5cce021fb0f577b748d081684a4" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 06eaf70069..6c5514aa57 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.428" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.429" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From a8a403ea94e924dbe55575e1a6f31686c60e02ea Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 27 Aug 2023 23:17:20 +0000 Subject: [PATCH 15/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index 0b52496187..8c6036ea7c 100644 --- a/flake.lock +++ b/flake.lock @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1692948181, - "narHash": "sha256-FzQ54MIexQcC+sNGxtm7t9MQbp5l7UWpUfdPfy/bYs0=", + "lastModified": 1693177411, + "narHash": "sha256-d6AOxbJVbzkMaA0ySvsq3I2I54cMaerTCwtmRhKnshQ=", "owner": "runtimeverification", "repo": "pyk", - "rev": "525c629460c24579ebc4d78a1cecaef44a0d89cb", + "rev": "8a27ac0637840bbee4d81e5df37cec5a2d8248d0", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.428", + "ref": "v0.1.429", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index 0e2d759eb2..dcc5300b48 100644 --- a/flake.nix +++ b/flake.nix @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.428"; + pyk.url = "github:runtimeverification/pyk/v0.1.429"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From f3d5177cc13ac1a3a85e603c85a6b2296c642a8a Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Mon, 28 Aug 2023 09:28:06 +0200 Subject: [PATCH 16/43] adding terminal nodes in calls to APR prover, fixing function names --- kevm-pyk/src/kevm_pyk/__main__.py | 4 ++-- kevm-pyk/src/kontrol/foundry.py | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index f3e8b6ba12..a83ced1a4c 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -294,7 +294,7 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: kcfg.replace_node(target_node_id, new_target) proof_problem = APRProof( - claim.label, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory + claim.label, kcfg, [], init_node_id, target_node_id, {}, proof_dir=save_directory ) passed = kevm_prove( @@ -374,7 +374,7 @@ def exec_prune_proof( ) apr_proof = APRProof.read_proof_data(save_directory, claim.label) - node_ids = apr_proof.prune_from(node) + node_ids = apr_proof.prune(node) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index ac0d2dbbb0..acd6e704f0 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -759,7 +759,7 @@ def foundry_list(foundry_root: Path) -> list[str]: def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike) -> None: foundry = Foundry(foundry_root) apr_proof = foundry.get_apr_proof(test) - node_ids = apr_proof.prune_from(node) + node_ids = apr_proof.prune(node) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() @@ -1034,10 +1034,10 @@ def _method_to_apr_proof( kcfg_explore.simplify(kcfg, {}) if bmc_depth is not None: apr_proof = APRBMCProof( - proof_digest, kcfg, init_node_id, target_node_id, {}, bmc_depth, proof_dir=save_directory + proof_digest, kcfg, [], init_node_id, target_node_id, {}, bmc_depth, proof_dir=save_directory ) else: - apr_proof = APRProof(proof_digest, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory) + apr_proof = APRProof(proof_digest, kcfg, [], init_node_id, target_node_id, {}, proof_dir=save_directory) apr_proof.write_proof_data() return apr_proof From 693f7ae99066de8d3edffb75fc487650751f9026 Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 10:36:06 +0300 Subject: [PATCH 17/43] keep init and target --- kevm-pyk/src/kevm_pyk/__main__.py | 2 +- kevm-pyk/src/kontrol/foundry.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index a83ced1a4c..51d4ca5af8 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -374,7 +374,7 @@ def exec_prune_proof( ) apr_proof = APRProof.read_proof_data(save_directory, claim.label) - node_ids = apr_proof.prune(node) + node_ids = apr_proof.prune(node, keep_nodes=[apr_proof.init, apr_proof.target]) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index acd6e704f0..aa84d3b984 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -759,7 +759,7 @@ def foundry_list(foundry_root: Path) -> list[str]: def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike) -> None: foundry = Foundry(foundry_root) apr_proof = foundry.get_apr_proof(test) - node_ids = apr_proof.prune(node) + node_ids = apr_proof.prune(node, keep_nodes=[apr_proof.init, apr_proof.target]) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() From 8a1fef4aeccef7b924706d1c39e66b40b0a691a6 Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 10:38:46 +0300 Subject: [PATCH 18/43] adapt to pyk new handling of CTerm bottom/top --- kevm-pyk/poetry.lock | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 17 ++++++++--------- kevm-pyk/src/kevm_pyk/kevm.py | 21 ++++++++++++--------- kevm-pyk/src/kevm_pyk/utils.py | 7 ++----- kevm-pyk/src/kontrol/foundry.py | 12 +++++++----- 5 files changed, 30 insertions(+), 29 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index f920a189a3..afe43f6b6f 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/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.5.1 and should not be changed by hand. [[package]] name = "attrs" diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 51d4ca5af8..06ec0f9f00 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -15,7 +15,7 @@ from pyk.kore.tools import PrintOutput, kore_print from pyk.ktool.kompile import LLVMKompileType from pyk.ktool.krun import KRunOutput -from pyk.prelude.ml import is_bottom, is_top +from pyk.prelude.ml import is_top, mlAnd from pyk.proof import APRProof from pyk.proof.equality import EqualityProof from pyk.proof.show import APRProofShow @@ -164,8 +164,9 @@ def exec_prove_legacy( branching_allowed=branching_allowed, haskell_backend_args=haskell_backend_args, ) - print(kevm.pretty_print(final_state)) - if not is_top(final_state): + final_kast = mlAnd([state.kast for state in final_state]) + print(kevm.pretty_print(final_kast)) + if not is_top(final_kast): raise SystemExit(1) @@ -277,18 +278,16 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: if simplify_init: _LOGGER.info(f'Simplifying initial and target node: {claim.label}') - _new_init, _ = kcfg_explore.cterm_simplify(new_init) - _new_target, _ = kcfg_explore.cterm_simplify(new_target) - if is_bottom(_new_init): + new_init, _ = kcfg_explore.cterm_simplify(new_init) + new_target, _ = kcfg_explore.cterm_simplify(new_target) + if type(new_init) is CTerm.cterm_bottom(): raise ValueError( 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' ) - if is_bottom(_new_target): + if type(new_target) is CTerm.cterm_top(): raise ValueError( 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' ) - new_init = CTerm.from_kast(_new_init) - new_target = CTerm.from_kast(_new_target) kcfg.replace_node(init_node_id, new_init) kcfg.replace_node(target_node_id, new_target) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index e370cf0edc..9098e53965 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -195,14 +195,17 @@ class Sorts: KEVM_CELL: Final = KSort('KevmCell') def short_info(self, cterm: CTerm) -> list[str]: - k_cell = self.pretty_print(cterm.cell('K_CELL')).replace('\n', ' ') - if len(k_cell) > 80: - k_cell = k_cell[0:80] + ' ...' - k_str = f'k: {k_cell}' - ret_strs = [k_str] - for cell, name in [('PC_CELL', 'pc'), ('CALLDEPTH_CELL', 'callDepth'), ('STATUSCODE_CELL', 'statusCode')]: - if cell in cterm.cells: - ret_strs.append(f'{name}: {self.pretty_print(cterm.cell(cell))}') + ret_strs = [] + k_cell = cterm.try_cell('K_CELL') + if k_cell is not None: + pretty_cell = self.pretty_print(k_cell).replace('\n', ' ') + if len(pretty_cell) > 80: + pretty_cell = pretty_cell[0:80] + ' ...' + k_str = f'k: {pretty_cell}' + ret_strs = [k_str] + for cell, name in [('PC_CELL', 'pc'), ('CALLDEPTH_CELL', 'callDepth'), ('STATUSCODE_CELL', 'statusCode')]: + if cell in cterm.cells: + ret_strs.append(f'{name}: {self.pretty_print(cterm.cell(cell))}') return ret_strs @staticmethod @@ -416,7 +419,7 @@ def prove_legacy( max_counterexamples: int | None = None, branching_allowed: int | None = None, haskell_backend_args: Iterable[str] = (), - ) -> KInner: + ) -> list[CTerm]: md_selector = 'k & ! node' args: list[str] = [] haskell_args: list[str] = [] diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 31a34392b2..2c19be7708 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -174,11 +174,8 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i res_lines.append('') res_lines.append(f' Node id: {str(node.id)}') - simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm) - simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm) - - node_cterm = CTerm.from_kast(simplified_node) - target_cterm = CTerm.from_kast(simplified_target) + node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) + target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) res_lines.append(' Failure reason:') _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index aa84d3b984..59e7de00cb 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -791,9 +791,9 @@ def foundry_simplify_node( ) as kcfg_explore: new_term, _ = kcfg_explore.cterm_simplify(cterm) if replace: - apr_proof.kcfg.replace_node(node, CTerm.from_kast(new_term)) + apr_proof.kcfg.replace_node(node, new_term) apr_proof.write_proof_data() - res_term = minimize_term(new_term) if minimize else new_term + res_term = minimize_term(new_term.kast) if minimize else new_term.kast return foundry.kevm.pretty_print(res_term, unalias=False, sort_collections=sort_collections) @@ -808,9 +808,11 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: nodes = list(nodes) if len(nodes) < 2: return True - cell_value = nodes[0].cterm.cell(cell) + cell_value = nodes[0].cterm.try_cell(cell) + if cell_value is None: + return False for node in nodes[1:]: - if cell_value != node.cterm.cell(cell): + if node.cterm.try_cell(cell) is None or cell_value != node.cterm.cell(cell): return False return True @@ -1254,7 +1256,7 @@ def __init__(self, foundry: Foundry, contract_name: str): def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: ret_strs = super().print_node(kcfg, node) - _pc = node.cterm.cell('PC_CELL') + _pc = node.cterm.try_cell('PC_CELL') if type(_pc) is KToken and _pc.sort == INT: srcmap_data = self.foundry.srcmap_data(self.contract_name, int(_pc.token)) if srcmap_data is not None: From 999f8339c95da70b048dc52d4c2b0111f50e05c5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Guyot?= Date: Mon, 28 Aug 2023 06:05:22 +0000 Subject: [PATCH 19/43] handle view-kcfg bottom --- kevm-pyk/src/kevm_pyk/__main__.py | 4 ++-- kevm-pyk/src/kontrol/foundry.py | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 06ec0f9f00..4f0309b335 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -280,11 +280,11 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: _LOGGER.info(f'Simplifying initial and target node: {claim.label}') new_init, _ = kcfg_explore.cterm_simplify(new_init) new_target, _ = kcfg_explore.cterm_simplify(new_target) - if type(new_init) is CTerm.cterm_bottom(): + if type(new_init) is CTerm.bottom(): raise ValueError( 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' ) - if type(new_target) is CTerm.cterm_top(): + if type(new_target) is CTerm.top(): raise ValueError( 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' ) diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index 59e7de00cb..f66bfcc61c 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -215,7 +215,7 @@ def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str] def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]: if type(element) is KCFG.Node: - pc_cell = element.cterm.cell('PC_CELL') + pc_cell = element.cterm.try_cell('PC_CELL') if type(pc_cell) is KToken and pc_cell.sort == INT: return self.solidity_src(contract_name, int(pc_cell.token)) return ['NO DATA'] From 1c0d557d7784ffc3d73ec505e344b8b5cfe85c7d Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 10:53:21 +0300 Subject: [PATCH 20/43] update foundry-list unit test terminal dict name --- .../foundry-list/apr_proofs/AssertTest.setUp()/proof.json | 2 +- .../apr_proofs/AssertTest.testFail_assert_false()/proof.json | 2 +- .../apr_proofs/AssertTest.testFail_assert_true()/proof.json | 2 +- .../apr_proofs/AssertTest.test_assert_false()/proof.json | 2 +- .../apr_proofs/AssertTest.test_assert_true()/proof.json | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json index 95363edf63..a957f62725 100644 --- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json +++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json @@ -1 +1 @@ -{"id": "AssertTest.setUp:c795c796f72d2e6aaa4d26a190f8855a2d9432cb510e944378ac2cf4cafae346", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} \ No newline at end of file +{"id": "AssertTest.setUp:c795c796f72d2e6aaa4d26a190f8855a2d9432cb510e944378ac2cf4cafae346", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false()/proof.json index f79e5c7bb2..7dc3479c4d 100644 --- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false()/proof.json +++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false()/proof.json @@ -1 +1 @@ -{"id": "AssertTest.testFail_assert_false:b5202d1b3fe2344c79708f9a3a2c67d446fb9d70c920a623ad408a2e224215b1", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} \ No newline at end of file +{"id": "AssertTest.testFail_assert_false:b5202d1b3fe2344c79708f9a3a2c67d446fb9d70c920a623ad408a2e224215b1", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true()/proof.json index 40e2fefa58..faaeead7a2 100644 --- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true()/proof.json +++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true()/proof.json @@ -1 +1 @@ -{"id": "AssertTest.testFail_assert_true:242f699b1574032456e9e771ae766945b79d19d3ef23d383a5a46634800e924d", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} \ No newline at end of file +{"id": "AssertTest.testFail_assert_true:242f699b1574032456e9e771ae766945b79d19d3ef23d383a5a46634800e924d", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false()/proof.json index f04a3664c5..b6d6caef50 100644 --- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false()/proof.json +++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false()/proof.json @@ -1 +1 @@ -{"id": "AssertTest.test_assert_false:6cbc877ca7d55dff8601da29b45e21f589afa4bb6200a47e7de1e24a74ee755c", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} \ No newline at end of file +{"id": "AssertTest.test_assert_false:6cbc877ca7d55dff8601da29b45e21f589afa4bb6200a47e7de1e24a74ee755c", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true()/proof.json index 34574cf2e5..f3945dab6d 100644 --- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true()/proof.json +++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true()/proof.json @@ -1 +1 @@ -{"id": "AssertTest.test_assert_true:49ed4957b0e11abe41ead027d5e5e0895d082b39dfa5694297dd0e87741d6a49", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} \ No newline at end of file +{"id": "AssertTest.test_assert_true:49ed4957b0e11abe41ead027d5e5e0895d082b39dfa5694297dd0e87741d6a49", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}} From 159b417aba4746248ef8fa93e33b654069e44935 Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 11:04:19 +0300 Subject: [PATCH 21/43] ignore keep_nodes= --- kevm-pyk/src/kevm_pyk/__main__.py | 7 +++---- kevm-pyk/src/kevm_pyk/kevm.py | 2 ++ kevm-pyk/src/kontrol/foundry.py | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 4f0309b335..e914af1511 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -9,7 +9,6 @@ from pathos.pools import ProcessPool # type: ignore from pyk.cli.utils import file_path -from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken from pyk.kcfg import KCFG from pyk.kore.tools import PrintOutput, kore_print @@ -280,11 +279,11 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: _LOGGER.info(f'Simplifying initial and target node: {claim.label}') new_init, _ = kcfg_explore.cterm_simplify(new_init) new_target, _ = kcfg_explore.cterm_simplify(new_target) - if type(new_init) is CTerm.bottom(): + if new_init.bottom(): raise ValueError( 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' ) - if type(new_target) is CTerm.top(): + if new_target.top(): raise ValueError( 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' ) @@ -373,7 +372,7 @@ def exec_prune_proof( ) apr_proof = APRProof.read_proof_data(save_directory, claim.label) - node_ids = apr_proof.prune(node, keep_nodes=[apr_proof.init, apr_proof.target]) + node_ids = apr_proof.prune(node) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 9098e53965..f15c53a629 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -206,6 +206,8 @@ def short_info(self, cterm: CTerm) -> list[str]: for cell, name in [('PC_CELL', 'pc'), ('CALLDEPTH_CELL', 'callDepth'), ('STATUSCODE_CELL', 'statusCode')]: if cell in cterm.cells: ret_strs.append(f'{name}: {self.pretty_print(cterm.cell(cell))}') + else: + ret_strs = ['(empty configuration)'] return ret_strs @staticmethod diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index f66bfcc61c..552fa4e389 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -759,7 +759,7 @@ def foundry_list(foundry_root: Path) -> list[str]: def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike) -> None: foundry = Foundry(foundry_root) apr_proof = foundry.get_apr_proof(test) - node_ids = apr_proof.prune(node, keep_nodes=[apr_proof.init, apr_proof.target]) + node_ids = apr_proof.prune(node) _LOGGER.info(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() From 438b2e43ff1eeae51a84780be8ecfef8ecd4310c Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 13:55:22 +0300 Subject: [PATCH 22/43] lock svm --- .github/workflows/Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 4d25d77427..4d8461128b 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -56,6 +56,6 @@ ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PAT RUN curl -sSL https://install.python-poetry.org | python3 - \ && poetry --version -RUN cargo install svm-rs --version 0.3.0 \ - && svm install 0.8.13 \ +RUN cargo install svm-rs --version 0.3.0 --locked \ + && svm install 0.8.13 \ && solc --version From b1aeded7d3978c198e04c7244316f4eb56a4883a Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 11:24:18 +0000 Subject: [PATCH 23/43] Set Version: 1.0.281 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 6c5514aa57..90ea990cb4 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.280" +version = "1.0.281" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index f416f538a6..91dab77f5e 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.280) unstable; urgency=medium +kevm (1.0.281) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 4418310f44..fbd4dd66f5 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.280 +1.0.281 From 179a05a44c55e4979e1e1b76de85629671141386 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 11:27:27 +0000 Subject: [PATCH 24/43] kevm-pyk/: sync poetry files pyk version v0.1.429 --- kevm-pyk/poetry.lock | 63 +------------------------------------------- 1 file changed, 1 insertion(+), 62 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index b7bfe3a028..f920a189a3 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -1,10 +1,9 @@ -# This file is automatically @generated by Poetry 1.4.2 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. [[package]] name = "attrs" version = "23.1.0" description = "Classes Without Boilerplate" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -23,7 +22,6 @@ tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pyte name = "autoflake" version = "2.2.0" description = "Removes unused imports and unused variables" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -39,7 +37,6 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} name = "black" version = "23.7.0" description = "The uncompromising code formatter." -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -85,7 +82,6 @@ uvloop = ["uvloop (>=0.15.2)"] name = "classify-imports" version = "4.2.0" description = "Utilities for refactoring imports in python-like syntax." -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -97,7 +93,6 @@ files = [ name = "click" version = "8.1.7" description = "Composable command line interface toolkit" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -112,7 +107,6 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""} name = "cmd2" version = "2.4.3" description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python" -category = "main" optional = false python-versions = ">=3.6" files = [ @@ -135,7 +129,6 @@ validate = ["flake8", "mypy", "types-pkg-resources"] name = "colorama" version = "0.4.6" description = "Cross-platform colored terminal text." -category = "dev" optional = false python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,!=3.3.*,!=3.4.*,!=3.5.*,!=3.6.*,>=2.7" files = [ @@ -147,7 +140,6 @@ files = [ name = "coloredlogs" version = "15.0.1" description = "Colored terminal output for Python's logging module" -category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" files = [ @@ -165,7 +157,6 @@ cron = ["capturer (>=2.4)"] name = "coverage" version = "7.3.0" description = "Code coverage measurement for Python" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -233,7 +224,6 @@ toml = ["tomli"] name = "dill" version = "0.3.7" description = "serialize all of Python" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -248,7 +238,6 @@ graph = ["objgraph (>=1.7.2)"] name = "exceptiongroup" version = "1.1.3" description = "Backport of PEP 654 (exception groups)" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -263,7 +252,6 @@ test = ["pytest (>=6)"] name = "execnet" version = "2.0.2" description = "execnet: rapid multi-Python deployment" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -278,7 +266,6 @@ testing = ["hatch", "pre-commit", "pytest", "tox"] name = "filelock" version = "3.12.2" description = "A platform independent file lock." -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -294,7 +281,6 @@ testing = ["covdefaults (>=2.3)", "coverage (>=7.2.7)", "diff-cover (>=7.5)", "p name = "flake8" version = "6.1.0" description = "the modular source code checker: pep8 pyflakes and co" -category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -311,7 +297,6 @@ pyflakes = ">=3.1.0,<3.2.0" name = "flake8-bugbear" version = "23.7.10" description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle." -category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -330,7 +315,6 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest", name = "flake8-comprehensions" version = "3.14.0" description = "A flake8 plugin to help you write better list/set/dict comprehensions." -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -345,7 +329,6 @@ flake8 = ">=3.0,<3.2.0 || >3.2.0" name = "flake8-quotes" version = "3.3.2" description = "Flake8 lint for quotes." -category = "dev" optional = false python-versions = "*" files = [ @@ -359,7 +342,6 @@ flake8 = "*" name = "flake8-type-checking" version = "2.4.1" description = "A flake8 plugin for managing type-checking imports & forward references" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -375,7 +357,6 @@ flake8 = "*" name = "graphviz" version = "0.20.1" description = "Simple Python interface for Graphviz" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -392,7 +373,6 @@ test = ["coverage", "mock (>=4)", "pytest (>=7)", "pytest-cov", "pytest-mock (>= name = "humanfriendly" version = "10.0" description = "Human friendly output for text interfaces using Python" -category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*" files = [ @@ -407,7 +387,6 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve name = "importlib-metadata" version = "6.8.0" description = "Read metadata from Python packages" -category = "main" optional = false python-versions = ">=3.8" files = [ @@ -427,7 +406,6 @@ testing = ["flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs name = "iniconfig" version = "2.0.0" description = "brain-dead simple config-ini parsing" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -439,7 +417,6 @@ files = [ name = "isort" version = "5.12.0" description = "A Python utility / library to sort Python imports." -category = "dev" optional = false python-versions = ">=3.8.0" files = [ @@ -457,7 +434,6 @@ requirements-deprecated-finder = ["pip-api", "pipreqs"] name = "linkify-it-py" version = "2.0.2" description = "Links recognition library with FULL unicode support." -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -478,7 +454,6 @@ test = ["coverage", "pytest", "pytest-cov"] name = "markdown-it-py" version = "2.2.0" description = "Python port of markdown-it. Markdown parsing, done right!" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -505,7 +480,6 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] name = "mccabe" version = "0.7.0" description = "McCabe checker, plugin for flake8" -category = "dev" optional = false python-versions = ">=3.6" files = [ @@ -517,7 +491,6 @@ files = [ name = "mdit-py-plugins" version = "0.4.0" description = "Collection of plugins for markdown-it-py" -category = "main" optional = false python-versions = ">=3.8" files = [ @@ -537,7 +510,6 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"] name = "mdurl" version = "0.1.2" description = "Markdown URL utilities" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -549,7 +521,6 @@ files = [ name = "multiprocess" version = "0.70.15" description = "better multiprocessing and multithreading in Python" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -578,7 +549,6 @@ dill = ">=0.3.7" name = "mypy" version = "1.5.1" description = "Optional static typing for Python" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -625,7 +595,6 @@ reports = ["lxml"] name = "mypy-extensions" version = "1.0.0" description = "Type system extensions for programs checked with the mypy type checker." -category = "dev" optional = false python-versions = ">=3.5" files = [ @@ -637,7 +606,6 @@ files = [ name = "packaging" version = "23.1" description = "Core utilities for Python packages" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -649,7 +617,6 @@ files = [ name = "pathos" version = "0.3.1" description = "parallel graph management and execution in heterogeneous computing" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -667,7 +634,6 @@ ppft = ">=1.7.6.7" name = "pathspec" version = "0.11.2" description = "Utility library for gitignore style pattern matching of file paths." -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -679,7 +645,6 @@ files = [ name = "pep8-naming" version = "0.13.3" description = "Check PEP-8 naming conventions, plugin for flake8" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -694,7 +659,6 @@ flake8 = ">=5.0.0" name = "platformdirs" version = "3.10.0" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a \"user data dir\"." -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -710,7 +674,6 @@ test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4)", "pytest-co name = "pluggy" version = "1.3.0" description = "plugin and hook calling mechanisms for python" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -726,7 +689,6 @@ testing = ["pytest", "pytest-benchmark"] name = "pox" version = "0.3.3" description = "utilities for filesystem exploration and automated builds" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -738,7 +700,6 @@ files = [ name = "ppft" version = "1.7.6.7" description = "distributed and parallel Python" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -753,7 +714,6 @@ dill = ["dill (>=0.3.7)"] name = "psutil" version = "5.9.5" description = "Cross-platform lib for process and system monitoring in Python." -category = "main" optional = false python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" files = [ @@ -780,7 +740,6 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"] name = "pybind11" version = "2.11.1" description = "Seamless operability between C++11 and Python" -category = "main" optional = false python-versions = ">=3.6" files = [ @@ -795,7 +754,6 @@ global = ["pybind11-global (==2.11.1)"] name = "pycodestyle" version = "2.11.0" description = "Python style guide checker" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -807,7 +765,6 @@ files = [ name = "pyflakes" version = "3.1.0" description = "passive checker of Python programs" -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -819,7 +776,6 @@ files = [ name = "pygments" version = "2.16.1" description = "Pygments is a syntax highlighting package written in Python." -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -834,7 +790,6 @@ plugins = ["importlib-metadata"] name = "pyk" version = "0.1.429" description = "" -category = "main" optional = false python-versions = "^3.10" files = [] @@ -860,7 +815,6 @@ resolved_reference = "8a27ac0637840bbee4d81e5df37cec5a2d8248d0" name = "pyperclip" version = "1.8.2" description = "A cross-platform clipboard module for Python. (Only handles plain text for now.)" -category = "main" optional = false python-versions = "*" files = [ @@ -871,7 +825,6 @@ files = [ name = "pyreadline3" version = "3.4.1" description = "A python implementation of GNU readline." -category = "main" optional = false python-versions = "*" files = [ @@ -883,7 +836,6 @@ files = [ name = "pytest" version = "7.4.0" description = "pytest: simple powerful testing with Python" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -906,7 +858,6 @@ testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "no name = "pytest-cov" version = "4.1.0" description = "Pytest plugin for measuring coverage." -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -925,7 +876,6 @@ testing = ["fields", "hunter", "process-tests", "pytest-xdist", "six", "virtuale name = "pytest-mock" version = "3.11.1" description = "Thin-wrapper around the mock package for easier use with pytest" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -943,7 +893,6 @@ dev = ["pre-commit", "pytest-asyncio", "tox"] name = "pytest-xdist" version = "3.3.1" description = "pytest xdist plugin for distributed testing, most importantly across multiple CPUs" -category = "dev" optional = false python-versions = ">=3.7" files = [ @@ -964,7 +913,6 @@ testing = ["filelock"] name = "pyupgrade" version = "3.10.1" description = "A tool to automatically upgrade syntax for newer versions." -category = "dev" optional = false python-versions = ">=3.8.1" files = [ @@ -979,7 +927,6 @@ tokenize-rt = ">=5.2.0" name = "rich" version = "13.5.2" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" -category = "main" optional = false python-versions = ">=3.7.0" files = [ @@ -998,7 +945,6 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] name = "textual" version = "0.27.0" description = "Modern Text User Interface framework" -category = "main" optional = false python-versions = ">=3.7,<4.0" files = [ @@ -1019,7 +965,6 @@ dev = ["aiohttp (>=3.8.1)", "click (>=8.1.2)", "msgpack (>=1.0.3)"] name = "tokenize-rt" version = "5.2.0" description = "A wrapper around the stdlib `tokenize` which roundtrips." -category = "dev" optional = false python-versions = ">=3.8" files = [ @@ -1031,7 +976,6 @@ files = [ name = "tomli" version = "2.0.1" description = "A lil' TOML parser" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1043,7 +987,6 @@ files = [ name = "tomlkit" version = "0.11.8" description = "Style preserving TOML library" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1055,7 +998,6 @@ files = [ name = "typing-extensions" version = "4.7.1" description = "Backported and Experimental Type Hints for Python 3.7+" -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1067,7 +1009,6 @@ files = [ name = "uc-micro-py" version = "1.0.2" description = "Micro subset of unicode data files for linkify-it-py projects." -category = "main" optional = false python-versions = ">=3.7" files = [ @@ -1082,7 +1023,6 @@ test = ["coverage", "pytest", "pytest-cov"] name = "wcwidth" version = "0.2.6" description = "Measures the displayed width of unicode strings in a terminal" -category = "main" optional = false python-versions = "*" files = [ @@ -1094,7 +1034,6 @@ files = [ name = "zipp" version = "3.16.2" description = "Backport of pathlib-compatible object wrapper for zip files" -category = "main" optional = false python-versions = ">=3.8" files = [ From c9a5caa03f6928fb37f532f7fc10b24b2cc2c0ea Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 15:13:39 +0000 Subject: [PATCH 25/43] deps/pyk_release: Set Version v0.1.430 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index 7ef627e7b5..851dc3e8ce 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.429 +v0.1.430 From 24e38b9692dd1d3b086a4b7a4adc64b64c998bda Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 15:14:05 +0000 Subject: [PATCH 26/43] Set Version: 1.0.282 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 90ea990cb4..a91c719541 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.281" +version = "1.0.282" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 91dab77f5e..6af877d97e 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.281) unstable; urgency=medium +kevm (1.0.282) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index fbd4dd66f5..e8b71fede6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.281 +1.0.282 From 51338d51a1310191b6f01a663c0cc350a42ccf1a Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 15:16:29 +0000 Subject: [PATCH 27/43] kevm-pyk/: sync poetry files pyk version v0.1.430 --- kevm-pyk/poetry.lock | 8 ++++---- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index f920a189a3..904908f54e 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -788,7 +788,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.429" +version = "0.1.430" description = "" optional = false python-versions = "^3.10" @@ -808,8 +808,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.429" -resolved_reference = "8a27ac0637840bbee4d81e5df37cec5a2d8248d0" +reference = "v0.1.430" +resolved_reference = "32409fc88cdf5d1f12cf664d145191f0964e065d" [[package]] name = "pyperclip" @@ -1048,4 +1048,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "5529c3175099002ee5b74e296fd5127f6012f5cce021fb0f577b748d081684a4" +content-hash = "cdc50fd20f196570db977f97112a0c6c37edbdbddb608d2a964a3c7cb8f569e2" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index a91c719541..25b10567c1 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.429" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.430" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From 91dd8130dd9f82ae491ba820f29a6a3d6982bdb3 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 15:23:46 +0000 Subject: [PATCH 28/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index 8c6036ea7c..ae43635e68 100644 --- a/flake.lock +++ b/flake.lock @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1693177411, - "narHash": "sha256-d6AOxbJVbzkMaA0ySvsq3I2I54cMaerTCwtmRhKnshQ=", + "lastModified": 1693235058, + "narHash": "sha256-VCZ/2EvrNpOS3nqsVJOWa+UtYqeCKZQuDGGKlIE0pEY=", "owner": "runtimeverification", "repo": "pyk", - "rev": "8a27ac0637840bbee4d81e5df37cec5a2d8248d0", + "rev": "32409fc88cdf5d1f12cf664d145191f0964e065d", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.429", + "ref": "v0.1.430", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index dcc5300b48..0705d1bad4 100644 --- a/flake.nix +++ b/flake.nix @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.429"; + pyk.url = "github:runtimeverification/pyk/v0.1.430"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From eba3483341732e551b3daeafb4faa13d437a5ec1 Mon Sep 17 00:00:00 2001 From: franfran Date: Mon, 28 Aug 2023 19:32:53 +0300 Subject: [PATCH 29/43] remove useless initialization --- kevm-pyk/src/kevm_pyk/kevm.py | 1 - 1 file changed, 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index f15c53a629..e806c4ed64 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -195,7 +195,6 @@ class Sorts: KEVM_CELL: Final = KSort('KevmCell') def short_info(self, cterm: CTerm) -> list[str]: - ret_strs = [] k_cell = cterm.try_cell('K_CELL') if k_cell is not None: pretty_cell = self.pretty_print(k_cell).replace('\n', ' ') From a26b3f0b04460baa1d59a65a5dafbc071c359b63 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 16:33:32 +0000 Subject: [PATCH 30/43] Set Version: 1.0.283 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 25b10567c1..08d3adfd55 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.282" +version = "1.0.283" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 6af877d97e..7861b00eef 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.282) unstable; urgency=medium +kevm (1.0.283) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e8b71fede6..2cde13a4c1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.282 +1.0.283 From 35ec5f1e32aa57e8d942b61aaa4370ddab1ad738 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 28 Aug 2023 16:36:10 +0000 Subject: [PATCH 31/43] kevm-pyk/: sync poetry files pyk version v0.1.430 --- kevm-pyk/poetry.lock | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 904908f54e..5b02774ef1 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -264,18 +264,21 @@ testing = ["hatch", "pre-commit", "pytest", "tox"] [[package]] name = "filelock" -version = "3.12.2" +version = "3.12.3" description = "A platform independent file lock." optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "filelock-3.12.2-py3-none-any.whl", hash = "sha256:cbb791cdea2a72f23da6ac5b5269ab0a0d161e9ef0100e653b69049a7706d1ec"}, - {file = "filelock-3.12.2.tar.gz", hash = "sha256:002740518d8aa59a26b0c76e10fb8c6e15eae825d34b6fdf670333fd7b938d81"}, + {file = "filelock-3.12.3-py3-none-any.whl", hash = "sha256:f067e40ccc40f2b48395a80fcbd4728262fab54e232e090a4063ab804179efeb"}, + {file = "filelock-3.12.3.tar.gz", hash = "sha256:0ecc1dd2ec4672a10c8550a8182f1bd0c0a5088470ecd5a125e45f49472fac3d"}, ] +[package.dependencies] +typing-extensions = {version = ">=4.7.1", markers = "python_version < \"3.11\""} + [package.extras] -docs = ["furo (>=2023.5.20)", "sphinx (>=7.0.1)", "sphinx-autodoc-typehints (>=1.23,!=1.23.4)"] -testing = ["covdefaults (>=2.3)", "coverage (>=7.2.7)", "diff-cover (>=7.5)", "pytest (>=7.3.1)", "pytest-cov (>=4.1)", "pytest-mock (>=3.10)", "pytest-timeout (>=2.1)"] +docs = ["furo (>=2023.7.26)", "sphinx (>=7.1.2)", "sphinx-autodoc-typehints (>=1.24)"] +testing = ["covdefaults (>=2.3)", "coverage (>=7.3)", "diff-cover (>=7.7)", "pytest (>=7.4)", "pytest-cov (>=4.1)", "pytest-mock (>=3.11.1)", "pytest-timeout (>=2.1)"] [[package]] name = "flake8" From aa5a313e3c8fa71f4af2e56b4ab831fcd7081f22 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 29 Aug 2023 17:35:08 +0000 Subject: [PATCH 32/43] deps/pyk_release: Set Version v0.1.431 --- deps/pyk_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/pyk_release b/deps/pyk_release index 851dc3e8ce..1a64f848ce 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.430 +v0.1.431 From 9d1e099606e45e246682f2c4fd799c1d5ad0d43e Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 29 Aug 2023 17:38:10 +0000 Subject: [PATCH 33/43] kevm-pyk/: sync poetry files pyk version v0.1.431 --- kevm-pyk/poetry.lock | 8 ++++---- kevm-pyk/pyproject.toml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 5b02774ef1..3d8857bf0c 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -791,7 +791,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.430" +version = "0.1.431" description = "" optional = false python-versions = "^3.10" @@ -811,8 +811,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.430" -resolved_reference = "32409fc88cdf5d1f12cf664d145191f0964e065d" +reference = "v0.1.431" +resolved_reference = "a18d76df9419194acf1f9d159d8fa697e0471bd9" [[package]] name = "pyperclip" @@ -1051,4 +1051,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "cdc50fd20f196570db977f97112a0c6c37edbdbddb608d2a964a3c7cb8f569e2" +content-hash = "52c02013a3aa448f371fadb4d9e4c27249a355e1591b7257fe9af57e44e0a524" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 08d3adfd55..8de27ea334 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.430" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.431" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From f777d0cccdf66e4c385196bd385f1e5162332b22 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 29 Aug 2023 17:40:58 +0000 Subject: [PATCH 34/43] flake.{nix,lock}: update Nix derivations --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index ae43635e68..d1002dc07a 100644 --- a/flake.lock +++ b/flake.lock @@ -1735,16 +1735,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1693235058, - "narHash": "sha256-VCZ/2EvrNpOS3nqsVJOWa+UtYqeCKZQuDGGKlIE0pEY=", + "lastModified": 1693330087, + "narHash": "sha256-gHc4wrk0nw070fYlJoup5scKM3Wx0I5NFp5RHi0T820=", "owner": "runtimeverification", "repo": "pyk", - "rev": "32409fc88cdf5d1f12cf664d145191f0964e065d", + "rev": "a18d76df9419194acf1f9d159d8fa697e0471bd9", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.430", + "ref": "v0.1.431", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index 0705d1bad4..f18aea326c 100644 --- a/flake.nix +++ b/flake.nix @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.430"; + pyk.url = "github:runtimeverification/pyk/v0.1.431"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases From 5d4735480ed76b2127c2488c862b2076fe5480af Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 30 Aug 2023 20:19:47 +0000 Subject: [PATCH 35/43] Set Version: 1.0.284 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8de27ea334..8668ad0d3a 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.283" +version = "1.0.284" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 7861b00eef..3459376d46 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.283) unstable; urgency=medium +kevm (1.0.284) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 2cde13a4c1..e9034ea560 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.283 +1.0.284 From 1f47292f7c712b65975bb738e5982c0aca3dae7b Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 30 Aug 2023 19:12:02 -0500 Subject: [PATCH 36/43] Fix bottom/top check --- kevm-pyk/src/kevm_pyk/__main__.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index e914af1511..6e62c906e5 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -9,6 +9,7 @@ from pathos.pools import ProcessPool # type: ignore from pyk.cli.utils import file_path +from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken from pyk.kcfg import KCFG from pyk.kore.tools import PrintOutput, kore_print @@ -279,11 +280,11 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: _LOGGER.info(f'Simplifying initial and target node: {claim.label}') new_init, _ = kcfg_explore.cterm_simplify(new_init) new_target, _ = kcfg_explore.cterm_simplify(new_target) - if new_init.bottom(): + if CTerm._is_bottom(new_init.kast): raise ValueError( 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' ) - if new_target.top(): + if CTerm._is_top(new_target.kast): raise ValueError( 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' ) From 0aa51ef5d83d6bc4578f9f230bacba8e862e57d4 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 30 Aug 2023 21:08:55 -0500 Subject: [PATCH 37/43] Update expected output for test_foundry_auto_abstraction --- .../test-data/gas-abstraction.expected | 45 ++++++++++++------- .../tests/integration/test_foundry_prove.py | 1 + 2 files changed, 30 insertions(+), 16 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected index 53f9095a0d..aef9b60a97 100644 --- a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected +++ b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected @@ -1,9 +1,9 @@ ┌─ 1 (root, init) -│ k: #execute ~> CONTINUATION:K +│ k: #execute ~> CONTINUATION │ pc: 0 │ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode +│ statusCode: STATUSCODE │ │ (511 steps) ├─ 3 @@ -92,10 +92,10 @@ ┌─ 2 (root, leaf, target) -│ k: #halt ~> CONTINUATION:K -│ pc: PC_CELL_5d410f2a:Int -│ callDepth: CALLDEPTH_CELL_5d410f2a:Int -│ statusCode: STATUSCODE_FINAL:StatusCode +│ k: #halt ~> CONTINUATION +│ pc: PC_CELL_5d410f2a +│ callDepth: CALLDEPTH_CELL_5d410f2a +│ statusCode: STATUSCODE_FINAL Node 8: @@ -407,10 +407,11 @@ Node 8: rule [BASIC-BLOCK-1-TO-3]: - ( .K => CALL 9223372036854772946 645326474426547203313410069153905908525362434349 0 128 4 128 0 - ~> #pc [ CALL ] ) + ( #execute + ~> CONTINUATION => CALL 9223372036854772946 645326474426547203313410069153905908525362434349 0 128 4 128 0 + ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> CONTINUATION:K ) NORMAL @@ -433,10 +434,10 @@ Node 8: 728815563385977040452943777879061427756277306518 - CALLER_ID:Int + CALLER_ID - b"c\xfe\xc36" + ( S2KGasTest . S2KtestInfiniteGas ( ) => b"c\xfe\xc36" ) 0 @@ -445,7 +446,7 @@ Node 8: ( .WordStack => ( 132 : ( selector ( "infiniteGas()" ) : ( 645326474426547203313410069153905908525362434349 : ( 167 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) - ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + ( .Bytes => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) ... ... @@ -475,11 +476,11 @@ Node 8: ... - ORIGIN_ID:Int + ORIGIN_ID - NUMBER_CELL:Int + NUMBER_CELL ... @@ -568,7 +569,7 @@ Node 8: 0 - b"" + ( .Bytes => b"" ) .OpcodeType @@ -599,7 +600,19 @@ Node 8: - requires ( 0 <=Int CALLER_ID:Int + requires ( 0 <=Int CALLER_ID + andBool ( CALLER_ID Date: Wed, 30 Aug 2023 21:50:30 -0500 Subject: [PATCH 38/43] Fix test_legacy_prove to handle kevm.prove returning a list of final terms --- kevm-pyk/src/tests/integration/test_prove.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 34e28c5e6a..938faf8cd9 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -6,6 +6,7 @@ import pytest from pyk.prelude.ml import mlTop +from pyk.cterm import CTerm from kevm_pyk import config from kevm_pyk.__main__ import exec_prove @@ -300,5 +301,7 @@ def test_legacy_prove( finally: log_file.write_text(caplog.text) + assert len(actual) == 1 + # Then - assert actual == mlTop('K') + assert CTerm._is_top(actual[0].kast) From 29a763d4423b0801ca3488942d500182738d3881 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 31 Aug 2023 06:54:27 +0000 Subject: [PATCH 39/43] Set Version: 1.0.285 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8668ad0d3a..1ff05c2d4e 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.284" +version = "1.0.285" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 4c841274ad..38a60b153d 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.284) unstable; urgency=medium +kevm (1.0.285) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e9034ea560..cff7ecca0a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.284 +1.0.285 From 060e192f7d44783e0ec97a706695321ab7755b1f Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 31 Aug 2023 11:14:08 -0500 Subject: [PATCH 40/43] Re-add simplify_init argument to test_foundry_auto_abstraction --- kevm-pyk/src/tests/integration/test_foundry_prove.py | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index ec2a9885c3..bc3cfd348b 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py @@ -257,6 +257,7 @@ def test_foundry_auto_abstraction( tests=[(test_id, None)], auto_abstract_gas=True, port=server.port, + simplify_init=False, ) if use_booster: @@ -278,7 +279,7 @@ def test_foundry_auto_abstraction( assert_or_update_show_output(show_res, TEST_DATA_DIR / 'gas-abstraction.expected', update=update_expected_output) -def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) -> None: +def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool, server: KoreServer) -> None: test = 'AssertTest.test_assert_true()' foundry = Foundry(foundry_root) @@ -286,8 +287,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) - prove_res = foundry_prove( foundry_root, tests=[(test, None)], - smt_timeout=300, - smt_retry_limit=10, + port=server.port, ) assert_pass(test, prove_res) @@ -304,8 +304,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) - prove_res = foundry_prove( foundry_root, tests=[(test, None)], - smt_timeout=300, - smt_retry_limit=10, + port=server.port, ) assert_pass(test, prove_res) From 9446a887c657bf68a9077f216aa375f23873cfa5 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Thu, 31 Aug 2023 13:31:20 -0500 Subject: [PATCH 41/43] Update kevm-pyk/src/tests/integration/test_prove.py --- kevm-pyk/src/tests/integration/test_prove.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 2f260170de..46b34f3ed5 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -300,7 +300,6 @@ def test_legacy_prove( finally: log_file.write_text(caplog.text) - assert len(actual) == 1 - # Then + assert len(actual) == 1 assert CTerm._is_top(actual[0].kast) From 81b78b04602f6c30f797e7311674c2f0e5c9c5d4 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Thu, 31 Aug 2023 14:13:22 -0500 Subject: [PATCH 42/43] Update kevm-pyk/src/kevm_pyk/__main__.py --- kevm-pyk/src/kevm_pyk/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 6e62c906e5..52f7382d0f 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -164,7 +164,7 @@ def exec_prove_legacy( branching_allowed=branching_allowed, haskell_backend_args=haskell_backend_args, ) - final_kast = mlAnd([state.kast for state in final_state]) + final_kast = mlOr([state.kast for state in final_state]) print(kevm.pretty_print(final_kast)) if not is_top(final_kast): raise SystemExit(1) From e0ae3a013bde29137edb39b094f09305f11af052 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 31 Aug 2023 14:14:07 -0500 Subject: [PATCH 43/43] Fix import --- kevm-pyk/src/kevm_pyk/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 52f7382d0f..35e20011e4 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -15,7 +15,7 @@ from pyk.kore.tools import PrintOutput, kore_print from pyk.ktool.kompile import LLVMKompileType from pyk.ktool.krun import KRunOutput -from pyk.prelude.ml import is_top, mlAnd +from pyk.prelude.ml import is_top, mlOr from pyk.proof import APRProof from pyk.proof.equality import EqualityProof from pyk.proof.show import APRProofShow