Wasmtime GitHub notifications bot (Aug 31 2026 at 21:54): Wasmtime GitHub notifications bot (Aug 31 2026 at 21:54):alexcrichton opened PR #14249 from alexcrichton:intentionally-break-egraphs to bytecodealliance:main:
I'm curious to see what the CI failure looks like
<!--
Please make sure you include the following information:
If this work has been discussed elsewhere, please include a link to that
conversation. If it was discussed in an issue, just mention "issue #...".Explain why this change is needed. If the details are in an issue already,
this can be brief.Our development process is documented in the Wasmtime book:
https://docs.wasmtime.dev/contributing-development-process.htmlPlease review the Bytecode Alliance's AI tool usage policy at
https://github.com/bytecodealliance/governance/blob/main/AI_TOOL_POLICY.mdPlease ensure all communication follows the code of conduct:
https://github.com/bytecodealliance/wasmtime/blob/main/CODE_OF_CONDUCT.md
-->
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:43):cfallin commented on PR #14249:
I guess such a core change to execution semantics also broke our ordinary execution-based tests but the verifier does catch this -- neat to see!
=== VERIFICATION FAILURES (4) === FAILURE #4 cranelift/codegen/src/opts/arithmetic.isle line 23 (instantiation 0) .veriisle/expansions/00004/000/failure.out FAILURE #4 cranelift/codegen/src/opts/arithmetic.isle line 23 (instantiation 14) .veriisle/expansions/00004/014/failure.out FAILURE #4 cranelift/codegen/src/opts/arithmetic.isle line 23 (instantiation 28) .veriisle/expansions/00004/028/failure.out FAILURE #4 cranelift/codegen/src/opts/arithmetic.isle line 23 (instantiation 42) .veriisle/expansions/00004/042/failure.out
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:44):avanhatt commented on PR #14249:
Ah, looks like we should update the config run in CI to dump the counterexample instead of just the name(s) of the file where the details of the failures live.
That would look like e.g. this for this example:
#4 cranelift/codegen/src/opts/arithmetic.isle line 23 instantiation=0 model: state: clif_store = {active: false, size_bits: 1, addr: #x0000000000000000, value: #x0000000000000000} state: clif_trap = false state: loaded_value = #x0000000000000000 state: relax_nan = false state: clif_load = {active: false, size_bits: 0, addr: #x0000000000000000} iadd({bits: 8}, #x40, #xdf) -> #x1f ineg({bits: 8}, #x21) -> #xdf isub({bits: 8}, #x21, #x40) -> #xe1 simplify(#x1f) -> #xe1The key bit being that
simplify(#x1f)gets rewritten to#xe1for inputs#x40and#xdf. I'm sure we could bike shed further on the display of this, as well. :smile:
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:44):avanhatt edited a comment on PR #14249:
Ah, looks like we should update the config run in CI to dump the counterexample instead of just the name(s) of the file where the details of the failures live.
That would look like e.g. this for this example:
#4 cranelift/codegen/src/opts/arithmetic.isle line 23 instantiation=0 model: state: clif_store = {active: false, size_bits: 1, addr: #x0000000000000000, value: #x0000000000000000} state: clif_trap = false state: loaded_value = #x0000000000000000 state: relax_nan = false state: clif_load = {active: false, size_bits: 0, addr: #x0000000000000000} iadd({bits: 8}, #x40, #xdf) -> #x1f ineg({bits: 8}, #x21) -> #xdf isub({bits: 8}, #x21, #x40) -> #xe1 simplify(#x1f) -> #xe1The key bit being that
simplify(#x1f)gets rewritten to#xe1for 8-bitisubwith inputs#x40and#xdf. I'm sure we could bike shed further on the display of this, as well. :smile:
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:45):avanhatt edited a comment on PR #14249:
Ah, looks like we should update the config run in CI to dump the counterexample instead of just the name(s) of the file where the details of the failures live.
That would look like e.g. this for this example:
#4 cranelift/codegen/src/opts/arithmetic.isle line 23 instantiation=0 model: state: clif_store = {active: false, size_bits: 1, addr: #x0000000000000000, value: #x0000000000000000} state: clif_trap = false state: loaded_value = #x0000000000000000 state: relax_nan = false state: clif_load = {active: false, size_bits: 0, addr: #x0000000000000000} iadd({bits: 8}, #x40, #xdf) -> #x1f ineg({bits: 8}, #x21) -> #xdf isub({bits: 8}, #x21, #x40) -> #xe1 simplify(#x1f) -> #xe1The key bit being that
simplify(#x1f)gets rewritten to#xe1for 8-bitiaddwith inputs#x40and#xdf. I'm sure we could bike shed further on the display of this, as well. :smile:
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:49):alexcrichton commented on PR #14249:
Nice! Yeah dumping to CI I think would work well, but definitely not urgent at all I was just curious to see what happened here. I figure seeing "verification failed" in CI is probably sufficient to trigger us to think harder about rules and figure out what went wrong.
Out of curiousity is the reason that this took 30m in CI that it basically didn't have any cache hits and the resulting queries probably just took awhile to compute?
Wasmtime GitHub notifications bot (Aug 31 2026 at 22:50)::cross_mark: alexcrichton closed without merge PR #14249.
Wasmtime GitHub notifications bot (Sep 01 2026 at 00:11):avanhatt commented on PR #14249:
Nice! Yeah dumping to CI I think would work well, but definitely not urgent at all I was just curious to see what happened here. I figure seeing "verification failed" in CI is probably sufficient to trigger us to think harder about rules and figure out what went wrong.
True, and the ISLE file + line number is at least here without needing another change. I'll followup in another PR for the counterexample.
Out of curiousity is the reason that this took 30m in CI that it basically didn't have any cache hits and the resulting queries probably just took awhile to compute?
Yeah, because:
isubon the RHS of this rule can be "chained" in many different ways with other rules (this rule firing, thenisuband later lowerings from intermediate terms follow combinatorially)- Each chain of rules requires 2 queries per type instantiation (
i8,i16`, etc)this changes 200+ SMT queries, so those actually hit the solver.
@cfallin's earlier 18 minutes run also excluded
opt, so we don't have a baseline number for what the midend alone would be with a cold cache (other than < 3 hours from the total full run ofopt+aarch64+ minimalx64).
Wasmtime GitHub notifications bot (Sep 01 2026 at 00:12):avanhatt edited a comment on PR #14249:
Nice! Yeah dumping to CI I think would work well, but definitely not urgent at all I was just curious to see what happened here. I figure seeing "verification failed" in CI is probably sufficient to trigger us to think harder about rules and figure out what went wrong.
True, and the ISLE file + line number is at least here without needing another change. I'll followup in another PR for the counterexample.
Out of curiousity is the reason that this took 30m in CI that it basically didn't have any cache hits and the resulting queries probably just took awhile to compute?
Yeah, because:
isubon the RHS of this rule can be "chained" in many different ways with other rules (this rule firing, thenisuband later lowerings from intermediate terms follow combinatorially)- Each chain of rules requires 2 queries per type instantiation (
i8,i16, etc)this changes 200+ SMT queries, so those actually hit the solver.
@cfallin's earlier 18 minutes run also excluded
opt, so we don't have a baseline number for what the midend alone would be with a cold cache (other than < 3 hours from the total full run ofopt+aarch64+ minimalx64).
Last updated: Sep 20 2026 at 18:08 UTC