Library zoo_std.inf_array
From Stdlib.Logic Require Import
FunctionalExtensionality.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
function.
From zoo.iris.base_logic Require Import
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
inf_array__code.
From zoo_std Require Import
array
inf_array__types
int
mutex.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types v v_resolve t fn : val.
Implicit Types us : list val.
Implicit Types vs : nat → val.
Class InfArrayG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_array_G_mutex_G :: MutexG Σ
; #[local] inf_array_G_model_G :: TwinsG Σ (nat -d> val_O)
}.
Definition inf_array_Σ :=
#[mutex_Σ
; twins_Σ (nat -d> val_O)
].
#[global] Instance subG_inf_array_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_array_Σ Σ →
InfArrayG Σ .
Section inf_array_G.
Context `{inf_array_G : InfArrayG Σ}.
Record metadata :=
{ metadata_default : val
; metadata_model : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition inv_2 l γ us : iProp Σ :=
∃ data vs,
l.[data] ↦ data ∗
array_model data (DfracOwn 1) us ∗
model₂ γ vs ∗
⌜vs = λ i, if decide (i < length us) then us !!! i else γ.(metadata_default)⌝.
#[local] Instance : CustomIpat "inv_2" :=
" ( %data & %vs & Hl_data & Hdata & Hmodel₂ & %Hvs ) ".
#[local] Definition inv_1 l γ : iProp Σ :=
∃ us,
inv_2 l γ us.
#[local] Instance : CustomIpat "inv_1" :=
" ( %us{} & {{lazy}Hinv;(:inv_2)} ) ".
Definition inf_array_inv t : iProp Σ :=
∃ l γ mtx,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[default] ↦□ γ.(metadata_default) ∗
l.[mutex] ↦□ mtx ∗
mutex_inv mtx (inv_1 l γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & %mtx & -> & #Hmeta & #Hl_mtx & #Hl_default & #Hmtx_inv ) ".
Definition inf_array_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l_ & %γ_ & %Heq & #Hmeta_ & Hmodel₁ ) ".
Definition inf_array_model' t vsₗ vsᵣ :=
inf_array_model t (
λ i,
if decide (i < length vsₗ) then vsₗ !!! i else vsᵣ (i - length vsₗ)
).
#[global] Instance inf_array_inv_persistent t :
Persistent (inf_array_inv t).
#[global] Instance inf_array_model_ne t n :
Proper (pointwise_relation nat (=) ==> (≡{n}≡)) (inf_array_model t).
#[global] Instance inf_array_model_proper t :
Proper (pointwise_relation nat (=) ==> (≡)) (inf_array_model t).
#[global] Instance inf_array_model_timeless t vs :
Timeless (inf_array_model t vs).
#[global] Instance inf_array_model'_ne t n :
Proper ((=) ==> pointwise_relation nat (=) ==> (≡{n}≡)) (inf_array_model' t).
#[global] Instance inf_array_model'_proper t :
Proper ((=) ==> pointwise_relation nat (=) ==> (≡)) (inf_array_model' t).
#[global] Instance inf_array_model'_timeless t vsₗ vsᵣ :
Timeless (inf_array_model' t vsₗ vsᵣ).
#[local] Lemma model_alloc default :
⊢ |==>
∃ γ_model,
model₁' γ_model (λ _, default) ∗
model₂' γ_model (λ _, default).
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
Lemma inf_array_model_to_model' {t vs} vsₗ :
(∀ i v, vsₗ !! i = Some v → vs i = v) →
inf_array_model t vs ⊢
inf_array_model' t vsₗ (λ i, vs (length vsₗ + i)).
Lemma inf_array_model_to_model'_replicate {t vs} n v :
(∀ i, i < n → vs i = v) →
inf_array_model t vs ⊢
inf_array_model' t (replicate n v) (λ i, vs (n + i)).
Lemma inf_array_model_to_model'_constant {t v} n :
inf_array_model t (λ _, v) ⊢
inf_array_model' t (replicate n v) (λ _, v).
Lemma inf_array_model'_shift t vsₗ v vsᵣ :
inf_array_model' t (vsₗ ++ [v]) vsᵣ ⊣⊢
inf_array_model' t vsₗ (v .: vsᵣ).
Lemma inf_array_model'_shift_r t vsₗ v vsᵣ :
inf_array_model' t (vsₗ ++ [v]) vsᵣ ⊢
inf_array_model' t vsₗ (v .: vsᵣ).
Lemma inf_array_model'_shift_l t vsₗ vsᵣ v vsᵣ' :
vsᵣ ≡ᶠ v .: vsᵣ' →
inf_array_model' t vsₗ vsᵣ ⊢
inf_array_model' t (vsₗ ++ [v]) vsᵣ'.
Lemma inf_array_model'_shift_l' t vsₗ vsᵣ :
inf_array_model' t vsₗ vsᵣ ⊢
inf_array_model' t (vsₗ ++ [vsᵣ 0]) (vsᵣ ∘ S).
Lemma inf_array٠create𑁒spec default :
{{{
True
}}}
inf_array٠create default
{{{
t
, RET t;
inf_array_inv t ∗
inf_array_model t (λ _, default)
}}}.
#[local] Lemma inf_array٠next_capacity𑁒spec n :
(0 ≤ n)%Z →
{{{
True
}}}
inf_array٠next_capacity #n
{{{
m
, RET #m;
⌜n ≤ m⌝%Z
}}}.
#[local] Lemma inf_array٠reserve𑁒spec l γ us n :
(0 ≤ n)%Z →
{{{
l.[default] ↦□ γ.(metadata_default) ∗
inv_2 l γ us
}}}
inf_array٠reserve #l #n
{{{
us
, RET ();
inv_2 l γ us ∗
⌜₊n ≤ length us⌝
}}}.
Lemma inf_array٠get𑁒spec t i :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠get t #i
<<<
inf_array_model t vs
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠get𑁒spec' t i :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vsₗ vsᵣ,
inf_array_model' t vsₗ vsᵣ
>>>
inf_array٠get t #i
<<<
inf_array_model' t vsₗ vsᵣ
| RET
if decide (₊i < length vsₗ) then
vsₗ !!! ₊i
else
vsᵣ (₊i - length vsₗ);
£ 1
>>>.
Lemma inf_array٠update𑁒spec Ψ1 Ψ2 t i fn :
(0 ≤ i)%Z →
<<<
inf_array_inv t ∗
(∀ v, Ψ1 v -∗ WP fn v {{ Ψ2 v }})
| ∀∀ vs,
inf_array_model t vs ∗
□ Ψ1 (vs ₊i)
>>>
inf_array٠update t #i fn
<<<
∃∃ v,
inf_array_model t (<[₊i := v]> vs) ∗
Ψ2 (vs ₊i) v
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠xchg𑁒spec t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠xchg t #i v
<<<
inf_array_model t (<[₊i := v]> vs)
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠xchg_resolve𑁒spec t i v pid v_resolve Φ E :
(0 ≤ i)%Z →
inf_array_inv t -∗
( |={⊤,E}=>
∃ vs,
inf_array_model t vs ∗
( ∀ e,
⌜PureExec True 1 e ()⌝ -∗
⌜to_val e = None⌝ -∗
inf_array_model t (<[₊i := v]> vs) -∗
WP Resolve e #pid v_resolve @ E {{ _,
|={E,⊤}=>
Φ (vs ₊i)
}}
)
) -∗
WP inf_array٠xchg_resolve t #i v #pid v_resolve {{ Φ }}.
Lemma inf_array٠set𑁒spec t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠set t #i v
<<<
inf_array_model t (<[₊i := v]> vs)
| RET ();
£ 1
>>>.
Lemma inf_array٠set𑁒spec' t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vsₗ vsᵣ,
inf_array_model' t vsₗ vsᵣ
>>>
inf_array٠set t #i v
<<<
if decide (₊i < length vsₗ) then
inf_array_model' t (<[₊i := v]> vsₗ) vsᵣ
else
inf_array_model' t vsₗ (<[₊i - length vsₗ := v]> vsᵣ)
| RET ();
£ 1
>>>.
Lemma inf_array٠cas𑁒spec t i v1 v2 :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠cas t #i v1 v2
<<<
∃∃ b,
⌜(if b then (≈) else (≉)) (vs ₊i) v1⌝ ∗
inf_array_model t (if b then <[₊i := v2]> vs else vs)
| RET #b;
£ 1
>>>.
Lemma inf_array٠cas_resolve𑁒spec t i v1 v2 pid v_resolve Φ E :
(0 ≤ i)%Z →
inf_array_inv t -∗
( |={⊤,E}=>
∃ vs,
inf_array_model t vs ∗
( ∀ e b,
⌜PureExec True 1 e ()⌝ -∗
⌜to_val e = None⌝ -∗
⌜(if b then (≈) else (≉)) (vs ₊i) v1⌝ -∗
inf_array_model t (if b then <[₊i := v2]> vs else vs) -∗
WP Resolve e #pid v_resolve @ E {{ _,
|={E,⊤}=>
Φ #b
}}
)
) -∗
WP inf_array٠cas_resolve t #i v1 v2 #pid v_resolve {{ Φ }}.
Lemma inf_array٠faa𑁒spec t i (incr : Z) :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs (n : Z),
⌜vs ₊i = #n⌝ ∗
inf_array_model t vs
>>>
inf_array٠faa t #i #incr
<<<
inf_array_model t (<[₊i := #(n + incr)]> vs)
| RET vs ₊i;
£ 1
>>>.
End inf_array_G.
From zoo_std Require
inf_array__opaque.
#[global] Opaque inf_array_inv.
#[global] Opaque inf_array_model.
#[global] Opaque inf_array_model'.
FunctionalExtensionality.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
function.
From zoo.iris.base_logic Require Import
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
inf_array__code.
From zoo_std Require Import
array
inf_array__types
int
mutex.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types l : location.
Implicit Types pid : prophet_id.
Implicit Types v v_resolve t fn : val.
Implicit Types us : list val.
Implicit Types vs : nat → val.
Class InfArrayG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_array_G_mutex_G :: MutexG Σ
; #[local] inf_array_G_model_G :: TwinsG Σ (nat -d> val_O)
}.
Definition inf_array_Σ :=
#[mutex_Σ
; twins_Σ (nat -d> val_O)
].
#[global] Instance subG_inf_array_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_array_Σ Σ →
InfArrayG Σ .
Section inf_array_G.
Context `{inf_array_G : InfArrayG Σ}.
Record metadata :=
{ metadata_default : val
; metadata_model : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition inv_2 l γ us : iProp Σ :=
∃ data vs,
l.[data] ↦ data ∗
array_model data (DfracOwn 1) us ∗
model₂ γ vs ∗
⌜vs = λ i, if decide (i < length us) then us !!! i else γ.(metadata_default)⌝.
#[local] Instance : CustomIpat "inv_2" :=
" ( %data & %vs & Hl_data & Hdata & Hmodel₂ & %Hvs ) ".
#[local] Definition inv_1 l γ : iProp Σ :=
∃ us,
inv_2 l γ us.
#[local] Instance : CustomIpat "inv_1" :=
" ( %us{} & {{lazy}Hinv;(:inv_2)} ) ".
Definition inf_array_inv t : iProp Σ :=
∃ l γ mtx,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[default] ↦□ γ.(metadata_default) ∗
l.[mutex] ↦□ mtx ∗
mutex_inv mtx (inv_1 l γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & %mtx & -> & #Hmeta & #Hl_mtx & #Hl_default & #Hmtx_inv ) ".
Definition inf_array_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l_ & %γ_ & %Heq & #Hmeta_ & Hmodel₁ ) ".
Definition inf_array_model' t vsₗ vsᵣ :=
inf_array_model t (
λ i,
if decide (i < length vsₗ) then vsₗ !!! i else vsᵣ (i - length vsₗ)
).
#[global] Instance inf_array_inv_persistent t :
Persistent (inf_array_inv t).
#[global] Instance inf_array_model_ne t n :
Proper (pointwise_relation nat (=) ==> (≡{n}≡)) (inf_array_model t).
#[global] Instance inf_array_model_proper t :
Proper (pointwise_relation nat (=) ==> (≡)) (inf_array_model t).
#[global] Instance inf_array_model_timeless t vs :
Timeless (inf_array_model t vs).
#[global] Instance inf_array_model'_ne t n :
Proper ((=) ==> pointwise_relation nat (=) ==> (≡{n}≡)) (inf_array_model' t).
#[global] Instance inf_array_model'_proper t :
Proper ((=) ==> pointwise_relation nat (=) ==> (≡)) (inf_array_model' t).
#[global] Instance inf_array_model'_timeless t vsₗ vsᵣ :
Timeless (inf_array_model' t vsₗ vsᵣ).
#[local] Lemma model_alloc default :
⊢ |==>
∃ γ_model,
model₁' γ_model (λ _, default) ∗
model₂' γ_model (λ _, default).
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
Lemma inf_array_model_to_model' {t vs} vsₗ :
(∀ i v, vsₗ !! i = Some v → vs i = v) →
inf_array_model t vs ⊢
inf_array_model' t vsₗ (λ i, vs (length vsₗ + i)).
Lemma inf_array_model_to_model'_replicate {t vs} n v :
(∀ i, i < n → vs i = v) →
inf_array_model t vs ⊢
inf_array_model' t (replicate n v) (λ i, vs (n + i)).
Lemma inf_array_model_to_model'_constant {t v} n :
inf_array_model t (λ _, v) ⊢
inf_array_model' t (replicate n v) (λ _, v).
Lemma inf_array_model'_shift t vsₗ v vsᵣ :
inf_array_model' t (vsₗ ++ [v]) vsᵣ ⊣⊢
inf_array_model' t vsₗ (v .: vsᵣ).
Lemma inf_array_model'_shift_r t vsₗ v vsᵣ :
inf_array_model' t (vsₗ ++ [v]) vsᵣ ⊢
inf_array_model' t vsₗ (v .: vsᵣ).
Lemma inf_array_model'_shift_l t vsₗ vsᵣ v vsᵣ' :
vsᵣ ≡ᶠ v .: vsᵣ' →
inf_array_model' t vsₗ vsᵣ ⊢
inf_array_model' t (vsₗ ++ [v]) vsᵣ'.
Lemma inf_array_model'_shift_l' t vsₗ vsᵣ :
inf_array_model' t vsₗ vsᵣ ⊢
inf_array_model' t (vsₗ ++ [vsᵣ 0]) (vsᵣ ∘ S).
Lemma inf_array٠create𑁒spec default :
{{{
True
}}}
inf_array٠create default
{{{
t
, RET t;
inf_array_inv t ∗
inf_array_model t (λ _, default)
}}}.
#[local] Lemma inf_array٠next_capacity𑁒spec n :
(0 ≤ n)%Z →
{{{
True
}}}
inf_array٠next_capacity #n
{{{
m
, RET #m;
⌜n ≤ m⌝%Z
}}}.
#[local] Lemma inf_array٠reserve𑁒spec l γ us n :
(0 ≤ n)%Z →
{{{
l.[default] ↦□ γ.(metadata_default) ∗
inv_2 l γ us
}}}
inf_array٠reserve #l #n
{{{
us
, RET ();
inv_2 l γ us ∗
⌜₊n ≤ length us⌝
}}}.
Lemma inf_array٠get𑁒spec t i :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠get t #i
<<<
inf_array_model t vs
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠get𑁒spec' t i :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vsₗ vsᵣ,
inf_array_model' t vsₗ vsᵣ
>>>
inf_array٠get t #i
<<<
inf_array_model' t vsₗ vsᵣ
| RET
if decide (₊i < length vsₗ) then
vsₗ !!! ₊i
else
vsᵣ (₊i - length vsₗ);
£ 1
>>>.
Lemma inf_array٠update𑁒spec Ψ1 Ψ2 t i fn :
(0 ≤ i)%Z →
<<<
inf_array_inv t ∗
(∀ v, Ψ1 v -∗ WP fn v {{ Ψ2 v }})
| ∀∀ vs,
inf_array_model t vs ∗
□ Ψ1 (vs ₊i)
>>>
inf_array٠update t #i fn
<<<
∃∃ v,
inf_array_model t (<[₊i := v]> vs) ∗
Ψ2 (vs ₊i) v
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠xchg𑁒spec t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠xchg t #i v
<<<
inf_array_model t (<[₊i := v]> vs)
| RET vs ₊i;
£ 1
>>>.
Lemma inf_array٠xchg_resolve𑁒spec t i v pid v_resolve Φ E :
(0 ≤ i)%Z →
inf_array_inv t -∗
( |={⊤,E}=>
∃ vs,
inf_array_model t vs ∗
( ∀ e,
⌜PureExec True 1 e ()⌝ -∗
⌜to_val e = None⌝ -∗
inf_array_model t (<[₊i := v]> vs) -∗
WP Resolve e #pid v_resolve @ E {{ _,
|={E,⊤}=>
Φ (vs ₊i)
}}
)
) -∗
WP inf_array٠xchg_resolve t #i v #pid v_resolve {{ Φ }}.
Lemma inf_array٠set𑁒spec t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠set t #i v
<<<
inf_array_model t (<[₊i := v]> vs)
| RET ();
£ 1
>>>.
Lemma inf_array٠set𑁒spec' t i v :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vsₗ vsᵣ,
inf_array_model' t vsₗ vsᵣ
>>>
inf_array٠set t #i v
<<<
if decide (₊i < length vsₗ) then
inf_array_model' t (<[₊i := v]> vsₗ) vsᵣ
else
inf_array_model' t vsₗ (<[₊i - length vsₗ := v]> vsᵣ)
| RET ();
£ 1
>>>.
Lemma inf_array٠cas𑁒spec t i v1 v2 :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs,
inf_array_model t vs
>>>
inf_array٠cas t #i v1 v2
<<<
∃∃ b,
⌜(if b then (≈) else (≉)) (vs ₊i) v1⌝ ∗
inf_array_model t (if b then <[₊i := v2]> vs else vs)
| RET #b;
£ 1
>>>.
Lemma inf_array٠cas_resolve𑁒spec t i v1 v2 pid v_resolve Φ E :
(0 ≤ i)%Z →
inf_array_inv t -∗
( |={⊤,E}=>
∃ vs,
inf_array_model t vs ∗
( ∀ e b,
⌜PureExec True 1 e ()⌝ -∗
⌜to_val e = None⌝ -∗
⌜(if b then (≈) else (≉)) (vs ₊i) v1⌝ -∗
inf_array_model t (if b then <[₊i := v2]> vs else vs) -∗
WP Resolve e #pid v_resolve @ E {{ _,
|={E,⊤}=>
Φ #b
}}
)
) -∗
WP inf_array٠cas_resolve t #i v1 v2 #pid v_resolve {{ Φ }}.
Lemma inf_array٠faa𑁒spec t i (incr : Z) :
(0 ≤ i)%Z →
<<<
inf_array_inv t
| ∀∀ vs (n : Z),
⌜vs ₊i = #n⌝ ∗
inf_array_model t vs
>>>
inf_array٠faa t #i #incr
<<<
inf_array_model t (<[₊i := #(n + incr)]> vs)
| RET vs ₊i;
£ 1
>>>.
End inf_array_G.
From zoo_std Require
inf_array__opaque.
#[global] Opaque inf_array_inv.
#[global] Opaque inf_array_model.
#[global] Opaque inf_array_model'.