Library zoo.iris.base_logic.lib.spsc_prop
From iris.base_logic Require Import
lib.invariants.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.base_logic Require Export
lib.base.
From zoo.iris.base_logic Require Import
lib.excl
lib.oneshot.
From zoo.iris Require Import
diaframe.
From zoo Require Import
options.
Class SpscPropG Σ `{inv_G : !invGS Σ} :=
{ #[local] spsc_prop_G_state_G :: OneshotG Σ () ()
; #[local] spsc_prop_G_consumer_G :: ExclG Σ unitO
}.
Definition spsc_prop_Σ :=
#[oneshot_Σ () ()
; excl_Σ unitO
].
#[global] Instance subG_spsc_prop_Σ Σ `{inv_G : !invGS Σ} :
subG spsc_prop_Σ Σ →
SpscPropG Σ.
Section spsc_prop_G.
Context `{spsc_prop_G : SpscPropG Σ}.
Implicit Types P : iProp Σ.
Record spsc_prop_name :=
{ spsc_prop_name_state : gname
; spsc_prop_name_consumer : gname
}.
Implicit Types γ : spsc_prop_name.
#[global] Instance spsc_prop_name_eq_dec : EqDecision spsc_prop_name :=
ltac:(solve_decision).
#[global] Instance spsc_prop_name_countable :
Countable spsc_prop_name.
#[local] Definition state_unset₁' γ_state :=
oneshot_pending γ_state (DfracOwn (2/3)) ().
#[local] Definition state_unset₁ γ :=
state_unset₁' γ.(spsc_prop_name_state).
#[local] Definition state_unset₂' γ_state :=
oneshot_pending γ_state (DfracOwn (1/3)) ().
#[local] Definition state_unset₂ γ :=
state_unset₂' γ.(spsc_prop_name_state).
#[local] Definition state_set' γ_state :=
oneshot_shot γ_state ().
#[local] Definition state_set γ :=
state_set' γ.(spsc_prop_name_state).
#[local] Definition consumer' γ_consumer :=
excl γ_consumer ().
#[local] Definition consumer γ :=
consumer' γ.(spsc_prop_name_consumer).
#[local] Definition inv_consumer γ P : iProp Σ :=
P ∨ consumer γ.
#[local] Instance : CustomIpat "inv_consumer" :=
" [ HP{_{!}} | >Hconsumer{_{!}} ] ".
#[local] Definition inv_inner γ P : iProp Σ :=
( state_unset₂ γ
) ∨ (
state_set γ ∗
inv_consumer γ P
).
#[local] Instance : CustomIpat "inv_inner" :=
" [ >Hstate_unset₂ | ( >Hstate_set{_{!}} & Hinv_consumer ) ] ".
Definition spsc_prop_inv γ ι P :=
inv ι (inv_inner γ P).
#[local] Instance : CustomIpat "inv" :=
" #Hinv ".
Definition spsc_prop_producer :=
state_unset₁.
#[local] Instance : CustomIpat "producer" :=
" Hstate_unset₁ ".
Definition spsc_prop_consumer :=
consumer.
#[local] Instance : CustomIpat "consumer" :=
" Hconsumer ".
Definition spsc_prop_resolved :=
state_set.
#[local] Instance : CustomIpat "resolved" :=
" #Hstate_set ".
#[global] Instance spsc_prop_inv_contractive γ ι :
Contractive (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_inv_ne γ ι :
NonExpansive (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_inv_proper γ ι :
Proper ((≡) ==> (≡)) (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_producer_timeless γ :
Timeless (spsc_prop_producer γ).
#[global] Instance spsc_prop_consumer_timeless γ :
Timeless (spsc_prop_consumer γ).
#[global] Instance spsc_prop_resolved_timeless γ :
Timeless (spsc_prop_resolved γ).
#[global] Instance spsc_prop_inv_persistent γ ι P :
Persistent (spsc_prop_inv γ ι P).
#[global] Instance spsc_prop_resolved_persistent γ :
Persistent (spsc_prop_resolved γ).
#[local] Lemma state_alloc :
⊢ |==>
∃ γ_state,
state_unset₁' γ_state ∗
state_unset₂' γ_state.
#[local] Lemma state_unset₁_exclusive γ :
state_unset₁ γ -∗
state_unset₁ γ -∗
False.
#[local] Lemma state_unset₁_set γ :
state_unset₁ γ -∗
state_set γ -∗
False.
#[local] Lemma state_unset₂_set γ :
state_unset₂ γ -∗
state_set γ -∗
False.
#[local] Lemma state_update γ :
state_unset₁ γ -∗
state_unset₂ γ ==∗
state_set γ.
#[local] Lemma consumer_alloc :
⊢ |==>
∃ γ_consumer,
consumer' γ_consumer.
#[local] Lemma consumer_exclusive γ :
consumer γ -∗
consumer γ -∗
False.
Lemma spsc_prop_alloc ι P E :
⊢ |={E}=>
∃ γ,
spsc_prop_inv γ ι P ∗
spsc_prop_producer γ ∗
spsc_prop_consumer γ.
Lemma spsc_prop_producer_exclusive γ :
spsc_prop_producer γ -∗
spsc_prop_producer γ -∗
False.
Lemma spcc_prop_producer_resolved γ :
spsc_prop_producer γ -∗
spsc_prop_resolved γ -∗
False.
Lemma spsc_prop_consumer_exclusive γ :
spsc_prop_consumer γ -∗
spsc_prop_consumer γ -∗
False.
Lemma spsc_prop_produce γ ι P E :
↑ι ⊆ E →
spsc_prop_inv γ ι P -∗
spsc_prop_producer γ -∗
▷ P ={E}=∗
spsc_prop_resolved γ.
Lemma spsc_prop_consume γ ι P E :
↑ι ⊆ E →
spsc_prop_inv γ ι P -∗
spsc_prop_consumer γ -∗
spsc_prop_resolved γ ={E}=∗
▷ P.
End spsc_prop_G.
#[global] Opaque spsc_prop_inv.
#[global] Opaque spsc_prop_producer.
#[global] Opaque spsc_prop_consumer.
#[global] Opaque spsc_prop_resolved.
lib.invariants.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.base_logic Require Export
lib.base.
From zoo.iris.base_logic Require Import
lib.excl
lib.oneshot.
From zoo.iris Require Import
diaframe.
From zoo Require Import
options.
Class SpscPropG Σ `{inv_G : !invGS Σ} :=
{ #[local] spsc_prop_G_state_G :: OneshotG Σ () ()
; #[local] spsc_prop_G_consumer_G :: ExclG Σ unitO
}.
Definition spsc_prop_Σ :=
#[oneshot_Σ () ()
; excl_Σ unitO
].
#[global] Instance subG_spsc_prop_Σ Σ `{inv_G : !invGS Σ} :
subG spsc_prop_Σ Σ →
SpscPropG Σ.
Section spsc_prop_G.
Context `{spsc_prop_G : SpscPropG Σ}.
Implicit Types P : iProp Σ.
Record spsc_prop_name :=
{ spsc_prop_name_state : gname
; spsc_prop_name_consumer : gname
}.
Implicit Types γ : spsc_prop_name.
#[global] Instance spsc_prop_name_eq_dec : EqDecision spsc_prop_name :=
ltac:(solve_decision).
#[global] Instance spsc_prop_name_countable :
Countable spsc_prop_name.
#[local] Definition state_unset₁' γ_state :=
oneshot_pending γ_state (DfracOwn (2/3)) ().
#[local] Definition state_unset₁ γ :=
state_unset₁' γ.(spsc_prop_name_state).
#[local] Definition state_unset₂' γ_state :=
oneshot_pending γ_state (DfracOwn (1/3)) ().
#[local] Definition state_unset₂ γ :=
state_unset₂' γ.(spsc_prop_name_state).
#[local] Definition state_set' γ_state :=
oneshot_shot γ_state ().
#[local] Definition state_set γ :=
state_set' γ.(spsc_prop_name_state).
#[local] Definition consumer' γ_consumer :=
excl γ_consumer ().
#[local] Definition consumer γ :=
consumer' γ.(spsc_prop_name_consumer).
#[local] Definition inv_consumer γ P : iProp Σ :=
P ∨ consumer γ.
#[local] Instance : CustomIpat "inv_consumer" :=
" [ HP{_{!}} | >Hconsumer{_{!}} ] ".
#[local] Definition inv_inner γ P : iProp Σ :=
( state_unset₂ γ
) ∨ (
state_set γ ∗
inv_consumer γ P
).
#[local] Instance : CustomIpat "inv_inner" :=
" [ >Hstate_unset₂ | ( >Hstate_set{_{!}} & Hinv_consumer ) ] ".
Definition spsc_prop_inv γ ι P :=
inv ι (inv_inner γ P).
#[local] Instance : CustomIpat "inv" :=
" #Hinv ".
Definition spsc_prop_producer :=
state_unset₁.
#[local] Instance : CustomIpat "producer" :=
" Hstate_unset₁ ".
Definition spsc_prop_consumer :=
consumer.
#[local] Instance : CustomIpat "consumer" :=
" Hconsumer ".
Definition spsc_prop_resolved :=
state_set.
#[local] Instance : CustomIpat "resolved" :=
" #Hstate_set ".
#[global] Instance spsc_prop_inv_contractive γ ι :
Contractive (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_inv_ne γ ι :
NonExpansive (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_inv_proper γ ι :
Proper ((≡) ==> (≡)) (spsc_prop_inv γ ι).
#[global] Instance spsc_prop_producer_timeless γ :
Timeless (spsc_prop_producer γ).
#[global] Instance spsc_prop_consumer_timeless γ :
Timeless (spsc_prop_consumer γ).
#[global] Instance spsc_prop_resolved_timeless γ :
Timeless (spsc_prop_resolved γ).
#[global] Instance spsc_prop_inv_persistent γ ι P :
Persistent (spsc_prop_inv γ ι P).
#[global] Instance spsc_prop_resolved_persistent γ :
Persistent (spsc_prop_resolved γ).
#[local] Lemma state_alloc :
⊢ |==>
∃ γ_state,
state_unset₁' γ_state ∗
state_unset₂' γ_state.
#[local] Lemma state_unset₁_exclusive γ :
state_unset₁ γ -∗
state_unset₁ γ -∗
False.
#[local] Lemma state_unset₁_set γ :
state_unset₁ γ -∗
state_set γ -∗
False.
#[local] Lemma state_unset₂_set γ :
state_unset₂ γ -∗
state_set γ -∗
False.
#[local] Lemma state_update γ :
state_unset₁ γ -∗
state_unset₂ γ ==∗
state_set γ.
#[local] Lemma consumer_alloc :
⊢ |==>
∃ γ_consumer,
consumer' γ_consumer.
#[local] Lemma consumer_exclusive γ :
consumer γ -∗
consumer γ -∗
False.
Lemma spsc_prop_alloc ι P E :
⊢ |={E}=>
∃ γ,
spsc_prop_inv γ ι P ∗
spsc_prop_producer γ ∗
spsc_prop_consumer γ.
Lemma spsc_prop_producer_exclusive γ :
spsc_prop_producer γ -∗
spsc_prop_producer γ -∗
False.
Lemma spcc_prop_producer_resolved γ :
spsc_prop_producer γ -∗
spsc_prop_resolved γ -∗
False.
Lemma spsc_prop_consumer_exclusive γ :
spsc_prop_consumer γ -∗
spsc_prop_consumer γ -∗
False.
Lemma spsc_prop_produce γ ι P E :
↑ι ⊆ E →
spsc_prop_inv γ ι P -∗
spsc_prop_producer γ -∗
▷ P ={E}=∗
spsc_prop_resolved γ.
Lemma spsc_prop_consume γ ι P E :
↑ι ⊆ E →
spsc_prop_inv γ ι P -∗
spsc_prop_consumer γ -∗
spsc_prop_resolved γ ={E}=∗
▷ P.
End spsc_prop_G.
#[global] Opaque spsc_prop_inv.
#[global] Opaque spsc_prop_producer.
#[global] Opaque spsc_prop_consumer.
#[global] Opaque spsc_prop_resolved.