Stream: git-wasmtime

Topic: wasmtime / PR #14207 CI: run the Cranelift verifier.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:14):

cfallin opened PR #14207 from cfallin:verification-in-ci to bytecodealliance:main:

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.

Note that the cache needs a unique key per run on main, because a cache entry is immutable once
created. Fortunately we can select the latest key by prefix.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:14):

cfallin requested alexcrichton for a review on PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:14):

cfallin requested wasmtime-compiler-reviewers for a review on PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:14):

cfallin requested wasmtime-default-reviewers for a review on PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:14):

cfallin commented on PR #14207:

cc @avanhatt @mmcloughlin

Let's see how long the run takes on the branch...

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:18):

cfallin commented on PR #14207:

Hmm, it seems that new workflows don't run until merge to main -- do I need to merge PRs as part of a debug loop?! That's awfully silly... (good security reasons for this I suppose but still)

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:23):

avanhatt commented on PR #14207:

@cfallin it seems like you can manually trigger without merging to main https://docs.github.com/en/actions/how-tos/manage-workflow-runs/approve-runs-from-forks

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 19:32):

cfallin commented on PR #14207:

Unfortunately it seems there is no "Approve workflows to run" option, at least for me. I wonder if the set of workflows is somehow fixed based on what is in main so an entirely new workflow isn't picked up... @alexcrichton let us know if there's a better way to test, here!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 20:24):

:memo: alexcrichton submitted PR review:

If it works I'd recommend moving this to main.yml because otherwise we need to reconfigure repository settings to actually gate on this check where if it's in main.yml we can just manage it via the text configuration there.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 20:24):

:speech_balloon: alexcrichton created PR review comment:

I think you'll need to specify branches here like with main.yml to get this to run on this PR

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 20:24):

:speech_balloon: alexcrichton created PR review comment:

This is currently missing merge_group as-is which means that this won't run as part of the merge queue

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 21:50):

github-actions[bot] added the label isle on PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 21:50):

github-actions[bot] added the label cranelift on PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 21:51):

github-actions[bot] commented on PR #14207:

Subscribe to Label Action

cc @cfallin, @fitzgen

<details>
This issue or pull request has been labeled: "cranelift", "isle"

Thus the following users have been cc'd because of the following labels:

To subscribe or unsubscribe from this label, edit the <code>.github/subscribe-to-label.json</code> configuration file.

Learn more.
</details>

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 23:15):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 23:16):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 23:19):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 25 2026 at 23:20):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 03:26):

cfallin commented on PR #14207:

Cool, the job finishes in 3h58m on a GitHub runner. That's definitely longer than I would have hoped for, but as long as the cache isn't dropped or mass-invalidated by some change it should be OK? (We should merge when the merge queue is otherwise quiet of course...)

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 03:32):

avanhatt commented on PR #14207:

Woo! :tada:

A few things:

  1. It looks like for aarch64, 54 instantiations result in unknown for this timeout/these runners. We may be okay with that, but at that point, we may also want to think about running the fast config that skips known-slow/more likely to be unknown queries? Would also reduce the runtime.
  2. Did we also want to verify the covered midend rules in this PR? Looks like from the logs this did a full aarch64 and the sanity-check x64 expansions, but not opt.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:11):

avanhatt commented on PR #14207:

Also re: the merge queue, it runs a superset of tests; you can run all for a commit by including prtest:full in the commit string.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:11):

avanhatt deleted a comment on PR #14207:

Also re: the merge queue, it runs a superset of tests; you can run all for a commit by including prtest:full in the commit string.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:34):

:memo: alexcrichton submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:34):

:speech_balloon: alexcrichton created PR review comment:

In CI this step took 3 seconds, so perhaps overkill to cache this step? Are you worried about flaky installation though?

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:34):

:speech_balloon: alexcrichton created PR review comment:

This should happen through the publish-artifacts.yml workflow which is already responsible for uploading artifacts. For example all artifacts from the commit are downloaded here, shuffled around here, and uploaded here.

There's custom handling of the gh-pages artifact and you can shuffle aruond isle-veri-cache.tar.gz in that workflow.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:34):

:speech_balloon: alexcrichton created PR review comment:

Could this use actions/cache to auto restore/save? I commented below but I don't believe there's any need to conditionally save.

Additionally, instead of using github.run_id could the key be a hash of input files? For example maybe the veri source code and aarch64 ISLE? That way when nothing is changing we're not making more caches.

Also, does the cvc5/z3 version need to be factored into this cache key?

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:34):

:speech_balloon: alexcrichton created PR review comment:

I think this should be removed and the cache should always be saved, and that way PRs can incrementally build up their own cache. PR caches aren't read by main and all workflow runs have a "branch base" where PRs are a different base than the main branch.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:39):

alexcrichton commented on PR #14207:

Oh, also, as-is this is going to run on every PR which while probably fine we perhaps want to tweak a bit to only run conditionally like we do for most other jobs. If you copy this configuration it'll only run with prtest:full or on the merge queue and if you copy this configuration there will be custom logic of when to trigger on PRs (found here.

do I need to merge PRs as part of a debug loop?! That's awfully silly...

