Sunday 15 June 2008

Correctness of an Expression Compiler in Coq

This is based on Correctness Of A Compiler For Arithmetic Expressions and A type-correct, stack-safe, provably correct expression compiler in Epigram


Require Import List.

Fixpoint Tuple (types : list Set) : Type :=
match types with
| nil => unit
| t::ts => (t * Tuple ts)%type
end.

Inductive Exp : Set -> Type :=
| Num : nat -> Exp nat
| Boo : bool -> Exp bool
| Sum : Exp nat -> Exp nat -> Exp nat
| Eql : Exp nat -> Exp nat -> Exp bool
| Iff : forall (a : Set), Exp bool -> Exp a -> Exp a -> Exp a.

Fixpoint nat_eq_bool (x y : nat) {struct x} : bool :=
match x, y with
| O, O => true
| S x', S y' => nat_eq_bool x' y'
| _,_ => false
end.

Fixpoint eval (a : Set) (e : Exp a) : a :=
match e in Exp t return t with
| Num n => n
| Boo b => b
| Sum p q => eval _ p + eval _ q
| Eql x y => nat_eq_bool (eval _ x) (eval _ y)
| Iff _ b t e => if eval _ b then eval _ t else eval _ e
end.

(* example *)
Eval compute in
(eval _
(Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
(Sum (Num 5) (Num 8))
(Num 0))).

Notation "x --> y" := (x,y) (at level 120, right associativity).

Inductive INST : list Set * list Set -> Type :=
| PUSHN : forall s, nat -> INST (s --> nat::s)
| PUSHB : forall s, bool -> INST (s --> bool::s)
| SUM : forall s, INST (nat::nat::s --> nat::s)
| EQL : forall s, INST (nat::nat::s --> bool::s)
| COND : forall s, forall a, INST (bool::a::a::s --> a::s).

Inductive stack : list Set -> Type :=
| snil : stack nil
| scons : forall p q, INST (p --> q) -> stack p -> stack q.

Fixpoint compile
(a : Set) (e : Exp a)
(tail : list Set) (rest : stack tail)
{ struct e } : stack (a::tail) :=
match e in Exp a return stack (a::tail) with
| Num n =>
scons _ _ (PUSHN _ n) rest
| Boo b =>
scons _ _ (PUSHB _ b) rest
| Sum u v =>
scons _ _ (SUM _)
(compile _ u _
(compile _ v _ rest))
| Eql x y =>
scons _ _ (EQL _)
(compile _ x _
(compile _ y _ rest))
| Iff a b t e =>
scons _ _ (COND _ _)
(compile _ b _
(compile _ t _
(compile _ e _ rest)))
end.

Definition evinst :
forall p q,
forall (i : INST (p --> q)),
Tuple p -> Tuple q :=
fun p q i =>
match i in INST pq return Tuple (fst pq) -> Tuple (snd pq) with
| PUSHN _ n => fun s =>
(n, s)
| PUSHB _ b => fun s =>
(b, s)
| SUM _ => fun s =>
match s with
| (u, (v, s)) => (u + v, s)
end
| EQL _ => fun s =>
match s with
| (x, (y, s)) => (nat_eq_bool x y, s)
end
| COND _ _ => fun s =>
match s with
| (b, (t, (e, s))) =>
(if b then t else e, s)
end
end.

Fixpoint evstack typs (program : stack typs)
{ struct program } : Tuple typs :=
match program in stack typs return Tuple typs with
| snil => tt
| scons t ts i is => evinst _ _ i (evstack _ is)
end.

Eval compute in
(evstack _ (compile _
(Iff _ (Eql (Num 7) (Sum (Num 4) (Num 3)))
(Sum (Num 5) (Num 8))
(Num 0)) nil snil)).

Lemma eval_correct :
forall a (e : Exp a),
forall typs (program_tail : stack typs),
(eval a e, (evstack typs program_tail))
=
evstack (a::typs) (compile a e typs program_tail).
Proof.
induction e.

reflexivity.

reflexivity.

intros.
unfold compile; fold compile; simpl.
rewrite <- IHe1.
rewrite <- IHe2.
reflexivity.

intros.
unfold compile; fold compile; simpl.
rewrite <- IHe1.
rewrite <- IHe2.
reflexivity.

intros.
unfold compile; fold compile; simpl.
rewrite <- IHe1.
rewrite <- IHe2.
rewrite <- IHe3.
reflexivity.
Qed.


No comments: