Library zoo_std.spsc_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
  spsc_waiter__code.
From zoo_std Require Import
  condition
  spsc_waiter__types.
From zoo Require Import
  options.

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

Class SpscWaiterG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] spsc_waiter_G_mutex_G :: MutexG Σ
  ; #[local] spsc_waiter_G_lstate_G :: OneshotG Σ unit unit
  ; #[local] spsc_waiter_G_excl_G :: ExclG Σ unitO
  }.

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

Section spsc_waiter_G.
  Context `{spsc_waiter_G : SpscWaiterG Σ}.

  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/3)) ().
  Definition spsc_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 spsc_waiter_producer t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    oneshot_pending γ.(metadata_lstate) (DfracOwn (2/3)) ().

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

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

  #[global] Instance spsc_waiter_inv_contractive t :
    Contractive (spsc_waiter_inv t).
  #[global] Instance spsc_waiter_inv_ne t :
    NonExpansive (spsc_waiter_inv t).
  #[global] Instance spsc_waiter_inv_proper t :
    Proper ((≡) ==> (≡)) (spsc_waiter_inv t).

  #[global] Instance spsc_waiter_producer_timeless t :
    Timeless (spsc_waiter_producer t).
  #[global] Instance spsc_waiter_consumer_timeless t :
    Timeless (spsc_waiter_consumer t).
  #[global] Instance spsc_waiter_notified_timeless t :
    Timeless (spsc_waiter_notified t).

  #[global] Instance spsc_waiter_inv_persistent t P :
    Persistent (spsc_waiter_inv t P).
  #[global] Instance spsc_waiter_notified_persistent t :
    Persistent (spsc_waiter_notified t).

  Lemma spsc_waiter_producer_exclusive t :
    spsc_waiter_producer t -∗
    spsc_waiter_producer t -∗
    False.

  Lemma spsc_waiter_consumer_exclusive t :
    spsc_waiter_consumer t -∗
    spsc_waiter_consumer t -∗
    False.

  Lemma spsc_waiter٠create𑁒spec P :
    {{{
      True
    }}}
      spsc_waiter٠create ()
    {{{
      t
    , RET t;
      spsc_waiter_inv t P ∗
      spsc_waiter_producer t ∗
      spsc_waiter_consumer t
    }}}.

  Lemma spsc_waiter٠notify𑁒spec t P :
    {{{
      spsc_waiter_inv t P ∗
      spsc_waiter_producer t ∗
      P
    }}}
      spsc_waiter٠notify t
    {{{
      RET ();
      spsc_waiter_notified t
    }}}.

  Lemma spsc_waiter٠try_wait𑁒spec t P :
    {{{
      spsc_waiter_inv t P ∗
      spsc_waiter_consumer t
    }}}
      spsc_waiter٠try_wait t
    {{{
      b
    , RET #b;
      if b then
        P
      else
        spsc_waiter_consumer t
    }}}.
  Lemma spsc_waiter٠try_wait𑁒spec_notified t P :
    {{{
      spsc_waiter_inv t P ∗
      spsc_waiter_consumer t ∗
      spsc_waiter_notified t
    }}}
      spsc_waiter٠try_wait t
    {{{
      RET true;
      P
    }}}.

  Lemma spsc_waiter٠wait𑁒spec t P :
    {{{
      spsc_waiter_inv t P ∗
      spsc_waiter_consumer t
    }}}
      spsc_waiter٠wait t
    {{{
      RET ();
      P
    }}}.
End spsc_waiter_G.

From zoo_std Require
  spsc_waiter__opaque.

#[global] Opaque spsc_waiter_inv.
#[global] Opaque spsc_waiter_producer.
#[global] Opaque spsc_waiter_consumer.
#[global] Opaque spsc_waiter_notified.