Update SMT-based ISLE verifier

[avanhatt]

Update the core ISLE verifier for formal, SMT-based checking of instruction lowering rules. This brings the implementation up-to-date with our work described at OOPSLA 2025, rather than the prior ASPLOS 2024 implementation.

The core improvements are:

1. Automatic rule chaining. Rather than requiring specifications on every ISLE term, terms can be marked veri chain to be automatically composed/inlined. This reduces the specification burden substantially. See the paper for details.
2. For the aarch64 backend, most machine inst Minst specifications are automatically derived from the authoritative ARM ASL reference, with our work building on the ASLp project to derive more targeted specifications for this domain.
3. Our state modeling now handles traps and other side effects more explicitly, see the paper for details.
4. The specification language is more expressive, including structs and macros. See the language reference updates for details.

[bjorn3]

Accidental commit?

[avanhatt]

Ah yes, thanks for spotting!

[cfallin]

This largely looks good! I skimmed over any spec/model/attr forms in the diffs of ISLE, and the cranelift/isle/veri tree in general; reviewed more carefully the bits that were touched in Cranelift and the ISLE compiler proper. Some logistical comments but nothing really substantial. Thanks for all the work in getting this in shape for upstreaming!

[cfallin]

Does this debug code need to stay in-tree? (It looks like it's trying to help find very deeply nested invocations? In any case I'd rather not have the ad-hoc thread-local magic here if we don't need this check permanently)

[avanhatt]

Oops, did not mean to include, removed!

[github-actions]

Subscribe to Label Action

cc @cfallin, @fitzgen

Details

This issue or pull request has been labeled: "cranelift", "cranelift:area:aarch64", "cranelift:meta", "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.

[cfallin]

@avanhatt I'm taking a look at the cargo-vets now and it looks like this PR bumps a bunch of dep versions in ways that I hope are not necessary -- the vet backlog is now

• 144 crate bumps (each of which takes a manual step from me, so this is ~a day of work)
• an audit backlog of 425,163 lines of code

Which is unfortunately probably infeasible for me to do. Could you (i) revert Cargo.lock to its state from your latest merge-from-main, and (ii) run a build again, to see if we can minimize the diff? I suspect that maybe this branch ran a cargo update at some point and did a bunch of incidental upgrades.

[cfallin]

Thanks for your last commit -- looks like the dep bumps and vet burden are real; still 425163 LoC.

Digging into one particular bump (tracing 0.1.41 -> 0.1.44, which alone is 61kLoC of diff), it looks like the aslp crate depends on tracing too, and probably pulled in a newer version somehow?

Would you mind doing a little dep gardening to see if we can get the diff to our deps a bit smaller? cargo vet should work locally for anyone to check the audit backlog size, too. Thanks!

[mmcloughlin]

Would you mind doing a little dep gardening

Done and pushed. I see 7 unvetted dependencies in cargo vet now. Some appear to be partially covered already trusted authors. The biggest remaining one is pest, which I think may fall under the "10,000 downloads a day" policy.

Let us know if you see the same, and the backlog is manageable.

[alexcrichton]

A note on the vets here -- we already exempt dependencies exclusively related to fuzzing from vetting and I think it would be reasonable to take a similar stance here. Specifically if you apply this diff:

diff --git a/supply-chain/config.toml b/supply-chain/config.toml
index 16d0abfb19..925447fe98 100644
--- a/supply-chain/config.toml
+++ b/supply-chain/config.toml
@@ -64,6 +64,12 @@ audit-as-crates-io = true
 [policy.cranelift-isle]
 audit-as-crates-io = true

+[policy.cranelift-isle-veri]
+criteria = []
+
+[policy.cranelift-isle-veri-aslp]
+criteria = []
+
 [policy.cranelift-jit]
 audit-as-crates-io = true

the cargo vet command succeeds and nothing else is necessary.

[cfallin]

With all of the tweaks and now a green CI run, this looks ready to merge.

Thanks again @avanhatt, @mmcloughlin and others for all the work on this! Looking forward to followup work to get this in CI by default (I have some tasks for this). It's a great addition to our correctness story.