diff --git a/deps/k_release b/deps/k_release index 6d96fbf..f47526b 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.288 +7.1.298 diff --git a/examples/specs/imp-sum-spec.k b/examples/specs/imp-sum-spec.k index 4c44ac2..8e6519b 100644 --- a/examples/specs/imp-sum-spec.k +++ b/examples/specs/imp-sum-spec.k @@ -18,6 +18,7 @@ module IMP-SUM-SPEC $s |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2)) requires N >=Int 0 + [circularity] claim [two-sum-spec]: @@ -41,5 +42,6 @@ module IMP-SUM-SPEC requires N >=Int 0 andBool M >=Int 0 + [circularity] endmodule diff --git a/flake.lock b/flake.lock index bfcb60f..c112c25 100644 --- a/flake.lock +++ b/flake.lock @@ -127,6 +127,7 @@ "nixpkgs": [ "nixpkgs" ], + "nixpkgs-unstable": "nixpkgs-unstable", "pyproject-build-systems": "pyproject-build-systems", "pyproject-nix": [ "k-framework", @@ -137,16 +138,16 @@ "uv2nix": "uv2nix" }, "locked": { - "lastModified": 1758173229, - "narHash": "sha256-h/Alhkrh0AXdk+BDrqiskADMwQU9zOcZ8p1wpAOVMBA=", + "lastModified": 1760461378, + "narHash": "sha256-QMMb4U7mIXR+t/Ip6VgKZWuzsEY7ew4Zs+yDQg1eOfk=", "owner": "runtimeverification", "repo": "k", - "rev": "62ce121afe7221670ed089097c44b3284531751f", + "rev": "a5156a20308cc25e66cb9ec64f2b9ab5f21a626e", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.288", + "ref": "v7.1.298", "repo": "k", "type": "github" } @@ -212,39 +213,39 @@ "type": "github" } }, - "nixpkgs_2": { + "nixpkgs-unstable_2": { "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", + "lastModified": 1760284886, + "narHash": "sha256-TK9Kr0BYBQ/1P5kAsnNQhmWWKgmZXwUQr4ZMjCzWf2c=", + "owner": "NixOS", "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "rev": "cf3f5c4def3c7b5f1fc012b3d839575dbe552d43", "type": "github" }, "original": { - "owner": "nixos", + "owner": "NixOS", + "ref": "nixos-unstable", "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", "type": "github" } }, - "nixpkgs_3": { + "nixpkgs_2": { "locked": { - "lastModified": 1744306051, - "narHash": "sha256-jWwqkmi8cplBu4CXUb4zdfpqKp3UJYVAs/b5m8M75sg=", - "owner": "runtimeverification", + "lastModified": 1716457947, + "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", + "owner": "nixos", "repo": "nixpkgs", - "rev": "e9a77bb24d408d3898f6a11fb065d350d6bc71f1", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", "type": "github" }, "original": { - "owner": "runtimeverification", - "ref": "libmatch", + "owner": "nixos", "repo": "nixpkgs", + "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", "type": "github" } }, - "nixpkgs_4": { + "nixpkgs_3": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -294,17 +295,17 @@ ] }, "locked": { - "lastModified": 1744599653, - "narHash": "sha256-nysSwVVjG4hKoOjhjvE6U5lIKA8sEr1d1QzEfZsannU=", + "lastModified": 1759113590, + "narHash": "sha256-fgxP2RCN4cg0jYiMYoETYc7TZ2JjgyvJa2y9l8oSUFE=", "owner": "pyproject-nix", "repo": "build-system-pkgs", - "rev": "7dba6dbc73120e15b558754c26024f6c93015dd7", + "rev": "dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5", "type": "github" }, "original": { "owner": "pyproject-nix", "repo": "build-system-pkgs", - "rev": "7dba6dbc73120e15b558754c26024f6c93015dd7", + "rev": "dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5", "type": "github" } }, @@ -345,11 +346,11 @@ ] }, "locked": { - "lastModified": 1745782090, - "narHash": "sha256-c/mqxgOVDcwrdcY3FqG22MwLPGY5rCz5gte1sxISKnM=", + "lastModified": 1758265079, + "narHash": "sha256-amLaLNwKSZPShQHzfgmc/9o76dU8xzN0743dWgvYlr8=", "owner": "pyproject-nix", "repo": "pyproject.nix", - "rev": "2db2d95ddbc4ff5e29730cb82fdba6647be258a7", + "rev": "02e9418fd4af638447dca4b17b1280da95527fc9", "type": "github" }, "original": { @@ -404,7 +405,7 @@ "rv-nix-tools", "nixpkgs" ], - "nixpkgs-unstable": "nixpkgs-unstable", + "nixpkgs-unstable": "nixpkgs-unstable_2", "pyproject-build-systems": "pyproject-build-systems_2", "pyproject-nix": [ "uv2nix", @@ -454,7 +455,7 @@ }, "rv-nix-tools_3": { "inputs": { - "nixpkgs": "nixpkgs_4" + "nixpkgs": "nixpkgs_3" }, "locked": { "lastModified": 1726497185, @@ -552,21 +553,24 @@ }, "uv2nix": { "inputs": { - "nixpkgs": "nixpkgs_3", + "nixpkgs": [ + "k-framework", + "nixpkgs-unstable" + ], "pyproject-nix": "pyproject-nix" }, "locked": { - "lastModified": 1746048139, - "narHash": "sha256-LdCLyiihLg6P2/mjzP0+W7RtraDSIaJJPTy6SCtW5Ag=", + "lastModified": 1760161183, + "narHash": "sha256-1USClOZthg+pGJp+p3ouVtTMO+ZY8Cd0+FbsNN/RpO8=", "owner": "pyproject-nix", "repo": "uv2nix", - "rev": "680e2f8e637bc79b84268949d2f2b2f5e5f1d81c", + "rev": "b6ed0901aec29583532abe65117b18d86a49b617", "type": "github" }, "original": { "owner": "pyproject-nix", "repo": "uv2nix", - "rev": "680e2f8e637bc79b84268949d2f2b2f5e5f1d81c", + "rev": "b6ed0901aec29583532abe65117b18d86a49b617", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 0e2d367..97b1b14 100644 --- a/flake.nix +++ b/flake.nix @@ -5,7 +5,7 @@ nixpkgs.follows = "rv-nix-tools/nixpkgs"; flake-utils.url = "github:numtide/flake-utils"; - k-framework.url = "github:runtimeverification/k/v7.1.288"; + k-framework.url = "github:runtimeverification/k/v7.1.298"; k-framework.inputs.nixpkgs.follows = "nixpkgs"; uv2nix.url = "github:pyproject-nix/uv2nix/b6ed0901aec29583532abe65117b18d86a49b617"; # uv2nix requires a newer version of nixpkgs diff --git a/pyproject.toml b/pyproject.toml index 245609b..2ed7ede 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -9,7 +9,7 @@ description = "" readme = "README.md" requires-python = "~=3.10" dependencies = [ - "kframework==7.1.288", + "kframework==7.1.298", ] [[project.authors]] diff --git a/uv.lock b/uv.lock index ee379b2..7fdd079 100644 --- a/uv.lock +++ b/uv.lock @@ -475,16 +475,16 @@ wheels = [ [[package]] name = "hypothesis" -version = "6.140.3" +version = "6.141.0" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "attrs" }, { name = "exceptiongroup", marker = "python_full_version < '3.11'" }, { name = "sortedcontainers" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/18/7f/946343e32881b56adc0eba64e428ad2f85251f9ef16e3e4ec1b6ab80199b/hypothesis-6.140.3.tar.gz", hash = "sha256:4f4a09bf77af21e0cc3dffed1ea639812dc75d38f81308ec9fb0e33f8557b0cb", size = 466925, upload-time = "2025-10-04T22:29:44.499Z" } +sdist = { url = "https://files.pythonhosted.org/packages/7d/ca/31352c7e7aa623eeb712efb415e7934d7bb7068983e8edfd688c647dcbff/hypothesis-6.141.0.tar.gz", hash = "sha256:a66861954dc1768945eda83ca28a9bbb5bc59a45edae899c219e2dd85a8ddd43", size = 467168, upload-time = "2025-10-15T05:00:28.494Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/65/2a/0553ac2a8af432df92f2ffc05ca97e7ed64e00c97a371b019ae2690de325/hypothesis-6.140.3-py3-none-any.whl", hash = "sha256:a2cfff51641a58a56081f5c90ae1da6ccf3d043404f411805f7f0e0d75742d0e", size = 534534, upload-time = "2025-10-04T22:29:40.635Z" }, + { url = "https://files.pythonhosted.org/packages/8e/e4/c92740135f9ad1cfe85aa7187eb72804fd5610d4a6ad72e39b6574e51588/hypothesis-6.141.0-py3-none-any.whl", hash = "sha256:29a1b4301611bdd2833a5ad5fc422c72b60071a169ee048e28b1435ac410d072", size = 534788, upload-time = "2025-10-15T05:00:24.387Z" }, ] [[package]] @@ -528,7 +528,7 @@ wheels = [ [[package]] name = "kframework" -version = "7.1.288" +version = "7.1.298" source = { registry = "https://pypi.org/simple" } dependencies = [ { name = "coloredlogs" }, @@ -545,9 +545,9 @@ dependencies = [ { name = "tomli" }, { name = "xdg-base-dirs" }, ] -sdist = { url = "https://files.pythonhosted.org/packages/ce/03/7ccd18f17c7d2f9b5b37041592e2e36b7dc054a0fecb05e8c39a4bcecf15/kframework-7.1.288.tar.gz", hash = "sha256:e08e5ee2821b8c8bb7da8871c8ef1e77fad3b5c2d1a6eaa5e08879f970f4c0ed", size = 242925, upload-time = "2025-09-18T05:48:02.013Z" } +sdist = { url = "https://files.pythonhosted.org/packages/61/89/4c8bbbe7b9fda869df93b5ec9e092e4b6fbe6f6bbb1be974fbed84aa7c1a/kframework-7.1.298.tar.gz", hash = "sha256:30aa8dd44803260809ff9c614c182d2617f2b7349bb7cb4004d3a8f5fb76b0f3", size = 242937, upload-time = "2025-10-14T17:57:44.363Z" } wheels = [ - { url = "https://files.pythonhosted.org/packages/fd/c5/64c539ea000ce6bdea700e0774d67d8506123ac046ee81d7eb8a7ce9a9ba/kframework-7.1.288-py3-none-any.whl", hash = "sha256:0b922c332550e9b50e70d0f34a89ed5dd281df8ddbb04ee883de7d089cf3b272", size = 294117, upload-time = "2025-09-18T05:48:00.422Z" }, + { url = "https://files.pythonhosted.org/packages/be/32/dd84ba58e8a8d1972f9fbaabcc575251a5601aa487268ebde3c9739c9e60/kframework-7.1.298-py3-none-any.whl", hash = "sha256:9110c2f93d5ad4c6eaf8c07b9afbcacfc0e347fe6a0b2c794c5e79560d4c3eba", size = 294134, upload-time = "2025-10-14T17:57:42.621Z" }, ] [[package]] @@ -578,7 +578,7 @@ dev = [ ] [package.metadata] -requires-dist = [{ name = "kframework", specifier = "==7.1.288" }] +requires-dist = [{ name = "kframework", specifier = "==7.1.298" }] [package.metadata.requires-dev] dev = [