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

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

Testing

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

Unit Tests

Run the unit tests with:

lake test

FileCheck Tests

FileCheck tests require uv to be installed.

First, install dependencies:

uv sync

Then run the tests:

uv run lit Test/ -v

Running the benchmarks

lake exe run-benchmarks add-fold-worklist

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