Library zoo_std.waiter_spsc

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.base.
Require Export zoo_std.waiter_spsc__code.
Require Import zoo_std.waiter_spsc__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type 𝑡 : location.

Class WaiterSpscG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] waiter_spsc ۰ G ۰ mutex ۰ G :: MutexG Σ
  ; #[local] waiter_spsc ۰ G ۰ lstate ۰ G :: OneshotG Σ unit unit
  ; #[local] waiter_spsc ۰ G ۰ excl ۰ G :: ExclG Σ unitO
  }.

Definition waiter_spsc ۰ Σ :=
  #[mutex ۰ Σ
  ; oneshot ۰ Σ unit unit
  ; excl ۰ Σ unitO
  ].
#[global] Instance subG ｰ waiter_spsc ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG waiter_spsc ۰ Σ Σ →
  WaiterSpscG Σ .

Section waiter_spsc ۰ G.
  Context `{waiter_spsc ۰ G : WaiterSpscG Σ}.

  Record metadata :=
    { metadata ۰ mutex : val
    ; metadata ۰ condition : val
    ; metadata ۰ lstate : gname
    ; metadata ۰ consumer : gname
    }.
  Implicit Type γ : metadata.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

  #[local] Definition inv ۰ inner 𝑡 γ P : iProp Σ :=
    ∃ b ,
    𝑡 .[flag ] ↦ #b ∗
    if b then
      oneshot ۰ shot γ.(metadata ۰ lstate) () ∗
      (P ∨ excl γ.(metadata ۰ consumer) ())
    else
      oneshot ۰ pending γ.(metadata ۰ lstate) (DfracOwn (1/3)) ().
  Definition waiter_spsc ۰ inv t P : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    𝑡 .[mutex ] ↦□ γ.(metadata ۰ mutex) ∗
    mutex ۰ inv γ.(metadata ۰ mutex) True ∗
    𝑡 .[condition ] ↦□ γ.(metadata ۰ condition) ∗
    condition ۰ inv γ.(metadata ۰ condition) ∗
    inv nroot (inv ۰ inner 𝑡 γ P).

  Definition waiter_spsc ۰ producer t : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    oneshot ۰ pending γ.(metadata ۰ lstate) (DfracOwn (2/3)) ().

  Definition waiter_spsc ۰ consumer t : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    excl γ.(metadata ۰ consumer) ().

  Definition waiter_spsc ۰ notified t : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    oneshot ۰ shot γ.(metadata ۰ lstate) ().

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

  #[global] Instance waiter_spsc ۰ producer ｰ timeless t :
    Timeless (waiter_spsc ۰ producer t).
  #[global] Instance waiter_spsc ۰ consumer ｰ timeless t :
    Timeless (waiter_spsc ۰ consumer t).
  #[global] Instance waiter_spsc ۰ notified ｰ timeless t :
    Timeless (waiter_spsc ۰ notified t).

  #[global] Instance waiter_spsc ۰ inv ｰ persistent t P :
    Persistent (waiter_spsc ۰ inv t P).
  #[global] Instance waiter_spsc ۰ notified ｰ persistent t :
    Persistent (waiter_spsc ۰ notified t).

  Lemma waiter_spsc ۰ producer ｰ exclusive t :
    waiter_spsc ۰ producer t -∗
    waiter_spsc ۰ producer t -∗
    False.

  Lemma waiter_spsc ۰ consumer ｰ exclusive t :
    waiter_spsc ۰ consumer t -∗
    waiter_spsc ۰ consumer t -∗
    False.

  Lemma waiter_spsc ٠ create ｰ spec P :
    {{{
      True
    }}}
      waiter_spsc ٠ create ()
    {{{
      t
    , RET t ;
      waiter_spsc ۰ inv t P ∗
      waiter_spsc ۰ producer t ∗
      waiter_spsc ۰ consumer t
    }}}.

  Lemma waiter_spsc ٠ notify ｰ spec t P :
    {{{
      waiter_spsc ۰ inv t P ∗
      waiter_spsc ۰ producer t ∗
      P
    }}}
      waiter_spsc ٠ notify t
    {{{
      RET ();
      waiter_spsc ۰ notified t
    }}}.

  Lemma waiter_spsc ٠ try_wait ｰ spec t P :
    {{{
      waiter_spsc ۰ inv t P ∗
      waiter_spsc ۰ consumer t
    }}}
      waiter_spsc ٠ try_wait t
    {{{
      b
    , RET #b ;
      if b then
        P
      else
        waiter_spsc ۰ consumer t
    }}}.
  Lemma waiter_spsc ٠ try_wait ｰ spec ｰ notified t P :
    {{{
      waiter_spsc ۰ inv t P ∗
      waiter_spsc ۰ consumer t ∗
      waiter_spsc ۰ notified t
    }}}
      waiter_spsc ٠ try_wait t
    {{{
      RET true ;
      P
    }}}.

  Lemma waiter_spsc ٠ wait ｰ spec t P :
    {{{
      waiter_spsc ۰ inv t P ∗
      waiter_spsc ۰ consumer t
    }}}
      waiter_spsc ٠ wait t
    {{{
      RET ();
      P
    }}}.
End waiter_spsc ۰ G.

Require zoo_std.waiter_spsc__opaque.

#[global] Opaque waiter_spsc ۰ inv.
#[global] Opaque waiter_spsc ۰ producer.
#[global] Opaque waiter_spsc ۰ consumer.
#[global] Opaque waiter_spsc ۰ notified.