Stream: cranelift

Topic: The new rule verifier

Bongjun Jang (Jan 04 2026 at 06:10):

Hi! I just found an interesting project arrival which seems like the next-gen of crocus.

The paper says it can verify stateful rules (traps, ...) and more, unlike crocus. So it can verify broader group of rules than crocus.

I want to use this tool for mid-end rules.
But it looks like there is only a demonstration for a codegen backend (aarch64, x64, ...).
And the paper states it verifies a instruction-selection backend.
Is this possible to use this tool only for mid-end ISLE rules?

Plus, I want to hear a plan to integrate project this into the upstream wasmtime/cranelift, if any, just like crocus.

Thanks!

Chris Fallin (Jan 05 2026 at 05:18):

cc @Alexa VanHattum and @Michael McLoughlin for upstreaming plans -- I know that they want to do this soon-ish

Alexa VanHattum (Jan 07 2026 at 20:33):

Yes, arrival also can be used for mid-end rules, though some of that work happened after the paper and some of the details (mostly for floating point) are work-in-progress.

We are working on upstreaming this spring! I will try and see if we can prioritize landing the non-floating point stuff first to have it available to you sooner. Feel free to DM me if you'd like to locally run it sooner and I can try and put together instructions beyond the artifact details

Bongjun Jang (Jan 12 2026 at 06:52):

Thanks for the reply!

Good to hear the upstreaming plan. I'd like to verify a single mid-end rule (i.e. one rule of simplify) and run it locally. I have a few questions:

1. The doc shows how to run the verifier (./script/veri.sh). But on my machine, it crashes:

Writing generated file: /tmp/tmp.LixEWtIdyN/clif_opt.isle
Writing generated file: /tmp/tmp.LixEWtIdyN/clif_lower.isle
#0      iconst
        iconst({bits: int}, bv 64) -> bv 8
                type solution status = solved
                applicability = applicable
                verification = success
        iconst({bits: int}, bv 64) -> bv 16
                type solution status = solved
                applicability = applicable
                verification = success
        iconst({bits: int}, bv 64) -> bv 32
                type solution status = solved
                applicability = applicable
                verification = success
        iconst({bits: int}, bv 64) -> bv 64
                type solution status = solved
                applicability = applicable
                verification = success
#1      operand_size_32
                type solution status = solved
                applicability = applicable
                verification = success
...
#59     f64const
                type solution status = solved
                applicability = applicable
                verification = success
#60     f64const
                type solution status = solved
                applicability = applicable
                verification = success
#61     f64const
Error: expanding constructor 'emit_u64_le_const'

Caused by:
    no spec for term emit_u64_le_const

Is it normal to miss the spec for the term emit_u64_le_const?

2. Is there a spec written for the mid-end rules?
3. I think I can verify mid-end rules one-by-one by removing rules other than the rule I want to verify. But there should be a better way to do this. When verifying a set of rules with arrival, can I see which rules are verified and which rules are not?

Last updated: Feb 24 2026 at 05:28 UTC