fold/docs/internal/mir-verification-research.md

MIR (Mid-level IR) Verification Research

Generated 2026-05-28. Research on MIR-level analysis for Rust and Swift.

Rust MIR vs HIR

Aspect	HIR	MIR
Abstraction level	High (desugared AST)	Mid (control-flow graph)
Control flow	Expressions, if-let, match	Basic blocks, terminators
Borrow checking	Not present	Full borrow-checked
Optimizations	None	Inlining, const-prop, GVN
Loops	Desugared to loop/match	Explicit backedges
Available in fold-rust	Yes (via rustc HIR visitor)	Partial (mir_analysis.rs)

MIR-Based Verification Tools

Kani (AWS)

• Approach: MIR → Goto-C → CBMC (bounded model checker)
• Output: proof of correctness or counterexample
• Key insight: MIR is already in SSA form — easy to translate to SMT
• Relevance to fold: Kani demonstrates that MIR → Z3 is feasible and proven

Prusti (ETH Zurich)

• Approach: MIR → Viper (verification intermediate language)
• Uses: Rust type system for permission-based reasoning
• Key insight: borrow-checker information carries through MIR
• Relevance: our MIR analysis can leverage borrow-checker facts

Creusot

• Approach: MIR → Why3 (deductive verification platform)
• Key insight: MIR is designed for analysis — all Rust verifiers use it

RustHorn

• Approach: MIR → CHC (Constrained Horn Clauses)
• Key insight: MIR BasicBlocks map naturally to CHC predicates

fold's MIR Analysis (existing)

tools/fold-rust/src/mir_analysis.rs:

• BorrowTracker: two-pass fixed-point analysis tracking borrow-safe locals
• Pass 0: reference types (&T, &mut T) → inherently borrow-backed
• Pass 1: seeds from Rvalue::Ref, Rvalue::RawPtr, Rvalue::CopyForDeref
• Pass 2: propagates through casts, field access, tuple indexing
• Output: is_borrow_safe() predicate for each MIR local

Gap: MIR analysis exists but is NOT wired into the Z3 encoder. The encoder still walks HIR expression trees.

What fold Needs from MIR

1. Control flow: MIR BasicBlock structure → Z3 path predicates (much richer than HIR if-let)
2. Borrow safety: BorrowTracker results → filter null-deref findings on safe borrows
3. Discriminant switches: MIR switchInt on enum discriminants → path refinement
4. Call terminators: MIR TerminatorKind::Call → interprocedural analysis
5. SSA form: MIR locals are immutable SSA values → direct Z3 variable mapping

Swift SIL → MIR Equivalence

Swift SIL is structurally similar to Rust MIR:

• Basic blocks with terminators (br, cond_br, switch_enum, return)
• SSA values (SIL values are immutable)
• Borrow scopes (SIL borrows map to Rust borrows)
• Witness tables (SIL protocol witnesses map to Rust trait objects)

The SWAN parser already produces structured SIL. The gap is:

1. SIL → fold IR tree conversion (SIL is CFG-based, fold IR is expression-tree-based)
2. Lowering the CFG back to trees for the current encoder

Recommended Approach

Short-term: Wire BorrowTracker into fold-rust's finding emission — skip null-deref on borrow-safe locals. ~30 lines, immediate FP reduction.

Medium-term: Add MIR control-flow to encodeRustIr — walk basic blocks instead of expression trees. Requires restructuring the encoder to understand basic blocks and terminators.

Long-term: Unify Rust MIR + Swift SIL into a common mid-level IR that the Z3 encoder operates on directly.