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

rename gen_heap_ctx -> gen_heap_interp, and similar for proph_map_ctx

parent f94e312e
......@@ -92,7 +92,10 @@ With this release, we dropped support for Coq 8.9.
but should be applied to `iProp`. This avoids clients from having to push
through the `iProp`/`iPreProp`-isomorphism themselves, which is now handled
once and for all by the `own` construction.
* Rename `gen_heap_ctx` to `gen_heap_interp`, since it is meant to be used in
the state interpretation of WP and since `_ctx` is elsewhere used as a suffix
indicating "this is a persistent assumption that clients should always have in
their context". Likewise, rename `proph_map_ctx` to `proph_map_interp`.
**Changes in `program_logic`:**
......@@ -113,6 +116,9 @@ s/\b(excl|frac|ufrac)_auth_agreeL/\1_auth_agree_L/g
# auth_both_valid
s/\bauth_both_valid\b/auth_both_valid_discrete/g
s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
# gen_heap_ctx and proph_map_ctx
s/\bgen_heap_ctx\b/gen_heap_interp/g
s/\bproph_map_ctx\b/proph_map_interp/g
EOF
```
......
......@@ -9,7 +9,7 @@ Import uPred.
(** This file provides a generic mechanism for a point-to connective [l ↦{q} v]
with fractional permissions (where [l : L] and [v : V] over some abstract type
[L] for locations and [V] for values). This mechanism can be plugged into a
language and related to the physical heap by using [gen_heap_ctx σ] in the state
language and related to the physical heap by using [gen_heap_interp σ] in the state
interpretation of the weakest precondition, where [σ : gmap L V]. See heap-lang
for an example.
......@@ -54,7 +54,7 @@ these can be matched up with the invariant namespaces. *)
[namespace_map (agree positive)], which store the actual meta information.
This indirection is needed because we cannot perform frame preserving updates
in an authoritative fragment without owning the full authoritative element
(in other words, without the indirection [meta_set] would need [gen_heap_ctx]
(in other words, without the indirection [meta_set] would need [gen_heap_interp]
as a premise).
Note that in principle we could have used one big authoritative RA to keep track
......@@ -92,7 +92,7 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := m : gmap L gname,
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) σ
......@@ -130,7 +130,7 @@ Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
Local Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
|==> _ : gen_heapG L V Σ, gen_heap_ctx σ.
|==> _ : gen_heapG L V Σ, gen_heap_interp σ.
Proof.
iMod (own_alloc (gmap_view_auth (σ : gmap L (leibnizO V)))) as (γh) "Hh".
{ exact: gmap_view_auth_valid. }
......@@ -262,9 +262,9 @@ Section gen_heap.
(** Update lemmas *)
Lemma gen_heap_alloc σ l v :
σ !! l = None
gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v meta_token l .
gen_heap_interp σ == gen_heap_interp (<[l:=v]>σ) l v meta_token l .
Proof.
iIntros (Hσl). rewrite /gen_heap_ctx mapsto_eq /mapsto_def meta_token_eq /meta_token_def /=.
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. }
......@@ -280,8 +280,8 @@ Section gen_heap.
Lemma gen_heap_alloc_gen σ σ' :
σ' ## σ
gen_heap_ctx σ ==
gen_heap_ctx (σ' σ) ([ map] l v σ', l v) ([ map] l _ σ', meta_token l ).
gen_heap_interp σ ==
gen_heap_interp (σ' σ) ([ map] l v σ', l v) ([ map] l _ σ', meta_token l ).
Proof.
revert σ; induction σ' as [| l v σ' Hl IH] using map_ind; iIntros (σ Hdisj) "Hσ".
{ rewrite left_id_L. auto. }
......@@ -292,19 +292,19 @@ Section gen_heap.
first by apply lookup_union_None.
Qed.
Lemma gen_heap_valid σ l q v : gen_heap_ctx σ - l {q} v - ⌜σ !! l = Some v.
Lemma gen_heap_valid σ l q v : gen_heap_interp σ - l {q} v - ⌜σ !! l = Some v.
Proof.
iDestruct 1 as (m Hσm) "[Hσ _]". iIntros "Hl".
rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
rewrite /gen_heap_interp mapsto_eq /mapsto_def.
iDestruct (own_valid_2 with "Hσ Hl") as %[??]%gmap_view_both_valid_L.
iPureIntro. done.
Qed.
Lemma gen_heap_update σ l v1 v2 :
gen_heap_ctx σ - l v1 == gen_heap_ctx (<[l:=v2]>σ) l v2.
gen_heap_interp σ - l v1 == gen_heap_interp (<[l:=v2]>σ) l v2.
Proof.
iDestruct 1 as (m Hσm) "[Hσ Hm]".
iIntros "Hl". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
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. }
......
......@@ -41,7 +41,7 @@ Section definitions.
Definition proph_resolves_in_list R pvs :=
map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
Definition proph_map_ctx pvs (ps : gset P) : iProp Σ :=
Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
( R, proph_resolves_in_list R pvs
dom (gset _) R ps
own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) R))%I.
......@@ -73,7 +73,7 @@ Section list_resolves.
End list_resolves.
Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
|==> _ : proph_mapG P V PVS, proph_map_ctx pvs ps.
|==> _ : proph_mapG P V PVS, proph_map_interp pvs ps.
Proof.
iMod (own_alloc (gmap_view_auth )) as (γ) "Hh".
{ apply gmap_view_auth_valid. }
......@@ -104,8 +104,8 @@ Section proph_map.
Lemma proph_map_new_proph p ps pvs :
p ps
proph_map_ctx pvs ps ==
proph_map_ctx pvs ({[p]} ps) proph p (proph_list_resolves pvs p).
proph_map_interp pvs ps ==
proph_map_interp pvs ({[p]} ps) proph p (proph_list_resolves pvs p).
Proof.
iIntros (Hp) "HR". iDestruct "HR" as (R) "[[% %] H●]".
rewrite proph_eq /proph_def.
......@@ -120,11 +120,11 @@ Section proph_map.
Qed.
Lemma proph_map_resolve_proph p v pvs ps vs :
proph_map_ctx ((p,v) :: pvs) ps proph p vs ==
vs', vs = v::vs' proph_map_ctx pvs ps proph p vs'.
proph_map_interp ((p,v) :: pvs) ps proph p vs ==
vs', vs = v::vs' proph_map_interp pvs ps proph p vs'.
Proof.
iIntros "[HR Hp]". iDestruct "HR" as (R) "[HP H●]". iDestruct "HP" as %[Hres Hdom].
rewrite /proph_map_ctx proph_eq /proph_def.
rewrite /proph_map_interp proph_eq /proph_def.
iDestruct (own_valid_2 with "H● Hp") as %[_ HR]%gmap_view_both_valid_L.
assert (vs = v :: proph_list_resolves pvs p) as ->.
{ rewrite (Hres p vs HR). simpl. by rewrite decide_True. }
......
......@@ -25,7 +25,7 @@ Proof.
iMod (inv_heap_init loc (option val)) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
iModIntro. iExists
(λ σ κs, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ σ κs, (gen_heap_interp σ.(heap) proph_map_interp κs σ.(used_proph_id))%I),
(λ _, True%I).
iFrame. iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed.
......@@ -22,7 +22,7 @@ Class heapG Σ := HeapG {
Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ :=
(gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I;
(gen_heap_interp σ.(heap) proph_map_interp κs σ.(used_proph_id))%I;
fork_post _ := True%I;
}.
......
......@@ -14,7 +14,7 @@ Proof.
iMod (proph_map_init [] σ.(used_proph_id)) as (?) "Hp".
iModIntro.
iExists
(λ σ κs _, (gen_heap_ctx σ.(heap) proph_map_ctx κs σ.(used_proph_id))%I),
(λ σ κs _, (gen_heap_interp σ.(heap) proph_map_interp κs σ.(used_proph_id))%I),
(λ _, True%I); iFrame.
iApply (Hwp (HeapG _ _ _ _ _)). done.
Qed.
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