Merge branch 'master' into sparse-bytes-lemmas

Author: bbyalcinkaya

.github/workflows/master-push.yml

@@ -41,7 +41,6 @@ jobs:
       matrix:
         include:
           - runner: normal
-          - runner: macos-13
           - runner: ARM64
     runs-on: ${{ matrix.runner }}
     steps:
@@ -53,20 +52,6 @@ jobs:
       - name: 'Upgrade bash'
         if: ${{ contains(matrix.os, 'macos') }}
         run: brew install bash
-      - name: 'Install Nix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v19
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.13.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/cachix-action@v12
-        with:
-          name: k-framework
-          signingKey: ${{ secrets.CACHIX_SIGNING_KEY }}
-          skipPush: true
       - name: 'Build and cache KWASM'
         uses: workflow/[email protected]
         env:

.github/workflows/test-pr.yml

@@ -115,7 +115,6 @@ jobs:
       matrix:
         include:
           - runner: normal
-          - runner: macos-13
           - runner: ARM64
     needs: pykwasm-code-quality-checks
     runs-on: ${{ matrix.runner }}
@@ -126,21 +125,6 @@ jobs:
         with:
           # Check out pull request HEAD instead of merge commit.
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Install Nix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/install-nix-action@v25
-        with:
-          install_url: https://releases.nixos.org/nix/nix-2.19.3/install
-          extra_nix_config: |
-            access-tokens = github.com=${{ secrets.GITHUB_TOKEN }}
-            substituters = http://cache.nixos.org https://cache.iog.io
-            trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ=
-      - name: 'Install Cachix'
-        if: ${{ matrix.runner == 'macos-13' }}
-        uses: cachix/cachix-action@v14
-        with:
-          name: k-framework
-          authToken: ${{ secrets.CACHIX_PUBLIC_TOKEN }}
       - name: 'Build KWASM'
         run: GC_DONT_GC=1 nix build .#kwasm --extra-experimental-features 'nix-command flakes' --print-build-logs
       - name: 'Build KWASM-Pyk'

.github/workflows/update-version.yml

@@ -47,7 +47,6 @@ jobs:
         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'

Dockerfile

@@ -26,11 +26,12 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
 USER user:user
 WORKDIR /home/user
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - \
-    && poetry --version
+RUN    curl -sSL https://install.python-poetry.org | POETRY_VERSION=1.8.3 python3 -
 
 RUN pip3 install --user  \
            cytoolz       \
            numpy
 
-ENV PATH=/home/user/wabt/build:/home/user/.local/bin:$PATH
+ENV PATH=/home/user/.local/bin:$PATH
+
+RUN poetry --version

Makefile

@@ -55,7 +55,7 @@ tests/%.run-term: tests/%
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 
 tests/%.parse: tests/%
-	K_OPTS='-Xmx16G -Xss512m' $(TEST) kast $< kast > $@-out
+	K_OPTS='-Xmx16G -Xss512m' $(TEST) kast --output kore $< > $@-out
 	rm -rf $@-out
 
 tests/%.prove: tests/%

README.md

@@ -6,8 +6,9 @@ KWasm: Semantics of WebAssembly in K
 
 ---
 
-This repository presents a prototype formal semantics of [WebAssembly].
-It is currently under construction.
+This repository presents the formal semantics of [WebAssembly].
+KWasm is a mature and production-ready semantics for WebAssembly, actively developed and maintained since 2019.
+
 For examples of current capabilities, see the unit tests under the `tests/simple` directory.
 
 Repository Structure

deps/k_release

@@ -1 +1 @@
-7.1.38
+7.1.191