Library zoo.iris.base_logic.lib.ghost_heap
Require Import stdpp.namespaces.
Require Import iris.algebra.reservation_map.
Require Import iris.algebra.agree.
Require Import iris.algebra.frac.
Require Import iris.base_logic.lib.ghost_map.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Implicit Type η : 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 Type l : L.
Implicit Type v : V.
Implicit Type σ : gmap L V.
Implicit Type m : gmap L gname.
Record ghost_heap۰name :=
{ ghost_heap۰name۰heap : gname
; ghost_heap۰name۰meta : gname
}.
Implicit Type γ : 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₁ γ 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₂ γ 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₁ `{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₂ `{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.
Require Import iris.algebra.reservation_map.
Require Import iris.algebra.agree.
Require Import iris.algebra.frac.
Require Import iris.base_logic.lib.ghost_map.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.diaframe.
Require Import zoo.options.
Implicit Type η : 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 Type l : L.
Implicit Type v : V.
Implicit Type σ : gmap L V.
Implicit Type m : gmap L gname.
Record ghost_heap۰name :=
{ ghost_heap۰name۰heap : gname
; ghost_heap۰name۰meta : gname
}.
Implicit Type γ : 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₁ γ 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₂ γ 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₁ `{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₂ `{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.