Commit 6b56559f authored by Hai Dang's avatar Hai Dang
Browse files

More minor cleanup in Treiber stack graph proof

parent 4f7546c5
......@@ -209,7 +209,6 @@ Proof.
intros e' n' In' Eq'.
assert (Sube':= Sub _ In').
destruct (ET' e') as [[v' Eqv'] _]. { by exists n'. }
(* TODO: remove lookup_fmap_Some'. *)
move : Eqv' => /list_lookup_fmap_inv' [eV' [Eqv' Eqe']].
assert (Eqe := prefix_lookup_inv _ _ _ _ Eqe' Sube' SubE).
destruct (ET e') as [_ [n'' ETx]]. { exists v'. by rewrite Eqe /= Eqv'. }
......@@ -631,6 +630,35 @@ Proof.
- eauto with iFrame.
Qed.
(* TODO: move *)
Lemma own_loc_na_own_loc_prim_subjectively n q v :
n {q} v (q' : Qp) (C' : cell), <subj> n p{q'} C'.
Proof.
rewrite own_loc_na_own_loc_prim. iDestruct 1 as (C) "En".
iExists q, C. iNext. by iApply monPred_subjectively_intro.
Qed.
Lemma own_loc_na_view_at_prim n q v V :
@{V} n {q} v (q' : Qp) (C' : cell), <subj> n p{q'} C'.
Proof.
rewrite own_loc_na_own_loc_prim_subjectively.
iDestruct 1 as (q' C) "En". iExists q', C. iNext.
by rewrite view_at_subjectively monPred_subjectively_idemp.
Qed.
Lemma all_slocs_node_access_prim t0 LVs t (l' : loc) Vb :
fst <$> toHeadHist t0 LVs !! t = Some #l'
@{Vb} all_slocs LVs (q' : Qp) (C' : cell), <subj> l' p{q'} C'.
Proof.
intros ([] & Eq' & (? & on & Eq & Eq2)%toHeadHist_lookup_Some)%lookup_fmap_Some'.
simpl in Eq'. subst v.
assert (on = Some l') as ->.
{ clear -Eq. destruct on; by inversion Eq. } clear Eq.
apply elem_of_list_lookup_2 in Eq2.
rewrite (all_slocs_node_next_access _ _ _ Eq2).
iIntros "[As En]". iDestruct "En" as (q' on) "En".
by rewrite view_at_view_at (shift_0 l') own_loc_na_view_at_prim.
Qed.
Lemma all_slocs_app LVs LVs' :
all_slocs (LVs ++ LVs') all_slocs LVs all_slocs LVs'.
Proof. by rewrite /all_slocs -big_sepL_app. Qed.
......@@ -1020,8 +1048,8 @@ Proof.
with "[$sH1' $H $sV1' $As]"); [done|done|done|solve_ndisj|..].
{ intros t' v' NE. rewrite lookup_fmap_Some'.
intros ([] & <- & ?). by eapply toHeadHist_lookup_Some_is_comparable_nullable_loc. }
{ iSplit; [done|]. iIntros "!>". destruct on' as [n'|]; [|done].
simpl. iIntros "As !>".
{ iSplit; [done|]. iIntros "{#} !>". destruct on' as [n'|]; [|done].
simpl. clear -Eqth1 Subζ0. iIntros "As !>".
(* acquire a fraction of n' *)
rewrite /Pr (all_slocs_node_next_access _ n' V0); last first.
{ eapply lookup_weaken in Eqth1; [|apply Subζ0]. simpl in Eqth1.
......@@ -1030,21 +1058,8 @@ Proof.
move : Eq1. by apply elem_of_list_lookup_2. }
iDestruct "As" as "[As oN]". iDestruct "oN" as (qn' on') "oN".
rewrite (view_at_view_at _ V0). iSplitL "oN".
- rewrite (shift_0 n') (own_loc_na_own_loc_prim n').
iDestruct (view_at_subjectively with "oN") as (C) "oN".
iExists qn', C. by iFrame "oN".
- (* TODO: make a lemma *)
iIntros (t l'). rewrite lookup_fmap_Some'.
iIntros ((_ & ([] & Eq' & (? & on & Eq & Eq2)%toHeadHist_lookup_Some) & _)).
simpl in Eq'. subst v0.
assert (on = Some l') as ->.
{ clear -Eq. destruct on; by inversion Eq. } clear Eq.
apply elem_of_list_lookup_2 in Eq2.
rewrite (all_slocs_node_next_access _ _ _ Eq2).
iDestruct "As" as "[As En]". iDestruct "En" as (q' on) "En".
rewrite view_at_view_at (shift_0 l') (own_loc_na_own_loc_prim l').
iDestruct (view_at_subjectively with "En") as (C) "En".
iExists q', C. iFrame "En". }
- by rewrite (shift_0 n') own_loc_na_view_at_prim.
- iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). }
iIntros (b t' v' Vr V2 ζ2 ζn) "(F & #sV2 & #sH2 & H & As & CASE)".
iDestruct "F" as %([Subζh02 Subζ2] & Eqt' & MAXt' & LeV1'). rewrite /Pr. clear Pr.
......@@ -1209,10 +1224,10 @@ Proof.
+ intros InT. inversion 1. subst e. exfalso. apply NInCD, codom_correct. by exists n1.
- intros n0 e0.
rewrite /popped_nodes list_to_set_cons dom_insert_L difference_union_distr_l_L.
rewrite subseteq_empty_difference_L; [|clear;set_solver].
rewrite subseteq_empty_difference_L; [|set_solver-].
rewrite left_id_L difference_union_distr_r_L difference_disjoint_L;
[|clear -FRnT; set_solver].
rewrite comm_L subseteq_intersection_1_L; [|clear; set_solver].
rewrite comm_L subseteq_intersection_1_L; [|set_solver-].
case (decide (n0 = n)) => [->|NEqn].
+ rewrite lookup_insert. inversion 1. subst e0. split.
* clear -FRnT. by intros []%elem_of_difference.
......@@ -1259,7 +1274,7 @@ Proof.
iAssert (@{Vb V2} (all_slocs LVs' @{Vw} in_slocs E' T' S'))%I
with "[As Is Hnd SYE]" as "[As Is]".
{ iDestruct (view_at_mono _ Vw with "Hnd") as "Hnd"; [solve_lat|eauto|].
iDestruct "Hnd" as "[[Hn1 Hn2] Hd]". iClear "#". iSplitL "As Hn1".
iDestruct "Hnd" as "[[Hn1 Hn2] Hd] {#}". iSplitL "As Hn1".
- rewrite(all_slocs_app (_ ++ _)). iSplitL "As"; [by iFrame "As"|].
rewrite /all_slocs /=. iSplitL; [|done]. iExists _, (hd_error S2).
rewrite view_at_view_at /=. iFrame "Hn1".
......@@ -1715,22 +1730,9 @@ Proof.
{ intros t v NE. rewrite lookup_fmap_Some'.
intros ([] & <- & ?).
by eapply (toHeadHist_lookup_Some_is_comparable_nullable_loc _ _ _ _ _ (Some n)). }
{ simpl. iFrame "HRE". iIntros "!> [oN As] !>". iSplitL "oN".
- rewrite shift_0.
iDestruct (own_loc_na_own_loc_prim with "oN") as (C) "oN".
iExists q, C. rewrite -monPred_subjectively_intro. by iFrame "oN".
- (* TODO: make a lemma *)
iIntros (t l'). rewrite lookup_fmap_Some'.
iIntros ((_ & ([] & Eq' & (? & on & Eq & Eq2)%toHeadHist_lookup_Some) & _)).
simpl in Eq'. subst v.
assert (on = Some l') as ->.
{ clear -Eq. destruct on; by inversion Eq. } clear Eq.
apply elem_of_list_lookup_2 in Eq2.
rewrite (all_slocs_node_next_access _ _ _ Eq2).
iDestruct "As" as "[As En]". iDestruct "En" as (q' on) "En".
rewrite view_at_view_at shift_0 own_loc_na_own_loc_prim.
iDestruct (view_at_subjectively with "En") as (C) "En".
iExists q', C. iFrame "En". }
{ simpl. iIntros "{# $HRE %} !> [oN As] !>". iSplitL "oN".
- by rewrite shift_0 own_loc_na_own_loc_prim_subjectively.
- iIntros (?? (_ & ? & _)). by iApply (all_slocs_node_access_prim with "As"). }
iIntros (b t' v' V2 V2' ζh2'' ζh2) "(F & #sV2' & #sH2 & H & [oN As] & CASE)".
iDestruct "F" as %([Subζh0'' Subζh2''] & Eqt' & MAXt' & LeV1). clear Pr.
......@@ -1973,7 +1975,7 @@ Proof.
have SP' : StackProps G' T2 S2'.
{ constructor.
- etrans; last apply SP2SB. clear. simpl. set_solver.
- etrans; last apply SP2SB. simpl. set_solver-.
- intros e. rewrite SP2ET. case (decide (e = ppId)) => [->|?].
+ rewrite lookup_app_1_eq (lookup_ge_None_2 E2); [clear; naive_solver|done].
+ by rewrite lookup_app_1_ne.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment