# 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.