Control flow specs in Arrival · cranelift

Hi! I am trying to use Arrival to reason about chains of instructions that contain control flow, like jumps and conditional branches. I was looking through the generated ISA specs in the Arrival repo, but instructions like CondBr, Jump and Call seem to lack accompanying specifications.

I noticed in the paper for both Crocus and Arrival control flow is specifically omitted from the current work, as I assume its hard to reason about in arbitrary programs. However, the code I am verifying isn't arbitrary, and we can possibly give information about the CFG to Arrival for example.

Does anyone have any suggestions on how to proceed? An example snippet of code I'm trying to reason about is the following:

_instr_I32Const:
    # read 1 byte from source program
    movzx rdx, byte ptr [rax]
    add rax, 1
    # jump to the call decode path if the sign bit is set (decoding needed)
    test dl, dl
    js label_else
    # jump over the sign if no decoding is needed
    jmp label_end

label_else:
    call _decode_leb128

label_end:
    # push the decoded value onto the value stack
    add rsi, -4
    mov DWORD PTR [rsi], edx

vec![
    Deref(Scratch2, InstructionPointer),
    IfThenElse(
        Sign,
        Scratch2,
        vec![Call(GlobalAddressLabels::DecodeLeb128)],
        vec![],
    ),
    Push(I32, Scratch2),
],

I could provide a small isle file with some more context if that would be helpful.

Alexa VanHattum (Jun 10 2026 at 17:37):

Yes, currently the verification logic in Arrival does not have support for arbitrary control flow. You'd need to choose an encoding for more restricted control flow (for example, we use the state support to encode reasoning over equivalent traps; you could do something similar for calls).

Stephan Stanisic (Jul 06 2026 at 09:59):

Thanks for the response! Sorry for the late reply as well, I missed the notification it seems.
Modeling the calls using state sounds like a good approach, I'll try that out.

I'm working on modelling Wasm instruction handlers for a fast interpreter, and while modelling i32.add I came across the following problem: add requires multiple memory accesses for verification to succeed:

All of these require the state loaded_value, and it seems that veri can't reason about this. When I try to call verification it returns with applicability = inapplicable.

(decl masm_pop (ScratchRegs ValueType MState) MState) ;; [...]
(decl masm_push (ValueType MState Reg) MState) ;; [...]
(decl handle_i32add (MState) MState)
;; (spec ...)
(rule handle_i32add_rule (handle_i32add state)
    (let ((p1 MState (masm_pop (ScratchRegs.Sc1) (ValueType.I32) state))
          (p2 MState (masm_pop (ScratchRegs.Sc2) (ValueType.I32) p1))
          (lhs Reg (get_sc1 p2))
          (rhs Reg (get_sc2 p2))

          (sum Reg (add $I32 lhs rhs)))
      (masm_push (ValueType.I32) p2 sum)))

MState contains the machine state, and a functional representation of the current stack. This is so we don't need to reason about memory accesses directly in handle_i32add and can keep that in the pop/push rules. But it seems that even with this indirection veri can't reason about the multiple uses of state.

I think the way to work around this issue would be to have a rule with just specs (e.g. masm_pop), and then have the implementation in another rule (e.g. masm_pop_impl). As long as we make sure the specs on masm_pop_impl fully contain masm_pop this should be fine I think.

Is this applicability = inapplicable a limitation of veri? Is splitting up the spec and implementation a good way forward?

Stream: cranelift

Topic: Control flow specs in Arrival

Stephan Stanisic (May 21 2026 at 08:33):

Alexa VanHattum (Jun 10 2026 at 17:37):

Stephan Stanisic (Jul 06 2026 at 09:59):