diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml deleted file mode 100644 index bf287acdb..000000000 --- a/.github/workflows/master-push.yml +++ /dev/null @@ -1,80 +0,0 @@ -name: 'Master Push' -on: - push: - branches: - - master - -jobs: - - release: - name: 'Publish Release' - runs-on: ubuntu-latest - environment: production - steps: - - name: 'Check out code' - uses: actions/checkout@v3 - with: - ref: ${{ github.event.push.head.sha }} - fetch-depth: 0 - - name: 'Make release' - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - run: | - set -x - VERSION=v$(cat package/version) - gh release create ${VERSION} --target ${{ github.sha }} - - name: 'Update dependents' - run: | - set -x - version="$(cat package/version)" - curl --fail \ - -X POST \ - -H "Accept: application/vnd.github+json" \ - -H "Authorization: Bearer ${{ secrets.JENKINS_GITHUB_PAT }}" \ - -H "X-GitHub-Api-Version: 2022-11-28" \ - https://api.github.com/repos/runtimeverification/devops/dispatches \ - -d '{"event_type":"on-demand-test","client_payload":{"repo":"runtimeverification/wasm-semantics","version":"'${version}'"}}' - - nix-cache: - name: 'Populate Nix Cache' - strategy: - matrix: - include: - - runner: normal - - runner: macos-13 - - runner: ARM64 - runs-on: ${{ matrix.runner }} - steps: - - name: 'Check out code' - uses: actions/checkout@v3 - with: - ref: ${{ github.event.push.head.sha }} - fetch-depth: 0 - - 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: - GC_DONT_GC: 1 - CACHIX_AUTH_TOKEN: '${{ secrets.CACHIX_PUBLIC_TOKEN }}' - with: - packages: jq - script: | - kwasm=$(nix build --extra-experimental-features 'nix-command flakes' .#kwasm --json | jq -r '.[].outputs | to_entries[].value') - drv=$(nix-store --query --deriver ${kwasm}) - nix-store --query --requisites --include-outputs ${drv} | cachix push k-framework diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index df937cb82..481abe6d2 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -8,41 +8,14 @@ concurrency: jobs: - version-bump: - name: 'Version Bump' - runs-on: [self-hosted, linux, flyweight-ephemeral] - steps: - - name: 'Check out code' - uses: actions/checkout@v3 - with: - token: ${{ secrets.JENKINS_GITHUB_PAT }} - # fetch-depth 0 means deep clone the repo - fetch-depth: 0 - ref: ${{ github.event.pull_request.head.sha }} - - name: 'Configure GitHub user' - run: | - git config user.name devops - git config user.email devops@runtimeverification.com - - name: 'Update version' - run: | - og_version=$(git show origin/${GITHUB_BASE_REF}:package/version) - ./package/version.sh bump ${og_version} - ./package/version.sh sub - new_version=$(cat package/version) - git add --update && git commit --message "Set Version: ${new_version}" || true - - name: 'Push updates' - run: git push origin HEAD:${GITHUB_HEAD_REF} - pykwasm-code-quality-checks: name: 'Code Quality Checks' runs-on: ubuntu-latest steps: - name: 'Check out code' - uses: actions/checkout@v3 - with: - submodules: recursive + uses: actions/checkout@v4 - name: 'Install Poetry' - uses: Gr1N/setup-poetry@v8 + uses: Gr1N/setup-poetry@v9 - name: 'Build pykwasm' run: poetry -C pykwasm install - name: 'Run code quality checks' @@ -82,68 +55,3 @@ jobs: if: always() run: | docker stop --time=0 kwasm-ci-conformance-${GITHUB_SHA} - - prove-tests: - name: 'Prover Tests' - needs: pykwasm-code-quality-checks - runs-on: [self-hosted, linux, normal] - timeout-minutes: 30 - steps: - - name: 'Check out code' - uses: actions/checkout@v3 - with: - submodules: recursive - - name: 'Set up Docker' - uses: ./.github/actions/with-docker - with: - container-name: kwasm-ci-prove-${{ github.sha }} - - name: 'Build pykwasm' - run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm install - - name: 'Build Haskell definitions' - run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.{kwasm-lemmas,wrc20} -j2 - - name: 'Run prover tests' - run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j6 test-prove - - name: 'Tear down Docker' - if: always() - run: | - docker stop --time=0 kwasm-ci-prove-${GITHUB_SHA} - - nix: - name: 'Nix' - strategy: - fail-fast: false - matrix: - include: - - runner: normal - - runner: macos-13 - - runner: ARM64 - needs: pykwasm-code-quality-checks - runs-on: ${{ matrix.runner }} - timeout-minutes: 60 - steps: - - name: 'Check out code' - uses: actions/checkout@v3 - 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' - run: GC_DONT_GC=1 nix build .#kwasm-pyk --extra-experimental-features 'nix-command flakes' --print-build-logs - - name: 'Test KWASM' - run: GC_DONT_GC=1 nix build .#kwasm-test --extra-experimental-features 'nix-command flakes' --print-build-logs diff --git a/.github/workflows/update-version.yml b/.github/workflows/update-version.yml index 70904a063..b1daeeec1 100644 --- a/.github/workflows/update-version.yml +++ b/.github/workflows/update-version.yml @@ -15,7 +15,7 @@ jobs: runs-on: ubuntu-22.04 steps: - name: 'Check out code' - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: submodules: recursive token: ${{ secrets.JENKINS_GITHUB_PAT }} @@ -24,31 +24,11 @@ jobs: git config user.email devops@runtimeverification.com - name: 'Install Poetry' uses: Gr1N/setup-poetry@v8 - - name: 'Install Nix' - uses: cachix/install-nix-action@v22 - with: - install_url: https://releases.nixos.org/nix/nix-2.13.3/install - extra_nix_config: | - access-tokens = github.com=${{ secrets.GITHUB_TOKEN }} - substituters = http://cache.nixos.org https://hydra.iohk.io - trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= - - name: 'Install Cachix' - uses: cachix/cachix-action@v14 - with: - name: k-framework - 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' run: git push diff --git a/deps/k_release b/deps/k_release index c291189b4..466cdc88f 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.0.130 +7.1.44 diff --git a/flake.lock b/flake.lock index ee8f8d0f1..36576eb9e 100644 --- a/flake.lock +++ b/flake.lock @@ -82,17 +82,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1717504162, - "narHash": "sha256-muZL1MfImaMimk+f/SwPj4xrlRvDnSpovDhAx/WqdCw=", + "lastModified": 1719881076, + "narHash": "sha256-t9RTbVarwaobMiJkQjXykP8Qt+26miKzr3inONULvck=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "abceb59fcbc47d1bc537ff797f806c8bb8649626", + "rev": "11265424aeb138168bc73f1f028273de192b5be4", "type": "github" }, "original": { "owner": "runtimeverification", + "ref": "v0.1.29", "repo": "haskell-backend", - "rev": "abceb59fcbc47d1bc537ff797f806c8bb8649626", "type": "github" } }, @@ -126,16 +126,16 @@ "rv-utils": "rv-utils_3" }, "locked": { - "lastModified": 1718204565, - "narHash": "sha256-kOeQjucGWCHj0isvj6BKbYjSavIj7WxT5pTidb9Nsn0=", + "lastModified": 1720086145, + "narHash": "sha256-tCHf9gbsFHZH9PM0r65CgmqHQsNfGJCuD7kib7KLELs=", "owner": "runtimeverification", "repo": "k", - "rev": "7e036e3f2ec92655c9a4077baac835235f899057", + "rev": "e6d4f896d7c51efd68f11c77141d457625472c43", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.0.130", + "ref": "v7.1.44", "repo": "k", "type": "github" } @@ -160,16 +160,16 @@ ] }, "locked": { - "lastModified": 1718022605, - "narHash": "sha256-2eDL/m8nROZid2tczwlzYPsJOj3gA2k60VVL8YuFJBc=", + "lastModified": 1719488252, + "narHash": "sha256-f6ppPl1kYpFX8MY3Jji6ky6BDpY6QrvQJ4wy0PCjqp4=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "2a33228656e168965e89d40ec77a758ccd8f1c29", + "rev": "9dfc379039bfa3a257d92feac6323eb246a8e995", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.49", + "ref": "v0.1.52", "repo": "llvm-backend", "type": "github" } @@ -320,17 +320,17 @@ }, "locked": { "dir": "pyk", - "lastModified": 1718204565, - "narHash": "sha256-kOeQjucGWCHj0isvj6BKbYjSavIj7WxT5pTidb9Nsn0=", + "lastModified": 1720086145, + "narHash": "sha256-tCHf9gbsFHZH9PM0r65CgmqHQsNfGJCuD7kib7KLELs=", "owner": "runtimeverification", "repo": "k", - "rev": "7e036e3f2ec92655c9a4077baac835235f899057", + "rev": "e6d4f896d7c51efd68f11c77141d457625472c43", "type": "github" }, "original": { "dir": "pyk", "owner": "runtimeverification", - "ref": "v7.0.130", + "ref": "v7.1.44", "repo": "k", "type": "github" } @@ -363,10 +363,6 @@ "k-framework", "nixpkgs" ], - "nixpkgs-pyk": [ - "pyk", - "nixpkgs" - ], "poetry2nix": [ "pyk", "poetry2nix" diff --git a/flake.nix b/flake.nix index 16b3f5527..17fdb6ff2 100644 --- a/flake.nix +++ b/flake.nix @@ -2,17 +2,16 @@ description = "K Semantics of WebAssembly"; inputs = { - k-framework.url = "github:runtimeverification/k/v7.0.130"; + k-framework.url = "github:runtimeverification/k/v7.1.44"; 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.130?dir=pyk"; - nixpkgs-pyk.follows = "pyk/nixpkgs"; + pyk.url = "github:runtimeverification/k/v7.1.44?dir=pyk"; poetry2nix.follows = "pyk/poetry2nix"; }; outputs = - { self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, ... }@inputs: + { self, k-framework, nixpkgs, flake-utils, rv-utils, pyk, poetry2nix }: let overlay = (final: prev: let @@ -23,26 +22,15 @@ ] ./.); 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; [ + buildInputs = with prev; [ k-framework.packages.${system}.k final.kwasm-pyk - python310-pyk + python310 ]; nativeBuildInputs = [ prev.makeWrapper ]; @@ -69,30 +57,33 @@ ''; }; - kwasm-pyk = poetry2nix.mkPoetryApplication { - python = nixpkgs-pyk.python310; + kwasm-pyk = prev.poetry2nix.mkPoetryApplication { + 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 ]; - }); - py-wasm = prevPython.py-wasm.overridePythonAttrs - ( - old: { - buildInputs = (old.buildInputs or [ ]) ++ [ prevPython.setuptools ]; - } - ); + + overrides = prev.poetry2nix.overrides.withDefaults + (finalPython: prevPython: { + pyk = prev.pyk-python310; + + pygments = prevPython.pygments.overridePythonAttrs + (old: { + buildInputs = (old.buildInputs or [ ]) + ++ [ prevPython.hatchling ]; + }); + + xdg-base-dirs = prevPython.xdg-base-dirs.overridePythonAttrs + (old: { + propagatedBuildInputs = (old.propagatedBuildInputs or [ ]) + ++ [ finalPython.poetry ]; + }); + + py-wasm = prevPython.py-wasm.overridePythonAttrs + (old: { + buildInputs = (old.buildInputs or [ ]) + ++ [ prevPython.setuptools ]; + }); }); - groups = [ ]; + checkGroups = [ ]; }; @@ -109,11 +100,11 @@ 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,7 +129,11 @@ let pkgs = import nixpkgs { inherit system; - overlays = [ overlay ]; + overlays = [ + poetry2nix.overlays.default + pyk.overlay + overlay + ]; }; in { packages = rec { 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 abf5cfcdc..1f7a170d7 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.63 +0.1.77 diff --git a/pykwasm/poetry.lock b/pykwasm/poetry.lock index 77e511365..81b5f9e37 100644 --- a/pykwasm/poetry.lock +++ b/pykwasm/poetry.lock @@ -157,63 +157,63 @@ cron = ["capturer (>=2.4)"] [[package]] name = "coverage" -version = "7.5.3" +version = "7.5.4" description = "Code coverage measurement for Python" optional = false python-versions = ">=3.8" 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.5.4-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6cfb5a4f556bb51aba274588200a46e4dd6b505fb1a5f8c5ae408222eb416f99"}, + {file = "coverage-7.5.4-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:2174e7c23e0a454ffe12267a10732c273243b4f2d50d07544a91198f05c48f47"}, + {file = "coverage-7.5.4-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2214ee920787d85db1b6a0bd9da5f8503ccc8fcd5814d90796c2f2493a2f4d2e"}, + {file = "coverage-7.5.4-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1137f46adb28e3813dec8c01fefadcb8c614f33576f672962e323b5128d9a68d"}, + {file = "coverage-7.5.4-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b385d49609f8e9efc885790a5a0e89f2e3ae042cdf12958b6034cc442de428d3"}, + {file = "coverage-7.5.4-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:b4a474f799456e0eb46d78ab07303286a84a3140e9700b9e154cfebc8f527016"}, + {file = "coverage-7.5.4-cp310-cp310-musllinux_1_2_i686.whl", hash = "sha256:5cd64adedf3be66f8ccee418473c2916492d53cbafbfcff851cbec5a8454b136"}, + {file = "coverage-7.5.4-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:e564c2cf45d2f44a9da56f4e3a26b2236504a496eb4cb0ca7221cd4cc7a9aca9"}, + {file = "coverage-7.5.4-cp310-cp310-win32.whl", hash = "sha256:7076b4b3a5f6d2b5d7f1185fde25b1e54eb66e647a1dfef0e2c2bfaf9b4c88c8"}, + {file = "coverage-7.5.4-cp310-cp310-win_amd64.whl", hash = "sha256:018a12985185038a5b2bcafab04ab833a9a0f2c59995b3cec07e10074c78635f"}, + {file = "coverage-7.5.4-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:db14f552ac38f10758ad14dd7b983dbab424e731588d300c7db25b6f89e335b5"}, + {file = "coverage-7.5.4-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:3257fdd8e574805f27bb5342b77bc65578e98cbc004a92232106344053f319ba"}, + {file = "coverage-7.5.4-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3a6612c99081d8d6134005b1354191e103ec9705d7ba2754e848211ac8cacc6b"}, + {file = "coverage-7.5.4-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:d45d3cbd94159c468b9b8c5a556e3f6b81a8d1af2a92b77320e887c3e7a5d080"}, + {file = "coverage-7.5.4-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ed550e7442f278af76d9d65af48069f1fb84c9f745ae249c1a183c1e9d1b025c"}, + {file = "coverage-7.5.4-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:7a892be37ca35eb5019ec85402c3371b0f7cda5ab5056023a7f13da0961e60da"}, + {file = "coverage-7.5.4-cp311-cp311-musllinux_1_2_i686.whl", hash = "sha256:8192794d120167e2a64721d88dbd688584675e86e15d0569599257566dec9bf0"}, + {file = "coverage-7.5.4-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:820bc841faa502e727a48311948e0461132a9c8baa42f6b2b84a29ced24cc078"}, + {file = "coverage-7.5.4-cp311-cp311-win32.whl", hash = "sha256:6aae5cce399a0f065da65c7bb1e8abd5c7a3043da9dceb429ebe1b289bc07806"}, + {file = "coverage-7.5.4-cp311-cp311-win_amd64.whl", hash = "sha256:d2e344d6adc8ef81c5a233d3a57b3c7d5181f40e79e05e1c143da143ccb6377d"}, + {file = "coverage-7.5.4-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:54317c2b806354cbb2dc7ac27e2b93f97096912cc16b18289c5d4e44fc663233"}, + {file = "coverage-7.5.4-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:042183de01f8b6d531e10c197f7f0315a61e8d805ab29c5f7b51a01d62782747"}, + {file = "coverage-7.5.4-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a6bb74ed465d5fb204b2ec41d79bcd28afccf817de721e8a807d5141c3426638"}, + {file = "coverage-7.5.4-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:b3d45ff86efb129c599a3b287ae2e44c1e281ae0f9a9bad0edc202179bcc3a2e"}, + {file = "coverage-7.5.4-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5013ed890dc917cef2c9f765c4c6a8ae9df983cd60dbb635df8ed9f4ebc9f555"}, + {file = "coverage-7.5.4-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:1014fbf665fef86cdfd6cb5b7371496ce35e4d2a00cda501cf9f5b9e6fced69f"}, + {file = "coverage-7.5.4-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:3684bc2ff328f935981847082ba4fdc950d58906a40eafa93510d1b54c08a66c"}, + {file = "coverage-7.5.4-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:581ea96f92bf71a5ec0974001f900db495488434a6928a2ca7f01eee20c23805"}, + {file = "coverage-7.5.4-cp312-cp312-win32.whl", hash = "sha256:73ca8fbc5bc622e54627314c1a6f1dfdd8db69788f3443e752c215f29fa87a0b"}, + {file = "coverage-7.5.4-cp312-cp312-win_amd64.whl", hash = "sha256:cef4649ec906ea7ea5e9e796e68b987f83fa9a718514fe147f538cfeda76d7a7"}, + {file = "coverage-7.5.4-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:cdd31315fc20868c194130de9ee6bfd99755cc9565edff98ecc12585b90be882"}, + {file = "coverage-7.5.4-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:02ff6e898197cc1e9fa375581382b72498eb2e6d5fc0b53f03e496cfee3fac6d"}, + {file = "coverage-7.5.4-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d05c16cf4b4c2fc880cb12ba4c9b526e9e5d5bb1d81313d4d732a5b9fe2b9d53"}, + {file = "coverage-7.5.4-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:c5986ee7ea0795a4095ac4d113cbb3448601efca7f158ec7f7087a6c705304e4"}, + {file = "coverage-7.5.4-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5df54843b88901fdc2f598ac06737f03d71168fd1175728054c8f5a2739ac3e4"}, + {file = "coverage-7.5.4-cp38-cp38-musllinux_1_2_aarch64.whl", hash = "sha256:ab73b35e8d109bffbda9a3e91c64e29fe26e03e49addf5b43d85fc426dde11f9"}, + {file = "coverage-7.5.4-cp38-cp38-musllinux_1_2_i686.whl", hash = "sha256:aea072a941b033813f5e4814541fc265a5c12ed9720daef11ca516aeacd3bd7f"}, + {file = "coverage-7.5.4-cp38-cp38-musllinux_1_2_x86_64.whl", hash = "sha256:16852febd96acd953b0d55fc842ce2dac1710f26729b31c80b940b9afcd9896f"}, + {file = "coverage-7.5.4-cp38-cp38-win32.whl", hash = "sha256:8f894208794b164e6bd4bba61fc98bf6b06be4d390cf2daacfa6eca0a6d2bb4f"}, + {file = "coverage-7.5.4-cp38-cp38-win_amd64.whl", hash = "sha256:e2afe743289273209c992075a5a4913e8d007d569a406ffed0bd080ea02b0633"}, + {file = "coverage-7.5.4-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:b95c3a8cb0463ba9f77383d0fa8c9194cf91f64445a63fc26fb2327e1e1eb088"}, + {file = "coverage-7.5.4-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:3d7564cc09dd91b5a6001754a5b3c6ecc4aba6323baf33a12bd751036c998be4"}, + {file = "coverage-7.5.4-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:44da56a2589b684813f86d07597fdf8a9c6ce77f58976727329272f5a01f99f7"}, + {file = "coverage-7.5.4-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:e16f3d6b491c48c5ae726308e6ab1e18ee830b4cdd6913f2d7f77354b33f91c8"}, + {file = "coverage-7.5.4-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:dbc5958cb471e5a5af41b0ddaea96a37e74ed289535e8deca404811f6cb0bc3d"}, + {file = "coverage-7.5.4-cp39-cp39-musllinux_1_2_aarch64.whl", hash = "sha256:a04e990a2a41740b02d6182b498ee9796cf60eefe40cf859b016650147908029"}, + {file = "coverage-7.5.4-cp39-cp39-musllinux_1_2_i686.whl", hash = "sha256:ddbd2f9713a79e8e7242d7c51f1929611e991d855f414ca9996c20e44a895f7c"}, + {file = "coverage-7.5.4-cp39-cp39-musllinux_1_2_x86_64.whl", hash = "sha256:b1ccf5e728ccf83acd313c89f07c22d70d6c375a9c6f339233dcf792094bcbf7"}, + {file = "coverage-7.5.4-cp39-cp39-win32.whl", hash = "sha256:56b4eafa21c6c175b3ede004ca12c653a88b6f922494b023aeb1e836df953ace"}, + {file = "coverage-7.5.4-cp39-cp39-win_amd64.whl", hash = "sha256:65e528e2e921ba8fd67d9055e6b9f9e34b21ebd6768ae1c1723f4ea6ace1234d"}, + {file = "coverage-7.5.4-pp38.pp39.pp310-none-any.whl", hash = "sha256:79b356f3dd5b26f3ad23b35c75dbdaf1f9e2450b6bcefc6d0825ea0aa3f86ca5"}, + {file = "coverage-7.5.4.tar.gz", hash = "sha256:a44963520b069e12789d0faea4e9fdb1e410cdc4aab89d94f7f55cbb7fef0353"}, ] [package.dependencies] @@ -371,34 +371,34 @@ testing = ["hatch", "pre-commit", "pytest", "tox"] [[package]] name = "filelock" -version = "3.15.1" +version = "3.15.4" description = "A platform independent file lock." optional = false python-versions = ">=3.8" files = [ - {file = "filelock-3.15.1-py3-none-any.whl", hash = "sha256:71b3102950e91dfc1bb4209b64be4dc8854f40e5f534428d8684f953ac847fac"}, - {file = "filelock-3.15.1.tar.gz", hash = "sha256:58a2549afdf9e02e10720eaa4d4470f56386d7a6f72edd7d0596337af8ed7ad8"}, + {file = "filelock-3.15.4-py3-none-any.whl", hash = "sha256:6ca1fffae96225dab4c6eaf1c4f4f28cd2568d3ec2a44e15a08520504de468e7"}, + {file = "filelock-3.15.4.tar.gz", hash = "sha256:2207938cbc1844345cb01a5a95524dae30f0ce089eba5b00378295a17e3e90cb"}, ] [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-asyncio (>=0.21)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)", "pytest-timeout (>=2.2)"] +testing = ["covdefaults (>=2.3)", "coverage (>=7.3.2)", "diff-cover (>=8.0.1)", "pytest (>=7.4.3)", "pytest-asyncio (>=0.21)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)", "pytest-timeout (>=2.2)", "virtualenv (>=20.26.2)"] typing = ["typing-extensions (>=4.8)"] [[package]] name = "flake8" -version = "7.0.0" +version = "7.1.0" 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.0-py2.py3-none-any.whl", hash = "sha256:2e416edcc62471a64cea09353f4e7bdba32aeb079b6e360554c659a122b1bc6a"}, + {file = "flake8-7.1.0.tar.gz", hash = "sha256:48a07b626b55236e0fb4784ee69a465fbf59d79eec1f5b4785c3d3bc57d17aa5"}, ] [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]] @@ -421,17 +421,17 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest", [[package]] name = "flake8-comprehensions" -version = "3.14.0" +version = "3.15.0" description = "A flake8 plugin to help you write better list/set/dict comprehensions." optional = false python-versions = ">=3.8" 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.15.0-py3-none-any.whl", hash = "sha256:b7e027bbb52be2ceb779ee12484cdeef52b0ad3c1fcb8846292bdb86d3034681"}, + {file = "flake8_comprehensions-3.15.0.tar.gz", hash = "sha256:923c22603e0310376a6b55b03efebdc09753c69f2d977755cba8bb73458a5d4d"}, ] [package.dependencies] -flake8 = ">=3.0,<3.2.0 || >3.2.0" +flake8 = ">=3,<3.2 || >3.2" [[package]] name = "flake8-quotes" @@ -492,24 +492,57 @@ files = [ [package.dependencies] pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_version >= \"3.8\""} +[[package]] +name = "hypothesis" +version = "6.104.2" +description = "A library for property-based testing" +optional = false +python-versions = ">=3.8" +files = [ + {file = "hypothesis-6.104.2-py3-none-any.whl", hash = "sha256:8b52b7e2462e552c75b819495d5cb6251a2b840accc79cf2ce52588004c915d9"}, + {file = "hypothesis-6.104.2.tar.gz", hash = "sha256:6f2a1489bc8fe1c87ffd202707319b66ec46b2bc11faf6e0161e957b8b9b1eab"}, +] + +[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 = ["backports.zoneinfo (>=0.2.1)", "black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.55)", "django (>=3.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.4)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.17.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.1)"] +cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"] +codemods = ["libcst (>=0.3.16)"] +crosshair = ["crosshair-tool (>=0.0.55)", "hypothesis-crosshair (>=0.0.4)"] +dateutil = ["python-dateutil (>=1.4)"] +django = ["django (>=3.2)"] +dpcontracts = ["dpcontracts (>=0.4)"] +ghostwriter = ["black (>=19.10b0)"] +lark = ["lark (>=0.10.1)"] +numpy = ["numpy (>=1.17.3)"] +pandas = ["pandas (>=1.1)"] +pytest = ["pytest (>=4.6)"] +pytz = ["pytz (>=2014.1)"] +redis = ["redis (>=3.0.0)"] +zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"] + [[package]] name = "importlib-metadata" -version = "7.1.0" +version = "8.0.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.0.0-py3-none-any.whl", hash = "sha256:15584cf2b1bf449d98ff8a6ff1abef57bf20f3ac6454f431736cd3e660921b2f"}, + {file = "importlib_metadata-8.0.0.tar.gz", hash = "sha256:188bd24e4c346d3f0a933f275c2fec67050326a856b9a359881d7c2a697e8812"}, ] [package.dependencies] zipp = ">=0.5" [package.extras] -docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"] +doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"] 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-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-mypy", "pytest-perf (>=0.9.2)", "pytest-ruff (>=0.2.1)"] [[package]] name = "iniconfig" @@ -536,6 +569,30 @@ files = [ [package.extras] colors = ["colorama (>=0.4.6)"] +[[package]] +name = "kframework" +version = "7.1.44" +description = "" +optional = false +python-versions = "<4.0,>=3.10" +files = [ + {file = "kframework-7.1.44-py3-none-any.whl", hash = "sha256:4ded11b61e1b79c23bd75d8e2a2895a49c5a0188692b11a394f1975ce0ee7d06"}, + {file = "kframework-7.1.44.tar.gz", hash = "sha256:5f932b796a8b8421744b42968daddf4fd815e2b278a9873717377202536094ac"}, +] + +[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" +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" @@ -625,38 +682,38 @@ files = [ [[package]] name = "mypy" -version = "1.10.0" +version = "1.10.1" 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.10.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:e36f229acfe250dc660790840916eb49726c928e8ce10fbdf90715090fe4ae02"}, + {file = "mypy-1.10.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:51a46974340baaa4145363b9e051812a2446cf583dfaeba124af966fa44593f7"}, + {file = "mypy-1.10.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:901c89c2d67bba57aaaca91ccdb659aa3a312de67f23b9dfb059727cce2e2e0a"}, + {file = "mypy-1.10.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:0cd62192a4a32b77ceb31272d9e74d23cd88c8060c34d1d3622db3267679a5d9"}, + {file = "mypy-1.10.1-cp310-cp310-win_amd64.whl", hash = "sha256:a2cbc68cb9e943ac0814c13e2452d2046c2f2b23ff0278e26599224cf164e78d"}, + {file = "mypy-1.10.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:bd6f629b67bb43dc0d9211ee98b96d8dabc97b1ad38b9b25f5e4c4d7569a0c6a"}, + {file = "mypy-1.10.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:a1bbb3a6f5ff319d2b9d40b4080d46cd639abe3516d5a62c070cf0114a457d84"}, + {file = "mypy-1.10.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b8edd4e9bbbc9d7b79502eb9592cab808585516ae1bcc1446eb9122656c6066f"}, + {file = "mypy-1.10.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:6166a88b15f1759f94a46fa474c7b1b05d134b1b61fca627dd7335454cc9aa6b"}, + {file = "mypy-1.10.1-cp311-cp311-win_amd64.whl", hash = "sha256:5bb9cd11c01c8606a9d0b83ffa91d0b236a0e91bc4126d9ba9ce62906ada868e"}, + {file = "mypy-1.10.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:d8681909f7b44d0b7b86e653ca152d6dff0eb5eb41694e163c6092124f8246d7"}, + {file = "mypy-1.10.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:378c03f53f10bbdd55ca94e46ec3ba255279706a6aacaecac52ad248f98205d3"}, + {file = "mypy-1.10.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6bacf8f3a3d7d849f40ca6caea5c055122efe70e81480c8328ad29c55c69e93e"}, + {file = "mypy-1.10.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:701b5f71413f1e9855566a34d6e9d12624e9e0a8818a5704d74d6b0402e66c04"}, + {file = "mypy-1.10.1-cp312-cp312-win_amd64.whl", hash = "sha256:3c4c2992f6ea46ff7fce0072642cfb62af7a2484efe69017ed8b095f7b39ef31"}, + {file = "mypy-1.10.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:604282c886497645ffb87b8f35a57ec773a4a2721161e709a4422c1636ddde5c"}, + {file = "mypy-1.10.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:37fd87cab83f09842653f08de066ee68f1182b9b5282e4634cdb4b407266bade"}, + {file = "mypy-1.10.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8addf6313777dbb92e9564c5d32ec122bf2c6c39d683ea64de6a1fd98b90fe37"}, + {file = "mypy-1.10.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:5cc3ca0a244eb9a5249c7c583ad9a7e881aa5d7b73c35652296ddcdb33b2b9c7"}, + {file = "mypy-1.10.1-cp38-cp38-win_amd64.whl", hash = "sha256:1b3a2ffce52cc4dbaeee4df762f20a2905aa171ef157b82192f2e2f368eec05d"}, + {file = "mypy-1.10.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:fe85ed6836165d52ae8b88f99527d3d1b2362e0cb90b005409b8bed90e9059b3"}, + {file = "mypy-1.10.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:c2ae450d60d7d020d67ab440c6e3fae375809988119817214440033f26ddf7bf"}, + {file = "mypy-1.10.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6be84c06e6abd72f960ba9a71561c14137a583093ffcf9bbfaf5e613d63fa531"}, + {file = "mypy-1.10.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:2189ff1e39db399f08205e22a797383613ce1cb0cb3b13d8bcf0170e45b96cc3"}, + {file = "mypy-1.10.1-cp39-cp39-win_amd64.whl", hash = "sha256:97a131ee36ac37ce9581f4220311247ab6cba896b4395b9c87af0675a13a755f"}, + {file = "mypy-1.10.1-py3-none-any.whl", hash = "sha256:71d8ac0b906354ebda8ef1673e5fde785936ac1f29ff6987c7483cfbd5a4235a"}, + {file = "mypy-1.10.1.tar.gz", hash = "sha256:1f8f492d7db9e3593ef42d4f115f04e556130f2819ad33ab84551403e97dd4c0"}, ] [package.dependencies] @@ -848,27 +905,27 @@ resolved_reference = "e5fb6ed5b1aebf1c0d67087397b3c1240ff412da" [[package]] name = "pybind11" -version = "2.12.0" +version = "2.13.1" 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.1-py3-none-any.whl", hash = "sha256:97881536abe0cd4260a9ccc5bf6d1cf3113318f08af1feb82d4b9f95e93f0aa4"}, + {file = "pybind11-2.13.1.tar.gz", hash = "sha256:65be498b1cac516161add1508e65375674916bebf2570d057dc9c3c7bcbbc7b0"}, ] [package.extras] -global = ["pybind11-global (==2.12.0)"] +global = ["pybind11-global (==2.13.1)"] [[package]] name = "pycodestyle" -version = "2.11.1" +version = "2.12.0" 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.0-py2.py3-none-any.whl", hash = "sha256:949a39f6b86c3e1515ba1787c2022131d165a8ad271b11370a8819aa070269e4"}, + {file = "pycodestyle-2.12.0.tar.gz", hash = "sha256:442f950141b4f43df752dd303511ffded3a04c2b6fb7f65980574f0c31e6e79c"}, ] [[package]] @@ -896,42 +953,14 @@ files = [ [package.extras] windows-terminal = ["colorama (>=0.4.6)"] -[[package]] -name = "pyk" -version = "7.0.130" -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" -pytest = "*" -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.130" -resolved_reference = "7e036e3f2ec92655c9a4077baac835235f899057" -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]] @@ -1056,18 +1085,29 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] [[package]] name = "setuptools" -version = "70.0.0" +version = "70.2.0" description = "Easily download, build, install, upgrade, and uninstall Python packages" optional = false python-versions = ">=3.8" 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-70.2.0-py3-none-any.whl", hash = "sha256:b8b8060bb426838fbe942479c90296ce976249451118ef566a5a0b7d8b78fb05"}, + {file = "setuptools-70.2.0.tar.gz", hash = "sha256:bd63e505105011b25c3c11f753f7e3b8465ea739efddaccef8f0efac2137bac1"}, ] [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"] +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"] +test = ["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)", "jaraco.test", "mypy (==1.10.0)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (>=0.3.2)", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] + +[[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" @@ -1187,4 +1227,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "429d9f0bd932d5783e5503c1059f01ee4c36f9acf9b3605916541531e6e92210" +content-hash = "5734af9a50eed783985751597dde8aa20d4c3bb1936e40f6b7421a77f7b28e38" diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index b4cafcd4f..3558850c8 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.63" +version = "0.1.77" 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.130", subdirectory = "pyk" } +kframework = "7.1.44" 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/wasm-semantics/auxil.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md index 1ed01b680..2cd20e5f1 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/auxil.md @@ -24,7 +24,7 @@ module WASM-AUXIL #clearConfig => .K ... _ => .Int _ => .ValStack - _ => .Map + _ => .List _ => .Bag _ => .Map _ => 0 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-ref.k b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/list-ref.k index 4c2f437db..6aecad8f3 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) ] 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 8bb1ece79..000000000 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/map-int-to-int.k +++ /dev/null @@ -1,463 +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), symbol(_MapIntToInt_), - assoc, comm, unit(.MapIntToInt), element(_Int2Int|->_), - index(0), format(%1%n%2) - ] - syntax MapIntToInt ::= ".MapIntToInt" - [ function, total, hook(MAP.unit), - symbol(.MapIntToInt) - ] - syntax MapIntToInt ::= WrappedInt "Int2Int|->" WrappedInt - [ function, total, hook(MAP.element), - symbol(_Int2Int|->_), - injective - ] - - syntax priority _Int2Int|->_ > _MapIntToInt_ .MapIntToInt - syntax non-assoc _Int2Int|->_ - syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" - [function, hook(MAP.lookup), symbol(MapIntToInt:lookup)] - syntax WrappedInt ::= MapIntToInt "[" WrappedInt "]" "orDefault" WrappedInt - [ function, total, hook(MAP.lookupOrDefault), - symbol(MapIntToInt:lookupOrDefault) - ] - syntax MapIntToInt ::= MapIntToInt "[" key: WrappedInt "<-" value: WrappedInt "]" - [ function, total, symbol(MapIntToInt:update), - hook(MAP.update), prefer - ] - syntax MapIntToInt ::= MapIntToInt "[" WrappedInt "<-" "undef" "]" - [ function, total, hook(MAP.remove), - symbol(_MapIntToInt[_<-undef]) - ] - 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), symbol(MapIntToInt.sizeMap)] - syntax Bool ::= MapIntToInt "<=Map" MapIntToInt - [function, total, hook(MAP.inclusion)] - syntax WrappedInt ::= choice(MapIntToInt) - [function, hook(MAP.choice), symbol(MapIntToInt:choice)] -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, symbol(MapIntToInt:primitiveLookup)] - syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int - [ function, total, symbol(MapIntToInt:primitiveLookupOrDefault) ] - syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}" - [ function, total, symbol(MapIntToInt:primitiveUpdate), - prefer - ] - syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}" - [ function, total, symbol(MapIntToInt:primitiveRemove) ] - syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}" - [function, total, symbol(MapIntToInt:primitiveInKeys)] - - 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(MapIntToInt:primitiveLookup)] - syntax Int ::= MapIntToInt "{{" Int "}}" "orDefault" Int - [ function, total, symbol(MapIntToInt:primitiveLookupOrDefault) ] - syntax MapIntToInt ::= MapIntToInt "{{" key: Int "<-" value: Int "}}" - [ function, total, symbol(MapIntToInt:primitiveUpdate), - prefer - ] - syntax MapIntToInt ::= MapIntToInt "{{" Int "<-" "undef" "}}" - [ function, total, symbol(MapIntToInt:primitiveRemove) ] - syntax Bool ::= Int "in_keys" "{{" MapIntToInt "}}" - [function, total, symbol(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, preserves-definedness] - - rule (K1 Int2Int|-> V1 M:MapIntToInt) {{ K2 <- undef }} - => (K1 Int2Int|-> V1 (M {{ K2 <- undef }})) - requires unwrap( K1 ) =/=K K2 - [simplification, preserves-definedness] - - 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 - [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), preserves-definedness] - - - 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, preserves-definedness] - rule M:MapIntToInt [ K <- V ] => (K Int2Int|-> V M) requires notBool (K in_keys(M)) - [simplification, preserves-definedness] - 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, preserves-definedness] - - 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, preserves-definedness] - - 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), preserves-definedness] - 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), preserves-definedness] - rule K1 in_keys((K2 Int2Int|-> V) M:MapIntToInt) - => K1 ==K K2 orBool K1 in_keys(M) - requires definedMapElementConcat(K2, V, M) - [simplification(100), preserves-definedness] - - - 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(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, preserves-definedness] - - 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 595cd85f7..63b0b3d00 100644 --- a/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k +++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/data/sparse-bytes.k @@ -4,8 +4,8 @@ module SPARSE-BYTES 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) @@ -13,41 +13,41 @@ module SPARSE-BYTES syntax SparseBytes ::= List{SBItemChunk, ""} syntax Bytes ::= unwrap(SparseBytes) - [function, total, symbol, klabel(SparseBytes:unwrap)] + [function, total, symbol(SparseBytes:unwrap)] // ----------------------------------------------------------------- rule unwrap(SBChunk(SBI) REST) => unwrap(SBI) +Bytes unwrap(REST) 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)) syntax Bytes ::= unwrap(SBItem) - [function, total, symbol, klabel(SBItem:unwrap)] + [function, total, symbol(SBItem:unwrap)] // ----------------------------------------------- rule unwrap(#bytes(Bs)) => Bs rule unwrap(#empty(N)) => zeros(N) - syntax Bytes ::= zeros(Int) [function, total, symbol, klabel(zeros)] + syntax Bytes ::= zeros(Int) [function, total, symbol(zeros)] // ------------------------------------------------------------------- rule zeros(N) => padLeftBytes(.Bytes, size(#empty(N)), 0) syntax Int ::= size(SparseBytes) - [function, total, klabel(SparseBytes:size), symbol] + [function, total, symbol(SparseBytes:size)] // --------------------------------------------------- rule size(SBChunk(SBI) SBS) => size(SBI) +Int size(SBS) rule size(.SparseBytes) => 0 syntax Int ::= size(SBItem) - [function, total, symbol, klabel(SBItem:size)] + [function, total, symbol(SBItem:size)] // ----------------------------------------------- rule size(#bytes(Bs)) => lengthBytes(Bs) rule size(#empty(N)) => maxInt(N,0) 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 ) @@ -66,7 +66,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 @@ -115,7 +115,7 @@ module SPARSE-BYTES requires S .SparseBytes @@ -156,7 +156,7 @@ module SPARSE-BYTES 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/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 #assertLocal INDEX VALUE _ => .K ... - ... INDEX |-> VALUE ... + LOCALS + requires LOCALS[INDEX] ==K VALUE rule #assertGlobal TFIDX VALUE _ => .K ... CUR @@ -569,7 +570,7 @@ This checks that the last allocated memory has the given size and max value. CUR IDS - wrap(#ContextLookup(IDS, TFIDX)) Int2Int|-> wrap(ADDR) + #ContextLookup(IDS, TFIDX) |-> ADDR ... @@ -588,7 +589,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..22ca53e56 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)] // ----------------------------------------------------------------------------------------------- ``` @@ -1174,7 +1186,6 @@ They are currently supported in KWasm text files, but may be deprecated. rule #t2aInstr(#block(VT:VecType, IS:Instrs, BLOCKINFO)) => #block(VT, #t2aInstrs(IS), BLOCKINFO) - rule #t2aInstr<_>(init_local I V) => init_local I V rule #t2aInstr<_>(init_locals VS) => init_locals VS ``` diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/wasm.md index a0d4e8bfd..721162e43 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,29 @@ 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)] // ----------------------------------- 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 +106,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)] // -------------------------------------------------------------- ``` @@ -164,10 +163,9 @@ Internal Syntax module WASM-INTERNAL-SYNTAX imports WASM-DATA-INTERNAL-SYNTAX - syntax Instr ::= "init_local" Int Val - | "init_locals" ValStack - | "#init_locals" Int ValStack - // -------------------------------------------- + syntax Instr ::= "init_locals" ValStack + | "#init_locals" ValStack + // ---------------------------------------- syntax Int ::= #pageSize() [function, total] syntax Int ::= #maxMemorySize() [function, total] @@ -184,8 +182,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 @@ -202,8 +199,8 @@ module WASM .K .ValStack - .Map - .Int + .List + .Int .Map .Map @@ -219,9 +216,9 @@ module WASM .Map 0 .Map - .MapIntToInt + .Map .Map - .MapIntToInt + .Map 0 .Map .Map @@ -449,11 +446,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 +489,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 +501,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 +509,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 +518,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 +543,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 @@ -549,39 +557,37 @@ Variable Operators The various `init_local` variants assist in setting up the `locals` cell. ```k - rule init_local INDEX VALUE => .K ... - LOCALS => LOCALS [ INDEX <- VALUE ] + rule init_locals VALUES => #init_locals VALUES ... + _ => .List - rule init_locals VALUES => #init_locals 0 VALUES ... - - rule #init_locals _ .ValStack => .K ... - rule #init_locals N (VALUE : VALSTACK) - => init_local N VALUE - ~> #init_locals (N +Int 1) VALSTACK + rule #init_locals .ValStack => .K ... + rule #init_locals (VALUE : VALSTACK) + => #init_locals VALSTACK ... + ... .List => ListItem(VALUE) ``` 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 - ... I |-> VALUE ... + VALSTACK => {LOCALS [ I ]}:>Val : VALSTACK + LOCALS rule #local.set(I) => .K ... VALUE : VALSTACK => VALSTACK LOCALS => LOCALS[I <- VALUE] - requires I in_keys(LOCALS) + requires I >=Int 0 andBool I #local.tee(I) => .K ... VALUE : _VALSTACK LOCALS => LOCALS[I <- VALUE] - requires I in_keys(LOCALS) + requires I >=Int 0 andBool I #global(... type: TYP, init: IS, metadata: OID) => sequenceInstrs(IS) ~> allocglobal(OID, TYP) ... @@ -629,8 +635,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 +676,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 +938,7 @@ The `get` and `set` instructions read and write globals. CUR ... TID |-> TA ... - ... wrap(EID) Int2Int|-> wrap(EA) ... + ... EID |-> EA ... ... @@ -965,7 +971,7 @@ The `get` and `set` instructions read and write globals. CUR CUR - ... wrap(EID) Int2Int|-> wrap(EA) ... + ... EID |-> EA ... ... @@ -1017,8 +1023,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 +1080,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 +1097,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 +1126,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 +1159,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)] // --------------------------------------------------------------------------------------- ``` @@ -1164,8 +1170,8 @@ Similar to labels, they sit on the instruction stack (the `` cell), and Unlike labels, only one frame can be "broken" through at a time. ```k - syntax Frame ::= "frame" Int ValTypes ValStack Map - // -------------------------------------------------- + syntax Frame ::= "frame" Int ValTypes ValStack List + // --------------------------------------------------- rule frame MODIDX' TRANGE VALSTACK' LOCAL' => .K ... VALSTACK => #take(lengthValTypes(TRANGE), VALSTACK) ++ VALSTACK' _ => LOCAL' @@ -1187,7 +1193,7 @@ The `#take` function will return the parameter stack in the reversed order, then ... VALSTACK => .ValStack - LOCAL => .Map + LOCAL MODIDX => MODIDX' FADDR @@ -1208,7 +1214,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 +1227,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 +1302,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) ... @@ -1341,7 +1347,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 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 +1361,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 @@ -1377,7 +1383,7 @@ The `storeX` operations first wrap the the value to be stored to the bit wdith ` The value is encoded as bytes and stored at the "effective address", which is the address given on the stack plus offset. ```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 +1392,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 ... @@ -1428,7 +1435,7 @@ The value is fetched from the "effective address", which is the address given on Sort `Signedness` is defined in module `BYTES`. ```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 +1452,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,6 +1480,11 @@ 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)) ... ``` @@ -1482,7 +1495,7 @@ The `size` operation returns the size of the memory, measured in pages. CUR CUR - wrap(0) Int2Int|-> wrap(ADDR) + 0 |-> ADDR ... @@ -1508,7 +1521,7 @@ By setting the `` field in the configuration to `true CUR CUR - wrap(0) Int2Int|-> wrap(ADDR) + 0 |-> ADDR ... @@ -1524,7 +1537,7 @@ By setting the `` field in the configuration to `true CUR CUR - wrap(0) Int2Int|-> wrap(ADDR) + 0 |-> ADDR ... @@ -1556,11 +1569,11 @@ 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 +1614,7 @@ Element Segments CUR FADDRS - ADDRS => ADDRS {{ NEXTIDX <- NEXTADDR }} + ADDRS => ADDRS [ NEXTIDX <- NEXTADDR ] NEXTIDX => NEXTIDX +Int 1 IDS => #saveId(IDS, OID, 0) ... @@ -1630,7 +1643,7 @@ 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. @@ -1642,7 +1655,7 @@ The `data` initializer simply puts these bytes into the specified memory, starti CUR CUR - wrap(MEMIDX) Int2Int|-> wrap(ADDR) + MEMIDX |-> ADDR ... @@ -1662,7 +1675,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 +1693,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 +1713,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) ... @@ -1763,14 +1776,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 +1850,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/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt index 64de12c20..ddf8d0117 100644 --- a/tests/conformance/unparseable.txt +++ b/tests/conformance/unparseable.txt @@ -22,3 +22,4 @@ memory.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..418a8b554 100644 --- a/tests/conformance/unsupported-llvm.txt +++ b/tests/conformance/unsupported-llvm.txt @@ -12,4 +12,5 @@ left-to-right.wast linking.wast memory_redundancy.wast memory_trap.wast +tokens.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/success-llvm.out b/tests/success-llvm.out index 0eae581e8..bdfd25dfa 100644 --- a/tests/success-llvm.out +++ b/tests/success-llvm.out @@ -11,7 +11,7 @@ - .Map + .List .Int 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