examples/toy_compiler.mlw

   1
   2 (** {1 Correctness of a toy compiler}
   3
   4   Along the lines of
   5   "Correctness of a Compiler for Arithmetic Expressions",
   6   John McCarthy and James Painter,
   7   1967
   8
   9   Author: Claude Marché (Inria)
  10 *)
  11
  12 theory Expr
  13
  14   use int.Int
  15
  16   type expr = Cte int | Plus expr expr | Minus expr expr | Mult expr expr
  17
  18   function eval_expr (e:expr) : int =
  19     match e with
  20     | Cte n -> n
  21     | Plus e1 e2 -> eval_expr e1 + eval_expr e2
  22     | Minus e1 e2 -> eval_expr e1 - eval_expr e2
  23     | Mult e1 e2 -> eval_expr e1 * eval_expr e2
  24     end
  25
  26 end
  27
  28 theory StackMachine
  29
  30   use int.Int
  31   use list.List
  32
  33   type asm = Push int | Add | Sub | Mul
  34   type code = list asm
  35
  36   type stack = list int
  37
  38   function compute (s: stack) (a: code) : stack =
  39     match a with
  40     | Nil -> s
  41     | Cons a r ->
  42       match a,s with
  43       | Push n, _                  -> compute (Cons n s) r
  44       | Add, (Cons n1 (Cons n2 s)) -> compute (Cons (n2+n1) s) r
  45       | Sub, (Cons n1 (Cons n2 s)) -> compute (Cons (n2-n1) s) r
  46       | Mul, (Cons n1 (Cons n2 s)) -> compute (Cons (n2*n1) s) r
  47       | _ -> s
  48       end
  49     end
  50
  51 end
  52
  53 module Compiler
  54
  55   use list.List
  56   use list.Append
  57   use Expr
  58   use StackMachine
  59
  60   function compile (e: expr) : code =
  61     match e with
  62     | Cte n -> Cons (Push n) Nil
  63     | Plus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Add Nil)
  64     | Minus e1 e2 -> compile e1 ++ (compile e2 ++ Cons Sub Nil)
  65     | Mult e1 e2 -> compile e1 ++ (compile e2 ++ Cons Mul Nil)
  66     end
  67
  68   let rec lemma soundness_gen (e: expr) (s: stack) (r: code) : unit
  69     variant { e }
  70     ensures { compute s (compile e ++ r) = compute (Cons (eval_expr e) s) r }
  71   = match e with
  72     | Cte n ->
  73       assert { compile e ++ r = Cons (Push n) r }
  74     | Plus e1 e2 ->
  75       soundness_gen e1 s (compile e2 ++ Cons Add r);
  76       soundness_gen e2 (Cons (eval_expr e1) s) (Cons Add r)
  77     | Minus e1 e2 ->
  78       soundness_gen e1 s (compile e2 ++ Cons Sub r);
  79       soundness_gen e2 (Cons (eval_expr e1) s) (Cons Sub r)
  80     | Mult e1 e2 ->
  81       soundness_gen e1 s (compile e2 ++ Cons Mul r);
  82       soundness_gen e2 (Cons (eval_expr e1) s) (Cons Mul r)
  83     end
  84
  85   let lemma soundness (e: expr) : unit
  86     ensures { compute Nil (compile e) = (Cons (eval_expr e) Nil) }
  87   =
  88     assert { compute Nil (compile e) = compute Nil (compile e ++ Nil) }
  89
  90 end