Library zoo_parabs.waiter

From zoo Require Import
  prelude.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  condition
  mutex.
From zoo_saturn Require Import
  mpmc_queue_1.
From zoo_parabs Require Export
  base
  waiter__code.
From zoo_parabs Require Import
  base
  waiter__types.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types 𝑡 : location.
Implicit Types 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.

From zoo_parabs Require
  waiter__opaque.

#[global] Opaque waiter_inv.