Cranelift verifier: run in CI, using an SMT query caching setup.

[cfallin]

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.

[cfallin]

cc @avanhatt @mmcloughlin

[github-actions]

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 .github/subscribe-to-label.json configuration file.

Learn more.

[avanhatt]

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.

[avanhatt]

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.

[avanhatt]

What's the reasoning for this unused argument?

[bjorn3]

Why duplicate this?

[bjorn3]

How will outdated files be GCed?

[avanhatt]

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

[alexcrichton]

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. #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.

[cfallin]

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. cranelift(aarch64): lower the i8 relaxed dot product to NEON SDOT #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.

[avanhatt]

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))

[mmcloughlin]

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:

1. Small modification. Modifying a rule that we expect to have isolated effect, and confirm we get cache hits on almost everything else.
2. New rule. Add a new rule. Should also have high cache hit rate.
3. 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.

[fitzgen]

LGTM modulo nitpicks below

[fitzgen]

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

[fitzgen]

Suggested change

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

[fitzgen]

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.

[fitzgen]

+1 for keeping the cache in tree. FWIW, we can hide diffs via #13929 (comment)

[mmcloughlin]

Including my Claude interactive review session summary below (collapsed) in case its useful. You'll see there the two points I already raised in #13929 (comment)

1. SMT Caching Layer, and a bunch of variants of that design.
2. 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:

3. Solver invoked regardless of caching mode? Have we run the CI job yet? Or just a local run where solvers are not installed?
4. Potential fragility of using the encoding as the cache key. It think this is technically valid point, but may be overly paranoid.

Robot Review

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

• PR: Cranelift verifier: run in CI, using an SMT query caching setup. #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:

1. 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)
2. 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)
3. 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:

1. 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.
2. Drop redundant fields. short_key = key_sha256[..12] = filename stem (bjorn3); solver_version is always null from the writer (bjorn3). Also strip the ;; response: success lines from the key material (they couple the key to solver output and hurt reproducibility — bjorn3).
3. Store as one file, not 703. 703 loose files are the source of the git pain (index bloat, per-file blame, slow checkout/status, noisy diffs, no .gitattributes). A single JSONL/CBOR of verdict records diffs cleanly and needs no linguist marking. With smt2_text gone it's tiny.
4. Compression is a fallback, not the fix. 9× is far worse than the ~200× from (1) and hurts diffability. Only relevant if the full text is kept anyway; then store it as one zstd file.

Churn / GC (bjorn3's "how will outdated files be GCed?"): update-cache.sh is purely additive and nothing prunes, so every encoding change orphans old entries and the dir grows monotonically. Fixes: (a) have the read-only-enforcing run emit the set of keys it actually hit, and a prune step delete the rest; and/or (b) make update-cache.sh clear the dir before regenerating. Cheap once entries are verdict-only.

Where else could it live? The in-repo-witness choice is deliberate and good — self-contained, fork-friendly, offline, no external trust boundary or infra — and worth keeping, provided it's verdict-only + single-file (hundreds of KB). Move out-of-repo only if that size ever becomes objectionable (it won't). For completeness: git-LFS (adds an LFS dep, complicates forks/CI, still "in repo"); actions/cache keyed on a source hash (not a durable witness — a cold cache forces the solver, defeating the point); a release-asset store fetched in CI (extra infra + new trust boundary). None fit the stated goals better than a small in-repo verdict file.

---

3. Empirical verification (receipts)

Local checkout at 5cbfb8f093b9; built with stable rustc 1.97.1; z3 4.12.2 and cvc5 available on PATH.

3.1 --cache-mode off panics [verified]

$ veri --config configs/x64-iadd-base-case.args --cache-dir <copy> --cache-mode off
Verification passed: 46
thread 'main' panicked at cranelift/isle/veri/veri/src/cache.rs:266:31:
internal error: entered unreachable code: should not print stats when cache is off
### exit status: 101 ###

off also serves hits and writes on miss (it only differs from read-write by the final panic).

3.2 Solver is spawned before the cache is checked [verified]

Running off/read-only-enforcing with PATH=/nonexistent fails every expansion with No such file or directory (os error 2) at solver spawn. Code: runner.rs:1194-1202 builds the easy-smt context and runs Solver::new + solver.encode() (thousands of send+recv round-trips); the cache is only consulted afterward at runner.rs:1210. With the solver on PATH, read-only-enforcing for x64-iadd passes (exit 0, 46/46, 1.83 s) — i.e. the solver was spawned and used for encoding; only check-sat was cached.

3.3 CI installs no solver, job is currently skipped [verified]

