From 5302b3e1ac4731b059f0e16c9bc6621305c4e7e9 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 11 Jul 2024 10:27:15 -0600 Subject: [PATCH] Update dependency: deps/kwasm_release (#297) * deps/kwasm_release: Set Version 0.1.72 * Set Version: 0.1.89 * kmultiversx/: sync poetry files 0.1.72 * deps/k_release: sync release file version 7.1.38 * flake.{nix,lock}: update Nix derivations * deps/kwasm_release: Set Version 0.1.73 * kmultiversx/: sync poetry files 0.1.73 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.93 * deps/kwasm_release: Set Version 0.1.83 * kmultiversx/: sync poetry files 0.1.83 * deps/k_release: sync release file version 7.1.54 * flake.{nix,lock}: update Nix derivations * Fix klabel, symbol cases * Set Version: 0.1.94 * deps/blockchain-k-plugin_release: sync release file version 98b82c75eaae9771f472e2fa6cb2d63808734791 * flake.{nix,lock}: update Nix derivations * Fix mistaken update of BKP * deps/blockchain-k-plugin_release: sync release file version b24fa372ca127d51cdc185e431d0ccf471980c04 * flake.{nix,lock}: update Nix derivations * Fix symbol from K --------- Co-authored-by: devops Co-authored-by: Bruce Collie --- deps/k_release | 2 +- deps/kwasm_release | 2 +- flake.lock | 515 ++++++++---------- flake.nix | 6 +- kmultiversx/poetry.lock | 16 +- kmultiversx/pyproject.toml | 4 +- kmultiversx/src/kmultiversx/kasmer.py | 2 +- .../kdist/mx-semantics/data/async-call.k | 2 +- .../kdist/mx-semantics/data/int-type.k | 4 +- .../kmultiversx/kdist/mx-semantics/kasmer.md | 6 +- package/version | 2 +- 11 files changed, 245 insertions(+), 316 deletions(-) diff --git a/deps/k_release b/deps/k_release index f4791f96..3e3ba255 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.30 +7.1.54 diff --git a/deps/kwasm_release b/deps/kwasm_release index 7c3ae4e0..660b5ae0 100644 --- a/deps/kwasm_release +++ b/deps/kwasm_release @@ -1 +1 @@ -0.1.71 +0.1.83 diff --git a/flake.lock b/flake.lock index e96e8ebb..7cd91ea0 100644 --- a/flake.lock +++ b/flake.lock @@ -115,24 +115,6 @@ } }, "flake-utils": { - "inputs": { - "systems": "systems" - }, - "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "flake-utils_2": { "inputs": { "systems": "systems_2" }, @@ -150,16 +132,16 @@ "type": "github" } }, - "flake-utils_3": { + "flake-utils_2": { "inputs": { "systems": "systems_4" }, "locked": { - "lastModified": 1710146030, - "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -168,9 +150,9 @@ "type": "github" } }, - "flake-utils_4": { + "flake-utils_3": { "inputs": { - "systems": "systems_5" + "systems": "systems_7" }, "locked": { "lastModified": 1694529238, @@ -224,25 +206,28 @@ "inputs": { "nixpkgs": [ "k-framework", - "haskell-backend", - "rv-utils", + "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils", + "rv-utils": [ + "k-framework", + "llvm-backend", + "rv-utils" + ], "stacklock2nix": "stacklock2nix", "z3": "z3" }, "locked": { - "lastModified": 1719218678, - "narHash": "sha256-7FVcMNEGulpwvzwrlPwqgd+qhArW3mE6TA/e6oSF0m4=", + "lastModified": 1719881076, + "narHash": "sha256-t9RTbVarwaobMiJkQjXykP8Qt+26miKzr3inONULvck=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "a6f5646a160c277e6e252552eee86563309a9776", + "rev": "11265424aeb138168bc73f1f028273de192b5be4", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.19", + "ref": "v0.1.29", "repo": "haskell-backend", "type": "github" } @@ -252,25 +237,29 @@ "nixpkgs": [ "wasm-semantics", "k-framework", - "haskell-backend", - "rv-utils", + "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils_6", + "rv-utils": [ + "wasm-semantics", + "k-framework", + "llvm-backend", + "rv-utils" + ], "stacklock2nix": "stacklock2nix_2", "z3": "z3_2" }, "locked": { - "lastModified": 1719218678, - "narHash": "sha256-7FVcMNEGulpwvzwrlPwqgd+qhArW3mE6TA/e6oSF0m4=", + "lastModified": 1719881076, + "narHash": "sha256-t9RTbVarwaobMiJkQjXykP8Qt+26miKzr3inONULvck=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "a6f5646a160c277e6e252552eee86563309a9776", + "rev": "11265424aeb138168bc73f1f028273de192b5be4", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.19", + "ref": "v0.1.29", "repo": "haskell-backend", "type": "github" } @@ -311,7 +300,11 @@ }, "k-framework": { "inputs": { - "flake-utils": "flake-utils", + "flake-utils": [ + "k-framework", + "llvm-backend", + "utils" + ], "haskell-backend": "haskell-backend", "llvm-backend": "llvm-backend", "nixpkgs": [ @@ -319,26 +312,36 @@ "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils_3" + "poetry2nix": "poetry2nix", + "rv-utils": [ + "k-framework", + "llvm-backend", + "rv-utils" + ] }, "locked": { - "lastModified": 1719331365, - "narHash": "sha256-2J/lEgLQNbJlmygMzwRkGDLJNBTTHiCtfFxckGTm6Ec=", + "lastModified": 1720638169, + "narHash": "sha256-Pxl5c5Ti3Dt+p3IKhwZNONiYHwELdypd39U6AQB51D0=", "owner": "runtimeverification", "repo": "k", - "rev": "0cfdcda602d13ef43f8fbc508c0e405dd0a5784e", + "rev": "349304ae7c223dd7451cd0671ab8c865c3e2994e", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.30", + "ref": "v7.1.54", "repo": "k", "type": "github" } }, "k-framework_2": { "inputs": { - "flake-utils": "flake-utils_3", + "flake-utils": [ + "wasm-semantics", + "k-framework", + "llvm-backend", + "utils" + ], "haskell-backend": "haskell-backend_2", "llvm-backend": "llvm-backend_2", "nixpkgs": [ @@ -347,19 +350,25 @@ "llvm-backend", "nixpkgs" ], - "rv-utils": "rv-utils_8" + "poetry2nix": "poetry2nix_3", + "rv-utils": [ + "wasm-semantics", + "k-framework", + "llvm-backend", + "rv-utils" + ] }, "locked": { - "lastModified": 1719331365, - "narHash": "sha256-2J/lEgLQNbJlmygMzwRkGDLJNBTTHiCtfFxckGTm6Ec=", + "lastModified": 1720638169, + "narHash": "sha256-Pxl5c5Ti3Dt+p3IKhwZNONiYHwELdypd39U6AQB51D0=", "owner": "runtimeverification", "repo": "k", - "rev": "0cfdcda602d13ef43f8fbc508c0e405dd0a5784e", + "rev": "349304ae7c223dd7451cd0671ab8c865c3e2994e", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.30", + "ref": "v7.1.54", "repo": "k", "type": "github" } @@ -394,23 +403,20 @@ ], "pybind11-src": "pybind11-src", "rapidjson-src": "rapidjson-src", - "rv-utils": "rv-utils_2", - "utils": [ - "k-framework", - "flake-utils" - ] + "rv-utils": "rv-utils", + "utils": "utils" }, "locked": { - "lastModified": 1718910118, - "narHash": "sha256-E2utS5SGK3B7IjHRBlyKSB6TR/gLli14m+7d8AAmp0I=", + "lastModified": 1720605767, + "narHash": "sha256-f2+y13P306W0Ws7gfjVkG4jytHqfSY0qAd4KeF/qZno=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "6671fe4b8de164ac2d141dcce869a06b628ed560", + "rev": "bd12ae4ace1f288b3b6236cc42f7004fe38e9965", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.51", + "ref": "v0.1.56", "repo": "llvm-backend", "type": "github" } @@ -429,24 +435,20 @@ ], "pybind11-src": "pybind11-src_2", "rapidjson-src": "rapidjson-src_2", - "rv-utils": "rv-utils_7", - "utils": [ - "wasm-semantics", - "k-framework", - "flake-utils" - ] + "rv-utils": "rv-utils_4", + "utils": "utils_2" }, "locked": { - "lastModified": 1718910118, - "narHash": "sha256-E2utS5SGK3B7IjHRBlyKSB6TR/gLli14m+7d8AAmp0I=", + "lastModified": 1720605767, + "narHash": "sha256-f2+y13P306W0Ws7gfjVkG4jytHqfSY0qAd4KeF/qZno=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "6671fe4b8de164ac2d141dcce869a06b628ed560", + "rev": "bd12ae4ace1f288b3b6236cc42f7004fe38e9965", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.51", + "ref": "v0.1.56", "repo": "llvm-backend", "type": "github" } @@ -454,7 +456,7 @@ "nix-github-actions": { "inputs": { "nixpkgs": [ - "pyk", + "k-framework", "poetry2nix", "nixpkgs" ] @@ -476,7 +478,6 @@ "nix-github-actions_2": { "inputs": { "nixpkgs": [ - "wasm-semantics", "pyk", "poetry2nix", "nixpkgs" @@ -496,55 +497,30 @@ "type": "github" } }, - "nixpkgs": { - "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - }, - "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - } - }, - "nixpkgs_2": { - "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" + "nix-github-actions_3": { + "inputs": { + "nixpkgs": [ + "wasm-semantics", + "k-framework", + "poetry2nix", + "nixpkgs" + ] }, - "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - } - }, - "nixpkgs_3": { "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "lastModified": 1693660503, + "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=", + "owner": "nix-community", + "repo": "nix-github-actions", + "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0", "type": "github" }, "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "owner": "nix-community", + "repo": "nix-github-actions", "type": "github" } }, - "nixpkgs_4": { + "nixpkgs": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -560,7 +536,7 @@ "type": "github" } }, - "nixpkgs_5": { + "nixpkgs_2": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -576,7 +552,7 @@ "type": "github" } }, - "nixpkgs_6": { + "nixpkgs_3": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -592,7 +568,7 @@ "type": "github" } }, - "nixpkgs_7": { + "nixpkgs_4": { "locked": { "lastModified": 1716457947, "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", @@ -608,48 +584,43 @@ "type": "github" } }, - "nixpkgs_8": { - "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" + "poetry2nix": { + "inputs": { + "flake-utils": "flake-utils", + "nix-github-actions": "nix-github-actions", + "nixpkgs": [ + "k-framework", + "llvm-backend", + "nixpkgs" + ], + "systems": "systems_3", + "treefmt-nix": "treefmt-nix" }, - "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", - "type": "github" - } - }, - "nixpkgs_9": { "locked": { - "lastModified": 1716457947, - "narHash": "sha256-Y+exebcqeprnhEpoPJrEUZmNeO60qeOxkVHhqG/OEwQ=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "lastModified": 1698640399, + "narHash": "sha256-mXzyx79/iFLZ0UDuSkqgFfejYRcSJfsCnJ9WlMusaI0=", + "owner": "nix-community", + "repo": "poetry2nix", + "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", "type": "github" }, "original": { - "owner": "nixos", - "repo": "nixpkgs", - "rev": "69493a13eaea0dc4682fd07e8a084f17813dbeeb", + "owner": "nix-community", + "repo": "poetry2nix", + "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c", "type": "github" } }, - "poetry2nix": { + "poetry2nix_2": { "inputs": { "flake-utils": "flake-utils_2", - "nix-github-actions": "nix-github-actions", + "nix-github-actions": "nix-github-actions_2", "nixpkgs": [ "pyk", "nixpkgs" ], - "systems": "systems_3", - "treefmt-nix": "treefmt-nix" + "systems": "systems_5", + "treefmt-nix": "treefmt-nix_2" }, "locked": { "lastModified": 1698640399, @@ -666,17 +637,18 @@ "type": "github" } }, - "poetry2nix_2": { + "poetry2nix_3": { "inputs": { - "flake-utils": "flake-utils_4", - "nix-github-actions": "nix-github-actions_2", + "flake-utils": "flake-utils_3", + "nix-github-actions": "nix-github-actions_3", "nixpkgs": [ "wasm-semantics", - "pyk", + "k-framework", + "llvm-backend", "nixpkgs" ], - "systems": "systems_6", - "treefmt-nix": "treefmt-nix_2" + "systems": "systems_8", + "treefmt-nix": "treefmt-nix_3" }, "locked": { "lastModified": 1698640399, @@ -739,56 +711,22 @@ "rv-utils", "nixpkgs" ], - "poetry2nix": "poetry2nix", - "rv-utils": "rv-utils_4" - }, - "locked": { - "dir": "pyk", - "lastModified": 1719331365, - "narHash": "sha256-2J/lEgLQNbJlmygMzwRkGDLJNBTTHiCtfFxckGTm6Ec=", - "owner": "runtimeverification", - "repo": "k", - "rev": "0cfdcda602d13ef43f8fbc508c0e405dd0a5784e", - "type": "github" - }, - "original": { - "dir": "pyk", - "owner": "runtimeverification", - "ref": "v7.1.30", - "repo": "k", - "type": "github" - } - }, - "pyk_2": { - "inputs": { - "flake-utils": [ - "wasm-semantics", - "pyk", - "poetry2nix", - "flake-utils" - ], - "nixpkgs": [ - "wasm-semantics", - "pyk", - "rv-utils", - "nixpkgs" - ], "poetry2nix": "poetry2nix_2", - "rv-utils": "rv-utils_9" + "rv-utils": "rv-utils_2" }, "locked": { "dir": "pyk", - "lastModified": 1719331365, - "narHash": "sha256-2J/lEgLQNbJlmygMzwRkGDLJNBTTHiCtfFxckGTm6Ec=", + "lastModified": 1720638169, + "narHash": "sha256-Pxl5c5Ti3Dt+p3IKhwZNONiYHwELdypd39U6AQB51D0=", "owner": "runtimeverification", "repo": "k", - "rev": "0cfdcda602d13ef43f8fbc508c0e405dd0a5784e", + "rev": "349304ae7c223dd7451cd0671ab8c865c3e2994e", "type": "github" }, "original": { "dir": "pyk", "owner": "runtimeverification", - "ref": "v7.1.30", + "ref": "v7.1.54", "repo": "k", "type": "github" } @@ -848,7 +786,7 @@ "poetry2nix" ], "pyk": "pyk", - "rv-utils": "rv-utils_5", + "rv-utils": "rv-utils_3", "wasm-semantics": "wasm-semantics" } }, @@ -924,96 +862,6 @@ "type": "github" } }, - "rv-utils_5": { - "inputs": { - "nixpkgs": "nixpkgs_5" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, - "rv-utils_6": { - "inputs": { - "nixpkgs": "nixpkgs_6" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, - "rv-utils_7": { - "inputs": { - "nixpkgs": "nixpkgs_7" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, - "rv-utils_8": { - "inputs": { - "nixpkgs": "nixpkgs_8" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, - "rv-utils_9": { - "inputs": { - "nixpkgs": "nixpkgs_9" - }, - "locked": { - "lastModified": 1716459074, - "narHash": "sha256-IpahO+EkWdGl9QP7B2YXfJWpSfghjxgpz4ab47nRJY4=", - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "rev": "a65058865cda201de504f5546271b8e997a0be9c", - "type": "github" - }, - "original": { - "owner": "runtimeverification", - "repo": "rv-nix-tools", - "type": "github" - } - }, "stacklock2nix": { "locked": { "lastModified": 1705051190, @@ -1104,6 +952,20 @@ } }, "systems_5": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "id": "systems", + "type": "indirect" + } + }, + "systems_6": { "locked": { "lastModified": 1681028828, "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", @@ -1118,7 +980,22 @@ "type": "github" } }, - "systems_6": { + "systems_7": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + }, + "systems_8": { "locked": { "lastModified": 1681028828, "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", @@ -1135,7 +1012,7 @@ "treefmt-nix": { "inputs": { "nixpkgs": [ - "pyk", + "k-framework", "poetry2nix", "nixpkgs" ] @@ -1157,7 +1034,6 @@ "treefmt-nix_2": { "inputs": { "nixpkgs": [ - "wasm-semantics", "pyk", "poetry2nix", "nixpkgs" @@ -1177,6 +1053,65 @@ "type": "github" } }, + "treefmt-nix_3": { + "inputs": { + "nixpkgs": [ + "wasm-semantics", + "k-framework", + "poetry2nix", + "nixpkgs" + ] + }, + "locked": { + "lastModified": 1697388351, + "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=", + "owner": "numtide", + "repo": "treefmt-nix", + "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "treefmt-nix", + "type": "github" + } + }, + "utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "utils_2": { + "inputs": { + "systems": "systems_6" + }, + "locked": { + "lastModified": 1705309234, + "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, "wasm-semantics": { "inputs": { "flake-utils": [ @@ -1190,17 +1125,11 @@ "k-framework", "nixpkgs" ], - "nixpkgs-pyk": [ - "wasm-semantics", - "pyk", - "nixpkgs" - ], "poetry2nix": [ "wasm-semantics", - "pyk", + "k-framework", "poetry2nix" ], - "pyk": "pyk_2", "rv-utils": [ "wasm-semantics", "k-framework", @@ -1208,16 +1137,16 @@ ] }, "locked": { - "lastModified": 1719501996, - "narHash": "sha256-BCrS904/gfV2Fsihn/yXGtmTFFZfxTQ1m+0ym50RN28=", + "lastModified": 1720692169, + "narHash": "sha256-r8uMESUW5kYlA0XUeZygcpjT/t3LwiOFpvxH/76MPc8=", "owner": "runtimeverification", "repo": "wasm-semantics", - "rev": "b353017e7178731daa12cba75dc81fd69e20a81f", + "rev": "d58b1043fcd3b6589eb106937dd132787e8a2c5d", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.71", + "ref": "v0.1.83", "repo": "wasm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index e09eb322..65115999 100644 --- a/flake.nix +++ b/flake.nix @@ -2,9 +2,9 @@ description = "K Semantics of MultiversX"; inputs = { - wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.71"; - k-framework.url = "github:runtimeverification/k/v7.1.30"; - pyk.url = "github:runtimeverification/k/v7.1.30?dir=pyk"; + wasm-semantics.url = "github:runtimeverification/wasm-semantics/v0.1.83"; + k-framework.url = "github:runtimeverification/k/v7.1.54"; + pyk.url = "github:runtimeverification/k/v7.1.54?dir=pyk"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.url = "github:runtimeverification/rv-nix-tools"; diff --git a/kmultiversx/poetry.lock b/kmultiversx/poetry.lock index 4cde0e50..9533ca62 100644 --- a/kmultiversx/poetry.lock +++ b/kmultiversx/poetry.lock @@ -571,13 +571,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.30" +version = "7.1.54" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.30-py3-none-any.whl", hash = "sha256:7f8de5d3b797593145aa69d92d89ce169e46a1254bb0d48354f1faedaeb1dcdd"}, - {file = "kframework-7.1.30.tar.gz", hash = "sha256:d3a07d7dd8b8af7e3e336254035ec3e08f12002e94d927a5bde2cef2c2b3225a"}, + {file = "kframework-7.1.54-py3-none-any.whl", hash = "sha256:3df4aa7880486f8ea49d2d49ea0d1d11c905e4a8ced3c364fecb6c1e74de16a1"}, + {file = "kframework-7.1.54.tar.gz", hash = "sha256:42c237061f0e6499a2cecbbdde89f50f457f4e7daedc17c31fa66dbf129c2cbd"}, ] [package.dependencies] @@ -996,7 +996,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pykwasm" -version = "0.1.71" +version = "0.1.83" description = "" optional = false python-versions = "^3.10" @@ -1005,15 +1005,15 @@ develop = false [package.dependencies] cytoolz = "^0.12.1" -kframework = "7.1.30" +kframework = "7.1.54" numpy = "^1.24.2" py-wasm = {git = "https://github.com/runtimeverification/py-wasm.git", tag = "0.2.1"} [package.source] type = "git" url = "https://github.com/runtimeverification/wasm-semantics.git" -reference = "v0.1.71" -resolved_reference = "b353017e7178731daa12cba75dc81fd69e20a81f" +reference = "v0.1.83" +resolved_reference = "d58b1043fcd3b6589eb106937dd132787e8a2c5d" subdirectory = "pykwasm" [[package]] @@ -1290,4 +1290,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "1a5d74eb2f5424ebe619cecd794e5bc5f7f4ea7eb3e56625ca0a028b5b72984b" +content-hash = "0bd0c3a47adc855a03683cb562c354b78014c8d0f5b739822269c76dee7497ff" diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index 543761c5..972554ae 100644 --- a/kmultiversx/pyproject.toml +++ b/kmultiversx/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kmultiversx" -version = "0.1.93" +version = "0.1.94" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", @@ -20,7 +20,7 @@ mx-semantics = "kmultiversx.kdist.plugin" [tool.poetry.dependencies] python = "^3.10" -pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.71", subdirectory = "pykwasm" } +pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.83", subdirectory = "pykwasm" } pycryptodomex = "^3.18.0" hypothesis = "^6.82.6" diff --git a/kmultiversx/src/kmultiversx/kasmer.py b/kmultiversx/src/kmultiversx/kasmer.py index 54338928..487ce1cb 100644 --- a/kmultiversx/src/kmultiversx/kasmer.py +++ b/kmultiversx/src/kmultiversx/kasmer.py @@ -428,7 +428,7 @@ def var_to_bytes(var: KVariable) -> KInner: if sort == KSort('Int'): return KApply( - 'Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Endianness_Signedness', # TODO add the 'symbol' attribute in domains.md to have a readable name + 'Int2BytesNoLen', [ var, KApply('bigEndianBytes', ()), diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/async-call.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/async-call.k index f73a4fb3..a842ae33 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/async-call.k +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/async-call.k @@ -53,5 +53,5 @@ module ASYNC-CALL syntax Bool ::= AsyncCall "in" ListAsyncCall [function, total, hook(LIST.in), symbol(_inListAsyncCall_)] syntax Int ::= size(ListAsyncCall) - [function, total, hook(LIST.size), klabel (sizeListAsyncCall), smtlib(smt_seq_len)] + [function, total, hook(LIST.size), symbol(sizeListAsyncCall), smtlib(smt_seq_len)] endmodule diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k index 788695e3..137be6e4 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/int-type.k @@ -5,7 +5,7 @@ module INT-TYPE syntax WrappedInt syntax Int - syntax WrappedInt ::= wrap(Int) [symbol, klabel(wrapInt)] - syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol, klabel(unwrapInt)] + syntax WrappedInt ::= wrap(Int) [symbol(wrapInt)] + syntax Int ::= unwrap(WrappedInt) [function, total, injective, symbol(unwrapInt)] rule unwrap(wrap(A:Int)) => A endmodule diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md index 3dcf880a..31f1d7e3 100644 --- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md +++ b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md @@ -529,7 +529,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions. 0 |-> P - syntax InternalInstr ::= #assert(Int) [symbol, klabel(kasmerAssert)] + syntax InternalInstr ::= #assert(Int) [symbol(kasmerAssert)] // ------------------------------------------------------------------------- rule [kasmerAssert-true]: #assert( I ) => .K ... @@ -550,7 +550,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions. 0 |-> P - syntax IternalInstr ::= #assume(Int) [symbol, klabel(kasmerAssume)] + syntax IternalInstr ::= #assume(Int) [symbol(kasmerAssume)] // ------------------------------------------------------------------------ rule [kasmerAssume-true]: #assume(P) => .K ... @@ -561,7 +561,7 @@ Only the `#kasmerRunner` account can execute these commands/host functions. requires P ==Int 0 syntax InternalInstr ::= "#endFoundryImmediately" - [symbol, klabel(endFoundryImmediately)] + [symbol(endFoundryImmediately)] // ------------------------------------------------------ rule [endFoundryImmediately]: ( diff --git a/package/version b/package/version index 7977b63f..e9822155 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.93 +0.1.94