From 9d936efcf5363877d65234558ef13270763e4ce4 Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Tue, 25 Aug 2026 18:19:53 +0000
Subject: [PATCH 1/7] CI: run the Cranelift verifier.

This PR adds a GitHub workflow that runs on pushes to main and on
PRs. It restores the verifier's SMT query cache from the
shared actions cache, runs 'verify.sh rebuild-cache' on top of it, and
(on main) republishes the rebuilt cache as the isle-veri-cache.tar.gz
asset on the rolling dev release plus a run artifact for use by
local developers.

It also adds a script, cranelift/isle/veri/setup/download-cache.sh, so a
local user can download the current CI cache from the dev release and
verify incrementally on top of it.
---
 .github/workflows/isle-veri.yml             | 121 ++++++++++++++++++++
 .gitignore                                  |   2 +
 cranelift/isle/veri/README.md               |  21 ++++
 cranelift/isle/veri/setup/download-cache.sh |  52 +++++++++
 cranelift/isle/veri/verify.sh               |   8 +-
 5 files changed, 201 insertions(+), 3 deletions(-)
 create mode 100644 .github/workflows/isle-veri.yml
 create mode 100755 cranelift/isle/veri/setup/download-cache.sh

diff --git a/.github/workflows/isle-veri.yml b/.github/workflows/isle-veri.yml
new file mode 100644
index 000000000000..6ae6a85ceff1
--- /dev/null
+++ b/.github/workflows/isle-veri.yml
@@ -0,0 +1,121 @@
+# Run the ISLE verifier (cranelift/isle/veri) on every push to `main` and on
+# pull requests, sharing the SMT query cache across runs so each run is
+# incremental.
+#
+# The cache is shared two ways:
+#
+#   * `actions/cache` keeps a rolling cache under the key prefix
+#     `isle-veri-cache-v1` (bump the version if the cache format changes).
+#     Cache entries are immutable and branch-scoped: each run saves under a
+#     unique key and restores the most recent entry by prefix. Runs on `main`
+#     save to the default-branch scope; PR runs can restore that cache
+#     read-only but cannot write to it, so PRs always verify on top of the
+#     latest `main` cache without being able to update it.
+#   * Runs on `main` additionally publish the rebuilt cache as the
+#     `isle-veri-cache.tar.gz` asset on the rolling `dev` release (maintained
+#     by `publish-artifacts.yml`) and as a run artifact, so the cache is
+#     durable and downloadable by local users via
+#     `cranelift/isle/veri/setup/download-cache.sh`.
+#
+# The job runs `verify.sh rebuild-cache`, which verifies every expansion
+# (invoking the SMT solver for cache misses) and garbage-collects unused
+# cache entries.
+name: ISLE Verifier
+on:
+  push:
+    branches: [main]
+    tags-ignore: [dev]
+  pull_request:
+  workflow_dispatch:
+
+# `cache: write` is required for the cache save steps when a permissions
+# block is present (everything unspecified defaults to `read`).
+permissions:
+  contents: write
+  cache: write
+
+jobs:
+  verify:
+    name: ISLE verifier
+    runs-on: ubuntu-latest
+    if: github.repository == 'bytecodealliance/wasmtime'
+    # Runs can be cold (no cached SMT queries) and are slow then; use the
+    # maximum allowed timeout to be safe.
+    timeout-minutes: 360
+    steps:
+    - uses: actions/checkout@v6
+      with:
+        submodules: true
+    - uses: ./.github/actions/install-rust
+    - name: Read pinned solver versions
+      run: |
+        echo "CVC5_VERSION=$(sed -n 's/^version="\([^"]*\)".*/\1/p' cranelift/isle/veri/setup/install-cvc5.sh)" >> "${GITHUB_ENV}"
+        echo "Z3_VERSION=$(sed -n 's/^version="\([^"]*\)".*/\1/p' cranelift/isle/veri/setup/install-z3.sh)" >> "${GITHUB_ENV}"
+    - uses: actions/cache/restore@v5
+      id: smt-solvers
+      with:
+        path: ~/.cache/smt-solvers
+        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
+    - uses: ./.github/actions/apt-get-install
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      with:
+        packages: wget unzip
+    - name: Install SMT solvers (cvc5, z3)
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      run: |
+        solver_dir="$HOME/.cache/smt-solvers"
+        mkdir -p "${solver_dir}/bin"
+        ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}"
+        ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
+    - uses: actions/cache/save@v5
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      with:
+        path: ~/.cache/smt-solvers
+        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
+    - name: Add solvers to PATH
+      run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
+    - name: Restore verifier SMT query cache
+      uses: actions/cache/restore@v5
+      id: veri-cache
+      with:
+        path: cranelift/isle/veri/cache
+        # Cache entries are immutable: each run saves under a unique key and
+        # restores the most recent entry by prefix. Bump `v1` if the cache
+        # format changes.
+        key: isle-veri-cache-v1-${{ github.run_id }}
+        restore-keys: |
+          isle-veri-cache-v1-
+    - name: Verify and rebuild cache
+      run: |
+        mkdir -p cranelift/isle/veri/cache
+        ./cranelift/isle/veri/verify.sh rebuild-cache
+    - name: Save verifier SMT query cache
+      # Only `main` writes to the shared cache; PR runs restore it read-only.
+      if: github.ref == 'refs/heads/main'
+      uses: actions/cache/save@v5
+      with:
+        path: cranelift/isle/veri/cache
+        key: isle-veri-cache-v1-${{ github.run_id }}
+    - name: Package rebuilt cache
+      if: github.ref == 'refs/heads/main'
+      run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
+    - name: Upload cache tarball as run artifact
+      if: github.ref == 'refs/heads/main'
+      uses: actions/upload-artifact@v6
+      with:
+        name: isle-veri-cache
+        path: isle-veri-cache.tar.gz
+    - name: Update dev release
+      if: github.ref == 'refs/heads/main'
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        if gh release view dev >/dev/null 2>&1; then
+            gh release upload dev isle-veri-cache.tar.gz --clobber
+        else
+            # Can happen on the very first run, before publish-artifacts
+            # has created the dev release yet. The tarball is still
+            # available as a run artifact, and the next run will pick up
+            # the rebuilt cache from the actions cache anyway.
+            echo "::warning::The dev release does not exist yet; skipping the release upload."
+        fi
diff --git a/.gitignore b/.gitignore
index b2bd0637572c..8c52fc21132f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -36,3 +36,5 @@ miri-wast/
 report/
 # Local SMT query cache for the ISLE verifier (see cranelift/isle/veri/verify.sh).
 cranelift/isle/veri/cache/
+# Staging directory used by `verify.sh rebuild-cache` before it swaps in.
+cranelift/isle/veri/cache.rebuild/
diff --git a/cranelift/isle/veri/README.md b/cranelift/isle/veri/README.md
index e44e3c56b63d..f3ad8c9749fb 100644
--- a/cranelift/isle/veri/README.md
+++ b/cranelift/isle/veri/README.md
@@ -38,6 +38,27 @@ Alternatively, on Linux or MacOS you can install from Github release with:
 
 If you use this method, ensure that `<install_path>/bin` is on your `$PATH`.
 
+## Sharing the cache with CI
+
+To keep local runs fast, CI maintains a shared copy of the verifier's SMT query
+cache. On every push to `main`, the "ISLE Verifier" workflow
+([`.github/workflows/isle-veri.yml`](../../.github/workflows/isle-veri.yml))
+runs `verify.sh rebuild-cache` on top of the previously published cache and
+publishes the result as the `isle-veri-cache.tar.gz` asset on the rolling
+[`dev` release](https://github.com/bytecodealliance/wasmtime/releases/tag/dev).
+Pull requests also run the verifier against the latest `main` cache (read-only).
+
+To start a local session from the cache CI is currently using, run:
+
+```
+./cranelift/isle/veri/setup/download-cache.sh
+```
+
+This downloads the latest asset from the `dev` release and installs it as
+`cranelift/isle/veri/cache`. You can then verify incrementally on top of it
+with `./cranelift/isle/veri/verify.sh` (and check full cache coverage with
+`verify.sh cache-only`).
+
 ## Configuration files
 
 Rather than configuring arguments on the command line, you can store
diff --git a/cranelift/isle/veri/setup/download-cache.sh b/cranelift/isle/veri/setup/download-cache.sh
new file mode 100755
index 000000000000..1b275fcd7616
--- /dev/null
+++ b/cranelift/isle/veri/setup/download-cache.sh
@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+#
+# Download the latest ISLE verifier SMT query cache from the `dev` release on
+# github.com/bytecodealliance/wasmtime and install it as
+# cranelift/isle/veri/cache, so a local run of verify.sh starts from the same
+# state CI is currently using.
+#
+# The `dev` release is refreshed on every push to `main` by the
+# "ISLE Verifier" CI workflow (see .github/workflows/isle-veri.yml).
+#
+# Usage:
+#   ./cranelift/isle/veri/setup/download-cache.sh
+#
+# Requires: curl, tar.
+# Optionally set GH_TOKEN to avoid GitHub API rate limits (unauthenticated
+# requests are limited to 60/hour per IP).
+
+set -euo pipefail
+
+repo="bytecodealliance/wasmtime"
+release="dev"
+asset="isle-veri-cache.tar.gz"
+cache_dir="cranelift/isle/veri/cache"
+
+cd "$(git rev-parse --show-toplevel)"
+
+if [ -n "${GH_TOKEN:-}" ]; then
+    curl_args=(-fsSL -H "Authorization: Bearer ${GH_TOKEN}")
+else
+    curl_args=(-fsSL)
+fi
+
+json=$(curl "${curl_args[@]}" \
+    "https://api.github.com/repos/${repo}/releases/tags/${release}")
+
+# Extract the browser_download_url of our asset from the release JSON.
+url=$(printf '%s\n' "$json" \
+    | { grep -o "\"browser_download_url\"[[:space:]]*:[[:space:]]*\"[^\"]*/${asset}\"" || true; } \
+    | sed 's/.*"browser_download_url"[[:space:]]*:[[:space:]]*"//; s/"$//')
+if [ -z "$url" ]; then
+    echo "ERROR: asset '${asset}' not found on release '${release}' of ${repo}" >&2
+    exit 1
+fi
+
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+curl -fL --progress-bar -o "${tmp}/${asset}" "$url"
+
+rm -rf "$cache_dir"
+tar xzf "${tmp}/${asset}" -C cranelift/isle/veri
+echo "Installed verifier cache to ${cache_dir}/"
+echo "You can now run ./cranelift/isle/veri/verify.sh (or cache-only / rebuild-cache)."
diff --git a/cranelift/isle/veri/verify.sh b/cranelift/isle/veri/verify.sh
index ea4e3dc649a1..72238f87303d 100755
--- a/cranelift/isle/veri/verify.sh
+++ b/cranelift/isle/veri/verify.sh
@@ -2,9 +2,11 @@
 #
 # Driver for VeriISLE verification with the SMT query cache.
 #
-# The cache lives locally at cranelift/isle/veri/cache (gitignored). Sharing
-# the cache across runs in CI (via artifacts) is planned separately; for now
-# these modes manage a local cache only.
+# The cache lives locally at cranelift/isle/veri/cache (gitignored). CI
+# refreshes the cache on every push to main and publishes it as
+# isle-veri-cache.tar.gz on the `dev` release (see
+# .github/workflows/isle-veri.yml); local users can download it with
+# setup/download-cache.sh.
 #
 # Usage:
 #   ./cranelift/isle/veri/verify.sh [MODE]

From 7b3702c1ed1a255fc033b5185aa86c6d109a7121 Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Tue, 25 Aug 2026 22:46:58 +0000
Subject: [PATCH 2/7] Review feedback:

- Move job into `main.yml` workflow.
- Add branch spec to PR section.
---
 .github/workflows/isle-veri.yml             | 121 --------------------
 .github/workflows/main.yml                  | 103 +++++++++++++++--
 cranelift/isle/veri/README.md               |   9 +-
 cranelift/isle/veri/setup/download-cache.sh |   4 +-
 cranelift/isle/veri/verify.sh               |   6 +-
 5 files changed, 104 insertions(+), 139 deletions(-)
 delete mode 100644 .github/workflows/isle-veri.yml

diff --git a/.github/workflows/isle-veri.yml b/.github/workflows/isle-veri.yml
deleted file mode 100644
index 6ae6a85ceff1..000000000000
--- a/.github/workflows/isle-veri.yml
+++ /dev/null
@@ -1,121 +0,0 @@
-# Run the ISLE verifier (cranelift/isle/veri) on every push to `main` and on
-# pull requests, sharing the SMT query cache across runs so each run is
-# incremental.
-#
-# The cache is shared two ways:
-#
-#   * `actions/cache` keeps a rolling cache under the key prefix
-#     `isle-veri-cache-v1` (bump the version if the cache format changes).
-#     Cache entries are immutable and branch-scoped: each run saves under a
-#     unique key and restores the most recent entry by prefix. Runs on `main`
-#     save to the default-branch scope; PR runs can restore that cache
-#     read-only but cannot write to it, so PRs always verify on top of the
-#     latest `main` cache without being able to update it.
-#   * Runs on `main` additionally publish the rebuilt cache as the
-#     `isle-veri-cache.tar.gz` asset on the rolling `dev` release (maintained
-#     by `publish-artifacts.yml`) and as a run artifact, so the cache is
-#     durable and downloadable by local users via
-#     `cranelift/isle/veri/setup/download-cache.sh`.
-#
-# The job runs `verify.sh rebuild-cache`, which verifies every expansion
-# (invoking the SMT solver for cache misses) and garbage-collects unused
-# cache entries.
-name: ISLE Verifier
-on:
-  push:
-    branches: [main]
-    tags-ignore: [dev]
-  pull_request:
-  workflow_dispatch:
-
-# `cache: write` is required for the cache save steps when a permissions
-# block is present (everything unspecified defaults to `read`).
-permissions:
-  contents: write
-  cache: write
-
-jobs:
-  verify:
-    name: ISLE verifier
-    runs-on: ubuntu-latest
-    if: github.repository == 'bytecodealliance/wasmtime'
-    # Runs can be cold (no cached SMT queries) and are slow then; use the
-    # maximum allowed timeout to be safe.
-    timeout-minutes: 360
-    steps:
-    - uses: actions/checkout@v6
-      with:
-        submodules: true
-    - uses: ./.github/actions/install-rust
-    - name: Read pinned solver versions
-      run: |
-        echo "CVC5_VERSION=$(sed -n 's/^version="\([^"]*\)".*/\1/p' cranelift/isle/veri/setup/install-cvc5.sh)" >> "${GITHUB_ENV}"
-        echo "Z3_VERSION=$(sed -n 's/^version="\([^"]*\)".*/\1/p' cranelift/isle/veri/setup/install-z3.sh)" >> "${GITHUB_ENV}"
-    - uses: actions/cache/restore@v5
-      id: smt-solvers
-      with:
-        path: ~/.cache/smt-solvers
-        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
-    - uses: ./.github/actions/apt-get-install
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
-      with:
-        packages: wget unzip
-    - name: Install SMT solvers (cvc5, z3)
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
-      run: |
-        solver_dir="$HOME/.cache/smt-solvers"
-        mkdir -p "${solver_dir}/bin"
-        ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}"
-        ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
-    - uses: actions/cache/save@v5
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
-      with:
-        path: ~/.cache/smt-solvers
-        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
-    - name: Add solvers to PATH
-      run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
-    - name: Restore verifier SMT query cache
-      uses: actions/cache/restore@v5
-      id: veri-cache
-      with:
-        path: cranelift/isle/veri/cache
-        # Cache entries are immutable: each run saves under a unique key and
-        # restores the most recent entry by prefix. Bump `v1` if the cache
-        # format changes.
-        key: isle-veri-cache-v1-${{ github.run_id }}
-        restore-keys: |
-          isle-veri-cache-v1-
-    - name: Verify and rebuild cache
-      run: |
-        mkdir -p cranelift/isle/veri/cache
-        ./cranelift/isle/veri/verify.sh rebuild-cache
-    - name: Save verifier SMT query cache
-      # Only `main` writes to the shared cache; PR runs restore it read-only.
-      if: github.ref == 'refs/heads/main'
-      uses: actions/cache/save@v5
-      with:
-        path: cranelift/isle/veri/cache
-        key: isle-veri-cache-v1-${{ github.run_id }}
-    - name: Package rebuilt cache
-      if: github.ref == 'refs/heads/main'
-      run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
-    - name: Upload cache tarball as run artifact
-      if: github.ref == 'refs/heads/main'
-      uses: actions/upload-artifact@v6
-      with:
-        name: isle-veri-cache
-        path: isle-veri-cache.tar.gz
-    - name: Update dev release
-      if: github.ref == 'refs/heads/main'
-      env:
-        GH_TOKEN: ${{ github.token }}
-      run: |
-        if gh release view dev >/dev/null 2>&1; then
-            gh release upload dev isle-veri-cache.tar.gz --clobber
-        else
-            # Can happen on the very first run, before publish-artifacts
-            # has created the dev release yet. The tarball is still
-            # available as a run artifact, and the next run will pick up
-            # the rebuilt cache from the actions cache anyway.
-            echo "::warning::The dev release does not exist yet; skipping the release upload."
-        fi
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 6bbc0afab669..fe631332267e 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1363,20 +1363,105 @@ jobs:
     - run: ${{ matrix.script }}
       if: ${{ matrix.script }}
 
-  # Check the ISLE verifier builds/runs (without invoking the SMT solver, for now).
-  isle_veri_basic_check:
-    needs: determine
-    if: needs.determine.outputs.run-full
-    name: ISLE verifier basic check
+  # Run the full ISLE verifier (see cranelift/isle/veri/) incrementally on top
+  # of a shared SMT query cache. Cache misses are solved with cvc5/z3, so this
+  # is fast when the shared cache is warm and can take a long time (up to the
+  # timeout) when it is cold.
+  #
+  # The cache is shared across runs via the actions cache under the key
+  # prefix `isle-veri-cache-v1` (bump the version if the cache format
+  # changes). Cache entries are immutable, so each run saves under a unique
+  # key and restores the most recent entry by prefix. Caches are
+  # branch-scoped: only runs that land on `main` (the merge queue) write to
+  # the shared cache; PR and release-branch runs restore it read-only.
+  #
+  # Runs that land on `main` also publish the rebuilt cache as the
+  # `isle-veri-cache.tar.gz` asset on the rolling `dev` release and as a run
+  # artifact, so local users can download it with
+  # `cranelift/isle/veri/setup/download-cache.sh`.
+  isle_veri_full_check:
+    name: ISLE verifier full check
     runs-on: ubuntu-latest
+    # Runs can be cold (no cached SMT queries) and are slow then; use the
+    # maximum allowed timeout to be safe.
+    timeout-minutes: 360
+    permissions:
+      contents: write
     steps:
     - uses: actions/checkout@v6
       with:
         submodules: true
     - uses: ./.github/actions/install-rust
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --config cranelift/isle/veri/configs/aarch64-fast.args --skip-solver
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --name x64 --rule iadd_base_case_32_or_64_lea --skip-solver
-    - run: cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes --skip-solver
+    - name: Read pinned solver versions
+      run: |
+        echo "CVC5_VERSION=$(sed -n 's/^version=\"([^\"]*)\".*/\1/p' cranelift/isle/veri/setup/install-cvc5.sh)" >> "${GITHUB_ENV}"
+        echo "Z3_VERSION=$(sed -n 's/^version=\"([^\"]*)\".*/\1/p' cranelift/isle/veri/setup/install-z3.sh)" >> "${GITHUB_ENV}"
+    - uses: actions/cache/restore@v5
+      id: smt-solvers
+      with:
+        path: ~/.cache/smt-solvers
+        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
+    - uses: ./.github/actions/apt-get-install
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      with:
+        packages: wget unzip
+    - name: Install SMT solvers (cvc5, z3)
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      run: |
+        solver_dir="$HOME/.cache/smt-solvers"
+        mkdir -p "${solver_dir}/bin"
+        ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}"
+        ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
+    - uses: actions/cache/save@v5
+      if: steps.smt-solvers.outputs.cache-hit != 'true'
+      with:
+        path: ~/.cache/smt-solvers
+        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
+    - name: Add solvers to PATH
+      run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
+    - name: Restore verifier SMT query cache
+      uses: actions/cache/restore@v5
+      with:
+        path: cranelift/isle/veri/cache
+        # Cache entries are immutable: each run saves under a unique key and
+        # restores the most recent entry by prefix. Bump `v1` if the cache
+        # format changes.
+        key: isle-veri-cache-v1-${{ github.run_id }}
+        restore-keys: |
+          isle-veri-cache-v1-
+    - name: Verify and rebuild cache
+      run: |
+        mkdir -p cranelift/isle/veri/cache
+        ./cranelift/isle/veri/verify.sh rebuild-cache
+    - name: Save verifier SMT query cache
+      # Only runs landing on `main` write to the shared cache; PR and
+      # release-branch runs restore it read-only.
+      if: github.ref_name == 'main'
+      uses: actions/cache/save@v5
+      with:
+        path: cranelift/isle/veri/cache
+        key: isle-veri-cache-v1-${{ github.run_id }}
+    - name: Package rebuilt cache
+      run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
+    - name: Upload cache tarball as run artifact
+      uses: actions/upload-artifact@v6
+      with:
+        name: isle-veri-cache
+        path: isle-veri-cache.tar.gz
+    - name: Update dev release
+      if: github.ref_name == 'main'
+      env:
+        GH_TOKEN: ${{ github.token }}
+      run: |
+        if gh release view dev >/dev/null 2>&1; then
+            gh release upload dev isle-veri-cache.tar.gz --clobber
+        else
+            # Can happen on the very first run, before publish-artifacts
+            # has created the dev release yet. The tarball is still
+            # available as a run artifact, and the next run will pick up
+            # the rebuilt cache from the actions cache anyway.
+            echo "::warning::The dev release does not exist yet; skipping the release upload."
+        fi
 
   # Perform release builds of `wasmtime` and `libwasmtime.so`. Builds a variety
   # of platforms and architectures and then uploads the release artifacts to
@@ -1487,7 +1572,7 @@ jobs:
       - verify-publish
       - determine
       - miri
-      - isle_veri_basic_check
+      - isle_veri_full_check
       - build-preview1-component-adapter
       - build-preview1-component-adapter-provider
       - test-min-platform-example
diff --git a/cranelift/isle/veri/README.md b/cranelift/isle/veri/README.md
index f3ad8c9749fb..28358e284ede 100644
--- a/cranelift/isle/veri/README.md
+++ b/cranelift/isle/veri/README.md
@@ -41,10 +41,11 @@ If you use this method, ensure that `<install_path>/bin` is on your `$PATH`.
 ## Sharing the cache with CI
 
 To keep local runs fast, CI maintains a shared copy of the verifier's SMT query
-cache. On every push to `main`, the "ISLE Verifier" workflow
-([`.github/workflows/isle-veri.yml`](../../.github/workflows/isle-veri.yml))
-runs `verify.sh rebuild-cache` on top of the previously published cache and
-publishes the result as the `isle-veri-cache.tar.gz` asset on the rolling
+cache. The "ISLE verifier full check" job in the CI workflow
+([`.github/workflows/main.yml`](../../.github/workflows/main.yml))
+runs `verify.sh rebuild-cache` on top of the previously published cache and,
+for runs that land on `main`, publishes the result as the
+`isle-veri-cache.tar.gz` asset on the rolling
 [`dev` release](https://github.com/bytecodealliance/wasmtime/releases/tag/dev).
 Pull requests also run the verifier against the latest `main` cache (read-only).
 
diff --git a/cranelift/isle/veri/setup/download-cache.sh b/cranelift/isle/veri/setup/download-cache.sh
index 1b275fcd7616..6c87d8c7d629 100755
--- a/cranelift/isle/veri/setup/download-cache.sh
+++ b/cranelift/isle/veri/setup/download-cache.sh
@@ -5,8 +5,8 @@
 # cranelift/isle/veri/cache, so a local run of verify.sh starts from the same
 # state CI is currently using.
 #
-# The `dev` release is refreshed on every push to `main` by the
-# "ISLE Verifier" CI workflow (see .github/workflows/isle-veri.yml).
+# The `dev` release is refreshed on runs landing on `main` by the
+# "ISLE verifier full check" CI job (see .github/workflows/main.yml).
 #
 # Usage:
 #   ./cranelift/isle/veri/setup/download-cache.sh
diff --git a/cranelift/isle/veri/verify.sh b/cranelift/isle/veri/verify.sh
index 72238f87303d..dd7e77c2ada3 100755
--- a/cranelift/isle/veri/verify.sh
+++ b/cranelift/isle/veri/verify.sh
@@ -3,9 +3,9 @@
 # Driver for VeriISLE verification with the SMT query cache.
 #
 # The cache lives locally at cranelift/isle/veri/cache (gitignored). CI
-# refreshes the cache on every push to main and publishes it as
-# isle-veri-cache.tar.gz on the `dev` release (see
-# .github/workflows/isle-veri.yml); local users can download it with
+# refreshes the cache on runs that land on main and publishes it as
+# isle-veri-cache.tar.gz on the `dev` release (see the isle_veri_full_check
+# job in .github/workflows/main.yml); local users can download it with
 # setup/download-cache.sh.
 #
 # Usage:

From 40c136778861e88183594712d264d727a0f6aaab Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Wed, 26 Aug 2026 16:00:13 -0700
Subject: [PATCH 3/7] Review feedback.

---
 .github/workflows/main.yml                  | 105 ++++++++------------
 .github/workflows/publish-artifacts.yml     |   6 ++
 cranelift/isle/veri/README.md               |  28 ++++--
 cranelift/isle/veri/setup/download-cache.sh |   5 +-
 cranelift/isle/veri/verify.sh               |  29 ++++--
 5 files changed, 95 insertions(+), 78 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index fe631332267e..9d052c51c637 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -189,6 +189,7 @@ jobs:
       run-dwarf: ${{ steps.calculate.outputs.run-dwarf }}
       platform-checks: ${{ steps.calculate.outputs.platform-checks }}
       test-gc-zeal: ${{ steps.calculate.outputs.test-gc-zeal }}
+      run-isle-veri: ${{ steps.calculate.outputs.run-isle-veri }}
     steps:
     - uses: actions/checkout@v6
     - id: calculate
@@ -245,6 +246,15 @@ jobs:
           if grep -q gc names.log; then
             echo test-gc-zeal=true >> $GITHUB_OUTPUT
           fi
+          # Run the ISLE verifier for PRs that touch the ISLE toolchain
+          # (cranelift/isle) or any ISLE source file (*.isle); `prtest:full`
+          # is handled by run_full below.
+          if grep -q cranelift/isle names.log; then
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
+          fi
+          if grep -qE '\.isle$' names.log; then
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
+          fi
         fi
         matrix="$(node ./ci/build-test-matrix.js ./commits.log ./names.log $run_full)"
         echo "test-matrix={\"include\":$(echo $matrix)}" >> $GITHUB_OUTPUT
@@ -263,6 +273,7 @@ jobs:
             echo preview1-adapter=true >> $GITHUB_OUTPUT
             echo run-dwarf=true >> $GITHUB_OUTPUT
             echo platform-checks=true >> $GITHUB_OUTPUT
+            echo run-isle-veri=true >> $GITHUB_OUTPUT
         fi
 
   # Build all documentation of Wasmtime, including the C API documentation,
@@ -1365,82 +1376,68 @@ jobs:
 
   # Run the full ISLE verifier (see cranelift/isle/veri/) incrementally on top
   # of a shared SMT query cache. Cache misses are solved with cvc5/z3, so this
-  # is fast when the shared cache is warm and can take a long time (up to the
-  # timeout) when it is cold.
+  # is fast when the cache is warm and can take a long time when it is cold.
   #
-  # The cache is shared across runs via the actions cache under the key
-  # prefix `isle-veri-cache-v1` (bump the version if the cache format
-  # changes). Cache entries are immutable, so each run saves under a unique
-  # key and restores the most recent entry by prefix. Caches are
-  # branch-scoped: only runs that land on `main` (the merge queue) write to
-  # the shared cache; PR and release-branch runs restore it read-only.
+  # The cache is a named entry in the actions cache, keyed by a hash of the
+  # ISLE sources and the ISLE toolchain (see the "Compute ISLE hash" step).
+  # Caches saved by merge-queue runs are stored in the default branch's
+  # cache scope and are visible to every PR and future merge-queue run, so
+  # each distinct ISLE state gets exactly one immutable entry on `main`, and
+  # no branch ever needs to "update" an existing entry: a new ISLE state is
+  # a new key. PR runs read those entries and, when their ISLE state is new,
+  # save an entry scoped to their own merge ref, so repeated runs of the
+  # same PR verify incrementally on top of their previous run's cache.
   #
-  # Runs that land on `main` also publish the rebuilt cache as the
-  # `isle-veri-cache.tar.gz` asset on the rolling `dev` release and as a run
-  # artifact, so local users can download it with
-  # `cranelift/isle/veri/setup/download-cache.sh`.
+  # The rebuilt cache is also uploaded as the `isle-veri-cache` run
+  # artifact; the `publish-artifacts.yml` workflow publishes it as the
+  # `isle-veri-cache.tar.gz` asset on the rolling `dev` release so local
+  # users can download it with `cranelift/isle/veri/setup/download-cache.sh`.
+  # That asset is a convenience snapshot for humans; CI itself only uses the
+  # named cache above.
   isle_veri_full_check:
+    needs: determine
+    if: needs.determine.outputs.run-isle-veri
     name: ISLE verifier full check
     runs-on: ubuntu-latest
-    # Runs can be cold (no cached SMT queries) and are slow then; use the
-    # maximum allowed timeout to be safe.
+    # Runs can be cold and take a long time; most will not take this long.
     timeout-minutes: 360
-    permissions:
-      contents: write
     steps:
     - uses: actions/checkout@v6
       with:
         submodules: true
     - uses: ./.github/actions/install-rust
-    - name: Read pinned solver versions
-      run: |
-        echo "CVC5_VERSION=$(sed -n 's/^version=\"([^\"]*)\".*/\1/p' cranelift/isle/veri/setup/install-cvc5.sh)" >> "${GITHUB_ENV}"
-        echo "Z3_VERSION=$(sed -n 's/^version=\"([^\"]*)\".*/\1/p' cranelift/isle/veri/setup/install-z3.sh)" >> "${GITHUB_ENV}"
-    - uses: actions/cache/restore@v5
-      id: smt-solvers
-      with:
-        path: ~/.cache/smt-solvers
-        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
     - uses: ./.github/actions/apt-get-install
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
       with:
         packages: wget unzip
     - name: Install SMT solvers (cvc5, z3)
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
       run: |
         solver_dir="$HOME/.cache/smt-solvers"
         mkdir -p "${solver_dir}/bin"
         ./cranelift/isle/veri/setup/install-cvc5.sh -i "${solver_dir}"
         ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
-    - uses: actions/cache/save@v5
-      if: steps.smt-solvers.outputs.cache-hit != 'true'
-      with:
-        path: ~/.cache/smt-solvers
-        key: isle-veri-solvers-${{ runner.os }}-cvc5-${{ env.CVC5_VERSION }}-z3-${{ env.Z3_VERSION }}
     - name: Add solvers to PATH
       run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
-    - name: Restore verifier SMT query cache
-      uses: actions/cache/restore@v5
+    - name: Compute ISLE hash
+      id: isle-hash
+      run: |
+        # Hash of the ISLE sources and the ISLE toolchain itself: list the
+        # cranelift/isle/**/*.rs and cranelift/codegen/**/*.isle files,
+        # sort the file list, hash each file individually (path and
+        # content), then hash the resulting manifest.
+        files=$(git ls-files 'cranelift/isle/**/*.rs' 'cranelift/codegen/**/*.isle' | LC_ALL=C sort -u)
+        echo "hash=$(printf '%s\n' "$files" | xargs -r -d '\n' sha256sum | sha256sum | cut -c1-32)" >> "$GITHUB_OUTPUT"
+    - name: Restore and save verifier cache
+      uses: actions/cache@v5
       with:
         path: cranelift/isle/veri/cache
-        # Cache entries are immutable: each run saves under a unique key and
-        # restores the most recent entry by prefix. Bump `v1` if the cache
-        # format changes.
-        key: isle-veri-cache-v1-${{ github.run_id }}
+        # Bump `v1` if the cache format changes.
+        key: isle-veri-cache-v1-${{ steps.isle-hash.outputs.hash }}
         restore-keys: |
           isle-veri-cache-v1-
     - name: Verify and rebuild cache
       run: |
         mkdir -p cranelift/isle/veri/cache
-        ./cranelift/isle/veri/verify.sh rebuild-cache
-    - name: Save verifier SMT query cache
-      # Only runs landing on `main` write to the shared cache; PR and
-      # release-branch runs restore it read-only.
-      if: github.ref_name == 'main'
-      uses: actions/cache/save@v5
-      with:
-        path: cranelift/isle/veri/cache
-        key: isle-veri-cache-v1-${{ github.run_id }}
+        ./cranelift/isle/veri/verify.sh rebuild-cache aarch64-fast aarch64 opt-fast opt x64-iadd-base-case
     - name: Package rebuilt cache
       run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
     - name: Upload cache tarball as run artifact
@@ -1448,20 +1445,6 @@ jobs:
       with:
         name: isle-veri-cache
         path: isle-veri-cache.tar.gz
-    - name: Update dev release
-      if: github.ref_name == 'main'
-      env:
-        GH_TOKEN: ${{ github.token }}
-      run: |
-        if gh release view dev >/dev/null 2>&1; then
-            gh release upload dev isle-veri-cache.tar.gz --clobber
-        else
-            # Can happen on the very first run, before publish-artifacts
-            # has created the dev release yet. The tarball is still
-            # available as a run artifact, and the next run will pick up
-            # the rebuilt cache from the actions cache anyway.
-            echo "::warning::The dev release does not exist yet; skipping the release upload."
-        fi
 
   # Perform release builds of `wasmtime` and `libwasmtime.so`. Builds a variety
   # of platforms and architectures and then uploads the release artifacts to
diff --git a/.github/workflows/publish-artifacts.yml b/.github/workflows/publish-artifacts.yml
index 2c244e6e9dca..65e43beb4f41 100644
--- a/.github/workflows/publish-artifacts.yml
+++ b/.github/workflows/publish-artifacts.yml
@@ -46,6 +46,12 @@ jobs:
           git push origin dev:dev -f
           gh release create dev --prerelease dist/* ||
             gh release upload dev --clobber dist/*
+          # Refresh the ISLE verifier's shared SMT query cache (see the
+          # isle_veri_full_check job in main.yml), if the CI run produced
+          # one (the job is skipped for runs where the verifier didn't run).
+          if [ -f isle-veri-cache/isle-veri-cache.tar.gz ]; then
+            gh release upload dev --clobber isle-veri-cache/isle-veri-cache.tar.gz
+          fi
       env:
         GH_TOKEN: ${{ github.token }}
 
diff --git a/cranelift/isle/veri/README.md b/cranelift/isle/veri/README.md
index 28358e284ede..23549fbd6ad9 100644
--- a/cranelift/isle/veri/README.md
+++ b/cranelift/isle/veri/README.md
@@ -40,14 +40,24 @@ If you use this method, ensure that `<install_path>/bin` is on your `$PATH`.
 
 ## Sharing the cache with CI
 
-To keep local runs fast, CI maintains a shared copy of the verifier's SMT query
-cache. The "ISLE verifier full check" job in the CI workflow
-([`.github/workflows/main.yml`](../../.github/workflows/main.yml))
-runs `verify.sh rebuild-cache` on top of the previously published cache and,
-for runs that land on `main`, publishes the result as the
-`isle-veri-cache.tar.gz` asset on the rolling
-[`dev` release](https://github.com/bytecodealliance/wasmtime/releases/tag/dev).
-Pull requests also run the verifier against the latest `main` cache (read-only).
+To keep local runs fast, CI maintains a shared copy of the verifier's SMT
+query cache in the GitHub Actions cache under keys of the form
+`isle-veri-cache-v1-<hash>`, where `<hash>` is derived from the ISLE sources
+and toolchain. Runs in the merge queue save entries in the default branch's
+cache scope, so every subsequent PR restores the most recent entry and
+verifies incrementally on top of it.
+
+The current cache is also published as the `isle-veri-cache.tar.gz` asset on
+the rolling
+[`dev` release](https://github.com/bytecodealliance/wasmtime/releases/tag/dev)
+for local use: the "ISLE verifier full check" job in the CI workflow
+([`.github/workflows/main.yml`](../../.github/workflows/main.yml)) uploads the
+rebuilt cache as a run artifact, and the
+[`publish-artifacts.yml`](../../.github/workflows/publish-artifacts.yml)
+workflow publishes it to the `dev` release when the run lands on `main`. The
+job runs on full CI and, on pull requests, when the PR touches the ISLE
+sources (`cranelift/codegen/**/*.isle`) or the ISLE toolchain
+(`cranelift/isle`), or a commit message contains `prtest:full`.
 
 To start a local session from the cache CI is currently using, run:
 
@@ -74,7 +84,7 @@ Blank lines and anything following a `#` (whole-line or trailing comments) are i
 The arguments from the file are applied *before* any passed on the command line, so the command line always takes precedence (for example, you can reuse a config but override its `--timeout`).
 Multi-valued arguments such as `--filter` accumulate, while single-valued arguments (like `--name`) take their last value.
 
-Three example configurations live in [`configs/`](configs):
+Five example configurations live in [`configs/`](configs):
 
 | File                              | Equivalent to                                                       |
 | --------------------------------- | ------------------------------------------------------------------- |
diff --git a/cranelift/isle/veri/setup/download-cache.sh b/cranelift/isle/veri/setup/download-cache.sh
index 6c87d8c7d629..e87a6616fd80 100755
--- a/cranelift/isle/veri/setup/download-cache.sh
+++ b/cranelift/isle/veri/setup/download-cache.sh
@@ -5,8 +5,9 @@
 # cranelift/isle/veri/cache, so a local run of verify.sh starts from the same
 # state CI is currently using.
 #
-# The `dev` release is refreshed on runs landing on `main` by the
-# "ISLE verifier full check" CI job (see .github/workflows/main.yml).
+# The `dev` release asset is refreshed by the `publish-artifacts.yml`
+# workflow from the "ISLE verifier full check" CI job's artifact (see
+# .github/workflows/main.yml).
 #
 # Usage:
 #   ./cranelift/isle/veri/setup/download-cache.sh
diff --git a/cranelift/isle/veri/verify.sh b/cranelift/isle/veri/verify.sh
index dd7e77c2ada3..66ff9c460848 100755
--- a/cranelift/isle/veri/verify.sh
+++ b/cranelift/isle/veri/verify.sh
@@ -3,13 +3,15 @@
 # Driver for VeriISLE verification with the SMT query cache.
 #
 # The cache lives locally at cranelift/isle/veri/cache (gitignored). CI
-# refreshes the cache on runs that land on main and publishes it as
-# isle-veri-cache.tar.gz on the `dev` release (see the isle_veri_full_check
-# job in .github/workflows/main.yml); local users can download it with
-# setup/download-cache.sh.
+# (the isle_veri_full_check job in .github/workflows/main.yml) verifies on
+# top of the shared entry in the GitHub Actions cache (keyed by a hash of
+# the ISLE sources and toolchain) and also uploads the rebuilt cache as a
+# run artifact, which the publish-artifacts.yml workflow publishes as
+# isle-veri-cache.tar.gz on the `dev` release when the run lands on main,
+# for local use. Local users can download it with setup/download-cache.sh.
 #
 # Usage:
-#   ./cranelift/isle/veri/verify.sh [MODE]
+#   ./cranelift/isle/veri/verify.sh [MODE] [CONFIG ...]
 #
 # Modes:
 #   cache-only     Verify purely from the local cache, in read-only, enforcing
@@ -27,16 +29,30 @@
 #                  Serves cached results where possible and invokes the solver
 #                  on misses, writing new entries back to the cache.
 #
+# CONFIG names (without the .args suffix) optionally select the
+# configurations to run from cranelift/isle/veri/configs/; the default is
+# CONFIGS below.
+
 set -euo pipefail
 cd "$(git rev-parse --show-toplevel)"
 
 MODE="${1:-local}"
+shift || true
 
 CACHE_DIR="cranelift/isle/veri/cache"
+# The default set of configurations to verify.
 CONFIGS=(
     cranelift/isle/veri/configs/aarch64.args
     cranelift/isle/veri/configs/x64-iadd-base-case.args
 )
+# CI passes its own list (see the isle_veri_full_check job in
+# .github/workflows/main.yml).
+if [ $# -gt 0 ]; then
+    CONFIGS=()
+    for name in "$@"; do
+        CONFIGS+=("cranelift/isle/veri/configs/${name}.args")
+    done
+fi
 
 # Run the verifier for every configuration, forwarding the given cache flags.
 run_all() {
@@ -96,8 +112,9 @@ local | "")
     ;;
 
 *)
-    echo "usage: $0 [cache-only | rebuild-cache]" >&2
+    echo "usage: $0 [cache-only | rebuild-cache] [CONFIG ...]" >&2
     echo "       (no argument runs a local, in-place read-write verification)" >&2
+    echo "       (CONFIG names are .args files in cranelift/isle/veri/configs/)" >&2
     exit 1
     ;;
 esac

From 38af68b67aa56a80d6ed08ce182ca4c273baccdf Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Wed, 26 Aug 2026 16:10:02 -0700
Subject: [PATCH 4/7] actually only run fast cases

---
 .github/workflows/main.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 9d052c51c637..e8e24dc91fb3 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1437,7 +1437,7 @@ jobs:
     - name: Verify and rebuild cache
       run: |
         mkdir -p cranelift/isle/veri/cache
-        ./cranelift/isle/veri/verify.sh rebuild-cache aarch64-fast aarch64 opt-fast opt x64-iadd-base-case
+        ./cranelift/isle/veri/verify.sh rebuild-cache aarch64-fast opt-fast x64-iadd-base-case
     - name: Package rebuilt cache
       run: tar czf isle-veri-cache.tar.gz -C cranelift/isle/veri cache
     - name: Upload cache tarball as run artifact

From 7762be2ab887cd3314f7053f5abf9e9ddf60af5b Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Wed, 26 Aug 2026 16:12:16 -0700
Subject: [PATCH 5/7] Add per-SMT-query timeout of 2 minutes as well.

---
 .github/workflows/main.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e8e24dc91fb3..e5b11395be33 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1435,6 +1435,10 @@ jobs:
         restore-keys: |
           isle-veri-cache-v1-
     - name: Verify and rebuild cache
+      env:
+        # Per-SMT-query timeout, in seconds (see the `--timeout` option in
+        # cranelift/isle/veri/veri/src/bin/veri.rs).
+        ISLE_VERI_TIMEOUT: "120"
       run: |
         mkdir -p cranelift/isle/veri/cache
         ./cranelift/isle/veri/verify.sh rebuild-cache aarch64-fast opt-fast x64-iadd-base-case

From 4cd79c206402e9ed16265f0c8baa7accb7bd0f42 Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Wed, 26 Aug 2026 16:32:33 -0700
Subject: [PATCH 6/7] Review feedback.

---
 .github/workflows/main.yml | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index e5b11395be33..e32fbb365087 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1379,7 +1379,7 @@ jobs:
   # is fast when the cache is warm and can take a long time when it is cold.
   #
   # The cache is a named entry in the actions cache, keyed by a hash of the
-  # ISLE sources and the ISLE toolchain (see the "Compute ISLE hash" step).
+  # ISLE sources and the ISLE toolchain (see `hashFiles` in the cache key).
   # Caches saved by merge-queue runs are stored in the default branch's
   # cache scope and are visible to every PR and future merge-queue run, so
   # each distinct ISLE state gets exactly one immutable entry on `main`, and
@@ -1417,21 +1417,14 @@ jobs:
         ./cranelift/isle/veri/setup/install-z3.sh -b "${solver_dir}/bin"
     - name: Add solvers to PATH
       run: echo "$HOME/.cache/smt-solvers/bin" >> "${GITHUB_PATH}"
-    - name: Compute ISLE hash
-      id: isle-hash
-      run: |
-        # Hash of the ISLE sources and the ISLE toolchain itself: list the
-        # cranelift/isle/**/*.rs and cranelift/codegen/**/*.isle files,
-        # sort the file list, hash each file individually (path and
-        # content), then hash the resulting manifest.
-        files=$(git ls-files 'cranelift/isle/**/*.rs' 'cranelift/codegen/**/*.isle' | LC_ALL=C sort -u)
-        echo "hash=$(printf '%s\n' "$files" | xargs -r -d '\n' sha256sum | sha256sum | cut -c1-32)" >> "$GITHUB_OUTPUT"
     - name: Restore and save verifier cache
       uses: actions/cache@v5
       with:
         path: cranelift/isle/veri/cache
-        # Bump `v1` if the cache format changes.
-        key: isle-veri-cache-v1-${{ steps.isle-hash.outputs.hash }}
+        # Bump `v1` if the cache format changes. `hashFiles` covers the ISLE
+        # sources and the ISLE toolchain itself by hashing the paths and
+        # contents of all matching files.
+        key: isle-veri-cache-v1-${{ hashFiles('cranelift/isle/**/*.rs', 'cranelift/codegen/**/*.isle') }}
         restore-keys: |
           isle-veri-cache-v1-
     - name: Verify and rebuild cache

From c975cdf9b45a2e8f3659209b5122e8d2762848f1 Mon Sep 17 00:00:00 2001
From: Chris Fallin <chris@cfallin.org>
Date: Wed, 26 Aug 2026 16:35:57 -0700
Subject: [PATCH 7/7] Review feedback.

---
 .github/workflows/publish-artifacts.yml | 6 ------
 ci/merge-artifacts.sh                   | 5 +++++
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/publish-artifacts.yml b/.github/workflows/publish-artifacts.yml
index 65e43beb4f41..2c244e6e9dca 100644
--- a/.github/workflows/publish-artifacts.yml
+++ b/.github/workflows/publish-artifacts.yml
@@ -46,12 +46,6 @@ jobs:
           git push origin dev:dev -f
           gh release create dev --prerelease dist/* ||
             gh release upload dev --clobber dist/*
-          # Refresh the ISLE verifier's shared SMT query cache (see the
-          # isle_veri_full_check job in main.yml), if the CI run produced
-          # one (the job is skipped for runs where the verifier didn't run).
-          if [ -f isle-veri-cache/isle-veri-cache.tar.gz ]; then
-            gh release upload dev --clobber isle-veri-cache/isle-veri-cache.tar.gz
-          fi
       env:
         GH_TOKEN: ${{ github.token }}
 
diff --git a/ci/merge-artifacts.sh b/ci/merge-artifacts.sh
index 57200c0f6af1..1cc0c35245f5 100755
--- a/ci/merge-artifacts.sh
+++ b/ci/merge-artifacts.sh
@@ -52,3 +52,8 @@ done
 
 # Copy over remaining source tarball into the dist folder
 mv -t dist bins-*/*.tar.*
+
+# Also move the ISLE verifier's SMT query cache, if present, into `dist/`.
+if [ -f isle-veri-cache/isle-veri-cache.tar.gz ]; then
+  mv isle-veri-cache/isle-veri-cache.tar.gz dist/
+fi