Library zoo_std.waiter_mpsc

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_mpsc__code.
Require Import zoo_std.waiter_mpsc__types.
Require Import zoo.options.

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

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

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

Section waiter_mpsc ۰ G.
  Context `{waiter_mpsc ۰ G : WaiterMpscG Σ}.

  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) ().
  Definition waiter_mpsc ۰ 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_mpsc ۰ consumer t : iProp Σ :=
    ∃ 𝑡 γ ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 ↪ γ ∗
    excl γ.(metadata ۰ consumer) ().

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

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

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

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

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

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

  Lemma waiter_mpsc ٠ notify ｰ spec t P :
    {{{
      waiter_mpsc ۰ inv t P ∗
      P
    }}}
      waiter_mpsc ٠ notify t
    {{{
      b
    , RET #b ;
      waiter_mpsc ۰ notified t
    }}}.

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

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

Require zoo_std.waiter_mpsc__opaque.

#[global] Opaque waiter_mpsc ۰ inv.
#[global] Opaque waiter_mpsc ۰ consumer.
#[global] Opaque waiter_mpsc ۰ notified.