From 3bf018b7ba599d997954223df8fae04dab9f0f73 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 13 Nov 2023 12:04:19 +0100
Subject: [PATCH] =?UTF-8?q?Patch=20now=20that=20iFrame=20=E2=88=83=20looks?=
=?UTF-8?q?=20beneath=20definitions?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
gpfsl-examples/exchanger/proof_graph_resource.v | 2 +-
gpfsl-examples/queue/proof_mp2_graph.v | 8 ++++----
gpfsl-examples/queue/proof_ms_abs_graph.v | 2 +-
gpfsl-examples/queue/proof_spsc_graph.v | 4 ++--
gpfsl-examples/stack/proof_mp_client_graph.v | 2 +-
gpfsl-examples/stack/proof_mp_client_history.v | 2 +-
gpfsl-examples/stack/proof_treiber_graph.v | 2 +-
gpfsl/gps/model_rules_init.v | 4 ++--
gpfsl/logic/atomic_preds.v | 2 +-
9 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/gpfsl-examples/exchanger/proof_graph_resource.v b/gpfsl-examples/exchanger/proof_graph_resource.v
index 6eec8094..67fad133 100644
--- a/gpfsl-examples/exchanger/proof_graph_resource.v
+++ b/gpfsl-examples/exchanger/proof_graph_resource.v
@@ -127,7 +127,7 @@ Proof.
{ iNext. iExists ∅. iFrame. by rewrite /TradeResources big_sepL_nil. }
iMod ("EL" $! _ (EI γb γg P) N) as "EL".
iIntros "!>". iApply ("Post" $! γg).
- iSplitR "I2"; iFrame. iExists _; iFrame.
+ iSplitR "I2"; iFrame.
Qed.
Lemma exchanger_resource_spec_derived :
diff --git a/gpfsl-examples/queue/proof_mp2_graph.v b/gpfsl-examples/queue/proof_mp2_graph.v
index b68f5c2c..cabb223a 100644
--- a/gpfsl-examples/queue/proof_mp2_graph.v
+++ b/gpfsl-examples/queue/proof_mp2_graph.v
@@ -112,7 +112,7 @@ Proof using All.
awp_apply (enqueue_spec with "⊒V QL"); [solve_ndisj|done|].
iInv mpN as (G1) "(FI & QI & >â—m & >â—¯m & >%Hv)".
iAaccIntro with "QI".
- { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+ { iFrame. iIntros "QI !> !>". iFrame. done. }
iIntros (V1 G1' enqId1 enq1 Venq1 M1') "(QI & #⊒V1 & #QL1 & %F) !>".
set (eV1 := mkGraphEvent enq1 Venq1 M1') in *.
rewrite /is_enqueue in F.
@@ -134,7 +134,7 @@ Proof using All.
iDestruct (graph_master_snap_included with "Gm Gs") as %SubG1'2.
iSpecialize ("QI" with "[$Gm]").
iAaccIntro with "QI".
- { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+ { iFrame. iIntros "QI !> !>". iFrame. done. }
iIntros (V2 G2' enqId2 enq2 Venq2 M2') "(QI & #⊒V2 & #QL2 & %F) !>".
set (eV2 := mkGraphEvent enq2 Venq2 M2') in *.
rewrite /is_enqueue in F.
@@ -184,7 +184,7 @@ Proof using All.
iInv mpN as (G) "(FI & QI & >â—m & >â—¯m & >%Hv)".
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC".
iAaccIntro with "QI".
- { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. }
+ { iFrame. iIntros "QI !> !>". iFrame. done. }
iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F) !>".
iSplitL; last by iIntros. iNext. iExists G'.
set (dV := mkGraphEvent deq Vdeq M') in *.
@@ -289,7 +289,7 @@ Proof using All.
iAaccIntro with "QI".
{ iDestruct "â—¯m" as "[â—¯m $]". iFrame. iIntros "QI !> !>".
- iExists _. iFrame. done. }
+ iFrame. done. }
iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F)".
set (dV := mkGraphEvent deq Vdeq M') in *.
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 2141fac9..46ae2bed 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1003,7 +1003,7 @@ Proof.
rewrite /Link. iDestruct 1 as (t0 V0 ζ) "[AT LR]".
iDestruct "LR" as (V e v) "(#F1 & #F2 & #SE & LV & NA)".
iSplitR "NA".
- - iExists t0, V0, ζ. iFrame. iExists V, e, v. by iFrame "#∗".
+ - iExists t0, V0, ζ. iFrame. iExists e, v. by iFrame "#∗".
- rewrite /seen_enqueued_val /SeenEvent.
iDestruct "SE" as (eV (Eqv & <- & SE) EqE) "SE". iDestruct "F2" as %EqT.
iExists e, eV, v. iSplit; [done|]. by iFrame "NA".
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index ddbfbc1a..5541b28c 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -180,7 +180,7 @@ Proof.
iSpecialize ("QI" with "[$Gm]").
iAaccIntro with "QI".
- { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+ { iFrame. iIntros "QI !>". iSplitL "QI"; [|by auto].
iNext. iExists _. iFrame. done. }
iIntros (V' G' enqId enq Venq M') "(QI & #⊒V' & #QL' & %F)".
iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC'".
@@ -255,7 +255,7 @@ Proof.
move=> /NoDup_app [?][_] /NoDup_app [?][_]? //. }
iAaccIntro with "QI".
- { iFrame. iIntros "QI !>". iSplitL "QI â—ed"; [|by auto].
+ { iFrame. iIntros "QI !>". iSplitL "QI"; [|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 *.
diff --git a/gpfsl-examples/stack/proof_mp_client_graph.v b/gpfsl-examples/stack/proof_mp_client_graph.v
index f1451e82..241d041a 100644
--- a/gpfsl-examples/stack/proof_mp_client_graph.v
+++ b/gpfsl-examples/stack/proof_mp_client_graph.v
@@ -139,7 +139,7 @@ Section Stack.
iDestruct (graph_master_consistent with "Gm") as %EGC.
iSpecialize ("SI" with "[$Gm]").
iAaccIntro with "SI".
- { iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists G. iFrame. }
+ { iIntros "SI !>". iFrame. }
iIntros (v V' G' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
iDestruct "F" as %((SubG' & SubM' & Sub' & Sub'') & CASE).
diff --git a/gpfsl-examples/stack/proof_mp_client_history.v b/gpfsl-examples/stack/proof_mp_client_history.v
index 99ae7626..79c31967 100644
--- a/gpfsl-examples/stack/proof_mp_client_history.v
+++ b/gpfsl-examples/stack/proof_mp_client_history.v
@@ -137,7 +137,7 @@ Section Stack.
iDestruct (history_master_wf with "Em") as %EWF.
iSpecialize ("SI" with "[$Em]").
iAaccIntro with "SI".
- { iIntros "SI !>". iFrame. iNext. rewrite /StackInv1. iExists E. iFrame. }
+ { iIntros "SI !>". iFrame. }
iIntros (v V' E' pushId popId push1 pop Vpush M') "(SI' & sV' & Local & F)".
iDestruct "F" as %((? & ?) & CASE).
diff --git a/gpfsl-examples/stack/proof_treiber_graph.v b/gpfsl-examples/stack/proof_treiber_graph.v
index 314a1cbf..97a6c290 100644
--- a/gpfsl-examples/stack/proof_treiber_graph.v
+++ b/gpfsl-examples/stack/proof_treiber_graph.v
@@ -777,7 +777,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 (γ T SC) "[? ?]". iExists _. iFrame.
- iIntros "G". iExists γ, T. by iFrame.
+ iIntros "G". by iFrame.
Qed.
Lemma StackInv_graph_snap_instance :
diff --git a/gpfsl/gps/model_rules_init.v b/gpfsl/gps/model_rules_init.v
index 4fd727fb..0b90f956 100644
--- a/gpfsl/gps/model_rules_init.v
+++ b/gpfsl/gps/model_rules_init.v
@@ -203,11 +203,11 @@ Section RawRules.
* by apply SWConnect_singleton. }
iIntros "!>". rewrite -Eqχ. iFrame "oS". destruct bs.
- iSplitR "W".
- + iExists μ, γs, γl, ζ, t. iSplit; [done|]. iNext. by iFrame.
+ + iExists μ, ζ, t. iNext. by iFrame.
+ iExists _. by iFrame.
- iDestruct (AtomicPtsToX_SW_to_CON_2 with "Pts W") as "[Pts SY]".
iSplitR "SY".
- + iExists μ, γs, γl, ζ, t. iSplit; [done|].
+ + iExists μ, ζ, t.
iNext. iFrame. iPureIntro. do 2 (split; [done|]).
by move => ? [?/lookup_singleton_Some [->]].
+ iExists _. by iFrame.
diff --git a/gpfsl/logic/atomic_preds.v b/gpfsl/logic/atomic_preds.v
index d33d36fd..fa36735d 100644
--- a/gpfsl/logic/atomic_preds.v
+++ b/gpfsl/logic/atomic_preds.v
@@ -1477,7 +1477,7 @@ Proof.
iIntros "P NA". rewrite AtomicPtsTo_eq.
iMod (AtomicPtsToX_from_na_cofinite_rel with "P NA")
as (γ t V FR) "(sV & P & W & Pt)".
- iIntros "!>". iExists γ, t, V. iFrame (FR) "∗". by iExists _.
+ iIntros "!>". iExists γ, t, V. iFrame (FR) "∗".
Qed.
Lemma AtomicPtsTo_from_na_cofinite l v (G : gset gname) :
l ↦ v ==∗ ∃ γ t V, ⌜γ ∉ G⌠∗ ⊒V ∗
--
GitLab