Library langs.L1.type_soundness
Require Import scopes frames L1.syntax L1.well_typedness L1.well_boundness L1.semantics.
Section TypeSoundness.
Context `{G: Graph (@AT T)}.
Section TypeSoundness.
Context `{G: Graph (@AT T)}.
Inductive vtyp' (h:H) : V → T → Prop :=
| vtyp'_n : ∀ z, vtyp' h (NumV z) Tint
| vtyp'_c : ∀
d e f t1 t2 sp
(FS: scopeofFrame h f sp)
(WT: wt_exp (E sp (Tarrow t1 t2) (Fn d t1 e)))
(WB: wb_exp (E sp (Tarrow t1 t2) (Fn d t1 e))),
vtyp' h (ClosV d e f) (Tarrow t1 t2)
.
Hint Constructors vtyp' : sgraph.
vtyp is preserved by the following frame operations.
Lemma setSlot_vtyp' :
∀ h0 f d v h1 v0 t0
(SET: setSlot h0 f d v h1)
(VT: vtyp' h0 v0 t0),
vtyp' h1 v0 t0.
Proof.
intros; inv SET; induction VT; sgauto.
econstructor; sgauto. inv FS. destruct (FrameIdDec f f0); subst.
- rewrite H1 in H0; inv H0. econstructor; rewrite get_set_same; eauto.
- econstructor; rewrite get_set_other; eauto.
Qed.
Lemma newFrame_vtyp' :
∀
h0 s f h1 ks v0 t0
(NF: newFrame h0 s ks f h1)
(VT: vtyp' h0 v0 t0),
vtyp' h1 v0 t0.
Proof.
intros; inv NF; induction VT; sgauto.
econstructor; sgauto. inv FS. destruct (FrameIdDec f f0); subst.
- apply keys_in in H0; contradiction.
- econstructor; rewrite get_set_other; eauto.
Qed.
Lemma fillFrame_vtyp' :
∀
slots f h1 h2 v0 t0
(FF: fillFrame f h1 slots h2)
(VT: vtyp' h1 v0 t0),
vtyp' h2 v0 t0.
Proof.
intros; destruct FF as [? [? [? [? ?]]]]; subst; induction VT; sgauto.
econstructor; sgauto. inv FS. destruct (FrameIdDec f f0); subst.
- rewrite H in H0; inv H0. econstructor; rewrite get_set_same; eauto.
- econstructor; rewrite get_set_other; eauto.
Qed.
Hint Resolve setSlot_vtyp : sgraph.
Hint Resolve newFrame_vtyp : sgraph.
Hint Resolve fillFrame_vtyp : sgraph.
The VTyp type class is instantiated using the lemmas above.
Instance VT : VTyp.
Proof.
econstructor.
apply setSlot_vtyp'.
apply newFrame_vtyp'.
apply fillFrame_vtyp'.
Defined.
Proof.
econstructor.
apply setSlot_vtyp'.
apply newFrame_vtyp'.
apply fillFrame_vtyp'.
Defined.
Lemma eval_exp_scopeofFrame :
∀ h0 f0 e v h1,
eval_exp h0 f0 e v h1 →
∀ f s,
scopeofFrame h0 f s →
scopeofFrame h1 f s.
Proof.
induction 1; intros; sgauto.
Qed.
∀ h0 f0 e v h1,
eval_exp h0 f0 e v h1 →
∀ f s,
scopeofFrame h0 f s →
scopeofFrame h1 f s.
Proof.
induction 1; intros; sgauto.
Qed.
Hint Constructors vtyp' : pres.
Hint Constructors wb_exp wt_exp : pres.
Hint Resolve eval_exp_scopeofFrame : pres.
Hint Resolve initFrameSame_scopeofFrame : pres.
Hint Resolve initFrame_good_heap1 : pres.
Hint Resolve initFrame_good_heap0 : pres.
Hint Resolve setSlot_good_heap : pres.
Hint Resolve setSlot_vtyp' : pres.
Hint Resolve setSlotScope : pres.
Ltac peauto := eauto with pres.
Hint Constructors wb_exp wt_exp : pres.
Hint Resolve eval_exp_scopeofFrame : pres.
Hint Resolve initFrameSame_scopeofFrame : pres.
Hint Resolve initFrame_good_heap1 : pres.
Hint Resolve initFrame_good_heap0 : pres.
Hint Resolve setSlot_good_heap : pres.
Hint Resolve setSlot_vtyp' : pres.
Hint Resolve setSlotScope : pres.
Ltac peauto := eauto with pres.
We prove that expressions are type sound. This is Theorem 2 in
the paper:
Lemma exp_preservation:
(∀ h0 f e v h1
(EVAL: eval_exp h0 f e v h1)
s t pe
(UNPACK: e = (E s t pe))
(FS: scopeofFrame h0 f s)
(GH: good_heap h0)
(WT: wt_exp (E s t pe))
(WB: wb_exp (E s t pe)),
(good_heap h1 ∧ vtyp h1 v t)).
Proof.
induction 1; intros; simpl; try (inv UNPACK; inv WT; inv WB); subst; try (peauto; fail).
-
edestruct IHEVAL1; peauto.
edestruct IHEVAL2; peauto.
-
edestruct IHEVAL; peauto.
inv H0; edestruct ABORTL; sgauto.
-
edestruct IHEVAL2; peauto.
edestruct IHEVAL1; peauto.
inv H0; edestruct ABORTR; sgauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
eapply getAddrDet in ADDR; eauto; inv ADDR.
split; auto.
edestruct GH as [WB WT]. inv SF. eapply keys_in in H. apply H.
inv WT.
eapply scopeofFrameDet in SF; eauto; subst.
eapply declsofScopeDet in DS; eauto; subst.
eapply rlookupDet in DR; eauto; subst. destruct DR as [? [? ?]]; subst.
eapply WT0; peauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
exfalso. eapply ADDR; eauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
eapply getAddrDet in ADDR; eauto; inv ADDR.
edestruct GH as [WB WT]. inversion SF. eapply keys_in; eauto.
edestruct well_bound_get as [v P]; eauto.
exfalso. eapply NGET; eauto.
-
edestruct IHEVAL1; eauto.
edestruct IHEVAL2; peauto. inv H0. inv WT. inv WB. inv H3.
edestruct IHEVAL3; peauto.
assert (SF':scopeofFrame h2 ff sp0) by peauto.
eapply scopeofFrameDet in SF; eauto; subst.
eapply initFrame_good_heap1; peauto.
intros.
simpl in IN. inv IN; try contradiction.
simpl in GET. destruct (Ddec d0 d0); inv GET.
eapply typofDeclDet in TD0; eauto; subst.
assumption.
-
edestruct IHEVAL; peauto. destruct v1; inv ABORT1; inv H0.
-
edestruct IHEVAL1; peauto.
edestruct IHEVAL2; peauto. inv H2.
Qed.
Theorem prog_sound :
∀
p v
(WT: wt_prog p)
(WB: wb_prog p)
(EVAL: eval_prog p v),
¬ v = AbortV Wrong.
Proof.
intros. inv EVAL.
inv WT. simpl in TOPFRM.
inv WB.
assert (scopeofFrame h0 f s0) by peauto.
assert (good_heap emptyHeap) by inversion 1.
assert (good_heap h0) by peauto.
edestruct exp_preservation as [? ?]; peauto.
intro; subst v. inv H3.
Qed.
End TypeSoundness.
(∀ h0 f e v h1
(EVAL: eval_exp h0 f e v h1)
s t pe
(UNPACK: e = (E s t pe))
(FS: scopeofFrame h0 f s)
(GH: good_heap h0)
(WT: wt_exp (E s t pe))
(WB: wb_exp (E s t pe)),
(good_heap h1 ∧ vtyp h1 v t)).
Proof.
induction 1; intros; simpl; try (inv UNPACK; inv WT; inv WB); subst; try (peauto; fail).
-
edestruct IHEVAL1; peauto.
edestruct IHEVAL2; peauto.
-
edestruct IHEVAL; peauto.
inv H0; edestruct ABORTL; sgauto.
-
edestruct IHEVAL2; peauto.
edestruct IHEVAL1; peauto.
inv H0; edestruct ABORTR; sgauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
eapply getAddrDet in ADDR; eauto; inv ADDR.
split; auto.
edestruct GH as [WB WT]. inv SF. eapply keys_in in H. apply H.
inv WT.
eapply scopeofFrameDet in SF; eauto; subst.
eapply declsofScopeDet in DS; eauto; subst.
eapply rlookupDet in DR; eauto; subst. destruct DR as [? [? ?]]; subst.
eapply WT0; peauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
exfalso. eapply ADDR; eauto.
-
edestruct good_addr as [? [ADDR' [SF [? [DS IN]]]]]; eauto.
eapply getAddrDet in ADDR; eauto; inv ADDR.
edestruct GH as [WB WT]. inversion SF. eapply keys_in; eauto.
edestruct well_bound_get as [v P]; eauto.
exfalso. eapply NGET; eauto.
-
edestruct IHEVAL1; eauto.
edestruct IHEVAL2; peauto. inv H0. inv WT. inv WB. inv H3.
edestruct IHEVAL3; peauto.
assert (SF':scopeofFrame h2 ff sp0) by peauto.
eapply scopeofFrameDet in SF; eauto; subst.
eapply initFrame_good_heap1; peauto.
intros.
simpl in IN. inv IN; try contradiction.
simpl in GET. destruct (Ddec d0 d0); inv GET.
eapply typofDeclDet in TD0; eauto; subst.
assumption.
-
edestruct IHEVAL; peauto. destruct v1; inv ABORT1; inv H0.
-
edestruct IHEVAL1; peauto.
edestruct IHEVAL2; peauto. inv H2.
Qed.
Theorem prog_sound :
∀
p v
(WT: wt_prog p)
(WB: wb_prog p)
(EVAL: eval_prog p v),
¬ v = AbortV Wrong.
Proof.
intros. inv EVAL.
inv WT. simpl in TOPFRM.
inv WB.
assert (scopeofFrame h0 f s0) by peauto.
assert (good_heap emptyHeap) by inversion 1.
assert (good_heap h0) by peauto.
edestruct exp_preservation as [? ?]; peauto.
intro; subst v. inv H3.
Qed.
End TypeSoundness.