Tutorial: Compiler Verification

In this tutorial, we verify a compiler from a simple expression language to a stack machine. This is a classic verification challenge that demonstrates custom induction schemes and the interplay between different data structures.

The expression language

type expr =
  | Int of int
  | Plus of expr * expr
  | Times of expr * expr
  | Sub of expr * expr
  | Div of expr * expr
 
let rec eval_expr e =
  match e with
  | Int i -> i
  | Plus (x, y) -> eval_expr x + eval_expr y
  | Times (x, y) -> eval_expr x * eval_expr y
  | Sub (x, y) -> eval_expr x - eval_expr y
  | Div (x, y) -> eval_expr x / eval_expr y

The stack machine

The target is a simple stack machine with push and arithmetic instructions:

type instr =
  | Add
  | Mult
  | Minus
  | Quot
  | Push of int
 
type state = {
  stack : int list;
}
 
let apply (s : state) (f : int -> int -> int) =
  match s.stack with
  | a :: b :: rst ->
    { stack = (f a b) :: rst }
  | _ -> s
 
let step s inst =
  match inst with
  | Add -> apply s (+)
  | Mult -> apply s ( * )
  | Minus -> apply s (fun x y -> y - x)
  | Quot -> apply s (fun x y -> y / x)
  | Push i -> { stack = i :: s.stack }
 
let rec run s program =
  match program with
  | [] -> s
  | i :: i' -> run (step s i) i'
[@@adm program]

The compiler

The compiler translates expressions into stack machine programs:

let rec compile (e : expr) : instr list =
  match e with
  | Int i -> [Push i]
  | Plus (x, y) -> compile x @ compile y @ [Add]
  | Times (x, y) -> compile x @ compile y @ [Mult]
  | Sub (x, y) -> compile x @ compile y @ [Minus]
  | Div (x, y) -> compile x @ compile y @ [Quot]

The key lemma

Before proving the main theorem, we need a lemma about how run distributes over program concatenation:

lemma run_assoc s program_1 program_2 =
  run s (program_1 @ program_2) = run (run s program_1) program_2
[@@by auto] [@@rw]

This says: running two programs in sequence is the same as concatenating them and running at once.

The custom induction scheme

The main correctness theorem requires a careful induction scheme. We define a function purely to induce the right recursion pattern:

let rec compiler_induct s e =
  let ih s x y =
    compiler_induct s x
    && compiler_induct
      { stack = (eval_expr x) :: s.stack }
      y
  in
  match e with
  | Plus (x, y)
  | Times (x, y)
  | Sub (x, y)
  | Div (x, y) ->
    ih s x y
  | _ -> true
[@@adm e]

This function encodes the key insight: when proving correctness for Plus(x, y), we need the inductive hypothesis for x with the original stack state s, and for y with the state after x has been compiled and run (i.e., with eval_expr x pushed onto the stack).

ImandraX only examines the recursion pattern of compiler_induct, not what it computes. The function exists solely to define the right induction scheme.

The main theorem

theorem compiler_correct s e =
  run s (compile e) = { stack = (eval_expr e) :: s.stack }
[@@by induct ~on_fun:[%id compiler_induct] ()]
[@@timeout 120]

This theorem states: running the compiled code on any initial state s produces a state where the expression's value has been pushed onto the stack.

The proof uses induct ~on_fun:[%id compiler_induct] () — the full waterfall with the custom induction scheme from compiler_induct. This tells ImandraX to use the recursion pattern of compiler_induct to structure the induction, then apply the full waterfall (simplification, rewriting with run_assoc, etc.) to close each subgoal.

Why it works

For each subgoal (one per constructor of expr):

Base case (e = Int i): compile (Int i) = [Push i], and run s [Push i] = { stack = i :: s.stack }, which equals { stack = eval_expr (Int i) :: s.stack } ✓

Inductive case (e = Plus(x, y)):

• compile (Plus(x, y)) = compile x @ compile y @ [Add]
• By run_assoc: run s (compile x @ compile y @ [Add]) = run (run (run s (compile x)) (compile y)) [Add]
• By IH for x: run s (compile x) = { stack = eval_expr x :: s.stack }
• By IH for y (with the updated state): run { stack = eval_expr x :: s.stack } (compile y) = { stack = eval_expr y :: eval_expr x :: s.stack }
• Applying Add: { stack = (eval_expr x + eval_expr y) :: s.stack } = { stack = eval_expr (Plus(x, y)) :: s.stack } ✓

What you've learned

• Custom induction schemes using auxiliary functions
• induction ~id:[%id f] () to select a specific scheme
• Compiler correctness — the classic "runs correctly" specification
• Lemma-driven proofs — run_assoc enables the main theorem
• @>>| to apply the same tactic to all subgoals

Next steps

Try extending the compiler with new operations (e.g., Mod, Abs) and updating the correctness proof. Or explore the Ripple-Carry Adder tutorial for hardware verification.