[Draft] 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!

[cfallin]

Looks like things are pretty much addressed -- thanks again! One comment above; once that's addressed, as well as the current merge conflict with main, go ahead and flip this out of Draft mode (assuming it's ready and there aren't more TODOs you want to address?), and add a commit with prtest:all in the description; that'll run the full CI pipeline and we can see failures.

(One of those failures will be a cargo vet failure most likely; I can pull down the branch, do my vets locally, and push a new commit on top of your branch to address)