Commit afe51813 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'persistent-points-to-2' into 'master'

Add persistent points-to predicate to Iris

See merge request iris/iris!554
parents 4884e2e9 55a89a20
...@@ -143,6 +143,23 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`. ...@@ -143,6 +143,23 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
initial heap. initial heap.
* Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler * Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler
`mapsto_ne` that does not require reasoning about fractions. `mapsto_ne` that does not require reasoning about fractions.
* Extend the `gen_heap` library with read-only points-to assertions using
[discardable fractions](iris/algebra/dfrac.v).
+ The `mapsto` connective now takes a `dfrac` rather than a `frac` (i.e.,
positive rational number `Qp`).
+ The notation `l ↦{ dq } v` is generalized to discardable fractions
`dq : dfrac`.
+ The new notation `l ↦{# q} v` is used for a concrete fraction `q : frac`
(e.g., to enable writing `l ↦{# 1/2} v`).
+ The new notation `l ↦□ v` is used for the discarded fraction. This
persistent proposition provides read-only access to `l`.
+ The lemma `mapsto_persist : l ↦{dq} v ==∗ l ↦□ v` is used for making the
location `l` read-only.
+ See the changes to HeapLang for an indication on how to adapt your language.
+ See the changes to iris-examples for an indication on how to adapt your
development. In particular, instead of `∃ q, l ↦{q} v` you likely want to
use `l ↦□ v`, which has the advantage of being persistent (rather than just
duplicable).
**Changes in `program_logic`:** **Changes in `program_logic`:**
...@@ -153,6 +170,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`. ...@@ -153,6 +170,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
avoid TC search attempting to apply this instance all the time. avoid TC search attempting to apply this instance all the time.
* Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by * Merge `wp_value_inv`/`wp_value_inv'` into `wp_value_fupd`/`wp_value_fupd'` by
making the lemma bidirectional. making the lemma bidirectional.
* Generalize HeapLang's `mapsto` (`↦`), `array` (`↦∗`), and atomic heap
connectives to discardable fractions. See the CHANGELOG entry in the category
`base_logic` for more information.
**Changes in `heap_lang`:** **Changes in `heap_lang`:**
......
...@@ -161,6 +161,16 @@ Section dfrac. ...@@ -161,6 +161,16 @@ Section dfrac.
Lemma dfrac_valid_own p : DfracOwn p (p 1)%Qp. Lemma dfrac_valid_own p : DfracOwn p (p 1)%Qp.
Proof. done. Qed. Proof. done. Qed.
Lemma dfrac_valid_own_r dq q : (dq DfracOwn q) (q < 1)%Qp.
Proof.
destruct dq as [q'| |q']; [|done|].
- apply Qp_lt_le_trans, Qp_lt_add_r.
- intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
Qed.
Lemma dfrac_valid_own_l dq q : (DfracOwn q dq) (q < 1)%Qp.
Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
Lemma dfrac_valid_discarded p : DfracDiscarded. Lemma dfrac_valid_discarded p : DfracDiscarded.
Proof. done. Qed. Proof. done. Qed.
...@@ -174,12 +184,11 @@ Section dfrac. ...@@ -174,12 +184,11 @@ Section dfrac.
Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed. Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
(** Discarding a fraction is a frame preserving update. *) (** Discarding a fraction is a frame preserving update. *)
Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded. Lemma dfrac_discard_update dq : dq ~~> DfracDiscarded.
Proof. Proof.
intros n [[q'| |q']|]; intros n [[q'| |q']|]; rewrite -!cmra_discrete_valid_iff //=.
rewrite /op /cmra_op -!cmra_discrete_valid_iff /valid /cmra_valid //=. - apply dfrac_valid_own_r.
- intros. apply Qp_lt_le_trans with (q + q')%Qp; [|done]. apply Qp_lt_add_r. - apply cmra_valid_op_r.
- intros. apply Qp_le_lt_trans with (q + q')%Qp; [|done]. apply Qp_le_add_r.
Qed. Qed.
End dfrac. End dfrac.
...@@ -378,13 +378,13 @@ Section lemmas. ...@@ -378,13 +378,13 @@ Section lemmas.
rewrite lookup_insert_ne //. rewrite lookup_insert_ne //.
Qed. Qed.
Lemma gmap_view_persist k q v : Lemma gmap_view_persist k dq v :
gmap_view_frag k (DfracOwn q) v ~~> gmap_view_frag k DfracDiscarded v. gmap_view_frag k dq v ~~> gmap_view_frag k DfracDiscarded v.
Proof. Proof.
apply view_update_frag=>m n bf Hrel j [df va] /=. apply view_update_frag=>m n bf Hrel j [df va] /=.
rewrite lookup_op. destruct (decide (j = k)) as [->|Hne]. rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].
- rewrite lookup_singleton. - rewrite lookup_singleton.
edestruct (Hrel k ((DfracOwn q, to_agree v) ? bf !! k)) as (v' & Hdf & Hva & Hm). edestruct (Hrel k ((dq, to_agree v) ? bf !! k)) as (v' & Hdf & Hva & Hm).
{ rewrite lookup_op lookup_singleton. { rewrite lookup_op lookup_singleton.
destruct (bf !! k) eqn:Hbf; by rewrite Hbf. } destruct (bf !! k) eqn:Hbf; by rewrite Hbf. }
rewrite Some_op_opM. intros [= Hbf]. rewrite Some_op_opM. intros [= Hbf].
......
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.
...@@ -7,7 +8,7 @@ From iris.prelude Require Import options. ...@@ -7,7 +8,7 @@ From iris.prelude Require Import options.
Import uPred. Import uPred.
(** This file provides a generic mechanism for a language-level point-to (** This file provides a generic mechanism for a language-level point-to
connective [l ↦{q} v] reflecting the physical heap. This library is designed to connective [l ↦{dq} v] reflecting the physical heap. This library is designed to
be used as a singleton (i.e., with only a single instance existing in any be used as a singleton (i.e., with only a single instance existing in any
proof), with the [gen_heapG] typeclass providing the ghost names of that unique proof), with the [gen_heapG] typeclass providing the ghost names of that unique
instance. That way, [mapsto] does not need an explicit [gname] parameter. instance. That way, [mapsto] does not need an explicit [gname] parameter.
...@@ -20,7 +21,7 @@ physical state, you will likely want explicit ghost names and are thus better ...@@ -20,7 +21,7 @@ physical state, you will likely want explicit ghost names and are thus better
off using [algebra.lib.gmap_view] together with [base_logic.lib.own]. off using [algebra.lib.gmap_view] together with [base_logic.lib.own].
This library is generic in the types [L] for locations and [V] for values and This library is generic in the types [L] for locations and [V] for values and
supports fractional permissions. Next to the point-to connective [l ↦{q} v], supports fractional permissions. Next to the point-to connective [l ↦{dq} v],
which keeps track of the value [v] of a location [l], this library also provides which keeps track of the value [v] of a location [l], this library also provides
a way to attach "meta" or "ghost" data to locations. This is done as follows: a way to attach "meta" or "ghost" data to locations. This is done as follows:
...@@ -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) (dq : 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 dq (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,16 @@ Section definitions. ...@@ -122,9 +123,16 @@ 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) (** FIXME: Refactor these notations using custom entries once Coq bug #13654
(at level 20, q at level 50, format "l ↦{ q } v") : bi_scope. has been fixed. *)
Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope. Local Notation "l ↦{ dq } v" := (mapsto l dq v)
(at level 20, format "l ↦{ dq } v") : bi_scope.
Local Notation "l ↦□ v" := (mapsto l DfracDiscarded v)
(at level 20, format "l ↦□ v") : bi_scope.
Local Notation "l ↦{# q } v" := (mapsto l (DfracOwn q) v)
(at level 20, format "l ↦{# q } v") : bi_scope.
Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
(at level 20, format "l ↦ v") : 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 Σ}.
...@@ -136,50 +144,59 @@ Section gen_heap. ...@@ -136,50 +144,59 @@ Section gen_heap.
Implicit Types v : V. Implicit Types v : V.
(** General properties of mapsto *) (** General properties of mapsto *)
Global Instance mapsto_timeless l q v : Timeless (l {q} v). Global Instance mapsto_timeless l dq v : Timeless (l {dq} 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 dq v : l {dq} v - dq%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 dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - (dq1 dq2) 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 dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - v1 = v2.
Proof. Proof.
iIntros "H1 H2". iIntros "H1 H2".
iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?]. iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
done. done.
Qed. Qed.
Lemma mapsto_combine l q1 q2 v1 v2 : Lemma mapsto_combine l dq1 dq2 v1 v2 :
l {q1} v1 - l {q2} v2 - l {q1 + q2} v1 v1 = v2. l {dq1} v1 - l {dq2} v2 - l {dq1 dq2} 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 dq1 dq2 v1 v2 :
¬ (q1 + q2 1)%Qp l1 {q1} v1 - l2 {q2} v2 - l1 l2. ¬ (dq1 dq2) l1 {dq1} v1 - l2 {dq2} 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 dq2 v1 v2 : l1 v1 - l2 {dq2} 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 any points-to predicate into a persistent
points-to predicate. *)
Lemma mapsto_persist l dq v : l {dq} 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).
...@@ -270,12 +287,11 @@ Section gen_heap. ...@@ -270,12 +287,11 @@ Section gen_heap.
first by apply lookup_union_None. first by apply lookup_union_None.
Qed. Qed.
Lemma gen_heap_valid σ l q v : gen_heap_interp σ - l {q} v - ⌜σ !! l = Some v. Lemma gen_heap_valid σ l dq v : gen_heap_interp σ - l {dq} 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,18 @@ From iris.prelude Require Import options. ...@@ -14,11 +14,18 @@ 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) (dq : dfrac) (vs : list val) : iProp Σ :=
([ list] i v vs, (l + i) {q} v)%I. ([ list] i v vs, (l + i) {dq} v)%I.
Notation "l ↦∗{ q } vs" := (array l q vs)
(at level 20, q at level 50, format "l ↦∗{ q } vs") : bi_scope. (** FIXME: Refactor these notations using custom entries once Coq bug #13654
Notation "l ↦∗ vs" := (array l 1 vs) has been fixed. *)
Notation "l ↦∗{ dq } vs" := (array l dq vs)
(at level 20, format "l ↦∗{ dq } vs") : bi_scope.
Notation "l ↦∗□ vs" := (array l DfracDiscarded vs)
(at level 20, format "l ↦∗□ vs") : bi_scope.
Notation "l ↦∗{# q } vs" := (array l (DfracOwn q) vs)
(at level 20, format "l ↦∗{# q } vs") : bi_scope.
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,32 +39,31 @@ Implicit Types Φ : val → iProp Σ. ...@@ -32,32 +39,31 @@ 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 dq : l ↦∗{dq} [] emp.
Proof. by rewrite /array. Qed. Proof. by rewrite /array. Qed.
Lemma array_singleton l q v : l ↦∗{q} [v] l {q} v. Lemma array_singleton l dq v : l ↦∗{dq} [v] l {dq} v.
Proof. by rewrite /array /= right_id loc_add_0. Qed. Proof. by rewrite /array /= right_id loc_add_0. Qed.
Lemma array_app l q vs ws : Lemma array_app l dq vs ws :
l ↦∗{q} (vs ++ ws) l ↦∗{q} vs (l + length vs) ↦∗{q} ws. l ↦∗{dq} (vs ++ ws) l ↦∗{dq} vs (l + length vs) ↦∗{dq} ws.
Proof. Proof.
rewrite /array big_sepL_app. rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add. setoid_rewrite Nat2Z.inj_add.
by setoid_rewrite loc_add_assoc. by setoid_rewrite loc_add_assoc.
Qed. Qed.
Lemma array_cons l q v vs : l ↦∗{q} (v :: vs) l {q} v (l + 1) ↦∗{q} vs. Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) l {dq} v (l + 1) ↦∗{dq} vs.
Proof. Proof.
rewrite /array big_sepL_cons loc_add_0. rewrite /array big_sepL_cons loc_add_0.
setoid_rewrite loc_add_assoc. setoid_rewrite loc_add_assoc.
...@@ -65,14 +71,14 @@ Proof. ...@@ -65,14 +71,14 @@ Proof.
by setoid_rewrite Z.add_1_l. by setoid_rewrite Z.add_1_l.
Qed. Qed.
Global Instance array_cons_frame l q v vs R Q : Global Instance array_cons_frame l dq v vs R Q :
Frame false R (l {q} v (l + 1) ↦∗{q} vs) Q Frame false R (l {dq} v (l + 1) ↦∗{dq} vs) Q
Frame false R (l ↦∗{q} (v :: vs)) Q. Frame false R (l ↦∗{dq} (v :: vs)) Q.
Proof. by rewrite /Frame array_cons. Qed. Proof. by rewrite /Frame array_cons. Qed.
Lemma update_array l q vs off v : Lemma update_array l dq vs off v :
vs !! off = Some v vs !! off = Some v
l ↦∗{q} vs - ((l + off) {q} v v', (l + off) {q} v' - l ↦∗{q} <[off:=v']>vs). l ↦∗{dq} vs - ((l + off) {dq} v v', (l + off) {dq} v' - l ↦∗{dq} <[off:=v']>vs).
Proof. Proof.
iIntros (Hlookup) "Hl". iIntros (Hlookup) "Hl".
rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done. rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
...@@ -90,9 +96,9 @@ Proof. ...@@ -90,9 +96,9 @@ Proof.
Qed. Qed.
(** * Rules for allocation *) (** * Rules for allocation *)
Lemma mapsto_seq_array l q v n : Lemma mapsto_seq_array l dq v n :
([ list] i seq 0 n, (l + (i : nat)) {q} v) - ([ list] i seq 0 n, (l + (i : nat)) {dq} v) -
l ↦∗{q} replicate n v. l ↦∗{dq} replicate n v.
Proof. Proof.
rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl. rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
{ done. } { done. }
...@@ -144,9 +150,9 @@ Proof. ...@@ -144,9 +150,9 @@ Proof.
Qed. Qed.
(** * Rules for accessing array elements *) (** * Rules for accessing array elements *)
Lemma twp_load_offset s E l q off vs v : Lemma twp_load_offset s E l dq off vs v :
vs !! off = Some v vs !! off = Some v
[[{ l ↦∗{q} vs }]] ! #(l + off) @ s; E [[{ RET v; l ↦∗{q} vs }]]. [[{ l ↦∗{dq} vs }]] ! #(l + off) @ s; E [[{ RET v; l ↦∗{dq} vs }]].
Proof. Proof.
iIntros (Hlookup Φ) "Hl HΦ". iIntros (Hlookup Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]". iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
...@@ -154,19 +160,19 @@ Proof. ...@@ -154,19 +160,19 @@ Proof.
iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done. iDestruct ("Hl2" $! v) as "Hl2". rewrite list_insert_id; last done.
iApply "Hl2". iApply "Hl1". iApply "Hl2". iApply "Hl1".
Qed. Qed.
Lemma wp_load_offset s E l q off vs v : Lemma wp_load_offset s E l dq off vs v :
vs !! off = Some v vs !! off = Some v
{{{ l ↦∗{q} vs }}} ! #(l + off) @ s; E {{{ RET v; l ↦∗{q} vs }}}. {{{ l ↦∗{dq} vs }}} ! #(l + off) @ s; E {{{ RET v; l ↦∗{dq} vs }}}.
Proof. Proof.
iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ"). iIntros (? Φ) ">H HΦ". iApply (twp_wp_step with "HΦ").
iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ". iApply (twp_load_offset with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed. Qed.
Lemma twp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) : Lemma twp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
[[{ l ↦∗{q} vs }]] ! #(l + off) @ s; E [[{ RET vs !!! off; l ↦∗{q} vs }]]. [[{ l ↦∗{dq} vs }]] ! #(l + off) @ s; E [[{ RET vs !!! off; l ↦∗{dq} vs }]].
Proof. apply twp_load_offset. by apply vlookup_lookup. Qed. Proof. apply twp_load_offset. by apply vlookup_lookup. Qed.
Lemma wp_load_offset_vec s E l q sz (off : fin sz) (vs : vec val sz) : Lemma wp_load_offset_vec s E l dq sz (off : fin sz) (vs : vec val sz) :
{{{ l ↦∗{q} vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗{q} vs }}}. {{{ l ↦∗{dq} vs }}} ! #(l + off) @ s; E {{{ RET vs !!! off; l ↦∗{dq} vs }}}.
Proof. apply wp_load_offset. by apply vlookup_lookup. Qed. Proof. apply wp_load_offset. by apply vlookup_lookup. Qed.
Lemma twp_store_offset s E l off vs v : Lemma twp_store_offset s E l off vs v :
...@@ -245,13 +251,13 @@ Proof. ...@@ -245,13 +251,13 @@ Proof.
iApply (twp_cmpxchg_suc_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ". iApply (twp_cmpxchg_suc_offset_vec with "H"); [eauto..|]; iIntros "H HΦ". by iApply "HΦ".
Qed. Qed.
Lemma twp_cmpxchg_fail_offset s E l q off vs v0 v1 v2 : Lemma twp_cmpxchg_fail_offset s E l dq off vs v0 v1 v2 :
vs !! off = Some v0 vs !! off = Some v0
v0 v1 v0 v1
vals_compare_safe v0 v1 vals_compare_safe v0 v1
[[{ l ↦∗{q} vs }]] [[{ l ↦∗{dq} vs }]]
CmpXchg #(l + off) v1 v2 @ s; E CmpXchg #(l + off) v1 v2 @ s; E
[[{ RET (v0, #false); l ↦∗{q} vs }]]. [[{ RET (v0, #false); l ↦∗{dq} vs }]].
Proof. Proof.
iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ". iIntros (Hlookup HNEq Hcmp Φ) "Hl HΦ".
iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]". iDestruct (update_array l _ _ _ _ Hlookup with "Hl") as "[Hl1 Hl2]".
...@@ -260,31 +266,31 @@ Proof. ...@@ -260,31 +266,31 @@ Proof.
iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2". iIntros "Hl1". iApply "HΦ". iDestruct ("Hl2" $! v0) as "Hl2".
rewrite list_insert_id; last done. iApply "Hl2". iApply "Hl1".