From e8de09e255de1a2612a01ad2f076f9a3ad58a5bd Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Thu, 26 Nov 2020 21:22:54 +0100
Subject: [PATCH] bump dependency
---
coq-lambda-rust.opam | 2 +-
theories/lang/arc.v | 87 +++++++++++++++++++++-----------------------
2 files changed, 43 insertions(+), 46 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6b749ba8..79b06f61 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.2020-11-17.0.921e8532") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2020-11-26.1.04496bec") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc.v b/theories/lang/arc.v
index d6074309..4cdbd4c3 100644
--- a/theories/lang/arc.v
+++ b/theories/lang/arc.v
@@ -361,16 +361,13 @@ Section arc.
(monPred_in Vb →
▷ GPS_INV (weak_interp P2 l γi γs γsw) (l >> 1) (weak_noCAS γsw) γw).
Proof.
- rewrite 4!bi.later_sep monPred_in_sep 3!monPred_in_sep.
+ rewrite -!view_join_unfold !view_join_later.
iDestruct 1 as "((SMA & SDA & WUA) & $ & $)".
- rewrite 3!bi.later_exist 3!monPred_in_exist.
- iDestruct "SMA" as (Mt) "SMA". iDestruct "SDA" as (Dt) "SDA".
- iDestruct "WUA" as (Ut) "WUA".
- iMod (monPred_in_later_timeless with "SMA") as "SMA".
- iMod (monPred_in_later_timeless with "SDA") as "SDA".
- iMod (monPred_in_later_timeless with "WUA") as "WUA".
- iIntros "!>". iSplitL "SMA"; last iSplitL "SDA"; iExists _;
- by iApply monPred_in_embed.
+ iDestruct "SMA" as (Mt) ">SMA". iDestruct "SDA" as (Dt) ">SDA".
+ iDestruct "WUA" as (Ut) ">WUA".
+ iIntros "!>".
+ iSplitL "SMA"; last iSplitL "SDA"; iExists _;
+ rewrite view_join_embed; iFrame.
Qed.
Lemma arc_inv_join Vb γi γs γw γsw l :
@@ -404,17 +401,17 @@ Section arc.
Proof.
iIntros "HP Hacc". iMod ("Hacc" with "HP") as (Vb q) "[Hown Hclose2]".
iExists Vb, q. iMod (monPred_in_later_timeless with "Hown") as "Hown".
- rewrite monPred_in_exist. iDestruct "Hown" as (v) "Hown".
- rewrite monPred_in_exist. iDestruct "Hown" as (Mt) "Hown".
- rewrite monPred_in_exist. iDestruct "Hown" as (Dt) "Hown".
- rewrite 7!monPred_in_sep.
+ rewrite monPred_in_exist'. iDestruct "Hown" as (v) "Hown".
+ rewrite monPred_in_exist'. iDestruct "Hown" as (Mt) "Hown".
+ rewrite monPred_in_exist'. iDestruct "Hown" as (Dt) "Hown".
+ rewrite 7!monPred_in_sep'.
iDestruct "Hown" as "(St & tok & SR & SM & SeenM & SD & SeenD & oW)".
iExists Mt, Dt. iFrame "tok". iSplitR "Hclose2 SeenM SeenD".
- - iSplitL "St". { by rewrite monPred_in_embed /StrongTok. }
+ - iSplitL "St". { by rewrite monPred_in_embed' /StrongTok. }
iSplitL "SR". { by iExists _. } iSplitL "SM".
- { by rewrite monPred_in_embed /StrMoves. } iSplitL "SD".
- { by rewrite monPred_in_embed /StrDowns. }
- by rewrite monPred_in_embed.
+ { by rewrite monPred_in_embed' /StrMoves. } iSplitL "SD".
+ { by rewrite monPred_in_embed' /StrDowns. }
+ by rewrite monPred_in_embed'.
- iIntros "!>" (Mt' Dt') "St tok SR SM SeenM' SD SeenD' oW".
iMod ("Hclose2" with "[-]") as "$"; [|done]. iIntros "#mb !>".
iSpecialize ("tok" with "mb").
@@ -504,12 +501,12 @@ Section arc.
Proof.
iIntros "HP Hacc". iMod ("Hacc" with "HP") as (Vb q) "[Hown Hclose2]".
iExists Vb, q. iMod (monPred_in_later_timeless with "Hown") as "Hown".
- rewrite monPred_in_exist. iDestruct "Hown" as (v) "Hown".
- rewrite monPred_in_exist. iDestruct "Hown" as (Ut) "Hown". iExists Ut.
- rewrite 4!monPred_in_sep. iDestruct "Hown" as "(Wt & $ & WR & WU & SeenU)".
+ rewrite monPred_in_exist'. iDestruct "Hown" as (v) "Hown".
+ rewrite monPred_in_exist'. iDestruct "Hown" as (Ut) "Hown". iExists Ut.
+ rewrite 4!monPred_in_sep'. iDestruct "Hown" as "(Wt & $ & WR & WU & SeenU)".
iSplitR "Hclose2 SeenU".
- - iSplitL "Wt". { by rewrite monPred_in_embed /WeakTok. }
- iSplitL "WR". { by iExists _. } by rewrite monPred_in_embed /WkUps.
+ - iSplitL "Wt". { by rewrite monPred_in_embed' /WeakTok. }
+ iSplitL "WR". { by iExists _. } by rewrite monPred_in_embed' /WkUps.
- iIntros "!>" (Ut') "Wt tok WR WU SeenU'".
iMod ("Hclose2" with "[-]") as "$"; [|done]. iIntros "#mb !>".
iDestruct "WR" as (v') "WR". iSpecialize ("WR" with "mb").
@@ -715,7 +712,7 @@ Section arc.
iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _ q
with "RR [SR]") as "[SR1 SR2]".
{ rewrite monPred_subjectively_unfold.
- iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+ iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
set R : time → unitProtocol → val → vProp :=
(λ t' _ v', (∃ z : Z, ⌜v' = #z ∧ 0 < z⌝) ∗
StrongTok γsw q ∗ StrongMoveAuth γsw Mt )%I.
@@ -830,7 +827,7 @@ Section arc.
iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _ q
with "RR [SR]") as "[SR1 SR2]".
{ rewrite monPred_subjectively_unfold.
- iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+ iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
set R : time → unitProtocol → val → vProp := (λ t' _ v', ∃ z : Z, ⌜v' = #z⌝)%I.
(* actual read *)
iApply (GPS_SWRaw_SharedReader_Read (strong_interp P1 (l >> 1) γi γw γsw) _
@@ -869,7 +866,7 @@ Section arc.
iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _ q
with "RR [SR]") as "[SR1 SR2]".
{ rewrite monPred_subjectively_unfold.
- iDestruct (monPred_in_elim_vProp with "SR") as (V') "SR". by iExists V'. }
+ iDestruct (monPred_in_view_elim with "SR") as (V') "SR". by iExists V'. }
iDestruct "SMA" as (Mt') "SMA".
iDestruct (StrongMoveAuth_agree with "[$SMA $SM]") as %?. subst Mt'.
set Q: time → unitProtocol → vProp :=
@@ -1256,7 +1253,7 @@ Section arc.
iDestruct (GPS_SWSharedReader_Reader_join_subjectively _ _ _ _ _ _ q
with "WR [WRq]") as "[WR1 WR2]".
{ rewrite monPred_subjectively_unfold.
- iDestruct (monPred_in_elim_vProp with "WRq") as (V') "?". by iExists V'. }
+ iDestruct (monPred_in_view_elim with "WRq") as (V') "?". by iExists V'. }
set Q: time → unitProtocol → vProp :=
(λ t'' s'',
@@ -1754,14 +1751,14 @@ Section arc.
rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
iDestruct (acq_exist with "SDA") 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").
- rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "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").
+ rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
rewrite bi.later_exist; setoid_rewrite <- embed_later.
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "SMA" as (Mt) "SMA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SMA" as (Mt) "SMA".
iExists Mt. by iFrame "SMA".
- - rewrite -embed_exist monPred_in_embed. iExists _. iFrame "SDA".
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+ - rewrite -embed_exist monPred_in_embed'. iExists _. iFrame "SDA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
iExists Ut'. by iFrame "WUA". }
iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
wp_case. by iApply ("HΦ"). }
@@ -1975,14 +1972,14 @@ Section arc.
rewrite acq_sep_elim. iDestruct "Q" as "[SDA _]".
iDestruct (acq_exist with "SDA") 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").
- rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "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").
+ rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
rewrite bi.later_exist; setoid_rewrite <- embed_later.
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "SMA" as (Mt') "SMA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SMA" as (Mt') "SMA".
iExists Mt'. by iFrame "SMA".
- - rewrite -embed_exist monPred_in_embed. iExists _. iFrame "SDA".
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+ - rewrite -embed_exist monPred_in_embed'. iExists _. iFrame "SDA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
iExists Ut'. by iFrame "WUA". }
iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
@@ -2200,14 +2197,14 @@ Section arc.
rewrite acq_sep_elim. iDestruct "Q" as "[SMA _]".
iDestruct (acq_exist with "SMA") 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").
- rewrite 2!bi.later_sep 2!monPred_in_sep. iSplitL "SMA"; last iSplitL "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").
+ rewrite 2!bi.later_sep 2!monPred_in_sep'. iSplitL "SMA"; last iSplitL "SDA";
rewrite bi.later_exist; setoid_rewrite <- embed_later.
- - rewrite -embed_exist monPred_in_embed. iExists Mt1. by iFrame "SMA".
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "SDA" as (?) "SDA".
+ - rewrite -embed_exist monPred_in_embed'. iExists Mt1. by iFrame "SMA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "SDA" as (?) "SDA".
iExists _. iFrame "SDA".
- - rewrite -2!embed_exist monPred_in_embed. iDestruct "WUA" as (Ut') "WUA".
+ - rewrite -2!embed_exist monPred_in_embed'. iDestruct "WUA" as (Ut') "WUA".
iExists Ut'. by iFrame "WUA". }
iModIntro. wp_case. wp_op. rewrite (bool_decide_false _ Eq).
wp_case. by iApply ("HΦ"). }
@@ -2548,7 +2545,7 @@ Section arc.
iMod (GPS_SWWriter_dealloc (weak_interp P2 l γi γs γsw) _ _ true
with "HINV IW WW") as "[wk _]"; [done|].
wp_let. wp_op. wp_let. wp_op. wp_bind (_ <-ʳᵉˡ _)%E.
- iApply (wp_write_rel _ #(1) with "[wk]");
+ iApply (wp_write _ #(1) with "[wk]");
[done|by iApply own_loc_na_own_loc|..].
iIntros "!> wk". wp_let. iApply "HΦ". by iFrame "str wk HP".
--
GitLab