wasmtime / PR #13929 Cranelift verifier: run in CI, using... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / PR #13929 Cranelift verifier: run in CI, using...

Wasmtime GitHub notifications bot (Jul 21 2026 at 23:35):

cfallin opened PR #13929 from cfallin:isle-veri-in-ci to bytecodealliance:main:

Implement a file-based cache for SMT solver queries in the Cranelift verifier, enabling fast re-verification without re-invoking the solver.

The cache is keyed on a hash of the full SMT-LIB transcript for a query, and provides the response (unsat or sat + the model). It can be configured in two ways:

Read-write cache: use the result on hit, invoke the solver and populate the cache on a miss. Meant for local usage.

Read-only enforcing cache: use results on a hit, or fail verification on a miss. This is meant to run in CI.

The intended workflow is to check in the cache into git; this enables CI to run with cached responses rather than re-invoke the solver on every CI run. This sidesteps the issue of long-running queries to the solver; we can reverify our verification on every commit.

One might reasonably ask: what is the TCB and what is the ground truth against which we're verifying, if the repo contains effectively a cache of "yes, it's verified"?

The point is that we re-run the full tool against the current source; this reduces "verify Cranelift" to "evaluate these SMT queries". We then trust that our checked-in SMT query results are valid, but only that and nothing more. If we ever change the source in a way that causes a new instruction lowering path to exist, the tool will attempt to verify this against the cache and (presumably) fail.

The idea is then that the local developer does the verification, and checks in the "SMT query witness"; we either trust that, for regular contributors, or we re-run the verification ourselves, for anonymous contributors. We also have the option of re-regenerating the cache (i.e., re-running verification from scratch) whenever we want.

This commits all the query results that we should need to verify what is in-tree, also, and adds the job to CI. There is still some compute in generation of the queries, but locally (on my 16-core Ryzen 9950X) the full AArch64 backend verification completes in 27 seconds.

Wasmtime GitHub notifications bot (Jul 21 2026 at 23:35):

cfallin requested alexcrichton for a review on PR #13929.

Wasmtime GitHub notifications bot (Jul 21 2026 at 23:35):

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

Wasmtime GitHub notifications bot (Jul 21 2026 at 23:35):

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

Wasmtime GitHub notifications bot (Jul 21 2026 at 23:35):

cfallin commented on PR #13929:

cc @avanhatt @mmcloughlin

Wasmtime GitHub notifications bot (Jul 22 2026 at 01:09):

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

Wasmtime GitHub notifications bot (Jul 22 2026 at 01:09):

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

Wasmtime GitHub notifications bot (Jul 22 2026 at 01:10):

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

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:

cfallin: isle

fitzgen: isle

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

Learn more.
</details>

Wasmtime GitHub notifications bot (Jul 22 2026 at 01:44):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 22 2026 at 14:19):

:memo: avanhatt submitted PR review:

Woo!

Have a few initial comments. Could you also add a description (similar to the PR description) to cranelift/isle/veri/README.md?

Will also test locally and report back.

Wasmtime GitHub notifications bot (Jul 22 2026 at 14:19):

:speech_balloon: avanhatt created PR review comment:

What's the reasoning for this unused argument?

Wasmtime GitHub notifications bot (Jul 22 2026 at 14:19):

:speech_balloon: avanhatt created PR review comment:

To be more specific: "the ISLE files for the backends".

This does bring to mind one slight risk here: someone could change the Rust implementation of an external extractor/constructor and not have any indication that they need to change the spec. As it stands, this would still require a manual change to the corresponding spec anyway, but just a case to look out for.

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:26):

:memo: bjorn3 submitted PR review.

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:26):

:speech_balloon: bjorn3 created PR review comment:

I think this should be omitted to allow reproducing these cache files.

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:26):

:memo: bjorn3 submitted PR review.

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:26):

:speech_balloon: bjorn3 created PR review comment:

Why duplicate this?

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:27):

bjorn3 commented on PR #13929:

