Library zoo.iris.base_logic.lib.prop_spsc

Require Import iris.base_logic.lib.invariants.

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Export zoo.iris.base_logic.lib.base.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.iris.diaframe.
Require Import zoo.options.

Class PropSpscG Σ `{inv ۰ G : !invGS Σ} :=
  { #[local] prop_spsc ۰ G ۰ state ۰ G :: OneshotG Σ () ()
  ; #[local] prop_spsc ۰ G ۰ consumer ۰ G :: ExclG Σ unitO
  }.

Definition prop_spsc ۰ Σ :=
  #[oneshot ۰ Σ () ()
  ; excl ۰ Σ unitO
  ].
#[global] Instance subG ｰ prop_spsc ۰ Σ Σ `{inv ۰ G : !invGS Σ} :
  subG prop_spsc ۰ Σ Σ →
  PropSpscG Σ.

Section prop_spsc ۰ G.
  Context `{prop_spsc ۰ G : PropSpscG Σ}.

  Implicit Type P : iProp Σ.

  Record prop_spsc ۰ name :=
    { prop_spsc ۰ name ۰ state : gname
    ; prop_spsc ۰ name ۰ consumer : gname
    }.
  Implicit Type γ : prop_spsc ۰ name.

  #[global] Instance prop_spsc ۰ name ｰ eq_dec : EqDecision prop_spsc ۰ name :=
    ltac:(solve_decision).
  #[global] Instance prop_spsc ۰ name ｰ countable :
    Countable prop_spsc ۰ name.

  #[local] Definition state ۰ unset₁' γ_state :=
    oneshot ۰ pending γ_state (DfracOwn (2/3)) ().
  #[local] Definition state ۰ unset₁ γ :=
    state ۰ unset₁' γ.(prop_spsc ۰ name ۰ state).
  #[local] Definition state ۰ unset₂' γ_state :=
    oneshot ۰ pending γ_state (DfracOwn (1/3)) ().
  #[local] Definition state ۰ unset₂ γ :=
    state ۰ unset₂' γ.(prop_spsc ۰ name ۰ state).
  #[local] Definition state ۰ set' γ_state :=
    oneshot ۰ shot γ_state ().
  #[local] Definition state ۰ set γ :=
    state ۰ set' γ.(prop_spsc ۰ name ۰ state).

  #[local] Definition consumer' γ_consumer :=
    excl γ_consumer ().
  #[local] Definition consumer γ :=
    consumer' γ.(prop_spsc ۰ 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 prop_spsc ۰ inv γ ι P :=
    inv ι (inv ۰ inner γ P).
  #[local] Instance : CustomIpat "inv" :=
    " #Hinv ".

  Definition prop_spsc ۰ producer :=
    state ۰ unset₁.
  #[local] Instance : CustomIpat "producer" :=
    " Hstate_unset₁ ".

  Definition prop_spsc ۰ consumer :=
    consumer.
  #[local] Instance : CustomIpat "consumer" :=
    " Hconsumer ".

  Definition prop_spsc ۰ resolved :=
    state ۰ set.
  #[local] Instance : CustomIpat "resolved" :=
    " #Hstate_set ".

  #[global] Instance prop_spsc ۰ inv ｰ contractive γ ι :
    Contractive (prop_spsc ۰ inv γ ι).
  #[global] Instance prop_spsc ۰ inv ｰ ne γ ι :
    NonExpansive (prop_spsc ۰ inv γ ι).
  #[global] Instance prop_spsc ۰ inv ｰ proper γ ι :
    Proper ((≡) ==> (≡)) (prop_spsc ۰ inv γ ι).

  #[global] Instance prop_spsc ۰ producer ｰ timeless γ :
    Timeless (prop_spsc ۰ producer γ).
  #[global] Instance prop_spsc ۰ consumer ｰ timeless γ :
    Timeless (prop_spsc ۰ consumer γ).
  #[global] Instance prop_spsc ۰ resolved ｰ timeless γ :
    Timeless (prop_spsc ۰ resolved γ).

  #[global] Instance prop_spsc ۰ inv ｰ persistent γ ι P :
    Persistent (prop_spsc ۰ inv γ ι P).
  #[global] Instance prop_spsc ۰ resolved ｰ persistent γ :
    Persistent (prop_spsc ۰ 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 prop_spsc ｰ alloc ι P E :
    ⊢ |={E }=>
      ∃ γ ,
      prop_spsc ۰ inv γ ι P ∗
      prop_spsc ۰ producer γ ∗
      prop_spsc ۰ consumer γ.

  Lemma prop_spsc ۰ producer ｰ exclusive γ :
    prop_spsc ۰ producer γ -∗
    prop_spsc ۰ producer γ -∗
    False.
  Lemma spcc_prop ۰ producer ｰ resolved γ :
    prop_spsc ۰ producer γ -∗
    prop_spsc ۰ resolved γ -∗
    False.

  Lemma prop_spsc ۰ consumer ｰ exclusive γ :
    prop_spsc ۰ consumer γ -∗
    prop_spsc ۰ consumer γ -∗
    False.

  Lemma prop_spsc ｰ produce γ ι P E :
    ↑ι ⊆ E →
    prop_spsc ۰ inv γ ι P -∗
    prop_spsc ۰ producer γ -∗
    ▷ P ={E }=∗
    prop_spsc ۰ resolved γ.
  Lemma prop_spsc ｰ consume γ ι P E :
    ↑ι ⊆ E →
    prop_spsc ۰ inv γ ι P -∗
    prop_spsc ۰ consumer γ -∗
    prop_spsc ۰ resolved γ ={E }=∗
    ▷ P.
End prop_spsc ۰ G.

#[global] Opaque prop_spsc ۰ inv.
#[global] Opaque prop_spsc ۰ producer.
#[global] Opaque prop_spsc ۰ consumer.
#[global] Opaque prop_spsc ۰ resolved.