diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 29ca524bb16ba08e7cb045294bf101960c5810ce..171c5c3a05da8e073915003dda7321e97e209804 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
"""
depends: [
- "coq-gpfsl" { (= "dev.2021-10-01.1.8da490e3") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2021-10-03.0.63d7ad95") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index af6184c4f1d4ff425a9e83e08a2987d07311e825..b86777e524bab87cb30f230557356d29a89e590c 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -837,8 +837,8 @@ Section arc.
iDestruct "Eq1" as %?. subst v'. by iExists _.
- iDestruct 1 as (st) "[Eq1 SI]". iDestruct "Eq1" as %?. subst v'.
iModIntro. iSplitR ""; [iExists _; by iFrame "SI"|by iExists _]. }
- iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & SR1 & IS & Rs)". rewrite acq_exist.
- iDestruct "Rs" as (z) "Rs". iDestruct (acq_pure_elim with "Rs") as %?. subst v'.
+ iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & SR1 & IS & Rs)".
+ iDestruct "Rs" as (z) "%". subst v'.
iDestruct (GPS_SWSharedReaders_join with "SR2 SR1") as "SR". rewrite Qp_div_2.
(* closing invariant *)
@@ -849,7 +849,7 @@ Section arc.
iMod ("Hclose2" with "St tok [SR] SM SD oW") as "HP"; [by iExists _|].
iModIntro. iMod "Hclose1" as "_".
- iModIntro. wp_let. wp_op. iClear "Rs". clear Vs R v0 Mt Dt t' Vb q.
+ iModIntro. wp_let. wp_op. clear Vs R v0 Mt Dt t' Vb q.
(* now we can CAS *)
wp_bind (CAS _ _ _ _ _ _).
(* not really, just preparing *)
@@ -957,31 +957,29 @@ Section arc.
(* finally done with the CAS *)
iIntros "!>" (b t' [] v') "(IS &%& [([%[%%]]&R'&Q) | ([%[_ %]] &R'&Rs&_)])".
- subst b v'.
- (* tedious removal of acq_mod *)
- rewrite 3!acq_sep_elim 3!acq_embed_elim acq_exist.
iDestruct "Q" as "(St & SMA & SM & Q)". iDestruct "Q" as (q'') "Q".
- rewrite 7!acq_sep_elim 4!acq_embed_elim acq_pure_elim.
- iDestruct "Q" as "(St'' & HP1 & tok'' & R'' & SM'' & #MAX'' & oW'' & SD'')".
+ iDestruct "Q" as "(St'' & HP1 & tok'' & R'' & SM'' & %MAX'' & oW'' & SD'')".
iDestruct (GPS_SWSharedReaders_join_subjectively _ _ _ _ _ _ _ _ q''
with "R' [R'']") as "[R' R'']". { by iApply acq_subjective. }
- (* done with acq_mod *)
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR'".
set Mt' := if decide (Z.to_pos z = 1%positive) then Mt ∪ {[t']} else Mt.
- iAssert (SeenActs γs l Mt')%I with "[MAX'']" as "#SeenM'".
- { iExists _, _. iFrame "RR' MAX''". }
+ iAssert (SeenActs γs l Mt')%I with "[]" as "#SeenM'".
+ { iExists _, _. iFrame (MAX'') "RR'". }
iDestruct (GPS_SWSharedReaders_join with "SR2 R'") as "SR".
+ (* tedious removal of acq_mod *)
rewrite Qp_div_2 2!acq_objectively_elim 2!monPred_objectively_elim.
+ rewrite 7!acq_embed_elim.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA MDU IW IS]").
- { iDestruct "MDU" as "[SDA WUA]".
+ { iClear "#". iDestruct "MDU" as "[SDA WUA]".
iApply (arc_inv_join with "[SMA] SDA WUA IS IW"). by iExists _. }
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" $! (if decide (Z.to_pos z = 1%positive) then {[t']} else ∅) ∅
with "[St] tok [SR] [SM] [] [SD] [] oW") as "HP";
- [by rewrite /StrongTok|by iExists _|..|by rewrite right_id_L|done|].
- { rewrite /Mt'. case decide; rewrite /StrMoves; [done|by rewrite right_id_L]. }
+ [by iExact "St"|by iExists _|..|by rewrite right_id_L|done|].
+ { rewrite /Mt'. case decide => _; [done|by rewrite right_id_L]. }
{ case (decide (Z.to_pos _ = _)) => ?; [|done].
rewrite decide_False; [|by apply non_empty_singleton_L].
iExists _,_. iFrame "RR'". iPureIntro. move => ? /elem_of_singleton -> //. }
@@ -991,8 +989,8 @@ Section arc.
iExists _,_,∅. rewrite /StrongTok. iFrame "St'' tok'' R''".
rewrite /StrMoves /StrDowns. iFrame "SM'' SeenM' oW'' SD''".
iDestruct "WR" as (??) "WR". iExists _, _. by iFrame "WR".
- - subst b. rewrite 2!acq_sep_elim 3!acq_embed_elim.
- iDestruct "Rs" as "(St & SMA & SM)".
+ - subst b.
+ iDestruct "Rs" as "(St & SMA & SM)". rewrite 3!acq_embed_elim.
iDestruct (GPS_SWSharedReaders_join with "SR2 R'") as "SR". rewrite Qp_div_2.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA MDU IW IS]").
@@ -1001,7 +999,7 @@ Section arc.
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" $! ∅ ∅ with "[St] tok [SR] [SM] [] [SD] [] oW") as "HP";
- [by rewrite /StrongTok|by iExists _| |done|by rewrite right_id_L|done|].
+ [by iExact "St"|by iExists _| |done|by rewrite right_id_L|done|].
{ by rewrite right_id_L /StrMoves. }
iModIntro. iMod "Hclose1" as "_". iModIntro.
wp_case. iApply ("IH" with "HP HΦ").
@@ -1060,8 +1058,7 @@ Section arc.
- iIntros "[% F]". subst v'. iModIntro. iFrame "F". iSplitL""; [done|].
iPureIntro. by eexists. }
iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & _ & IW & Rs)".
- iDestruct (acq_exist with "Rs") as (z) "Rs".
- iDestruct (acq_pure_elim with "Rs") as %[? Le1]. subst v'.
+ iDestruct "Rs" as (z) "[% %Le1]". subst v'.
(* closing invariant *)
iSpecialize ("Hclose1" with "tok [MA IW IS]").
@@ -1070,7 +1067,7 @@ Section arc.
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" with "St tok SR SM SD oW") as "HP".
iModIntro. iMod "Hclose1" as "_".
- iClear "Rs". clear R t' Mt Dt Vb q Vs.
+ clear R t' Mt Dt Vb q Vs.
iModIntro. wp_let. wp_op.
case (decide (z = -1)) => Eq; [subst z|rewrite (bool_decide_false _ Eq)];
@@ -1184,8 +1181,8 @@ Section arc.
iModIntro. iMod "Hclose1" as "_". iModIntro.
wp_case. iApply ("HΦ" with "[- $HP]").
iExists _, ∅. iFrame "Wt' WRs".
- - subst b. rewrite 2!acq_sep_elim 3!acq_embed_elim.
- iDestruct "Rs" as "(SDA & SD & oW)".
+ - subst b.
+ iDestruct "Rs" as "(SDA & SD & oW)". rewrite 3!acq_embed_elim.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"). by iExists _. }
@@ -1227,8 +1224,7 @@ Section arc.
- iIntros "[% F]". subst v'. iModIntro. iFrame "F". iSplitL""; [done|].
iPureIntro. by eexists. }
iIntros "!>" (t' [] v'). iDestruct 1 as "(_ & _ & IW & Rs)".
- iDestruct (acq_exist with "Rs") as (z) "Rs".
- iDestruct (acq_pure_elim with "Rs") as %?. subst v'.
+ iDestruct "Rs" as (z) "%". subst v'.
(* closing *)
iSpecialize ("Hclose1" with "tok [MA IW IS]").
@@ -1237,7 +1233,7 @@ Section arc.
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" with "Wt tok WRq WU") as "HP".
iModIntro. iMod "Hclose1" as "_". iModIntro.
- wp_let. wp_op. iClear "Rs". clear R Ut t' Vb Vs q.
+ wp_let. wp_op. clear R Ut t' Vb Vs q.
(* now we can CAS *)
wp_op. wp_bind (CAS _ _ _ _ _ _).
@@ -1347,15 +1343,12 @@ Section arc.
(* finally done with the CAS *)
iIntros "!>" (b t' [] v') "(IW &%& [([%[%%]]&R'&Q) | ([%[_ %]] &R'&Rs&_)])".
- subst b v'.
- (* tedious removal of acq_mod *)
- rewrite 2!acq_sep_elim 2!acq_embed_elim acq_exist.
iDestruct "Q" as "(SDA & Wt & Q)". iDestruct "Q" as (q'') "Q".
- rewrite 3!acq_sep_elim 2!acq_embed_elim
- acq_objectively_elim monPred_objectively_elim.
iDestruct "Q" as "(Wt'' & tok'' & R'' & WU'')".
+ (* tedious removal of acq_mod *)
+ rewrite 4!acq_embed_elim acq_objectively_elim monPred_objectively_elim.
iDestruct (GPS_SWSharedReaders_join_subjectively _ _ _ _ _ _ _ _ q''
with "R' [R'']") as "[R' R'']". { by iApply acq_subjective. }
- (* done with acq_mod *)
iDestruct (GPS_SWSharedReader_Reader with "R'") as "#RR".
iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq". rewrite Qp_div_2.
@@ -1364,22 +1357,23 @@ Section arc.
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"). by iExists _. }
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" with "[Wt] tok [WRq] WU") as "HP";
- [by rewrite /WeakTok|by iExists _|].
+ [by iExact "Wt"|by iExists _|].
iModIntro. iMod "Hclose1" as "_". iModIntro.
wp_case. iApply ("HΦ" with "[- $HP]"). iExists _, ∅.
rewrite /WeakTok. iFrame "Wt'' tok'' R''". rewrite /WkUps.
iFrame "WU''". iDestruct "SR" as (??) "SR". iExists _, _. by iFrame "SR".
- - subst b. rewrite acq_sep_elim 2!acq_embed_elim.
- iDestruct "Rs" as "(Wt & SDA)".
- iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq". rewrite Qp_div_2.
+ - subst b.
+ iDestruct "Rs" as "(Wt & SDA)". rewrite 2!acq_embed_elim.
+ iDestruct (GPS_SWSharedReaders_join with "WR2 R'") as "WRq".
+ rewrite Qp_div_2.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"). by iExists _. }
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" with "[Wt] tok [WRq] WU") as "HP";
- [by rewrite /WeakTok|by iExists _|].
+ [by iExact "Wt"|by iExists _|].
iModIntro. iMod "Hclose1" as "_". iModIntro.
wp_case. iApply ("IH" with "HP HΦ").
Qed.
@@ -1413,8 +1407,8 @@ Section arc.
- iDestruct 1 as (st) "[Eq1 SI]". iDestruct "Eq1" as %?. subst v'.
iModIntro. iSplitR ""; [iExists _; by iFrame "SI"|by iExists _].
- iIntros "% !>". subst v'. iSplit; [done|]. by iExists _. }
- iIntros "!>" (t' [] v'). iDestruct 1 as "(_ &_& IS & Rs)". rewrite acq_exist.
- iDestruct "Rs" as (z) "Rs". iDestruct (acq_pure_elim with "Rs") as %?. subst v'.
+ iIntros "!>" (t' [] v'). iDestruct 1 as "(_ &_& IS & Rs)".
+ iDestruct "Rs" as (z) "%". subst v'.
(* closing *)
iSpecialize ("Hclose1" with "tok [MA IW IS]").
@@ -1423,7 +1417,7 @@ Section arc.
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
iMod ("Hclose2" with "Wt tok WRq WU") as "HP".
iModIntro. iMod "Hclose1" as "_". iModIntro.
- wp_let. wp_op. iClear "Rs". clear R Ut t' Vb Vs q.
+ wp_let. wp_op. clear R Ut t' Vb Vs q.
case (decide (z = 0)) => NEq0; [subst z|rewrite (bool_decide_false _ NEq0)];
wp_if; first by iApply ("HΦ" $! _ 1%Qp with "[$HP]").
@@ -1506,16 +1500,12 @@ Section arc.
(* finally done with the CAS *)
iIntros "!>" (b t' [] v') "(IS &%& [([%[%%]]&#R'&Q) | ([%[_ %]] &R'&Rs&_)])".
- subst b v'.
+ iDestruct "Q" as "(WUA & WU & Q)".
+ iDestruct "Q" as (q'' Mt'') "(St'' & HP1 & tok'' & R'' & SM'' & %MAX'' & SD'' & oW'')".
(* tedious removal of acq_mod *)
- rewrite 2!acq_sep_elim 2!acq_embed_elim. iDestruct "Q" as "(WUA & WU & Q)".
- iDestruct (acq_exist with "Q") as (q'') "Q".
- iDestruct (acq_exist with "Q") as (Mt'') "Q".
- rewrite 7!acq_sep_elim 4!acq_embed_elim acq_pure_elim 2!acq_objectively_elim.
- iDestruct "Q" as "(St'' & HP1 & tok'' & R'' & SM'' & MAX'' & SD'' & oW'')".
- iDestruct "MAX''" as %MAX''.
+ rewrite 6!acq_embed_elim 2!acq_objectively_elim.
iDestruct (GPS_SWSharedReader_Reader_join_subjectively with "R' [R'']") as "R''".
{ by iApply acq_subjective. }
- (* done with acq_mod *)
set Ut' := if decide (Z.to_pos z = 1%positive) then {[t']} else ∅.
iAssert (SeenActs γs l Ut')%I with "[]" as "#SeenU'".
{ iExists _, _. iFrame "R'". iPureIntro. rewrite /Ut'. case decide; [|done].
@@ -1526,7 +1516,7 @@ Section arc.
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
{ iApply (arc_inv_join with "SMA SDA [WUA] IS IW"). by iExists _. }
iMod (fupd_mask_mono with "Hclose1") as "[tok Hclose1]"; [set_solver|].
- iMod ("Hclose2" with "Wt tok WRq [WU] []") as "HP"; [by rewrite /WkUps|..].
+ iMod ("Hclose2" with "Wt tok WRq [WU] []") as "HP"; [by iExact "WU"|..].
{ rewrite /Ut'. case decide; [|done].
rewrite decide_False; [done|by apply non_empty_singleton_L]. }
iModIntro. iMod "Hclose1" as "_". iModIntro.
@@ -1537,8 +1527,8 @@ Section arc.
rewrite /StrMoves /StrDowns. iFrame "SM'' oW'' SD''".
iDestruct "WRR" as (??) "WRR".
iSplitL""; iExists _,_; [by iFrame (MAX'') "R'"|by iFrame "WRR"].
- - subst b. rewrite acq_sep_elim 2!acq_embed_elim.
- iDestruct "Rs" as "[WUA WU]".
+ - subst b.
+ iDestruct "Rs" as "[WUA WU]". rewrite 2!acq_embed_elim.
(* closing *)
iSpecialize ("Hclose1" with "tok [SMA SDA WUA IW IS]").
@@ -1574,11 +1564,10 @@ Section arc.
- iDestruct 1 as (st) "[Eq1 WI]". iDestruct "Eq1" as %?. subst v'.
iModIntro. iSplitR "". { iExists _. by iFrame "WI". } by iExists _. }
iIntros "!>" (t' [] v'). iDestruct 1 as ([_ Ext']) "(WR & IW & Rs)".
- iDestruct (acq_exist with "Rs") as (z) "Rs".
- iDestruct (acq_pure_elim with "Rs") as %?. subst v'.
+ iDestruct "Rs" as (z) "%". subst v'.
iMod ("Hclose1" with "tok [MA IW IS]") as "tok".
{ iDestruct "MA" as "(SMA & SDA & WUA)".
- by iApply (arc_inv_join with "SMA SDA WUA IS IW"). } iClear "Rs".
+ by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
clear Vb R. iModIntro. wp_let. wp_op. wp_op.
wp_bind (CAS _ _ _ _ _ _).
@@ -1747,9 +1736,7 @@ Section arc.
{ iIntros "tok". iMod ("VS" with "[$Wt $WU SDA tok]") as "[IW Q]".
{ rewrite decide_False; last done. iFrame "tok".
iDestruct "SDA" as (Dt) "SDA". by iExists Dt. }
- iDestruct "Q" as ([]) "(_&_&Q)".
- rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
- iDestruct (acq_exist with "SDA") as (Dt) "SDA".
+ iDestruct "Q" as ([]) "(_&_&[[%Dt SDA] _])".
iDestruct (acq_embed_elim with "SDA") as "SDA".
iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
@@ -1764,10 +1751,7 @@ Section arc.
wp_case. by iApply ("HΦ"). }
iMod ("VS" with "P") as "(IW & QI)".
- iDestruct "QI" as ([]) "(_&_&Q)".
- (* tedious removal of acq_mod *)
- rewrite acq_sep_elim. iDestruct "Q" as "[SDA Q]".
- iDestruct (acq_exist with "SDA") as (Dt') "SDA".
+ iDestruct "QI" as ([]) "(_&_&[[%Dt' SDA] Q])".
iDestruct (acq_embed_elim with "SDA") as "SDA".
rewrite bi.and_elim_l.
iMod ("Hclose1" with "tokn [SMA SDA WUA IW IS]") as "tok".
@@ -1839,11 +1823,10 @@ Section arc.
- iIntros "[% F]". subst v'. iModIntro. iFrame "F". iSplitL""; [done|].
iPureIntro. by eexists. }
iIntros "!>" (t' [] v'). iDestruct 1 as (_) "(_ & IW & Rs)".
- iDestruct (acq_exist with "Rs") as (z) "Rs".
- iDestruct (acq_pure_elim with "Rs") as %[? Le1]. subst v'.
+ iDestruct "Rs" as (z) "[% %Le1]". subst v'.
iMod ("Hclose1" with "tok [MA IW IS]") as "tok".
{ iDestruct "MA" as "(SMA & SDA & WUA)".
- by iApply (arc_inv_join with "SMA SDA WUA IS IW"). } iClear "Rs".
+ by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
clear Vb R. iModIntro. wp_let. wp_op. wp_op.
wp_bind (CAS _ _ _ _ _ _).
@@ -1968,9 +1951,7 @@ Section arc.
{ iIntros "tok".
iMod ("VS" with "[$HP2 $SW $SM $SD $oW $SDA tok]") as "[IW Q]".
{ rewrite decide_False; last done. iFrame "tok". }
- iDestruct "Q" as ([]) "(_&_&Q)".
- rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
- iDestruct (acq_exist with "SDA") as (Dt') "SDA".
+ iDestruct "Q" as ([]) "(_&_&[[%Dt' SDA] _])".
iDestruct (acq_embed_elim with "SDA") as "SDA".
iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
@@ -1986,10 +1967,7 @@ Section arc.
wp_case. by iApply ("HΦ"). }
iMod ("VS" with "P") as "(IW & QI)".
- iDestruct "QI" as ([]) "(_&_&Q)".
- (* tedious removal of acq_mod *)
- rewrite acq_sep_elim. iDestruct "Q" as "(SDA & Q)".
- iDestruct (acq_exist with "SDA") as (Dt') "SDA".
+ iDestruct "QI" as ([]) "(_&_&[[%Dt' SDA] Q])".
iDestruct (acq_embed_elim with "SDA") as "SDA".
rewrite bi.and_elim_l.
iMod ("Hclose1" with "tokn [SMA SDA WUA IW IS]") as "tok".
@@ -2053,11 +2031,10 @@ Section arc.
- iDestruct 1 as (st) "[Eq1 SI]". iDestruct "Eq1" as %?. subst v'.
iModIntro. iSplitR "". { iExists _. by iFrame "SI". } by iExists _. }
iIntros "!>" (t' [] v'). iDestruct 1 as ([_ Ext']) "(SR & IS & Rs)".
- iDestruct (acq_exist with "Rs") as (z) "Rs".
- iDestruct (acq_pure_elim with "Rs") as %?. subst v'.
+ iDestruct "Rs" as (z) "%". subst v'.
iMod ("Hclose1" with "tok [MA IW IS]") as "tok".
{ iDestruct "MA" as "(SMA & SDA & WUA)".
- by iApply (arc_inv_join with "SMA SDA WUA IS IW"). } iClear "Rs".
+ by iApply (arc_inv_join with "SMA SDA WUA IS IW"). }
clear Vb R. iModIntro. wp_let. wp_op.
wp_bind (CAS _ _ _ _ _ _).
(* preparing to CAS *)
@@ -2193,9 +2170,7 @@ Section arc.
iMod ("VS" with "[$HP1 $St $SM $SD $oW SMA tok]") as "[IS Q]".
{ rewrite decide_False; last done. iFrame "tok".
iDestruct "SMA" as (Mt1) "SMA". by iExists Mt1. }
- iDestruct "Q" as ([]) "(_&_&Q)".
- rewrite acq_sep_elim. iDestruct "Q" as "[SMA _]".
- iDestruct (acq_exist with "SMA") as (Mt1) "SMA".
+ iDestruct "Q" as ([]) "(_&_&[[%Mt1 SMA] _])".
iDestruct (acq_embed_elim with "SMA") as "SMA".
iIntros "!>". iSplitR ""; last done. rewrite bi.later_sep monPred_in_sep'.
iSplitR "IS IW"; last (rewrite bi.later_sep monPred_in_sep'; iFrame "IS IW").
@@ -2210,12 +2185,7 @@ Section arc.
wp_case. by iApply ("HΦ"). }
iMod ("VS" with "P") as "(IS & QI)".
- iDestruct "QI" as ([]) "(_&_&Q)".
-
-
- (* tedious removal of acq_mod *)
- rewrite acq_sep_elim. iDestruct "Q" as "[SMA Q]".
- iDestruct (acq_exist with "SMA") as (Mt') "SMA".
+ iDestruct "QI" as ([]) "(_&_&[[%Mt' SMA] Q])".
iDestruct (acq_embed_elim with "SMA") as "SMA".
rewrite bi.and_elim_l.
iMod ("Hclose1" with "tokn [SMA SDA WUA IW IS]") as "tok".
@@ -2338,7 +2308,7 @@ Section arc.
iIntros "!>" (b t2 [] v2) "(IS &%& [([%[%%]]&_&Q) | ([%[_ %]] &R'&Rs&P)])";
last first.
{ (* CAS fails*)
- subst b. iDestruct (acq_exist with "Rs") as (Mt') "SMA".
+ subst b. iDestruct "Rs" as (Mt') "SMA".
iDestruct (acq_embed_elim with "SMA") as "SMA".
iDestruct "P" as "(HP1 & St & SM & SD & oW)".
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
@@ -2347,9 +2317,7 @@ Section arc.
iExists _,_,_,_. by iFrame "St tok R' SM SeenM SD SeenD oW". }
clear P Q1 Q2 R. subst b v2.
- (* tedious removal of acq_mod *)
- rewrite acq_sep_elim. iDestruct "Q" as "[SMA Q]".
- iDestruct (acq_exist with "SMA") as (Mt') "SMA".
+ iDestruct "Q" as "[[%Mt' SMA] Q]".
iDestruct (acq_embed_elim with "SMA") as "SMA".
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
{ iApply (arc_inv_join with "[SMA] SDA WUA IS IW"). by iExists _. }
@@ -2448,8 +2416,9 @@ Section arc.
iIntros "!>" (b t' [] v') "(IW &_& [([%[%%]]&_&Q) | ([%[_ %]] &R'&Rs&_)])";
last first.
{ (* CAS fail first *)
- subst b. rewrite 2!acq_sep_elim /StrDowns 3!acq_embed_elim.
- iDestruct "Rs" as "(SDA & SD & oW)". clear Q Q1 Q2 R.
+ subst b.
+ iDestruct "Rs" as "(SDA & SD & oW)". rewrite 3!acq_embed_elim.
+ clear Q Q1 Q2 R.
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"). by iExists _. }
iModIntro. wp_case. iApply "HΦ". iFrame "HP1". iExists _,_,_,_.
@@ -2457,8 +2426,7 @@ Section arc.
iExists _,_. iFrame (MAX) "WR". }
(* CAS success, we have all weak pointers! *)
- subst b v'. iDestruct "Q" as "(SDA & SD & MAX & oW & WL & WW & WS)".
- iDestruct "MAX" as %MAX1.
+ subst b v'. iDestruct "Q" as "(SDA & SD & %MAX1 & oW & WL & WW & WS)".
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
{ iApply (arc_inv_join with "SMA [SDA] WUA IS IW"). by iExists _. }
@@ -2687,8 +2655,8 @@ Section arc.
iIntros "!>" (b t' [] v') "(IS &_& [([% [% _]]&R'&Q) | ([% _] &R'&Rs&_)])";
last first.
{ (* CAS failure case first *)
- subst b. rewrite 2!acq_sep_elim 3!acq_embed_elim.
- iDestruct "Rs" as "(St & SMA & SM)".
+ subst b.
+ iDestruct "Rs" as "(St & SMA & SM)". rewrite 3!acq_embed_elim.
iMod ("Hclose1" with "tok [SMA SDA WUA IW IS]") as "tok".
{ iApply (arc_inv_join with "[SMA] SDA WUA IS IW"). by iExists _. }
iModIntro. wp_case. iApply ("HΦ" $! 2%fin). simpl. iFrame "HP1".
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index a8fb584f541a267c39a003c1c81eb6a8e52b7ad2..5c4f50cd5a3e6121c75f39d8be9126e111802704 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -350,11 +350,7 @@ Section rwlock_inv.
Lemma rwlock_interp_read_acq l t s v γ γs α tyO tyS tid:
(▽{tid} rwlock_interp γs α tyO tyS false l γ t s v : vProp) -∗
∃ st, ⌜v = #(Z_of_rwlock_st st)âŒ.
- Proof.
- iIntros "Int". iDestruct (acq_exist with "Int") as (?) "Int".
- iDestruct (acq_sep_elim with "Int") as "[Int _]".
- iDestruct (acq_pure_elim with "Int") as "?". iExists _. iFrame.
- Qed.
+ Proof. iDestruct 1 as (?) "[% _]". by iExists _. Qed.
Lemma rwlock_proto_change_tid_own l γ γs α tyS tyO tid_own1 tid_own2 tid_shr ty :
Send ty →
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 6134729ff4e4b4b7805e01ad5ff4a956747319c4..6931f4b6cbed8665333e23aec5d7030ebe8bb146 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -191,9 +191,7 @@ Section rwlock_functions.
- iDestruct 1 as (st Eqvs) "F".
iIntros "!>". iSplitR ""; iExists st; [by iFrame "F"|done].
- iIntros (Eqvs) "!>". iSplit; [done|]. by iExists (Some (inl ())). }
- iIntros "!>" (t' [] v') "(_ & #R' & Hβtok1 & Int)".
- iDestruct (acq_exist with "Int") as (st') "Int".
- iDestruct (acq_pure_elim with "Int") as %?. subst v'.
+ iIntros "!>" (t' [] v') "(_ & #R' & Hβtok1 & [%st' %])". subst v'.
wp_let. wp_op; case_bool_decide as Hm1; wp_if.
- iDestruct (monPred_objectively_elim with "Hβtok2") as "Hβtok2".
iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index b76a91d4482e148e523a3c275d8b66d2d67cb619..3df7e309e3fed3ed9ec32e081049bfddb8d7396f 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -89,9 +89,7 @@ Section rwlockreadguard_functions.
- iDestruct 1 as (st Eqvs) "F".
iIntros "!>". iSplitR ""; iExists st; [by iFrame "F"|done].
- iIntros (Eqvs) "!>". iSplit; [done|]. by iExists (Some (inl ())). }
- iIntros "!>" (t' [] v') "(_ & #R' & Hβ & Int)".
- iDestruct (acq_exist with "Int") as (st2) "Int".
- iDestruct (acq_pure_elim with "Int") as %?. subst v'. iClear "Int". clear tR vR.
+ iIntros "!>" (t' [] v') "(_ & #R' & Hβ & [%st2 %])". subst v'. clear tR vR.
wp_let. wp_op. wp_bind (CAS _ _ _ _ _ _).
set P : vProp Σ := (rwown γs (reading_st q ν) ∗ (q).[ν])%I.