How will unused files to be GCed?

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:27):

bjorn3 edited a comment on PR #13929:

How will outdated files be GCed?

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:30):

:memo: avanhatt submitted PR review.

Wasmtime GitHub notifications bot (Jul 22 2026 at 16:30):

:speech_balloon: avanhatt created PR review comment:

This is currently superset of aarch64-fast.args, so we shouldn't need to run both

Wasmtime GitHub notifications bot (Jul 22 2026 at 18:16):

alexcrichton commented on PR #13929:

Personally I think infrastructure-wise it would be best to invest in some storage for this cache outside of the git-tracked state of this repo. I mentioned this in the cranelift meeting earlier today but I'm concerned about adding another ~1000 generated files to the repo, the weight of the generated files (77M right now locally), churn (up to +77M of diff if hashes change, huge PRs to sift through, etc), and the required changes to handle contributors PRs (vets are already a pain enough as-is I'd rather not add a second vector of "you can't land this until a maintainer pushes a thing to your branch"). I don't know what the best alternative would be, though, as I'm not entirely sure what the experience will be running this (e.g. how frequent, how difficult, etc). One thing I'd like to preserve though is to ideally continue to have contribution of new rules by contributors be pretty low friction -- if adding a new optimization/lowering rule (e.g. https://github.com/bytecodealliance/wasmtime/pull/13640) is blocked until verification is 100% working we'll probably basically not get outside contributions to the backend would be my guess.

For CI we could use a github-actions cache, but that's not easily downloadable by users to verify it themselves. One possible idea is a separate git repo pulled in as a submodule, but that doesn't really help with download size. Another possible option is a separate repo but manually managed (not via submodules) but instead by the verification script/etc. That could then be auto-updated in CI and/or by us.

Before brainstorming too much I'd like to get agreement on "yes this is in-repo" or "no, this is not in-repo" first. I'd personally like to push this to be outside, but if you'd like to push to instead put this inside I'd like to work through that first.

Wasmtime GitHub notifications bot (Jul 22 2026 at 18:36):

cfallin commented on PR #13929:

