Miden assembly decompiler

This crate implements a best-effort decompiler for the Miden assembly language. It is used by the MASM-LSP language server to provide high-level representations of MASM procedures.

Overview

Miden assembly (MASM) is a stack-based assembly language used in the Miden zero-knowledge VM. It is challenging to provide faithful decompilation for hand-written MASM (like the Miden stdlib) for a few different reasons.

• MASM exec calls do not conform to a well-defined ABI, and the net stack effect of such calls is generally impossible to determine statically.
• Most procedures do not have declared signatures, which means that the number of inputs and outputs have to be inferred from context.
• While-loops do not need to be stack neutral. In particular, the while-loop condition may occupy a different stack slot in each iteration.
• Branches in conditional statements may have different stack effects, which makes stack tracking and signature inference challenging.

Example

The following MASM procedure implements an u256 equality check against 0.

// Miden assembly implementation
pub proc eqz
    eq.0
    repeat.7
        swap
        eq.0
        and
    end
end

This is the corresponding pseudocode output generated by the decompiler.

// Decompiled pseudocode
proc eqz(v_0: Felt, v_1: Felt, v_2: Felt, v_3: Felt, v_4: Felt, v_5: Felt, v_6: Felt, v_7_1: Felt) -> Bool {
  v_7 = v_7_1 == 0;
  for i in 0..7 {
    v_(6 - i)_1 = v_(6 - i) == 0;
    v_7 = v_7 and v_(6 - i)_1;
  }
  return v_7;
}

Architecture and design constraints

See the ARCHITECTURE.md file for an overview of the design and architecture of the decompiler.