Library zoo_std.domain
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
list
fin_maps.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
counter.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
domain__code.
From zoo_std Require Import
option
ivar_2
dynarray_1.
From zoo Require Import
options.
Implicit Types id : nat.
Implicit Types l : location.
Implicit Types t fn key : val.
Implicit Types vs : list (option val).
Implicit Types ws : gmap nat (option val).
Implicit Types ids : gmap val nat.
#[local] Notation "'id'" := (
in_type "key" 0
)(in custom zoo_proj
).
#[local] Notation "'init'" := (
in_type "key" 1
)(in custom zoo_proj
).
Definition domain٠spawn : val :=
fun: "fn" ⇒
let: "t" := ivar_2٠create () in
Fork (
let: "local" := dynarray_1٠create () in
SetLocal "local" ;;
ivar_2٠set "t" ("fn" ())
) ;;
"t".
Definition domain٠join : val :=
ivar_2٠get.
Definition domain٠local_new : val :=
fun: "fn" ⇒
let: "id" := zoo_counter٠incr () in
("id", "fn").
Definition domain٠key_id : val :=
fun: "key" ⇒
"key".<id>.
Definition domain٠key_init : val :=
fun: "key" ⇒
"key".<init> ().
Definition domain٠local_get : val :=
fun: "key" ⇒
let: "local" := GetLocal in
let: "id" := domain٠key_id "key" in
dynarray_1٠grow "local" ("id" + 1) §None ;;
match: dynarray_1٠get "local" "id" with
| None ⇒
let: "v" := domain٠key_init "key" in
dynarray_1٠set "local" "id" ‘Some( "v" ) ;;
"v"
| Some "v" ⇒
"v"
end.
Definition domain٠local_set : val :=
fun: "key" "v" ⇒
let: "local" := GetLocal in
let: "id" := domain٠key_id "key" in
dynarray_1٠grow "local" ("id" + 1) §None ;;
dynarray_1٠set "local" "id" ‘Some( "v" ).
Class DomainG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] domain_G_ivar_G :: Ivar2G Σ
; #[local] domain_G_locals_G :: ghost_mapG Σ nat (option val)
}.
Definition domain_Σ :=
#[ivar_2_Σ
; ghost_mapΣ nat (option val)
].
#[global] Instance subG_domain_Σ Σ `{zoo_G : !ZooG Σ} :
subG domain_Σ Σ →
DomainG Σ.
#[local] Definition consistent vs ws :=
map_oflatten (map_seq 0 vs) = map_oflatten ws.
#[local] Lemma consistent_app_None vs ws n :
consistent vs ws →
consistent (vs ++ replicate n None) ws.
#[local] Lemma consistent_lookup_None {vs ws} id o :
consistent vs ws →
ws !! id = None →
vs !! id = Some o →
o = None.
#[local] Lemma consistent_lookup_Some_None {vs ws} id :
id < length vs →
consistent vs ws →
ws !! id = Some None →
vs !! id = Some None.
#[local] Lemma consistent_lookup_Some_Some {vs ws} id v :
consistent vs ws →
ws !! id = Some (Some v) →
vs !! id = Some (Some v).
#[local] Lemma consistent_insert {vs ws} id :
ws !! id = None →
consistent vs ws →
consistent vs (<[id := None]> ws).
#[local] Lemma consistent_update {vs ws} id w :
id < length vs →
consistent vs ws →
consistent (<[id := Some w]> vs) (<[id := Some w]> ws).
Opaque consistent.
Section domain_G.
Context `{domain_G : DomainG Σ}.
Implicit Types Ψ : val → iProp Σ.
#[local] Definition local_auth γ :=
ghost_map_auth γ 1.
#[local] Definition local_at :=
ghost_map_elem.
Definition domain_model t Ψ : iProp Σ :=
ivar_2_inv t Ψ (λ _, True)%I ∗
ivar_2_consumer t Ψ.
#[local] Instance : CustomIpat "model" :=
" ( #Hivar_inv & Hivar_consumer ) ".
#[local] Definition key_id key id : iProp Σ :=
∃ fn,
⌜key = (#id, fn)%V⌝ ∗
zoo_counter_at id fn.
#[local] Instance : CustomIpat "key_id" :=
" ( %fn{} & %Heq{} & #Hcounter_at{} ) ".
Definition domain_key key Ψ : iProp Σ :=
∃ id fn,
⌜key = (#id, fn)%V⌝ ∗
zoo_counter_at id fn ∗
□ WP fn () {{ Ψ }}.
#[local] Instance : CustomIpat "key" :=
" ( %id & %fn{} & -> & Hcounter_at & #Hfn{} ) ".
Definition domain_key' key : iProp Σ :=
∃ Ψ,
domain_key key Ψ.
Definition domain_local tid keys : iProp Σ :=
∃ l γ vs ws ids,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
dynarray_1_model #l (option_to_val <$> vs) ∗
local_auth γ ws ∗
⌜dom ids = keys⌝ ∗
⌜map_img ids = dom ws⌝ ∗
([∗ map] key ↦ id ∈ ids, key_id key id) ∗
⌜consistent vs ws⌝.
#[local] Instance : CustomIpat "local" :=
" ( %l & %γ & %vs & %ws & %ids & #Hlocal & #Hl_meta & Hl & Hlocal_auth & %Hids_dom & %Hids_img & Hids & %Hconsistent ) ".
Definition domain_local_init tid key : iProp Σ :=
∃ l γ id,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
key_id key id ∗
local_at γ id (DfracOwn 1) None.
#[local] Instance : CustomIpat "local_init" :=
" ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".
Definition domain_local_pointsto tid key dq v : iProp Σ :=
∃ l γ id,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
key_id key id ∗
local_at γ id dq (Some v).
#[local] Instance : CustomIpat "local_pointsto" :=
" ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".
Definition domain_local_pointstopred tid key Ψ : iProp Σ :=
domain_local_init tid key ∗
domain_key key Ψ
∨ ∃ v,
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v.
#[local] Instance : CustomIpat "local_pointstopred" :=
" [ ( Hinit & Hkey ) | ( % & Hlocal_pointsto & HΨ ) ] ".
#[global] Instance domain_local_timeless tid keys :
Timeless (domain_local tid keys).
#[global] Instance domain_local_init_timeless tid key :
Timeless (domain_local_init tid key).
#[global] Instance domain_local_pointsto_timeless tid key dq v :
Timeless (domain_local_pointsto tid key dq v).
#[local] Instance key_id_persistent key id :
Persistent (key_id key id).
#[global] Instance domain_key_persistent key Ψ :
Persistent (domain_key key Ψ).
#[global] Instance domain_local_pointsto_persistent tid key v :
Persistent (domain_local_pointsto tid key DfracDiscarded v).
#[local] Lemma local_alloc :
⊢ |==>
∃ γ,
local_auth γ ∅.
#[local] Lemma local_at_valid γ ws id dq v :
local_auth γ ws -∗
local_at γ id dq v -∗
⌜ws !! id = Some v⌝.
#[local] Lemma local_insert {γ ws} id :
ws !! id = None →
local_auth γ ws ⊢ |==>
local_auth γ (<[id := None]> ws) ∗
local_at γ id (DfracOwn 1) None.
#[local] Lemma local_update {γ ws id w} w' :
local_auth γ ws -∗
local_at γ id (DfracOwn 1) w ==∗
local_auth γ (<[id := w']> ws) ∗
local_at γ id (DfracOwn 1) w'.
#[local] Lemma key_id_agree key id1 id2 :
key_id key id1 -∗
key_id key id2 -∗
⌜id1 = id2⌝.
#[local] Lemma key_id_inj key1 id1 key2 id2 :
key1 ≠ key2 →
key_id key1 id1 -∗
key_id key2 id2 -∗
⌜id1 ≠ id2⌝.
#[local] Lemma domain_key_to_id key Ψ :
domain_key key Ψ ⊢
∃ id,
key_id key id.
#[local] Lemma domain٠key_id𑁒spec key id :
{{{
key_id key id
}}}
domain٠key_id key
{{{
RET #id;
True
}}}.
#[local] Lemma domain٠key_init𑁒spec key Ψ :
{{{
domain_key key Ψ
}}}
domain٠key_init key
{{{
v
, RET v;
Ψ v
}}}.
Opaque key_id.
Lemma domain_local_get_key {tid keys} key Ψ :
key ∉ keys →
domain_local tid keys -∗
domain_key key Ψ ==∗
domain_local tid (keys ∪ {[key]}) ∗
domain_local_init tid key.
#[global] Instance domain_local_pointsto_fractional tid key v :
Fractional (λ q, domain_local_pointsto tid key (DfracOwn q) v).
#[global] Instance domain_local_pointsto_as_fractional tid key q v :
AsFractional (domain_local_pointsto tid key (DfracOwn q) v) (λ q, domain_local_pointsto tid key (DfracOwn q) v)%I q.
Lemma domain_local_pointsto_valid tid key dq v :
domain_local_pointsto tid key dq v ⊢
⌜✓ dq⌝.
Lemma domain_local_pointsto_combine tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜v1 = v2⌝ ∗
domain_local_pointsto tid key (dq1 ⋅ dq2) v1.
Lemma domain_local_pointsto_valid_2 tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma domain_local_pointsto_agree tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜v1 = v2⌝.
Lemma domain_local_pointsto_dfrac_ne tid1 key1 dq1 v1 tid2 key2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
domain_local_pointsto tid1 key1 dq1 v1 -∗
domain_local_pointsto tid2 key2 dq2 v2 -∗
⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
Lemma domain_local_pointsto_ne tid1 key1 v1 tid2 key2 dq2 v2 :
domain_local_pointsto tid1 key1 (DfracOwn 1) v1 -∗
domain_local_pointsto tid2 key2 dq2 v2 -∗
⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
Lemma domain_local_pointsto_exclusive tid key v1 dq2 v2 :
domain_local_pointsto tid key (DfracOwn 1) v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
False.
Lemma domain_local_pointsto_persist tid key dq v :
domain_local_pointsto tid key dq v ⊢ |==>
domain_local_pointsto tid key DfracDiscarded v.
Lemma domain٠spawn𑁒spec Ψ fn :
{{{
∀ tid,
domain_local tid ∅ -∗
WP fn () ∶ tid {{ Ψ }}
}}}
domain٠spawn fn
{{{
t
, RET t;
domain_model t Ψ
}}}.
Lemma domain٠join𑁒spec t Ψ :
{{{
domain_model t Ψ
}}}
domain٠join t
{{{
v
, RET v;
Ψ v
}}}.
Lemma domain٠local_new𑁒spec {fn} Ψ keys :
{{{
□ WP fn () {{ Ψ }} ∗
[∗ list] key ∈ keys, domain_key' key
}}}
domain٠local_new fn
{{{
key
, RET key;
domain_key key Ψ ∗
⌜Forall (.≠ key) keys⌝
}}}.
Lemma domain٠local_get𑁒spec_init keys key Ψ tid :
{{{
domain_local tid keys ∗
domain_key key Ψ ∗
domain_local_init tid key
}}}
domain٠local_get key ∶ tid
{{{
v
, RET v;
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v
}}}.
Lemma domain٠local_get𑁒spec_pointsto keys key dq v tid :
{{{
domain_local tid keys ∗
domain_local_pointsto tid key dq v
}}}
domain٠local_get key ∶ tid
{{{
RET v;
domain_local tid keys ∗
domain_local_pointsto tid key dq v
}}}.
Lemma domain٠local_get𑁒spec_pointstopred keys key Ψ tid :
{{{
domain_local tid keys ∗
domain_local_pointstopred tid key Ψ
}}}
domain٠local_get key ∶ tid
{{{
v
, RET v;
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v
}}}.
Lemma domain٠local_set𑁒spec_init keys key Ψ v tid :
{{{
domain_local tid keys ∗
domain_key key Ψ ∗
domain_local_init tid key
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
Lemma domain٠local_set𑁒spec_pointsto keys key w v tid :
{{{
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) w
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
Lemma domain٠local_set𑁒spec_pointstopred keys key Ψ v tid :
{{{
domain_local tid keys ∗
domain_local_pointstopred tid key Ψ
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
End domain_G.
Axiom domain٠yield𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
▷ Φ ()%V ⊢
WP domain٠yield () {{ Φ }}.
Axiom domain٠self_index𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
(∀ (i : nat), ▷ Φ #i) ⊢
WP domain٠self_index () {{ Φ }}.
Axiom domain٠recommended_domain_count𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
(∀ (i : nat), ▷ Φ #i) ⊢
WP domain٠recommended_domain_count () {{ Φ }}.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance domain٠yield𑁒diaspec :
DIASPEC
{{
True
}}
domain٠yield ()%V
{{
RET ();
True
}}.
#[global] Instance domain٠self_index𑁒diaspec :
DIASPEC
{{
True
}}
domain٠self_index ()%V
{{ (i : nat),
RET #i;
True
}}.
#[global] Instance domain٠recommended_domain_count𑁒diaspec :
DIASPEC
{{
True
}}
domain٠recommended_domain_count ()%V
{{ (i : nat),
RET #i;
True
}}.
End zoo_G.
#[global] Opaque domain٠spawn.
#[global] Opaque domain٠join.
#[global] Opaque domain٠local_new.
#[global] Opaque domain٠local_get.
#[global] Opaque domain٠local_set.
#[global] Opaque domain٠yield.
#[global] Opaque domain٠self_index.
#[global] Opaque domain٠recommended_domain_count.
#[global] Opaque domain_model.
#[global] Opaque domain_key.
#[global] Opaque domain_local.
#[global] Opaque domain_local_init.
#[global] Opaque domain_local_pointsto.
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
list
fin_maps.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
counter.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
domain__code.
From zoo_std Require Import
option
ivar_2
dynarray_1.
From zoo Require Import
options.
Implicit Types id : nat.
Implicit Types l : location.
Implicit Types t fn key : val.
Implicit Types vs : list (option val).
Implicit Types ws : gmap nat (option val).
Implicit Types ids : gmap val nat.
#[local] Notation "'id'" := (
in_type "key" 0
)(in custom zoo_proj
).
#[local] Notation "'init'" := (
in_type "key" 1
)(in custom zoo_proj
).
Definition domain٠spawn : val :=
fun: "fn" ⇒
let: "t" := ivar_2٠create () in
Fork (
let: "local" := dynarray_1٠create () in
SetLocal "local" ;;
ivar_2٠set "t" ("fn" ())
) ;;
"t".
Definition domain٠join : val :=
ivar_2٠get.
Definition domain٠local_new : val :=
fun: "fn" ⇒
let: "id" := zoo_counter٠incr () in
("id", "fn").
Definition domain٠key_id : val :=
fun: "key" ⇒
"key".<id>.
Definition domain٠key_init : val :=
fun: "key" ⇒
"key".<init> ().
Definition domain٠local_get : val :=
fun: "key" ⇒
let: "local" := GetLocal in
let: "id" := domain٠key_id "key" in
dynarray_1٠grow "local" ("id" + 1) §None ;;
match: dynarray_1٠get "local" "id" with
| None ⇒
let: "v" := domain٠key_init "key" in
dynarray_1٠set "local" "id" ‘Some( "v" ) ;;
"v"
| Some "v" ⇒
"v"
end.
Definition domain٠local_set : val :=
fun: "key" "v" ⇒
let: "local" := GetLocal in
let: "id" := domain٠key_id "key" in
dynarray_1٠grow "local" ("id" + 1) §None ;;
dynarray_1٠set "local" "id" ‘Some( "v" ).
Class DomainG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] domain_G_ivar_G :: Ivar2G Σ
; #[local] domain_G_locals_G :: ghost_mapG Σ nat (option val)
}.
Definition domain_Σ :=
#[ivar_2_Σ
; ghost_mapΣ nat (option val)
].
#[global] Instance subG_domain_Σ Σ `{zoo_G : !ZooG Σ} :
subG domain_Σ Σ →
DomainG Σ.
#[local] Definition consistent vs ws :=
map_oflatten (map_seq 0 vs) = map_oflatten ws.
#[local] Lemma consistent_app_None vs ws n :
consistent vs ws →
consistent (vs ++ replicate n None) ws.
#[local] Lemma consistent_lookup_None {vs ws} id o :
consistent vs ws →
ws !! id = None →
vs !! id = Some o →
o = None.
#[local] Lemma consistent_lookup_Some_None {vs ws} id :
id < length vs →
consistent vs ws →
ws !! id = Some None →
vs !! id = Some None.
#[local] Lemma consistent_lookup_Some_Some {vs ws} id v :
consistent vs ws →
ws !! id = Some (Some v) →
vs !! id = Some (Some v).
#[local] Lemma consistent_insert {vs ws} id :
ws !! id = None →
consistent vs ws →
consistent vs (<[id := None]> ws).
#[local] Lemma consistent_update {vs ws} id w :
id < length vs →
consistent vs ws →
consistent (<[id := Some w]> vs) (<[id := Some w]> ws).
Opaque consistent.
Section domain_G.
Context `{domain_G : DomainG Σ}.
Implicit Types Ψ : val → iProp Σ.
#[local] Definition local_auth γ :=
ghost_map_auth γ 1.
#[local] Definition local_at :=
ghost_map_elem.
Definition domain_model t Ψ : iProp Σ :=
ivar_2_inv t Ψ (λ _, True)%I ∗
ivar_2_consumer t Ψ.
#[local] Instance : CustomIpat "model" :=
" ( #Hivar_inv & Hivar_consumer ) ".
#[local] Definition key_id key id : iProp Σ :=
∃ fn,
⌜key = (#id, fn)%V⌝ ∗
zoo_counter_at id fn.
#[local] Instance : CustomIpat "key_id" :=
" ( %fn{} & %Heq{} & #Hcounter_at{} ) ".
Definition domain_key key Ψ : iProp Σ :=
∃ id fn,
⌜key = (#id, fn)%V⌝ ∗
zoo_counter_at id fn ∗
□ WP fn () {{ Ψ }}.
#[local] Instance : CustomIpat "key" :=
" ( %id & %fn{} & -> & Hcounter_at & #Hfn{} ) ".
Definition domain_key' key : iProp Σ :=
∃ Ψ,
domain_key key Ψ.
Definition domain_local tid keys : iProp Σ :=
∃ l γ vs ws ids,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
dynarray_1_model #l (option_to_val <$> vs) ∗
local_auth γ ws ∗
⌜dom ids = keys⌝ ∗
⌜map_img ids = dom ws⌝ ∗
([∗ map] key ↦ id ∈ ids, key_id key id) ∗
⌜consistent vs ws⌝.
#[local] Instance : CustomIpat "local" :=
" ( %l & %γ & %vs & %ws & %ids & #Hlocal & #Hl_meta & Hl & Hlocal_auth & %Hids_dom & %Hids_img & Hids & %Hconsistent ) ".
Definition domain_local_init tid key : iProp Σ :=
∃ l γ id,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
key_id key id ∗
local_at γ id (DfracOwn 1) None.
#[local] Instance : CustomIpat "local_init" :=
" ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".
Definition domain_local_pointsto tid key dq v : iProp Σ :=
∃ l γ id,
tid ↦ₗ□ #l ∗
meta l (nroot.@"user") γ ∗
key_id key id ∗
local_at γ id dq (Some v).
#[local] Instance : CustomIpat "local_pointsto" :=
" ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".
Definition domain_local_pointstopred tid key Ψ : iProp Σ :=
domain_local_init tid key ∗
domain_key key Ψ
∨ ∃ v,
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v.
#[local] Instance : CustomIpat "local_pointstopred" :=
" [ ( Hinit & Hkey ) | ( % & Hlocal_pointsto & HΨ ) ] ".
#[global] Instance domain_local_timeless tid keys :
Timeless (domain_local tid keys).
#[global] Instance domain_local_init_timeless tid key :
Timeless (domain_local_init tid key).
#[global] Instance domain_local_pointsto_timeless tid key dq v :
Timeless (domain_local_pointsto tid key dq v).
#[local] Instance key_id_persistent key id :
Persistent (key_id key id).
#[global] Instance domain_key_persistent key Ψ :
Persistent (domain_key key Ψ).
#[global] Instance domain_local_pointsto_persistent tid key v :
Persistent (domain_local_pointsto tid key DfracDiscarded v).
#[local] Lemma local_alloc :
⊢ |==>
∃ γ,
local_auth γ ∅.
#[local] Lemma local_at_valid γ ws id dq v :
local_auth γ ws -∗
local_at γ id dq v -∗
⌜ws !! id = Some v⌝.
#[local] Lemma local_insert {γ ws} id :
ws !! id = None →
local_auth γ ws ⊢ |==>
local_auth γ (<[id := None]> ws) ∗
local_at γ id (DfracOwn 1) None.
#[local] Lemma local_update {γ ws id w} w' :
local_auth γ ws -∗
local_at γ id (DfracOwn 1) w ==∗
local_auth γ (<[id := w']> ws) ∗
local_at γ id (DfracOwn 1) w'.
#[local] Lemma key_id_agree key id1 id2 :
key_id key id1 -∗
key_id key id2 -∗
⌜id1 = id2⌝.
#[local] Lemma key_id_inj key1 id1 key2 id2 :
key1 ≠ key2 →
key_id key1 id1 -∗
key_id key2 id2 -∗
⌜id1 ≠ id2⌝.
#[local] Lemma domain_key_to_id key Ψ :
domain_key key Ψ ⊢
∃ id,
key_id key id.
#[local] Lemma domain٠key_id𑁒spec key id :
{{{
key_id key id
}}}
domain٠key_id key
{{{
RET #id;
True
}}}.
#[local] Lemma domain٠key_init𑁒spec key Ψ :
{{{
domain_key key Ψ
}}}
domain٠key_init key
{{{
v
, RET v;
Ψ v
}}}.
Opaque key_id.
Lemma domain_local_get_key {tid keys} key Ψ :
key ∉ keys →
domain_local tid keys -∗
domain_key key Ψ ==∗
domain_local tid (keys ∪ {[key]}) ∗
domain_local_init tid key.
#[global] Instance domain_local_pointsto_fractional tid key v :
Fractional (λ q, domain_local_pointsto tid key (DfracOwn q) v).
#[global] Instance domain_local_pointsto_as_fractional tid key q v :
AsFractional (domain_local_pointsto tid key (DfracOwn q) v) (λ q, domain_local_pointsto tid key (DfracOwn q) v)%I q.
Lemma domain_local_pointsto_valid tid key dq v :
domain_local_pointsto tid key dq v ⊢
⌜✓ dq⌝.
Lemma domain_local_pointsto_combine tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜v1 = v2⌝ ∗
domain_local_pointsto tid key (dq1 ⋅ dq2) v1.
Lemma domain_local_pointsto_valid_2 tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜v1 = v2⌝.
Lemma domain_local_pointsto_agree tid key dq1 v1 dq2 v2 :
domain_local_pointsto tid key dq1 v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
⌜v1 = v2⌝.
Lemma domain_local_pointsto_dfrac_ne tid1 key1 dq1 v1 tid2 key2 dq2 v2 :
¬ ✓ (dq1 ⋅ dq2) →
domain_local_pointsto tid1 key1 dq1 v1 -∗
domain_local_pointsto tid2 key2 dq2 v2 -∗
⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
Lemma domain_local_pointsto_ne tid1 key1 v1 tid2 key2 dq2 v2 :
domain_local_pointsto tid1 key1 (DfracOwn 1) v1 -∗
domain_local_pointsto tid2 key2 dq2 v2 -∗
⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
Lemma domain_local_pointsto_exclusive tid key v1 dq2 v2 :
domain_local_pointsto tid key (DfracOwn 1) v1 -∗
domain_local_pointsto tid key dq2 v2 -∗
False.
Lemma domain_local_pointsto_persist tid key dq v :
domain_local_pointsto tid key dq v ⊢ |==>
domain_local_pointsto tid key DfracDiscarded v.
Lemma domain٠spawn𑁒spec Ψ fn :
{{{
∀ tid,
domain_local tid ∅ -∗
WP fn () ∶ tid {{ Ψ }}
}}}
domain٠spawn fn
{{{
t
, RET t;
domain_model t Ψ
}}}.
Lemma domain٠join𑁒spec t Ψ :
{{{
domain_model t Ψ
}}}
domain٠join t
{{{
v
, RET v;
Ψ v
}}}.
Lemma domain٠local_new𑁒spec {fn} Ψ keys :
{{{
□ WP fn () {{ Ψ }} ∗
[∗ list] key ∈ keys, domain_key' key
}}}
domain٠local_new fn
{{{
key
, RET key;
domain_key key Ψ ∗
⌜Forall (.≠ key) keys⌝
}}}.
Lemma domain٠local_get𑁒spec_init keys key Ψ tid :
{{{
domain_local tid keys ∗
domain_key key Ψ ∗
domain_local_init tid key
}}}
domain٠local_get key ∶ tid
{{{
v
, RET v;
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v
}}}.
Lemma domain٠local_get𑁒spec_pointsto keys key dq v tid :
{{{
domain_local tid keys ∗
domain_local_pointsto tid key dq v
}}}
domain٠local_get key ∶ tid
{{{
RET v;
domain_local tid keys ∗
domain_local_pointsto tid key dq v
}}}.
Lemma domain٠local_get𑁒spec_pointstopred keys key Ψ tid :
{{{
domain_local tid keys ∗
domain_local_pointstopred tid key Ψ
}}}
domain٠local_get key ∶ tid
{{{
v
, RET v;
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v ∗
Ψ v
}}}.
Lemma domain٠local_set𑁒spec_init keys key Ψ v tid :
{{{
domain_local tid keys ∗
domain_key key Ψ ∗
domain_local_init tid key
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
Lemma domain٠local_set𑁒spec_pointsto keys key w v tid :
{{{
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) w
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
Lemma domain٠local_set𑁒spec_pointstopred keys key Ψ v tid :
{{{
domain_local tid keys ∗
domain_local_pointstopred tid key Ψ
}}}
domain٠local_set key v ∶ tid
{{{
RET ();
domain_local tid keys ∗
domain_local_pointsto tid key (DfracOwn 1) v
}}}.
End domain_G.
Axiom domain٠yield𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
▷ Φ ()%V ⊢
WP domain٠yield () {{ Φ }}.
Axiom domain٠self_index𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
(∀ (i : nat), ▷ Φ #i) ⊢
WP domain٠self_index () {{ Φ }}.
Axiom domain٠recommended_domain_count𑁒spec : ∀ `{zoo_G : !ZooG Σ} Φ,
(∀ (i : nat), ▷ Φ #i) ⊢
WP domain٠recommended_domain_count () {{ Φ }}.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[global] Instance domain٠yield𑁒diaspec :
DIASPEC
{{
True
}}
domain٠yield ()%V
{{
RET ();
True
}}.
#[global] Instance domain٠self_index𑁒diaspec :
DIASPEC
{{
True
}}
domain٠self_index ()%V
{{ (i : nat),
RET #i;
True
}}.
#[global] Instance domain٠recommended_domain_count𑁒diaspec :
DIASPEC
{{
True
}}
domain٠recommended_domain_count ()%V
{{ (i : nat),
RET #i;
True
}}.
End zoo_G.
#[global] Opaque domain٠spawn.
#[global] Opaque domain٠join.
#[global] Opaque domain٠local_new.
#[global] Opaque domain٠local_get.
#[global] Opaque domain٠local_set.
#[global] Opaque domain٠yield.
#[global] Opaque domain٠self_index.
#[global] Opaque domain٠recommended_domain_count.
#[global] Opaque domain_model.
#[global] Opaque domain_key.
#[global] Opaque domain_local.
#[global] Opaque domain_local_init.
#[global] Opaque domain_local_pointsto.