Stephan Stanisic (Apr 23 2026 at 06:59): Stephan Stanisic (Apr 23 2026 at 06:59):Hi! I've been working on verifying parts of a Wasm fast interpreter similar to A fast in-place interpreter for WebAssembly (Titzer, 2022). Our goal is to define an interpreter template in a meta language (Masm), and then lower this template into a target architecture (e.g. x86 or aarch64). From this template we'd like to generate proofs that our handlers indeed align with Wasm specification in spectec.
We want to generate proofs from the lowered assembly, because this allows us to skip specifying semantics for Masm. And for this we'd like to use Arrival as it already has simplified ISA semantics available.
Ideally we'd like to specify
; Dropping from the stack moves the stack pointer (rsi on x86)
(decl handle_drop () SerializedHandlerBody)
(spec (handle_drop)
(provide (= (:rsi (:registers_out result)) (bvadd (:rsi (:registers_in result)) (int2bv 64 4)))))
(rule (handle_drop)
(SerializedHandlerBody.Inst (lower (Masm.AddImm (Register.ValueStackPointer) 4))))
But it seems having the call to lower requires us to specify the semantics of Masm. This does seems to work:
; inline the pre-lowered code
(rule (handle_drop)
(SideEffectNoResult.Inst (MInst.AddImm (X86Reg.Rsi) 4)))
Am I correct in understanding that there's no way around this? I've attached a minimal mwe.isle file for anyone that is interested in more context.
mwe.isle
Chris Fallin (Apr 23 2026 at 15:47):I guess the core issue here is that you want to somehow "const-prop" the invocation of lower so we get just its result, and then use the spec that we already have on that result? Unfortunately we don't have such an optimization/canonicalization at the moment, but I guess you could do it by hand as you wrote (I can see why you'd prefer not to...)
Last updated: May 03 2026 at 21:15 UTC