ISLE rule verification (Crocus-style)

[avrabe]

Overview

Verify ISLE rewrite rules at build time using SMT, similar to Cranelift's Crocus project.

Approach

1. Parse ISLE rule files
2. Extract LHS/RHS of each rule
3. Generate SMT verification conditions
4. Prove ∀ inputs. eval(LHS) = eval(RHS)

Benefits

• Catch incorrect ISLE rules at build time
• Complement Z3 runtime verification
• Reduce trust in ISLE compiler

References

• Crocus paper
• loom-shared/isle/wasm_terms.isle