Library zoo_saturn.ws_bdeque_1
From zoo Require Import
prelude.
From zoo.common Require Import
countable
function
relations.
From zoo.iris.base_logic Require Import
lib.auth_nat_max
lib.auth_twins
lib.excl
lib.mono_list
lib.twins.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
identifier
prophet_identifier
prophet_multi.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array
domain
option.
From zoo_saturn Require Export
base
ws_bdeque_1__code.
From zoo_saturn Require Import
ws_bdeque_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front front_cache back : nat.
Implicit Types id : prophet_id.
Implicit Types v : val.
Implicit Types us vs ws hist priv : list val.
Implicit Types past prophs : list prophet_identifier.(prophet_typed_type).
Implicit Types pasts prophss : nat → list prophet_identifier.(prophet_typed_type).
Variant state :=
| Empty
| Nonempty
| Emptyish
| Superempty.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Empty.
Variant stability :=
| Stable
| Unstable.
Implicit Types stable : stability.
#[local] Instance stability_inhabited : Inhabited stability :=
populate Stable.
Class WsBdeque1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_bdeque_1_G_prophet_G :: ProphetMultiG Σ prophet_identifier
; #[local] ws_bdeque_1_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] ws_bdeque_1_G_owner_G :: TwinsG Σ (leibnizO (stability × nat))
; #[local] ws_bdeque_1_G_front_G :: AuthNatMaxG Σ
; #[local] ws_bdeque_1_G_history_G :: MonoListG Σ val
; #[local] ws_bdeque_1_G_winner_G :: TwinsG Σ (natO × ▶ ∙)
}.
Definition ws_bdeque_1_Σ :=
#[prophet_multi_Σ prophet_identifier
; auth_twins_Σ (leibnizO (list val)) suffix
; twins_Σ (leibnizO (stability × nat))
; auth_nat_max_Σ
; mono_list_Σ val
; twins_Σ (natO × ▶ ∙)
].
#[global] Instance subG_ws_bdeque_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_bdeque_1_Σ Σ →
WsBdeque1G Σ .
Module base.
Section ws_bdeque_1_G.
Context `{ws_bdeque_1_G : WsBdeque1G Σ}.
Implicit Types t : location.
Implicit Types P : iProp Σ.
Record ws_bdeque_1_name :=
{ ws_bdeque_1_name_capacity : nat
; ws_bdeque_1_name_data : val
; ws_bdeque_1_name_inv : namespace
; ws_bdeque_1_name_prophet : prophet_id
; ws_bdeque_1_name_prophet_name : prophet_multi_name
; ws_bdeque_1_name_model : auth_twins_name
; ws_bdeque_1_name_owner : gname
; ws_bdeque_1_name_front : gname
; ws_bdeque_1_name_history : gname
; ws_bdeque_1_name_winner : gname
}.
Implicit Types γ : ws_bdeque_1_name.
#[global] Instance ws_bdeque_1_name_eq_dec : EqDecision ws_bdeque_1_name :=
ltac:(solve_decision).
#[global] Instance ws_bdeque_1_name_countable :
Countable ws_bdeque_1_name.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_bdeque_1_name_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_bdeque_1_name_model).
#[local] Definition owner₁' γ_owner γ_model stable back ws : iProp Σ :=
twins_twin1 (twins_G := ws_bdeque_1_G_owner_G) γ_owner (DfracOwn 1) (stable, back) ∗
auth_twins_auth _ γ_model ws.
#[local] Definition owner₁ γ :=
owner₁' γ.(ws_bdeque_1_name_owner) γ.(ws_bdeque_1_name_model).
#[local] Instance : CustomIpat "owner₁" :=
" ( Howner₁{_{}} & Hmodel_auth{_{}} ) ".
#[local] Definition owner₂' γ_owner stable back :=
twins_twin2 (twins_G := ws_bdeque_1_G_owner_G) γ_owner (stable, back).
#[local] Definition owner₂ γ :=
owner₂' γ.(ws_bdeque_1_name_owner).
#[local] Definition front_auth' γ_front :=
auth_nat_max_auth γ_front (DfracOwn 1).
#[local] Definition front_auth γ :=
front_auth' γ.(ws_bdeque_1_name_front).
#[local] Definition front_lb γ :=
auth_nat_max_lb γ.(ws_bdeque_1_name_front).
#[local] Definition history_auth' γ_history :=
mono_list_auth γ_history (DfracOwn 1).
#[local] Definition history_auth γ :=
history_auth' γ.(ws_bdeque_1_name_history).
#[local] Definition history_at γ :=
mono_list_at γ.(ws_bdeque_1_name_history).
#[local] Definition winner_pop' γ_winner front P : iProp Σ :=
twins_twin1 γ_winner (DfracOwn 1) (front, Next P).
#[local] Definition winner_pop γ :=
winner_pop' γ.(ws_bdeque_1_name_winner).
#[local] Definition winner_steal' γ_winner front P :=
twins_twin2 γ_winner (front, Next P).
#[local] Definition winner_steal γ :=
winner_steal' γ.(ws_bdeque_1_name_winner).
#[local] Definition winner γ : iProp Σ :=
∃ front P1 P2,
winner_pop γ front P1 ∗
winner_steal γ front P2.
#[local] Instance : CustomIpat "winner" :=
" ( %front_winner & %P_winner_1 & %P_winner_2 & Hwinner_pop{_{}} & Hwinner_steal{_{}} ) ".
#[local] Definition winner_au γ front P : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(ws_bdeque_1_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs' ∗
history_at γ front v
, COMM
P
}>.
#[local] Definition winner_pending_1 γ front P id : iProp Σ :=
winner_steal γ front P ∗
identifier_model' id ∗
winner_au γ front P.
#[local] Instance : CustomIpat "winner_pending_1" :=
" ( Hwinner_steal{_{!}} & Hid{_{!}} & HP ) ".
#[local] Definition winner_pending_2 γ front id : iProp Σ :=
∃ P,
winner_pending_1 γ front P id.
#[local] Instance : CustomIpat "winner_pending_2" :=
" ( %P{} & (:winner_pending_1) ) ".
#[local] Definition winner_linearized γ front P : iProp Σ :=
winner_steal γ front P ∗
P.
#[local] Instance : CustomIpat "winner_linearized" :=
" ( Hwinner_steal{_{!}} & HP ) ".
#[local] Definition inv_state_empty γ stable front back hist : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv_state_empty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv_state_nonempty γ stable front back hist vs prophs : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant vs) ∗
( winner γ
∨ match prophs with
| [] ⇒
False
| id :: _ ⇒
winner_pending_2 γ front id
end
).
#[local] Instance : CustomIpat "inv_state_nonempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}% & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_nonempty_steal γ state stable front back hist vs prophs P : iProp Σ :=
⌜state = Nonempty⌝ ∗
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant vs) ∗
match prophs with
| [] ⇒
False
| id :: _ ⇒
winner_pending_1 γ front P id
end.
#[local] Instance : CustomIpat "inv_state_nonempty_steal" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}% & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_emptyish γ stable front back hist priv : iProp Σ :=
∃ P,
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
( winner_pop γ front P
∨ winner_linearized γ front P
).
#[local] Instance : CustomIpat "inv_state_emptyish" :=
" ( %P_ & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_emptyish_pop γ state stable front back hist priv P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
winner_pop γ front P.
#[local] Instance : CustomIpat "inv_state_emptyish_pop" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner_pop ) ".
#[local] Definition inv_state_emptyish_steal γ state stable front back hist priv P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
winner_linearized γ front P.
#[local] Instance : CustomIpat "inv_state_emptyish_steal" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & (:winner_linearized) ) ".
#[local] Definition inv_state_superempty γ stable front back hist : iProp Σ :=
⌜stable = Unstable⌝ ∗
⌜front = S back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv_state_superempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv_state γ state stable front back hist vs priv prophs : iProp Σ :=
match state with
| Empty ⇒
inv_state_empty γ stable front back hist
| Nonempty ⇒
inv_state_nonempty γ stable front back hist vs prophs
| Emptyish ⇒
inv_state_emptyish γ stable front back hist priv
| Superempty ⇒
inv_state_superempty γ stable front back hist
end.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ state stable front back hist vs priv pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
owner₂ γ stable back ∗
front_auth γ front ∗
⌜0 < front⌝ ∗
model₂ γ vs ∗
⌜length vs = back - front⌝ ∗
array_cslice γ.(ws_bdeque_1_name_data) γ.(ws_bdeque_1_name_capacity) front (DfracOwn (1/2)) (vs ++ priv) ∗
⌜(length vs + length priv)%nat = γ.(ws_bdeque_1_name_capacity)⌝ ∗
history_auth γ hist ∗
prophet_multi_model prophet_identifier γ.(ws_bdeque_1_name_prophet) γ.(ws_bdeque_1_name_prophet_name) pasts prophss ∗
⌜∀ i, front ≤ i → pasts i = []⌝ ∗
inv_state γ state stable front back hist vs priv (prophss front).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %state{} & %stable{} & %front{} & %back{} & %hist{} & %vs{} & %priv{} & %pasts{} & %prophss{} & >Ht_front & >Ht_back & >Howner₂ & >Hfront_auth & >%Hfront{} & >Hmodel₂ & >%Hvs{} & >Hdata_cslice₁ & >%Hdata{} & >Hhistory_auth & >Hprophet_model & >%Hpasts{} & Hstate ) ".
#[local] Definition inv' t γ : iProp Σ :=
⌜0 < γ.(ws_bdeque_1_name_capacity)⌝ ∗
t.[capacity] ↦□ #γ.(ws_bdeque_1_name_capacity) ∗
t.[data] ↦□ γ.(ws_bdeque_1_name_data) ∗
t.[proph] ↦□ #γ.(ws_bdeque_1_name_prophet) ∗
inv γ.(ws_bdeque_1_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( %Hcapacity & #Ht_capacity & #Ht_data & #Ht_proph & #Hinv ) ".
Definition ws_bdeque_1_inv t γ ι cap : iProp Σ :=
⌜ι = γ.(ws_bdeque_1_name_inv)⌝ ∗
⌜cap = γ.(ws_bdeque_1_name_capacity)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & -> & (:inv') ) ".
Definition ws_bdeque_1_model γ vs : iProp Σ :=
model₁ γ vs ∗
⌜length vs ≤ γ.(ws_bdeque_1_name_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( Hmodel₁{_{}} & %Hvs{} ) ".
Variant owner_flag :=
| OwnerNormal
| OwnerPop.
#[local] Definition owner_1 flag t γ stable back ws front_cache i us : iProp Σ :=
owner₁ γ stable back ws ∗
t.[front_cache] ↦ #front_cache ∗
front_lb γ front_cache ∗
⌜(if flag is OwnerPop then S back else back) ≤ front_cache + γ.(ws_bdeque_1_name_capacity)⌝ ∗
array_cslice γ.(ws_bdeque_1_name_data) γ.(ws_bdeque_1_name_capacity) i (DfracOwn (1/2)) us ∗
⌜length us = γ.(ws_bdeque_1_name_capacity)⌝.
#[local] Instance : CustomIpat "owner_1" :=
" ( Howner₁{_{}} & Ht_front_cache{_{}} & { {!} _ ; #Hfront_lb_cache_{} ; #Hfront_lb_cache } & { {!} _ ; %Hfront_cache_{} ; %Hfront_cache } & Hdata_cslice₂{_{}} & { {!} _ ; %Hus{} ; %Hus } ) ".
#[local] Definition owner_2 :=
owner_1 OwnerNormal.
#[local] Instance : CustomIpat "owner_2" :=
" (:owner_1) ".
Definition ws_bdeque_1_owner t γ ws : iProp Σ :=
∃ back front_cache i us,
owner_2 t γ Stable back ws front_cache i us.
#[local] Instance : CustomIpat "owner" :=
" ( %back{} & %front_cache{_{}} & %i{} & %us{} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_1_model_timeless γ vs :
Timeless (ws_bdeque_1_model γ vs).
#[global] Instance ws_bdeque_1_owner_timeless t γ ws :
Timeless (ws_bdeque_1_owner t γ ws).
#[global] Instance ws_bdeque_1_inv_persistent t γ ι cap :
Persistent (ws_bdeque_1_inv t γ ι cap).
#[local] Lemma model_owner_alloc :
⊢ |==>
∃ γ_model γ_owner,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner₁' γ_owner γ_model Stable 1 [] ∗
owner₂' γ_owner Stable 1.
#[local] Lemma model₁_valid γ stable back ws vs :
owner₁ γ stable back ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_owner₁_agree γ stable back ws vs1 vs2 :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma model_empty {γ stable back ws vs1 vs2} :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back [] ∗
model₁ γ [] ∗
model₂ γ [].
#[local] Lemma model_push {γ stable back ws vs1 vs2} v :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_steal γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ (tail vs1) ∗
model₂ γ (tail vs1).
#[local] Lemma model_pop γ stable back ws vs1 vs2 :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma model_pop' γ stable back ws vs1 v vs2 :
owner₁ γ stable back ws -∗
model₁ γ (vs1 ++ [v]) -∗
model₂ γ vs2 ==∗
owner₁ γ stable back vs1 ∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma owner₁_exclusive γ stable1 back1 ws1 stable2 back2 ws2 :
owner₁ γ stable1 back1 ws1 -∗
owner₁ γ stable2 back2 ws2 -∗
False.
#[local] Lemma owner_agree γ stable1 back1 ws stable2 back2 :
owner₁ γ stable1 back1 ws -∗
owner₂ γ stable2 back2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝.
#[local] Lemma owner₁_update γ stable back ws vs :
owner₁ γ stable back ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner₁ γ stable back vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma owner_update {γ stable1 back1 ws stable2 back2} stable back :
owner₁ γ stable1 back1 ws -∗
owner₂ γ stable2 back2 ==∗
owner₁ γ stable back ws ∗
owner₂ γ stable back.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 1.
#[local] Lemma front_lb_get γ front :
front_auth γ front ⊢
front_lb γ front.
#[local] Lemma front_lb_le {γ front} front' :
front' ≤ front →
front_lb γ front ⊢
front_lb γ front'.
#[local] Lemma front_lb_valid γ front1 front2 :
front_auth γ front1 -∗
front_lb γ front2 -∗
⌜front2 ≤ front1⌝.
#[local] Lemma front_update γ front :
front_auth γ front ⊢ |==>
front_auth γ (S front).
#[local] Lemma history_alloc :
⊢ |==>
∃ γ_hist,
history_auth' γ_hist [()%V].
#[local] Lemma history_at_get {γ hist v} i :
i = length hist →
history_auth γ (hist ++ [v]) ⊢
history_at γ i v.
#[local] Lemma history_at_lookup γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_at_agree γ i v1 v2 :
history_at γ i v1 -∗
history_at γ i v2 -∗
⌜v1 = v2⌝.
#[local] Lemma history_update {γ hist} i v :
i = length hist →
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]) ∗
history_at γ i v.
#[local] Lemma winner_alloc :
⊢ |==>
∃ γ_winner,
winner_pop' γ_winner 1 True ∗
winner_steal' γ_winner 1 True.
#[local] Lemma winner_pop_exclusive γ front1 P1 front2 P2 :
winner_pop γ front1 P1 -∗
winner_pop γ front2 P2 -∗
False.
#[local] Lemma winner_pop_exclusive' γ front P :
winner_pop γ front P -∗
winner γ -∗
False.
#[local] Lemma winner_steal_exclusive γ front1 P1 front2 P2 :
winner_steal γ front1 P1 -∗
winner_steal γ front2 P2 -∗
False.
#[local] Lemma winner_steal_exclusive' γ front P :
winner_steal γ front P -∗
winner γ -∗
False.
#[local] Lemma winner_agree γ front1 P1 front2 P2 :
winner_pop γ front1 P1 -∗
winner_steal γ front2 P2 -∗
⌜front1 = front2⌝ ∗
▷ (P1 ≡ P2).
#[local] Lemma winner_update {γ front1 P1 front2 P2} front P :
winner_pop γ front1 P1 -∗
winner_steal γ front2 P2 ==∗
winner_pop γ front P ∗
winner_steal γ front P.
Opaque owner₁'.
Lemma ws_bdeque_1_model_valid t γ ι cap vs :
ws_bdeque_1_inv t γ ι cap -∗
ws_bdeque_1_model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_1_model_exclusive γ vs1 vs2 :
ws_bdeque_1_model γ vs1 -∗
ws_bdeque_1_model γ vs2 -∗
False.
#[local] Lemma owner_2_rebase {t γ stable back ws front_cache i1 us} i2 :
0 < γ.(ws_bdeque_1_name_capacity) →
owner_2 t γ stable back ws front_cache i1 us ⊢
∃ us,
owner_2 t γ stable back ws front_cache i2 us.
Lemma ws_bdeque_1_owner_exclusive t γ ws1 ws2 :
ws_bdeque_1_owner t γ ws1 -∗
ws_bdeque_1_owner t γ ws2 -∗
False.
Lemma ws_bdeque_1_owner_model t γ ws vs :
ws_bdeque_1_owner t γ ws -∗
ws_bdeque_1_model γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma inv_state_Stable γ state front back hist vs priv prophs :
length vs = back - front →
inv_state γ state Stable front back hist vs priv prophs ⊢
⌜state = Empty ∨ state = Nonempty⌝ ∗
⌜front ≤ back⌝.
#[local] Lemma inv_state_Unstable γ state front back hist vs priv prophs :
inv_state γ state Unstable front back hist vs priv prophs ⊢
⌜state = Emptyish ∨ state = Superempty⌝ ∗
⌜front = back ∨ front = S back⌝.
#[local] Lemma inv_state_Nonempty γ state stable front back hist vs priv prophs :
front < back →
inv_state γ state stable front back hist vs priv prophs ⊢
⌜state = Nonempty⌝.
#[local] Lemma inv_state_Superempty γ state front back hist vs priv prophs :
back < front →
inv_state γ state Unstable front back hist vs priv prophs -∗
⌜state = Superempty⌝.
#[local] Lemma inv_state_winner_pop γ state stable front1 back hist vs priv prophs front2 P :
inv_state γ state stable front1 back hist vs priv prophs -∗
winner_pop γ front2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P ≡ P_) ∗
( inv_state_nonempty_steal γ state stable front2 back hist vs prophs P_
∨ inv_state_emptyish_steal γ state stable front2 back hist priv P_
) ∗
winner_pop γ front2 P.
#[local] Lemma inv_state_winner_steal γ state stable front1 back hist vs priv prophs front2 P :
inv_state γ state stable front1 back hist vs priv prophs -∗
winner_steal γ front2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P_ ≡ P) ∗
inv_state_emptyish_pop γ state stable front2 back hist priv P_ ∗
winner_steal γ front2 P.
Lemma ws_bdeque_1٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_1٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_bdeque_1_inv t γ ι ₊cap ∗
ws_bdeque_1_model γ [] ∗
ws_bdeque_1_owner t γ []
}}}.
Lemma ws_bdeque_1٠capacity𑁒spec t γ ι cap :
{{{
ws_bdeque_1_inv t γ ι cap
}}}
ws_bdeque_1٠capacity #t
{{{
RET #cap;
True
}}}.
#[local] Lemma front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front
, RET #front;
front_lb γ front
}}}.
#[local] Lemma front𑁒spec_owner_Stable t γ back ws :
{{{
inv' t γ ∗
owner₁ γ Stable back ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Stable back ws ∗
front_lb γ front ∗
⌜front ≤ back⌝
}}}.
#[local] Lemma front𑁒spec_owner_Unstable t γ back ws :
{{{
inv' t γ ∗
owner₁ γ Unstable back ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Unstable back ws ∗
front_lb γ front ∗
⌜front = back ∨ front = S back⌝
}}}.
#[local] Lemma front𑁒spec_Superempty t γ back ws front :
back < front →
{{{
inv' t γ ∗
owner₁ γ Unstable back ws ∗
front_lb γ front
}}}
(#t).{front}
{{{
RET #front;
owner₁ γ Unstable back ws
}}}.
#[local] Lemma front𑁒spec_winner_steal t γ front P :
{{{
inv' t γ ∗
winner_steal γ front P
}}}
(#t).{front}
{{{
RET #front;
winner_steal γ front P
}}}.
#[local] Lemma back𑁒spec t γ stable back ws :
{{{
inv' t γ ∗
owner₁ γ stable back ws
}}}
(#t).{back}
{{{
RET #back;
owner₁ γ stable back ws
}}}.
#[local] Lemma set_back𑁒spec_Superempty t γ back ws front (back' : Z) :
back < front →
back' = S back →
{{{
inv' t γ ∗
owner₁ γ Unstable back ws ∗
front_lb γ front
}}}
#t <-{back} #back'
{{{
RET ();
owner₁ γ Stable (S back) ws
}}}.
#[local] Lemma array٠unsafe_cget𑁒spec_loser t γ i :
(0 ≤ i)%Z →
{{{
inv' t γ
}}}
array٠unsafe_cget γ.(ws_bdeque_1_name_data) #i
{{{
v
, RET v;
True
}}}.
#[local] Lemma array٠unsafe_cget𑁒spec_winner_pop t γ front P v :
{{{
inv' t γ ∗
winner_pop γ front P ∗
history_at γ front v
}}}
array٠unsafe_cget γ.(ws_bdeque_1_name_data) #front
{{{
RET v;
winner_pop γ front P
}}}.
#[local] Lemma array٠unsafe_cset𑁒spec_owner t γ back ws front_cache us front v :
back < front + γ.(ws_bdeque_1_name_capacity) →
{{{
inv' t γ ∗
owner_2 t γ Stable back ws front_cache back us ∗
front_lb γ front
}}}
array٠unsafe_cset γ.(ws_bdeque_1_name_data) #back v
{{{
RET ();
owner_2 t γ Stable back ws front_cache back (<[0 := v]> us)
}}}.
#[local] Lemma resolve𑁒spec_loser_1 t γ front1 front2 id :
front1 < front2 →
{{{
inv' t γ ∗
front_lb γ front2
}}}
Resolve (CAS (#t).[front]%V #front1 #(front1 + 1)) #γ.(ws_bdeque_1_name_prophet) (#front1, #id)%V
{{{
RET false;
True
}}}.
#[local] Lemma resolve𑁒spec_loser_2 t γ front id prophs0 :
head prophs0 ≠ Some id →
{{{
inv' t γ ∗
front_lb γ front ∗
prophet_multi_full prophet_identifier γ.(ws_bdeque_1_name_prophet_name) front prophs0
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET false;
front_lb γ (S front)
}}}.
#[local] Lemma resolve𑁒spec_winner_pop t γ front P id :
{{{
inv' t γ ∗
winner_pop γ front P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET true;
▷ P
}}}.
#[local] Lemma resolve𑁒spec_winner_steal t γ front P id :
{{{
inv' t γ ∗
winner_steal γ front P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET true;
front_lb γ (S front)
}}}.
#[local] Lemma resolve𑁒spec_Empty t γ back ws id :
{{{
inv' t γ ∗
owner₁ γ Stable back ws ∗
front_lb γ back
}}}
Resolve (CAS (#t).[front]%V #back #(back + 1)) #γ.(ws_bdeque_1_name_prophet) (#back, #id)%V
{{{
RET true;
owner₁ γ Unstable back ws ∗
front_lb γ (S back)
}}}.
Lemma ws_bdeque_1٠size𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ vs
| RET #(length vs);
ws_bdeque_1_owner t γ vs
>>>.
Lemma ws_bdeque_1٠is_empty𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_1_owner t γ vs
>>>.
#[local] Definition push_au t γ ws v Φ : iProp Σ :=
AU <{
∃∃ vs,
ws_bdeque_1_model γ vs
}> @ ⊤ ∖ ↑γ.(ws_bdeque_1_name_inv), ∅ <{
∀∀ b,
⌜b = bool_decide (length vs < γ.(ws_bdeque_1_name_capacity))⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ (if b then vs ++ [v] else vs)
, COMM
ws_bdeque_1_owner t γ (if b then vs ++ [v] else ws) -∗
Φ #b
}>.
Lemma ws_bdeque_1٠push𑁒spec t γ ι cap ws v :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_1_owner t γ (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_1٠steal𑁒spec t γ ι cap :
<<<
ws_bdeque_1_inv t γ ι cap
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠steal #t @ ↑ι
<<<
ws_bdeque_1_model γ (tail vs)
| RET head vs;
True
>>>.
Variant pop_state :=
| PopNonempty v
| PopEmptyishWinner v
| PopEmptyishLoser
| PopSuperempty.
#[local] Lemma ws_bdeque_1٠pop₀𑁒spec {t γ} (state : pop_state) {stable} back ws front_cache us id (back_ : Z) :
back_ = back →
{{{
inv' t γ ∗
owner_1 OwnerPop t γ stable back ws front_cache back us ∗
match state with
| PopNonempty v ⇒
⌜stable = Stable⌝ ∗
⌜us !! 0 = Some v⌝
| PopEmptyishWinner v ⇒
⌜stable = Unstable⌝ ∗
⌜us !! 0 = Some v⌝ ∗
winner_steal γ back inhabitant
| PopEmptyishLoser ⇒
∃ id_winner prophs,
⌜stable = Unstable⌝ ∗
prophet_multi_full prophet_identifier γ.(ws_bdeque_1_name_prophet_name) back (id_winner :: prophs) ∗
⌜head (id_winner :: prophs) ≠ Some id⌝
| PopSuperempty ⇒
∃ front,
⌜stable = Unstable⌝ ∗
front_lb γ front ∗
⌜front = S back⌝
end
}}}
ws_bdeque_1٠pop₀ #t #id #back_
{{{
o back front_cache i us
, RET o;
owner_2 t γ Stable back ws front_cache i us ∗
match state with
| PopNonempty v ⇒
⌜o = Some v⌝
| PopEmptyishWinner v ⇒
⌜o = Some v⌝
| PopEmptyishLoser ⇒
⌜o = None⌝
| PopSuperempty ⇒
⌜o = None⌝
end
}}}.
Lemma ws_bdeque_1٠pop𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_1_model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_1_model γ vs'
end
| RET o;
ws_bdeque_1_owner t γ ws'
>>>.
End ws_bdeque_1_G.
#[global] Opaque ws_bdeque_1_inv.
#[global] Opaque ws_bdeque_1_model.
#[global] Opaque ws_bdeque_1_owner.
End base.
From zoo_saturn Require
ws_bdeque_1__opaque.
Section ws_bdeque_1_G.
Context `{ws_bdeque_1_G : WsBdeque1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition ws_bdeque_1_inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_bdeque_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_bdeque_1_owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_owner 𝑡 γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_1_model_timeless γ vs :
Timeless (ws_bdeque_1_model γ vs).
#[global] Instance ws_bdeque_1_owner_timeless γ ws :
Timeless (ws_bdeque_1_owner γ ws).
#[global] Instance ws_bdeque_1_inv_persistent t ι cap :
Persistent (ws_bdeque_1_inv t ι cap).
Lemma ws_bdeque_1_model_valid t ι cap vs :
ws_bdeque_1_inv t ι cap -∗
ws_bdeque_1_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_1_model_exclusive t vs1 vs2 :
ws_bdeque_1_model t vs1 -∗
ws_bdeque_1_model t vs2 -∗
False.
Lemma ws_bdeque_1_owner_exclusive t ws1 ws2 :
ws_bdeque_1_owner t ws1 -∗
ws_bdeque_1_owner t ws2 -∗
False.
Lemma ws_bdeque_1_owner_model γ ws vs :
ws_bdeque_1_owner γ ws -∗
ws_bdeque_1_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_1٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_1٠create #cap
{{{
t
, RET t;
ws_bdeque_1_inv t ι ₊cap ∗
ws_bdeque_1_model t [] ∗
ws_bdeque_1_owner t []
}}}.
Lemma ws_bdeque_1٠capacity𑁒spec t ι cap :
{{{
ws_bdeque_1_inv t ι cap
}}}
ws_bdeque_1٠capacity t
{{{
RET #cap;
True
}}}.
Lemma ws_bdeque_1٠size𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t vs
| RET #(length vs);
ws_bdeque_1_owner t vs
>>>.
Lemma ws_bdeque_1٠is_empty𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_1_owner t vs
>>>.
Lemma ws_bdeque_1٠push𑁒spec t ι cap ws v :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_1_owner t (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_1٠steal𑁒spec t ι cap :
<<<
ws_bdeque_1_inv t ι cap
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠steal t @ ↑ι
<<<
ws_bdeque_1_model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_1٠pop𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_1_model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_1_model t vs'
end
| RET o;
ws_bdeque_1_owner t ws'
>>>.
End ws_bdeque_1_G.
#[global] Opaque ws_bdeque_1_inv.
#[global] Opaque ws_bdeque_1_model.
#[global] Opaque ws_bdeque_1_owner.
prelude.
From zoo.common Require Import
countable
function
relations.
From zoo.iris.base_logic Require Import
lib.auth_nat_max
lib.auth_twins
lib.excl
lib.mono_list
lib.twins.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
identifier
prophet_identifier
prophet_multi.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array
domain
option.
From zoo_saturn Require Export
base
ws_bdeque_1__code.
From zoo_saturn Require Import
ws_bdeque_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front front_cache back : nat.
Implicit Types id : prophet_id.
Implicit Types v : val.
Implicit Types us vs ws hist priv : list val.
Implicit Types past prophs : list prophet_identifier.(prophet_typed_type).
Implicit Types pasts prophss : nat → list prophet_identifier.(prophet_typed_type).
Variant state :=
| Empty
| Nonempty
| Emptyish
| Superempty.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Empty.
Variant stability :=
| Stable
| Unstable.
Implicit Types stable : stability.
#[local] Instance stability_inhabited : Inhabited stability :=
populate Stable.
Class WsBdeque1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_bdeque_1_G_prophet_G :: ProphetMultiG Σ prophet_identifier
; #[local] ws_bdeque_1_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] ws_bdeque_1_G_owner_G :: TwinsG Σ (leibnizO (stability × nat))
; #[local] ws_bdeque_1_G_front_G :: AuthNatMaxG Σ
; #[local] ws_bdeque_1_G_history_G :: MonoListG Σ val
; #[local] ws_bdeque_1_G_winner_G :: TwinsG Σ (natO × ▶ ∙)
}.
Definition ws_bdeque_1_Σ :=
#[prophet_multi_Σ prophet_identifier
; auth_twins_Σ (leibnizO (list val)) suffix
; twins_Σ (leibnizO (stability × nat))
; auth_nat_max_Σ
; mono_list_Σ val
; twins_Σ (natO × ▶ ∙)
].
#[global] Instance subG_ws_bdeque_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_bdeque_1_Σ Σ →
WsBdeque1G Σ .
Module base.
Section ws_bdeque_1_G.
Context `{ws_bdeque_1_G : WsBdeque1G Σ}.
Implicit Types t : location.
Implicit Types P : iProp Σ.
Record ws_bdeque_1_name :=
{ ws_bdeque_1_name_capacity : nat
; ws_bdeque_1_name_data : val
; ws_bdeque_1_name_inv : namespace
; ws_bdeque_1_name_prophet : prophet_id
; ws_bdeque_1_name_prophet_name : prophet_multi_name
; ws_bdeque_1_name_model : auth_twins_name
; ws_bdeque_1_name_owner : gname
; ws_bdeque_1_name_front : gname
; ws_bdeque_1_name_history : gname
; ws_bdeque_1_name_winner : gname
}.
Implicit Types γ : ws_bdeque_1_name.
#[global] Instance ws_bdeque_1_name_eq_dec : EqDecision ws_bdeque_1_name :=
ltac:(solve_decision).
#[global] Instance ws_bdeque_1_name_countable :
Countable ws_bdeque_1_name.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_bdeque_1_name_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_bdeque_1_name_model).
#[local] Definition owner₁' γ_owner γ_model stable back ws : iProp Σ :=
twins_twin1 (twins_G := ws_bdeque_1_G_owner_G) γ_owner (DfracOwn 1) (stable, back) ∗
auth_twins_auth _ γ_model ws.
#[local] Definition owner₁ γ :=
owner₁' γ.(ws_bdeque_1_name_owner) γ.(ws_bdeque_1_name_model).
#[local] Instance : CustomIpat "owner₁" :=
" ( Howner₁{_{}} & Hmodel_auth{_{}} ) ".
#[local] Definition owner₂' γ_owner stable back :=
twins_twin2 (twins_G := ws_bdeque_1_G_owner_G) γ_owner (stable, back).
#[local] Definition owner₂ γ :=
owner₂' γ.(ws_bdeque_1_name_owner).
#[local] Definition front_auth' γ_front :=
auth_nat_max_auth γ_front (DfracOwn 1).
#[local] Definition front_auth γ :=
front_auth' γ.(ws_bdeque_1_name_front).
#[local] Definition front_lb γ :=
auth_nat_max_lb γ.(ws_bdeque_1_name_front).
#[local] Definition history_auth' γ_history :=
mono_list_auth γ_history (DfracOwn 1).
#[local] Definition history_auth γ :=
history_auth' γ.(ws_bdeque_1_name_history).
#[local] Definition history_at γ :=
mono_list_at γ.(ws_bdeque_1_name_history).
#[local] Definition winner_pop' γ_winner front P : iProp Σ :=
twins_twin1 γ_winner (DfracOwn 1) (front, Next P).
#[local] Definition winner_pop γ :=
winner_pop' γ.(ws_bdeque_1_name_winner).
#[local] Definition winner_steal' γ_winner front P :=
twins_twin2 γ_winner (front, Next P).
#[local] Definition winner_steal γ :=
winner_steal' γ.(ws_bdeque_1_name_winner).
#[local] Definition winner γ : iProp Σ :=
∃ front P1 P2,
winner_pop γ front P1 ∗
winner_steal γ front P2.
#[local] Instance : CustomIpat "winner" :=
" ( %front_winner & %P_winner_1 & %P_winner_2 & Hwinner_pop{_{}} & Hwinner_steal{_{}} ) ".
#[local] Definition winner_au γ front P : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(ws_bdeque_1_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs' ∗
history_at γ front v
, COMM
P
}>.
#[local] Definition winner_pending_1 γ front P id : iProp Σ :=
winner_steal γ front P ∗
identifier_model' id ∗
winner_au γ front P.
#[local] Instance : CustomIpat "winner_pending_1" :=
" ( Hwinner_steal{_{!}} & Hid{_{!}} & HP ) ".
#[local] Definition winner_pending_2 γ front id : iProp Σ :=
∃ P,
winner_pending_1 γ front P id.
#[local] Instance : CustomIpat "winner_pending_2" :=
" ( %P{} & (:winner_pending_1) ) ".
#[local] Definition winner_linearized γ front P : iProp Σ :=
winner_steal γ front P ∗
P.
#[local] Instance : CustomIpat "winner_linearized" :=
" ( Hwinner_steal{_{!}} & HP ) ".
#[local] Definition inv_state_empty γ stable front back hist : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv_state_empty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv_state_nonempty γ stable front back hist vs prophs : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant vs) ∗
( winner γ
∨ match prophs with
| [] ⇒
False
| id :: _ ⇒
winner_pending_2 γ front id
end
).
#[local] Instance : CustomIpat "inv_state_nonempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}% & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_nonempty_steal γ state stable front back hist vs prophs P : iProp Σ :=
⌜state = Nonempty⌝ ∗
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant vs) ∗
match prophs with
| [] ⇒
False
| id :: _ ⇒
winner_pending_1 γ front P id
end.
#[local] Instance : CustomIpat "inv_state_nonempty_steal" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}% & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_emptyish γ stable front back hist priv : iProp Σ :=
∃ P,
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
( winner_pop γ front P
∨ winner_linearized γ front P
).
#[local] Instance : CustomIpat "inv_state_emptyish" :=
" ( %P_ & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner ) ".
#[local] Definition inv_state_emptyish_pop γ state stable front back hist priv P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
winner_pop γ front P.
#[local] Instance : CustomIpat "inv_state_emptyish_pop" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & Hwinner_pop ) ".
#[local] Definition inv_state_emptyish_steal γ state stable front back hist priv P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = S front⌝ ∗
history_at γ front (hd inhabitant priv) ∗
winner_linearized γ front P.
#[local] Instance : CustomIpat "inv_state_emptyish_steal" :=
" ( {>;}-> & { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & #Hhistory_at_front{} & (:winner_linearized) ) ".
#[local] Definition inv_state_superempty γ stable front back hist : iProp Σ :=
⌜stable = Unstable⌝ ∗
⌜front = S back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv_state_superempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv_state γ state stable front back hist vs priv prophs : iProp Σ :=
match state with
| Empty ⇒
inv_state_empty γ stable front back hist
| Nonempty ⇒
inv_state_nonempty γ stable front back hist vs prophs
| Emptyish ⇒
inv_state_emptyish γ stable front back hist priv
| Superempty ⇒
inv_state_superempty γ stable front back hist
end.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ state stable front back hist vs priv pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
owner₂ γ stable back ∗
front_auth γ front ∗
⌜0 < front⌝ ∗
model₂ γ vs ∗
⌜length vs = back - front⌝ ∗
array_cslice γ.(ws_bdeque_1_name_data) γ.(ws_bdeque_1_name_capacity) front (DfracOwn (1/2)) (vs ++ priv) ∗
⌜(length vs + length priv)%nat = γ.(ws_bdeque_1_name_capacity)⌝ ∗
history_auth γ hist ∗
prophet_multi_model prophet_identifier γ.(ws_bdeque_1_name_prophet) γ.(ws_bdeque_1_name_prophet_name) pasts prophss ∗
⌜∀ i, front ≤ i → pasts i = []⌝ ∗
inv_state γ state stable front back hist vs priv (prophss front).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %state{} & %stable{} & %front{} & %back{} & %hist{} & %vs{} & %priv{} & %pasts{} & %prophss{} & >Ht_front & >Ht_back & >Howner₂ & >Hfront_auth & >%Hfront{} & >Hmodel₂ & >%Hvs{} & >Hdata_cslice₁ & >%Hdata{} & >Hhistory_auth & >Hprophet_model & >%Hpasts{} & Hstate ) ".
#[local] Definition inv' t γ : iProp Σ :=
⌜0 < γ.(ws_bdeque_1_name_capacity)⌝ ∗
t.[capacity] ↦□ #γ.(ws_bdeque_1_name_capacity) ∗
t.[data] ↦□ γ.(ws_bdeque_1_name_data) ∗
t.[proph] ↦□ #γ.(ws_bdeque_1_name_prophet) ∗
inv γ.(ws_bdeque_1_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( %Hcapacity & #Ht_capacity & #Ht_data & #Ht_proph & #Hinv ) ".
Definition ws_bdeque_1_inv t γ ι cap : iProp Σ :=
⌜ι = γ.(ws_bdeque_1_name_inv)⌝ ∗
⌜cap = γ.(ws_bdeque_1_name_capacity)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & -> & (:inv') ) ".
Definition ws_bdeque_1_model γ vs : iProp Σ :=
model₁ γ vs ∗
⌜length vs ≤ γ.(ws_bdeque_1_name_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( Hmodel₁{_{}} & %Hvs{} ) ".
Variant owner_flag :=
| OwnerNormal
| OwnerPop.
#[local] Definition owner_1 flag t γ stable back ws front_cache i us : iProp Σ :=
owner₁ γ stable back ws ∗
t.[front_cache] ↦ #front_cache ∗
front_lb γ front_cache ∗
⌜(if flag is OwnerPop then S back else back) ≤ front_cache + γ.(ws_bdeque_1_name_capacity)⌝ ∗
array_cslice γ.(ws_bdeque_1_name_data) γ.(ws_bdeque_1_name_capacity) i (DfracOwn (1/2)) us ∗
⌜length us = γ.(ws_bdeque_1_name_capacity)⌝.
#[local] Instance : CustomIpat "owner_1" :=
" ( Howner₁{_{}} & Ht_front_cache{_{}} & { {!} _ ; #Hfront_lb_cache_{} ; #Hfront_lb_cache } & { {!} _ ; %Hfront_cache_{} ; %Hfront_cache } & Hdata_cslice₂{_{}} & { {!} _ ; %Hus{} ; %Hus } ) ".
#[local] Definition owner_2 :=
owner_1 OwnerNormal.
#[local] Instance : CustomIpat "owner_2" :=
" (:owner_1) ".
Definition ws_bdeque_1_owner t γ ws : iProp Σ :=
∃ back front_cache i us,
owner_2 t γ Stable back ws front_cache i us.
#[local] Instance : CustomIpat "owner" :=
" ( %back{} & %front_cache{_{}} & %i{} & %us{} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_1_model_timeless γ vs :
Timeless (ws_bdeque_1_model γ vs).
#[global] Instance ws_bdeque_1_owner_timeless t γ ws :
Timeless (ws_bdeque_1_owner t γ ws).
#[global] Instance ws_bdeque_1_inv_persistent t γ ι cap :
Persistent (ws_bdeque_1_inv t γ ι cap).
#[local] Lemma model_owner_alloc :
⊢ |==>
∃ γ_model γ_owner,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner₁' γ_owner γ_model Stable 1 [] ∗
owner₂' γ_owner Stable 1.
#[local] Lemma model₁_valid γ stable back ws vs :
owner₁ γ stable back ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_owner₁_agree γ stable back ws vs1 vs2 :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma model_empty {γ stable back ws vs1 vs2} :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back [] ∗
model₁ γ [] ∗
model₂ γ [].
#[local] Lemma model_push {γ stable back ws vs1 vs2} v :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_steal γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ (tail vs1) ∗
model₂ γ (tail vs1).
#[local] Lemma model_pop γ stable back ws vs1 vs2 :
owner₁ γ stable back ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma model_pop' γ stable back ws vs1 v vs2 :
owner₁ γ stable back ws -∗
model₁ γ (vs1 ++ [v]) -∗
model₂ γ vs2 ==∗
owner₁ γ stable back vs1 ∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma owner₁_exclusive γ stable1 back1 ws1 stable2 back2 ws2 :
owner₁ γ stable1 back1 ws1 -∗
owner₁ γ stable2 back2 ws2 -∗
False.
#[local] Lemma owner_agree γ stable1 back1 ws stable2 back2 :
owner₁ γ stable1 back1 ws -∗
owner₂ γ stable2 back2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝.
#[local] Lemma owner₁_update γ stable back ws vs :
owner₁ γ stable back ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner₁ γ stable back vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma owner_update {γ stable1 back1 ws stable2 back2} stable back :
owner₁ γ stable1 back1 ws -∗
owner₂ γ stable2 back2 ==∗
owner₁ γ stable back ws ∗
owner₂ γ stable back.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 1.
#[local] Lemma front_lb_get γ front :
front_auth γ front ⊢
front_lb γ front.
#[local] Lemma front_lb_le {γ front} front' :
front' ≤ front →
front_lb γ front ⊢
front_lb γ front'.
#[local] Lemma front_lb_valid γ front1 front2 :
front_auth γ front1 -∗
front_lb γ front2 -∗
⌜front2 ≤ front1⌝.
#[local] Lemma front_update γ front :
front_auth γ front ⊢ |==>
front_auth γ (S front).
#[local] Lemma history_alloc :
⊢ |==>
∃ γ_hist,
history_auth' γ_hist [()%V].
#[local] Lemma history_at_get {γ hist v} i :
i = length hist →
history_auth γ (hist ++ [v]) ⊢
history_at γ i v.
#[local] Lemma history_at_lookup γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_at_agree γ i v1 v2 :
history_at γ i v1 -∗
history_at γ i v2 -∗
⌜v1 = v2⌝.
#[local] Lemma history_update {γ hist} i v :
i = length hist →
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]) ∗
history_at γ i v.
#[local] Lemma winner_alloc :
⊢ |==>
∃ γ_winner,
winner_pop' γ_winner 1 True ∗
winner_steal' γ_winner 1 True.
#[local] Lemma winner_pop_exclusive γ front1 P1 front2 P2 :
winner_pop γ front1 P1 -∗
winner_pop γ front2 P2 -∗
False.
#[local] Lemma winner_pop_exclusive' γ front P :
winner_pop γ front P -∗
winner γ -∗
False.
#[local] Lemma winner_steal_exclusive γ front1 P1 front2 P2 :
winner_steal γ front1 P1 -∗
winner_steal γ front2 P2 -∗
False.
#[local] Lemma winner_steal_exclusive' γ front P :
winner_steal γ front P -∗
winner γ -∗
False.
#[local] Lemma winner_agree γ front1 P1 front2 P2 :
winner_pop γ front1 P1 -∗
winner_steal γ front2 P2 -∗
⌜front1 = front2⌝ ∗
▷ (P1 ≡ P2).
#[local] Lemma winner_update {γ front1 P1 front2 P2} front P :
winner_pop γ front1 P1 -∗
winner_steal γ front2 P2 ==∗
winner_pop γ front P ∗
winner_steal γ front P.
Opaque owner₁'.
Lemma ws_bdeque_1_model_valid t γ ι cap vs :
ws_bdeque_1_inv t γ ι cap -∗
ws_bdeque_1_model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_1_model_exclusive γ vs1 vs2 :
ws_bdeque_1_model γ vs1 -∗
ws_bdeque_1_model γ vs2 -∗
False.
#[local] Lemma owner_2_rebase {t γ stable back ws front_cache i1 us} i2 :
0 < γ.(ws_bdeque_1_name_capacity) →
owner_2 t γ stable back ws front_cache i1 us ⊢
∃ us,
owner_2 t γ stable back ws front_cache i2 us.
Lemma ws_bdeque_1_owner_exclusive t γ ws1 ws2 :
ws_bdeque_1_owner t γ ws1 -∗
ws_bdeque_1_owner t γ ws2 -∗
False.
Lemma ws_bdeque_1_owner_model t γ ws vs :
ws_bdeque_1_owner t γ ws -∗
ws_bdeque_1_model γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma inv_state_Stable γ state front back hist vs priv prophs :
length vs = back - front →
inv_state γ state Stable front back hist vs priv prophs ⊢
⌜state = Empty ∨ state = Nonempty⌝ ∗
⌜front ≤ back⌝.
#[local] Lemma inv_state_Unstable γ state front back hist vs priv prophs :
inv_state γ state Unstable front back hist vs priv prophs ⊢
⌜state = Emptyish ∨ state = Superempty⌝ ∗
⌜front = back ∨ front = S back⌝.
#[local] Lemma inv_state_Nonempty γ state stable front back hist vs priv prophs :
front < back →
inv_state γ state stable front back hist vs priv prophs ⊢
⌜state = Nonempty⌝.
#[local] Lemma inv_state_Superempty γ state front back hist vs priv prophs :
back < front →
inv_state γ state Unstable front back hist vs priv prophs -∗
⌜state = Superempty⌝.
#[local] Lemma inv_state_winner_pop γ state stable front1 back hist vs priv prophs front2 P :
inv_state γ state stable front1 back hist vs priv prophs -∗
winner_pop γ front2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P ≡ P_) ∗
( inv_state_nonempty_steal γ state stable front2 back hist vs prophs P_
∨ inv_state_emptyish_steal γ state stable front2 back hist priv P_
) ∗
winner_pop γ front2 P.
#[local] Lemma inv_state_winner_steal γ state stable front1 back hist vs priv prophs front2 P :
inv_state γ state stable front1 back hist vs priv prophs -∗
winner_steal γ front2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P_ ≡ P) ∗
inv_state_emptyish_pop γ state stable front2 back hist priv P_ ∗
winner_steal γ front2 P.
Lemma ws_bdeque_1٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_1٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_bdeque_1_inv t γ ι ₊cap ∗
ws_bdeque_1_model γ [] ∗
ws_bdeque_1_owner t γ []
}}}.
Lemma ws_bdeque_1٠capacity𑁒spec t γ ι cap :
{{{
ws_bdeque_1_inv t γ ι cap
}}}
ws_bdeque_1٠capacity #t
{{{
RET #cap;
True
}}}.
#[local] Lemma front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front
, RET #front;
front_lb γ front
}}}.
#[local] Lemma front𑁒spec_owner_Stable t γ back ws :
{{{
inv' t γ ∗
owner₁ γ Stable back ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Stable back ws ∗
front_lb γ front ∗
⌜front ≤ back⌝
}}}.
#[local] Lemma front𑁒spec_owner_Unstable t γ back ws :
{{{
inv' t γ ∗
owner₁ γ Unstable back ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Unstable back ws ∗
front_lb γ front ∗
⌜front = back ∨ front = S back⌝
}}}.
#[local] Lemma front𑁒spec_Superempty t γ back ws front :
back < front →
{{{
inv' t γ ∗
owner₁ γ Unstable back ws ∗
front_lb γ front
}}}
(#t).{front}
{{{
RET #front;
owner₁ γ Unstable back ws
}}}.
#[local] Lemma front𑁒spec_winner_steal t γ front P :
{{{
inv' t γ ∗
winner_steal γ front P
}}}
(#t).{front}
{{{
RET #front;
winner_steal γ front P
}}}.
#[local] Lemma back𑁒spec t γ stable back ws :
{{{
inv' t γ ∗
owner₁ γ stable back ws
}}}
(#t).{back}
{{{
RET #back;
owner₁ γ stable back ws
}}}.
#[local] Lemma set_back𑁒spec_Superempty t γ back ws front (back' : Z) :
back < front →
back' = S back →
{{{
inv' t γ ∗
owner₁ γ Unstable back ws ∗
front_lb γ front
}}}
#t <-{back} #back'
{{{
RET ();
owner₁ γ Stable (S back) ws
}}}.
#[local] Lemma array٠unsafe_cget𑁒spec_loser t γ i :
(0 ≤ i)%Z →
{{{
inv' t γ
}}}
array٠unsafe_cget γ.(ws_bdeque_1_name_data) #i
{{{
v
, RET v;
True
}}}.
#[local] Lemma array٠unsafe_cget𑁒spec_winner_pop t γ front P v :
{{{
inv' t γ ∗
winner_pop γ front P ∗
history_at γ front v
}}}
array٠unsafe_cget γ.(ws_bdeque_1_name_data) #front
{{{
RET v;
winner_pop γ front P
}}}.
#[local] Lemma array٠unsafe_cset𑁒spec_owner t γ back ws front_cache us front v :
back < front + γ.(ws_bdeque_1_name_capacity) →
{{{
inv' t γ ∗
owner_2 t γ Stable back ws front_cache back us ∗
front_lb γ front
}}}
array٠unsafe_cset γ.(ws_bdeque_1_name_data) #back v
{{{
RET ();
owner_2 t γ Stable back ws front_cache back (<[0 := v]> us)
}}}.
#[local] Lemma resolve𑁒spec_loser_1 t γ front1 front2 id :
front1 < front2 →
{{{
inv' t γ ∗
front_lb γ front2
}}}
Resolve (CAS (#t).[front]%V #front1 #(front1 + 1)) #γ.(ws_bdeque_1_name_prophet) (#front1, #id)%V
{{{
RET false;
True
}}}.
#[local] Lemma resolve𑁒spec_loser_2 t γ front id prophs0 :
head prophs0 ≠ Some id →
{{{
inv' t γ ∗
front_lb γ front ∗
prophet_multi_full prophet_identifier γ.(ws_bdeque_1_name_prophet_name) front prophs0
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET false;
front_lb γ (S front)
}}}.
#[local] Lemma resolve𑁒spec_winner_pop t γ front P id :
{{{
inv' t γ ∗
winner_pop γ front P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET true;
▷ P
}}}.
#[local] Lemma resolve𑁒spec_winner_steal t γ front P id :
{{{
inv' t γ ∗
winner_steal γ front P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_bdeque_1_name_prophet) (#front, #id)%V
{{{
RET true;
front_lb γ (S front)
}}}.
#[local] Lemma resolve𑁒spec_Empty t γ back ws id :
{{{
inv' t γ ∗
owner₁ γ Stable back ws ∗
front_lb γ back
}}}
Resolve (CAS (#t).[front]%V #back #(back + 1)) #γ.(ws_bdeque_1_name_prophet) (#back, #id)%V
{{{
RET true;
owner₁ γ Unstable back ws ∗
front_lb γ (S back)
}}}.
Lemma ws_bdeque_1٠size𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ vs
| RET #(length vs);
ws_bdeque_1_owner t γ vs
>>>.
Lemma ws_bdeque_1٠is_empty𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_1_owner t γ vs
>>>.
#[local] Definition push_au t γ ws v Φ : iProp Σ :=
AU <{
∃∃ vs,
ws_bdeque_1_model γ vs
}> @ ⊤ ∖ ↑γ.(ws_bdeque_1_name_inv), ∅ <{
∀∀ b,
⌜b = bool_decide (length vs < γ.(ws_bdeque_1_name_capacity))⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ (if b then vs ++ [v] else vs)
, COMM
ws_bdeque_1_owner t γ (if b then vs ++ [v] else ws) -∗
Φ #b
}>.
Lemma ws_bdeque_1٠push𑁒spec t γ ι cap ws v :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model γ (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_1_owner t γ (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_1٠steal𑁒spec t γ ι cap :
<<<
ws_bdeque_1_inv t γ ι cap
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠steal #t @ ↑ι
<<<
ws_bdeque_1_model γ (tail vs)
| RET head vs;
True
>>>.
Variant pop_state :=
| PopNonempty v
| PopEmptyishWinner v
| PopEmptyishLoser
| PopSuperempty.
#[local] Lemma ws_bdeque_1٠pop₀𑁒spec {t γ} (state : pop_state) {stable} back ws front_cache us id (back_ : Z) :
back_ = back →
{{{
inv' t γ ∗
owner_1 OwnerPop t γ stable back ws front_cache back us ∗
match state with
| PopNonempty v ⇒
⌜stable = Stable⌝ ∗
⌜us !! 0 = Some v⌝
| PopEmptyishWinner v ⇒
⌜stable = Unstable⌝ ∗
⌜us !! 0 = Some v⌝ ∗
winner_steal γ back inhabitant
| PopEmptyishLoser ⇒
∃ id_winner prophs,
⌜stable = Unstable⌝ ∗
prophet_multi_full prophet_identifier γ.(ws_bdeque_1_name_prophet_name) back (id_winner :: prophs) ∗
⌜head (id_winner :: prophs) ≠ Some id⌝
| PopSuperempty ⇒
∃ front,
⌜stable = Unstable⌝ ∗
front_lb γ front ∗
⌜front = S back⌝
end
}}}
ws_bdeque_1٠pop₀ #t #id #back_
{{{
o back front_cache i us
, RET o;
owner_2 t γ Stable back ws front_cache i us ∗
match state with
| PopNonempty v ⇒
⌜o = Some v⌝
| PopEmptyishWinner v ⇒
⌜o = Some v⌝
| PopEmptyishLoser ⇒
⌜o = None⌝
| PopSuperempty ⇒
⌜o = None⌝
end
}}}.
Lemma ws_bdeque_1٠pop𑁒spec t γ ι cap ws :
<<<
ws_bdeque_1_inv t γ ι cap ∗
ws_bdeque_1_owner t γ ws
| ∀∀ vs,
ws_bdeque_1_model γ vs
>>>
ws_bdeque_1٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_1_model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_1_model γ vs'
end
| RET o;
ws_bdeque_1_owner t γ ws'
>>>.
End ws_bdeque_1_G.
#[global] Opaque ws_bdeque_1_inv.
#[global] Opaque ws_bdeque_1_model.
#[global] Opaque ws_bdeque_1_owner.
End base.
From zoo_saturn Require
ws_bdeque_1__opaque.
Section ws_bdeque_1_G.
Context `{ws_bdeque_1_G : WsBdeque1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition ws_bdeque_1_inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_bdeque_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_bdeque_1_owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_1_owner 𝑡 γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_1_model_timeless γ vs :
Timeless (ws_bdeque_1_model γ vs).
#[global] Instance ws_bdeque_1_owner_timeless γ ws :
Timeless (ws_bdeque_1_owner γ ws).
#[global] Instance ws_bdeque_1_inv_persistent t ι cap :
Persistent (ws_bdeque_1_inv t ι cap).
Lemma ws_bdeque_1_model_valid t ι cap vs :
ws_bdeque_1_inv t ι cap -∗
ws_bdeque_1_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_1_model_exclusive t vs1 vs2 :
ws_bdeque_1_model t vs1 -∗
ws_bdeque_1_model t vs2 -∗
False.
Lemma ws_bdeque_1_owner_exclusive t ws1 ws2 :
ws_bdeque_1_owner t ws1 -∗
ws_bdeque_1_owner t ws2 -∗
False.
Lemma ws_bdeque_1_owner_model γ ws vs :
ws_bdeque_1_owner γ ws -∗
ws_bdeque_1_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_1٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_1٠create #cap
{{{
t
, RET t;
ws_bdeque_1_inv t ι ₊cap ∗
ws_bdeque_1_model t [] ∗
ws_bdeque_1_owner t []
}}}.
Lemma ws_bdeque_1٠capacity𑁒spec t ι cap :
{{{
ws_bdeque_1_inv t ι cap
}}}
ws_bdeque_1٠capacity t
{{{
RET #cap;
True
}}}.
Lemma ws_bdeque_1٠size𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t vs
| RET #(length vs);
ws_bdeque_1_owner t vs
>>>.
Lemma ws_bdeque_1٠is_empty𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_1_owner t vs
>>>.
Lemma ws_bdeque_1٠push𑁒spec t ι cap ws v :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_1_model t (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_1_owner t (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_1٠steal𑁒spec t ι cap :
<<<
ws_bdeque_1_inv t ι cap
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠steal t @ ↑ι
<<<
ws_bdeque_1_model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_1٠pop𑁒spec t ι cap ws :
<<<
ws_bdeque_1_inv t ι cap ∗
ws_bdeque_1_owner t ws
| ∀∀ vs,
ws_bdeque_1_model t vs
>>>
ws_bdeque_1٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_1_model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_1_model t vs'
end
| RET o;
ws_bdeque_1_owner t ws'
>>>.
End ws_bdeque_1_G.
#[global] Opaque ws_bdeque_1_inv.
#[global] Opaque ws_bdeque_1_model.
#[global] Opaque ws_bdeque_1_owner.