From a64342ca89bc74b6bf4ec44559cd09ba59f88323 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2023 15:34:28 +0100
Subject: [PATCH] Bump Iris (beautify code for `iCombine .. gives`).
---
coq-iris-examples.opam | 2 +-
theories/concurrent_stacks/concurrent_stack2.v | 2 +-
theories/concurrent_stacks/concurrent_stack4.v | 4 ++--
theories/hocap/concurrent_runners.v | 10 +++++-----
theories/hocap/contrib_bag.v | 4 ++--
theories/hocap/lib/oneshot.v | 2 +-
theories/lecture_notes/ccounter.v | 4 ++--
theories/lecture_notes/coq_intro_example_2.v | 6 +++---
theories/lecture_notes/lock.v | 2 +-
theories/lecture_notes/lock_unary_spec.v | 4 ++--
theories/lecture_notes/modular_incr.v | 2 +-
theories/locks/array_based_queuing_lock/abql.v | 12 ++++++------
.../locks/freeable_lock/freeable_logatom_lock.v | 2 +-
.../locks/freeable_lock/freeable_spin_lock.v | 4 ++--
theories/logatom/conditional_increment/cinc.v | 12 ++++++------
.../logatom/counter_with_backup/counter_proof.v | 6 +++---
theories/logatom/elimination_stack/hocap_spec.v | 6 +++---
theories/logatom/elimination_stack/stack.v | 16 ++++++++--------
theories/logatom/herlihy_wing_queue/hwq.v | 14 +++++++-------
theories/logatom/rdcss/rdcss.v | 10 +++++-----
theories/logatom/snapshot/atomic_snapshot.v | 6 +++---
theories/logrel/F_mu_ref_conc/binary/logrel.v | 12 ++++++------
theories/logrel/F_mu_ref_conc/binary/rules.v | 8 ++++++++
theories/logrel/F_mu_ref_conc/binary/soundness.v | 2 +-
.../F_mu_ref_conc/unary/examples/symbol_nat.v | 2 +-
theories/proph/eager_coin.v | 2 +-
theories/proph/lazy_coin_one_shot.v | 2 +-
theories/proph/lazy_coin_one_shot_typed.v | 2 +-
28 files changed, 84 insertions(+), 76 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 32c9e12a..8ce1ebf6 100644
--- a/coq-iris-examples.opam
+++ b/coq-iris-examples.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
depends: [
- "coq-iris-heap-lang" { (= "dev.2023-02-16.2.bcedf1c7") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-03-09.0.f91e8eab") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/concurrent_stacks/concurrent_stack2.v b/theories/concurrent_stacks/concurrent_stack2.v
index 3e6d7fc3..9d83ac54 100644
--- a/theories/concurrent_stacks/concurrent_stack2.v
+++ b/theories/concurrent_stacks/concurrent_stack2.v
@@ -111,7 +111,7 @@ Section side_channel.
wp_pures.
by iApply "HΦ"; iRight.
- wp_cmpxchg_fail.
- iDestruct (own_valid_2 with "H Hγ") as %[].
+ iCombine "H Hγ" gives %[].
Qed.
(* A partial specification for take that will be useful later *)
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 0f1605d7..918989ec 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -136,9 +136,9 @@ Section proofs.
wp_pures.
iApply ("HΦ" with "[HQ]"); iRight; auto.
- wp_cmpxchg_fail.
- iDestruct (own_valid_2 with "H Hγ") as %[].
+ iCombine "H Hγ" gives %[].
- wp_cmpxchg_fail.
- iDestruct (own_valid_2 with "H Hγ") as %[].
+ iCombine "H Hγ" gives %[].
Qed.
Lemma take_works γ P Q Q' o Ψ :
diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index eb1428c3..e3c0f949 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -46,25 +46,25 @@ Lemma INIT_not_SET_RES `{saG Σ} γ q q' v :
INIT γ q -∗ SET_RES γ q' v -∗ False.
Proof.
iIntros "Hs Hp".
- iDestruct (own_valid_2 with "Hs Hp") as %[].
+ iCombine "Hs Hp" gives %[].
Qed.
Lemma INIT_not_FIN `{saG Σ} γ q v :
INIT γ q -∗ FIN γ v -∗ False.
Proof.
iIntros "Hs Hp".
- iDestruct (own_valid_2 with "Hs Hp") as %[].
+ iCombine "Hs Hp" gives %[].
Qed.
Lemma SET_RES_not_FIN `{saG Σ} γ q v v' :
SET_RES γ q v -∗ FIN γ v' -∗ False.
Proof.
iIntros "Hs Hp".
- iDestruct (own_valid_2 with "Hs Hp") as %[].
+ iCombine "Hs Hp" gives %[].
Qed.
Lemma SET_RES_agree `{saG Σ} (γ: gname) (q q': Qp) (v w: val) :
SET_RES γ q v -∗ SET_RES γ q' w -∗ ⌜v = w⌝.
Proof.
iIntros "Hs1 Hs2".
- iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+ iCombine "Hs1 Hs2" gives %Hfoo.
iPureIntro. rewrite -Cinr_op -Cinl_op -pair_op in Hfoo.
by destruct Hfoo as [_ ?%to_agree_op_inv_L].
Qed.
@@ -72,7 +72,7 @@ Lemma FIN_agree `{saG Σ} (γ: gname) (v w: val) :
FIN γ v -∗ FIN γ w -∗ ⌜v = w⌝.
Proof.
iIntros "Hs1 Hs2".
- iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+ iCombine "Hs1 Hs2" gives %Hfoo.
iPureIntro. rewrite -Cinr_op -Cinr_op in Hfoo.
by apply to_agree_op_inv_L.
Qed.
diff --git a/theories/hocap/contrib_bag.v b/theories/hocap/contrib_bag.v
index 5c442d58..56573c38 100644
--- a/theories/hocap/contrib_bag.v
+++ b/theories/hocap/contrib_bag.v
@@ -98,7 +98,7 @@ Section proof.
iMod (bag_contents_update b Y with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
rewrite /bagPart.
iAssert (⌜X = ({[+ y +]} ⊎ Y)⌝)%I with "[Hpart HPs]" as %->.
- { iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+ { iCombine "HPs Hpart" gives %Hfoo.
apply frac_auth_agree in Hfoo. by unfold_leibniz. }
iMod (own_update_2 with "HPs Hpart") as "Hown".
{ apply (frac_auth_update _ _ _ (({[+ y +]} ⊎ Y) ∖ {[+ y +]}) (({[+ y +]} ⊎ Y) ∖ {[+ y +]})).
@@ -117,7 +117,7 @@ Section proof.
iDestruct (bag_contents_agree with "Hb1 Hb2") as %<-.
iAssert (⌜X = ∅⌝)%I with "[Hpart HPs]" as %->.
{ rewrite /bagPart.
- iDestruct (own_valid_2 with "HPs Hpart") as %Hfoo.
+ iCombine "HPs Hpart" gives %Hfoo.
apply frac_auth_agree in Hfoo. by unfold_leibniz. }
iMod ("Hcl" with "[Hb2 HPs]") as "_".
{ iNext. iExists _; iFrame. }
diff --git a/theories/hocap/lib/oneshot.v b/theories/hocap/lib/oneshot.v
index 070e2c63..2527c932 100644
--- a/theories/hocap/lib/oneshot.v
+++ b/theories/hocap/lib/oneshot.v
@@ -32,7 +32,7 @@ Lemma shot_agree `{oneshotG Σ} γ (v w: val) :
shot γ v -∗ shot γ w -∗ ⌜v = w⌝.
Proof.
iIntros "Hs1 Hs2".
- iDestruct (own_valid_2 with "Hs1 Hs2") as %Hfoo.
+ iCombine "Hs1 Hs2" gives %Hfoo.
iPureIntro. by apply to_agree_op_inv_L.
Qed.
Global Instance pending_fractional `{oneshotG Σ} γ : Fractional (pending γ)%I.
diff --git a/theories/lecture_notes/ccounter.v b/theories/lecture_notes/ccounter.v
index 2761d844..aec7ca2f 100644
--- a/theories/lecture_notes/ccounter.v
+++ b/theories/lecture_notes/ccounter.v
@@ -101,7 +101,7 @@ Section ccounter.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
- iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid.
+ iCombine "H1 HOwnfrag" gives %Hleq%ccounterRA_valid.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
iFrame; iIntros "!>!%".
@@ -122,7 +122,7 @@ Section ccounter.
- iIntros (m) "!# [HownE HOwnfrag]".
iInv (N .@ "counter") as (k) "[>H1 >H2]" "HClose".
iDestruct (makeElem_eq with "HownE H2") as %->.
- iDestruct (own_valid_2 with "H1 HOwnfrag") as %Hleq%ccounterRA_valid_full; simplify_eq.
+ iCombine "H1 HOwnfrag" gives %Hleq%ccounterRA_valid_full; simplify_eq.
iMod ("HClose" with "[H1 H2]") as "_".
{ iExists _; by iFrame. }
iFrame; by iIntros "!>!%".
diff --git a/theories/lecture_notes/coq_intro_example_2.v b/theories/lecture_notes/coq_intro_example_2.v
index 208e2ad6..1affbc1b 100644
--- a/theories/lecture_notes/coq_intro_example_2.v
+++ b/theories/lecture_notes/coq_intro_example_2.v
@@ -295,7 +295,7 @@ Section monotone_counter.
wp_load.
(* NOTE: We use the validity property of the RA we have constructed. From the fact that we own
◯ n and ● m to conclude that n ≤ m. *)
- iDestruct (own_valid_2 with "HOwnAuth HOwnFrag") as %H%mcounterRA_valid_auth_frag.
+ iCombine "HOwnAuth HOwnFrag" gives %H%mcounterRA_valid_auth_frag.
iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
{ iNext; iExists m; iFrame. }
iModIntro.
@@ -653,7 +653,7 @@ Section ccounter.
Proof.
iIntros (Φ) "[Hown #Hinv] HΦ".
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
- iDestruct (own_valid_2 with "Hγ Hown") as % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
+ iCombine "Hγ Hown" gives % ?%ccounterRA_valid. (* We use the validity property of our RA. *)
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists c; by iFrame|].
iApply ("HΦ" with "[-]"); rewrite /is_ccounter; eauto.
Qed.
@@ -664,7 +664,7 @@ Section ccounter.
Proof.
iIntros (Φ) "[Hown #Hinv] HΦ".
rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hpt]" "Hclose". wp_load.
- iDestruct (own_valid_2 with "Hγ Hown") as % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
+ iCombine "Hγ Hown" gives % <-%ccounterRA_valid_full. (* We use the validity property of our RA. *)
iMod ("Hclose" with "[Hpt Hγ]") as "_"; [iNext; iExists n; by iFrame|].
iApply "HΦ"; iModIntro. iFrame "Hown #"; done.
Qed.
diff --git a/theories/lecture_notes/lock.v b/theories/lecture_notes/lock.v
index 4994a2e5..b1bc4d52 100644
--- a/theories/lecture_notes/lock.v
+++ b/theories/lecture_notes/lock.v
@@ -122,7 +122,7 @@ Section lock_spec.
iDestruct "Hi" as (ℓ ->) "Hinv".
wp_lam.
iInv (lockN #ℓ) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+ - iCombine "Hld Ht" gives %Hv. done.
- wp_store.
iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
iApply "Hcont".
diff --git a/theories/lecture_notes/lock_unary_spec.v b/theories/lecture_notes/lock_unary_spec.v
index 7ab0883f..e122dd36 100644
--- a/theories/lecture_notes/lock_unary_spec.v
+++ b/theories/lecture_notes/lock_unary_spec.v
@@ -135,7 +135,7 @@ Section lock_spec.
iIntros (HE φ) "(#Hi & Hld & HP) Hcont"; rewrite /release.
wp_lam.
iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+ - iCombine "Hld Ht" gives %Hv. done.
- wp_store.
iMod ("Hcl" with "[-Hcont]") as "_"; first by iNext; iLeft; iFrame.
iApply "Hcont".
@@ -194,7 +194,7 @@ Section lock_spec.
iIntros (HE) "(#Hi & Hld & HP)"; rewrite /release.
wp_lam.
iInv (lockN l) as "[(Hl & HQ & >Ht)|Hl]" "Hcl".
- - iDestruct (own_valid_2 with "Hld Ht") as %Hv. done.
+ - iCombine "Hld Ht" gives %Hv. done.
- wp_store.
iMod ("Hcl" with "[-]") as "_"; first by iNext; iLeft; iFrame.
done.
diff --git a/theories/lecture_notes/modular_incr.v b/theories/lecture_notes/modular_incr.v
index 9edae971..8ff6a39b 100644
--- a/theories/lecture_notes/modular_incr.v
+++ b/theories/lecture_notes/modular_incr.v
@@ -75,7 +75,7 @@ Section cnt_model.
γ ⤇[p] n -∗ γ ⤇[q] m -∗ ⌜n = m⌝.
Proof.
iIntros "H1 H2".
- iDestruct (own_valid_2 with "H1 H2") as %HValid.
+ iCombine "H1 H2" gives %HValid.
destruct HValid as [_ H2].
iIntros "!%"; by apply to_agree_op_inv_L.
Qed.
diff --git a/theories/locks/array_based_queuing_lock/abql.v b/theories/locks/array_based_queuing_lock/abql.v
index ba86dd4d..a0af4571 100644
--- a/theories/locks/array_based_queuing_lock/abql.v
+++ b/theories/locks/array_based_queuing_lock/abql.v
@@ -282,7 +282,7 @@ Section proof.
Lemma locked_exclusive (γ κ : gname) o o' : locked γ κ o -∗ locked γ κ o' -∗ False.
Proof.
iIntros "[H1 _] [H2 _]".
- iDestruct (own_valid_2 with "H1 H2") as %[[] _]%auth_frag_op_valid_1.
+ iCombine "H1 H2" gives %[[] _]%auth_frag_op_valid_1.
Qed.
(* Only one thread can know the exact value of `o`. *)
@@ -290,7 +290,7 @@ Section proof.
own γ (◯ (Excl' o, GSet ∅)) -∗ own γ (◯ (Excl' o', GSet ∅)) -∗ False.
Proof.
iIntros "H1 H2".
- iDestruct (own_valid_2 with "H1 H2") as %[[]]%auth_frag_op_valid_1.
+ iCombine "H1 H2" gives %[[]]%auth_frag_op_valid_1.
Qed.
(* Lemmas about both, left, and right. *)
@@ -317,7 +317,7 @@ Section proof.
-∗ ⌜o ≤ x < o + i⌝ ∗ own γ (◯ (ε, GSet {[ x ]})) ∗ own γ (● (Excl' o, GSet (set_seq o i))).
Proof.
iIntros "P O".
- iDestruct (own_valid_2 with "O P") as %[[_ xIncl%gset_disj_included]%prod_included Hv]%auth_both_valid_discrete.
+ iCombine "O P" gives %[[_ xIncl%gset_disj_included]%prod_included Hv]%auth_both_valid_discrete.
iFrame. iPureIntro.
apply elem_of_subseteq_singleton, elem_of_set_seq in xIncl.
lia.
@@ -328,7 +328,7 @@ Section proof.
-∗ ⌜0 < i⌝ ∗ own γ (◯ (ε, GSet {[ o ]})) ∗ own γ (● (Excl' o, GSet (set_seq o i))).
Proof.
iIntros "P O".
- iDestruct (own_valid_2 with "O P") as %HV%auth_both_valid_discrete.
+ iCombine "O P" gives %HV%auth_both_valid_discrete.
iFrame. iPureIntro.
destruct HV as [[_ H%gset_disj_included]%prod_included _].
apply elem_of_subseteq_singleton, set_seq_len_pos in H.
@@ -542,7 +542,7 @@ Section proof.
wp_bind (_ <- _)%E.
iInv N as (o' i xs) "(>%lenEq & >nextPts & arrPts & >Invs & >Auth & Part)" "Close".
(* We want to show that o and o' are equal. We know this from the loked γ o ghost state. *)
- iDestruct (own_valid_2 with "Auth Locked") as
+ iCombine "Auth Locked" gives
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
rewrite rem_mod_eq //.
iApply (array_store with "[arrPts]").
@@ -569,7 +569,7 @@ Section proof.
* iDestruct (know_o_exclusive with "Locked Locked'") as "[]".
(* This is the case where the lock is clopen, that is, the actual state
of the lock. *)
- * iDestruct (own_valid_2 with "Auth Locked") as
+ * iCombine "Auth Locked" gives
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid_discrete.
rewrite rem_mod_eq //.
iApply (wp_store_offset with "arrPts").
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index 6ac6b470..e650008a 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -85,7 +85,7 @@ Section tada.
tada_lock_state γ s1 -∗ ghost_var γ.(tada_lock_name_state) (3/4) s2 -∗ False.
Proof.
iIntros "[Hvar1 _] Hvar2".
- iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[Hval _].
+ iCombine "Hvar1 Hvar2" gives %[Hval _].
exfalso. done.
Qed.
Lemma tada_lock_state_exclusive γ s1 s2 :
diff --git a/theories/locks/freeable_lock/freeable_spin_lock.v b/theories/locks/freeable_lock/freeable_spin_lock.v
index 83237eca..b59be583 100644
--- a/theories/locks/freeable_lock/freeable_spin_lock.v
+++ b/theories/locks/freeable_lock/freeable_spin_lock.v
@@ -49,7 +49,7 @@ Section proof.
own γ.(spin_lock_name_own) q.
Lemma locked_exclusive (γ : spin_lock_name) : locked γ -∗ locked γ -∗ False.
- Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
+ Proof. iIntros "H1 H2". by iCombine "H1 H2" gives %?. Qed.
Lemma own_lock_valid (γ : spin_lock_name) q :
own_lock γ q -∗ ⌜q ≤ 1⌝%Qp.
@@ -105,7 +105,7 @@ Section proof.
Proof.
iIntros (Φ) "[#Hl Hown] HΦ". iDestruct "Hl" as (l ->) "#Hinv".
wp_rec. wp_bind (CmpXchg _ _ _). iInv N as "[Hlock|>[_ Hcancel]]"; last first.
- { rewrite /own_lock. iDestruct (own_valid_2 with "Hown Hcancel") as %Hc.
+ { rewrite /own_lock. iCombine "Hown Hcancel" gives %Hc.
rewrite frac_op frac_valid in Hc. exfalso. eapply Qp.not_add_le_r. done. }
iDestruct "Hlock" as ([]) "[Hl HR]".
- wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iLeft; iExists true; eauto).
diff --git a/theories/logatom/conditional_increment/cinc.v b/theories/logatom/conditional_increment/cinc.v
index f4682c4c..6afcd992 100644
--- a/theories/logatom/conditional_increment/cinc.v
+++ b/theories/logatom/conditional_increment/cinc.v
@@ -220,7 +220,7 @@ Section conditional_counter.
counter_content γs c1 -∗ counter_content γs c2 -∗ False.
Proof.
iIntros "Hb1 Hb2".
- iDestruct (own_valid_2 with "Hb1 Hb2") as %?%auth_frag_op_valid_1.
+ iCombine "Hb1 Hb2" gives %?%auth_frag_op_valid_1.
done.
Qed.
@@ -243,10 +243,10 @@ Section conditional_counter.
iInv stateN as (vs) "(Hp & [NotDone | Done])".
* (* Moved back to NotDone: contradiction. *)
iDestruct "NotDone" as "(>Hs' & _ & _)".
- iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
+ iCombine "Hs Hs'" gives %?. contradiction.
* iDestruct "Done" as "(_ & QT & Hghost)".
iDestruct "QT" as "[Q | >T]"; last first.
- { iDestruct (own_valid_2 with "Ht T") as %Contra.
+ { iCombine "Ht T" gives %Contra.
by inversion Contra. }
iSplitR "Q"; last done. iIntros "!> !>". unfold state_inv.
iExists _. iFrame "Hp". iRight.
@@ -273,7 +273,7 @@ Section conditional_counter.
as token for that transition. *)
iDestruct "Done" as "(_ & _ & Hlghost & _)".
iDestruct "Hlghost" as (v') ">Hlghost".
- by iDestruct (mapsto_valid_2 with "Hl_ghost Hlghost") as %[??].
+ by iCombine "Hl_ghost Hlghost" gives %[??].
}
iDestruct "NotDone" as "(>Hs & >Hc' & [Pending | Accepted])".
{ (* We also cannot be [Pending] any more we have [own γ_n] showing that this
@@ -408,12 +408,12 @@ Section conditional_counter.
iDestruct "Accepted" as "[>Hl_ghost_inv _]".
iDestruct "Hl_ghost_inv" as (v) "Hlghost".
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
- by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %[??].
+ by iCombine "Hlghost Hl_ghost'" gives %[??].
+ (* Done: contradiction *)
iDestruct "Done" as "[QT >[Hlghost _]]".
iDestruct "Hlghost" as (v) "Hlghost".
iCombine "Hl_ghost'" "Hl_ghost'2" as "Hl_ghost'".
- by iDestruct (mapsto_valid_2 with "Hlghost Hl_ghost'") as %[??].
+ by iCombine "Hlghost Hl_ghost'" gives %[??].
- (* we are the failing thread. exploit that [f] is a GC location. *)
iMod (inv_mapsto_acc with "GC isGC") as (b) "(_ & H↦ & Hclose)"; first solve_ndisj.
wp_load.
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 97713ff4..220e3f97 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -425,7 +425,7 @@ Section counter_proof.
iExists Ψ. rewrite bool_decide_eq_false_2 //. iFrame.
- iDestruct "Done" as "[_ Htok]".
(* contradictory *)
- iDestruct (own_valid_2 with "Hex Htok") as %[].
+ iCombine "Hex Htok" gives %[].
Qed.
(** We obtain the post condition of the AU for [put] after it has been executed,
@@ -466,7 +466,7 @@ Section counter_proof.
rewrite bool_decide_eq_false_2 //.
iFrame.
- iDestruct "Done" as "[_ Htok]".
- iDestruct (own_valid_2 with "Hex Htok") as %[].
+ iCombine "Hex Htok" gives %[].
Qed.
(** ** Proving the actual specs for the counter operations *)
@@ -653,7 +653,7 @@ Next Obligation.
Qed.
Next Obligation.
intros ???? [γ_cnt γ_ex] ??. iIntros "[_ H1] [_ H2]".
- iDestruct (own_valid_2 with "H1 H2") as %[].
+ iCombine "H1 H2" gives %[].
Qed.
Global Typeclasses Opaque value is_counter.
diff --git a/theories/logatom/elimination_stack/hocap_spec.v b/theories/logatom/elimination_stack/hocap_spec.v
index ed453a27..885c1d77 100644
--- a/theories/logatom/elimination_stack/hocap_spec.v
+++ b/theories/logatom/elimination_stack/hocap_spec.v
@@ -350,14 +350,14 @@ Section hocap_pred_auth.
hocap_auth.pop_spec := hocap_auth_pop |}.
Next Obligation.
iIntros (???) "Hf1 Hf2".
- iDestruct (own_valid_2 with "Hf1 Hf2") as %[]%auth_frag_op_valid_1.
+ iCombine "Hf1 Hf2" gives %[]%auth_frag_op_valid_1.
Qed.
Next Obligation.
iIntros (???) "Ha1 Ha2".
- iDestruct (own_valid_2 with "Ha1 Ha2") as %[]%auth_auth_op_valid.
+ iCombine "Ha1 Ha2" gives %[]%auth_auth_op_valid.
Qed.
Next Obligation.
- iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
+ iIntros (???) "Hf Ha". iCombine "Ha Hf" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete. done.
Qed.
Next Obligation.
diff --git a/theories/logatom/elimination_stack/stack.v b/theories/logatom/elimination_stack/stack.v
index 28bdeae8..146a6c70 100644
--- a/theories/logatom/elimination_stack/stack.v
+++ b/theories/logatom/elimination_stack/stack.v
@@ -96,7 +96,7 @@ Section stack.
stack_content γs l1 -∗ stack_content γs l2 -∗ False.
Proof.
iIntros "Hl1 Hl2".
- iDestruct (own_valid_2 with "Hl1 Hl2") as %[]%auth_frag_op_valid_1.
+ iCombine "Hl1 Hl2" gives %[]%auth_frag_op_valid_1.
Qed.
Definition stack_elem_to_val (stack_rep : option loc) : val :=
@@ -210,7 +210,7 @@ Section stack.
- (* The CAS succeeded. Update everything accordingly. *)
iMod "AU" as (l') "[Hl' [_ Hclose]]".
iMod (mapsto_persist with "Hhead_new") as "#Hhead_new".
- iDestruct (own_valid_2 with "Hs● Hl'") as
+ iCombine "Hs● Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
@@ -255,14 +255,14 @@ Section stack.
wp_if. iApply ("IH" with "AU").
+ (* Offer revoked by someone else? Impossible! *)
iDestruct "Hst" as ">Hst".
- iDestruct (own_valid_2 with "Htok Hst") as %[].
+ iCombine "Htok Hst" gives %[].
+ (* Offer got accepted by someone, awesome! We are done. *)
iModIntro. iSplitR "Hst".
{ iNext. iExists OfferAcked. iFrame. }
wp_if. by iApply "Hst".
+ (* Offer got acked by someone else? Impossible! *)
iDestruct "Hst" as ">Hst".
- iDestruct (own_valid_2 with "Htok Hst") as %[].
+ iCombine "Htok Hst" gives %[].
Qed.
Lemma pop_spec γs (s : val) :
@@ -284,7 +284,7 @@ Section stack.
prove that. *)
iDestruct "Hlist" as ">%". subst stack_rep.
iMod "AU" as (l') "[Hl' [_ Hclose]]".
- iDestruct (own_valid_2 with "Hs● Hl'") as
+ iCombine "Hs● Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod ("Hclose" with "Hl'") as "HΦ".
iSplitR "HΦ"; first by eauto 10 with iFrame.
@@ -306,7 +306,7 @@ Section stack.
+ (* CAS succeeded! It must still be the same head element in the list,
and we are done. *)
iMod "AU" as (l') "[Hl' [_ Hclose]]".
- iDestruct (own_valid_2 with "Hs● Hl'") as
+ iCombine "Hs● Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
destruct l as [|v' l]; simpl.
{ (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
@@ -346,13 +346,13 @@ Section stack.
iMod (lc_fupd_elim_later with "Hlc Hoff") as "AUoff".
iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
- iDestruct (own_valid_2 with "Hs● Hl'") as
+ iCombine "Hs● Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
iMod ("Hclose" with "Hl'") as "HQoff".
iMod "AU" as (l') "[Hl' [_ Hclose]]".
- iDestruct (own_valid_2 with "Hs● Hl'") as
+ iCombine "Hs● Hl'" gives
%[->%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
{ eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index fa6f4eaa..0aa9e761 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -180,7 +180,7 @@ Lemma hwq_cont_exclusive γe elts1 elts2 :
hwq_cont γe elts1 -∗ hwq_cont γe elts2 -∗ False.
Proof.
iIntros "H1 H2".
- by iDestruct (own_valid_2 with "H1 H2") as %?%auth_frag_op_valid_1.
+ by iCombine "H1 H2" gives %?%auth_frag_op_valid_1.
Qed.
(** Operations for the CMRA used to show that back only increases. *)
@@ -258,12 +258,12 @@ Proof. apply own_update. by apply cmra_update_exclusive. Qed.
Lemma contra_not_no_contra i1 i2 γc :
no_contra γc -∗ contra γc i1 i2 -∗ False.
-Proof. iIntros "HnoC HC". iDestruct (own_valid_2 with "HnoC HC") as %[]. Qed.
+Proof. iIntros "HnoC HC". iCombine "HnoC HC" gives %[]. Qed.
Lemma contra_agree i1 i2 i1' i2' γc :
contra γc i1 i2 -∗ contra γc i1' i2' -∗ ⌜i1' = i1 ∧ i2' = i2⌝.
Proof.
- iIntros "HC HC'". iDestruct (own_valid_2 with "HC HC'") as %H.
+ iIntros "HC HC'". iCombine "HC HC'" gives %H.
iPureIntro. apply to_agree_op_inv_L in H. by inversion H.
Qed.
@@ -436,7 +436,7 @@ Lemma use_val_wit γs slots i l :
slot_val_wit γs i l -∗
⌜val_of <$> slots !! i = Some l⌝.
Proof.
- iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -469,7 +469,7 @@ Lemma use_name_tok γs slots i γ :
slot_name_tok γs i γ -∗
⌜name_of <$> slots !! i = Some (Some γ)⌝.
Proof.
- iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -538,7 +538,7 @@ Lemma use_committed_wit γs slots i :
slot_committed_wit γs i -∗
⌜was_committed <$> slots !! i = Some true⌝.
Proof.
- iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
@@ -564,7 +564,7 @@ Lemma use_written_wit γs slots i :
slot_written_wit γs i -∗
⌜was_written <$> slots !! i = Some true⌝.
Proof.
- iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
+ iIntros "H● Hwit". iCombine "H● Hwit" gives %H.
iPureIntro. apply auth_both_valid_discrete in H as [H%singleton_included_l _].
destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index b33a7e92..00dc678c 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -334,7 +334,7 @@ Section rdcss.
iDestruct "Hn1" as (γ_1) "[#Meta1 Hn1]".
iDestruct "Hn2" as (γ_2) "[#Meta2 Hn2]".
iDestruct (meta_agree with "Meta1 Meta2") as %->.
- by iDestruct (own_valid_2 with "Hn1 Hn2") as %?%auth_frag_op_valid_1.
+ by iCombine "Hn1 Hn2" gives %?%auth_frag_op_valid_1.
Qed.
(** A few more helper lemmas that will come up later *)
@@ -350,10 +350,10 @@ Section rdcss.
iInv descrN as (vs) "(Hp & [NotDone | Done])".
* (* Moved back to NotDone: contradiction. *)
iDestruct "NotDone" as "(>Hs' & _ & _)".
- iDestruct (own_valid_2 with "Hs Hs'") as %?. contradiction.
+ iCombine "Hs Hs'" gives %?. contradiction.
* iDestruct "Done" as "(_ & QT & Hrest)".
iDestruct "QT" as "[Qn | >T]"; last first.
- { iDestruct (own_valid_2 with "Ht T") as %Contra.
+ { iCombine "Ht T" gives %Contra.
by inversion Contra. }
iSplitR "Qn"; last done. iIntros "!> !>". unfold descr_inv.
iExists _. iFrame "Hp". iRight.
@@ -378,12 +378,12 @@ Section rdcss.
{ (* We cannot be [done] yet, as we own the [γ_a] token that serves
as token for that transition. *)
iDestruct "Done" as "(_ & _ & _ & _ & >Token_a')".
- by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
+ by iCombine "Token_a Token_a'" gives %?.
}
iDestruct "NotDone" as "(>Hs & >Hln' & [Pending | Accepted])".
{ (* We also cannot be [Pending] any more because we own the [γ_a] token. *)
iDestruct "Pending" as "[_ >(_ & _ & Token_a')]".
- by iDestruct (own_valid_2 with "Token_a Token_a'") as %?.
+ by iCombine "Token_a Token_a'" gives %?.
}
(* So, we are [Accepted]. Now we can show that (InjRV l_descr) = (state_to_val s), because
while a [descr] protocol is not [done], it owns enough of
diff --git a/theories/logatom/snapshot/atomic_snapshot.v b/theories/logatom/snapshot/atomic_snapshot.v
index 07f8cf69..02f0625a 100644
--- a/theories/logatom/snapshot/atomic_snapshot.v
+++ b/theories/logatom/snapshot/atomic_snapshot.v
@@ -117,7 +117,7 @@ Section atomic_snapshot.
snapshot_content γs a1 -∗ snapshot_content γs a2 -∗ False.
Proof.
iIntros "H1 H2".
- iDestruct (own_valid_2 with "H1 H2") as %[]%auth_frag_op_valid_1.
+ iCombine "H1 H2" gives %[]%auth_frag_op_valid_1.
Qed.
Definition new_timestamp t v : gmap Z val := {[ t := v ]}.
@@ -165,7 +165,7 @@ Section atomic_snapshot.
own γ (● (Excl' n)) -∗ own γ (◯ (Excl' m)) -∗ ⌜m = n⌝.
Proof.
iIntros "Hγ● Hγ◯".
- iDestruct (own_valid_2 with "Hγ● Hγ◯") as
+ iCombine "Hγ● Hγ◯" gives
%[H%Excl_included%leibniz_equiv _]%auth_both_valid_discrete.
done.
Qed.
@@ -196,7 +196,7 @@ Section atomic_snapshot.
⌜∀ t x, T2 !! t = Some x → T1 !! t = Some x⌝.
Proof.
iIntros "[Hγ⚫ Hγ◯]".
- iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
+ iCombine "Hγ⚫ Hγ◯" gives
%[H Hv]%auth_both_valid_discrete. iPureIntro. intros t x HT2.
pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
rewrite !lookup_fmap HT2 /= in Ht.
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index 83746b9d..3b25de1d 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -257,26 +257,26 @@ Section logrel.
+ destruct (decide (l2 = l)); simplify_eq.
* destruct (decide (l2' = l')); simplify_eq; first by iFrame.
iInv (logN.@(l, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
- iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+ iCombine "Hl Hlx" gives %[? ?]; done.
* destruct (decide (l2' = l')); simplify_eq; last first.
{ iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
iInv (logN.@(l2, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
- iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+ iCombine "Hl' Hlx'" gives %[??]; done.
+ iInv (logN.@(l, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
- iDestruct (mapsto_valid_2 with "Hl Hlx") as %[? ?]; done.
+ iCombine "Hl Hlx" gives %[? ?]; done.
- destruct (decide (l1 = l2)); simplify_eq.
+ destruct (decide (l1' = l2')); simplify_eq; first by iFrame.
iInv (logN.@(l2, l1')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
- iDestruct (mapsto_valid_2 with "Hly Hlx") as %[? ?]; done.
+ iCombine "Hly Hlx" gives %[? ?]; done.
+ destruct (decide (l1' = l2')); simplify_eq; last first.
{ iModIntro; iFrame; iPureIntro; intuition simplify_eq. }
destruct (decide (l2' = l')); simplify_eq.
* iInv (logN.@(l1, l')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
- iDestruct (mapstoS_valid_2 with "Hl' Hlx'") as %?; done.
+ iCombine "Hl' Hlx'" gives %[??]; done.
* iInv (logN.@(l1, l2')) as ([v v']) "(>Hlx & >Hlx' & Hvv) /=" "Hclose".
iInv (logN.@(l2, l2')) as ([w w']) "(>Hly & >Hly' & Hww) /=" "Hclose'".
- iDestruct (mapstoS_valid_2 with "Hly' Hlx'") as %?; done.
+ iCombine "Hly' Hlx'" gives %[??]; done.
Qed.
End logrel.
diff --git a/theories/logrel/F_mu_ref_conc/binary/rules.v b/theories/logrel/F_mu_ref_conc/binary/rules.v
index 616ab06b..b5a9e31b 100644
--- a/theories/logrel/F_mu_ref_conc/binary/rules.v
+++ b/theories/logrel/F_mu_ref_conc/binary/rules.v
@@ -189,6 +189,14 @@ Section cfg.
by iApply (mapstoS_valid l _ v2).
Qed.
+ Global Instance mapstoS_combine_sep_gives l dq1 dq2 v1 v2 :
+ CombineSepGives (l ↦ₛ{dq1} v1) (l ↦ₛ{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+ Proof.
+ rewrite /CombineSepGives. iIntros "[H1 H2]". iSplit.
+ - iDestruct (mapstoS_valid_2 with "H1 H2") as %?; auto.
+ - iDestruct (mapstoS_agree with "H1 H2") as %?; auto.
+ Qed.
+
Lemma step_insert K tp j e σ κ e' σ' efs :
tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs →
erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
diff --git a/theories/logrel/F_mu_ref_conc/binary/soundness.v b/theories/logrel/F_mu_ref_conc/binary/soundness.v
index 91c9fd8c..d17fc858 100644
--- a/theories/logrel/F_mu_ref_conc/binary/soundness.v
+++ b/theories/logrel/F_mu_ref_conc/binary/soundness.v
@@ -44,7 +44,7 @@ Proof.
- iModIntro. iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
rewrite /tpool_mapsto /=.
- iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
+ iCombine "Hown Hj" gives %Hvalid.
move: Hvalid=> /auth_both_valid_discrete
[/prod_included [/tpool_singleton_included Hv2 _] _].
destruct tp as [|? tp']; simplify_eq/=.
diff --git a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
index aa06206f..11439b0f 100644
--- a/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
+++ b/theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
@@ -47,7 +47,7 @@ Section symbol_nat_sem_typ.
Proof.
iIntros "Hmt Htk".
rewrite /Max_token /Token; simpl.
- by iDestruct (own_valid_2 with "Hmt Htk") as
+ by iCombine "Hmt Htk" gives
%[?%max_nat_included _]%auth_both_valid_discrete.
Qed.
diff --git a/theories/proph/eager_coin.v b/theories/proph/eager_coin.v
index 91958dc2..572a49a0 100644
--- a/theories/proph/eager_coin.v
+++ b/theories/proph/eager_coin.v
@@ -26,7 +26,7 @@ Section proof.
iDestruct "H1" as (l1) "[% Hl1]".
iDestruct "H2" as (l2) "[% Hl2]".
simplify_eq.
- by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
+ by iCombine "Hl1 Hl2" gives %[??].
Qed.
Lemma new_eager_coin_spec :
diff --git a/theories/proph/lazy_coin_one_shot.v b/theories/proph/lazy_coin_one_shot.v
index ed9c68e1..b6015f30 100644
--- a/theories/proph/lazy_coin_one_shot.v
+++ b/theories/proph/lazy_coin_one_shot.v
@@ -48,7 +48,7 @@ Section proof.
simplify_eq.
iDestruct "H1" as "[Hc1 | [Hc1 _]]";
iDestruct "H2" as "[Hc2 | [Hc2 _]]";
- by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %[??].
+ by iCombine "Hc1 Hc2" gives %[??].
Qed.
Lemma new_lazy_coin_spec :
diff --git a/theories/proph/lazy_coin_one_shot_typed.v b/theories/proph/lazy_coin_one_shot_typed.v
index 2cc2d5e1..9abef6be 100644
--- a/theories/proph/lazy_coin_one_shot_typed.v
+++ b/theories/proph/lazy_coin_one_shot_typed.v
@@ -40,7 +40,7 @@ Section proof.
simplify_eq.
iDestruct "H1" as "[Hc1 | [Hc1 _]]";
iDestruct "H2" as "[Hc2 | [Hc2 _]]";
- by iDestruct (mapsto_valid_2 with "Hc1 Hc2") as %[??].
+ by iCombine "Hc1 Hc2" gives %[??].
Qed.
Lemma new_lazy_coin_spec :
--
GitLab