Commit 543b9218 authored by Ralf Jung's avatar Ralf Jung
Browse files

port gen_heap to ghost_map

parent 456eccfa
From stdpp Require Export namespaces.
From iris.algebra Require Import gmap_view namespace_map agree frac.
From iris.algebra Require Import namespace_map agree frac.
From iris.algebra Require Export dfrac.
From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import ghost_map.
From iris.prelude Require Import options.
Import uPred.
......@@ -17,8 +18,9 @@ by using [gen_heap_interp σ] in the state interpretation of the weakest
precondition. See heap-lang for an example.
If you are looking for a library providing "ghost heaps" independent of the
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].
physical state, you will likely want explicit ghost names to disambiguate
multiple heaps and are thus better off using [ghost_map], or (if you need more
flexibility), directly using the underlying [algebra.lib.gmap_view].
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 ↦{dq} v],
......@@ -64,8 +66,8 @@ these can be matched up with the invariant namespaces. *)
(** The CMRAs we need, and the global ghost names we are using. *)
Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} := {
gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO V));
gen_meta_preG_inG :> inG Σ (gmap_viewR L gnameO);
gen_heap_preG_inG :> ghost_mapG Σ L V;
gen_meta_preG_inG :> ghost_mapG Σ L gname;
gen_meta_data_preG_inG :> inG Σ (namespace_mapR (agreeR positiveO));
}.
......@@ -79,8 +81,8 @@ Global Arguments gen_heap_name {L V Σ _ _} _ : assert.
Global Arguments gen_meta_name {L V Σ _ _} _ : assert.
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors := #[
GFunctor (gmap_viewR L (leibnizO V));
GFunctor (gmap_viewR L gnameO);
ghost_mapΣ L V;
ghost_mapΣ L gname;
GFunctor (namespace_mapR (agreeR positiveO))
].
......@@ -94,25 +96,24 @@ Section definitions.
Definition gen_heap_interp (σ : gmap L V) : iProp Σ := m : gmap L gname,
(* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *)
dom _ m dom (gset L) σ
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)).
dom _ m dom (gset L) σ
ghost_map_auth (gen_heap_name hG) 1 σ
ghost_map_auth (gen_meta_name hG) 1 m.
Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO V)).
l [gen_heap_name hG]{dq} v.
Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
Definition mapsto := mapsto_aux.(unseal).
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
γm, own (gen_meta_name hG) (gmap_view_frag l DfracDiscarded γm)
own γm (namespace_map_token E).
γm, l [gen_meta_name hG] γm own γm (namespace_map_token E).
Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
γm, own (gen_meta_name hG) (gmap_view_frag l DfracDiscarded γm)
γm, l [gen_meta_name hG] γm
own γm (namespace_map_data N (to_agree (encode x))).
Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta := meta_aux.(unseal).
......@@ -144,64 +145,43 @@ Section gen_heap.
Global Instance mapsto_timeless l dq v : Timeless (l {dq} v).
Proof. rewrite mapsto_eq. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {#q} v)%I.
Proof.
intros p q. rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_add //.
Qed.
Proof. rewrite mapsto_eq. apply _. Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {#q} v) (λ q, l {#q} v)%I q.
Proof. split; [done|]. apply _. Qed.
Proof. rewrite mapsto_eq. apply _. Qed.
Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
Proof. rewrite mapsto_eq. apply _. Qed.
Lemma mapsto_valid l dq v : l {dq} v - ⌜✓ dq%Qp.
Proof.
rewrite mapsto_eq. iIntros "Hl".
iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_valid. Qed.
Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - ⌜✓ (dq1 dq2) v1 = v2.
Proof.
rewrite mapsto_eq. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
auto.
Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_valid_2. Qed.
(** Almost all the time, this is all you really need. *)
Lemma mapsto_agree l dq1 dq2 v1 v2 : l {dq1} v1 - l {dq2} v2 - v1 = v2.
Proof.
iIntros "H1 H2".
iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
done.
Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_agree. Qed.
Lemma mapsto_combine l dq1 dq2 v1 v2 :
l {dq1} v1 - l {dq2} v2 - l {dq1 dq2} v1 v1 = v2.
Proof.
iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
iCombine "Hl1 Hl2" as "Hl".
rewrite mapsto_eq /mapsto_def -own_op gmap_view_frag_op.
auto.
Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_combine. Qed.
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ (dq1 dq2) l1 {dq1} v1 - l2 {dq2} v2 - l1 l2.
Proof.
iIntros (?) "Hl1 Hl2"; iIntros (->).
by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_frac_ne. Qed.
Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 v1 - l2 {dq2} v2 - l1 l2.
Proof. apply mapsto_frac_ne. intros ?%exclusive_l; [done|apply _]. Qed.
Proof. rewrite mapsto_eq. apply ghost_map_elem_ne. 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.
Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
(** General properties of [meta] and [meta_token] *)
Global Instance meta_token_timeless l N : Timeless (meta_token l N).
Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
Proof. rewrite meta_token_eq. apply _. Qed.
Global Instance meta_timeless `{Countable A} l N (x : A) : Timeless (meta l N x).
Proof. rewrite meta_eq /meta_def. apply _. Qed.
Proof. rewrite meta_eq. apply _. Qed.
Global Instance meta_persistent `{Countable A} l N (x : A) : Persistent (meta l N x).
Proof. rewrite meta_eq /meta_def. apply _. Qed.
Proof. rewrite meta_eq. apply _. Qed.
Lemma meta_token_union_1 l E1 E2 :
E1 ## E2 meta_token l (E1 E2) - meta_token l E1 meta_token l E2.
......@@ -215,7 +195,7 @@ Section gen_heap.
Proof.
rewrite meta_token_eq /meta_token_def.
iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %?%namespace_map_token_valid_op.
iExists γm2. iFrame "Hγm2". rewrite namespace_map_token_union //. by iSplitL "Hm1".
Qed.
......@@ -238,7 +218,7 @@ Section gen_heap.
Proof.
rewrite meta_eq /meta_def.
iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
iDestruct (own_valid_2 with "Hγm1 Hγm2") as %[_ ->]%gmap_view_frag_op_valid_L.
iDestruct (ghost_map_elem_valid_2 with "Hγm1 Hγm2") as %[_ ->].
iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
move: Hγ. rewrite -namespace_map_data_op namespace_map_data_valid.
move=> /to_agree_op_inv_L. naive_solver.
......@@ -258,13 +238,11 @@ Section gen_heap.
Proof.
iIntros (Hσl). rewrite /gen_heap_interp mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply (gmap_view_alloc _ l (DfracOwn 1)); done. }
iMod (ghost_map_insert l with "Hσ") as "[Hσ Hl]"; first done.
iMod (own_alloc (namespace_map_token )) as (γm) "Hγm".
{ apply namespace_map_token_valid. }
iMod (own_update with "Hm") as "[Hm Hlm]".
{ eapply (gmap_view_alloc _ l DfracDiscarded); last done.
move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
iMod (ghost_map_insert_persist l with "Hm") as "[Hm Hlm]".
{ move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
iModIntro. iFrame "Hl". iSplitL "Hσ Hm"; last by eauto with iFrame.
iExists (<[l:=γm]> m). iFrame. iPureIntro.
rewrite !dom_insert_L. set_solver.
......@@ -288,7 +266,7 @@ Section gen_heap.
Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_interp mapsto_eq.
by iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
by iDestruct (ghost_map_lookup with "Hσ Hl") as %?.
Qed.
Lemma gen_heap_update σ l v1 v2 :
......@@ -296,9 +274,8 @@ Section gen_heap.
Proof.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_interp mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl") as %[_ Hl]%gmap_view_both_valid_L.
iMod (own_update_2 with "Hσ Hl") as "[Hσ Hl]".
{ eapply gmap_view_update. }
iDestruct (ghost_map_lookup with "Hσ Hl") as %Hl.
iMod (ghost_map_update with "Hσ Hl") as "[Hσ Hl]".
iModIntro. iFrame "Hl". iExists m. iFrame.
iPureIntro. apply (elem_of_dom_2 (D:=gset L)) in Hl.
rewrite dom_insert_L. set_solver.
......@@ -314,10 +291,8 @@ Lemma gen_heap_init_names `{Countable L, !gen_heapPreG L V Σ} σ :
let hG := GenHeapG L V Σ γh γm in
gen_heap_interp σ ([ map] l v σ, l v) ([ map] l _ σ, meta_token l ).
Proof.
iMod (own_alloc (gmap_view_auth 1 ( : gmap L (leibnizO V)))) as (γh) "Hh".
{ exact: gmap_view_auth_valid. }
iMod (own_alloc (gmap_view_auth 1 ( : gmap L gnameO))) as (γm) "Hm".
{ exact: gmap_view_auth_valid. }
iMod (ghost_map_alloc_empty (V:=V)) as (γh) "Hh".
iMod (ghost_map_alloc_empty (V:=gname)) as (γm) "Hm".
iExists γh, γm.
iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ) with "[Hh Hm]" as "Hinterp".
{ iExists ; simpl. iFrame "Hh Hm". by rewrite dom_empty_L. }
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment