Library zoo.iris.base_logic.lib.ghost_heap
From stdpp Require Import
namespaces.
From iris.algebra Require Import
reservation_map
agree
frac.
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.base_logic Require Export
lib.base.
From zoo.iris Require Import
diaframe.
From zoo Require Import
options.
Implicit Types η : gname.
Class GhostHeapG Σ L V `{Countable L} :=
{ #[local] ghost_heap_G_heap_G :: ghost_mapG Σ L V
; #[local] ghost_heap_G_meta_G :: ghost_mapG Σ L gname
; #[local] ghost_heap_G_meta_data_G :: inG Σ (reservation_mapR $ agreeR positiveO)
}.
Definition ghost_heap_Σ L V `{Countable L} :=
#[ghost_mapΣ L V
; ghost_mapΣ L gname
; GFunctor (reservation_mapR $ agreeR positiveO)
].
#[global] Instance subG_ghost_heap_Σ Σ L V `{Countable L} :
subG (ghost_heap_Σ L V) Σ →
GhostHeapG Σ L V.
Section ghost_heap_G.
Context `{ghost_heap_G : GhostHeapG Σ L V}.
Implicit Types l : L.
Implicit Types v : V.
Implicit Types σ : gmap L V.
Implicit Types m : gmap L gname.
Record ghost_heap_name :=
{ ghost_heap_name_heap : gname
; ghost_heap_name_meta : gname
}.
Implicit Types γ : ghost_heap_name.
#[global] Instance ghost_heap_name_eq_dec : EqDecision ghost_heap_name :=
ltac:(solve_decision).
#[global] Instance ghost_heap_name_countable :
Countable ghost_heap_name.
Definition ghost_heap_auth γ σ : iProp Σ :=
∃ m,
⌜dom m ⊆ dom σ⌝ ∗
ghost_map_auth γ.(ghost_heap_name_heap) 1 σ ∗
ghost_map_auth γ.(ghost_heap_name_meta) 1 m.
#[local] Instance : CustomIpat "auth" :=
" ( %m & %Hdom & Hσ & Hm ) ".
Definition ghost_heap_at γ l dq v :=
ghost_map_elem γ.(ghost_heap_name_heap) l dq v.
Definition ghost_heap_meta_token γ l E : iProp Σ :=
∃ η,
ghost_map_elem γ.(ghost_heap_name_meta) l DfracDiscarded η ∗
own η (reservation_map_token E).
#[local] Instance : CustomIpat "meta_token" :=
" ( %η{} & #Hl{_{}} & Hη{} ) ".
Definition ghost_heap_meta `{Countable A} γ l ι (x : A) : iProp Σ :=
∃ η,
ghost_map_elem γ.(ghost_heap_name_meta) l DfracDiscarded η ∗
own η (reservation_map_data (coPpick (↑ι)) $ to_agree $ encode x).
#[local] Instance : CustomIpat "meta" :=
" ( %η{} & #Hl{_{}} & Hη{} ) ".
#[global] Instance ghost_heap_auth_timeless γ σ :
Timeless (ghost_heap_auth γ σ).
#[global] Instance ghost_heap_at_timeless γ l dq v :
Timeless (ghost_heap_at γ l dq v).
#[global] Instance ghost_heap_at_persistent γ l v :
Persistent (ghost_heap_at γ l DfracDiscarded v).
#[global] Instance ghost_heap_at_fractional γ l v :
Fractional (λ q, ghost_heap_at γ l (DfracOwn q) v)%I.
#[global] Instance ghost_heap_at_as_fractional γ l q v :
AsFractional (ghost_heap_at γ l (DfracOwn q) v) (λ q, ghost_heap_at γ l (DfracOwn q) v)%I q.
Lemma ghost_heap_at_valid γ l dq v :
ghost_heap_at γ l dq v ⊢
⌜✓ dq⌝.
Lemma ghost_heap_at_combine γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜v1 = v2⌝ ∗
ghost_heap_at γ l (dq1 ⋅ dq2) v1.
Lemma ghost_heap_at_valid_2 γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma ghost_heap_at_agree γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜v1 = v2⌝.
Lemma ghost_heap_at_dfrac_ne γ l1 dq1 v1 l2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
ghost_heap_at γ l1 dq1 v1 -∗
ghost_heap_at γ l2 dq2 v2 -∗
⌜l1 ≠ l2⌝.
Lemma ghost_heap_at_ne γ l1 v1 l2 dq2 v2 :
ghost_heap_at γ l1 (DfracOwn 1) v1 -∗
ghost_heap_at γ l2 dq2 v2 -∗
⌜l1 ≠ l2⌝.
Lemma ghost_heap_at_exclusive γ l v1 dq2 v2 :
ghost_heap_at γ l (DfracOwn 1) v1 -∗
ghost_heap_at γ l dq2 v2 -∗
False.
Lemma ghost_heap_at_persist γ l dq v :
ghost_heap_at γ l dq v ⊢ |==>
ghost_heap_at γ l DfracDiscarded v.
#[global] Instance ghost_heap_at_combine_sep_gives γ l dq1 v1 dq2 v2 :
CombineSepGives (ghost_heap_at γ l dq1 v1) (ghost_heap_at γ l dq2 v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝
| 30.
#[global] Instance ghost_heap_at_combine_as γ l dq1 dq2 v1 v2 :
CombineSepAs (ghost_heap_at γ l dq1 v1) (ghost_heap_at γ l dq2 v2) (ghost_heap_at γ l (dq1 ⋅ dq2) v1)
| 60.
#[global] Instance frame_ghost_heap_at p γ l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (ghost_heap_at γ l (DfracOwn q1) v) (ghost_heap_at γ l (DfracOwn q2) v) (ghost_heap_at γ l (DfracOwn q) v)
| 5.
#[global] Instance ghost_heap_meta_token_timeless γ l E :
Timeless (ghost_heap_meta_token γ l E).
#[global] Instance ghost_heap_meta_timeless `{Countable A} γ l ι (x : A) :
Timeless (ghost_heap_meta γ l ι x).
#[global] Instance ghost_heap_meta_persistent `{Countable A} γ l ι (x : A) :
Persistent (ghost_heap_meta γ l ι x).
Lemma ghost_heap_meta_token_union_1 γ l E1 E2 :
E1 ## E2 →
ghost_heap_meta_token γ l (E1 ∪ E2) ⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l E2.
Lemma ghost_heap_meta_token_union_2 γ l E1 E2 :
ghost_heap_meta_token γ l E1 -∗
ghost_heap_meta_token γ l E2 -∗
ghost_heap_meta_token γ l (E1 ∪ E2).
Lemma ghost_heap_meta_token_union γ l E1 E2 :
E1 ## E2 →
ghost_heap_meta_token γ l (E1 ∪ E2) ⊣⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l E2.
Lemma ghost_heap_meta_token_difference γ l E1 E2 :
E1 ⊆ E2 →
ghost_heap_meta_token γ l E2 ⊣⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l (E2 ∖ E1).
Lemma ghost_heap_meta_agree `{Countable A} γ l ι (x1 x2 : A) :
ghost_heap_meta γ l ι x1 -∗
ghost_heap_meta γ l ι x2 -∗
⌜x1 = x2⌝.
Lemma ghost_heap_meta_set `{Countable A} γ E l (x : A) ι :
↑ι ⊆ E →
ghost_heap_meta_token γ l E ⊢ |==>
ghost_heap_meta γ l ι x.
Lemma ghost_heap_meta_meta_token_valid `{Countable A} γ l (x : A) ι E :
ghost_heap_meta γ l ι x -∗
ghost_heap_meta_token γ l E -∗
⌜↑ι ⊈ E⌝.
Lemma ghost_heap_meta_meta_token_valid' `{Countable A} γ l (x : A) ι E :
↑ι ⊆ E →
ghost_heap_meta γ l ι x -∗
ghost_heap_meta_token γ l E -∗
False.
#[global] Instance ghost_heap_combine_sep_gives_meta_meta_token_1 `{Countable A} γ l (x : A) ι E :
CombineSepGives (ghost_heap_meta γ l ι x) (ghost_heap_meta_token γ l E) ⌜↑ι ⊈ E⌝.
#[global] Instance ghost_heap_combine_sep_gives_meta_meta_token_2 `{Countable A} γ l (x : A) ι E :
CombineSepGives (ghost_heap_meta_token γ l E) (ghost_heap_meta γ l ι x) ⌜↑ι ⊈ E⌝.
Lemma ghost_heap_lookup γ σ l dq v :
ghost_heap_auth γ σ -∗
ghost_heap_at γ l dq v -∗
⌜σ !! l = Some v⌝.
Lemma ghost_heap_insert {γ σ} l v :
σ !! l = None →
ghost_heap_auth γ σ ⊢ |==>
ghost_heap_auth γ (<[l := v]> σ) ∗
ghost_heap_at γ l (DfracOwn 1) v ∗
ghost_heap_meta_token γ l ⊤.
Lemma ghost_heap_insert_big {γ σ1} σ2 :
σ2 ##ₘ σ1 →
ghost_heap_auth γ σ1 ⊢ |==>
ghost_heap_auth γ (σ2 ∪ σ1) ∗
([∗ map] l ↦ v ∈ σ2, ghost_heap_at γ l (DfracOwn 1) v) ∗
([∗ map] l ↦ _ ∈ σ2, ghost_heap_meta_token γ l ⊤).
Lemma ghost_heap_update {γ σ l v1} v2 :
ghost_heap_auth γ σ -∗
ghost_heap_at γ l (DfracOwn 1) v1 ==∗
ghost_heap_auth γ (<[l := v2]> σ) ∗
ghost_heap_at γ l (DfracOwn 1) v2.
Lemma ghost_heap_alloc σ :
⊢ |==>
∃ γ,
ghost_heap_auth γ σ ∗
([∗ map] l ↦ v ∈ σ, ghost_heap_at γ l (DfracOwn 1) v) ∗
([∗ map] l ↦ _ ∈ σ, ghost_heap_meta_token γ l ⊤).
End ghost_heap_G.
#[global] Opaque ghost_heap_auth.
#[global] Opaque ghost_heap_at.
#[global] Opaque ghost_heap_meta_token.
#[global] Opaque ghost_heap_meta.
namespaces.
From iris.algebra Require Import
reservation_map
agree
frac.
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.base_logic Require Export
lib.base.
From zoo.iris Require Import
diaframe.
From zoo Require Import
options.
Implicit Types η : gname.
Class GhostHeapG Σ L V `{Countable L} :=
{ #[local] ghost_heap_G_heap_G :: ghost_mapG Σ L V
; #[local] ghost_heap_G_meta_G :: ghost_mapG Σ L gname
; #[local] ghost_heap_G_meta_data_G :: inG Σ (reservation_mapR $ agreeR positiveO)
}.
Definition ghost_heap_Σ L V `{Countable L} :=
#[ghost_mapΣ L V
; ghost_mapΣ L gname
; GFunctor (reservation_mapR $ agreeR positiveO)
].
#[global] Instance subG_ghost_heap_Σ Σ L V `{Countable L} :
subG (ghost_heap_Σ L V) Σ →
GhostHeapG Σ L V.
Section ghost_heap_G.
Context `{ghost_heap_G : GhostHeapG Σ L V}.
Implicit Types l : L.
Implicit Types v : V.
Implicit Types σ : gmap L V.
Implicit Types m : gmap L gname.
Record ghost_heap_name :=
{ ghost_heap_name_heap : gname
; ghost_heap_name_meta : gname
}.
Implicit Types γ : ghost_heap_name.
#[global] Instance ghost_heap_name_eq_dec : EqDecision ghost_heap_name :=
ltac:(solve_decision).
#[global] Instance ghost_heap_name_countable :
Countable ghost_heap_name.
Definition ghost_heap_auth γ σ : iProp Σ :=
∃ m,
⌜dom m ⊆ dom σ⌝ ∗
ghost_map_auth γ.(ghost_heap_name_heap) 1 σ ∗
ghost_map_auth γ.(ghost_heap_name_meta) 1 m.
#[local] Instance : CustomIpat "auth" :=
" ( %m & %Hdom & Hσ & Hm ) ".
Definition ghost_heap_at γ l dq v :=
ghost_map_elem γ.(ghost_heap_name_heap) l dq v.
Definition ghost_heap_meta_token γ l E : iProp Σ :=
∃ η,
ghost_map_elem γ.(ghost_heap_name_meta) l DfracDiscarded η ∗
own η (reservation_map_token E).
#[local] Instance : CustomIpat "meta_token" :=
" ( %η{} & #Hl{_{}} & Hη{} ) ".
Definition ghost_heap_meta `{Countable A} γ l ι (x : A) : iProp Σ :=
∃ η,
ghost_map_elem γ.(ghost_heap_name_meta) l DfracDiscarded η ∗
own η (reservation_map_data (coPpick (↑ι)) $ to_agree $ encode x).
#[local] Instance : CustomIpat "meta" :=
" ( %η{} & #Hl{_{}} & Hη{} ) ".
#[global] Instance ghost_heap_auth_timeless γ σ :
Timeless (ghost_heap_auth γ σ).
#[global] Instance ghost_heap_at_timeless γ l dq v :
Timeless (ghost_heap_at γ l dq v).
#[global] Instance ghost_heap_at_persistent γ l v :
Persistent (ghost_heap_at γ l DfracDiscarded v).
#[global] Instance ghost_heap_at_fractional γ l v :
Fractional (λ q, ghost_heap_at γ l (DfracOwn q) v)%I.
#[global] Instance ghost_heap_at_as_fractional γ l q v :
AsFractional (ghost_heap_at γ l (DfracOwn q) v) (λ q, ghost_heap_at γ l (DfracOwn q) v)%I q.
Lemma ghost_heap_at_valid γ l dq v :
ghost_heap_at γ l dq v ⊢
⌜✓ dq⌝.
Lemma ghost_heap_at_combine γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜v1 = v2⌝ ∗
ghost_heap_at γ l (dq1 ⋅ dq2) v1.
Lemma ghost_heap_at_valid_2 γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma ghost_heap_at_agree γ l dq1 v1 dq2 v2 :
ghost_heap_at γ l dq1 v1 -∗
ghost_heap_at γ l dq2 v2 -∗
⌜v1 = v2⌝.
Lemma ghost_heap_at_dfrac_ne γ l1 dq1 v1 l2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
ghost_heap_at γ l1 dq1 v1 -∗
ghost_heap_at γ l2 dq2 v2 -∗
⌜l1 ≠ l2⌝.
Lemma ghost_heap_at_ne γ l1 v1 l2 dq2 v2 :
ghost_heap_at γ l1 (DfracOwn 1) v1 -∗
ghost_heap_at γ l2 dq2 v2 -∗
⌜l1 ≠ l2⌝.
Lemma ghost_heap_at_exclusive γ l v1 dq2 v2 :
ghost_heap_at γ l (DfracOwn 1) v1 -∗
ghost_heap_at γ l dq2 v2 -∗
False.
Lemma ghost_heap_at_persist γ l dq v :
ghost_heap_at γ l dq v ⊢ |==>
ghost_heap_at γ l DfracDiscarded v.
#[global] Instance ghost_heap_at_combine_sep_gives γ l dq1 v1 dq2 v2 :
CombineSepGives (ghost_heap_at γ l dq1 v1) (ghost_heap_at γ l dq2 v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝
| 30.
#[global] Instance ghost_heap_at_combine_as γ l dq1 dq2 v1 v2 :
CombineSepAs (ghost_heap_at γ l dq1 v1) (ghost_heap_at γ l dq2 v2) (ghost_heap_at γ l (dq1 ⋅ dq2) v1)
| 60.
#[global] Instance frame_ghost_heap_at p γ l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (ghost_heap_at γ l (DfracOwn q1) v) (ghost_heap_at γ l (DfracOwn q2) v) (ghost_heap_at γ l (DfracOwn q) v)
| 5.
#[global] Instance ghost_heap_meta_token_timeless γ l E :
Timeless (ghost_heap_meta_token γ l E).
#[global] Instance ghost_heap_meta_timeless `{Countable A} γ l ι (x : A) :
Timeless (ghost_heap_meta γ l ι x).
#[global] Instance ghost_heap_meta_persistent `{Countable A} γ l ι (x : A) :
Persistent (ghost_heap_meta γ l ι x).
Lemma ghost_heap_meta_token_union_1 γ l E1 E2 :
E1 ## E2 →
ghost_heap_meta_token γ l (E1 ∪ E2) ⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l E2.
Lemma ghost_heap_meta_token_union_2 γ l E1 E2 :
ghost_heap_meta_token γ l E1 -∗
ghost_heap_meta_token γ l E2 -∗
ghost_heap_meta_token γ l (E1 ∪ E2).
Lemma ghost_heap_meta_token_union γ l E1 E2 :
E1 ## E2 →
ghost_heap_meta_token γ l (E1 ∪ E2) ⊣⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l E2.
Lemma ghost_heap_meta_token_difference γ l E1 E2 :
E1 ⊆ E2 →
ghost_heap_meta_token γ l E2 ⊣⊢
ghost_heap_meta_token γ l E1 ∗
ghost_heap_meta_token γ l (E2 ∖ E1).
Lemma ghost_heap_meta_agree `{Countable A} γ l ι (x1 x2 : A) :
ghost_heap_meta γ l ι x1 -∗
ghost_heap_meta γ l ι x2 -∗
⌜x1 = x2⌝.
Lemma ghost_heap_meta_set `{Countable A} γ E l (x : A) ι :
↑ι ⊆ E →
ghost_heap_meta_token γ l E ⊢ |==>
ghost_heap_meta γ l ι x.
Lemma ghost_heap_meta_meta_token_valid `{Countable A} γ l (x : A) ι E :
ghost_heap_meta γ l ι x -∗
ghost_heap_meta_token γ l E -∗
⌜↑ι ⊈ E⌝.
Lemma ghost_heap_meta_meta_token_valid' `{Countable A} γ l (x : A) ι E :
↑ι ⊆ E →
ghost_heap_meta γ l ι x -∗
ghost_heap_meta_token γ l E -∗
False.
#[global] Instance ghost_heap_combine_sep_gives_meta_meta_token_1 `{Countable A} γ l (x : A) ι E :
CombineSepGives (ghost_heap_meta γ l ι x) (ghost_heap_meta_token γ l E) ⌜↑ι ⊈ E⌝.
#[global] Instance ghost_heap_combine_sep_gives_meta_meta_token_2 `{Countable A} γ l (x : A) ι E :
CombineSepGives (ghost_heap_meta_token γ l E) (ghost_heap_meta γ l ι x) ⌜↑ι ⊈ E⌝.
Lemma ghost_heap_lookup γ σ l dq v :
ghost_heap_auth γ σ -∗
ghost_heap_at γ l dq v -∗
⌜σ !! l = Some v⌝.
Lemma ghost_heap_insert {γ σ} l v :
σ !! l = None →
ghost_heap_auth γ σ ⊢ |==>
ghost_heap_auth γ (<[l := v]> σ) ∗
ghost_heap_at γ l (DfracOwn 1) v ∗
ghost_heap_meta_token γ l ⊤.
Lemma ghost_heap_insert_big {γ σ1} σ2 :
σ2 ##ₘ σ1 →
ghost_heap_auth γ σ1 ⊢ |==>
ghost_heap_auth γ (σ2 ∪ σ1) ∗
([∗ map] l ↦ v ∈ σ2, ghost_heap_at γ l (DfracOwn 1) v) ∗
([∗ map] l ↦ _ ∈ σ2, ghost_heap_meta_token γ l ⊤).
Lemma ghost_heap_update {γ σ l v1} v2 :
ghost_heap_auth γ σ -∗
ghost_heap_at γ l (DfracOwn 1) v1 ==∗
ghost_heap_auth γ (<[l := v2]> σ) ∗
ghost_heap_at γ l (DfracOwn 1) v2.
Lemma ghost_heap_alloc σ :
⊢ |==>
∃ γ,
ghost_heap_auth γ σ ∗
([∗ map] l ↦ v ∈ σ, ghost_heap_at γ l (DfracOwn 1) v) ∗
([∗ map] l ↦ _ ∈ σ, ghost_heap_meta_token γ l ⊤).
End ghost_heap_G.
#[global] Opaque ghost_heap_auth.
#[global] Opaque ghost_heap_at.
#[global] Opaque ghost_heap_meta_token.
#[global] Opaque ghost_heap_meta.