CertIMP: A Lean-Verified Toy Implementation of IMP

Welcome! This repository contains a Lean 4 development of IMP, a simple imperative language commonly used in introductory programming language theory classes. It adapts and expands upon the first five chapters of Software Foundations Vol. 2: Programming Language Foundations.

Why?

Our main contribution beyond the textbook presentation is a verified compiler from IMP to the instruction set of a simple stack-based machine, by a proof of semantics preservation. This composes neatly with correctness proofs for other code transformations, e.g., constant folding. We therefore provide a very simple optimizing compiler, along with its machine-checked proof of correctness.

This work was done as part of the Program Verification master's lab at the Faculty of Mathematics & Computer Science, Univ. of Bucharest. All proofs in this Lean project have been written collaboratively by students over the course of a semester.

Navigating this project

We embed IMP syntax to Lean via metaprogramming, drawing inspiration from the Rocq notations in the Software Foundations book.

On this basis, our project follows with the basic development of IMP:

• its big-step operational semantics;
• a Hoare calculus, along with its soundness & completeness theorems;
• a custom tactic for automatically proving Hoare triple goals by verification condition generation;
• we also touch upon weakest precondition calculus using total correctness triples.

As previously mentioned, this project also contains:

• the definition of an idealized stack machine;
• its corresponding instruction set, along with its semantics;
• a semantics-preservation proof for compiling IMP to this ISA;
• a simple constant folding optimization pass which we similarly prove correct.

Building

Before you start, make sure you have Lean installed in your environment.

1. Clone this repository.
2. From your cloned directory, run lake exe cache get. This will fetch a compressed version of the Mathlib library, which would normally be huge.
3. Run lake build.

Acknowledgments

Our semantics preservation proof was initially modelled following the one developed by @palexand and his students for the EECS 755 course, which only covers arithmetic and boolean expressions. For the semantics of the ISA, we took inspiration from @NethermindEth's formal model of the Ethereum Virtual Machine in Lean.