Library zoo_std.mpsc_waiter

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.base_logic Require Import
  lib.oneshot
  lib.excl.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  mpsc_waiter__code.
From zoo_std Require Import
  condition
  mpsc_waiter__types.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types 𝑡 : location.

Class MpscWaiterG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] mpsc_waiter_G_mutex_G :: MutexG Σ
  ; #[local] mpsc_waiter_G_lstate_G :: OneshotG Σ unit unit
  ; #[local] mpsc_waiter_G_consumer_G :: ExclG Σ unitO
  }.

Definition mpsc_waiter_Σ :=
  #[mutex_Σ
  ; oneshot_Σ unit unit
  ; excl_Σ unitO
  ].
#[global] Instance subG_mpsc_waiter_Σ Σ `{zoo_G : !ZooG Σ} :
  subG mpsc_waiter_Σ Σ →
  MpscWaiterG Σ .

Section mpsc_waiter_G.
  Context `{mpsc_waiter_G : MpscWaiterG Σ}.

  Record metadata :=
    { metadata_mutex : val
    ; metadata_condition : val
    ; metadata_lstate : gname
    ; metadata_consumer : gname
    }.
  Implicit Types γ : 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) ().
  Definition mpsc_waiter_inv t P : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    𝑡.[mutex] ↦□ γ.(metadata_mutex) ∗
    mutex_inv γ.(metadata_mutex) True ∗
    𝑡.[condition] ↦□ γ.(metadata_condition) ∗
    condition_inv γ.(metadata_condition) ∗
    inv nroot (inv_inner 𝑡 γ P).

  Definition mpsc_waiter_consumer t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    excl γ.(metadata_consumer) ().

  Definition mpsc_waiter_notified t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    oneshot_shot γ.(metadata_lstate) ().

  #[global] Instance mpsc_waiter_inv_contractive t :
    Contractive (mpsc_waiter_inv t).
  #[global] Instance mpsc_waiter_inv_ne t :
    NonExpansive (mpsc_waiter_inv t).
  #[global] Instance mpsc_waiter_inv_proper t :
    Proper ((≡) ==> (≡)) (mpsc_waiter_inv t).

  #[global] Instance mpsc_waiter_consumer_timeless t :
    Timeless (mpsc_waiter_consumer t).
  #[global] Instance mpsc_waiter_notified_timeless t :
    Timeless (mpsc_waiter_notified t).

  #[global] Instance mpsc_waiter_inv_persistent t P :
    Persistent (mpsc_waiter_inv t P).
  #[global] Instance mpsc_waiter_notified_persistent t :
    Persistent (mpsc_waiter_notified t).

  Lemma mpsc_waiter_consumer_exclusive t :
    mpsc_waiter_consumer t -∗
    mpsc_waiter_consumer t -∗
    False.

  Lemma mpsc_waiter٠create𑁒spec P :
    {{{
      True
    }}}
      mpsc_waiter٠create ()
    {{{
      t
    , RET t;
      mpsc_waiter_inv t P ∗
      mpsc_waiter_consumer t
    }}}.

  Lemma mpsc_waiter٠notify𑁒spec t P :
    {{{
      mpsc_waiter_inv t P ∗
      P
    }}}
      mpsc_waiter٠notify t
    {{{
      b
    , RET #b;
      mpsc_waiter_notified t
    }}}.

  Lemma mpsc_waiter٠try_wait𑁒spec t P :
    {{{
      mpsc_waiter_inv t P ∗
      mpsc_waiter_consumer t
    }}}
      mpsc_waiter٠try_wait t
    {{{
      b
    , RET #b;
      if b then
        P
      else
        mpsc_waiter_consumer t
    }}}.
  Lemma mpsc_waiter٠try_wait𑁒spec_notified t P :
    {{{
      mpsc_waiter_inv t P ∗
      mpsc_waiter_consumer t ∗
      mpsc_waiter_notified t
    }}}
      mpsc_waiter٠try_wait t
    {{{
      RET true;
      P
    }}}.

  Lemma mpsc_waiter٠wait𑁒spec t P :
    {{{
      mpsc_waiter_inv t P ∗
      mpsc_waiter_consumer t
    }}}
      mpsc_waiter٠wait t
    {{{
      RET ();
      P
    }}}.
End mpsc_waiter_G.

From zoo_std Require
  mpsc_waiter__opaque.

#[global] Opaque mpsc_waiter_inv.
#[global] Opaque mpsc_waiter_consumer.
#[global] Opaque mpsc_waiter_notified.