| A compilation from PSLC to Imp and its soundness proof |
Require Import Arith List Omega.
Require Import Binding.
Require Import PSLC.
Require Import MemMonad.
Require Import Imp.
Set Implicit Arguments.
The compiler |
Fixpoint compile_ty (t : ty) : ity :=
match t with
| Data _ => IData INat
| Arrow t1 t2 => IArrow (compile_ty t1) (compile_ty t2)
end.
The main thing to note in compile_term's definition is that we use the
library function VarConvert from Binding to convert a Debruijn variable
from one type system to another.
The cases for Pair, Inl, Inr, and Case are rather busy.
They're using the standard trick of encoding "let" binding with abstraction
and application.
This compilation uses an obvious representation strategy where memory location 0 is reserved to store a heap limit pointer, such that a new allocation involves picking this pointer as the address of the new object and then incrementing the pointer with the new object's length. Products are simply stored in adjacent memory cells, while sums are represented like products, where the first cell is a tag (with 0 signifying inl and 1 signifying inr) and the second cell holds the data value (of tag-dependent type). |
Fixpoint compile_term (G : list ty) (t : ty) (e : term G t) {struct e}
: iterm (map compile_ty G) (compile_ty t) :=
match e in (term G t) return (iterm (map compile_ty G) (compile_ty t)) with
| EVar _ _ v => IVar (VarConvert _ v)
| Lam _ _ _ e' => ILam (compile_term e')
| App _ _ _ e1 e2 => IApp (compile_term e1) (compile_term e2)
| Const _ n => IConst _ n
| Pair _ _ _ e1 e2 =>
IApp
(IApp
(IApp
(ILam (ILam (ILam
(ISeq (IWrite (ISucc (IVar (First _ _))) (IVar (Next _ (Next _ (First _ _)))))
(ISeq (IWrite (ISucc (ISucc (IVar (First _ _)))) (IVar (Next _ (First _ _))))
(ISeq (IWrite (IConst _ 0) (ISucc (ISucc (IVar (First _ _)))))
(IVar (First _ _))))))))
(compile_term e1))
(compile_term e2))
(IRead (IConst _ 0))
| Fst _ _ _ e1 => IRead (ISucc (compile_term e1))
| Snd _ _ _ e1 => IRead (ISucc (ISucc (compile_term e1)))
| Inl _ _ _ e1 =>
IApp
(IApp
(ILam (ILam
(ISeq (IWrite (ISucc (IVar (First _ _))) (IConst _ 0))
(ISeq (IWrite (ISucc (ISucc (IVar (First _ _)))) (IVar (Next _ (First _ _))))
(ISeq (IWrite (IConst _ 0) (ISucc (ISucc (IVar (First _ _)))))
(IVar (First _ _)))))))
(compile_term e1))
(IRead (IConst _ 0))
| Inr _ _ _ e1 =>
IApp
(IApp
(ILam (ILam
(ISeq (IWrite (ISucc (IVar (First _ _))) (IConst _ 1))
(ISeq (IWrite (ISucc (ISucc (IVar (First _ _)))) (IVar (Next _ (First _ _))))
(ISeq (IWrite (IConst _ 0) (ISucc (ISucc (IVar (First _ _)))))
(IVar (First _ _)))))))
(compile_term e1))
(IRead (IConst _ 0))
| Case _ _ _ _ e e1 e2 =>
IApp
(IApp
(IApp
(ILam (ILam (ILam
(IIf (IRead (ISucc (IVar (Next _ (Next _ (First _ _))))))
(IApp (IVar (Next _ (First _ _))) (IRead (ISucc (ISucc (IVar (Next _ (Next _ (First _ _))))))))
(IApp (IVar (First _ _)) (IRead (ISucc (ISucc (IVar (Next _ (Next _ (First _ _))))))))))))
(compile_term e))
(ILam (compile_term e2)))
(ILam (compile_term e1))
end.
Soundness proof |
| The proof is based around a standard logical relations argument. We start by defining the relation for data values. |
Section dval_lr.
Variable m : memory.
Fixpoint dval_lr (t : dty) : dtyDenote t -> nat -> Prop :=
match t return (dtyDenote t -> _) with
| Nat => fun n1 n2 => n1 = n2
| Prod t1 t2 => fun p a =>
S a < m O
/\ dval_lr t1 (fst p) (m (S a))
/\ dval_lr t2 (snd p) (m (S (S a)))
| Sum t1 t2 => fun s a =>
S a < m O
/\ match s with
| inl v => m (S a) = 0 /\ dval_lr t1 v (m (S (S a)))
| inr v => m (S a) = 1 /\ dval_lr t2 v (m (S (S a)))
end
end.
End dval_lr.
Now we define what it means for one memory to extend another. In
particular:
|
Record extends (m m' : memory) : Prop := {
aptr : m' O >= m O;
apres : forall a, a < m O -> m (S a) = m' (S a)
}.
Hint Constructors extends.
| Now we can define the logical relation for values in general. |
Fixpoint val_lr (m : memory) (t : ty) {struct t} : tyDenote t -> ivalDenote (compile_ty t) -> Prop :=
match t return (tyDenote t -> ivalDenote (compile_ty t) -> _) with
| Data t => dval_lr m t
| Arrow t1 t2 => fun bf lf => forall m',
extends m m'
-> forall bx lx, val_lr m' t1 bx lx
-> mspec (fun m'' v =>
extends m' m''
/\ val_lr m'' t2 (bf bx) v)
(lf lx) m'
end.
The data value LR is monotone with respect to extends.
|
Lemma dval_lr_monotone : forall m m' t bx lx,
dval_lr m t bx lx
-> extends m m'
-> dval_lr m' t bx lx.
induction t; memM_simplify.
Qed.
Hint Resolve dval_lr_monotone.
extends is transitive.
|
Lemma extends_trans : forall m1 m2 m3,
extends m1 m2
-> extends m2 m3
-> extends m1 m3.
memM_simplify.
Qed.
Hint Resolve extends_trans.
The value LR is monotone with respect to extends.
|
Lemma val_lr_monotone : forall m m' t bx lx,
extends m m'
-> val_lr m t bx lx
-> val_lr m' t bx lx.
induction t; memM_simplify.
Qed.
Hint Resolve val_lr_monotone.
Definition Slr_Cons' :=
Slr_Cons (dom1:= ty) (denote1:= tyDenote) (denote2:= ivalDenote) (compile:= compile_ty).
Hint Resolve Slr_Nil.
Hint Resolve Slr_Cons'.
We use a generic logical relation over substitutions: Subst_lr, which
comes from Binding. It's parameterized by the function for converting a
type in the first world into a type in the second, as well as by the logical
relation which each corresponding pair of values in the two substitutions
should inhabit.
This lemma proves the usual monotonicity property for this LR. |
Lemma subst_lr_monotone : forall m G (s : Subst _ G) s',
Subst_lr compile_ty (val_lr m) s s'
-> forall m', extends m m'
-> Subst_lr compile_ty (val_lr m') s s'.
induction 1; eauto 6.
Qed.
Hint Resolve subst_lr_monotone.
| Our last logical relation is for expressions. It asserts a fact for any two substitutions for the free variables of the terms being compared, as long as those substitutions are related. In such a case, we want that the imperative expression evaluates to a memory that extends the original, and that the value the imperative expression produces is related to its functional counterpart. |
Definition exp_lr G t (Be : term G t) (Le : iterm (map compile_ty G) (compile_ty t)) :=
forall m s s',
Subst_lr compile_ty (val_lr m) s s'
-> mspec (fun m' v =>
extends m m'
/\ val_lr m' t (termDenote Be s) v)
(itermDenote Le s') m.
This is a thin wrapper around a generic theorem from Binding.
That theorem's form is too complicated for it to be used automatically in
logic programming, so we just prove a specific form to add as a hint.
|
Lemma compile_sound_var : forall G m (s : Subst _ G) s',
Subst_lr compile_ty (val_lr m) s s'
-> forall t v, val_lr m t (VarDenote v s) (VarDenote (VarConvert compile_ty v) s').
intros.
apply Subst_lr_Var; trivial.
Qed.
Hint Resolve compile_sound_var.
| A key lemma in the final proof, which we've almost reached. It allows us to replace a memory in a particular form of monad spec with another memory that is extended by the original. |
Lemma mspec_switch : forall m1 ran apped v0 m,
mspec (fun m'' v =>
extends m1 m'' /\ val_lr m'' ran v0 v)
apped m1
-> extends m m1
-> mspec (fun m'' v =>
extends m m'' /\ val_lr m'' ran v0 v)
apped m1.
unfold mspec; intros; destruct H; eauto.
Qed.
Hint Resolve mspec_switch.
| A trivial rephrasing of a fact to help unification |
Lemma nat_Slr : forall G m t d (s : Subst _ G) v s',
Subst_lr compile_ty (val_lr m)
(SCons (Data t) d s)
(SCons (compile_ty (Data t)) v s')
-> Subst_lr compile_ty (val_lr m)
(SCons (Data t) d s)
(SCons (IData INat) v s').
trivial.
Qed.
Hint Resolve nat_Slr.
Our workshorse tactic, which instantiates a general forward reasoning tactic
in Binding.
|
Ltac my_crush :=
crush
| First, we give a tactic that decides, given the type of a universally quantified variable in an assumption, whether we should try all in-scope variables of that type as possible instantiations. Here, we choose to try this for all types. |
ltac:(fun T => idtac)
| Next, an analagous "predicate" for deciding whether to look for possible instantiations that are subterms of the conclusion. Here, we choose to try this only for substitutions. |
ltac:(fun T => match T with
| Subst _ _ => idtac
end)
This tactic decides when the result of fully instantiating a quantified
assumption is "useful".
Here, the result is "useful" when it makes an mspec statement about the
same program and memory that the conclusion does.
|
ltac:(fun E => match E with
| mspec _ ?V1 ?M1 =>
match goal with
| [ |- mspec _ ?V2 ?M2 ] =>
check_eq V1 V2;
check_eq M1 M2
end
end)
This is a simplification procedure to apply at several points during proof
search.
We drop most of the work onto the Monad library.
|
ltac:(try match goal with
| [ H : match ?E with inl _ => _ | inr _ => _ end |- _ ] =>
destruct E
end; memM_simplify; try (rewriteNat; memM_simplify))
This is a "solver" tactic to apply repeatedly at places where we hope that
the remaining goal is "easy."
Again, Monad does most of the work.
|
ltac:(memM_simplify; eauto 7).
Monad can help us prove extends facts easily.
|
Hint Extern 2 (extends _ _) => memM_simplify.
| The final soundness proof! Any expression inhabits the expression LR with its compilation. |
Theorem compile_sound : forall G t (e : term G t),
exp_lr e (compile_term e).
induction e; unfold exp_lr in *; my_crush.
Qed.
| With that theorem proved, this one comes quite easily. |
Theorem compile_sound_Nat : forall (e : term nil (Data Nat)) m,
mspec (fun _ n => termDenote e (SNil _) = n)
(itermDenote (compile_term e) (SNil _)) m.
intros.
generalize (compile_sound e m (Slr_Nil _ _ _ _)).
unfold mspec; intuition.
Qed.