Thanks for your perspective on this! A few thoughts (some repeated from this morning's meeting, but for purposes of wider visibility in the discussion):

I think the highest-order bit for decisionmaking is this: "f adding a new optimization/lowering rule (e.g. https://github.com/bytecodealliance/wasmtime/pull/13640) is blocked until verification is 100% working we'll probably basically not get outside contributions to the backend would be my guess." That's more or less the point of putting verification in CI: the backends stay verified. We've talked a bunch in our verification sub-meeting about the expected developer experience here, and noted that we'll probably need to keep investing in tooling. But if we don't put a blocking check in CI, then we essentially give up on the rolling verification project, because no one will have the incentive to come back later and verify new bits that have been added. I'll note that one of our recent CVEs in the aarch64 backend would have been caught by verification, but wasn't, because we had only verified a snapshot of the backend and hadn't stayed up-to-date.

So I do think it is worth making this a blocking check, and then working through any friction we see. One of the design aspects of the approach is that it tries to automate/infer as much as possible, e.g. via "rule chaining" -- so adding a new lowering rule may just work, because we already have the semantics defined on both sides (CLIF and machine instructions). Or one may need to engineer things a bit more. There is a possibility of growing pains but again, if we don't do this, we are essentially giving up the most important part of verification, namely that the software that we ship (not an earlier snapshot) is verified.

Part of the motivation for putting the cache in-tree (or, otherwise having it somehow accessible/downloadable to the end-developer) is exactly the new-developer experience. If we don't have this, then any given verification run ("I added one rule, let me verify it") needs to do hours of SMT queries, or needs careful, manual subsetting of the local run -- which goes against the "easy for newcomers" goal.

I too am wary of diff-churn, but note that the way that this cache is structured, it's a content-addressable store: files are named by hash, so there will never (absent an actual SHA-2 hash collision) be a merge conflict or diff to an existing file. It's always new files.

The world where we don't have a full cache somewhere that CI can run off of (in an "enforcing" mode) is one where we need to run solvers in CI, and that results in potentially very long runtimes. I don't think that's tenable.

And to avoid that, we need to ensure the cache is complete, which again comes back to the "blocking check" bit above: we need to enforce that everything passes, with checked-in cache, for the CI checks to remain fast.

Wasmtime GitHub notifications bot (Jul 22 2026 at 18:48):

cfallin edited a comment on PR #13929:

Thanks for your perspective on this! A few thoughts (some repeated from this morning's meeting, but for purposes of wider visibility in the discussion):

I think the highest-order bit for decisionmaking is this: "if adding a new optimization/lowering rule (e.g. https://github.com/bytecodealliance/wasmtime/pull/13640) is blocked until verification is 100% working we'll probably basically not get outside contributions to the backend would be my guess." That's more or less the point of putting verification in CI: the backends stay verified. We've talked a bunch in our verification sub-meeting about the expected developer experience here, and noted that we'll probably need to keep investing in tooling. But if we don't put a blocking check in CI, then we essentially give up on the rolling verification project, because no one will have the incentive to come back later and verify new bits that have been added. I'll note that one of our recent CVEs in the aarch64 backend would have been caught by verification, but wasn't, because we had only verified a snapshot of the backend and hadn't stayed up-to-date.

So I do think it is worth making this a blocking check, and then working through any friction we see. One of the design aspects of the approach is that it tries to automate/infer as much as possible, e.g. via "rule chaining" -- so adding a new lowering rule may just work, because we already have the semantics defined on both sides (CLIF and machine instructions). Or one may need to engineer things a bit more. There is a possibility of growing pains but again, if we don't do this, we are essentially giving up the most important part of verification, namely that the software that we ship (not an earlier snapshot) is verified.

Part of the motivation for putting the cache in-tree (or, otherwise having it somehow accessible/downloadable to the end-developer) is exactly the new-developer experience. If we don't have this, then any given verification run ("I added one rule, let me verify it") needs to do hours of SMT queries, or needs careful, manual subsetting of the local run -- which goes against the "easy for newcomers" goal.

I too am wary of diff-churn, but note that the way that this cache is structured, it's a content-addressable store: files are named by hash, so there will never (absent an actual SHA-2 hash collision) be a merge conflict or diff to an existing file. It's always new files.

The world where we don't have a full cache somewhere that CI can run off of (in an "enforcing" mode) is one where we need to run solvers in CI, and that results in potentially very long runtimes. I don't think that's tenable.

And to avoid that, we need to ensure the cache is complete, which again comes back to the "blocking check" bit above: we need to enforce that everything passes, with checked-in cache, for the CI checks to remain fast.

Wasmtime GitHub notifications bot (Jul 22 2026 at 19:29):

avanhatt commented on PR #13929:

Also to @alexcrichton 's point about rule additions by new contributors: if the rule is truly outside of the scope of the verification's "default excludes" (e.g., what we think is most likely to cause CVEs), it's a ~1 line addition for the contributor to mark it as such and then quiet any cache miss/failure.

For example, it looks like the PR you link would pass just by tagging the new term as vector, e.g.,
(attr sdot (tag vector))

Wasmtime GitHub notifications bot (Jul 22 2026 at 19:31):

mmcloughlin commented on PR #13929:

Thanks for working on this! It should be a massive usability improvement.

I have not done a full review, but I wanted to raise some high-level questions first.

Generic SMT Caching Wrapper. This design tightly integrates the cache with the verifier. When I imagined building this feature, what I had in mind was an SMT-proxy binary that would wrap an SMT solver call and add a caching layer. Ideally this would be transparent to the verifier, only requiring a change to the command-line it uses for the backend solver. Theoretically, it would be a reusable component that could slot into any SMT-backed project (though I doubt we'd actually want to go that far).

I think this might actually be doable. The challenge at the moment is solver statefulness: the wrapper would need to proxy stdin and understand push/pop/check-sat etc.

A variant of this approach is to modify the verifier to render the full SMT query instead of using the solver interactively and dynamically branching on the applicability-check result. I think this may be doable too, though I'd need to think it through a bit more. The advantage here is your SMT wrapper becomes somewhat trivial, it's essentially a hash of the full input SMT file and returns a cached response.

So I think the possible alternatives might be a generic SMT caching proxy that's either (a) stateful and handles interactive SMT queries or (b) stateless and handles only full SMT files.

Cache Location and Size. I tend to agree with @alexcrichton that ideally a cache of this size wouldn't be in the main git repository. It seems that a separate git repository for the cache would avoid the downsides of adding it to the main repository whilst also being usable for new contributors?

However, this may be less of an issue if we could address the size. Is most of it coming from smt2_text? I may have missed something but it looks like the field is read-only in this code. For example, the cache lookup relies entirely on the SHA256 hash.

https://github.com/cfallin/wasmtime/blob/5cbfb8f093b9808b6d1664b4a3610bb7a0b6994a/cranelift/isle/veri/veri/src/cache.rs#L159-L191

Could we drop the SMT2 text field and save a load of cache space?

Churn. It might be a good idea for us to run some hypothetical workflows and confirm the cache helps in the way we expect. Maybe you have already? For example:

Small modification. Modifying a rule that we expect to have isolated effect, and confirm we get cache hits on almost everything else.

New rule. Add a new rule. Should also have high cache hit rate.

Modify something low-level. Expect mostly cache misses.

I think it should all work this way, but it would be good to validate, since the usability of the cache depends on it.

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:20):

:thumbs_up: fitzgen submitted PR review:

LGTM modulo nitpicks below

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:20):

:speech_balloon: fitzgen created PR review comment:

    #[serde(skip)]
    pub short_key: String,

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:20):

