diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
index bf287acdb..8fd35489f 100644
--- a/.github/workflows/master-push.yml
+++ b/.github/workflows/master-push.yml
@@ -41,7 +41,6 @@ jobs:
matrix:
include:
- runner: normal
- - runner: macos-13
- runner: ARM64
runs-on: ${{ matrix.runner }}
steps:
@@ -53,20 +52,6 @@ jobs:
- name: 'Upgrade bash'
if: ${{ contains(matrix.os, 'macos') }}
run: brew install bash
- - name: 'Install Nix'
- if: ${{ matrix.runner == 'macos-13' }}
- uses: cachix/install-nix-action@v19
- with:
- install_url: https://releases.nixos.org/nix/nix-2.13.3/install
- extra_nix_config: |
- access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
- - name: 'Install Cachix'
- if: ${{ matrix.runner == 'macos-13' }}
- uses: cachix/cachix-action@v12
- with:
- name: k-framework
- signingKey: ${{ secrets.CACHIX_SIGNING_KEY }}
- skipPush: true
- name: 'Build and cache KWASM'
uses: workflow/nix-shell-action@v3.0.3
env:
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index df937cb82..281a80a6a 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -115,7 +115,6 @@ jobs:
matrix:
include:
- runner: normal
- - runner: macos-13
- runner: ARM64
needs: pykwasm-code-quality-checks
runs-on: ${{ matrix.runner }}
@@ -126,21 +125,6 @@ jobs:
with:
# Check out pull request HEAD instead of merge commit.
ref: ${{ github.event.pull_request.head.sha }}
- - name: 'Install Nix'
- if: ${{ matrix.runner == 'macos-13' }}
- uses: cachix/install-nix-action@v25
- with:
- install_url: https://releases.nixos.org/nix/nix-2.19.3/install
- extra_nix_config: |
- access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
- substituters = http://cache.nixos.org https://cache.iog.io
- trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
- - name: 'Install Cachix'
- if: ${{ matrix.runner == 'macos-13' }}
- uses: cachix/cachix-action@v14
- with:
- name: k-framework
- authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
- name: 'Build KWASM'
run: GC_DONT_GC=1 nix build .#kwasm --extra-experimental-features 'nix-command flakes' --print-build-logs
- name: 'Build KWASM-Pyk'
diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml
index 70904a063..566f84162 100644
--- a/.github/workflows/update-version.yml
+++ b/.github/workflows/update-version.yml
@@ -39,15 +39,14 @@ jobs:
authToken: '${{ secrets.CACHIX_PUBLIC_TOKEN }}'
- name: 'Update pyk release tag'
run: |
- K_VERSION=v"$(cat deps/k_release)"
- sed -i 's!pyk = { git = "https://github.com/runtimeverification/k.git", tag="[v0-9\.]*", subdirectory = "pyk" }!pyk = { git = "https://github.com/runtimeverification/k.git", tag="'${K_VERSION}'", subdirectory = "pyk" }!' pykwasm/pyproject.toml
+ K_VERSION=$(cat deps/k_release)
+ sed -i 's!kframework = "[v0-9\.]*"!kframework = "'${K_VERSION}'"!' pykwasm/pyproject.toml
poetry -C pykwasm update
git add pykwasm/ && git commit -m "pykwasm/: sync poetry files ${K_VERSION}" || true
- name: 'Update Nix flake inputs'
run: |
K_VERSION=v"$(cat deps/k_release)"
sed -i 's! k-framework.url = "github:runtimeverification/k/v[[:digit:]]\+\.[[:digit:]]\+\.[[:digit:]]\+"! k-framework.url = "github:runtimeverification/k/'"${K_VERSION}"'"!' flake.nix
- sed -i 's! pyk.url = "github:runtimeverification/k/v[[:digit:]]\+\.[[:digit:]]\+\.[[:digit:]]\+?dir=pyk"! pyk.url = "github:runtimeverification/k/'"${K_VERSION}"'?dir=pyk"!' flake.nix
nix flake update
git add flake.nix flake.lock && git commit -m 'flake.{nix,lock}: update Nix derivations' || true
- name: 'Push updates'
diff --git a/Dockerfile b/Dockerfile
index 651856474..1861696cc 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -26,11 +26,12 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
USER user:user
WORKDIR /home/user
-RUN curl -sSL https://install.python-poetry.org | python3 - \
- && poetry --version
+RUN curl -sSL https://install.python-poetry.org | python3 -
RUN pip3 install --user \
cytoolz \
numpy
-ENV PATH=/home/user/wabt/build:/home/user/.local/bin:$PATH
+ENV PATH=/home/user/.local/bin:$PATH
+
+RUN poetry --version
diff --git a/Makefile b/Makefile
index 9af5e1eb9..3a5ad4abf 100644
--- a/Makefile
+++ b/Makefile
@@ -55,7 +55,7 @@ tests/%.run-term: tests/%
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
tests/%.parse: tests/%
- K_OPTS='-Xmx16G -Xss512m' $(TEST) kast $< kast > $@-out
+ K_OPTS='-Xmx16G -Xss512m' $(TEST) kast --output kore $< > $@-out
rm -rf $@-out
tests/%.prove: tests/%
diff --git a/README.md b/README.md
index 0cd181456..e4955b595 100644
--- a/README.md
+++ b/README.md
@@ -6,8 +6,9 @@ KWasm: Semantics of WebAssembly in K
---
-This repository presents a prototype formal semantics of [WebAssembly].
-It is currently under construction.
+This repository presents the formal semantics of [WebAssembly].
+KWasm is a mature and production-ready semantics for WebAssembly, actively developed and maintained since 2019.
+
For examples of current capabilities, see the unit tests under the `tests/simple` directory.
Repository Structure
diff --git a/deps/k_release b/deps/k_release
index 45158c60d..d40142978 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-7.0.106
+7.1.191
diff --git a/flake.lock b/flake.lock
index 50867c2fa..76846844b 100644
--- a/flake.lock
+++ b/flake.lock
@@ -18,7 +18,7 @@
},
"flake-utils": {
"inputs": {
- "systems": "systems"
+ "systems": "systems_2"
},
"locked": {
"lastModified": 1710146030,
@@ -34,24 +34,6 @@
"type": "github"
}
},
- "flake-utils_2": {
- "inputs": {
- "systems": "systems_2"
- },
- "locked": {
- "lastModified": 1694529238,
- "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
- "owner": "numtide",
- "repo": "flake-utils",
- "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
- "type": "github"
- },
- "original": {
- "owner": "numtide",
- "repo": "flake-utils",
- "type": "github"
- }
- },
"fmt-src": {
"flake": false,
"locked": {
@@ -73,26 +55,29 @@
"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": 1717048155,
- "narHash": "sha256-HHrXt2UoG1RbKmAGmOroQJjUbyiE+6c1dJxqoIfp3H0=",
+ "lastModified": 1733283993,
+ "narHash": "sha256-CK126KzmZQfPqqn0SFba1vg4DL/V/13dsjcFareE8Lo=",
"owner": "runtimeverification",
"repo": "haskell-backend",
- "rev": "b6ab7a9054ae900c97c48e61027fd602dbd2acb8",
+ "rev": "1b6cacb3eab29c7e449b2d255321c3ed348f4229",
"type": "github"
},
"original": {
"owner": "runtimeverification",
+ "ref": "v0.1.104",
"repo": "haskell-backend",
- "rev": "b6ab7a9054ae900c97c48e61027fd602dbd2acb8",
"type": "github"
}
},
@@ -115,7 +100,11 @@
},
"k-framework": {
"inputs": {
- "flake-utils": "flake-utils",
+ "flake-utils": [
+ "k-framework",
+ "llvm-backend",
+ "utils"
+ ],
"haskell-backend": "haskell-backend",
"llvm-backend": "llvm-backend",
"nixpkgs": [
@@ -123,19 +112,24 @@
"llvm-backend",
"nixpkgs"
],
- "rv-utils": "rv-utils_3"
+ "poetry2nix": "poetry2nix",
+ "rv-utils": [
+ "k-framework",
+ "llvm-backend",
+ "rv-utils"
+ ]
},
"locked": {
- "lastModified": 1717398151,
- "narHash": "sha256-6xKGH3t5ePt7CZPYACGpwx0VOxOQ6L8Wk2Vlcafui88=",
+ "lastModified": 1734443427,
+ "narHash": "sha256-IVE4m5PzItHrzJrEh5JOaP3WEzkXCmCj4FzclvkkTi0=",
"owner": "runtimeverification",
"repo": "k",
- "rev": "9100689e357a7e5820362869a73684468ef9c91b",
+ "rev": "06a03e825b9ca8ef030e4b9014c2a0767cccdf5a",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v7.0.106",
+ "ref": "v7.1.191",
"repo": "k",
"type": "github"
}
@@ -153,23 +147,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": 1716543761,
- "narHash": "sha256-YQIrz7KjDiwLtHMzRYxzt1+rcCUdeGDmBQl+zWOq5us=",
+ "lastModified": 1730229432,
+ "narHash": "sha256-2Y4U7TCmSf9NAZCBmvXiHLOXrHxpiRgIpw5ERYDdNSM=",
"owner": "runtimeverification",
"repo": "llvm-backend",
- "rev": "0b0bdaeaf5acfed9034c40bec68b285dc5fac4dc",
+ "rev": "d5eab4b0f0e610bc60843ebb482f79c043b92702",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v0.1.31",
+ "ref": "v0.1.103",
"repo": "llvm-backend",
"type": "github"
}
@@ -177,17 +168,17 @@
"nix-github-actions": {
"inputs": {
"nixpkgs": [
- "pyk",
+ "k-framework",
"poetry2nix",
"nixpkgs"
]
},
"locked": {
- "lastModified": 1693660503,
- "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=",
+ "lastModified": 1703863825,
+ "narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=",
"owner": "nix-community",
"repo": "nix-github-actions",
- "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0",
+ "rev": "5163432afc817cf8bd1f031418d1869e4c9d5547",
"type": "github"
},
"original": {
@@ -212,76 +203,30 @@
"type": "github"
}
},
- "nixpkgs_2": {
- "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_3": {
- "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_4": {
- "locked": {
- "lastModified": 1698675399,
- "narHash": "sha256-nj+LNEeVXGP31vxoL3x7HW7+oEiyoLVDqwMg30yFBMA=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "7378978469efa3b2b2f97d645a2a0b0e2447da2b",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
"poetry2nix": {
"inputs": {
- "flake-utils": "flake-utils_2",
+ "flake-utils": "flake-utils",
"nix-github-actions": "nix-github-actions",
"nixpkgs": [
- "pyk",
+ "k-framework",
+ "llvm-backend",
"nixpkgs"
],
"systems": "systems_3",
"treefmt-nix": "treefmt-nix"
},
"locked": {
- "lastModified": 1698640399,
- "narHash": "sha256-mXzyx79/iFLZ0UDuSkqgFfejYRcSJfsCnJ9WlMusaI0=",
+ "lastModified": 1725253878,
+ "narHash": "sha256-HwXut4WbOUAjmybhui2eNSE6+Wb0nigYgDzBBOZaPG4=",
"owner": "nix-community",
"repo": "poetry2nix",
- "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c",
+ "rev": "0d3fad5740d892487805cd2d60d8e4ed828486e9",
"type": "github"
},
"original": {
"owner": "nix-community",
+ "ref": "2024.9.219347",
"repo": "poetry2nix",
- "rev": "626111646fe236cb1ddc8191a48c75e072a82b7c",
"type": "github"
}
},
@@ -302,33 +247,6 @@
"type": "github"
}
},
- "pyk": {
- "inputs": {
- "flake-utils": [
- "pyk",
- "poetry2nix",
- "flake-utils"
- ],
- "nixpkgs": "nixpkgs_4",
- "poetry2nix": "poetry2nix"
- },
- "locked": {
- "dir": "pyk",
- "lastModified": 1717398151,
- "narHash": "sha256-6xKGH3t5ePt7CZPYACGpwx0VOxOQ6L8Wk2Vlcafui88=",
- "owner": "runtimeverification",
- "repo": "k",
- "rev": "9100689e357a7e5820362869a73684468ef9c91b",
- "type": "github"
- },
- "original": {
- "dir": "pyk",
- "owner": "runtimeverification",
- "ref": "v7.0.106",
- "repo": "k",
- "type": "github"
- }
- },
"rapidjson-src": {
"flake": false,
"locked": {
@@ -357,15 +275,10 @@
"k-framework",
"nixpkgs"
],
- "nixpkgs-pyk": [
- "pyk",
- "nixpkgs"
- ],
"poetry2nix": [
- "pyk",
+ "k-framework",
"poetry2nix"
],
- "pyk": "pyk",
"rv-utils": [
"k-framework",
"rv-utils"
@@ -390,42 +303,6 @@
"type": "github"
}
},
- "rv-utils_2": {
- "inputs": {
- "nixpkgs": "nixpkgs_2"
- },
- "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_3": {
- "inputs": {
- "nixpkgs": "nixpkgs_3"
- },
- "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,
@@ -488,17 +365,17 @@
"treefmt-nix": {
"inputs": {
"nixpkgs": [
- "pyk",
+ "k-framework",
"poetry2nix",
"nixpkgs"
]
},
"locked": {
- "lastModified": 1697388351,
- "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=",
+ "lastModified": 1719749022,
+ "narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=",
"owner": "numtide",
"repo": "treefmt-nix",
- "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a",
+ "rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd",
"type": "github"
},
"original": {
@@ -507,19 +384,37 @@
"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"
+ }
+ },
"z3": {
"flake": false,
"locked": {
- "lastModified": 1674011426,
- "narHash": "sha256-7cuUf29TMpX62PwO1ab3ZuzmzlcrRjTKB1CyXnYgYus=",
+ "lastModified": 1709835916,
+ "narHash": "sha256-MIbP3QgKIGF/qUMTupaO7xD46LbmH69kF/394Sajhkg=",
"owner": "Z3Prover",
"repo": "z3",
- "rev": "3012293c35eadbfd73e5b94adbe50b0cc44ffb83",
+ "rev": "3049f578a8f98a0b0992eca193afe57a73b30ca3",
"type": "github"
},
"original": {
"owner": "Z3Prover",
- "ref": "z3-4.12.1",
+ "ref": "z3-4.13.0",
"repo": "z3",
"type": "github"
}
diff --git a/flake.nix b/flake.nix
index 4a73f0f08..1eb6fc60a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,17 +2,14 @@
description = "K Semantics of WebAssembly";
inputs = {
- k-framework.url = "github:runtimeverification/k/v7.0.106";
+ k-framework.url = "github:runtimeverification/k/v7.1.191";
nixpkgs.follows = "k-framework/nixpkgs";
flake-utils.follows = "k-framework/flake-utils";
rv-utils.follows = "k-framework/rv-utils";
- pyk.url = "github:runtimeverification/k/v7.0.106?dir=pyk";
- nixpkgs-pyk.follows = "pyk/nixpkgs";
- poetry2nix.follows = "pyk/poetry2nix";
+ poetry2nix.follows = "k-framework/poetry2nix";
};
- outputs =
- { self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, ... }@inputs:
+ outputs = { self, k-framework, nixpkgs, flake-utils, rv-utils, ... }@inputs:
let
overlay = (final: prev:
let
@@ -21,29 +18,14 @@
"flake.lock"
./.gitignore
] ./.);
-
+ poetry2nix = inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = prev; };
version = self.rev or "dirty";
-
- nixpkgs-pyk = import inputs.nixpkgs-pyk {
- system = prev.system;
- overlays = [ pyk.overlay ];
- };
-
- python310-pyk = nixpkgs-pyk.python310;
-
- poetry2nix = inputs.poetry2nix.lib.mkPoetry2Nix { pkgs = nixpkgs-pyk; };
in {
- pyk = pyk.packages.${prev.system}.pyk;
-
kwasm = prev.stdenv.mkDerivation {
pname = "kwasm";
inherit src version;
- buildInputs = with final; [
- k-framework.packages.${system}.k
- final.kwasm-pyk
- python310-pyk
- ];
+ buildInputs = with prev; [ k final.kwasm-pyk python310 ];
nativeBuildInputs = [ prev.makeWrapper ];
@@ -59,40 +41,24 @@
cp -r ./kdist-*/* $out/
mkdir -p $out/bin
makeWrapper ${final.kwasm-pyk}/bin/kwasm $out/bin/kwasm \
- --prefix PATH : ${
- prev.lib.makeBinPath [
- prev.which
- k-framework.packages.${prev.system}.k
- ]
- } \
+ --prefix PATH : ${prev.lib.makeBinPath [ prev.which prev.k ]} \
--set KDIST_DIR $out
'';
};
kwasm-pyk = poetry2nix.mkPoetryApplication {
- python = nixpkgs-pyk.python310;
+ python = prev.python310;
projectDir = ./pykwasm;
- src = rv-utils.lib.mkPykAppSrc {
- pkgs = import nixpkgs { system = prev.system; };
- src = ./pykwasm;
- cleaner = poetry2nix.cleanPythonSources;
- };
+
overrides = poetry2nix.overrides.withDefaults
- (finalPython: prevPython: {
- pyk = nixpkgs-pyk.pyk-python310;
- xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs
- (old: {
- propagatedBuildInputs = (old.propagatedBuildInputs or [ ])
- ++ [ finalPython.poetry ];
+ (finalPython: prevPython: {
+ kframework = prev.pyk-python310;
+ py-wasm = prevPython.py-wasm.overridePythonAttrs (old: {
+ buildInputs = (old.buildInputs or [ ])
+ ++ [ prevPython.setuptools ];
});
- py-wasm = prevPython.py-wasm.overridePythonAttrs
- (
- old: {
- buildInputs = (old.buildInputs or [ ]) ++ [ prevPython.setuptools ];
- }
- );
});
- groups = [ ];
+
checkGroups = [ ];
};
@@ -102,18 +68,13 @@
pname = "kwasm-test";
src = final.kwasm.src;
- buildInputs = with final; [
- kwasm
- kwasm-pyk
- which
- git
- ];
+ buildInputs = with final; [ kwasm kwasm-pyk which git ];
- patchPhase = ''
+ patchPhase = with final; ''
substituteInPlace Makefile \
- --replace-fail '$(TEST)' '${final.kwasm}/bin/kwasm' \
- --replace-fail '$(KDIST)' '${nixpkgs-pyk.pyk-python310}/bin/kdist' \
- --replace-fail '$(SOURCE_DIR)' '${final.kwasm}/wasm-semantics/source'
+ --replace-fail '$(TEST)' '${kwasm}/bin/kwasm' \
+ --replace-fail '$(KDIST)' '${pyk-python310}/bin/kdist' \
+ --replace-fail '$(SOURCE_DIR)' '${kwasm}/wasm-semantics/source'
'';
buildPhase = ''
@@ -138,14 +99,14 @@
let
pkgs = import nixpkgs {
inherit system;
- overlays = [ overlay ];
+ overlays = [ k-framework.overlay overlay ];
};
in {
packages = rec {
inherit (pkgs) kwasm kwasm-pyk kwasm-test;
default = kwasm;
};
- }) // {
- overlays.default = overlay;
- };
+ }) // {
+ overlays.default = overlay;
+ };
}
diff --git a/media/201903-report-chalmers.md b/media/201903-report-chalmers.md
index 10ad7770e..886c3402b 100644
--- a/media/201903-report-chalmers.md
+++ b/media/201903-report-chalmers.md
@@ -800,7 +800,7 @@ This is the full definition of the `(memory.grow)` operation:
#then SIZE
#else -1
#fi ...
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
ADDR
MAX
diff --git a/media/memory-demo/memory-spec.k b/media/memory-demo/memory-spec.k
index 3c12d7cdd..e8dc009c5 100644
--- a/media/memory-demo/memory-spec.k
+++ b/media/memory-demo/memory-spec.k
@@ -2,14 +2,14 @@ module MEMORY-SPEC
imports WASM
rule ( memory.size ) => (i32.const SZ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
rule (memory.grow (i32.const X)) => (i32.const SZ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ => (SZ +Int X)
@@ -21,7 +21,7 @@ module MEMORY-SPEC
andBool SZ >=Int 0
rule (memory.grow (i32.const X)) => (i32.const -1) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
diff --git a/media/memory-demo/wasm.k b/media/memory-demo/wasm.k
index d17cd5707..4d3e548da 100644
--- a/media/memory-demo/wasm.k
+++ b/media/memory-demo/wasm.k
@@ -104,7 +104,7 @@ endmodule
false
rule (( memory ) ~> ELSE) => ELSE
- .MapIntToInt => wrap(0) Int2Int|-> wrap(NEXT)
+ .Map => 0 |-> NEXT
NEXT => NEXT +Int 1
(.Bag =>
@@ -118,7 +118,7 @@ endmodule
syntax Instr ::= "(" "memory.size" ")"
// --------------------------------------
rule ( memory.size ) => ( i32.const SZ ) ...
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ
@@ -131,7 +131,7 @@ endmodule
rule (memory.grow I:Instr) => I ~> (memory.grow) ...
rule (memory.grow) => (i32.const SZ) ...
< i32 > V : S => S
- wrap(0) Int2Int|-> wrap(A)
+ 0 |-> A
A
SZ => SZ +Int V
diff --git a/package/version b/package/version
index 09d8256ac..1fcba8fa1 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.59
+0.1.118
diff --git a/pykwasm/poetry.lock b/pykwasm/poetry.lock
index 20a6eccb2..923e634c6 100644
--- a/pykwasm/poetry.lock
+++ b/pykwasm/poetry.lock
@@ -1,23 +1,23 @@
-# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand.
+# This file is automatically @generated by Poetry 1.8.5 and should not be changed by hand.
[[package]]
name = "attrs"
-version = "23.2.0"
+version = "24.3.0"
description = "Classes Without Boilerplate"
optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
files = [
- {file = "attrs-23.2.0-py3-none-any.whl", hash = "sha256:99b87a485a5820b23b879f04c2305b44b951b502fd64be915879d77a7e8fc6f1"},
- {file = "attrs-23.2.0.tar.gz", hash = "sha256:935dc3b529c262f6cf76e50877d35a4bd3c1de194fd41f47a2b7ae8f19971f30"},
+ {file = "attrs-24.3.0-py3-none-any.whl", hash = "sha256:ac96cd038792094f438ad1f6ff80837353805ac950cd2aa0e0625ef19850c308"},
+ {file = "attrs-24.3.0.tar.gz", hash = "sha256:8f5c07333d543103541ba7be0e2ce16eeee8130cb0b3f9238ab904ce1e85baff"},
]
[package.extras]
-cov = ["attrs[tests]", "coverage[toml] (>=5.3)"]
-dev = ["attrs[tests]", "pre-commit"]
-docs = ["furo", "myst-parser", "sphinx", "sphinx-notfound-page", "sphinxcontrib-towncrier", "towncrier", "zope-interface"]
-tests = ["attrs[tests-no-zope]", "zope-interface"]
-tests-mypy = ["mypy (>=1.6)", "pytest-mypy-plugins"]
-tests-no-zope = ["attrs[tests-mypy]", "cloudpickle", "hypothesis", "pympler", "pytest (>=4.3.0)", "pytest-xdist[psutil]"]
+benchmark = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-codspeed", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
+cov = ["cloudpickle", "coverage[toml] (>=5.3)", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
+dev = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pre-commit-uv", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
+docs = ["cogapp", "furo", "myst-parser", "sphinx", "sphinx-notfound-page", "sphinxcontrib-towncrier", "towncrier (<24.7)"]
+tests = ["cloudpickle", "hypothesis", "mypy (>=1.11.1)", "pympler", "pytest (>=4.3.0)", "pytest-mypy-plugins", "pytest-xdist[psutil]"]
+tests-mypy = ["mypy (>=1.11.1)", "pytest-mypy-plugins"]
[[package]]
name = "autoflake"
@@ -36,33 +36,33 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""}
[[package]]
name = "black"
-version = "24.4.2"
+version = "24.10.0"
description = "The uncompromising code formatter."
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "black-24.4.2-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:dd1b5a14e417189db4c7b64a6540f31730713d173f0b63e55fabd52d61d8fdce"},
- {file = "black-24.4.2-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:8e537d281831ad0e71007dcdcbe50a71470b978c453fa41ce77186bbe0ed6021"},
- {file = "black-24.4.2-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:eaea3008c281f1038edb473c1aa8ed8143a5535ff18f978a318f10302b254063"},
- {file = "black-24.4.2-cp310-cp310-win_amd64.whl", hash = "sha256:7768a0dbf16a39aa5e9a3ded568bb545c8c2727396d063bbaf847df05b08cd96"},
- {file = "black-24.4.2-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:257d724c2c9b1660f353b36c802ccece186a30accc7742c176d29c146df6e474"},
- {file = "black-24.4.2-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:bdde6f877a18f24844e381d45e9947a49e97933573ac9d4345399be37621e26c"},
- {file = "black-24.4.2-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e151054aa00bad1f4e1f04919542885f89f5f7d086b8a59e5000e6c616896ffb"},
- {file = "black-24.4.2-cp311-cp311-win_amd64.whl", hash = "sha256:7e122b1c4fb252fd85df3ca93578732b4749d9be076593076ef4d07a0233c3e1"},
- {file = "black-24.4.2-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:accf49e151c8ed2c0cdc528691838afd217c50412534e876a19270fea1e28e2d"},
- {file = "black-24.4.2-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:88c57dc656038f1ab9f92b3eb5335ee9b021412feaa46330d5eba4e51fe49b04"},
- {file = "black-24.4.2-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:be8bef99eb46d5021bf053114442914baeb3649a89dc5f3a555c88737e5e98fc"},
- {file = "black-24.4.2-cp312-cp312-win_amd64.whl", hash = "sha256:415e686e87dbbe6f4cd5ef0fbf764af7b89f9057b97c908742b6008cc554b9c0"},
- {file = "black-24.4.2-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:bf10f7310db693bb62692609b397e8d67257c55f949abde4c67f9cc574492cc7"},
- {file = "black-24.4.2-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:98e123f1d5cfd42f886624d84464f7756f60ff6eab89ae845210631714f6db94"},
- {file = "black-24.4.2-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:48a85f2cb5e6799a9ef05347b476cce6c182d6c71ee36925a6c194d074336ef8"},
- {file = "black-24.4.2-cp38-cp38-win_amd64.whl", hash = "sha256:b1530ae42e9d6d5b670a34db49a94115a64596bc77710b1d05e9801e62ca0a7c"},
- {file = "black-24.4.2-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:37aae07b029fa0174d39daf02748b379399b909652a806e5708199bd93899da1"},
- {file = "black-24.4.2-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:da33a1a5e49c4122ccdfd56cd021ff1ebc4a1ec4e2d01594fef9b6f267a9e741"},
- {file = "black-24.4.2-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ef703f83fc32e131e9bcc0a5094cfe85599e7109f896fe8bc96cc402f3eb4b6e"},
- {file = "black-24.4.2-cp39-cp39-win_amd64.whl", hash = "sha256:b9176b9832e84308818a99a561e90aa479e73c523b3f77afd07913380ae2eab7"},
- {file = "black-24.4.2-py3-none-any.whl", hash = "sha256:d36ed1124bb81b32f8614555b34cc4259c3fbc7eec17870e8ff8ded335b58d8c"},
- {file = "black-24.4.2.tar.gz", hash = "sha256:c872b53057f000085da66a19c55d68f6f8ddcac2642392ad3a355878406fbd4d"},
+ {file = "black-24.10.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:e6668650ea4b685440857138e5fe40cde4d652633b1bdffc62933d0db4ed9812"},
+ {file = "black-24.10.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:1c536fcf674217e87b8cc3657b81809d3c085d7bf3ef262ead700da345bfa6ea"},
+ {file = "black-24.10.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:649fff99a20bd06c6f727d2a27f401331dc0cc861fb69cde910fe95b01b5928f"},
+ {file = "black-24.10.0-cp310-cp310-win_amd64.whl", hash = "sha256:fe4d6476887de70546212c99ac9bd803d90b42fc4767f058a0baa895013fbb3e"},
+ {file = "black-24.10.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:5a2221696a8224e335c28816a9d331a6c2ae15a2ee34ec857dcf3e45dbfa99ad"},
+ {file = "black-24.10.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:f9da3333530dbcecc1be13e69c250ed8dfa67f43c4005fb537bb426e19200d50"},
+ {file = "black-24.10.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:4007b1393d902b48b36958a216c20c4482f601569d19ed1df294a496eb366392"},
+ {file = "black-24.10.0-cp311-cp311-win_amd64.whl", hash = "sha256:394d4ddc64782e51153eadcaaca95144ac4c35e27ef9b0a42e121ae7e57a9175"},
+ {file = "black-24.10.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:b5e39e0fae001df40f95bd8cc36b9165c5e2ea88900167bddf258bacef9bbdc3"},
+ {file = "black-24.10.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:d37d422772111794b26757c5b55a3eade028aa3fde43121ab7b673d050949d65"},
+ {file = "black-24.10.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:14b3502784f09ce2443830e3133dacf2c0110d45191ed470ecb04d0f5f6fcb0f"},
+ {file = "black-24.10.0-cp312-cp312-win_amd64.whl", hash = "sha256:30d2c30dc5139211dda799758559d1b049f7f14c580c409d6ad925b74a4208a8"},
+ {file = "black-24.10.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:1cbacacb19e922a1d75ef2b6ccaefcd6e93a2c05ede32f06a21386a04cedb981"},
+ {file = "black-24.10.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:1f93102e0c5bb3907451063e08b9876dbeac810e7da5a8bfb7aeb5a9ef89066b"},
+ {file = "black-24.10.0-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ddacb691cdcdf77b96f549cf9591701d8db36b2f19519373d60d31746068dbf2"},
+ {file = "black-24.10.0-cp313-cp313-win_amd64.whl", hash = "sha256:680359d932801c76d2e9c9068d05c6b107f2584b2a5b88831c83962eb9984c1b"},
+ {file = "black-24.10.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:17374989640fbca88b6a448129cd1745c5eb8d9547b464f281b251dd00155ccd"},
+ {file = "black-24.10.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:63f626344343083322233f175aaf372d326de8436f5928c042639a4afbbf1d3f"},
+ {file = "black-24.10.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ccfa1d0cb6200857f1923b602f978386a3a2758a65b52e0950299ea014be6800"},
+ {file = "black-24.10.0-cp39-cp39-win_amd64.whl", hash = "sha256:2cd9c95431d94adc56600710f8813ee27eea544dd118d45896bb734e9d7a0dc7"},
+ {file = "black-24.10.0-py3-none-any.whl", hash = "sha256:3bb2b7a1f7b685f85b11fed1ef10f8a9148bceb49853e47a294a3dd963c1dd7d"},
+ {file = "black-24.10.0.tar.gz", hash = "sha256:846ea64c97afe3bc677b761787993be4991810ecc7a4a937816dd6bddedc4875"},
]
[package.dependencies]
@@ -76,7 +76,7 @@ typing-extensions = {version = ">=4.0.1", markers = "python_version < \"3.11\""}
[package.extras]
colorama = ["colorama (>=0.4.3)"]
-d = ["aiohttp (>=3.7.4)", "aiohttp (>=3.7.4,!=3.9.0)"]
+d = ["aiohttp (>=3.10)"]
jupyter = ["ipython (>=7.8.0)", "tokenize-rt (>=3.2.0)"]
uvloop = ["uvloop (>=0.15.2)"]
@@ -107,25 +107,27 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""}
[[package]]
name = "cmd2"
-version = "2.4.3"
+version = "2.5.7"
description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python"
optional = false
-python-versions = ">=3.6"
+python-versions = ">=3.8"
files = [
- {file = "cmd2-2.4.3-py3-none-any.whl", hash = "sha256:f1988ff2fff0ed812a2d25218a081b0fa0108d45b48ba2a9272bb98091b654e6"},
- {file = "cmd2-2.4.3.tar.gz", hash = "sha256:71873c11f72bd19e2b1db578214716f0d4f7c8fa250093c601265a9a717dee52"},
+ {file = "cmd2-2.5.7-py3-none-any.whl", hash = "sha256:7e5856fd1a75716288d4638e68946f9697404f377dfdeeddc19045c7012de9b7"},
+ {file = "cmd2-2.5.7.tar.gz", hash = "sha256:0219e2bb75075fa16deffb88edf86efdd2a87439d1fa7b94fdea4b929a3dc914"},
]
[package.dependencies]
-attrs = ">=16.3.0"
-pyperclip = ">=1.6"
-pyreadline3 = {version = "*", markers = "sys_platform == \"win32\""}
-wcwidth = ">=0.1.7"
+gnureadline = {version = "*", markers = "platform_system == \"Darwin\""}
+pyperclip = "*"
+pyreadline3 = {version = "*", markers = "platform_system == \"Windows\""}
+wcwidth = "*"
[package.extras]
-dev = ["codecov", "doc8", "flake8", "invoke", "mypy", "nox", "pytest (>=4.6)", "pytest-cov", "pytest-mock", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme", "twine (>=1.11)"]
-test = ["codecov", "coverage", "gnureadline", "pytest (>=4.6)", "pytest-cov", "pytest-mock"]
-validate = ["flake8", "mypy", "types-pkg-resources"]
+build = ["build", "setuptools", "setuptools-scm"]
+dev = ["codecov", "doc8", "invoke", "mypy", "pytest", "pytest-cov", "pytest-mock", "ruff", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme", "twine"]
+docs = ["setuptools", "setuptools_scm", "sphinx", "sphinx-autobuild", "sphinx-rtd-theme"]
+test = ["codecov", "coverage", "pytest", "pytest-cov", "pytest-mock"]
+validate = ["mypy", "ruff", "types-setuptools"]
[[package]]
name = "colorama"
@@ -157,63 +159,73 @@ cron = ["capturer (>=2.4)"]
[[package]]
name = "coverage"
-version = "7.5.3"
+version = "7.6.9"
description = "Code coverage measurement for Python"
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "coverage-7.5.3-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:a6519d917abb15e12380406d721e37613e2a67d166f9fb7e5a8ce0375744cd45"},
- {file = "coverage-7.5.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:aea7da970f1feccf48be7335f8b2ca64baf9b589d79e05b9397a06696ce1a1ec"},
- {file = "coverage-7.5.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:923b7b1c717bd0f0f92d862d1ff51d9b2b55dbbd133e05680204465f454bb286"},
- {file = "coverage-7.5.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:62bda40da1e68898186f274f832ef3e759ce929da9a9fd9fcf265956de269dbc"},
- {file = "coverage-7.5.3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d8b7339180d00de83e930358223c617cc343dd08e1aa5ec7b06c3a121aec4e1d"},
- {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:25a5caf742c6195e08002d3b6c2dd6947e50efc5fc2c2205f61ecb47592d2d83"},
- {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:05ac5f60faa0c704c0f7e6a5cbfd6f02101ed05e0aee4d2822637a9e672c998d"},
- {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:239a4e75e09c2b12ea478d28815acf83334d32e722e7433471fbf641c606344c"},
- {file = "coverage-7.5.3-cp310-cp310-win32.whl", hash = "sha256:a5812840d1d00eafae6585aba38021f90a705a25b8216ec7f66aebe5b619fb84"},
- {file = "coverage-7.5.3-cp310-cp310-win_amd64.whl", hash = "sha256:33ca90a0eb29225f195e30684ba4a6db05dbef03c2ccd50b9077714c48153cac"},
- {file = "coverage-7.5.3-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:f81bc26d609bf0fbc622c7122ba6307993c83c795d2d6f6f6fd8c000a770d974"},
- {file = "coverage-7.5.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:7cec2af81f9e7569280822be68bd57e51b86d42e59ea30d10ebdbb22d2cb7232"},
- {file = "coverage-7.5.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:55f689f846661e3f26efa535071775d0483388a1ccfab899df72924805e9e7cd"},
- {file = "coverage-7.5.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:50084d3516aa263791198913a17354bd1dc627d3c1639209640b9cac3fef5807"},
- {file = "coverage-7.5.3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:341dd8f61c26337c37988345ca5c8ccabeff33093a26953a1ac72e7d0103c4fb"},
- {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:ab0b028165eea880af12f66086694768f2c3139b2c31ad5e032c8edbafca6ffc"},
- {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:5bc5a8c87714b0c67cfeb4c7caa82b2d71e8864d1a46aa990b5588fa953673b8"},
- {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:38a3b98dae8a7c9057bd91fbf3415c05e700a5114c5f1b5b0ea5f8f429ba6614"},
- {file = "coverage-7.5.3-cp311-cp311-win32.whl", hash = "sha256:fcf7d1d6f5da887ca04302db8e0e0cf56ce9a5e05f202720e49b3e8157ddb9a9"},
- {file = "coverage-7.5.3-cp311-cp311-win_amd64.whl", hash = "sha256:8c836309931839cca658a78a888dab9676b5c988d0dd34ca247f5f3e679f4e7a"},
- {file = "coverage-7.5.3-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:296a7d9bbc598e8744c00f7a6cecf1da9b30ae9ad51c566291ff1314e6cbbed8"},
- {file = "coverage-7.5.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:34d6d21d8795a97b14d503dcaf74226ae51eb1f2bd41015d3ef332a24d0a17b3"},
- {file = "coverage-7.5.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8e317953bb4c074c06c798a11dbdd2cf9979dbcaa8ccc0fa4701d80042d4ebf1"},
- {file = "coverage-7.5.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:705f3d7c2b098c40f5b81790a5fedb274113373d4d1a69e65f8b68b0cc26f6db"},
- {file = "coverage-7.5.3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b1196e13c45e327d6cd0b6e471530a1882f1017eb83c6229fc613cd1a11b53cd"},
- {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:015eddc5ccd5364dcb902eaecf9515636806fa1e0d5bef5769d06d0f31b54523"},
- {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:fd27d8b49e574e50caa65196d908f80e4dff64d7e592d0c59788b45aad7e8b35"},
- {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:33fc65740267222fc02975c061eb7167185fef4cc8f2770267ee8bf7d6a42f84"},
- {file = "coverage-7.5.3-cp312-cp312-win32.whl", hash = "sha256:7b2a19e13dfb5c8e145c7a6ea959485ee8e2204699903c88c7d25283584bfc08"},
- {file = "coverage-7.5.3-cp312-cp312-win_amd64.whl", hash = "sha256:0bbddc54bbacfc09b3edaec644d4ac90c08ee8ed4844b0f86227dcda2d428fcb"},
- {file = "coverage-7.5.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:f78300789a708ac1f17e134593f577407d52d0417305435b134805c4fb135adb"},
- {file = "coverage-7.5.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:b368e1aee1b9b75757942d44d7598dcd22a9dbb126affcbba82d15917f0cc155"},
- {file = "coverage-7.5.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f836c174c3a7f639bded48ec913f348c4761cbf49de4a20a956d3431a7c9cb24"},
- {file = "coverage-7.5.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:244f509f126dc71369393ce5fea17c0592c40ee44e607b6d855e9c4ac57aac98"},
- {file = "coverage-7.5.3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c4c2872b3c91f9baa836147ca33650dc5c172e9273c808c3c3199c75490e709d"},
- {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:dd4b3355b01273a56b20c219e74e7549e14370b31a4ffe42706a8cda91f19f6d"},
- {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:f542287b1489c7a860d43a7d8883e27ca62ab84ca53c965d11dac1d3a1fab7ce"},
- {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:75e3f4e86804023e991096b29e147e635f5e2568f77883a1e6eed74512659ab0"},
- {file = "coverage-7.5.3-cp38-cp38-win32.whl", hash = "sha256:c59d2ad092dc0551d9f79d9d44d005c945ba95832a6798f98f9216ede3d5f485"},
- {file = "coverage-7.5.3-cp38-cp38-win_amd64.whl", hash = "sha256:fa21a04112c59ad54f69d80e376f7f9d0f5f9123ab87ecd18fbb9ec3a2beed56"},
- {file = "coverage-7.5.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:f5102a92855d518b0996eb197772f5ac2a527c0ec617124ad5242a3af5e25f85"},
- {file = "coverage-7.5.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:d1da0a2e3b37b745a2b2a678a4c796462cf753aebf94edcc87dcc6b8641eae31"},
- {file = "coverage-7.5.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8383a6c8cefba1b7cecc0149415046b6fc38836295bc4c84e820872eb5478b3d"},
- {file = "coverage-7.5.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9aad68c3f2566dfae84bf46295a79e79d904e1c21ccfc66de88cd446f8686341"},
- {file = "coverage-7.5.3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2e079c9ec772fedbade9d7ebc36202a1d9ef7291bc9b3a024ca395c4d52853d7"},
- {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:bde997cac85fcac227b27d4fb2c7608a2c5f6558469b0eb704c5726ae49e1c52"},
- {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:990fb20b32990b2ce2c5f974c3e738c9358b2735bc05075d50a6f36721b8f303"},
- {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:3d5a67f0da401e105753d474369ab034c7bae51a4c31c77d94030d59e41df5bd"},
- {file = "coverage-7.5.3-cp39-cp39-win32.whl", hash = "sha256:e08c470c2eb01977d221fd87495b44867a56d4d594f43739a8028f8646a51e0d"},
- {file = "coverage-7.5.3-cp39-cp39-win_amd64.whl", hash = "sha256:1d2a830ade66d3563bb61d1e3c77c8def97b30ed91e166c67d0632c018f380f0"},
- {file = "coverage-7.5.3-pp38.pp39.pp310-none-any.whl", hash = "sha256:3538d8fb1ee9bdd2e2692b3b18c22bb1c19ffbefd06880f5ac496e42d7bb3884"},
- {file = "coverage-7.5.3.tar.gz", hash = "sha256:04aefca5190d1dc7a53a4c1a5a7f8568811306d7a8ee231c42fb69215571944f"},
+ {file = "coverage-7.6.9-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:85d9636f72e8991a1706b2b55b06c27545448baf9f6dbf51c4004609aacd7dcb"},
+ {file = "coverage-7.6.9-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:608a7fd78c67bee8936378299a6cb9f5149bb80238c7a566fc3e6717a4e68710"},
+ {file = "coverage-7.6.9-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:96d636c77af18b5cb664ddf12dab9b15a0cfe9c0bde715da38698c8cea748bfa"},
+ {file = "coverage-7.6.9-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:d75cded8a3cff93da9edc31446872d2997e327921d8eed86641efafd350e1df1"},
+ {file = "coverage-7.6.9-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f7b15f589593110ae767ce997775d645b47e5cbbf54fd322f8ebea6277466cec"},
+ {file = "coverage-7.6.9-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:44349150f6811b44b25574839b39ae35291f6496eb795b7366fef3bd3cf112d3"},
+ {file = "coverage-7.6.9-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:d891c136b5b310d0e702e186d70cd16d1119ea8927347045124cb286b29297e5"},
+ {file = "coverage-7.6.9-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:db1dab894cc139f67822a92910466531de5ea6034ddfd2b11c0d4c6257168073"},
+ {file = "coverage-7.6.9-cp310-cp310-win32.whl", hash = "sha256:41ff7b0da5af71a51b53f501a3bac65fb0ec311ebed1632e58fc6107f03b9198"},
+ {file = "coverage-7.6.9-cp310-cp310-win_amd64.whl", hash = "sha256:35371f8438028fdccfaf3570b31d98e8d9eda8bb1d6ab9473f5a390969e98717"},
+ {file = "coverage-7.6.9-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:932fc826442132dde42ee52cf66d941f581c685a6313feebed358411238f60f9"},
+ {file = "coverage-7.6.9-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:085161be5f3b30fd9b3e7b9a8c301f935c8313dcf928a07b116324abea2c1c2c"},
+ {file = "coverage-7.6.9-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ccc660a77e1c2bf24ddbce969af9447a9474790160cfb23de6be4fa88e3951c7"},
+ {file = "coverage-7.6.9-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:c69e42c892c018cd3c8d90da61d845f50a8243062b19d228189b0224150018a9"},
+ {file = "coverage-7.6.9-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0824a28ec542a0be22f60c6ac36d679e0e262e5353203bea81d44ee81fe9c6d4"},
+ {file = "coverage-7.6.9-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:4401ae5fc52ad8d26d2a5d8a7428b0f0c72431683f8e63e42e70606374c311a1"},
+ {file = "coverage-7.6.9-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:98caba4476a6c8d59ec1eb00c7dd862ba9beca34085642d46ed503cc2d440d4b"},
+ {file = "coverage-7.6.9-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:ee5defd1733fd6ec08b168bd4f5387d5b322f45ca9e0e6c817ea6c4cd36313e3"},
+ {file = "coverage-7.6.9-cp311-cp311-win32.whl", hash = "sha256:f2d1ec60d6d256bdf298cb86b78dd715980828f50c46701abc3b0a2b3f8a0dc0"},
+ {file = "coverage-7.6.9-cp311-cp311-win_amd64.whl", hash = "sha256:0d59fd927b1f04de57a2ba0137166d31c1a6dd9e764ad4af552912d70428c92b"},
+ {file = "coverage-7.6.9-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:99e266ae0b5d15f1ca8d278a668df6f51cc4b854513daab5cae695ed7b721cf8"},
+ {file = "coverage-7.6.9-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:9901d36492009a0a9b94b20e52ebfc8453bf49bb2b27bca2c9706f8b4f5a554a"},
+ {file = "coverage-7.6.9-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:abd3e72dd5b97e3af4246cdada7738ef0e608168de952b837b8dd7e90341f015"},
+ {file = "coverage-7.6.9-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ff74026a461eb0660366fb01c650c1d00f833a086b336bdad7ab00cc952072b3"},
+ {file = "coverage-7.6.9-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:65dad5a248823a4996724a88eb51d4b31587aa7aa428562dbe459c684e5787ae"},
+ {file = "coverage-7.6.9-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:22be16571504c9ccea919fcedb459d5ab20d41172056206eb2994e2ff06118a4"},
+ {file = "coverage-7.6.9-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:0f957943bc718b87144ecaee70762bc2bc3f1a7a53c7b861103546d3a403f0a6"},
+ {file = "coverage-7.6.9-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:0ae1387db4aecb1f485fb70a6c0148c6cdaebb6038f1d40089b1fc84a5db556f"},
+ {file = "coverage-7.6.9-cp312-cp312-win32.whl", hash = "sha256:1a330812d9cc7ac2182586f6d41b4d0fadf9be9049f350e0efb275c8ee8eb692"},
+ {file = "coverage-7.6.9-cp312-cp312-win_amd64.whl", hash = "sha256:b12c6b18269ca471eedd41c1b6a1065b2f7827508edb9a7ed5555e9a56dcfc97"},
+ {file = "coverage-7.6.9-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:899b8cd4781c400454f2f64f7776a5d87bbd7b3e7f7bda0cb18f857bb1334664"},
+ {file = "coverage-7.6.9-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:61f70dc68bd36810972e55bbbe83674ea073dd1dcc121040a08cdf3416c5349c"},
+ {file = "coverage-7.6.9-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8a289d23d4c46f1a82d5db4abeb40b9b5be91731ee19a379d15790e53031c014"},
+ {file = "coverage-7.6.9-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7e216d8044a356fc0337c7a2a0536d6de07888d7bcda76febcb8adc50bdbbd00"},
+ {file = "coverage-7.6.9-cp313-cp313-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3c026eb44f744acaa2bda7493dad903aa5bf5fc4f2554293a798d5606710055d"},
+ {file = "coverage-7.6.9-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:e77363e8425325384f9d49272c54045bbed2f478e9dd698dbc65dbc37860eb0a"},
+ {file = "coverage-7.6.9-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:777abfab476cf83b5177b84d7486497e034eb9eaea0d746ce0c1268c71652077"},
+ {file = "coverage-7.6.9-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:447af20e25fdbe16f26e84eb714ba21d98868705cb138252d28bc400381f6ffb"},
+ {file = "coverage-7.6.9-cp313-cp313-win32.whl", hash = "sha256:d872ec5aeb086cbea771c573600d47944eea2dcba8be5f3ee649bfe3cb8dc9ba"},
+ {file = "coverage-7.6.9-cp313-cp313-win_amd64.whl", hash = "sha256:fd1213c86e48dfdc5a0cc676551db467495a95a662d2396ecd58e719191446e1"},
+ {file = "coverage-7.6.9-cp313-cp313t-macosx_10_13_x86_64.whl", hash = "sha256:ba9e7484d286cd5a43744e5f47b0b3fb457865baf07bafc6bee91896364e1419"},
+ {file = "coverage-7.6.9-cp313-cp313t-macosx_11_0_arm64.whl", hash = "sha256:e5ea1cf0872ee455c03e5674b5bca5e3e68e159379c1af0903e89f5eba9ccc3a"},
+ {file = "coverage-7.6.9-cp313-cp313t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2d10e07aa2b91835d6abec555ec8b2733347956991901eea6ffac295f83a30e4"},
+ {file = "coverage-7.6.9-cp313-cp313t-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:13a9e2d3ee855db3dd6ea1ba5203316a1b1fd8eaeffc37c5b54987e61e4194ae"},
+ {file = "coverage-7.6.9-cp313-cp313t-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9c38bf15a40ccf5619fa2fe8f26106c7e8e080d7760aeccb3722664c8656b030"},
+ {file = "coverage-7.6.9-cp313-cp313t-musllinux_1_2_aarch64.whl", hash = "sha256:d5275455b3e4627c8e7154feaf7ee0743c2e7af82f6e3b561967b1cca755a0be"},
+ {file = "coverage-7.6.9-cp313-cp313t-musllinux_1_2_i686.whl", hash = "sha256:8f8770dfc6e2c6a2d4569f411015c8d751c980d17a14b0530da2d7f27ffdd88e"},
+ {file = "coverage-7.6.9-cp313-cp313t-musllinux_1_2_x86_64.whl", hash = "sha256:8d2dfa71665a29b153a9681edb1c8d9c1ea50dfc2375fb4dac99ea7e21a0bcd9"},
+ {file = "coverage-7.6.9-cp313-cp313t-win32.whl", hash = "sha256:5e6b86b5847a016d0fbd31ffe1001b63355ed309651851295315031ea7eb5a9b"},
+ {file = "coverage-7.6.9-cp313-cp313t-win_amd64.whl", hash = "sha256:97ddc94d46088304772d21b060041c97fc16bdda13c6c7f9d8fcd8d5ae0d8611"},
+ {file = "coverage-7.6.9-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:adb697c0bd35100dc690de83154627fbab1f4f3c0386df266dded865fc50a902"},
+ {file = "coverage-7.6.9-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:be57b6d56e49c2739cdf776839a92330e933dd5e5d929966fbbd380c77f060be"},
+ {file = "coverage-7.6.9-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f1592791f8204ae9166de22ba7e6705fa4ebd02936c09436a1bb85aabca3e599"},
+ {file = "coverage-7.6.9-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4e12ae8cc979cf83d258acb5e1f1cf2f3f83524d1564a49d20b8bec14b637f08"},
+ {file = "coverage-7.6.9-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:bb5555cff66c4d3d6213a296b360f9e1a8e323e74e0426b6c10ed7f4d021e464"},
+ {file = "coverage-7.6.9-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:b9389a429e0e5142e69d5bf4a435dd688c14478a19bb901735cdf75e57b13845"},
+ {file = "coverage-7.6.9-cp39-cp39-musllinux_1_2_i686.whl", hash = "sha256:592ac539812e9b46046620341498caf09ca21023c41c893e1eb9dbda00a70cbf"},
+ {file = "coverage-7.6.9-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:a27801adef24cc30871da98a105f77995e13a25a505a0161911f6aafbd66e678"},
+ {file = "coverage-7.6.9-cp39-cp39-win32.whl", hash = "sha256:8e3c3e38930cfb729cb8137d7f055e5a473ddaf1217966aa6238c88bd9fd50e6"},
+ {file = "coverage-7.6.9-cp39-cp39-win_amd64.whl", hash = "sha256:e28bf44afa2b187cc9f41749138a64435bf340adfcacb5b2290c070ce99839d4"},
+ {file = "coverage-7.6.9-pp39.pp310-none-any.whl", hash = "sha256:f3ca78518bc6bc92828cd11867b121891d75cae4ea9e908d72030609b996db1b"},
+ {file = "coverage-7.6.9.tar.gz", hash = "sha256:4a8d8977b0c6ef5aeadcb644da9e69ae0dcfe66ec7f368c89c72e058bd71164d"},
]
[package.dependencies]
@@ -343,13 +355,13 @@ cython = ["cython"]
[[package]]
name = "exceptiongroup"
-version = "1.2.1"
+version = "1.2.2"
description = "Backport of PEP 654 (exception groups)"
optional = false
python-versions = ">=3.7"
files = [
- {file = "exceptiongroup-1.2.1-py3-none-any.whl", hash = "sha256:5258b9ed329c5bbdd31a309f53cbfb0b155341807f6ff7606a1e801a891b29ad"},
- {file = "exceptiongroup-1.2.1.tar.gz", hash = "sha256:a4785e48b045528f5bfe627b6ad554ff32def154f42372786903b7abcfe1aa16"},
+ {file = "exceptiongroup-1.2.2-py3-none-any.whl", hash = "sha256:3111b9d131c238bec2f8f516e123e14ba243563fb135d3fe885990585aa7795b"},
+ {file = "exceptiongroup-1.2.2.tar.gz", hash = "sha256:47c2edf7c6738fafb49fd34290706d1a1a2f4d1c6df275526b62cbb4aa5393cc"},
]
[package.extras]
@@ -371,49 +383,49 @@ testing = ["hatch", "pre-commit", "pytest", "tox"]
[[package]]
name = "filelock"
-version = "3.14.0"
+version = "3.16.1"
description = "A platform independent file lock."
optional = false
python-versions = ">=3.8"
files = [
- {file = "filelock-3.14.0-py3-none-any.whl", hash = "sha256:43339835842f110ca7ae60f1e1c160714c5a6afd15a2873419ab185334975c0f"},
- {file = "filelock-3.14.0.tar.gz", hash = "sha256:6ea72da3be9b8c82afd3edcf99f2fffbb5076335a5ae4d03248bb5b6c3eae78a"},
+ {file = "filelock-3.16.1-py3-none-any.whl", hash = "sha256:2082e5703d51fbf98ea75855d9d5527e33d8ff23099bec374a134febee6946b0"},
+ {file = "filelock-3.16.1.tar.gz", hash = "sha256:c249fbfcd5db47e5e2d6d62198e565475ee65e4831e2561c8e313fa7eb961435"},
]
[package.extras]
-docs = ["furo (>=2023.9.10)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.25.2)"]
-testing = ["covdefaults (>=2.3)", "coverage (>=7.3.2)", "diff-cover (>=8.0.1)", "pytest (>=7.4.3)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)", "pytest-timeout (>=2.2)"]
-typing = ["typing-extensions (>=4.8)"]
+docs = ["furo (>=2024.8.6)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4.1)"]
+testing = ["covdefaults (>=2.3)", "coverage (>=7.6.1)", "diff-cover (>=9.2)", "pytest (>=8.3.3)", "pytest-asyncio (>=0.24)", "pytest-cov (>=5)", "pytest-mock (>=3.14)", "pytest-timeout (>=2.3.1)", "virtualenv (>=20.26.4)"]
+typing = ["typing-extensions (>=4.12.2)"]
[[package]]
name = "flake8"
-version = "7.0.0"
+version = "7.1.1"
description = "the modular source code checker: pep8 pyflakes and co"
optional = false
python-versions = ">=3.8.1"
files = [
- {file = "flake8-7.0.0-py2.py3-none-any.whl", hash = "sha256:a6dfbb75e03252917f2473ea9653f7cd799c3064e54d4c8140044c5c065f53c3"},
- {file = "flake8-7.0.0.tar.gz", hash = "sha256:33f96621059e65eec474169085dc92bf26e7b2d47366b70be2f67ab80dc25132"},
+ {file = "flake8-7.1.1-py2.py3-none-any.whl", hash = "sha256:597477df7860daa5aa0fdd84bf5208a043ab96b8e96ab708770ae0364dd03213"},
+ {file = "flake8-7.1.1.tar.gz", hash = "sha256:049d058491e228e03e67b390f311bbf88fce2dbaa8fa673e7aea87b7198b8d38"},
]
[package.dependencies]
mccabe = ">=0.7.0,<0.8.0"
-pycodestyle = ">=2.11.0,<2.12.0"
+pycodestyle = ">=2.12.0,<2.13.0"
pyflakes = ">=3.2.0,<3.3.0"
[[package]]
name = "flake8-bugbear"
-version = "24.4.26"
+version = "24.12.12"
description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle."
optional = false
python-versions = ">=3.8.1"
files = [
- {file = "flake8_bugbear-24.4.26-py3-none-any.whl", hash = "sha256:cb430dd86bc821d79ccc0b030789a9c87a47a369667f12ba06e80f11305e8258"},
- {file = "flake8_bugbear-24.4.26.tar.gz", hash = "sha256:ff8d4ba5719019ebf98e754624c30c05cef0dadcf18a65d91c7567300e52a130"},
+ {file = "flake8_bugbear-24.12.12-py3-none-any.whl", hash = "sha256:1b6967436f65ca22a42e5373aaa6f2d87966ade9aa38d4baf2a1be550767545e"},
+ {file = "flake8_bugbear-24.12.12.tar.gz", hash = "sha256:46273cef0a6b6ff48ca2d69e472f41420a42a46e24b2a8972e4f0d6733d12a64"},
]
[package.dependencies]
-attrs = ">=19.2.0"
+attrs = ">=22.2.0"
flake8 = ">=6.0.0"
[package.extras]
@@ -421,17 +433,17 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest",
[[package]]
name = "flake8-comprehensions"
-version = "3.14.0"
+version = "3.16.0"
description = "A flake8 plugin to help you write better list/set/dict comprehensions."
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "flake8_comprehensions-3.14.0-py3-none-any.whl", hash = "sha256:7b9d07d94aa88e62099a6d1931ddf16c344d4157deedf90fe0d8ee2846f30e97"},
- {file = "flake8_comprehensions-3.14.0.tar.gz", hash = "sha256:81768c61bfc064e1a06222df08a2580d97de10cb388694becaf987c331c6c0cf"},
+ {file = "flake8_comprehensions-3.16.0-py3-none-any.whl", hash = "sha256:7c1eadc9d22e765f39857798febe7766b4d9c519793c6c149e3e13bf99693f70"},
+ {file = "flake8_comprehensions-3.16.0.tar.gz", hash = "sha256:9cbf789905a8f03f9d350fb82b17b264d9a16c7ce3542b2a7b871ef568cafabe"},
]
[package.dependencies]
-flake8 = ">=3.0,<3.2.0 || >3.2.0"
+flake8 = ">=3,<3.2 || >3.2"
[[package]]
name = "flake8-quotes"
@@ -462,6 +474,45 @@ files = [
classify-imports = "*"
flake8 = "*"
+[[package]]
+name = "gnureadline"
+version = "8.2.13"
+description = "The standard Python readline extension statically linked against the GNU readline library."
+optional = false
+python-versions = "*"
+files = [
+ {file = "gnureadline-8.2.13-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:0ca03501ce0939d7ecf9d075860d6f6ceb2f49f30331b4e96e4678ce03687bab"},
+ {file = "gnureadline-8.2.13-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:c28e33bfc56d4204693f213abeab927f65c505ce91f668a039720bc7c46b0353"},
+ {file = "gnureadline-8.2.13-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6472e3a780087eecd67c03e5455aecb209de51bcae74583222976f6b816f6192"},
+ {file = "gnureadline-8.2.13-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:94b143ea5d22b0c1ca4a591265afe135272c69b7757e968e34fbb47a7858d1ce"},
+ {file = "gnureadline-8.2.13-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:561a60b12f74ea7234036cc4fe558f3b46023be0dac5ed73541ece58cba2f88a"},
+ {file = "gnureadline-8.2.13-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:daa405028b9fe92bfbb93624e13e0674a242a1c5434b70ef61a04294502fdb65"},
+ {file = "gnureadline-8.2.13-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:576dac060887adc6067ee9d23fb2f0031fb2b3e560e07a6c9e666e05f0473af7"},
+ {file = "gnureadline-8.2.13-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:10fcaf561bc4ed6ab7075ab3ead188a18faaf4e6e92d916f81a09c0a670ce906"},
+ {file = "gnureadline-8.2.13-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:9c152a82613fa012ab4331bb9a0ffddb415e37561d376b910bf9e7d535607faf"},
+ {file = "gnureadline-8.2.13-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:85e362d2d0e85e45f0affae7bbfaf998b00167c55a78d31ee0f214de9ff429d2"},
+ {file = "gnureadline-8.2.13-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:b69e6608cc94e110018b721a11718d480a6330e0b62cbab65a22880e84011205"},
+ {file = "gnureadline-8.2.13-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0cc77fc9c8a8fcf10e0a554e49ee763219683386b8f906b7e6ef07c9e40e8420"},
+ {file = "gnureadline-8.2.13-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:2d3e33d2e0dd694d623a2ca1fae6990b52f1d25955504b7293a9350fb9912940"},
+ {file = "gnureadline-8.2.13-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:6c550d08c4d2882a83293a724b14a262ee5078fd4fa7acdc78aa59cab26ae343"},
+ {file = "gnureadline-8.2.13-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a7d6e3f5d9fd0cf8a84fb382d4e3ad2914331be4d929f17d50da01f1571c4b03"},
+ {file = "gnureadline-8.2.13-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f59275168cae1b02ca1ec7586a9804bb04ce427df92f8582a80d16e96c846b78"},
+ {file = "gnureadline-8.2.13-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:59c5505026646da6d5ced6a5316d6d191d011e8be422cba4abce71730ef37dc6"},
+ {file = "gnureadline-8.2.13-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3f1050ecf789f34d0ab0aacdb605f177725009a864e0038e70380614af92dc0d"},
+ {file = "gnureadline-8.2.13-cp36-cp36m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:23b43c8e9e2e6566cb3094749826181a86dba1d94b1e023b5f9923dc26e37876"},
+ {file = "gnureadline-8.2.13-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:4f5fc90af56a1ae6f88c9c7122fc76141c395b6c342a63800abed8c813f48b85"},
+ {file = "gnureadline-8.2.13-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d708e8f655d3b556a138f13e9fcb2d8a10a6901e3125c04cad5ef7c883191fe8"},
+ {file = "gnureadline-8.2.13-cp37-cp37m-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:265bcf6ef7082e130160fb34b9664284affb216a22c5bffcd518b35d02bcc4e9"},
+ {file = "gnureadline-8.2.13-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:07231f8191adb7f204010a86a91df9df9a80944981a16576a471f59304ad6a16"},
+ {file = "gnureadline-8.2.13-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:30cc1b6cb11d94554815cb91eb1dfa6a11887185aae50f253adaa393e91c6a86"},
+ {file = "gnureadline-8.2.13-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:50c40bfffffa82d4fcb0fde4940d4ff128ba2f876c1da09bae9d6d9ff770095e"},
+ {file = "gnureadline-8.2.13-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:dcfa601d95c00aa670ec5e4bf791caf6ba0bcf266de940fb54d44c278bd302fe"},
+ {file = "gnureadline-8.2.13-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:c7b8d3f2a2c9b7e6feaf1f20bdb6ebb8210e207b8c5360ffe407a47efeeb3fb8"},
+ {file = "gnureadline-8.2.13-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:811d85a70ac97cddeb1755282915e8a93c279dcf89513426f28617b8feff5aec"},
+ {file = "gnureadline-8.2.13-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4f57a3aa97c3379b2513c8bfbac0de2dfb41f695623c0b2ad337babb646b51a7"},
+ {file = "gnureadline-8.2.13.tar.gz", hash = "sha256:c9b9e1e7ba99a80bb50c12027d6ce692574f77a65bf57bc97041cf81c0f49bd1"},
+]
+
[[package]]
name = "graphviz"
version = "0.20.3"
@@ -492,24 +543,61 @@ files = [
[package.dependencies]
pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_version >= \"3.8\""}
+[[package]]
+name = "hypothesis"
+version = "6.122.3"
+description = "A library for property-based testing"
+optional = false
+python-versions = ">=3.9"
+files = [
+ {file = "hypothesis-6.122.3-py3-none-any.whl", hash = "sha256:f0f57036d3b95b979491602b32c95b6725c3af678cccb6165d8de330857f3c83"},
+ {file = "hypothesis-6.122.3.tar.gz", hash = "sha256:f4c927ce0ec739fa6266e4572949d0b54e24a14601a2bc5fec8f78e16af57918"},
+]
+
+[package.dependencies]
+attrs = ">=22.2.0"
+exceptiongroup = {version = ">=1.0.0", markers = "python_version < \"3.11\""}
+sortedcontainers = ">=2.1.0,<3.0.0"
+
+[package.extras]
+all = ["black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.78)", "django (>=4.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.18)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.19.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"]
+cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"]
+codemods = ["libcst (>=0.3.16)"]
+crosshair = ["crosshair-tool (>=0.0.78)", "hypothesis-crosshair (>=0.0.18)"]
+dateutil = ["python-dateutil (>=1.4)"]
+django = ["django (>=4.2)"]
+dpcontracts = ["dpcontracts (>=0.4)"]
+ghostwriter = ["black (>=19.10b0)"]
+lark = ["lark (>=0.10.1)"]
+numpy = ["numpy (>=1.19.3)"]
+pandas = ["pandas (>=1.1)"]
+pytest = ["pytest (>=4.6)"]
+pytz = ["pytz (>=2014.1)"]
+redis = ["redis (>=3.0.0)"]
+zoneinfo = ["tzdata (>=2024.2)"]
+
[[package]]
name = "importlib-metadata"
-version = "7.1.0"
+version = "8.5.0"
description = "Read metadata from Python packages"
optional = false
python-versions = ">=3.8"
files = [
- {file = "importlib_metadata-7.1.0-py3-none-any.whl", hash = "sha256:30962b96c0c223483ed6cc7280e7f0199feb01a0e40cfae4d4450fc6fab1f570"},
- {file = "importlib_metadata-7.1.0.tar.gz", hash = "sha256:b78938b926ee8d5f020fc4772d487045805a55ddbad2ecf21c6d60938dc7fcd2"},
+ {file = "importlib_metadata-8.5.0-py3-none-any.whl", hash = "sha256:45e54197d28b7a7f1559e60b95e7c567032b602131fbd588f1497f47880aa68b"},
+ {file = "importlib_metadata-8.5.0.tar.gz", hash = "sha256:71522656f0abace1d072b9e5481a48f07c138e00f079c38c8f883823f9c26bd7"},
]
[package.dependencies]
-zipp = ">=0.5"
+zipp = ">=3.20"
[package.extras]
-docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"]
+check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)"]
+cover = ["pytest-cov"]
+doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"]
+enabler = ["pytest-enabler (>=2.2)"]
perf = ["ipython"]
-testing = ["flufl.flake8", "importlib-resources (>=1.3)", "jaraco.test (>=5.4)", "packaging", "pyfakefs", "pytest (>=6)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-mypy", "pytest-perf (>=0.9.2)", "pytest-ruff (>=0.2.1)"]
+test = ["flufl.flake8", "importlib-resources (>=1.3)", "jaraco.test (>=5.4)", "packaging", "pyfakefs", "pytest (>=6,!=8.1.*)", "pytest-perf (>=0.9.2)"]
+type = ["pytest-mypy"]
[[package]]
name = "iniconfig"
@@ -536,6 +624,30 @@ files = [
[package.extras]
colors = ["colorama (>=0.4.6)"]
+[[package]]
+name = "kframework"
+version = "7.1.191"
+description = ""
+optional = false
+python-versions = "<4.0,>=3.10"
+files = [
+ {file = "kframework-7.1.191-py3-none-any.whl", hash = "sha256:b12d60a8a178fabdd6b12caa0041f4af64655a199f08e569c50170d5e8a74cde"},
+ {file = "kframework-7.1.191.tar.gz", hash = "sha256:f2bc40c5ab5ba81140f61e34bdc8b93c4296d456b9a59dfd478a220232926b8e"},
+]
+
+[package.dependencies]
+cmd2 = ">=2.4.2,<3.0.0"
+coloredlogs = ">=15.0.1,<16.0.0"
+filelock = ">=3.9.0,<4.0.0"
+graphviz = ">=0.20.1,<0.21.0"
+hypothesis = ">=6.103.1,<7.0.0"
+psutil = ">=5.9.5,<6.0.0"
+pybind11 = ">=2.10.3,<3.0.0"
+pytest = "*"
+textual = ">=0.27.0,<0.28.0"
+tomli = ">=2.0.1,<3.0.0"
+xdg-base-dirs = ">=6.0.1,<7.0.0"
+
[[package]]
name = "linkify-it-py"
version = "2.0.3"
@@ -595,13 +707,13 @@ files = [
[[package]]
name = "mdit-py-plugins"
-version = "0.4.1"
+version = "0.4.2"
description = "Collection of plugins for markdown-it-py"
optional = false
python-versions = ">=3.8"
files = [
- {file = "mdit_py_plugins-0.4.1-py3-none-any.whl", hash = "sha256:1020dfe4e6bfc2c79fb49ae4e3f5b297f5ccd20f010187acc52af2921e27dc6a"},
- {file = "mdit_py_plugins-0.4.1.tar.gz", hash = "sha256:834b8ac23d1cd60cec703646ffd22ae97b7955a6d596eb1d304be1e251ae499c"},
+ {file = "mdit_py_plugins-0.4.2-py3-none-any.whl", hash = "sha256:0c673c3f889399a33b95e88d2f0d111b4447bdfea7f237dab2d488f459835636"},
+ {file = "mdit_py_plugins-0.4.2.tar.gz", hash = "sha256:5f2cd1fdb606ddf152d37ec30e46101a60512bc0e5fa1a7002c36647b09e26b5"},
]
[package.dependencies]
@@ -625,47 +737,53 @@ files = [
[[package]]
name = "mypy"
-version = "1.10.0"
+version = "1.13.0"
description = "Optional static typing for Python"
optional = false
python-versions = ">=3.8"
files = [
- {file = "mypy-1.10.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:da1cbf08fb3b851ab3b9523a884c232774008267b1f83371ace57f412fe308c2"},
- {file = "mypy-1.10.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:12b6bfc1b1a66095ab413160a6e520e1dc076a28f3e22f7fb25ba3b000b4ef99"},
- {file = "mypy-1.10.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9e36fb078cce9904c7989b9693e41cb9711e0600139ce3970c6ef814b6ebc2b2"},
- {file = "mypy-1.10.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:2b0695d605ddcd3eb2f736cd8b4e388288c21e7de85001e9f85df9187f2b50f9"},
- {file = "mypy-1.10.0-cp310-cp310-win_amd64.whl", hash = "sha256:cd777b780312ddb135bceb9bc8722a73ec95e042f911cc279e2ec3c667076051"},
- {file = "mypy-1.10.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:3be66771aa5c97602f382230165b856c231d1277c511c9a8dd058be4784472e1"},
- {file = "mypy-1.10.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:8b2cbaca148d0754a54d44121b5825ae71868c7592a53b7292eeb0f3fdae95ee"},
- {file = "mypy-1.10.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:1ec404a7cbe9fc0e92cb0e67f55ce0c025014e26d33e54d9e506a0f2d07fe5de"},
- {file = "mypy-1.10.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:e22e1527dc3d4aa94311d246b59e47f6455b8729f4968765ac1eacf9a4760bc7"},
- {file = "mypy-1.10.0-cp311-cp311-win_amd64.whl", hash = "sha256:a87dbfa85971e8d59c9cc1fcf534efe664d8949e4c0b6b44e8ca548e746a8d53"},
- {file = "mypy-1.10.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:a781f6ad4bab20eef8b65174a57e5203f4be627b46291f4589879bf4e257b97b"},
- {file = "mypy-1.10.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:b808e12113505b97d9023b0b5e0c0705a90571c6feefc6f215c1df9381256e30"},
- {file = "mypy-1.10.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8f55583b12156c399dce2df7d16f8a5095291354f1e839c252ec6c0611e86e2e"},
- {file = "mypy-1.10.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:4cf18f9d0efa1b16478c4c129eabec36148032575391095f73cae2e722fcf9d5"},
- {file = "mypy-1.10.0-cp312-cp312-win_amd64.whl", hash = "sha256:bc6ac273b23c6b82da3bb25f4136c4fd42665f17f2cd850771cb600bdd2ebeda"},
- {file = "mypy-1.10.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:9fd50226364cd2737351c79807775136b0abe084433b55b2e29181a4c3c878c0"},
- {file = "mypy-1.10.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:f90cff89eea89273727d8783fef5d4a934be2fdca11b47def50cf5d311aff727"},
- {file = "mypy-1.10.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fcfc70599efde5c67862a07a1aaf50e55bce629ace26bb19dc17cece5dd31ca4"},
- {file = "mypy-1.10.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:075cbf81f3e134eadaf247de187bd604748171d6b79736fa9b6c9685b4083061"},
- {file = "mypy-1.10.0-cp38-cp38-win_amd64.whl", hash = "sha256:3f298531bca95ff615b6e9f2fc0333aae27fa48052903a0ac90215021cdcfa4f"},
- {file = "mypy-1.10.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:fa7ef5244615a2523b56c034becde4e9e3f9b034854c93639adb667ec9ec2976"},
- {file = "mypy-1.10.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:3236a4c8f535a0631f85f5fcdffba71c7feeef76a6002fcba7c1a8e57c8be1ec"},
- {file = "mypy-1.10.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4a2b5cdbb5dd35aa08ea9114436e0d79aceb2f38e32c21684dcf8e24e1e92821"},
- {file = "mypy-1.10.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:92f93b21c0fe73dc00abf91022234c79d793318b8a96faac147cd579c1671746"},
- {file = "mypy-1.10.0-cp39-cp39-win_amd64.whl", hash = "sha256:28d0e038361b45f099cc086d9dd99c15ff14d0188f44ac883010e172ce86c38a"},
- {file = "mypy-1.10.0-py3-none-any.whl", hash = "sha256:f8c083976eb530019175aabadb60921e73b4f45736760826aa1689dda8208aee"},
- {file = "mypy-1.10.0.tar.gz", hash = "sha256:3d087fcbec056c4ee34974da493a826ce316947485cef3901f511848e687c131"},
+ {file = "mypy-1.13.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6607e0f1dd1fb7f0aca14d936d13fd19eba5e17e1cd2a14f808fa5f8f6d8f60a"},
+ {file = "mypy-1.13.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:8a21be69bd26fa81b1f80a61ee7ab05b076c674d9b18fb56239d72e21d9f4c80"},
+ {file = "mypy-1.13.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:7b2353a44d2179846a096e25691d54d59904559f4232519d420d64da6828a3a7"},
+ {file = "mypy-1.13.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:0730d1c6a2739d4511dc4253f8274cdd140c55c32dfb0a4cf8b7a43f40abfa6f"},
+ {file = "mypy-1.13.0-cp310-cp310-win_amd64.whl", hash = "sha256:c5fc54dbb712ff5e5a0fca797e6e0aa25726c7e72c6a5850cfd2adbc1eb0a372"},
+ {file = "mypy-1.13.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:581665e6f3a8a9078f28d5502f4c334c0c8d802ef55ea0e7276a6e409bc0d82d"},
+ {file = "mypy-1.13.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:3ddb5b9bf82e05cc9a627e84707b528e5c7caaa1c55c69e175abb15a761cec2d"},
+ {file = "mypy-1.13.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:20c7ee0bc0d5a9595c46f38beb04201f2620065a93755704e141fcac9f59db2b"},
+ {file = "mypy-1.13.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:3790ded76f0b34bc9c8ba4def8f919dd6a46db0f5a6610fb994fe8efdd447f73"},
+ {file = "mypy-1.13.0-cp311-cp311-win_amd64.whl", hash = "sha256:51f869f4b6b538229c1d1bcc1dd7d119817206e2bc54e8e374b3dfa202defcca"},
+ {file = "mypy-1.13.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:5c7051a3461ae84dfb5dd15eff5094640c61c5f22257c8b766794e6dd85e72d5"},
+ {file = "mypy-1.13.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:39bb21c69a5d6342f4ce526e4584bc5c197fd20a60d14a8624d8743fffb9472e"},
+ {file = "mypy-1.13.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:164f28cb9d6367439031f4c81e84d3ccaa1e19232d9d05d37cb0bd880d3f93c2"},
+ {file = "mypy-1.13.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:a4c1bfcdbce96ff5d96fc9b08e3831acb30dc44ab02671eca5953eadad07d6d0"},
+ {file = "mypy-1.13.0-cp312-cp312-win_amd64.whl", hash = "sha256:a0affb3a79a256b4183ba09811e3577c5163ed06685e4d4b46429a271ba174d2"},
+ {file = "mypy-1.13.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:a7b44178c9760ce1a43f544e595d35ed61ac2c3de306599fa59b38a6048e1aa7"},
+ {file = "mypy-1.13.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:5d5092efb8516d08440e36626f0153b5006d4088c1d663d88bf79625af3d1d62"},
+ {file = "mypy-1.13.0-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:de2904956dac40ced10931ac967ae63c5089bd498542194b436eb097a9f77bc8"},
+ {file = "mypy-1.13.0-cp313-cp313-musllinux_1_1_x86_64.whl", hash = "sha256:7bfd8836970d33c2105562650656b6846149374dc8ed77d98424b40b09340ba7"},
+ {file = "mypy-1.13.0-cp313-cp313-win_amd64.whl", hash = "sha256:9f73dba9ec77acb86457a8fc04b5239822df0c14a082564737833d2963677dbc"},
+ {file = "mypy-1.13.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:100fac22ce82925f676a734af0db922ecfea991e1d7ec0ceb1e115ebe501301a"},
+ {file = "mypy-1.13.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:7bcb0bb7f42a978bb323a7c88f1081d1b5dee77ca86f4100735a6f541299d8fb"},
+ {file = "mypy-1.13.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:bde31fc887c213e223bbfc34328070996061b0833b0a4cfec53745ed61f3519b"},
+ {file = "mypy-1.13.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:07de989f89786f62b937851295ed62e51774722e5444a27cecca993fc3f9cd74"},
+ {file = "mypy-1.13.0-cp38-cp38-win_amd64.whl", hash = "sha256:4bde84334fbe19bad704b3f5b78c4abd35ff1026f8ba72b29de70dda0916beb6"},
+ {file = "mypy-1.13.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:0246bcb1b5de7f08f2826451abd947bf656945209b140d16ed317f65a17dc7dc"},
+ {file = "mypy-1.13.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:7f5b7deae912cf8b77e990b9280f170381fdfbddf61b4ef80927edd813163732"},
+ {file = "mypy-1.13.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:7029881ec6ffb8bc233a4fa364736789582c738217b133f1b55967115288a2bc"},
+ {file = "mypy-1.13.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:3e38b980e5681f28f033f3be86b099a247b13c491f14bb8b1e1e134d23bb599d"},
+ {file = "mypy-1.13.0-cp39-cp39-win_amd64.whl", hash = "sha256:a6789be98a2017c912ae6ccb77ea553bbaf13d27605d2ca20a76dfbced631b24"},
+ {file = "mypy-1.13.0-py3-none-any.whl", hash = "sha256:9c250883f9fd81d212e0952c92dbfcc96fc237f4b7c92f56ac81fd48460b3e5a"},
+ {file = "mypy-1.13.0.tar.gz", hash = "sha256:0291a61b6fbf3e6673e3405cfcc0e7650bebc7939659fdca2702958038bd835e"},
]
[package.dependencies]
mypy-extensions = ">=1.0.0"
tomli = {version = ">=1.1.0", markers = "python_version < \"3.11\""}
-typing-extensions = ">=4.1.0"
+typing-extensions = ">=4.6.0"
[package.extras]
dmypy = ["psutil (>=4.0)"]
+faster-cache = ["orjson"]
install-types = ["pip"]
mypyc = ["setuptools (>=50)"]
reports = ["lxml"]
@@ -728,13 +846,13 @@ files = [
[[package]]
name = "packaging"
-version = "24.0"
+version = "24.2"
description = "Core utilities for Python packages"
optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
files = [
- {file = "packaging-24.0-py3-none-any.whl", hash = "sha256:2ddfb553fdf02fb784c234c7ba6ccc288296ceabec964ad2eae3777778130bc5"},
- {file = "packaging-24.0.tar.gz", hash = "sha256:eb82c5e3e56209074766e6885bb04b8c38a0c015d0a30036ebe7ece34c9989e9"},
+ {file = "packaging-24.2-py3-none-any.whl", hash = "sha256:09abb1bccd265c01f4a3aa3f7a7db064b36514d2cba19a2f694fe6150451a759"},
+ {file = "packaging-24.2.tar.gz", hash = "sha256:c228a6dc5e932d346bc5739379109d49e8853dd8223571c7c5b55260edc0b97f"},
]
[[package]]
@@ -764,19 +882,19 @@ flake8 = ">=5.0.0"
[[package]]
name = "platformdirs"
-version = "4.2.2"
+version = "4.3.6"
description = "A small Python package for determining appropriate platform-specific dirs, e.g. a `user data dir`."
optional = false
python-versions = ">=3.8"
files = [
- {file = "platformdirs-4.2.2-py3-none-any.whl", hash = "sha256:2d7a1657e36a80ea911db832a8a6ece5ee53d8de21edd5cc5879af6530b1bfee"},
- {file = "platformdirs-4.2.2.tar.gz", hash = "sha256:38b7b51f512eed9e84a22788b4bce1de17c0adb134d6becb09836e37d8654cd3"},
+ {file = "platformdirs-4.3.6-py3-none-any.whl", hash = "sha256:73e575e1408ab8103900836b97580d5307456908a03e92031bab39e4554cc3fb"},
+ {file = "platformdirs-4.3.6.tar.gz", hash = "sha256:357fb2acbc885b0419afd3ce3ed34564c13c9b95c89360cd9563f73aa5e2b907"},
]
[package.extras]
-docs = ["furo (>=2023.9.10)", "proselint (>=0.13)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.25.2)"]
-test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4.3)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)"]
-type = ["mypy (>=1.8)"]
+docs = ["furo (>=2024.8.6)", "proselint (>=0.14)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4)"]
+test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=8.3.2)", "pytest-cov (>=5)", "pytest-mock (>=3.14)"]
+type = ["mypy (>=1.11.2)"]
[[package]]
name = "pluggy"
@@ -795,25 +913,27 @@ testing = ["pytest", "pytest-benchmark"]
[[package]]
name = "psutil"
-version = "5.9.5"
+version = "5.9.8"
description = "Cross-platform lib for process and system monitoring in Python."
optional = false
-python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*"
+python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*, !=3.5.*"
files = [
- {file = "psutil-5.9.5-cp27-cp27m-macosx_10_9_x86_64.whl", hash = "sha256:be8929ce4313f9f8146caad4272f6abb8bf99fc6cf59344a3167ecd74f4f203f"},
- {file = "psutil-5.9.5-cp27-cp27m-manylinux2010_i686.whl", hash = "sha256:ab8ed1a1d77c95453db1ae00a3f9c50227ebd955437bcf2a574ba8adbf6a74d5"},
- {file = "psutil-5.9.5-cp27-cp27m-manylinux2010_x86_64.whl", hash = "sha256:4aef137f3345082a3d3232187aeb4ac4ef959ba3d7c10c33dd73763fbc063da4"},
- {file = "psutil-5.9.5-cp27-cp27mu-manylinux2010_i686.whl", hash = "sha256:ea8518d152174e1249c4f2a1c89e3e6065941df2fa13a1ab45327716a23c2b48"},
- {file = "psutil-5.9.5-cp27-cp27mu-manylinux2010_x86_64.whl", hash = "sha256:acf2aef9391710afded549ff602b5887d7a2349831ae4c26be7c807c0a39fac4"},
- {file = "psutil-5.9.5-cp27-none-win32.whl", hash = "sha256:5b9b8cb93f507e8dbaf22af6a2fd0ccbe8244bf30b1baad6b3954e935157ae3f"},
- {file = "psutil-5.9.5-cp27-none-win_amd64.whl", hash = "sha256:8c5f7c5a052d1d567db4ddd231a9d27a74e8e4a9c3f44b1032762bd7b9fdcd42"},
- {file = "psutil-5.9.5-cp36-abi3-macosx_10_9_x86_64.whl", hash = "sha256:3c6f686f4225553615612f6d9bc21f1c0e305f75d7d8454f9b46e901778e7217"},
- {file = "psutil-5.9.5-cp36-abi3-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7a7dd9997128a0d928ed4fb2c2d57e5102bb6089027939f3b722f3a210f9a8da"},
- {file = "psutil-5.9.5-cp36-abi3-manylinux_2_12_x86_64.manylinux2010_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:89518112647f1276b03ca97b65cc7f64ca587b1eb0278383017c2a0dcc26cbe4"},
- {file = "psutil-5.9.5-cp36-abi3-win32.whl", hash = "sha256:104a5cc0e31baa2bcf67900be36acde157756b9c44017b86b2c049f11957887d"},
- {file = "psutil-5.9.5-cp36-abi3-win_amd64.whl", hash = "sha256:b258c0c1c9d145a1d5ceffab1134441c4c5113b2417fafff7315a917a026c3c9"},
- {file = "psutil-5.9.5-cp38-abi3-macosx_11_0_arm64.whl", hash = "sha256:c607bb3b57dc779d55e1554846352b4e358c10fff3abf3514a7a6601beebdb30"},
- {file = "psutil-5.9.5.tar.gz", hash = "sha256:5410638e4df39c54d957fc51ce03048acd8e6d60abc0f5107af51e5fb566eb3c"},
+ {file = "psutil-5.9.8-cp27-cp27m-macosx_10_9_x86_64.whl", hash = "sha256:26bd09967ae00920df88e0352a91cff1a78f8d69b3ecabbfe733610c0af486c8"},
+ {file = "psutil-5.9.8-cp27-cp27m-manylinux2010_i686.whl", hash = "sha256:05806de88103b25903dff19bb6692bd2e714ccf9e668d050d144012055cbca73"},
+ {file = "psutil-5.9.8-cp27-cp27m-manylinux2010_x86_64.whl", hash = "sha256:611052c4bc70432ec770d5d54f64206aa7203a101ec273a0cd82418c86503bb7"},
+ {file = "psutil-5.9.8-cp27-cp27mu-manylinux2010_i686.whl", hash = "sha256:50187900d73c1381ba1454cf40308c2bf6f34268518b3f36a9b663ca87e65e36"},
+ {file = "psutil-5.9.8-cp27-cp27mu-manylinux2010_x86_64.whl", hash = "sha256:02615ed8c5ea222323408ceba16c60e99c3f91639b07da6373fb7e6539abc56d"},
+ {file = "psutil-5.9.8-cp27-none-win32.whl", hash = "sha256:36f435891adb138ed3c9e58c6af3e2e6ca9ac2f365efe1f9cfef2794e6c93b4e"},
+ {file = "psutil-5.9.8-cp27-none-win_amd64.whl", hash = "sha256:bd1184ceb3f87651a67b2708d4c3338e9b10c5df903f2e3776b62303b26cb631"},
+ {file = "psutil-5.9.8-cp36-abi3-macosx_10_9_x86_64.whl", hash = "sha256:aee678c8720623dc456fa20659af736241f575d79429a0e5e9cf88ae0605cc81"},
+ {file = "psutil-5.9.8-cp36-abi3-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:8cb6403ce6d8e047495a701dc7c5bd788add903f8986d523e3e20b98b733e421"},
+ {file = "psutil-5.9.8-cp36-abi3-manylinux_2_12_x86_64.manylinux2010_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d06016f7f8625a1825ba3732081d77c94589dca78b7a3fc072194851e88461a4"},
+ {file = "psutil-5.9.8-cp36-cp36m-win32.whl", hash = "sha256:7d79560ad97af658a0f6adfef8b834b53f64746d45b403f225b85c5c2c140eee"},
+ {file = "psutil-5.9.8-cp36-cp36m-win_amd64.whl", hash = "sha256:27cc40c3493bb10de1be4b3f07cae4c010ce715290a5be22b98493509c6299e2"},
+ {file = "psutil-5.9.8-cp37-abi3-win32.whl", hash = "sha256:bc56c2a1b0d15aa3eaa5a60c9f3f8e3e565303b465dbf57a1b730e7a2b9844e0"},
+ {file = "psutil-5.9.8-cp37-abi3-win_amd64.whl", hash = "sha256:8db4c1b57507eef143a15a6884ca10f7c73876cdf5d51e713151c1236a0e68cf"},
+ {file = "psutil-5.9.8-cp38-abi3-macosx_11_0_arm64.whl", hash = "sha256:d16bbddf0693323b8c6123dd804100241da461e41d6e332fb0ba6058f630f8c8"},
+ {file = "psutil-5.9.8.tar.gz", hash = "sha256:6be126e3225486dff286a8fb9a06246a5253f4c7c53b475ea5f5ac934e64194c"},
]
[package.extras]
@@ -848,27 +968,27 @@ resolved_reference = "e5fb6ed5b1aebf1c0d67087397b3c1240ff412da"
[[package]]
name = "pybind11"
-version = "2.12.0"
+version = "2.13.6"
description = "Seamless operability between C++11 and Python"
optional = false
-python-versions = ">=3.6"
+python-versions = ">=3.7"
files = [
- {file = "pybind11-2.12.0-py3-none-any.whl", hash = "sha256:df8d60b94f9e714d81013db233393d430ebf9f3551642b82291cf1b14d1afdbd"},
- {file = "pybind11-2.12.0.tar.gz", hash = "sha256:5e3c557a84b06b969247630407fc4d985bed157b4253b13153b8e8e165e0c3dc"},
+ {file = "pybind11-2.13.6-py3-none-any.whl", hash = "sha256:237c41e29157b962835d356b370ededd57594a26d5894a795960f0047cb5caf5"},
+ {file = "pybind11-2.13.6.tar.gz", hash = "sha256:ba6af10348c12b24e92fa086b39cfba0eff619b61ac77c406167d813b096d39a"},
]
[package.extras]
-global = ["pybind11-global (==2.12.0)"]
+global = ["pybind11-global (==2.13.6)"]
[[package]]
name = "pycodestyle"
-version = "2.11.1"
+version = "2.12.1"
description = "Python style guide checker"
optional = false
python-versions = ">=3.8"
files = [
- {file = "pycodestyle-2.11.1-py2.py3-none-any.whl", hash = "sha256:44fe31000b2d866f2e41841b18528a505fbd7fef9017b04eff4e2648a0fadc67"},
- {file = "pycodestyle-2.11.1.tar.gz", hash = "sha256:41ba0e7afc9752dfb53ced5489e89f8186be00e599e712660695b7a75ff2663f"},
+ {file = "pycodestyle-2.12.1-py2.py3-none-any.whl", hash = "sha256:46f0fb92069a7c28ab7bb558f05bfc0110dac69a0cd23c61ea0040283a9d78b3"},
+ {file = "pycodestyle-2.12.1.tar.gz", hash = "sha256:6838eae08bbce4f6accd5d5572075c63626a15ee3e6f842df996bf62f6d73521"},
]
[[package]]
@@ -896,63 +1016,39 @@ files = [
[package.extras]
windows-terminal = ["colorama (>=0.4.6)"]
-[[package]]
-name = "pyk"
-version = "7.0.106"
-description = ""
-optional = false
-python-versions = "^3.10"
-files = []
-develop = false
-
-[package.dependencies]
-cmd2 = "^2.4.2"
-coloredlogs = "^15.0.1"
-filelock = "^3.9.0"
-graphviz = "^0.20.1"
-psutil = "5.9.5"
-pybind11 = "^2.10.3"
-textual = "^0.27.0"
-tomli = "^2.0.1"
-xdg-base-dirs = "^6.0.1"
-
-[package.source]
-type = "git"
-url = "https://github.com/runtimeverification/k.git"
-reference = "v7.0.106"
-resolved_reference = "9100689e357a7e5820362869a73684468ef9c91b"
-subdirectory = "pyk"
-
[[package]]
name = "pyperclip"
-version = "1.8.2"
+version = "1.9.0"
description = "A cross-platform clipboard module for Python. (Only handles plain text for now.)"
optional = false
python-versions = "*"
files = [
- {file = "pyperclip-1.8.2.tar.gz", hash = "sha256:105254a8b04934f0bc84e9c24eb360a591aaf6535c9def5f29d92af107a9bf57"},
+ {file = "pyperclip-1.9.0.tar.gz", hash = "sha256:b7de0142ddc81bfc5c7507eea19da920b92252b548b96186caf94a5e2527d310"},
]
[[package]]
name = "pyreadline3"
-version = "3.4.1"
+version = "3.5.4"
description = "A python implementation of GNU readline."
optional = false
-python-versions = "*"
+python-versions = ">=3.8"
files = [
- {file = "pyreadline3-3.4.1-py3-none-any.whl", hash = "sha256:b0efb6516fd4fb07b45949053826a62fa4cb353db5be2bbb4a7aa1fdd1e345fb"},
- {file = "pyreadline3-3.4.1.tar.gz", hash = "sha256:6f3d1f7b8a31ba32b73917cefc1f28cc660562f39aea8646d30bd6eff21f7bae"},
+ {file = "pyreadline3-3.5.4-py3-none-any.whl", hash = "sha256:eaf8e6cc3c49bcccf145fc6067ba8643d1df34d604a1ec0eccbf7a18e6d3fae6"},
+ {file = "pyreadline3-3.5.4.tar.gz", hash = "sha256:8d57d53039a1c75adba8e50dd3d992b28143480816187ea5efbd5c78e6c885b7"},
]
+[package.extras]
+dev = ["build", "flake8", "mypy", "pytest", "twine"]
+
[[package]]
name = "pytest"
-version = "8.2.1"
+version = "8.3.4"
description = "pytest: simple powerful testing with Python"
optional = false
python-versions = ">=3.8"
files = [
- {file = "pytest-8.2.1-py3-none-any.whl", hash = "sha256:faccc5d332b8c3719f40283d0d44aa5cf101cec36f88cde9ed8f2bc0538612b1"},
- {file = "pytest-8.2.1.tar.gz", hash = "sha256:5046e5b46d8e4cac199c373041f26be56fdb81eb4e67dc11d4e10811fc3408fd"},
+ {file = "pytest-8.3.4-py3-none-any.whl", hash = "sha256:50e16d954148559c9a74109af1eaf0c945ba2d8f30f0a3d3335edde19788b6f6"},
+ {file = "pytest-8.3.4.tar.gz", hash = "sha256:965370d062bce11e73868e0335abac31b4d3de0e82f4007408d242b4f8610761"},
]
[package.dependencies]
@@ -960,7 +1056,7 @@ colorama = {version = "*", markers = "sys_platform == \"win32\""}
exceptiongroup = {version = ">=1.0.0rc8", markers = "python_version < \"3.11\""}
iniconfig = "*"
packaging = "*"
-pluggy = ">=1.5,<2.0"
+pluggy = ">=1.5,<2"
tomli = {version = ">=1", markers = "python_version < \"3.11\""}
[package.extras]
@@ -968,17 +1064,17 @@ dev = ["argcomplete", "attrs (>=19.2)", "hypothesis (>=3.56)", "mock", "pygments
[[package]]
name = "pytest-cov"
-version = "5.0.0"
+version = "6.0.0"
description = "Pytest plugin for measuring coverage."
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "pytest-cov-5.0.0.tar.gz", hash = "sha256:5837b58e9f6ebd335b0f8060eecce69b662415b16dc503883a02f45dfeb14857"},
- {file = "pytest_cov-5.0.0-py3-none-any.whl", hash = "sha256:4f0764a1219df53214206bf1feea4633c3b558a2925c8b59f144f682861ce652"},
+ {file = "pytest-cov-6.0.0.tar.gz", hash = "sha256:fde0b595ca248bb8e2d76f020b465f3b107c9632e6a1d1705f17834c89dcadc0"},
+ {file = "pytest_cov-6.0.0-py3-none-any.whl", hash = "sha256:eee6f1b9e61008bd34975a4d5bab25801eb31898b032dd55addc93e96fcaaa35"},
]
[package.dependencies]
-coverage = {version = ">=5.2.1", extras = ["toml"]}
+coverage = {version = ">=7.5", extras = ["toml"]}
pytest = ">=4.6"
[package.extras]
@@ -1023,50 +1119,67 @@ testing = ["filelock"]
[[package]]
name = "pyupgrade"
-version = "3.15.2"
+version = "3.19.1"
description = "A tool to automatically upgrade syntax for newer versions."
optional = false
-python-versions = ">=3.8.1"
+python-versions = ">=3.9"
files = [
- {file = "pyupgrade-3.15.2-py2.py3-none-any.whl", hash = "sha256:ce309e0ff8ecb73f56a45f12570be84bbbde9540d13697cacb261a7f595fb1f5"},
- {file = "pyupgrade-3.15.2.tar.gz", hash = "sha256:c488d6896c546d25845712ef6402657123008d56c1063174e27aabe15bd6b4e5"},
+ {file = "pyupgrade-3.19.1-py2.py3-none-any.whl", hash = "sha256:8c5b0bfacae5ff30fa136a53eb7f22c34ba007450d4099e9da8089dabb9e67c9"},
+ {file = "pyupgrade-3.19.1.tar.gz", hash = "sha256:d10e8c5f54b8327211828769e98d95d95e4715de632a3414f1eef3f51357b9e2"},
]
[package.dependencies]
-tokenize-rt = ">=5.2.0"
+tokenize-rt = ">=6.1.0"
[[package]]
name = "rich"
-version = "13.7.1"
+version = "13.9.4"
description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal"
optional = false
-python-versions = ">=3.7.0"
+python-versions = ">=3.8.0"
files = [
- {file = "rich-13.7.1-py3-none-any.whl", hash = "sha256:4edbae314f59eb482f54e9e30bf00d33350aaa94f4bfcd4e9e3110e64d0d7222"},
- {file = "rich-13.7.1.tar.gz", hash = "sha256:9be308cb1fe2f1f57d67ce99e95af38a1e2bc71ad9813b0e247cf7ffbcc3a432"},
+ {file = "rich-13.9.4-py3-none-any.whl", hash = "sha256:6049d5e6ec054bf2779ab3358186963bac2ea89175919d699e378b99738c2a90"},
+ {file = "rich-13.9.4.tar.gz", hash = "sha256:439594978a49a09530cff7ebc4b5c7103ef57baf48d5ea3184f21d9a2befa098"},
]
[package.dependencies]
markdown-it-py = ">=2.2.0"
pygments = ">=2.13.0,<3.0.0"
+typing-extensions = {version = ">=4.0.0,<5.0", markers = "python_version < \"3.11\""}
[package.extras]
jupyter = ["ipywidgets (>=7.5.1,<9)"]
[[package]]
name = "setuptools"
-version = "70.0.0"
+version = "75.6.0"
description = "Easily download, build, install, upgrade, and uninstall Python packages"
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "setuptools-70.0.0-py3-none-any.whl", hash = "sha256:54faa7f2e8d2d11bcd2c07bed282eef1046b5c080d1c32add737d7b5817b1ad4"},
- {file = "setuptools-70.0.0.tar.gz", hash = "sha256:f211a66637b8fa059bb28183da127d4e86396c991a942b028c6650d4319c3fd0"},
+ {file = "setuptools-75.6.0-py3-none-any.whl", hash = "sha256:ce74b49e8f7110f9bf04883b730f4765b774ef3ef28f722cce7c273d253aaf7d"},
+ {file = "setuptools-75.6.0.tar.gz", hash = "sha256:8199222558df7c86216af4f84c30e9b34a61d8ba19366cc914424cdbd28252f6"},
]
[package.extras]
-docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier"]
-testing = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "mypy (==1.9)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.1)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (>=0.2.1)", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"]
+check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)", "ruff (>=0.7.0)"]
+core = ["importlib_metadata (>=6)", "jaraco.collections", "jaraco.functools (>=4)", "jaraco.text (>=3.7)", "more_itertools", "more_itertools (>=8.8)", "packaging", "packaging (>=24.2)", "platformdirs (>=4.2.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"]
+cover = ["pytest-cov"]
+doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier", "towncrier (<24.7)"]
+enabler = ["pytest-enabler (>=2.2)"]
+test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test (>=5.5)", "packaging (>=24.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-home (>=0.5)", "pytest-perf", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"]
+type = ["importlib_metadata (>=7.0.2)", "jaraco.develop (>=7.21)", "mypy (>=1.12,<1.14)", "pytest-mypy"]
+
+[[package]]
+name = "sortedcontainers"
+version = "2.4.0"
+description = "Sorted Containers -- Sorted List, Sorted Dict, Sorted Set"
+optional = false
+python-versions = "*"
+files = [
+ {file = "sortedcontainers-2.4.0-py2.py3-none-any.whl", hash = "sha256:a163dcaede0f1c021485e957a39245190e74249897e2ae4b2aa38595db237ee0"},
+ {file = "sortedcontainers-2.4.0.tar.gz", hash = "sha256:25caa5a06cc30b6b83d11423433f65d1f9d76c4c6a0c90e3379eaa43b9bfdb88"},
+]
[[package]]
name = "textual"
@@ -1090,24 +1203,54 @@ dev = ["aiohttp (>=3.8.1)", "click (>=8.1.2)", "msgpack (>=1.0.3)"]
[[package]]
name = "tokenize-rt"
-version = "5.2.0"
+version = "6.1.0"
description = "A wrapper around the stdlib `tokenize` which roundtrips."
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "tokenize_rt-5.2.0-py2.py3-none-any.whl", hash = "sha256:b79d41a65cfec71285433511b50271b05da3584a1da144a0752e9c621a285289"},
- {file = "tokenize_rt-5.2.0.tar.gz", hash = "sha256:9fe80f8a5c1edad2d3ede0f37481cc0cc1538a2f442c9c2f9e4feacd2792d054"},
+ {file = "tokenize_rt-6.1.0-py2.py3-none-any.whl", hash = "sha256:d706141cdec4aa5f358945abe36b911b8cbdc844545da99e811250c0cee9b6fc"},
+ {file = "tokenize_rt-6.1.0.tar.gz", hash = "sha256:e8ee836616c0877ab7c7b54776d2fefcc3bde714449a206762425ae114b53c86"},
]
[[package]]
name = "tomli"
-version = "2.0.1"
+version = "2.2.1"
description = "A lil' TOML parser"
optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
files = [
- {file = "tomli-2.0.1-py3-none-any.whl", hash = "sha256:939de3e7a6161af0c887ef91b7d41a53e7c5a1ca976325f429cb46ea9bc30ecc"},
- {file = "tomli-2.0.1.tar.gz", hash = "sha256:de526c12914f0c550d15924c62d72abc48d6fe7364aa87328337a31007fe8a4f"},
+ {file = "tomli-2.2.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:678e4fa69e4575eb77d103de3df8a895e1591b48e740211bd1067378c69e8249"},
+ {file = "tomli-2.2.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:023aa114dd824ade0100497eb2318602af309e5a55595f76b626d6d9f3b7b0a6"},
+ {file = "tomli-2.2.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ece47d672db52ac607a3d9599a9d48dcb2f2f735c6c2d1f34130085bb12b112a"},
+ {file = "tomli-2.2.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6972ca9c9cc9f0acaa56a8ca1ff51e7af152a9f87fb64623e31d5c83700080ee"},
+ {file = "tomli-2.2.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:c954d2250168d28797dd4e3ac5cf812a406cd5a92674ee4c8f123c889786aa8e"},
+ {file = "tomli-2.2.1-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:8dd28b3e155b80f4d54beb40a441d366adcfe740969820caf156c019fb5c7ec4"},
+ {file = "tomli-2.2.1-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:e59e304978767a54663af13c07b3d1af22ddee3bb2fb0618ca1593e4f593a106"},
+ {file = "tomli-2.2.1-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:33580bccab0338d00994d7f16f4c4ec25b776af3ffaac1ed74e0b3fc95e885a8"},
+ {file = "tomli-2.2.1-cp311-cp311-win32.whl", hash = "sha256:465af0e0875402f1d226519c9904f37254b3045fc5084697cefb9bdde1ff99ff"},
+ {file = "tomli-2.2.1-cp311-cp311-win_amd64.whl", hash = "sha256:2d0f2fdd22b02c6d81637a3c95f8cd77f995846af7414c5c4b8d0545afa1bc4b"},
+ {file = "tomli-2.2.1-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:4a8f6e44de52d5e6c657c9fe83b562f5f4256d8ebbfe4ff922c495620a7f6cea"},
+ {file = "tomli-2.2.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:8d57ca8095a641b8237d5b079147646153d22552f1c637fd3ba7f4b0b29167a8"},
+ {file = "tomli-2.2.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4e340144ad7ae1533cb897d406382b4b6fede8890a03738ff1683af800d54192"},
+ {file = "tomli-2.2.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:db2b95f9de79181805df90bedc5a5ab4c165e6ec3fe99f970d0e302f384ad222"},
+ {file = "tomli-2.2.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:40741994320b232529c802f8bc86da4e1aa9f413db394617b9a256ae0f9a7f77"},
+ {file = "tomli-2.2.1-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:400e720fe168c0f8521520190686ef8ef033fb19fc493da09779e592861b78c6"},
+ {file = "tomli-2.2.1-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:02abe224de6ae62c19f090f68da4e27b10af2b93213d36cf44e6e1c5abd19fdd"},
+ {file = "tomli-2.2.1-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:b82ebccc8c8a36f2094e969560a1b836758481f3dc360ce9a3277c65f374285e"},
+ {file = "tomli-2.2.1-cp312-cp312-win32.whl", hash = "sha256:889f80ef92701b9dbb224e49ec87c645ce5df3fa2cc548664eb8a25e03127a98"},
+ {file = "tomli-2.2.1-cp312-cp312-win_amd64.whl", hash = "sha256:7fc04e92e1d624a4a63c76474610238576942d6b8950a2d7f908a340494e67e4"},
+ {file = "tomli-2.2.1-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:f4039b9cbc3048b2416cc57ab3bda989a6fcf9b36cf8937f01a6e731b64f80d7"},
+ {file = "tomli-2.2.1-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:286f0ca2ffeeb5b9bd4fcc8d6c330534323ec51b2f52da063b11c502da16f30c"},
+ {file = "tomli-2.2.1-cp313-cp313-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a92ef1a44547e894e2a17d24e7557a5e85a9e1d0048b0b5e7541f76c5032cb13"},
+ {file = "tomli-2.2.1-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:9316dc65bed1684c9a98ee68759ceaed29d229e985297003e494aa825ebb0281"},
+ {file = "tomli-2.2.1-cp313-cp313-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:e85e99945e688e32d5a35c1ff38ed0b3f41f43fad8df0bdf79f72b2ba7bc5272"},
+ {file = "tomli-2.2.1-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:ac065718db92ca818f8d6141b5f66369833d4a80a9d74435a268c52bdfa73140"},
+ {file = "tomli-2.2.1-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:d920f33822747519673ee656a4b6ac33e382eca9d331c87770faa3eef562aeb2"},
+ {file = "tomli-2.2.1-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:a198f10c4d1b1375d7687bc25294306e551bf1abfa4eace6650070a5c1ae2744"},
+ {file = "tomli-2.2.1-cp313-cp313-win32.whl", hash = "sha256:d3f5614314d758649ab2ab3a62d4f2004c825922f9e370b29416484086b264ec"},
+ {file = "tomli-2.2.1-cp313-cp313-win_amd64.whl", hash = "sha256:a38aa0308e754b0e3c67e344754dff64999ff9b513e691d0e786265c93583c69"},
+ {file = "tomli-2.2.1-py3-none-any.whl", hash = "sha256:cb55c73c5f4408779d0cf3eef9f762b9c9f147a77de7b258bef0a5628adc85cc"},
+ {file = "tomli-2.2.1.tar.gz", hash = "sha256:cd45e1dc79c835ce60f7404ec8119f2eb06d38b1deba146f07ced3bbc44505ff"},
]
[[package]]
@@ -1123,13 +1266,13 @@ files = [
[[package]]
name = "typing-extensions"
-version = "4.12.1"
+version = "4.12.2"
description = "Backported and Experimental Type Hints for Python 3.8+"
optional = false
python-versions = ">=3.8"
files = [
- {file = "typing_extensions-4.12.1-py3-none-any.whl", hash = "sha256:6024b58b69089e5a89c347397254e35f1bf02a907728ec7fee9bf0fe837d203a"},
- {file = "typing_extensions-4.12.1.tar.gz", hash = "sha256:915f5e35ff76f56588223f15fdd5938f9a1cf9195c0de25130c627e4d597f6d1"},
+ {file = "typing_extensions-4.12.2-py3-none-any.whl", hash = "sha256:04e5ca0351e0f3f85c6853954072df659d0d13fac324d0072316b67d7794700d"},
+ {file = "typing_extensions-4.12.2.tar.gz", hash = "sha256:1a7ead55c7e559dd4dee8856e3a88b41225abfe1ce8df57b7c13915fe121ffb8"},
]
[[package]]
@@ -1159,31 +1302,35 @@ files = [
[[package]]
name = "xdg-base-dirs"
-version = "6.0.1"
+version = "6.0.2"
description = "Variables defined by the XDG Base Directory Specification"
optional = false
-python-versions = ">=3.10,<4.0"
+python-versions = "<4.0,>=3.10"
files = [
- {file = "xdg_base_dirs-6.0.1-py3-none-any.whl", hash = "sha256:63f6ebc1721ced2e86c340856e004ef829501a30a37e17079c52cfaf0e1741b9"},
- {file = "xdg_base_dirs-6.0.1.tar.gz", hash = "sha256:b4c8f4ba72d1286018b25eea374ec6fbf4fddda3d4137edf50de95de53e195a6"},
+ {file = "xdg_base_dirs-6.0.2-py3-none-any.whl", hash = "sha256:3c01d1b758ed4ace150ac960ac0bd13ce4542b9e2cdf01312dcda5012cfebabe"},
+ {file = "xdg_base_dirs-6.0.2.tar.gz", hash = "sha256:950504e14d27cf3c9cb37744680a43bf0ac42efefc4ef4acf98dc736cab2bced"},
]
[[package]]
name = "zipp"
-version = "3.19.1"
+version = "3.21.0"
description = "Backport of pathlib-compatible object wrapper for zip files"
optional = false
-python-versions = ">=3.8"
+python-versions = ">=3.9"
files = [
- {file = "zipp-3.19.1-py3-none-any.whl", hash = "sha256:2828e64edb5386ea6a52e7ba7cdb17bb30a73a858f5eb6eb93d8d36f5ea26091"},
- {file = "zipp-3.19.1.tar.gz", hash = "sha256:35427f6d5594f4acf82d25541438348c26736fa9b3afa2754bcd63cdb99d8e8f"},
+ {file = "zipp-3.21.0-py3-none-any.whl", hash = "sha256:ac1bbe05fd2991f160ebce24ffbac5f6d11d83dc90891255885223d42b3cd931"},
+ {file = "zipp-3.21.0.tar.gz", hash = "sha256:2c9958f6430a2040341a52eb608ed6dd93ef4392e02ffe219417c1b28b5dd1f4"},
]
[package.extras]
+check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)"]
+cover = ["pytest-cov"]
doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"]
-test = ["big-O", "jaraco.functools", "jaraco.itertools", "jaraco.test", "more-itertools", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-ignore-flaky", "pytest-mypy", "pytest-ruff (>=0.2.1)"]
+enabler = ["pytest-enabler (>=2.2)"]
+test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", "jaraco.test", "more-itertools", "pytest (>=6,!=8.1.*)", "pytest-ignore-flaky"]
+type = ["pytest-mypy"]
[metadata]
lock-version = "2.0"
python-versions = "^3.10"
-content-hash = "9970503efc0ced0dae48405b13280b9b71c87c9e91dbf92b17a977e6dd04441a"
+content-hash = "a63e155c94be1b4ed3fbbd4ebff4ce9d0a5562d63abeb76c485c6bb95ee837d4"
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
index 2d76dc206..9756040c9 100644
--- a/pykwasm/pyproject.toml
+++ b/pykwasm/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
[tool.poetry]
name = "pykwasm"
-version = "0.1.59"
+version = "0.1.118"
description = ""
authors = [
"Runtime Verification, Inc. ",
@@ -23,7 +23,7 @@ wasm-semantics = "pykwasm.kdist.plugin"
python = "^3.10"
cytoolz = "^0.12.1"
numpy = "^1.24.2"
-pyk = { git = "https://github.com/runtimeverification/k.git", tag="v7.0.106", subdirectory = "pyk" }
+kframework = "7.1.191"
py-wasm = { git = "https://github.com/runtimeverification/py-wasm.git", tag="0.2.1" }
[tool.poetry.group.dev.dependencies]
diff --git a/pykwasm/src/pykwasm/kdist/plugin.py b/pykwasm/src/pykwasm/kdist/plugin.py
index bda111e99..97d1f9554 100644
--- a/pykwasm/src/pykwasm/kdist/plugin.py
+++ b/pykwasm/src/pykwasm/kdist/plugin.py
@@ -51,7 +51,7 @@ def deps(self) -> tuple[str]:
'md_selector': 'k',
'warnings_to_errors': True,
'gen_glr_bison_parser': True,
- 'opt_level': 2,
+ 'opt_level': 3,
'ccopts': ['-g'],
},
),
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md
index a9bf64119..0dffdad7e 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data.md
@@ -34,7 +34,7 @@ And we use `OptionalId` to handle the case where an identifier could be omitted.
```k
syntax Identifier ::= IdentifierToken
- syntax OptionalId ::= "" [klabel(.Identifier), symbol]
+ syntax OptionalId ::= "" [symbol(.Identifier)]
| Identifier
// --------------------------------
```
@@ -88,15 +88,15 @@ WebAssembly has three kinds of [Value types](https://webassembly.github.io/spec/
3. [Reference types](https://webassembly.github.io/spec/core/syntax/types.html#reference-types)
```k
- syntax IValType ::= "i32" [klabel(i32), symbol] | "i64" [klabel(i64), symbol]
- syntax FValType ::= "f32" [klabel(f32), symbol] | "f64" [klabel(f64), symbol]
- syntax RefValType ::= "funcref" [klabel(funcref), symbol]
- | "externref" [klabel(externref), symbol]
+ syntax IValType ::= "i32" [symbol(i32)] | "i64" [symbol(i64)]
+ syntax FValType ::= "f32" [symbol(f32)] | "f64" [symbol(f64)]
+ syntax RefValType ::= "funcref" [symbol(funcref)]
+ | "externref" [symbol(externref)]
syntax ValType ::= IValType | FValType | RefValType
// ---------------------------------------
- syntax HeapType ::= "func" [klabel(func), symbol]
- | "extern" [klabel(extern), symbol]
+ syntax HeapType ::= "func" [symbol(func)]
+ | "extern" [symbol(extern)]
```
#### Type Constructors
@@ -120,8 +120,8 @@ For the core language, only regular integers are allowed.
### Type Mutability
```k
- syntax Mut ::= "const" [klabel(mutConst), symbol]
- | "var" [klabel(mutVar), symbol]
+ syntax Mut ::= "const" [symbol(mutConst)]
+ | "var" [symbol(mutVar)]
// -----------------------------------------------
```
@@ -158,8 +158,8 @@ module WASM-DATA-INTERNAL-SYNTAX
imports WASM-DATA-COMMON-SYNTAX
imports BOOL
- syntax ValStack ::= ".ValStack" [klabel(.ValStack), symbol]
- | Val ":" ValStack [klabel(concatValStack), symbol]
+ syntax ValStack ::= ".ValStack" [symbol(.ValStack)]
+ | Val ":" ValStack [symbol(concatValStack)]
```
### Values
@@ -167,10 +167,10 @@ module WASM-DATA-INTERNAL-SYNTAX
Proper values are numbers annotated with their types.
```k
- syntax IVal ::= "<" IValType ">" Int [klabel(IVal), symbol]
- syntax FVal ::= "<" FValType ">" Float [klabel(FVal), symbol]
- syntax RefVal ::= "<" RefValType ">" Int [klabel(RefVal), symbol]
- | "<" RefValType ">" "null" [klabel(RefValNull), symbol]
+ syntax IVal ::= "<" IValType ">" Int [symbol(IVal)]
+ syntax FVal ::= "<" FValType ">" Float [symbol(FVal)]
+ syntax RefVal ::= "<" RefValType ">" Int [symbol(RefVal)]
+ | "<" RefValType ">" "null" [symbol(RefValNull)]
syntax Val ::= IVal | FVal | RefVal
// ---------------------------
@@ -204,9 +204,9 @@ We also add `undefined` as a value, which makes many partial functions in the se
There are two basic type-constructors: sequencing (`[_]`) and function spaces (`_->_`).
```k
- syntax VecType ::= "[" ValTypes "]" [klabel(aVecType), symbol]
+ syntax VecType ::= "[" ValTypes "]" [symbol(aVecType)]
- syntax FuncType ::= VecType "->" VecType [klabel(aFuncType), symbol]
+ syntax FuncType ::= VecType "->" VecType [symbol(aFuncType)]
```
All told, a `Type` can be a value type, vector of types, or function type.
@@ -221,7 +221,7 @@ In some cases, an integer is optional, such as when either giving or omitting th
The sort `OptionalInt` provides this potentially "undefined" `Int`.
```k
- syntax OptionalInt ::= Int | ".Int" [klabel(.Int), symbol]
+ syntax OptionalInt ::= Int | ".Int" [symbol(.Int)]
```
### Integer bounds
@@ -332,8 +332,8 @@ For `Int`, however, a the context is irrelevant and the index always just resolv
Tables and memories have limits, defined as either a single `Int` or two `Int`s, representing min and max bounds.
```k
- syntax Limits ::= #limitsMin(Int) [klabel(limitsMin), symbol]
- | #limits(Int, Int) [klabel(limitsMinMax), symbol]
+ syntax Limits ::= #limitsMin(Int) [symbol(limitsMin)]
+ | #limits(Int, Int) [symbol(limitsMinMax)]
// ------------------------------------------------------------------
```
@@ -360,7 +360,7 @@ Also we can reverse a `ValTypes` with `#revt`
```k
syntax ValTypes ::= #revt ( ValTypes ) [function, total]
- | #revt ( ValTypes , ValTypes ) [function, total, klabel(#revtAux)]
+ | #revt ( ValTypes , ValTypes ) [function, total, symbol(#revtAux)]
// ------------------------------------------------------------------------------------------
rule #revt(VT) => #revt(VT, .ValTypes)
@@ -480,7 +480,7 @@ Some operations extend integers from 1, 2, or 4 bytes, so a special function wit
Function `#bool` converts a `Bool` into an `Int`.
```k
- syntax Int ::= #bool ( Bool ) [function, total, smtlib(boolToInt), symbol, klabel(boolToInt)]
+ syntax Int ::= #bool ( Bool ) [function, total, smtlib(boolToInt), symbol(boolToInt)]
// ----------------------------------------------------
rule #bool( B:Bool ) => 1 requires B
rule #bool( B:Bool ) => 0 requires notBool B
@@ -511,7 +511,7 @@ Each call site _must_ ensure that this is desired behavior before using these fu
| #take ( Int , ValStack ) [function, total]
| #drop ( Int , ValStack ) [function, total]
| #revs ( ValStack ) [function, total]
- | #revs ( ValStack , ValStack ) [function, total, klabel(#revsAux)]
+ | #revs ( ValStack , ValStack ) [function, total, symbol(#revsAux)]
// ------------------------------------------------------------------------------------------
rule #zero(.ValTypes) => .ValStack
rule #zero(ITYPE:IValType VTYPES) => < ITYPE > 0 : #zero(VTYPES)
@@ -538,7 +538,7 @@ Wasm uses a different character escape rule with K, so we need to define the `un
```k
syntax String ::= unescape(String) [function]
- | unescape(String, Int, String) [function, klabel(unescapeAux)]
+ | unescape(String, Int, String) [function, symbol(unescapeAux)]
// -------------------------------------------------------------------------------
rule unescape(S ) => unescape(S, 1, "")
rule unescape(S, IDX, SB) => SB requires IDX ==Int lengthString(S) -Int 1
@@ -616,7 +616,7 @@ The strings to connect needs to be unescaped before concatenated, because the `u
```k
syntax String ::= #concatDS ( DataString ) [function]
- | #concatDS ( DataString, String ) [function, klabel(#concatDSAux)]
+ | #concatDS ( DataString, String ) [function, symbol(#concatDSAux)]
// -----------------------------------------------------------------------------------
rule #concatDS ( DS ) => #concatDS ( DS, "" )
rule #concatDS ( .DataString , S ) => S
@@ -690,7 +690,7 @@ endmodule
module WASM-DATA-SYMBOLIC [symbolic]
imports WASM-DATA-COMMON
- syntax Int ::= #signedTotal ( IValType , Int) [function, total, klabel(#signedTotal), symbol, no-evaluators, smtlib(signedTotal)]
+ syntax Int ::= #signedTotal ( IValType , Int) [function, total, symbol(#signedTotal), no-evaluators, smtlib(signedTotal)]
rule #signedTotal(Arg0:IValType, Arg1:Int)
=> #signed(Arg0, Arg1)
@@ -730,4 +730,4 @@ module WASM-DATA
imports WASM-DATA-CONCRETE
imports WASM-DATA-SYMBOLIC
endmodule
-```
\ No newline at end of file
+```
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/int-type.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/int-type.k
index 788695e39..137be6e4c 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/int-type.k
+++ b/pykwasm/src/pykwasm/kdist/wasm-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/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-int.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-int.k
index f1f08d136..8606e0f33 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-int.k
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-int.k
@@ -10,22 +10,22 @@ module LIST-INT
syntax ListInt [hook(LIST.List)]
syntax ListInt ::= ListInt ListInt
[ left, function, total, hook(LIST.concat),
- klabel(_ListInt_), symbol, smtlib(smt_seq_concat),
+ symbol(_ListInt_), smtlib(smt_seq_concat),
assoc, unit(.ListInt), element(ListIntItem),
- format(%1%n%2)
+ format(%1%n%2), update(ListInt:set)
]
syntax ListInt ::= ".ListInt"
- [ function, total, hook(LIST.unit), klabel(.ListInt),
- symbol, smtlib(smt_seq_nil)
+ [ function, total, hook(LIST.unit), symbol(.ListInt),
+ smtlib(smt_seq_nil)
]
syntax ListInt ::= ListItem(WrappedInt)
- [ function, total, hook(LIST.element), klabel(ListIntItem),
- symbol, smtlib(smt_seq_elem)
+ [ function, total, hook(LIST.element), symbol(ListIntItem),
+ smtlib(smt_seq_elem)
]
syntax WrappedInt ::= ListInt "[" Int "]"
- [ function, hook(LIST.get), klabel(ListInt:get), symbol ]
+ [ function, hook(LIST.get), symbol(ListInt:get) ]
syntax ListInt ::= ListInt "[" index: Int "<-" value: WrappedInt "]"
- [function, hook(LIST.update), symbol, klabel(ListInt:set)]
+ [function, hook(LIST.update), symbol(ListInt:set)]
syntax ListInt ::= makeListInt(length: Int, value: WrappedInt)
[function, hook(LIST.make)]
syntax ListInt ::= updateList(dest: ListInt, index: Int, src: ListInt)
@@ -33,11 +33,11 @@ module LIST-INT
syntax ListInt ::= fillList(ListInt, index: Int, length: Int, value: WrappedInt)
[function, hook(LIST.fill)]
syntax ListInt ::= range(ListInt, fromFront: Int, fromBack: Int)
- [function, hook(LIST.range), klabel(ListInt:range), symbol]
+ [function, hook(LIST.range), symbol(ListInt:range)]
syntax Bool ::= WrappedInt "in" ListInt
- [function, total, hook(LIST.in), symbol, klabel(_inListInt_)]
+ [function, total, hook(LIST.in), symbol(_inListInt_)]
syntax Int ::= size(ListInt)
- [function, total, hook(LIST.size), symbol, klabel (sizeListInt), smtlib(smt_seq_len)]
+ [function, total, hook(LIST.size), symbol(sizeListInt), smtlib(smt_seq_len)]
endmodule
module LIST-INT-PRIMITIVE
@@ -46,15 +46,15 @@ module LIST-INT-PRIMITIVE
imports LIST-INT
syntax WrappedInt ::= ListInt "[" Int "]" "orDefault" WrappedInt
- [ function, total, klabel(ListInt:getOrDefault), symbol ]
+ [ function, total, symbol(ListInt:getOrDefault) ]
syntax Int ::= ListInt "{{" Int "}}"
- [function, symbol, klabel(ListInt:primitiveLookup)]
+ [function, symbol(ListInt:primitiveLookup)]
// -----------------------------------------------------------
rule L:ListInt {{ I:Int }} => unwrap( L[ I ] )
-
+
syntax Int ::= ListInt "{{" Int "}}" "orDefault" Int
- [ function, total, symbol, klabel(ListInt:primitiveLookupOrDefault) ]
+ [ function, total, symbol(ListInt:primitiveLookupOrDefault) ]
// -----------------------------------------------------------------------------
rule L:ListInt {{ I:Int }} orDefault Value:Int
=> unwrap( L [I] orDefault wrap(Value) )
@@ -77,12 +77,12 @@ module LIST-INT-PRIMITIVE
[simplification]
syntax ListInt ::= ListItemWrap( Int )
- [function, total, symbol, klabel(ListIntItemWrap)]
+ [function, total, symbol(ListIntItemWrap)]
rule ListItemWrap( B:Int ) => ListItem(wrap(B))
syntax ListInt ::= ListInt "{{" Int "<-" Int "}}"
- [function, symbol, klabel(ListInt:primitiveSet)]
+ [function, symbol(ListInt:primitiveSet)]
// -----------------------------------------------------------
rule L:ListInt {{ I:Int <- V:Int }}
=> L[ I <- wrap(V)]
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k
index 4c2f437db..d2e8192e7 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k
@@ -10,22 +10,22 @@ module LIST-REF
syntax ListRef [hook(LIST.List)]
syntax ListRef ::= ListRef ListRef
[ left, function, total, hook(LIST.concat),
- klabel(_ListRef_), symbol, smtlib(smt_seq_concat),
+ symbol(_ListRef_), smtlib(smt_seq_concat),
assoc, unit(.ListRef), element(ListRefItem),
- format(%1%n%2)
+ format(%1%n%2), update(ListRef:set)
]
syntax ListRef ::= ".ListRef"
- [ function, total, hook(LIST.unit), klabel(.ListRef),
- symbol, smtlib(smt_seq_nil)
+ [ function, total, hook(LIST.unit), symbol(.ListRef),
+ smtlib(smt_seq_nil)
]
syntax ListRef ::= ListItem(RefVal)
- [ function, total, hook(LIST.element), klabel(ListRefItem),
- symbol, smtlib(smt_seq_elem)
+ [ function, total, hook(LIST.element), symbol(ListRefItem),
+ smtlib(smt_seq_elem)
]
syntax RefVal ::= ListRef "[" Int "]"
- [ function, hook(LIST.get), klabel(ListRef:get), symbol ]
+ [ function, hook(LIST.get), symbol(ListRef:get) ]
syntax ListRef ::= ListRef "[" index: Int "<-" value: RefVal "]"
- [function, hook(LIST.update), symbol, klabel(ListRef:set)]
+ [function, hook(LIST.update), symbol(ListRef:set)]
syntax ListRef ::= makeListRef(length: Int, value: RefVal)
[function, hook(LIST.make)]
syntax ListRef ::= updateList(dest: ListRef, index: Int, src: ListRef)
@@ -33,11 +33,11 @@ module LIST-REF
syntax ListRef ::= fillList(ListRef, index: Int, length: Int, value: RefVal)
[function, hook(LIST.fill)]
syntax ListRef ::= range(ListRef, fromFront: Int, fromBack: Int)
- [function, hook(LIST.range), klabel(ListRef:range), symbol]
+ [function, hook(LIST.range), symbol(ListRef:range)]
syntax Bool ::= RefVal "in" ListRef
- [function, total, hook(LIST.in), symbol, klabel(_inListRef_)]
+ [function, total, hook(LIST.in), symbol(_inListRef_)]
syntax Int ::= size(ListRef)
- [function, total, hook(LIST.size), symbol, klabel (sizeListRef), smtlib(smt_seq_len)]
+ [function, total, hook(LIST.size), symbol(sizeListRef), smtlib(smt_seq_len)]
endmodule
module LIST-REF-EXTENSIONS
@@ -46,7 +46,7 @@ module LIST-REF-EXTENSIONS
imports INT
syntax RefVal ::= ListRef "[" Int "]" "orDefault" RefVal
- [ function, total, klabel(ListRef:getOrDefault), symbol ]
+ [ function, total, symbol(ListRef:getOrDefault) ]
// ----------------------------------------------------------------
rule ListItem(V:RefVal) _:ListRef [0] orDefault _:RefVal
=> V
@@ -66,12 +66,12 @@ module LIST-REF-EXTENSIONS
[simplification]
syntax RefVal ::= getRefOrNull(ListRef, Int)
- [ function, total, klabel(ListRef:getOrNull), symbol ]
+ [ function, total, symbol(ListRef:getOrNull) ]
// -------------------------------------------------------------
rule getRefOrNull(L, N) => L [N] orDefault ( null)
syntax ListRef ::= makeListRefTotal(Int, RefVal)
- [function, total, klabel(ListRef:makeTotal), symbol]
+ [function, total, symbol(ListRef:makeTotal)]
// ----------------------------------------------------
rule makeListRefTotal(N, V) => makeListRef(N, V)
requires N >=Int 0
@@ -79,11 +79,11 @@ module LIST-REF-EXTENSIONS
requires N dropListRef(N -Int 1, L)
requires N >Int 0
rule dropListRef(_, L) => L
[owise]
-endmodule
\ No newline at end of file
+endmodule
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k
deleted file mode 100644
index 6238a8e07..000000000
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k
+++ /dev/null
@@ -1,462 +0,0 @@
-
-requires "int-type.k"
-// requires "int-type.k"
-requires "list-int.k"
-
-module MAP-INT-TO-INT
- imports private BOOL-SYNTAX
- imports private INT-SYNTAX
- imports private LIST-INT
- imports private LIST-INT
- // imports private LIST
- // imports private SET-INT
- imports private SET
- imports INT-TYPE
- imports INT-TYPE
-
- syntax Int
- syntax Int
-
- syntax MapIntToInt [hook(MAP.Map)]
- syntax MapIntToInt ::= MapIntToInt MapIntToInt
- [ left, function, hook(MAP.concat), klabel(_MapIntToInt_),
- symbol, assoc, comm, unit(.MapIntToInt), element(_Int2Int|->_),
- index(0), format(%1%n%2)
- ]
- syntax MapIntToInt ::= ".MapIntToInt"
- [ function, total, hook(MAP.unit),
- klabel(.MapIntToInt), symbol
- ]
- syntax MapIntToInt ::= WrappedInt "Int2Int|->" WrappedInt
- [ function, total, hook(MAP.element),
- klabel(_Int2Int|->_), symbol,
- injective
- ]
-
- syntax priority _Int2Int|->_ > _MapIntToInt_ .MapIntToInt
- syntax non-assoc _Int2Int|->_
- syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]"
- [function, hook(MAP.lookup), klabel(MapIntToInt:lookup), symbol]
- syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" "orDefault" WrappedInt
- [ function, total, hook(MAP.lookupOrDefault),
- klabel(MapIntToInt:lookupOrDefault), symbol
- ]
- syntax MapIntToInt ::= MapIntToInt "[" key: WrappedInt "<-" value: WrappedInt "]"
- [ function, total, klabel(MapIntToInt:update), symbol,
- hook(MAP.update), prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "[" WrappedInt "<-" "undef" "]"
- [ function, total, hook(MAP.remove),
- klabel(_MapIntToInt[_<-undef]), symbol
- ]
- syntax MapIntToInt ::= MapIntToInt "-Map" MapIntToInt
- [ function, total, hook(MAP.difference) ]
- syntax MapIntToInt ::= updateMap(MapIntToInt, MapIntToInt)
- [function, total, hook(MAP.updateAll)]
-
- syntax MapIntToInt ::= removeAll(MapIntToInt, Set)
- [function, total, hook(MAP.removeAll)]
- // syntax MapIntToInt ::= removeAll(MapIntToInt, SetInt)
- // [function, total, hook(MAP.removeAll)]
-
- syntax Set ::= keys(MapIntToInt)
- [function, total, hook(MAP.keys)]
- // syntax SetInt ::= keys(MapIntToInt)
- // [function, total, hook(MAP.keys)]
-
- // syntax List ::= "keys_list" "(" MapIntToInt ")"
- // [function, hook(MAP.keys_list)]
- syntax ListInt ::= "keys_list" "(" MapIntToInt ")"
- [function, hook(MAP.keys_list)]
-
- syntax Bool ::= WrappedInt "in_keys" "(" MapIntToInt ")"
- [function, total, hook(MAP.in_keys)]
-
- // syntax List ::= values(MapIntToInt)
- // [function, hook(MAP.values)]
- syntax ListInt ::= values(MapIntToInt)
- [function, hook(MAP.values)]
-
- syntax Int ::= size(MapIntToInt)
- [function, total, hook(MAP.size), klabel(MapIntToInt.sizeMap), symbol]
- syntax Bool ::= MapIntToInt "<=Map" MapIntToInt
- [function, total, hook(MAP.inclusion)]
- syntax WrappedInt ::= choice(MapIntToInt)
- [function, hook(MAP.choice), klabel(MapIntToInt:choice), symbol]
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE
- imports MAP-INT-TO-INT-PRIMITIVE-CONCRETE
- imports MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE-CONCRETE [concrete]
- imports public BOOL
- imports private K-EQUAL
- imports public MAP-INT-TO-INT
-
- syntax Int ::= MapIntToInt "{{" Int "}}"
- [function, klabel(MapIntToInt:primitiveLookup), symbol]
- syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int
- [ function, total, klabel(MapIntToInt:primitiveLookupOrDefault), symbol ]
- syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}"
- [ function, total, klabel(MapIntToInt:primitiveUpdate), symbol,
- prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}"
- [ function, total, klabel(MapIntToInt:primitiveRemove), symbol ]
- syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}"
- [function, total, klabel(MapIntToInt:primitiveInKeys), symbol]
-
- rule (M:MapIntToInt {{ Key:Int }})
- => (unwrap( M[wrap(Key)] ))
- rule M:MapIntToInt {{ Key:Int }} orDefault Value:Int
- => unwrap( M[wrap(Key)] orDefault wrap(Value) )
- rule M:MapIntToInt {{ Key:Int <- Value:Int }}
- => M[wrap(Key) <- wrap(Value)]
- rule M:MapIntToInt {{ Key:Int <- undef }}
- => M[wrap(Key) <- undef]
- rule Key:Int in_keys {{ M:MapIntToInt }} => wrap(Key) in_keys(M)
-endmodule
-
-module MAP-INT-TO-INT-PRIMITIVE-SYMBOLIC [symbolic]
- imports public BOOL
- imports private K-EQUAL
- imports public MAP-INT-TO-INT
- imports private MAP-INT-TO-INT-KORE-SYMBOLIC
-
- syntax Int ::= MapIntToInt "{{" Int "}}"
- [function, symbol, klabel(MapIntToInt:primitiveLookup)]
- syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int
- [ function, total, symbol, klabel(MapIntToInt:primitiveLookupOrDefault) ]
- syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}"
- [ function, total, klabel(MapIntToInt:primitiveUpdate), symbol,
- prefer
- ]
- syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}"
- [ function, total, symbol, klabel(MapIntToInt:primitiveRemove) ]
- syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}"
- [function, total, symbol, klabel(MapIntToInt:primitiveInKeys)]
-
- // Definitions
- // -----------
-
- rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt)
- {{ Key:Int }}
- => unwrap( V )
- ensures notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> V:WrappedInt M:MapIntToInt)
- {{ Key:Int }} orDefault _:Int
- => unwrap( V )
- ensures notBool Key in_keys {{ M }}
- rule M:MapIntToInt {{ Key:Int }} orDefault V:Int
- => V
- requires notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt)
- {{ Key:Int <- Value:Int }}
- => (wrap(Key) Int2Int|-> wrap(Value)) M
- rule M:MapIntToInt {{ Key:Int <- Value:Int }}
- => (wrap(Key) Int2Int|-> wrap(Value)) M
- requires notBool Key in_keys {{ M }}
-
- rule (wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt)
- {{ Key:Int <- undef }}
- => M
- ensures notBool Key in_keys {{ M }}
- rule M:MapIntToInt {{ Key:Int <- undef }}
- => M
- requires notBool Key in_keys {{ M }}
-
- rule Key:Int in_keys
- {{wrap(Key) Int2Int|-> _:WrappedInt M:MapIntToInt}}
- => true
- ensures notBool Key in_keys {{ M }}
- rule _Key:Int in_keys {{ .MapIntToInt }}
- => false
- // TODO: This may create an exponential evaluation tree, depending on how
- // caching works in the backend. It should be rewritten to finish in
- // O(n^2) or something like that, where n is the number of explicit keys
- // in the map.
- rule Key:Int in_keys
- {{Key2:WrappedInt Int2Int|-> _:WrappedInt M:MapIntToInt}}
- => Key in_keys {{ M }}
- requires Key =/=K unwrap( Key2 )
- ensures notBool Key2 in_keys (M)
- [simplification]
-
- // Translation rules
- rule M:MapIntToInt[Key:WrappedInt]
- => wrap(M{{unwrap( Key )}})
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt]
- => wrap(M{{unwrap( Key )}})
- [simplification, symbolic(Key)]
- rule M:MapIntToInt{{Key}}
- => unwrap( M[wrap(Key)] )
- [simplification, concrete]
-
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(M)]
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(Key)]
- rule M:MapIntToInt [ Key:WrappedInt ] orDefault Value:WrappedInt
- => wrap(M {{ unwrap( Key ) }} orDefault unwrap( Value ))
- [simplification, symbolic(Value)]
- rule M:MapIntToInt{{Key}} orDefault Value
- => unwrap( M[wrap(Key)] orDefault wrap(Value) )
- [simplification, concrete]
-
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(Key)]
- rule M:MapIntToInt[Key:WrappedInt <- Value:WrappedInt]
- => M {{ unwrap( Key ) <- unwrap( Value ) }}
- [simplification, symbolic(Value)]
- rule M:MapIntToInt{{Key <- Value}} => M[wrap(Key) <- wrap(Value) ]
- [simplification, concrete]
-
- rule M:MapIntToInt[Key:WrappedInt <- undef]
- => M {{ unwrap( Key ) <- undef }}
- [simplification, symbolic(M)]
- rule M:MapIntToInt[Key:WrappedInt <- undef]
- => M {{ unwrap( Key ) <- undef }}
- [simplification, symbolic(Key)]
- rule M:MapIntToInt{{Key <- undef}} => M[wrap(Key) <- undef]
- [simplification, concrete]
-
- rule Key:WrappedInt in_keys (M:MapIntToInt)
- => unwrap( Key ) in_keys {{M}}
- [simplification, symbolic(M)]
- rule Key:WrappedInt in_keys (M:MapIntToInt)
- => unwrap( Key ) in_keys {{M}}
- [simplification, symbolic(Key)]
- rule Key in_keys {{M:MapIntToInt}} => wrap(Key) in_keys(M)
- [simplification, concrete]
-
- // Symbolic execution rules
- // ------------------------
- syntax Bool ::= definedPrimitiveLookup(MapIntToInt, Int) [function, total]
- rule definedPrimitiveLookup(M:MapIntToInt, K:Int) => K in_keys{{M}}
-
- rule #Ceil(@M:MapIntToInt {{@K:Int}})
- => {definedPrimitiveLookup(@M, @K) #Equals true}
- #And #Ceil(@M) #And #Ceil(@K)
- [simplification]
-
- rule M:MapIntToInt {{ K <- _ }} {{ K <- V }} => M {{ K <- V }} [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- V2 }}
- => (K1 Int2Int|-> V1 (M {{ K2 <- V2 }}))
- requires unwrap( K1 ) =/=K K2
- [simplification]
-
- rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- undef }}
- => (K1 Int2Int|-> V1 (M {{ K2 <- undef }}))
- requires unwrap( K1 ) =/=K K2
- [simplification]
-
- rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} => M {{K2}}
- requires unwrap( K1 ) =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} => V1 [simplification]
- rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} => MAP {{ K2 }}
- requires K1 =/=K K2
- [simplification]
-
- rule (K1 Int2Int|-> _V M:MapIntToInt) {{ K2 }} orDefault D
- => M {{K2}} orDefault D
- requires unwrap( K1 ) =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt {{ K <- V1 }}) {{ K }} orDefault _ => V1 [simplification]
- rule ( MAP:MapIntToInt {{ K1 <- _V1 }}) {{ K2 }} orDefault D
- => MAP {{ K2 }} orDefault D
- requires K1 =/=K K2
- [simplification]
-
- rule K in_keys{{_M:MapIntToInt {{ K <- undef }} }} => false [simplification]
- rule K in_keys{{_M:MapIntToInt {{ K <- _ }} }} => true [simplification]
- rule K1 in_keys{{ M:MapIntToInt {{ K2 <- _ }} }}
- => true requires K1 ==K K2 orBool K1 in_keys{{M}}
- [simplification]
- rule K1 in_keys{{ M:MapIntToInt {{ K2 <- _ }} }}
- => K1 in_keys {{ M }}
- requires K1 =/=K K2
- [simplification]
-
- rule K1 in_keys {{ (K2 Int2Int|-> V) M:MapIntToInt }}
- => K1 ==K unwrap( K2 ) orBool K1 in_keys {{ M }}
- requires definedMapElementConcat(K2, V, M)
- [simplification(100)]
-
-
- rule {false #Equals @Key in_keys{{ Key' Int2Int|-> Val @M:MapIntToInt }}}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({ @Key #Equals unwrap( Key' ) })
- #And {false #Equals @Key in_keys{{@M}}}
- [simplification]
- rule {@Key in_keys{{Key' Int2Int|-> Val @M:MapIntToInt}} #Equals false}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals unwrap( Key' ) })
- #And {@Key in_keys{{@M}} #Equals false}
- [simplification]
-
-endmodule
-
-module MAP-INT-TO-INT-KORE-SYMBOLIC
- imports MAP-INT-TO-INT
- imports private K-EQUAL
- imports private BOOL
-
- syntax Bool ::= definedMapElementConcat(WrappedInt, WrappedInt, MapIntToInt) [function, total]
- rule definedMapElementConcat(K, _V, M:MapIntToInt) => notBool K in_keys(M)
-
- rule #Ceil(@M:MapIntToInt [@K:WrappedInt])
- => {(@K in_keys(@M)) #Equals true}
- #And #Ceil(@M) #And #Ceil(@K)
- [simplification]
-
- rule (K Int2Int|-> _ M:MapIntToInt) [ K <- V ] => (K Int2Int|-> V M) [simplification]
- rule M:MapIntToInt [ K <- V ] => (K Int2Int|-> V M) requires notBool (K in_keys(M))
- [simplification]
- rule M:MapIntToInt [ K <- _ ] [ K <- V ] => M [ K <- V ] [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- V2 ] => (K1 Int2Int|-> V1 (M [ K2 <- V2 ]))
- requires K1 =/=K K2
- [simplification]
-
- rule (K Int2Int|-> _ M:MapIntToInt) [ K <- undef ] => M
- ensures notBool (K in_keys(M))
- [simplification]
- rule M:MapIntToInt [ K <- undef ] => M
- requires notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> V1 M:MapIntToInt) [ K2 <- undef ]
- => (K1 Int2Int|-> V1 (M [ K2 <- undef ]))
- requires K1 =/=K K2
- [simplification]
-
- rule (K Int2Int|-> V M:MapIntToInt) [ K ] => V
- ensures notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] => M [K2]
- requires K1 =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] => V1 [simplification]
- rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] => MAP [ K2 ]
- requires K1 =/=K K2
- [simplification]
-
- rule (K Int2Int|-> V M:MapIntToInt) [ K ] orDefault _ => V
- ensures notBool (K in_keys(M))
- [simplification]
- rule (K1 Int2Int|-> _V M:MapIntToInt) [ K2 ] orDefault D
- => M [K2] orDefault D
- requires K1 =/=K K2
- ensures notBool (K1 in_keys(M))
- [simplification]
- rule (_MAP:MapIntToInt [ K <- V1 ]) [ K ] orDefault _ => V1 [simplification]
- rule ( MAP:MapIntToInt [ K1 <- _V1 ]) [ K2 ] orDefault D
- => MAP [ K2 ] orDefault D
- requires K1 =/=K K2
- [simplification]
- rule .MapIntToInt [ _ ] orDefault D => D [simplification]
-
- rule K in_keys(_M:MapIntToInt [ K <- undef ]) => false [simplification]
- rule K in_keys(_M:MapIntToInt [ K <- _ ]) => true [simplification]
- rule K1 in_keys(M:MapIntToInt [ K2 <- _ ])
- => true requires K1 ==K K2 orBool K1 in_keys(M)
- [simplification]
- rule K1 in_keys(M:MapIntToInt [ K2 <- _ ])
- => K1 in_keys(M)
- requires K1 =/=K K2
- [simplification]
-
- rule K in_keys((K Int2Int|-> V) M:MapIntToInt)
- => true
- requires definedMapElementConcat(K, V, M)
- [simplification(50)]
- rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt)
- => K1 in_keys(M)
- requires true
- andBool definedMapElementConcat(K2, V, M)
- andBool K1 =/=K K2
- [simplification(50)]
- rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt)
- => K1 ==K K2 orBool K1 in_keys(M)
- requires definedMapElementConcat(K2, V, M)
- [simplification(100)]
-
-
- rule {false #Equals @Key in_keys(.MapIntToInt)} => #Ceil(@Key) [simplification]
- rule {@Key in_keys(.MapIntToInt) #Equals false} => #Ceil(@Key) [simplification]
- rule {false #Equals @Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt)}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals Key'})
- #And {false #Equals @Key in_keys(@M)}
- [simplification]
- rule {@Key in_keys(Key' Int2Int|-> Val @M:MapIntToInt) #Equals false}
- => #Ceil(@Key) #And #Ceil(Key' Int2Int|-> Val @M)
- #And #Not({@Key #Equals Key'})
- #And {@Key in_keys(@M) #Equals false}
- [simplification]
-endmodule
-
-module MAP-INT-TO-INT-CURLY-BRACE
- imports private BOOL
- imports private K-EQUAL-SYNTAX
- imports MAP-INT-TO-INT
-
- syntax MapIntToInt ::= MapIntToInt "{" key:WrappedInt "<-" value:WrappedInt "}"
- [function, total, symbol, klabel(MapIntToInt:curly_update)]
- rule M:MapIntToInt{Key <- Value} => M (Key Int2Int|-> Value)
- requires notBool Key in_keys(M)
- rule (Key Int2Int|-> _ M:MapIntToInt){Key <- Value}
- => M (Key Int2Int|-> Value)
- rule (M:MapIntToInt{Key <- Value})(A Int2Int|-> B N:MapIntToInt)
- => (M (A Int2Int|-> B)) {Key <- Value} N
- requires notBool A ==K Key
- [simplification]
-
- rule M:MapIntToInt{Key1 <- Value1}[Key2 <- Value2]
- => ((M:MapIntToInt[Key2 <- Value2]{Key1 <- Value1}) #And #Not ({Key1 #Equals Key2}))
- #Or ((M:MapIntToInt[Key2 <- Value2]) #And {Key1 #Equals Key2})
- [simplification(20)]
- rule M:MapIntToInt[Key <- Value]
- => M:MapIntToInt{Key <- Value}
- [simplification(100)]
- rule M:MapIntToInt{Key1 <- _Value1}[Key2] orDefault Value2
- => M[Key2] orDefault Value2
- requires Key1 =/=K Key2
- [simplification]
- rule _M:MapIntToInt{Key <- Value1}[Key] orDefault _Value2
- => Value1
- [simplification]
- // rule M:MapIntToInt{Key1 <- Value1}[Key2] orDefault Value2
- // => (M[Key2] orDefault Value2 #And #Not ({Key1 #Equals Key2}))
- // #Or (Value1 #And {Key1 #Equals Key2})
- // [simplification]
- rule M:MapIntToInt{Key1 <- Value1}[Key2]
- => (M[Key2] #And #Not ({Key1 #Equals Key2}))
- #Or (Value1 #And {Key1 #Equals Key2})
- [simplification]
-
- rule Key1 in_keys(_:MapIntToInt{Key1 <- _})
- => true
- [simplification(50)]
- rule Key1 in_keys(M:MapIntToInt{Key2 <- _})
- => Key1 in_keys(M)
- requires notBool Key1 ==K Key2
- [simplification(50)]
- rule K1 in_keys(M:MapIntToInt { K2 <- _ })
- => K1 ==K K2 orBool K1 in_keys(M)
- [simplification(100)]
-
-endmodule
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k
index 6372996ad..08d628844 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k
@@ -2,8 +2,8 @@ module SPARSE-BYTES-SYNTAX
imports BYTES
imports INT
- syntax SBItem ::= #empty(Int) [symbol, klabel(SBItem:empty)]
- | #bytes(Bytes) [symbol, klabel(SBItem:bytes)]
+ syntax SBItem ::= #empty(Int) [symbol(SBItem:empty)]
+ | #bytes(Bytes) [symbol(SBItem:bytes)]
syntax SBItemChunk ::= SBChunk(SBItem)
@@ -39,7 +39,7 @@ module SPARSE-BYTES
rule unwrap(.SparseBytes) => .Bytes
syntax SparseBytes ::= fromBytes(Bytes)
- [function, total, symbol, klabel(SparseBytes:fromBytes)]
+ [function, total, symbol(SparseBytes:fromBytes)]
// ---------------------------------------------------------
rule fromBytes(Bs) => SBChunk(#bytes(Bs))
@@ -67,7 +67,7 @@ module SPARSE-BYTES
syntax SparseBytes ::= substrSparseBytes(SparseBytes, from: Int, to: Int)
- [function, total, klabel(SparseBytes:substr), symbol]
+ [function, total, symbol(SparseBytes:substr)]
// ------------------------------------------------------------------------
rule substrSparseBytes(_, S, E) => .SparseBytes
requires notBool( 0 <=Int S andBool S <=Int E )
@@ -86,7 +86,7 @@ module SPARSE-BYTES
andBool size(SBI) >Int S
syntax SparseBytes ::= substrSBItem(SBItem, from: Int, to: Int)
- [function, total, klabel(SBItem:substr), symbol]
+ [function, total, symbol(SBItem:substr)]
// -------------------------------------------------------------
rule substrSBItem(_SBI, S, E) => .SparseBytes
requires S .SparseBytes
@@ -135,7 +135,7 @@ module REPLACE-AT-COMMON
requires size(SBI) <=Int S
syntax SparseBytes ::= replaceAtZ(Int, SparseBytes, Int, Bytes)
- [function, total, symbol, klabel(SparseBytes:replaceAtZ)]
+ [function, total, symbol(SparseBytes:replaceAtZ)]
// ---------------------------------------------------------------
////////////// S < 0
rule replaceAtZ(_, _, S, _) => .SparseBytes
@@ -176,7 +176,7 @@ module REPLACE-AT-COMMON
syntax SparseBytes ::= replaceAtB(Bytes, SparseBytes, Int, Bytes)
- [function, total, symbol, klabel(SparseBytes:replaceAtB)]
+ [function, total, symbol(SparseBytes:replaceAtB)]
// ---------------------------------------------------------------
////////// S + len(Bs) <= len(MB)
rule replaceAtB(MB, REST, S, Bs)
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
index 60c658bfa..cfb43da1f 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
@@ -286,12 +286,13 @@ Bounds on `#getRange`:
rule #getRange(_, _, WIDTH) true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification]
rule #getRange(_, _, WIDTH) < true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX [simplification]
- rule VAL1 +Int VAL2 true requires VAL1 true
+ requires VAL1 true requires WIDTH *Int 8 <=Int SHIFT
- [simplification]
```
`#wrap` over `#getRange`:
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/numeric.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/numeric.md
index c4fc186d8..f6dcf0bcb 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/numeric.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/numeric.md
@@ -10,96 +10,96 @@ requires "data.md"
module WASM-NUMERIC-SYNTAX
- syntax IUnOp ::= "clz" [klabel(aClz), symbol]
- | "ctz" [klabel(aCtz), symbol]
- | "popcnt" [klabel(aPopcnt), symbol]
+ syntax IUnOp ::= "clz" [symbol(aClz)]
+ | "ctz" [symbol(aCtz)]
+ | "popcnt" [symbol(aPopcnt)]
// ---------------------------------------------------
- syntax FUnOp ::= "abs" [klabel(aAbs) , symbol]
- | "neg" [klabel(aNeg) , symbol]
- | "sqrt" [klabel(aSqrt) , symbol]
- | "floor" [klabel(aFloor) , symbol]
- | "ceil" [klabel(aCeil) , symbol]
- | "trunc" [klabel(aTrunc) , symbol]
- | "nearest" [klabel(aNearest), symbol]
+ syntax FUnOp ::= "abs" [symbol(aAbs)]
+ | "neg" [symbol(aNeg)]
+ | "sqrt" [symbol(aSqrt)]
+ | "floor" [symbol(aFloor)]
+ | "ceil" [symbol(aCeil)]
+ | "trunc" [symbol(aTrunc)]
+ | "nearest" [symbol(aNearest)]
// -----------------------------------------------------
- syntax ExtendS ::= "extend8_s" [klabel(aExtend8_s) , symbol]
- | "extend16_s" [klabel(aExtend16_s), symbol]
- | "extend32_s" [klabel(aExtend32_s), symbol]
+ syntax ExtendS ::= "extend8_s" [symbol(aExtend8_s)]
+ | "extend16_s" [symbol(aExtend16_s)]
+ | "extend32_s" [symbol(aExtend32_s)]
// ---------------------------------------------------------------
- syntax IBinOp ::= "add" [klabel(intAdd), symbol]
- | "sub" [klabel(intSub), symbol]
- | "mul" [klabel(intMul), symbol]
- | "div_u" [klabel(intDiv_u), symbol]
- | "rem_u" [klabel(intRem_u), symbol]
- | "div_s" [klabel(intDiv_s), symbol]
- | "rem_s" [klabel(intRem_s), symbol]
- | "and" [klabel(intAnd), symbol]
- | "or" [klabel(intOr), symbol]
- | "xor" [klabel(intXor), symbol]
- | "shl" [klabel(intShl), symbol]
- | "shr_u" [klabel(intShr_u), symbol]
- | "shr_s" [klabel(intShr_s), symbol]
- | "rotl" [klabel(intRotl), symbol]
- | "rotr" [klabel(intRotr), symbol]
+ syntax IBinOp ::= "add" [symbol(intAdd)]
+ | "sub" [symbol(intSub)]
+ | "mul" [symbol(intMul)]
+ | "div_u" [symbol(intDiv_u)]
+ | "rem_u" [symbol(intRem_u)]
+ | "div_s" [symbol(intDiv_s)]
+ | "rem_s" [symbol(intRem_s)]
+ | "and" [symbol(intAnd)]
+ | "or" [symbol(intOr)]
+ | "xor" [symbol(intXor)]
+ | "shl" [symbol(intShl)]
+ | "shr_u" [symbol(intShr_u)]
+ | "shr_s" [symbol(intShr_s)]
+ | "rotl" [symbol(intRotl)]
+ | "rotr" [symbol(intRotr)]
// --------------------------------------------------
- syntax FBinOp ::= "add" [klabel(floatAdd), symbol]
- | "sub" [klabel(floatSub), symbol]
- | "mul" [klabel(floatMul), symbol]
- | "div" [klabel(floatDiv), symbol]
- | "min" [klabel(floatMin), symbol]
- | "max" [klabel(floatMax), symbol]
- | "copysign" [klabel(floatCopysign), symbol]
+ syntax FBinOp ::= "add" [symbol(floatAdd)]
+ | "sub" [symbol(floatSub)]
+ | "mul" [symbol(floatMul)]
+ | "div" [symbol(floatDiv)]
+ | "min" [symbol(floatMin)]
+ | "max" [symbol(floatMax)]
+ | "copysign" [symbol(floatCopysign)]
// ------------------------------------------------------------
- syntax TestOp ::= "eqz" [klabel(aEqz), symbol]
+ syntax TestOp ::= "eqz" [symbol(aEqz)]
// ----------------------------------------------
- syntax IRelOp ::= "eq" [klabel(intEq), symbol]
- | "ne" [klabel(intNe), symbol]
- | "lt_u" [klabel(intLt_u), symbol]
- | "gt_u" [klabel(intGt_u), symbol]
- | "lt_s" [klabel(intLt_s), symbol]
- | "gt_s" [klabel(intGt_s), symbol]
- | "le_u" [klabel(intLe_u), symbol]
- | "ge_u" [klabel(intGe_u), symbol]
- | "le_s" [klabel(intLe_s), symbol]
- | "ge_s" [klabel(intGe_s), symbol]
+ syntax IRelOp ::= "eq" [symbol(intEq)]
+ | "ne" [symbol(intNe)]
+ | "lt_u" [symbol(intLt_u)]
+ | "gt_u" [symbol(intGt_u)]
+ | "lt_s" [symbol(intLt_s)]
+ | "gt_s" [symbol(intGt_s)]
+ | "le_u" [symbol(intLe_u)]
+ | "ge_u" [symbol(intGe_u)]
+ | "le_s" [symbol(intLe_s)]
+ | "ge_s" [symbol(intGe_s)]
// --------------------------------------------------
- syntax FRelOp ::= "lt" [klabel(floatLt), symbol]
- | "gt" [klabel(floatGt), symbol]
- | "le" [klabel(floatLe), symbol]
- | "ge" [klabel(floatGe), symbol]
- | "eq" [klabel(floatEq), symbol]
- | "ne" [klabel(floatNe), symbol]
+ syntax FRelOp ::= "lt" [symbol(floatLt)]
+ | "gt" [symbol(floatGt)]
+ | "le" [symbol(floatLe)]
+ | "ge" [symbol(floatGe)]
+ | "eq" [symbol(floatEq)]
+ | "ne" [symbol(floatNe)]
// ------------------------------------------------
syntax CvtOp ::= Cvti32Op | Cvti64Op | Cvtf32Op | Cvtf64Op
// ----------------------------------------------------------
- syntax Cvti32Op ::= "extend_i32_u" [klabel(aExtend_i32_u), symbol]
- | "extend_i32_s" [klabel(aExtend_i32_s), symbol]
- | "convert_i32_s" [klabel(aConvert_i32_s), symbol]
- | "convert_i32_u" [klabel(aConvert_i32_u), symbol]
+ syntax Cvti32Op ::= "extend_i32_u" [symbol(aExtend_i32_u)]
+ | "extend_i32_s" [symbol(aExtend_i32_s)]
+ | "convert_i32_s" [symbol(aConvert_i32_s)]
+ | "convert_i32_u" [symbol(aConvert_i32_u)]
// --------------------------------------------------------------------
- syntax Cvti64Op ::= "wrap_i64" [klabel(aWrap_i64), symbol]
- | "convert_i64_s" [klabel(aConvert_i64_s), symbol]
- | "convert_i64_u" [klabel(aConvert_i64_u), symbol]
+ syntax Cvti64Op ::= "wrap_i64" [symbol(aWrap_i64)]
+ | "convert_i64_s" [symbol(aConvert_i64_s)]
+ | "convert_i64_u" [symbol(aConvert_i64_u)]
// --------------------------------------------------------------------
- syntax Cvtf32Op ::= "promote_f32" [klabel(aPromote_f32), symbol]
- | "trunc_f32_s" [klabel(aTrunc_f32_s), symbol]
- | "trunc_f32_u" [klabel(aTrunc_f32_u), symbol]
+ syntax Cvtf32Op ::= "promote_f32" [symbol(aPromote_f32)]
+ | "trunc_f32_s" [symbol(aTrunc_f32_s)]
+ | "trunc_f32_u" [symbol(aTrunc_f32_u)]
// ----------------------------------------------------------------
- syntax Cvtf64Op ::= "demote_f64" [klabel(aDemote_f64), symbol]
- | "trunc_f64_s" [klabel(aTrunc_f64_s), symbol]
- | "trunc_f64_u" [klabel(aTrunc_f64_u), symbol]
+ syntax Cvtf64Op ::= "demote_f64" [symbol(aDemote_f64)]
+ | "trunc_f64_s" [symbol(aTrunc_f64_s)]
+ | "trunc_f64_u" [symbol(aTrunc_f64_u)]
// ----------------------------------------------------------------
endmodule
@@ -115,9 +115,9 @@ module WASM-NUMERIC
`*UnOp` takes one oprand and returns a `Val`.
```k
- syntax Val ::= IValType "." IUnOp Int [klabel(intUnOp) , function]
- | FValType "." FUnOp Float [klabel(floatUnOp) , function]
- | IValType "." ExtendS Int [klabel(extendSUnOp), function]
+ syntax Val ::= IValType "." IUnOp Int [symbol(intUnOp) , function, total]
+ | FValType "." FUnOp Float [symbol(floatUnOp) , function]
+ | IValType "." ExtendS Int [symbol(extendSUnOp), function, total]
// ---------------------------------------------------------------------------
```
@@ -133,21 +133,33 @@ Note: The actual `ctz` operator considers the integer 0 to have *all* zero-bits,
```k
rule ITYPE . clz I1 => < ITYPE > #width(ITYPE) -Int #minWidth(I1)
+ requires 0 <=Int I1
rule ITYPE . ctz I1 => < ITYPE > #if I1 ==Int 0 #then #width(ITYPE) #else #ctz(I1) #fi
+ requires 0 <=Int I1
rule ITYPE . popcnt I1 => < ITYPE > #popcnt(I1)
+ requires 0 <=Int I1
+ rule _:IValType . _:IUnOp I1 => undefined
+ requires I1 0
- rule #minWidth(N) => 1 +Int #minWidth(N >>Int 1) requires N =/=Int 0
-
- rule #ctz(0) => 0
- rule #ctz(N) => #if N modInt 2 ==Int 1 #then 0 #else 1 +Int #ctz(N >>Int 1) #fi requires N =/=Int 0
-
- rule #popcnt(0) => 0
- rule #popcnt(N) => #bool(N modInt 2 ==Int 1) +Int #popcnt(N >>Int 1) requires N =/=Int 0
+ rule #minWidth(N) => 0 requires N ==Int 0
+ rule #minWidth(N) => 1 +Int #minWidth(N >>Int 1) requires N >Int 0
+ rule [minWidth-invalid]:
+ #minWidth(N) => -1 requires N 0 requires N ==Int 0
+ rule #ctz(N) => 0 requires N >Int 0 andBool N &Int 1 ==Int 1
+ rule #ctz(N) => 1 +Int #ctz(N >>Int 1) [owise]
+ rule [ctz-invalid]:
+ #ctz(N) => -1 requires N 0 requires N ==Int 0
+ rule #popcnt(N) => #bool(N &Int 1 ==Int 1) +Int #popcnt(N >>Int 1) requires N >Int 0
+ rule [popcnt-invalid]:
+ #popcnt(N) => -1 requires N
CUR
IDS
- wrap(#ContextLookup(IDS, TFIDX)) Int2Int|-> wrap(ADDR)
+ #ContextLookup(IDS, TFIDX) |-> ADDR
...
@@ -588,7 +588,7 @@ This checks that the last allocated memory has the given size and max value.
rule #assertMemoryData MODIDX (KEY , VAL) _MSG => .K ...
MODIDX
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
index 4d23c2dda..f4f0ffdee 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm-text.md
@@ -77,7 +77,7 @@ module WASM-TEXT-COMMON-SYNTAX
imports WASM-COMMON-SYNTAX
syntax WasmInt ::= Int
- syntax WasmInt ::= WasmIntToken [klabel(WasmInt), avoid, symbol, function]
+ syntax WasmInt ::= WasmIntToken [symbol(WasmInt), avoid, function]
syntax Index ::= Identifier
// ---------------------------
@@ -107,17 +107,29 @@ module WASM-TEXT-COMMON-SYNTAX
| "table.grow" Index
| "table.fill" Index
| "table.copy" Index Index
- | "table.copy" [macro]
| "table.init" Index Index
- | "table.init" Index [macro]
| "elem.drop" Index
| "call_indirect" Index TypeUse
- | "call_indirect" TypeUse [macro]
- // ---------------------------------------
+ // ---------------------------------------------------
+
// Abbreviations
+ syntax PlainInstr ::= "table.get" [macro]
+ | "table.set" [macro]
+ | "table.size" [macro]
+ | "table.grow" [macro]
+ | "table.fill" [macro]
+ | "table.copy" [macro]
+ | "table.init" Index [macro]
+ | "call_indirect" TypeUse [macro]
+ // -----------------------------------------------------
+ rule table.get => table.get 0
+ rule table.set => table.set 0
+ rule table.size => table.size 0
+ rule table.grow => table.grow 0
+ rule table.fill => table.fill 0
+ rule table.copy => table.copy 0 0
rule table.init I => table.init 0 I
rule call_indirect TU:TypeUse => call_indirect 0 TU
- rule table.copy => table.copy 0 0
syntax PlainInstr ::= IValType "." StoreOpM
| FValType "." StoreOpM
@@ -209,10 +221,10 @@ Imports can be declared like regular functions, memories, etc., by giving an inl
The following is the text format representation of an import specification.
```k
- syntax ImportDesc ::= "(" "func" OptionalId TypeUse ")" [klabel(funcImportDesc)]
- | "(" "global" OptionalId TextFormatGlobalType ")" [klabel(globImportDesc)]
- | "(" "table" OptionalId TableType ")" [klabel( tabImportDesc)]
- | "(" "memory" OptionalId MemType ")" [klabel( memImportDesc)]
+ syntax ImportDesc ::= "(" "func" OptionalId TypeUse ")" [symbol(funcImportDesc)]
+ | "(" "global" OptionalId TextFormatGlobalType ")" [symbol(globImportDesc)]
+ | "(" "table" OptionalId TableType ")" [symbol( tabImportDesc)]
+ | "(" "memory" OptionalId MemType ")" [symbol( memImportDesc)]
// -----------------------------------------------------------------------------------------------
```
@@ -1129,6 +1141,8 @@ The `align` parameter is for optimization only and is not allowed to influence t
rule #t2aInstr<_>(FTYPE:FValType.OP:LoadOp MemArg) => #load(FTYPE, OP, #getOffset(MemArg))
rule #t2aInstr<_>(memory.size) => memory.size
rule #t2aInstr<_>(memory.grow) => memory.grow
+ rule #t2aInstr<_>(memory.fill) => memory.fill
+ rule #t2aInstr<_>(memory.copy) => memory.copy
syntax Int ::= #getOffset ( MemArg ) [function, total]
// -----------------------------------------------------------
diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
index a0d4e8bfd..3a6b438d6 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md
@@ -5,7 +5,6 @@ WebAssembly State and Semantics
requires "data.md"
requires "data/list-int.k"
requires "data/list-ref.k"
-requires "data/map-int-to-int.k"
requires "data/sparse-bytes.k"
requires "data/tools.k"
requires "numeric.md"
@@ -76,29 +75,31 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list
**TODO**: Implement `Float` in the format of `-nan`, `nan:0x n:hexnum` and `hexfloat`.
```k
- syntax PlainInstr ::= IValType "." "const" WasmInt [klabel(aIConst), symbol]
- | FValType "." "const" Number [klabel(aFConst), symbol]
- | "ref.null" HeapType [klabel(aRef.null), symbol]
- | IValType "." IUnOp [klabel(aIUnOp), symbol]
- | FValType "." FUnOp [klabel(aFUnOp), symbol]
- | IValType "." ExtendS [klabel(aExtendS), symbol] // TODO this is more permissive than the official spec as it allows 'i32.extend32_s'
- | IValType "." IBinOp [klabel(aIBinOp), symbol]
- | FValType "." FBinOp [klabel(aFBinOp), symbol]
- | IValType "." TestOp [klabel(aTestOp), symbol]
- | IValType "." IRelOp [klabel(aIRelOp), symbol]
- | FValType "." FRelOp [klabel(aFRelOp), symbol]
- | ValType "." CvtOp [klabel(aCvtOp), symbol]
- | "drop" [klabel(aDrop), symbol]
- | "select" [klabel(aSelect), symbol]
- | "nop" [klabel(aNop), symbol]
- | "unreachable" [klabel(aUnreachable), symbol]
- | "return" [klabel(aReturn), symbol]
- | "memory.size" [klabel(aSize), symbol]
- | "memory.grow" [klabel(aGrow), symbol]
+ syntax PlainInstr ::= IValType "." "const" WasmInt [symbol(aIConst)]
+ | FValType "." "const" Number [symbol(aFConst)]
+ | "ref.null" HeapType [symbol(aRef.null)]
+ | IValType "." IUnOp [symbol(aIUnOp)]
+ | FValType "." FUnOp [symbol(aFUnOp)]
+ | IValType "." ExtendS [symbol(aExtendS)] // TODO this is more permissive than the official spec as it allows 'i32.extend32_s'
+ | IValType "." IBinOp [symbol(aIBinOp)]
+ | FValType "." FBinOp [symbol(aFBinOp)]
+ | IValType "." TestOp [symbol(aTestOp)]
+ | IValType "." IRelOp [symbol(aIRelOp)]
+ | FValType "." FRelOp [symbol(aFRelOp)]
+ | ValType "." CvtOp [symbol(aCvtOp)]
+ | "drop" [symbol(aDrop)]
+ | "select" [symbol(aSelect)]
+ | "nop" [symbol(aNop)]
+ | "unreachable" [symbol(aUnreachable)]
+ | "return" [symbol(aReturn)]
+ | "memory.size" [symbol(aSize)]
+ | "memory.grow" [symbol(aGrow)]
+ | "memory.fill" [symbol(aFill)]
+ | "memory.copy" [symbol(aCopy)]
// -----------------------------------
syntax TypeUse ::= TypeDecls
- | "(type" Index ")" [prefer, klabel(aTypeUseIndex), symbol] // TODO: Remove and move to wasm-text.
+ | "(type" Index ")" [prefer, symbol(aTypeUseIndex)] // TODO: Remove and move to wasm-text.
| "(type" Index ")" TypeDecls
syntax TypeKeyWord ::= "param" | "result"
syntax TypeDecl ::= "(" TypeDecl ")" [bracket]
@@ -107,17 +108,17 @@ The sorts `EmptyStmt` and `EmptyStmts` are administrative so that the empty list
syntax TypeDecls ::= List{TypeDecl , ""} [symbol(listTypeDecl), terminator-symbol(".List{\"listTypeDecl\"}")]
// -----------------------------------------------------------------
- syntax StoreOp ::= "store" [klabel(storeOpStore), symbol]
- | "store8" [klabel(storeOpStore8), symbol]
- | "store16" [klabel(storeOpStore16), symbol]
- | "store32" [klabel(storeOpStore32), symbol]
- syntax LoadOp ::= "load" [klabel(loadOpLoad), symbol]
- | "load8_u" [klabel(loadOpLoad8_u), symbol]
- | "load16_u" [klabel(loadOpLoad16_u), symbol]
- | "load32_u" [klabel(loadOpLoad32_u), symbol]
- | "load8_s" [klabel(loadOpLoad8_s), symbol]
- | "load16_s" [klabel(loadOpLoad16_s), symbol]
- | "load32_s" [klabel(loadOpLoad32_s), symbol]
+ syntax StoreOp ::= "store" [symbol(storeOpStore)]
+ | "store8" [symbol(storeOpStore8)]
+ | "store16" [symbol(storeOpStore16)]
+ | "store32" [symbol(storeOpStore32)]
+ syntax LoadOp ::= "load" [symbol(loadOpLoad)]
+ | "load8_u" [symbol(loadOpLoad8_u)]
+ | "load16_u" [symbol(loadOpLoad16_u)]
+ | "load32_u" [symbol(loadOpLoad32_u)]
+ | "load8_s" [symbol(loadOpLoad8_s)]
+ | "load16_s" [symbol(loadOpLoad16_s)]
+ | "load32_s" [symbol(loadOpLoad32_s)]
// --------------------------------------------------------------
```
@@ -184,8 +185,7 @@ Semantics
module WASM
imports LIST-INT
imports LIST-INT-PRIMITIVE
- imports MAP-INT-TO-INT
- imports MAP-INT-TO-INT-PRIMITIVE
+ imports MAP
imports WASM-COMMON-SYNTAX
imports WASM-INTERNAL-SYNTAX
imports WASM-DATA
@@ -219,9 +219,9 @@ module WASM
.Map
0
.Map
- .MapIntToInt
+ .Map
.Map
- .MapIntToInt
+ .Map
0
.Map
.Map
@@ -449,11 +449,16 @@ The `select` operator picks one of the second or third stack values based on the
_ : VALSTACK => VALSTACK
rule select => .K ...
- < i32 > C : V2 : V1 : VALSTACK
- => #if C =/=Int 0 #then V1 #else V2 #fi : VALSTACK
+ < i32 > C : V2 : V1 : VALSTACK
+ => V2 : VALSTACK
- requires #sameType(V1, V2)
+ requires C ==Int 0 andBool #sameType(V1, V2)
+ rule select => .K ...
+ < i32 > C : V2 : V1 : VALSTACK
+ => V1 : VALSTACK
+
+ requires C =/=Int 0 andBool #sameType(V1, V2)
```
Structured Control Flow
@@ -487,7 +492,7 @@ It simply executes the block then records a label with an empty continuation.
syntax BlockMetaData ::= OptionalInt
// ------------------------------------
- syntax Instr ::= #block(VecType, Instrs, BlockMetaData) [klabel(aBlock), symbol]
+ syntax Instr ::= #block(VecType, Instrs, BlockMetaData) [symbol(aBlock)]
// --------------------------------------------------------------------------------
rule #block(VECTYP, IS, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ...
VALSTACK => .ValStack
@@ -499,7 +504,7 @@ Upon reaching it, the label itself is executed.
Note that, unlike in the WebAssembly specification document, we do not need the special "context" operator here because the value and instruction stacks are separate.
```k
- syntax Instr ::= #br( Int ) [klabel(aBr), symbol]
+ syntax Instr ::= #br( Int ) [symbol(aBr)]
// -------------------------------------------------
rule #br(_IDX) ~> (_S:Stmt => .K) ...
rule #br(0 ) ~> label [ TYPES ] { IS } VALSTACK' => sequenceInstrs(IS) ...
@@ -507,7 +512,7 @@ Note that, unlike in the WebAssembly specification document, we do not need the
rule #br(N:Int) ~> _L:Label => #br(N -Int 1) ...
requires N >Int 0
- syntax Instr ::= "#br_if" "(" Int ")" [klabel(aBr_if), symbol]
+ syntax Instr ::= "#br_if" "(" Int ")" [symbol(aBr_if)]
// --------------------------------------------------------------
rule #br_if(IDX) => #br(IDX) ...
VAL : VALSTACK => VALSTACK
@@ -516,16 +521,22 @@ Note that, unlike in the WebAssembly specification document, we do not need the
VAL : VALSTACK => VALSTACK
requires VAL ==Int 0
- syntax Instr ::= "#br_table" "(" Ints ")" [klabel(aBr_table), symbol]
+ syntax Instr ::= "#br_table" "(" Ints ")" [symbol(aBr_table)]
// ---------------------------------------------------------------------
rule #br_table(ES) => #br(#getInts(ES, minInt(VAL, #lenInts(ES) -Int 1))) ...
VAL : VALSTACK => VALSTACK
+ requires 0 <=Int VAL
+ andBool #lenInts(ES) >Int 0
+ [preserves-definedness]
+ // preserves-definedness:
+ // - 0 <= VAL and minInt(VAL, #lenInts(ES) -Int 1) ensures #getInts(_) is defined
+
```
Finally, we have the conditional and loop instructions.
```k
- syntax Instr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [klabel(aIf), symbol]
+ syntax Instr ::= #if( VecType, then : Instrs, else : Instrs, blockInfo: BlockMetaData) [symbol(aIf)]
// ------------------------------------------------------------------------------------------------------------
rule #if(VECTYP, IS, _, _) => sequenceInstrs(IS) ~> label VECTYP { .Instrs } VALSTACK ...
< i32 > VAL : VALSTACK => VALSTACK
@@ -535,7 +546,7 @@ Finally, we have the conditional and loop instructions.
< i32 > VAL : VALSTACK => VALSTACK
requires VAL ==Int 0
- syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [klabel(aLoop), symbol]
+ syntax Instr ::= #loop(VecType, Instrs, BlockMetaData) [symbol(aLoop)]
// ------------------------------------------------------------------------------
rule #loop(VECTYP, IS, BLOCKMETA) => sequenceInstrs(IS) ~> label VECTYP { #loop(VECTYP, IS, BLOCKMETA) } VALSTACK ...
VALSTACK => .ValStack
@@ -565,9 +576,9 @@ The various `init_local` variants assist in setting up the `locals` cell.
The `*_local` instructions are defined here.
```k
- syntax Instr ::= "#local.get" "(" Int ")" [klabel(aLocal.get), symbol]
- | "#local.set" "(" Int ")" [klabel(aLocal.set), symbol]
- | "#local.tee" "(" Int ")" [klabel(aLocal.tee), symbol]
+ syntax Instr ::= "#local.get" "(" Int ")" [symbol(aLocal.get)]
+ | "#local.set" "(" Int ")" [symbol(aLocal.set)]
+ | "#local.tee" "(" Int ")" [symbol(aLocal.tee)]
// ----------------------------------------------------------------------
rule #local.get(I) => .K ...
VALSTACK => VALUE : VALSTACK
@@ -593,10 +604,10 @@ The specification can also include export directives.
The importing and exporting parts of specifications are dealt with in the respective sections for import and export.
```k
- syntax GlobalType ::= Mut ValType [klabel(aGlobalType), symbol]
+ syntax GlobalType ::= Mut ValType [symbol(aGlobalType)]
// ---------------------------------------------------------------
- syntax GlobalDefn ::= #global(type: GlobalType, init: Instrs, metadata: OptionalId) [klabel(aGlobalDefn), symbol]
+ syntax GlobalDefn ::= #global(type: GlobalType, init: Instrs, metadata: OptionalId) [symbol(aGlobalDefn)]
syntax Alloc ::= allocglobal (OptionalId, GlobalType)
// ----------------------------------------------------------
rule #global(... type: TYP, init: IS, metadata: OID) => sequenceInstrs(IS) ~> allocglobal(OID, TYP) ...
@@ -629,8 +640,8 @@ The importing and exporting parts of specifications are dealt with in the respec
The `get` and `set` instructions read and write globals.
```k
- syntax Instr ::= "#global.get" "(" Int ")" [klabel(aGlobal.get), symbol]
- | "#global.set" "(" Int ")" [klabel(aGlobal.set), symbol]
+ syntax Instr ::= "#global.get" "(" Int ")" [symbol(aGlobal.get)]
+ | "#global.set" "(" Int ")" [symbol(aGlobal.set)]
// ------------------------------------------------------------------------
rule #global.get(IDX) => .K ...
VALSTACK => VALUE : VALSTACK
@@ -670,14 +681,14 @@ The `get` and `set` instructions read and write globals.
- [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#table-instructions)
```k
- syntax Instr ::= "#table.get" "(" Int ")" [klabel(aTable.get), symbol]
- | "#table.set" "(" Int ")" [klabel(aTable.set), symbol]
- | "#table.size" "(" Int ")" [klabel(aTable.size), symbol]
- | "#table.grow" "(" Int ")" [klabel(aTable.grow), symbol]
- | "#table.fill" "(" Int ")" [klabel(aTable.fill), symbol]
- | "#table.copy" "(" Int "," Int ")" [klabel(aTable.copy), symbol]
- | "#table.init" "(" Int "," Int ")" [klabel(aTable.init), symbol]
- | "#elem.drop" "(" Int ")" [klabel(aElem.drop), symbol]
+ syntax Instr ::= "#table.get" "(" Int ")" [symbol(aTable.get)]
+ | "#table.set" "(" Int ")" [symbol(aTable.set)]
+ | "#table.size" "(" Int ")" [symbol(aTable.size)]
+ | "#table.grow" "(" Int ")" [symbol(aTable.grow)]
+ | "#table.fill" "(" Int ")" [symbol(aTable.fill)]
+ | "#table.copy" "(" Int "," Int ")" [symbol(aTable.copy)]
+ | "#table.init" "(" Int "," Int ")" [symbol(aTable.init)]
+ | "#elem.drop" "(" Int ")" [symbol(aElem.drop)]
// ---------------------------------------------------------------------------------
```
@@ -932,7 +943,7 @@ The `get` and `set` instructions read and write globals.
CUR
... TID |-> TA ...
- ... wrap(EID) Int2Int|-> wrap(EA) ...
+ ... EID |-> EA ...
...
@@ -965,7 +976,7 @@ The `get` and `set` instructions read and write globals.
CUR
CUR
- ... wrap(EID) Int2Int|-> wrap(EA) ...
+ ... EID |-> EA ...
...
@@ -1017,8 +1028,8 @@ The `get` and `set` instructions read and write globals.
- [Execution](https://webassembly.github.io/spec/core/exec/instructions.html#reference-instructions)
```k
- syntax Instr ::= "#ref.is_null" [klabel(aRef.is_null), symbol]
- | "#ref.func" "(" Int ")" [klabel(aRef.func), symbol]
+ syntax Instr ::= "#ref.is_null" [symbol(aRef.is_null)]
+ | "#ref.func" "(" Int ")" [symbol(aRef.func)]
// ------------------------------------------------------------------------
rule [ref.null.func]:
@@ -1074,8 +1085,8 @@ It may optionally be augmented by explicit inlined parameter and result declarat
A type use should start with `'(' 'type' x:typeidx ')'` followed by a group of inlined parameter or result declarations.
```k
- syntax FuncType ::= asFuncType ( TypeDecls ) [function, klabel(TypeDeclsAsFuncType)]
- | asFuncType ( Map, Map, TypeUse ) [function, klabel(TypeUseAsFuncType) ]
+ syntax FuncType ::= asFuncType ( TypeDecls ) [function, symbol(TypeDeclsAsFuncType)]
+ | asFuncType ( Map, Map, TypeUse ) [function, symbol(TypeUseAsFuncType) ]
// --------------------------------------------------------------------------------------------
rule asFuncType(TDECLS:TypeDecls) => gatherTypes(param, TDECLS) -> gatherTypes(result, TDECLS)
rule asFuncType( _ , _ , TDECLS:TypeDecls) => asFuncType(TDECLS)
@@ -1091,7 +1102,7 @@ Type could be declared explicitly and could optionally bind with an identifier.
When defining `TypeDefn`, the `identifier` for `param` will be ignored and will not be saved into the module instance.
```k
- syntax TypeDefn ::= #type(type: FuncType, metadata: OptionalId) [klabel(aTypeDefn), symbol]
+ syntax TypeDefn ::= #type(type: FuncType, metadata: OptionalId) [symbol(aTypeDefn)]
syntax Alloc ::= alloctype (OptionalId, FuncType)
// ----------------------------------------------------
rule #type(... type: TYPE, metadata: OID) => alloctype(OID, TYPE) ...
@@ -1120,7 +1131,7 @@ The specification can also include export directives.
The importing and exporting parts of specifications are dealt with in the respective sections for import and export.
```k
- syntax FuncDefn ::= #func(type: Int, locals: VecType, body: Instrs, metadata: FuncMetadata) [klabel(aFuncDefn), symbol]
+ syntax FuncDefn ::= #func(type: Int, locals: VecType, body: Instrs, metadata: FuncMetadata) [symbol(aFuncDefn)]
syntax Alloc ::= allocfunc ( Int , Int , FuncType , VecType , Instrs , FuncMetadata )
// ----------------------------------------------------------------------------------------
rule #func(... type: TYPIDX, locals: LOCALS, body: INSTRS, metadata: META) => allocfunc(CUR, NEXTADDR, TYPE, LOCALS, INSTRS, META) ...
@@ -1153,7 +1164,7 @@ The importing and exporting parts of specifications are dealt with in the respec
...
- syntax FuncMetadata ::= #meta(id: OptionalId, localIds: Map) [klabel(funcMeta), symbol]
+ syntax FuncMetadata ::= #meta(id: OptionalId, localIds: Map) [symbol(funcMeta)]
// ---------------------------------------------------------------------------------------
```
@@ -1208,7 +1219,7 @@ The `#take` function will return the parameter stack in the reversed order, then
`call funcidx` and `call_indirect tableidx typeuse` are 2 control instructions that invoke a function in the current frame.
```k
- syntax Instr ::= #call(Int) [klabel(aCall), symbol]
+ syntax Instr ::= #call(Int) [symbol(aCall)]
// ---------------------------------------------------
rule #call(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault 0 ) ...
CUR
@@ -1221,7 +1232,7 @@ The `#take` function will return the parameter stack in the reversed order, then
```
```k
- syntax Instr ::= "#call_indirect" "(" Int "," TypeUse ")" [klabel(aCall_indirect), symbol]
+ syntax Instr ::= "#call_indirect" "(" Int "," TypeUse ")" [symbol(aCall_indirect)]
// ------------------------------------------------------------------------------
```
@@ -1296,7 +1307,7 @@ The specification can also include export directives.
The importing and exporting parts of specifications are dealt with in the respective sections for import and export.
```k
- syntax TableDefn ::= #table (limits: Limits, type: RefValType, metadata: OptionalId) [klabel(aTableDefn), symbol]
+ syntax TableDefn ::= #table (limits: Limits, type: RefValType, metadata: OptionalId) [symbol(aTableDefn)]
syntax Alloc ::= alloctable (OptionalId, Int, OptionalInt, RefValType)
// --------------------------------------------------------------------
rule #table(... limits: #limitsMin(MIN), type: TYP, metadata: OID) => alloctable(OID, MIN, .Int, TYP) ...
@@ -1339,9 +1350,10 @@ The `MemorySpec` production is used to define all ways that a global can specifi
A memory can either be specified by giving its type (limits); by specifying a vector of its initial `data`; or by an import and its expected type.
The specification can also include export directives.
The importing and exporting parts of specifications are dealt with in the respective sections for import and export.
+[Memory Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#memory-instructions)
```k
- syntax MemoryDefn ::= #memory(limits: Limits, metadata: OptionalId) [klabel(aMemoryDefn), symbol]
+ syntax MemoryDefn ::= #memory(limits: Limits, metadata: OptionalId) [symbol(aMemoryDefn)]
syntax Alloc ::= allocmemory (OptionalId, Int, OptionalInt)
// -----------------------------------------------------------
rule #memory(... limits: #limitsMin(MIN), metadata: OID) => allocmemory(OID, MIN, .Int) ...
@@ -1355,7 +1367,7 @@ The importing and exporting parts of specifications are dealt with in the respec
CUR
IDS => #saveId(IDS, ID, 0)
- .MapIntToInt => (wrap(0) Int2Int|-> wrap(NEXTADDR))
+ .Map => (0 |-> NEXTADDR)
...
NEXTADDR => NEXTADDR +Int 1
@@ -1375,9 +1387,10 @@ The importing and exporting parts of specifications are dealt with in the respec
The assorted store operations take an address of type `i32` and a value.
The `storeX` operations first wrap the the value to be stored to the bit wdith `X`.
The value is encoded as bytes and stored at the "effective address", which is the address given on the stack plus offset.
+[Store Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
```k
- syntax Instr ::= #store(ValType, StoreOp, offset : Int) [klabel(aStore), symbol]
+ syntax Instr ::= #store(ValType, StoreOp, offset : Int) [symbol(aStore)]
| IValType "." StoreOp Int Int
// | FValType "." StoreOp Int Float
| "store" "{" IWidth Int Number "}"
@@ -1386,14 +1399,15 @@ The value is encoded as bytes and stored at the "effective address", which is th
rule #store(ITYPE:IValType, SOP, OFFSET) => ITYPE . SOP (IDX +Int OFFSET) VAL ...
< ITYPE > VAL : < i32 > IDX : VALSTACK => VALSTACK
- rule store { WIDTH EA VAL } => store { WIDTH EA VAL (MEMADDRS{{0}} orDefault 0) } ...
+ rule store { WIDTH EA VAL } => store { WIDTH EA VAL ({MEMADDRS[0] orDefault 0}:>Int) } ...
CUR
CUR
MEMADDRS
...
- requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1
+ requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0)
+ [preserves-definedness]
rule store { WIDTH EA VAL ADDR } => .K ...
@@ -1426,9 +1440,10 @@ The assorted load operations take an address of type `i32`.
The `loadX_sx` operations loads `X` bits from memory, and extend it to the right length for the return value, interpreting the bytes as either signed or unsigned according to `sx`.
The value is fetched from the "effective address", which is the address given on the stack plus offset.
Sort `Signedness` is defined in module `BYTES`.
+[Load Instructions](https://webassembly.github.io/spec/core/exec/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg-and-t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
```k
- syntax Instr ::= #load(ValType, LoadOp, offset : Int) [klabel(aLoad), symbol]
+ syntax Instr ::= #load(ValType, LoadOp, offset : Int) [symbol(aLoad)]
| "load" "{" IValType IWidth Int Signedness"}"
| "load" "{" IValType IWidth Int Signedness Int"}"
| "load" "{" IValType IWidth Int Signedness SparseBytes"}"
@@ -1445,14 +1460,15 @@ Sort `Signedness` is defined in module `BYTES`.
rule ITYPE . load16_s EA:Int => load { ITYPE i16 EA Signed } ...
rule i64 . load32_s EA:Int => load { i64 i32 EA Signed } ...
- rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN (MEMADDRS{{0}} orDefault 0)} ...
+ rule load { ITYPE WIDTH EA SIGN } => load { ITYPE WIDTH EA SIGN ({MEMADDRS[0] orDefault 0}:>Int)} ...
CUR
CUR
MEMADDRS
...
- requires 0 in_keys{{MEMADDRS}} andBool size(MEMADDRS) ==Int 1
+ requires 0 in_keys(MEMADDRS) andBool size(MEMADDRS) ==Int 1 andBool isInt(MEMADDRS[0] orDefault 0)
+ [preserves-definedness]
rule load { ITYPE WIDTH EA SIGN ADDR:Int} => load { ITYPE WIDTH EA SIGN DATA } ...
@@ -1472,17 +1488,23 @@ Sort `Signedness` is defined in module `BYTES`.
requires (EA +Int #numBytes(WIDTH)) >Int (SIZE *Int #pageSize())
rule load { ITYPE WIDTH EA Signed DATA:SparseBytes } => #chop(< ITYPE > #signed(WIDTH, #getRange(DATA, EA, #numBytes(WIDTH)))) ...
+ [preserves-definedness]
+ // #signed(WIDTH, N) is defined for 0 <= N <= #pow(WIDTH)
+ // #pow(WIDTH) == 2 ^ #width(WIDTH) == 2 ^ (#numBytes(WIDTH) * 8)
+ // and #getRange(_, _, SIZE) < 2 ^ (SIZE * 8)
+
rule load { ITYPE WIDTH EA Unsigned DATA:SparseBytes } => < ITYPE > #getRange(DATA, EA, #numBytes(WIDTH)) ...
```
The `size` operation returns the size of the memory, measured in pages.
+[Memory Size](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-size)
```k
rule memory.size => < i32 > SIZE ...
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1497,6 +1519,7 @@ Failure to grow is indicated by pushing -1 to the stack.
Success is indicated by pushing the previous memory size to the stack.
`grow` is non-deterministic and may fail either due to trying to exceed explicit max values, or because the embedder does not have resources available.
By setting the `` field in the configuration to `true`, the sematnics ensure memory growth only fails if the memory in question would exceed max bounds.
+[Memory Grow](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-grow)
```k
syntax Instr ::= "grow" Int
@@ -1508,7 +1531,7 @@ By setting the `` field in the configuration to `true
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1524,7 +1547,7 @@ By setting the `` field in the configuration to `true
CUR
CUR
- wrap(0) Int2Int|-> wrap(ADDR)
+ 0 |-> ADDR
...
@@ -1552,15 +1575,108 @@ The maximum of table size is 2^32 bytes.
rule #maxTableSize() => 4294967296
```
+`fill` fills a contiguous section of memory with a value.
+When the section specified goes beyond the bounds of the memory region, that causes a trap.
+If the section has length 0, nothing happens.
+The spec states that this is really a sequence of `i32.store8` instructions, but we use `replaceAt` here.
+[Memory Fill](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-fill)
+
+```k
+ syntax Instr ::= "fillTrap" Int Int Int
+ | "fill" Int Int Int
+ // ---------------------------------------
+ rule memory.fill => fillTrap N VAL D ...
+ < i32 > N : < i32 > VAL : < i32 > D : VALSTACK => VALSTACK
+
+ rule fillTrap N _VAL D => trap ...
+ CUR
+
+ CUR
+ 0 |-> ADDR
+ ...
+
+
+ ADDR
+ SIZE
+ ...
+
+ requires N +Int D >Int SIZE *Int #pageSize()
+
+ rule fillTrap N VAL D => fill N VAL D ... [owise]
+
+ rule fill 0 _VAL _D => .K ...
+
+ rule fill N VAL D => .K ...
+ CUR
+
+ CUR
+ 0 |-> ADDR
+ ...
+
+
+ ADDR
+ DATA => replaceAt(DATA, D, padRightBytes(.Bytes, N, VAL))
+ ...
+
+ requires notBool N ==Int 0
+```
+
+`copy` will copy a section of memory from one location to another.
+The source and destination segments may overlap.
+Similar to `fill`, we perform the entire copy in one internal operation as opposed to
+performing a series of load and store operations as stated in the spec.
+[Memory Copy](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-copy)
+
+```k
+ syntax Instr ::= "copyTrap" Int Int Int
+ | "copy" Int Int Int
+ // ---------------------------------------
+ rule memory.copy => copyTrap N S D ...
+ < i32 > N : < i32 > S : < i32 > D : VALSTACK => VALSTACK
+
+ rule copyTrap N S D => trap ...
+ CUR
+
+ CUR
+ 0 |-> ADDR
+ ...
+
+
+ ADDR
+ SIZE
+ ...
+
+ requires D +Int N >Int SIZE *Int #pageSize()
+ orBool S +Int N >Int SIZE *Int #pageSize()
+
+ rule copyTrap N S D => copy N S D ... [owise]
+
+ rule copy 0 _S _D => .K ...
+
+ rule copy N S D => .K ...
+ CUR
+
+ CUR
+ 0 |-> ADDR
+ ...
+
+
+ ADDR
+ DATA => replaceAt(DATA, D, #getBytesRange(DATA, S, N))
+ ...
+
+ requires notBool N ==Int 0
+```
+
Element Segments
----------------
```k
- syntax ElemDefn ::= #elem(type: RefValType, elemSegment: ListRef, mode: ElemMode, oid: OptionalId) [klabel(aElemDefn), symbol]
+ syntax ElemDefn ::= #elem(type: RefValType, elemSegment: ListRef, mode: ElemMode, oid: OptionalId) [symbol(aElemDefn)]
| #elemAux(segmentLen: Int, mode: ElemMode)
- syntax ElemMode ::= #elemActive(table: Int, offset: Instrs) [klabel(aElemActive), symbol]
- | "#elemPassive" [klabel(aElemPassive), symbol]
- | "#elemDeclarative" [klabel(aElemDeclarative), symbol]
+ syntax ElemMode ::= #elemActive(table: Int, offset: Instrs) [symbol(aElemActive)]
+ | "#elemPassive" [symbol(aElemPassive)]
+ | "#elemDeclarative" [symbol(aElemDeclarative)]
syntax Alloc ::= allocelem(RefValType, ListRef, OptionalId)
// -----------------------------------------------------
@@ -1601,7 +1717,7 @@ Element Segments
CUR
FADDRS
- ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }}
+ ADDRS => ADDRS [ NEXTIDX <- NEXTADDR ]
NEXTIDX => NEXTIDX +Int 1
IDS => #saveId(IDS, OID, 0)
...
@@ -1630,19 +1746,34 @@ Memories can be initialized with data, specified as a list of bytes together wit
The `data` initializer simply puts these bytes into the specified memory, starting at the offset.
```k
- syntax DataDefn ::= #data(index : Int, offset : Instrs, data : Bytes) [klabel(aDataDefn), symbol]
+ syntax DataDefn ::= #data(index : Int, offset : Instrs, data : Bytes) [symbol(aDataDefn)]
| "data" "{" Int Bytes "}"
// --------------------------------------------
// Default to memory 0.
rule #data(IDX, IS, DATA) => sequenceInstrs(IS) ~> data { IDX DATA } ...
+ rule data { MEMIDX DSBYTES } => trap ...
+ < i32 > OFFSET : _STACK
+ CUR
+
+ CUR
+ MEMIDX |-> ADDR
+ ...
+
+
+ ADDR
+ SIZE
+ ...
+
+ requires OFFSET +Int lengthBytes(DSBYTES) >Int SIZE *Int #pageSize()
+
// For now, deal only with memory 0.
rule data { MEMIDX DSBYTES } => .K ...
< i32 > OFFSET : STACK => STACK
CUR
CUR
- wrap(MEMIDX) Int2Int|-> wrap(ADDR)
+ MEMIDX |-> ADDR
...
@@ -1650,6 +1781,7 @@ The `data` initializer simply puts these bytes into the specified memory, starti
DATA => #setRange(DATA, OFFSET, Bytes2Int(DSBYTES, LE, Unsigned), lengthBytes(DSBYTES))
...
+ [owise]
syntax Int ::= Int "up/Int" Int [function]
// ------------------------------------------
@@ -1662,7 +1794,7 @@ Start Function
The `start` component of a module declares the function index of a `start function` that is automatically invoked when the module is instantiated, after `tables` and `memories` have been initialized.
```k
- syntax StartDefn ::= #start(Int) [klabel(aStartDefn), symbol]
+ syntax StartDefn ::= #start(Int) [symbol(aStartDefn)]
// -------------------------------------------------------------
rule #start(IDX) => ( invoke FUNCADDRS {{ IDX }} orDefault -1 ) ...
CUR
@@ -1680,7 +1812,7 @@ Export
Exports make functions, tables, memories and globals available for importing into other modules.
```k
- syntax ExportDefn ::= #export(name : WasmString, index : Int) [klabel(aExportDefn), symbol]
+ syntax ExportDefn ::= #export(name : WasmString, index : Int) [symbol(aExportDefn)]
syntax Alloc ::= ExportDefn
// ---------------------------
rule #export(ENAME, IDX) => .K ...
@@ -1700,12 +1832,12 @@ That an import is really a subtype of the declared import needs to be checked at
The value of a global gets copied when it is imported.
```k
- syntax ImportDefn ::= #import(mod : WasmString, name : WasmString, ImportDesc) [klabel(aImportDefn), symbol]
- | #importHelper(ImportDesc, importedAddr:Int) [klabel(aImportDefnHelper), symbol]
- syntax ImportDesc ::= #funcDesc (id: OptionalId, type: Int) [klabel(aFuncDesc), symbol]
- | #globalDesc (id: OptionalId, type: GlobalType) [klabel(aGlobalDesc), symbol]
- | #tableDesc (id: OptionalId, type: Limits) [klabel(aTableDesc), symbol]
- | #memoryDesc (id: OptionalId, type: Limits) [klabel(aMemoryDesc), symbol]
+ syntax ImportDefn ::= #import(mod : WasmString, name : WasmString, ImportDesc) [symbol(aImportDefn)]
+ | #importHelper(ImportDesc, importedAddr:Int) [symbol(aImportDefnHelper)]
+ syntax ImportDesc ::= #funcDesc (id: OptionalId, type: Int) [symbol(aFuncDesc)]
+ | #globalDesc (id: OptionalId, type: GlobalType) [symbol(aGlobalDesc)]
+ | #tableDesc (id: OptionalId, type: Limits) [symbol(aTableDesc)]
+ | #memoryDesc (id: OptionalId, type: Limits) [symbol(aMemoryDesc)]
syntax Alloc ::= ImportDefn
// --------------------------------
rule #import(MOD, NAME, #funcDesc(...) #as FD ) => #importHelper(FD, FS2 {{ IDX }} orDefault -1) ...
@@ -1739,7 +1871,8 @@ The value of a global gets copied when it is imported.
CUR
IDS => #saveId(IDS, OID, 0)
- .Map => 0 |-> ADDR
+ TABADDRS => TABADDRS[NEXT <- ADDR]
+ NEXT => NEXT +Int 1
...
... MOD |-> MODIDX ...
@@ -1763,14 +1896,14 @@ The value of a global gets copied when it is imported.
CUR
IDS => #saveId(IDS, OID, 0)
- .MapIntToInt => wrap(0) Int2Int|-> wrap(ADDR)
+ .Map => 0 |-> ADDR
...
... MOD |-> MODIDX ...
MODIDX
IDS'
- ... wrap(#ContextLookup(IDS' , TFIDX)) Int2Int|-> wrap(ADDR) ...
+ ... #ContextLookup(IDS' , TFIDX) |-> ADDR ...
... NAME |-> TFIDX ...
...
@@ -1837,15 +1970,15 @@ A subtle point is related to tables with inline `elem` definitions: since these
The groups are chosen to represent different stages of allocation and instantiation.
```k
- syntax ModuleDecl ::= #module ( types: Defns, funcs: Defns, tables: Defns, mems: Defns, globals: Defns, elem: Defns, data: Defns, start: Defns, importDefns: Defns, exports: Defns, metadata: ModuleMetadata) [klabel(aModuleDecl), symbol]
+ syntax ModuleDecl ::= #module ( types: Defns, funcs: Defns, tables: Defns, mems: Defns, globals: Defns, elem: Defns, data: Defns, start: Defns, importDefns: Defns, exports: Defns, metadata: ModuleMetadata) [symbol(aModuleDecl)]
// -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
syntax ModuleDecl ::= #emptyModule(OptionalId) [function, total]
// ---------------------------------------------------------------------
rule #emptyModule(OID) => #module (... types: .Defns, funcs: .Defns, tables: .Defns, mems: .Defns, globals: .Defns, elem: .Defns, data: .Defns, start: .Defns, importDefns: .Defns, exports: .Defns, metadata: #meta(... id: OID, funcIds: .Map, filename: .String))
- syntax ModuleMetadata ::= #meta(id: OptionalId, funcIds: Map, filename : OptionalString) [klabel(moduleMeta), symbol]
- syntax OptionalString ::= ".String" [klabel(.String), symbol] | String
+ syntax ModuleMetadata ::= #meta(id: OptionalId, funcIds: Map, filename : OptionalString) [symbol(moduleMeta)]
+ syntax OptionalString ::= ".String" [symbol(.String)] | String
// ----------------------------------------------------------------------
```
diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py
index 50c82dc86..83580d748 100644
--- a/pykwasm/src/pykwasm/kwasm_ast.py
+++ b/pykwasm/src/pykwasm/kwasm_ast.py
@@ -580,6 +580,8 @@ def I64_LOAD32_S(offset: int) -> KInner:
MEMORY_GROW = KApply('aGrow', [])
MEMORY_SIZE = KApply('aSize', [])
+MEMORY_FILL = KApply('aFill', [])
+MEMORY_COPY = KApply('aCopy', [])
#######################
# Global Instructions #
diff --git a/pykwasm/src/pykwasm/scripts/kwasm.py b/pykwasm/src/pykwasm/scripts/kwasm.py
index 03e517b81..05fd03ccd 100644
--- a/pykwasm/src/pykwasm/scripts/kwasm.py
+++ b/pykwasm/src/pykwasm/scripts/kwasm.py
@@ -10,9 +10,10 @@
from pyk.cli.utils import dir_path, file_path
from pyk.kdist import kdist
-from pyk.ktool.kprint import KAstOutput, _kast
+from pyk.ktool.kprint import KAstInput, KAstOutput, _kast
from pyk.ktool.kprove import _kprove
from pyk.ktool.krun import _krun
+from pyk.utils import run_process
from .preprocessor import preprocess
@@ -51,9 +52,25 @@ def _exec_run(program: Path) -> None:
def _exec_kast(program: Path, output: KAstOutput | None) -> None:
definition_dir = kdist.get('wasm-semantics.llvm')
+ pgm_parser = definition_dir / 'parser_PGM'
- with _preprocessed(program) as input_file:
- proc_res = _kast(input_file, definition_dir=definition_dir, output=output, check=False)
+ with _preprocessed(program) as preprocessed_file:
+ input = KAstInput.PROGRAM
+ input_file = preprocessed_file
+
+ if pgm_parser.exists():
+ f = NamedTemporaryFile()
+ proc_res = run_process([str(pgm_parser), str(input_file)], check=False)
+ if proc_res.returncode != 0:
+ _exit_with_output(proc_res)
+ tmp_file = Path(f.name)
+ tmp_file.write_text(proc_res.stdout)
+
+ input = KAstInput.KORE
+ input_file = tmp_file
+
+ if (not pgm_parser.exists()) or output != KAstOutput.KORE:
+ proc_res = _kast(input_file, definition_dir=definition_dir, input=input, output=output, check=False)
_exit_with_output(proc_res)
diff --git a/tests/conformance/look_for_supported.sh b/tests/conformance/look_for_supported.sh
old mode 100644
new mode 100755
diff --git a/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt
index 64de12c20..740795561 100644
--- a/tests/conformance/unparseable.txt
+++ b/tests/conformance/unparseable.txt
@@ -5,20 +5,13 @@ comments.wast
conversions.wast
data.wast
endianness.wast
-f32_cmp.wast
-f32.wast
-f64_cmp.wast
-f64.wast
float_exprs.wast
float_literals.wast
global.wast
if.wast
imports.wast
loop.wast
-memory_copy.wast
-memory_fill.wast
-memory_init.wast
memory.wast
+memory_init.wast
select.wast
-skip-stack-guard-page.wast
-table_copy.wast
+tokens.wast
diff --git a/tests/conformance/unsupported-llvm.txt b/tests/conformance/unsupported-llvm.txt
index d154172d0..da5157a28 100644
--- a/tests/conformance/unsupported-llvm.txt
+++ b/tests/conformance/unsupported-llvm.txt
@@ -2,14 +2,15 @@ address.wast
align.wast
call_indirect.wast
const.wast
+f32.wast
f32_bitwise.wast
+f64.wast
f64_bitwise.wast
fac.wast
float_memory.wast
float_misc.wast
func.wast
left-to-right.wast
-linking.wast
memory_redundancy.wast
memory_trap.wast
traps.wast
diff --git a/tests/proofs/memory-spec.k b/tests/proofs/memory-spec.k
index 6ec2442a1..04ef37314 100644
--- a/tests/proofs/memory-spec.k
+++ b/tests/proofs/memory-spec.k
@@ -7,7 +7,7 @@ module MEMORY-SPEC
CUR
CUR
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
...
@@ -24,7 +24,7 @@ module MEMORY-SPEC
CUR
CUR
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
...
diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k
index 0f2a1734f..4a71fdbf7 100644
--- a/tests/proofs/wrc20-spec.k
+++ b/tests/proofs/wrc20-spec.k
@@ -20,7 +20,7 @@ module WRC20-SPEC
CUR
#wrc20ReverseBytesTypeIdx |-> #wrc20ReverseBytesType
- wrap(0) Int2Int|-> wrap(MEMADDR)
+ 0 |-> MEMADDR
_ => ?_
NEXTFUNCIDX => NEXTFUNCIDX +Int 1
...
diff --git a/tests/wasm-tests b/tests/wasm-tests
index 7fa2f20a6..6798f054a 160000
--- a/tests/wasm-tests
+++ b/tests/wasm-tests
@@ -1 +1 @@
-Subproject commit 7fa2f20a6df4cf1c114582c8cb60f5bfcdbf1be1
+Subproject commit 6798f054ad1b0493919f0b5244fa46682ccd3e69