From 23b3ff1dc6e60b845566447a9a0e3ef516fea940 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 27 Feb 2024 08:46:00 -0700 Subject: [PATCH] Update dependency: deps/pyk_release (#326) * deps/pyk_release: Set Version v0.1.620 * Set Version: 0.2.27 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.621 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.622 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.623 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.624 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.625 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.626 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.627 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.628 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.27 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.629 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.630 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.631 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.632 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.633 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.30 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.634 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.635 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.31 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.636 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.33 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.637 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.35 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.638 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.639 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.640 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.641 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.642 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.643 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.37 * flake.{nix,lock}: update Nix derivations * Change EqualityProver to ImpliesProver * Moved arguments for `advance_proof` to `APRProver` * deps/pyk_release: Set Version v0.1.644 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.2.38 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.645 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.646 * Set Version: 0.2.28 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.647 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.648 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.3.3 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.649 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.3.4 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.650 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * deps/k_release: sync release file version 6.3.5 * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.651 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.653 * Set Version: 0.2.29 * deps/pyk_release: Set Version v0.1.654 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * deps/pyk_release: Set Version v0.1.655 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations * kmir.py/: adjustments for new CTermSymbolic/KCFGExplore interface * sum-to-n.run.out: update expected output * deps/pyk_release: Set Version v0.1.656 * kmir/{pyproject.toml,poetry.lock}: sync Poetry files * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops Co-authored-by: dkcumming Co-authored-by: Everett Hildenbrandt --- deps/k_release | 2 +- deps/pyk_release | 2 +- flake.lock | 148 +++++++++++++++++++++------- flake.nix | 4 +- kmir/poetry.lock | 100 +++++++++++-------- kmir/pyproject.toml | 4 +- kmir/src/kmir/__init__.py | 2 +- kmir/src/kmir/kmir.py | 30 +++--- kmir/src/tests/nix/sum-to-n.run.out | 2 +- package/version | 2 +- 10 files changed, 193 insertions(+), 103 deletions(-) diff --git a/deps/k_release b/deps/k_release index 42cc526d6..b98d1d3fa 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.2.4 +6.3.5 diff --git a/deps/pyk_release b/deps/pyk_release index 6e0233d00..26010ce5f 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.619 +v0.1.656 diff --git a/flake.lock b/flake.lock index bb7d60b26..c307308a2 100644 --- a/flake.lock +++ b/flake.lock @@ -18,17 +18,33 @@ ] }, "locked": { - "lastModified": 1706622743, - "narHash": "sha256-hdgFFYz2NorC9mIU8arNyN2H/fOJ50bDW7ptMjsliYk=", + "lastModified": 1708422161, + "narHash": "sha256-0iGpmXEdDE0lK66slTyYlbylE4eVOM6nIEM9ffhWYsw=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "0ef6ecd37e193a736ddc1d9dc047c24646c4a324", + "rev": "54a1eb9c4278460b69b19d72280db54108f2d467", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "0ef6ecd37e193a736ddc1d9dc047c24646c4a324", + "rev": "54a1eb9c4278460b69b19d72280db54108f2d467", + "type": "github" + } + }, + "flake-compat": { + "flake": false, + "locked": { + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", + "owner": "edolstra", + "repo": "flake-compat", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", + "type": "github" + }, + "original": { + "owner": "edolstra", + "repo": "flake-compat", "type": "github" } }, @@ -92,34 +108,34 @@ "z3": "z3" }, "locked": { - "lastModified": 1706261911, - "narHash": "sha256-ntTfZAkMT/F8iw2A4sC03oCR5Gt1ijqXHAIjDcQ3xhE=", + "lastModified": 1708380172, + "narHash": "sha256-rIKNZKY+a2XX2MnUlMGeKT7kcsiX4BgoQoAQHqXk85w=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "3779155b609ae78c928d7b47c541b9b6ca969181", + "rev": "ac6908d0ca26f194802c72f66f200e7079139f1b", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "3779155b609ae78c928d7b47c541b9b6ca969181", + "rev": "ac6908d0ca26f194802c72f66f200e7079139f1b", "type": "github" } }, "immer-src": { "flake": false, "locked": { - "lastModified": 1634324349, - "narHash": "sha256-1OicqmyM3Rcrs/jkRMip2pXITQnVDRrHbQbEpZZ4nnU=", + "lastModified": 1708038459, + "narHash": "sha256-aV/mQFuPzioy1PxROc85ypeP7/d0nn+xcBPzy9taw2s=", "owner": "runtimeverification", "repo": "immer", - "rev": "198c2ae260d49ef1800a2fe4433e07d7dec20059", + "rev": "4b0914f0b2acb33befe0ba4cd3a7954f2687e9bb", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "immer", - "rev": "198c2ae260d49ef1800a2fe4433e07d7dec20059", + "rev": "4b0914f0b2acb33befe0ba4cd3a7954f2687e9bb", "type": "github" } }, @@ -131,49 +147,52 @@ "llvm-backend": "llvm-backend", "nixpkgs": [ "k-framework", - "haskell-backend", + "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils" + "rv-utils": "rv-utils_2" }, "locked": { - "lastModified": 1707088968, - "narHash": "sha256-12EhD5jFFzBu3/6CvcpprGsSvGC7AbeMGOYpaKfKs5g=", + "lastModified": 1708691408, + "narHash": "sha256-LsY4LjQZD0IpTSHmCcPJvHQdULR6mteQCgkcqPXzMPk=", "owner": "runtimeverification", "repo": "k", - "rev": "65e11e3a04feee8238654e2d6583abf9c8b04bc8", + "rev": "457642e3f660265157573771cb5ee46d7662642b", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.2.4", + "ref": "v6.3.5", "repo": "k", "type": "github" } }, "llvm-backend": { "inputs": { + "flake-compat": "flake-compat", "fmt-src": "fmt-src", "immer-src": "immer-src", "mavenix": "mavenix", "nixpkgs": [ "k-framework", - "haskell-backend", + "llvm-backend", + "rv-utils", "nixpkgs" ], "pybind11-src": "pybind11-src", "rapidjson-src": "rapidjson-src", + "rv-utils": "rv-utils", "utils": [ "k-framework", "flake-utils" ] }, "locked": { - "lastModified": 1706906990, - "narHash": "sha256-XcKR4HVjds9LX75gzXpuXUOCFVs7ivN89++w0pqeGaU=", + "lastModified": 1708687355, + "narHash": "sha256-+hxlSYI5NGNg1yS7wzdqnPRWwt+K4Gl5rDEwA7Rn9Ss=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "01dd3699f084bbc8f7e1bbff3412735f7d2ca366", + "rev": "411cfc5ffc51a48422a021cb1a70d9353be2ffc5", "type": "github" }, "original": { @@ -188,15 +207,15 @@ "utils": "utils" }, "locked": { - "lastModified": 1643802645, - "narHash": "sha256-BynM25iwp/l3FyrcHqiNJdDxvN6IxSM3/zkFR6PD3B0=", - "owner": "nix-community", + "lastModified": 1689018333, + "narHash": "sha256-sthxx50rj0E7gv38oeMj8GZOp7i1776P1qZsM7pVLd0=", + "owner": "goodlyrottenapple", "repo": "mavenix", - "rev": "ce9ddfd7f361190e8e8dcfaf6b8282eebbb3c7cb", + "rev": "153d69e62f87e5dd37d35492cc3e35dd80d2b5fa", "type": "github" }, "original": { - "owner": "nix-community", + "owner": "goodlyrottenapple", "repo": "mavenix", "type": "github" } @@ -225,11 +244,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1696983906, - "narHash": "sha256-L7GyeErguS7Pg4h8nK0wGlcUTbfUMDu+HMf1UcyP72k=", + "lastModified": 1704290814, + "narHash": "sha256-LWvKHp7kGxk/GEtlrGYV68qIvPHkU9iToomNFGagixU=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "bd1cde45c77891214131cbbea5b1203e485a9d51", + "rev": "70bdadeb94ffc8806c0570eb5c2695ad29f0e421", "type": "github" }, "original": { @@ -253,6 +272,38 @@ } }, "nixpkgs_3": { + "locked": { + "lastModified": 1707163378, + "narHash": "sha256-oz+BzUDwtyircjjxv9aPYOS5gobxLCjD2il+gb/bCRo=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + } + }, + "nixpkgs_4": { + "locked": { + "lastModified": 1707163378, + "narHash": "sha256-oz+BzUDwtyircjjxv9aPYOS5gobxLCjD2il+gb/bCRo=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e2ffefe304d941bb98989847944f3b58e0adcdd5", + "type": "github" + } + }, + "nixpkgs_5": { "locked": { "lastModified": 1698675399, "narHash": "sha256-nj+LNEeVXGP31vxoL3x7HW7+oEiyoLVDqwMg30yFBMA=", @@ -317,20 +368,20 @@ "poetry2nix", "flake-utils" ], - "nixpkgs": "nixpkgs_3", + "nixpkgs": "nixpkgs_5", "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1707497025, - "narHash": "sha256-7mcEdPkH9GtI96Mzrl9PktScw3M9dqFk6/nSp2gxpYc=", + "lastModified": 1709047520, + "narHash": "sha256-LRwhxm+m/uPowK8YgbzJLtwwoVILBxfqr8DjF/0pO0c=", "owner": "runtimeverification", "repo": "pyk", - "rev": "e68db42142d1e03d23cabd4cfff9082a08798f12", + "rev": "41b67113055d1396537283b8dd1a9d3fe879bada", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.619", + "ref": "v0.1.656", "repo": "pyk", "type": "github" } @@ -379,12 +430,33 @@ } }, "rv-utils": { + "inputs": { + "nixpkgs": "nixpkgs_3" + }, + "locked": { + "lastModified": 1707492220, + "narHash": "sha256-KRndaUPzUumDlNcKF7KzA8F/EZKLYCvurh7Z13sw2PI=", + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "rev": "abf86805a623948c941e603e2fc4c26a06ea6eb6", + "type": "github" + }, + "original": { + "owner": "runtimeverification", + "repo": "rv-nix-tools", + "type": "github" + } + }, + "rv-utils_2": { + "inputs": { + "nixpkgs": "nixpkgs_4" + }, "locked": { - "lastModified": 1659349707, - "narHash": "sha256-+RwJvYwRS4In+pl8R5Uz+R/yZ5yO5SAa7X6UR+eSC2U=", + "lastModified": 1707492220, + "narHash": "sha256-KRndaUPzUumDlNcKF7KzA8F/EZKLYCvurh7Z13sw2PI=", "owner": "runtimeverification", "repo": "rv-nix-tools", - "rev": "7026604726c5247ceb6e7a1a7532302a58e7e2bf", + "rev": "abf86805a623948c941e603e2fc4c26a06ea6eb6", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 53804bac6..c7cc887ba 100644 --- a/flake.nix +++ b/flake.nix @@ -2,11 +2,11 @@ description = " A flake for KMIR Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v6.2.4"; + k-framework.url = "github:runtimeverification/k/v6.3.5"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/pyk/v0.1.619"; + pyk.url = "github:runtimeverification/pyk/v0.1.656"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; }; diff --git a/kmir/poetry.lock b/kmir/poetry.lock index da9e69dc9..1503072a5 100644 --- a/kmir/poetry.lock +++ b/kmir/poetry.lock @@ -22,14 +22,14 @@ tests-no-zope = ["attrs[tests-mypy]", "cloudpickle", "hypothesis", "pympler", "p [[package]] name = "autoflake" -version = "2.2.1" +version = "2.3.0" description = "Removes unused imports and unused variables" category = "dev" optional = false python-versions = ">=3.8" files = [ - {file = "autoflake-2.2.1-py3-none-any.whl", hash = "sha256:265cde0a43c1f44ecfb4f30d95b0437796759d07be7706a2f70e4719234c0f79"}, - {file = "autoflake-2.2.1.tar.gz", hash = "sha256:62b7b6449a692c3c9b0c916919bbc21648da7281e8506bcf8d3f8280e431ebc1"}, + {file = "autoflake-2.3.0-py3-none-any.whl", hash = "sha256:79a51eb8c0744759d2efe052455ab20aa6a314763510c3fd897499a402126327"}, + {file = "autoflake-2.3.0.tar.gz", hash = "sha256:8c2011fa34701b9d7dcf05b9873bc4859d4fce4e62dfea90dffefd1576f5f01d"}, ] [package.dependencies] @@ -38,34 +38,34 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} [[package]] name = "black" -version = "24.1.1" +version = "24.2.0" description = "The uncompromising code formatter." category = "dev" optional = false python-versions = ">=3.8" files = [ - {file = "black-24.1.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:2588021038bd5ada078de606f2a804cadd0a3cc6a79cb3e9bb3a8bf581325a4c"}, - {file = "black-24.1.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:1a95915c98d6e32ca43809d46d932e2abc5f1f7d582ffbe65a5b4d1588af7445"}, - {file = "black-24.1.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2fa6a0e965779c8f2afb286f9ef798df770ba2b6cee063c650b96adec22c056a"}, - {file = "black-24.1.1-cp310-cp310-win_amd64.whl", hash = "sha256:5242ecd9e990aeb995b6d03dc3b2d112d4a78f2083e5a8e86d566340ae80fec4"}, - {file = "black-24.1.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:fc1ec9aa6f4d98d022101e015261c056ddebe3da6a8ccfc2c792cbe0349d48b7"}, - {file = "black-24.1.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:0269dfdea12442022e88043d2910429bed717b2d04523867a85dacce535916b8"}, - {file = "black-24.1.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b3d64db762eae4a5ce04b6e3dd745dcca0fb9560eb931a5be97472e38652a161"}, - {file = "black-24.1.1-cp311-cp311-win_amd64.whl", hash = "sha256:5d7b06ea8816cbd4becfe5f70accae953c53c0e53aa98730ceccb0395520ee5d"}, - {file = "black-24.1.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:e2c8dfa14677f90d976f68e0c923947ae68fa3961d61ee30976c388adc0b02c8"}, - {file = "black-24.1.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:a21725862d0e855ae05da1dd25e3825ed712eaaccef6b03017fe0853a01aa45e"}, - {file = "black-24.1.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:07204d078e25327aad9ed2c64790d681238686bce254c910de640c7cc4fc3aa6"}, - {file = "black-24.1.1-cp312-cp312-win_amd64.whl", hash = "sha256:a83fe522d9698d8f9a101b860b1ee154c1d25f8a82ceb807d319f085b2627c5b"}, - {file = "black-24.1.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:08b34e85170d368c37ca7bf81cf67ac863c9d1963b2c1780c39102187ec8dd62"}, - {file = "black-24.1.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:7258c27115c1e3b5de9ac6c4f9957e3ee2c02c0b39222a24dc7aa03ba0e986f5"}, - {file = "black-24.1.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:40657e1b78212d582a0edecafef133cf1dd02e6677f539b669db4746150d38f6"}, - {file = "black-24.1.1-cp38-cp38-win_amd64.whl", hash = "sha256:e298d588744efda02379521a19639ebcd314fba7a49be22136204d7ed1782717"}, - {file = "black-24.1.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:34afe9da5056aa123b8bfda1664bfe6fb4e9c6f311d8e4a6eb089da9a9173bf9"}, - {file = "black-24.1.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:854c06fb86fd854140f37fb24dbf10621f5dab9e3b0c29a690ba595e3d543024"}, - {file = "black-24.1.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3897ae5a21ca132efa219c029cce5e6bfc9c3d34ed7e892113d199c0b1b444a2"}, - {file = "black-24.1.1-cp39-cp39-win_amd64.whl", hash = "sha256:ecba2a15dfb2d97105be74bbfe5128bc5e9fa8477d8c46766505c1dda5883aac"}, - {file = "black-24.1.1-py3-none-any.whl", hash = "sha256:5cdc2e2195212208fbcae579b931407c1fa9997584f0a415421748aeafff1168"}, - {file = "black-24.1.1.tar.gz", hash = "sha256:48b5760dcbfe5cf97fd4fba23946681f3a81514c6ab8a45b50da67ac8fbc6c7b"}, + {file = "black-24.2.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6981eae48b3b33399c8757036c7f5d48a535b962a7c2310d19361edeef64ce29"}, + {file = "black-24.2.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:d533d5e3259720fdbc1b37444491b024003e012c5173f7d06825a77508085430"}, + {file = "black-24.2.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:61a0391772490ddfb8a693c067df1ef5227257e72b0e4108482b8d41b5aee13f"}, + {file = "black-24.2.0-cp310-cp310-win_amd64.whl", hash = "sha256:992e451b04667116680cb88f63449267c13e1ad134f30087dec8527242e9862a"}, + {file = "black-24.2.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:163baf4ef40e6897a2a9b83890e59141cc8c2a98f2dda5080dc15c00ee1e62cd"}, + {file = "black-24.2.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:e37c99f89929af50ffaf912454b3e3b47fd64109659026b678c091a4cd450fb2"}, + {file = "black-24.2.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4f9de21bafcba9683853f6c96c2d515e364aee631b178eaa5145fc1c61a3cc92"}, + {file = "black-24.2.0-cp311-cp311-win_amd64.whl", hash = "sha256:9db528bccb9e8e20c08e716b3b09c6bdd64da0dd129b11e160bf082d4642ac23"}, + {file = "black-24.2.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:d84f29eb3ee44859052073b7636533ec995bd0f64e2fb43aeceefc70090e752b"}, + {file = "black-24.2.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:1e08fb9a15c914b81dd734ddd7fb10513016e5ce7e6704bdd5e1251ceee51ac9"}, + {file = "black-24.2.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:810d445ae6069ce64030c78ff6127cd9cd178a9ac3361435708b907d8a04c693"}, + {file = "black-24.2.0-cp312-cp312-win_amd64.whl", hash = "sha256:ba15742a13de85e9b8f3239c8f807723991fbfae24bad92d34a2b12e81904982"}, + {file = "black-24.2.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:7e53a8c630f71db01b28cd9602a1ada68c937cbf2c333e6ed041390d6968faf4"}, + {file = "black-24.2.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:93601c2deb321b4bad8f95df408e3fb3943d85012dddb6121336b8e24a0d1218"}, + {file = "black-24.2.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a0057f800de6acc4407fe75bb147b0c2b5cbb7c3ed110d3e5999cd01184d53b0"}, + {file = "black-24.2.0-cp38-cp38-win_amd64.whl", hash = "sha256:faf2ee02e6612577ba0181f4347bcbcf591eb122f7841ae5ba233d12c39dcb4d"}, + {file = "black-24.2.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:057c3dc602eaa6fdc451069bd027a1b2635028b575a6c3acfd63193ced20d9c8"}, + {file = "black-24.2.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:08654d0797e65f2423f850fc8e16a0ce50925f9337fb4a4a176a7aa4026e63f8"}, + {file = "black-24.2.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ca610d29415ee1a30a3f30fab7a8f4144e9d34c89a235d81292a1edb2b55f540"}, + {file = "black-24.2.0-cp39-cp39-win_amd64.whl", hash = "sha256:4dd76e9468d5536abd40ffbc7a247f83b2324f0c050556d9c371c2b9a9a95e31"}, + {file = "black-24.2.0-py3-none-any.whl", hash = "sha256:e8a6ae970537e67830776488bca52000eaa37fa63b9988e8c487458d9cd5ace6"}, + {file = "black-24.2.0.tar.gz", hash = "sha256:bce4f25c27c3435e4dace4815bcb2008b87e167e3bf4ee47ccdc5ce906eb4894"}, ] [package.dependencies] @@ -250,17 +250,18 @@ flake8 = ">=3.0,<3.2.0 || >3.2.0" [[package]] name = "flake8-quotes" -version = "3.3.2" +version = "3.4.0" description = "Flake8 lint for quotes." category = "dev" optional = false python-versions = "*" files = [ - {file = "flake8-quotes-3.3.2.tar.gz", hash = "sha256:6e26892b632dacba517bf27219c459a8396dcfac0f5e8204904c5a4ba9b480e1"}, + {file = "flake8-quotes-3.4.0.tar.gz", hash = "sha256:aad8492fb710a2d3eabe68c5f86a1428de650c8484127e14c43d0504ba30276c"}, ] [package.dependencies] flake8 = "*" +setuptools = "*" [[package]] name = "graphviz" @@ -648,7 +649,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.619" +version = "0.1.656" description = "" category = "main" optional = false @@ -670,8 +671,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.619" -resolved_reference = "e68db42142d1e03d23cabd4cfff9082a08798f12" +reference = "v0.1.656" +resolved_reference = "41b67113055d1396537283b8dd1a9d3fe879bada" [[package]] name = "pyperclip" @@ -698,14 +699,14 @@ files = [ [[package]] name = "pytest" -version = "8.0.0" +version = "8.0.2" description = "pytest: simple powerful testing with Python" category = "main" optional = false python-versions = ">=3.8" files = [ - {file = "pytest-8.0.0-py3-none-any.whl", hash = "sha256:50fb9cbe836c3f20f0dfa99c565201fb75dc54c8d76373cd1bde06b06657bdb6"}, - {file = "pytest-8.0.0.tar.gz", hash = "sha256:249b1b0864530ba251b7438274c4d251c58d868edaaec8762893ad4a0d71c36c"}, + {file = "pytest-8.0.2-py3-none-any.whl", hash = "sha256:edfaaef32ce5172d5466b5127b42e0d6d35ebbe4453f0e3505d96afd93f6b096"}, + {file = "pytest-8.0.2.tar.gz", hash = "sha256:d4051d623a2e0b7e51960ba963193b09ce6daeb9759a451844a21e4ddedfc1bd"}, ] [package.dependencies] @@ -792,6 +793,23 @@ pygments = ">=2.13.0,<3.0.0" [package.extras] jupyter = ["ipywidgets (>=7.5.1,<9)"] +[[package]] +name = "setuptools" +version = "69.1.1" +description = "Easily download, build, install, upgrade, and uninstall Python packages" +category = "dev" +optional = false +python-versions = ">=3.8" +files = [ + {file = "setuptools-69.1.1-py3-none-any.whl", hash = "sha256:02fa291a0471b3a18b2b2481ed902af520c69e8ae0919c13da936542754b4c56"}, + {file = "setuptools-69.1.1.tar.gz", hash = "sha256:5c0806c7d9af348e6dd3777b4f4dbb42c7ad85b190104837488eab9a7c945cf8"}, +] + +[package.extras] +docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "rst.linker (>=1.9)", "sphinx (<7.2.5)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier"] +testing = ["build[virtualenv]", "filelock (>=3.4.0)", "flake8-2020", "ini2toml[lite] (>=0.9)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pip (>=19.1)", "pytest (>=6)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy (>=0.9.1)", "pytest-perf", "pytest-ruff (>=0.2.1)", "pytest-timeout", "pytest-xdist", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] +testing-integration = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pytest", "pytest-enabler", "pytest-xdist", "tomli", "virtualenv (>=13.0.0)", "wheel"] + [[package]] name = "textual" version = "0.27.0" @@ -827,26 +845,26 @@ files = [ [[package]] name = "typing-extensions" -version = "4.9.0" +version = "4.10.0" description = "Backported and Experimental Type Hints for Python 3.8+" category = "main" optional = false python-versions = ">=3.8" files = [ - {file = "typing_extensions-4.9.0-py3-none-any.whl", hash = "sha256:af72aea155e91adfc61c3ae9e0e342dbc0cba726d6cba4b6c72c1f34e47291cd"}, - {file = "typing_extensions-4.9.0.tar.gz", hash = "sha256:23478f88c37f27d76ac8aee6c905017a143b0b1b886c3c9f66bc2fd94f9f5783"}, + {file = "typing_extensions-4.10.0-py3-none-any.whl", hash = "sha256:69b1a937c3a517342112fb4c6df7e72fc39a38e7891a5730ed4985b5214b5475"}, + {file = "typing_extensions-4.10.0.tar.gz", hash = "sha256:b0abd7c89e8fb96f98db18d86106ff1d90ab692004eb746cf6eda2682f91b3cb"}, ] [[package]] name = "uc-micro-py" -version = "1.0.2" +version = "1.0.3" description = "Micro subset of unicode data files for linkify-it-py projects." category = "main" optional = false python-versions = ">=3.7" files = [ - {file = "uc-micro-py-1.0.2.tar.gz", hash = "sha256:30ae2ac9c49f39ac6dce743bd187fcd2b574b16ca095fa74cd9396795c954c54"}, - {file = "uc_micro_py-1.0.2-py3-none-any.whl", hash = "sha256:8c9110c309db9d9e87302e2f4ad2c3152770930d88ab385cd544e7a7e75f3de0"}, + {file = "uc-micro-py-1.0.3.tar.gz", hash = "sha256:d321b92cff673ec58027c04015fcaa8bb1e005478643ff4a500882eaab88c48a"}, + {file = "uc_micro_py-1.0.3-py3-none-any.whl", hash = "sha256:db1dffff340817673d7b466ec86114a9dc0e9d4d9b5ba229d9d60e5c12600cd5"}, ] [package.extras] @@ -895,4 +913,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "e6337a7e3744f59fc99d8e1bb01fb555d1195ea56fb8d0f91233c14d71a927b4" +content-hash = "6995220a9a1291a429f417a301c107600fc89ba1e99e0af24d9f27bb77aee79b" diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 32ce98757..55a33bfa7 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmir" -version = "0.2.28" +version = "0.2.29" description = "" authors = [ "Runtime Verification, Inc. ", @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" filelock = "3.9.0" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.619" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.656" } pytest-timeout = "2.1.0" [tool.poetry.group.dev.dependencies] diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 9aab1d164..692a98b7f 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -5,4 +5,4 @@ from .prove import prove, show_proof, view_proof from .run import run -VERSION: Final = '0.2.28' +VERSION: Final = '0.2.29' diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 8ac9a4d87..ff774c8b8 100644 --- a/kmir/src/kmir/kmir.py +++ b/kmir/src/kmir/kmir.py @@ -8,7 +8,7 @@ from subprocess import CalledProcessError, CompletedProcess from typing import Callable, Final, Iterable, Iterator, Optional, final -from pyk.cterm import CTerm +from pyk.cterm import CTerm, CTermSymbolic from pyk.kast.inner import KInner from pyk.kast.outer import KClaim from pyk.kcfg import KCFG, KCFGExplore @@ -18,7 +18,7 @@ from pyk.kore.syntax import Pattern, SortApp from pyk.kore.tools import PrintOutput, kore_print from pyk.ktool.kprove import KProve -from pyk.proof import APRProof, APRProver, EqualityProof, EqualityProver +from pyk.proof import APRProof, APRProver, EqualityProof, ImpliesProver from pyk.proof.proof import Proof, Prover # not exported explicitly from pyk.utils import BugReport, check_file_path, run_process @@ -101,13 +101,10 @@ def set_kore_server( def rpc_session(self, server: KoreServer, claim_id: str, trace_rewrites: bool = False) -> Iterator[KCFGExplore]: with server as server: with KoreClient('localhost', server.port, bug_report=self.bug_report) as client: - yield KCFGExplore( - kprint=self.mir_prove, - kore_client=client, - kcfg_semantics=KMIRSemantics(), - id=claim_id, - trace_rewrites=trace_rewrites, + cterm_symbolic = CTermSymbolic( + client, self.mir_prove.definition, self.mir_prove.kompiled_kore, trace_rewrites=trace_rewrites ) + yield KCFGExplore(self.mir_prove, cterm_symbolic, kcfg_semantics=KMIRSemantics(), id=claim_id) # A wrapper on KProve's get_claims def get_all_claims(self, spec_file: Path, claim_label: Optional[str]) -> list[KClaim]: @@ -147,11 +144,11 @@ def initialise_a_proof( new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm) _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') - new_init = kcfg_explore.cterm_assume_defined(new_init) + new_init = kcfg_explore.cterm_symbolic.assume_defined(new_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) + new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init) + new_target, _ = kcfg_explore.cterm_symbolic.simplify(new_target) if CTerm._is_bottom(new_init.kast): raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?') if CTerm._is_top(new_target.kast): @@ -277,17 +274,20 @@ def prove_driver( prover: Prover # case APRProof: if isinstance(proof, APRProof): - prover = APRProver(proof, rpc_session) - prover.advance_proof( - max_iterations=max_iterations, + prover = APRProver( + proof, + kcfg_explore=rpc_session, execute_depth=max_depth, terminal_rules=terminal_rules, cut_point_rules=cut_point_rules, ) + prover.advance_proof( + max_iterations=max_iterations, + ) passed = proof.status elif isinstance(proof, EqualityProof): # case EqualityProof: - prover = EqualityProver(proof, rpc_session) + prover = ImpliesProver(proof, rpc_session) prover.advance_proof() passed = proof.status else: diff --git a/kmir/src/tests/nix/sum-to-n.run.out b/kmir/src/tests/nix/sum-to-n.run.out index 147f05c53..539fcd8ef 100644 --- a/kmir/src/tests/nix/sum-to-n.run.out +++ b/kmir/src/tests/nix/sum-to-n.run.out @@ -1,6 +1,6 @@   - #halt ~> . + #halt ~> .K   0 diff --git a/package/version b/package/version index 8bc53d520..1b87bf5de 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.2.28 +0.2.29