Correctness of a toy compiler

Along the lines of "Correctness of a Compiler for Arithmetic Expressions", John McCarthy and James Painter, 1967

Author: Claude Marché (Inria)

theory Expr

  use int.Int

  type expr = Cte int | Plus expr expr | Minus expr expr | Mult expr expr

  function eval_expr (e:expr) : int =
    match e with
    | Cte n -> n
    | Plus e1 e2 -> eval_expr e1 + eval_expr e2
    | Minus e1 e2 -> eval_expr e1 - eval_expr e2
    | Mult e1 e2 -> eval_expr e1 * eval_expr e2
    end

end

theory StackMachine

  use int.Int
  use list.List

  type asm = Push int | Add | Sub | Mul
  type code = list asm

  type stack = list int

  function compute (s: stack) (a: code) : stack =
    match a with
    | Nil -> s
    | Cons a r ->
      match a,s with
      | Push n, _                  -> compute (Cons n s) r
      | Add, (Cons n1 (Cons n2 s)) -> compute (Cons (n2+n1) s) r
      | Sub, (Cons n1 (Cons n2 s)) -> compute (Cons (n2-n1) s) r
      | Mul, (Cons n1 (Cons n2 s)) -> compute (Cons (n2*n1) s) r
      | _ -> s
      end
    end

end

module Compiler

  use list.List
  use list.Append
  use Expr
  use StackMachine

  function compile (e: expr) : code =
    match e with
    | Cte n -> Cons (Push n) Nil
    | Plus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Add Nil)
    | Minus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Sub Nil)
    | Mult e1 e2 -> compile e1 ++ (compile e2 ++ Cons Mul Nil)
    end

  let rec lemma soundness_gen (e: expr) (s: stack) (r: code) : unit
    variant { e }
    ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r }
  = match e with
    | Cte n ->
      assert { compile e ++ r = Cons (Push n) r }
    | Plus e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Add r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r)
    | Minus e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Sub r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r)
    | Mult e1 e2 ->
      soundness_gen e1 s (compile e2 ++ Cons Mul r);
      soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r)
    end

  let lemma soundness (e: expr) : unit
    ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) }
  =
    assert { compute Nil (compile e) = compute Nil (compile e ++ Nil) }

end