I'll caution that this'll probably need an iteration or two of landing on main to fiddle with the logic around caching and the dev release and such. I agree it's unfortunate, but it's all we've got.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:49):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 14:49):

:speech_balloon: cfallin created PR review comment:

Oh, no, I was just worried it would take longer (and didn't have numbers until actually creating the PR). I can remove the caching step here.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:06):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:08):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:09):

:speech_balloon: cfallin created PR review comment:

Done!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:09):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:09):

:speech_balloon: cfallin created PR review comment:

Ah, yes, done!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:09):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:09):

:speech_balloon: cfallin created PR review comment:

Done!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:10):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:12):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:18):

:speech_balloon: alexcrichton created PR review comment:

Oh sorry, but for this I meant the built-in hashFiles function which I think should subsume this

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:18):

:speech_balloon: alexcrichton created PR review comment:

I think this always produced as this is always run, so the conditional logic here may not be necessary? You could also, in a prior step, move it into the dist/ directory to get auto-uploaded by the previous glob to cut this down a bit.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:18):

:thumbs_up: alexcrichton submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:36):

cfallin updated PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:36):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:36):

:speech_balloon: cfallin created PR review comment:

Done -- added to ci/merge-artifacts.sh instead.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:36):

:memo: cfallin submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:36):

:speech_balloon: cfallin created PR review comment:

Ah, that's much easier!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 26 2026 at 23:43):

cfallin commented on PR #14207:

OK, switching to the aarch64-fast config got the run down to 18 minutes, which is great!

view this post on Zulip Wasmtime GitHub notifications bot (Aug 27 2026 at 16:16):

cfallin added PR #14207 CI: run the Cranelift verifier. to the merge queue

view this post on Zulip Wasmtime GitHub notifications bot (Aug 27 2026 at 16:41):

:check: cfallin merged PR #14207.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 27 2026 at 16:41):

cfallin removed PR #14207 CI: run the Cranelift verifier. from the merge queue

view this post on Zulip Wasmtime GitHub notifications bot (Aug 27 2026 at 17:25):

alexcrichton commented on PR #14207:

I see the asset on the dev release so looks like that's going well, @cfallin wanna double-check the download script pulls that for local development?

view this post on Zulip Wasmtime GitHub notifications bot (Aug 27 2026 at 19:01):

cfallin commented on PR #14207:

I see the asset on the dev release so looks like that's going well, @cfallin wanna double-check the download script pulls that for local development?

Yes, the download worked and verification from cache-only worked as well!

$ cranelift/isle/veri/setup/download-cache.sh
############################################################################################################################################################################################################### 100.0%
Installed verifier cache to cranelift/isle/veri/cache/
You can now run ./cranelift/isle/veri/verify.sh (or cache-only / rebuild-cache).

$ time cranelift/isle/veri/verify.sh cache-only aarch64-fast
=== Verifying from cache (read-only, enforcing; no solver) ===
=== veri: cranelift/isle/veri/configs/aarch64-fast.args ===
    Finished `release` profile [optimized] target(s) in 0.07s
     Running `target/release/veri --config cranelift/isle/veri/configs/aarch64-fast.args --cache-source-dir cranelift/isle/veri/cache --cache-mode read-only-enforcing`
[ ... ]
Verification passed: 523
Verification failed: 0
Verification unknown: 0
===============================================================================
========================== Cache statistics ===========================
Mode:            read-only-enforcing
Source:          cranelift/isle/veri/cache
Destination:     (none)
Hits:            1219 (100.0%)
Misses:          0 (0.0%)
New entries:     0
Retained:        0
========================================================================
=== Cache verification passed ===
cranelift/isle/veri/verify.sh cache-only aarch64-fast  6.28s user 1.08s system 324% cpu 2.264 total

view this post on Zulip Wasmtime GitHub notifications bot (Aug 28 2026 at 13:53):

avanhatt commented on PR #14207:

OK, switching to the aarch64-fast config got the run down to 18 minutes, which is great!

This is great!

I did think our conclusion from the last verification meeting was that it was worth it to run the full config with a lower timeout, since even the slow tagged queries tend to fail fast if actually unsound despite normally returning unknown with a lower timeout. With this PR being that in the aarch64-fast mode, the slow tagged queries are just skipped.

I'm running a local check to see how long our slowest-completing fast query completes, then we can use that to try and go back to the full config with a timeout just above that? If that sounds reasonable @cfallin.

view this post on Zulip Wasmtime GitHub notifications bot (Aug 28 2026 at 14:10):

cfallin commented on PR #14207:

I did think our conclusion from the last verification meeting was that it was worth it to run the full config with a lower timeout, since even the slow tagged queries tend to fail fast if actually unsound despite normally returning unknown with a lower timeout. With this PR being that in the aarch64-fast mode, the slow tagged queries are just skipped.

Ah, sorry, I was just going down the list of feedback from above but I guess didn't account for updates to the consensus after your initial comment / forgot we had concluded differently. I'm happy to review a PR that bumps to the full config (s/aarch64-fast/aarch64/ in the CI is all it takes I guess?). We'd even benefit from the cache on all but the new (currently excluded) queries!

Last updated: Aug 30 2026 at 09:07 UTC