Lean-MLIR

Theory of static single assignment developed in the Lean proof assistant. We also build a wealth of tooling to interact closely with the MLIR compiler ecosystem, to enable workflows that include formal verification in the day-to-day of MLIR development.

Documentation

• Publication: Verifying Peephole Rewriting In SSA Compiler IRs
• API Documentation (auto-generated)

Installation

• First, setup the Lean toolchain with elan.
• Next, run:

git clone https://github.com/opencompl/lean-mlir.git && cd lean-mlir && lake exe cache get && lake build

Core theorems

• The proof that rewrites preserve semantics is found at denote_rewritePeepholeAt.
• All core theorems are guarded by #guard_msgs in #print axioms to make sure that we never use sorry as an axiom to prove a core theorem of the framework.

Directory Structure

This directory structure is heavily inspired by the Research Codebase Manifesto.

SSA/Core:

Libraries for reusable components. Code is reviewed to engineering standards. Code is tested, covered by continuous integration, and should never be broken. Very low tolerance for tech debt. Breaking changes to core code should be accompanied by fixes to affected project code. The project owner should assist in identifying potential breakage. No need to fix experimental code.

SSA/Projects:

A top-level folder for each major effort (rough criteria: a project represents 1-6 months of work).

• Code is reviewed for correctness. Testing is recommended but optional, as is continuous integration.
• No cross-project dependencies. If you need code from a different project, either go through the effort of polishing the code into core, or clone the code.