.github/actions/install-rust installs no z3/cvc5; the isle_veri_check job is only checkout + install-rust + verify-cache.sh. ubuntu-latest ships neither solver. PR check-runs show Cranelift ISLE verifier check: completed/skipped (gated on run-full), so it has not exercised this path yet.

3.4 Distinct tasks collide on the same key [verified]

The Hits counter during a from-empty read-write generation counts two different tasks producing the same key:

Config	Type instantiations	Distinct keys	Intra-run Hits (collisions)
x64-iadd-base-case	69	69	0
aarch64-fast	463	460	3 (~0.6%)

Verification is dispatched with par_iter() (runner.rs:688), so colliding tasks can run concurrently.

---

4. Findings

4.1 CI will fail / "no solver in CI" is inaccurate — high [verified]

The solver is spawned and the entire prelude+encode phase round-tripped through it before the cache is consulted (runner.rs:1194-1210); the CI job installs no solver (§3.2, §3.3). When isle_veri_check runs on run-full it will fail at solver spawn. The cache only skips check-sat reasoning, not the solver process. Fix: either install a solver in the job (contradicts the narrative and keeps encode overhead), or — better — compute the key from Conditions without the solver (Q1 render approach) so a full-hit run spawns nothing.

4.2 Cache key is the encoding, not the query — high / latent unsoundness [reasoned + partially verified]

The PR says the key is "a hash of the full SMT-LIB transcript for a query." The implementation keys on baseline = solver.take_baseline_transcript() taken right after encode() (runner.rs:1206); encode() only emits per-expression declare-const/(assert (= eN …)). The actual queries — applicability (assert (and assumptions))(check-sat) and VC (assert (not (=> assumptions assertions)))(check-sat) — live in the phase transcript, which is discarded (runner.rs:1304 let _ = solver.take_phase_transcript();). The assumptions/assertions partition over conditions.exprs never appears in the key. So the cache maps encoding → verdict and trusts that the encoding determines the answer — not enforced anywhere. §3.4 shows distinct tasks already collide on the baseline key at ~0.6%; today they happen to share verdicts, so no wrong answer, but the silent-false-"verified" channel is live. Fix: key on the full query (Q1 Design A/B).

4.3 Storage: each entry stores unused full SMT text — high (footprint) [verified]

See Q2. smt2_text (~97% of each file, 76 MB total) is never read on lookup. Drop it → ~200× smaller.

4.4 Smaller issues

• --cache-mode off incoherent — medium [verified]. Reachable unreachable! panic at cache.rs:266; check() has no Off branch so it serves hits (cache.rs:228); store() writes in Off (only ReadOnlyEnforcing early-returns, cache.rs:197). Documented as "No caching." Either remove Off (redundant with omitting --cache-dir) or make it truly bypass and not panic.
• Dead counterexample-model machinery — medium [reasoned]. store_cache_entry always writes model: None (runner.rs:1150); cache_verdict_to_verify_report ignores _model (runner.rs:1128, avanhatt's comment). CacheModel/model/values are never populated or consumed; a cached Failure silently loses its counterexample. Wire it end-to-end or remove it ("no phantom features").
• Temp-file race under rayon — low [verified precondition]. store() uses a fixed {short_key}.json.tmp (cache.rs:207); §3.4 shows same-key collisions and par_iter() runs them concurrently. Only affects read-write generation (never ReadOnlyEnforcing — no writes), and a torn file is caught as a parse error → miss → self-heals. Use tempfile::NamedTempFile::new_in(dir) (already a dep).
• Silent swallow of store errors + dead error stat — low [reasoned]. Three let _ = self.store_cache_entry(...) sites (runner.rs:1230/1277/1310); inc_errors is #[allow(dead_code)] (cache.rs:102) so "Errors" always prints 0. Wire failures into inc_errors + log::warn!.
• Redundant stored fields — low [reasoned]. short_key, solver_version (bjorn3). Drop.
• Responses baked into transcript/key — low [reasoned]. ;; response: success lines (solver.rs:139) couple the key to solver output. Strip.
• Duplicated methods — trivial [verified]. take_baseline_transcript and take_phase_transcript are byte-identical (solver.rs:166 / 174). Collapse.
• CacheStore::open panics — trivial [reasoned]. panic! on mkdir failure (cache.rs:132) while the rest of the API returns Result. Make fallible.
• CI redundancy — trivial [verified]. aarch64.args = aarch64-fast.args ∪ slow, so running both verify-cache.sh invocations duplicates work (avanhatt).
• README not updated (avanhatt).
• No .gitattributes for the cache dir — 703 JSON files pollute language stats, diffs, blame. Moot if adopting one-file storage (Q2.3).
• No GC/prune (bjorn3) — see Q2.

[cfallin]

@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)

[alexcrichton]

@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

[mmcloughlin]

@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.