From 90cc90c2eb1c6ac7a8fde15dc83e8fb0ef6038bb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Dec 2020 19:58:10 +0100
Subject: [PATCH] Bump Iris (persistent mapsto).
---
opam | 2 +-
theories/examples/stack/refinement.v | 93 +++++++------------
theories/examples/symbol.v | 8 +-
theories/examples/various.v | 4 +-
theories/experimental/helping/helping_stack.v | 51 +++-------
theories/logic/proofmode/tactics.v | 35 ++++---
6 files changed, 74 insertions(+), 119 deletions(-)
diff --git a/opam b/opam
index ed7c7f7..7228577 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
- "coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2020-12-18.1.afe51813") | (= "dev") }
"coq-autosubst" { = "dev" }
]
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index abefef6..f0dd49e 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -8,24 +8,10 @@ Definition stackN := nroot.@"stack".
Section proof.
Context `{relocG Σ}.
- (** The "partial pointsto" proposition is duplicable *)
- Local Instance istk_fromand (istk : loc) (w : val) :
- FromSep (∃ q, istk ↦{q} w) (∃ q, istk ↦{q} w) (∃ q, istk ↦{q} w).
- Proof.
- rewrite /FromSep. iIntros "[$ _]".
- Qed.
- Local Instance istk_intoand (istk : loc) (w : val) :
- IntoSep (∃ q, istk ↦{q} w) (∃ q, istk ↦{q} w) (∃ q, istk ↦{q} w).
- Proof.
- rewrite /IntoSep /=. iDestruct 1 as (q) "[H1 H2]".
- iSplitL "H1"; eauto with iFrame.
- Qed.
-
Fixpoint stack_contents (v1 : loc) (ls : list val) :=
match ls with
- | [] => ∃ q, v1 ↦{q} NONEV
- | h::tl => ∃ (z1 : loc) q, v1 ↦{q} SOMEV (h, #z1) ∗
- stack_contents z1 tl
+ | [] => v1 ↦□ NONEV
+ | h::tl => ∃ (z1 : loc), v1 ↦□ SOMEV (h, #z1) ∗ stack_contents z1 tl
end%I.
Definition stack_link (A : lrel Σ) (v1 : loc) (v2 : val) :=
@@ -33,34 +19,26 @@ Section proof.
stack_contents v1 ls1 ∗ is_stack v2 ls2 ∗
[∗ list] v1;v2 ∈ ls1;ls2, A v1 v2)%I.
- (** Actually, the whole `stack_contents` predicate is duplicable *)
- Local Instance stack_contents_intoand (istk : loc) (ls : list val) :
- IntoSep (stack_contents istk ls) (stack_contents istk ls) (stack_contents istk ls).
- Proof.
- rewrite /IntoSep /=.
- revert istk. induction ls as [|h ls]; intros istk; simpl.
- - apply istk_intoand.
- - iDestruct 1 as (z1 q) "[Histk Hc]".
- rewrite IHls. iDestruct "Hc" as "[Hc1 Hc2]". iDestruct "Histk" as "[Histk1 Histk2]".
- iSplitL "Hc1 Histk1"; iExists _, (q/2)%Qp; by iFrame.
- Qed.
+ Global Instance stack_contents_persistent v1 ls :
+ Persistent (stack_contents v1 ls).
+ Proof. revert v1. induction ls; apply _. Qed.
Lemma stack_contents_agree istk ls ls' :
stack_contents istk ls -∗ stack_contents istk ls' -∗ ⌜ls = ls'âŒ.
Proof.
revert istk ls'. induction ls as [|h ls]; intros istk ls'; simpl.
- - iDestruct 1 as (q) "Histk".
+ - iIntros "#Histk".
destruct ls' as [|h' ls']; first by eauto.
- simpl. iDestruct 1 as (z q') "[Histk' _]".
- iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo.
+ simpl. iDestruct 1 as (z) "[Histk' _]".
+ iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo.
exfalso. naive_solver.
- - iDestruct 1 as (z q) "[Histk Hls]".
+ - iDestruct 1 as (z) "[Histk Hls]".
destruct ls' as [|h' ls']; simpl.
- + iDestruct 1 as (q') "Histk'".
- iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo.
+ + iIntros "Histk'".
+ iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo.
exfalso. naive_solver.
- + iDestruct 1 as (z' q') "[Histk' Hls']".
- iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
+ + iDestruct 1 as (z') "[Histk' Hls']".
+ iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo; simplify_eq/=.
iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
eauto.
Qed.
@@ -68,11 +46,6 @@ Section proof.
Definition sinv (A : lrel Σ) stk stk' : iProp Σ :=
(∃ (istk : loc), stk ↦ #istk ∗ stack_link A istk stk')%I.
- Ltac close_sinv Hcl asn :=
- iMod (Hcl with asn) as "_";
- [iNext; rewrite /sinv; iExists _;
- (by iFrame || iFrame; iExists _,_; by eauto with iFrame) |]; try iModIntro.
-
Lemma FG_CG_push_refinement N st st' (A : lrel Σ) (v v' : val) :
N ## relocN →
inv N (sinv A st st') -∗
@@ -88,7 +61,8 @@ Section proof.
iInv N as (isk) "(>Hstk & Hlnk)" "Hclose".
iExists _. iFrame.
iModIntro. iNext. iIntros "Hstk".
- close_sinv "Hclose" "[Hlnk Hstk]".
+ iMod ("Hclose" with "[Hlnk Hstk]") as "_".
+ { iExists _. by iFrame. }
rel_pures_l.
rel_alloc_l nstk as "Hnstk".
rel_cmpxchg_l_atomic.
@@ -97,17 +71,19 @@ Section proof.
iModIntro. iSplit.
- (* CmpXchg fails *)
iIntros (?); iNext; iIntros "Hstk".
- close_sinv "Hclose" "[Hlnk Hstk]".
+ iMod ("Hclose" with "[Hlnk Hstk]") as "_".
+ { iExists _. iFrame. }
rel_pures_l. rel_rec_l. by iApply "IH".
- (* CmpXchg succeeds *)
iIntros (?). simplify_eq/=. iNext. iIntros "Hstk".
+ iMod (mapsto_persist with "Hnstk") as "Hnstk".
rewrite /stack_link. iDestruct "Hlnk" as (ls1 ls2) "(Hls1 & Hls2 & #HA)".
rel_apply_r (refines_CG_push_r with "Hls2").
iIntros "Hls2".
iMod ("Hclose" with "[-]").
{ iNext. rewrite {2}/sinv. iExists _. iFrame.
iExists (v::ls1),_. simpl. iFrame "Hls2 Hvv HA".
- iExists _,_. iFrame. }
+ iExists _. iFrame. }
rel_pures_l. rel_values.
Qed.
@@ -125,38 +101,40 @@ Section proof.
iExists _. iFrame "Hstk".
iModIntro. iNext. iIntros "Hstk /=".
rel_pures_l. rel_rec_l.
- iDestruct "Hlnk" as (ls1 ls2) "(Hls1 & Hls2 & #HA)".
- iDestruct "Hls1" as "[Histk1 Histk2]".
- destruct ls1 as [|h1 ls1]; iSimpl in "Histk1".
+ iDestruct "Hlnk" as (ls1 ls2) "(#Hls1 & Hls2 & #HA)".
+ destruct ls1 as [|h1 ls1]; iSimpl in "Hls1".
- iDestruct (big_sepL2_length with "HA") as %Hfoo.
assert (ls2 = []) as -> by (apply length_zero_iff_nil; done). clear Hfoo.
rel_apply_r (refines_CG_pop_fail_r with "Hls2").
- iIntros "Hls2".
- close_sinv "Hclose" "[Histk2 Hstk Hls2]".
- iDestruct "Histk1" as (q) "Histk'". rel_load_l.
+ iIntros "Hls2". simpl in *.
+ iMod ("Hclose" with "[Hstk Hls2]") as "_".
+ { iExists _. iFrame. iExists [], []. iFrame; auto. }
+ rel_load_l.
rel_pures_l. rel_values.
iModIntro. iExists _,_. eauto.
- - iDestruct "Histk1" as (z1 q) "[Histk1 Hrest]".
- close_sinv "Hclose" "[Histk2 Hstk Hls2]".
+ - iDestruct "Hls1" as (z1) "[Hls1 Hrest]".
+ iMod ("Hclose" with "[Hstk Hls2]") as "_".
+ { iExists _. iFrame. iExists (h1 :: ls1), _. simpl. auto. }
rel_load_l. rel_pures_l.
rel_cmpxchg_l_atomic.
iInv N as (istk') "(>Hstk & Hlnk)" "Hclose".
iModIntro. iExists _. iFrame "Hstk". iSplit.
+ iIntros (?). iNext. iIntros "Hstk".
- close_sinv "Hclose" "[Hstk Hlnk]".
+ iMod ("Hclose" with "[Hstk Hlnk]") as "_".
+ { iExists _. iFrame. }
rel_pures_l. iApply "IH".
+ iIntros (?). simplify_eq/=. iNext.
iIntros "Hstk". rel_pures_l.
iDestruct "Hlnk" as (ls1' ls2') "(Hc2 & Hst & #HA')".
- iDestruct "Hrest" as "[Hrest Hz1]".
- iAssert (stack_contents istk (h1::ls1)) with "[Histk1 Hrest]" as "Histk1".
- { simpl. iExists _,_. by iFrame. }
- iDestruct (stack_contents_agree with "Histk1 Hc2") as %<-.
+ iAssert (stack_contents istk (h1::ls1)) with "[Hls1]" as "{Hls1} Hls1".
+ { simpl. iExists _. auto. }
+ iDestruct (stack_contents_agree with "Hls1 Hc2") as %<-.
iClear "HA".
rewrite big_sepL2_cons_inv_l. iDestruct "HA'" as (h2 l2' ->) "[Hh HA]".
rel_apply_r (refines_CG_pop_suc_r with "Hst").
iIntros "Hst".
- close_sinv "Hclose" "[-]".
+ iMod ("Hclose" with "[-]") as "_".
+ { iExists _. iFrame. iExists _, _; auto. }
rel_values. iModIntro. iExists _,_; eauto.
Qed.
@@ -179,6 +157,7 @@ Section proof.
rel_alloc_r st' as "Hst'". rel_pures_r.
rel_apply_r refines_newlock_r. iIntros (l) "Hl". rel_pures_r.
rel_values.
+ iMod (mapsto_persist with "Hisk") as "#Hisk".
iMod (inv_alloc (stackN.@(st,(#st', l)%V)) _ (sinv A st (#st', l)%V) with "[-]")
as "#Hinv".
{ iNext. iExists _. iFrame. iExists [],[]. simpl.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 444c7fb..a05b387 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -104,13 +104,13 @@ Section rules.
Definition table_inv (size1 size2 tbl1 tbl2 : loc) : iProp Σ :=
(∃ (n : nat) (ls : val), own γ (◠(MaxNat n))
- ∗ size1 ↦{1/2} #n ∗ size2 ↦ₛ{1/2} #n
- ∗ tbl1 ↦{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
+ ∗ size1 ↦{#1/2} #n ∗ size2 ↦ₛ{1/2} #n
+ ∗ tbl1 ↦{#1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
∗ lrel_list lrel_int ls ls)%I.
Definition lok_inv (size1 size2 tbl1 tbl2 : loc) (l : val) : iProp Σ :=
- (∃ (n : nat) (ls : val), size1 ↦{1/2} #n ∗ size2 ↦ₛ{1/2} #n
- ∗ tbl1 ↦{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
+ (∃ (n : nat) (ls : val), size1 ↦{#1/2} #n ∗ size2 ↦ₛ{1/2} #n
+ ∗ tbl1 ↦{#1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
∗ is_locked_r l false)%I.
End rules.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index afae675..0ba4470 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -158,8 +158,8 @@ Section proofs.
(** A "callback with lock" example *)
Definition i3 (x x' b b' : loc) : iProp Σ :=
- (∃ (n:nat), x ↦{1/2} #n ∗ x' ↦ₛ{1/2} #n ∗
- ((b ↦ #true ∗ b' ↦ₛ #true ∗ x ↦{1/2} #n ∗ x' ↦ₛ{1/2} #n)
+ (∃ (n:nat), x ↦{#1/2} #n ∗ x' ↦ₛ{1/2} #n ∗
+ ((b ↦ #true ∗ b' ↦ₛ #true ∗ x ↦{#1/2} #n ∗ x' ↦ₛ{1/2} #n)
∨ (b ↦ #false ∗ b' ↦ₛ #false)))%I.
Definition i3n := nroot .@ "i3".
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index fa5138f..fb81cb0 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -273,20 +273,6 @@ Section refinement.
rewrite refines_eq. by iApply "Hcont".
Qed.
- (** We will also use the following instances for splitting and
- compining read-only pointsto permissions. *)
- Local Instance ro_pointsto_fromand (l : loc) (w : val) :
- FromSep (∃ q, l ↦{q} w) (∃ q, l ↦{q} w) (∃ q, l ↦{q} w).
- Proof.
- rewrite /FromSep. iIntros "[$ _]".
- Qed.
- Local Instance ro_pointsto_intoand (l : loc) (w : val) :
- IntoSep (∃ q, l ↦{q} w) (∃ q, l ↦{q} w) (∃ q, l ↦{q} w).
- Proof.
- rewrite /IntoSep /=. iDestruct 1 as (q) "[H1 H2]".
- iSplitL "H1"; eauto with iFrame.
- Qed.
-
(** Then we have definitions and lemmas that we use for actually
liking the contents of the two stacks together *)
Definition olocO := leibnizO (option loc).
@@ -304,23 +290,13 @@ Section refinement.
match ol,ls with
| None,[] => True
| Some l,(h::t) =>
- ∃ (ol : option loc),
- ∃ q, l ↦{q} (h, oloc_to_val ol) ∗ stack_contents ol t
+ ∃ (ol : option loc), l ↦□ (h, oloc_to_val ol) ∗ stack_contents ol t
| _,_ => False
end%I.
- Existing Instance istk_fromand.
- Existing Instance istk_intoand.
- Local Instance stack_contents_intoand (istk : option loc) (ls : list val) :
- IntoSep (stack_contents istk ls) (stack_contents istk ls) (stack_contents istk ls).
- Proof.
- rewrite /IntoSep /=.
- revert istk. induction ls as [|h ls]; intros istk; simpl.
- - destruct istk; eauto.
- - destruct istk; last by eauto. iDestruct 1 as (z1 q) "[Histk Hc]".
- rewrite IHls. iDestruct "Hc" as "[Hc1 Hc2]". iDestruct "Histk" as "[Histk1 Histk2]".
- iSplitL "Hc1 Histk1"; iExists _, (q/2)%Qp; by iFrame.
- Qed.
+ Global Instance stack_contents_persistent ol ls :
+ Persistent (stack_contents ol ls).
+ Proof. revert ol. induction ls; apply _. Qed.
Lemma stack_contents_agree istk ls ls' :
stack_contents istk ls -∗ stack_contents istk ls' -∗ ⌜ls = ls'âŒ.
@@ -329,10 +305,10 @@ Section refinement.
- destruct istk; eauto.
destruct ls' as [|h' ls']; simpl; eauto.
- destruct istk; last eauto.
- iDestruct 1 as (z q) "[Histk Hls]".
+ iDestruct 1 as (z) "[Histk Hls]".
destruct ls' as [|h' ls']; simpl; eauto.
- iDestruct 1 as (z' q') "[Histk' Hls']".
- iDestruct (gen_heap.mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
+ iDestruct 1 as (z') "[Histk' Hls']".
+ iDestruct (mapsto_agree with "Histk' Histk") as %Hfoo. simplify_eq/=.
iDestruct (IHls with "Hls Hls'") as %Hbar. simplify_eq/=.
eauto.
Qed.
@@ -366,7 +342,7 @@ Section refinement.
Proof.
iIntros "#Hinv IH". rel_rec_l. rel_pures_l.
rel_load_l_atomic.
- iInv stackN as (ol N ls1 ls2) "(Hol & Hst1 & Hst2 & HA & Hmb & Hown & HN)" "Hcl".
+ iInv stackN as (ol N ls1 ls2) "(Hol & #Hst1 & Hst2 & HA & Hmb & Hown & HN)" "Hcl".
iModIntro. iExists _; iFrame. iNext. iIntros "Hol".
destruct ls1 as [|h1 ls1].
- iSimpl in "Hst1".
@@ -379,13 +355,13 @@ Section refinement.
{ iNext. iExists None,_,[],_. simpl; iFrame.
by rewrite big_sepL2_nil. }
rel_values. iExists _,_. eauto with iFrame.
- - iDestruct "Hst1" as "[Hst1 Hst1']".
- iSimpl in "Hst1". destruct ol as [l|]; last by eauto with iFrame.
- iDestruct "Hst1" as (ol q) "[[Hl Hl'] [Hol' Hol2]]".
- rel_pures_l. iMod ("Hcl" with "[-Hl IH Hst1' Hol2]") as "_".
+ - destruct ol as [l|]; last by eauto with iFrame.
+ iPoseProof "Hst1" as "Hst1'". iSimpl in "Hst1".
+ iDestruct "Hst1" as (ol) "[Hl Hol']".
+ rel_pures_l. iMod ("Hcl" with "[-IH]") as "_".
{ iNext. iExists (Some l),_,(h1::ls1),_. iFrame.
simpl. eauto with iFrame. }
- rel_load_l. rel_pures_l. iClear "Hl".
+ rel_load_l. rel_pures_l.
rel_cmpxchg_l_atomic.
iInv stackN as (ol2 N' ls1' ls2') "(Hol & Hst1 & Hst2 & HA & Hmb & Hown & HN)" "Hcl".
iModIntro. iExists _. iFrame "Hol". iSplit.
@@ -561,6 +537,7 @@ Section refinement.
iIntros "Hol".
rel_apply_r (refines_CG_push_r with "Hst2").
iIntros "Hst2".
+ iMod (mapsto_persist with "Hnew") as "#Hnew".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (Some new),_,(h1::ls1'),_; iFrame.
simpl. by eauto with iFrame. }
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index f0c6357..95661a1 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -212,38 +212,37 @@ Ltac rel_pures_r :=
(** Load *)
-Lemma tac_rel_load_l_simp `{!relocG Σ} K ℶ1 ℶ2 i1 (l : loc) q v e t eres A :
+Lemma tac_rel_load_l_simp `{!relocG Σ} K ℶ1 ℶ2 i1 p (l : loc) q v e t eres A :
e = fill K (Load (# l)) →
MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
- envs_lookup i1 ℶ2 = Some (false, l ↦{q} v)%I →
+ envs_lookup i1 ℶ2 = Some (p, l ↦{q} v)%I →
eres = fill K (of_val v) →
envs_entails ℶ2 (refines ⊤ eres t A) →
envs_entails ℶ1 (refines ⊤ e t A).
Proof.
- rewrite envs_entails_eq. intros ???? Hℶ2; subst.
- rewrite into_laterN_env_sound envs_lookup_split // /=.
- rewrite bi.later_sep. rewrite Hℶ2.
- apply: bi.wand_elim_l' =>/=.
- rewrite -(refines_load_l K ⊤ l q).
- rewrite -fupd_intro.
- rewrite -(bi.exist_intro v).
- by apply bi.wand_intro_r.
+ rewrite envs_entails_eq. iIntros (-> ?? -> Hℶ2) "Henvs".
+ iDestruct (into_laterN_env_sound with "Henvs") as "Henvs".
+ iDestruct (envs_lookup_split with "Henvs") as "[Hl Henvs]"; first done.
+ rewrite Hℶ2. iApply (refines_load_l K ⊤ l q). iModIntro. iExists v.
+ destruct p; simpl; [|by iFrame].
+ iDestruct "Hl" as "#Hl". iSplitR; [by auto|].
+ iIntros "!> _". by iApply "Henvs".
Qed.
-Lemma tac_rel_load_r `{!relocG Σ} K ℶ1 E i1 (l : loc) q e t tres A v :
+Lemma tac_rel_load_r `{!relocG Σ} K ℶ1 E i1 p (l : loc) q e t tres A v :
t = fill K (Load (# l)) →
nclose specN ⊆ E →
- envs_lookup i1 ℶ1 = Some (false, l ↦ₛ{q} v)%I →
+ envs_lookup i1 ℶ1 = Some (p, l ↦ₛ{q} v)%I →
tres = fill K (of_val v) →
envs_entails ℶ1 (refines E e tres A) →
envs_entails ℶ1 (refines E e t A).
Proof.
- rewrite envs_entails_eq. intros ???? Hg.
- subst t tres.
- rewrite (envs_lookup_split ℶ1) //; simpl.
- rewrite {1}(refines_load_r E); [ | eassumption ].
- rewrite Hg.
- apply bi.wand_elim_l.
+ rewrite envs_entails_eq. iIntros (-> ?? -> Hg) "Henvs".
+ iDestruct (envs_lookup_split with "Henvs") as "[Hl Henvs]"; first done.
+ rewrite Hg. destruct p; simpl.
+ - iDestruct "Hl" as "#Hl". iApply (refines_load_r with "Hl"); first done.
+ iIntros "_". by iApply "Henvs".
+ - by iApply (refines_load_r with "Hl").
Qed.
Tactic Notation "rel_load_l" :=
--
GitLab