Stream: git-wasmtime

Topic: wasmtime / PR #13991 Fix mid-end ISLE spec causing verifi...

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

yagehu opened PR #13991 from yagehu:veri-opt to bytecodealliance:main:

This commit fixes a recently upstreamed VeriISLE follow-up work to verify many mid-end ISLE rules in #13935. Currently, the verification times out for this specific rule:

(rule (simplify (imul ty x (iconst _ (imm64_power_of_two c))))
      (ishl ty x (iconst ty (imm64 c))))

This is because the imm64_power_of_two extractor contains a buggy provides block. This commit changes the specification to a more intuitive one that successfully verifies.

Before fix:

============================= Verification summary ============================
Total expansions:    1331
In scope expansions: 1054
Type instantiations: 5148
Applicable:          5134
Verification passed: 5133
Verification failed: 0
Verification unknown: 1
===============================================================================

After fix:

============================= Verification summary ============================
Total expansions:    1331
In scope expansions: 1054
Type instantiations: 5148
Applicable:          5134
Verification passed: 5134
Verification failed: 0
Verification unknown: 0
===============================================================================

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

yagehu requested wasmtime-compiler-reviewers for a review on PR #13991.

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

yagehu requested cfallin for a review on PR #13991.

Wasmtime GitHub notifications bot (Jul 27 2026 at 02:34):

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

Wasmtime GitHub notifications bot (Jul 27 2026 at 18:58):

avanhatt commented on PR #13991:

Thanks for this improvement!

Per z3, old and new are equivalent when the match condition holds (the old spec was sound and did terminate with success on my machine, but the new is substantially faster).

Wasmtime GitHub notifications bot (Jul 27 2026 at 19:10):

:thumbs_up: cfallin submitted PR review:

Thanks!

Wasmtime GitHub notifications bot (Jul 27 2026 at 19:10):

cfallin added PR #13991 Fix mid-end ISLE spec causing verification timeout to the merge queue.

Wasmtime GitHub notifications bot (Jul 27 2026 at 20:18):

:check: cfallin merged PR #13991.

Wasmtime GitHub notifications bot (Jul 27 2026 at 20:18):

cfallin removed PR #13991 Fix mid-end ISLE spec causing verification timeout from the merge queue.

Last updated: Jul 29 2026 at 05:03 UTC