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

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

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