From a15d9e2ea567783ee62ab62ce6463f7709ec0a07 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 13 Nov 2023 11:20:41 +0100
Subject: [PATCH] =?UTF-8?q?Patch=20now=20that=20frame=20=E2=88=83=20looks?=
=?UTF-8?q?=20beneath=20definitions=20again?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
.../concurrent_stacks/concurrent_stack3.v | 2 +-
.../concurrent_stacks/concurrent_stack4.v | 2 +-
theories/lecture_notes/stack.v | 6 ++----
.../freeable_lock/freeable_logatom_lock.v | 3 +--
.../counter_with_backup/counter_proof.v | 9 ++++-----
theories/logatom/flat_combiner/flat.v | 19 +++++++------------
theories/logatom/flat_combiner/peritem.v | 11 ++++-------
theories/logatom/herlihy_wing_queue/hwq.v | 8 +++-----
8 files changed, 23 insertions(+), 37 deletions(-)
diff --git a/theories/concurrent_stacks/concurrent_stack3.v b/theories/concurrent_stacks/concurrent_stack3.v
index 233bf783..932a1f19 100644
--- a/theories/concurrent_stacks/concurrent_stack3.v
+++ b/theories/concurrent_stacks/concurrent_stack3.v
@@ -106,7 +106,7 @@ Section stack_works.
iMod (pointsto_persist with "Hl'") as "#Hl'".
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod ("Hclose" with "[Hl HP Hlist]") as "_".
- { iNext; iExists (Some _), (v :: xs); iFrame; iExists _; iFrame; auto. }
+ { iNext; iExists (Some _), (v :: xs); iFrame "#∗". }
iModIntro.
wp_pures.
by iApply ("HΦ" with "HΨ").
diff --git a/theories/concurrent_stacks/concurrent_stack4.v b/theories/concurrent_stacks/concurrent_stack4.v
index 22224c11..ea991680 100644
--- a/theories/concurrent_stacks/concurrent_stack4.v
+++ b/theories/concurrent_stacks/concurrent_stack4.v
@@ -340,7 +340,7 @@ Section proofs.
iMod ("Hupd" with "HP") as "[HP HΨ]".
iMod "Hupd'" as "_".
iMod ("Hclose" with "[Hl HP Hlist]") as "_".
- { iNext; iExists (Some _), (v' :: xs); iFrame; iExists _; iFrame; auto. }
+ { iNext; iExists (Some _), (v' :: xs); iFrame "#∗". }
iModIntro.
wp_pures.
by iApply ("HΦ" with "HΨ").
diff --git a/theories/lecture_notes/stack.v b/theories/lecture_notes/stack.v
index 0ce8e928..7a572cc0 100644
--- a/theories/lecture_notes/stack.v
+++ b/theories/lecture_notes/stack.v
@@ -89,8 +89,7 @@ Section stack_spec.
wp_store.
iApply "HΦ".
iExists â„“, (SOMEV #â„“'); iFrame.
- iSplitR; first done.
- iExists â„“', hd; by iFrame.
+ iSplitR; done.
Qed.
Lemma pop_spec_nonempty s (x : val) xs:
@@ -183,8 +182,7 @@ Proof.
wp_store.
iApply "HΨ".
iExists â„“, (SOMEV #â„“'); iFrame.
- iSplitR; first done.
- iExists â„“', x, hd; by iFrame.
+ iSplitR; done.
Qed.
Lemma pop_ownership_spec_nonempty s Φ Φs:
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index 97e795fb..9c400364 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/theories/locks/freeable_lock/freeable_logatom_lock.v
@@ -137,8 +137,7 @@ Section tada.
rewrite {1}/sum_loans /= map_fold_sum_loans_add Qp.div_2. done.
- iApply big_sepM_insert; first done. iFrame "Hloans".
iExists _. by iFrame. }
- iModIntro. iExists _. iFrame.
- iExists _, _. by iFrame.
+ iModIntro. iExists _. iFrame "#∗".
Qed.
Local Lemma return_lock_loan γ q Q :
diff --git a/theories/logatom/counter_with_backup/counter_proof.v b/theories/logatom/counter_with_backup/counter_proof.v
index 7482f654..ad53ab7e 100644
--- a/theories/logatom/counter_with_backup/counter_proof.v
+++ b/theories/logatom/counter_with_backup/counter_proof.v
@@ -493,8 +493,7 @@ Section counter_proof.
iDestruct (mono_nat_auth_own_agree with "Hcnt Cnt") as %[_ ->].
iDestruct (mono_nat_lb_own_valid with "Hprim Hn_p") as %[_ Hle].
iAaccIntro with "Hb".
- { iIntros "Hb". iFrame. iModIntro. iNext. rewrite /counter_inv /counter_inv_inner.
- iExists G, P, n, n_p'. iFrame. iPureIntro. lia. }
+ { iIntros "Hb". iFrame. iPureIntro. lia. }
iIntros "Hb". iMod (lc_fupd_elim_later with "Hone Hrest") as "(HG & #Hlook & HP & Hgets & Hputs)".
iMod (logically_execute_gets_and_puts _ _ _ _ _ n_p with "Hputs Hgets Cnt Cnt2 Hcnt") as "(Hputs & Hgets & Cnt & Cnt2 & Hcnt)"; first (split; by eauto).
iModIntro. iSplitR "Cnt Cnt2".
@@ -537,7 +536,7 @@ Section counter_proof.
awp_apply load_spec.
iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
iAaccIntro with "Hp".
- { iIntros "Hp". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+ { iIntros "Hp". iModIntro. iFrame. eauto. }
iIntros "Hp". iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
assert (n_b = n_p ∨ n_b < n_p) as [->|Hlt] by lia.
- (* we are reading the latest value, we can linearize now *)
@@ -574,7 +573,7 @@ Section counter_proof.
awp_apply load_spec.
iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
iAaccIntro with "Hb".
- { iIntros "Hb". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+ { iIntros "Hb". iModIntro. by iFrame. }
iIntros "Hb".
iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
iMod "AU" as (n) "[[Hc Hex] [_ Hclose]]".
@@ -595,7 +594,7 @@ Section counter_proof.
awp_apply faa_spec.
iInv "I" as (G P n_b n_p) "(>% & >Hb & >Hp & Hrest)".
iAaccIntro with "Hp".
- { iIntros "Hp". iModIntro. iFrame. iNext. rewrite /counter_inv /counter_inv_inner. iExists G, P, n_b, n_p. eauto with iFrame. }
+ { iIntros "Hp". iModIntro. by iFrame. }
iIntros "Hp". iMod (lc_fupd_elim_later with "Hone' Hrest") as "(Hcnt & Hprim & HG & #Hlook & HP & Hget & Hput)".
iMod (counter_inv_inner_register_put _ _ (γ_cnt, γ_ex) with "AU Hone Hb [Hp] Hcnt Hprim HG Hlook HP Hget Hput") as "Hupd"; first lia.
{ replace (n_p + 1)%Z with (S n_p : Z) by lia. iExact "Hp". }
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index b6a6f4eb..0a3cabc7 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -126,13 +126,10 @@ Section proof.
iModIntro. wp_let. wp_bind (push _ _).
iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
- { iNext. iRight. iLeft. iExists f, x. iFrame.
- iExists (λ _, P), (λ _ v, Q v).
- iFrame. iFrame "#". }
+ { iNext. iRight. iLeft. iExists f, x. iFrame "#∗". }
iApply (push_spec N (p_inv' R γm γr) s #p
with "[-HΦ Hx2 Ho3]")=>//.
- { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
- iSplitR; first done. iFrame "#". }
+ { by iFrame "#". }
iNext. iIntros "?".
wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
iFrame. by iFrame "#".
@@ -172,7 +169,7 @@ Section proof.
wp_store. iDestruct (m_frag_agree' with "Hx Hx2") as "[Hx %]".
subst. rewrite Qp.div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
{ iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
- iRight. iExists _, v. iFrame. iExists Q. iFrame. }
+ iRight. iExists _, v. by iFrame. }
iApply "HΦ". iFrame. done.
* iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
iApply excl_falso. iFrame.
@@ -181,7 +178,7 @@ Section proof.
- destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
- { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
+ { iNext. iRight. iRight. iRight. iExists x', y. by iFrame. }
iModIntro. wp_match. iApply "HΦ". by iFrame.
Qed.
@@ -230,7 +227,7 @@ Section proof.
iDestruct "H" as (xs' hd') "[>Hs #Hxs]".
wp_load.
iMod ("Hclose" with "[Hs]").
- { iNext. iFrame. iExists xs', hd'. by iFrame. }
+ { iFrame "#∗". }
iModIntro. wp_let. wp_bind (treiber.iter _ _).
iApply wp_wand_r. iSplitL "HR Ho2".
{ iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ()) ∗ R)%I with "[-]")=>//.
@@ -262,8 +259,7 @@ Section proof.
iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
+ iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
wp_load. iMod ("Hclose" with "[-Ho3 HΦ]") as "_".
- { iNext. (* FIXME: iFrame here divergses, with an enormous TC trace *)
- iRight. iRight. iLeft. iExists f, x. iFrame. }
+ { iNext. iRight. iRight. iLeft. iFrame. }
iModIntro. wp_match.
wp_apply try_srv_spec=>//.
iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
@@ -271,8 +267,7 @@ Section proof.
iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
{ iNext. iLeft. iExists y. iFrame. }
- iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
- iExists Q. iFrame.
+ iModIntro. wp_match. iApply ("HΦ" with "[-]"). by iFrame.
Qed.
Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
diff --git a/theories/logatom/flat_combiner/peritem.v b/theories/logatom/flat_combiner/peritem.v
index 6eabb56f..7a913e44 100644
--- a/theories/logatom/flat_combiner/peritem.v
+++ b/theories/logatom/flat_combiner/peritem.v
@@ -46,8 +46,7 @@ Section proofs.
iMod (pointsto_persist with "Hl") as "#Hl".
wp_alloc s as "Hs".
iAssert (∃ xs, is_bag_R N R xs s)%I with "[-HΦ]" as "Hxs".
- { iFrame. iExists [], l.
- iFrame. simpl. eauto. }
+ { iFrame. iExists []. eauto. }
iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
iApply "HΦ". iFrame "#". done.
Qed.
@@ -61,7 +60,7 @@ Section proofs.
iInv N as "H1" "Hclose".
iDestruct "H1" as (xs hd) "[>Hs H1]".
wp_load. iMod ("Hclose" with "[Hs H1]").
- { iNext. iFrame. iExists xs, hd. iFrame. }
+ { iFrame. }
iModIntro. wp_let. wp_alloc l as "Hl".
wp_let. wp_bind (CmpXchg _ _ _)%E.
iInv N as "H1" "Hclose".
@@ -71,13 +70,11 @@ Section proofs.
iMod (pointsto_persist with "Hl") as "#Hl".
iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
iMod ("Hclose" with "[Hs Hl H1]").
- { iNext. iFrame. iExists (x::xs'), l.
- iFrame. simpl. iExists hd'. iFrame.
- by iFrame "#". }
+ { iExists (x::xs'). iFrame "#∗". }
iModIntro. wp_pures. by iApply "HΦ".
- wp_cmpxchg_fail.
iMod ("Hclose" with "[Hs H1]").
- { iNext. iFrame. iExists (xs'), hd'. iFrame. }
+ { iFrame. }
iModIntro. wp_pures. iApply ("IH" with "HRx").
by iNext.
Qed.
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index ee5dbc4a..901a7f54 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -1512,7 +1512,7 @@ Proof.
pose (cont := NoCont (map (λ i, (i, [])) pvs)).
iNext. iExists 0, pvs, [], [], cont, ∅, ∅.
rewrite array_content_empty Nat2Z.id fmap_empty /=.
- iFrame. iSplitL. { iExists rs. by iFrame. }
+ iFrame.
repeat (iSplit; first done). iPureIntro.
repeat split_and; try done.
- intros i. split; intros Hi; [ by lia | by inversion Hi].
@@ -2674,8 +2674,6 @@ Proof.
iNext. iExists back', new_pvs, new_pref, rest, cont', slots, new_deqs.
subst new_deqs. iFrame. iSplitL "Hâ„“_ar".
{ rewrite array_content_dequeue; [ done | by lia | done ]. }
- iSplitL "Hp".
- { iExists rs'. by iFrame "Hp". }
iPureIntro. repeat split_and; try done.
- intros k. split; intros Hk; first by apply Hstate.
intros Hk_in_deqs. apply elem_of_union in Hk_in_deqs.
@@ -2742,8 +2740,8 @@ Proof.
[ by rewrite Hi | by rewrite Hi | by right | ]. iIntros "Hâ„“a" (rs' ->) "Hp".
(* We can close the invariant. *)
iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
- { iNext. iExists _, _, _, _, cont', _, _. iFrame. iSplit; last done.
- iExists rs'. rewrite Hpvs /= decide_True; last by lia. by iFrame. }
+ { iNext. iExists _, _, _, _, cont', _, _. iFrame. iSplit; last done. iPureIntro.
+ rewrite Hpvs /= decide_True; last by lia. done. }
(* And conclude using the loop induction hypothesis. *)
wp_pures. assert (S n - 1 = n)%Z as -> by lia. iClear "Hval_wit_i".
iApply ("IH_loop" with "[] [] AU Hback_snap").
--
GitLab