:speech_balloon: fitzgen created PR review comment:

I think all these custom methods to push to the transcript could use the existing https://docs.rs/easy-smt/latest/easy_smt/struct.ContextBuilder.html#method.replay_file functionality instead.

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:20):

:speech_balloon: fitzgen created PR review comment:

Can we add the following to .gitattributes in the root of the repo?
cranelift/isle/veri/cache/*.json -diff
That will hide their diffs in github and in the git cli

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:25):

fitzgen commented on PR #13929:

+1 for keeping the cache in tree. FWIW, we can hide diffs via https://github.com/bytecodealliance/wasmtime/pull/13929#discussion_r3633470635

Wasmtime GitHub notifications bot (Jul 22 2026 at 20:43):

mmcloughlin commented on PR #13929:

Including my Claude interactive review session summary below (collapsed) in case its useful. You'll see there the two points I already raised in https://github.com/bytecodealliance/wasmtime/pull/13929#issuecomment-5050568783

SMT Caching Layer, and a bunch of variants of that design.

Dropping SMT text field to reduce cache size.

It reports a few other claims that I haven't independently confirmed but we should look into:

Solver invoked regardless of caching mode? Have we run the CI job yet? Or just a local run where solvers are not installed?

Potential fragility of using the encoding as the cache key. It think this is technically valid point, but may be overly paranoid.

<details>
<summary>Robot Review</summary>

Review: wasmtime PR #13929 — "Cranelift verifier: run in CI, using an SMT query caching setup"

PR: <https://github.com/bytecodealliance/wasmtime/pull/13929> (author: cfallin, base main, head isle-veri-in-ci)

Head reviewed: 5cbfb8f093b9 ("clippy cleanups.")

Date: 2026-07-22

Scope: SMT query cache for the Cranelift ISLE verifier, checked into the repo, run in CI in read-only-enforcing mode.

This document records the review and the findings verified empirically against a local checkout at the PR head. All claims marked [verified] were reproduced by running the tool; [reasoned] are from code reading only.

1. What the PR does

Adds a file-based cache of SMT solver query results to the verifier:

Key = SHA-256 of "{solver_backend}\n{smt2_text}"; file cache/<first-12-hex>.json per entry.

Two modes: read-write (hit → use; miss → solve + store; local use) and read-only-enforcing (hit → use; miss → hard fail; CI use). There is also an off variant.

Intent: check the cache into git so CI re-runs the tool against source but trusts the checked-in query results instead of re-invoking the solver. New CI job isle_veri_check runs verify-cache.sh for aarch64-fast.args, aarch64.args, x64-iadd-base-case.args.

Non-cache source changed (the rest of the 713 files are cache JSON):

File Change

cranelift/isle/veri/veri/src/cache.rs +418 new — CacheStore, CacheEntry, modes, tests

cranelift/isle/veri/veri/src/solver.rs +147/-29 — transcript capture via send_and_capture

cranelift/isle/veri/veri/src/runner.rs +122/-5 — check/store orchestration

cranelift/isle/veri/veri/src/bin/veri.rs +34 — --cache-dir, --cache-mode

verify-cache.sh, update-cache.sh new — CI/local drivers

.github/workflows/main.yml +16 — isle_veri_check job

2. Overall assessment

The core idea is sound and valuable: reduce "verify Cranelift" to "evaluate a fixed set of SMT queries," commit the witnesses, and let CI re-run the tool while trusting the results. cache.rs is clean and tested; the read-write / read-only split is the right shape.

Three things stand out, in priority order:

The PR's central claim — "we do not run the SMT solver in CI" — is not true, and the CI job will fail when it runs. The solver is spawned and the full encode phase is round-tripped through it before the cache is consulted, and the CI job installs no solver. (§4.1)

The cache key is the encoding, not the query. It omits the actual check-sat queries (applicability + verification condition). Latent unsoundness; the collision channel that would trigger it is already active at ~0.6%. (§4.2)

The cache is ~200× larger on disk than it needs to be, because each entry stores the full SMT text that is never read back. (§4.3 / Q2)

Plus the deep coupling into solver.rs/runner.rs that Q1 is about (§Q1), and a set of smaller issues (§4.4).

Q1 — Separating the cache from the verifier

Where the coupling actually lives. cache.rs is nearly standalone already (only tie is the verifier's CacheVerdict). The deep coupling is elsewhere:

solver.rs: ~15 easy-smt convenience calls (set_logic, assert, declare_*, push, pop) hand-rewritten into explicit list(...) + send_and_capture, purely to capture a transcript. This re-implements easy-smt's own s-expression rendering and must be kept in lockstep with it — the most fragile part of the PR.

runner.rs: check-before-solve / store-after-solve threaded through verify_expansion_type_instantiation.

Option (a) — module/crate in cranelift/isle/veri/. Cheap and worth doing regardless: make CacheStore generic over the stored value (hash(bytes) → V: Serialize) and instantiate with the verifier's verdict. But this only relocates cache.rs; it does nothing about the real coupling in solver.rs/runner.rs. Least valuable on its own.

Option (b) — transparent SMT-proxy binary. The genuinely reusable primitive and the ideal end-state. easy-smt already talks to the solver as a subprocess over an SMT-LIB text pipe; SolverBackend::prog() is just the binary path. A proxy in that slot accumulates the active assertion context and, at each (check-sat), replays a cached response (if the active context hashes to a known key) or forwards to the real solver and records. Verifier changes reduce to "point --solver at the wrapper." Payoffs: deletes the solver.rs rewrite and the runner.rs orchestration; keys on the actual query bytes (fixes §4.2 for free); reusable by any project that shells out to z3/cvc5. Cost: solvers are stateful (push/pop, incremental asserts), so the proxy must track the assertion stack and key each check-sat on the flattened active context, and replay get-value to cache models. Tractable but the bulk of the work.

The "render the query script" middle path (recommended for this PR). Don't capture the transcript as a side effect of sending; render the query text deterministically from Conditions and hash that. Two shapes, both preserve the existing applicability→branch→VC control flow:

Design A — one key per task. Pure render_task_script(&Conditions, backend, dialect) emits, unconditionally, prelude + encode + (assert assumptions)(check-sat) + (assert (not (=> assumptions assertions)))(check-sat). It's a deterministic function of the task, never executed, only hashed. Before anything: render → hash → look up; hit → return cached verdict and spawn nothing; miss → run today's control flow and store. Minimal change; puts the assumptions/assertions partition into the key.

Design B — one key per query (proxy-shaped, preferred). Key each check-sat on its own rendered text and wrap each solver call:
let ak = hash(render_applicability_query(conditions, backend)); let applic = cache.get(ak).unwrap_or_else(|| { let v = solver.check_assumptions_feasibility(); cache.put(ak, v); v }); match applic { Inapplicable|Unknown => return, Applicable => {} } let vk = hash(render_vc_query(conditions, backend)); let verif = cache.get(vk).unwrap_or_else(|| { let v = solver.check_verification_condition(); cache.put(vk, v); v });
The branch structure is identical to today; each solver call just gains a cache wrapper. Each key is unambiguously the full query (sound + reproducible, no captured solver responses); sub-results are shared across tasks that agree on applicability; it's the in-process form of the proxy, so extracting (b) later is natural.

Decisive benefit of rendering over the current capture: because the key is computed from Conditions without touching the solver, a full-cache-hit run never spawns z3/cvc5 — which is what makes "no solver in CI" actually true and removes the CI-needs-a-solver problem (§4.1). It also lets the whole send_and_capture apparatus in solver.rs be deleted and those ~15 sites reverted to plain easy-smt calls.

Sync cost (rendered text must match what's sent): keep each renderer tiny and local to its check-sat (Design B) and guard with a debug-only assert comparing rendered text to a captured transcript, so drift is caught by tests.

Recommendation: Design B — it answers "how does the control flow adapt" (it doesn't; each solver call gets a cache wrapper), fixes §4.2, makes "no solver in CI" real, and is the migration path to the reusable proxy (b). Design A is the fallback if exactly one entry per task is preferred. Pure (a) alone leaves the real coupling in place.

Q2 — Storing the cache in the repo

Measured [verified] on the checked-in cache (cranelift/isle/veri/cache):

Metric Value

Total size 76 MB

Files 703

Per-entry size mean ~110 KB, median ~96 KB, max 648 KB

smt2_text share of a sampled entry 116,610 / 120,569 bytes ≈ 97%

gzip -9 of the whole dir 76 MB → 8.5 MB (~9×)

Decisive fact: smt2_text is never read back. CacheStore::lookup (cache.rs:159) compares only key_sha256; it never re-hashes smt2_text. So the stored text is not part of the trust chain — it's documentation, not data. Functionally the cache needs only { key → verdict }.

Options, most impactful first:

Drop smt2_text from stored entries. Keep key_sha256, verdict, timings. ~703 × a few hundred bytes ≈ 200–400 KB total (~200× smaller); per-change churn drops from ~100 KB/entry to a few hundred bytes. Essentially free, since the text is unused. If an audit trail of what was proven is wanted, keep it as a compressed sidecar, not inline in the hot cache.

Drop redundant fields. short_key = key_sha256[..12] = filename stem (bjorn3); solver_version is always null fro
[message truncated]

File	Change
`cranelift/isle/veri/veri/src/cache.rs`	+418 new — `CacheStore`, `CacheEntry`, modes, tests
`cranelift/isle/veri/veri/src/solver.rs`	+147/-29 — transcript capture via `send_and_capture`
`cranelift/isle/veri/veri/src/runner.rs`	+122/-5 — check/store orchestration
`cranelift/isle/veri/veri/src/bin/veri.rs`	+34 — `--cache-dir`, `--cache-mode`
`verify-cache.sh`, `update-cache.sh`	new — CI/local drivers
`.github/workflows/main.yml`	+16 — `isle_veri_check` job

Metric	Value
Total size	76 MB
Files	703
Per-entry size	mean ~110 KB, median ~96 KB, max 648 KB
`smt2_text` share of a sampled entry	116,610 / 120,569 bytes ≈ 97%
`gzip -9` of the whole dir	76 MB → 8.5 MB (~9×)

Wasmtime GitHub notifications bot (Jul 22 2026 at 21:18):

cfallin commented on PR #13929:

@mmcloughlin thanks for this; I will note however that our AI tool policy states that one should not post the direct outputs of LLMs without verifying, so "here is the robot's review that I haven't verified" is pretty directly not the sort of thing that we've decided is helpful. I know you mean well and you're not a drive-by contributor like most folks who run astray of that; just thought I should mention to set/remind norms we've decided on. Thanks!

(Thanks to all for the input above -- will refine+synthesize and post another comment about cache location and CI integration in a bit)

Wasmtime GitHub notifications bot (Jul 22 2026 at 21:28):

alexcrichton commented on PR #13929:

@cfallin, @avanhatt, @mmcloughlin, and I chatted a bit about this as well and I wanted to write down what we concluded (correct me if I'm wrong). The current thinking is that we'll model the primitive here as: there's a script which takes an input cache directory, runs full verification using that, then generates a new directory of all cache entries needed. This will take a bit of time for uncached queries but will unconditionally run full verification. This script will land first in this PR not hooked up to CI.

Next we'll hook this up to CI, notably creating a github actions artifact which is the output directory. This'll thread its way through our CI processes to get published in the dev release and all other releases as well. The final piece, making it so CI is not the slowest thing the world, will be fetching the previous cache results from some other run. This would, for example, fetch from the last-commit-to-main's workflow or the dev release or similar. This CI piece is expected to get integrated in a second PR

Wasmtime GitHub notifications bot (Jul 22 2026 at 22:00):

mmcloughlin commented on PR #13929:

@mmcloughlin thanks for this; I will note however that our AI tool policy states that one should not post the direct outputs of LLMs without verifying, so "here is the robot's review that I haven't verified" is pretty directly not the sort of thing that we've decided is helpful. I know you mean well and you're not a drive-by contributor like most folks who run astray of that; just thought I should mention to set/remind norms we've decided on. Thanks!

(Thanks to all for the input above -- will refine+synthesize and post another comment about cache location and CI integration in a bit)

Ah, apologies for that. My mistake for not being aware of the AI policy. I was trying to be reasonable by explicitly declaring and hiding the AI output in a <details> block, and adding my commentary on the points that I think worthy of attention.

Points 1 was my idea, I verified point 2. While not quite verified, I had thought through points 3 and 4 enough to think they were worth raising. Seeing the PR approval also made me think it might be worth raising potential issues sooner.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:10):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:13):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:14):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:14):

:speech_balloon: cfallin created PR review comment:

Removed, thanks!

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:19):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:19):

:speech_balloon: cfallin created PR review comment:

Removed.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:19):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:19):

:speech_balloon: cfallin created PR review comment:

No longer relevant (refactored away from this approach).

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:21):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:21):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:21):

:speech_balloon: cfallin created PR review comment:

Reworded, thanks.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:speech_balloon: cfallin created PR review comment:

Ah, great, wasn't sure -- removed (from verify.sh now post-refactor).

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:speech_balloon: cfallin created PR review comment:

(no longer relevant now that cache isn't in git)

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:22):

:speech_balloon: cfallin created PR review comment:

Removed entirely, cleaner still!

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:23):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:23):

:speech_balloon: cfallin created PR review comment:

Refactored to add a layer on top of easy-smt (will comment below), but the replay_file approach unfortunately isn't workable because the goal is to avoid spawning the solver at all until we know we have a miss; we'd have to start up a live easy-smt session to get the replay to compute the cache key.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:26):

cfallin commented on PR #13929:

OK, I've refactored this substantially since the last version. Per @mmcloughlin's thoughts I decided that indeed this is cleaner if there is a separate, coherent caching layer on top of easy-smt with an API that otherwise looks identical, so the veri crate has almost no diff now (imports the caching crate instead, sets it up; but API on the object is unchanged). The caching crate is new, and it computes cache keys based on the path down the tree implied by solver push/pops.

I've also reworked the driver and the shell script based on the discussion that Alexa, Michael, Alex and I had: mechanism to rebuild the cache into a new directory (addressing the cache-GC'ing concern), and no longer a CI job. I'll do the CI integration (consume artifact from latest dev, produce artifact with updated cache, and script for a local user to download it) in a followup PR.

Let me know what you think!

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:26):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 23 2026 at 21:54):

:thumbs_up: alexcrichton submitted PR review:

all sounds good to me high-level-wise, although I'd defer to @avanhatt or @mmcloughlin for review of the veri bits

Wasmtime GitHub notifications bot (Jul 23 2026 at 22:40):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 18:02):

:memo: mmcloughlin submitted PR review:

Thank you for making this change! I think the crate separation is cleaner.

I did try out an AI-assisted prototype of an independent SMT caching wrapper binary. At a high level it's quite similar to your approach, but with extra overhead of an SExpr/SMT parser. That would be worth it if we were trying to build a re-usable caching layer, but we're not.

I have left a comment about handling of timeouts and unknown responses. I'm not yet sure what the right answer is here.

Wasmtime GitHub notifications bot (Jul 24 2026 at 18:02):

:speech_balloon: mmcloughlin created PR review comment:

I'm wondering if we need more than just the solver name in the key? In particular, do we need all/part of the command-line?

The case I have in mind is unknown results due to a timeout. If you increase the timeout you don't want to be returned a cached unknown from a prior run with a lower timeout. But you probably do want the cached unsat results.

So as I write this, I'm thinking we probably need something more nuanced than using the command-line in the cache key. That would just cause 100% cache misses when you change a timeout. Instead, perhaps we do need the cache to be aware of timeouts/rlimits, or to treat unknowns specially.

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:28):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:30):

:memo: cfallin submitted PR review.

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:30):

:speech_balloon: cfallin created PR review comment:

Good point. In full generality, anything we change about the environment could cause a nondeterministic timeout to flip status: solver version, runner hardware, phase of the moon affecting the tides and thereby thermal properties of the atmosphere and thereby the clock speed at which those runners run, ...

In order to give us a lever to bulk-invalidate everything everywhere if we want to flush cached timeouts, I've added a static "version" counter here; we can bump it in a PR if we also change something else. The resulting CI run will repopulate the full cache.

We should also probably address the nondeterminism stemming from wallclock-related timeouts, as we talked about before -- happy to take a followup PR doing something with rlimits if you want to poke at that (I wouldn't know exactly how to configure or tune it properly)...

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:30):

cfallin has enabled auto merge for PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:33):

avanhatt commented on PR #13929:

Changes look good to me! I'll hold off on local testing until we have CI integration/local script. Agreed the rlimit change can come later, from one of us.

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:36):

cfallin added PR #13929 Cranelift verifier: run in CI, using an SMT query caching setup. to the merge queue

Wasmtime GitHub notifications bot (Jul 24 2026 at 21:55):

github-merge-queue[bot] removed PR #13929 Cranelift verifier: run in CI, using an SMT query caching setup. from the merge queue

Wasmtime GitHub notifications bot (Jul 24 2026 at 22:27):

cfallin updated PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 22:27):

cfallin has enabled auto merge for PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 22:36):

cfallin added PR #13929 Cranelift verifier: run in CI, using an SMT query caching setup. to the merge queue

Wasmtime GitHub notifications bot (Jul 24 2026 at 23:01):

:check: cfallin merged PR #13929.

Wasmtime GitHub notifications bot (Jul 24 2026 at 23:01):

cfallin removed PR #13929 Cranelift verifier: run in CI, using an SMT query caching setup. from the merge queue

Last updated: Jul 29 2026 at 05:03 UTC