From 1178ec3690c838438fb464ecc80cf44166714d0d Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 10 Nov 2023 22:19:43 +0100
Subject: [PATCH] =?UTF-8?q?Fix=20for=20improved=20iFrame=20=E2=88=83?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
gpfsl-examples/exchanger/proof_mp_client.v | 5 ++---
gpfsl-examples/queue/proof_ms_abs_graph.v | 8 ++++----
gpfsl-examples/queue/proof_spsc_graph.v | 10 +++++-----
gpfsl-examples/stack/proof_elim_graph.v | 2 +-
gpfsl-examples/stack/proof_treiber_at.v | 2 +-
gpfsl-examples/stack/proof_treiber_graph.v | 2 +-
gpfsl-examples/stack/proof_treiber_history.v | 6 +++---
gpfsl/base_logic/frame_instances.v | 5 +++--
gpfsl/logic/atomic_ops.v | 5 ++---
gpfsl/logic/atomic_ops_vj.v | 3 +--
gpfsl/logic/atomic_preds.v | 4 ++--
gpfsl/logic/readonly_ptsto.v | 3 +--
12 files changed, 26 insertions(+), 29 deletions(-)
diff --git a/gpfsl-examples/exchanger/proof_mp_client.v b/gpfsl-examples/exchanger/proof_mp_client.v
index 155926b6..726ee011 100644
--- a/gpfsl-examples/exchanger/proof_mp_client.v
+++ b/gpfsl-examples/exchanger/proof_mp_client.v
@@ -79,8 +79,7 @@ Section ex.
iMod (own_alloc (â—E false â‹… â—¯E false)) as (γ2) "[Tokγ22 Tokγ21]";
[apply excl_auth_valid|].
iMod (inv_alloc N' _ (ExInv γg γ1 γ2) with "[Hex Tokγ12 Tokγ22]") as "#II".
- { iNext; iExists ∅; iFrame.
- iExists false, false. rewrite /list_max_2 /=. by iFrame. }
+ { iNext; iExists ∅; iFrame. rewrite /list_max_2 //=. }
iDestruct (view_at_intro True%I with "[//]") as (V0) "[#sV0 _]".
wp_apply (wp_fork with "[Tokγ11]"); [done|..].
@@ -198,7 +197,7 @@ Section ex.
iMod "Hclose" as "_".
iDestruct "Hown" as (b1' b2') "[Hown >[%Hsize %Eqb1]]".
iMod ("Close" with "[Hown EI]") as "_".
- { iNext. iExists G2'. iFrame. iExists b1', b2'. by iFrame. }
+ { iNext. iExists G2'. iFrame. done. }
iIntros "!>". iApply "Post". iPureIntro.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index ddb84f16..2141fac9 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1361,7 +1361,7 @@ Lemma QueueInv_no_exist_QueueLocs_access γg q Q G γ γh γl η s D L T :
Proof.
iIntros (E) "(LEL & LD & LT & F & QV & QL)".
iDestruct "QL" as (Vb) "QL".
- iExists Vb. iFrame "QL". iIntros (Vb') "QL". iFrame. by iExists Vb'.
+ iExists Vb. iFrame "QL". iIntros (Vb') "QL". iFrame.
Qed.
Lemma QueueInv_no_exist_tail_access γg q Q G γ γh γl η s D L T :
@@ -1391,7 +1391,7 @@ Lemma QueueInv_no_exist_tail_immut_access γg q Q G γ γh γl η s D L T :
Proof.
intros E. rewrite ->QueueInv_no_exist_tail_access.
iDestruct 1 as (Vb ζl) "[[T #Tls] Close]".
- iExists Vb, ζl. iFrame "T Tls".
+ iExists Vb, ζl. iFrame "T". iSplitR; [iFrame "#" | ].
iIntros (Vb') "T". iApply ("Close" $! (Vb' ⊔ Vb)). by iFrame "#∗".
Qed.
@@ -1406,8 +1406,8 @@ Proof.
intros DL E. rewrite ->QueueInv_no_exist_QueueLocs_access.
iDestruct 1 as (Vb) "[[H TNs] Close]".
iDestruct "H" as (t0 Vs) "[H #Hs]".
- iExists Vb, t0, Vs. iFrame "#∗". iIntros (Vb') "H".
- iApply ("Close" $! (Vb' ⊔ Vb)). iFrame. iExists t0, Vs. by iFrame "#∗".
+ iExists Vb, t0, Vs. iFrame "H". iSplitR; [iFrame "Hs" | ]. iIntros (Vb') "H".
+ iApply ("Close" $! (Vb' ⊔ Vb)). iFrame "#∗".
Qed.
Lemma QueueInv_agree γg q Q G Q' G' :
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 2afaa935..ddbfbc1a 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -157,7 +157,7 @@ Proof.
iIntros (Φ) "_ Post".
iMod QE_alloc as (γed) "(â—ed & â—¯e & â—¯d)".
iApply (wq.(new_queue_spec) with "[%//]").
- iIntros "!> * [#QL QI]". iApply "Post".
+ iIntros "!> * [#QL QI]". iApply "Post". unfold SPSCInv.
iFrame "#∗". iPureIntro. split_and!; [done..|].
exists []. split_and!; [done|done|done| |done..].
split; [done|]. intros (?&?&?). done.
@@ -180,8 +180,8 @@ Proof.
iSpecialize ("QI" with "[$Gm]").
iAaccIntro with "QI".
- { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
- iNext. iExists _. iFrame "QI". done. }
+ { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+ iNext. iExists _. iFrame. done. }
iIntros (V' G' enqId enq Venq M') "(QI & #⊒V' & #QL' & %F)".
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
rewrite /is_enqueue in F.
@@ -255,8 +255,8 @@ Proof.
move=> /NoDup_app [?][_] /NoDup_app [?][_]? //. }
iAaccIntro with "QI".
- { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
- iNext. iExists _. iFrame "QI". done. }
+ { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+ iNext. iExists _. iFrame. done. }
iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F)".
set (dV := mkGraphEvent deq Vdeq M') in *.
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index dc940919..1f24d1d6 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -749,7 +749,7 @@ Lemma StackInv'_graph_master_acc_instance :
∃ q', graph_master γg q' G ∗ (graph_master γg q' G -∗ StackInv' γg s q G).
Proof.
intros. iDestruct 1 as (?????????) "[(?&?&?) ?]".
- iExists _. iFrame. iIntros "?". eauto 10 with iFrame.
+ iExists _. iFrame. iIntros "?". unfold StackInv'. eauto 10 with iFrame.
Qed.
Lemma StackInv'_graph_snap_instance :
diff --git a/gpfsl-examples/stack/proof_treiber_at.v b/gpfsl-examples/stack/proof_treiber_at.v
index 3090bebc..8ce8dede 100644
--- a/gpfsl-examples/stack/proof_treiber_at.v
+++ b/gpfsl-examples/stack/proof_treiber_at.v
@@ -366,7 +366,7 @@ Proof.
rewrite /all_slocs /=. iSplitL; [|done]. iExists _, (hd_error S2).
iFrame "Hn1".
- rewrite in_sloc_cons. iFrame "Is".
- iExists v. rewrite /= /in_sloc. iFrame. iExists _. by iFrame "Hn2". }
+ iExists v. rewrite /= /in_sloc. by iFrame. }
(* re-establish the invariant *)
iMod ("Close" with "[-Post Hmn]") as "_".
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index e214c702..314a1cbf 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -602,7 +602,7 @@ Lemma StackInv_no_exist_StackLocs_access s G γ γh T S :
∗ (∀ Vb, @{Vb} StackLocs s G.(Es) γh T S -∗ StackInv_no_exist s G γ γh T S).
Proof.
iIntros "(F & SV & SL)". iDestruct "SL" as (Vb) "SL".
- iExists Vb. iFrame "SL". iIntros (Vb') "SL". iFrame. by iExists Vb'.
+ iExists Vb. iFrame "SL". iIntros (Vb') "SL". iFrame.
Qed.
Lemma StackLocs_no_exist_head_immut_access s E γh T S t0 LVs Vh :
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index 3fe11fb6..a650468b 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -1432,7 +1432,7 @@ Lemma StackInv_history_master_acc_instance :
history_master γg 1 E ∗
(history_master γg 1 E -∗ StackInv γg s E).
Proof.
- intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". eauto 11 with iFrame.
+ intros. iDestruct 1 as (?????????) "(? & $ & ?)". unfold StackInv. iIntros "$". eauto 11 with iFrame.
Qed.
Lemma StackInv_history_snap_instance :
@@ -2003,7 +2003,7 @@ Proof.
iSplitL.
+ iExists _,_,_. iExists esi1',emo1,stk1',ont1,Vt1,Vi1.
- iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
+ iFrame "∗". iSplitL.
{ (* SeenMsgsAll γh s E1' esi1' emo1 ti. *)
iNext. iIntros (e eidx eV EV EMO_LOOKUP).
case (decide (eidx = emo_e O (length esi1))) as [->|NEeidx].
@@ -2113,7 +2113,7 @@ Proof.
iSplitL.
+ iExists _,_,_. iExists esi1,emo1',stk1',ont1,Vt1,Vi1.
rewrite (_ : emo1.*2 = emo1'.*2); last by rewrite emo_insert_e_2.
- iFrame "∗". iSplitL; last iSplitL; first by eauto with iFrame.
+ iFrame "∗". iSplitL.
{ (* SeenMsgsAll γh s E1' esi1 emo1' ti *)
iNext. iIntros (e eidx eV EV EMO_LOOKUP).
case (decide (eidx = emo_e (S gen') (length es))) as [->|NEeidx].
diff --git a/gpfsl/base_logic/frame_instances.v b/gpfsl/base_logic/frame_instances.v
index 0a633d2f..ef7bf57f 100644
--- a/gpfsl/base_logic/frame_instances.v
+++ b/gpfsl/base_logic/frame_instances.v
@@ -102,10 +102,11 @@ Proof.
Qed.
#[global] Instance frame_view_at_view_mono p R P Q V1 V2 :
- IsBiIndexRel V1 V2 →
+ TCNoBackTrack (IsBiIndexRel V1 V2) →
+ (* [IsBiIndexRel] can loop if V2 is an evar, due to the [lat_meet_glb] hint *)
Frame p R P Q → Frame p (@{V1} R) (@{V2} P) (@{V2} Q).
Proof.
- rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => -> H.
+ rewrite /Frame /IsBiIndexRel -view_at_intuitionistically_if => [[->]] H.
rewrite -view_at_sep.
by apply bi.wand_entails, view_at_wand_2, view_at_at, bi.entails_wand.
Qed.
diff --git a/gpfsl/logic/atomic_ops.v b/gpfsl/logic/atomic_ops.v
index 1915b7b5..da165976 100644
--- a/gpfsl/logic/atomic_ops.v
+++ b/gpfsl/logic/atomic_ops.v
@@ -591,8 +591,7 @@ Proof.
iApply (AtomicSeen_write _ _ _ _ _ q tx' with "[$SS $Pts SE $sV $HV]");
[done..|].
iIntros "!>" (t' V' V'') "(F & sV'' & SN' & SE & SY & Pts)".
- iApply ("Post" $! t' V' V''). iFrame.
- iExists tx'. iFrame "SE". iPureIntro.
+ iApply ("Post" $! t' V' V''). iFrame. iPureIntro.
case (decide (tx' = t')) => [->|?].
- rewrite lookup_insert. by eexists.
- by rewrite lookup_insert_ne.
@@ -1519,7 +1518,7 @@ Proof.
iApply (AtomicSeen_CAS with "[$S $P $sV $HRel Pr]"); [done..|].
iIntros "!>" (b t' v' Vr V'' ζ'' ζn) "(F & sV'' & S' & P & Pr & CASE)".
iApply "Post". iFrame.
- rewrite AtomicPtsTo_CON_CAS. iFrame. iExists _. by iFrame.
+ rewrite AtomicPtsTo_CON_CAS. iFrame. done.
Qed.
Lemma AtomicSeen_CON_CAS_int
diff --git a/gpfsl/logic/atomic_ops_vj.v b/gpfsl/logic/atomic_ops_vj.v
index ebb0c5a4..ec128f47 100644
--- a/gpfsl/logic/atomic_ops_vj.v
+++ b/gpfsl/logic/atomic_ops_vj.v
@@ -208,8 +208,7 @@ Proof.
iApply (AtomicSeen_write_vj _ _ _ _ _ q tx' with "[$SS $Pts SE $sV $HV]");
[done..|].
iIntros "!>" (t' V' V'') "(F & sV'' & SN' & SE & SY & Pts)".
- iApply ("Post" $! t' V' V''). iFrame.
- iExists tx'. iFrame "SE". iPureIntro.
+ iApply ("Post" $! t' V' V''). iFrame. iPureIntro.
case (decide (tx' = t')) => [->|?].
- rewrite lookup_insert. by eexists.
- by rewrite lookup_insert_ne.
diff --git a/gpfsl/logic/atomic_preds.v b/gpfsl/logic/atomic_preds.v
index 638f1b4d..d33d36fd 100644
--- a/gpfsl/logic/atomic_preds.v
+++ b/gpfsl/logic/atomic_preds.v
@@ -1278,7 +1278,7 @@ Proof.
intros C GH VAL.
iIntros "(? & sVm & ? & ? & NAL & HC & AR & AW & NA)".
iExists t, m. iFrame (VAL) "sVm".
- iExists rsa, rsn, ws. iFrame (GH) "∗". iSplitR "NAL"; last by eauto.
+ iExists rsa, rsn, ws. iFrame (GH) "∗".
iStopProof. constructor => V. iPureIntro. intros ?.
exists t, m. split; last split; [by rewrite lookup_singleton|by inversion VAL|done].
Qed.
@@ -1404,7 +1404,7 @@ Proof.
* apply map_non_empty_singleton.
* exists {[t := m]}. split; [done|].
move => ?? /lookup_singleton_Some [? <-]. by inversion VAL.
- + iExists t. iFrame. iPureIntro. rewrite Eqζ. split.
+ + iPureIntro. rewrite Eqζ. split.
* rewrite lookup_insert. by eexists.
* move => t1 [VV1 /lookup_singleton_Some [<-//]].
- iExists {[t := m]}, Va, rsa, rsn, ws. iFrame "SA". iFrame "#∗".
diff --git a/gpfsl/logic/readonly_ptsto.v b/gpfsl/logic/readonly_ptsto.v
index af767f91..007c9221 100644
--- a/gpfsl/logic/readonly_ptsto.v
+++ b/gpfsl/logic/readonly_ptsto.v
@@ -260,8 +260,7 @@ Proof.
iSplitL; last first. { by iApply (monPred_in_mono with "sV'"). }
iDestruct (view_at_elim with "sV' AWL") as "AWL".
iExists rsa, rns, ws. iFrame (GH) "∗".
- iDestruct (seen_time_AllocLocal_singleton with "st") as "$"; [by inversion Eqv'|].
- eauto.
+ iDestruct (seen_time_AllocLocal_singleton with "st") as "$". by inversion Eqv'.
Qed.
End ops_rules.
--
GitLab