Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.
Require Import ihc drf memsafe initread path.
Require Import GpsSepAlg permission.
Set Implicit Arguments.
Lemma upd_fin T:
∀ (ga: nat → option T) max x (FIN: ∀ n, max < n → ga n = None) l (L: max < l),
∃ max', ∀ n, max' < n → (mupd ga l x) n = None.
Proof.
ins; ∃ l; ins.
unfold mupd; desf; desf.
by rewrite ltnn in H.
by apply FIN; eauto using ltn_trans.
Qed.
Lemma agrees_trans PS PSg sb rf V hmap hmap' hmap'':
@agrees PS PSg sb rf V hmap hmap' → agrees sb rf V hmap' hmap'' → agrees sb rf V hmap hmap''.
Proof.
split; ins.
by rewrite (proj1 (H _ IN b)), (proj1 (H0 _ IN b)).
by rewrite (proj2 (H _ IN b)), (proj2 (H0 _ IN b)).
Qed.
Lemma new_ghost_def PS PSg :
∀ hf (g: ghost_resource) l g' (GL: g l = None),
Hdef hf g +!+ gsingl _ _ l g' ≠ @Hundef PS PSg.
Proof.
ins; rewrite hplus_unfold; desf.
destruct n; unnw; split.
by ins; apply hvplusDEFC.
unfold gres_plus; des_eqrefl; try edone.
inv_lplus2 x; ins; desf; desf.
by rewrite GL in EQ.
rewrite olift_plusC in EQ; ins.
apply plift_plusC; ins.
apply salg_plusC.
Qed.
Lemma no_unallocated_ghosts PS PSg:
∀ lab sb rf mo hmap ga V
(ACYCLIC: IrreflexiveHBuRF sb rf)
(CONS_A: ConsistentAlloc lab)
(CONS_RF: ConsistentRF_basic lab sb rf mo)
(HC: hist_closed sb rf V)
(VLD: ∀ e, In e V → hmap_valid lab sb rf hmap ga e)
max (GAfin: ∀ n, max < n → ga n = None)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
hf g (MAP: hmap (edge) = @Hdef PS PSg hf g),
∀ n, max < n → g n = None.
Proof.
ins; apply NNPP; intro N.
exploit ghost_allocated; try exact CONS_RF; try exact VLD; try exact OLDq; try exact N;
ins; eauto; desf; exploit GAfin; eauto; ins; instantiate; congruence.
Qed.
Lemma clos_trans_sb_implies_hbUrf:
∀ sb rf a b, clos_trans _ sb a b → happens_before_union_rf sb rf a b.
Proof.
ins; induction H; vauto.
Qed.
Lemma allocating_new_ghosts_helper:
∀ ga (e: actid) max l g (gnew : ghost_resource)
(NG: ∀ x : nat, gnew x ≠ None ↔ ga x = Some e)
(GAfin: ∀ n : nat, max < n → ga n = None)
(MAX: max < l),
∀ x, (gres_plus_total gnew (gres_one l (Some g))) x ≠ None ↔
mupd ga l (Some e) x = Some e.
Proof.
split; ins.
+ rewrite gres_plus_totalC in ×.
unfold mupd; desf; desf.
apply NG.
unfold gres_plus_total in *; desf.
unfold gres_plus in *; des_eqrefl; try done.
desf; ins.
inv_lplus x. desf; desf. ins. desf.
congruence.
+ assert (NL: gnew l = None) by (apply NNPP; intro L; rewrite NG in L; apply GAfin in MAX; congruence).
unfold gres_plus_total; desf; desf.
- unfold gres_plus in *; des_eqrefl; try done.
desf; ins.
inv_lplus x. desf; desf.
by rewrite NL in EQ; ins; congruence.
unfold olift_plus in EQ; desf; try congruence.
rewrite mupdo in H; firstorder.
- unfold gres_plus in Heq; des_eqrefl; try done.
inv_lplus2 y.
unfold olift_plus in EQ; desf.
inv Heq0; desf; desf.
Qed.
Lemma allocating_new_ghosts_preserves_validity PS PSg:
∀ lab sb rf hmap ga e next max l g
(ACYCLIC: IrreflexiveHBuRF sb rf)
(VLD: hmap_valid lab sb rf hmap ga e)
(GAfin: ∀ n, max < n → ga n = None)
(SB: sb e next) (N: max < l)
(gNEW: ∀ edge (EV: edge_valid lab sb rf edge) (FST: hb_fst edge = e)
hf gh (MAP: hmap edge = Hdef hf gh), gh l = None),
hmap_valid lab sb rf
(mupd hmap (hb_sb e next) (hmap (hb_sb e next) +!+ gsingl PS PSg l (Some g)))
(mupd ga l (Some e)) e.
Proof.
unfold hmap_valid; ins; desc.
assert (gEQ: gheap PS PSg (gres_plus_total gnew (gres_one l (Some g)))
= gheap _ _ gnew +!+ gsingl _ _ l (Some g)).
{
clear VLD0 gNEW.
rewrite hplus_unfold; desf.
destruct n; split; try done.
unfold gres_plus; des_eqrefl; try done.
inv_lplus2 x.
unfold olift_plus in EQ; desf.
inv Heq0; desf; desf.
apply GAfin in N.
assert (X: gnew x ≠ None) by congruence.
rewrite NG in X; congruence.
}
desf; desc; ∃ (gres_plus_total gnew (gres_one l (Some g))); split;
try exact (allocating_new_ghosts_helper _ _ _ _ _ NG GAfin N).
{
assert (EQ': hsum (@map hbcase (heap PS PSg)
(mupd hmap (hb_sb e next) (hmap (hb_sb e next) +!+ gsingl _ _ l (Some g)))
(map (hb_sb e) posts))
= hsum (map hmap (map (hb_sb e) posts)) +!+ gsingl _ _ l (Some g)).
{
apply qOK in SB.
apply In_split in SB; desf; clear - qND.
rewrite !map_app; ins.
rewrite mupds, !map_upd_irr;
solve [ by rewrite !hsum_app, !hsum_cons, !hplusA, (hplusC (gheap _ _ _)) |
intros ? IN EQ; apply In_split in IN; desf;
rewrite <- ?app_assoc in qND; ins;
apply nodup_app in qND; desf;
apply nodup_cons in qND0; desf;
by destruct qND0; find_in_list
].
}
∃ pres, posts; repeat (split; try done); rewrite EQ'.
× rewrite mupdo; try done.
rewrite hdef_alt in DEF; desf.
rewrite hplusA, <- hplusAC, DEF, hplusC.
apply new_ghost_def.
apply NNPP; intro NALL.
eapply hplus_galloc in DEF; eauto; desf.
+ eapply hsum_galloc in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
apply gNEW in DEF; ins.
by apply qOK.
+ apply gNEW in DEF; ins.
by red; rewrite Heq.
× rewrite map_upd_irr.
2: by ins; intro; desf; eapply ACYCLIC; vauto.
rewrite gEQ, mupdo; try done.
by rewrite hplusA, (hplusC (gheap _ _ _) (hmap _)), <- !hplusA, <- EQ.
}
{
∃ pre, post, hf, g0; repeat (split; try done); rewrite (proj2 qU _ SB) in ×.
× rewrite mupdo; try done.
by intro; desf; eapply ACYCLIC; vauto.
× rewrite hdef_alt in DEF; desc.
rewrite mupds, DEF.
apply new_ghost_def.
by eapply gNEW; eauto.
× rewrite !mupds, !gEQ; desf; rewrite qEQ, !hplusA; eauto.
}
{
∃ pre, post, hf, g0; repeat (split; try done); rewrite (proj2 qU _ SB) in ×.
× rewrite hdef_alt in qD; desc.
rewrite mupds, qD.
apply new_ghost_def.
by eapply gNEW; eauto.
× rewrite mupdo; try done.
by intro; desf; eapply ACYCLIC; vauto.
× destruct DISJ; desc; [left | right]; repeat (split; try done).
+ rewrite mupds, mupdo, gEQ, qEQ, !hplusA; try done.
by intro; desf; eapply ACYCLIC; vauto.
+ ∃ rfs, hr, hF, P; repeat (split; try done); rewrite ?map_upd_irr; ins.
eby eexists; split.
by rewrite mupds, gEQ, qEQ, !hplusA.
}
{
∃ pre, post, hf, g0; repeat (split; try done); rewrite (proj2 qU _ SB) in ×.
× rewrite mupdo; try done.
by intro; desf; eapply ACYCLIC; vauto.
× destruct DISJ; desc; [left | right]; repeat (split; try done).
+ by ∃ Perm; rewrite mupds, gEQ, qEQ, hplusA.
+ rewrite hdef_alt in DEF; desc.
rewrite mupds, DEF.
apply new_ghost_def.
by eapply gNEW; eauto.
+ ∃ rfs, hr, hF, P, (sbg +!+ gsingl _ _ l (Some g)), rfg;
repeat (split; try done); rewrite ?map_upd_irr; ins.
- by rewrite mupds, qEQ, !hplusA.
- rewrite mupds, mupdo, !hplusA; try done.
rewrite hdef_alt in DEF; desc.
rewrite hplusAC, DEF, hplusC.
apply new_ghost_def.
apply NNPP; intro NL.
clear TYP.
eapply hplus_galloc in DEF; eauto; desf.
by destruct DEF0; eapply gNEW; eauto.
eapply hplus_galloc in DEF; eauto; desf.
eapply hsum_galloc in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
destruct DEF2; eapply gNEW; eauto; ins.
by apply rfsOK.
destruct DEF1; eapply gNEW; eauto; ins.
by red; rewrite Heq.
- by rewrite hplusC, hplusAC, <- hplusA, ghostEQ.
- rewrite mupdo; try done.
eby eexists; split.
}
{
∃ pre, post, rfsIn, rfsOut; repeat (split; try done); rewrite (proj2 qU _ SB) in *;
rewrite ?map_upd_irr, ?mupds; ins.
× rewrite hdef_alt in DEF; desc.
rewrite mupdo, !hplusA, hplusAC, DEF, hplusC; try done.
apply new_ghost_def.
apply NNPP; intro NL.
eapply hplus_galloc in DEF; eauto; desf.
by destruct DEF0; eapply gNEW; eauto.
eapply hplus_galloc in DEF; eauto; desf.
eapply hsum_galloc in DEF; eauto; desf.
repeat (rewrite In_map in *; desf).
destruct DEF2; eapply gNEW; eauto; ins.
by apply rfsOutOK.
destruct DEF1; eapply gNEW; eauto; ins.
by red; rewrite Heq.
× ∃ P, QQ, hrel, hrel', hacq, hacq', ht, hF, (sbg +!+ gsingl _ _ l (Some g)), rfg; repeat (split; try done).
+ rewrite mupdo; try done.
by intro; desf; eapply ACYCLIC; vauto.
+ by rewrite qEQ, !hplusA.
+ by rewrite hplusC, hplusAC, <- hplusA, ghostEQ.
+ eexists; (repeat split; try edone).
+ eexists; (repeat split; try edone).
}
{
∃ pre, post; repeat (split; try done); rewrite (proj2 qU _ SB) in *; rewrite ?mupds.
× rewrite hdef_alt in DEF; desc.
rewrite DEF.
apply new_ghost_def.
by eapply gNEW; eauto.
× ∃ hF, hrel, hrel', hacq, hacq'; repeat (split; try done).
+ rewrite mupdo; try done.
by intro; desf; eapply ACYCLIC; vauto.
+ by rewrite qEQ, gEQ, !hplusA.
}
Qed.
Theorem rule_ghost_intro PS PSg :
∀ P E QQ (T: triple P E QQ) PCM (IN: In PCM PSg) g,
triple P E (fun v ⇒ Astar (QQ v) (Aexists (fun l ⇒ (@Aghost PS PSg PCM IN l g)))).
Proof.
Opaque assn_sem.
ins; apply triple_helper_start; ins.
destruct (eqP fst lst) as [|NEQ]; subst.
{
exploit (T _ _ _ _ _ _ SEM); try edone.
instantiate (1 := 2); ins; desc.
clear POST RELY.
specialize (GUAR _ (exp_sem_lst _ _ _ _ _ _ _ SEM) NIN HC0); desc.
clear RELY GUAR.
assert (VALID' := VALID0); red in VALID0; desc; red in VALIDS; desc.
remember (mupd hmap' (hb_sb lst next) ((hmap' (hb_sb lst next)) +!+
gsingl _ _ (S max) (Some (existT (fun m : salg_mod ⇒ m) PCM g))))
as hmap''.
∃ hmap''.
assert (hmap_valids_strong lab sb rf hmap'' (lst :: V)).
{
subst hmap''; split.
{
∃ (mupd ga (S max) (Some lst)).
split.
eby eapply upd_fin.
red; ins; desf.
{
red in CONS; ins; desc.
eapply allocating_new_ghosts_preserves_validity; eauto.
by by exact (proj1 LST).
by ins; eapply no_unallocated_ghosts; eauto; ins; eauto.
}
{
eapply hmap_irr_change_valid; eauto.
× split; ins.
+ rewrite mupdo; try done.
intro; subst x.
exploit (GAfin (S max)); ins; congruence.
+ unfold mupd in H; desf; desf.
× ins; rewrite mupdo; try done.
intro; subst edge; ins; desf.
red in LST; desc.
destruct NIN; eapply HC; vauto.
}
}
{
red; ins. rewrite mupdo.
2: by intro; subst edge; clear - NIN0 H; firstorder.
apply not_or_and in NIN0; desc.
apply (RESTR e); try done.
intro; desf.
}
}
split; [|split]; try done.
{
eapply agrees_trans; try done.
red; ins.
subst hmap''; rewrite !mupdo; eauto; congruence.
}
{
apply safe_final1; try done.
ins. generalize (proj2 LST _ SB); intro; subst next0.
red; desf; rewrite !mupds.
exploit POST; eauto.
simpl; intro OLDq; desf.
∃ hFR', (hq +!+ gsingl _ _ (S max) (Some (existT (fun m : salg_mod ⇒ m) PCM g))).
repeat (apply conj).
× rewrite hdef_alt in OLDq; desc; rewrite OLDq in ×.
apply new_ghost_def.
red in CONS; ins; desc.
eapply no_unallocated_ghosts; eauto; ins; eauto.
× by rewrite OLDq0, !hplusA, (hplusC hFR'), !(hplusAC (gheap _ _ _)).
× Transparent assn_sem. hnf. Opaque assn_sem.
eexists _, _; repeat (apply conj; try edone).
+ rewrite hdef_alt in OLDq; desc; rewrite OLDq in ×.
symmetry in OLDq0; assert (HQ := hplus_def_inv_l _ _ OLDq0); desc; rewrite HQ in ×.
apply new_ghost_def.
eapply hplus_gnalloc_l; eauto.
red in CONS; ins; desc.
by eapply no_unallocated_ghosts; eauto; ins; eauto.
+ by apply assn_sem_exists; ∃ (S max).
}
}
{
exploit (T _ _ _ _ _ _ SEM); try edone.
instantiate (1 := S (S n)); remember (S n) as n'; intro X; simpls; desc.
clear POST RELY.
specialize (GUAR _ (exp_sem_fst _ _ _ _ _ _ _ SEM) NIN HC0); desc.
∃ hmap'; repeat (split; try done).
assert (LLL: ¬ In lst (fst :: V)).
{
simpl; intro; desf.
destruct NIN; eapply hist_closedD; eauto.
exploit exp_sem_lst_reach; eauto.
eby eapply exp_sem_fst.
rewrite clos_refl_transE; ins; desf.
by apply clos_trans_sb_implies_hbUrf.
}
revert SAFE LLL VALID0 HC0; generalize (fst :: V).
generalize hmap'.
subst n'.
clear - T SEM CONS LST UNIQ LR.
induction n; intros; desc; try done.
simpl; unfold NW; repeat split; intros; try done.
{ assert (¬ In lst acts_ctx).
{
apply exp_sem_lst in SEM; clear - SEM UNIQ.
intro I; apply In_split in SEM; apply In_split in I; desf.
rewrite <- app_assoc in UNIQ; ins.
apply nodup_app in UNIQ; desf.
apply nodup_cons in UNIQ0; desf.
destruct UNIQ0; find_in_list.
}
ins; apply IHn; desc; try done.
by unnw; split; [|split]; solve [ins; desf | exploit RELY; eauto; ins; desc; eauto].
by simpl; intro; desf.
}
{
destruct (eqP a lst); subst.
{
ins; desc; clear POST RELY IHn.
specialize (GUAR _ (exp_sem_lst _ _ _ _ _ _ _ SEM) NIN HC'); desc.
clear RELY GUAR.
assert (VALID'0 := VALID); red in VALID; desc; red in VALIDS; desc.
remember (mupd hmap'0 (hb_sb lst next) ((hmap'0 (hb_sb lst next)) +!+
gsingl _ _ (S max) (Some (existT (fun m : salg_mod ⇒ m) PCM g))))
as hmap''.
∃ hmap''.
assert (hmap_valids_strong lab sb rf hmap'' (lst :: l)).
{
subst hmap''; split.
{
∃ (mupd ga (S max) (Some lst)).
split.
eby eapply upd_fin.
red; ins; desf.
{
red in CONS; ins; desc.
eapply allocating_new_ghosts_preserves_validity; eauto.
by by exact (proj1 LST).
by ins; eapply no_unallocated_ghosts; eauto; ins; eauto.
}
{
eapply hmap_irr_change_valid; eauto.
× split; ins.
+ rewrite mupdo; try done.
intro; subst x.
exploit (GAfin (S max)); ins; congruence.
+ unfold mupd in H; desf; desf.
× ins; rewrite mupdo; try done.
intro; subst edge; ins; desf.
red in LST; desc.
destruct NIN; eapply HC0; vauto.
}
}
{
red; ins. rewrite mupdo.
2: by intro; subst edge; clear - NIN0 H; firstorder.
apply not_or_and in NIN0; desc.
apply (RESTR e); try done.
intro; desf.
}
}
split; [|split]; try done.
{
eapply agrees_trans; try done.
red; ins.
subst hmap''; rewrite !mupdo; eauto; congruence.
}
{
apply safe_final1; try done.
ins. generalize (proj2 LST _ SB); intro; subst next0.
red; desf; rewrite !mupds.
exploit POST; eauto.
simpl; intro OLDq; desf.
∃ hFR', (hq +!+ gsingl _ _ (S max) (Some (existT (fun m : salg_mod ⇒ m) PCM g))).
repeat (apply conj).
× rewrite hdef_alt in OLDq; desc; rewrite OLDq in ×.
apply new_ghost_def.
red in CONS; ins; desc.
eapply no_unallocated_ghosts; eauto; ins; eauto.
× by rewrite OLDq0, !hplusA, (hplusC hFR'), !(hplusAC (gheap _ _ _)).
× Transparent assn_sem. hnf. Opaque assn_sem.
eexists _, _; repeat (apply conj; try edone).
+ rewrite hdef_alt in OLDq; desc; rewrite OLDq in ×.
symmetry in OLDq0; assert (HQ := hplus_def_inv_l _ _ OLDq0); desc; rewrite HQ in ×.
apply new_ghost_def.
eapply hplus_gnalloc_l; eauto.
red in CONS; ins; desc.
by eapply no_unallocated_ghosts; eauto; ins; eauto.
+ by apply assn_sem_exists; ∃ (S max).
}
}
{
remember (S n) as n'; ins; desc.
exploit GUAR; eauto; ins; desc.
eexists; repeat (split; try edone); try eapply IHn; eauto.
simpl; intro; desf.
}
}
}
Transparent assn_sem.
Qed.
This page has been generated by coqdoc