Library zoo_saturn.ws_deque_1
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.function.
Require Import zoo.common.list.
Require Import zoo.common.relations.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.auth_twins.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.mono_gmultiset.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_identifier.
Require Import zoo.program_logic.prophet_multi.
Require Import zoo_std.option.
Require Export zoo_saturn.ws_deque_1__code.
Require Import zoo_saturn.ws_deque_1__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type front back : nat.
Implicit Type id : prophet_id.
Implicit Type v : val.
Implicit Type us vs ws hist priv : list val.
Implicit Type datas : gmultiset val.
Implicit Type past prophs : list prophet_identifier.(prophet_typed۰type).
Implicit Type pasts prophss : nat → list prophet_identifier.(prophet_typed۰type).
Variant state :=
| Empty
| Nonempty
| Emptyish
| Superempty.
Implicit Type state : state.
#[local] Instance stateｰinhabited : Inhabited state :=
populate Empty.
Variant stability :=
| Stable
| Unstable.
Implicit Type stable : stability.
#[local] Instance stabilityｰinhabited : Inhabited stability :=
populate Stable.
Class WsDeque1G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deque_1۰G۰prophet۰G :: ProphetMultiG Σ prophet_identifier
; #[local] ws_deque_1۰G۰model۰G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] ws_deque_1۰G۰owner۰G :: TwinsG Σ (leibnizO (stability × nat × val × nat))
; #[local] ws_deque_1۰G۰front۰G :: AuthNatMaxG Σ
; #[local] ws_deque_1۰G۰history۰G :: MonoListG Σ val
; #[local] ws_deque_1۰G۰winner۰G :: TwinsG Σ (natO × leibnizO (option val) × ▶ ∙)
; #[local] ws_deque_1۰G۰datas۰G :: MonoGmultisetG Σ val
}.
Definition ws_deque_1۰Σ :=
#[prophet_multi۰Σ prophet_identifier
; auth_twins۰Σ (leibnizO (list val)) suffix
; twins۰Σ (leibnizO (stability × nat × val × nat))
; auth_nat_max۰Σ
; mono_list۰Σ val
; twins۰Σ (natO × leibnizO (option val) × ▶ ∙)
; mono_gmultiset۰Σ val
].
#[global] Instance subGｰws_deque_1۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deque_1۰Σ Σ →
WsDeque1G Σ .
#[local] Definition min_capacity :=
val۰to_nat' ws_deque_1٠min_capacity.
#[local] Lemma min_capacityｰnonzero :
0 < min_capacity.
#[local] Hint Resolve
min_capacityｰnonzero
: core.
#[local] Lemma ws_deque_1٠min_capacityｰunfold :
ws_deque_1٠min_capacity = #min_capacity.
Opaque ws_deque_1٠min_capacity.
Opaque min_capacity.
Module base.
Section ws_deque_1۰G.
Context `{ws_deque_1۰G : WsDeque1G Σ}.
Implicit Type t : location.
Implicit Type P : iProp Σ.
Record ws_deque_1۰name :=
{ ws_deque_1۰name۰inv : namespace
; ws_deque_1۰name۰prophet : prophet_id
; ws_deque_1۰name۰prophet_name : prophet_multi۰name
; ws_deque_1۰name۰model : auth_twins۰name
; ws_deque_1۰name۰owner : gname
; ws_deque_1۰name۰front : gname
; ws_deque_1۰name۰history : gname
; ws_deque_1۰name۰winner : gname
; ws_deque_1۰name۰datas : gname
}.
Implicit Type γ : ws_deque_1۰name.
#[global] Instance ws_deque_1۰nameｰeq_dec : EqDecision ws_deque_1۰name :=
ltac:(solve_decision).
#[global] Instance ws_deque_1۰nameｰcountable :
Countable ws_deque_1۰name.
#[local] Definition model₁' γ_model vs :=
auth_twins۰twin₁ _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_deque_1۰name۰model).
#[local] Definition model₂' γ_model vs :=
auth_twins۰twin₂ _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_deque_1۰name۰model).
#[local] Definition owner₁' γ_owner γ_model stable back data cap ws : iProp Σ :=
twins۰twin₁ (twins۰G := ws_deque_1۰G۰owner۰G) γ_owner (DfracOwn 1) (stable, back, data, cap) ∗
auth_twins۰auth _ γ_model ws.
#[local] Definition owner₁ γ :=
owner₁' γ.(ws_deque_1۰name۰owner) γ.(ws_deque_1۰name۰model).
#[local] Instance : CustomIpat "owner₁" :=
" ( Howner₁{_{}} & Hmodel_auth{_{}} ) ".
#[local] Definition owner₂' γ_owner stable back data cap :=
twins۰twin₂ (twins۰G := ws_deque_1۰G۰owner۰G) γ_owner (stable, back, data, cap).
#[local] Definition owner₂ γ :=
owner₂' γ.(ws_deque_1۰name۰owner).
#[local] Definition front۰auth' γ_front :=
auth_nat_max۰auth γ_front (DfracOwn 1).
#[local] Definition front۰auth γ :=
front۰auth' γ.(ws_deque_1۰name۰front).
#[local] Definition front۰lb γ :=
auth_nat_max۰lb γ.(ws_deque_1۰name۰front).
#[local] Definition history۰auth' γ_history :=
mono_list۰auth γ_history (DfracOwn 1).
#[local] Definition history۰auth γ :=
history۰auth' γ.(ws_deque_1۰name۰history).
#[local] Definition history۰at γ :=
mono_list۰at γ.(ws_deque_1۰name۰history).
#[local] Definition winner۰pop' γ_winner front (data : option val) P : iProp Σ :=
twins۰twin₁ γ_winner (DfracOwn 1) (front, data, Next P).
#[local] Definition winner۰pop γ :=
winner۰pop' γ.(ws_deque_1۰name۰winner).
#[local] Definition winner۰steal' γ_winner front (data : option val) P :=
twins۰twin₂ γ_winner (front, data, Next P).
#[local] Definition winner۰steal γ :=
winner۰steal' γ.(ws_deque_1۰name۰winner).
#[local] Definition winner γ : iProp Σ :=
∃ front data P1 P2,
winner۰pop γ front data P1 ∗
winner۰steal γ front data P2.
#[local] Instance : CustomIpat "winner" :=
" ( %front_winner & %data_winner & %P1 & %P2 & Hwinner_pop{_{}} & Hwinner_steal{_{}} ) ".
#[local] Definition datas۰auth' γ_datas :=
mono_gmultiset۰auth γ_datas (DfracOwn 1).
#[local] Definition datas۰auth γ :=
datas۰auth' γ.(ws_deque_1۰name۰datas).
#[local] Definition datas۰elem' γ_datas :=
mono_gmultiset۰elem γ_datas.
#[local] Definition datas۰elem γ :=
datas۰elem' γ.(ws_deque_1۰name۰datas).
#[local] Definition data۰model data : iProp Σ :=
∃ cap i vs,
array۰cslice data cap i DfracDiscarded vs ∗
⌜0 < cap⌝ ∗
⌜length vs = cap⌝.
#[local] Instance : CustomIpat "data۰model" :=
" ( %cap_data{} & %i_data{} & %vs_data{} & Hdata{}_cslice & %Hcap_data{} & %Hvs_data{} ) ".
#[local] Definition winner۰au γ front P : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(ws_deque_1۰name۰inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs' ∗
history۰at γ front v
, COMM
P
}>.
#[local] Definition winner۰model₁ γ front data data_winner : iProp Σ :=
⌜data = data_winner⌝
∨ ∃ cap_winner v,
array۰cslice data_winner cap_winner front DfracDiscarded [v] ∗
history۰at γ front v.
#[local] Instance : CustomIpat "winner۰model₁" :=
" [ -> | ( %cap & %v_ & Hdata_cslice & Hhistory_at_ ) ] ".
#[local] Definition winner۰model₂ γ front data data_winner P : iProp Σ :=
winner۰steal γ front (Some data_winner) P ∗
winner۰model₁ γ front data data_winner.
#[local] Instance : CustomIpat "winner۰model₂" :=
" ( Hwinner_steal{_{!}} & Hwinner ) ".
#[local] Definition winner۰pending₁ γ front data data_winner P id : iProp Σ :=
winner۰model₂ γ front data data_winner P ∗
identifier۰model id ∗
winner۰au γ front P.
#[local] Instance : CustomIpat "winner۰pending₁" :=
" ( (:winner۰model₂) & Hid{_{!}} & HP ) ".
#[local] Definition winner۰pending₂ γ front data id : iProp Σ :=
∃ data_winner P,
winner۰pending₁ γ front data data_winner P id.
#[local] Instance : CustomIpat "winner۰pending₂" :=
" ( %data_winner & %P{} & (:winner۰pending₁) ) ".
#[local] Definition winner۰linearized₁ γ front data data_winner P : iProp Σ :=
winner۰model₂ γ front data data_winner P ∗
P.
#[local] Instance : CustomIpat "winner۰linearized₁" :=
" ( (:winner۰model₂) & HP ) ".
#[local] Definition winner۰linearized₂ γ front data P : iProp Σ :=
∃ data_winner,
winner۰linearized₁ γ front data data_winner P.
#[local] Instance : CustomIpat "winner۰linearized₂" :=
" ( %data_winner & (:winner۰linearized₁) ) ".
#[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 data hist vs prophs : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant vs) ∗
( winner γ
∨ match prophs with
| [] ⇒
False
| id :: _ ⇒
winner۰pending₂ γ front data 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 data hist vs prophs data_winner P : iProp Σ :=
⌜state = Nonempty⌝ ∗
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant vs) ∗
match prophs with
| [] ⇒
False
| id :: _ ⇒
winner۰pending₁ γ front data data_winner 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 data hist priv : iProp Σ :=
∃ P,
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
( winner۰pop γ front None P
∨ winner۰linearized₂ γ front data 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 = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
winner۰pop γ front None 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 data hist priv data_winner P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
winner۰linearized₁ γ front data data_winner 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 = ˖back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv۰state۰superempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv۰state γ state stable front back data hist vs priv prophs : iProp Σ :=
match state with
| Empty ⇒
inv۰state۰empty γ stable front back hist
| Nonempty ⇒
inv۰state۰nonempty γ stable front back data hist vs prophs
| Emptyish ⇒
inv۰state۰emptyish γ stable front back data hist priv
| Superempty ⇒
inv۰state۰superempty γ stable front back hist
end.
#[local] Definition inv۰inner t γ : iProp Σ :=
∃ state stable front back data cap hist vs priv datas pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
t.[data] ↦ data ∗
owner₂ γ stable back data cap ∗
front۰auth γ front ∗
⌜0 < front⌝ ∗
model₂ γ vs ∗
⌜length vs = back - front⌝ ∗
array۰cslice data cap front (DfracOwn (1/2)) (vs ++ priv) ∗
⌜0 < cap⌝ ∗
⌜(length vs + length priv)%nat = cap⌝ ∗
history۰auth γ hist ∗
datas۰auth γ ({[+data+]} ⊎ datas) ∗
([∗ mset] data ∈ datas, data۰model data) ∗
prophet_multi۰model prophet_identifier γ.(ws_deque_1۰name۰prophet) γ.(ws_deque_1۰name۰prophet_name) pasts prophss ∗
⌜∀ i, front ≤ i → pasts i = []⌝ ∗
inv۰state γ state stable front back data hist vs priv (prophss front).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %state{} & %stable{} & %front{} & %back{} & %data{} & %cap{} & %hist{} & %vs{} & %priv{} & %datas{} & %pasts{} & %prophss{} & >Ht_front & >Ht_back & >Ht_data & >Howner₂ & >Hfront_auth & >%Hfront{} & >Hmodel₂ & >%Hvs{} & >Hdata{}_cslice₁ & >%Hcap{} & >%Hdata{} & >Hhistory_auth & >Hdatas_auth & >Hdatas & >Hprophet_model & >%Hpasts{} & Hstate ) ".
#[local] Definition inv' t γ : iProp Σ :=
t.[proph] ↦□ #γ.(ws_deque_1۰name۰prophet) ∗
inv γ.(ws_deque_1۰name۰inv) (inv۰inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Ht_proph & #Hinv ) ".
Definition ws_deque_1۰inv t γ ι : iProp Σ :=
⌜ι = γ.(ws_deque_1۰name۰inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & (:inv') ) ".
Definition ws_deque_1۰model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Definition owner' γ stable back data cap ws i us : iProp Σ :=
owner₁ γ stable back data cap ws ∗
array۰cslice data cap i (DfracOwn (1/2)) us ∗
⌜0 < cap⌝ ∗
⌜length us = cap⌝.
#[local] Instance : CustomIpat "owner'" :=
" ( Howner₁{_{}} & Hdata_cslice₂{_{}} & { {!} _ ; %Hcap{} ; %Hcap } & { {!} _ ; %Hus{} ; %Hus } ) ".
Definition ws_deque_1۰owner γ ws : iProp Σ :=
∃ back data cap i us,
owner' γ Stable back data cap ws i us.
#[local] Instance : CustomIpat "owner" :=
" ( %back{} & %data{} & %cap{} & %i{} & %us{} & Howner{_{}} ) ".
#[global] Instance ws_deque_1۰modelｰtimeless γ vs :
Timeless (ws_deque_1۰model γ vs).
#[global] Instance ws_deque_1۰ownerｰtimeless γ ws :
Timeless (ws_deque_1۰owner γ ws).
#[global] Instance ws_deque_1۰invｰpersistent t γ ι :
Persistent (ws_deque_1۰inv t γ ι).
#[local] Lemma modelｰownerｰalloc data cap :
⊢ |==>
∃ γ_model γ_owner,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner₁' γ_owner γ_model Stable 1 data cap [] ∗
owner₂' γ_owner Stable 1 data cap.
#[local] Lemma model₁ｰvalid γ stable back data cap ws vs :
owner₁ γ stable back data cap 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 data cap ws vs1 vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma modelｰempty {γ stable back data cap ws vs1 vs2} :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap [] ∗
model₁ γ [] ∗
model₂ γ [].
#[local] Lemma modelｰpush {γ stable back data cap ws vs1 vs2} v :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap (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 data cap ws vs1 vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma modelｰpop' γ stable back data cap ws vs1 v vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ (vs1 ++ [v]) -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap vs1 ∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma owner₁ｰexclusive γ stable1 back1 data1 cap1 ws1 stable2 back2 data2 cap2 ws2 :
owner₁ γ stable1 back1 data1 cap1 ws1 -∗
owner₁ γ stable2 back2 data2 cap2 ws2 -∗
False.
#[local] Lemma ownerｰagree γ stable1 back1 data1 cap1 ws stable2 back2 data2 cap2 :
owner₁ γ stable1 back1 data1 cap1 ws -∗
owner₂ γ stable2 back2 data2 cap2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝ ∗
⌜data1 = data2⌝ ∗
⌜cap1 = cap2⌝.
#[local] Lemma owner₁ｰupdate γ stable back data cap ws vs :
owner₁ γ stable back data cap ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner₁ γ stable back data cap vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma ownerｰupdate {γ stable1 back1 data1 cap1 ws stable2 back2 data2 cap2} stable back data cap :
owner₁ γ stable1 back1 data1 cap1 ws -∗
owner₂ γ stable2 back2 data2 cap2 ==∗
owner₁ γ stable back data cap ws ∗
owner₂ γ stable back data cap.
#[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 γ ˖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 None True ∗
winner۰steal' γ_winner 1 None True.
#[local] Lemma winner۰popｰexclusive γ front1 data1 P1 front2 data2 P2 :
winner۰pop γ front1 data1 P1 -∗
winner۰pop γ front2 data2 P2 -∗
False.
#[local] Lemma winner۰popｰexclusive' γ front data P :
winner۰pop γ front data P -∗
winner γ -∗
False.
#[local] Lemma winner۰stealｰexclusive γ front1 data1 P1 front2 data2 P2 :
winner۰steal γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 -∗
False.
#[local] Lemma winner۰stealｰexclusive' γ front data P :
winner۰steal γ front data P -∗
winner γ -∗
False.
#[local] Lemma winnerｰagree γ front1 data1 P1 front2 data2 P2 :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 -∗
⌜front1 = front2⌝ ∗
⌜data1 = data2⌝ ∗
▷ (P1 ≡ P2).
#[local] Lemma winnerｰupdate' {γ front1 data1 P1 front2 data2 P2} front data :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 ==∗
winner۰pop γ front data P1 ∗
winner۰steal γ front data P2.
#[local] Lemma winnerｰupdate {γ front1 data1 P1 front2 data2 P2} front data P :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 ==∗
winner۰pop γ front data P ∗
winner۰steal γ front data P.
#[local] Lemma datasｰalloc data :
⊢ |==>
∃ γ_datas,
datas۰auth' γ_datas ({[+data+]} ⊎ ∅).
#[local] Lemma datas۰elemｰget γ data datas :
datas۰auth γ ({[+data+]} ⊎ datas) ⊢
datas۰elem γ data.
#[local] Lemma datas۰elemｰvalid γ data1 datas data2 :
datas۰auth γ ({[+data1+]} ⊎ datas) -∗
datas۰elem γ data2 -∗
⌜data1 = data2 ∨ data2 ∈ datas⌝.
#[local] Lemma datasｰinsert {γ datas} data :
datas۰auth γ datas ⊢ |==>
datas۰auth γ ({[+data+]} ⊎ datas).
Opaque owner₁'.
Lemma ws_deque_1۰modelｰexclusive γ vs1 vs2 :
ws_deque_1۰model γ vs1 -∗
ws_deque_1۰model γ vs2 -∗
False.
#[local] Lemma owner'ｰrebase {γ stable back data cap ws i1 us} i2 :
owner' γ stable back data cap ws i1 us ⊢
∃ us,
owner' γ stable back data cap ws i2 us.
#[local] Lemma array۰csliceｰreshape {data cap back dq us} front :
0 < cap →
length us = cap →
front ≤ back →
back ≤ front + cap →
array۰cslice data cap back dq us ⊢
∃ vs priv,
⌜(front + length vs)%nat = back⌝ ∗
⌜(length vs + length priv)%nat = cap⌝ ∗
array۰cslice data cap front dq (vs ++ priv) ∗
( array۰cslice data cap front dq (vs ++ priv) -∗
array۰cslice data cap back dq us
).
Lemma ws_deque_1۰ownerｰexclusive γ ws1 ws2 :
ws_deque_1۰owner γ ws1 -∗
ws_deque_1۰owner γ ws2 -∗
False.
Lemma ws_deque_1ｰownerｰmodel γ ws vs :
ws_deque_1۰owner γ ws -∗
ws_deque_1۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma inv۰stateｰStable γ state front data back hist vs priv prophs :
length vs = back - front →
inv۰state γ state Stable front back data hist vs priv prophs ⊢
⌜state = Empty ∨ state = Nonempty⌝ ∗
⌜front ≤ back⌝.
#[local] Lemma inv۰stateｰUnstable γ state front back data hist vs priv prophs :
inv۰state γ state Unstable front back data hist vs priv prophs ⊢
⌜state = Emptyish ∨ state = Superempty⌝ ∗
⌜front = back ∨ front = ˖back⌝.
#[local] Lemma inv۰stateｰNonempty γ state stable front back data hist vs priv prophs :
front < back →
inv۰state γ state stable front back data hist vs priv prophs ⊢
⌜state = Nonempty⌝.
#[local] Lemma inv۰stateｰSuperempty γ state front back data hist vs priv prophs :
back < front →
inv۰state γ state Unstable front back data hist vs priv prophs -∗
⌜state = Superempty⌝.
#[local] Lemma inv۰stateｰwinner۰pop γ state stable front1 back data1 hist vs priv prophs front2 data2 P :
inv۰state γ state stable front1 back data1 hist vs priv prophs -∗
winner۰pop γ front2 (Some data2) P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P ≡ P_) ∗
( inv۰state۰nonempty۰steal γ state stable front2 back data1 hist vs prophs data2 P_
∨ inv۰state۰emptyish۰steal γ state stable front2 back data1 hist priv data2 P_
) ∗
winner۰model₁ γ front2 data1 data2 ∗
winner۰pop γ front2 (Some data2) P.
#[local] Lemma inv۰stateｰwinner۰steal γ state stable front2 back data1 hist vs priv prophs front1 data2 P :
inv۰state γ state stable front1 back data1 hist vs priv prophs -∗
winner۰steal γ front2 data2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P_ ≡ P) ∗
inv۰state۰emptyish۰pop γ state stable front2 back hist priv P_ ∗
winner۰steal γ front2 data2 P.
Lemma ws_deque_1٠createｰspec ι :
{{{
True
}}}
ws_deque_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰model γ [] ∗
ws_deque_1۰owner γ []
}}}.
#[local] Lemma frontｰspec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front
, RET #front;
front۰lb γ front
}}}.
#[local] Lemma frontｰspecｰownerｰStable t γ back data cap ws :
{{{
inv' t γ ∗
owner₁ γ Stable back data cap ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Stable back data cap ws ∗
front۰lb γ front ∗
⌜front ≤ back⌝
}}}.
#[local] Lemma frontｰspecｰownerｰUnstable t γ back data cap ws :
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front ∗
⌜front = back ∨ front = ˖back⌝
}}}.
#[local] Lemma frontｰspecｰSuperempty t γ back data cap ws front :
back < front →
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front
}}}
(#t).{front}
{{{
RET #front;
owner₁ γ Unstable back data cap ws
}}}.
#[local] Lemma frontｰspecｰwinner۰steal t γ front data P :
{{{
inv' t γ ∗
winner۰steal γ front data P
}}}
(#t).{front}
{{{
RET #front;
winner۰steal γ front data P
}}}.
#[local] Lemma backｰspec t γ stable back data cap ws :
{{{
inv' t γ ∗
owner₁ γ stable back data cap ws
}}}
(#t).{back}
{{{
RET #back;
owner₁ γ stable back data cap ws
}}}.
#[local] Lemma set_backｰspecｰSuperempty t γ back data cap ws front (back' : Z) :
back < front →
back' = ˖back →
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front
}}}
#t <-{back} #back'
{{{
RET ();
owner₁ γ Stable ˖back data cap ws
}}}.
#[local] Lemma dataｰspec t γ :
{{{
inv' t γ
}}}
(#t).{data}
{{{
data
, RET data;
datas۰elem γ data
}}}.
#[local] Lemma dataｰspecｰowner t γ stable back data cap ws :
{{{
inv' t γ ∗
owner₁ γ stable back data cap ws
}}}
(#t).{data}
{{{
RET data;
owner₁ γ stable back data cap ws
}}}.
#[local] Lemma dataｰspecｰwinner۰pop t γ front data P :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P
}}}
(#t).{data}
{{{
data
, RET data;
winner۰pop γ front (Some data) P
}}}.
#[local] Lemma set_dataｰspec t γ front vs back data1 cap1 priv1 ws data2 cap2 priv2 :
0 < cap2 →
front + length vs = back →
length vs + length priv1 = cap1 →
length vs + length priv2 = cap2 →
{{{
inv' t γ ∗
owner₁ γ Stable back data1 cap1 ws ∗
front۰lb γ front ∗
array۰cslice data1 cap1 front (DfracOwn (1/2)) (vs ++ priv1) ∗
array۰cslice data2 cap2 front (DfracOwn (1/2)) (vs ++ priv2)
}}}
#t <-{data} data2
{{{
RET ();
owner₁ γ Stable back data2 cap2 ws ∗
array۰cslice data1 cap1 front (DfracOwn (1/2)) (vs ++ priv1)
}}}.
#[local] Lemma array٠unsafe_cgetｰspecｰloser t γ (data : val) i :
(0 ≤ i)%Z →
{{{
inv' t γ ∗
datas۰elem γ data
}}}
array٠unsafe_cget data #i
{{{
v
, RET v;
True
}}}.
#[local] Lemma array٠unsafe_cgetｰspecｰwinner۰pop t γ front data P v :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P ∗
history۰at γ front v
}}}
array٠unsafe_cget data #front
{{{
RET v;
winner۰pop γ front (Some data) P
}}}.
#[local] Lemma array٠unsafe_csetｰspecｰowner t γ back data cap ws us front v :
back < front + cap →
{{{
inv' t γ ∗
owner' γ Stable back data cap ws back us ∗
front۰lb γ front
}}}
array٠unsafe_cset data #back v
{{{
RET ();
owner' γ Stable back data cap ws back (<[0 := v]> us)
}}}.
#[local] Lemma resolveｰspecｰloser₁ t γ front1 front2 id :
front1 < front2 →
{{{
inv' t γ ∗
front۰lb γ front2
}}}
Resolve (CAS (#t).[front]%V #front1 #(front1 + 1)) #γ.(ws_deque_1۰name۰prophet) (#front1, #id)%V
{{{
RET false;
True
}}}.
#[local] Lemma resolveｰspecｰloser₂ t γ front id prophs0 :
head prophs0 ≠ Some id →
{{{
inv' t γ ∗
front۰lb γ front ∗
prophet_multi۰full prophet_identifier γ.(ws_deque_1۰name۰prophet_name) front prophs0
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET false;
front۰lb γ ˖front
}}}.
#[local] Lemma resolveｰspecｰwinner۰pop t γ front data P id :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET true;
▷ P
}}}.
#[local] Lemma resolveｰspecｰwinner۰steal t γ front P id :
{{{
inv' t γ ∗
winner۰steal γ front None P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET true;
front۰lb γ ˖front
}}}.
#[local] Lemma resolveｰspecｰEmpty t γ back data cap ws id :
{{{
inv' t γ ∗
owner₁ γ Stable back data cap ws ∗
front۰lb γ back
}}}
Resolve (CAS (#t).[front]%V #back #(back + 1)) #γ.(ws_deque_1۰name۰prophet) (#back, #id)%V
{{{
RET true;
owner₁ γ Unstable back data cap ws ∗
front۰lb γ ˖back
}}}.
Lemma ws_deque_1٠sizeｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ vs
| RET #(length vs);
ws_deque_1۰owner γ vs
>>>.
Lemma ws_deque_1٠is_emptyｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ vs
| RET #(bool_decide (vs = []%list));
ws_deque_1۰owner γ vs
>>>.
Lemma ws_deque_1٠pushｰspec t γ ι ws v :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠push #t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ (vs ++ [v])
| RET ();
ws_deque_1۰owner γ (vs ++ [v])
>>>.
Lemma ws_deque_1٠stealｰspec t γ ι :
<<<
ws_deque_1۰inv t γ ι
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠steal #t @ ↑ι
<<<
ws_deque_1۰model γ (tail vs)
| RET head vs;
True
>>>.
Variant pop_state :=
| PopNonempty v
| PopEmptyishWinner v
| PopEmptyishLoser
| PopSuperempty.
#[local] Lemma ws_deque_1٠pop₁ｰspec {t γ} (state : pop_state) stable back (back_ : Z) data cap ws us id :
back_ = back →
{{{
inv' t γ ∗
owner' γ stable back data cap ws back us ∗
match state with
| PopNonempty v ⇒
⌜stable = Stable⌝ ∗
⌜us !! 0 = Some v⌝
| PopEmptyishWinner v ⇒
⌜stable = Unstable⌝ ∗
⌜us !! 0 = Some v⌝ ∗
winner۰steal γ back None inhabitant
| PopEmptyishLoser ⇒
∃ id_winner prophs,
⌜stable = Unstable⌝ ∗
prophet_multi۰full prophet_identifier γ.(ws_deque_1۰name۰prophet_name) back (id_winner :: prophs) ∗
⌜head (id_winner :: prophs) ≠ Some id⌝
| PopSuperempty ⇒
∃ front,
⌜stable = Unstable⌝ ∗
front۰lb γ front ∗
⌜front = ˖back⌝
end
}}}
ws_deque_1٠pop₁ #t #id #back_
{{{
o back data cap i us
, RET o;
owner' γ Stable back data cap ws i us ∗
match state with
| PopNonempty v ⇒
⌜o = Some v⌝
| PopEmptyishWinner v ⇒
⌜o = Some v⌝
| PopEmptyishLoser ⇒
⌜o = None⌝
| PopSuperempty ⇒
⌜o = None⌝
end
}}}.
Lemma ws_deque_1٠popｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_1۰model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_1۰model γ vs'
end
| RET o;
ws_deque_1۰owner γ ws'
>>>.
End ws_deque_1۰G.
#[global] Opaque ws_deque_1۰inv.
#[global] Opaque ws_deque_1۰model.
#[global] Opaque ws_deque_1۰owner.
End base.
Require zoo_saturn.ws_deque_1__opaque.
Section ws_deque_1۰G.
Context `{ws_deque_1۰G : WsDeque1G Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition ws_deque_1۰inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_deque_1۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_deque_1۰owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_1۰modelｰtimeless γ vs :
Timeless (ws_deque_1۰model γ vs).
#[global] Instance ws_deque_1۰ownerｰtimeless γ ws :
Timeless (ws_deque_1۰owner γ ws).
#[global] Instance ws_deque_1۰invｰpersistent t ι :
Persistent (ws_deque_1۰inv t ι).
Lemma ws_deque_1۰modelｰexclusive t vs1 vs2 :
ws_deque_1۰model t vs1 -∗
ws_deque_1۰model t vs2 -∗
False.
Lemma ws_deque_1۰ownerｰexclusive t ws1 ws2 :
ws_deque_1۰owner t ws1 -∗
ws_deque_1۰owner t ws2 -∗
False.
Lemma ws_deque_1ｰownerｰmodel γ ws vs :
ws_deque_1۰owner γ ws -∗
ws_deque_1۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_1٠createｰspec ι :
{{{
True
}}}
ws_deque_1٠create ()
{{{
t
, RET t;
ws_deque_1۰inv t ι ∗
ws_deque_1۰model t [] ∗
ws_deque_1۰owner t []
}}}.
Lemma ws_deque_1٠sizeｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t vs
| RET #(length vs);
ws_deque_1۰owner t vs
>>>.
Lemma ws_deque_1٠is_emptyｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t vs
| RET #(bool_decide (vs = []%list));
ws_deque_1۰owner t vs
>>>.
Lemma ws_deque_1٠pushｰspec t ι ws v :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠push t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t (vs ++ [v])
| RET ();
ws_deque_1۰owner t (vs ++ [v])
>>>.
Lemma ws_deque_1٠stealｰspec t ι :
<<<
ws_deque_1۰inv t ι
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠steal t @ ↑ι
<<<
ws_deque_1۰model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_1٠popｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_1۰model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_1۰model t vs'
end
| RET o;
ws_deque_1۰owner t ws'
>>>.
End ws_deque_1۰G.
#[global] Opaque ws_deque_1۰inv.
#[global] Opaque ws_deque_1۰model.
#[global] Opaque ws_deque_1۰owner.
Require Import zoo.common.countable.
Require Import zoo.common.function.
Require Import zoo.common.list.
Require Import zoo.common.relations.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.auth_twins.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.mono_gmultiset.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_identifier.
Require Import zoo.program_logic.prophet_multi.
Require Import zoo_std.option.
Require Export zoo_saturn.ws_deque_1__code.
Require Import zoo_saturn.ws_deque_1__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type front back : nat.
Implicit Type id : prophet_id.
Implicit Type v : val.
Implicit Type us vs ws hist priv : list val.
Implicit Type datas : gmultiset val.
Implicit Type past prophs : list prophet_identifier.(prophet_typed۰type).
Implicit Type pasts prophss : nat → list prophet_identifier.(prophet_typed۰type).
Variant state :=
| Empty
| Nonempty
| Emptyish
| Superempty.
Implicit Type state : state.
#[local] Instance stateｰinhabited : Inhabited state :=
populate Empty.
Variant stability :=
| Stable
| Unstable.
Implicit Type stable : stability.
#[local] Instance stabilityｰinhabited : Inhabited stability :=
populate Stable.
Class WsDeque1G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deque_1۰G۰prophet۰G :: ProphetMultiG Σ prophet_identifier
; #[local] ws_deque_1۰G۰model۰G :: AuthTwinsG Σ (leibnizO (list val)) suffix
; #[local] ws_deque_1۰G۰owner۰G :: TwinsG Σ (leibnizO (stability × nat × val × nat))
; #[local] ws_deque_1۰G۰front۰G :: AuthNatMaxG Σ
; #[local] ws_deque_1۰G۰history۰G :: MonoListG Σ val
; #[local] ws_deque_1۰G۰winner۰G :: TwinsG Σ (natO × leibnizO (option val) × ▶ ∙)
; #[local] ws_deque_1۰G۰datas۰G :: MonoGmultisetG Σ val
}.
Definition ws_deque_1۰Σ :=
#[prophet_multi۰Σ prophet_identifier
; auth_twins۰Σ (leibnizO (list val)) suffix
; twins۰Σ (leibnizO (stability × nat × val × nat))
; auth_nat_max۰Σ
; mono_list۰Σ val
; twins۰Σ (natO × leibnizO (option val) × ▶ ∙)
; mono_gmultiset۰Σ val
].
#[global] Instance subGｰws_deque_1۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deque_1۰Σ Σ →
WsDeque1G Σ .
#[local] Definition min_capacity :=
val۰to_nat' ws_deque_1٠min_capacity.
#[local] Lemma min_capacityｰnonzero :
0 < min_capacity.
#[local] Hint Resolve
min_capacityｰnonzero
: core.
#[local] Lemma ws_deque_1٠min_capacityｰunfold :
ws_deque_1٠min_capacity = #min_capacity.
Opaque ws_deque_1٠min_capacity.
Opaque min_capacity.
Module base.
Section ws_deque_1۰G.
Context `{ws_deque_1۰G : WsDeque1G Σ}.
Implicit Type t : location.
Implicit Type P : iProp Σ.
Record ws_deque_1۰name :=
{ ws_deque_1۰name۰inv : namespace
; ws_deque_1۰name۰prophet : prophet_id
; ws_deque_1۰name۰prophet_name : prophet_multi۰name
; ws_deque_1۰name۰model : auth_twins۰name
; ws_deque_1۰name۰owner : gname
; ws_deque_1۰name۰front : gname
; ws_deque_1۰name۰history : gname
; ws_deque_1۰name۰winner : gname
; ws_deque_1۰name۰datas : gname
}.
Implicit Type γ : ws_deque_1۰name.
#[global] Instance ws_deque_1۰nameｰeq_dec : EqDecision ws_deque_1۰name :=
ltac:(solve_decision).
#[global] Instance ws_deque_1۰nameｰcountable :
Countable ws_deque_1۰name.
#[local] Definition model₁' γ_model vs :=
auth_twins۰twin₁ _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_deque_1۰name۰model).
#[local] Definition model₂' γ_model vs :=
auth_twins۰twin₂ _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_deque_1۰name۰model).
#[local] Definition owner₁' γ_owner γ_model stable back data cap ws : iProp Σ :=
twins۰twin₁ (twins۰G := ws_deque_1۰G۰owner۰G) γ_owner (DfracOwn 1) (stable, back, data, cap) ∗
auth_twins۰auth _ γ_model ws.
#[local] Definition owner₁ γ :=
owner₁' γ.(ws_deque_1۰name۰owner) γ.(ws_deque_1۰name۰model).
#[local] Instance : CustomIpat "owner₁" :=
" ( Howner₁{_{}} & Hmodel_auth{_{}} ) ".
#[local] Definition owner₂' γ_owner stable back data cap :=
twins۰twin₂ (twins۰G := ws_deque_1۰G۰owner۰G) γ_owner (stable, back, data, cap).
#[local] Definition owner₂ γ :=
owner₂' γ.(ws_deque_1۰name۰owner).
#[local] Definition front۰auth' γ_front :=
auth_nat_max۰auth γ_front (DfracOwn 1).
#[local] Definition front۰auth γ :=
front۰auth' γ.(ws_deque_1۰name۰front).
#[local] Definition front۰lb γ :=
auth_nat_max۰lb γ.(ws_deque_1۰name۰front).
#[local] Definition history۰auth' γ_history :=
mono_list۰auth γ_history (DfracOwn 1).
#[local] Definition history۰auth γ :=
history۰auth' γ.(ws_deque_1۰name۰history).
#[local] Definition history۰at γ :=
mono_list۰at γ.(ws_deque_1۰name۰history).
#[local] Definition winner۰pop' γ_winner front (data : option val) P : iProp Σ :=
twins۰twin₁ γ_winner (DfracOwn 1) (front, data, Next P).
#[local] Definition winner۰pop γ :=
winner۰pop' γ.(ws_deque_1۰name۰winner).
#[local] Definition winner۰steal' γ_winner front (data : option val) P :=
twins۰twin₂ γ_winner (front, data, Next P).
#[local] Definition winner۰steal γ :=
winner۰steal' γ.(ws_deque_1۰name۰winner).
#[local] Definition winner γ : iProp Σ :=
∃ front data P1 P2,
winner۰pop γ front data P1 ∗
winner۰steal γ front data P2.
#[local] Instance : CustomIpat "winner" :=
" ( %front_winner & %data_winner & %P1 & %P2 & Hwinner_pop{_{}} & Hwinner_steal{_{}} ) ".
#[local] Definition datas۰auth' γ_datas :=
mono_gmultiset۰auth γ_datas (DfracOwn 1).
#[local] Definition datas۰auth γ :=
datas۰auth' γ.(ws_deque_1۰name۰datas).
#[local] Definition datas۰elem' γ_datas :=
mono_gmultiset۰elem γ_datas.
#[local] Definition datas۰elem γ :=
datas۰elem' γ.(ws_deque_1۰name۰datas).
#[local] Definition data۰model data : iProp Σ :=
∃ cap i vs,
array۰cslice data cap i DfracDiscarded vs ∗
⌜0 < cap⌝ ∗
⌜length vs = cap⌝.
#[local] Instance : CustomIpat "data۰model" :=
" ( %cap_data{} & %i_data{} & %vs_data{} & Hdata{}_cslice & %Hcap_data{} & %Hvs_data{} ) ".
#[local] Definition winner۰au γ front P : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(ws_deque_1۰name۰inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs' ∗
history۰at γ front v
, COMM
P
}>.
#[local] Definition winner۰model₁ γ front data data_winner : iProp Σ :=
⌜data = data_winner⌝
∨ ∃ cap_winner v,
array۰cslice data_winner cap_winner front DfracDiscarded [v] ∗
history۰at γ front v.
#[local] Instance : CustomIpat "winner۰model₁" :=
" [ -> | ( %cap & %v_ & Hdata_cslice & Hhistory_at_ ) ] ".
#[local] Definition winner۰model₂ γ front data data_winner P : iProp Σ :=
winner۰steal γ front (Some data_winner) P ∗
winner۰model₁ γ front data data_winner.
#[local] Instance : CustomIpat "winner۰model₂" :=
" ( Hwinner_steal{_{!}} & Hwinner ) ".
#[local] Definition winner۰pending₁ γ front data data_winner P id : iProp Σ :=
winner۰model₂ γ front data data_winner P ∗
identifier۰model id ∗
winner۰au γ front P.
#[local] Instance : CustomIpat "winner۰pending₁" :=
" ( (:winner۰model₂) & Hid{_{!}} & HP ) ".
#[local] Definition winner۰pending₂ γ front data id : iProp Σ :=
∃ data_winner P,
winner۰pending₁ γ front data data_winner P id.
#[local] Instance : CustomIpat "winner۰pending₂" :=
" ( %data_winner & %P{} & (:winner۰pending₁) ) ".
#[local] Definition winner۰linearized₁ γ front data data_winner P : iProp Σ :=
winner۰model₂ γ front data data_winner P ∗
P.
#[local] Instance : CustomIpat "winner۰linearized₁" :=
" ( (:winner۰model₂) & HP ) ".
#[local] Definition winner۰linearized₂ γ front data P : iProp Σ :=
∃ data_winner,
winner۰linearized₁ γ front data data_winner P.
#[local] Instance : CustomIpat "winner۰linearized₂" :=
" ( %data_winner & (:winner۰linearized₁) ) ".
#[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 data hist vs prophs : iProp Σ :=
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant vs) ∗
( winner γ
∨ match prophs with
| [] ⇒
False
| id :: _ ⇒
winner۰pending₂ γ front data 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 data hist vs prophs data_winner P : iProp Σ :=
⌜state = Nonempty⌝ ∗
⌜stable = Stable⌝ ∗
⌜front < back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant vs) ∗
match prophs with
| [] ⇒
False
| id :: _ ⇒
winner۰pending₁ γ front data data_winner 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 data hist priv : iProp Σ :=
∃ P,
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
( winner۰pop γ front None P
∨ winner۰linearized₂ γ front data 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 = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
winner۰pop γ front None 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 data hist priv data_winner P : iProp Σ :=
⌜state = Emptyish⌝ ∗
⌜stable = Unstable⌝ ∗
⌜front = back⌝ ∗
⌜length hist = ˖front⌝ ∗
history۰at γ front (hd inhabitant priv) ∗
winner۰linearized₁ γ front data data_winner 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 = ˖back⌝ ∗
⌜length hist = front⌝ ∗
winner γ.
#[local] Instance : CustomIpat "inv۰state۰superempty" :=
" ( { {lazy}{>}% ; {lazy}% ; {>}-> ; -> } & {>;}-> & {>;}%Hhist{} & Hwinner ) ".
#[local] Definition inv۰state γ state stable front back data hist vs priv prophs : iProp Σ :=
match state with
| Empty ⇒
inv۰state۰empty γ stable front back hist
| Nonempty ⇒
inv۰state۰nonempty γ stable front back data hist vs prophs
| Emptyish ⇒
inv۰state۰emptyish γ stable front back data hist priv
| Superempty ⇒
inv۰state۰superempty γ stable front back hist
end.
#[local] Definition inv۰inner t γ : iProp Σ :=
∃ state stable front back data cap hist vs priv datas pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
t.[data] ↦ data ∗
owner₂ γ stable back data cap ∗
front۰auth γ front ∗
⌜0 < front⌝ ∗
model₂ γ vs ∗
⌜length vs = back - front⌝ ∗
array۰cslice data cap front (DfracOwn (1/2)) (vs ++ priv) ∗
⌜0 < cap⌝ ∗
⌜(length vs + length priv)%nat = cap⌝ ∗
history۰auth γ hist ∗
datas۰auth γ ({[+data+]} ⊎ datas) ∗
([∗ mset] data ∈ datas, data۰model data) ∗
prophet_multi۰model prophet_identifier γ.(ws_deque_1۰name۰prophet) γ.(ws_deque_1۰name۰prophet_name) pasts prophss ∗
⌜∀ i, front ≤ i → pasts i = []⌝ ∗
inv۰state γ state stable front back data hist vs priv (prophss front).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %state{} & %stable{} & %front{} & %back{} & %data{} & %cap{} & %hist{} & %vs{} & %priv{} & %datas{} & %pasts{} & %prophss{} & >Ht_front & >Ht_back & >Ht_data & >Howner₂ & >Hfront_auth & >%Hfront{} & >Hmodel₂ & >%Hvs{} & >Hdata{}_cslice₁ & >%Hcap{} & >%Hdata{} & >Hhistory_auth & >Hdatas_auth & >Hdatas & >Hprophet_model & >%Hpasts{} & Hstate ) ".
#[local] Definition inv' t γ : iProp Σ :=
t.[proph] ↦□ #γ.(ws_deque_1۰name۰prophet) ∗
inv γ.(ws_deque_1۰name۰inv) (inv۰inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Ht_proph & #Hinv ) ".
Definition ws_deque_1۰inv t γ ι : iProp Σ :=
⌜ι = γ.(ws_deque_1۰name۰inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & (:inv') ) ".
Definition ws_deque_1۰model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Definition owner' γ stable back data cap ws i us : iProp Σ :=
owner₁ γ stable back data cap ws ∗
array۰cslice data cap i (DfracOwn (1/2)) us ∗
⌜0 < cap⌝ ∗
⌜length us = cap⌝.
#[local] Instance : CustomIpat "owner'" :=
" ( Howner₁{_{}} & Hdata_cslice₂{_{}} & { {!} _ ; %Hcap{} ; %Hcap } & { {!} _ ; %Hus{} ; %Hus } ) ".
Definition ws_deque_1۰owner γ ws : iProp Σ :=
∃ back data cap i us,
owner' γ Stable back data cap ws i us.
#[local] Instance : CustomIpat "owner" :=
" ( %back{} & %data{} & %cap{} & %i{} & %us{} & Howner{_{}} ) ".
#[global] Instance ws_deque_1۰modelｰtimeless γ vs :
Timeless (ws_deque_1۰model γ vs).
#[global] Instance ws_deque_1۰ownerｰtimeless γ ws :
Timeless (ws_deque_1۰owner γ ws).
#[global] Instance ws_deque_1۰invｰpersistent t γ ι :
Persistent (ws_deque_1۰inv t γ ι).
#[local] Lemma modelｰownerｰalloc data cap :
⊢ |==>
∃ γ_model γ_owner,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner₁' γ_owner γ_model Stable 1 data cap [] ∗
owner₂' γ_owner Stable 1 data cap.
#[local] Lemma model₁ｰvalid γ stable back data cap ws vs :
owner₁ γ stable back data cap 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 data cap ws vs1 vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma modelｰempty {γ stable back data cap ws vs1 vs2} :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap [] ∗
model₁ γ [] ∗
model₂ γ [].
#[local] Lemma modelｰpush {γ stable back data cap ws vs1 vs2} v :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap (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 data cap ws vs1 vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma modelｰpop' γ stable back data cap ws vs1 v vs2 :
owner₁ γ stable back data cap ws -∗
model₁ γ (vs1 ++ [v]) -∗
model₂ γ vs2 ==∗
owner₁ γ stable back data cap vs1 ∗
model₁ γ vs1 ∗
model₂ γ vs1.
#[local] Lemma owner₁ｰexclusive γ stable1 back1 data1 cap1 ws1 stable2 back2 data2 cap2 ws2 :
owner₁ γ stable1 back1 data1 cap1 ws1 -∗
owner₁ γ stable2 back2 data2 cap2 ws2 -∗
False.
#[local] Lemma ownerｰagree γ stable1 back1 data1 cap1 ws stable2 back2 data2 cap2 :
owner₁ γ stable1 back1 data1 cap1 ws -∗
owner₂ γ stable2 back2 data2 cap2 -∗
⌜stable1 = stable2⌝ ∗
⌜back1 = back2⌝ ∗
⌜data1 = data2⌝ ∗
⌜cap1 = cap2⌝.
#[local] Lemma owner₁ｰupdate γ stable back data cap ws vs :
owner₁ γ stable back data cap ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner₁ γ stable back data cap vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma ownerｰupdate {γ stable1 back1 data1 cap1 ws stable2 back2 data2 cap2} stable back data cap :
owner₁ γ stable1 back1 data1 cap1 ws -∗
owner₂ γ stable2 back2 data2 cap2 ==∗
owner₁ γ stable back data cap ws ∗
owner₂ γ stable back data cap.
#[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 γ ˖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 None True ∗
winner۰steal' γ_winner 1 None True.
#[local] Lemma winner۰popｰexclusive γ front1 data1 P1 front2 data2 P2 :
winner۰pop γ front1 data1 P1 -∗
winner۰pop γ front2 data2 P2 -∗
False.
#[local] Lemma winner۰popｰexclusive' γ front data P :
winner۰pop γ front data P -∗
winner γ -∗
False.
#[local] Lemma winner۰stealｰexclusive γ front1 data1 P1 front2 data2 P2 :
winner۰steal γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 -∗
False.
#[local] Lemma winner۰stealｰexclusive' γ front data P :
winner۰steal γ front data P -∗
winner γ -∗
False.
#[local] Lemma winnerｰagree γ front1 data1 P1 front2 data2 P2 :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 -∗
⌜front1 = front2⌝ ∗
⌜data1 = data2⌝ ∗
▷ (P1 ≡ P2).
#[local] Lemma winnerｰupdate' {γ front1 data1 P1 front2 data2 P2} front data :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 ==∗
winner۰pop γ front data P1 ∗
winner۰steal γ front data P2.
#[local] Lemma winnerｰupdate {γ front1 data1 P1 front2 data2 P2} front data P :
winner۰pop γ front1 data1 P1 -∗
winner۰steal γ front2 data2 P2 ==∗
winner۰pop γ front data P ∗
winner۰steal γ front data P.
#[local] Lemma datasｰalloc data :
⊢ |==>
∃ γ_datas,
datas۰auth' γ_datas ({[+data+]} ⊎ ∅).
#[local] Lemma datas۰elemｰget γ data datas :
datas۰auth γ ({[+data+]} ⊎ datas) ⊢
datas۰elem γ data.
#[local] Lemma datas۰elemｰvalid γ data1 datas data2 :
datas۰auth γ ({[+data1+]} ⊎ datas) -∗
datas۰elem γ data2 -∗
⌜data1 = data2 ∨ data2 ∈ datas⌝.
#[local] Lemma datasｰinsert {γ datas} data :
datas۰auth γ datas ⊢ |==>
datas۰auth γ ({[+data+]} ⊎ datas).
Opaque owner₁'.
Lemma ws_deque_1۰modelｰexclusive γ vs1 vs2 :
ws_deque_1۰model γ vs1 -∗
ws_deque_1۰model γ vs2 -∗
False.
#[local] Lemma owner'ｰrebase {γ stable back data cap ws i1 us} i2 :
owner' γ stable back data cap ws i1 us ⊢
∃ us,
owner' γ stable back data cap ws i2 us.
#[local] Lemma array۰csliceｰreshape {data cap back dq us} front :
0 < cap →
length us = cap →
front ≤ back →
back ≤ front + cap →
array۰cslice data cap back dq us ⊢
∃ vs priv,
⌜(front + length vs)%nat = back⌝ ∗
⌜(length vs + length priv)%nat = cap⌝ ∗
array۰cslice data cap front dq (vs ++ priv) ∗
( array۰cslice data cap front dq (vs ++ priv) -∗
array۰cslice data cap back dq us
).
Lemma ws_deque_1۰ownerｰexclusive γ ws1 ws2 :
ws_deque_1۰owner γ ws1 -∗
ws_deque_1۰owner γ ws2 -∗
False.
Lemma ws_deque_1ｰownerｰmodel γ ws vs :
ws_deque_1۰owner γ ws -∗
ws_deque_1۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
#[local] Lemma inv۰stateｰStable γ state front data back hist vs priv prophs :
length vs = back - front →
inv۰state γ state Stable front back data hist vs priv prophs ⊢
⌜state = Empty ∨ state = Nonempty⌝ ∗
⌜front ≤ back⌝.
#[local] Lemma inv۰stateｰUnstable γ state front back data hist vs priv prophs :
inv۰state γ state Unstable front back data hist vs priv prophs ⊢
⌜state = Emptyish ∨ state = Superempty⌝ ∗
⌜front = back ∨ front = ˖back⌝.
#[local] Lemma inv۰stateｰNonempty γ state stable front back data hist vs priv prophs :
front < back →
inv۰state γ state stable front back data hist vs priv prophs ⊢
⌜state = Nonempty⌝.
#[local] Lemma inv۰stateｰSuperempty γ state front back data hist vs priv prophs :
back < front →
inv۰state γ state Unstable front back data hist vs priv prophs -∗
⌜state = Superempty⌝.
#[local] Lemma inv۰stateｰwinner۰pop γ state stable front1 back data1 hist vs priv prophs front2 data2 P :
inv۰state γ state stable front1 back data1 hist vs priv prophs -∗
winner۰pop γ front2 (Some data2) P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P ≡ P_) ∗
( inv۰state۰nonempty۰steal γ state stable front2 back data1 hist vs prophs data2 P_
∨ inv۰state۰emptyish۰steal γ state stable front2 back data1 hist priv data2 P_
) ∗
winner۰model₁ γ front2 data1 data2 ∗
winner۰pop γ front2 (Some data2) P.
#[local] Lemma inv۰stateｰwinner۰steal γ state stable front2 back data1 hist vs priv prophs front1 data2 P :
inv۰state γ state stable front1 back data1 hist vs priv prophs -∗
winner۰steal γ front2 data2 P -∗
∃ P_,
⌜front1 = front2⌝ ∗
▷ (P_ ≡ P) ∗
inv۰state۰emptyish۰pop γ state stable front2 back hist priv P_ ∗
winner۰steal γ front2 data2 P.
Lemma ws_deque_1٠createｰspec ι :
{{{
True
}}}
ws_deque_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰model γ [] ∗
ws_deque_1۰owner γ []
}}}.
#[local] Lemma frontｰspec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front
, RET #front;
front۰lb γ front
}}}.
#[local] Lemma frontｰspecｰownerｰStable t γ back data cap ws :
{{{
inv' t γ ∗
owner₁ γ Stable back data cap ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Stable back data cap ws ∗
front۰lb γ front ∗
⌜front ≤ back⌝
}}}.
#[local] Lemma frontｰspecｰownerｰUnstable t γ back data cap ws :
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws
}}}
(#t).{front}
{{{
front
, RET #front;
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front ∗
⌜front = back ∨ front = ˖back⌝
}}}.
#[local] Lemma frontｰspecｰSuperempty t γ back data cap ws front :
back < front →
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front
}}}
(#t).{front}
{{{
RET #front;
owner₁ γ Unstable back data cap ws
}}}.
#[local] Lemma frontｰspecｰwinner۰steal t γ front data P :
{{{
inv' t γ ∗
winner۰steal γ front data P
}}}
(#t).{front}
{{{
RET #front;
winner۰steal γ front data P
}}}.
#[local] Lemma backｰspec t γ stable back data cap ws :
{{{
inv' t γ ∗
owner₁ γ stable back data cap ws
}}}
(#t).{back}
{{{
RET #back;
owner₁ γ stable back data cap ws
}}}.
#[local] Lemma set_backｰspecｰSuperempty t γ back data cap ws front (back' : Z) :
back < front →
back' = ˖back →
{{{
inv' t γ ∗
owner₁ γ Unstable back data cap ws ∗
front۰lb γ front
}}}
#t <-{back} #back'
{{{
RET ();
owner₁ γ Stable ˖back data cap ws
}}}.
#[local] Lemma dataｰspec t γ :
{{{
inv' t γ
}}}
(#t).{data}
{{{
data
, RET data;
datas۰elem γ data
}}}.
#[local] Lemma dataｰspecｰowner t γ stable back data cap ws :
{{{
inv' t γ ∗
owner₁ γ stable back data cap ws
}}}
(#t).{data}
{{{
RET data;
owner₁ γ stable back data cap ws
}}}.
#[local] Lemma dataｰspecｰwinner۰pop t γ front data P :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P
}}}
(#t).{data}
{{{
data
, RET data;
winner۰pop γ front (Some data) P
}}}.
#[local] Lemma set_dataｰspec t γ front vs back data1 cap1 priv1 ws data2 cap2 priv2 :
0 < cap2 →
front + length vs = back →
length vs + length priv1 = cap1 →
length vs + length priv2 = cap2 →
{{{
inv' t γ ∗
owner₁ γ Stable back data1 cap1 ws ∗
front۰lb γ front ∗
array۰cslice data1 cap1 front (DfracOwn (1/2)) (vs ++ priv1) ∗
array۰cslice data2 cap2 front (DfracOwn (1/2)) (vs ++ priv2)
}}}
#t <-{data} data2
{{{
RET ();
owner₁ γ Stable back data2 cap2 ws ∗
array۰cslice data1 cap1 front (DfracOwn (1/2)) (vs ++ priv1)
}}}.
#[local] Lemma array٠unsafe_cgetｰspecｰloser t γ (data : val) i :
(0 ≤ i)%Z →
{{{
inv' t γ ∗
datas۰elem γ data
}}}
array٠unsafe_cget data #i
{{{
v
, RET v;
True
}}}.
#[local] Lemma array٠unsafe_cgetｰspecｰwinner۰pop t γ front data P v :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P ∗
history۰at γ front v
}}}
array٠unsafe_cget data #front
{{{
RET v;
winner۰pop γ front (Some data) P
}}}.
#[local] Lemma array٠unsafe_csetｰspecｰowner t γ back data cap ws us front v :
back < front + cap →
{{{
inv' t γ ∗
owner' γ Stable back data cap ws back us ∗
front۰lb γ front
}}}
array٠unsafe_cset data #back v
{{{
RET ();
owner' γ Stable back data cap ws back (<[0 := v]> us)
}}}.
#[local] Lemma resolveｰspecｰloser₁ t γ front1 front2 id :
front1 < front2 →
{{{
inv' t γ ∗
front۰lb γ front2
}}}
Resolve (CAS (#t).[front]%V #front1 #(front1 + 1)) #γ.(ws_deque_1۰name۰prophet) (#front1, #id)%V
{{{
RET false;
True
}}}.
#[local] Lemma resolveｰspecｰloser₂ t γ front id prophs0 :
head prophs0 ≠ Some id →
{{{
inv' t γ ∗
front۰lb γ front ∗
prophet_multi۰full prophet_identifier γ.(ws_deque_1۰name۰prophet_name) front prophs0
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET false;
front۰lb γ ˖front
}}}.
#[local] Lemma resolveｰspecｰwinner۰pop t γ front data P id :
{{{
inv' t γ ∗
winner۰pop γ front (Some data) P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET true;
▷ P
}}}.
#[local] Lemma resolveｰspecｰwinner۰steal t γ front P id :
{{{
inv' t γ ∗
winner۰steal γ front None P
}}}
Resolve (CAS (#t).[front]%V #front #(front + 1)) #γ.(ws_deque_1۰name۰prophet) (#front, #id)%V
{{{
RET true;
front۰lb γ ˖front
}}}.
#[local] Lemma resolveｰspecｰEmpty t γ back data cap ws id :
{{{
inv' t γ ∗
owner₁ γ Stable back data cap ws ∗
front۰lb γ back
}}}
Resolve (CAS (#t).[front]%V #back #(back + 1)) #γ.(ws_deque_1۰name۰prophet) (#back, #id)%V
{{{
RET true;
owner₁ γ Unstable back data cap ws ∗
front۰lb γ ˖back
}}}.
Lemma ws_deque_1٠sizeｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ vs
| RET #(length vs);
ws_deque_1۰owner γ vs
>>>.
Lemma ws_deque_1٠is_emptyｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ vs
| RET #(bool_decide (vs = []%list));
ws_deque_1۰owner γ vs
>>>.
Lemma ws_deque_1٠pushｰspec t γ ι ws v :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠push #t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model γ (vs ++ [v])
| RET ();
ws_deque_1۰owner γ (vs ++ [v])
>>>.
Lemma ws_deque_1٠stealｰspec t γ ι :
<<<
ws_deque_1۰inv t γ ι
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠steal #t @ ↑ι
<<<
ws_deque_1۰model γ (tail vs)
| RET head vs;
True
>>>.
Variant pop_state :=
| PopNonempty v
| PopEmptyishWinner v
| PopEmptyishLoser
| PopSuperempty.
#[local] Lemma ws_deque_1٠pop₁ｰspec {t γ} (state : pop_state) stable back (back_ : Z) data cap ws us id :
back_ = back →
{{{
inv' t γ ∗
owner' γ stable back data cap ws back us ∗
match state with
| PopNonempty v ⇒
⌜stable = Stable⌝ ∗
⌜us !! 0 = Some v⌝
| PopEmptyishWinner v ⇒
⌜stable = Unstable⌝ ∗
⌜us !! 0 = Some v⌝ ∗
winner۰steal γ back None inhabitant
| PopEmptyishLoser ⇒
∃ id_winner prophs,
⌜stable = Unstable⌝ ∗
prophet_multi۰full prophet_identifier γ.(ws_deque_1۰name۰prophet_name) back (id_winner :: prophs) ∗
⌜head (id_winner :: prophs) ≠ Some id⌝
| PopSuperempty ⇒
∃ front,
⌜stable = Unstable⌝ ∗
front۰lb γ front ∗
⌜front = ˖back⌝
end
}}}
ws_deque_1٠pop₁ #t #id #back_
{{{
o back data cap i us
, RET o;
owner' γ Stable back data cap ws i us ∗
match state with
| PopNonempty v ⇒
⌜o = Some v⌝
| PopEmptyishWinner v ⇒
⌜o = Some v⌝
| PopEmptyishLoser ⇒
⌜o = None⌝
| PopSuperempty ⇒
⌜o = None⌝
end
}}}.
Lemma ws_deque_1٠popｰspec t γ ι ws :
<<<
ws_deque_1۰inv t γ ι ∗
ws_deque_1۰owner γ ws
| ∀∀ vs,
ws_deque_1۰model γ vs
>>>
ws_deque_1٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_1۰model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_1۰model γ vs'
end
| RET o;
ws_deque_1۰owner γ ws'
>>>.
End ws_deque_1۰G.
#[global] Opaque ws_deque_1۰inv.
#[global] Opaque ws_deque_1۰model.
#[global] Opaque ws_deque_1۰owner.
End base.
Require zoo_saturn.ws_deque_1__opaque.
Section ws_deque_1۰G.
Context `{ws_deque_1۰G : WsDeque1G Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition ws_deque_1۰inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_deque_1۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_deque_1۰owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_1۰owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_1۰modelｰtimeless γ vs :
Timeless (ws_deque_1۰model γ vs).
#[global] Instance ws_deque_1۰ownerｰtimeless γ ws :
Timeless (ws_deque_1۰owner γ ws).
#[global] Instance ws_deque_1۰invｰpersistent t ι :
Persistent (ws_deque_1۰inv t ι).
Lemma ws_deque_1۰modelｰexclusive t vs1 vs2 :
ws_deque_1۰model t vs1 -∗
ws_deque_1۰model t vs2 -∗
False.
Lemma ws_deque_1۰ownerｰexclusive t ws1 ws2 :
ws_deque_1۰owner t ws1 -∗
ws_deque_1۰owner t ws2 -∗
False.
Lemma ws_deque_1ｰownerｰmodel γ ws vs :
ws_deque_1۰owner γ ws -∗
ws_deque_1۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_1٠createｰspec ι :
{{{
True
}}}
ws_deque_1٠create ()
{{{
t
, RET t;
ws_deque_1۰inv t ι ∗
ws_deque_1۰model t [] ∗
ws_deque_1۰owner t []
}}}.
Lemma ws_deque_1٠sizeｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t vs
| RET #(length vs);
ws_deque_1۰owner t vs
>>>.
Lemma ws_deque_1٠is_emptyｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t vs
| RET #(bool_decide (vs = []%list));
ws_deque_1۰owner t vs
>>>.
Lemma ws_deque_1٠pushｰspec t ι ws v :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠push t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_1۰model t (vs ++ [v])
| RET ();
ws_deque_1۰owner t (vs ++ [v])
>>>.
Lemma ws_deque_1٠stealｰspec t ι :
<<<
ws_deque_1۰inv t ι
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠steal t @ ↑ι
<<<
ws_deque_1۰model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_1٠popｰspec t ι ws :
<<<
ws_deque_1۰inv t ι ∗
ws_deque_1۰owner t ws
| ∀∀ vs,
ws_deque_1۰model t vs
>>>
ws_deque_1٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_1۰model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_1۰model t vs'
end
| RET o;
ws_deque_1۰owner t ws'
>>>.
End ws_deque_1۰G.
#[global] Opaque ws_deque_1۰inv.
#[global] Opaque ws_deque_1۰model.
#[global] Opaque ws_deque_1۰owner.