avanhatt opened PR #9178 from wellesley-prog-sys:upstream-08-28 to bytecodealliance:main:
Draft PR to upstream the ongoing ISLE verification work, as described in our ASPLOS 2024 paper: Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection. The motivation for this work is described in detail in the paper.
Using the tool is described in detail at cranelift/isle/veri/README.md.
Alternatives considered
We could continue to develop this work in a fork, but that runs the risk of becoming quickly out-of-date. In discussions with @cfallin, @fitzgen, and @jameysharp, we have designed the specifications and verification to sit alongside the ISLE source.
However, we have also discussed delaying the upstreaming effort to instead upstream the newer version under development by @mmcloughlin. But, this version is much further from having the coverage of the original prototype.
avanhatt updated PR #9178.
cfallin requested cfallin for a review on PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
avanhatt updated PR #9178.
alexcrichton commented on PR #9178:
@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.
- https://github.com/alexcrichton/wasmtime/commit/9c546728430b161a658e998d9a6decfdad2f0d7e - this undoes what looks like a
cargo updatethat may have been performed during development? If you need the updates though let me know and we can try to get that working. That fixes bothcargo denyandcargo vet- https://github.com/alexcrichton/wasmtime/commit/f8e5f3e4cbfc163e1a274e829b27987bb2df8f0b - this flags the two new crates as
publish = falseto fix integration with the auto-publish workflow that we have. If you want these crates published though just let me know and I can help out with that tooNo need to preserve authorship on those, feel free to include the commits here however's easiest to you!
avanhatt updated PR #9178.
avanhatt commented on PR #9178:
@avanhatt for the deny/vet CI errors I have two commits at https://github.com/alexcrichton/wasmtime/commits/verifier which should resolve the issues.
@alexcrichton thanks so much for the help with these, passing all checks now!
avanhatt has marked PR #9178 as ready for review.
avanhatt requested wasmtime-compiler-reviewers for a review on PR #9178.
avanhatt requested wasmtime-default-reviewers for a review on PR #9178.
Last updated: Dec 13 2025 at 21:03 UTC