Library zoo.program_logic.ghost_state
From iris.bi Require Export
lib.fractional.
From iris.base_logic Require Import
lib.ghost_map
lib.invariants.
From zoo Require Import
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_nat_max
lib.ghost_heap
lib.ghost_list
lib.mono_list.
From zoo.iris Require Import
diaframe.
From zoo.language Require Export
language.
From zoo.language Require Import
notations.
From zoo Require Import
options.
Implicit Types cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Types tid : thread_id.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types hdr : header.
Implicit Types hdrs : gmap location header.
Implicit Types σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Types κ κs : list observation.
Parameter zoo_counter : location.
Class ZooG₀ Σ :=
{ #[local] zoo_G₀_headers_G :: GhostHeapG Σ location header
; #[local] zoo_G₀_heap_G :: ghost_mapG Σ location val
; #[local] zoo_G_prophets_G :: ghost_mapG Σ prophet_id (list (val × val))
; #[local] zoo_G₀_steps_G :: AuthNatMaxG Σ
; #[local] zoo_G₀_locals_G :: GhostListG Σ val
; #[local] zoo_G₀_counter_G :: MonoListG Σ val
}.
#[local] Definition zoo_Σ₀ :=
#[ghost_heap_Σ location header
; ghost_mapΣ location val
; ghost_mapΣ prophet_id (list (val × val))
; auth_nat_max_Σ
; ghost_list_Σ val
; mono_list_Σ val
].
#[local] Instance subG_zoo_Σ₀ Σ :
subG zoo_Σ₀ Σ →
ZooG₀ Σ.
Class ZooGpre Σ :=
{ #[global] zoo_Gpre_inv_Gpre :: invGpreS Σ
; #[local] zoo_Gpre_G₀ :: ZooG₀ Σ
}.
Definition zoo_Σ :=
#[invΣ
; zoo_Σ₀
].
#[global] Instance subG_zoo_Σ Σ :
subG zoo_Σ Σ →
ZooGpre Σ.
Class ZooG Σ :=
{ #[global] zoo_G_inv_G :: invGS Σ
; #[local] zoo_G_G₀ :: ZooG₀ Σ
; zoo_G_headers_name : ghost_heap_name
; zoo_G_heap_name : gname
; zoo_G_prophets_name : gname
; zoo_G_steps_name : gname
; zoo_G_locals_name : gname
; zoo_G_counter_name : gname
}.
#[global] Arguments Build_ZooG {_ _ _} _ _ _ _ _ _ : assert.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition headers_auth' γ_headers hdrs :=
ghost_heap_auth γ_headers hdrs.
#[local] Definition headers_at' γ_headers l hdr :=
ghost_heap_at γ_headers l DfracDiscarded hdr.
#[local] Definition meta_token' γ_headers l E :=
ghost_heap_meta_token γ_headers l E.
#[local] Definition meta' `{Countable A} γ_headers l ι (x : A) :=
ghost_heap_meta γ_headers l ι x.
#[local] Lemma headers_alloc hdrs :
⊢ |==>
∃ γ_headers,
headers_auth' γ_headers hdrs.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition headers_auth :=
headers_auth' zoo_G_headers_name.
Definition headers_at :=
headers_at' zoo_G_headers_name.
Definition meta_token :=
meta_token' zoo_G_headers_name.
Definition meta `{Countable A} :=
meta' (A := A) zoo_G_headers_name.
End zoo_G.
Notation "l ↦ₕ hdr" := (
headers_at l hdr
)(at level 20,
format "l ↦ₕ hdr"
) : bi_scope.
Notation "l ↪[ ι ] x" := (
meta l ι x
)(at level 20,
format "l ↪[ ι ] x"
) : bi_scope.
Notation "l ↪ x" := (
meta l nroot x
)(at level 20,
format "l ↪ x"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance headers_at_timeless l hdr :
Timeless (l ↦ₕ hdr).
#[global] Instance headers_at_persistent l hdr :
Persistent (l ↦ₕ hdr).
Lemma headers_at_agree l hdr1 hdr2 :
l ↦ₕ hdr1 -∗
l ↦ₕ hdr2 -∗
⌜hdr1 = hdr2⌝.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance meta_token_timeless l N :
Timeless (meta_token l N).
#[global] Instance meta_timeless `{Countable A} l ι (x : A) :
Timeless (l ↪[ι] x).
#[global] Instance meta_persistent `{Countable A} l ι (x : A) :
Persistent (l ↪[ι] x).
Lemma meta_token_difference {l} E1 E2 :
E1 ⊆ E2 →
meta_token l E2 ⊣⊢
meta_token l E1 ∗
meta_token l (E2 ∖ E1).
Lemma meta_set `{Countable A} {l E} (x : A) ι :
↑ ι ⊆ E →
meta_token l E ⊢ |==>
l ↪[ι] x.
Lemma meta_agree `{Countable A} l ι (x1 x2 : A) :
l ↪[ι] x1 -∗
l ↪[ι] x2 -∗
⌜x1 = x2⌝.
Lemma headers_lookup hdrs l hdr :
headers_auth hdrs -∗
l ↦ₕ hdr -∗
⌜hdrs !! l = Some hdr⌝.
Lemma headers_insert {hdrs} l hdr :
hdrs !! l = None →
headers_auth hdrs ⊢ |==>
headers_auth (<[l := hdr]> hdrs) ∗
l ↦ₕ hdr ∗
meta_token l ⊤.
End zoo_G.
#[global] Opaque headers_auth'.
#[global] Opaque headers_at'.
#[global] Opaque meta_token'.
#[global] Opaque meta'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition heap_auth' γ_heap h :=
ghost_map_auth (V := val) γ_heap 1 h.
#[local] Definition pointsto' γ_heap l dq v :=
ghost_map_elem (V := val) γ_heap l dq v.
#[local] Lemma heap_alloc h :
⊢ |==>
∃ γ_heap,
heap_auth' γ_heap h ∗
[∗ map] l ↦ v ∈ h, pointsto' γ_heap l (DfracOwn 1) v.
End zoo_G₀.
Section cheriot_G.
Context `{zoo_G : !ZooG Σ}.
Definition heap_auth :=
heap_auth' zoo_G_heap_name.
Definition pointsto :=
pointsto' zoo_G_heap_name.
End cheriot_G.
Notation "l ↦ dq v" := (
pointsto l dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "l ↦ dq v"
) : bi_scope.
Notation "l ↦-" := (
(∃ v, l ↦ v)%I
)(at level 20,
format "l ↦-"
) : bi_scope.
Notation "l ↦∗ dq vs" :=
([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I
( at level 20,
dq custom dfrac at level 1,
format "l ↦∗ dq vs"
) : bi_scope.
Notation "l ↦∗-" :=
(∃ vs, l ↦∗ vs)%I
( at level 20,
format "l ↦∗-"
) : bi_scope.
Notation "l ↦ᵣ dq v" := (
pointsto (location_add l (Z.of_nat (in_type "@ref" 0))) dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "l ↦ᵣ dq v"
) : bi_scope.
Notation "l ↦ᵣ-" := (
(∃ v, l ↦ᵣ v)%I
)(at level 20,
format "l ↦ᵣ-"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance pointsto_timeless l dq v :
Timeless (l ↦{dq} v).
#[global] Instance pointsto_persistent l v :
Persistent (l ↦□ v).
#[global] Instance pointsto_fractional l v :
Fractional (λ q, l ↦{#q} v)%I.
#[global] Instance pointsto_as_fractional l q v :
AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
Lemma pointsto_valid l dq v :
l ↦{dq} v ⊢
⌜✓ dq⌝.
Lemma pointsto_combine l dq1 v1 dq2 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜v1 = v2⌝ ∗
l ↦{dq1 ⋅ dq2} v1.
Lemma pointsto_valid_2 l dq1 v1 dq2 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma pointsto_agree l dq2 v1 dq1 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜v1 = v2⌝.
Lemma pointsto_dfrac_ne l1 dq1 v1 l2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
l1 ↦{dq1} v1 -∗
l2 ↦{dq2} v2 -∗
⌜l1 ≠ l2⌝.
Lemma pointsto_ne l1 v1 l2 dq2 v2 :
l1 ↦ v1 -∗
l2 ↦{dq2} v2 -∗
⌜l1 ≠ l2⌝.
Lemma pointsto_exclusive l v1 dq2 v2 :
l ↦ v1 -∗
l ↦{dq2} v2 -∗
False.
Lemma pointsto_persist l dq v :
l ↦{dq} v ⊢ |==>
l ↦□ v.
#[global] Instance pointsto_combine_sep_gives l dq1 v1 dq2 v2 :
CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝
| 30.
#[global] Instance pointsto_combine_as l dq1 dq2 v1 v2 :
CombineSepAs (l ↦{dq1} v1) (l ↦{dq2} v2) (l ↦{dq1 ⋅ dq2} v1)
| 60.
#[global] Instance frame_pointsto p l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v)
| 5.
Lemma heap_lookup h a dq c :
heap_auth h -∗
a ↦{dq} c -∗
⌜h !! a = Some c⌝.
Lemma heap_insert {h1} h2 :
h2 ##ₘ h1 →
heap_auth h1 ⊢ |==>
heap_auth (h2 ∪ h1) ∗
[∗ map] l ↦ v ∈ h2, l ↦ v.
Lemma heap_update {h a c1} c2 :
heap_auth h -∗
a ↦ c1 ==∗
heap_auth (<[a := c2]> h) ∗
a ↦ c2.
End zoo_G.
#[global] Opaque heap_auth'.
#[global] Opaque pointsto'.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma big_sepL2_pointsto_agree ls dq1 vs1 dq2 vs2 :
([∗ list] l; v ∈ ls; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls; vs2, l ↦{dq2} v) -∗
⌜vs1 = vs2⌝.
Lemma big_sepL2_ref_pointsto_agree ls dq1 vs1 dq2 vs2 :
([∗ list] l; v ∈ ls; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 = vs2⌝.
Lemma big_sepL2_pointsto_prefix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `prefix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦{dq2} v) -∗
⌜vs1 `prefix_of` vs2⌝.
Lemma big_sepL2_ref_pointsto_prefix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `prefix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 `prefix_of` vs2⌝.
Lemma big_sepL2_pointsto_suffix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `suffix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦{dq2} v) -∗
⌜vs1 `suffix_of` vs2⌝.
Lemma big_sepL2_ref_pointsto_suffix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `suffix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 `suffix_of` vs2⌝.
End zoo_G.
Section resolve_prophecies.
#[local] Fixpoint resolve_prophecies κs pid :=
match κs with
| [] ⇒
[]
| κ :: κs ⇒
if decide (pid = κ.1) then
κ.2 :: resolve_prophecies κs pid
else
resolve_prophecies κs pid
end.
#[local] Definition resolve_prophets prophets κs :=
map_Forall (λ pid prophs, prophs = resolve_prophecies κs pid) prophets.
#[local] Lemma resolve_prophets_insert κs pid prophets :
resolve_prophets prophets κs →
pid ∉ dom prophets →
resolve_prophets (<[pid := resolve_prophecies κs pid]> prophets) κs.
End resolve_prophecies.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition prophets_auth' γ_prophets κs pids : iProp Σ :=
∃ prophets,
⌜resolve_prophets prophets κs⌝ ∗
⌜dom prophets ⊆ pids⌝ ∗
ghost_map_auth γ_prophets 1 prophets.
#[local] Definition prophet_model' γ_prophets pid prophs :=
ghost_map_elem γ_prophets pid (DfracOwn 1) prophs.
#[local] Lemma prophets_alloc κs pids :
⊢ |==>
∃ γ_prophets,
prophets_auth' γ_prophets κs pids.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition prophets_auth :=
prophets_auth' zoo_G_prophets_name.
Definition prophet_model :=
prophet_model' zoo_G_prophets_name.
#[global] Instance prophet_model_timeless pid prophs :
Timeless (prophet_model pid prophs).
Lemma prophet_model_exclusive pid prophs1 prophs2 :
prophet_model pid prophs1 -∗
prophet_model pid prophs2 -∗
False.
Lemma prophets_new {κs pids} pid :
pid ∉ pids →
prophets_auth κs pids ⊢ |==>
∃ prophs,
prophets_auth κs ({[pid]} ∪ pids) ∗
prophet_model pid prophs.
Lemma prophets_resolve pid proph κs pids prophs :
prophets_auth ((pid, proph) :: κs) pids -∗
prophet_model pid prophs ==∗
∃ prophs',
⌜prophs = proph :: prophs'⌝ ∗
prophets_auth κs pids ∗
prophet_model pid prophs'.
End zoo_G.
#[global] Opaque prophets_auth'.
#[global] Opaque prophet_model'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition steps_auth' γ_steps :=
auth_nat_max_auth γ_steps (DfracOwn 1).
#[local] Definition steps_lb' :=
auth_nat_max_lb.
#[local] Lemma steps_alloc :
⊢ |==>
∃ γ_steps,
steps_auth' γ_steps 0.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition steps_auth :=
steps_auth' zoo_G_steps_name.
Definition steps_lb :=
auth_nat_max_lb zoo_G_steps_name.
End zoo_G.
Notation "⧖ n" := (
steps_lb n
)(at level 1,
format "⧖ n"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance steps_auth_timeless ns :
Timeless (steps_auth ns).
#[global] Instance steps_lb_timeless ns :
Timeless (⧖ ns).
#[global] Instance steps_lb_persistent ns :
Persistent (⧖ ns).
Lemma steps_lb_0 :
⊢ |==>
⧖ 0.
Lemma steps_lb_le ns1 ns2 :
ns2 ≤ ns1 →
⧖ ns1 ⊢
⧖ ns2.
Lemma steps_lb_max ns1 ns2 :
⧖ ns1 -∗
⧖ ns2 -∗
⧖ (ns1 `max` ns2).
Lemma steps_lb_get ns :
steps_auth ns ⊢
⧖ ns.
Lemma steps_lb_valid ns1 ns2 :
steps_auth ns1 -∗
⧖ ns2 -∗
⌜ns2 ≤ ns1⌝.
Lemma steps_update ns :
steps_auth ns ⊢ |==>
steps_auth (S ns).
#[global] Instance hint_steps_lb_le ns1 ns2 :
SolveSepSideCondition (ns1 ≤ ns2) →
HINT
⧖ ns2
✱ [- ;
emp
] ⊫ [id];
⧖ ns1
✱ [
emp
]
| 60.
#[global] Instance merge_steps_lbs ns1 ns2 :
MergableConsume (⧖ ns1) true (λ p Pin Pout,
TCAnd (
TCEq Pin (⧖ ns2)%I
) (
TCEq Pout (⧖ (ns1 `max` ns2))%I
)
).
End zoo_G.
#[global] Opaque steps_auth'.
#[global] Opaque steps_lb'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition locals_auth' γ_locals vs :=
ghost_list_auth γ_locals vs.
#[local] Definition local_pointsto' γ_locals tid dq v :=
ghost_list_at γ_locals tid dq v.
#[local] Lemma locals_alloc vs :
⊢ |==>
∃ γ_locals,
locals_auth' γ_locals vs ∗
[∗ list] tid ↦ v ∈ vs, local_pointsto' γ_locals tid (DfracOwn 1) v.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition locals_auth :=
locals_auth' zoo_G_locals_name.
Definition local_pointsto :=
local_pointsto' zoo_G_locals_name.
End zoo_G.
Notation "tid ↦ₗ dq v" := (
local_pointsto tid dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "tid ↦ₗ dq v"
) : bi_scope.
Notation "tid ↦ₗ-" := (
(∃ v, tid ↦ₗ v)%I
)(at level 20,
format "tid ↦ₗ-"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance local_pointsto_timeless tid dq v :
Timeless (tid ↦ₗ{dq} v).
#[global] Instance local_pointsto_persistent tid v :
Persistent (tid ↦ₗ□ v).
#[global] Instance local_pointsto_fractional tid v :
Fractional (λ q, tid ↦ₗ{#q} v)%I.
#[global] Instance local_pointsto_as_fractional tid q v :
AsFractional (tid ↦ₗ{#q} v) (λ q, tid ↦ₗ{#q} v)%I q.
Lemma local_pointsto_valid tid dq v :
tid ↦ₗ{dq} v ⊢
⌜✓ dq⌝.
Lemma local_pointsto_combine tid dq1 v1 dq2 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜v1 = v2⌝ ∗
tid ↦ₗ{dq1 ⋅ dq2} v1.
Lemma local_pointsto_valid_2 tid dq1 v1 dq2 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma local_pointsto_agree tid dq2 v1 dq1 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜v1 = v2⌝.
Lemma local_pointsto_dfrac_ne tid1 dq1 v1 tid2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
tid1 ↦ₗ{dq1} v1 -∗
tid2 ↦ₗ{dq2} v2 -∗
⌜tid1 ≠ tid2⌝.
Lemma local_pointsto_ne tid1 v1 tid2 dq2 v2 :
tid1 ↦ₗ v1 -∗
tid2 ↦ₗ{dq2} v2 -∗
⌜tid1 ≠ tid2⌝.
Lemma local_pointsto_exclusive tid v1 dq2 v2 :
tid ↦ₗ v1 -∗
tid ↦ₗ{dq2} v2 -∗
False.
Lemma local_pointsto_persist tid dq v :
tid ↦ₗ{dq} v ⊢ |==>
tid ↦ₗ□ v.
Lemma locals_lookup vs tid dq v :
locals_auth vs -∗
tid ↦ₗ{dq} v -∗
⌜vs !! tid = Some v⌝.
Lemma locals_update_push {vs} v :
locals_auth vs ⊢ |==>
locals_auth (vs ++ [v]) ∗
length vs ↦ₗ v.
Lemma locals_update_pointsto {vs tid v} v' :
locals_auth vs -∗
tid ↦ₗ v ==∗
locals_auth (<[tid := v']> vs) ∗
tid ↦ₗ v'.
End zoo_G.
#[global] Opaque locals_auth'.
#[global] Opaque local_pointsto'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition zoo_counter_auth' γ_counter vs :=
mono_list_auth γ_counter (DfracOwn 1) vs.
#[local] Definition zoo_counter_at' γ_counter id v :=
mono_list_at γ_counter id v.
#[local] Lemma zoo_counter_alloc :
⊢ |==>
∃ γ_counter,
zoo_counter_auth' γ_counter (replicate 0 inhabitant).
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition zoo_counter_auth :=
zoo_counter_auth' zoo_G_counter_name.
Definition zoo_counter_at :=
zoo_counter_at' zoo_G_counter_name.
#[global] Instance zoo_counter_auth_timeless vs :
Timeless (zoo_counter_auth vs).
#[global] Instance zoo_counter_at_timeless id v :
Timeless (zoo_counter_at id v).
#[global] Instance zoo_counter_at_persistent id v :
Persistent (zoo_counter_at id v).
Lemma zoo_counter_at_get {vs} id v :
vs !! id = Some v →
zoo_counter_auth vs ⊢
zoo_counter_at id v.
Lemma zoo_counter_at_valid vs id v :
zoo_counter_auth vs -∗
zoo_counter_at id v -∗
⌜vs !! id = Some v⌝.
Lemma zoo_counter_at_agree id v1 v2 :
zoo_counter_at id v1 -∗
zoo_counter_at id v2 -∗
⌜v1 = v2⌝.
Lemma zoo_counter_update {vs} v :
zoo_counter_auth vs ⊢ |==>
zoo_counter_auth (vs ++ [v]).
End zoo_G.
#[global] Opaque zoo_counter_auth'.
#[global] Opaque zoo_counter_at'.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition zoo_counter_name :=
zoo_G_counter_name.
Definition zoo_counter_inv_inner : iProp Σ :=
∃ cnt vs,
zoo_counter ↦ᵣ #cnt ∗
zoo_counter_auth vs ∗
⌜length vs = cnt⌝.
Definition zoo_counter_inv :=
inv nroot zoo_counter_inv_inner.
End zoo_G.
Lemma zoo_init `{zoo_Gpre : !ZooGpre Σ} `{inv_G : !invGS Σ} hdrs h pids vs κs :
h !! zoo_counter = Some 0%V →
⊢ |={⊤}=>
∃ zoo_G : ZooG Σ,
⌜zoo_G.(zoo_G_inv_G) = inv_G⌝ ∗
headers_auth hdrs ∗
heap_auth h ∗
prophets_auth κs pids ∗
steps_auth 0 ∗
locals_auth vs ∗
zoo_counter_inv ∗
([∗ map] l ↦ v ∈ delete zoo_counter h, l ↦ v) ∗
([∗ list] tid ↦ v ∈ vs, tid ↦ₗ v).
#[global] Opaque headers_auth.
#[global] Opaque headers_at.
#[global] Opaque meta_token.
#[global] Opaque meta.
#[global] Opaque heap_auth.
#[global] Opaque pointsto.
#[global] Opaque prophets_auth.
#[global] Opaque prophet_model.
#[global] Opaque steps_auth.
#[global] Opaque steps_lb.
#[global] Opaque locals_auth.
#[global] Opaque local_pointsto.
#[global] Opaque zoo_counter_auth.
#[global] Opaque zoo_counter_at.
Variant ownership :=
| Own
| Discard.
Coercion ownership_to_dfrac own :=
match own with
| Own ⇒
DfracOwn 1
| Discard ⇒
DfracDiscarded
end.
lib.fractional.
From iris.base_logic Require Import
lib.ghost_map
lib.invariants.
From zoo Require Import
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_nat_max
lib.ghost_heap
lib.ghost_list
lib.mono_list.
From zoo.iris Require Import
diaframe.
From zoo.language Require Export
language.
From zoo.language Require Import
notations.
From zoo Require Import
options.
Implicit Types cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Types tid : thread_id.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types vs : list val.
Implicit Types hdr : header.
Implicit Types hdrs : gmap location header.
Implicit Types σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Types κ κs : list observation.
Parameter zoo_counter : location.
Class ZooG₀ Σ :=
{ #[local] zoo_G₀_headers_G :: GhostHeapG Σ location header
; #[local] zoo_G₀_heap_G :: ghost_mapG Σ location val
; #[local] zoo_G_prophets_G :: ghost_mapG Σ prophet_id (list (val × val))
; #[local] zoo_G₀_steps_G :: AuthNatMaxG Σ
; #[local] zoo_G₀_locals_G :: GhostListG Σ val
; #[local] zoo_G₀_counter_G :: MonoListG Σ val
}.
#[local] Definition zoo_Σ₀ :=
#[ghost_heap_Σ location header
; ghost_mapΣ location val
; ghost_mapΣ prophet_id (list (val × val))
; auth_nat_max_Σ
; ghost_list_Σ val
; mono_list_Σ val
].
#[local] Instance subG_zoo_Σ₀ Σ :
subG zoo_Σ₀ Σ →
ZooG₀ Σ.
Class ZooGpre Σ :=
{ #[global] zoo_Gpre_inv_Gpre :: invGpreS Σ
; #[local] zoo_Gpre_G₀ :: ZooG₀ Σ
}.
Definition zoo_Σ :=
#[invΣ
; zoo_Σ₀
].
#[global] Instance subG_zoo_Σ Σ :
subG zoo_Σ Σ →
ZooGpre Σ.
Class ZooG Σ :=
{ #[global] zoo_G_inv_G :: invGS Σ
; #[local] zoo_G_G₀ :: ZooG₀ Σ
; zoo_G_headers_name : ghost_heap_name
; zoo_G_heap_name : gname
; zoo_G_prophets_name : gname
; zoo_G_steps_name : gname
; zoo_G_locals_name : gname
; zoo_G_counter_name : gname
}.
#[global] Arguments Build_ZooG {_ _ _} _ _ _ _ _ _ : assert.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition headers_auth' γ_headers hdrs :=
ghost_heap_auth γ_headers hdrs.
#[local] Definition headers_at' γ_headers l hdr :=
ghost_heap_at γ_headers l DfracDiscarded hdr.
#[local] Definition meta_token' γ_headers l E :=
ghost_heap_meta_token γ_headers l E.
#[local] Definition meta' `{Countable A} γ_headers l ι (x : A) :=
ghost_heap_meta γ_headers l ι x.
#[local] Lemma headers_alloc hdrs :
⊢ |==>
∃ γ_headers,
headers_auth' γ_headers hdrs.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition headers_auth :=
headers_auth' zoo_G_headers_name.
Definition headers_at :=
headers_at' zoo_G_headers_name.
Definition meta_token :=
meta_token' zoo_G_headers_name.
Definition meta `{Countable A} :=
meta' (A := A) zoo_G_headers_name.
End zoo_G.
Notation "l ↦ₕ hdr" := (
headers_at l hdr
)(at level 20,
format "l ↦ₕ hdr"
) : bi_scope.
Notation "l ↪[ ι ] x" := (
meta l ι x
)(at level 20,
format "l ↪[ ι ] x"
) : bi_scope.
Notation "l ↪ x" := (
meta l nroot x
)(at level 20,
format "l ↪ x"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance headers_at_timeless l hdr :
Timeless (l ↦ₕ hdr).
#[global] Instance headers_at_persistent l hdr :
Persistent (l ↦ₕ hdr).
Lemma headers_at_agree l hdr1 hdr2 :
l ↦ₕ hdr1 -∗
l ↦ₕ hdr2 -∗
⌜hdr1 = hdr2⌝.
End zoo_G.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance meta_token_timeless l N :
Timeless (meta_token l N).
#[global] Instance meta_timeless `{Countable A} l ι (x : A) :
Timeless (l ↪[ι] x).
#[global] Instance meta_persistent `{Countable A} l ι (x : A) :
Persistent (l ↪[ι] x).
Lemma meta_token_difference {l} E1 E2 :
E1 ⊆ E2 →
meta_token l E2 ⊣⊢
meta_token l E1 ∗
meta_token l (E2 ∖ E1).
Lemma meta_set `{Countable A} {l E} (x : A) ι :
↑ ι ⊆ E →
meta_token l E ⊢ |==>
l ↪[ι] x.
Lemma meta_agree `{Countable A} l ι (x1 x2 : A) :
l ↪[ι] x1 -∗
l ↪[ι] x2 -∗
⌜x1 = x2⌝.
Lemma headers_lookup hdrs l hdr :
headers_auth hdrs -∗
l ↦ₕ hdr -∗
⌜hdrs !! l = Some hdr⌝.
Lemma headers_insert {hdrs} l hdr :
hdrs !! l = None →
headers_auth hdrs ⊢ |==>
headers_auth (<[l := hdr]> hdrs) ∗
l ↦ₕ hdr ∗
meta_token l ⊤.
End zoo_G.
#[global] Opaque headers_auth'.
#[global] Opaque headers_at'.
#[global] Opaque meta_token'.
#[global] Opaque meta'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition heap_auth' γ_heap h :=
ghost_map_auth (V := val) γ_heap 1 h.
#[local] Definition pointsto' γ_heap l dq v :=
ghost_map_elem (V := val) γ_heap l dq v.
#[local] Lemma heap_alloc h :
⊢ |==>
∃ γ_heap,
heap_auth' γ_heap h ∗
[∗ map] l ↦ v ∈ h, pointsto' γ_heap l (DfracOwn 1) v.
End zoo_G₀.
Section cheriot_G.
Context `{zoo_G : !ZooG Σ}.
Definition heap_auth :=
heap_auth' zoo_G_heap_name.
Definition pointsto :=
pointsto' zoo_G_heap_name.
End cheriot_G.
Notation "l ↦ dq v" := (
pointsto l dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "l ↦ dq v"
) : bi_scope.
Notation "l ↦-" := (
(∃ v, l ↦ v)%I
)(at level 20,
format "l ↦-"
) : bi_scope.
Notation "l ↦∗ dq vs" :=
([∗ list] i ↦ v ∈ vs, (l +ₗ i) ↦{dq} v)%I
( at level 20,
dq custom dfrac at level 1,
format "l ↦∗ dq vs"
) : bi_scope.
Notation "l ↦∗-" :=
(∃ vs, l ↦∗ vs)%I
( at level 20,
format "l ↦∗-"
) : bi_scope.
Notation "l ↦ᵣ dq v" := (
pointsto (location_add l (Z.of_nat (in_type "@ref" 0))) dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "l ↦ᵣ dq v"
) : bi_scope.
Notation "l ↦ᵣ-" := (
(∃ v, l ↦ᵣ v)%I
)(at level 20,
format "l ↦ᵣ-"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance pointsto_timeless l dq v :
Timeless (l ↦{dq} v).
#[global] Instance pointsto_persistent l v :
Persistent (l ↦□ v).
#[global] Instance pointsto_fractional l v :
Fractional (λ q, l ↦{#q} v)%I.
#[global] Instance pointsto_as_fractional l q v :
AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
Lemma pointsto_valid l dq v :
l ↦{dq} v ⊢
⌜✓ dq⌝.
Lemma pointsto_combine l dq1 v1 dq2 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜v1 = v2⌝ ∗
l ↦{dq1 ⋅ dq2} v1.
Lemma pointsto_valid_2 l dq1 v1 dq2 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma pointsto_agree l dq2 v1 dq1 v2 :
l ↦{dq1} v1 -∗
l ↦{dq2} v2 -∗
⌜v1 = v2⌝.
Lemma pointsto_dfrac_ne l1 dq1 v1 l2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
l1 ↦{dq1} v1 -∗
l2 ↦{dq2} v2 -∗
⌜l1 ≠ l2⌝.
Lemma pointsto_ne l1 v1 l2 dq2 v2 :
l1 ↦ v1 -∗
l2 ↦{dq2} v2 -∗
⌜l1 ≠ l2⌝.
Lemma pointsto_exclusive l v1 dq2 v2 :
l ↦ v1 -∗
l ↦{dq2} v2 -∗
False.
Lemma pointsto_persist l dq v :
l ↦{dq} v ⊢ |==>
l ↦□ v.
#[global] Instance pointsto_combine_sep_gives l dq1 v1 dq2 v2 :
CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝
| 30.
#[global] Instance pointsto_combine_as l dq1 dq2 v1 v2 :
CombineSepAs (l ↦{dq1} v1) (l ↦{dq2} v2) (l ↦{dq1 ⋅ dq2} v1)
| 60.
#[global] Instance frame_pointsto p l v q1 q2 q :
FrameFractionalQp q1 q2 q →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v)
| 5.
Lemma heap_lookup h a dq c :
heap_auth h -∗
a ↦{dq} c -∗
⌜h !! a = Some c⌝.
Lemma heap_insert {h1} h2 :
h2 ##ₘ h1 →
heap_auth h1 ⊢ |==>
heap_auth (h2 ∪ h1) ∗
[∗ map] l ↦ v ∈ h2, l ↦ v.
Lemma heap_update {h a c1} c2 :
heap_auth h -∗
a ↦ c1 ==∗
heap_auth (<[a := c2]> h) ∗
a ↦ c2.
End zoo_G.
#[global] Opaque heap_auth'.
#[global] Opaque pointsto'.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Lemma big_sepL2_pointsto_agree ls dq1 vs1 dq2 vs2 :
([∗ list] l; v ∈ ls; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls; vs2, l ↦{dq2} v) -∗
⌜vs1 = vs2⌝.
Lemma big_sepL2_ref_pointsto_agree ls dq1 vs1 dq2 vs2 :
([∗ list] l; v ∈ ls; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 = vs2⌝.
Lemma big_sepL2_pointsto_prefix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `prefix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦{dq2} v) -∗
⌜vs1 `prefix_of` vs2⌝.
Lemma big_sepL2_ref_pointsto_prefix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `prefix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 `prefix_of` vs2⌝.
Lemma big_sepL2_pointsto_suffix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `suffix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦{dq2} v) -∗
⌜vs1 `suffix_of` vs2⌝.
Lemma big_sepL2_ref_pointsto_suffix ls1 dq1 vs1 ls2 dq2 vs2 :
ls1 `suffix_of` ls2 →
([∗ list] l; v ∈ ls1; vs1, l ↦ᵣ{dq1} v) -∗
([∗ list] l; v ∈ ls2; vs2, l ↦ᵣ{dq2} v) -∗
⌜vs1 `suffix_of` vs2⌝.
End zoo_G.
Section resolve_prophecies.
#[local] Fixpoint resolve_prophecies κs pid :=
match κs with
| [] ⇒
[]
| κ :: κs ⇒
if decide (pid = κ.1) then
κ.2 :: resolve_prophecies κs pid
else
resolve_prophecies κs pid
end.
#[local] Definition resolve_prophets prophets κs :=
map_Forall (λ pid prophs, prophs = resolve_prophecies κs pid) prophets.
#[local] Lemma resolve_prophets_insert κs pid prophets :
resolve_prophets prophets κs →
pid ∉ dom prophets →
resolve_prophets (<[pid := resolve_prophecies κs pid]> prophets) κs.
End resolve_prophecies.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition prophets_auth' γ_prophets κs pids : iProp Σ :=
∃ prophets,
⌜resolve_prophets prophets κs⌝ ∗
⌜dom prophets ⊆ pids⌝ ∗
ghost_map_auth γ_prophets 1 prophets.
#[local] Definition prophet_model' γ_prophets pid prophs :=
ghost_map_elem γ_prophets pid (DfracOwn 1) prophs.
#[local] Lemma prophets_alloc κs pids :
⊢ |==>
∃ γ_prophets,
prophets_auth' γ_prophets κs pids.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition prophets_auth :=
prophets_auth' zoo_G_prophets_name.
Definition prophet_model :=
prophet_model' zoo_G_prophets_name.
#[global] Instance prophet_model_timeless pid prophs :
Timeless (prophet_model pid prophs).
Lemma prophet_model_exclusive pid prophs1 prophs2 :
prophet_model pid prophs1 -∗
prophet_model pid prophs2 -∗
False.
Lemma prophets_new {κs pids} pid :
pid ∉ pids →
prophets_auth κs pids ⊢ |==>
∃ prophs,
prophets_auth κs ({[pid]} ∪ pids) ∗
prophet_model pid prophs.
Lemma prophets_resolve pid proph κs pids prophs :
prophets_auth ((pid, proph) :: κs) pids -∗
prophet_model pid prophs ==∗
∃ prophs',
⌜prophs = proph :: prophs'⌝ ∗
prophets_auth κs pids ∗
prophet_model pid prophs'.
End zoo_G.
#[global] Opaque prophets_auth'.
#[global] Opaque prophet_model'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition steps_auth' γ_steps :=
auth_nat_max_auth γ_steps (DfracOwn 1).
#[local] Definition steps_lb' :=
auth_nat_max_lb.
#[local] Lemma steps_alloc :
⊢ |==>
∃ γ_steps,
steps_auth' γ_steps 0.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition steps_auth :=
steps_auth' zoo_G_steps_name.
Definition steps_lb :=
auth_nat_max_lb zoo_G_steps_name.
End zoo_G.
Notation "⧖ n" := (
steps_lb n
)(at level 1,
format "⧖ n"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance steps_auth_timeless ns :
Timeless (steps_auth ns).
#[global] Instance steps_lb_timeless ns :
Timeless (⧖ ns).
#[global] Instance steps_lb_persistent ns :
Persistent (⧖ ns).
Lemma steps_lb_0 :
⊢ |==>
⧖ 0.
Lemma steps_lb_le ns1 ns2 :
ns2 ≤ ns1 →
⧖ ns1 ⊢
⧖ ns2.
Lemma steps_lb_max ns1 ns2 :
⧖ ns1 -∗
⧖ ns2 -∗
⧖ (ns1 `max` ns2).
Lemma steps_lb_get ns :
steps_auth ns ⊢
⧖ ns.
Lemma steps_lb_valid ns1 ns2 :
steps_auth ns1 -∗
⧖ ns2 -∗
⌜ns2 ≤ ns1⌝.
Lemma steps_update ns :
steps_auth ns ⊢ |==>
steps_auth (S ns).
#[global] Instance hint_steps_lb_le ns1 ns2 :
SolveSepSideCondition (ns1 ≤ ns2) →
HINT
⧖ ns2
✱ [- ;
emp
] ⊫ [id];
⧖ ns1
✱ [
emp
]
| 60.
#[global] Instance merge_steps_lbs ns1 ns2 :
MergableConsume (⧖ ns1) true (λ p Pin Pout,
TCAnd (
TCEq Pin (⧖ ns2)%I
) (
TCEq Pout (⧖ (ns1 `max` ns2))%I
)
).
End zoo_G.
#[global] Opaque steps_auth'.
#[global] Opaque steps_lb'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition locals_auth' γ_locals vs :=
ghost_list_auth γ_locals vs.
#[local] Definition local_pointsto' γ_locals tid dq v :=
ghost_list_at γ_locals tid dq v.
#[local] Lemma locals_alloc vs :
⊢ |==>
∃ γ_locals,
locals_auth' γ_locals vs ∗
[∗ list] tid ↦ v ∈ vs, local_pointsto' γ_locals tid (DfracOwn 1) v.
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition locals_auth :=
locals_auth' zoo_G_locals_name.
Definition local_pointsto :=
local_pointsto' zoo_G_locals_name.
End zoo_G.
Notation "tid ↦ₗ dq v" := (
local_pointsto tid dq v%V
)(at level 20,
dq custom dfrac at level 1,
format "tid ↦ₗ dq v"
) : bi_scope.
Notation "tid ↦ₗ-" := (
(∃ v, tid ↦ₗ v)%I
)(at level 20,
format "tid ↦ₗ-"
) : bi_scope.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance local_pointsto_timeless tid dq v :
Timeless (tid ↦ₗ{dq} v).
#[global] Instance local_pointsto_persistent tid v :
Persistent (tid ↦ₗ□ v).
#[global] Instance local_pointsto_fractional tid v :
Fractional (λ q, tid ↦ₗ{#q} v)%I.
#[global] Instance local_pointsto_as_fractional tid q v :
AsFractional (tid ↦ₗ{#q} v) (λ q, tid ↦ₗ{#q} v)%I q.
Lemma local_pointsto_valid tid dq v :
tid ↦ₗ{dq} v ⊢
⌜✓ dq⌝.
Lemma local_pointsto_combine tid dq1 v1 dq2 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜v1 = v2⌝ ∗
tid ↦ₗ{dq1 ⋅ dq2} v1.
Lemma local_pointsto_valid_2 tid dq1 v1 dq2 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma local_pointsto_agree tid dq2 v1 dq1 v2 :
tid ↦ₗ{dq1} v1 -∗
tid ↦ₗ{dq2} v2 -∗
⌜v1 = v2⌝.
Lemma local_pointsto_dfrac_ne tid1 dq1 v1 tid2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
tid1 ↦ₗ{dq1} v1 -∗
tid2 ↦ₗ{dq2} v2 -∗
⌜tid1 ≠ tid2⌝.
Lemma local_pointsto_ne tid1 v1 tid2 dq2 v2 :
tid1 ↦ₗ v1 -∗
tid2 ↦ₗ{dq2} v2 -∗
⌜tid1 ≠ tid2⌝.
Lemma local_pointsto_exclusive tid v1 dq2 v2 :
tid ↦ₗ v1 -∗
tid ↦ₗ{dq2} v2 -∗
False.
Lemma local_pointsto_persist tid dq v :
tid ↦ₗ{dq} v ⊢ |==>
tid ↦ₗ□ v.
Lemma locals_lookup vs tid dq v :
locals_auth vs -∗
tid ↦ₗ{dq} v -∗
⌜vs !! tid = Some v⌝.
Lemma locals_update_push {vs} v :
locals_auth vs ⊢ |==>
locals_auth (vs ++ [v]) ∗
length vs ↦ₗ v.
Lemma locals_update_pointsto {vs tid v} v' :
locals_auth vs -∗
tid ↦ₗ v ==∗
locals_auth (<[tid := v']> vs) ∗
tid ↦ₗ v'.
End zoo_G.
#[global] Opaque locals_auth'.
#[global] Opaque local_pointsto'.
Section zoo_G₀.
Context `{zoo_G₀ : !ZooG₀ Σ}.
#[local] Definition zoo_counter_auth' γ_counter vs :=
mono_list_auth γ_counter (DfracOwn 1) vs.
#[local] Definition zoo_counter_at' γ_counter id v :=
mono_list_at γ_counter id v.
#[local] Lemma zoo_counter_alloc :
⊢ |==>
∃ γ_counter,
zoo_counter_auth' γ_counter (replicate 0 inhabitant).
End zoo_G₀.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition zoo_counter_auth :=
zoo_counter_auth' zoo_G_counter_name.
Definition zoo_counter_at :=
zoo_counter_at' zoo_G_counter_name.
#[global] Instance zoo_counter_auth_timeless vs :
Timeless (zoo_counter_auth vs).
#[global] Instance zoo_counter_at_timeless id v :
Timeless (zoo_counter_at id v).
#[global] Instance zoo_counter_at_persistent id v :
Persistent (zoo_counter_at id v).
Lemma zoo_counter_at_get {vs} id v :
vs !! id = Some v →
zoo_counter_auth vs ⊢
zoo_counter_at id v.
Lemma zoo_counter_at_valid vs id v :
zoo_counter_auth vs -∗
zoo_counter_at id v -∗
⌜vs !! id = Some v⌝.
Lemma zoo_counter_at_agree id v1 v2 :
zoo_counter_at id v1 -∗
zoo_counter_at id v2 -∗
⌜v1 = v2⌝.
Lemma zoo_counter_update {vs} v :
zoo_counter_auth vs ⊢ |==>
zoo_counter_auth (vs ++ [v]).
End zoo_G.
#[global] Opaque zoo_counter_auth'.
#[global] Opaque zoo_counter_at'.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
Definition zoo_counter_name :=
zoo_G_counter_name.
Definition zoo_counter_inv_inner : iProp Σ :=
∃ cnt vs,
zoo_counter ↦ᵣ #cnt ∗
zoo_counter_auth vs ∗
⌜length vs = cnt⌝.
Definition zoo_counter_inv :=
inv nroot zoo_counter_inv_inner.
End zoo_G.
Lemma zoo_init `{zoo_Gpre : !ZooGpre Σ} `{inv_G : !invGS Σ} hdrs h pids vs κs :
h !! zoo_counter = Some 0%V →
⊢ |={⊤}=>
∃ zoo_G : ZooG Σ,
⌜zoo_G.(zoo_G_inv_G) = inv_G⌝ ∗
headers_auth hdrs ∗
heap_auth h ∗
prophets_auth κs pids ∗
steps_auth 0 ∗
locals_auth vs ∗
zoo_counter_inv ∗
([∗ map] l ↦ v ∈ delete zoo_counter h, l ↦ v) ∗
([∗ list] tid ↦ v ∈ vs, tid ↦ₗ v).
#[global] Opaque headers_auth.
#[global] Opaque headers_at.
#[global] Opaque meta_token.
#[global] Opaque meta.
#[global] Opaque heap_auth.
#[global] Opaque pointsto.
#[global] Opaque prophets_auth.
#[global] Opaque prophet_model.
#[global] Opaque steps_auth.
#[global] Opaque steps_lb.
#[global] Opaque locals_auth.
#[global] Opaque local_pointsto.
#[global] Opaque zoo_counter_auth.
#[global] Opaque zoo_counter_at.
Variant ownership :=
| Own
| Discard.
Coercion ownership_to_dfrac own :=
match own with
| Own ⇒
DfracOwn 1
| Discard ⇒
DfracDiscarded
end.