Lvc.Spilling.SpillSound
Require Import List Map Envs AllInRel Exp.
Require Import IL Annotation AnnP AutoIndTac Liveness.Liveness LabelsDefined.
Require Import ExpVarsBounded PartialOrder.
Require Export SpillUtil.
Require Import IL Annotation AnnP AutoIndTac Liveness.Liveness LabelsDefined.
Require Import ExpVarsBounded PartialOrder.
Require Export SpillUtil.
Inductive spill_sound (k:nat) :
(list params)
→ (list (⦃var⦄ × ⦃var⦄))
→ (⦃var⦄ × ⦃var⦄)
→ stmt
→ spilling
→ Prop
:=
| SpillLet
(ZL : list params)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K Kx : ⦃var⦄)
(x : var)
(e : exp)
(s : stmt)
(sl : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ spill_sound k ZL Λ ({x;(R\K ∪ L)\Kx }, Sp ∪ M) s sl
→ Exp.freeVars e ⊆ R\K ∪ L
→ k > 0
→ cardinal (R\K ∪ L) ≤ k
→ cardinal ({x;((R\K) ∪ L)\Kx }) ≤ k
→ spill_sound k ZL Λ (R,M) (stmtLet x e s) (ann1 (Sp,L,nil) sl)
| SpillReturn
(ZL : list (params))
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(e : op)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ Ops.freeVars e ⊆ R\K ∪ L
→ cardinal ((R\K) ∪ L) ≤ k
→ spill_sound k ZL Λ (R,M) (stmtReturn e)
(ann0 (Sp,L,nil))
| SpillIf
(ZL : list (params))
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(e : op)
(s t : stmt)
(sl_s sl_t : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ Ops.freeVars e ⊆ R\K ∪ L
→ cardinal (R\K ∪ L) ≤ k
→ spill_sound k ZL Λ (R\K ∪ L, Sp ∪ M) s sl_s
→ spill_sound k ZL Λ (R\K ∪ L, Sp ∪ M) t sl_t
→ spill_sound k ZL Λ (R,M) (stmtIf e s t) (ann2 (Sp,L,nil) sl_s sl_t)
| SpillApp
(ZL : list params)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K R_f M_f R' M' : ⦃var⦄)
(f : lab)
(Z : params)
(Y : args)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ cardinal (R\K ∪ L) ≤ k
→ get ZL (counted f) Z
→ get Λ (counted f) (R_f,M_f)
→ R_f \ of_list Z ⊆ R\K ∪ L
→ M_f \ of_list Z ⊆ Sp ∪ M
→ list_union (Ops.freeVars ⊝ Y) [=] R' ∪ M'
→ R' ⊆ R\K ∪ L
→ M' ⊆ Sp ∪ M
→ spill_sound k ZL Λ (R,M) (stmtApp f Y)
(ann0 (Sp,L, (R', M')::nil))
| SpillFun
(ZL : list params)
(Λ rms : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(F : list (params × stmt))
(t : stmt)
(sl_F : list spilling)
(sl_t : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ cardinal (R\K ∪ L) ≤ k
→ length F = length sl_F
→ length F = length rms
→ (∀ n rm, get rms n rm → cardinal (fst rm) ≤ k)
→ (∀ n Zs rm sl_s, get rms n rm
→ get F n Zs
→ get sl_F n sl_s
→ spill_sound k ((fst ⊝ F) ++ ZL)
(rms ++ Λ) rm (snd Zs) sl_s
)
→ spill_sound k ((fst ⊝ F) ++ ZL) (rms ++ Λ) (R\K ∪ L, Sp ∪ M) t sl_t
→ spill_sound k ZL Λ (R,M) (stmtFun F t)
(annF (Sp,L,rms) sl_F sl_t)
.
Lemma Sp_sub_R
(ZL : list params)
(k : nat)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M : ⦃var⦄)
(s : stmt)
(sl : spilling)
:
spill_sound k ZL Λ (R,M) s sl
→ getSp sl ⊆ R
.
Proof.
intros spillSnd.
invc spillSnd;
cset_tac.
Qed.
Lemma L_sub_SpM (ZL : list params) (k : nat) (Λ : list (⦃var⦄ × ⦃var⦄))
(R M : ⦃var⦄) (s : stmt) (sl : spilling)
: spill_sound k ZL Λ (R,M) s sl → getL sl ⊆ getSp sl ∪ M .
Proof.
intros spillSnd.
invc spillSnd; cset_tac.
Qed.
Inductive spill_live
(VD : ⦃var⦄)
:
spilling → ann (set var) → Prop
:=
| SomeSpLv0 a b
: spill_live VD (ann0 a) (ann0 b)
| SomeSpLv1 a b sl lv
: spill_live VD sl lv
→ spill_live VD (ann1 a sl) (ann1 b lv)
| SomeSpLv2 a b sl1 sl2 lv1 lv2
: spill_live VD sl1 lv1
→ spill_live VD sl2 lv2
→ spill_live VD (ann2 a sl1 sl2) (ann2 b lv1 lv2)
| SomeSpLvF a b sl_F sl_t lv_F lv_t rms
: PIR2 Equal (merge ⊝ rms) (getAnn ⊝ lv_F)
→ spill_live VD sl_t lv_t
→ (∀ n rm,
get rms n rm
→ fst rm ⊆ VD ∧ snd rm ⊆ VD)
→ (∀ n sl_s lv_s,
get sl_F n sl_s
→ get lv_F n lv_s
→ spill_live VD sl_s lv_s
)
→ spill_live VD (annF (a, rms) sl_F sl_t)
(annF b lv_F lv_t)
.
Lemma spill_sound_ext Λ Λ' k ZL R M s sl
: poEq Λ Λ'
→ spill_sound k ZL Λ (R,M) s sl
→ spill_sound k ZL Λ' (R,M) s sl .
Proof.
intros Λeq spillSnd. general induction spillSnd.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
- eapply PIR2_nth in Λeq as [[R_f' M_f'] [get_blk' blk'_eq]]; eauto.
invc blk'_eq; simpl in ×.
econstructor; eauto.
+ rewrite <- H4, H9. reflexivity.
+ rewrite <- H10, H5. eauto.
- econstructor; eauto.
+ intros. inv_get. eapply H6; eauto.
× apply surjective_pairing.
Qed.
Lemma spill_sound_monotone Λ Λ' k ZL R M s sl
: poLe Λ' Λ
→ spill_sound k ZL Λ (R,M) s sl
→ spill_sound k ZL Λ' (R,M) s sl.
Proof.
intros Λeq spillSnd. general induction spillSnd.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
- eapply PIR2_nth_2 in Λeq as [[R_f' M_f'] [get_blk' blk'_eq]]; eauto. cbn in ×. invc blk'_eq.
econstructor; eauto; cbn in ×.
+ rewrite H9. eauto.
+ rewrite H10. eauto.
- econstructor; eauto.
+ intros. inv_get. eapply H6; eauto.
× apply surjective_pairing.
Qed.
Lemma list_eq_PIR2 X `{OrderedType X} (L L':list X)
: L === L' → PIR2 _eq L L'.
Proof.
intros. general induction H0; eauto using PIR2.
Qed.
Smpl Add match goal with
| [ H : S _ < 0 |- _ ] ⇒ exfalso; inv H
| [ H : S _ ≤ 0 |- _ ] ⇒ exfalso; inv H
end : inv_trivial.
Lemma spill_sound_ext2 (k : nat) (ZL : list params) s (Λ Λ2 : list (⦃var⦄ × ⦃var⦄))
(R R2 M M2 : ⦃var⦄) (sl sl2 : spilling)
:
Λ === Λ2
→ R [=] R2
→ M [=] M2
→ sl === sl2
→ spill_sound k ZL Λ (R,M) s sl → spill_sound k ZL Λ2 (R2,M2) s sl2.
Proof.
intros Λeq Req Meq sleq H.
general induction H; simpl; eauto.
destruct sl2; isabsurd;
destruct a as [[Sp' L'] rm'];
clear_trivial_eqs.
- eapply SpillLet with (K:=K) (Kx:=Kx); simpl; eauto with cset.
+ rewrite <-Req, <-H9. assumption.
+ rewrite <-Meq, <-H7, <-H9. assumption.
+ eapply IHspill_sound; eauto.
× rewrite Req, H7; clear; cset_tac.
× rewrite H9, Meq; clear; cset_tac.
+ rewrite <-Req, <-H7; assumption.
+ rewrite <-Req, <-H7; assumption.
+ rewrite <-Req, <-H7; assumption.
- invc sleq. destruct b as [[? ?] ?]. clear_trivial_eqs.
econstructor; eauto.
+ rewrite <- H4. rewrite <- Req. eauto.
+ rewrite <- H4, <- H5. rewrite <- Meq. eauto.
+ rewrite <- H5. rewrite <- Req. eauto.
+ rewrite <- Req, <- H5. eauto.
- invc sleq.
destruct b as [[? ?] ?]. clear_trivial_eqs.
eapply SpillIf with (K:=K).
+ rewrite <-H8, <-Req. assumption.
+ rewrite <-Meq, <-H8, <-H6; assumption.
+ rewrite <-Req, <-H6; assumption.
+ rewrite <-Req, <-H6; assumption.
+ eapply IHspill_sound1; eauto.
× rewrite Req, H6; clear; cset_tac.
× rewrite Meq, H8; clear; cset_tac.
+ eapply IHspill_sound2; eauto.
× rewrite Req, H6; clear; cset_tac.
× rewrite Meq, H8; clear; cset_tac.
- hnf in Λeq. PIR2_inv.
invc sleq.
destruct b as [[? ?] ?]. destruct x. simpl in ×.
clear_trivial_eqs.
destruct y. simpl in ×.
invc H16.
eapply SpillApp with (K:=K); eauto;
try rewrite <- H13;
try rewrite <- H14;
try rewrite <- Req;
try rewrite <- Req;
try rewrite <- Λeq0;
try rewrite <- Λeq2;
try rewrite <- H10;
try rewrite <- H11;
try rewrite <- Meq; eauto.
- invc sleq.
destruct b as [[? ?] ?]. clear_trivial_eqs.
eapply SpillFun with (K:=K); eauto.
+ rewrite <- H11, <- Req; eauto.
+ rewrite <- H9, <- H11, <- Meq; eauto.
+ rewrite <- H9, <- Req. eauto.
+ eauto with len.
+ hnf in H8. eapply PIR2_length in H8. eauto with len.
+ intros. hnf in H8. inv_get.
edestruct @PIR2_nth_2; try eapply H8; eauto; dcr.
exploit H4; eauto.
rewrite <- H17. eauto.
+ intros. inv_get.
exploit H7; eauto.
edestruct @PIR2_nth_2; try eapply H8; eauto; dcr.
inv_get. destruct x,rm; clear_trivial_eqs.
eapply H6; eauto.
× eapply PIR2_app; eauto.
× eauto.
× eauto.
× eapply H14; eauto.
+ eapply IHspill_sound; eauto.
× eapply PIR2_app; eauto.
× rewrite <- Req, <- H9. eauto.
× rewrite <- H11. rewrite <- Meq. eauto.
Qed.
Instance spill_sound_morphX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> iff) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful; intros; subst; split; intros; inv H.
- eapply spill_sound_ext2; eauto; try reflexivity.
eapply H2. eapply H3.
- eapply spill_sound_ext2; try eapply H0; try reflexivity.
rewrite H2; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morph_implX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> impl) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful, impl; intros; subst; intros; inv H.
- eapply spill_sound_ext2; try eapply H2; try reflexivity.
rewrite H0; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morph_flip_implX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> flip impl) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful, flip, impl; intros; subst; intros; inv H.
- eapply spill_sound_ext2; try eapply H2; try reflexivity.
rewrite H0; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morphX' k ZL Λ
: Proper (@pe _ _ ==> eq ==> @equiv _ _ _ ==> iff) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful; intros; subst; split; intros; inv H.
- eapply spill_sound_ext2; eauto; try reflexivity.
- eapply spill_sound_ext2; try eapply H0; try reflexivity.
rewrite H2; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Lemma spill_sound_spill_ext k ZL Λ (R0 M0:set var) s sl
(SPS: spill_sound k ZL Λ (R0, getSp sl ∪ M0) s (clear_Sp sl))
(Sp_sub : getSp sl [<=] R0)
(Rsmall : cardinal R0 ≤ k)
: spill_sound k ZL Λ (R0, M0) s sl.
Proof.
destruct sl; invc SPS; simpl in *; clear_trivial_eqs.
- destruct p. econstructor; eauto.
- simpl in ×. destruct p. econstructor; eauto.
- destruct p; simpl in ×. econstructor; eauto.
set_simpl. eauto.
- destruct p; simpl in ×. set_simpl.
econstructor; eauto.
- destruct a. destruct p.
econstructor; eauto.
simpl in ×. set_simpl. eauto.
Qed.
Lemma spill_sound_incl_R k ZL Λ R R' s sl M
(SPS:spill_sound k ZL Λ (R,M) s sl)
(Incl: R ⊆ R')
(Card:cardinal R' ≤ k)
: spill_sound k ZL Λ (R',M) s sl.
Proof.
destruct sl; invc SPS; simpl in ×.
- eapply SpillReturn with (K:=K ∪ R' \ R); eauto with cset.
+ rewrite H7.
revert Incl; clear_all; cset_tac.
+ rewrite <- H8. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
- eapply SpillApp with (K:=K ∪ R' \ R); eauto.
+ eauto with cset.
+ rewrite <- H4. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
+ rewrite H7.
revert Incl; clear_all; cset_tac.
+ rewrite H13.
revert Incl; clear_all; cset_tac.
- eapply SpillLet with (K:=K ∪ R' \ R); eauto.
+ eauto with cset.
+ assert ({x; (R' \ (K ∪ R' \ R) ∪ L) \ Kx}
[=] {x; (R \ K ∪ L) \ Kx}). {
revert Incl; clear_all; cset_tac.
}
rewrite H. eauto.
+ rewrite H8.
revert Incl; clear_all; cset_tac.
+ rewrite <- H11. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
+ rewrite <- H12. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
- assert (EQ:R' \ (K ∪ R' \ R) ∪ L
[=] R \ K ∪ L). {
revert Incl; clear_all; cset_tac.
}
eapply SpillIf with (K:=K ∪ R' \ R); eauto;
try rewrite EQ; eauto with cset.
- assert (EQ:R' \ (K ∪ R' \ R) ∪ L
[=] R \ K ∪ L). {
revert Incl; clear_all; cset_tac.
}
eapply SpillFun with (K:=K ∪ R' \ R); eauto;
try rewrite EQ; eauto.
+ eauto with cset.
Qed.
Lemma spill_sound_load_ext k ZL Λ (R0 M0:set var) Ka s sl
(card:cardinal R0 ≤ k)
(card2: cardinal (R0 \ Ka ∪ getL sl) ≤ k)
(SPS: spill_sound k ZL Λ (R0 \ Ka ∪ getL sl, M0) s (clear_L sl))
(L_sub : getL sl [<=] M0)
(SpE:getSp sl [=] ∅)
: spill_sound k ZL Λ (R0, M0) s sl.
Proof.
destruct sl; inv SPS; simpl in *; clear_trivial_eqs;
try destruct p as [Sp L]; simpl in ×.
- eapply SpillReturn with (K:=Ka).
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H9. cset_tac.
+ eauto.
- econstructor; eauto.
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H11. clear; cset_tac.
+ rewrite H15. clear; cset_tac.
- econstructor; eauto.
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ instantiate (1:=K ∪ Kx).
rewrite <- minus_union. eauto.
revert H10; clear. set_simpl. eauto.
+ rewrite H11. clear; cset_tac.
+ rewrite <- H14.
eapply subset_cardinal.
clear_all. cset_tac'.
- eapply SpillIf with (K:=K ∪ Ka).
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H11. clear_all. cset_tac.
+ rewrite <- card2. eapply subset_cardinal. clear; cset_tac.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
× rewrite <- card2. eapply subset_cardinal.
clear; cset_tac.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
× rewrite <- card2. eapply subset_cardinal.
clear; cset_tac.
- destruct a, p; simpl in ×.
econstructor; eauto.
+ rewrite SpE; eauto with cset.
+ rewrite L_sub; eauto with cset.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
Qed.
(list params)
→ (list (⦃var⦄ × ⦃var⦄))
→ (⦃var⦄ × ⦃var⦄)
→ stmt
→ spilling
→ Prop
:=
| SpillLet
(ZL : list params)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K Kx : ⦃var⦄)
(x : var)
(e : exp)
(s : stmt)
(sl : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ spill_sound k ZL Λ ({x;(R\K ∪ L)\Kx }, Sp ∪ M) s sl
→ Exp.freeVars e ⊆ R\K ∪ L
→ k > 0
→ cardinal (R\K ∪ L) ≤ k
→ cardinal ({x;((R\K) ∪ L)\Kx }) ≤ k
→ spill_sound k ZL Λ (R,M) (stmtLet x e s) (ann1 (Sp,L,nil) sl)
| SpillReturn
(ZL : list (params))
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(e : op)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ Ops.freeVars e ⊆ R\K ∪ L
→ cardinal ((R\K) ∪ L) ≤ k
→ spill_sound k ZL Λ (R,M) (stmtReturn e)
(ann0 (Sp,L,nil))
| SpillIf
(ZL : list (params))
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(e : op)
(s t : stmt)
(sl_s sl_t : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ Ops.freeVars e ⊆ R\K ∪ L
→ cardinal (R\K ∪ L) ≤ k
→ spill_sound k ZL Λ (R\K ∪ L, Sp ∪ M) s sl_s
→ spill_sound k ZL Λ (R\K ∪ L, Sp ∪ M) t sl_t
→ spill_sound k ZL Λ (R,M) (stmtIf e s t) (ann2 (Sp,L,nil) sl_s sl_t)
| SpillApp
(ZL : list params)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K R_f M_f R' M' : ⦃var⦄)
(f : lab)
(Z : params)
(Y : args)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ cardinal (R\K ∪ L) ≤ k
→ get ZL (counted f) Z
→ get Λ (counted f) (R_f,M_f)
→ R_f \ of_list Z ⊆ R\K ∪ L
→ M_f \ of_list Z ⊆ Sp ∪ M
→ list_union (Ops.freeVars ⊝ Y) [=] R' ∪ M'
→ R' ⊆ R\K ∪ L
→ M' ⊆ Sp ∪ M
→ spill_sound k ZL Λ (R,M) (stmtApp f Y)
(ann0 (Sp,L, (R', M')::nil))
| SpillFun
(ZL : list params)
(Λ rms : list (⦃var⦄ × ⦃var⦄))
(R M Sp L K : ⦃var⦄)
(F : list (params × stmt))
(t : stmt)
(sl_F : list spilling)
(sl_t : spilling)
: Sp ⊆ R
→ L ⊆ Sp ∪ M
→ cardinal (R\K ∪ L) ≤ k
→ length F = length sl_F
→ length F = length rms
→ (∀ n rm, get rms n rm → cardinal (fst rm) ≤ k)
→ (∀ n Zs rm sl_s, get rms n rm
→ get F n Zs
→ get sl_F n sl_s
→ spill_sound k ((fst ⊝ F) ++ ZL)
(rms ++ Λ) rm (snd Zs) sl_s
)
→ spill_sound k ((fst ⊝ F) ++ ZL) (rms ++ Λ) (R\K ∪ L, Sp ∪ M) t sl_t
→ spill_sound k ZL Λ (R,M) (stmtFun F t)
(annF (Sp,L,rms) sl_F sl_t)
.
Lemma Sp_sub_R
(ZL : list params)
(k : nat)
(Λ : list (⦃var⦄ × ⦃var⦄))
(R M : ⦃var⦄)
(s : stmt)
(sl : spilling)
:
spill_sound k ZL Λ (R,M) s sl
→ getSp sl ⊆ R
.
Proof.
intros spillSnd.
invc spillSnd;
cset_tac.
Qed.
Lemma L_sub_SpM (ZL : list params) (k : nat) (Λ : list (⦃var⦄ × ⦃var⦄))
(R M : ⦃var⦄) (s : stmt) (sl : spilling)
: spill_sound k ZL Λ (R,M) s sl → getL sl ⊆ getSp sl ∪ M .
Proof.
intros spillSnd.
invc spillSnd; cset_tac.
Qed.
Inductive spill_live
(VD : ⦃var⦄)
:
spilling → ann (set var) → Prop
:=
| SomeSpLv0 a b
: spill_live VD (ann0 a) (ann0 b)
| SomeSpLv1 a b sl lv
: spill_live VD sl lv
→ spill_live VD (ann1 a sl) (ann1 b lv)
| SomeSpLv2 a b sl1 sl2 lv1 lv2
: spill_live VD sl1 lv1
→ spill_live VD sl2 lv2
→ spill_live VD (ann2 a sl1 sl2) (ann2 b lv1 lv2)
| SomeSpLvF a b sl_F sl_t lv_F lv_t rms
: PIR2 Equal (merge ⊝ rms) (getAnn ⊝ lv_F)
→ spill_live VD sl_t lv_t
→ (∀ n rm,
get rms n rm
→ fst rm ⊆ VD ∧ snd rm ⊆ VD)
→ (∀ n sl_s lv_s,
get sl_F n sl_s
→ get lv_F n lv_s
→ spill_live VD sl_s lv_s
)
→ spill_live VD (annF (a, rms) sl_F sl_t)
(annF b lv_F lv_t)
.
Lemma spill_sound_ext Λ Λ' k ZL R M s sl
: poEq Λ Λ'
→ spill_sound k ZL Λ (R,M) s sl
→ spill_sound k ZL Λ' (R,M) s sl .
Proof.
intros Λeq spillSnd. general induction spillSnd.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
- eapply PIR2_nth in Λeq as [[R_f' M_f'] [get_blk' blk'_eq]]; eauto.
invc blk'_eq; simpl in ×.
econstructor; eauto.
+ rewrite <- H4, H9. reflexivity.
+ rewrite <- H10, H5. eauto.
- econstructor; eauto.
+ intros. inv_get. eapply H6; eauto.
× apply surjective_pairing.
Qed.
Lemma spill_sound_monotone Λ Λ' k ZL R M s sl
: poLe Λ' Λ
→ spill_sound k ZL Λ (R,M) s sl
→ spill_sound k ZL Λ' (R,M) s sl.
Proof.
intros Λeq spillSnd. general induction spillSnd.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
- eapply PIR2_nth_2 in Λeq as [[R_f' M_f'] [get_blk' blk'_eq]]; eauto. cbn in ×. invc blk'_eq.
econstructor; eauto; cbn in ×.
+ rewrite H9. eauto.
+ rewrite H10. eauto.
- econstructor; eauto.
+ intros. inv_get. eapply H6; eauto.
× apply surjective_pairing.
Qed.
Lemma list_eq_PIR2 X `{OrderedType X} (L L':list X)
: L === L' → PIR2 _eq L L'.
Proof.
intros. general induction H0; eauto using PIR2.
Qed.
Smpl Add match goal with
| [ H : S _ < 0 |- _ ] ⇒ exfalso; inv H
| [ H : S _ ≤ 0 |- _ ] ⇒ exfalso; inv H
end : inv_trivial.
Lemma spill_sound_ext2 (k : nat) (ZL : list params) s (Λ Λ2 : list (⦃var⦄ × ⦃var⦄))
(R R2 M M2 : ⦃var⦄) (sl sl2 : spilling)
:
Λ === Λ2
→ R [=] R2
→ M [=] M2
→ sl === sl2
→ spill_sound k ZL Λ (R,M) s sl → spill_sound k ZL Λ2 (R2,M2) s sl2.
Proof.
intros Λeq Req Meq sleq H.
general induction H; simpl; eauto.
destruct sl2; isabsurd;
destruct a as [[Sp' L'] rm'];
clear_trivial_eqs.
- eapply SpillLet with (K:=K) (Kx:=Kx); simpl; eauto with cset.
+ rewrite <-Req, <-H9. assumption.
+ rewrite <-Meq, <-H7, <-H9. assumption.
+ eapply IHspill_sound; eauto.
× rewrite Req, H7; clear; cset_tac.
× rewrite H9, Meq; clear; cset_tac.
+ rewrite <-Req, <-H7; assumption.
+ rewrite <-Req, <-H7; assumption.
+ rewrite <-Req, <-H7; assumption.
- invc sleq. destruct b as [[? ?] ?]. clear_trivial_eqs.
econstructor; eauto.
+ rewrite <- H4. rewrite <- Req. eauto.
+ rewrite <- H4, <- H5. rewrite <- Meq. eauto.
+ rewrite <- H5. rewrite <- Req. eauto.
+ rewrite <- Req, <- H5. eauto.
- invc sleq.
destruct b as [[? ?] ?]. clear_trivial_eqs.
eapply SpillIf with (K:=K).
+ rewrite <-H8, <-Req. assumption.
+ rewrite <-Meq, <-H8, <-H6; assumption.
+ rewrite <-Req, <-H6; assumption.
+ rewrite <-Req, <-H6; assumption.
+ eapply IHspill_sound1; eauto.
× rewrite Req, H6; clear; cset_tac.
× rewrite Meq, H8; clear; cset_tac.
+ eapply IHspill_sound2; eauto.
× rewrite Req, H6; clear; cset_tac.
× rewrite Meq, H8; clear; cset_tac.
- hnf in Λeq. PIR2_inv.
invc sleq.
destruct b as [[? ?] ?]. destruct x. simpl in ×.
clear_trivial_eqs.
destruct y. simpl in ×.
invc H16.
eapply SpillApp with (K:=K); eauto;
try rewrite <- H13;
try rewrite <- H14;
try rewrite <- Req;
try rewrite <- Req;
try rewrite <- Λeq0;
try rewrite <- Λeq2;
try rewrite <- H10;
try rewrite <- H11;
try rewrite <- Meq; eauto.
- invc sleq.
destruct b as [[? ?] ?]. clear_trivial_eqs.
eapply SpillFun with (K:=K); eauto.
+ rewrite <- H11, <- Req; eauto.
+ rewrite <- H9, <- H11, <- Meq; eauto.
+ rewrite <- H9, <- Req. eauto.
+ eauto with len.
+ hnf in H8. eapply PIR2_length in H8. eauto with len.
+ intros. hnf in H8. inv_get.
edestruct @PIR2_nth_2; try eapply H8; eauto; dcr.
exploit H4; eauto.
rewrite <- H17. eauto.
+ intros. inv_get.
exploit H7; eauto.
edestruct @PIR2_nth_2; try eapply H8; eauto; dcr.
inv_get. destruct x,rm; clear_trivial_eqs.
eapply H6; eauto.
× eapply PIR2_app; eauto.
× eauto.
× eauto.
× eapply H14; eauto.
+ eapply IHspill_sound; eauto.
× eapply PIR2_app; eauto.
× rewrite <- Req, <- H9. eauto.
× rewrite <- H11. rewrite <- Meq. eauto.
Qed.
Instance spill_sound_morphX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> iff) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful; intros; subst; split; intros; inv H.
- eapply spill_sound_ext2; eauto; try reflexivity.
eapply H2. eapply H3.
- eapply spill_sound_ext2; try eapply H0; try reflexivity.
rewrite H2; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morph_implX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> impl) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful, impl; intros; subst; intros; inv H.
- eapply spill_sound_ext2; try eapply H2; try reflexivity.
rewrite H0; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morph_flip_implX k ZL Λ
: Proper (_eq ==> eq ==> @equiv _ _ _ ==> flip impl) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful, flip, impl; intros; subst; intros; inv H.
- eapply spill_sound_ext2; try eapply H2; try reflexivity.
rewrite H0; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Instance spill_sound_morphX' k ZL Λ
: Proper (@pe _ _ ==> eq ==> @equiv _ _ _ ==> iff) (spill_sound k ZL Λ).
Proof.
unfold Proper, respectful; intros; subst; split; intros; inv H.
- eapply spill_sound_ext2; eauto; try reflexivity.
- eapply spill_sound_ext2; try eapply H0; try reflexivity.
rewrite H2; eauto. rewrite H3; eauto. symmetry; eauto.
Qed.
Lemma spill_sound_spill_ext k ZL Λ (R0 M0:set var) s sl
(SPS: spill_sound k ZL Λ (R0, getSp sl ∪ M0) s (clear_Sp sl))
(Sp_sub : getSp sl [<=] R0)
(Rsmall : cardinal R0 ≤ k)
: spill_sound k ZL Λ (R0, M0) s sl.
Proof.
destruct sl; invc SPS; simpl in *; clear_trivial_eqs.
- destruct p. econstructor; eauto.
- simpl in ×. destruct p. econstructor; eauto.
- destruct p; simpl in ×. econstructor; eauto.
set_simpl. eauto.
- destruct p; simpl in ×. set_simpl.
econstructor; eauto.
- destruct a. destruct p.
econstructor; eauto.
simpl in ×. set_simpl. eauto.
Qed.
Lemma spill_sound_incl_R k ZL Λ R R' s sl M
(SPS:spill_sound k ZL Λ (R,M) s sl)
(Incl: R ⊆ R')
(Card:cardinal R' ≤ k)
: spill_sound k ZL Λ (R',M) s sl.
Proof.
destruct sl; invc SPS; simpl in ×.
- eapply SpillReturn with (K:=K ∪ R' \ R); eauto with cset.
+ rewrite H7.
revert Incl; clear_all; cset_tac.
+ rewrite <- H8. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
- eapply SpillApp with (K:=K ∪ R' \ R); eauto.
+ eauto with cset.
+ rewrite <- H4. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
+ rewrite H7.
revert Incl; clear_all; cset_tac.
+ rewrite H13.
revert Incl; clear_all; cset_tac.
- eapply SpillLet with (K:=K ∪ R' \ R); eauto.
+ eauto with cset.
+ assert ({x; (R' \ (K ∪ R' \ R) ∪ L) \ Kx}
[=] {x; (R \ K ∪ L) \ Kx}). {
revert Incl; clear_all; cset_tac.
}
rewrite H. eauto.
+ rewrite H8.
revert Incl; clear_all; cset_tac.
+ rewrite <- H11. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
+ rewrite <- H12. eapply subset_cardinal.
revert Incl; clear_all; cset_tac.
- assert (EQ:R' \ (K ∪ R' \ R) ∪ L
[=] R \ K ∪ L). {
revert Incl; clear_all; cset_tac.
}
eapply SpillIf with (K:=K ∪ R' \ R); eauto;
try rewrite EQ; eauto with cset.
- assert (EQ:R' \ (K ∪ R' \ R) ∪ L
[=] R \ K ∪ L). {
revert Incl; clear_all; cset_tac.
}
eapply SpillFun with (K:=K ∪ R' \ R); eauto;
try rewrite EQ; eauto.
+ eauto with cset.
Qed.
Lemma spill_sound_load_ext k ZL Λ (R0 M0:set var) Ka s sl
(card:cardinal R0 ≤ k)
(card2: cardinal (R0 \ Ka ∪ getL sl) ≤ k)
(SPS: spill_sound k ZL Λ (R0 \ Ka ∪ getL sl, M0) s (clear_L sl))
(L_sub : getL sl [<=] M0)
(SpE:getSp sl [=] ∅)
: spill_sound k ZL Λ (R0, M0) s sl.
Proof.
destruct sl; inv SPS; simpl in *; clear_trivial_eqs;
try destruct p as [Sp L]; simpl in ×.
- eapply SpillReturn with (K:=Ka).
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H9. cset_tac.
+ eauto.
- econstructor; eauto.
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H11. clear; cset_tac.
+ rewrite H15. clear; cset_tac.
- econstructor; eauto.
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ instantiate (1:=K ∪ Kx).
rewrite <- minus_union. eauto.
revert H10; clear. set_simpl. eauto.
+ rewrite H11. clear; cset_tac.
+ rewrite <- H14.
eapply subset_cardinal.
clear_all. cset_tac'.
- eapply SpillIf with (K:=K ∪ Ka).
+ rewrite SpE. eauto with cset.
+ rewrite L_sub. eauto with cset.
+ rewrite H11. clear_all. cset_tac.
+ rewrite <- card2. eapply subset_cardinal. clear; cset_tac.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
× rewrite <- card2. eapply subset_cardinal.
clear; cset_tac.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
× rewrite <- card2. eapply subset_cardinal.
clear; cset_tac.
- destruct a, p; simpl in ×.
econstructor; eauto.
+ rewrite SpE; eauto with cset.
+ rewrite L_sub; eauto with cset.
+ eapply spill_sound_incl_R; eauto.
× clear; cset_tac.
Qed.