Verified Intermediate Representation

VeIR is a compiler infrastructure written in Lean that offers both an MLIR-style imperative design and (optional) ITP-level verification. VeIR connects with MLIR via the MLIR textual format, making it easy to combine MLIR and VeIR tools.

VeIR Features	Complete	Verified
MLIR core data structures (block, operation, region)	✅	🔒
define dialects	✅ (basic)
pass infrastructure	✅
peephole rewriter	✅
peephole rewriter (declarative)
interpreter framework	✅

Building and testing

Building VeIR requires Lean 4 and its build tool Lake.

Common tasks are wrapped in the Makefile: make build to build and make tests to run the tests. Run make to list every target.

Lake builds ExArray's native C code with Lean's bundled LLVM toolchain. Non-Nix builds need GMP development headers and pkg-config (or pkgconf).

With Nix, nix develop enters a development shell containing Lean's toolchain manager and all native and Python dependencies needed by those Make targets. Executable targets like veir-opt and veir-interpret can be run with nix run .#veir-opt, nix run .#veir-interpret, etc. For convenience, makefile targets are also exposed as flake apps with nix run .#build and nix run .#tests; nix run . displays the Makefile help. If both direnv and Nix are installed, run direnv allow to automatically activate the development shell whenever you enter the project directory.

Our testing framework is split into two parts: unit tests written in Lean and FileCheck tests for the command line tool veir-opt. The FileCheck tests require uv to be installed.

Run a single benchmark with lake exe run-benchmarks <name> (see Veir/Benchmarks.lean for the available names).

From C to VeIR

This section gives an example showing how to run code through a VeIR pass, starting from C code.

Prerequisite: An up-to-date MLIR bin directory in your PATH.

Start with a C function:

cat << _end_ > demorgan.c
unsigned d1(unsigned p, unsigned q) {
  return ~(~p & ~q);
}

unsigned short d2(unsigned short p, unsigned short q) {
  return ~(~p | ~q);
}
_end_

Compile to LLVM IR:

clang -cc1 -O0 -disable-O0-optnone -emit-llvm demorgan.c

Optimize it a little:

opt -passes=sroa demorgan.ll -S -o demorgan-opt.ll

Translate to MLIR:

mlir-translate --import-llvm demorgan-opt.ll | mlir-opt --mlir-print-op-generic --mlir-print-local-scope > demorgan-opt.mlir

Optimize using VeIR's InstCombine and DCE (dead code elimination) passes:

lake exec veir-opt -p=instcombine,dce demorgan-opt.mlir

Alternatively, you can batch up these commands using the provided compiler driver and emit the optimized MLIR to stdout:

Tools/vcc demorgan.c --emit-mlir -O -o -

Without an explicit emit mode, vcc translates VeIR's output back to LLVM IR and asks clang to produce an executable:

cat << _end_ > hello.c
#include <stdio.h>

int main(void) {
  printf("hello, world\n");
}
_end_

Tools/vcc hello.c -o hello