Library zoo_parabs.waiter

Require Import zoo.prelude.
Require Import zoo.base.
Require Export zoo_parabs.base.
Require Export zoo_parabs.waiter__code.
Require Import zoo_parabs.waiter__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type 𝑡 : location.
Implicit Type v t mtx cond : val.

Class WaiterG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] waiter ۰ G ۰ mutex ۰ G :: MutexG Σ
  }.

Definition waiter ۰ Σ :=
  #[mutex ۰ Σ
  ].
#[global] Instance subG ｰ ws_hub_Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG waiter ۰ Σ Σ →
  WaiterG Σ.

Section waiter ۰ G.
  Context `{waiter ۰ G : WaiterG Σ}.

  #[local] Definition inv ۰ inner 𝑡 : iProp Σ :=
    ∃ b ,
    𝑡 .[flag ] ↦ #b.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %b & H𝑡_flag ) ".
  Definition waiter ۰ inv t : iProp Σ :=
    ∃ 𝑡 mtx cond ,
    ⌜t = #𝑡 ⌝ ∗
    𝑡 .[mutex ] ↦□ mtx ∗
    mutex ۰ inv mtx (inv ۰ inner 𝑡) ∗
    𝑡 .[condition ] ↦□ cond ∗
    condition ۰ inv cond.
  #[local] Instance : CustomIpat "inv" :=
    " ( %𝑡 & %mtx & %cond & -> & #H𝑡_mutex & #Hmtx_inv & #H𝑡_condition & #Hcond_inv ) ".

  #[global] Instance waiter ۰ inv ｰ persistent t :
    Persistent (waiter ۰ inv t).

  Lemma waiter ٠ create ｰ spec :
    {{{
      True
    }}}
      waiter ٠ create ()
    {{{
      t
    , RET t ;
      waiter ۰ inv t
    }}}.

  Lemma waiter ٠ notify ｰ spec t :
    {{{
      waiter ۰ inv t
    }}}
      waiter ٠ notify t
    {{{
      b
    , RET #b ;
      True
    }}}.

  Lemma waiter ٠ prepare_wait ｰ spec t :
    {{{
      waiter ۰ inv t
    }}}
      waiter ٠ prepare_wait t
    {{{
      RET ();
      True
    }}}.

  Lemma waiter ٠ cancel_wait ｰ spec t :
    {{{
      waiter ۰ inv t
    }}}
      waiter ٠ cancel_wait t
    {{{
      b
    , RET #b ;
      True
    }}}.

  Lemma waiter ٠ commit_wait ｰ spec t :
    {{{
      waiter ۰ inv t
    }}}
      waiter ٠ commit_wait t
    {{{
      RET ();
      True
    }}}.
End waiter ۰ G.

Require zoo_parabs.waiter__opaque.

#[global] Opaque waiter ۰ inv.