Commit b57aac09 authored by Simon Friis Vindum's avatar Simon Friis Vindum Committed by Robbert Krebbers
Browse files

Add persistent points-to predicate

parent 097b7b69
...@@ -32,6 +32,13 @@ Inductive dfrac := ...@@ -32,6 +32,13 @@ Inductive dfrac :=
| DfracDiscarded : dfrac | DfracDiscarded : dfrac
| DfracBoth : Qp dfrac. | DfracBoth : Qp dfrac.
Declare Scope dfrac_scope.
Delimit Scope dfrac_scope with dfrac.
Notation "# q" := (DfracOwn q%Qp) (at level 8, format "# q") : dfrac_scope.
Notation "#□" := (DfracDiscarded) : dfrac_scope.
Notation "□" := (DfracDiscarded) : dfrac_scope.
Section dfrac. Section dfrac.
Canonical Structure dfracO := leibnizO dfrac. Canonical Structure dfracO := leibnizO dfrac.
......
From stdpp Require Export namespaces. From stdpp Require Export namespaces.
From iris.algebra Require Import gmap_view namespace_map agree frac. From iris.algebra Require Import gmap_view namespace_map agree frac.
From iris.algebra Require Export dfrac.
From iris.bi.lib Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own. From iris.base_logic.lib Require Export own.
...@@ -100,8 +101,8 @@ Section definitions. ...@@ -100,8 +101,8 @@ Section definitions.
own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V)))
own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)). own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L gnameO)).
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ := Definition mapsto_def (l : L) (q : dfrac) (v: V) : iProp Σ :=
own (gen_heap_name hG) (gmap_view_frag l (DfracOwn q) (v : leibnizO V)). own (gen_heap_name hG) (gmap_view_frag l q (v : leibnizO V)).
Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed. Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal). Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq). Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
...@@ -122,9 +123,9 @@ Section definitions. ...@@ -122,9 +123,9 @@ Section definitions.
End definitions. End definitions.
Arguments meta {L _ _ V Σ _ A _ _} l N x. Arguments meta {L _ _ V Σ _ A _ _} l N x.
Local Notation "l ↦{ q } v" := (mapsto l q v) Local Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope. Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
Section gen_heap. Section gen_heap.
Context {L V} `{Countable L, !gen_heapG L V Σ}. Context {L V} `{Countable L, !gen_heapG L V Σ}.
...@@ -137,25 +138,27 @@ Section gen_heap. ...@@ -137,25 +138,27 @@ Section gen_heap.
(** General properties of mapsto *) (** General properties of mapsto *)
Global Instance mapsto_timeless l q v : Timeless (l {q} v). Global Instance mapsto_timeless l q v : Timeless (l {q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed. Proof. rewrite mapsto_eq. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I. Global Instance mapsto_fractional l v : Fractional (λ q, l {#q} v)%I.
Proof. Proof.
intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //. intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //.
Qed. Qed.
Global Instance mapsto_as_fractional l q v : Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q. AsFractional (l {#q} v) (λ q, l {#q} v)%I q.
Proof. split; [done|]. apply _. Qed. Proof. split; [done|]. apply _. Qed.
Global Instance mapsto_persistent l v : Persistent (l {#} v).
Proof. rewrite mapsto_eq. apply _. Qed.
Lemma mapsto_valid l q v : l {q} v - q 1%Qp. Lemma mapsto_valid l q v : l {q} v - q%Qp.
Proof. Proof.
rewrite mapsto_eq. iIntros "Hl". rewrite mapsto_eq. iIntros "Hl".
iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done. iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
Qed. Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - (q1 + q2 1)%Qp v1 = v2. Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - (q1 q2) v1 = v2.
Proof. Proof.
rewrite mapsto_eq. iIntros "H1 H2". rewrite mapsto_eq. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L. iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
eauto. auto.
Qed. Qed.
(** Almost all the time, this is all you really need. *) (** Almost all the time, this is all you really need. *)
Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2. Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
...@@ -166,20 +169,27 @@ Section gen_heap. ...@@ -166,20 +169,27 @@ Section gen_heap.
Qed. Qed.
Lemma mapsto_combine l q1 q2 v1 v2 : Lemma mapsto_combine l q1 q2 v1 v2 :
l {q1} v1 - l {q2} v2 - l {q1 + q2} v1 v1 = v2. l {q1} v1 - l {q2} v2 - l {q1 q2} v1 v1 = v2.
Proof. Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->. iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl". eauto with iFrame. iCombine "Hl1 Hl2" as "Hl".
rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_op.
auto.
Qed. Qed.
Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 : Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
¬ (q1 + q2 1)%Qp l1 {q1} v1 - l2 {q2} v2 - l1 l2. ¬ (q1 q2)%Qp l1 {q1} v1 - l2 {q2} v2 - l1 l2.
Proof. Proof.
iIntros (?) "Hl1 Hl2"; iIntros (->). iIntros (?) "Hl1 Hl2"; iIntros (->).
by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??]. by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
Qed. Qed.
Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 v1 - l2 {q2} v2 - l1 l2. Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 v1 - l2 {q2} v2 - l1 l2.
Proof. apply mapsto_frac_ne, Qp_not_add_le_l. Qed. Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
(** Permanently turn a fractional points-to predicate into a persistent
points-to predicate. *)
Lemma mapsto_persist l q v : l {#q} v == l {#} v.
Proof. rewrite mapsto_eq. apply own_update, gmap_view_persist. Qed.
(** General properties of [meta] and [meta_token] *) (** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l N : Timeless (meta_token l N). Global Instance meta_token_timeless l N : Timeless (meta_token l N).
...@@ -273,9 +283,8 @@ Section gen_heap. ...@@ -273,9 +283,8 @@ Section gen_heap.
Lemma gen_heap_valid σ l q v : gen_heap_interp σ - l {q} v - ⌜σ !! l = Some v. Lemma gen_heap_valid σ l q v : gen_heap_interp σ - l {q} v - ⌜σ !! l = Some v.
Proof. Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl". iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_interp mapsto_eq /mapsto_def. rewrite /gen_heap_interp mapsto_eq.
iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L. by iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
iPureIntro. done.
Qed. Qed.
Lemma gen_heap_update σ l v1 v2 : Lemma gen_heap_update σ l v1 v2 :
......
...@@ -20,7 +20,7 @@ using a separate assertion [inv_mapsto_own] for "invariant" locations, we can ...@@ -20,7 +20,7 @@ using a separate assertion [inv_mapsto_own] for "invariant" locations, we can
keep all the other proofs that do not need it conservative. *) keep all the other proofs that do not need it conservative. *)
Definition inv_heapN: namespace := nroot .@ "inv_heap". Definition inv_heapN: namespace := nroot .@ "inv_heap".
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope. Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR Definition inv_heap_mapUR (L V : Type) `{Countable L} : ucmraT := gmapUR L $ prodR
(optionR $ exclR $ leibnizO V) (optionR $ exclR $ leibnizO V)
......
...@@ -14,11 +14,11 @@ From iris.prelude Require Import options. ...@@ -14,11 +14,11 @@ From iris.prelude Require Import options.
(** The [array] connective is a version of [mapsto] that works (** The [array] connective is a version of [mapsto] that works
with lists of values. *) with lists of values. *)
Definition array `{!heapG Σ} (l : loc) (q : Qp) (vs : list val) : iProp Σ := Definition array `{!heapG Σ} (l : loc) (q : dfrac) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) {q} v)%I. ([ list] i v vs, (l + i) {q} v)%I.
Notation "l ↦∗{ q } vs" := (array l q vs) Notation "l ↦∗{ q } vs" := (array l q%dfrac vs)
(at level 20, q at level 50, format "l ↦∗{ q } vs") : bi_scope. (at level 20, q at level 50, format "l ↦∗{ q } vs") : bi_scope.
Notation "l ↦∗ vs" := (array l 1 vs) Notation "l ↦∗ vs" := (array l (DfracOwn 1) vs)
(at level 20, format "l ↦∗ vs") : bi_scope. (at level 20, format "l ↦∗ vs") : bi_scope.
(** We have [FromSep] and [IntoSep] instances to split the fraction (via the (** We have [FromSep] and [IntoSep] instances to split the fraction (via the
...@@ -32,15 +32,14 @@ Implicit Types Φ : val → iProp Σ. ...@@ -32,15 +32,14 @@ Implicit Types Φ : val → iProp Σ.
Implicit Types σ : state. Implicit Types σ : state.
Implicit Types v : val. Implicit Types v : val.
Implicit Types vs : list val. Implicit Types vs : list val.
Implicit Types q : Qp.
Implicit Types l : loc. Implicit Types l : loc.
Implicit Types sz off : nat. Implicit Types sz off : nat.
Global Instance array_timeless l q vs : Timeless (array l q vs) := _. Global Instance array_timeless l q vs : Timeless (array l q vs) := _.
Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{q} vs)%I := _. Global Instance array_fractional l vs : Fractional (λ q, l ↦∗{#q} vs)%I := _.
Global Instance array_as_fractional l q vs : Global Instance array_as_fractional l q vs :
AsFractional (l ↦∗{q} vs) (λ q, l ↦∗{q} vs)%I q. AsFractional (l ↦∗{#q} vs) (λ q, l ↦∗{#q} vs)%I q.
Proof. split; done || apply _. Qed. Proof. split; done || apply _. Qed.
Lemma array_nil l q : l ↦∗{q} [] emp. Lemma array_nil l q : l ↦∗{q} [] emp.
......
...@@ -14,23 +14,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -14,23 +14,23 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
store : val; store : val;
cmpxchg : val; cmpxchg : val;
(* -- predicates -- *) (* -- predicates -- *)
mapsto (l : loc) (q: Qp) (v : val) : iProp Σ; mapsto (l : loc) (q: dfrac) (v : val) : iProp Σ;
(* -- mapsto properties -- *) (* -- mapsto properties -- *)
mapsto_timeless l q v :> Timeless (mapsto l q v); mapsto_timeless l q v :> Timeless (mapsto l q v);
mapsto_fractional l v :> Fractional (λ q, mapsto l q v); mapsto_fractional l v :> Fractional (λ (q : Qp), mapsto l (DfracOwn q) v);
mapsto_as_fractional l q v :> mapsto_as_fractional l q v :>
AsFractional (mapsto l q v) (λ q, mapsto l q v) q; AsFractional (mapsto l (DfracOwn q) v) (λ q, mapsto l (DfracOwn q) v) q;
mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2; mapsto_agree l q1 q2 v1 v2 : mapsto l q1 v1 - mapsto l q2 v2 - v1 = v2;
(* -- operation specs -- *) (* -- operation specs -- *)
alloc_spec (v : val) : alloc_spec (v : val) :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}}; {{{ True }}} alloc v {{{ l, RET #l; mapsto l (DfracOwn 1) v }}};
free_spec (l : loc) (v : val) : free_spec (l : loc) (v : val) :
{{{ mapsto l 1 v }}} free #l {{{ l, RET #l; True }}}; {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
load_spec (l : loc) : load_spec (l : loc) :
<<< (v : val) q, mapsto l q v >>> load #l @ <<< mapsto l q v, RET v >>>; <<< (v : val) q, mapsto l q v >>> load #l @ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (w : val) : store_spec (l : loc) (w : val) :
<<< v, mapsto l 1 v >>> store #l w @ <<< v, mapsto l (DfracOwn 1) v >>> store #l w @
<<< mapsto l 1 w, RET #() >>>; <<< mapsto l (DfracOwn 1) w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1] (* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed] *or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the is outside the atomic triple, which makes it much easier to use -- and the
...@@ -39,17 +39,17 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap { ...@@ -39,17 +39,17 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
[destruct (decide (a = b))] and it will simplify in both places. *) [destruct (decide (a = b))] and it will simplify in both places. *)
cmpxchg_spec (l : loc) (w1 w2 : val) : cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 val_is_unboxed w1
<<< v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ <<< v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v, <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
RET (v, #if decide (v = w1) then true else false) >>>; RET (v, #if decide (v = w1) then true else false) >>>;
}. }.
Arguments atomic_heap _ {_}. Arguments atomic_heap _ {_}.
(** Notation for heap primitives, in a module so you can import it separately. *) (** Notation for heap primitives, in a module so you can import it separately. *)
Module notation. Module notation.
Notation "l ↦{ q } v" := (mapsto l q v) Notation "l ↦{ q } v" := (mapsto l q%dfrac v)
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope. Notation "l ↦ v" := (mapsto l (DfracOwn 1) v) (at level 20) : bi_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I Notation "l ↦{ q } -" := ( v, l {q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } -") : bi_scope.
...@@ -70,8 +70,8 @@ Section derived. ...@@ -70,8 +70,8 @@ Section derived.
Lemma cas_spec (l : loc) (w1 w2 : val) : Lemma cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 val_is_unboxed w1
<<< v, mapsto l 1 v >>> CAS #l w1 w2 @ <<< v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v, <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
RET #if decide (v = w1) then true else false >>>. RET #if decide (v = w1) then true else false >>>.
Proof. Proof.
iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done. iIntros (? Φ) "AU". awp_apply cmpxchg_spec; first done.
......
...@@ -111,8 +111,8 @@ Section increment. ...@@ -111,8 +111,8 @@ Section increment.
(* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto" (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
connective that works on [option Qp] (the type of 1-q). *) connective that works on [option Qp] (the type of 1-q). *)
Lemma weak_incr_spec (l: loc) (v : Z) : Lemma weak_incr_spec (l: loc) (v : Z) :
l {1/2} #v - l {#(1/2)} #v -
<<< (v' : Z), l {1/2} #v' >>> <<< (v' : Z), l {#(1/2)} #v' >>>
weak_incr #l @ weak_incr #l @
<<< v = v' l #(v + 1), RET #v >>>. <<< v = v' l #(v + 1), RET #v >>>.
Proof. Proof.
......
...@@ -28,9 +28,9 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := { ...@@ -28,9 +28,9 @@ Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
(** Since we use an [option val] instance of [gen_heap], we need to overwrite (** Since we use an [option val] instance of [gen_heap], we need to overwrite
the notations. That also helps for scopes and coercions. *) the notations. That also helps for scopes and coercions. *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q (Some v%V)) Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q%dfrac (Some v%V))
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l 1%Qp (Some v%V)) Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
(at level 20) : bi_scope. (at level 20) : bi_scope.
(** Same for [gen_inv_heap], except that these are higher-order notations so to (** Same for [gen_inv_heap], except that these are higher-order notations so to
...@@ -277,10 +277,10 @@ Qed. ...@@ -277,10 +277,10 @@ Qed.
(** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
value type being [option val]. *) value type being [option val]. *)
Lemma mapsto_valid l q v : l {q} v - q 1%Qp. Lemma mapsto_valid l q v : l {q} v - q%Qp.
Proof. apply mapsto_valid. Qed. Proof. apply mapsto_valid. Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : Lemma mapsto_valid_2 l q1 q2 v1 v2 :
l {q1} v1 - l {q2} v2 - (q1 + q2 1)%Qp v1 = v2. l {q1} v1 - l {q2} v2 - (q1 q2) v1 = v2.
Proof. Proof.
iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done. iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
Qed. Qed.
...@@ -288,18 +288,21 @@ Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v ...@@ -288,18 +288,21 @@ Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v
Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed. Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
Lemma mapsto_combine l q1 q2 v1 v2 : Lemma mapsto_combine l q1 q2 v1 v2 :
l {q1} v1 - l {q2} v2 - l {q1 + q2} v1 v1 = v2. l {q1} v1 - l {q2} v2 - l {q1 q2} v1 v1 = v2.
Proof. Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->. iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
iCombine "Hl1 Hl2" as "Hl". eauto with iFrame. by iDestruct "Heq" as %[= ->].
Qed. Qed.
Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 : Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
¬ (q1 + q2 1)%Qp l1 {q1} v1 - l2 {q2} v2 - l1 l2. ¬ (q1 q2)%Qp l1 {q1} v1 - l2 {q2} v2 - l1 l2.
Proof. apply mapsto_frac_ne. Qed. Proof. apply mapsto_frac_ne. Qed.
Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 v1 - l2 {q2} v2 - l1 l2. Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 v1 - l2 {q2} v2 - l1 l2.
Proof. apply mapsto_ne. Qed. Proof. apply mapsto_ne. Qed.
Lemma mapsto_persist l q v : l {#q} v == l {#} v.
Proof. apply mapsto_persist. Qed.
Global Instance inv_mapsto_own_proper l v : Global Instance inv_mapsto_own_proper l v :
Proper (pointwise_relation _ iff ==> ()) (inv_mapsto_own l v). Proper (pointwise_relation _ iff ==> ()) (inv_mapsto_own l v).
Proof. Proof.
...@@ -372,7 +375,7 @@ Proof. ...@@ -372,7 +375,7 @@ Proof.
Qed. Qed.
Lemma heap_array_to_seq_mapsto l v (n : nat) : Lemma heap_array_to_seq_mapsto l v (n : nat) :
([ map] l' ov heap_array l (replicate n v), gen_heap.mapsto l' 1 ov) - ([ map] l' ov heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -
[ list] i seq 0 n, (l + (i : nat)) v. [ list] i seq 0 n, (l + (i : nat)) v.
Proof. Proof.
iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl. iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
...@@ -458,7 +461,7 @@ Lemma wp_load s E l q v : ...@@ -458,7 +461,7 @@ Lemma wp_load s E l q v :
{{{ l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}. {{{ l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
Proof. Proof.
iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ"). iIntros (Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_load with "H"); [auto..|]; iIntros "H HΦ". by iApply "HΦ". iApply (twp_load with "H"). iIntros "H HΦ". by iApply "HΦ".
Qed. Qed.
Lemma twp_store s E l v' v : Lemma twp_store s E l v' v :
......
...@@ -218,7 +218,7 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ : ...@@ -218,7 +218,7 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
(0 < n)%Z (0 < n)%Z
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
( l, ( l,
match envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ' with match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ' with
| Some Δ'' => | Some Δ'' =>
envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }}) envs_entails Δ'' (WP fill K (Val $ LitV $ LitLoc l) @ s; E {{ Φ }})
| None => False | None => False
...@@ -236,7 +236,7 @@ Qed. ...@@ -236,7 +236,7 @@ Qed.
Lemma tac_twp_allocN Δ s E j K v n Φ : Lemma tac_twp_allocN Δ s E j K v n Φ :
(0 < n)%Z (0 < n)%Z
( l, ( l,
match envs_app false (Esnoc Enil j (array l 1 (replicate (Z.to_nat n) v))) Δ with match envs_app false (Esnoc Enil j (array l (DfracOwn 1) (replicate (Z.to_nat n) v))) Δ with
| Some Δ' => | Some Δ' =>
envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }]) envs_entails Δ' (WP fill K (Val $ LitV $ LitLoc l) @ s; E [{ Φ }])
| None => False | None => False
...@@ -314,26 +314,31 @@ Proof. ...@@ -314,26 +314,31 @@ Proof.
apply sep_mono_r, wand_intro_r. rewrite right_id //. apply sep_mono_r, wand_intro_r. rewrite right_id //.
Qed. Qed.
Lemma tac_wp_load Δ Δ' s E i K l q v Φ : Lemma tac_wp_load Δ Δ' s E i K b l q v Φ :
MaybeIntoLaterNEnvs 1 Δ Δ' MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I envs_lookup i Δ' = Some (b, l {q} v)%I
envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}). envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
Proof. Proof.
rewrite envs_entails_eq=> ???. rewrite envs_entails_eq=> ?? Hi.
rewrite -wp_bind. eapply wand_apply; first exact: wp_load. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl. rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono. apply later_mono.
destruct b; simpl.
* iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
* by apply sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_twp_load Δ s E i K l q v Φ : Lemma tac_twp_load Δ s E i K b l q v Φ :
envs_lookup i Δ = Some (false, l {q} v)%I envs_lookup i Δ = Some (b, l {q} v)%I
envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }])
envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]). envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
Proof. Proof.
rewrite envs_entails_eq=> ??. rewrite envs_entails_eq=> ? Hi.
rewrite -twp_bind. eapply wand_apply; first exact: twp_load. rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
rewrite envs_lookup_split //; simpl. rewrite envs_lookup_split //; simpl.