Library zoo_kcas.kcas_1
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
list.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.excl
lib.saved_prop
lib.saved_pred
lib.mono_list.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_bool
identifier.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
list.
From zoo_kcas Require Import
kcas_1__types.
From zoo_kcas Require Export
kcas_1__code.
From zoo Require Import
options.
Implicit Types b full : bool.
Implicit Types i : nat.
Implicit Types l loc casn : location.
Implicit Types casns : list location.
Implicit Types gid : identifier.
Implicit Types v w state : val.
Implicit Types vs befores afters : list val.
Implicit Types cas : location × (val × val).
Implicit Types cass : list (location × (val × val)).
Implicit Types helpers : gmap gname nat.
#[local] Program Definition global_prophet :=
{|prophet_typed_type :=
identifier × bool
; prophet_typed_of_val v :=
match v with
| ValTuple [ValProph gid; ValBool b] ⇒
Some (gid, b)
| _ ⇒
None
end
; prophet_typed_to_val '(gid, b) :=
(#gid, #b)%V
|}.
Solve Obligations of global_prophet with
try done.
Implicit Types prophs : list global_prophet.(prophet_typed_type).
Record loc_metadata :=
{ loc_metadata_model : gname
; loc_metadata_history : gname
}.
Implicit Types γ : loc_metadata.
#[local] Instance loc_metadata_inhabited : Inhabited loc_metadata :=
populate
{|loc_metadata_model := inhabitant
; loc_metadata_history := inhabitant
|}.
#[local] Instance loc_metadata_eq_dec : EqDecision loc_metadata :=
ltac:(solve_decision).
#[local] Instance loc_metadata_countable :
Countable loc_metadata.
Record descriptor :=
{ descriptor_loc : location
; descriptor_meta : loc_metadata
; descriptor_before : val
; descriptor_after : val
; descriptor_state : location
}.
Implicit Types descr : descriptor.
Implicit Types descrs : list descriptor.
#[local] Definition descriptor_cas descr : val :=
(#descr.(descriptor_loc), #descr.(descriptor_state)).
#[local] Instance descriptor_inhabited : Inhabited descriptor :=
populate
{|descriptor_loc := inhabitant
; descriptor_meta := inhabitant
; descriptor_before := inhabitant
; descriptor_after := inhabitant
; descriptor_state := inhabitant
|}.
#[local] Instance descriptor_eq_dec : EqDecision descriptor :=
ltac:(solve_decision).
#[local] Instance descriptor_countable :
Countable descriptor.
Variant status :=
| Undetermined
| After
| Before.
Implicit Types status : status.
Variant final_status :=
| FinalAfter
| FinalBefore.
Implicit Types fstatus : final_status.
Definition final_status_to_bool fstatus :=
if fstatus then true else false.
#[global] Arguments final_status_to_bool !_ : assert.
Definition final_status_of_bool b :=
if b then FinalAfter else FinalBefore.
#[global] Arguments final_status_of_bool !_ : assert.
Definition final_status_to_val fstatus :=
match fstatus with
| FinalAfter ⇒
§After
| FinalBefore ⇒
§Before
end%V.
#[global] Arguments final_status_to_val !_ : assert.
#[local] Lemma final_status_to_of_bool b :
final_status_to_bool (final_status_of_bool b) = b.
#[local] Lemma final_status_to_val_undetermined fstatus bid 𝑐𝑎𝑠𝑠 :
¬ final_status_to_val fstatus ≈ ‘Undetermined@bid[ 𝑐𝑎𝑠𝑠 ]%V.
Record metadata :=
{ metadata_descrs : list descriptor
; metadata_prophet : prophet_id
; metadata_prophs : list global_prophet.(prophet_typed_type)
; metadata_undetermined : block_id
; metadata_post : gname
; metadata_lstatus : gname
; metadata_locks : list gname
; metadata_helpers : gname
; metadata_winning : gname
; metadata_owner : gname
}.
Implicit Types η : metadata.
#[local] Instance metadata_inhabited : Inhabited metadata :=
populate
{|metadata_descrs := inhabitant
; metadata_prophet := inhabitant
; metadata_prophs := inhabitant
; metadata_undetermined := inhabitant
; metadata_post := inhabitant
; metadata_lstatus := inhabitant
; metadata_locks := inhabitant
; metadata_helpers := inhabitant
; metadata_winning := inhabitant
; metadata_owner := inhabitant
|}.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition metadata_size η :=
length η.(metadata_descrs).
#[local] Definition metadata_cass η :=
descriptor_cas <$> η.(metadata_descrs).
#[local] Definition metadata_cass_val η :=
list_to_val $ metadata_cass η.
#[local] Definition metadata_outcome η :=
hd inhabitant η.(metadata_prophs).
#[local] Definition metadata_winner η :=
(metadata_outcome η).1.
#[local] Definition metadata_success η :=
(metadata_outcome η).2.
#[local] Definition metadata_final η :=
final_status_to_val $ final_status_of_bool $ metadata_success η.
#[local] Instance status_inhabited : Inhabited status :=
populate Undetermined.
#[local] Definition status_to_val η status : val :=
match status with
| Undetermined ⇒
‘Undetermined@η.(metadata_undetermined)[ metadata_cass_val η ]
| After ⇒
§After
| Before ⇒
§Before
end.
Variant lstatus :=
| Running i
| Finished.
Implicit Types lstatus : lstatus.
#[local] Instance lstatus_inhabited : Inhabited lstatus :=
populate Finished.
Variant lstep : lstatus → lstatus → Prop :=
| lstep_incr i :
lstep (Running i) (Running (S i))
| lstep_finish i :
lstep (Running i) Finished.
#[local] Hint Constructors lstep : core.
#[local] Lemma lsteps_running0 lstatus :
rtc lstep (Running 0) lstatus.
#[local] Lemma lstep_finished lstatus :
¬ lstep Finished lstatus.
#[local] Lemma lsteps_finished lstatus :
rtc lstep Finished lstatus →
lstatus = Finished.
#[local] Lemma lsteps_le lstatus1 i1 lstatus2 i2 :
rtc lstep lstatus1 lstatus2 →
lstatus1 = Running i1 →
lstatus2 = Running i2 →
i1 ≤ i2.
#[local] Definition descriptor_final descr η :=
if metadata_success η then
descr.(descriptor_after)
else
descr.(descriptor_before).
Class Kcas1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] kcas_1_G_model_G :: TwinsG Σ val_O
; #[local] kcas_1_G_helper_G :: SavedPropG Σ
; #[local] kcas_1_G_post_G :: SavedPredG Σ bool
; #[local] kcas_1_G_lstatus_G :: AuthMonoG (A := leibnizO lstatus) Σ lstep
; #[local] kcas_1_G_history_G :: MonoListG Σ location
; #[local] kcas_1_G_lock_G :: ExclG Σ unitO
; #[local] kcas_1_G_helpers_G :: ghost_mapG Σ gname nat
; #[local] kcas_1_G_winning_G :: ExclG Σ unitO
; #[local] kcas_1_G_owner_G :: ExclG Σ unitO
}.
Definition kcas_1_Σ :=
#[twins_Σ val_O
; saved_prop_Σ
; saved_pred_Σ bool
; auth_mono_Σ (A := leibnizO lstatus) lstep
; mono_list_Σ location
; excl_Σ unitO
; ghost_mapΣ gname nat
; excl_Σ unitO
; excl_Σ unitO
].
#[global] Instance subG_kcas_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG kcas_1_Σ Σ →
Kcas1G Σ.
Section kcas_1_G.
Context `{kcas_1_G : Kcas1G Σ}.
Implicit Types P : iProp Σ.
#[local] Definition model₁' γ_model v :=
twins_twin1 γ_model (DfracOwn 1) v.
#[local] Definition model₁ γ v :=
model₁' γ.(loc_metadata_model) v.
#[local] Definition model₂' γ_model v : iProp Σ :=
∃ w,
⌜v ≈ w⌝ ∗
twins_twin2 γ_model w.
#[local] Definition model₂ γ v :=
model₂' γ.(loc_metadata_model) v.
#[local] Definition lstatus_auth' η_lstatus lstatus :=
auth_mono_auth _ η_lstatus (DfracOwn 1) lstatus.
#[local] Definition lstatus_auth η lstatus :=
lstatus_auth' η.(metadata_lstatus) lstatus.
#[local] Definition lstatus_lb η lstatus :=
auth_mono_lb _ η.(metadata_lstatus) lstatus.
#[local] Definition history_auth' γ_history casns : iProp Σ :=
mono_list_auth γ_history (DfracOwn 1) casns ∗
⌜NoDup casns⌝ ∗
[∗ list] casn ∈ removelast casns,
∃ η,
meta casn nroot η ∗
lstatus_lb η Finished.
#[local] Definition history_auth γ casns :=
history_auth' γ.(loc_metadata_history) casns.
#[local] Definition history_lb γ casns : iProp Σ :=
mono_list_lb γ.(loc_metadata_history) casns ∗
⌜NoDup casns⌝.
#[local] Definition history_elem' γ_history casn : iProp Σ :=
mono_list_elem γ_history casn.
#[local] Definition history_elem γ casn :=
history_elem' γ.(loc_metadata_history) casn.
#[local] Definition lock' η_lock :=
excl η_lock ().
#[local] Definition lock η i : iProp Σ :=
∃ η_lock,
⌜η.(metadata_locks) !! i = Some η_lock⌝ ∗
lock' η_lock.
#[local] Definition helpers_auth' η_helpers helpers :=
ghost_map_auth η_helpers 1 helpers.
#[local] Definition helpers_auth η helpers :=
helpers_auth' η.(metadata_helpers) helpers.
#[local] Definition helpers_elem η helper i :=
ghost_map_elem η.(metadata_helpers) helper (DfracOwn 1) i.
#[local] Definition winning' η_winning :=
excl η_winning ().
#[local] Definition winning η :=
winning' η.(metadata_winning).
#[local] Definition owner' η_owner :=
excl η_owner ().
#[local] Definition owner η :=
owner' η.(metadata_owner).
#[local] Definition au η ι Ψ : iProp Σ :=
AU <{
∃∃ vs,
[∗ list] descr; v ∈ η.(metadata_descrs); vs,
model₁ descr.(descriptor_meta) v
}> @ ⊤ ∖ ↑ι, ∅ <{
∀∀ b,
if b then
⌜vs ≈ descriptor_before <$> η.(metadata_descrs)⌝ ∗
[∗ list] descr ∈ η.(metadata_descrs),
model₁ descr.(descriptor_meta) descr.(descriptor_after)
else
∃ i descr v,
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜descr.(descriptor_before) ≉ v⌝ ∗
[∗ list] descr; v ∈ η.(metadata_descrs); vs,
model₁ descr.(descriptor_meta) v
, COMM
Ψ b
}>.
#[local] Definition helper_au' η ι descr P : iProp Σ :=
AU <{
∃∃ v,
model₁ descr.(descriptor_meta) v
}> @ ⊤ ∖ ↑ι, ∅ <{
⌜v ≈ descriptor_final descr η⌝ ∗
model₁ descr.(descriptor_meta) v
, COMM
P
}>.
#[local] Definition helper_au η ι i P : iProp Σ :=
∃ descr,
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
helper_au' η ι descr P.
#[local] Definition casn_inv_name ι casn :=
ι.@"casn".@casn.
#[local] Definition casn_inv_inner casn η ι Ψ : iProp Σ :=
∃ 𝑠𝑡𝑎𝑡𝑢𝑠 lstatus helpers prophs,
casn.[status] ↦ 𝑠𝑡𝑎𝑡𝑢𝑠 ∗
lstatus_auth η lstatus ∗
helpers_auth η helpers ∗
prophet_typed_model global_prophet η.(metadata_prophet) prophs ∗
match lstatus with
| Running i ⇒
⌜𝑠𝑡𝑎𝑡𝑢𝑠 = status_to_val η Undetermined⌝ ∗
⌜prophs = η.(metadata_prophs)⌝ ∗
( au η ι Ψ ∗
winning η
∨ identifier_model' (metadata_winner η)
) ∗
( [∗ map] helper ↦ j ∈ helpers,
∃ P,
⌜j < i⌝ ∗
saved_prop helper P ∗
helper_au η ι j P
) ∗
( [∗ list] descr ∈ η.(metadata_descrs),
descr.(descriptor_state).[before] ↦ descr.(descriptor_before) ∗
descr.(descriptor_state).[after] ↦ descr.(descriptor_after)
) ∗
( [∗ list] descr ∈ take i η.(metadata_descrs),
model₂ descr.(descriptor_meta) descr.(descriptor_before) ∗
history_elem descr.(descriptor_meta) casn
) ∗
( [∗ list] j ∈ seq i (metadata_size η - i),
lock η j
)
| Finished ⇒
⌜𝑠𝑡𝑎𝑡𝑢𝑠 = metadata_final η⌝ ∗
identifier_model' (metadata_winner η) ∗
(owner η ∨ Ψ (metadata_success η)) ∗
( [∗ map] helper ↦ _ ∈ helpers,
∃ P,
saved_prop helper P ∗
P
) ∗
( [∗ list] i ↦ descr ∈ η.(metadata_descrs),
( model₂ descr.(descriptor_meta) (descriptor_final descr η)
∨ lock η i
) ∗
if metadata_success η then
history_elem descr.(descriptor_meta) casn ∗
descr.(descriptor_state).[after] ↦ descr.(descriptor_after) ∗
descr.(descriptor_state).[before] ↦-
else
descr.(descriptor_state).[before] ↦ descr.(descriptor_before) ∗
descr.(descriptor_state).[after] ↦-
)
end.
#[local] Instance : CustomIpat "casn_inv_inner" :=
" ( %status{} & %lstatus{} & %helpers{} & %prophs{} & >Hcasn{}_status & >Hlstatus{}_auth & >Hhelpers{}_auth & >Hgproph{} & Hlstatus{} ) ".
#[local] Instance : CustomIpat "casn_inv_inner_running" :=
" ( {>;}-> & {>;}-> & Hau{} & Hhelpers{} & {>;}Hdescrs{} & {>;}Hmodels₂{} & {>;}Hlocks{} ) ".
#[local] Instance : CustomIpat "casn_inv_inner_finished" :=
" ( {>;}-> & {>;}Hwinner{} & HΨ{} & Hhelpers{} & {>;}Hdescrs{} ) ".
#[local] Definition casn_inv_pre ι
(casn_inv' : location × metadata × option nat -d> iProp Σ)
(loc_inv' : location × loc_metadata -d> iProp Σ)
: location × metadata × option nat -d> iProp Σ
:=
λ '(casn, η, i), (
∃ Ψ,
casn.[proph] ↦□ #η.(metadata_prophet) ∗
saved_pred η.(metadata_post) Ψ ∗
⌜NoDup (descriptor_loc <$> η.(metadata_descrs))⌝ ∗
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) ∗
[∗ list] j ↦ descr ∈ η.(metadata_descrs),
if i is Some i then
if decide (j = i) then
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn
else
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn ∗
loc_inv' (descr.(descriptor_loc), descr.(descriptor_meta))
else
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn ∗
loc_inv' (descr.(descriptor_loc), descr.(descriptor_meta))
)%I.
#[local] Instance : CustomIpat "casn_inv" :=
" ( %Ψ{} & Hcasn{}_proph & Hpost{} & %Hlocs{} & Hcasn{}_inv & Hlocs{} ) ".
#[local] Instance casn_inv_pre_contractive ι n :
Proper (dist_later n ==> (≡{n}≡) ==> (≡{n}≡)) (casn_inv_pre ι).
#[local] Definition loc_inv_name ι :=
ι.@"loc".
#[local] Definition loc_inv_inner'' full casn_inv' loc γ : iProp Σ :=
∃ casns casn η i descr,
meta casn nroot η ∗
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜loc = descr.(descriptor_loc)⌝ ∗
loc ↦ᵣ #descr.(descriptor_state) ∗
lstatus_lb η (Running (S i)) ∗
lock η i ∗
history_auth γ (casns ++ [casn]) ∗
casn_inv' (casn, η, if full then None else Some i).
#[local] Instance : CustomIpat "loc_inv_inner" :=
" ( %casns{} & %casn{} & %η{} & %i{} & %descr{} & {>;}{#}Hcasn{}_meta & {>;}%Hdescrs{}_lookup & {>;}{%Hloc{};->} & {>;}Hloc & {>;}{#}Hlstatus{}_lb & {>;}Hlock{} & {>;}Hhistory_auth & {#}Hcasn{}_inv' ) ".
#[local] Definition loc_inv_inner' :=
loc_inv_inner'' false.
#[local] Definition loc_inv_pre ι
(casn_inv' : location × metadata × option nat -d> iProp Σ)
(loc_inv' : location × loc_metadata -d> iProp Σ)
: location × loc_metadata -d> iProp Σ
:=
λ '(loc, γ),
inv (loc_inv_name ι) (loc_inv_inner' casn_inv' loc γ).
#[local] Instance loc_inv_pre_contractive ι n :
Proper (dist_later n ==> dist_later n ==> (≡{n}≡)) (loc_inv_pre ι).
#[local] Definition casn_inv'' ι :=
fixpoint_A (casn_inv_pre ι) (loc_inv_pre ι).
#[local] Definition casn_inv' ι casn η :=
casn_inv'' ι (casn, η, None).
#[local] Definition casn_inv casn ι : iProp Σ :=
∃ η,
meta casn nroot η ∗
casn_inv' ι casn η.
#[local] Definition loc_inv' ι :=
fixpoint_B (casn_inv_pre ι) (loc_inv_pre ι).
#[local] Definition loc_inv_inner loc γ ι : iProp Σ :=
loc_inv_inner'' true (casn_inv'' ι) loc γ.
Definition kcas_1_loc_inv loc ι : iProp Σ :=
∃ γ,
meta loc nroot γ ∗
loc_inv' ι (loc, γ).
Definition kcas_1_loc_model loc v : iProp Σ :=
∃ γ,
meta loc nroot γ ∗
model₁ γ v.
#[local] Instance : CustomIpat "loc_model" :=
" ( %γ{} & Hmeta{_{}} & Hmodel₁{_{}} ) ".
#[local] Lemma casn_inv''_unfold ι casn (i : option nat) η :
casn_inv'' ι (casn, η, i) ⊣⊢
casn_inv_pre ι (casn_inv'' ι) (loc_inv' ι) (casn, η, i).
#[local] Lemma casn_inv'_unfold ι casn η :
casn_inv' ι casn η ⊣⊢
casn_inv_pre ι (casn_inv'' ι) (loc_inv' ι) (casn, η, None).
#[local] Lemma loc_inv'_unfold loc γ ι :
loc_inv' ι (loc, γ) ⊣⊢
inv (loc_inv_name ι) (loc_inv_inner' (casn_inv'' ι) loc γ).
#[local] Lemma loc_inv'_intro loc γ ι :
inv (loc_inv_name ι) (loc_inv_inner' (casn_inv'' ι) loc γ) ⊢
loc_inv' ι (loc, γ).
#[local] Lemma loc_inv'_elim loc γ ι :
meta loc nroot γ -∗
loc_inv' ι (loc, γ) -∗
inv (loc_inv_name ι) (loc_inv_inner loc γ ι).
#[local] Instance model₂_timeless γ v :
Timeless (model₂ γ v).
#[local] Instance history_auth_timeless γ casns :
Timeless (history_auth γ casns).
#[local] Instance lock_timeless η i :
Timeless (lock η i).
#[global] Instance kcas_1_loc_model_timeless loc ι :
Timeless (kcas_1_loc_model loc ι).
#[local] Instance history_lb_persistent γ casns :
Persistent (history_lb γ casns).
#[local] Instance loc_inv'_persistent loc γ ι :
Persistent (loc_inv' ι (loc, γ)).
#[global] Instance kcas_1_loc_inv_persistent loc γ ι :
Persistent (kcas_1_loc_inv loc ι).
#[local] Instance casn_inv''_persistent casn η (i : option nat) ι :
Persistent (casn_inv'' ι (casn, η, i)).
#[local] Instance casn_inv'_persistent casn η ι :
Persistent (casn_inv' ι casn η).
#[local] Lemma model_alloc v :
⊢ |==>
∃ γ_model,
model₁' γ_model v ∗
model₂' γ_model v.
#[local] Lemma model₁_exclusive γ v1 v2 :
model₁ γ v1 -∗
model₁ γ v2 -∗
False.
#[local] Lemma model₂_similar {γ v1} v2 :
v1 ≈ v2 →
model₂ γ v1 ⊢
model₂ γ v2.
#[local] Lemma model₂_exclusive γ v1 v2 :
model₂ γ v1 -∗
model₂ γ v2 -∗
False.
#[local] Lemma model_agree γ v1 v2 :
model₁ γ v1 -∗
model₂ γ v2 -∗
⌜v1 ≈ v2⌝.
#[local] Lemma model_update {γ v1 v2} v :
model₁ γ v1 -∗
model₂ γ v2 ==∗
model₁ γ v ∗
model₂ γ v.
#[local] Lemma lstatus_alloc lstatus :
⊢ |==>
∃ η_lstatus,
lstatus_auth' η_lstatus lstatus.
#[local] Lemma lstatus_lb_get η lstatus :
lstatus_auth η lstatus ⊢
lstatus_lb η lstatus.
#[local] Lemma lstatus_lb_get_running0 η lstatus :
lstatus_auth η lstatus ⊢
lstatus_lb η (Running 0).
#[local] Lemma lstatus_lb_get_finished {η} lstatus :
lstatus_auth η Finished ⊢
lstatus_lb η lstatus.
#[local] Lemma lstatus_finished η lstatus :
lstatus_auth η lstatus -∗
lstatus_lb η Finished -∗
⌜lstatus = Finished⌝.
#[local] Lemma lstatus_le η i1 i2 :
lstatus_auth η (Running i1) -∗
lstatus_lb η (Running i2) -∗
⌜i2 ≤ i1⌝.
#[local] Lemma lstatus_update {η lstatus} lstatus' :
lstep lstatus lstatus' →
lstatus_auth η lstatus ⊢ |==>
lstatus_auth η lstatus'.
#[local] Lemma history_alloc casn :
⊢ |==>
∃ γ_history,
history_auth' γ_history [casn] ∗
history_elem' γ_history casn.
#[local] Lemma history_lb_get γ casns :
history_auth γ casns ⊢
history_lb γ casns.
#[local] Lemma history_lb_valid_eq γ casns1 casn casns2 casns3 :
history_auth γ (casns1 ++ [casn]) -∗
history_lb γ (casns2 ++ casn :: casns3) -∗
⌜casns1 = casns2⌝ ∗
⌜casns3 = []⌝.
#[local] Lemma history_lb_valid_ne γ casns1 casn1 casns2 casn2 :
casn1 ≠ casn2 →
history_auth γ (casns1 ++ [casn1]) -∗
history_lb γ (casns2 ++ [casn2]) -∗
∃ casns3,
history_lb γ (casns2 ++ [casn2] ++ casns3 ++ [casn1]).
#[local] Lemma history_elem_valid γ casns casn :
history_auth γ casns -∗
history_elem γ casn -∗
⌜casn ∈ casns⌝.
#[local] Lemma history_running γ casns casn1 casn2 η2 i :
history_auth γ (casns ++ [casn1]) -∗
meta casn2 nroot η2 -∗
lstatus_auth η2 (Running i) -∗
⌜casn2 ∉ casns⌝.
#[local] Lemma history_update {γ casns casn1 η1} casn2 :
casn2 ∉ casns →
casn2 ≠ casn1 →
history_auth γ (casns ++ [casn1]) -∗
meta casn1 nroot η1 -∗
lstatus_lb η1 Finished ==∗
history_auth γ ((casns ++ [casn1]) ++ [casn2]) ∗
history_elem γ casn2.
#[local] Lemma history_update_running {γ casns casn1 η1} casn2 η2 i :
casn1 ≠ casn2 →
history_auth γ (casns ++ [casn1]) -∗
meta casn1 nroot η1 -∗
lstatus_lb η1 Finished -∗
meta casn2 nroot η2 -∗
lstatus_auth η2 (Running i) ==∗
history_auth γ ((casns ++ [casn1]) ++ [casn2]) ∗
history_elem γ casn2 ∗
lstatus_auth η2 (Running i).
#[local] Lemma lock_alloc :
⊢ |==>
∃ η_lock,
lock' η_lock.
#[local] Lemma lock_allocs n :
⊢ |==>
∃ ηs_lock,
⌜length ηs_lock = n⌝ ∗
[∗ list] η_lock ∈ ηs_lock,
lock' η_lock.
#[local] Lemma lock_exclusive η i :
lock η i -∗
lock η i -∗
False.
#[local] Lemma helpers_alloc :
⊢ |==>
∃ η_helpers,
helpers_auth' η_helpers ∅.
#[local] Lemma helpers_insert {η helpers} i P :
helpers_auth η helpers ⊢ |==>
∃ helper,
helpers_auth η (<[helper := i]> helpers) ∗
helpers_elem η helper i ∗
saved_prop helper P.
#[local] Lemma helpers_lookup η helpers helper i :
helpers_auth η helpers -∗
helpers_elem η helper i -∗
⌜helpers !! helper = Some i⌝.
#[local] Lemma helpers_delete η helpers helper i :
helpers_auth η helpers -∗
helpers_elem η helper i ==∗
helpers_auth η (delete helper helpers).
#[local] Lemma winning_alloc :
⊢ |==>
∃ η_winning,
winning' η_winning.
#[local] Lemma winning_exclusive η :
winning η -∗
winning η -∗
False.
#[local] Lemma owner_alloc :
⊢ |==>
∃ η_owner,
owner' η_owner.
#[local] Lemma owner_exclusive η :
owner η -∗
owner η -∗
False.
Opaque model₂'.
Opaque history_auth'.
Opaque history_lb.
Lemma kcas_1_loc_model_exclusive loc v1 v2 :
kcas_1_loc_model loc v1 -∗
kcas_1_loc_model loc v2 -∗
False.
#[local] Lemma casn_help {casn η ι Ψ i} descr P :
η.(metadata_descrs) !! i = Some descr →
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) -∗
lock η i -∗
helper_au' η ι descr P -∗
|={⊤ ∖ ↑loc_inv_name ι}=>
∃ helper,
lock η i ∗
saved_prop helper P ∗
helpers_elem η helper i.
#[local] Lemma casn_retrieve casn η ι Ψ helper P i :
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) -∗
lstatus_lb η Finished -∗
saved_prop helper P -∗
helpers_elem η helper i ={⊤}=∗
▷^2 P.
#[local] Lemma status𑁒spec_finished casn η ι :
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#casn).{status}
{{{
RET metadata_final η;
True
}}}.
#[local] Lemma before𑁒spec {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
{{{
casn_inv' ι casn η
}}}
(#descr.(descriptor_state)).{before}
{{{
v
, RET v;
⌜v = descr.(descriptor_before)⌝
∨ lstatus_lb η Finished
}}}.
#[local] Lemma before𑁒spec_finished {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = false →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)).{before}
{{{
RET descr.(descriptor_before);
True
}}}.
#[local] Lemma set_before𑁒spec_finished {casn η ι} i descr v :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = true →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)) <-{before} v
{{{
RET ();
True
}}}.
#[local] Lemma after𑁒spec_finished {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = true →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)).{after}
{{{
RET descr.(descriptor_after);
True
}}}.
#[local] Lemma set_after𑁒spec_finished {casn η ι} i descr v :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = false →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)) <-{after} v
{{{
RET ();
True
}}}.
#[local] Lemma kcas_1٠status_to_bool𑁒spec fstatus :
{{{
True
}}}
kcas_1٠status_to_bool (final_status_to_val fstatus)
{{{
RET #(final_status_to_bool fstatus);
True
}}}.
#[local] Lemma kcas_1٠clear𑁒spec casn η ι b :
b = metadata_success η →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
kcas_1٠clear (metadata_cass_val η) #b
{{{
RET ();
True
}}}.
#[local] Lemma kcas_1٠finish𑁒spec {gid casn η ι} fstatus :
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
( ( ⌜gid ≠ metadata_winner η⌝ ∗
identifier_model' gid
) ∨ (
∃ Ψ,
⌜fstatus = FinalBefore⌝ ∗
winning η ∗
saved_pred η.(metadata_post) Ψ ∗
Ψ false
) ∨ (
∃ i,
⌜gid = metadata_winner η⌝ ∗
identifier_model' gid ∗
⌜fstatus = FinalAfter⌝ ∗
⌜metadata_size η ≤ i⌝ ∗
lstatus_lb η (Running i)
) ∨ (
lstatus_lb η Finished
)
)
}}}
kcas_1٠finish #gid #casn (final_status_to_val fstatus)
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_loser {gid casn η ι} fstatus :
gid ≠ metadata_winner η →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
identifier_model' gid
}}}
kcas_1٠finish #gid #casn (final_status_to_val fstatus)
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_winner_before gid casn η ι Ψ :
gid = metadata_winner η →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
winning η ∗
saved_pred η.(metadata_post) Ψ ∗
Ψ false
}}}
kcas_1٠finish #gid #casn §Before
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_after {gid casn η ι} i :
metadata_size η ≤ i →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
identifier_model' gid ∗
lstatus_lb η (Running i)
}}}
kcas_1٠finish #gid #casn §After
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_finished gid casn η ι :
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
kcas_1٠finish #gid #casn §Before
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma descriptor_state_inj {ι casn1 η1 casn2 η2} i1 descr1 i2 descr2 :
casn1 ≠ casn2 →
η1.(metadata_descrs) !! i1 = Some descr1 →
η2.(metadata_descrs) !! i2 = Some descr2 →
casn_inv' ι casn1 η1 -∗
casn_inv' ι casn2 η2 ={⊤ ∖ ↑loc_inv_name ι}=∗
⌜descr1.(descriptor_state) ≠ descr2.(descriptor_state)⌝.
#[local] Lemma kcas_1٠determine_as_eval_determine𑁒spec ι :
⊢ (
∀ casn η 𝑐𝑎𝑠𝑠 i,
{{{
⌜𝑐𝑎𝑠𝑠 = list_to_val (drop i (metadata_cass η))⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i)
}}}
kcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
) ∧ (
∀ casn η i descr casn1 η1 i1 descr1 casns1 𝑟𝑒𝑡𝑟𝑦 𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒,
{{{
⌜𝑟𝑒𝑡𝑟𝑦 = list_to_val (drop i (metadata_cass η))⌝ ∗
⌜𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒 = list_to_val (drop (S i) (metadata_cass η))⌝ ∗
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜η1.(metadata_descrs) !! i1 = Some descr1⌝ ∗
⌜descr1.(descriptor_loc) = descr.(descriptor_loc)⌝ ∗
⌜descr1.(descriptor_meta) = descr.(descriptor_meta)⌝ ∗
⌜casn1 ≠ casn⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i) ∗
meta casn1 nroot η1 ∗
casn_inv' ι casn1 η1 ∗
lstatus_lb η1 Finished ∗
history_lb descr.(descriptor_meta) (casns1 ++ [casn1]) ∗
( lstatus_lb η Finished
∨ ⌜descriptor_final descr1 η1 ≈ descr.(descriptor_before)⌝
)
}}}
kcas_1٠lock #casn #descr.(descriptor_loc) #descr1.(descriptor_state) #descr.(descriptor_state) 𝑟𝑒𝑡𝑟𝑦 𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
) ∧ (
∀ casn η i descr,
{{{
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠eval #descr.(descriptor_state)
{{{
RET descriptor_final descr η;
lstatus_lb η Finished ∗
£ 1
}}}
) ∧ (
∀ casn η,
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠determine #casn
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
).
#[local] Lemma kcas_1٠determine_as𑁒spec casn η ι 𝑐𝑎𝑠𝑠 i :
𝑐𝑎𝑠𝑠 = list_to_val (drop i (metadata_cass η)) →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i)
}}}
kcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠eval𑁒spec {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠eval #descr.(descriptor_state)
{{{
RET descriptor_final descr η;
lstatus_lb η Finished ∗
£ 1
}}}.
#[local] Lemma kcas_1٠determine𑁒spec casn η ι :
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠determine #casn
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
Lemma kcas_1٠make𑁒spec ι v :
{{{
True
}}}
kcas_1٠make v
{{{
loc
, RET #loc;
kcas_1_loc_inv loc ι ∗
kcas_1_loc_model loc v
}}}.
Lemma kcas_1٠get𑁒spec loc ι :
<<<
kcas_1_loc_inv loc ι
| ∀∀ v,
kcas_1_loc_model loc v
>>>
kcas_1٠get #loc @ ↑ι
<<<
kcas_1_loc_model loc v
| w,
RET w;
⌜v ≈ w⌝
>>>.
Lemma kcas_1٠cas𑁒spec {ι 𝑠𝑝𝑒𝑐} locs befores afters :
length locs = length befores →
length locs = length afters →
NoDup locs →
list_model' 𝑠𝑝𝑒𝑐 $ zip3_with (λ loc before after, (#loc, before, after)%V) locs befores afters →
<<<
[∗ list] loc ∈ locs, kcas_1_loc_inv loc ι
| ∀∀ vs,
[∗ list] loc; v ∈ locs; vs, kcas_1_loc_model loc v
>>>
kcas_1٠cas 𝑠𝑝𝑒𝑐 @ ↑ι
<<<
∃∃ b,
if b then
⌜vs ≈ befores⌝ ∗
[∗ list] loc; v ∈ locs; afters, kcas_1_loc_model loc v
else
∃ i before v,
⌜befores !! i = Some before⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜v ≉ before⌝ ∗
[∗ list] loc; v ∈ locs; vs, kcas_1_loc_model loc v
| RET #b;
True
>>>.
End kcas_1_G.
From zoo_kcas Require
kcas_1__opaque.
#[global] Opaque kcas_1_loc_inv.
#[global] Opaque kcas_1_loc_model.
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable
list.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.excl
lib.saved_prop
lib.saved_pred
lib.mono_list.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_bool
identifier.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
list.
From zoo_kcas Require Import
kcas_1__types.
From zoo_kcas Require Export
kcas_1__code.
From zoo Require Import
options.
Implicit Types b full : bool.
Implicit Types i : nat.
Implicit Types l loc casn : location.
Implicit Types casns : list location.
Implicit Types gid : identifier.
Implicit Types v w state : val.
Implicit Types vs befores afters : list val.
Implicit Types cas : location × (val × val).
Implicit Types cass : list (location × (val × val)).
Implicit Types helpers : gmap gname nat.
#[local] Program Definition global_prophet :=
{|prophet_typed_type :=
identifier × bool
; prophet_typed_of_val v :=
match v with
| ValTuple [ValProph gid; ValBool b] ⇒
Some (gid, b)
| _ ⇒
None
end
; prophet_typed_to_val '(gid, b) :=
(#gid, #b)%V
|}.
Solve Obligations of global_prophet with
try done.
Implicit Types prophs : list global_prophet.(prophet_typed_type).
Record loc_metadata :=
{ loc_metadata_model : gname
; loc_metadata_history : gname
}.
Implicit Types γ : loc_metadata.
#[local] Instance loc_metadata_inhabited : Inhabited loc_metadata :=
populate
{|loc_metadata_model := inhabitant
; loc_metadata_history := inhabitant
|}.
#[local] Instance loc_metadata_eq_dec : EqDecision loc_metadata :=
ltac:(solve_decision).
#[local] Instance loc_metadata_countable :
Countable loc_metadata.
Record descriptor :=
{ descriptor_loc : location
; descriptor_meta : loc_metadata
; descriptor_before : val
; descriptor_after : val
; descriptor_state : location
}.
Implicit Types descr : descriptor.
Implicit Types descrs : list descriptor.
#[local] Definition descriptor_cas descr : val :=
(#descr.(descriptor_loc), #descr.(descriptor_state)).
#[local] Instance descriptor_inhabited : Inhabited descriptor :=
populate
{|descriptor_loc := inhabitant
; descriptor_meta := inhabitant
; descriptor_before := inhabitant
; descriptor_after := inhabitant
; descriptor_state := inhabitant
|}.
#[local] Instance descriptor_eq_dec : EqDecision descriptor :=
ltac:(solve_decision).
#[local] Instance descriptor_countable :
Countable descriptor.
Variant status :=
| Undetermined
| After
| Before.
Implicit Types status : status.
Variant final_status :=
| FinalAfter
| FinalBefore.
Implicit Types fstatus : final_status.
Definition final_status_to_bool fstatus :=
if fstatus then true else false.
#[global] Arguments final_status_to_bool !_ : assert.
Definition final_status_of_bool b :=
if b then FinalAfter else FinalBefore.
#[global] Arguments final_status_of_bool !_ : assert.
Definition final_status_to_val fstatus :=
match fstatus with
| FinalAfter ⇒
§After
| FinalBefore ⇒
§Before
end%V.
#[global] Arguments final_status_to_val !_ : assert.
#[local] Lemma final_status_to_of_bool b :
final_status_to_bool (final_status_of_bool b) = b.
#[local] Lemma final_status_to_val_undetermined fstatus bid 𝑐𝑎𝑠𝑠 :
¬ final_status_to_val fstatus ≈ ‘Undetermined@bid[ 𝑐𝑎𝑠𝑠 ]%V.
Record metadata :=
{ metadata_descrs : list descriptor
; metadata_prophet : prophet_id
; metadata_prophs : list global_prophet.(prophet_typed_type)
; metadata_undetermined : block_id
; metadata_post : gname
; metadata_lstatus : gname
; metadata_locks : list gname
; metadata_helpers : gname
; metadata_winning : gname
; metadata_owner : gname
}.
Implicit Types η : metadata.
#[local] Instance metadata_inhabited : Inhabited metadata :=
populate
{|metadata_descrs := inhabitant
; metadata_prophet := inhabitant
; metadata_prophs := inhabitant
; metadata_undetermined := inhabitant
; metadata_post := inhabitant
; metadata_lstatus := inhabitant
; metadata_locks := inhabitant
; metadata_helpers := inhabitant
; metadata_winning := inhabitant
; metadata_owner := inhabitant
|}.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition metadata_size η :=
length η.(metadata_descrs).
#[local] Definition metadata_cass η :=
descriptor_cas <$> η.(metadata_descrs).
#[local] Definition metadata_cass_val η :=
list_to_val $ metadata_cass η.
#[local] Definition metadata_outcome η :=
hd inhabitant η.(metadata_prophs).
#[local] Definition metadata_winner η :=
(metadata_outcome η).1.
#[local] Definition metadata_success η :=
(metadata_outcome η).2.
#[local] Definition metadata_final η :=
final_status_to_val $ final_status_of_bool $ metadata_success η.
#[local] Instance status_inhabited : Inhabited status :=
populate Undetermined.
#[local] Definition status_to_val η status : val :=
match status with
| Undetermined ⇒
‘Undetermined@η.(metadata_undetermined)[ metadata_cass_val η ]
| After ⇒
§After
| Before ⇒
§Before
end.
Variant lstatus :=
| Running i
| Finished.
Implicit Types lstatus : lstatus.
#[local] Instance lstatus_inhabited : Inhabited lstatus :=
populate Finished.
Variant lstep : lstatus → lstatus → Prop :=
| lstep_incr i :
lstep (Running i) (Running (S i))
| lstep_finish i :
lstep (Running i) Finished.
#[local] Hint Constructors lstep : core.
#[local] Lemma lsteps_running0 lstatus :
rtc lstep (Running 0) lstatus.
#[local] Lemma lstep_finished lstatus :
¬ lstep Finished lstatus.
#[local] Lemma lsteps_finished lstatus :
rtc lstep Finished lstatus →
lstatus = Finished.
#[local] Lemma lsteps_le lstatus1 i1 lstatus2 i2 :
rtc lstep lstatus1 lstatus2 →
lstatus1 = Running i1 →
lstatus2 = Running i2 →
i1 ≤ i2.
#[local] Definition descriptor_final descr η :=
if metadata_success η then
descr.(descriptor_after)
else
descr.(descriptor_before).
Class Kcas1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] kcas_1_G_model_G :: TwinsG Σ val_O
; #[local] kcas_1_G_helper_G :: SavedPropG Σ
; #[local] kcas_1_G_post_G :: SavedPredG Σ bool
; #[local] kcas_1_G_lstatus_G :: AuthMonoG (A := leibnizO lstatus) Σ lstep
; #[local] kcas_1_G_history_G :: MonoListG Σ location
; #[local] kcas_1_G_lock_G :: ExclG Σ unitO
; #[local] kcas_1_G_helpers_G :: ghost_mapG Σ gname nat
; #[local] kcas_1_G_winning_G :: ExclG Σ unitO
; #[local] kcas_1_G_owner_G :: ExclG Σ unitO
}.
Definition kcas_1_Σ :=
#[twins_Σ val_O
; saved_prop_Σ
; saved_pred_Σ bool
; auth_mono_Σ (A := leibnizO lstatus) lstep
; mono_list_Σ location
; excl_Σ unitO
; ghost_mapΣ gname nat
; excl_Σ unitO
; excl_Σ unitO
].
#[global] Instance subG_kcas_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG kcas_1_Σ Σ →
Kcas1G Σ.
Section kcas_1_G.
Context `{kcas_1_G : Kcas1G Σ}.
Implicit Types P : iProp Σ.
#[local] Definition model₁' γ_model v :=
twins_twin1 γ_model (DfracOwn 1) v.
#[local] Definition model₁ γ v :=
model₁' γ.(loc_metadata_model) v.
#[local] Definition model₂' γ_model v : iProp Σ :=
∃ w,
⌜v ≈ w⌝ ∗
twins_twin2 γ_model w.
#[local] Definition model₂ γ v :=
model₂' γ.(loc_metadata_model) v.
#[local] Definition lstatus_auth' η_lstatus lstatus :=
auth_mono_auth _ η_lstatus (DfracOwn 1) lstatus.
#[local] Definition lstatus_auth η lstatus :=
lstatus_auth' η.(metadata_lstatus) lstatus.
#[local] Definition lstatus_lb η lstatus :=
auth_mono_lb _ η.(metadata_lstatus) lstatus.
#[local] Definition history_auth' γ_history casns : iProp Σ :=
mono_list_auth γ_history (DfracOwn 1) casns ∗
⌜NoDup casns⌝ ∗
[∗ list] casn ∈ removelast casns,
∃ η,
meta casn nroot η ∗
lstatus_lb η Finished.
#[local] Definition history_auth γ casns :=
history_auth' γ.(loc_metadata_history) casns.
#[local] Definition history_lb γ casns : iProp Σ :=
mono_list_lb γ.(loc_metadata_history) casns ∗
⌜NoDup casns⌝.
#[local] Definition history_elem' γ_history casn : iProp Σ :=
mono_list_elem γ_history casn.
#[local] Definition history_elem γ casn :=
history_elem' γ.(loc_metadata_history) casn.
#[local] Definition lock' η_lock :=
excl η_lock ().
#[local] Definition lock η i : iProp Σ :=
∃ η_lock,
⌜η.(metadata_locks) !! i = Some η_lock⌝ ∗
lock' η_lock.
#[local] Definition helpers_auth' η_helpers helpers :=
ghost_map_auth η_helpers 1 helpers.
#[local] Definition helpers_auth η helpers :=
helpers_auth' η.(metadata_helpers) helpers.
#[local] Definition helpers_elem η helper i :=
ghost_map_elem η.(metadata_helpers) helper (DfracOwn 1) i.
#[local] Definition winning' η_winning :=
excl η_winning ().
#[local] Definition winning η :=
winning' η.(metadata_winning).
#[local] Definition owner' η_owner :=
excl η_owner ().
#[local] Definition owner η :=
owner' η.(metadata_owner).
#[local] Definition au η ι Ψ : iProp Σ :=
AU <{
∃∃ vs,
[∗ list] descr; v ∈ η.(metadata_descrs); vs,
model₁ descr.(descriptor_meta) v
}> @ ⊤ ∖ ↑ι, ∅ <{
∀∀ b,
if b then
⌜vs ≈ descriptor_before <$> η.(metadata_descrs)⌝ ∗
[∗ list] descr ∈ η.(metadata_descrs),
model₁ descr.(descriptor_meta) descr.(descriptor_after)
else
∃ i descr v,
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜descr.(descriptor_before) ≉ v⌝ ∗
[∗ list] descr; v ∈ η.(metadata_descrs); vs,
model₁ descr.(descriptor_meta) v
, COMM
Ψ b
}>.
#[local] Definition helper_au' η ι descr P : iProp Σ :=
AU <{
∃∃ v,
model₁ descr.(descriptor_meta) v
}> @ ⊤ ∖ ↑ι, ∅ <{
⌜v ≈ descriptor_final descr η⌝ ∗
model₁ descr.(descriptor_meta) v
, COMM
P
}>.
#[local] Definition helper_au η ι i P : iProp Σ :=
∃ descr,
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
helper_au' η ι descr P.
#[local] Definition casn_inv_name ι casn :=
ι.@"casn".@casn.
#[local] Definition casn_inv_inner casn η ι Ψ : iProp Σ :=
∃ 𝑠𝑡𝑎𝑡𝑢𝑠 lstatus helpers prophs,
casn.[status] ↦ 𝑠𝑡𝑎𝑡𝑢𝑠 ∗
lstatus_auth η lstatus ∗
helpers_auth η helpers ∗
prophet_typed_model global_prophet η.(metadata_prophet) prophs ∗
match lstatus with
| Running i ⇒
⌜𝑠𝑡𝑎𝑡𝑢𝑠 = status_to_val η Undetermined⌝ ∗
⌜prophs = η.(metadata_prophs)⌝ ∗
( au η ι Ψ ∗
winning η
∨ identifier_model' (metadata_winner η)
) ∗
( [∗ map] helper ↦ j ∈ helpers,
∃ P,
⌜j < i⌝ ∗
saved_prop helper P ∗
helper_au η ι j P
) ∗
( [∗ list] descr ∈ η.(metadata_descrs),
descr.(descriptor_state).[before] ↦ descr.(descriptor_before) ∗
descr.(descriptor_state).[after] ↦ descr.(descriptor_after)
) ∗
( [∗ list] descr ∈ take i η.(metadata_descrs),
model₂ descr.(descriptor_meta) descr.(descriptor_before) ∗
history_elem descr.(descriptor_meta) casn
) ∗
( [∗ list] j ∈ seq i (metadata_size η - i),
lock η j
)
| Finished ⇒
⌜𝑠𝑡𝑎𝑡𝑢𝑠 = metadata_final η⌝ ∗
identifier_model' (metadata_winner η) ∗
(owner η ∨ Ψ (metadata_success η)) ∗
( [∗ map] helper ↦ _ ∈ helpers,
∃ P,
saved_prop helper P ∗
P
) ∗
( [∗ list] i ↦ descr ∈ η.(metadata_descrs),
( model₂ descr.(descriptor_meta) (descriptor_final descr η)
∨ lock η i
) ∗
if metadata_success η then
history_elem descr.(descriptor_meta) casn ∗
descr.(descriptor_state).[after] ↦ descr.(descriptor_after) ∗
descr.(descriptor_state).[before] ↦-
else
descr.(descriptor_state).[before] ↦ descr.(descriptor_before) ∗
descr.(descriptor_state).[after] ↦-
)
end.
#[local] Instance : CustomIpat "casn_inv_inner" :=
" ( %status{} & %lstatus{} & %helpers{} & %prophs{} & >Hcasn{}_status & >Hlstatus{}_auth & >Hhelpers{}_auth & >Hgproph{} & Hlstatus{} ) ".
#[local] Instance : CustomIpat "casn_inv_inner_running" :=
" ( {>;}-> & {>;}-> & Hau{} & Hhelpers{} & {>;}Hdescrs{} & {>;}Hmodels₂{} & {>;}Hlocks{} ) ".
#[local] Instance : CustomIpat "casn_inv_inner_finished" :=
" ( {>;}-> & {>;}Hwinner{} & HΨ{} & Hhelpers{} & {>;}Hdescrs{} ) ".
#[local] Definition casn_inv_pre ι
(casn_inv' : location × metadata × option nat -d> iProp Σ)
(loc_inv' : location × loc_metadata -d> iProp Σ)
: location × metadata × option nat -d> iProp Σ
:=
λ '(casn, η, i), (
∃ Ψ,
casn.[proph] ↦□ #η.(metadata_prophet) ∗
saved_pred η.(metadata_post) Ψ ∗
⌜NoDup (descriptor_loc <$> η.(metadata_descrs))⌝ ∗
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) ∗
[∗ list] j ↦ descr ∈ η.(metadata_descrs),
if i is Some i then
if decide (j = i) then
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn
else
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn ∗
loc_inv' (descr.(descriptor_loc), descr.(descriptor_meta))
else
meta descr.(descriptor_loc) nroot descr.(descriptor_meta) ∗
descr.(descriptor_state).[casn] ↦□ #casn ∗
loc_inv' (descr.(descriptor_loc), descr.(descriptor_meta))
)%I.
#[local] Instance : CustomIpat "casn_inv" :=
" ( %Ψ{} & Hcasn{}_proph & Hpost{} & %Hlocs{} & Hcasn{}_inv & Hlocs{} ) ".
#[local] Instance casn_inv_pre_contractive ι n :
Proper (dist_later n ==> (≡{n}≡) ==> (≡{n}≡)) (casn_inv_pre ι).
#[local] Definition loc_inv_name ι :=
ι.@"loc".
#[local] Definition loc_inv_inner'' full casn_inv' loc γ : iProp Σ :=
∃ casns casn η i descr,
meta casn nroot η ∗
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜loc = descr.(descriptor_loc)⌝ ∗
loc ↦ᵣ #descr.(descriptor_state) ∗
lstatus_lb η (Running (S i)) ∗
lock η i ∗
history_auth γ (casns ++ [casn]) ∗
casn_inv' (casn, η, if full then None else Some i).
#[local] Instance : CustomIpat "loc_inv_inner" :=
" ( %casns{} & %casn{} & %η{} & %i{} & %descr{} & {>;}{#}Hcasn{}_meta & {>;}%Hdescrs{}_lookup & {>;}{%Hloc{};->} & {>;}Hloc & {>;}{#}Hlstatus{}_lb & {>;}Hlock{} & {>;}Hhistory_auth & {#}Hcasn{}_inv' ) ".
#[local] Definition loc_inv_inner' :=
loc_inv_inner'' false.
#[local] Definition loc_inv_pre ι
(casn_inv' : location × metadata × option nat -d> iProp Σ)
(loc_inv' : location × loc_metadata -d> iProp Σ)
: location × loc_metadata -d> iProp Σ
:=
λ '(loc, γ),
inv (loc_inv_name ι) (loc_inv_inner' casn_inv' loc γ).
#[local] Instance loc_inv_pre_contractive ι n :
Proper (dist_later n ==> dist_later n ==> (≡{n}≡)) (loc_inv_pre ι).
#[local] Definition casn_inv'' ι :=
fixpoint_A (casn_inv_pre ι) (loc_inv_pre ι).
#[local] Definition casn_inv' ι casn η :=
casn_inv'' ι (casn, η, None).
#[local] Definition casn_inv casn ι : iProp Σ :=
∃ η,
meta casn nroot η ∗
casn_inv' ι casn η.
#[local] Definition loc_inv' ι :=
fixpoint_B (casn_inv_pre ι) (loc_inv_pre ι).
#[local] Definition loc_inv_inner loc γ ι : iProp Σ :=
loc_inv_inner'' true (casn_inv'' ι) loc γ.
Definition kcas_1_loc_inv loc ι : iProp Σ :=
∃ γ,
meta loc nroot γ ∗
loc_inv' ι (loc, γ).
Definition kcas_1_loc_model loc v : iProp Σ :=
∃ γ,
meta loc nroot γ ∗
model₁ γ v.
#[local] Instance : CustomIpat "loc_model" :=
" ( %γ{} & Hmeta{_{}} & Hmodel₁{_{}} ) ".
#[local] Lemma casn_inv''_unfold ι casn (i : option nat) η :
casn_inv'' ι (casn, η, i) ⊣⊢
casn_inv_pre ι (casn_inv'' ι) (loc_inv' ι) (casn, η, i).
#[local] Lemma casn_inv'_unfold ι casn η :
casn_inv' ι casn η ⊣⊢
casn_inv_pre ι (casn_inv'' ι) (loc_inv' ι) (casn, η, None).
#[local] Lemma loc_inv'_unfold loc γ ι :
loc_inv' ι (loc, γ) ⊣⊢
inv (loc_inv_name ι) (loc_inv_inner' (casn_inv'' ι) loc γ).
#[local] Lemma loc_inv'_intro loc γ ι :
inv (loc_inv_name ι) (loc_inv_inner' (casn_inv'' ι) loc γ) ⊢
loc_inv' ι (loc, γ).
#[local] Lemma loc_inv'_elim loc γ ι :
meta loc nroot γ -∗
loc_inv' ι (loc, γ) -∗
inv (loc_inv_name ι) (loc_inv_inner loc γ ι).
#[local] Instance model₂_timeless γ v :
Timeless (model₂ γ v).
#[local] Instance history_auth_timeless γ casns :
Timeless (history_auth γ casns).
#[local] Instance lock_timeless η i :
Timeless (lock η i).
#[global] Instance kcas_1_loc_model_timeless loc ι :
Timeless (kcas_1_loc_model loc ι).
#[local] Instance history_lb_persistent γ casns :
Persistent (history_lb γ casns).
#[local] Instance loc_inv'_persistent loc γ ι :
Persistent (loc_inv' ι (loc, γ)).
#[global] Instance kcas_1_loc_inv_persistent loc γ ι :
Persistent (kcas_1_loc_inv loc ι).
#[local] Instance casn_inv''_persistent casn η (i : option nat) ι :
Persistent (casn_inv'' ι (casn, η, i)).
#[local] Instance casn_inv'_persistent casn η ι :
Persistent (casn_inv' ι casn η).
#[local] Lemma model_alloc v :
⊢ |==>
∃ γ_model,
model₁' γ_model v ∗
model₂' γ_model v.
#[local] Lemma model₁_exclusive γ v1 v2 :
model₁ γ v1 -∗
model₁ γ v2 -∗
False.
#[local] Lemma model₂_similar {γ v1} v2 :
v1 ≈ v2 →
model₂ γ v1 ⊢
model₂ γ v2.
#[local] Lemma model₂_exclusive γ v1 v2 :
model₂ γ v1 -∗
model₂ γ v2 -∗
False.
#[local] Lemma model_agree γ v1 v2 :
model₁ γ v1 -∗
model₂ γ v2 -∗
⌜v1 ≈ v2⌝.
#[local] Lemma model_update {γ v1 v2} v :
model₁ γ v1 -∗
model₂ γ v2 ==∗
model₁ γ v ∗
model₂ γ v.
#[local] Lemma lstatus_alloc lstatus :
⊢ |==>
∃ η_lstatus,
lstatus_auth' η_lstatus lstatus.
#[local] Lemma lstatus_lb_get η lstatus :
lstatus_auth η lstatus ⊢
lstatus_lb η lstatus.
#[local] Lemma lstatus_lb_get_running0 η lstatus :
lstatus_auth η lstatus ⊢
lstatus_lb η (Running 0).
#[local] Lemma lstatus_lb_get_finished {η} lstatus :
lstatus_auth η Finished ⊢
lstatus_lb η lstatus.
#[local] Lemma lstatus_finished η lstatus :
lstatus_auth η lstatus -∗
lstatus_lb η Finished -∗
⌜lstatus = Finished⌝.
#[local] Lemma lstatus_le η i1 i2 :
lstatus_auth η (Running i1) -∗
lstatus_lb η (Running i2) -∗
⌜i2 ≤ i1⌝.
#[local] Lemma lstatus_update {η lstatus} lstatus' :
lstep lstatus lstatus' →
lstatus_auth η lstatus ⊢ |==>
lstatus_auth η lstatus'.
#[local] Lemma history_alloc casn :
⊢ |==>
∃ γ_history,
history_auth' γ_history [casn] ∗
history_elem' γ_history casn.
#[local] Lemma history_lb_get γ casns :
history_auth γ casns ⊢
history_lb γ casns.
#[local] Lemma history_lb_valid_eq γ casns1 casn casns2 casns3 :
history_auth γ (casns1 ++ [casn]) -∗
history_lb γ (casns2 ++ casn :: casns3) -∗
⌜casns1 = casns2⌝ ∗
⌜casns3 = []⌝.
#[local] Lemma history_lb_valid_ne γ casns1 casn1 casns2 casn2 :
casn1 ≠ casn2 →
history_auth γ (casns1 ++ [casn1]) -∗
history_lb γ (casns2 ++ [casn2]) -∗
∃ casns3,
history_lb γ (casns2 ++ [casn2] ++ casns3 ++ [casn1]).
#[local] Lemma history_elem_valid γ casns casn :
history_auth γ casns -∗
history_elem γ casn -∗
⌜casn ∈ casns⌝.
#[local] Lemma history_running γ casns casn1 casn2 η2 i :
history_auth γ (casns ++ [casn1]) -∗
meta casn2 nroot η2 -∗
lstatus_auth η2 (Running i) -∗
⌜casn2 ∉ casns⌝.
#[local] Lemma history_update {γ casns casn1 η1} casn2 :
casn2 ∉ casns →
casn2 ≠ casn1 →
history_auth γ (casns ++ [casn1]) -∗
meta casn1 nroot η1 -∗
lstatus_lb η1 Finished ==∗
history_auth γ ((casns ++ [casn1]) ++ [casn2]) ∗
history_elem γ casn2.
#[local] Lemma history_update_running {γ casns casn1 η1} casn2 η2 i :
casn1 ≠ casn2 →
history_auth γ (casns ++ [casn1]) -∗
meta casn1 nroot η1 -∗
lstatus_lb η1 Finished -∗
meta casn2 nroot η2 -∗
lstatus_auth η2 (Running i) ==∗
history_auth γ ((casns ++ [casn1]) ++ [casn2]) ∗
history_elem γ casn2 ∗
lstatus_auth η2 (Running i).
#[local] Lemma lock_alloc :
⊢ |==>
∃ η_lock,
lock' η_lock.
#[local] Lemma lock_allocs n :
⊢ |==>
∃ ηs_lock,
⌜length ηs_lock = n⌝ ∗
[∗ list] η_lock ∈ ηs_lock,
lock' η_lock.
#[local] Lemma lock_exclusive η i :
lock η i -∗
lock η i -∗
False.
#[local] Lemma helpers_alloc :
⊢ |==>
∃ η_helpers,
helpers_auth' η_helpers ∅.
#[local] Lemma helpers_insert {η helpers} i P :
helpers_auth η helpers ⊢ |==>
∃ helper,
helpers_auth η (<[helper := i]> helpers) ∗
helpers_elem η helper i ∗
saved_prop helper P.
#[local] Lemma helpers_lookup η helpers helper i :
helpers_auth η helpers -∗
helpers_elem η helper i -∗
⌜helpers !! helper = Some i⌝.
#[local] Lemma helpers_delete η helpers helper i :
helpers_auth η helpers -∗
helpers_elem η helper i ==∗
helpers_auth η (delete helper helpers).
#[local] Lemma winning_alloc :
⊢ |==>
∃ η_winning,
winning' η_winning.
#[local] Lemma winning_exclusive η :
winning η -∗
winning η -∗
False.
#[local] Lemma owner_alloc :
⊢ |==>
∃ η_owner,
owner' η_owner.
#[local] Lemma owner_exclusive η :
owner η -∗
owner η -∗
False.
Opaque model₂'.
Opaque history_auth'.
Opaque history_lb.
Lemma kcas_1_loc_model_exclusive loc v1 v2 :
kcas_1_loc_model loc v1 -∗
kcas_1_loc_model loc v2 -∗
False.
#[local] Lemma casn_help {casn η ι Ψ i} descr P :
η.(metadata_descrs) !! i = Some descr →
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) -∗
lock η i -∗
helper_au' η ι descr P -∗
|={⊤ ∖ ↑loc_inv_name ι}=>
∃ helper,
lock η i ∗
saved_prop helper P ∗
helpers_elem η helper i.
#[local] Lemma casn_retrieve casn η ι Ψ helper P i :
inv (casn_inv_name ι casn) (casn_inv_inner casn η ι Ψ) -∗
lstatus_lb η Finished -∗
saved_prop helper P -∗
helpers_elem η helper i ={⊤}=∗
▷^2 P.
#[local] Lemma status𑁒spec_finished casn η ι :
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#casn).{status}
{{{
RET metadata_final η;
True
}}}.
#[local] Lemma before𑁒spec {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
{{{
casn_inv' ι casn η
}}}
(#descr.(descriptor_state)).{before}
{{{
v
, RET v;
⌜v = descr.(descriptor_before)⌝
∨ lstatus_lb η Finished
}}}.
#[local] Lemma before𑁒spec_finished {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = false →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)).{before}
{{{
RET descr.(descriptor_before);
True
}}}.
#[local] Lemma set_before𑁒spec_finished {casn η ι} i descr v :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = true →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)) <-{before} v
{{{
RET ();
True
}}}.
#[local] Lemma after𑁒spec_finished {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = true →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)).{after}
{{{
RET descr.(descriptor_after);
True
}}}.
#[local] Lemma set_after𑁒spec_finished {casn η ι} i descr v :
η.(metadata_descrs) !! i = Some descr →
metadata_success η = false →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
(#descr.(descriptor_state)) <-{after} v
{{{
RET ();
True
}}}.
#[local] Lemma kcas_1٠status_to_bool𑁒spec fstatus :
{{{
True
}}}
kcas_1٠status_to_bool (final_status_to_val fstatus)
{{{
RET #(final_status_to_bool fstatus);
True
}}}.
#[local] Lemma kcas_1٠clear𑁒spec casn η ι b :
b = metadata_success η →
{{{
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
kcas_1٠clear (metadata_cass_val η) #b
{{{
RET ();
True
}}}.
#[local] Lemma kcas_1٠finish𑁒spec {gid casn η ι} fstatus :
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
( ( ⌜gid ≠ metadata_winner η⌝ ∗
identifier_model' gid
) ∨ (
∃ Ψ,
⌜fstatus = FinalBefore⌝ ∗
winning η ∗
saved_pred η.(metadata_post) Ψ ∗
Ψ false
) ∨ (
∃ i,
⌜gid = metadata_winner η⌝ ∗
identifier_model' gid ∗
⌜fstatus = FinalAfter⌝ ∗
⌜metadata_size η ≤ i⌝ ∗
lstatus_lb η (Running i)
) ∨ (
lstatus_lb η Finished
)
)
}}}
kcas_1٠finish #gid #casn (final_status_to_val fstatus)
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_loser {gid casn η ι} fstatus :
gid ≠ metadata_winner η →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
identifier_model' gid
}}}
kcas_1٠finish #gid #casn (final_status_to_val fstatus)
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_winner_before gid casn η ι Ψ :
gid = metadata_winner η →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
winning η ∗
saved_pred η.(metadata_post) Ψ ∗
Ψ false
}}}
kcas_1٠finish #gid #casn §Before
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_after {gid casn η ι} i :
metadata_size η ≤ i →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
identifier_model' gid ∗
lstatus_lb η (Running i)
}}}
kcas_1٠finish #gid #casn §After
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠finish𑁒spec_finished gid casn η ι :
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η Finished
}}}
kcas_1٠finish #gid #casn §Before
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma descriptor_state_inj {ι casn1 η1 casn2 η2} i1 descr1 i2 descr2 :
casn1 ≠ casn2 →
η1.(metadata_descrs) !! i1 = Some descr1 →
η2.(metadata_descrs) !! i2 = Some descr2 →
casn_inv' ι casn1 η1 -∗
casn_inv' ι casn2 η2 ={⊤ ∖ ↑loc_inv_name ι}=∗
⌜descr1.(descriptor_state) ≠ descr2.(descriptor_state)⌝.
#[local] Lemma kcas_1٠determine_as_eval_determine𑁒spec ι :
⊢ (
∀ casn η 𝑐𝑎𝑠𝑠 i,
{{{
⌜𝑐𝑎𝑠𝑠 = list_to_val (drop i (metadata_cass η))⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i)
}}}
kcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
) ∧ (
∀ casn η i descr casn1 η1 i1 descr1 casns1 𝑟𝑒𝑡𝑟𝑦 𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒,
{{{
⌜𝑟𝑒𝑡𝑟𝑦 = list_to_val (drop i (metadata_cass η))⌝ ∗
⌜𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒 = list_to_val (drop (S i) (metadata_cass η))⌝ ∗
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
⌜η1.(metadata_descrs) !! i1 = Some descr1⌝ ∗
⌜descr1.(descriptor_loc) = descr.(descriptor_loc)⌝ ∗
⌜descr1.(descriptor_meta) = descr.(descriptor_meta)⌝ ∗
⌜casn1 ≠ casn⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i) ∗
meta casn1 nroot η1 ∗
casn_inv' ι casn1 η1 ∗
lstatus_lb η1 Finished ∗
history_lb descr.(descriptor_meta) (casns1 ++ [casn1]) ∗
( lstatus_lb η Finished
∨ ⌜descriptor_final descr1 η1 ≈ descr.(descriptor_before)⌝
)
}}}
kcas_1٠lock #casn #descr.(descriptor_loc) #descr1.(descriptor_state) #descr.(descriptor_state) 𝑟𝑒𝑡𝑟𝑦 𝑐𝑜𝑛𝑡𝑖𝑛𝑢𝑒
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
) ∧ (
∀ casn η i descr,
{{{
⌜η.(metadata_descrs) !! i = Some descr⌝ ∗
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠eval #descr.(descriptor_state)
{{{
RET descriptor_final descr η;
lstatus_lb η Finished ∗
£ 1
}}}
) ∧ (
∀ casn η,
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠determine #casn
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}
).
#[local] Lemma kcas_1٠determine_as𑁒spec casn η ι 𝑐𝑎𝑠𝑠 i :
𝑐𝑎𝑠𝑠 = list_to_val (drop i (metadata_cass η)) →
{{{
meta casn nroot η ∗
casn_inv' ι casn η ∗
lstatus_lb η (Running i)
}}}
kcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
#[local] Lemma kcas_1٠eval𑁒spec {casn η ι} i descr :
η.(metadata_descrs) !! i = Some descr →
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠eval #descr.(descriptor_state)
{{{
RET descriptor_final descr η;
lstatus_lb η Finished ∗
£ 1
}}}.
#[local] Lemma kcas_1٠determine𑁒spec casn η ι :
{{{
meta casn nroot η ∗
casn_inv' ι casn η
}}}
kcas_1٠determine #casn
{{{
RET #(metadata_success η);
lstatus_lb η Finished
}}}.
Lemma kcas_1٠make𑁒spec ι v :
{{{
True
}}}
kcas_1٠make v
{{{
loc
, RET #loc;
kcas_1_loc_inv loc ι ∗
kcas_1_loc_model loc v
}}}.
Lemma kcas_1٠get𑁒spec loc ι :
<<<
kcas_1_loc_inv loc ι
| ∀∀ v,
kcas_1_loc_model loc v
>>>
kcas_1٠get #loc @ ↑ι
<<<
kcas_1_loc_model loc v
| w,
RET w;
⌜v ≈ w⌝
>>>.
Lemma kcas_1٠cas𑁒spec {ι 𝑠𝑝𝑒𝑐} locs befores afters :
length locs = length befores →
length locs = length afters →
NoDup locs →
list_model' 𝑠𝑝𝑒𝑐 $ zip3_with (λ loc before after, (#loc, before, after)%V) locs befores afters →
<<<
[∗ list] loc ∈ locs, kcas_1_loc_inv loc ι
| ∀∀ vs,
[∗ list] loc; v ∈ locs; vs, kcas_1_loc_model loc v
>>>
kcas_1٠cas 𝑠𝑝𝑒𝑐 @ ↑ι
<<<
∃∃ b,
if b then
⌜vs ≈ befores⌝ ∗
[∗ list] loc; v ∈ locs; afters, kcas_1_loc_model loc v
else
∃ i before v,
⌜befores !! i = Some before⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜v ≉ before⌝ ∗
[∗ list] loc; v ∈ locs; vs, kcas_1_loc_model loc v
| RET #b;
True
>>>.
End kcas_1_G.
From zoo_kcas Require
kcas_1__opaque.
#[global] Opaque kcas_1_loc_inv.
#[global] Opaque kcas_1_loc_model.