Library framework.frames
Definition FrameId := nat.
Lemma FrameIdDec : ∀ (frm1 frm2:FrameId), {frm1 = frm2} + {frm1 ≠ frm2}.
Proof.
repeat (decide equality).
Qed.
A heap H is represented as a finite map from FrameIds to Frames.
A Frame consists of:
- A ScopeId.
- A set of linked scopes, represented as a (curried) finite map from EdgeLabels and ScopeIds to FrameIds.
- A set of slots, represented as a finite map from Declarations to Values.
Class FrameHeap {V : Type} :=
{ Frame := ((ScopeId × (map EdgeLabel (map ScopeId FrameId)))%type × map D V)%type ;
H := map FrameId Frame
}.
Section FrameHeapProperties.
Context `{FH : FrameHeap}.
Extracting frame components
Inductive scopeofFrame (h: H) (f: FrameId) (s: ScopeId) : Prop :=
| scopeofFrame_ :
∀ ks slots,
get FrameIdDec h f = Some (s, ks, slots) →
scopeofFrame h f s.
Lemma scopeofFrameDet :
∀ h f s,
scopeofFrame h f s →
∀ s',
scopeofFrame h f s' →
s = s'.
Proof.
do 2 inversion 1. rewrite H3 in H1. inv H1; auto.
Qed.
Lemma scopeofFrameFrame :
∀ h f s,
scopeofFrame h f s →
frame h f.
Proof.
inversion 1; unfold frame; eauto using keys_in.
Qed.
linksofFrame h f ks says that ks is the finite map of links
from frame f in heap h. (Corresponds to (K_h(f)) in the Fig. 12
in the paper.)
Inductive linksofFrame (h: H) (f: FrameId) (ks: map EdgeLabel (map ScopeId FrameId)) : Prop :=
| linksofFrame_ :
∀ s slots,
get FrameIdDec h f = Some (s, ks, slots) →
linksofFrame h f ks.
Lemma linksofFrameDet :
∀ ks ks' h f ,
linksofFrame h f ks →
linksofFrame h f ks' → ks = ks'.
Proof.
induction ks; intros.
- inv H0. inv H1. rewrite H0 in H2. inv H2; eauto.
- inv H0. inv H1. rewrite H0 in H2. inv H2; eauto.
Qed.
llinksofFrame h f l ks says that ks is the finite map of
links for edge label l from frame f in heap h.
Inductive llinksofFrame (h: H) (f: FrameId) (l: EdgeLabel) (lks: map ScopeId FrameId) : Prop :=
| llinksofFrame_ :
∀ ks,
linksofFrame h f ks →
get ELdec ks l = Some lks →
llinksofFrame h f l lks.
Lemma llinksofFrameDet :
∀ ks ks' h f l,
llinksofFrame h f l ks →
llinksofFrame h f l ks' → ks = ks'.
Proof.
induction ks; intros.
- inv H0. inv H1.
eapply linksofFrameDet in H2; eauto; subst.
rewrite H4 in H3. inv H3; eauto.
- inv H0. inv H1.
eapply linksofFrameDet in H2; eauto; subst.
rewrite H4 in H3. inv H3; eauto.
Qed.
Getting all slots of a frame. (Corresponds to (D_h(f)) in the
Fig. 12 in the paper.)
Inductive slotsofFrame (heap: H) (f: FrameId) (slots:map D V) : Prop :=
| getSlots_ : ∀
scope links,
get FrameIdDec heap f = Some (scope, links, slots) →
slotsofFrame heap f slots.
Lemma slotsofFrameDet:
∀ h f slots1 slots2,
slotsofFrame h f slots1 →
slotsofFrame h f slots2 →
slots1 = slots2.
Proof.
intros. inv H0. inv H1.
rewrite H0 in H2; inv H2; auto.
Qed.
| getSlots_ : ∀
scope links,
get FrameIdDec heap f = Some (scope, links, slots) →
slotsofFrame heap f slots.
Lemma slotsofFrameDet:
∀ h f slots1 slots2,
slotsofFrame h f slots1 →
slotsofFrame h f slots2 →
slots1 = slots2.
Proof.
intros. inv H0. inv H1.
rewrite H0 in H2; inv H2; auto.
Qed.
Getting value from a slot. (Corresponds to the [GetSlot] rule
in Fig. 12 in the paper.)
Inductive getSlot (heap: H) (f: FrameId) (d: D) (v: V) : Prop :=
| getSlot_ : ∀
scope links slots,
get FrameIdDec heap f = Some (scope, links, slots) →
Some v = get Ddec slots d →
getSlot heap f d v.
Lemma getSlotDet:
∀ h f d v1 v2,
getSlot h f d v1 →
getSlot h f d v2 →
v1 = v2.
Proof.
intros. inv H0. inv H1.
rewrite H0 in H2; inv H2. rewrite <- H4 in H3; inv H3; auto.
Qed.
Lemma getSlotFrame :
∀ h f d v,
getSlot h f d v →
frame h f.
Proof.
intros. inv H0. eapply keys_in; eauto.
Qed.
| getSlot_ : ∀
scope links slots,
get FrameIdDec heap f = Some (scope, links, slots) →
Some v = get Ddec slots d →
getSlot heap f d v.
Lemma getSlotDet:
∀ h f d v1 v2,
getSlot h f d v1 →
getSlot h f d v2 →
v1 = v2.
Proof.
intros. inv H0. inv H1.
rewrite H0 in H2; inv H2. rewrite <- H4 in H3; inv H3; auto.
Qed.
Lemma getSlotFrame :
∀ h f d v,
getSlot h f d v →
frame h f.
Proof.
intros. inv H0. eapply keys_in; eauto.
Qed.
Definition emptyHeap : H := empty.
Lemma emptyHeapNoFrames :
∀ f,
¬ frame emptyHeap f.
Proof.
intros. intro. unfold frame, emptyHeap in H0. simpl in H0. auto.
Qed.
Adding a new frame, whose FrameId is required to be fresh,
with no slots.
Definition newFrame
(h: H)
(s: ScopeId)
(ks: map EdgeLabel (map ScopeId FrameId))
(f: FrameId)
(h': H) : Prop :=
¬ In f (keys h) ∧
h' = set FrameIdDec h f (s, ks, empty).
Lemma newFrameNew :
∀ h0 s ks f h1,
newFrame h0 s ks f h1 →
¬ frame h0 f.
Proof.
intros. inv H0. auto.
Qed.
Lemma newFrameFrames :
∀ h0 s ks f0 h1,
newFrame h0 s ks f0 h1 →
∀ f,
frame h1 f ↔ f = f0 ∨ frame h0 f.
Proof.
intros. inv H0. split; intros.
unfold frame in H1.
eapply in_keys_set; eauto.
eapply set_in_keys; eauto.
Qed.
Lemma newFrameSame :
∀ h0 s ks frm h1,
newFrame h0 s ks frm h1 →
get FrameIdDec h1 frm = Some (s, ks, []).
Proof.
intros. inv H0. eapply get_set_same.
Qed.
Lemma newFrameDiff :
∀ h0 f0 s0 ks0 slots0 s ks f h1,
get FrameIdDec h0 f0 = Some (s0, ks0, slots0) →
newFrame h0 s ks f h1 →
get FrameIdDec h1 f0 = Some (s0, ks0, slots0).
Proof.
intros. inv H1. inv H0. rewrite get_set_other; eauto.
intro; subst. eapply keys_in in H3. contradiction.
Qed.
Lemma newFrameDiff' :
∀ h0 s frm0 frm1 h1 ks ds s' ks',
get FrameIdDec h1 frm0 = Some (s, ks, ds) →
frm0 ≠ frm1 →
newFrame h0 s' ks' frm1 h1 →
get FrameIdDec h0 frm0 = Some (s, ks, ds).
Proof.
intros. inv H2. rewrite get_set_other in H0; eauto.
Qed.
Lemma newFrameSlotSame :
∀ s frm h0 h1 d v ks,
newFrame h0 s ks frm h1 →
¬ getSlot h1 frm d v.
Proof.
intros. inv H0. intro. inv H0. rewrite get_set_same in H2. inv H2. inv H3.
Qed.
Lemma newFrameSlotDiff :
∀ s frm0 frm1 h0 h1 d v ks,
getSlot h0 frm0 d v →
newFrame h0 s ks frm1 h1 →
getSlot h1 frm0 d v .
Proof.
intros. inv H1. inv H0. econstructor; eauto. rewrite get_set_other; eauto.
eapply keys_in in H1. intro; subst; contradiction.
Qed.
Lemma newFrameSlotDiff':
∀ s frm0 frm1 h0 h1 d v ks,
getSlot h1 frm0 d v →
newFrame h0 s ks frm1 h1 →
frm0 ≠ frm1 →
getSlot h0 frm0 d v .
Proof.
intros. inv H1. inv H0. rewrite get_set_other in H1; auto.
econstructor; eauto.
Qed.
(h: H)
(s: ScopeId)
(ks: map EdgeLabel (map ScopeId FrameId))
(f: FrameId)
(h': H) : Prop :=
¬ In f (keys h) ∧
h' = set FrameIdDec h f (s, ks, empty).
Lemma newFrameNew :
∀ h0 s ks f h1,
newFrame h0 s ks f h1 →
¬ frame h0 f.
Proof.
intros. inv H0. auto.
Qed.
Lemma newFrameFrames :
∀ h0 s ks f0 h1,
newFrame h0 s ks f0 h1 →
∀ f,
frame h1 f ↔ f = f0 ∨ frame h0 f.
Proof.
intros. inv H0. split; intros.
unfold frame in H1.
eapply in_keys_set; eauto.
eapply set_in_keys; eauto.
Qed.
Lemma newFrameSame :
∀ h0 s ks frm h1,
newFrame h0 s ks frm h1 →
get FrameIdDec h1 frm = Some (s, ks, []).
Proof.
intros. inv H0. eapply get_set_same.
Qed.
Lemma newFrameDiff :
∀ h0 f0 s0 ks0 slots0 s ks f h1,
get FrameIdDec h0 f0 = Some (s0, ks0, slots0) →
newFrame h0 s ks f h1 →
get FrameIdDec h1 f0 = Some (s0, ks0, slots0).
Proof.
intros. inv H1. inv H0. rewrite get_set_other; eauto.
intro; subst. eapply keys_in in H3. contradiction.
Qed.
Lemma newFrameDiff' :
∀ h0 s frm0 frm1 h1 ks ds s' ks',
get FrameIdDec h1 frm0 = Some (s, ks, ds) →
frm0 ≠ frm1 →
newFrame h0 s' ks' frm1 h1 →
get FrameIdDec h0 frm0 = Some (s, ks, ds).
Proof.
intros. inv H2. rewrite get_set_other in H0; eauto.
Qed.
Lemma newFrameSlotSame :
∀ s frm h0 h1 d v ks,
newFrame h0 s ks frm h1 →
¬ getSlot h1 frm d v.
Proof.
intros. inv H0. intro. inv H0. rewrite get_set_same in H2. inv H2. inv H3.
Qed.
Lemma newFrameSlotDiff :
∀ s frm0 frm1 h0 h1 d v ks,
getSlot h0 frm0 d v →
newFrame h0 s ks frm1 h1 →
getSlot h1 frm0 d v .
Proof.
intros. inv H1. inv H0. econstructor; eauto. rewrite get_set_other; eauto.
eapply keys_in in H1. intro; subst; contradiction.
Qed.
Lemma newFrameSlotDiff':
∀ s frm0 frm1 h0 h1 d v ks,
getSlot h1 frm0 d v →
newFrame h0 s ks frm1 h1 →
frm0 ≠ frm1 →
getSlot h0 frm0 d v .
Proof.
intros. inv H1. inv H0. rewrite get_set_other in H1; auto.
econstructor; eauto.
Qed.
Filling all slots of a frame at once.
Definition fillFrame (f: FrameId) (h0: H) (slots: map D V) (h1: H) : Prop :=
∃ s ks slots0,
get FrameIdDec h0 f = Some (s, ks, slots0) ∧
h1 = set FrameIdDec h0 f (s, ks, slots).
Lemma fillFrameFrames :
∀ f0 h0 slots h1,
fillFrame f0 h0 slots h1 →
∀ f, frame h0 f ↔ frame h1 f.
Proof.
intros. destruct H0 as [? [? [? [GF SF]]]]. subst.
split; unfold frame; intro. simpl.
destruct (FrameIdDec f0 f); auto. right.
eapply remove_in_keys; eauto.
destruct (FrameIdDec f0 f); auto.
simpl in H0. inv H0. eapply keys_in; eauto. eapply keys_in; eauto.
simpl in H0. inv H0; [intuition|]. eapply in_keys_remove; eauto.
Qed.
Hint Resolve fillFrameFrames : sgraph.
Lemma fillFrameSame :
∀
h0 f slots h1
(FF: fillFrame f h0 slots h1)
scope links slots0
(GF: get FrameIdDec h0 f = Some (scope, links, slots0)),
get FrameIdDec h1 f = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_same. rewrite GF in GF'. inv GF'; auto.
Qed.
Lemma fillFrameSame' :
∀
h0 f slots h1
(FF: fillFrame f h0 slots h1)
scope links slots
(GF: get FrameIdDec h1 f = Some (scope, links, slots)),
∃ slots', get FrameIdDec h0 f = Some (scope, links, slots').
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_same in GF. inv GF. eauto.
Qed.
Hint Resolve fillFrameSame' : sgraph.
Lemma fillFrameDiff :
∀
h0 f1 slots h1
(FF: fillFrame f1 h0 slots h1)
f0 scope links slots
(NEQ: f0 ≠ f1)
(GF: get FrameIdDec h0 f0 = Some (scope, links, slots)),
get FrameIdDec h1 f0 = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_other; auto.
Qed.
Lemma fillFrameDiff' :
∀
h0 f1 slots h1
(FF: fillFrame f1 h0 slots h1)
f0 scope links slots
(NEQ: f0 ≠ f1)
(GF: get FrameIdDec h1 f0 = Some (scope, links, slots)),
get FrameIdDec h0 f0 = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_other in GF; auto.
Qed.
Lemma fillFrameSlotDiff :
∀ h0 f0 d v f1 h1 slots,
fillFrame f1 h0 slots h1 →
getSlot h0 f0 d v →
f0 ≠ f1 →
getSlot h1 f0 d v.
Proof.
intros. inversion H0 as [? [? [? [GF' SF]]]]. subst.
inv H1. econstructor. rewrite get_set_other; eauto. assumption.
Qed.
Lemma fillFrameSlotDiff' :
∀ h0 f0 d v f1 h1 slots,
fillFrame f1 h0 slots h1 →
getSlot h1 f0 d v →
f0 ≠ f1 →
getSlot h0 f0 d v.
Proof.
intros; inversion H0 as [? [? [? [GF' SF]]]]. subst.
inv H1. rewrite get_set_other in H3; eauto. econstructor; eauto.
Qed.
∃ s ks slots0,
get FrameIdDec h0 f = Some (s, ks, slots0) ∧
h1 = set FrameIdDec h0 f (s, ks, slots).
Lemma fillFrameFrames :
∀ f0 h0 slots h1,
fillFrame f0 h0 slots h1 →
∀ f, frame h0 f ↔ frame h1 f.
Proof.
intros. destruct H0 as [? [? [? [GF SF]]]]. subst.
split; unfold frame; intro. simpl.
destruct (FrameIdDec f0 f); auto. right.
eapply remove_in_keys; eauto.
destruct (FrameIdDec f0 f); auto.
simpl in H0. inv H0. eapply keys_in; eauto. eapply keys_in; eauto.
simpl in H0. inv H0; [intuition|]. eapply in_keys_remove; eauto.
Qed.
Hint Resolve fillFrameFrames : sgraph.
Lemma fillFrameSame :
∀
h0 f slots h1
(FF: fillFrame f h0 slots h1)
scope links slots0
(GF: get FrameIdDec h0 f = Some (scope, links, slots0)),
get FrameIdDec h1 f = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_same. rewrite GF in GF'. inv GF'; auto.
Qed.
Lemma fillFrameSame' :
∀
h0 f slots h1
(FF: fillFrame f h0 slots h1)
scope links slots
(GF: get FrameIdDec h1 f = Some (scope, links, slots)),
∃ slots', get FrameIdDec h0 f = Some (scope, links, slots').
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_same in GF. inv GF. eauto.
Qed.
Hint Resolve fillFrameSame' : sgraph.
Lemma fillFrameDiff :
∀
h0 f1 slots h1
(FF: fillFrame f1 h0 slots h1)
f0 scope links slots
(NEQ: f0 ≠ f1)
(GF: get FrameIdDec h0 f0 = Some (scope, links, slots)),
get FrameIdDec h1 f0 = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_other; auto.
Qed.
Lemma fillFrameDiff' :
∀
h0 f1 slots h1
(FF: fillFrame f1 h0 slots h1)
f0 scope links slots
(NEQ: f0 ≠ f1)
(GF: get FrameIdDec h1 f0 = Some (scope, links, slots)),
get FrameIdDec h0 f0 = Some (scope, links, slots).
Proof.
intros; destruct FF as [? [? [? [GF' SF]]]]. subst.
rewrite get_set_other in GF; auto.
Qed.
Lemma fillFrameSlotDiff :
∀ h0 f0 d v f1 h1 slots,
fillFrame f1 h0 slots h1 →
getSlot h0 f0 d v →
f0 ≠ f1 →
getSlot h1 f0 d v.
Proof.
intros. inversion H0 as [? [? [? [GF' SF]]]]. subst.
inv H1. econstructor. rewrite get_set_other; eauto. assumption.
Qed.
Lemma fillFrameSlotDiff' :
∀ h0 f0 d v f1 h1 slots,
fillFrame f1 h0 slots h1 →
getSlot h1 f0 d v →
f0 ≠ f1 →
getSlot h0 f0 d v.
Proof.
intros; inversion H0 as [? [? [? [GF' SF]]]]. subst.
inv H1. rewrite get_set_other in H3; eauto. econstructor; eauto.
Qed.
Create and fully initialize a frame from a list of
values. (Corresponds to [initFrame] defined in Fig. 12 in the
paper.)
Inductive initFrame
(h1: H)
(s: ScopeId)
(ks: map EdgeLabel (map ScopeId FrameId))
(slots: map D V)
(f: FrameId)
(h3: H) : Prop :=
| initFrame_ : ∀
h2
(NF: newFrame h1 s ks f h2)
(FF: fillFrame f h2 slots h3),
initFrame h1 s ks slots f h3.
Lemma initFrameFrames :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
∀ f, f = f0 ∨ frame h0 f ↔ frame h1 f.
Proof.
intros. inv H0. eapply iff_trans.
eapply iff_sym. eapply newFrameFrames; eauto.
eapply fillFrameFrames; eauto.
Qed.
Lemma initFrameSame :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
∃ slots, get FrameIdDec h1 f0 = Some (s, ks, slots).
Proof.
intros. inversion H0.
eapply newFrameSame in NF; eauto. inv NF.
eapply fillFrameSame in FF; eauto.
Qed.
Lemma initFrameDiff :
∀ h0 f0 s ks slots f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
get FrameIdDec h0 f0 = Some (s, ks, slots) →
get FrameIdDec h1 f0 = Some (s, ks, slots).
Proof.
intros. inv H0.
assert (get FrameIdDec h2 f0 = Some (s, ks, slots)).
eapply newFrameDiff; eauto. inv NF.
eapply fillFrameDiff; eauto.
intro. subst. eapply keys_in in H1. contradiction.
Qed.
Lemma initFrameDiff' :
∀ h0 f0 s ks slots f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
get FrameIdDec h1 f0 = Some (s, ks, slots) →
f ≠ f0 →
get FrameIdDec h0 f0 = Some (s, ks, slots).
Proof.
intros. inv H0.
eauto using fillFrameDiff', newFrameDiff'.
Qed.
Lemma initFrameSlotDiff' :
∀ f0 d v f h1 vs ks s h0,
initFrame h0 s ks vs f h1 →
getSlot h1 f0 d v →
f0 ≠ f →
getSlot h0 f0 d v.
Proof.
intros. inv H0.
eapply newFrameSlotDiff'. 2: eauto. 2: auto. eapply fillFrameSlotDiff'; eauto.
Qed.
Lemma initFrameSame_scopeofFrame :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
scopeofFrame h1 f0 s.
Proof.
intros. eapply initFrameSame in H0. inv H0; econstructor; eauto.
Qed.
Lemma initFrameDiff_scopeofFrame :
∀ h0 f0 s f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
scopeofFrame h0 f0 s →
scopeofFrame h1 f0 s.
Proof.
intros. inv H1. eapply initFrameDiff in H2; eauto; inv H2; econstructor; eauto.
Qed.
(h1: H)
(s: ScopeId)
(ks: map EdgeLabel (map ScopeId FrameId))
(slots: map D V)
(f: FrameId)
(h3: H) : Prop :=
| initFrame_ : ∀
h2
(NF: newFrame h1 s ks f h2)
(FF: fillFrame f h2 slots h3),
initFrame h1 s ks slots f h3.
Lemma initFrameFrames :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
∀ f, f = f0 ∨ frame h0 f ↔ frame h1 f.
Proof.
intros. inv H0. eapply iff_trans.
eapply iff_sym. eapply newFrameFrames; eauto.
eapply fillFrameFrames; eauto.
Qed.
Lemma initFrameSame :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
∃ slots, get FrameIdDec h1 f0 = Some (s, ks, slots).
Proof.
intros. inversion H0.
eapply newFrameSame in NF; eauto. inv NF.
eapply fillFrameSame in FF; eauto.
Qed.
Lemma initFrameDiff :
∀ h0 f0 s ks slots f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
get FrameIdDec h0 f0 = Some (s, ks, slots) →
get FrameIdDec h1 f0 = Some (s, ks, slots).
Proof.
intros. inv H0.
assert (get FrameIdDec h2 f0 = Some (s, ks, slots)).
eapply newFrameDiff; eauto. inv NF.
eapply fillFrameDiff; eauto.
intro. subst. eapply keys_in in H1. contradiction.
Qed.
Lemma initFrameDiff' :
∀ h0 f0 s ks slots f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
get FrameIdDec h1 f0 = Some (s, ks, slots) →
f ≠ f0 →
get FrameIdDec h0 f0 = Some (s, ks, slots).
Proof.
intros. inv H0.
eauto using fillFrameDiff', newFrameDiff'.
Qed.
Lemma initFrameSlotDiff' :
∀ f0 d v f h1 vs ks s h0,
initFrame h0 s ks vs f h1 →
getSlot h1 f0 d v →
f0 ≠ f →
getSlot h0 f0 d v.
Proof.
intros. inv H0.
eapply newFrameSlotDiff'. 2: eauto. 2: auto. eapply fillFrameSlotDiff'; eauto.
Qed.
Lemma initFrameSame_scopeofFrame :
∀ h0 s ks vs f0 h1,
initFrame h0 s ks vs f0 h1 →
scopeofFrame h1 f0 s.
Proof.
intros. eapply initFrameSame in H0. inv H0; econstructor; eauto.
Qed.
Lemma initFrameDiff_scopeofFrame :
∀ h0 f0 s f h1 s' ks' vs',
initFrame h0 s' ks' vs' f h1 →
scopeofFrame h0 f0 s →
scopeofFrame h1 f0 s.
Proof.
intros. inv H1. eapply initFrameDiff in H2; eauto; inv H2; econstructor; eauto.
Qed.
Setting a slot that already has a value. (Corresponding to
[SetSlot] in Fig. 20 in the paper.)
Inductive setSlot (h: H) (f:FrameId) (d:D) (v:V) (h': H) : Prop :=
| setSlot_ :
∀
scope links slots slots',
In d (keys slots) →
get FrameIdDec h f = Some (scope, links, slots) →
slots' = set Ddec slots d v →
h' = set FrameIdDec h f (scope, links, slots') →
setSlot h f d v h'.
Lemma setSlotFrame :
∀ h0 f d v h1,
setSlot h0 f d v h1 →
frame h0 f.
Proof.
intros. inv H0. apply keys_in in H2. auto.
Qed.
Lemma setSlotFrames :
∀ h0 d v h1 f0,
setSlot h0 f0 d v h1 →
∀ f,
frame h0 f ↔ frame h1 f.
Proof.
intros. split; intros.
inv H0. eapply set_in_keys. auto.
inv H0.
unfold frame in H1; apply in_keys_set in H1. inv H1; subst.
eapply keys_in; eauto.
auto.
Qed.
Lemma setSlotSlotSame:
∀ frm d v h0 h1,
setSlot h0 frm d v h1 →
getSlot h1 frm d v.
Proof.
intros. inv H0. econstructor.
rewrite get_set_same; eauto.
rewrite get_set_same; auto.
Qed.
Lemma setSlotSlotDiff :
∀ frm0 frm1 d0 d1 v0 v1 h0 h1,
getSlot h0 frm0 d0 v0 →
setSlot h0 frm1 d1 v1 h1 →
frm1 ≠ frm0 ∨ d1 ≠ d0 →
getSlot h1 frm0 d0 v0.
Proof.
intros. inv H0. inv H1. destruct H2.
econstructor; eauto. rewrite get_set_other; eauto.
destruct (FrameIdDec frm1 frm0); subst.
rewrite H3 in H5; inv H5.
econstructor. rewrite get_set_same; eauto.
rewrite get_set_other; eauto.
econstructor; eauto. rewrite get_set_other; eauto.
Qed.
Lemma setSlotSlotDiff' :
∀ frm0 frm1 d0 d1 v0 v1 h0 h1,
setSlot h0 frm1 d1 v1 h1 →
getSlot h1 frm0 d0 v0 →
frm1 ≠ frm0 ∨ d1 ≠ d0 →
getSlot h0 frm0 d0 v0.
Proof.
intros. inv H0. inv H1. destruct H2.
rewrite get_set_other in H0.
econstructor; eauto. intro. subst. apply H1; auto.
destruct (FrameIdDec frm1 frm0); subst.
rewrite get_set_same in H0. inv H0; subst.
econstructor; eauto.
rewrite get_set_other in H5. eauto. intro. subst. apply H1; auto.
rewrite get_set_other in H0. econstructor; eauto.
intro. subst. apply n; auto.
Qed.
Lemma setSlotSame :
∀ h0 frm0 frm1 d v h1 scope links slots,
setSlot h0 frm1 d v h1 →
get FrameIdDec h0 frm0 = Some (scope, links, slots) →
∃ slots, get FrameIdDec h1 frm0 = Some (scope, links, slots).
Proof.
intros. inv H0.
destruct (FrameIdDec frm1 frm0); subst.
unfold Frame in *; rewrite H1 in H3; inv H3. rewrite get_set_same. eexists; eauto.
rewrite get_set_other. eexists; eauto. intuition.
Qed.
Lemma setSlotScope :
∀
h0 frm0 frm1 s d v h1,
setSlot h0 frm1 d v h1 →
scopeofFrame h0 frm0 s →
scopeofFrame h1 frm0 s.
Proof.
inversion 1; intros; subst.
eapply setSlotSame in H0; eauto.
destruct H0. inv H5. destruct (FrameIdDec frm0 frm1). subst.
rewrite H3 in H2; inv H2. econstructor; eauto.
econstructor. rewrite get_set_other; eauto.
Qed.
| setSlot_ :
∀
scope links slots slots',
In d (keys slots) →
get FrameIdDec h f = Some (scope, links, slots) →
slots' = set Ddec slots d v →
h' = set FrameIdDec h f (scope, links, slots') →
setSlot h f d v h'.
Lemma setSlotFrame :
∀ h0 f d v h1,
setSlot h0 f d v h1 →
frame h0 f.
Proof.
intros. inv H0. apply keys_in in H2. auto.
Qed.
Lemma setSlotFrames :
∀ h0 d v h1 f0,
setSlot h0 f0 d v h1 →
∀ f,
frame h0 f ↔ frame h1 f.
Proof.
intros. split; intros.
inv H0. eapply set_in_keys. auto.
inv H0.
unfold frame in H1; apply in_keys_set in H1. inv H1; subst.
eapply keys_in; eauto.
auto.
Qed.
Lemma setSlotSlotSame:
∀ frm d v h0 h1,
setSlot h0 frm d v h1 →
getSlot h1 frm d v.
Proof.
intros. inv H0. econstructor.
rewrite get_set_same; eauto.
rewrite get_set_same; auto.
Qed.
Lemma setSlotSlotDiff :
∀ frm0 frm1 d0 d1 v0 v1 h0 h1,
getSlot h0 frm0 d0 v0 →
setSlot h0 frm1 d1 v1 h1 →
frm1 ≠ frm0 ∨ d1 ≠ d0 →
getSlot h1 frm0 d0 v0.
Proof.
intros. inv H0. inv H1. destruct H2.
econstructor; eauto. rewrite get_set_other; eauto.
destruct (FrameIdDec frm1 frm0); subst.
rewrite H3 in H5; inv H5.
econstructor. rewrite get_set_same; eauto.
rewrite get_set_other; eauto.
econstructor; eauto. rewrite get_set_other; eauto.
Qed.
Lemma setSlotSlotDiff' :
∀ frm0 frm1 d0 d1 v0 v1 h0 h1,
setSlot h0 frm1 d1 v1 h1 →
getSlot h1 frm0 d0 v0 →
frm1 ≠ frm0 ∨ d1 ≠ d0 →
getSlot h0 frm0 d0 v0.
Proof.
intros. inv H0. inv H1. destruct H2.
rewrite get_set_other in H0.
econstructor; eauto. intro. subst. apply H1; auto.
destruct (FrameIdDec frm1 frm0); subst.
rewrite get_set_same in H0. inv H0; subst.
econstructor; eauto.
rewrite get_set_other in H5. eauto. intro. subst. apply H1; auto.
rewrite get_set_other in H0. econstructor; eauto.
intro. subst. apply n; auto.
Qed.
Lemma setSlotSame :
∀ h0 frm0 frm1 d v h1 scope links slots,
setSlot h0 frm1 d v h1 →
get FrameIdDec h0 frm0 = Some (scope, links, slots) →
∃ slots, get FrameIdDec h1 frm0 = Some (scope, links, slots).
Proof.
intros. inv H0.
destruct (FrameIdDec frm1 frm0); subst.
unfold Frame in *; rewrite H1 in H3; inv H3. rewrite get_set_same. eexists; eauto.
rewrite get_set_other. eexists; eauto. intuition.
Qed.
Lemma setSlotScope :
∀
h0 frm0 frm1 s d v h1,
setSlot h0 frm1 d v h1 →
scopeofFrame h0 frm0 s →
scopeofFrame h1 frm0 s.
Proof.
inversion 1; intros; subst.
eapply setSlotSame in H0; eauto.
destruct H0. inv H5. destruct (FrameIdDec frm0 frm1). subst.
rewrite H3 in H2; inv H2. econstructor; eauto.
econstructor. rewrite get_set_other; eauto.
Qed.
Removing a frame.
Definition removeFrame (h0: H) (f:FrameId) (h1: H) : Prop :=
h1 = remove FrameIdDec h0 f.
Lemma removeFrameFrames0:
∀ h0 f h1 f0,
removeFrame h0 f h1 →
(frame h1 f0 ↔ (f ≠ f0 ∧ frame h0 f0)).
Proof.
intros. unfold frame. inv H0. split; intros. apply in_keys_remove in H0. intuition.
eapply remove_in_keys; intuition.
Qed.
Lemma removeFrameFrames:
∀ h0 f h1 f0,
removeFrame h0 f h1 →
f ≠ f0 →
frame h0 f0 →
frame h1 f0.
Proof.
unfold frame; intros. inv H0. eapply remove_in_keys; eauto.
Qed.
Lemma removeFrameFrames':
∀ h0 f h1 f0,
removeFrame h0 f h1 →
frame h1 f0 →
(f ≠ f0 ∧ frame h0 f0).
Proof.
unfold frame; intros. inv H0. apply in_keys_remove in H1. intuition.
Qed.
Lemma removeFrameSame :
∀ h0 frm0 s0 ks0 slots0 h1 frm,
removeFrame h0 frm h1 →
(get FrameIdDec h1 frm0 = Some (s0, ks0, slots0) ↔
(get FrameIdDec h0 frm0 = Some (s0, ks0, slots0) ∧ frm ≠ frm0)).
Proof.
intros. split; intros.
inv H1. inv H0.
destruct (FrameIdDec frm frm0); subst.
rewrite get_remove_same in H3. inv H3.
rewrite get_remove_other in H3; eauto.
erewrite get_remove_other; eauto.
inv H0. inv H1; eauto.
rewrite get_remove_other; eauto.
Qed.
Lemma removeFrameScope:
∀ h0 frm0 s0 h1 frm,
removeFrame h0 frm h1 →
(scopeofFrame h1 frm0 s0 ↔ (scopeofFrame h0 frm0 s0 ∧ frm ≠ frm0)).
Proof.
intros. split;intros.
inv H1. eapply removeFrameSame in H2; eauto. destruct H2. split; eauto.
econstructor; eauto.
destruct H1. inv H1. econstructor. eapply removeFrameSame; eauto.
Qed.
Lemma removeFrameSlot :
∀ h0 f0 d v f h1,
removeFrame h0 f h1 →
(getSlot h1 f0 d v ↔ (getSlot h0 f0 d v ∧ f ≠ f0)).
Proof.
intros. inv H0. split; intros.
inv H0. inv H1. destruct (FrameIdDec f f0); subst.
rewrite get_remove_same in H3; inv H3.
rewrite get_remove_other in H3; eauto. split; eauto.
inv H3. inv H2; econstructor; eauto.
inv H0. inv H1.
econstructor; eauto. erewrite get_remove_other; eauto.
Qed.
h1 = remove FrameIdDec h0 f.
Lemma removeFrameFrames0:
∀ h0 f h1 f0,
removeFrame h0 f h1 →
(frame h1 f0 ↔ (f ≠ f0 ∧ frame h0 f0)).
Proof.
intros. unfold frame. inv H0. split; intros. apply in_keys_remove in H0. intuition.
eapply remove_in_keys; intuition.
Qed.
Lemma removeFrameFrames:
∀ h0 f h1 f0,
removeFrame h0 f h1 →
f ≠ f0 →
frame h0 f0 →
frame h1 f0.
Proof.
unfold frame; intros. inv H0. eapply remove_in_keys; eauto.
Qed.
Lemma removeFrameFrames':
∀ h0 f h1 f0,
removeFrame h0 f h1 →
frame h1 f0 →
(f ≠ f0 ∧ frame h0 f0).
Proof.
unfold frame; intros. inv H0. apply in_keys_remove in H1. intuition.
Qed.
Lemma removeFrameSame :
∀ h0 frm0 s0 ks0 slots0 h1 frm,
removeFrame h0 frm h1 →
(get FrameIdDec h1 frm0 = Some (s0, ks0, slots0) ↔
(get FrameIdDec h0 frm0 = Some (s0, ks0, slots0) ∧ frm ≠ frm0)).
Proof.
intros. split; intros.
inv H1. inv H0.
destruct (FrameIdDec frm frm0); subst.
rewrite get_remove_same in H3. inv H3.
rewrite get_remove_other in H3; eauto.
erewrite get_remove_other; eauto.
inv H0. inv H1; eauto.
rewrite get_remove_other; eauto.
Qed.
Lemma removeFrameScope:
∀ h0 frm0 s0 h1 frm,
removeFrame h0 frm h1 →
(scopeofFrame h1 frm0 s0 ↔ (scopeofFrame h0 frm0 s0 ∧ frm ≠ frm0)).
Proof.
intros. split;intros.
inv H1. eapply removeFrameSame in H2; eauto. destruct H2. split; eauto.
econstructor; eauto.
destruct H1. inv H1. econstructor. eapply removeFrameSame; eauto.
Qed.
Lemma removeFrameSlot :
∀ h0 f0 d v f h1,
removeFrame h0 f h1 →
(getSlot h1 f0 d v ↔ (getSlot h0 f0 d v ∧ f ≠ f0)).
Proof.
intros. inv H0. split; intros.
inv H0. inv H1. destruct (FrameIdDec f f0); subst.
rewrite get_remove_same in H3; inv H3.
rewrite get_remove_other in H3; eauto. split; eauto.
inv H3. inv H2; econstructor; eauto.
inv H0. inv H1.
econstructor; eauto. erewrite get_remove_other; eauto.
Qed.
Removing multiple frames.
Inductive removeFrames : H → list FrameId → H → Prop :=
| rfs_nil :
∀ h0, removeFrames h0 [] h0
| rfs_cons :
∀ h0 h1 h2 f fs,
removeFrame h0 f h1 →
removeFrames h1 fs h2 →
removeFrames h0 (f::fs) h2.
Lemma removeFramesFrames :
∀ h0 fs h1 f0,
removeFrames h0 fs h1 → (frame h1 f0 ↔ (¬ In f0 fs ∧ frame h0 f0)).
Proof.
intros.
induction H0; intros.
intuition.
eapply removeFrameFrames0 with (f0:=f0) in H0.
split; intros.
rewrite IHremoveFrames in H2. destruct H2. rewrite H0 in H3. destruct H3.
split; auto. intro; exfalso. inv H5. eapply H3; eauto. eapply H2; contradiction.
rewrite IHremoveFrames. destruct H2. split. intro. apply H2. right; auto.
eapply H0. split; auto. intro; eapply H2; left; auto.
Qed.
Lemma removeFramesSame :
∀ h0 frm0 s0 h1 frms ks0 slots0,
removeFrames h0 frms h1 →
(get FrameIdDec h1 frm0 = Some (s0, ks0, slots0) ↔
(¬ In frm0 frms ∧ get FrameIdDec h0 frm0 = Some (s0, ks0, slots0))).
Proof.
intros. induction H0; intros.
intuition.
eapply removeFrameSame with (frm0:=frm0) (s0:=s0) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
Lemma removeFramesScope: ∀ h0 frm0 s0 h1 frms,
removeFrames h0 frms h1 →
(scopeofFrame h1 frm0 s0 ↔ (¬ In frm0 frms ∧ scopeofFrame h0 frm0 s0)).
Proof.
intros. induction H0; intros.
intuition.
eapply removeFrameScope with (frm0 := frm0) (s0:=s0) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
Lemma removeFramesSlot :
∀ h0 f0 d v fs h1,
removeFrames h0 fs h1 →
(getSlot h1 f0 d v ↔ (¬ In f0 fs ∧ getSlot h0 f0 d v)).
Proof.
intros.
induction H0.
intuition.
eapply removeFrameSlot with (h0:= h0) (f := f) (h1:=h1) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
| rfs_nil :
∀ h0, removeFrames h0 [] h0
| rfs_cons :
∀ h0 h1 h2 f fs,
removeFrame h0 f h1 →
removeFrames h1 fs h2 →
removeFrames h0 (f::fs) h2.
Lemma removeFramesFrames :
∀ h0 fs h1 f0,
removeFrames h0 fs h1 → (frame h1 f0 ↔ (¬ In f0 fs ∧ frame h0 f0)).
Proof.
intros.
induction H0; intros.
intuition.
eapply removeFrameFrames0 with (f0:=f0) in H0.
split; intros.
rewrite IHremoveFrames in H2. destruct H2. rewrite H0 in H3. destruct H3.
split; auto. intro; exfalso. inv H5. eapply H3; eauto. eapply H2; contradiction.
rewrite IHremoveFrames. destruct H2. split. intro. apply H2. right; auto.
eapply H0. split; auto. intro; eapply H2; left; auto.
Qed.
Lemma removeFramesSame :
∀ h0 frm0 s0 h1 frms ks0 slots0,
removeFrames h0 frms h1 →
(get FrameIdDec h1 frm0 = Some (s0, ks0, slots0) ↔
(¬ In frm0 frms ∧ get FrameIdDec h0 frm0 = Some (s0, ks0, slots0))).
Proof.
intros. induction H0; intros.
intuition.
eapply removeFrameSame with (frm0:=frm0) (s0:=s0) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
Lemma removeFramesScope: ∀ h0 frm0 s0 h1 frms,
removeFrames h0 frms h1 →
(scopeofFrame h1 frm0 s0 ↔ (¬ In frm0 frms ∧ scopeofFrame h0 frm0 s0)).
Proof.
intros. induction H0; intros.
intuition.
eapply removeFrameScope with (frm0 := frm0) (s0:=s0) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
Lemma removeFramesSlot :
∀ h0 f0 d v fs h1,
removeFrames h0 fs h1 →
(getSlot h1 f0 d v ↔ (¬ In f0 fs ∧ getSlot h0 f0 d v)).
Proof.
intros.
induction H0.
intuition.
eapply removeFrameSlot with (h0:= h0) (f := f) (h1:=h1) in H0.
split; intros.
eapply IHremoveFrames in H2. inv H2. eapply H0 in H4. inv H4.
split. intro. inv H4. apply H5; auto. contradiction. auto.
inv H2. eapply IHremoveFrames; eauto. split.
intro. eapply H3; right; auto.
erewrite H0. split; auto.
intro; subst; eapply H3; left; auto.
Qed.
Dynamic lookup by path.
Inductive lookup (h: H) : FrameId → path → D → FrameId → Prop :=
| lookupD : ∀ f d,
(∃ v, getSlot h f d v) →
lookup h f (Dp d) d f
| lookupI : ∀
f p f' f'' l s ks d
(IMS: llinksofFrame h f l ks)
(S: get ScopeIdDec ks s = Some f')
(REST: lookup h f' p d f''),
lookup h f (Ep l s p) d f''
.
Lemma lookupDet :
∀ h f p d1 f1,
lookup h f p d1 f1 →
∀ d2 f2,
lookup h f p d2 f2 → d1 = d2 ∧ f1 = f2.
Proof.
induction 1; intros.
- inv H1; auto.
- inv H1. eapply llinksofFrameDet in IMS; eauto; subst.
rewrite S in S0; inv S0; eauto.
Qed.
getAddr h f r addr says that addr is the address of the
slot to which reference r resolves, starting from frame f.
Inductive getAddr (h: H) (f: FrameId) (r: R) : Addr → Prop :=
| getAddr_ :
∀
p f' d
(PATH: pathofRefP r p)
(LK: lookup h f p d f'),
getAddr h f r (Addr_ f' d).
Lemma getAddrDet :
∀ h f r a1 a2,
getAddr h f r a1 →
getAddr h f r a2 →
a1 = a2.
Proof.
intros. inv H0. inv H1.
pose proof (pathofRefDet _ _ PATH _ PATH0). subst p0. clear PATH0.
eapply lookupDet in LK; eauto. destruct LK; subst; eauto.
Qed.
getRef h f r v says that v is the value in the slot
address to which reference r resolves, starting from frame f.
Inductive getRef (h: H) (f:FrameId) (r: R) (v: V) : Prop :=
| getRef_ : ∀
ff d
(ADDR: getAddr h f r (Addr_ ff d))
(SLOT: getSlot h ff d v),
getRef h f r v.
Lemma getRefDet :
∀ h f r v1 v2,
getRef h f r v1 → getRef h f r v2 → v1 = v2.
Proof.
intros. inv H0. inv H1.
pose proof (getAddrDet _ _ _ _ _ ADDR ADDR0). inv H0. clear ADDR0.
eapply getSlotDet; eauto.
Qed.
End CombiningStaticAndDynamic.
End FrameHeapProperties.
Hint Constructors Addr : sgraph.
Hint Constructors getAddr : sgraph.
Hint Constructors slotsofFrame : sgraph.
Hint Constructors getSlot : sgraph.
Hint Constructors typofDecl : sgraph.
Hint Constructors scopeofFrame : sgraph.
Hint Constructors linksofFrame : sgraph.
Hint Constructors llinksofFrame : sgraph.
Hint Constructors lookup : sgraph.
Hint Resolve scopeofFrameFrame : sgraph.
Hint Resolve setSlotSlotSame : sgraph.
Hint Resolve getAddrDet : sgraph.
Hint Resolve getRefDet : sgraph.
Hint Resolve fillFrameSame : sgraph.
Hint Resolve fillFrameDiff : sgraph.
Hint Resolve fillFrameDiff : sgraph.
Hint Resolve initFrameSame_scopeofFrame : sgraph.
Hint Resolve initFrameSame : sgraph.
Hint Resolve initFrameDiff_scopeofFrame : sgraph.
Hint Resolve initFrameDiff : sgraph.
Hint Resolve initFrameSlotDiff' : sgraph.
Hint Resolve setSlotScope : sgraph.
| getRef_ : ∀
ff d
(ADDR: getAddr h f r (Addr_ ff d))
(SLOT: getSlot h ff d v),
getRef h f r v.
Lemma getRefDet :
∀ h f r v1 v2,
getRef h f r v1 → getRef h f r v2 → v1 = v2.
Proof.
intros. inv H0. inv H1.
pose proof (getAddrDet _ _ _ _ _ ADDR ADDR0). inv H0. clear ADDR0.
eapply getSlotDet; eauto.
Qed.
End CombiningStaticAndDynamic.
End FrameHeapProperties.
Hint Constructors Addr : sgraph.
Hint Constructors getAddr : sgraph.
Hint Constructors slotsofFrame : sgraph.
Hint Constructors getSlot : sgraph.
Hint Constructors typofDecl : sgraph.
Hint Constructors scopeofFrame : sgraph.
Hint Constructors linksofFrame : sgraph.
Hint Constructors llinksofFrame : sgraph.
Hint Constructors lookup : sgraph.
Hint Resolve scopeofFrameFrame : sgraph.
Hint Resolve setSlotSlotSame : sgraph.
Hint Resolve getAddrDet : sgraph.
Hint Resolve getRefDet : sgraph.
Hint Resolve fillFrameSame : sgraph.
Hint Resolve fillFrameDiff : sgraph.
Hint Resolve fillFrameDiff : sgraph.
Hint Resolve initFrameSame_scopeofFrame : sgraph.
Hint Resolve initFrameSame : sgraph.
Hint Resolve initFrameDiff_scopeofFrame : sgraph.
Hint Resolve initFrameDiff : sgraph.
Hint Resolve initFrameSlotDiff' : sgraph.
Hint Resolve setSlotScope : sgraph.
Definition of value typing.
Class VTyp {T: Type} `{dwc: Graph (@AT T)} `{fh: FrameHeap} :=
{ vtyp : H → V → T → Prop ;
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 ;
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 ;
fillFrame_vtyp :
∀
slots f h1 h2 v0 t0
(FF: fillFrame f h1 slots h2)
(VT: vtyp h1 v0 t0),
vtyp h2 v0 t0;
}.
Section VTypProperties.
Context `{VT : VTyp}.
Lemma initFrame_vtyp :
∀
h0 s ks slots f h1 v0 t0
(INF: initFrame h0 s ks slots f h1)
(VTYP: vtyp h0 v0 t0),
vtyp h1 v0 t0.
Proof.
inversion 1; intros. eapply fillFrame_vtyp; eauto. eapply newFrame_vtyp; eauto.
Qed.
End VTypProperties.
WellBound declarations
(DSS: ∀ ds,
ddataofScopeP s ds →
∃ slots, slotsofFrame h f slots ∧ DomEq slots ds)
(DSF: ∀ slots,
slotsofFrame h f slots →
∃ ds, ddataofScopeP s ds ∧ DomEq slots ds)
ddataofScopeP s ds →
∃ slots, slotsofFrame h f slots ∧ DomEq slots ds)
(DSF: ∀ slots,
slotsofFrame h f slots →
∃ ds, ddataofScopeP s ds ∧ DomEq slots ds)
WellBound links:
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ ks,
llinksofFrame h f l ks ∧
keys ks = ss ∧
∀ s',
In s' ss →
∃ f', get ScopeIdDec ks s' = Some f' ∧
scopeofFrame h f' s')
(LNF: ∀ l ks,
llinksofFrame h f l ks →
llinksofScopeP s l (keys ks)),
well_bound h f.
llinksofScopeP s l ss →
∃ ks,
llinksofFrame h f l ks ∧
keys ks = ss ∧
∀ s',
In s' ss →
∃ f', get ScopeIdDec ks s' = Some f' ∧
scopeofFrame h f' s')
(LNF: ∀ l ks,
llinksofFrame h f l ks →
llinksofScopeP s l (keys ks)),
well_bound h f.
The formalization of well-boundness above differs slightly from
Figure 15 in the paper. The differences are mainly due to
differences in representation. In particular:
Below, we prove that the formulation of well_bound guarantees
that: (a) the slots of a frame are in one-to-one correspondence with
the declarations in the frame’s scope; (b) the links of a frame are
in one-to-one correspondence with the labeled edges of the frame’s
scope, and the scope of each link target matches the corresponding
edge target. (Figure 4 in the paper illustrates the resulting
commuting diagram.)
- K(s)(l) as defined in the paper (Figure 5) returns an empty set if
s has no l-labeled edges; in contrast, llinksofScope s l ks
fails if s has no l-labeled edges; and
- The paper uses sets to represent links and labeled edges, whereas this artifact uses lists.
Lemma wb_representation_sound :
∀ h f,
well_bound h f →
∃ s, scopeofFrame h f s ∧
(∃ ds slots, ddataofScopeP s ds ∧
slotsofFrame h f slots ∧ DomEq ds slots) ∧
(∀ l s', ((∃ ks, llinksofScopeP s l ks ∧ In s' ks) ↔
(∃ ks', llinksofFrame h f l ks' ∧
∃ f', get ScopeIdDec ks' s' = Some f' ∧
scopeofFrame h f' s'))) ∧
(∀ l ks, llinksofScopeP s l ks ↔ (∃ ks', llinksofFrame h f l ks' ∧ keys ks' = ks)).
Proof.
destruct 1. eexists; split; eauto.
split.
- inversion SC. edestruct DSF. econstructor; eauto. destruct H1.
do 2 eexists; split; sgauto. split; sgauto. unfold DomEq in H2.
split; intros; eauto. apply H2; auto. apply H2; auto.
- intros. split; intros. split; intros.
+ destruct H0 as [? [? ?]]. edestruct LNS as [? [? [? ?]]]; eauto.
+ destruct H0 as [? [? [? [? ?]]]]. edestruct LNF as [? [? ?]]; eauto.
eexists; split; eauto. eapply keys_in; eauto.
+ split; intros. eapply LNS in H0.
destruct H0 as [? [? [? ?]]]. subst. eauto.
destruct H0 as [? [? ?]]. subst. eauto.
Qed.
Lemma wb_representation_complete :
∀ h f s,
scopeofFrame h f s ∧
((∃ ds slots, ddataofScopeP s ds ∧
slotsofFrame h f slots ∧ DomEq ds slots) ∧
(∀ l s', ((∃ ks, llinksofScopeP s l ks ∧ In s' ks) ↔
(∃ ks', llinksofFrame h f l ks' ∧
∃ f', get ScopeIdDec ks' s' = Some f' ∧
scopeofFrame h f' s')))) →
(∀ l ks, llinksofScopeP s l ks ↔ (∃ ks', llinksofFrame h f l ks' ∧ keys ks' = ks)) →
well_bound h f.
Proof.
destruct 1 as [? [[? [? [? [? ?]]]] ?]].
econstructor; sgauto; intros.
- eapply ddataofScopeDet in H1; eauto; subst.
eexists; split; sgauto. intros; split; intro; eapply H3; eauto.
- eapply slotsofFrameDet in H2; eauto; subst.
eexists; split; sgauto. intros; split; intro; eapply H3; eauto.
- assert ((∃ s', In s' ss) ∨ ss = nil).
{ destruct ss; eauto. left; eexists; econstructor; eauto. }
destruct H7 as [[? ?]|].
+ assert (IFF:=H4). specialize (H4 l x1).
destruct H4. edestruct H4; sgauto.
destruct H9 as [? [? [? ?]]].
eexists; split; eauto. split.
edestruct H5. edestruct H12 as [? [? ?]]; eauto.
eapply llinksofFrameDet in H9; eauto; subst. auto.
intros.
specialize (IFF l s'). destruct IFF.
edestruct H13 as [? [? ?]]; eauto.
eapply llinksofFrameDet in H9; eauto; subst. eauto.
+ subst. edestruct H4.
specialize (H5 l []). simpl in H5. destruct H5. eapply H5 in H6.
edestruct H5 as [? [? ?]]; eauto. destruct x1; inv H11.
eexists; split; eauto. simpl. split. split; auto.
inversion 1.
- apply H5. eauto.
Grab Existential Variables. assumption. assumption.
Qed.
Inductive well_typed (h: H) (f: FrameId) : Prop :=
| well_typed_ :
∀
s
(SC: scopeofFrame h f s)
ds
(DS: declsofScopeP s ds)
(WT: ∀ d t v,
In d ds →
typofDecl d t →
getSlot h f d v →
vtyp h v t),
well_typed h f.
Definition good_frame h f := well_bound h f ∧ well_typed h f.
Definition good_heap h := ∀ f, frame h f → good_frame h f.
Hint Constructors well_bound : sgraph.
Hint Constructors well_typed : sgraph.
Lemma well_bound_get :
∀ h f s d ds
(WB: well_bound h f)
(SF: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∃ v, getSlot h f d v.
Proof.
intros. inv WB.
eapply scopeofFrameDet in SF; eauto; subst.
inv DS. inv H0.
edestruct DSS as [slots [GS DE]]; eauto.
inv GS.
assert (In d (keys slots)) by (apply DE; auto).
eapply in_keys in H2. destruct H2 as [v P].
∃ v; econstructor; eauto.
Qed.
Lemma well_bound_set:
∀
h f s ds d
(WB: well_bound h f)
(SC: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∀ v,
∃ h', setSlot h f d v h'.
Proof.
intros. inv WB. eapply scopeofFrameDet in SC; eauto; subst.
inv DS. destruct H0. subst. inv H0.
assert (ddataofScopeP s x) by sgauto.
eapply DSS in H0. destruct H0 as [? [? ?]].
destruct H0. inv SC0. erewrite H3 in H0; inv H0.
eexists. econstructor; sgauto. eapply H1. assumption.
Qed.
Lemma setSlot_well_bound :
∀
h0 f d v h1
(SET: setSlot h0 f d v h1)
(WB: well_bound h0 f),
well_bound h1 f.
Proof.
intros; inv WB; sgauto.
inversion SET; subst. inversion SC. rewrite H2 in H1; inv H1.
econstructor.
- econstructor; eauto. rewrite get_set_same; eauto.
- intros. eapply DSS in H1. inv H1. inv H3.
eexists; split. econstructor. simpl. destruct (FrameIdDec f f); [|intuition]. clear e.
eauto. eapply DomEq_set; eauto.
inv H1. rewrite H3 in H2. inv H2. auto.
- intros. inv H1. rewrite get_set_same in H3. inv H3.
assert (slotsofFrame h0 f slots). econstructor; eauto.
eapply DSF in H1. inv H1. inv H3. eexists; split; eauto.
eapply DomEq_set; eauto.
- intros. eapply LNS in H1; eauto.
destruct H1 as [? [LLN [KS SS]]]. subst. inv LLN.
eexists; split; eauto. econstructor; eauto. inv H1. rewrite H4 in H2. inv H2.
econstructor. rewrite get_set_same; eauto.
split; auto. intros. apply SS in H4. destruct H4 as [? [? ?]].
eexists; split; eauto. inv H5.
destruct (FrameIdDec f x0). subst.
rewrite H2 in H6. inv H6.
econstructor. rewrite get_set_same; eauto.
econstructor. rewrite get_set_other; eauto.
- intros. inv H1. inv H3. rewrite get_set_same in H1. inv H1.
assert (llinksofFrame h0 f l ks).
econstructor; eauto. econstructor; eauto.
eapply LNF in H1. auto.
Qed.
Lemma setSlot_well_typed :
∀
h0 f d v h1 t
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: well_typed h0 f),
well_typed h1 f.
Proof.
intros; inv WT; sgauto.
inversion SET; subst. inversion SC. rewrite H2 in H1; inv H1.
econstructor; eauto.
- econstructor; eauto. rewrite get_set_same; eauto.
- intros. inv H4. rewrite get_set_same in H5. inv H5.
eapply setSlot_vtyp; eauto. simpl in H6.
destruct (Ddec d0 d); subst. inv H6. simpl in H3. eapply typofDeclDet in TD; eauto; subst; eauto.
eapply WT0 in H1; eauto. econstructor; eauto. assert (d ≠ d0). intuition.
apply get_remove_other with (Kdec:=Ddec) (m:=slots) in H4.
rewrite H4 in H6. auto.
Qed.
Hint Resolve setSlot_well_bound : sgraph.
Hint Resolve setSlot_well_typed : sgraph.
Hint Unfold good_frame : sgraph.
Lemma setSlot_good_frame :
∀
h0 f d v h1 t
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: good_frame h0 f),
good_frame h1 f.
Proof.
intros. inv WT. sgauto.
Qed.
Hint Resolve setSlot_good_frame : sgraph.
Lemma setSlot_other_well_bound :
∀
h0 f d v h1 f0
(SET: setSlot h0 f d v h1)
(WB: well_bound h0 f0)
(DIFF: f ≠ f0),
well_bound h1 f0.
Proof.
intros; inv WB; sgauto. inv SC; inv SET.
econstructor.
- econstructor; eauto. rewrite get_set_other; eauto.
- intros. eapply DSS in H3. destruct H3 as [? [? ?]]. inv H3. rewrite H5 in H0; inv H0.
eexists; split; eauto. econstructor; rewrite get_set_other; eauto.
- intros. inv H3. rewrite get_set_other in H4; [|intuition]. rewrite H4 in H0; inv H0.
assert (slotsofFrame h0 f0 slots). econstructor; eauto. eauto.
- intros. eapply LNS in H3. destruct H3 as [? [? [? ?]]]; subst.
inv H3. inv H4. rewrite H3 in H0; inv H0.
eexists; split; eauto. econstructor; sgauto. econstructor; rewrite get_set_other; eauto.
split; eauto. intros. eapply H5 in H0. destruct H0 as [? [? ?]].
inv H4.
eexists; split; eauto. destruct (FrameIdDec x0 f); subst.
rewrite H7 in H2; inv H2. econstructor; rewrite get_set_same; sgauto.
econstructor; rewrite get_set_other; sgauto.
- intros. inv H3. inv H4. rewrite get_set_other in H3; auto. rewrite H3 in H0; inv H0.
assert (llinksofFrame h0 f0 l ks0); sgauto.
Qed.
Lemma setSlot_other_well_typed :
∀
h0 f d v h1 t f0
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: well_typed h0 f0)
(DIFF: f ≠ f0),
well_typed h1 f0.
Proof.
intros; inv WT. inv SC; inv SET.
econstructor; eauto.
- econstructor; rewrite get_set_other; eauto.
- intros. inv H5. rewrite get_set_other in H6; eauto.
eapply setSlot_vtyp. econstructor; eauto. eapply WT0; eauto. econstructor; eauto.
Qed.
Hint Resolve setSlot_other_well_bound : sgraph.
Hint Resolve setSlot_other_well_typed : sgraph.
Lemma setSlot_other_good_frame :
∀
h0 f d v h1 t f0
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: good_frame h0 f0)
(DIFF: f ≠ f0),
good_frame h1 f0.
Proof.
intros; inv WT; sgauto.
Qed.
Lemma initFrame_other_well_bound :
∀
h0 s ks vs f h1
(INIT: initFrame h0 s ks vs f h1)
f'
(WB: well_bound h0 f'),
well_bound h1 f'.
Proof.
intros; inv WB. inv INIT.
assert (NF':=NF); eapply newFrameSame in NF'.
assert (FF':=FF); eapply fillFrameSame in FF; eauto. inv FF.
inv NF. rewrite get_set_same in NF'. inv NF'.
inv SC.
assert (f' ≠ f). intro. subst. apply H0. eapply keys_in; eauto.
assert (FF'':=FF').
eapply fillFrameDiff in FF'; eauto. Focus 2.
apply get_set_other with (Kdec:=FrameIdDec) (m:=h0) (v:=(s, ks, empty)) in H3.
rewrite H3. eauto.
econstructor; sgauto.
- intros. eapply DSS in H4. destruct H4 as [? [GS DE]].
eexists; split; sgauto. inv GS. rewrite H4 in H2. inv H2. auto.
- intros. inversion H4. rewrite H5 in FF'. inv FF'.
assert (slotsofFrame h0 f' slots). econstructor; eauto.
eauto.
- intros. eapply LNS in H4. destruct H4 as [? [LL [KS GS]]].
inv LL. inv H4. rewrite H6 in H2. inv H2.
eexists; split. econstructor; eauto. econstructor; eauto.
split; eauto. intros. eapply GS in H2.
destruct H2 as [? [? ?]]; eexists; split; eauto.
inv H4.
destruct (FrameIdDec x0 f). subst. destruct H0. eapply keys_in in H7; auto.
destruct (FrameIdDec x0 f'). subst.
rewrite H7 in H6; inv H6.
econstructor; eauto.
eapply fillFrameDiff in FF''; eauto.
econstructor. eauto. rewrite get_set_other; eauto.
- intros.
assert (llinksofFrame h0 f' l ks1).
inv H4. inv H5. rewrite H4 in FF'. inv FF'. econstructor; sgauto.
eapply LNF in H5; eauto.
Qed.
Lemma initFrame_other_well_typed :
∀
h0 s ks slots f h1
(INIT: initFrame h0 s ks slots f h1)
slots
(TDs: declsofScopeP s (@keys D V slots))
f'
(WT: well_typed h0 f'),
well_typed h1 f'.
Proof.
intros. inv INIT.
assert (NF':=NF); eapply newFrameSame in NF'.
assert (FF':=FF); eapply fillFrameSame in FF; eauto. inv FF.
inversion NF; subst. rewrite get_set_same in NF'. inv NF'. inv WT. inv SC.
assert (f' ≠ f). intro. subst. apply H0. eapply keys_in; eauto.
assert (FF'':=FF').
eapply fillFrameDiff in FF'; eauto. Focus 2.
apply get_set_other with (Kdec:=FrameIdDec) (m:=h0) (v:=(s, ks, empty)) in H3.
rewrite H3. eauto.
econstructor; sgauto. intros.
eapply fillFrame_vtyp in FF''; eauto.
eapply newFrame_vtyp in NF; eauto.
inv H6. rewrite H7 in FF'; inv FF'.
eapply WT0; eauto. econstructor; eauto.
Qed.
Hint Resolve initFrame_other_well_bound : sgraph.
Hint Resolve initFrame_other_well_typed : sgraph.
Lemma initFrame_other_good_frame :
∀
h0 s ks slots f h1
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
f'
(GF: good_frame h0 f'),
good_frame h1 f'.
Proof.
intros; inv GF; sgauto.
Qed.
Lemma initFrame_well_bound :
∀
h0 s ks slots f h1
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
well_bound h1 f.
Proof.
intros; inv INIT. inv NF. assert (FF':=FF).
eapply fillFrameSame in FF; try rewrite get_set_same; eauto.
eexists; sgauto.
- intros.
assert (declsofScopeP s (keys ds)) by (econstructor; eauto).
eapply declsofScopeDet in TDs; eauto; subst.
eexists; split; sgauto. split; rewrite <- TDs; auto.
- intros. inv H1. rewrite H2 in FF; inv FF. inv TDs. inv H1.
eexists; split; sgauto. split; rewrite <- H4; auto.
- intros. eapply LNS in H1. destruct H1 as [? [M [KS SF]]]. subst.
eexists; split. econstructor; eauto. econstructor; eauto.
split; eauto. intros. apply SF in H1. destruct H1 as [? [GS SF']]. inv SF'.
assert (x0 ≠ f). intro. subst. apply keys_in in H1. contradiction.
eapply fillFrameDiff in FF'; eauto. Focus 2. rewrite get_set_other; eauto.
eexists; split; sgauto.
- intros. inv H1. inv H2. rewrite H1 in FF; inv FF.
apply LNF in H3; auto.
Qed.
Lemma initFrame_well_bound1 :
∀
h0 s slots f h1 l sl fl
(INIT: initFrame h0 s [(l, [(sl, fl)])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(LNS: linksofScopeP s [(l, [sl])])
(SL: scopeofFrame h0 fl sl),
well_bound h1 f.
Proof.
intros; eapply initFrame_well_bound; eauto.
intros. inv H0. inv H1. eapply linksofScopeDet in LNS; eauto; subst.
destruct (ELdec l0 l). subst; simpl in ×. destruct (ELdec l l); [|intuition].
inv H2. eexists; split; eauto. split; eauto. intros. inv H1.
eexists; split; eauto. simpl. destruct (ScopeIdDec s0 s0); intuition.
inv H2. simpl in H2. destruct (ELdec l0 l); intuition. inv H2.
intros. simpl in H0. destruct (ELdec l0 l); intuition. subst. inv H0.
inv LNS. econstructor; split; eauto. simpl. destruct (ELdec l l); intuition.
inv H0.
Qed.
Lemma initFrame_well_bound2 :
∀
h0 s slots f h1 l sl fl l' sl' fl'
(INIT: initFrame h0 s [(l, [(sl, fl)]); (l', [(sl', fl')])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(LNS: linksofScopeP s [(l, [sl]); (l', [sl'])])
(SL: scopeofFrame h0 fl sl)
(SL: scopeofFrame h0 fl' sl'),
well_bound h1 f.
Proof.
intros; eapply initFrame_well_bound; eauto.
intros. inv H0. inv H1. eapply linksofScopeDet in LNS; eauto; subst.
destruct (ELdec l0 l). subst; simpl in ×. destruct (ELdec l l); [|intuition].
inv H2. eexists; split; eauto. split; eauto. intros. inv H1.
eexists; split; eauto. simpl. destruct (ScopeIdDec s0 s0); intuition.
inv H2. simpl in H2. simpl.
destruct (ELdec l0 l); intuition.
destruct (ELdec l0 l'); intuition.
subst. inv H2. eexists; split; simpl; sgauto. split; sgauto. intros.
destruct H1; inv H1. simpl. destruct (ScopeIdDec s0 s0); [|intuition].
sgauto. inv H2.
intros. simpl in H0.
eexists; split; sgauto. simpl.
destruct (ELdec l0 l); intuition. subst. inv H0.
inv LNS. econstructor; split; eauto. simpl. destruct (ELdec l l); intuition.
destruct (ELdec l0 l'); intuition. inv H0.
eexists; split; sgauto. inv H0.
Qed.
Hint Resolve initFrame_well_bound : sgraph.
Hint Resolve initFrame_well_bound1 : sgraph.
Hint Resolve initFrame_well_bound2 : sgraph.
Lemma initFrame_well_typed :
∀
h0 s ks slots f h1
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP: ∀ d t v,
In d (keys slots) →
typofDecl d t →
get Ddec slots d = Some v → vtyp h0 v t),
well_typed h1 f.
Proof.
intros; inversion INIT. inv NF. assert (FF':=FF).
eapply fillFrameSame in FF; try rewrite get_set_same; eauto.
eexists; sgauto.
intros. eapply declsofScopeDet in TDs; eauto; subst.
inv H3. rewrite H4 in FF; inv FF.
eapply TYP in H1; eauto. eapply initFrame_vtyp; eauto.
Qed.
Hint Resolve initFrame_well_typed : sgraph.
Lemma initFrame_good_frame :
∀
h0 s ks slots f h1
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP: ∀ d t v,
In d (keys slots) →
typofDecl d t →
get Ddec slots d = Some v → vtyp h0 v t)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_frame h1 f.
Proof.
intros; sgauto.
Qed.
Hint Resolve initFrame_good_frame : sgraph.
Public Good Heap and Frame Properties
Lemma good_path0 :
∀
h
(GH: good_heap h)
p f s d s'
(SF: scopeofFrame h f s)
(SLK: slookup s p s' d),
∃ f', lookup h f p d f' ∧ scopeofFrame h f' s'.
Proof.
induction p; intros.
- destruct SLK as [? [? [? [? ?]]]]; subst.
eexists; split; eauto. econstructor.
edestruct GH as [WB _]; sgauto.
eapply well_bound_get; eauto. econstructor; eauto.
- destruct SLK as [? [? [LL [GL [IN SL]]]]].
assert (GF: good_frame h f) by (eapply GH; eauto using scopeofFrameFrame).
inv GF. inv H0. eapply scopeofFrameDet in SF; eauto; subst.
assert (llinksofScopeP s0 e x0) by (econstructor; eauto).
eapply LNS in H0.
destruct H0 as [? [IMF [KEYS IMSC]]]; subst.
eapply IMSC in IN. inv IN. inv H0.
eapply IHp in SL; eauto.
destruct SL as [? [LOOK SF]].
eexists; split; sgauto.
Qed.
∀
h
(GH: good_heap h)
p f s d s'
(SF: scopeofFrame h f s)
(SLK: slookup s p s' d),
∃ f', lookup h f p d f' ∧ scopeofFrame h f' s'.
Proof.
induction p; intros.
- destruct SLK as [? [? [? [? ?]]]]; subst.
eexists; split; eauto. econstructor.
edestruct GH as [WB _]; sgauto.
eapply well_bound_get; eauto. econstructor; eauto.
- destruct SLK as [? [? [LL [GL [IN SL]]]]].
assert (GF: good_frame h f) by (eapply GH; eauto using scopeofFrameFrame).
inv GF. inv H0. eapply scopeofFrameDet in SF; eauto; subst.
assert (llinksofScopeP s0 e x0) by (econstructor; eauto).
eapply LNS in H0.
destruct H0 as [? [IMF [KEYS IMSC]]]; subst.
eapply IMSC in IN. inv IN. inv H0.
eapply IHp in SL; eauto.
destruct SL as [? [LOOK SF]].
eexists; split; sgauto.
Qed.
Lemma 1 in the paper:
Lemma good_path :
∀
h
(GH: good_heap h)
r p f s d s'
(SF: scopeofFrame h f s)
(SR: scopeofRefP r s)
(SLK: rlookup r p s' d),
∃ f', lookup h f p d f' ∧ scopeofFrame h f' s'.
Proof.
destruct 4 as [? [SR' [PR SL]]].
eapply scopeofRefDet in SR; eauto; subst.
eapply good_path0 in SL; eauto.
Qed.
∀
h
(GH: good_heap h)
r p f s d s'
(SF: scopeofFrame h f s)
(SR: scopeofRefP r s)
(SLK: rlookup r p s' d),
∃ f', lookup h f p d f' ∧ scopeofFrame h f' s'.
Proof.
destruct 4 as [? [SR' [PR SL]]].
eapply scopeofRefDet in SR; eauto; subst.
eapply good_path0 in SL; eauto.
Qed.
In practice, we use this corollary of good_path:
In a good heap, each static lookup starting from a reference
scope corresponds to a dynamic lookup to the address of
a corresponding scope and declaration.
Corollary good_addr :
∀
h r p f s d s'
(SR: scopeofRefP r s)
(SLK: rlookup r p s' d)
(GH: good_heap h)
(SF: scopeofFrame h f s),
∃ ff, getAddr h f r (Addr_ ff d) ∧
scopeofFrame h ff s' ∧
∃ ds,
declsofScopeP s' ds ∧
In d ds.
Proof.
intros. destruct SLK as [? [? [? ?]]].
eapply scopeofRefDet in SR; eauto; subst.
assert (H2':=H2).
eapply good_path0 in H2; eauto.
destruct H2. destruct H2.
eexists; split; sgauto. econstructor; sgauto.
inv H0.
edestruct path_connectivity' as [? [? SL]]; eauto.
eapply slookupDet in H2'; eauto. destruct H2'; subst.
edestruct slookup_ddata as [dd [P1 P2]]; eauto.
Qed.
∀
h r p f s d s'
(SR: scopeofRefP r s)
(SLK: rlookup r p s' d)
(GH: good_heap h)
(SF: scopeofFrame h f s),
∃ ff, getAddr h f r (Addr_ ff d) ∧
scopeofFrame h ff s' ∧
∃ ds,
declsofScopeP s' ds ∧
In d ds.
Proof.
intros. destruct SLK as [? [? [? ?]]].
eapply scopeofRefDet in SR; eauto; subst.
assert (H2':=H2).
eapply good_path0 in H2; eauto.
destruct H2. destruct H2.
eexists; split; sgauto. econstructor; sgauto.
inv H0.
edestruct path_connectivity' as [? [? SL]]; eauto.
eapply slookupDet in H2'; eauto. destruct H2'; subst.
edestruct slookup_ddata as [dd [P1 P2]]; eauto.
Qed.
It is possible to get any declared field in a good frame.
Corollary good_frame_getSlot :
∀ h f s d ds
(GF: good_frame h f)
(SF: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∃ v, getSlot h f d v.
Proof.
intros. inv GF. eapply well_bound_get; eauto.
Qed.
∀ h f s d ds
(GF: good_frame h f)
(SF: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∃ v, getSlot h f d v.
Proof.
intros. inv GF. eapply well_bound_get; eauto.
Qed.
It is possible to set any declared field in a good frame.
Corollary good_frame_setSlot :
∀
h f s ds d
(GF: good_frame h f)
(SC: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∀ v,
∃ h', setSlot h f d v h'.
Proof.
intros. inv GF. eapply well_bound_set; eauto.
Qed.
∀
h f s ds d
(GF: good_frame h f)
(SC: scopeofFrame h f s)
(DS: declsofScopeP s ds)
(IN: In d ds),
∀ v,
∃ h', setSlot h f d v h'.
Proof.
intros. inv GF. eapply well_bound_set; eauto.
Qed.
Setting a correctly typed value in a slot
maintains heap goodness.
Lemma setSlot_good_heap :
∀
h0 f d v h1 t
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: good_heap h0),
good_heap h1.
Proof.
intros. intro. intro. destruct (FrameIdDec f f0); subst.
- eapply setSlot_good_frame; eauto. eapply WT. unfold frame. inv SET; eapply keys_in; eauto.
- eapply setSlot_other_good_frame; eauto. eapply WT.
inv SET. unfold frame in H0. eapply in_keys in H0. rewrite get_set_other in H0; auto.
destruct H0. eapply keys_in; eauto.
Qed.
∀
h0 f d v h1 t
(SET: setSlot h0 f d v h1)
(TD: typofDecl d t)
(VT': vtyp h0 v t)
(WT: good_heap h0),
good_heap h1.
Proof.
intros. intro. intro. destruct (FrameIdDec f f0); subst.
- eapply setSlot_good_frame; eauto. eapply WT. unfold frame. inv SET; eapply keys_in; eauto.
- eapply setSlot_other_good_frame; eauto. eapply WT.
inv SET. unfold frame in H0. eapply in_keys in H0. rewrite get_set_other in H0; auto.
destruct H0. eapply keys_in; eauto.
Qed.
Initializing a new frame with well-typed slots and well-bound links
maintains heap goodness.
Lemma initFrame_good_heap :
∀
h0 s ks slots f h1
(GH: good_heap h0)
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP: ∀ d t v,
In d (keys slots) →
typofDecl d t →
get Ddec slots d = Some v → vtyp h0 v t)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst. eauto using initFrame_good_frame.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
∀
h0 s ks slots f h1
(GH: good_heap h0)
(INIT: initFrame h0 s ks slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP: ∀ d t v,
In d (keys slots) →
typofDecl d t →
get Ddec slots d = Some v → vtyp h0 v t)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst. eauto using initFrame_good_frame.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
Specialization to a new frame with no links or slots
Corollary initFrame_good_heap0 :
∀
h0 s f h1
(GH: good_heap h0)
(DS: declsofScopeP s [])
(PS: linksofScopeP s [])
(INIT: initFrame h0 s [] [] f h1),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
eapply initFrame_good_heap; eauto.
+ intros. inv H1.
+ intros. inv H1. destruct H2 as [P1 P2]. eapply linksofScopeDet in PS; eauto; subst. inv P2.
+ intros. inv H1.
Qed.
∀
h0 s f h1
(GH: good_heap h0)
(DS: declsofScopeP s [])
(PS: linksofScopeP s [])
(INIT: initFrame h0 s [] [] f h1),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
eapply initFrame_good_heap; eauto.
+ intros. inv H1.
+ intros. inv H1. destruct H2 as [P1 P2]. eapply linksofScopeDet in PS; eauto; subst. inv P2.
+ intros. inv H1.
Qed.
Specialization to a new frame with exactly one link
Corollary initFrame_good_heap1 :
∀
h0 s slots f h1 l sl fl
(GH: good_heap h0)
(INIT: initFrame h0 s [(l, [(sl, fl)])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP:
∀
d t v
(IN: In d (keys slots))
(TD: typofDecl d t)
(GET: get Ddec slots d = Some v),
vtyp h0 v t)
(LNS: linksofScopeP s [(l, [sl])])
(SL: scopeofFrame h0 fl sl),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_typed, initFrame_well_bound1.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
Lemma initFrame_good_heap2 :
∀
h0 s slots f h1 l sl fl l' sl' fl'
(GH: good_heap h0)
(INIT: initFrame h0 s [(l, [(sl, fl)]); (l', [(sl', fl')])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP:
∀
d t v
(IN: In d (keys slots))
(TD: typofDecl d t)
(GET: get Ddec slots d = Some v),
vtyp h0 v t)
(LNS: linksofScopeP s [(l, [sl]); (l', [sl'])])
(SL: scopeofFrame h0 fl sl)
(SL': scopeofFrame h0 fl' sl'),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_typed, initFrame_well_bound2.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
End Goodness.
Hint Resolve setSlot_good_heap : sgraph.
Hint Resolve good_addr : sgraph.
Hint Resolve initFrame_good_frame : sgraph.
Hint Resolve initFrame_good_heap : sgraph.
Hint Resolve initFrame_good_heap1 : sgraph.
Hint Resolve initFrame_good_heap2 : sgraph.
∀
h0 s slots f h1 l sl fl
(GH: good_heap h0)
(INIT: initFrame h0 s [(l, [(sl, fl)])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP:
∀
d t v
(IN: In d (keys slots))
(TD: typofDecl d t)
(GET: get Ddec slots d = Some v),
vtyp h0 v t)
(LNS: linksofScopeP s [(l, [sl])])
(SL: scopeofFrame h0 fl sl),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_typed, initFrame_well_bound1.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
Lemma initFrame_good_heap2 :
∀
h0 s slots f h1 l sl fl l' sl' fl'
(GH: good_heap h0)
(INIT: initFrame h0 s [(l, [(sl, fl)]); (l', [(sl', fl')])] slots f h1)
(TDs: declsofScopeP s (keys slots))
(TYP:
∀
d t v
(IN: In d (keys slots))
(TD: typofDecl d t)
(GET: get Ddec slots d = Some v),
vtyp h0 v t)
(LNS: linksofScopeP s [(l, [sl]); (l', [sl'])])
(SL: scopeofFrame h0 fl sl)
(SL': scopeofFrame h0 fl' sl'),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
pose proof (initFrameFrames _ _ _ _ _ _ INIT f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_typed, initFrame_well_bound2.
eapply initFrame_other_good_frame in INIT; eauto.
Qed.
End Goodness.
Hint Resolve setSlot_good_heap : sgraph.
Hint Resolve good_addr : sgraph.
Hint Resolve initFrame_good_frame : sgraph.
Hint Resolve initFrame_good_heap : sgraph.
Hint Resolve initFrame_good_heap1 : sgraph.
Hint Resolve initFrame_good_heap2 : sgraph.
Class DefaultVTyp `{VT: VTyp} :=
{ default : T → V → Prop ;
default_vtyp :
∀ v t,
default t v → ∀ h, vtyp h v t
}.
Section DefaultVTypProperties.
Context `{DVT : DefaultVTyp}.
Inductive defaults : map D V → Prop :=
| defaults_nil : defaults []
| default_cons :
∀
d slots t v
(TD: typofDecl d t)
(DF: default t v)
(TAIL: defaults slots),
defaults ((d,v) :: slots).
Lemma defaults_vtyp :
∀
slots
(DF: defaults slots)
ts
(TDs: typofDecls (keys slots) ts)
h,
Forall2 (fun dv t ⇒
match dv, t with
| (_, v), t ⇒
vtyp h v t
end) slots ts.
Proof.
induction 1; intros. inv TDs; eauto.
inv TDs. eapply typofDeclDet in TD; eauto; subst.
eapply default_vtyp in DF; eauto.
Qed.
Lemma defaults_vtyp' :
∀
slots
(DF: defaults slots),
∀ d t v,
In d (keys slots) →
typofDecl d t →
get Ddec slots d = Some v →
∀ h,
vtyp h v t.
Proof.
induction 1; intros.
- inv H0.
- simpl in ×. destruct (Ddec d d0); subst.
eapply typofDeclDet in H1; eauto; subst.
destruct (Ddec d0 d0); inv H2; auto. apply default_vtyp; auto. intuition.
destruct H0; [contradiction|]. destruct (Ddec d0 d); subst; [intuition|].
eauto.
Qed.
Hint Resolve defaults_vtyp' : sgraph.
Inductive initDefault
(h0: H)
(s: ScopeId) (ks: map EdgeLabel (map ScopeId FrameId))
(f: FrameId) (h1: H) : Prop :=
| initDefault_ : ∀
slots
(DS: declsofScopeP s (keys slots))
(DF: defaults slots)
(NF: initFrame h0 s ks slots f h1),
initDefault h0 s ks f h1.
Lemma initDefaultFrames :
∀ h0 s ks f0 h1,
initDefault h0 s ks f0 h1 →
∀ f, f = f0 ∨ frame h0 f ↔ frame h1 f.
Proof.
inversion 1; eauto using initFrameFrames.
Qed.
Lemma initDefaultDiff_scopeofFrame :
∀ h0 f0 s0 s ks f h1,
initDefault h0 s ks f h1 →
scopeofFrame h0 f0 s0 →
scopeofFrame h1 f0 s0.
Proof.
intros. inv H0. eapply initFrameDiff_scopeofFrame; eauto.
Qed.
Lemma initDefaultSame_scopeofFrame :
∀ h0 s ks f0 h1,
initDefault h0 s ks f0 h1 →
scopeofFrame h1 f0 s.
Proof.
intros. inv H0. eapply initFrameSame_scopeofFrame; eauto.
Qed.
Lemma initDefault_vtyp: ∀
h0 s ks f h1 v0 t0
(INF: initDefault h0 s ks f h1)
(VT: vtyp h0 v0 t0),
vtyp h1 v0 t0.
Proof.
inversion 1; intros; eauto using initFrame_vtyp.
Qed.
Lemma initDefault_good_frame :
∀ h0 s ks f h1
(INIT: initDefault h0 s ks f h1)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_frame h1 f.
Proof.
intros. inv INIT. eapply initFrame_good_frame; sgauto.
Qed.
Public Good Heap Properties for Defaults
Lemma initDefault_good_heap :
∀ h0 s ks f h1
(GH: good_heap h0)
(INIT: initDefault h0 s ks f h1)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_heap h1.
Proof.
inversion 2; intros; sgauto.
Qed.
Corollary initDefault_good_heap0 :
∀ h0 s f h1
(GH: good_heap h0)
(PS: linksofScopeP s [])
(INIT: initDefault h0 s [] f h1),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
eapply initDefault_good_heap; sgauto.
+ intros. inv H1. destruct H2.
inv PS. rewrite H1 in H4; inv H4. inv H2.
+ intros. inv H1.
Qed.
Lemma initDefault_good_heap1 :
∀ h0 s f h1 l sl fl
(GH: good_heap h0)
(INIT: initDefault h0 s [(l, [(sl, fl)])] f h1)
(LNS: linksofScopeP s [(l, [sl])])
(SL: scopeofFrame h0 fl sl),
good_heap h1.
Proof.
intros. unfold good_heap. intros. inv INIT.
pose proof (initFrameFrames _ _ _ _ _ _ NF f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_bound1, initFrame_well_typed, defaults_vtyp'.
eapply initFrame_other_good_frame in NF; eauto.
Qed.
End DefaultVTypProperties.
Hint Resolve defaults_vtyp' : sgraph.
Hint Resolve initDefaultSame_scopeofFrame : sgraph.
Hint Resolve initDefaultDiff_scopeofFrame : sgraph.
Hint Resolve initDefault_good_frame : sgraph.
Hint Resolve initDefault_good_heap : sgraph.
Hint Resolve initDefault_good_heap0 : sgraph.
Hint Resolve initDefault_good_heap1 : sgraph.
∀ h0 s ks f h1
(GH: good_heap h0)
(INIT: initDefault h0 s ks f h1)
(LNS: ∀ l ss,
llinksofScopeP s l ss →
∃ m,
get ELdec ks l = Some m ∧
keys m = ss ∧
∀ s,
In s ss →
∃ f', get ScopeIdDec m s = Some f' ∧
scopeofFrame h0 f' s)
(LNF: ∀ l m,
get ELdec ks l = Some m →
llinksofScopeP s l (keys m)),
good_heap h1.
Proof.
inversion 2; intros; sgauto.
Qed.
Corollary initDefault_good_heap0 :
∀ h0 s f h1
(GH: good_heap h0)
(PS: linksofScopeP s [])
(INIT: initDefault h0 s [] f h1),
good_heap h1.
Proof.
intros. unfold good_heap. intros.
eapply initDefault_good_heap; sgauto.
+ intros. inv H1. destruct H2.
inv PS. rewrite H1 in H4; inv H4. inv H2.
+ intros. inv H1.
Qed.
Lemma initDefault_good_heap1 :
∀ h0 s f h1 l sl fl
(GH: good_heap h0)
(INIT: initDefault h0 s [(l, [(sl, fl)])] f h1)
(LNS: linksofScopeP s [(l, [sl])])
(SL: scopeofFrame h0 fl sl),
good_heap h1.
Proof.
intros. unfold good_heap. intros. inv INIT.
pose proof (initFrameFrames _ _ _ _ _ _ NF f0). destruct H1.
apply H2 in H0. destruct H0. subst.
split; eauto using initFrame_well_bound1, initFrame_well_typed, defaults_vtyp'.
eapply initFrame_other_good_frame in NF; eauto.
Qed.
End DefaultVTypProperties.
Hint Resolve defaults_vtyp' : sgraph.
Hint Resolve initDefaultSame_scopeofFrame : sgraph.
Hint Resolve initDefaultDiff_scopeofFrame : sgraph.
Hint Resolve initDefault_good_frame : sgraph.
Hint Resolve initDefault_good_heap : sgraph.
Hint Resolve initDefault_good_heap0 : sgraph.
Hint Resolve initDefault_good_heap1 : sgraph.