Lvc.Spilling.RegisterBound
Require Import List Map Envs AllInRel Exp AppExpFree RenamedApart.
Require Import IL Annotation AutoIndTac AnnotationLattice.
Require Import Liveness.Liveness LabelsDefined.
Require Import SpillSound DoSpill DoSpillRm SpillUtil ReconstrLive.
Require Import ReconstrLiveSmall ReconstrLiveSound InVD AnnP.
Require Import BoundedIn SlotLiftArgs SlotLiftParams.
Set Implicit Arguments.
Require Import IL Annotation AutoIndTac AnnotationLattice.
Require Import Liveness.Liveness LabelsDefined.
Require Import SpillSound DoSpill DoSpillRm SpillUtil ReconstrLive.
Require Import ReconstrLiveSmall ReconstrLiveSound InVD AnnP.
Require Import BoundedIn SlotLiftArgs SlotLiftParams.
Set Implicit Arguments.
Lemma bounded_in_incl VD G G' k Lv ZL s (an : (ann ⦃var⦄))
: VD ∩ G' ⊆ VD ∩ G
→ ann_P (bounded_in VD k) (reconstr_live Lv ZL G s an)
→ ann_P (bounded_in VD k) (reconstr_live Lv ZL G' s an).
Proof.
intros Gincl base.
assert (bounded_in VD k G') as biG'.
{
apply ann_P_get in base.
unfold bounded_in in base.
unfold bounded_in.
rewrite subset_cardinal with (s':=VD ∩ (getAnn (reconstr_live Lv ZL G s an))); eauto.
rewrite reconstr_live_G_eq.
rewrite Gincl.
clear; cset_tac.
}
unfold bounded_in.
unfold bounded_in in base.
unfold bounded_in in biG'.
destruct s, an;
simpl;
try destruct a;
simpl; try eassumption;
invc base;
econstructor; try eassumption;
clear biG';
erewrite subset_cardinal; try eassumption;
repeat rewrite union_meet_distr_l;
rewrite Gincl; try reflexivity.
Qed.
Lemma register_bound_loads
(k : nat)
(ZL : list params)
(Lv : list ⦃var⦄)
(VD R : ⦃var⦄)
(s : stmt)
(slot : var → var)
(xs : list var)
(an : ann ⦃var⦄)
(x : var)
: disj VD (map slot VD)
→ R ⊆ VD
→ singleton x ⊆ R
→ of_list xs ⊆ R
→ bounded_in VD k R
→ VD ∩ getAnn (reconstr_live Lv ZL ∅ s an) ⊆ R
→ (∀ (x' : var),
singleton x' ⊆ R
→ of_list xs ⊆ R
→ VD ∩ getAnn (reconstr_live Lv ZL ∅ s an) ⊆ R
→ bounded_in VD k R
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL (singleton x') s an)
)
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL
(singleton x)
(write_moves xs (slot ⊝ xs) s)
(add_anns ∅ (length xs) an)
).
Proof.
intros disj_VD R_VD x_R xs_R
bound_R H base.
unfold bounded_in in bound_R.
general induction xs;
simpl in *; eauto.
rewrite add_anns_S.
rewrite add_union_singleton in xs_R.
apply union_incl_split2 in xs_R as [a_R xs_R].
econstructor.
- unfold bounded_in.
rewrite reconstr_live_write_loads; [ | | eauto];
[ | rewrite xs_R, R_VD; clear; cset_tac].
rewrite subset_cardinal with (s':=VD ∩ R); eauto.
apply incl_meet_split; [clear; cset_tac | ].
setoid_rewrite union_comm at 3.
rewrite union_minus_incl.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split; eauto.
+ rewrite incl_minus.
rewrite H.
clear; cset_tac.
+ rewrite disj_empty_cut; eauto.
× clear; cset_tac.
× rewrite xs_R, R_VD; clear; cset_tac.
+ rewrite <- map_singleton; eauto.
rewrite disj_empty_cut; eauto.
× clear; cset_tac.
× rewrite a_R, R_VD; clear; cset_tac.
+ rewrite <- x_R.
clear; cset_tac.
- eapply IHxs with (R:=R); eauto.
intros x' x'_R' xs_R' al_R' bound_R'.
eapply base; eauto.
rewrite add_union_singleton, a_R, xs_R.
clear; cset_tac.
Qed.
Lemma register_bound_spills
(k : nat)
(ZL : list params)
(Lv : list ⦃var⦄)
(VD R G : ⦃var⦄)
(s : stmt)
(slot : var → var)
(xs : list var)
(an : ann ⦃var⦄)
:
disj VD (map slot VD)
→ R ⊆ VD
→ of_list xs ⊆ R
→ bounded_in VD k R
→ VD ∩ G ⊆ R
→ VD ∩ getAnn (reconstr_live Lv ZL ∅ s an) ⊆ R
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL G s an)
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL
G
(write_moves (slot ⊝ xs) xs s)
(add_anns ∅ (length xs) an)
).
Proof.
intros disj_VD R'_VD xs_R'
bound_G G_rkl H base.
unfold bounded_in in bound_G.
general induction xs;
simpl in *; eauto.
rewrite add_anns_S.
rewrite add_union_singleton in xs_R'.
apply union_incl_split2 in xs_R' as [a_R' xs_R'].
econstructor.
- unfold bounded_in.
rewrite reconstr_live_write_spills; eauto;
[ | rewrite xs_R', R'_VD; clear; cset_tac].
rewrite subset_cardinal with (s':=VD ∩ R); eauto.
apply incl_meet_split; [clear; cset_tac | ].
setoid_rewrite union_comm at 3.
rewrite union_minus_incl.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split; eauto.
+ rewrite incl_minus.
rewrite H.
clear; cset_tac.
+ rewrite xs_R'.
clear; cset_tac.
+ rewrite a_R'.
clear; cset_tac.
- eapply IHxs with (R:=R) ; eauto.
rewrite <- map_singleton; eauto.
rewrite disj_empty_cut; eauto.
+ clear; cset_tac.
+ rewrite a_R', R'_VD.
reflexivity.
+ eapply bounded_in_incl; eauto.
rewrite <- map_singleton; eauto.
rewrite disj_empty_cut; eauto.
× clear; cset_tac.
× rewrite a_R', R'_VD.
reflexivity.
Qed.
Lemma meet_minus_assoc (X : Type) `{OrderedType X} (s t u : ⦃X⦄)
: (s ∩ t) \ u [=] s ∩ (t \ u) .
Proof.
cset_tac.
Qed.
Lemma register_bound_s k ZL Lv VD R G s slot xs ys (an : ann ⦃var⦄)
: disj VD (map slot VD)
→ R ⊆ VD
→ of_list xs ⊆ R
→ of_list ys ⊆ VD
→ cardinal R ≤ k
→ bounded_in VD k (getAnn (reconstr_live Lv ZL ∅ s an) ∪ of_list ys)
→ VD ∩ G ⊆ R
→ VD ∩ getAnn (reconstr_live Lv ZL ∅ s an) ⊆ R ∪ of_list ys
→ (∀ (G' R' : ⦃var⦄),
VD ∩ G' ⊆ R'
→ of_list ys ⊆ R'
→ VD ∩ getAnn (reconstr_live Lv ZL ∅ s an) ⊆ R'
→ cardinal R' ≤ k
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL G' s an)
)
→ ann_P (bounded_in VD k)
(reconstr_live Lv ZL
G
(write_moves (slot ⊝ xs) xs
(write_moves ys (slot ⊝ ys) s)
)
(add_anns ∅ (length xs + length ys) an)
).
Proof.
intros disj_VD R_VD xs_R ys_VD bound_R2 bound_al_L G_R al_R base.
assert (bounded_in VD k R) as bound_R.
{
clear - bound_R2.
unfold bounded_in.
rewrite subset_cardinal; eauto.
cset_tac.
}
rewrite add_anns_add.
destruct ys as [|v ?].
- simpl in ×.
apply register_bound_spills with (R:=R); eauto.
rewrite add_anns_zero.
+ rewrite al_R; clear; cset_tac.
+ eapply base with (R':=R); eauto.
× clear; cset_tac.
× rewrite al_R; clear; cset_tac.
- eapply register_bound_spills with (R:=R); eauto.
{
rewrite reconstr_live_write_loads; eauto.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split.
- rewrite <- meet_minus_assoc.
rewrite al_R.
clear; cset_tac.
- rewrite disj_empty_cut; eauto.
clear; cset_tac.
- clear; cset_tac.
}
simpl in ×.
rewrite add_union_singleton in ys_VD.
apply union_incl_split2 in ys_VD as [v_VD ys_VD].
rewrite add_anns_S.
econstructor.
+ unfold bounded_in.
rewrite reconstr_live_write_loads; eauto.
repeat rewrite union_meet_distr_l.
rewrite <- meet_minus_assoc.
repeat rewrite union_meet_distr_l.
rewrite <- meet_minus_assoc.
rewrite al_R.
assert (∀ (x : var) (s t u v : ⦃var⦄),
((s ∪ {x; t}) \ t ∪ (v ∩ u) ∪ (v ∩ singleton x) ) \ singleton x
⊆ ((s ∪ (v ∩ u))))
as seteq by (clear; cset_tac).
rewrite seteq.
rewrite subset_cardinal with (s':=VD ∩ R); eauto.
repeat apply union_incl_split; eauto.
× clear - R_VD; cset_tac.
× rewrite disj_empty_cut; eauto.
clear; cset_tac.
× rewrite <- map_singleton; eauto.
rewrite disj_empty_cut; eauto.
clear; cset_tac.
× rewrite G_R.
clear - R_VD; cset_tac.
+ eapply register_bound_loads
with (R:=VD ∩ getAnn (reconstr_live Lv ZL ∅ s an)
∪ {v; of_list ys}); eauto.
× rewrite add_union_singleton, v_VD, ys_VD.
clear; cset_tac.
× clear; cset_tac.
× clear; cset_tac.
× unfold bounded_in.
assert (∀ (s t u : ⦃var⦄),
s ∩ (s ∩ t ∪ u) ⊆ s ∩ (t ∪ u))
as setsub by (clear; cset_tac).
rewrite setsub.
assumption.
× intros.
eapply base; eauto.
-- rewrite H.
clear; cset_tac.
-- clear; cset_tac.
-- unfold bounded_in in H2.
rewrite subset_cardinal; eauto.
apply union_incl_split.
++ clear; cset_tac.
++ rewrite union_meet_distr_l.
apply incl_union_right.
apply incl_meet_split; eauto.
rewrite add_union_singleton, v_VD, ys_VD.
clear; cset_tac.
Qed.
Lemma slot_lift_args_RMapp_incl (slot : var → var) (Y : args) RM RMapp Z
: (∀ (n : nat) (y : op), get Y n y → isVar y)
→ (list_union (Ops.freeVars ⊝ Y) ⊆ fst RMapp ∪ snd RMapp)
→ list_union (Ops.freeVars ⊝ slot_lift_args slot RM RMapp Y Z)
⊆ fst RMapp ∪ map slot (snd RMapp).
Proof.
general induction Y; destruct Z; simpl in *; only 1,2,3: eauto with cset.
revert H0.
exploit H as IV; eauto using get. invc IV. simpl.
repeat cases; simpl; norm_lunion; intro;
rewrite IHY; eauto using get; intros; clear IHY H.
- assert (v ∈ fst RMapp ∪ snd RMapp). cset_tac.
unfold choose_y; simpl; repeat cases; simpl.
+ revert COND1. clear_all. cset_tac.
+ revert COND1 COND2. clear_all. cset_tac.
+ revert COND1. clear_all. cset_tac.
+ revert H NOTCOND. clear_all. cset_tac.
+ revert COND1. clear_all. cset_tac.
+ exfalso. cset_tac.
+ revert COND0 COND2. clear_all. cset_tac.
+ revert COND0. clear_all. cset_tac.
+ revert COND0. clear_all. cset_tac.
+ revert COND1. clear_all. cset_tac.
+ exfalso. revert H NOTCOND0 NOTCOND1. cset_tac.
+ revert NOTCOND0 H. clear_all. cset_tac.
- rewrite <- H0. cset_tac.
- assert (v ∈ fst RMapp ∪ snd RMapp). cset_tac.
unfold choose_y; simpl; repeat cases; simpl.
+ revert COND1. clear_all. cset_tac.
+ revert NOTCOND0 H. clear_all. cset_tac.
- rewrite <- H0. cset_tac.
- assert (v ∈ fst RMapp ∪ snd RMapp). cset_tac.
unfold choose_y; simpl; repeat cases; simpl.
+ revert COND0. clear_all. cset_tac.
+ revert NOTCOND1 H. clear_all. cset_tac.
+ revert COND. clear_all. cset_tac.
+ revert NOTCOND2 H. clear_all. cset_tac.
- rewrite <- H0. cset_tac.
Qed.
Lemma register_bounded k (slot : var → var) ZL G Λ R M VD s Lv sl al ra
: cardinal R ≤ k
→ injective_on VD slot
→ disj VD (map slot VD)
→ R ⊆ VD
→ M ⊆ VD
→ fst (getAnn ra) ∪ snd (getAnn ra) ⊆ VD
→ app_expfree s
→ renamedApart s ra
→ spill_sound k ZL Λ (R,M) s sl
→ spill_live VD sl al
→ live_sound Imperative ZL Lv s al
→ PIR2 Equal (merge ⊝ Λ) Lv
→ (∀ (Z : params) n,
get ZL n Z
→ of_list Z ⊆ VD)
→ (∀ (n : nat) Z blv,
get ZL n Z →
get Lv n blv →
of_list Z [<=] blv)
→ VD ∩ G ⊆ R
→ ann_P (bounded_in VD k)
(reconstr_live_do_spill slot Λ ZL G s sl).
Proof.
intros card_R inj_VD disj_VD R_VD M_VD ra_VD
aeFree rena spillSnd spilli lvSnd
H16 Z_VD Z_LV G_R.
unfold reconstr_live_do_spill.
general induction lvSnd;
invc aeFree;
inv rena;
inv spilli;
inv spillSnd;
eapply renamedApart_incl in rena; eauto;
simpl in *; eauto;
unfold count;
simpl;
do 2 rewrite <- elements_length.
- eapply register_bound_s with (VD:=VD) (R:=R); simpl; eauto.
+ rewrite of_list_elements, H19.
reflexivity.
+ rewrite of_list_elements, H20, H19, R_VD, M_VD.
clear; cset_tac.
+ unfold bounded_in.
rewrite of_list_elements.
rewrite reconstr_live_small with (VD:=VD) (R:={x; (R\K ∪ L) \ Kx}) (M:=Sp ∪ M); eauto.
× rewrite subset_cardinal with (s':=R \K ∪ L); eauto.
assert (∀ (x : var) (s t : ⦃var⦄),
({x; s} ∪ t ∪ singleton x) \ singleton x
⊆ s ∪ t)
as setsub by (clear; cset_tac).
rewrite setsub.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split.
-- clear; cset_tac.
-- rewrite disj_empty_cut; eauto.
++ clear; cset_tac.
++ rewrite H19, R_VD, M_VD.
clear; cset_tac.
-- rewrite H22. clear; cset_tac.
-- clear; cset_tac.
-- clear; cset_tac.
× rewrite H20, H19, R_VD, M_VD.
eapply x_VD in H10; eauto.
revert H10; clear; cset_tac.
× rewrite H19, M_VD, R_VD.
clear; cset_tac.
× rewrite rena, <- ra_VD.
eauto.
+ rewrite of_list_elements.
rewrite reconstr_live_small with (VD:=VD) (R:={x; (R\K ∪ L) \ Kx}) (M:=Sp ∪ M); eauto.
× assert (∀ (x : var) (s t : ⦃var⦄),
({x; s} ∪ t ∪ singleton x) \ singleton x
⊆ s ∪ t)
as setsub by (clear; cset_tac).
rewrite setsub.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split.
-- clear; cset_tac.
-- rewrite disj_empty_cut; eauto.
++ clear; cset_tac.
++ rewrite H19, R_VD, M_VD.
clear; cset_tac.
-- rewrite H22. clear; cset_tac.
-- clear; cset_tac.
× rewrite H20, H19, R_VD, M_VD.
eapply x_VD in H10; eauto.
revert H10; clear; cset_tac.
× rewrite H19, M_VD, R_VD.
clear; cset_tac.
× rewrite rena, <- ra_VD.
eauto.
+ intros G' R' G'_R' L_R' al_R' bound_R'.
rewrite of_list_elements in L_R'.
econstructor.
× unfold bounded_in.
rewrite subset_cardinal with (s':=R'); eauto.
-- rewrite union_meet_distr_l.
rewrite G'_R'.
rewrite empty_neutral_union_r in al_R'.
rewrite al_R'.
clear; cset_tac.
× eapply IHlvSnd with (R:={x; (R\K ∪ L) \ Kx})
(M:=Sp ∪ M); try eassumption.
-- eapply Rx_VD with (VD:=VD) (M:=M); eauto.
eapply x_VD; eauto.
-- eauto using M'_VD.
-- rewrite rena, <- ra_VD; eauto.
-- clear; cset_tac.
- destruct rena as [rena1 rena2].
eapply register_bound_s with (VD:=VD) (R:=R); simpl; eauto.
+ rewrite of_list_elements; assumption.
+ rewrite of_list_elements, H25, H24, R_VD, M_VD.
clear; cset_tac.
+ unfold bounded_in.
rewrite of_list_elements.
rewrite subset_cardinal; eauto.
rewrite reconstr_live_small with (VD:=VD) (R:=R\K ∪ L) (M:=Sp ∪ M); eauto.
× rewrite reconstr_live_small with (VD:=VD) (R:=R\K ∪ L) (M:=Sp ∪ M); eauto.
-- repeat rewrite union_meet_distr_l.
clear - H24 H25 H26 R_VD M_VD disj_VD.
assert (VD ∩ map slot (Sp ∪ M) ⊆ R \ K ∪ L) as goal37.
{
rewrite disj_empty_cut; eauto.
- clear; cset_tac.
- rewrite H24, R_VD, M_VD; cset_tac.
}
repeat apply union_incl_split; eauto; try rewrite H26;
clear; cset_tac.
-- rewrite H25, H24, R_VD, M_VD. clear; cset_tac.
-- rewrite H24, R_VD, M_VD; clear; cset_tac.
-- rewrite rena2, <- ra_VD; eauto.
× rewrite H25, H24, R_VD, M_VD. clear; cset_tac.
× rewrite H24, R_VD, M_VD; clear; cset_tac.
× rewrite rena1, <- ra_VD; eauto.
+ rewrite of_list_elements.
rewrite reconstr_live_small with (VD:=VD) (R:=R\K ∪ L) (M:=Sp ∪ M); eauto.
× rewrite reconstr_live_small with (VD:=VD) (R:=R\K ∪ L) (M:=Sp ∪ M); eauto.
-- repeat rewrite union_meet_distr_l.
clear - H24 H25 H26 R_VD M_VD disj_VD.
assert (VD ∩ map slot (Sp ∪ M) ⊆ R ∪ L) as goal37.
{
rewrite disj_empty_cut; eauto.
- clear; cset_tac.
- rewrite H24, R_VD, M_VD; cset_tac.
}
repeat apply union_incl_split; eauto;
try rewrite H26; clear; cset_tac.
-- rewrite H25, H24, R_VD, M_VD. clear; cset_tac.
-- rewrite H24, R_VD, M_VD; clear; cset_tac.
-- rewrite rena2, <- ra_VD; eauto.
× rewrite H25, H24, R_VD, M_VD. clear; cset_tac.
× rewrite H24, R_VD, M_VD; clear; cset_tac.
× rewrite rena1, <- ra_VD; eauto.
+ intros G' R' G'_R' L_R' al_R' bound_R'.
rewrite of_list_elements in L_R'.
econstructor.
× unfold bounded_in.
rewrite subset_cardinal with (s':=R'); eauto.
-- rewrite union_meet_distr_l.
rewrite G'_R'.
rewrite empty_neutral_union_r in al_R'.
rewrite al_R'.
clear; cset_tac.
× eapply IHlvSnd1 with (R:=R\K ∪ L)
(M:=Sp ∪ M); eauto.
-- eapply R'_VD with (VD:=VD) (M:=M); eauto.
-- eapply M'_VD with (VD:=VD) (M:=M) (R:=R); eauto.
-- rewrite rena1, <- ra_VD; eauto.
-- clear; cset_tac.
× eapply IHlvSnd2 with (R:=R\K ∪ L)
(M:=Sp ∪ M); eauto.
-- eapply R'_VD with (VD:=VD) (M:=M); eauto.
-- eapply M'_VD with (VD:=VD) (M:=M) (R:=R); eauto.
-- rewrite rena2, <- ra_VD; eauto.
-- clear; cset_tac.
- eapply register_bound_s with (VD:=VD) (R:=R); simpl; eauto.
+ rewrite of_list_elements; assumption.
+ rewrite of_list_elements, H13, H12, R_VD, M_VD.
clear; cset_tac.
+ erewrite nth_zip; eauto.
unfold bounded_in.
rewrite subset_cardinal; eauto.
erewrite !get_nth; eauto using map_get_1. simpl.
rewrite slot_lift_args_RMapp_incl; simpl; eauto; [|rewrite H22; reflexivity].
rewrite of_list_elements.
eapply PIR2_nth in H16; eauto; dcr. inv_get. unfold merge in H8. simpl in ×.
rewrite of_list_slot_lift_params; [|rewrite Z_LV; eauto; rewrite H8; reflexivity].
simpl in ×.
rewrite H9 in *; clear H9 D'.
rewrite H23.
assert (M'VD:M' [<=] VD). {
rewrite H24, H12, R_VD, M_VD. eauto with cset.
}
assert (M_fVD:M_f ⊆ VD). {
rewrite Mf_VD with (R:=R) (M:=M) (VD:=VD); eauto.
}
rewrite empty_neutral_union_r.
repeat rewrite union_meet_distr_l.
rewrite (@disj_empty_cut VD); eauto.
unfold slot_merge. simpl.
rewrite minus_dist_union.
repeat rewrite union_meet_distr_l.
rewrite (@incl_minus _ _ (map slot M_f)).
rewrite (@disj_empty_cut VD); eauto.
rewrite empty_neutral_union_r.
assert (of_list Z ∩ R_f ⊆ of_list Z \ (M_f \ R_f) ∪ map slot (of_list Z \ (R_f \ M_f))). {
clear_all. cset_tac.
}
rewrite <- H4.
revert H20. clear_all. cset_tac.
+ erewrite nth_zip; eauto.
rewrite slot_lift_args_RMapp_incl; eauto; simpl; [|rewrite H22; reflexivity].
erewrite !get_nth; eauto using map_get_1.
rewrite of_list_elements. unfold slot_merge; simpl.
rewrite slp_union_minus_incl; eauto; simpl.
assert (M'VD:M' [<=] VD). {
rewrite H24, H12, R_VD, M_VD. eauto with cset.
}
assert (M_fVD:M_f ⊆ VD). {
rewrite Mf_VD with (R:=R) (M:=M) (VD:=VD); eauto.
}
× rewrite H20, H23.
rewrite empty_neutral_union_r.
repeat rewrite union_meet_distr_l.
rewrite (@disj_empty_cut VD); eauto.
rewrite minus_incl with (t:=map slot (of_list Z0)).
rewrite (@disj_empty_cut VD); eauto.
clear_all. cset_tac.
× rewrite Rf_VD with (R:=R) (M:=M) (VD:=VD) (L:=L); eauto.
× rewrite Mf_VD with (R:=R) (M:=M) (VD:=VD); eauto.
+ intros G' R'' G'_R' L_R' al_R' bound_R'.
econstructor.
unfold bounded_in.
rewrite subset_cardinal; eauto.
rewrite union_meet_distr_l.
rewrite empty_neutral_union_r in al_R'.
rewrite al_R', G'_R'.
clear; cset_tac.
- eapply register_bound_s with (VD:=VD) (R:=R); simpl; eauto.
+ rewrite of_list_elements; assumption.
+ rewrite of_list_elements, H9, H8, R_VD, M_VD.
clear; cset_tac.
+ unfold bounded_in.
rewrite of_list_elements.
rewrite subset_cardinal; eauto.
rewrite H10.
clear; cset_tac.
+ rewrite H10, of_list_elements.
clear; cset_tac.
+ intros G' R' G'_R' L_R' al_R' bound_R'.
rewrite empty_neutral_union_r in al_R'.
econstructor.
unfold bounded_in.
rewrite subset_cardinal; eauto.
rewrite union_meet_distr_l, G'_R', al_R'.
clear; cset_tac.
- destruct rena as [renaF rena2].
eapply register_bound_s with (VD:=VD) (R:=R); simpl; eauto.
+ rewrite of_list_elements; assumption.
+ rewrite of_list_elements, H29, H28, R_VD, M_VD; clear; cset_tac.
+ unfold bounded_in.
rewrite fst_zip_pair; eauto with len.
rewrite slot_lift_params_app; eauto with len.
rewrite getAnn_map_setTopAnn.
rewrite Take.take_eq_ge;
[|unfold slot_merge; len_simpl; rewrite <- H31, <- H32; omega].
rewrite slot_merge_app.
rewrite subset_cardinal; eauto.
rewrite reconstr_live_small with (VD:=VD) (R:=R\K∪L) (M:=Sp ∪ M); eauto.
× rewrite of_list_elements, !empty_neutral_union_r.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split.
-- clear; cset_tac.
-- clear; cset_tac.
-- rewrite disj_empty_cut; eauto.
++ clear; cset_tac.
++ rewrite H28, R_VD, M_VD; clear; cset_tac.
-- clear; cset_tac.
× eapply R'_VD with (VD:=VD) (L:=L) (M:=M); eauto.
× rewrite H28, R_VD, M_VD; clear; cset_tac.
× rewrite rena2, <- ra_VD; eauto.
× eapply getAnn_als_EQ_merge_rms; eauto.
× intros.
eapply get_ofl_VD; eauto.
+ rewrite fst_zip_pair; eauto with len.
rewrite slot_lift_params_app; eauto with len.
rewrite getAnn_map_setTopAnn.
rewrite Take.take_eq_ge;
[|unfold slot_merge; len_simpl; rewrite <- H31, <- H32; omega].
rewrite slot_merge_app.
rewrite reconstr_live_small with (VD:=VD) (R:=R\K∪L) (M:=Sp ∪ M); eauto.
× rewrite of_list_elements, !empty_neutral_union_r.
repeat rewrite union_meet_distr_l.
repeat apply union_incl_split.
-- clear; cset_tac.
-- clear; cset_tac.
-- rewrite disj_empty_cut; eauto.
++ clear; cset_tac.
++ rewrite H28, R_VD, M_VD; clear; cset_tac.
× eapply R'_VD with (VD:=VD) (L:=L) (M:=M); eauto.
× rewrite H28, R_VD, M_VD; clear; cset_tac.
× rewrite rena2, <- ra_VD; eauto.
× eapply getAnn_als_EQ_merge_rms; eauto.
× intros.
eapply get_ofl_VD; eauto.
+ intros G' R' G'_R' L_R' al_R' bound_R'.
rewrite fst_zip_pair; eauto with len.
rewrite slot_lift_params_app; eauto with len.
rewrite getAnn_map_setTopAnn.
rewrite Take.take_eq_ge;
[|unfold slot_merge; len_simpl; rewrite <- H31, <- H32; omega].
rewrite slot_merge_app.
rewrite fst_zip_pair in al_R'; eauto with len.
rewrite slot_lift_params_app in al_R'; eauto with len.
rewrite getAnn_map_setTopAnn in al_R'.
rewrite Take.take_eq_ge in al_R';
[|unfold slot_merge; len_simpl; rewrite <- H31, <- H32; omega].
rewrite slot_merge_app in al_R'.
econstructor.
× unfold bounded_in.
rewrite subset_cardinal; eauto.
rewrite union_meet_distr_l.
rewrite empty_neutral_union_r in al_R'.
rewrite G'_R', al_R'.
clear; cset_tac.
× intros; inv_get.
rewrite <- reconstr_live_setTopAnn.
exploit H10 as funConstr; eauto.
exploit renaF as renaF'; eauto.
exploit H34 as spillSnd'; eauto.
exploit H20 as rm_VD; eauto.
destruct rm_VD as [f_x3_VD s_x3_VD]; eauto.
rewrite pair_eta with (p:=x3) in spillSnd'.
destruct funConstr as [funConstr _].
apply incl_from_union_eq in funConstr as funConstr1.
rewrite union_comm in funConstr.
apply incl_from_union_eq in funConstr as funConstr2.
simpl.
eapply H1 with (R:=fst x3) (M:=snd x3); eauto.
-- rewrite renaF', <- ra_VD; eauto.
-- eapply getAnn_als_EQ_merge_rms; eauto.
-- intros.
eapply get_ofl_VD; eauto.
-- intros.
eapply get_app_cases in H4 as [?|[? ?]]; inv_get.
edestruct H2; eauto. len_simpl.
eapply get_app_ge in H14. len_simpl.
rewrite <- H in ×.
eapply Z_LV; eauto. len_simpl. rewrite <- H. eauto.
-- setoid_rewrite pair_eta with (p:=x3) at 1.
rewrite pair_eta with (p:=x3) in H23.
eapply al_sub_RfMf in H23; eauto.
rewrite ofl_slp_sub_rm; eauto.
++ rewrite union_meet_distr_l.
apply union_incl_split.
** clear; cset_tac.
** rewrite disj_empty_cut; eauto.
clear; cset_tac.
++ exploit H2 as H2'; eauto.
× eapply IHlvSnd with (R:=R\K ∪ L) (M:=Sp ∪ M); eauto.
-- eapply R'_VD with (VD:=VD) (L:=L) (M:=M); eauto.
-- rewrite H28, R_VD, M_VD; eauto.
clear; cset_tac.
-- rewrite rena2, <- ra_VD; eauto.
-- apply getAnn_als_EQ_merge_rms; eauto.
-- intros.
eapply get_ofl_VD; eauto.
-- intros.
eapply get_app_cases in H4 as [?|[? ?]]; inv_get.
edestruct H2; eauto. len_simpl.
eapply get_app_ge in H5. len_simpl.
rewrite <- H in ×.
eapply Z_LV; eauto. len_simpl. rewrite <- H. eauto.
-- clear; cset_tac.
Qed.