Library zoo_mcas.mcas_1
Require Import iris.base_logic.lib.ghost_map.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_bool.
Require Import zoo.program_logic.identifier.
Require Export zoo_mcas.mcas_1__code.
Require Import zoo_mcas.mcas_1__types.
Require Import zoo.options.
Implicit Type b full : bool.
Implicit Type i : nat.
Implicit Type loc casn : location.
Implicit Type casns : list location.
Implicit Type gid : identifier.
Implicit Type v w state : val.
Implicit Type vs befores afters : list val.
Implicit Type cas : location × (val × val).
Implicit Type cass : list (location × (val × val)).
Implicit Type helpers : gmap gname nat.
#[local] Definition global_prophet :=
{|prophet_typed۰type :=
identifier × bool
; prophet_typed۰of_val _ v :=
match v with
| ValTuple [ValProph gid; ValBool b] ⇒
Some $ Some (gid, b)
| _ ⇒
None
end
|}.
Implicit Type prophs : list global_prophet.(prophet_typed۰type).
Record loc۰metadata :=
{ loc۰metadata۰model : gname
; loc۰metadata۰history : gname
}.
Implicit Type γ : 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 Type descr : descriptor.
Implicit Type 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 Type status : status.
Variant final_status :=
| FinalAfter
| FinalBefore.
Implicit Type 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_boolｰ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 Type η : 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 Type lstatus : lstatus.
#[local] Instance lstatusｰinhabited : Inhabited lstatus :=
populate Finished.
Variant lstep : lstatus → lstatus → Prop :=
| lstepｰincr i :
lstep (Running i) (Running ˖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 Mcas1G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] mcas_1۰G۰model۰G :: TwinsG Σ val_O
; #[local] mcas_1۰G۰helper۰G :: SavedPropG Σ
; #[local] mcas_1۰G۰post۰G :: SavedPredG Σ bool
; #[local] mcas_1۰G۰lstatus۰G :: AuthMonoG (A := leibnizO lstatus) Σ lstep
; #[local] mcas_1۰G۰history۰G :: MonoListG Σ location
; #[local] mcas_1۰G۰lock۰G :: ExclG Σ unitO
; #[local] mcas_1۰G۰helpers۰G :: ghost_mapG Σ gname nat
; #[local] mcas_1۰G۰winning۰G :: ExclG Σ unitO
; #[local] mcas_1۰G۰owner۰G :: ExclG Σ unitO
}.
Definition mcas_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ｰmcas_1۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG mcas_1۰Σ Σ →
Mcas1G Σ.
Section mcas_1۰G.
Context `{mcas_1۰G : Mcas1G Σ}.
Implicit Type P : iProp Σ.
#[local] Definition model₁' γ_model v :=
twins۰twin₁ γ_model (DfracOwn 1) v.
#[local] Definition model₁ γ v :=
model₁' γ.(loc۰metadata۰model) v.
#[local] Definition model₂' γ_model v : iProp Σ :=
∃ w,
⌜v ≈ w⌝ ∗
twins۰twin₂ γ_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,
∃ η,
casn ↪ η ∗
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
descr.(descriptor۰loc) ↪ descr.(descriptor۰meta) ∗
descr.(descriptor۰state).[casn] ↦□ #casn
else
descr.(descriptor۰loc) ↪ descr.(descriptor۰meta) ∗
descr.(descriptor۰state).[casn] ↦□ #casn ∗
loc۰inv' (descr.(descriptor۰loc), descr.(descriptor۰meta))
else
descr.(descriptor۰loc) ↪ 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,
casn ↪ η ∗
⌜η.(metadata۰descrs) !! i = Some descr⌝ ∗
⌜loc = descr.(descriptor۰loc)⌝ ∗
loc ↦ᵣ #descr.(descriptor۰state) ∗
lstatus۰lb η (Running ˖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 Σ :=
∃ η,
casn ↪ η ∗
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 mcas_1۰loc۰inv loc ι : iProp Σ :=
∃ γ,
loc ↪ γ ∗
loc۰inv' ι (loc, γ).
Definition mcas_1۰loc۰model loc v : iProp Σ :=
∃ γ,
loc ↪ γ ∗
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 γ ι :
loc ↪ γ -∗
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 mcas_1۰loc۰modelｰtimeless loc ι :
Timeless (mcas_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 mcas_1۰loc۰invｰpersistent loc γ ι :
Persistent (mcas_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]) -∗
casn2 ↪ η2 -∗
lstatus۰auth η2 (Running i) -∗
⌜casn2 ∉ casns⌝.
#[local] Lemma historyｰupdate {γ casns casn1 η1} casn2 :
casn2 ∉ casns →
casn2 ≠ casn1 →
history۰auth γ (casns ++ [casn1]) -∗
casn1 ↪ η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]) -∗
casn1 ↪ η1 -∗
lstatus۰lb η1 Finished -∗
casn2 ↪ η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 mcas_1۰loc۰modelｰexclusive loc v1 v2 :
mcas_1۰loc۰model loc v1 -∗
mcas_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 mcas_1٠status_to_boolｰspec fstatus :
{{{
True
}}}
mcas_1٠status_to_bool (final_status۰to_val fstatus)
{{{
RET #(final_status۰to_bool fstatus);
True
}}}.
#[local] Lemma mcas_1٠clearｰspec casn η ι b :
b = metadata۰success η →
{{{
casn۰inv' ι casn η ∗
lstatus۰lb η Finished
}}}
mcas_1٠clear (metadata۰cass۰val η) #b
{{{
RET ();
True
}}}.
#[local] Lemma mcas_1٠finishｰspec {gid casn η ι} fstatus :
{{{
casn ↪ η ∗
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
)
)
}}}
mcas_1٠finish #gid #casn (final_status۰to_val fstatus)
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰloser {gid casn η ι} fstatus :
gid ≠ metadata۰winner η →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
identifier۰model gid
}}}
mcas_1٠finish #gid #casn (final_status۰to_val fstatus)
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰwinnerｰbefore gid casn η ι Ψ :
gid = metadata۰winner η →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
winning η ∗
saved_pred η.(metadata۰post) Ψ ∗
Ψ false
}}}
mcas_1٠finish #gid #casn §Before
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰafter {gid casn η ι} i :
metadata۰size η ≤ i →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
identifier۰model gid ∗
lstatus۰lb η (Running i)
}}}
mcas_1٠finish #gid #casn §After
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰfinished gid casn η ι :
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η Finished
}}}
mcas_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 mcas_1٠determine_asｰevalｰdetermineｰspec ι :
⊢ (
∀ casn η 𝑐𝑎𝑠𝑠 i,
{{{
⌜𝑐𝑎𝑠𝑠 = list۰to_val (drop i (metadata۰cass η))⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i)
}}}
mcas_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 ˖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⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i) ∗
casn1 ↪ η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)⌝
)
}}}
mcas_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⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠eval #descr.(descriptor۰state)
{{{
RET descriptor۰final descr η;
lstatus۰lb η Finished ∗
£ 1
}}}
) ∧ (
∀ casn η,
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠determine #casn
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}
).
#[local] Lemma mcas_1٠determine_asｰspec casn η ι 𝑐𝑎𝑠𝑠 i :
𝑐𝑎𝑠𝑠 = list۰to_val (drop i (metadata۰cass η)) →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i)
}}}
mcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠evalｰspec {casn η ι} i descr :
η.(metadata۰descrs) !! i = Some descr →
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠eval #descr.(descriptor۰state)
{{{
RET descriptor۰final descr η;
lstatus۰lb η Finished ∗
£ 1
}}}.
#[local] Lemma mcas_1٠determineｰspec casn η ι :
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠determine #casn
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
Lemma mcas_1٠makeｰspec ι v :
{{{
True
}}}
mcas_1٠make v
{{{
loc
, RET #loc;
mcas_1۰loc۰inv loc ι ∗
mcas_1۰loc۰model loc v
}}}.
Lemma mcas_1٠getｰspec loc ι :
<<<
mcas_1۰loc۰inv loc ι
| ∀∀ v,
mcas_1۰loc۰model loc v
>>>
mcas_1٠get #loc @ ↑ι
<<<
mcas_1۰loc۰model loc v
| w,
RET w;
⌜v ≈ w⌝
>>>.
Lemma mcas_1٠mcasｰ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, mcas_1۰loc۰inv loc ι
| ∀∀ vs,
[∗ list] loc; v ∈ locs; vs, mcas_1۰loc۰model loc v
>>>
mcas_1٠mcas 𝑠𝑝𝑒𝑐 @ ↑ι
<<<
∃∃ b,
if b then
⌜vs ≈ befores⌝ ∗
[∗ list] loc; v ∈ locs; afters, mcas_1۰loc۰model loc v
else
∃ i before v,
⌜befores !! i = Some before⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜v ≉ before⌝ ∗
[∗ list] loc; v ∈ locs; vs, mcas_1۰loc۰model loc v
| RET #b;
True
>>>.
End mcas_1۰G.
Require zoo_mcas.mcas_1__opaque.
#[global] Opaque mcas_1۰loc۰inv.
#[global] Opaque mcas_1۰loc۰model.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_bool.
Require Import zoo.program_logic.identifier.
Require Export zoo_mcas.mcas_1__code.
Require Import zoo_mcas.mcas_1__types.
Require Import zoo.options.
Implicit Type b full : bool.
Implicit Type i : nat.
Implicit Type loc casn : location.
Implicit Type casns : list location.
Implicit Type gid : identifier.
Implicit Type v w state : val.
Implicit Type vs befores afters : list val.
Implicit Type cas : location × (val × val).
Implicit Type cass : list (location × (val × val)).
Implicit Type helpers : gmap gname nat.
#[local] Definition global_prophet :=
{|prophet_typed۰type :=
identifier × bool
; prophet_typed۰of_val _ v :=
match v with
| ValTuple [ValProph gid; ValBool b] ⇒
Some $ Some (gid, b)
| _ ⇒
None
end
|}.
Implicit Type prophs : list global_prophet.(prophet_typed۰type).
Record loc۰metadata :=
{ loc۰metadata۰model : gname
; loc۰metadata۰history : gname
}.
Implicit Type γ : 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 Type descr : descriptor.
Implicit Type 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 Type status : status.
Variant final_status :=
| FinalAfter
| FinalBefore.
Implicit Type 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_boolｰ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 Type η : 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 Type lstatus : lstatus.
#[local] Instance lstatusｰinhabited : Inhabited lstatus :=
populate Finished.
Variant lstep : lstatus → lstatus → Prop :=
| lstepｰincr i :
lstep (Running i) (Running ˖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 Mcas1G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] mcas_1۰G۰model۰G :: TwinsG Σ val_O
; #[local] mcas_1۰G۰helper۰G :: SavedPropG Σ
; #[local] mcas_1۰G۰post۰G :: SavedPredG Σ bool
; #[local] mcas_1۰G۰lstatus۰G :: AuthMonoG (A := leibnizO lstatus) Σ lstep
; #[local] mcas_1۰G۰history۰G :: MonoListG Σ location
; #[local] mcas_1۰G۰lock۰G :: ExclG Σ unitO
; #[local] mcas_1۰G۰helpers۰G :: ghost_mapG Σ gname nat
; #[local] mcas_1۰G۰winning۰G :: ExclG Σ unitO
; #[local] mcas_1۰G۰owner۰G :: ExclG Σ unitO
}.
Definition mcas_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ｰmcas_1۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG mcas_1۰Σ Σ →
Mcas1G Σ.
Section mcas_1۰G.
Context `{mcas_1۰G : Mcas1G Σ}.
Implicit Type P : iProp Σ.
#[local] Definition model₁' γ_model v :=
twins۰twin₁ γ_model (DfracOwn 1) v.
#[local] Definition model₁ γ v :=
model₁' γ.(loc۰metadata۰model) v.
#[local] Definition model₂' γ_model v : iProp Σ :=
∃ w,
⌜v ≈ w⌝ ∗
twins۰twin₂ γ_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,
∃ η,
casn ↪ η ∗
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
descr.(descriptor۰loc) ↪ descr.(descriptor۰meta) ∗
descr.(descriptor۰state).[casn] ↦□ #casn
else
descr.(descriptor۰loc) ↪ descr.(descriptor۰meta) ∗
descr.(descriptor۰state).[casn] ↦□ #casn ∗
loc۰inv' (descr.(descriptor۰loc), descr.(descriptor۰meta))
else
descr.(descriptor۰loc) ↪ 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,
casn ↪ η ∗
⌜η.(metadata۰descrs) !! i = Some descr⌝ ∗
⌜loc = descr.(descriptor۰loc)⌝ ∗
loc ↦ᵣ #descr.(descriptor۰state) ∗
lstatus۰lb η (Running ˖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 Σ :=
∃ η,
casn ↪ η ∗
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 mcas_1۰loc۰inv loc ι : iProp Σ :=
∃ γ,
loc ↪ γ ∗
loc۰inv' ι (loc, γ).
Definition mcas_1۰loc۰model loc v : iProp Σ :=
∃ γ,
loc ↪ γ ∗
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 γ ι :
loc ↪ γ -∗
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 mcas_1۰loc۰modelｰtimeless loc ι :
Timeless (mcas_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 mcas_1۰loc۰invｰpersistent loc γ ι :
Persistent (mcas_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]) -∗
casn2 ↪ η2 -∗
lstatus۰auth η2 (Running i) -∗
⌜casn2 ∉ casns⌝.
#[local] Lemma historyｰupdate {γ casns casn1 η1} casn2 :
casn2 ∉ casns →
casn2 ≠ casn1 →
history۰auth γ (casns ++ [casn1]) -∗
casn1 ↪ η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]) -∗
casn1 ↪ η1 -∗
lstatus۰lb η1 Finished -∗
casn2 ↪ η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 mcas_1۰loc۰modelｰexclusive loc v1 v2 :
mcas_1۰loc۰model loc v1 -∗
mcas_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 mcas_1٠status_to_boolｰspec fstatus :
{{{
True
}}}
mcas_1٠status_to_bool (final_status۰to_val fstatus)
{{{
RET #(final_status۰to_bool fstatus);
True
}}}.
#[local] Lemma mcas_1٠clearｰspec casn η ι b :
b = metadata۰success η →
{{{
casn۰inv' ι casn η ∗
lstatus۰lb η Finished
}}}
mcas_1٠clear (metadata۰cass۰val η) #b
{{{
RET ();
True
}}}.
#[local] Lemma mcas_1٠finishｰspec {gid casn η ι} fstatus :
{{{
casn ↪ η ∗
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
)
)
}}}
mcas_1٠finish #gid #casn (final_status۰to_val fstatus)
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰloser {gid casn η ι} fstatus :
gid ≠ metadata۰winner η →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
identifier۰model gid
}}}
mcas_1٠finish #gid #casn (final_status۰to_val fstatus)
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰwinnerｰbefore gid casn η ι Ψ :
gid = metadata۰winner η →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
winning η ∗
saved_pred η.(metadata۰post) Ψ ∗
Ψ false
}}}
mcas_1٠finish #gid #casn §Before
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰafter {gid casn η ι} i :
metadata۰size η ≤ i →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
identifier۰model gid ∗
lstatus۰lb η (Running i)
}}}
mcas_1٠finish #gid #casn §After
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠finishｰspecｰfinished gid casn η ι :
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η Finished
}}}
mcas_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 mcas_1٠determine_asｰevalｰdetermineｰspec ι :
⊢ (
∀ casn η 𝑐𝑎𝑠𝑠 i,
{{{
⌜𝑐𝑎𝑠𝑠 = list۰to_val (drop i (metadata۰cass η))⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i)
}}}
mcas_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 ˖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⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i) ∗
casn1 ↪ η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)⌝
)
}}}
mcas_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⌝ ∗
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠eval #descr.(descriptor۰state)
{{{
RET descriptor۰final descr η;
lstatus۰lb η Finished ∗
£ 1
}}}
) ∧ (
∀ casn η,
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠determine #casn
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}
).
#[local] Lemma mcas_1٠determine_asｰspec casn η ι 𝑐𝑎𝑠𝑠 i :
𝑐𝑎𝑠𝑠 = list۰to_val (drop i (metadata۰cass η)) →
{{{
casn ↪ η ∗
casn۰inv' ι casn η ∗
lstatus۰lb η (Running i)
}}}
mcas_1٠determine_as #casn 𝑐𝑎𝑠𝑠
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
#[local] Lemma mcas_1٠evalｰspec {casn η ι} i descr :
η.(metadata۰descrs) !! i = Some descr →
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠eval #descr.(descriptor۰state)
{{{
RET descriptor۰final descr η;
lstatus۰lb η Finished ∗
£ 1
}}}.
#[local] Lemma mcas_1٠determineｰspec casn η ι :
{{{
casn ↪ η ∗
casn۰inv' ι casn η
}}}
mcas_1٠determine #casn
{{{
RET #(metadata۰success η);
lstatus۰lb η Finished
}}}.
Lemma mcas_1٠makeｰspec ι v :
{{{
True
}}}
mcas_1٠make v
{{{
loc
, RET #loc;
mcas_1۰loc۰inv loc ι ∗
mcas_1۰loc۰model loc v
}}}.
Lemma mcas_1٠getｰspec loc ι :
<<<
mcas_1۰loc۰inv loc ι
| ∀∀ v,
mcas_1۰loc۰model loc v
>>>
mcas_1٠get #loc @ ↑ι
<<<
mcas_1۰loc۰model loc v
| w,
RET w;
⌜v ≈ w⌝
>>>.
Lemma mcas_1٠mcasｰ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, mcas_1۰loc۰inv loc ι
| ∀∀ vs,
[∗ list] loc; v ∈ locs; vs, mcas_1۰loc۰model loc v
>>>
mcas_1٠mcas 𝑠𝑝𝑒𝑐 @ ↑ι
<<<
∃∃ b,
if b then
⌜vs ≈ befores⌝ ∗
[∗ list] loc; v ∈ locs; afters, mcas_1۰loc۰model loc v
else
∃ i before v,
⌜befores !! i = Some before⌝ ∗
⌜vs !! i = Some v⌝ ∗
⌜v ≉ before⌝ ∗
[∗ list] loc; v ∈ locs; vs, mcas_1۰loc۰model loc v
| RET #b;
True
>>>.
End mcas_1۰G.
Require zoo_mcas.mcas_1__opaque.
#[global] Opaque mcas_1۰loc۰inv.
#[global] Opaque mcas_1۰loc۰model.